fof(l70_algstr_1,theorem,(
    1 = k2_group_1(k6_algstr_1) ),
    inference(mizar_proof,[status(thm)],[l68_algstr_1,d5_group_1]),
    [file(algstr_1,l70_algstr_1),interesting(1.00)]).

fof(t5_algstr_1,theorem,(
    ! [A] : 
      ( m1_subset_1(A,u1_struct_0(k2_algstr_1))
     => ! [B] : 
          ( m1_subset_1(B,u1_struct_0(k2_algstr_1))
         => A = B ) ) ),
    inference(mizar_proof,[status(thm)],[d1_tarski,d1_tarski]),
    [file(algstr_1,t5_algstr_1),interesting(0.89)]).

fof(t18_algstr_1,theorem,(
    ! [A] : 
      ( m1_subset_1(A,u1_struct_0(k3_algstr_1))
     => ! [B] : 
          ( m1_subset_1(B,u1_struct_0(k3_algstr_1))
         => A = B ) ) ),
    inference(mizar_proof,[status(thm)],[d1_tarski,d1_tarski]),
    [file(algstr_1,t18_algstr_1),interesting(0.88)]).

fof(l94_algstr_1,theorem,(
    ! [A] : 
      ( m1_subset_1(A,u1_struct_0(k6_algstr_1))
     => ! [B] : 
          ( m1_subset_1(B,u1_struct_0(k6_algstr_1))
         => k1_group_1(k6_algstr_1,A,B) = k1_group_1(k6_algstr_1,B,A) ) ) ),
    inference(mizar_proof,[status(thm)],[l67_algstr_1,l67_algstr_1]),
    [file(algstr_1,l94_algstr_1),interesting(0.86)]).

fof(l68_algstr_1,theorem,(
    ! [A] : 
      ( m1_subset_1(A,u1_struct_0(k6_algstr_1))
     => ! [B] : 
          ( m1_subset_1(B,u1_struct_0(k6_algstr_1))
         => ( B = 1
           => ( k1_group_1(k6_algstr_1,A,B) = A
              & k1_group_1(k6_algstr_1,B,A) = A ) ) ) ) ),
    inference(mizar_proof,[status(thm)],[d11_binop_2,d11_binop_2]),
    [file(algstr_1,l68_algstr_1),interesting(0.79)]).

fof(l25_algstr_1,theorem,(
    ! [A] : 
      ( m1_subset_1(A,u1_struct_0(k2_algstr_1))
     => ! [B] : 
          ( m1_subset_1(B,u1_struct_0(k2_algstr_1))
         => k2_rlvect_1(k2_algstr_1,A,B) = k2_rlvect_1(k2_algstr_1,B,A) ) ) ),
    inference(mizar_proof,[status(thm)],[t5_algstr_1]),
    [file(algstr_1,l25_algstr_1),interesting(0.76)]).

fof(l13_algstr_1,theorem,(
    ! [A] : 
      ( m1_subset_1(A,u1_struct_0(k2_algstr_1))
     => ! [B] : 
          ( m1_subset_1(B,u1_struct_0(k2_algstr_1))
         => ? [C] : 
              ( m1_subset_1(C,u1_struct_0(k2_algstr_1))
              & k2_rlvect_1(k2_algstr_1,A,C) = B ) ) ) ),
    inference(mizar_proof,[status(thm)],[t5_algstr_1]),
    [file(algstr_1,l13_algstr_1),interesting(0.75)]).

fof(l14_algstr_1,theorem,(
    ! [A] : 
      ( m1_subset_1(A,u1_struct_0(k2_algstr_1))
     => ! [B] : 
          ( m1_subset_1(B,u1_struct_0(k2_algstr_1))
         => ? [C] : 
              ( m1_subset_1(C,u1_struct_0(k2_algstr_1))
              & k2_rlvect_1(k2_algstr_1,C,A) = B ) ) ) ),
    inference(mizar_proof,[status(thm)],[t5_algstr_1]),
    [file(algstr_1,l14_algstr_1),interesting(0.75)]).

fof(l54_algstr_1,theorem,(
    ! [A] : 
      ( m1_subset_1(A,u1_struct_0(k3_algstr_1))
     => ! [B] : 
          ( m1_subset_1(B,u1_struct_0(k3_algstr_1))
         => k1_group_1(k3_algstr_1,A,B) = k1_group_1(k3_algstr_1,B,A) ) ) ),
    inference(mizar_proof,[status(thm)],[t18_algstr_1]),
    [file(algstr_1,l54_algstr_1),interesting(0.75)]).

