fof(l31_vectsp_1,theorem,(
    ! [A] : 
      ( ( ~ v3_struct_0(A)
        & l3_vectsp_1(A) )
     => ( v7_vectsp_1(A)
       => ( v4_vectsp_1(A)
          & v5_vectsp_1(A) ) ) ) ),
    inference(mizar_proof,[status(thm)],[d18_vectsp_1,d11_vectsp_1,d18_vectsp_1,d12_vectsp_1]),
    [file(vectsp_1,l31_vectsp_1),interesting(1.00)]).

fof(t42_vectsp_1,theorem,(
    ! [A] : 
      ( ( ~ v3_struct_0(A)
        & v4_rlvect_1(A)
        & v5_rlvect_1(A)
        & v6_rlvect_1(A)
        & v7_vectsp_1(A)
        & l3_vectsp_1(A) )
     => ! [B] : 
          ( m1_subset_1(B,u1_struct_0(A))
         => ! [C] : 
              ( m1_subset_1(C,u1_struct_0(A))
             => k1_group_1(A,k5_rlvect_1(A,B),k5_rlvect_1(A,C)) = k1_group_1(A,B,C) ) ) ) ),
    inference(mizar_proof,[status(thm)],[t41_vectsp_1,t40_vectsp_1,t30_rlvect_1]),
    [file(vectsp_1,t42_vectsp_1),interesting(0.97)]).

fof(l30_vectsp_1,theorem,(
    k2_group_1(k3_vectsp_1) = 1 ),
    inference(mizar_proof,[status(thm)],[l29_vectsp_1,d5_group_1]),
    [file(vectsp_1,l30_vectsp_1),interesting(0.95)]).

fof(t69_vectsp_1,theorem,(
    ! [A] : 
      ( ( ~ v3_struct_0(A)
        & v3_rlvect_1(A)
        & v4_rlvect_1(A)
        & v5_rlvect_1(A)
        & v6_rlvect_1(A)
        & v4_group_1(A)
        & v6_vectsp_1(A)
        & v7_vectsp_1(A)
        & v8_vectsp_1(A)
        & l3_vectsp_1(A) )
     => ! [B] : 
          ( ( ~ v3_struct_0(B)
            & v4_rlvect_1(B)
            & v5_rlvect_1(B)
            & v6_rlvect_1(B)
            & v12_vectsp_1(B,A)
            & l4_vectsp_1(B,A) )
         => ! [C] : 
              ( m1_subset_1(C,u1_struct_0(A))
             => ! [D] : 
                  ( m1_subset_1(D,u1_struct_0(B))
                 => k6_vectsp_1(A,B,C,k5_rlvect_1(B,D)) = k5_rlvect_1(B,k6_vectsp_1(A,B,C,D)) ) ) ) ) ),
    inference(mizar_proof,[status(thm)],[t59_vectsp_1,d26_vectsp_1,t40_vectsp_1,d13_vectsp_1,t68_vectsp_1]),
    [file(vectsp_1,t69_vectsp_1),interesting(0.94)]).

fof(t20_vectsp_1,theorem,(
    k2_group_1(k3_vectsp_1) = 1 ),
    inference(mizar_proof,[status(thm)],[l30_vectsp_1]),
    [file(vectsp_1,t20_vectsp_1),interesting(0.91)]).

fof(t70_vectsp_1,theorem,(
    ! [A] : 
      ( ( ~ v3_struct_0(A)
        & v3_rlvect_1(A)
        & v4_rlvect_1(A)
        & v5_rlvect_1(A)
        & v6_rlvect_1(A)
        & v4_group_1(A)
        & v6_vectsp_1(A)
        & v7_vectsp_1(A)
        & v8_vectsp_1(A)
        & l3_vectsp_1(A) )
     => ! [B] : 
          ( ( ~ v3_struct_0(B)
            & v4_rlvect_1(B)
            & v5_rlvect_1(B)
            & v6_rlvect_1(B)
            & v12_vectsp_1(B,A)
            & l4_vectsp_1(B,A) )
         => ! [C] : 
              ( m1_subset_1(C,u1_struct_0(A))
             => ! [D] : 
                  ( m1_subset_1(D,u1_struct_0(B))
                 => ! [E] : 
                      ( m1_subset_1(E,u1_struct_0(B))
                     => k6_vectsp_1(A,B,C,k6_rlvect_1(B,D,E)) = k6_rlvect_1(B,k6_vectsp_1(A,B,C,D),k6_vectsp_1(A,B,C,E)) ) ) ) ) ) ),
    inference(mizar_proof,[status(thm)],[d26_vectsp_1,t69_vectsp_1]),
    [file(vectsp_1,t70_vectsp_1),interesting(0.86)]).

fof(t36_vectsp_1,theorem,(
    ! [A] : 
      ( ( ~ v3_struct_0(A)
        & v4_rlvect_1(A)
        & v5_rlvect_1(A)
        & v6_rlvect_1(A)
        & v4_vectsp_1(A)
        & l3_vectsp_1(A) )
     => ! [B] : 
          ( m1_subset_1(B,u1_struct_0(A))
         => k1_group_1(A,B,k1_rlvect_1(A)) = k1_rlvect_1(A) ) ) ),
    inference(mizar_proof,[status(thm)],[t10_rlvect_1,t10_rlvect_1,d11_vectsp_1,t21_rlvect_1]),
    [file(vectsp_1,t36_vectsp_1),interesting(0.85)]).

fof(t39_vectsp_1,theorem,(
    ! [A] : 
      ( ( ~ v3_struct_0(A)
        & v4_rlvect_1(A)
        & v5_rlvect_1(A)
        & v6_rlvect_1(A)
        & v5_vectsp_1(A)
        & l3_vectsp_1(A) )
     => ! [B] : 
          ( m1_subset_1(B,u1_struct_0(A))
         => k1_group_1(A,k1_rlvect_1(A),B) = k1_rlvect_1(A) ) ) ),
    inference(mizar_proof,[status(thm)],[t10_rlvect_1,t10_rlvect_1,d12_vectsp_1,t21_rlvect_1]),
    [file(vectsp_1,t39_vectsp_1),interesting(0.85)]).

fof(t78_vectsp_1,theorem,(
    k4_rlvect_1(k3_vectsp_1,k2_group_1(k3_vectsp_1),k2_group_1(k3_vectsp_1)) != k1_rlvect_1(k3_vectsp_1) ),
    inference(mizar_proof,[status(thm)],[l30_vectsp_1,t5_rlvect_1,d9_binop_2]),
    [file(vectsp_1,t78_vectsp_1),interesting(0.85)]).

fof(t40_vectsp_1,theorem,(
    ! [A] : 
      ( ( ~ v3_struct_0(A)
        & v4_rlvect_1(A)
        & v5_rlvect_1(A)
        & v6_rlvect_1(A)
        & v4_vectsp_1(A)
        & l3_vectsp_1(A) )
     => ! [B] : 
          ( m1_subset_1(B,u1_struct_0(A))
         => ! [C] : 
              ( m1_subset_1(C,u1_struct_0(A))
             => k1_group_1(A,B,k5_rlvect_1(A,C)) = k5_rlvect_1(A,k1_group_1(A,B,C)) ) ) ) ),
    inference(mizar_proof,[status(thm)],[d11_vectsp_1,d10_rlvect_1,t36_vectsp_1,d10_rlvect_1]),
    [file(vectsp_1,t40_vectsp_1),interesting(0.83)]).

fof(t41_vectsp_1,theorem,(
    ! [A] : 
      ( ( ~ v3_struct_0(A)
        & v4_rlvect_1(A)
        & v5_rlvect_1(A)
        & v6_rlvect_1(A)
        & v5_vectsp_1(A)
        & l3_vectsp_1(A) )
     => ! [B] : 
          ( m1_subset_1(B,u1_struct_0(A))
         => ! [C] : 
              ( m1_subset_1(C,u1_struct_0(A))
             => k1_group_1(A,k5_rlvect_1(A,B),C) = k5_rlvect_1(A,k1_group_1(A,B,C)) ) ) ) ),
    inference(mizar_proof,[status(thm)],[d12_vectsp_1,d10_rlvect_1,t39_vectsp_1,d10_rlvect_1]),
    [file(vectsp_1,t41_vectsp_1),interesting(0.83)]).

fof(l29_vectsp_1,theorem,(
    ! [A] : 
      ( m1_subset_1(A,u1_struct_0(k3_vectsp_1))
     => ! [B] : 
          ( m1_subset_1(B,u1_struct_0(k3_vectsp_1))
         => ( B = 1
           => ( k1_group_1(k3_vectsp_1,A,B) = A
              & k1_group_1(k3_vectsp_1,B,A) = A ) ) ) ) ),
    inference(mizar_proof,[status(thm)],[d11_binop_2,d11_binop_2]),
    [file(vectsp_1,l29_vectsp_1),interesting(0.81)]).

fof(t84_vectsp_1,theorem,(
    ! [A] : 
      ( ( ~ v3_struct_0(A)
        & v4_rlvect_1(A)
        & v5_rlvect_1(A)
        & v6_rlvect_1(A)
        & l1_rlvect_1(A) )
     => ! [B] : 
          ( m1_subset_1(B,u1_struct_0(A))
         => ! [C] : 
              ( m1_subset_1(C,u1_struct_0(A))
             => ( k6_rlvect_1(A,B,C) = k1_rlvect_1(A)
               => B = C ) ) ) ) ),
    inference(mizar_proof,[status(thm)],[t66_vectsp_1]),
    [file(vectsp_1,t84_vectsp_1),interesting(0.80)]).

