fof(l2_algstr_2,theorem,(
    0 = k1_rlvect_1(k3_vectsp_1) ),
    inference(mizar_proof,[status(thm)],[d2_rlvect_1,d15_vectsp_1]),
    [file(algstr_2,l2_algstr_2),interesting(1.00)]).

fof(l3_algstr_2,theorem,(
    ! [A] : 
      ( m1_subset_1(A,u1_struct_0(k3_vectsp_1))
     => ! [B] : 
          ( m1_subset_1(B,u1_struct_0(k3_vectsp_1))
         => ~ ( A != k1_rlvect_1(k3_vectsp_1)
              & ! [C] : 
                  ( m1_subset_1(C,u1_struct_0(k3_vectsp_1))
                 => k10_group_1(k3_vectsp_1,A,C) != B ) ) ) ) ),
    inference(mizar_proof,[status(thm)],[d15_vectsp_1,l2_algstr_2,t32_algstr_1,d15_vectsp_1,l1_algstr_2]),
    [file(algstr_2,l3_algstr_2),interesting(1.00)]).

fof(t21_algstr_2,theorem,(
    ! [A] : 
      ( ( ~ v3_struct_0(A)
        & v5_rlvect_1(A)
        & v2_group_1(A)
        & v5_vectsp_1(A)
        & v1_algstr_1(A)
        & v6_algstr_1(A)
        & v11_algstr_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,k1_algstr_2(A,B),C) = k1_algstr_2(A,k1_group_1(A,B,C)) ) ) ) ),
    inference(mizar_proof,[status(thm)],[d12_vectsp_1,d7_algstr_2,t34_algstr_1,d7_algstr_2]),
    [file(algstr_2,t21_algstr_2),interesting(0.94)]).

fof(l4_algstr_2,theorem,(
    ! [A] : 
      ( m1_subset_1(A,u1_struct_0(k3_vectsp_1))
     => ! [B] : 
          ( m1_subset_1(B,u1_struct_0(k3_vectsp_1))
         => ~ ( A != k1_rlvect_1(k3_vectsp_1)
              & ! [C] : 
                  ( m1_subset_1(C,u1_struct_0(k3_vectsp_1))
                 => k10_group_1(k3_vectsp_1,C,A) != B ) ) ) ) ),
    inference(mizar_proof,[status(thm)],[l3_algstr_2]),
    [file(algstr_2,l4_algstr_2),interesting(0.93)]).

fof(t14_algstr_2,theorem,(
    ! [A] : 
      ( ( ~ v3_struct_0(A)
        & v3_rlvect_1(A)
        & v5_rlvect_1(A)
        & v2_group_1(A)
        & v4_vectsp_1(A)
        & v1_algstr_1(A)
        & v6_algstr_1(A)
        & v11_algstr_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,k1_algstr_2(A,C)) = k1_algstr_2(A,k1_group_1(A,B,C)) ) ) ) ),
    inference(mizar_proof,[status(thm)],[d11_vectsp_1,d7_algstr_2,t34_algstr_1,d7_algstr_2]),
    [file(algstr_2,t14_algstr_2),interesting(0.90)]).

fof(l1_algstr_2,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,k1_numbers)
             => ! [D] : 
                  ( m1_subset_1(D,k1_numbers)
                 => ( ( A = C
                      & B = D )
                   => k10_group_1(k3_vectsp_1,A,B) = k11_binop_2(C,D) ) ) ) ) ) ),
    inference(mizar_proof,[status(thm)],[d1_group_1,d15_vectsp_1,d11_binop_2]),
    [file(algstr_2,l1_algstr_2),interesting(0.89)]).

fof(t16_algstr_2,theorem,(
    ! [A] : 
      ( ( ~ v3_struct_0(A)
        & v3_rlvect_1(A)
        & v5_rlvect_1(A)
        & v2_group_1(A)
        & v4_vectsp_1(A)
        & v1_algstr_1(A)
        & v6_algstr_1(A)
        & v11_algstr_1(A)
        & l3_vectsp_1(A) )
     => k1_group_1(A,k1_algstr_2(A,k2_group_1(A)),k1_algstr_2(A,k2_group_1(A))) = k2_group_1(A) ) ),
    inference(mizar_proof,[status(thm)],[t14_algstr_2,d13_vectsp_1,t15_algstr_2]),
    [file(algstr_2,t16_algstr_2),interesting(0.89)]).