fof(l11_algstr_1,theorem,(
    ! [A] : 
      ( m1_subset_1(A,u1_struct_0(k2_algstr_1))
     => k2_rlvect_1(k2_algstr_1,A,k1_rlvect_1(k2_algstr_1)) = A ) ),
    inference(mizar_proof,[status(thm)],[t5_algstr_1]),
    [file(algstr_1,l11_algstr_1),interesting(0.74)]).

fof(l12_algstr_1,theorem,(
    ! [A] : 
      ( m1_subset_1(A,u1_struct_0(k2_algstr_1))
     => k2_rlvect_1(k2_algstr_1,k1_rlvect_1(k2_algstr_1),A) = A ) ),
    inference(mizar_proof,[status(thm)],[t5_algstr_1]),
    [file(algstr_1,l12_algstr_1),interesting(0.74)]).

fof(l41_algstr_1,theorem,(
    ! [A] : 
      ( m1_subset_1(A,u1_struct_0(k3_algstr_1))
     => ! [B] : 
          ( m1_subset_1(B,u1_struct_0(k3_algstr_1))
         => ? [C] : 
              ( m1_subset_1(C,u1_struct_0(k3_algstr_1))
              & k1_group_1(k3_algstr_1,A,C) = B ) ) ) ),
    inference(mizar_proof,[status(thm)],[t18_algstr_1]),
    [file(algstr_1,l41_algstr_1),interesting(0.74)]).

fof(l42_algstr_1,theorem,(
    ! [A] : 
      ( m1_subset_1(A,u1_struct_0(k3_algstr_1))
     => ! [B] : 
          ( m1_subset_1(B,u1_struct_0(k3_algstr_1))
         => ? [C] : 
              ( m1_subset_1(C,u1_struct_0(k3_algstr_1))
              & k1_group_1(k3_algstr_1,C,A) = B ) ) ) ),
    inference(mizar_proof,[status(thm)],[t18_algstr_1]),
    [file(algstr_1,l42_algstr_1),interesting(0.74)]).

fof(l82_algstr_1,theorem,(
    ! [A] : 
      ( m1_subset_1(A,u1_struct_0(k6_algstr_1))
     => k1_group_1(k6_algstr_1,A,k1_rlvect_1(k6_algstr_1)) = k1_rlvect_1(k6_algstr_1) ) ),
    inference(mizar_proof,[status(thm)],[l67_algstr_1]),
    [file(algstr_1,l82_algstr_1),interesting(0.74)]).

fof(l83_algstr_1,theorem,(
    ! [A] : 
      ( m1_subset_1(A,u1_struct_0(k6_algstr_1))
     => k1_group_1(k6_algstr_1,k1_rlvect_1(k6_algstr_1),A) = k1_rlvect_1(k6_algstr_1) ) ),
    inference(mizar_proof,[status(thm)],[l67_algstr_1]),
    [file(algstr_1,l83_algstr_1),interesting(0.74)]).

fof(l39_algstr_1,theorem,(
    ! [A] : 
      ( m1_subset_1(A,u1_struct_0(k3_algstr_1))
     => k1_group_1(k3_algstr_1,A,k2_group_1(k3_algstr_1)) = A ) ),
    inference(mizar_proof,[status(thm)],[t18_algstr_1]),
    [file(algstr_1,l39_algstr_1),interesting(0.73)]).

fof(l40_algstr_1,theorem,(
    ! [A] : 
      ( m1_subset_1(A,u1_struct_0(k3_algstr_1))
     => k1_group_1(k3_algstr_1,k2_group_1(k3_algstr_1),A) = A ) ),
    inference(mizar_proof,[status(thm)],[t18_algstr_1]),
    [file(algstr_1,l40_algstr_1),interesting(0.73)]).

fof(t26_algstr_1,theorem,(
    ! [A] : 
      ( ( ~ v3_struct_0(A)
        & v2_group_1(A)
        & v4_group_1(A)
        & v7_algstr_1(A)
        & v8_algstr_1(A)
        & l1_vectsp_1(A) )
     => ! [B] : 
          ( m1_subset_1(B,u1_struct_0(A))
         => ( k1_group_1(A,B,k4_algstr_1(A,B)) = k2_group_1(A)
            & k1_group_1(A,k4_algstr_1(A,B),B) = k2_group_1(A) ) ) ) ),
    inference(mizar_proof,[status(thm)],[d16_algstr_1,t22_algstr_1,l48_algstr_1]),
    [file(algstr_1,t26_algstr_1),interesting(0.70)]).