fof(t90_vectsp_1,theorem,(
    ! [A] : 
      ( ( ~ v3_struct_0(A)
        & v4_rlvect_1(A)
        & v5_rlvect_1(A)
        & v6_rlvect_1(A)
        & l1_rlvect_1(A) )
     => ! [B] : 
          ( m1_subset_1(B,u1_struct_0(A))
         => ! [C] : 
              ( m1_subset_1(C,u1_struct_0(A))
             => ! [D] : 
                  ( m1_subset_1(D,u1_struct_0(A))
                 => k6_rlvect_1(A,k2_rlvect_1(A,C,B),k2_rlvect_1(A,D,B)) = k6_rlvect_1(A,C,D) ) ) ) ) ),
    inference(mizar_proof,[status(thm)],[t45_rlvect_1,d6_rlvect_1,d6_rlvect_1,t16_rlvect_1,t10_rlvect_1]),
    [file(vectsp_1,t90_vectsp_1),interesting(0.78)]).

fof(t63_vectsp_1,theorem,(
    ! [A] : 
      ( ( ~ v3_struct_0(A)
        & v4_rlvect_1(A)
        & v5_rlvect_1(A)
        & v6_rlvect_1(A)
        & l1_rlvect_1(A) )
     => ! [B] : 
          ( m1_subset_1(B,u1_struct_0(A))
         => ! [C] : 
              ( m1_subset_1(C,u1_struct_0(A))
             => ( k2_rlvect_1(A,B,C) = k1_rlvect_1(A)
              <=> k5_rlvect_1(A,B) = C ) ) ) ) ),
    inference(mizar_proof,[status(thm)],[t10_rlvect_1,t16_rlvect_1,d6_rlvect_1,t10_rlvect_1,t16_rlvect_1]),
    [file(vectsp_1,t63_vectsp_1),interesting(0.75)]).

fof(t68_vectsp_1,theorem,(
    ! [A] : 
      ( ( ~ v3_struct_0(A)
        & v3_rlvect_1(A)
        & v4_rlvect_1(A)
        & v5_rlvect_1(A)
        & v6_rlvect_1(A)
        & v4_group_1(A)
        & v7_vectsp_1(A)
        & v8_vectsp_1(A)
        & l3_vectsp_1(A) )
     => ! [B] : 
          ( ( ~ v3_struct_0(B)
            & v4_rlvect_1(B)
            & v5_rlvect_1(B)
            & v6_rlvect_1(B)
            & v12_vectsp_1(B,A)
            & l4_vectsp_1(B,A) )
         => ! [C] : 
              ( m1_subset_1(C,u1_struct_0(A))
             => ! [D] : 
                  ( m1_subset_1(D,u1_struct_0(B))
                 => ! [E] : 
                      ( m1_subset_1(E,u1_struct_0(B))
                     => ( k5_rlvect_1(B,k6_vectsp_1(A,B,C,D)) = k6_vectsp_1(A,B,k5_rlvect_1(A,C),D)
                        & k6_rlvect_1(B,E,k6_vectsp_1(A,B,C,D)) = k2_rlvect_1(B,E,k6_vectsp_1(A,B,k5_rlvect_1(A,C),D)) ) ) ) ) ) ) ),
    inference(mizar_proof,[status(thm)],[t59_vectsp_1,d26_vectsp_1,t41_vectsp_1,d19_vectsp_1]),
    [file(vectsp_1,t68_vectsp_1),interesting(0.75)]).

fof(t74_vectsp_1,theorem,(
    ! [A] : 
      ( ( ~ v3_struct_0(A)
        & v3_rlvect_1(A)
        & v4_rlvect_1(A)
        & v5_rlvect_1(A)
        & v6_rlvect_1(A)
        & v4_group_1(A)
        & v7_group_1(A)
        & v7_vectsp_1(A)
        & v8_vectsp_1(A)
        & v9_vectsp_1(A)
        & ~ v10_vectsp_1(A)
        & l3_vectsp_1(A) )
     => ! [B] : 
          ( m1_subset_1(B,u1_struct_0(A))
         => ( B != k1_rlvect_1(A)
           => ( k4_vectsp_1(A,B) != k1_rlvect_1(A)
              & k5_rlvect_1(A,k4_vectsp_1(A,B)) != k1_rlvect_1(A) ) ) ) ) ),
    inference(mizar_proof,[status(thm)],[d22_vectsp_1,t39_vectsp_1,d21_vectsp_1,t42_vectsp_1,t39_vectsp_1,d19_vectsp_1,d22_vectsp_1,t39_vectsp_1,d21_vectsp_1]),
    [file(vectsp_1,t74_vectsp_1),interesting(0.75)]).

fof(t59_vectsp_1,theorem,(
    ! [A] : 
      ( ( ~ v3_struct_0(A)
        & v3_rlvect_1(A)
        & v4_rlvect_1(A)
        & v5_rlvect_1(A)
        & v6_rlvect_1(A)
        & v4_group_1(A)
        & v7_vectsp_1(A)
        & v8_vectsp_1(A)
        & l3_vectsp_1(A) )
     => ! [B] : 
          ( m1_subset_1(B,u1_struct_0(A))
         => ! [C] : 
              ( ( ~ v3_struct_0(C)
                & v4_rlvect_1(C)
                & v5_rlvect_1(C)
                & v6_rlvect_1(C)
                & v12_vectsp_1(C,A)
                & l4_vectsp_1(C,A) )
             => ! [D] : 
                  ( m1_subset_1(D,u1_struct_0(C))
                 => ( k6_vectsp_1(A,C,k1_rlvect_1(A),D) = k1_rlvect_1(C)
                    & k6_vectsp_1(A,C,k5_rlvect_1(A,k2_group_1(A)),D) = k5_rlvect_1(C,D)
                    & k6_vectsp_1(A,C,B,k1_rlvect_1(C)) = k1_rlvect_1(C) ) ) ) ) ) ),
    inference(mizar_proof,[status(thm)],[d26_vectsp_1,d26_vectsp_1,t10_rlvect_1,d26_vectsp_1,t10_rlvect_1,t21_rlvect_1,d26_vectsp_1,d26_vectsp_1,d10_rlvect_1,d6_rlvect_1,t16_rlvect_1,t10_rlvect_1,t10_rlvect_1,d26_vectsp_1,t36_vectsp_1]),
    [file(vectsp_1,t59_vectsp_1),interesting(0.69)]).

fof(t86_vectsp_1,theorem,(
    ! [A] : 
      ( ( ~ v3_struct_0(A)
        & v4_rlvect_1(A)
        & v5_rlvect_1(A)
        & v6_rlvect_1(A)
        & l1_rlvect_1(A) )
     => ! [B] : 
          ( m1_subset_1(B,u1_struct_0(A))
         => ( k5_rlvect_1(A,B) = k1_rlvect_1(A)
           => B = k1_rlvect_1(A) ) ) ) ),
    inference(mizar_proof,[status(thm)],[t30_rlvect_1,t25_rlvect_1]),
    [file(vectsp_1,t86_vectsp_1),interesting(0.69)]).

fof(l95_vectsp_1,theorem,(
    ! [A] : 
      ( ( ~ v3_struct_0(A)
        & v4_rlvect_1(A)
        & v5_rlvect_1(A)
        & v6_rlvect_1(A)
        & l1_rlvect_1(A) )
     => ! [B] : 
          ( m1_subset_1(B,u1_struct_0(A))
         => ! [C] : 
              ( m1_subset_1(C,u1_struct_0(A))
             => k5_rlvect_1(A,k2_rlvect_1(A,C,k5_rlvect_1(A,B))) = k6_rlvect_1(A,B,C) ) ) ) ),
    inference(mizar_proof,[status(thm)],[t44_rlvect_1,t30_rlvect_1]),
    [file(vectsp_1,l95_vectsp_1),interesting(0.67)]).

fof(l96_vectsp_1,theorem,(
    ! [A] : 
      ( ( ~ v3_struct_0(A)
        & v4_rlvect_1(A)
        & v5_rlvect_1(A)
        & v6_rlvect_1(A)
        & l1_rlvect_1(A) )
     => ! [B] : 
          ( m1_subset_1(B,u1_struct_0(A))
         => ! [C] : 
              ( m1_subset_1(C,u1_struct_0(A))
             => k5_rlvect_1(A,k6_rlvect_1(A,k5_rlvect_1(A,B),C)) = k2_rlvect_1(A,C,B) ) ) ) ),
    inference(mizar_proof,[status(thm)],[t47_rlvect_1,t30_rlvect_1]),
    [file(vectsp_1,l96_vectsp_1),interesting(0.67)]).

fof(t65_vectsp_1,theorem,(
    ! [A] : 
      ( ( ~ v3_struct_0(A)
        & v4_rlvect_1(A)
        & v5_rlvect_1(A)
        & v6_rlvect_1(A)
        & l1_rlvect_1(A) )
     => ! [B] : 
          ( m1_subset_1(B,u1_struct_0(A))
         => ( k6_rlvect_1(A,k1_rlvect_1(A),B) = k5_rlvect_1(A,B)
            & k6_rlvect_1(A,B,k1_rlvect_1(A)) = B ) ) ) ),
    inference(mizar_proof,[status(thm)],[t26_rlvect_1,t27_rlvect_1]),
    [file(vectsp_1,t65_vectsp_1),interesting(0.66)]).

fof(t44_vectsp_1,theorem,(
    ! [A] : 
      ( ( ~ v3_struct_0(A)
        & v4_rlvect_1(A)
        & v5_rlvect_1(A)
        & v6_rlvect_1(A)
        & v4_group_1(A)
        & v7_group_1(A)
        & v7_vectsp_1(A)
        & v8_vectsp_1(A)
        & v9_vectsp_1(A)
        & l3_vectsp_1(A) )
     => ! [B] : 
          ( m1_subset_1(B,u1_struct_0(A))
         => ! [C] : 
              ( m1_subset_1(C,u1_struct_0(A))
             => ( k10_group_1(A,B,C) = k1_rlvect_1(A)
              <=> ( B = k1_rlvect_1(A)
                  | C = k1_rlvect_1(A) ) ) ) ) ) ),
    inference(mizar_proof,[status(thm)],[d4_group_1,d22_vectsp_1,d19_vectsp_1,t39_vectsp_1,t39_vectsp_1]),
    [file(vectsp_1,t44_vectsp_1),interesting(0.65)]).