fof(t23_algstr_2,theorem,(
    ! [A] : 
      ( ( ~ v3_struct_0(A)
        & v3_rlvect_1(A)
        & v5_rlvect_1(A)
        & v2_group_1(A)
        & v5_vectsp_1(A)
        & v1_algstr_1(A)
        & v6_algstr_1(A)
        & v11_algstr_1(A)
        & l3_vectsp_1(A) )
     => k1_group_1(A,k1_algstr_2(A,k2_group_1(A)),k1_algstr_2(A,k2_group_1(A))) = k2_group_1(A) ) ),
    inference(mizar_proof,[status(thm)],[t21_algstr_2,d19_vectsp_1,t15_algstr_2]),
    [file(algstr_2,t23_algstr_2),interesting(0.89)]).

fof(t15_algstr_2,theorem,(
    ! [A] : 
      ( ( ~ v3_struct_0(A)
        & v3_rlvect_1(A)
        & v2_algstr_1(A)
        & v5_algstr_1(A)
        & l1_rlvect_1(A) )
     => ! [B] : 
          ( m1_subset_1(B,u1_struct_0(A))
         => k1_algstr_2(A,k1_algstr_2(A,B)) = B ) ) ),
    inference(mizar_proof,[status(thm)],[d7_algstr_2,d7_algstr_2]),
    [file(algstr_2,t15_algstr_2),interesting(0.87)]).

fof(t24_algstr_2,theorem,(
    ! [A] : 
      ( ( ~ v3_struct_0(A)
        & v5_rlvect_1(A)
        & v2_group_1(A)
        & v5_vectsp_1(A)
        & v1_algstr_1(A)
        & v6_algstr_1(A)
        & v11_algstr_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,k2_algstr_2(A,B,C),D) = k2_algstr_2(A,k1_group_1(A,B,D),k1_group_1(A,C,D)) ) ) ) ) ),
    inference(mizar_proof,[status(thm)],[d12_vectsp_1,t21_algstr_2]),
    [file(algstr_2,t24_algstr_2),interesting(0.81)]).

fof(l44_algstr_2,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))
                 => k1_group_1(A,C,k2_group_1(A)) = C )
              & ! [C] : 
                  ( m1_subset_1(C,u1_struct_0(A))
                 => ~ ( C != k1_rlvect_1(A)
                      & ! [D] : 
                          ( m1_subset_1(D,u1_struct_0(A))
                         => k1_group_1(A,C,D) != k2_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(A))
                         => k1_group_1(A,k1_group_1(A,C,D),E) = k1_group_1(A,C,k1_group_1(A,D,E)) ) ) )
              & ! [C] : 
                  ( m1_subset_1(C,u1_struct_0(A))
                 => k1_group_1(A,C,k1_rlvect_1(A)) = k1_rlvect_1(A) )
              & ! [C] : 
                  ( m1_subset_1(C,u1_struct_0(A))
                 => k1_group_1(A,k1_rlvect_1(A),C) = k1_rlvect_1(A) ) )
           => ( k1_rlvect_1(A) = k2_group_1(A)
              | k1_group_1(A,k2_group_1(A),B) = k1_group_1(A,B,k2_group_1(A)) ) ) ) ) ),
    inference(mizar_proof,[status(thm)],[l43_algstr_2]),
    [file(algstr_2,l44_algstr_2),interesting(0.81)]).

fof(l7_algstr_2,theorem,(
    ! [A] : 
      ( m1_subset_1(A,u1_struct_0(k3_vectsp_1))
     => k10_group_1(k3_vectsp_1,A,k1_rlvect_1(k3_vectsp_1)) = k1_rlvect_1(k3_vectsp_1) ) ),
    inference(mizar_proof,[status(thm)],[t44_vectsp_1]),
    [file(algstr_2,l7_algstr_2),interesting(0.80)]).

fof(l8_algstr_2,theorem,(
    ! [A] : 
      ( m1_subset_1(A,u1_struct_0(k3_vectsp_1))
     => k10_group_1(k3_vectsp_1,k1_rlvect_1(k3_vectsp_1),A) = k1_rlvect_1(k3_vectsp_1) ) ),
    inference(mizar_proof,[status(thm)],[t44_vectsp_1]),
    [file(algstr_2,l8_algstr_2),interesting(0.80)]).