fof(t6_algstr_1,theorem,(
    ! [A] : 
      ( m1_subset_1(A,u1_struct_0(k2_algstr_1))
     => ! [B] : 
          ( m1_subset_1(B,u1_struct_0(k2_algstr_1))
         => k2_rlvect_1(k2_algstr_1,A,B) = k1_rlvect_1(k2_algstr_1) ) ) ),
    inference(mizar_proof,[status(thm)],[t5_algstr_1]),
    [file(algstr_1,t6_algstr_1),interesting(0.69)]).

fof(t9_algstr_1,theorem,(
    ! [A] : 
      ( ( ~ v3_struct_0(A)
        & l1_rlvect_1(A) )
     => ( ( ~ v3_struct_0(A)
          & v4_rlvect_1(A)
          & v5_rlvect_1(A)
          & v1_algstr_1(A)
          & v6_algstr_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 )
          & ! [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)) ) ) ) ) ) ) ),
    inference(mizar_proof,[status(thm)],[t7_algstr_1,d6_rlvect_1,d7_rlvect_1,t2_algstr_1,t3_algstr_1,t3_algstr_1,d5_algstr_1,t7_algstr_1,d6_rlvect_1,d7_rlvect_1]),
    [file(algstr_1,t9_algstr_1),interesting(0.68)]).

fof(t19_algstr_1,theorem,(
    ! [A] : 
      ( m1_subset_1(A,u1_struct_0(k3_algstr_1))
     => ! [B] : 
          ( m1_subset_1(B,u1_struct_0(k3_algstr_1))
         => k1_group_1(k3_algstr_1,A,B) = k2_group_1(k3_algstr_1) ) ) ),
    inference(mizar_proof,[status(thm)],[t18_algstr_1]),
    [file(algstr_1,t19_algstr_1),interesting(0.68)]).

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) ) ) ) ) ),
    inference(mizar_proof,[status(thm)],[t88_xcmplx_1]),
    [file(algstr_1,t32_algstr_1),interesting(0.66)]).

fof(t33_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(C,A) ) ) ) ) ),
    inference(mizar_proof,[status(thm)],[t88_xcmplx_1]),
    [file(algstr_1,t33_algstr_1),interesting(0.66)]).

fof(t2_algstr_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,C,k1_rlvect_1(A)) = C )
              & ! [C] : 
                  ( m1_subset_1(C,u1_struct_0(A))
                 => ? [D] : 
                      ( m1_subset_1(D,u1_struct_0(A))
                      & k2_rlvect_1(A,C,D) = k1_rlvect_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))
                         => k2_rlvect_1(A,k2_rlvect_1(A,C,D),E) = k2_rlvect_1(A,C,k2_rlvect_1(A,D,E)) ) ) ) )
           => k2_rlvect_1(A,k1_rlvect_1(A),B) = k2_rlvect_1(A,B,k1_rlvect_1(A)) ) ) ) ),
    inference(mizar_proof,[status(thm)],[t1_algstr_1]),
    [file(algstr_1,t2_algstr_1),interesting(0.62)]).

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) ) ) ) ) ),
    inference(mizar_proof,[status(thm)],[t1_algstr_1]),
    [file(algstr_1,t3_algstr_1),interesting(0.62)]).

fof(l49_algstr_1,theorem,(
    ! [A] : 
      ( ( ~ v3_struct_0(A)
        & l1_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))
                 => ? [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)) ) ) ) )
           => k1_group_1(A,k2_group_1(A),B) = k1_group_1(A,B,k2_group_1(A)) ) ) ) ),
    inference(mizar_proof,[status(thm)],[l48_algstr_1]),
    [file(algstr_1,l49_algstr_1),interesting(0.62)]).

fof(l50_algstr_1,theorem,(
    ! [A] : 
      ( ( ~ v3_struct_0(A)
        & l1_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))
             => ? [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))
           => ? [C] : 
                ( m1_subset_1(C,u1_struct_0(A))
                & k1_group_1(A,C,B) = k2_group_1(A) ) ) ) ) ),
    inference(mizar_proof,[status(thm)],[l48_algstr_1]),
    [file(algstr_1,l50_algstr_1),interesting(0.62)]).

fof(l67_algstr_1,theorem,(
    ! [A] : 
      ( m1_subset_1(A,u1_struct_0(k6_algstr_1))
     => ! [B] : 
          ( m1_subset_1(B,u1_struct_0(k6_algstr_1))
         => ! [C] : 
              ( m1_subset_1(C,k1_numbers)
             => ! [D] : 
                  ( m1_subset_1(D,k1_numbers)
                 => ( ( A = C
                      & B = D )
                   => k1_group_1(k6_algstr_1,A,B) = k11_binop_2(C,D) ) ) ) ) ) ),
    inference(mizar_proof,[status(thm)],[d11_binop_2]),
    [file(algstr_1,l67_algstr_1),interesting(0.58)]).