fof(t81_vectsp_1,theorem,(
    ! [A] : 
      ( ( ~ v3_struct_0(A)
        & v4_rlvect_1(A)
        & v5_rlvect_1(A)
        & v6_rlvect_1(A)
        & l1_rlvect_1(A) )
     => ! [B] : 
          ( m1_subset_1(B,u1_struct_0(A))
         => ! [C] : 
              ( m1_subset_1(C,u1_struct_0(A))
             => k5_rlvect_1(A,k6_rlvect_1(A,B,C)) = k6_rlvect_1(A,C,B) ) ) ) ),
    inference(mizar_proof,[status(thm)],[t47_rlvect_1]),
    [file(vectsp_1,t81_vectsp_1),interesting(0.65)]).

fof(t73_vectsp_1,theorem,(
    ! [A] : 
      ( ( ~ v3_struct_0(A)
        & v4_rlvect_1(A)
        & v5_rlvect_1(A)
        & v6_rlvect_1(A)
        & v4_group_1(A)
        & v7_group_1(A)
        & v7_vectsp_1(A)
        & v8_vectsp_1(A)
        & v9_vectsp_1(A)
        & ~ v10_vectsp_1(A)
        & l3_vectsp_1(A) )
     => ! [B] : 
          ( m1_subset_1(B,u1_struct_0(A))
         => ( B != k1_rlvect_1(A)
           => k4_vectsp_1(A,k4_vectsp_1(A,B)) = B ) ) ) ),
    inference(mizar_proof,[status(thm)],[d22_vectsp_1,t39_vectsp_1,d21_vectsp_1,d22_vectsp_1,d4_group_1,d22_vectsp_1,d19_vectsp_1,d19_vectsp_1]),
    [file(vectsp_1,t73_vectsp_1),interesting(0.64)]).

fof(t94_vectsp_1,theorem,(
    ! [A] : 
      ( ( ~ v3_struct_0(A)
        & v3_rlvect_1(A)
        & v4_rlvect_1(A)
        & v5_rlvect_1(A)
        & v6_rlvect_1(A)
        & l1_rlvect_1(A) )
     => ( ~ v3_struct_0(g1_group_1(u1_struct_0(A),u1_rlvect_1(A)))
        & v3_group_1(g1_group_1(u1_struct_0(A),u1_rlvect_1(A)))
        & v4_group_1(g1_group_1(u1_struct_0(A),u1_rlvect_1(A)))
        & v7_group_1(g1_group_1(u1_struct_0(A),u1_rlvect_1(A)))
        & l1_group_1(g1_group_1(u1_struct_0(A),u1_rlvect_1(A))) ) ) ),
    inference(mizar_proof,[status(thm)],[t5_rlvect_1,d6_rlvect_1,d4_group_1,d3_group_1,t10_rlvect_1,t10_rlvect_1,t16_rlvect_1,t16_rlvect_1,d16_group_1]),
    [file(vectsp_1,t94_vectsp_1),interesting(0.63)]).

fof(t33_vectsp_1,theorem,(
    ! [A] : 
      ( ( ~ v3_struct_0(A)
        & v4_group_1(A)
        & v7_group_1(A)
        & v7_vectsp_1(A)
        & v8_vectsp_1(A)
        & v9_vectsp_1(A)
        & l3_vectsp_1(A) )
     => ! [B] : 
          ( m1_subset_1(B,u1_struct_0(A))
         => ! [C] : 
              ( m1_subset_1(C,u1_struct_0(A))
             => ! [D] : 
                  ( m1_subset_1(D,u1_struct_0(A))
                 => ( k10_group_1(A,B,C) = k10_group_1(A,B,D)
                   => ( B = k1_rlvect_1(A)
                      | C = D ) ) ) ) ) ) ),
    inference(mizar_proof,[status(thm)],[d20_vectsp_1,d4_group_1,d19_vectsp_1,d19_vectsp_1]),
    [file(vectsp_1,t33_vectsp_1),interesting(0.62)]).

fof(t60_vectsp_1,theorem,(
    ! [A] : 
      ( ( ~ v3_struct_0(A)
        & v3_rlvect_1(A)
        & v4_rlvect_1(A)
        & v5_rlvect_1(A)
        & v6_rlvect_1(A)
        & v4_group_1(A)
        & v7_group_1(A)
        & v7_vectsp_1(A)
        & v8_vectsp_1(A)
        & v9_vectsp_1(A)
        & ~ v10_vectsp_1(A)
        & l3_vectsp_1(A) )
     => ! [B] : 
          ( m1_subset_1(B,u1_struct_0(A))
         => ! [C] : 
              ( ( ~ v3_struct_0(C)
                & v4_rlvect_1(C)
                & v5_rlvect_1(C)
                & v6_rlvect_1(C)
                & v12_vectsp_1(C,A)
                & l4_vectsp_1(C,A) )
             => ! [D] : 
                  ( m1_subset_1(D,u1_struct_0(C))
                 => ( k6_vectsp_1(A,C,B,D) = k1_rlvect_1(C)
                  <=> ( B = k1_rlvect_1(A)
                      | D = k1_rlvect_1(C) ) ) ) ) ) ) ),
    inference(mizar_proof,[status(thm)],[d26_vectsp_1,t59_vectsp_1,d22_vectsp_1,d26_vectsp_1,t59_vectsp_1]),
    [file(vectsp_1,t60_vectsp_1),interesting(0.60)]).

fof(t22_vectsp_1,theorem,(
    ! [A] : 
      ( ( ~ v3_struct_0(A)
        & l3_vectsp_1(A) )
     => ( ! [B] : 
            ( m1_subset_1(B,u1_struct_0(A))
           => ! [C] : 
                ( m1_subset_1(C,u1_struct_0(A))
               => ! [D] : 
                    ( m1_subset_1(D,u1_struct_0(A))
                   => ( ~ ( B != k1_rlvect_1(A)
                          & ! [E] : 
                              ( m1_subset_1(E,u1_struct_0(A))
                             => k1_group_1(A,B,E) != k2_group_1(A) ) )
                      & k1_group_1(A,B,k2_rlvect_1(A,C,D)) = k2_rlvect_1(A,k1_group_1(A,B,C),k1_group_1(A,B,D))
                      & k1_group_1(A,k2_rlvect_1(A,C,D),B) = k2_rlvect_1(A,k1_group_1(A,C,B),k1_group_1(A,D,B)) ) ) ) )
      <=> ( ~ v3_struct_0(A)
          & v7_vectsp_1(A)
          & v9_vectsp_1(A)
          & l3_vectsp_1(A) ) ) ) ),
    inference(mizar_proof,[status(thm)],[d18_vectsp_1,d20_vectsp_1]),
    [file(vectsp_1,t22_vectsp_1),interesting(0.58)]).

fof(l74_vectsp_1,theorem,(
    ! [A] : 
      ( ( ~ v3_struct_0(A)
        & v3_rlvect_1(A)
        & v4_rlvect_1(A)
        & v5_rlvect_1(A)
        & v6_rlvect_1(A)
        & v4_group_1(A)
        & v7_vectsp_1(A)
        & v8_vectsp_1(A)
        & l3_vectsp_1(A) )
     => ! [B] : 
          ( ( v1_funct_1(B)
            & v1_funct_2(B,k2_zfmisc_1(u1_struct_0(A),u1_struct_0(A)),u1_struct_0(A))
            & m2_relset_1(B,k2_zfmisc_1(u1_struct_0(A),u1_struct_0(A)),u1_struct_0(A)) )
         => ( ~ v3_struct_0(g4_vectsp_1(A,u1_struct_0(A),u1_rlvect_1(A),u2_struct_0(A),B))
            & v3_rlvect_1(g4_vectsp_1(A,u1_struct_0(A),u1_rlvect_1(A),u2_struct_0(A),B))
            & v4_rlvect_1(g4_vectsp_1(A,u1_struct_0(A),u1_rlvect_1(A),u2_struct_0(A),B))
            & v5_rlvect_1(g4_vectsp_1(A,u1_struct_0(A),u1_rlvect_1(A),u2_struct_0(A),B))
            & v6_rlvect_1(g4_vectsp_1(A,u1_struct_0(A),u1_rlvect_1(A),u2_struct_0(A),B))
            & l1_rlvect_1(g4_vectsp_1(A,u1_struct_0(A),u1_rlvect_1(A),u2_struct_0(A),B)) ) ) ) ),
    inference(mizar_proof,[status(thm)],[t5_rlvect_1,t5_rlvect_1,t5_rlvect_1,t5_rlvect_1,t5_rlvect_1,t5_rlvect_1,t5_rlvect_1,t5_rlvect_1,d6_rlvect_1,t5_rlvect_1,t5_rlvect_1,t5_rlvect_1,t5_rlvect_1,t5_rlvect_1,t5_rlvect_1,t10_rlvect_1,d8_rlvect_1,t5_rlvect_1,t5_rlvect_1,d5_rlvect_1,d6_rlvect_1,d7_rlvect_1,d8_rlvect_1]),
    [file(vectsp_1,l74_vectsp_1),interesting(0.38)]).

fof(t67_vectsp_1,theorem,(
    ! [A] : 
      ( ( ~ v3_struct_0(A)
        & v3_rlvect_1(A)
        & v4_rlvect_1(A)
        & v5_rlvect_1(A)
        & v6_rlvect_1(A)
        & v4_group_1(A)
        & v7_group_1(A)
        & v7_vectsp_1(A)
        & v8_vectsp_1(A)
        & v9_vectsp_1(A)
        & ~ v10_vectsp_1(A)
        & l3_vectsp_1(A) )
     => ! [B] : 
          ( m1_subset_1(B,u1_struct_0(A))
         => ! [C] : 
              ( ( ~ v3_struct_0(C)
                & v4_rlvect_1(C)
                & v5_rlvect_1(C)
                & v6_rlvect_1(C)
                & v12_vectsp_1(C,A)
                & l4_vectsp_1(C,A) )
             => ! [D] : 
                  ( m1_subset_1(D,u1_struct_0(C))
                 => ( B != k1_rlvect_1(A)
                   => k6_vectsp_1(A,C,k4_vectsp_1(A,B),k6_vectsp_1(A,C,B,D)) = D ) ) ) ) ) ),
    inference(mizar_proof,[status(thm)],[d26_vectsp_1,d22_vectsp_1,d26_vectsp_1]),
    [file(vectsp_1,t67_vectsp_1),interesting(0.37)]).