fof(l45_algstr_2,theorem,(
    ! [A] : 
      ( ( ~ v3_struct_0(A)
        & l3_vectsp_1(A) )
     => ( ( ! [B] : 
              ( m1_subset_1(B,u1_struct_0(A))
             => k1_group_1(A,B,k2_group_1(A)) = B )
          & ! [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) ) ) )
          & ! [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)) ) ) )
          & ! [B] : 
              ( m1_subset_1(B,u1_struct_0(A))
             => k1_group_1(A,B,k1_rlvect_1(A)) = k1_rlvect_1(A) )
          & ! [B] : 
              ( m1_subset_1(B,u1_struct_0(A))
             => k1_group_1(A,k1_rlvect_1(A),B) = k1_rlvect_1(A) ) )
       => ( k1_rlvect_1(A) = k2_group_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,C,B) != k2_group_1(A) ) ) ) ) ) ) ),
    inference(mizar_proof,[status(thm)],[l43_algstr_2]),
    [file(algstr_2,l45_algstr_2),interesting(0.80)]).

fof(t17_algstr_2,theorem,(
    ! [A] : 
      ( ( ~ v3_struct_0(A)
        & v3_rlvect_1(A)
        & v5_rlvect_1(A)
        & v2_group_1(A)
        & v4_vectsp_1(A)
        & v1_algstr_1(A)
        & v6_algstr_1(A)
        & v11_algstr_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,k2_algstr_2(A,C,D)) = k2_algstr_2(A,k1_group_1(A,B,C),k1_group_1(A,B,D)) ) ) ) ) ),
    inference(mizar_proof,[status(thm)],[d11_vectsp_1,t14_algstr_2]),
    [file(algstr_2,t17_algstr_2),interesting(0.77)]).

fof(l5_algstr_2,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))
             => ( k10_group_1(k3_vectsp_1,A,B) = k10_group_1(k3_vectsp_1,A,C)
               => ( A = k1_rlvect_1(k3_vectsp_1)
                  | B = C ) ) ) ) ) ),
    inference(mizar_proof,[status(thm)],[t33_vectsp_1]),
    [file(algstr_2,l5_algstr_2),interesting(0.76)]).

fof(l6_algstr_2,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))
             => ( k10_group_1(k3_vectsp_1,B,A) = k10_group_1(k3_vectsp_1,C,A)
               => ( A = k1_rlvect_1(k3_vectsp_1)
                  | B = C ) ) ) ) ) ),
    inference(mizar_proof,[status(thm)],[t33_vectsp_1]),
    [file(algstr_2,l6_algstr_2),interesting(0.76)]).

fof(t32_algstr_2,theorem,(
    ! [A] : 
      ( ( ~ v3_struct_0(A)
        & l3_vectsp_1(A) )
     => ( ( ~ v3_struct_0(A)
          & v3_rlvect_1(A)
          & v4_rlvect_1(A)
          & v5_rlvect_1(A)
          & v2_group_1(A)
          & v4_group_1(A)
          & v7_vectsp_1(A)
          & ~ v10_vectsp_1(A)
          & v1_algstr_1(A)
          & v6_algstr_1(A)
          & v11_algstr_1(A)
          & l3_vectsp_1(A) )
      <=> ( ! [B] : 
              ( m1_subset_1(B,u1_struct_0(A))
             => k2_rlvect_1(A,B,k1_rlvect_1(A)) = B )
          & ! [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) ) )
          & ! [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)) ) ) )
          & ! [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) ) )
          & k1_rlvect_1(A) != k2_group_1(A)
          & ! [B] : 
              ( m1_subset_1(B,u1_struct_0(A))
             => k1_group_1(A,B,k2_group_1(A)) = B )
          & ! [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) ) ) )
          & ! [B] : 
              ( m1_subset_1(B,u1_struct_0(A))
             => k1_group_1(A,B,k1_rlvect_1(A)) = k1_rlvect_1(A) )
          & ! [B] : 
              ( m1_subset_1(B,u1_struct_0(A))
             => k1_group_1(A,k1_rlvect_1(A),B) = k1_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))
                     => k1_group_1(A,k1_group_1(A,B,C),D) = k1_group_1(A,B,k1_group_1(A,C,D)) ) ) )
          & ! [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)) ) ) )
          & ! [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)) ) ) ) ) ) ) ),
    inference(mizar_proof,[status(thm)],[t7_algstr_1,t34_algstr_1,d4_group_1,d5_rlvect_1,d6_rlvect_1,d7_rlvect_1,d18_vectsp_1,d21_vectsp_1,d13_vectsp_1,t3_algstr_1,t3_algstr_1,l44_algstr_2,l45_algstr_2,l45_algstr_2,t7_algstr_1,t34_algstr_1,d5_algstr_1,d4_group_1,d5_rlvect_1,d6_rlvect_1,d7_rlvect_1,d18_vectsp_1,d21_vectsp_1,d2_group_1]),
    [file(algstr_2,t32_algstr_2),interesting(0.43)]).