fof(t22_algstr_1,theorem,(
    ! [A] : 
      ( ( ~ v3_struct_0(A)
        & l1_vectsp_1(A) )
     => ( ( ~ v3_struct_0(A)
          & v2_group_1(A)
          & v4_group_1(A)
          & v7_algstr_1(A)
          & v8_algstr_1(A)
          & l1_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))
             => ? [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)) ) ) ) ) ) ) ),
    inference(mizar_proof,[status(thm)],[d12_algstr_1,d4_group_1,d13_vectsp_1,l49_algstr_1,l50_algstr_1,l50_algstr_1,d12_algstr_1,d13_algstr_1,d4_group_1,d2_group_1]),
    [file(algstr_1,t22_algstr_1),interesting(0.58)]).

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 ) ) ) ) ) ) ) ),
    inference(mizar_proof,[status(thm)],[d10_algstr_1,d9_algstr_1,d8_algstr_1,d6_algstr_1,d7_algstr_1,d6_algstr_1,d7_algstr_1,d8_algstr_1,d9_algstr_1,d10_algstr_1]),
    [file(algstr_1,t7_algstr_1),interesting(0.55)]).

fof(l90_algstr_1,theorem,(
    ! [A] : 
      ( ( ~ v3_struct_0(A)
        & l2_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) ) )
           => ( 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)],[l89_algstr_1]),
    [file(algstr_1,l90_algstr_1),interesting(0.47)]).

fof(l91_algstr_1,theorem,(
    ! [A] : 
      ( ( ~ v3_struct_0(A)
        & l2_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) ) )
       => ( 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)],[l89_algstr_1]),
    [file(algstr_1,l91_algstr_1),interesting(0.46)]).

fof(t36_algstr_1,theorem,(
    ! [A] : 
      ( ( ~ v3_struct_0(A)
        & l2_vectsp_1(A) )
     => ( ( ~ v3_struct_0(A)
          & v2_group_1(A)
          & v4_group_1(A)
          & ~ v10_vectsp_1(A)
          & v11_algstr_1(A)
          & l2_vectsp_1(A) )
      <=> ( 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))
             => ! [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) ) ) ) ) ),
    inference(mizar_proof,[status(thm)],[t34_algstr_1,d4_group_1,d21_vectsp_1,d13_vectsp_1,l90_algstr_1,l91_algstr_1,l91_algstr_1,t34_algstr_1,d4_group_1,d21_vectsp_1,d2_group_1]),
    [file(algstr_1,t36_algstr_1),interesting(0.43)]).

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) ) ) ) ) ),
    inference(mizar_proof,[status(thm)],[d24_algstr_1,d22_algstr_1,d23_algstr_1,d22_algstr_1,d23_algstr_1,d24_algstr_1]),
    [file(algstr_1,t34_algstr_1),interesting(0.34)]).

fof(t11_algstr_1,theorem,(
    ! [A] : 
      ( ( ~ v3_struct_0(A)
        & l1_rlvect_1(A) )
     => ( ( ~ v3_struct_0(A)
          & v3_rlvect_1(A)
          & v4_rlvect_1(A)
          & v5_rlvect_1(A)
          & v1_algstr_1(A)
          & v6_algstr_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 )
          & ! [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) ) ) ) ) ) ),
    inference(mizar_proof,[status(thm)],[t9_algstr_1,d5_rlvect_1]),
    [file(algstr_1,t11_algstr_1),interesting(0.33)]).

fof(t24_algstr_1,theorem,(
    ! [A] : 
      ( ( ~ v3_struct_0(A)
        & l1_vectsp_1(A) )
     => ( ( ~ v3_struct_0(A)
          & v2_group_1(A)
          & v4_group_1(A)
          & v7_group_1(A)
          & v7_algstr_1(A)
          & v8_algstr_1(A)
          & l1_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))
             => ? [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))
             => ! [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)],[t22_algstr_1,d16_group_1]),
    [file(algstr_1,t24_algstr_1),interesting(0.20)]).

fof(t38_algstr_1,theorem,(
    ! [A] : 
      ( ( ~ v3_struct_0(A)
        & l2_vectsp_1(A) )
     => ( ( ~ v3_struct_0(A)
          & v2_group_1(A)
          & v4_group_1(A)
          & v7_group_1(A)
          & ~ v10_vectsp_1(A)
          & v11_algstr_1(A)
          & l2_vectsp_1(A) )
      <=> ( 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))
             => ! [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) )
          & ! [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)],[t36_algstr_1,d16_group_1]),
    [file(algstr_1,t38_algstr_1),interesting(0.04)]).