fof(d18_vectsp_1,definition,(
    ! [A] : 
      ( ( ~ v3_struct_0(A)
        & l3_vectsp_1(A) )
     => ( v7_vectsp_1(A)
      <=> ! [B] : 
            ( m1_subset_1(B,u1_struct_0(A))
           => ! [C] : 
                ( m1_subset_1(C,u1_struct_0(A))
               => ! [D] : 
                    ( m1_subset_1(D,u1_struct_0(A))
                   => ( k1_group_1(A,B,k2_rlvect_1(A,C,D)) = k2_rlvect_1(A,k1_group_1(A,B,C),k1_group_1(A,B,D))
                      & k1_group_1(A,k2_rlvect_1(A,C,D),B) = k2_rlvect_1(A,k1_group_1(A,C,B),k1_group_1(A,D,B)) ) ) ) ) ) ) ),
    file(vectsp_1,d18_vectsp_1),
    [interesting(0.00)]).

fof(d11_vectsp_1,definition,(
    ! [A] : 
      ( ( ~ v3_struct_0(A)
        & l3_vectsp_1(A) )
     => ( v4_vectsp_1(A)
      <=> ! [B] : 
            ( m1_subset_1(B,u1_struct_0(A))
           => ! [C] : 
                ( m1_subset_1(C,u1_struct_0(A))
               => ! [D] : 
                    ( m1_subset_1(D,u1_struct_0(A))
                   => k1_group_1(A,B,k2_rlvect_1(A,C,D)) = k2_rlvect_1(A,k1_group_1(A,B,C),k1_group_1(A,B,D)) ) ) ) ) ) ),
    file(vectsp_1,d11_vectsp_1),
    [interesting(0.00)]).

fof(d12_vectsp_1,definition,(
    ! [A] : 
      ( ( ~ v3_struct_0(A)
        & l3_vectsp_1(A) )
     => ( v5_vectsp_1(A)
      <=> ! [B] : 
            ( m1_subset_1(B,u1_struct_0(A))
           => ! [C] : 
                ( m1_subset_1(C,u1_struct_0(A))
               => ! [D] : 
                    ( m1_subset_1(D,u1_struct_0(A))
                   => k1_group_1(A,k2_rlvect_1(A,C,D),B) = k2_rlvect_1(A,k1_group_1(A,C,B),k1_group_1(A,D,B)) ) ) ) ) ) ),
    file(vectsp_1,d12_vectsp_1),
    [interesting(0.00)]).

fof(t5_rlvect_1,theorem,(
    ! [A] : 
      ( ( ~ v3_struct_0(A)
        & l1_rlvect_1(A) )
     => ! [B] : 
          ( m1_subset_1(B,u1_struct_0(A))
         => ! [C] : 
              ( m1_subset_1(C,u1_struct_0(A))
             => k2_rlvect_1(A,B,C) = k2_binop_1(u1_struct_0(A),u1_struct_0(A),u1_struct_0(A),u1_rlvect_1(A),B,C) ) ) ) ),
    file(rlvect_1,t5_rlvect_1),
    [interesting(0.00)]).

fof(d6_rlvect_1,definition,(
    ! [A] : 
      ( ( ~ v3_struct_0(A)
        & l1_rlvect_1(A) )
     => ( v4_rlvect_1(A)
      <=> ! [B] : 
            ( m1_subset_1(B,u1_struct_0(A))
           => ! [C] : 
                ( m1_subset_1(C,u1_struct_0(A))
               => ! [D] : 
                    ( m1_subset_1(D,u1_struct_0(A))
                   => k2_rlvect_1(A,k2_rlvect_1(A,B,C),D) = k2_rlvect_1(A,B,k2_rlvect_1(A,C,D)) ) ) ) ) ) ),
    file(rlvect_1,d6_rlvect_1),
    [interesting(0.00)]).

fof(t10_rlvect_1,theorem,(
    ! [A] : 
      ( ( ~ v3_struct_0(A)
        & v4_rlvect_1(A)
        & v5_rlvect_1(A)
        & v6_rlvect_1(A)
        & l1_rlvect_1(A) )
     => ! [B] : 
          ( m1_subset_1(B,u1_struct_0(A))
         => ( k2_rlvect_1(A,B,k1_rlvect_1(A)) = B
            & k2_rlvect_1(A,k1_rlvect_1(A),B) = B ) ) ) ),
    file(rlvect_1,t10_rlvect_1),
    [interesting(0.00)]).

fof(d8_rlvect_1,definition,(
    ! [A] : 
      ( ( ~ v3_struct_0(A)
        & l1_rlvect_1(A) )
     => ( v6_rlvect_1(A)
      <=> ! [B] : 
            ( m1_subset_1(B,u1_struct_0(A))
           => ? [C] : 
                ( m1_subset_1(C,u1_struct_0(A))
                & k2_rlvect_1(A,B,C) = k1_rlvect_1(A) ) ) ) ) ),
    file(rlvect_1,d8_rlvect_1),
    [interesting(0.00)]).

fof(d5_rlvect_1,definition,(
    ! [A] : 
      ( ( ~ v3_struct_0(A)
        & l1_rlvect_1(A) )
     => ( v3_rlvect_1(A)
      <=> ! [B] : 
            ( m1_subset_1(B,u1_struct_0(A))
           => ! [C] : 
                ( m1_subset_1(C,u1_struct_0(A))
               => k2_rlvect_1(A,B,C) = k2_rlvect_1(A,C,B) ) ) ) ) ),
    file(rlvect_1,d5_rlvect_1),
    [interesting(0.00)]).

fof(d7_rlvect_1,definition,(
    ! [A] : 
      ( ( ~ v3_struct_0(A)
        & l1_rlvect_1(A) )
     => ( v5_rlvect_1(A)
      <=> ! [B] : 
            ( m1_subset_1(B,u1_struct_0(A))
           => k2_rlvect_1(A,B,k1_rlvect_1(A)) = B ) ) ) ),
    file(rlvect_1,d7_rlvect_1),
    [interesting(0.00)]).

fof(d4_group_1,definition,(
    ! [A] : 
      ( ( ~ v3_struct_0(A)
        & l1_group_1(A) )
     => ( v4_group_1(A)
      <=> ! [B] : 
            ( m1_subset_1(B,u1_struct_0(A))
           => ! [C] : 
                ( m1_subset_1(C,u1_struct_0(A))
               => ! [D] : 
                    ( m1_subset_1(D,u1_struct_0(A))
                   => k1_group_1(A,k1_group_1(A,B,C),D) = k1_group_1(A,B,k1_group_1(A,C,D)) ) ) ) ) ) ),
    file(group_1,d4_group_1),
    [interesting(0.00)]).

fof(d19_vectsp_1,definition,(
    ! [A] : 
      ( ( ~ v3_struct_0(A)
        & l1_vectsp_1(A) )
     => ( v8_vectsp_1(A)
      <=> ! [B] : 
            ( m1_subset_1(B,u1_struct_0(A))
           => k1_group_1(A,k2_group_1(A),B) = B ) ) ) ),
    file(vectsp_1,d19_vectsp_1),
    [interesting(0.00)]).

fof(l75_vectsp_1,theorem,(
    ! [A] : 
      ( ( ~ v3_struct_0(A)
        & v4_rlvect_1(A)
        & v5_rlvect_1(A)
        & v6_rlvect_1(A)
        & v4_group_1(A)
        & v7_vectsp_1(A)
        & v8_vectsp_1(A)
        & l3_vectsp_1(A) )
     => ! [B] : 
          ( ( v1_funct_1(B)
            & v1_funct_2(B,k2_zfmisc_1(u1_struct_0(A),u1_struct_0(A)),u1_struct_0(A))
            & m2_relset_1(B,k2_zfmisc_1(u1_struct_0(A),u1_struct_0(A)),u1_struct_0(A)) )
         => ( B = u1_group_1(A)
           => ! [C] : 
                ( m1_subset_1(C,u1_struct_0(A))
               => ! [D] : 
                    ( m1_subset_1(D,u1_struct_0(A))
                   => ! [E] : 
                        ( m1_subset_1(E,u1_struct_0(g4_vectsp_1(A,u1_struct_0(A),u1_rlvect_1(A),u2_struct_0(A),B)))
                       => ! [F] : 
                            ( m1_subset_1(F,u1_struct_0(g4_vectsp_1(A,u1_struct_0(A),u1_rlvect_1(A),u2_struct_0(A),B)))
                           => ( k6_vectsp_1(A,g4_vectsp_1(A,u1_struct_0(A),u1_rlvect_1(A),u2_struct_0(A),B),C,k2_rlvect_1(g4_vectsp_1(A,u1_struct_0(A),u1_rlvect_1(A),u2_struct_0(A),B),E,F)) = k2_rlvect_1(g4_vectsp_1(A,u1_struct_0(A),u1_rlvect_1(A),u2_struct_0(A),B),k6_vectsp_1(A,g4_vectsp_1(A,u1_struct_0(A),u1_rlvect_1(A),u2_struct_0(A),B),C,E),k6_vectsp_1(A,g4_vectsp_1(A,u1_struct_0(A),u1_rlvect_1(A),u2_struct_0(A),B),C,F))
                              & k6_vectsp_1(A,g4_vectsp_1(A,u1_struct_0(A),u1_rlvect_1(A),u2_struct_0(A),B),k2_rlvect_1(A,C,D),E) = k2_rlvect_1(g4_vectsp_1(A,u1_struct_0(A),u1_rlvect_1(A),u2_struct_0(A),B),k6_vectsp_1(A,g4_vectsp_1(A,u1_struct_0(A),u1_rlvect_1(A),u2_struct_0(A),B),C,E),k6_vectsp_1(A,g4_vectsp_1(A,u1_struct_0(A),u1_rlvect_1(A),u2_struct_0(A),B),D,E))
                              & k6_vectsp_1(A,g4_vectsp_1(A,u1_struct_0(A),u1_rlvect_1(A),u2_struct_0(A),B),k1_group_1(A,C,D),E) = k6_vectsp_1(A,g4_vectsp_1(A,u1_struct_0(A),u1_rlvect_1(A),u2_struct_0(A),B),C,k6_vectsp_1(A,g4_vectsp_1(A,u1_struct_0(A),u1_rlvect_1(A),u2_struct_0(A),B),D,E))
                              & k6_vectsp_1(A,g4_vectsp_1(A,u1_struct_0(A),u1_rlvect_1(A),u2_struct_0(A),B),k2_group_1(A),E) = E ) ) ) ) ) ) ) ) ),
    inference(mizar_proof,[status(thm)],[t5_rlvect_1,t5_rlvect_1,d18_vectsp_1,t5_rlvect_1,t5_rlvect_1,d18_vectsp_1,t5_rlvect_1,t5_rlvect_1,d4_group_1,d19_vectsp_1]),
    [file(vectsp_1,l75_vectsp_1),interesting(0.00)]).