fof(t34_algstr_2,theorem,(
    ! [A] : 
      ( ( ~ v3_struct_0(A)
        & l3_vectsp_1(A) )
     => ( ( ~ v3_struct_0(A)
          & v3_rlvect_1(A)
          & v4_rlvect_1(A)
          & v5_rlvect_1(A)
          & v2_group_1(A)
          & v4_group_1(A)
          & v7_group_1(A)
          & v7_vectsp_1(A)
          & ~ v10_vectsp_1(A)
          & v1_algstr_1(A)
          & v6_algstr_1(A)
          & v11_algstr_1(A)
          & l3_vectsp_1(A) )
      <=> ( ! [B] : 
              ( m1_subset_1(B,u1_struct_0(A))
             => k2_rlvect_1(A,B,k1_rlvect_1(A)) = B )
          & ! [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) ) )
          & ! [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)) ) ) )
          & ! [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) ) )
          & k1_rlvect_1(A) != k2_group_1(A)
          & ! [B] : 
              ( m1_subset_1(B,u1_struct_0(A))
             => k1_group_1(A,B,k2_group_1(A)) = B )
          & ! [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) ) ) )
          & ! [B] : 
              ( m1_subset_1(B,u1_struct_0(A))
             => k1_group_1(A,B,k1_rlvect_1(A)) = k1_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))
                     => k1_group_1(A,k1_group_1(A,B,C),D) = k1_group_1(A,B,k1_group_1(A,C,D)) ) ) )
          & ! [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)) ) ) )
          & ! [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) ) ) ) ) ) ),
    inference(mizar_proof,[status(thm)],[t32_algstr_2,d16_group_1,t32_algstr_2,d16_group_1]),
    [file(algstr_2,t34_algstr_2),interesting(0.42)]).

fof(t12_algstr_2,theorem,(
    ! [A] : 
      ( ( ~ v3_struct_0(A)
        & l3_vectsp_1(A) )
     => ( ( ~ v3_struct_0(A)
          & v3_rlvect_1(A)
          & v4_rlvect_1(A)
          & v5_rlvect_1(A)
          & v2_group_1(A)
          & v4_vectsp_1(A)
          & ~ v10_vectsp_1(A)
          & v1_algstr_1(A)
          & v6_algstr_1(A)
          & v11_algstr_1(A)
          & l3_vectsp_1(A) )
      <=> ( ! [B] : 
              ( m1_subset_1(B,u1_struct_0(A))
             => k2_rlvect_1(A,B,k1_rlvect_1(A)) = B )
          & ! [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) ) )
          & ! [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)) ) ) )
          & ! [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) ) )
          & k1_rlvect_1(A) != k2_group_1(A)
          & ! [B] : 
              ( m1_subset_1(B,u1_struct_0(A))
             => k1_group_1(A,B,k2_group_1(A)) = B )
          & ! [B] : 
              ( m1_subset_1(B,u1_struct_0(A))
             => k1_group_1(A,k2_group_1(A),B) = B )
          & ! [B] : 
              ( m1_subset_1(B,u1_struct_0(A))
             => ! [C] : 
                  ( m1_subset_1(C,u1_struct_0(A))
                 => ~ ( B != k1_rlvect_1(A)
                      & ! [D] : 
                          ( m1_subset_1(D,u1_struct_0(A))
                         => k1_group_1(A,B,D) != C ) ) ) )
          & ! [B] : 
              ( m1_subset_1(B,u1_struct_0(A))
             => ! [C] : 
                  ( m1_subset_1(C,u1_struct_0(A))
                 => ~ ( B != k1_rlvect_1(A)
                      & ! [D] : 
                          ( m1_subset_1(D,u1_struct_0(A))
                         => k1_group_1(A,D,B) != C ) ) ) )
          & ! [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,C) = k1_group_1(A,B,D)
                       => ( B = k1_rlvect_1(A)
                          | C = D ) ) ) ) )
          & ! [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,C,B) = k1_group_1(A,D,B)
                       => ( B = k1_rlvect_1(A)
                          | C = D ) ) ) ) )
          & ! [B] : 
              ( m1_subset_1(B,u1_struct_0(A))
             => k1_group_1(A,B,k1_rlvect_1(A)) = k1_rlvect_1(A) )
          & ! [B] : 
              ( m1_subset_1(B,u1_struct_0(A))
             => k1_group_1(A,k1_rlvect_1(A),B) = k1_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))
                     => 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)) ) ) ) ) ) ) ),
    inference(mizar_proof,[status(thm)],[t7_algstr_1,t34_algstr_1,d5_rlvect_1,d6_rlvect_1,d7_rlvect_1,d11_vectsp_1,d21_vectsp_1,d13_vectsp_1,d19_vectsp_1,t3_algstr_1,t7_algstr_1,t34_algstr_1,d5_algstr_1,d5_rlvect_1,d6_rlvect_1,d7_rlvect_1,d11_vectsp_1,d21_vectsp_1,d2_group_1]),
    [file(algstr_2,t12_algstr_2),interesting(0.03)]).