fof(d1_tarski,definition,(
    ! [A,B] : 
      ( B = k1_tarski(A)
    <=> ! [C] : 
          ( r2_hidden(C,B)
        <=> C = A ) ) ),
    file(tarski,d1_tarski),
    [interesting(0.00)]).

fof(l15_algstr_1,theorem,(
    ! [A] : 
      ( m1_subset_1(A,u1_struct_0(k2_algstr_1))
     => ! [B] : 
          ( m1_subset_1(B,u1_struct_0(k2_algstr_1))
         => ! [C] : 
              ( m1_subset_1(C,u1_struct_0(k2_algstr_1))
             => ( k2_rlvect_1(k2_algstr_1,A,B) = k2_rlvect_1(k2_algstr_1,A,C)
               => B = C ) ) ) ) ),
    inference(mizar_proof,[status(thm)],[t5_algstr_1]),
    [file(algstr_1,l15_algstr_1),interesting(0.00)]).

fof(l16_algstr_1,theorem,(
    ! [A] : 
      ( m1_subset_1(A,u1_struct_0(k2_algstr_1))
     => ! [B] : 
          ( m1_subset_1(B,u1_struct_0(k2_algstr_1))
         => ! [C] : 
              ( m1_subset_1(C,u1_struct_0(k2_algstr_1))
             => ( k2_rlvect_1(k2_algstr_1,B,A) = k2_rlvect_1(k2_algstr_1,C,A)
               => B = C ) ) ) ) ),
    inference(mizar_proof,[status(thm)],[t5_algstr_1]),
    [file(algstr_1,l16_algstr_1),interesting(0.00)]).

fof(l24_algstr_1,theorem,(
    ! [A] : 
      ( m1_subset_1(A,u1_struct_0(k2_algstr_1))
     => ! [B] : 
          ( m1_subset_1(B,u1_struct_0(k2_algstr_1))
         => ! [C] : 
              ( m1_subset_1(C,u1_struct_0(k2_algstr_1))
             => k2_rlvect_1(k2_algstr_1,k2_rlvect_1(k2_algstr_1,A,B),C) = k2_rlvect_1(k2_algstr_1,A,k2_rlvect_1(k2_algstr_1,B,C)) ) ) ) ),
    inference(mizar_proof,[status(thm)],[t5_algstr_1]),
    [file(algstr_1,l24_algstr_1),interesting(0.00)]).

fof(l43_algstr_1,theorem,(
    ! [A] : 
      ( m1_subset_1(A,u1_struct_0(k3_algstr_1))
     => ! [B] : 
          ( m1_subset_1(B,u1_struct_0(k3_algstr_1))
         => ! [C] : 
              ( m1_subset_1(C,u1_struct_0(k3_algstr_1))
             => ( k1_group_1(k3_algstr_1,A,B) = k1_group_1(k3_algstr_1,A,C)
               => B = C ) ) ) ) ),
    inference(mizar_proof,[status(thm)],[t18_algstr_1]),
    [file(algstr_1,l43_algstr_1),interesting(0.00)]).

fof(l44_algstr_1,theorem,(
    ! [A] : 
      ( m1_subset_1(A,u1_struct_0(k3_algstr_1))
     => ! [B] : 
          ( m1_subset_1(B,u1_struct_0(k3_algstr_1))
         => ! [C] : 
              ( m1_subset_1(C,u1_struct_0(k3_algstr_1))
             => ( k1_group_1(k3_algstr_1,B,A) = k1_group_1(k3_algstr_1,C,A)
               => B = C ) ) ) ) ),
    inference(mizar_proof,[status(thm)],[t18_algstr_1]),
    [file(algstr_1,l44_algstr_1),interesting(0.00)]).

fof(l47_algstr_1,theorem,(
    ! [A] : 
      ( m1_subset_1(A,u1_struct_0(k3_algstr_1))
     => ! [B] : 
          ( m1_subset_1(B,u1_struct_0(k3_algstr_1))
         => ! [C] : 
              ( m1_subset_1(C,u1_struct_0(k3_algstr_1))
             => k1_group_1(k3_algstr_1,k1_group_1(k3_algstr_1,A,B),C) = k1_group_1(k3_algstr_1,A,k1_group_1(k3_algstr_1,B,C)) ) ) ) ),
    inference(mizar_proof,[status(thm)],[t18_algstr_1]),
    [file(algstr_1,l47_algstr_1),interesting(0.00)]).