fof(t10_vectsp_1,theorem,(
    $true ),
    file(vectsp_1,t10_vectsp_1),
    [interesting(0.00)]).

fof(t11_vectsp_1,theorem,(
    $true ),
    file(vectsp_1,t11_vectsp_1),
    [interesting(0.00)]).

fof(t12_vectsp_1,theorem,(
    $true ),
    file(vectsp_1,t12_vectsp_1),
    [interesting(0.00)]).

fof(t13_vectsp_1,theorem,(
    $true ),
    file(vectsp_1,t13_vectsp_1),
    [interesting(0.00)]).

fof(t14_vectsp_1,theorem,(
    $true ),
    file(vectsp_1,t14_vectsp_1),
    [interesting(0.00)]).

fof(t15_vectsp_1,theorem,(
    $true ),
    file(vectsp_1,t15_vectsp_1),
    [interesting(0.00)]).

fof(t16_vectsp_1,theorem,(
    $true ),
    file(vectsp_1,t16_vectsp_1),
    [interesting(0.00)]).

fof(t17_vectsp_1,theorem,(
    $true ),
    file(vectsp_1,t17_vectsp_1),
    [interesting(0.00)]).

fof(t18_vectsp_1,theorem,(
    $true ),
    file(vectsp_1,t18_vectsp_1),
    [interesting(0.00)]).

fof(t19_vectsp_1,theorem,(
    $true ),
    file(vectsp_1,t19_vectsp_1),
    [interesting(0.00)]).

fof(t1_vectsp_1,theorem,(
    $true ),
    file(vectsp_1,t1_vectsp_1),
    [interesting(0.00)]).

fof(d11_binop_2,definition,(
    ! [A] : 
      ( ( v1_funct_1(A)
        & v1_funct_2(A,k2_zfmisc_1(k1_numbers,k1_numbers),k1_numbers)
        & m2_relset_1(A,k2_zfmisc_1(k1_numbers,k1_numbers),k1_numbers) )
     => ( A = k35_binop_2
      <=> ! [B] : 
            ( m1_subset_1(B,k1_numbers)
           => ! [C] : 
                ( m1_subset_1(C,k1_numbers)
               => k2_binop_1(k1_numbers,k1_numbers,k1_numbers,A,B,C) = k11_binop_2(B,C) ) ) ) ) ),
    file(binop_2,d11_binop_2),
    [interesting(0.00)]).

fof(d5_group_1,definition,(
    ! [A] : 
      ( ( ~ v3_struct_0(A)
        & l1_group_1(A) )
     => ( v2_group_1(A)
       => ! [B] : 
            ( m1_subset_1(B,u1_struct_0(A))
           => ( B = k2_group_1(A)
            <=> ! [C] : 
                  ( m1_subset_1(C,u1_struct_0(A))
                 => ( k1_group_1(A,C,B) = C
                    & k1_group_1(A,B,C) = C ) ) ) ) ) ) ),
    file(group_1,d5_group_1),
    [interesting(0.00)]).

fof(d20_vectsp_1,definition,(
    ! [A] : 
      ( ( ~ v3_struct_0(A)
        & l2_vectsp_1(A) )
     => ( v9_vectsp_1(A)
      <=> ! [B] : 
            ( m1_subset_1(B,u1_struct_0(A))
           => ~ ( B != k1_rlvect_1(A)
                & ! [C] : 
                    ( m1_subset_1(C,u1_struct_0(A))
                   => k1_group_1(A,B,C) != k2_group_1(A) ) ) ) ) ) ),
    file(vectsp_1,d20_vectsp_1),
    [interesting(0.00)]).

fof(d10_rlvect_1,definition,(
    ! [A] : 
      ( ( ~ v3_struct_0(A)
        & l1_rlvect_1(A) )
     => ! [B] : 
          ( m1_subset_1(B,u1_struct_0(A))
         => ( ( v4_rlvect_1(A)
              & v5_rlvect_1(A)
              & v6_rlvect_1(A) )
           => ! [C] : 
                ( m1_subset_1(C,u1_struct_0(A))
               => ( C = k5_rlvect_1(A,B)
                <=> k2_rlvect_1(A,B,C) = k1_rlvect_1(A) ) ) ) ) ) ),
    file(rlvect_1,d10_rlvect_1),
    [interesting(0.00)]).

fof(t21_vectsp_1,theorem,(
    ! [A] : 
      ( m1_subset_1(A,u1_struct_0(k3_vectsp_1))
     => ! [B] : 
          ( m1_subset_1(B,u1_struct_0(k3_vectsp_1))
         => ! [C] : 
              ( m1_subset_1(C,u1_struct_0(k3_vectsp_1))
             => ( k4_rlvect_1(k3_vectsp_1,A,B) = k4_rlvect_1(k3_vectsp_1,B,A)
                & k4_rlvect_1(k3_vectsp_1,k4_rlvect_1(k3_vectsp_1,A,B),C) = k4_rlvect_1(k3_vectsp_1,A,k4_rlvect_1(k3_vectsp_1,B,C))
                & k4_rlvect_1(k3_vectsp_1,A,k1_rlvect_1(k3_vectsp_1)) = A
                & k4_rlvect_1(k3_vectsp_1,A,k5_rlvect_1(k3_vectsp_1,A)) = k1_rlvect_1(k3_vectsp_1)
                & k10_group_1(k3_vectsp_1,A,B) = k10_group_1(k3_vectsp_1,B,A)
                & k10_group_1(k3_vectsp_1,k10_group_1(k3_vectsp_1,A,B),C) = k10_group_1(k3_vectsp_1,A,k10_group_1(k3_vectsp_1,B,C))
                & k10_group_1(k3_vectsp_1,k2_group_1(k3_vectsp_1),A) = A
                & ~ ( A != k1_rlvect_1(k3_vectsp_1)
                    & ! [D] : 
                        ( m1_subset_1(D,u1_struct_0(k3_vectsp_1))
                       => k10_group_1(k3_vectsp_1,A,D) != k2_group_1(k3_vectsp_1) ) )
                & k10_group_1(k3_vectsp_1,A,k4_rlvect_1(k3_vectsp_1,B,C)) = k4_rlvect_1(k3_vectsp_1,k10_group_1(k3_vectsp_1,A,B),k10_group_1(k3_vectsp_1,A,C))
                & k10_group_1(k3_vectsp_1,k4_rlvect_1(k3_vectsp_1,B,C),A) = k4_rlvect_1(k3_vectsp_1,k10_group_1(k3_vectsp_1,B,A),k10_group_1(k3_vectsp_1,C,A)) ) ) ) ) ),
    inference(mizar_proof,[status(thm)],[d18_vectsp_1,d19_vectsp_1,d20_vectsp_1,d4_group_1,d6_rlvect_1,d7_rlvect_1,d10_rlvect_1]),
    [file(vectsp_1,t21_vectsp_1),interesting(0.00)]).

fof(t23_vectsp_1,theorem,(
    $true ),
    file(vectsp_1,t23_vectsp_1),
    [interesting(0.00)]).

fof(t24_vectsp_1,theorem,(
    $true ),
    file(vectsp_1,t24_vectsp_1),
    [interesting(0.00)]).

fof(t25_vectsp_1,theorem,(
    $true ),
    file(vectsp_1,t25_vectsp_1),
    [interesting(0.00)]).

fof(t26_vectsp_1,theorem,(
    $true ),
    file(vectsp_1,t26_vectsp_1),
    [interesting(0.00)]).

fof(t27_vectsp_1,theorem,(
    $true ),
    file(vectsp_1,t27_vectsp_1),
    [interesting(0.00)]).

fof(t28_vectsp_1,theorem,(
    $true ),
    file(vectsp_1,t28_vectsp_1),
    [interesting(0.00)]).

fof(t29_vectsp_1,theorem,(
    $true ),
    file(vectsp_1,t29_vectsp_1),
    [interesting(0.00)]).

fof(t2_vectsp_1,theorem,(
    $true ),
    file(vectsp_1,t2_vectsp_1),
    [interesting(0.00)]).

fof(t30_vectsp_1,theorem,(
    $true ),
    file(vectsp_1,t30_vectsp_1),
    [interesting(0.00)]).

fof(t31_vectsp_1,theorem,(
    $true ),
    file(vectsp_1,t31_vectsp_1),
    [interesting(0.00)]).