fof(t19_algstr_2,theorem,(
    ! [A] : 
      ( ( ~ v3_struct_0(A)
        & l3_vectsp_1(A) )
     => ( ( ~ v3_struct_0(A)
          & v3_rlvect_1(A)
          & v4_rlvect_1(A)
          & v5_rlvect_1(A)
          & v2_group_1(A)
          & v5_vectsp_1(A)
          & ~ v10_vectsp_1(A)
          & v1_algstr_1(A)
          & v6_algstr_1(A)
          & v11_algstr_1(A)
          & l3_vectsp_1(A) )
      <=> ( ! [B] : 
              ( m1_subset_1(B,u1_struct_0(A))
             => k2_rlvect_1(A,B,k1_rlvect_1(A)) = B )
          & ! [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) ) )
          & ! [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)) ) ) )
          & ! [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) ) )
          & k1_rlvect_1(A) != k2_group_1(A)
          & ! [B] : 
              ( m1_subset_1(B,u1_struct_0(A))
             => k1_group_1(A,B,k2_group_1(A)) = B )
          & ! [B] : 
              ( m1_subset_1(B,u1_struct_0(A))
             => k1_group_1(A,k2_group_1(A),B) = B )
          & ! [B] : 
              ( m1_subset_1(B,u1_struct_0(A))
             => ! [C] : 
                  ( m1_subset_1(C,u1_struct_0(A))
                 => ~ ( B != k1_rlvect_1(A)
                      & ! [D] : 
                          ( m1_subset_1(D,u1_struct_0(A))
                         => k1_group_1(A,B,D) != C ) ) ) )
          & ! [B] : 
              ( m1_subset_1(B,u1_struct_0(A))
             => ! [C] : 
                  ( m1_subset_1(C,u1_struct_0(A))
                 => ~ ( B != k1_rlvect_1(A)
                      & ! [D] : 
                          ( m1_subset_1(D,u1_struct_0(A))
                         => k1_group_1(A,D,B) != C ) ) ) )
          & ! [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,C) = k1_group_1(A,B,D)
                       => ( B = k1_rlvect_1(A)
                          | C = D ) ) ) ) )
          & ! [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,C,B) = k1_group_1(A,D,B)
                       => ( B = k1_rlvect_1(A)
                          | C = D ) ) ) ) )
          & ! [B] : 
              ( m1_subset_1(B,u1_struct_0(A))
             => k1_group_1(A,B,k1_rlvect_1(A)) = k1_rlvect_1(A) )
          & ! [B] : 
              ( m1_subset_1(B,u1_struct_0(A))
             => k1_group_1(A,k1_rlvect_1(A),B) = k1_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))
                     => 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)) ) ) ) ) ) ) ),
    inference(mizar_proof,[status(thm)],[t7_algstr_1,t34_algstr_1,d5_rlvect_1,d6_rlvect_1,d7_rlvect_1,d12_vectsp_1,d21_vectsp_1,d13_vectsp_1,d19_vectsp_1,t3_algstr_1,t3_algstr_1,t7_algstr_1,t34_algstr_1,d5_algstr_1,d5_rlvect_1,d6_rlvect_1,d7_rlvect_1,d12_vectsp_1,d21_vectsp_1,d2_group_1]),
    [file(algstr_2,t19_algstr_2),interesting(0.03)]).