fof(l69_algstr_1,theorem,(
    0 = k1_rlvect_1(k6_algstr_1) ),
    file(algstr_1,l69_algstr_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(t88_xcmplx_1,theorem,(
    ! [A] : 
      ( v1_xcmplx_0(A)
     => ! [B] : 
          ( v1_xcmplx_0(B)
         => ( A != 0
           => k3_xcmplx_0(k7_xcmplx_0(B,A),A) = B ) ) ) ),
    file(xcmplx_1,t88_xcmplx_1),
    [interesting(0.00)]).

fof(l78_algstr_1,theorem,(
    ! [A] : 
      ( m1_subset_1(A,u1_struct_0(k6_algstr_1))
     => ! [B] : 
          ( m1_subset_1(B,u1_struct_0(k6_algstr_1))
         => ~ ( A != k1_rlvect_1(k6_algstr_1)
              & ! [C] : 
                  ( m1_subset_1(C,u1_struct_0(k6_algstr_1))
                 => k1_group_1(k6_algstr_1,A,C) != B ) ) ) ) ),
    inference(mizar_proof,[status(thm)],[t32_algstr_1,l67_algstr_1]),
    [file(algstr_1,l78_algstr_1),interesting(0.00)]).

fof(l79_algstr_1,theorem,(
    ! [A] : 
      ( m1_subset_1(A,u1_struct_0(k6_algstr_1))
     => ! [B] : 
          ( m1_subset_1(B,u1_struct_0(k6_algstr_1))
         => ~ ( A != k1_rlvect_1(k6_algstr_1)
              & ! [C] : 
                  ( m1_subset_1(C,u1_struct_0(k6_algstr_1))
                 => k1_group_1(k6_algstr_1,C,A) != B ) ) ) ) ),
    inference(mizar_proof,[status(thm)],[t33_algstr_1,l67_algstr_1]),
    [file(algstr_1,l79_algstr_1),interesting(0.00)]).

fof(t5_xcmplx_1,theorem,(
    ! [A] : 
      ( v1_xcmplx_0(A)
     => ! [B] : 
          ( v1_xcmplx_0(B)
         => ! [C] : 
              ( v1_xcmplx_0(C)
             => ( k3_xcmplx_0(B,A) = k3_xcmplx_0(C,A)
               => ( A = 0
                  | B = C ) ) ) ) ) ),
    file(xcmplx_1,t5_xcmplx_1),
    [interesting(0.00)]).

fof(l80_algstr_1,theorem,(
    ! [A] : 
      ( m1_subset_1(A,u1_struct_0(k6_algstr_1))
     => ! [B] : 
          ( m1_subset_1(B,u1_struct_0(k6_algstr_1))
         => ! [C] : 
              ( m1_subset_1(C,u1_struct_0(k6_algstr_1))
             => ( k1_group_1(k6_algstr_1,A,B) = k1_group_1(k6_algstr_1,A,C)
               => ( A = k1_rlvect_1(k6_algstr_1)
                  | B = C ) ) ) ) ) ),
    inference(mizar_proof,[status(thm)],[l67_algstr_1,l67_algstr_1,t5_xcmplx_1]),
    [file(algstr_1,l80_algstr_1),interesting(0.00)]).

fof(l81_algstr_1,theorem,(
    ! [A] : 
      ( m1_subset_1(A,u1_struct_0(k6_algstr_1))
     => ! [B] : 
          ( m1_subset_1(B,u1_struct_0(k6_algstr_1))
         => ! [C] : 
              ( m1_subset_1(C,u1_struct_0(k6_algstr_1))
             => ( k1_group_1(k6_algstr_1,B,A) = k1_group_1(k6_algstr_1,C,A)
               => ( A = k1_rlvect_1(k6_algstr_1)
                  | B = C ) ) ) ) ) ),
    inference(mizar_proof,[status(thm)],[l67_algstr_1,l67_algstr_1,t5_xcmplx_1]),
    [file(algstr_1,l81_algstr_1),interesting(0.00)]).

fof(l88_algstr_1,theorem,(
    ! [A] : 
      ( m1_subset_1(A,u1_struct_0(k6_algstr_1))
     => ! [B] : 
          ( m1_subset_1(B,u1_struct_0(k6_algstr_1))
         => ! [C] : 
              ( m1_subset_1(C,u1_struct_0(k6_algstr_1))
             => k1_group_1(k6_algstr_1,k1_group_1(k6_algstr_1,A,B),C) = k1_group_1(k6_algstr_1,A,k1_group_1(k6_algstr_1,B,C)) ) ) ) ),
    inference(mizar_proof,[status(thm)],[l67_algstr_1,l67_algstr_1,l67_algstr_1,l67_algstr_1]),
    [file(algstr_1,l88_algstr_1),interesting(0.00)]).

fof(t10_algstr_1,theorem,(
    $true ),
    file(algstr_1,t10_algstr_1),
    [interesting(0.00)]).

fof(d10_algstr_1,definition,(
    ! [A] : 
      ( ( ~ v3_struct_0(A)
        & l1_rlvect_1(A) )
     => ( v6_algstr_1(A)
      <=> ( v2_algstr_1(A)
          & v3_algstr_1(A)
          & v4_algstr_1(A)
          & v5_algstr_1(A) ) ) ) ),
    file(algstr_1,d10_algstr_1),
    [interesting(0.00)]).

fof(d9_algstr_1,definition,(
    ! [A] : 
      ( ( ~ v3_struct_0(A)
        & l1_rlvect_1(A) )
     => ( v5_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 ) ) ) ) ) ),
    file(algstr_1,d9_algstr_1),
    [interesting(0.00)]).

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

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