fof(t32_vectsp_1,theorem,(
    $true ),
    file(vectsp_1,t32_vectsp_1),
    [interesting(0.00)]).

fof(t34_vectsp_1,theorem,(
    $true ),
    file(vectsp_1,t34_vectsp_1),
    [interesting(0.00)]).

fof(t35_vectsp_1,theorem,(
    $true ),
    file(vectsp_1,t35_vectsp_1),
    [interesting(0.00)]).

fof(t37_vectsp_1,theorem,(
    $true ),
    file(vectsp_1,t37_vectsp_1),
    [interesting(0.00)]).

fof(t38_vectsp_1,theorem,(
    $true ),
    file(vectsp_1,t38_vectsp_1),
    [interesting(0.00)]).

fof(t3_vectsp_1,theorem,(
    $true ),
    file(vectsp_1,t3_vectsp_1),
    [interesting(0.00)]).

fof(t21_rlvect_1,theorem,(
    ! [A] : 
      ( ( ~ v3_struct_0(A)
        & v4_rlvect_1(A)
        & v5_rlvect_1(A)
        & v6_rlvect_1(A)
        & l1_rlvect_1(A) )
     => ! [B] : 
          ( m1_subset_1(B,u1_struct_0(A))
         => ! [C] : 
              ( m1_subset_1(C,u1_struct_0(A))
             => ! [D] : 
                  ( m1_subset_1(D,u1_struct_0(A))
                 => ! [E] : 
                      ( m1_subset_1(E,u1_struct_0(A))
                     => ( ( k2_rlvect_1(A,B,D) = k2_rlvect_1(A,B,E)
                          | k2_rlvect_1(A,D,B) = k2_rlvect_1(A,E,B) )
                       => D = E ) ) ) ) ) ) ),
    file(rlvect_1,t21_rlvect_1),
    [interesting(0.00)]).

fof(t43_vectsp_1,theorem,(
    ! [A] : 
      ( ( ~ v3_struct_0(A)
        & v4_rlvect_1(A)
        & v5_rlvect_1(A)
        & v6_rlvect_1(A)
        & v4_vectsp_1(A)
        & l3_vectsp_1(A) )
     => ! [B] : 
          ( m1_subset_1(B,u1_struct_0(A))
         => ! [C] : 
              ( m1_subset_1(C,u1_struct_0(A))
             => ! [D] : 
                  ( m1_subset_1(D,u1_struct_0(A))
                 => k1_group_1(A,B,k6_rlvect_1(A,C,D)) = k6_rlvect_1(A,k1_group_1(A,B,C),k1_group_1(A,B,D)) ) ) ) ) ),
    inference(mizar_proof,[status(thm)],[d11_vectsp_1,t40_vectsp_1]),
    [file(vectsp_1,t43_vectsp_1),interesting(0.00)]).

fof(d22_vectsp_1,definition,(
    ! [A] : 
      ( ( ~ v3_struct_0(A)
        & v4_group_1(A)
        & v7_group_1(A)
        & v7_vectsp_1(A)
        & v8_vectsp_1(A)
        & v9_vectsp_1(A)
        & l3_vectsp_1(A) )
     => ! [B] : 
          ( m1_subset_1(B,u1_struct_0(A))
         => ( B != k1_rlvect_1(A)
           => ! [C] : 
                ( m1_subset_1(C,u1_struct_0(A))
               => ( C = k4_vectsp_1(A,B)
                <=> k10_group_1(A,B,C) = k2_group_1(A) ) ) ) ) ) ),
    file(vectsp_1,d22_vectsp_1),
    [interesting(0.00)]).

fof(t45_vectsp_1,theorem,(
    ! [A] : 
      ( ( ~ v3_struct_0(A)
        & v4_rlvect_1(A)
        & v5_rlvect_1(A)
        & v6_rlvect_1(A)
        & v5_vectsp_1(A)
        & l3_vectsp_1(A) )
     => ! [B] : 
          ( m1_subset_1(B,u1_struct_0(A))
         => ! [C] : 
              ( m1_subset_1(C,u1_struct_0(A))
             => ! [D] : 
                  ( m1_subset_1(D,u1_struct_0(A))
                 => k1_group_1(A,k6_rlvect_1(A,B,C),D) = k6_rlvect_1(A,k1_group_1(A,B,D),k1_group_1(A,C,D)) ) ) ) ) ),
    inference(mizar_proof,[status(thm)],[d12_vectsp_1,t41_vectsp_1]),
    [file(vectsp_1,t45_vectsp_1),interesting(0.00)]).

fof(t46_vectsp_1,theorem,(
    $true ),
    file(vectsp_1,t46_vectsp_1),
    [interesting(0.00)]).

fof(t47_vectsp_1,theorem,(
    $true ),
    file(vectsp_1,t47_vectsp_1),
    [interesting(0.00)]).

fof(t48_vectsp_1,theorem,(
    $true ),
    file(vectsp_1,t48_vectsp_1),
    [interesting(0.00)]).

fof(t49_vectsp_1,theorem,(
    $true ),
    file(vectsp_1,t49_vectsp_1),
    [interesting(0.00)]).

fof(t4_vectsp_1,theorem,(
    $true ),
    file(vectsp_1,t4_vectsp_1),
    [interesting(0.00)]).

fof(t50_vectsp_1,theorem,(
    $true ),
    file(vectsp_1,t50_vectsp_1),
    [interesting(0.00)]).

fof(t51_vectsp_1,theorem,(
    $true ),
    file(vectsp_1,t51_vectsp_1),
    [interesting(0.00)]).

fof(t52_vectsp_1,theorem,(
    $true ),
    file(vectsp_1,t52_vectsp_1),
    [interesting(0.00)]).

fof(t53_vectsp_1,theorem,(
    $true ),
    file(vectsp_1,t53_vectsp_1),
    [interesting(0.00)]).

fof(t54_vectsp_1,theorem,(
    $true ),
    file(vectsp_1,t54_vectsp_1),
    [interesting(0.00)]).

fof(t55_vectsp_1,theorem,(
    $true ),
    file(vectsp_1,t55_vectsp_1),
    [interesting(0.00)]).

fof(t56_vectsp_1,theorem,(
    $true ),
    file(vectsp_1,t56_vectsp_1),
    [interesting(0.00)]).

fof(t57_vectsp_1,theorem,(
    $true ),
    file(vectsp_1,t57_vectsp_1),
    [interesting(0.00)]).

fof(t58_vectsp_1,theorem,(
    $true ),
    file(vectsp_1,t58_vectsp_1),
    [interesting(0.00)]).

fof(t5_vectsp_1,theorem,(
    $true ),
    file(vectsp_1,t5_vectsp_1),
    [interesting(0.00)]).

fof(d26_vectsp_1,definition,(
    ! [A] : 
      ( ( ~ v3_struct_0(A)
        & l3_vectsp_1(A) )
     => ! [B] : 
          ( ( ~ v3_struct_0(B)
            & l4_vectsp_1(B,A) )
         => ( v12_vectsp_1(B,A)
          <=> ! [C] : 
                ( m1_subset_1(C,u1_struct_0(A))
               => ! [D] : 
                    ( m1_subset_1(D,u1_struct_0(A))
                   => ! [E] : 
                        ( m1_subset_1(E,u1_struct_0(B))
                       => ! [F] : 
                            ( m1_subset_1(F,u1_struct_0(B))
                           => ( k6_vectsp_1(A,B,C,k2_rlvect_1(B,E,F)) = k2_rlvect_1(B,k6_vectsp_1(A,B,C,E),k6_vectsp_1(A,B,C,F))
                              & k6_vectsp_1(A,B,k2_rlvect_1(A,C,D),E) = k2_rlvect_1(B,k6_vectsp_1(A,B,C,E),k6_vectsp_1(A,B,D,E))
                              & k6_vectsp_1(A,B,k1_group_1(A,C,D),E) = k6_vectsp_1(A,B,C,k6_vectsp_1(A,B,D,E))
                              & k6_vectsp_1(A,B,k2_group_1(A),E) = E ) ) ) ) ) ) ) ) ),
    file(vectsp_1,d26_vectsp_1),
    [interesting(0.00)]).

fof(t16_rlvect_1,theorem,(
    ! [A] : 
      ( ( ~ v3_struct_0(A)
        & v4_rlvect_1(A)
        & v5_rlvect_1(A)
        & v6_rlvect_1(A)
        & l1_rlvect_1(A) )
     => ! [B] : 
          ( m1_subset_1(B,u1_struct_0(A))
         => ( k2_rlvect_1(A,B,k5_rlvect_1(A,B)) = k1_rlvect_1(A)
            & k2_rlvect_1(A,k5_rlvect_1(A,B),B) = k1_rlvect_1(A) ) ) ) ),
    file(rlvect_1,t16_rlvect_1),
    [interesting(0.00)]).

fof(t61_vectsp_1,theorem,(
    $true ),
    file(vectsp_1,t61_vectsp_1),
    [interesting(0.00)]).

fof(t62_vectsp_1,theorem,(
    $true ),
    file(vectsp_1,t62_vectsp_1),
    [interesting(0.00)]).

fof(t44_rlvect_1,theorem,(
    ! [A] : 
      ( ( ~ v3_struct_0(A)
        & v4_rlvect_1(A)
        & v5_rlvect_1(A)
        & v6_rlvect_1(A)
        & l1_rlvect_1(A) )
     => ! [B] : 
          ( m1_subset_1(B,u1_struct_0(A))
         => ! [C] : 
              ( m1_subset_1(C,u1_struct_0(A))
             => k5_rlvect_1(A,k2_rlvect_1(A,B,C)) = k6_rlvect_1(A,k5_rlvect_1(A,C),B) ) ) ) ),
    file(rlvect_1,t44_rlvect_1),
    [interesting(0.00)]).