fof(d15_vectsp_1,definition,(
    k3_vectsp_1 = g3_vectsp_1(k1_numbers,k33_binop_2,k35_binop_2,1,0) ),
    file(vectsp_1,d15_vectsp_1),
    [interesting(0.00)]).

fof(d2_rlvect_1,definition,(
    ! [A] : 
      ( l2_struct_0(A)
     => k1_rlvect_1(A) = u2_struct_0(A) ) ),
    file(rlvect_1,d2_rlvect_1),
    [interesting(0.00)]).

fof(t32_algstr_1,theorem,(
    ! [A] : 
      ( m1_subset_1(A,k1_numbers)
     => ! [B] : 
          ( m1_subset_1(B,k1_numbers)
         => ~ ( A != 0
              & ! [C] : 
                  ( m1_subset_1(C,k1_numbers)
                 => B != k11_binop_2(A,C) ) ) ) ) ),
    file(algstr_1,t32_algstr_1),
    [interesting(0.00)]).

fof(d1_group_1,definition,(
    ! [A] : 
      ( ( ~ v3_struct_0(A)
        & l1_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) = k2_binop_1(u1_struct_0(A),u1_struct_0(A),u1_struct_0(A),u1_group_1(A),B,C) ) ) ) ),
    file(group_1,d1_group_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(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 ) ) ) ) ) ) ),
    file(vectsp_1,t33_vectsp_1),
    [interesting(0.00)]).

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) ) ) ) ) ) ),
    file(vectsp_1,t44_vectsp_1),
    [interesting(0.00)]).

fof(t10_algstr_2,theorem,(
    $true ),
    file(algstr_2,t10_algstr_2),
    [interesting(0.00)]).

fof(t11_algstr_2,theorem,(
    $true ),
    file(algstr_2,t11_algstr_2),
    [interesting(0.00)]).

fof(t7_algstr_1,theorem,(
    ! [A] : 
      ( ( ~ v3_struct_0(A)
        & l1_rlvect_1(A) )
     => ( v6_algstr_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,D) = C ) ) )
          & ! [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,D,B) = C ) ) )
          & ! [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,B,D)
                       => C = D ) ) ) )
          & ! [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,C,B) = k2_rlvect_1(A,D,B)
                       => C = D ) ) ) ) ) ) ) ),
    file(algstr_1,t7_algstr_1),
    [interesting(0.00)]).

fof(t34_algstr_1,theorem,(
    ! [A] : 
      ( ( ~ v3_struct_0(A)
        & l2_vectsp_1(A) )
     => ( v11_algstr_1(A)
      <=> ( ! [B] : 
              ( m1_subset_1(B,u1_struct_0(A))
             => ! [C] : 
                  ( m1_subset_1(C,u1_struct_0(A))
                 => ~ ( B != k1_rlvect_1(A)
                      & ! [D] : 
                          ( m1_subset_1(D,u1_struct_0(A))
                         => k1_group_1(A,B,D) != C ) ) ) )
          & ! [B] : 
              ( m1_subset_1(B,u1_struct_0(A))
             => ! [C] : 
                  ( m1_subset_1(C,u1_struct_0(A))
                 => ~ ( B != k1_rlvect_1(A)
                      & ! [D] : 
                          ( m1_subset_1(D,u1_struct_0(A))
                         => k1_group_1(A,D,B) != C ) ) ) )
          & ! [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,C) = k1_group_1(A,B,D)
                       => ( B = k1_rlvect_1(A)
                          | C = D ) ) ) ) )
          & ! [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,C,B) = k1_group_1(A,D,B)
                       => ( B = k1_rlvect_1(A)
                          | C = D ) ) ) ) )
          & ! [B] : 
              ( m1_subset_1(B,u1_struct_0(A))
             => k1_group_1(A,B,k1_rlvect_1(A)) = k1_rlvect_1(A) )
          & ! [B] : 
              ( m1_subset_1(B,u1_struct_0(A))
             => k1_group_1(A,k1_rlvect_1(A),B) = k1_rlvect_1(A) ) ) ) ) ),
    file(algstr_1,t34_algstr_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(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(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(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(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(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(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(t3_algstr_1,theorem,(
    ! [A] : 
      ( ( ~ v3_struct_0(A)
        & l1_rlvect_1(A) )
     => ( ( ! [B] : 
              ( m1_subset_1(B,u1_struct_0(A))
             => k2_rlvect_1(A,B,k1_rlvect_1(A)) = B )
          & ! [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) ) )
          & ! [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)) ) ) ) )
       => ! [B] : 
            ( m1_subset_1(B,u1_struct_0(A))
           => ? [C] : 
                ( m1_subset_1(C,u1_struct_0(A))
                & k2_rlvect_1(A,C,B) = k1_rlvect_1(A) ) ) ) ) ),
    file(algstr_1,t3_algstr_1),
    [interesting(0.00)]).

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

fof(d2_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))
            & ! [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,d2_group_1),
    [interesting(0.00)]).