fof(d7_algstr_1,definition,(
    ! [A] : 
      ( ( ~ v3_struct_0(A)
        & l1_rlvect_1(A) )
     => ( v3_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,C,B) = k2_rlvect_1(A,D,B)
                     => C = D ) ) ) ) ) ) ),
    file(algstr_1,d7_algstr_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(t1_algstr_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,D,k1_rlvect_1(A)) = D )
                  & ! [D] : 
                      ( m1_subset_1(D,u1_struct_0(A))
                     => ? [E] : 
                          ( m1_subset_1(E,u1_struct_0(A))
                          & k2_rlvect_1(A,D,E) = k1_rlvect_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))
                             => k2_rlvect_1(A,k2_rlvect_1(A,D,E),F) = k2_rlvect_1(A,D,k2_rlvect_1(A,E,F)) ) ) )
                  & k2_rlvect_1(A,B,C) = k1_rlvect_1(A) )
               => k2_rlvect_1(A,C,B) = k1_rlvect_1(A) ) ) ) ) ),
    file(algstr_1,t1_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(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(t12_algstr_1,theorem,(
    $true ),
    file(algstr_1,t12_algstr_1),
    [interesting(0.00)]).

fof(t13_algstr_1,theorem,(
    $true ),
    file(algstr_1,t13_algstr_1),
    [interesting(0.00)]).

fof(t14_algstr_1,theorem,(
    $true ),
    file(algstr_1,t14_algstr_1),
    [interesting(0.00)]).

fof(t15_algstr_1,theorem,(
    $true ),
    file(algstr_1,t15_algstr_1),
    [interesting(0.00)]).

fof(t16_algstr_1,theorem,(
    $true ),
    file(algstr_1,t16_algstr_1),
    [interesting(0.00)]).

fof(t17_algstr_1,theorem,(
    $true ),
    file(algstr_1,t17_algstr_1),
    [interesting(0.00)]).

fof(t20_algstr_1,theorem,(
    $true ),
    file(algstr_1,t20_algstr_1),
    [interesting(0.00)]).

fof(t21_algstr_1,theorem,(
    $true ),
    file(algstr_1,t21_algstr_1),
    [interesting(0.00)]).

fof(t23_algstr_1,theorem,(
    $true ),
    file(algstr_1,t23_algstr_1),
    [interesting(0.00)]).

fof(d12_algstr_1,definition,(
    ! [A] : 
      ( ( ~ v3_struct_0(A)
        & l1_vectsp_1(A) )
     => ( v7_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))
                      & 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))
                 => ? [D] : 
                      ( m1_subset_1(D,u1_struct_0(A))
                      & k1_group_1(A,D,B) = C ) ) ) ) ) ) ),
    file(algstr_1,d12_algstr_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(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(l48_algstr_1,theorem,(
    ! [A] : 
      ( ( ~ v3_struct_0(A)
        & l1_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))
                     => ? [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)) ) ) )
                  & k1_group_1(A,B,C) = k2_group_1(A) )
               => k1_group_1(A,C,B) = k2_group_1(A) ) ) ) ) ),
    file(algstr_1,l48_algstr_1),
    [interesting(0.00)]).