fof(t30_rlvect_1,theorem,(
    ! [A] : 
      ( ( ~ v3_struct_0(A)
        & v4_rlvect_1(A)
        & v5_rlvect_1(A)
        & v6_rlvect_1(A)
        & l1_rlvect_1(A) )
     => ! [B] : 
          ( m1_subset_1(B,u1_struct_0(A))
         => k5_rlvect_1(A,k5_rlvect_1(A,B)) = B ) ) ),
    file(rlvect_1,t30_rlvect_1),
    [interesting(0.00)]).

fof(t47_rlvect_1,theorem,(
    ! [A] : 
      ( ( ~ v3_struct_0(A)
        & v4_rlvect_1(A)
        & v5_rlvect_1(A)
        & v6_rlvect_1(A)
        & l1_rlvect_1(A) )
     => ! [B] : 
          ( m1_subset_1(B,u1_struct_0(A))
         => ! [C] : 
              ( m1_subset_1(C,u1_struct_0(A))
             => k5_rlvect_1(A,k6_rlvect_1(A,B,C)) = k2_rlvect_1(A,C,k5_rlvect_1(A,B)) ) ) ) ),
    file(rlvect_1,t47_rlvect_1),
    [interesting(0.00)]).

fof(t41_rlvect_1,theorem,(
    ! [A] : 
      ( ( ~ v3_struct_0(A)
        & v4_rlvect_1(A)
        & v5_rlvect_1(A)
        & v6_rlvect_1(A)
        & l1_rlvect_1(A) )
     => ! [B] : 
          ( m1_subset_1(B,u1_struct_0(A))
         => ! [C] : 
              ( m1_subset_1(C,u1_struct_0(A))
             => ! [D] : 
                  ( m1_subset_1(D,u1_struct_0(A))
                 => k6_rlvect_1(A,B,k2_rlvect_1(A,C,D)) = k6_rlvect_1(A,k6_rlvect_1(A,B,D),C) ) ) ) ) ),
    file(rlvect_1,t41_rlvect_1),
    [interesting(0.00)]).

fof(t64_vectsp_1,theorem,(
    ! [A] : 
      ( ( ~ v3_struct_0(A)
        & v4_rlvect_1(A)
        & v5_rlvect_1(A)
        & v6_rlvect_1(A)
        & l1_rlvect_1(A) )
     => ! [B] : 
          ( m1_subset_1(B,u1_struct_0(A))
         => ! [C] : 
              ( m1_subset_1(C,u1_struct_0(A))
             => ! [D] : 
                  ( m1_subset_1(D,u1_struct_0(A))
                 => ( k5_rlvect_1(A,k2_rlvect_1(A,C,D)) = k6_rlvect_1(A,k5_rlvect_1(A,D),C)
                    & k5_rlvect_1(A,k2_rlvect_1(A,D,k5_rlvect_1(A,C))) = k6_rlvect_1(A,C,D)
                    & k5_rlvect_1(A,k6_rlvect_1(A,C,D)) = k2_rlvect_1(A,D,k5_rlvect_1(A,C))
                    & k5_rlvect_1(A,k6_rlvect_1(A,k5_rlvect_1(A,C),D)) = k2_rlvect_1(A,D,C)
                    & k6_rlvect_1(A,B,k2_rlvect_1(A,D,C)) = k6_rlvect_1(A,k6_rlvect_1(A,B,C),D) ) ) ) ) ) ),
    inference(mizar_proof,[status(thm)],[l95_vectsp_1,l96_vectsp_1,t41_rlvect_1,t44_rlvect_1,t47_rlvect_1]),
    [file(vectsp_1,t64_vectsp_1),interesting(0.00)]).

fof(t26_rlvect_1,theorem,(
    ! [A] : 
      ( ( ~ v3_struct_0(A)
        & v4_rlvect_1(A)
        & v5_rlvect_1(A)
        & v6_rlvect_1(A)
        & l1_rlvect_1(A) )
     => ! [B] : 
          ( m1_subset_1(B,u1_struct_0(A))
         => k6_rlvect_1(A,B,k1_rlvect_1(A)) = B ) ) ),
    file(rlvect_1,t26_rlvect_1),
    [interesting(0.00)]).

fof(t27_rlvect_1,theorem,(
    ! [A] : 
      ( ( ~ v3_struct_0(A)
        & v4_rlvect_1(A)
        & v5_rlvect_1(A)
        & v6_rlvect_1(A)
        & l1_rlvect_1(A) )
     => ! [B] : 
          ( m1_subset_1(B,u1_struct_0(A))
         => k6_rlvect_1(A,k1_rlvect_1(A),B) = k5_rlvect_1(A,B) ) ) ),
    file(rlvect_1,t27_rlvect_1),
    [interesting(0.00)]).

fof(t6_vectsp_1,theorem,(
    ! [A] : 
      ( m1_subset_1(A,u1_struct_0(k1_vectsp_1))
     => ! [B] : 
          ( m1_subset_1(B,u1_struct_0(k1_vectsp_1))
         => ! [C] : 
              ( m1_subset_1(C,u1_struct_0(k1_vectsp_1))
             => ( k4_rlvect_1(k1_vectsp_1,A,B) = k4_rlvect_1(k1_vectsp_1,B,A)
                & k4_rlvect_1(k1_vectsp_1,k4_rlvect_1(k1_vectsp_1,A,B),C) = k4_rlvect_1(k1_vectsp_1,A,k4_rlvect_1(k1_vectsp_1,B,C))
                & k4_rlvect_1(k1_vectsp_1,A,k1_rlvect_1(k1_vectsp_1)) = A
                & k4_rlvect_1(k1_vectsp_1,A,k5_rlvect_1(k1_vectsp_1,A)) = k1_rlvect_1(k1_vectsp_1) ) ) ) ) ),
    inference(mizar_proof,[status(thm)],[d6_rlvect_1,d7_rlvect_1,d10_rlvect_1]),
    [file(vectsp_1,t6_vectsp_1),interesting(0.00)]).

fof(d13_vectsp_1,definition,(
    ! [A] : 
      ( ( ~ v3_struct_0(A)
        & l1_vectsp_1(A) )
     => ( v6_vectsp_1(A)
      <=> ! [B] : 
            ( m1_subset_1(B,u1_struct_0(A))
           => k1_group_1(A,B,k2_group_1(A)) = B ) ) ) ),
    file(vectsp_1,d13_vectsp_1),
    [interesting(0.00)]).

fof(t71_vectsp_1,theorem,(
    $true ),
    file(vectsp_1,t71_vectsp_1),
    [interesting(0.00)]).

fof(t72_vectsp_1,theorem,(
    $true ),
    file(vectsp_1,t72_vectsp_1),
    [interesting(0.00)]).

fof(d21_vectsp_1,definition,(
    ! [A] : 
      ( ( ~ v3_struct_0(A)
        & l2_vectsp_1(A) )
     => ( v10_vectsp_1(A)
      <=> k1_rlvect_1(A) = k2_group_1(A) ) ) ),
    file(vectsp_1,d21_vectsp_1),
    [interesting(0.00)]).

fof(t75_vectsp_1,theorem,(
    $true ),
    file(vectsp_1,t75_vectsp_1),
    [interesting(0.00)]).

fof(t76_vectsp_1,theorem,(
    $true ),
    file(vectsp_1,t76_vectsp_1),
    [interesting(0.00)]).

fof(t77_vectsp_1,theorem,(
    $true ),
    file(vectsp_1,t77_vectsp_1),
    [interesting(0.00)]).

fof(d9_binop_2,definition,(
    ! [A] : 
      ( ( v1_funct_1(A)
        & v1_funct_2(A,k2_zfmisc_1(k1_numbers,k1_numbers),k1_numbers)
        & m2_relset_1(A,k2_zfmisc_1(k1_numbers,k1_numbers),k1_numbers) )
     => ( A = k33_binop_2
      <=> ! [B] : 
            ( m1_subset_1(B,k1_numbers)
           => ! [C] : 
                ( m1_subset_1(C,k1_numbers)
               => k2_binop_1(k1_numbers,k1_numbers,k1_numbers,A,B,C) = k9_binop_2(B,C) ) ) ) ) ),
    file(binop_2,d9_binop_2),
    [interesting(0.00)]).

fof(t79_vectsp_1,theorem,(
    $true ),
    file(vectsp_1,t79_vectsp_1),
    [interesting(0.00)]).

fof(t7_vectsp_1,theorem,(
    ! [A] : 
      ( ( ~ v3_struct_0(A)
        & l1_rlvect_1(A) )
     => ( ! [B] : 
            ( m1_subset_1(B,u1_struct_0(A))
           => ! [C] : 
                ( m1_subset_1(C,u1_struct_0(A))
               => ! [D] : 
                    ( m1_subset_1(D,u1_struct_0(A))
                   => ( k2_rlvect_1(A,B,C) = k2_rlvect_1(A,C,B)
                      & k2_rlvect_1(A,k2_rlvect_1(A,B,C),D) = k2_rlvect_1(A,B,k2_rlvect_1(A,C,D))
                      & k2_rlvect_1(A,B,k1_rlvect_1(A)) = B
                      & ? [E] : 
                          ( m1_subset_1(E,u1_struct_0(A))
                          & k2_rlvect_1(A,B,E) = k1_rlvect_1(A) ) ) ) ) )
      <=> ( ~ v3_struct_0(A)
          & v3_rlvect_1(A)
          & v4_rlvect_1(A)
          & v5_rlvect_1(A)
          & v6_rlvect_1(A)
          & l1_rlvect_1(A) ) ) ) ),
    inference(mizar_proof,[status(thm)],[d5_rlvect_1,d6_rlvect_1,d7_rlvect_1,d8_rlvect_1]),
    [file(vectsp_1,t7_vectsp_1),interesting(0.00)]).

fof(t80_vectsp_1,theorem,(
    $true ),
    file(vectsp_1,t80_vectsp_1),
    [interesting(0.00)]).

fof(t82_vectsp_1,theorem,(
    $true ),
    file(vectsp_1,t82_vectsp_1),
    [interesting(0.00)]).