fof(t13_algstr_2,theorem,(
    $true ),
    file(algstr_2,t13_algstr_2),
    [interesting(0.00)]).

fof(d7_algstr_2,definition,(
    ! [A] : 
      ( ( ~ v3_struct_0(A)
        & v2_algstr_1(A)
        & v5_algstr_1(A)
        & l1_rlvect_1(A) )
     => ! [B] : 
          ( m1_subset_1(B,u1_struct_0(A))
         => ! [C] : 
              ( m1_subset_1(C,u1_struct_0(A))
             => ( C = k1_algstr_2(A,B)
              <=> k2_rlvect_1(A,B,C) = k1_rlvect_1(A) ) ) ) ) ),
    file(algstr_2,d7_algstr_2),
    [interesting(0.00)]).

fof(t18_algstr_2,theorem,(
    $true ),
    file(algstr_2,t18_algstr_2),
    [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(t1_algstr_2,theorem,(
    $true ),
    file(algstr_2,t1_algstr_2),
    [interesting(0.00)]).

fof(t20_algstr_2,theorem,(
    $true ),
    file(algstr_2,t20_algstr_2),
    [interesting(0.00)]).

fof(t22_algstr_2,theorem,(
    $true ),
    file(algstr_2,t22_algstr_2),
    [interesting(0.00)]).

fof(t25_algstr_2,theorem,(
    $true ),
    file(algstr_2,t25_algstr_2),
    [interesting(0.00)]).

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(t26_algstr_2,theorem,(
    ! [A] : 
      ( ( ~ v3_struct_0(A)
        & l3_vectsp_1(A) )
     => ( ( ~ v3_struct_0(A)
          & v3_rlvect_1(A)
          & v4_rlvect_1(A)
          & v5_rlvect_1(A)
          & v2_group_1(A)
          & v7_vectsp_1(A)
          & ~ v10_vectsp_1(A)
          & v1_algstr_1(A)
          & v6_algstr_1(A)
          & v11_algstr_1(A)
          & l3_vectsp_1(A) )
      <=> ( ! [B] : 
              ( m1_subset_1(B,u1_struct_0(A))
             => k2_rlvect_1(A,B,k1_rlvect_1(A)) = B )
          & ! [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) ) )
          & ! [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)) ) ) )
          & ! [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) ) )
          & k1_rlvect_1(A) != k2_group_1(A)
          & ! [B] : 
              ( m1_subset_1(B,u1_struct_0(A))
             => k1_group_1(A,B,k2_group_1(A)) = B )
          & ! [B] : 
              ( m1_subset_1(B,u1_struct_0(A))
             => k1_group_1(A,k2_group_1(A),B) = B )
          & ! [B] : 
              ( m1_subset_1(B,u1_struct_0(A))
             => ! [C] : 
                  ( m1_subset_1(C,u1_struct_0(A))
                 => ~ ( B != k1_rlvect_1(A)
                      & ! [D] : 
                          ( m1_subset_1(D,u1_struct_0(A))
                         => k1_group_1(A,B,D) != C ) ) ) )
          & ! [B] : 
              ( m1_subset_1(B,u1_struct_0(A))
             => ! [C] : 
                  ( m1_subset_1(C,u1_struct_0(A))
                 => ~ ( B != k1_rlvect_1(A)
                      & ! [D] : 
                          ( m1_subset_1(D,u1_struct_0(A))
                         => k1_group_1(A,D,B) != C ) ) ) )
          & ! [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,C) = k1_group_1(A,B,D)
                       => ( B = k1_rlvect_1(A)
                          | C = D ) ) ) ) )
          & ! [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,C,B) = k1_group_1(A,D,B)
                       => ( B = k1_rlvect_1(A)
                          | C = D ) ) ) ) )
          & ! [B] : 
              ( m1_subset_1(B,u1_struct_0(A))
             => k1_group_1(A,B,k1_rlvect_1(A)) = k1_rlvect_1(A) )
          & ! [B] : 
              ( m1_subset_1(B,u1_struct_0(A))
             => k1_group_1(A,k1_rlvect_1(A),B) = k1_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))
                     => 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)) ) ) )
          & ! [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)) ) ) ) ) ) ) ),
    inference(mizar_proof,[status(thm)],[t7_algstr_1,t34_algstr_1,d5_rlvect_1,d6_rlvect_1,d7_rlvect_1,d18_vectsp_1,d21_vectsp_1,d13_vectsp_1,d19_vectsp_1,t3_algstr_1,t3_algstr_1,t7_algstr_1,t34_algstr_1,d5_algstr_1,d5_rlvect_1,d6_rlvect_1,d7_rlvect_1,d18_vectsp_1,d21_vectsp_1,d2_group_1]),
    [file(algstr_2,t26_algstr_2),interesting(0.00)]).