fof(d13_algstr_1,definition,(
    ! [A] : 
      ( ( ~ v3_struct_0(A)
        & l1_vectsp_1(A) )
     => ( v8_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))
                     => ( k1_group_1(A,B,C) = k1_group_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))
                     => ( k1_group_1(A,C,B) = k1_group_1(A,D,B)
                       => C = D ) ) ) ) ) ) ) ),
    file(algstr_1,d13_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(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(t25_algstr_1,theorem,(
    $true ),
    file(algstr_1,t25_algstr_1),
    [interesting(0.00)]).

fof(d16_algstr_1,definition,(
    ! [A] : 
      ( ( ~ v3_struct_0(A)
        & v7_algstr_1(A)
        & v8_algstr_1(A)
        & l1_vectsp_1(A) )
     => ! [B] : 
          ( m1_subset_1(B,u1_struct_0(A))
         => ! [C] : 
              ( m1_subset_1(C,u1_struct_0(A))
             => ( C = k4_algstr_1(A,B)
              <=> k1_group_1(A,B,C) = k2_group_1(A) ) ) ) ) ),
    file(algstr_1,d16_algstr_1),
    [interesting(0.00)]).

fof(t27_algstr_1,theorem,(
    $true ),
    file(algstr_1,t27_algstr_1),
    [interesting(0.00)]).

fof(t28_algstr_1,theorem,(
    $true ),
    file(algstr_1,t28_algstr_1),
    [interesting(0.00)]).

fof(t29_algstr_1,theorem,(
    $true ),
    file(algstr_1,t29_algstr_1),
    [interesting(0.00)]).

fof(t30_algstr_1,theorem,(
    $true ),
    file(algstr_1,t30_algstr_1),
    [interesting(0.00)]).

fof(t31_algstr_1,theorem,(
    $true ),
    file(algstr_1,t31_algstr_1),
    [interesting(0.00)]).

fof(t35_algstr_1,theorem,(
    $true ),
    file(algstr_1,t35_algstr_1),
    [interesting(0.00)]).

fof(t37_algstr_1,theorem,(
    $true ),
    file(algstr_1,t37_algstr_1),
    [interesting(0.00)]).

fof(d24_algstr_1,definition,(
    ! [A] : 
      ( ( ~ v3_struct_0(A)
        & l2_vectsp_1(A) )
     => ( v11_algstr_1(A)
      <=> ( v9_algstr_1(A)
          & v10_algstr_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) ) ) ) ) ),
    file(algstr_1,d24_algstr_1),
    [interesting(0.00)]).

fof(d22_algstr_1,definition,(
    ! [A] : 
      ( ( ~ v3_struct_0(A)
        & l2_vectsp_1(A) )
     => ( v9_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 ) ) ) ) ) ) ) ),
    file(algstr_1,d22_algstr_1),
    [interesting(0.00)]).

fof(d23_algstr_1,definition,(
    ! [A] : 
      ( ( ~ v3_struct_0(A)
        & l2_vectsp_1(A) )
     => ( v10_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))
                     => ( 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 ) ) ) ) ) ) ) ) ),
    file(algstr_1,d23_algstr_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(l89_algstr_1,theorem,(
    ! [A] : 
      ( ( ~ v3_struct_0(A)
        & l2_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) )
                  & 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_1,l89_algstr_1),
    [interesting(0.00)]).

fof(t39_algstr_1,theorem,(
    $true ),
    file(algstr_1,t39_algstr_1),
    [interesting(0.00)]).

fof(d25_algstr_1,definition,(
    ! [A] : 
      ( ( ~ v3_struct_0(A)
        & v9_algstr_1(A)
        & v10_algstr_1(A)
        & l2_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 = k7_algstr_1(A,B)
                <=> k1_group_1(A,B,C) = k2_group_1(A) ) ) ) ) ) ),
    file(algstr_1,d25_algstr_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(t40_algstr_1,theorem,(
    ! [A] : 
      ( ( ~ v3_struct_0(A)
        & v2_group_1(A)
        & v4_group_1(A)
        & v9_algstr_1(A)
        & v10_algstr_1(A)
        & l2_vectsp_1(A) )
     => ! [B] : 
          ( m1_subset_1(B,u1_struct_0(A))
         => ( B != k1_rlvect_1(A)
           => ( k1_group_1(A,B,k7_algstr_1(A,B)) = k2_group_1(A)
              & k1_group_1(A,k7_algstr_1(A,B),B) = k2_group_1(A) ) ) ) ) ),
    inference(mizar_proof,[status(thm)],[d25_algstr_1,d22_algstr_1,d4_group_1,d13_vectsp_1,d19_vectsp_1]),
    [file(algstr_1,t40_algstr_1),interesting(0.00)]).

fof(t4_algstr_1,theorem,(
    $true ),
    file(algstr_1,t4_algstr_1),
    [interesting(0.00)]).

fof(t8_algstr_1,theorem,(
    $true ),
    file(algstr_1,t8_algstr_1),
    [interesting(0.00)]).