fof(t83_vectsp_1,theorem,(
    $true ),
    file(vectsp_1,t83_vectsp_1),
    [interesting(0.00)]).

fof(t66_vectsp_1,theorem,(
    ! [A] : 
      ( ( ~ v3_struct_0(A)
        & v4_rlvect_1(A)
        & v5_rlvect_1(A)
        & v6_rlvect_1(A)
        & l1_rlvect_1(A) )
     => ! [B] : 
          ( m1_subset_1(B,u1_struct_0(A))
         => ! [C] : 
              ( m1_subset_1(C,u1_struct_0(A))
             => ( ( k2_rlvect_1(A,B,k5_rlvect_1(A,C)) = k1_rlvect_1(A)
                 => B = C )
                & ( B = C
                 => k2_rlvect_1(A,B,k5_rlvect_1(A,C)) = k1_rlvect_1(A) )
                & ( k6_rlvect_1(A,B,C) = k1_rlvect_1(A)
                 => B = C )
                & ( B = C
                 => k6_rlvect_1(A,B,C) = k1_rlvect_1(A) ) ) ) ) ) ),
    inference(mizar_proof,[status(thm)],[d6_rlvect_1,t16_rlvect_1,t10_rlvect_1,t10_rlvect_1,t16_rlvect_1]),
    [file(vectsp_1,t66_vectsp_1),interesting(0.00)]).

fof(t85_vectsp_1,theorem,(
    $true ),
    file(vectsp_1,t85_vectsp_1),
    [interesting(0.00)]).

fof(t25_rlvect_1,theorem,(
    ! [A] : 
      ( ( ~ v3_struct_0(A)
        & v4_rlvect_1(A)
        & v5_rlvect_1(A)
        & v6_rlvect_1(A)
        & l1_rlvect_1(A) )
     => k5_rlvect_1(A,k1_rlvect_1(A)) = k1_rlvect_1(A) ) ),
    file(rlvect_1,t25_rlvect_1),
    [interesting(0.00)]).

fof(t87_vectsp_1,theorem,(
    ! [A] : 
      ( ( ~ v3_struct_0(A)
        & v4_rlvect_1(A)
        & v5_rlvect_1(A)
        & v6_rlvect_1(A)
        & l1_rlvect_1(A) )
     => ! [B] : 
          ( m1_subset_1(B,u1_struct_0(A))
         => ! [C] : 
              ( m1_subset_1(C,u1_struct_0(A))
             => ( k6_rlvect_1(A,B,C) = k1_rlvect_1(A)
               => k6_rlvect_1(A,C,B) = k1_rlvect_1(A) ) ) ) ) ),
    inference(mizar_proof,[status(thm)],[t81_vectsp_1,t86_vectsp_1]),
    [file(vectsp_1,t87_vectsp_1),interesting(0.00)]).

fof(t35_rlvect_1,theorem,(
    ! [A] : 
      ( ( ~ v3_struct_0(A)
        & v4_rlvect_1(A)
        & v5_rlvect_1(A)
        & v6_rlvect_1(A)
        & l1_rlvect_1(A) )
     => ! [B] : 
          ( m1_subset_1(B,u1_struct_0(A))
         => ! [C] : 
              ( m1_subset_1(C,u1_struct_0(A))
             => ( k6_rlvect_1(A,B,C) = k1_rlvect_1(A)
               => B = C ) ) ) ) ),
    file(rlvect_1,t35_rlvect_1),
    [interesting(0.00)]).

fof(t88_vectsp_1,theorem,(
    ! [A] : 
      ( ( ~ v3_struct_0(A)
        & v3_rlvect_1(A)
        & v4_rlvect_1(A)
        & v5_rlvect_1(A)
        & v6_rlvect_1(A)
        & v4_group_1(A)
        & v7_group_1(A)
        & v7_vectsp_1(A)
        & v8_vectsp_1(A)
        & v9_vectsp_1(A)
        & ~ v10_vectsp_1(A)
        & l3_vectsp_1(A) )
     => ! [B] : 
          ( m1_subset_1(B,u1_struct_0(A))
         => ! [C] : 
              ( m1_subset_1(C,u1_struct_0(A))
             => ! [D] : 
                  ( m1_subset_1(D,u1_struct_0(A))
                 => ( ( k6_rlvect_1(A,k10_group_1(A,B,D),C) = k1_rlvect_1(A)
                     => ( B = k1_rlvect_1(A)
                        | D = k10_group_1(A,C,k4_vectsp_1(A,B)) ) )
                    & ( k6_rlvect_1(A,C,k10_group_1(A,D,B)) = k1_rlvect_1(A)
                     => ( B = k1_rlvect_1(A)
                        | D = k10_group_1(A,C,k4_vectsp_1(A,B)) ) ) ) ) ) ) ) ),
    inference(mizar_proof,[status(thm)],[t35_rlvect_1,d22_vectsp_1,d4_group_1,d19_vectsp_1,t25_rlvect_1,t47_rlvect_1]),
    [file(vectsp_1,t88_vectsp_1),interesting(0.00)]).

fof(t45_rlvect_1,theorem,(
    ! [A] : 
      ( ( ~ v3_struct_0(A)
        & v4_rlvect_1(A)
        & v5_rlvect_1(A)
        & v6_rlvect_1(A)
        & l1_rlvect_1(A) )
     => ! [B] : 
          ( m1_subset_1(B,u1_struct_0(A))
         => ! [C] : 
              ( m1_subset_1(C,u1_struct_0(A))
             => k5_rlvect_1(A,k2_rlvect_1(A,B,C)) = k2_rlvect_1(A,k5_rlvect_1(A,C),k5_rlvect_1(A,B)) ) ) ) ),
    file(rlvect_1,t45_rlvect_1),
    [interesting(0.00)]).

fof(t89_vectsp_1,theorem,(
    ! [A] : 
      ( ( ~ v3_struct_0(A)
        & v4_rlvect_1(A)
        & v5_rlvect_1(A)
        & v6_rlvect_1(A)
        & l1_rlvect_1(A) )
     => ! [B] : 
          ( m1_subset_1(B,u1_struct_0(A))
         => ! [C] : 
              ( m1_subset_1(C,u1_struct_0(A))
             => k2_rlvect_1(A,B,C) = k5_rlvect_1(A,k2_rlvect_1(A,k5_rlvect_1(A,C),k5_rlvect_1(A,B))) ) ) ) ),
    inference(mizar_proof,[status(thm)],[t30_rlvect_1,t45_rlvect_1]),
    [file(vectsp_1,t89_vectsp_1),interesting(0.00)]).

fof(t8_vectsp_1,theorem,(
    $true ),
    file(vectsp_1,t8_vectsp_1),
    [interesting(0.00)]).

fof(t91_vectsp_1,theorem,(
    $true ),
    file(vectsp_1,t91_vectsp_1),
    [interesting(0.00)]).

fof(t92_vectsp_1,theorem,(
    ! [A] : 
      ( ( ~ v3_struct_0(A)
        & v4_rlvect_1(A)
        & v5_rlvect_1(A)
        & v6_rlvect_1(A)
        & l1_rlvect_1(A) )
     => ! [B] : 
          ( m1_subset_1(B,u1_struct_0(A))
         => ! [C] : 
              ( m1_subset_1(C,u1_struct_0(A))
             => k5_rlvect_1(A,k2_rlvect_1(A,k5_rlvect_1(A,B),C)) = k2_rlvect_1(A,k5_rlvect_1(A,C),B) ) ) ) ),
    inference(mizar_proof,[status(thm)],[t45_rlvect_1,t30_rlvect_1]),
    [file(vectsp_1,t92_vectsp_1),interesting(0.00)]).

fof(t93_vectsp_1,theorem,(
    ! [A] : 
      ( ( ~ v3_struct_0(A)
        & v3_rlvect_1(A)
        & v4_rlvect_1(A)
        & v5_rlvect_1(A)
        & v6_rlvect_1(A)
        & l1_rlvect_1(A) )
     => ! [B] : 
          ( m1_subset_1(B,u1_struct_0(A))
         => ! [C] : 
              ( m1_subset_1(C,u1_struct_0(A))
             => ! [D] : 
                  ( m1_subset_1(D,u1_struct_0(A))
                 => k6_rlvect_1(A,k6_rlvect_1(A,B,C),D) = k6_rlvect_1(A,k6_rlvect_1(A,B,D),C) ) ) ) ) ),
    inference(mizar_proof,[status(thm)],[d6_rlvect_1]),
    [file(vectsp_1,t93_vectsp_1),interesting(0.00)]).

fof(d3_group_1,definition,(
    ! [A] : 
      ( ( ~ v3_struct_0(A)
        & l1_group_1(A) )
     => ( v3_group_1(A)
      <=> ? [B] : 
            ( m1_subset_1(B,u1_struct_0(A))
            & ! [C] : 
                ( m1_subset_1(C,u1_struct_0(A))
               => ( k1_group_1(A,C,B) = C
                  & k1_group_1(A,B,C) = C
                  & ? [D] : 
                      ( m1_subset_1(D,u1_struct_0(A))
                      & k1_group_1(A,C,D) = B
                      & k1_group_1(A,D,C) = B ) ) ) ) ) ) ),
    file(group_1,d3_group_1),
    [interesting(0.00)]).

fof(d16_group_1,definition,(
    ! [A] : 
      ( ( ~ v3_struct_0(A)
        & l1_group_1(A) )
     => ( v7_group_1(A)
      <=> ! [B] : 
            ( m1_subset_1(B,u1_struct_0(A))
           => ! [C] : 
                ( m1_subset_1(C,u1_struct_0(A))
               => k1_group_1(A,B,C) = k1_group_1(A,C,B) ) ) ) ) ),
    file(group_1,d16_group_1),
    [interesting(0.00)]).

fof(t9_vectsp_1,theorem,(
    $true ),
    file(vectsp_1,t9_vectsp_1),
    [interesting(0.00)]).