fof(t27_algstr_2,theorem,(
    $true ),
    file(algstr_2,t27_algstr_2),
    [interesting(0.00)]).

fof(t28_algstr_2,theorem,(
    $true ),
    file(algstr_2,t28_algstr_2),
    [interesting(0.00)]).

fof(t29_algstr_2,theorem,(
    $true ),
    file(algstr_2,t29_algstr_2),
    [interesting(0.00)]).

fof(t2_algstr_2,theorem,(
    $true ),
    file(algstr_2,t2_algstr_2),
    [interesting(0.00)]).

fof(t30_algstr_2,theorem,(
    $true ),
    file(algstr_2,t30_algstr_2),
    [interesting(0.00)]).

fof(t31_algstr_2,theorem,(
    $true ),
    file(algstr_2,t31_algstr_2),
    [interesting(0.00)]).

fof(t33_algstr_2,theorem,(
    $true ),
    file(algstr_2,t33_algstr_2),
    [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(l43_algstr_2,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))
                     => k1_group_1(A,D,k2_group_1(A)) = D )
                  & ! [D] : 
                      ( m1_subset_1(D,u1_struct_0(A))
                     => ~ ( D != k1_rlvect_1(A)
                          & ! [E] : 
                              ( m1_subset_1(E,u1_struct_0(A))
                             => k1_group_1(A,D,E) != k2_group_1(A) ) ) )
                  & ! [D] : 
                      ( m1_subset_1(D,u1_struct_0(A))
                     => ! [E] : 
                          ( m1_subset_1(E,u1_struct_0(A))
                         => ! [F] : 
                              ( m1_subset_1(F,u1_struct_0(A))
                             => k1_group_1(A,k1_group_1(A,D,E),F) = k1_group_1(A,D,k1_group_1(A,E,F)) ) ) )
                  & ! [D] : 
                      ( m1_subset_1(D,u1_struct_0(A))
                     => k1_group_1(A,D,k1_rlvect_1(A)) = k1_rlvect_1(A) )
                  & ! [D] : 
                      ( m1_subset_1(D,u1_struct_0(A))
                     => k1_group_1(A,k1_rlvect_1(A),D) = k1_rlvect_1(A) )
                  & k1_group_1(A,B,C) = k2_group_1(A) )
               => ( k1_rlvect_1(A) = k2_group_1(A)
                  | k1_group_1(A,C,B) = k2_group_1(A) ) ) ) ) ) ),
    file(algstr_2,l43_algstr_2),
    [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(t3_algstr_2,theorem,(
    $true ),
    file(algstr_2,t3_algstr_2),
    [interesting(0.00)]).

fof(t4_algstr_2,theorem,(
    $true ),
    file(algstr_2,t4_algstr_2),
    [interesting(0.00)]).

fof(t5_algstr_2,theorem,(
    $true ),
    file(algstr_2,t5_algstr_2),
    [interesting(0.00)]).

fof(t6_algstr_2,theorem,(
    $true ),
    file(algstr_2,t6_algstr_2),
    [interesting(0.00)]).

fof(t7_algstr_2,theorem,(
    $true ),
    file(algstr_2,t7_algstr_2),
    [interesting(0.00)]).

fof(t8_algstr_2,theorem,(
    $true ),
    file(algstr_2,t8_algstr_2),
    [interesting(0.00)]).

fof(t9_algstr_2,theorem,(
    $true ),
    file(algstr_2,t9_algstr_2),
    [interesting(0.00)]).