fof(t67_group_1,theorem,(
    ! [A] : 
      ( v1_int_1(A)
     => ! [B] : 
          ( v1_int_1(B)
         => ! [C] : 
              ( ( ~ v3_struct_0(C)
                & v3_group_1(C)
                & v4_group_1(C)
                & l1_group_1(C) )
             => ! [D] : 
                  ( m1_subset_1(D,u1_struct_0(C))
                 => k6_group_1(C,k3_xcmplx_0(A,B),D) = k6_group_1(C,B,k6_group_1(C,A,D)) ) ) ) ) ),
    inference(mizar_proof,[status(thm)],[t16_int_1,t50_group_1,t26_xreal_1,t16_int_1,l76_group_1,l85_group_1,t50_group_1,l85_group_1,l76_group_1,l85_group_1,t19_group_1,t26_xreal_1,t16_int_1,l76_group_1,l85_group_1,t50_group_1,l76_group_1,l85_group_1,t19_group_1,t26_xreal_1,t16_int_1,t50_group_1,l76_group_1,l76_group_1,l85_group_1,l85_group_1,l85_group_1,t19_group_1]),
    [file(group_1,t67_group_1),interesting(1.00)]).

fof(t36_group_1,theorem,(
    ! [A] : 
      ( ( ~ v3_struct_0(A)
        & v3_group_1(A)
        & v4_group_1(A)
        & l1_group_1(A) )
     => v1_finseqop(u1_group_1(A),u1_struct_0(A)) ) ),
    inference(mizar_proof,[status(thm)],[t35_group_1,d2_finseqop]),
    [file(group_1,t36_group_1),interesting(0.94)]).

fof(t79_group_1,theorem,(
    ! [A] : 
      ( ( ~ v3_struct_0(A)
        & v3_group_1(A)
        & v4_group_1(A)
        & l1_group_1(A) )
     => ~ v5_group_1(k2_group_1(A),A) ) ),
    inference(mizar_proof,[status(thm)],[t42_group_1,d11_group_1]),
    [file(group_1,t79_group_1),interesting(0.92)]).

fof(t16_group_1,theorem,(
    ! [A] : 
      ( ( ~ v3_struct_0(A)
        & v3_group_1(A)
        & v4_group_1(A)
        & l1_group_1(A) )
     => k3_group_1(A,k2_group_1(A)) = k2_group_1(A) ) ),
    inference(mizar_proof,[status(thm)],[d5_group_1,d6_group_1,t14_group_1]),
    [file(group_1,t16_group_1),interesting(0.86)]).

fof(t35_group_1,theorem,(
    ! [A] : 
      ( ( ~ v3_struct_0(A)
        & v3_group_1(A)
        & v4_group_1(A)
        & l1_group_1(A) )
     => r1_finseqop(u1_struct_0(A),k4_group_1(A),u1_group_1(A)) ) ),
    inference(mizar_proof,[status(thm)],[d1_finseqop,d7_group_1,d6_group_1,t33_group_1,d7_group_1,d6_group_1,t33_group_1]),
    [file(group_1,t35_group_1),interesting(0.86)]).

fof(t31_group_1,theorem,(
    ! [A] : 
      ( ( ~ v3_struct_0(A)
        & v4_group_1(A)
        & l1_group_1(A) )
     => v2_binop_1(u1_group_1(A),u1_struct_0(A)) ) ),
    inference(mizar_proof,[status(thm)],[d14_binop_1,d4_group_1]),
    [file(group_1,t31_group_1),interesting(0.84)]).

fof(t34_group_1,theorem,(
    ! [A] : 
      ( ( ~ v3_struct_0(A)
        & v2_group_1(A)
        & l1_group_1(A) )
     => v1_setwiseo(u1_group_1(A),u1_struct_0(A)) ) ),
    inference(mizar_proof,[status(thm)],[d2_setwiseo,t32_group_1]),
    [file(group_1,t34_group_1),interesting(0.84)]).

fof(t37_group_1,theorem,(
    ! [A] : 
      ( ( ~ v3_struct_0(A)
        & v3_group_1(A)
        & v4_group_1(A)
        & l1_group_1(A) )
     => k6_finseqop(u1_struct_0(A),u1_group_1(A)) = k4_group_1(A) ) ),
    inference(mizar_proof,[status(thm)],[t31_group_1,t34_group_1,t35_group_1,t36_group_1,d3_finseqop]),
    [file(group_1,t37_group_1),interesting(0.83)]).

fof(l77_group_1,theorem,(
    ! [A] : 
      ( v1_int_1(A)
     => ~ ( ~ r1_xreal_0(1,A)
          & A != 0
          & r1_xreal_0(0,A) ) ) ),
    inference(mizar_proof,[status(thm)],[t16_int_1,t39_nat_1]),
    [file(group_1,l77_group_1),interesting(0.77)]).

fof(t32_group_1,theorem,(
    ! [A] : 
      ( ( ~ v3_struct_0(A)
        & v2_group_1(A)
        & l1_group_1(A) )
     => r3_binop_1(u1_struct_0(A),k2_group_1(A),u1_group_1(A)) ) ),
    inference(mizar_proof,[status(thm)],[d5_group_1,d5_group_1,t11_binop_1]),
    [file(group_1,t32_group_1),interesting(0.76)]).

fof(t63_group_1,theorem,(
    ! [A] : 
      ( v1_int_1(A)
     => ! [B] : 
          ( v1_int_1(B)
         => ! [C] : 
              ( ( ~ v3_struct_0(C)
                & v3_group_1(C)
                & v4_group_1(C)
                & l1_group_1(C) )
             => ! [D] : 
                  ( m1_subset_1(D,u1_struct_0(C))
                 => k6_group_1(C,k2_xcmplx_0(A,B),D) = k1_group_1(C,k6_group_1(C,A,D),k6_group_1(C,B,D)) ) ) ) ) ),
    inference(mizar_proof,[status(thm)],[d5_group_1,l50_group_1,l78_group_1,d4_group_1,l80_group_1,d4_group_1,s4_int_1]),
    [file(group_1,t63_group_1),interesting(0.76)]).

fof(t68_group_1,theorem,(
    ! [A] : 
      ( m2_subset_1(A,k1_numbers,k5_numbers)
     => ! [B] : 
          ( v1_int_1(B)
         => ! [C] : 
              ( ( ~ v3_struct_0(C)
                & v3_group_1(C)
                & v4_group_1(C)
                & l1_group_1(C) )
             => ! [D] : 
                  ( m1_subset_1(D,u1_struct_0(C))
                 => k6_group_1(C,k3_xcmplx_0(A,B),D) = k6_group_1(C,B,k6_group_1(C,A,D)) ) ) ) ) ),
    inference(mizar_proof,[status(thm)],[t67_group_1]),
    [file(group_1,t68_group_1),interesting(0.76)]).

fof(t69_group_1,theorem,(
    ! [A] : 
      ( m2_subset_1(A,k1_numbers,k5_numbers)
     => ! [B] : 
          ( v1_int_1(B)
         => ! [C] : 
              ( ( ~ v3_struct_0(C)
                & v3_group_1(C)
                & v4_group_1(C)
                & l1_group_1(C) )
             => ! [D] : 
                  ( m1_subset_1(D,u1_struct_0(C))
                 => k6_group_1(C,k3_xcmplx_0(B,A),D) = k6_group_1(C,A,k6_group_1(C,B,D)) ) ) ) ) ),
    inference(mizar_proof,[status(thm)],[t67_group_1]),
    [file(group_1,t69_group_1),interesting(0.76)]).

fof(t33_group_1,theorem,(
    ! [A] : 
      ( ( ~ v3_struct_0(A)
        & v2_group_1(A)
        & l1_group_1(A) )
     => k3_binop_1(u1_struct_0(A),u1_group_1(A)) = k2_group_1(A) ) ),
    inference(mizar_proof,[status(thm)],[t32_group_1,d8_binop_1]),
    [file(group_1,t33_group_1),interesting(0.75)]).

fof(t84_group_1,theorem,(
    ! [A] : 
      ( ( ~ v3_struct_0(A)
        & v3_group_1(A)
        & v4_group_1(A)
        & l1_group_1(A) )
     => k7_group_1(A,k2_group_1(A)) = 1 ) ),
    inference(mizar_proof,[status(thm)],[t79_group_1,t42_group_1,t39_nat_1,d12_group_1]),
    [file(group_1,t84_group_1),interesting(0.75)]).

fof(t19_group_1,theorem,(
    ! [A] : 
      ( ( ~ v3_struct_0(A)
        & v3_group_1(A)
        & v4_group_1(A)
        & l1_group_1(A) )
     => ! [B] : 
          ( m1_subset_1(B,u1_struct_0(A))
         => k3_group_1(A,k3_group_1(A,B)) = B ) ) ),
    inference(mizar_proof,[status(thm)],[d6_group_1,t14_group_1]),
    [file(group_1,t19_group_1),interesting(0.74)]).

fof(l79_group_1,theorem,(
    ! [A] : 
      ( v1_int_1(A)
     => ~ ( ~ r1_xreal_0(0,A)
          & A != k7_binop_2(1)
          & r1_xreal_0(k7_binop_2(1),A) ) ) ),
    inference(mizar_proof,[status(thm)],[t26_xreal_1,t16_int_1,t39_nat_1,d5_real_1,t26_xreal_1]),
    [file(group_1,l79_group_1),interesting(0.73)]).

fof(l85_group_1,theorem,(
    ! [A] : 
      ( v1_int_1(A)
     => ! [B] : 
          ( ( ~ v3_struct_0(B)
            & v3_group_1(B)
            & v4_group_1(B)
            & l1_group_1(B) )
         => ! [C] : 
              ( m1_subset_1(C,u1_struct_0(B))
             => k6_group_1(B,A,k3_group_1(B,C)) = k3_group_1(B,k6_group_1(B,A,C)) ) ) ) ),
    inference(mizar_proof,[status(thm)],[t16_int_1,t51_group_1,t56_group_1,t51_group_1,t19_group_1,t19_group_1,t56_group_1]),
    [file(group_1,l85_group_1),interesting(0.72)]).

fof(t61_group_1,theorem,(
    ! [A] : 
      ( v1_int_1(A)
     => ! [B] : 
          ( ( ~ v3_struct_0(B)
            & v3_group_1(B)
            & v4_group_1(B)
            & l1_group_1(B) )
         => k6_group_1(B,A,k2_group_1(B)) = k2_group_1(B) ) ) ),
    inference(mizar_proof,[status(thm)],[t16_group_1,t55_group_1,t56_group_1,t42_group_1]),
    [file(group_1,t61_group_1),interesting(0.71)]).

fof(t17_group_1,theorem,(
    ! [A] : 
      ( ( ~ v3_struct_0(A)
        & v3_group_1(A)
        & v4_group_1(A)
        & l1_group_1(A) )
     => ! [B] : 
          ( m1_subset_1(B,u1_struct_0(A))
         => ! [C] : 
              ( m1_subset_1(C,u1_struct_0(A))
             => ( k3_group_1(A,B) = k3_group_1(A,C)
               => B = C ) ) ) ) ),
    inference(mizar_proof,[status(thm)],[d6_group_1,t14_group_1]),
    [file(group_1,t17_group_1),interesting(0.69)]).

fof(t7_group_1,theorem,
    ( v4_group_1(g1_group_1(k1_numbers,k33_binop_2))
    & v3_group_1(g1_group_1(k1_numbers,k33_binop_2)) ),
    inference(mizar_proof,[status(thm)],[d9_binop_2,d4_group_1,d3_group_1]),
    [file(group_1,t7_group_1),interesting(0.67)]).

fof(l76_group_1,theorem,(
    ! [A] : 
      ( v1_int_1(A)
     => ! [B] : 
          ( ( ~ v3_struct_0(B)
            & v3_group_1(B)
            & v4_group_1(B)
            & l1_group_1(B) )
         => ! [C] : 
              ( m1_subset_1(C,u1_struct_0(B))
             => k6_group_1(B,k4_xcmplx_0(A),C) = k3_group_1(B,k6_group_1(B,A,C)) ) ) ) ),
    inference(mizar_proof,[status(thm)],[t56_group_1,d1_absvalue,l50_group_1,t16_group_1,l50_group_1,t26_xreal_1,t56_group_1,t19_group_1,d1_absvalue]),
    [file(group_1,l76_group_1),interesting(0.67)]).

fof(t44_group_1,theorem,(
    ! [A] : 
      ( ( ~ v3_struct_0(A)
        & v3_group_1(A)
        & v4_group_1(A)
        & l1_group_1(A) )
     => ! [B] : 
          ( m1_subset_1(B,u1_struct_0(A))
         => k6_group_1(A,1,B) = B ) ) ),
    inference(mizar_proof,[status(thm)],[l49_group_1,l50_group_1,d5_group_1]),
    [file(group_1,t44_group_1),interesting(0.66)]).

fof(t82_group_1,theorem,(
    ! [A] : 
      ( ( ~ v3_struct_0(A)
        & v3_group_1(A)
        & v4_group_1(A)
        & l1_group_1(A) )
     => ! [B] : 
          ( m1_subset_1(B,u1_struct_0(A))
         => k6_group_1(A,k7_group_1(A,B),B) = k2_group_1(A) ) ) ),
    inference(mizar_proof,[status(thm)],[d12_group_1,l50_group_1,d12_group_1]),
    [file(group_1,t82_group_1),interesting(0.66)]).

fof(t45_group_1,theorem,(
    ! [A] : 
      ( ( ~ v3_struct_0(A)
        & v3_group_1(A)
        & v4_group_1(A)
        & l1_group_1(A) )
     => ! [B] : 
          ( m1_subset_1(B,u1_struct_0(A))
         => k6_group_1(A,2,B) = k1_group_1(A,B,B) ) ) ),
    inference(mizar_proof,[status(thm)],[l49_group_1,t44_group_1]),
    [file(group_1,t45_group_1),interesting(0.65)]).

fof(t42_group_1,theorem,(
    ! [A] : 
      ( m2_subset_1(A,k1_numbers,k5_numbers)
     => ! [B] : 
          ( ( ~ v3_struct_0(B)
            & v3_group_1(B)
            & v4_group_1(B)
            & l1_group_1(B) )
         => k6_group_1(B,A,k2_group_1(B)) = k2_group_1(B) ) ) ),
    inference(mizar_proof,[status(thm)],[l50_group_1,l49_group_1,d5_group_1,s1_nat_1]),
    [file(group_1,t42_group_1),interesting(0.65)]).

fof(l80_group_1,theorem,(
    ! [A] : 
      ( v1_int_1(A)
     => ! [B] : 
          ( ( ~ v3_struct_0(B)
            & v3_group_1(B)
            & v4_group_1(B)
            & l1_group_1(B) )
         => ! [C] : 
              ( m1_subset_1(C,u1_struct_0(B))
             => k6_group_1(B,k2_xcmplx_0(A,1),C) = k1_group_1(B,k6_group_1(B,A,C),k6_group_1(B,1,C)) ) ) ) ),
    inference(mizar_proof,[status(thm)],[t16_int_1,d1_absvalue,t55_group_1,t62_group_1,l76_group_1,t55_group_1,t25_group_1,t49_group_1,d1_absvalue,d6_group_1,t8_xreal_1,t56_group_1,t62_group_1,d4_group_1,t25_group_1,t49_group_1,d1_absvalue,d6_group_1,l50_group_1,d5_group_1,t62_group_1,l76_group_1,t62_group_1,d6_group_1,l79_group_1,l76_group_1,d6_group_1,t14_group_1,l76_group_1,t25_group_1,l76_group_1,l76_group_1]),
    [file(group_1,l80_group_1),interesting(0.64)]).

fof(t62_group_1,theorem,(
    ! [A] : 
      ( ( ~ v3_struct_0(A)
        & v3_group_1(A)
        & v4_group_1(A)
        & l1_group_1(A) )
     => ! [B] : 
          ( m1_subset_1(B,u1_struct_0(A))
         => k6_group_1(A,k7_binop_2(1),B) = k3_group_1(A,B) ) ) ),
    inference(mizar_proof,[status(thm)],[d1_absvalue,t56_group_1,t44_group_1]),
    [file(group_1,t62_group_1),interesting(0.62)]).

fof(l50_group_1,theorem,(
    ! [A] : 
      ( ( ~ v3_struct_0(A)
        & v3_group_1(A)
        & v4_group_1(A)
        & l1_group_1(A) )
     => ! [B] : 
          ( m1_subset_1(B,u1_struct_0(A))
         => k6_group_1(A,0,B) = k2_group_1(A) ) ) ),
    inference(mizar_proof,[status(thm)],[d8_group_1]),
    [file(group_1,l50_group_1),interesting(0.60)]).

fof(t51_group_1,theorem,(
    ! [A] : 
      ( m2_subset_1(A,k1_numbers,k5_numbers)
     => ! [B] : 
          ( ( ~ v3_struct_0(B)
            & v3_group_1(B)
            & v4_group_1(B)
            & l1_group_1(B) )
         => ! [C] : 
              ( m1_subset_1(C,u1_struct_0(B))
             => k6_group_1(B,A,k3_group_1(B,C)) = k3_group_1(B,k6_group_1(B,A,C)) ) ) ) ),
    inference(mizar_proof,[status(thm)],[l50_group_1,t16_group_1,l50_group_1,l49_group_1,t25_group_1,t49_group_1,s1_nat_1]),
    [file(group_1,t51_group_1),interesting(0.57)]).

fof(t72_group_1,theorem,(
    ! [A] : 
      ( v1_int_1(A)
     => ! [B] : 
          ( ( ~ v3_struct_0(B)
            & v3_group_1(B)
            & v4_group_1(B)
            & l1_group_1(B) )
         => ! [C] : 
              ( m1_subset_1(C,u1_struct_0(B))
             => k6_group_1(B,A,k3_group_1(B,C)) = k3_group_1(B,k6_group_1(B,A,C)) ) ) ) ),
    inference(mizar_proof,[status(thm)],[l85_group_1]),
    [file(group_1,t72_group_1),interesting(0.57)]).

fof(t18_group_1,theorem,(
    ! [A] : 
      ( ( ~ v3_struct_0(A)
        & v3_group_1(A)
        & v4_group_1(A)
        & l1_group_1(A) )
     => ! [B] : 
          ( m1_subset_1(B,u1_struct_0(A))
         => ( k3_group_1(A,B) = k2_group_1(A)
           => B = k2_group_1(A) ) ) ) ),
    inference(mizar_proof,[status(thm)],[t16_group_1,t17_group_1]),
    [file(group_1,t18_group_1),interesting(0.56)]).

fof(t60_group_1,theorem,(
    ! [A] : 
      ( v1_int_1(A)
     => ! [B] : 
          ( ( ~ v3_struct_0(B)
            & v3_group_1(B)
            & v4_group_1(B)
            & l1_group_1(B) )
         => ! [C] : 
              ( m1_subset_1(C,u1_struct_0(B))
             => ( r1_xreal_0(A,0)
               => k6_group_1(B,A,C) = k3_group_1(B,k6_group_1(B,k1_int_2(A),C)) ) ) ) ) ),
    inference(mizar_proof,[status(thm)],[t56_group_1,l50_group_1,t16_group_1,l50_group_1,d1_absvalue]),
    [file(group_1,t60_group_1),interesting(0.54)]).

fof(t90_group_1,theorem,(
    ! [A] : 
      ( ( ~ v3_struct_0(A)
        & v3_group_1(A)
        & v4_group_1(A)
        & l1_group_1(A) )
     => ( v6_group_1(A)
       => r1_xreal_0(1,k9_group_1(A)) ) ) ),
    inference(mizar_proof,[status(thm)],[d14_group_1,t79_card_1,t37_zfmisc_1,t80_card_1,d15_group_1]),
    [file(group_1,t90_group_1),interesting(0.54)]).

fof(t23_group_1,theorem,(
    ! [A] : 
      ( ( ~ v3_struct_0(A)
        & v3_group_1(A)
        & v4_group_1(A)
        & l1_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,B,D) = C ) ) ) ) ),
    inference(mizar_proof,[status(thm)],[t21_group_1]),
    [file(group_1,t23_group_1),interesting(0.53)]).

fof(t24_group_1,theorem,(
    ! [A] : 
      ( ( ~ v3_struct_0(A)
        & v3_group_1(A)
        & v4_group_1(A)
        & l1_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,D,B) = C ) ) ) ) ),
    inference(mizar_proof,[status(thm)],[t22_group_1]),
    [file(group_1,t24_group_1),interesting(0.53)]).

fof(t70_group_1,theorem,(
    ! [A] : 
      ( v1_int_1(A)
     => ! [B] : 
          ( ( ~ v3_struct_0(B)
            & v3_group_1(B)
            & v4_group_1(B)
            & l1_group_1(B) )
         => ! [C] : 
              ( m1_subset_1(C,u1_struct_0(B))
             => k6_group_1(B,k4_xcmplx_0(A),C) = k3_group_1(B,k6_group_1(B,A,C)) ) ) ) ),
    inference(mizar_proof,[status(thm)],[l76_group_1]),
    [file(group_1,t70_group_1),interesting(0.51)]).

fof(t25_group_1,theorem,(
    ! [A] : 
      ( ( ~ v3_struct_0(A)
        & v3_group_1(A)
        & v4_group_1(A)
        & l1_group_1(A) )
     => ! [B] : 
          ( m1_subset_1(B,u1_struct_0(A))
         => ! [C] : 
              ( m1_subset_1(C,u1_struct_0(A))
             => k3_group_1(A,k1_group_1(A,B,C)) = k1_group_1(A,k3_group_1(A,C),k3_group_1(A,B)) ) ) ) ),
    inference(mizar_proof,[status(thm)],[d4_group_1,d4_group_1,d6_group_1,d5_group_1,d6_group_1,t20_group_1]),
    [file(group_1,t25_group_1),interesting(0.49)]).

fof(t85_group_1,theorem,(
    ! [A] : 
      ( ( ~ v3_struct_0(A)
        & v3_group_1(A)
        & v4_group_1(A)
        & l1_group_1(A) )
     => ! [B] : 
          ( m1_subset_1(B,u1_struct_0(A))
         => ( k7_group_1(A,B) = 1
           => B = k2_group_1(A) ) ) ) ),
    inference(mizar_proof,[status(thm)],[d12_group_1,d12_group_1,t44_group_1]),
    [file(group_1,t85_group_1),interesting(0.49)]).

fof(t64_group_1,theorem,(
    ! [A] : 
      ( m2_subset_1(A,k1_numbers,k5_numbers)
     => ! [B] : 
          ( v1_int_1(B)
         => ! [C] : 
              ( ( ~ v3_struct_0(C)
                & v3_group_1(C)
                & v4_group_1(C)
                & l1_group_1(C) )
             => ! [D] : 
                  ( m1_subset_1(D,u1_struct_0(C))
                 => k6_group_1(C,k2_xcmplx_0(A,B),D) = k1_group_1(C,k6_group_1(C,A,D),k6_group_1(C,B,D)) ) ) ) ) ),
    inference(mizar_proof,[status(thm)],[t63_group_1]),
    [file(group_1,t64_group_1),interesting(0.48)]).

fof(t65_group_1,theorem,(
    ! [A] : 
      ( m2_subset_1(A,k1_numbers,k5_numbers)
     => ! [B] : 
          ( v1_int_1(B)
         => ! [C] : 
              ( ( ~ v3_struct_0(C)
                & v3_group_1(C)
                & v4_group_1(C)
                & l1_group_1(C) )
             => ! [D] : 
                  ( m1_subset_1(D,u1_struct_0(C))
                 => k6_group_1(C,k2_xcmplx_0(B,A),D) = k1_group_1(C,k6_group_1(C,B,D),k6_group_1(C,A,D)) ) ) ) ) ),
    inference(mizar_proof,[status(thm)],[t63_group_1]),
    [file(group_1,t65_group_1),interesting(0.48)]).

fof(t47_group_1,theorem,(
    ! [A] : 
      ( ( ~ v3_struct_0(A)
        & v3_group_1(A)
        & v4_group_1(A)
        & l1_group_1(A) )
     => ! [B] : 
          ( m1_subset_1(B,u1_struct_0(A))
         => ( k6_group_1(A,2,B) = k2_group_1(A)
          <=> k3_group_1(A,B) = B ) ) ) ),
    inference(mizar_proof,[status(thm)],[t45_group_1,t20_group_1,t45_group_1,d6_group_1]),
    [file(group_1,t47_group_1),interesting(0.46)]).

fof(t46_group_1,theorem,(
    ! [A] : 
      ( ( ~ v3_struct_0(A)
        & v3_group_1(A)
        & v4_group_1(A)
        & l1_group_1(A) )
     => ! [B] : 
          ( m1_subset_1(B,u1_struct_0(A))
         => k6_group_1(A,3,B) = k1_group_1(A,k1_group_1(A,B,B),B) ) ) ),
    inference(mizar_proof,[status(thm)],[l49_group_1,t45_group_1]),
    [file(group_1,t46_group_1),interesting(0.44)]).

fof(t15_group_1,theorem,(
    ! [A] : 
      ( ( ~ v3_struct_0(A)
        & v3_group_1(A)
        & v4_group_1(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) = B
                  | k1_group_1(A,C,B) = B )
               => C = k2_group_1(A) ) ) ) ) ),
    inference(mizar_proof,[status(thm)],[d5_group_1,t14_group_1]),
    [file(group_1,t15_group_1),interesting(0.43)]).

fof(t43_group_1,theorem,(
    ! [A] : 
      ( ( ~ v3_struct_0(A)
        & v3_group_1(A)
        & v4_group_1(A)
        & l1_group_1(A) )
     => ! [B] : 
          ( m1_subset_1(B,u1_struct_0(A))
         => k6_group_1(A,0,B) = k2_group_1(A) ) ) ),
    inference(mizar_proof,[status(thm)],[l50_group_1]),
    [file(group_1,t43_group_1),interesting(0.43)]).

fof(t86_group_1,theorem,(
    ! [A] : 
      ( m2_subset_1(A,k1_numbers,k5_numbers)
     => ! [B] : 
          ( ( ~ v3_struct_0(B)
            & v3_group_1(B)
            & v4_group_1(B)
            & l1_group_1(B) )
         => ! [C] : 
              ( m1_subset_1(C,u1_struct_0(B))
             => ( k6_group_1(B,A,C) = k2_group_1(B)
               => r1_nat_1(k7_group_1(B,C),A) ) ) ) ) ),
    inference(mizar_proof,[status(thm)],[t53_nat_1,d12_group_1,d11_group_1,d12_group_1,d12_group_1,t28_nat_1,t48_group_1,t82_group_1,d5_group_1,t41_nat_1,d3_nat_1,d3_nat_1,s4_nat_1]),
    [file(group_1,t86_group_1),interesting(0.43)]).

fof(t66_group_1,theorem,(
    ! [A] : 
      ( v1_int_1(A)
     => ! [B] : 
          ( ( ~ v3_struct_0(B)
            & v3_group_1(B)
            & v4_group_1(B)
            & l1_group_1(B) )
         => ! [C] : 
              ( m1_subset_1(C,u1_struct_0(B))
             => ( k6_group_1(B,k2_xcmplx_0(A,1),C) = k1_group_1(B,k6_group_1(B,A,C),C)
                & k6_group_1(B,k2_xcmplx_0(A,1),C) = k1_group_1(B,C,k6_group_1(B,A,C)) ) ) ) ) ),
    inference(mizar_proof,[status(thm)],[t44_group_1,t63_group_1]),
    [file(group_1,t66_group_1),interesting(0.40)]).

fof(t52_group_1,theorem,(
    ! [A] : 
      ( m2_subset_1(A,k1_numbers,k5_numbers)
     => ! [B] : 
          ( ( ~ v3_struct_0(B)
            & v3_group_1(B)
            & v4_group_1(B)
            & l1_group_1(B) )
         => ! [C] : 
              ( m1_subset_1(C,u1_struct_0(B))
             => ! [D] : 
                  ( m1_subset_1(D,u1_struct_0(B))
                 => ( k1_group_1(B,C,D) = k1_group_1(B,D,C)
                   => k1_group_1(B,C,k6_group_1(B,A,D)) = k1_group_1(B,k6_group_1(B,A,D),C) ) ) ) ) ) ),
    inference(mizar_proof,[status(thm)],[l50_group_1,d5_group_1,d5_group_1,l50_group_1,t49_group_1,d4_group_1,d4_group_1,d4_group_1,t49_group_1,s1_nat_1]),
    [file(group_1,t52_group_1),interesting(0.40)]).

fof(t55_group_1,theorem,(
    ! [A] : 
      ( v1_int_1(A)
     => ! [B] : 
          ( ( ~ v3_struct_0(B)
            & v3_group_1(B)
            & v4_group_1(B)
            & l1_group_1(B) )
         => ! [C] : 
              ( m1_subset_1(C,u1_struct_0(B))
             => ( r1_xreal_0(0,A)
               => k6_group_1(B,A,C) = k6_group_1(B,k1_int_2(A),C) ) ) ) ) ),
    inference(mizar_proof,[status(thm)],[d9_group_1]),
    [file(group_1,t55_group_1),interesting(0.38)]).

fof(t10_group_1,theorem,(
    ! [A] : 
      ( ( ~ v3_struct_0(A)
        & v3_group_1(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,C,B) = C
                  & k1_group_1(A,B,C) = C ) )
           => B = k2_group_1(A) ) ) ) ),
    inference(mizar_proof,[status(thm)],[d5_group_1]),
    [file(group_1,t10_group_1),interesting(0.37)]).

fof(t71_group_1,theorem,(
    ! [A] : 
      ( m2_subset_1(A,k1_numbers,k5_numbers)
     => ! [B] : 
          ( ( ~ v3_struct_0(B)
            & v3_group_1(B)
            & v4_group_1(B)
            & l1_group_1(B) )
         => ! [C] : 
              ( m1_subset_1(C,u1_struct_0(B))
             => k6_group_1(B,k7_binop_2(A),C) = k3_group_1(B,k6_group_1(B,A,C)) ) ) ) ),
    inference(mizar_proof,[status(thm)],[l76_group_1]),
    [file(group_1,t71_group_1),interesting(0.37)]).

fof(l49_group_1,theorem,(
    ! [A] : 
      ( m2_subset_1(A,k1_numbers,k5_numbers)
     => ! [B] : 
          ( ( ~ v3_struct_0(B)
            & v3_group_1(B)
            & v4_group_1(B)
            & l1_group_1(B) )
         => ! [C] : 
              ( m1_subset_1(C,u1_struct_0(B))
             => k6_group_1(B,k1_nat_1(A,1),C) = k1_group_1(B,k6_group_1(B,A,C),C) ) ) ) ),
    inference(mizar_proof,[status(thm)],[d8_group_1]),
    [file(group_1,l49_group_1),interesting(0.35)]).

fof(t56_group_1,theorem,(
    ! [A] : 
      ( v1_int_1(A)
     => ! [B] : 
          ( ( ~ v3_struct_0(B)
            & v3_group_1(B)
            & v4_group_1(B)
            & l1_group_1(B) )
         => ! [C] : 
              ( m1_subset_1(C,u1_struct_0(B))
             => ( ~ r1_xreal_0(0,A)
               => k6_group_1(B,A,C) = k3_group_1(B,k6_group_1(B,k1_int_2(A),C)) ) ) ) ) ),
    inference(mizar_proof,[status(thm)],[d9_group_1]),
    [file(group_1,t56_group_1),interesting(0.35)]).

fof(t54_group_1,theorem,(
    ! [A] : 
      ( m2_subset_1(A,k1_numbers,k5_numbers)
     => ! [B] : 
          ( ( ~ v3_struct_0(B)
            & v3_group_1(B)
            & v4_group_1(B)
            & l1_group_1(B) )
         => ! [C] : 
              ( m1_subset_1(C,u1_struct_0(B))
             => ! [D] : 
                  ( m1_subset_1(D,u1_struct_0(B))
                 => ( k1_group_1(B,C,D) = k1_group_1(B,D,C)
                   => k6_group_1(B,A,k1_group_1(B,C,D)) = k1_group_1(B,k6_group_1(B,A,C),k6_group_1(B,A,D)) ) ) ) ) ) ),
    inference(mizar_proof,[status(thm)],[l50_group_1,d5_group_1,l50_group_1,l50_group_1,t49_group_1,d4_group_1,d4_group_1,t49_group_1,t53_group_1,d4_group_1,t49_group_1,t53_group_1,s1_nat_1]),
    [file(group_1,t54_group_1),interesting(0.35)]).

fof(t59_group_1,theorem,(
    ! [A] : 
      ( v1_int_1(A)
     => ! [B] : 
          ( ( ~ v3_struct_0(B)
            & v3_group_1(B)
            & v4_group_1(B)
            & l1_group_1(B) )
         => ! [C] : 
              ( m1_subset_1(C,u1_struct_0(B))
             => ( A = 0
               => k6_group_1(B,A,C) = k2_group_1(B) ) ) ) ) ),
    inference(mizar_proof,[status(thm)],[l50_group_1]),
    [file(group_1,t59_group_1),interesting(0.33)]).

fof(t48_group_1,theorem,(
    ! [A] : 
      ( m2_subset_1(A,k1_numbers,k5_numbers)
     => ! [B] : 
          ( m2_subset_1(B,k1_numbers,k5_numbers)
         => ! [C] : 
              ( ( ~ v3_struct_0(C)
                & v3_group_1(C)
                & v4_group_1(C)
                & l1_group_1(C) )
             => ! [D] : 
                  ( m1_subset_1(D,u1_struct_0(C))
                 => k6_group_1(C,k1_nat_1(A,B),D) = k1_group_1(C,k6_group_1(C,A,D),k6_group_1(C,B,D)) ) ) ) ) ),
    inference(mizar_proof,[status(thm)],[d5_group_1,l50_group_1,l49_group_1,d4_group_1,l49_group_1,s1_nat_1]),
    [file(group_1,t48_group_1),interesting(0.33)]).

fof(t75_group_1,theorem,(
    ! [A] : 
      ( m2_subset_1(A,k1_numbers,k5_numbers)
     => ! [B] : 
          ( v1_int_1(B)
         => ! [C] : 
              ( ( ~ v3_struct_0(C)
                & v3_group_1(C)
                & v4_group_1(C)
                & l1_group_1(C) )
             => ! [D] : 
                  ( m1_subset_1(D,u1_struct_0(C))
                 => ! [E] : 
                      ( m1_subset_1(E,u1_struct_0(C))
                     => ( k1_group_1(C,D,E) = k1_group_1(C,E,D)
                       => k1_group_1(C,k6_group_1(C,A,D),k6_group_1(C,B,E)) = k1_group_1(C,k6_group_1(C,B,E),k6_group_1(C,A,D)) ) ) ) ) ) ) ),
    inference(mizar_proof,[status(thm)],[t74_group_1]),
    [file(group_1,t75_group_1),interesting(0.29)]).

fof(t49_group_1,theorem,(
    ! [A] : 
      ( m2_subset_1(A,k1_numbers,k5_numbers)
     => ! [B] : 
          ( ( ~ v3_struct_0(B)
            & v3_group_1(B)
            & v4_group_1(B)
            & l1_group_1(B) )
         => ! [C] : 
              ( m1_subset_1(C,u1_struct_0(B))
             => ( k6_group_1(B,k1_nat_1(A,1),C) = k1_group_1(B,k6_group_1(B,A,C),C)
                & k6_group_1(B,k1_nat_1(A,1),C) = k1_group_1(B,C,k6_group_1(B,A,C)) ) ) ) ) ),
    inference(mizar_proof,[status(thm)],[l49_group_1,t48_group_1,t44_group_1]),
    [file(group_1,t49_group_1),interesting(0.28)]).

fof(t95_group_1,theorem,(
    ! [A] : 
      ( m2_subset_1(A,k1_numbers,k5_numbers)
     => ! [B] : 
          ( ( ~ v3_struct_0(B)
            & v3_group_1(B)
            & v4_group_1(B)
            & v7_group_1(B)
            & l1_group_1(B) )
         => ! [C] : 
              ( m1_subset_1(C,u1_struct_0(B))
             => ! [D] : 
                  ( m1_subset_1(D,u1_struct_0(B))
                 => k6_group_1(B,A,k10_group_1(B,C,D)) = k10_group_1(B,k6_group_1(B,A,C),k6_group_1(B,A,D)) ) ) ) ) ),
    inference(mizar_proof,[status(thm)],[t54_group_1]),
    [file(group_1,t95_group_1),interesting(0.27)]).

fof(l78_group_1,theorem,(
    ! [A] : 
      ( v1_int_1(A)
     => ! [B] : 
          ( ( ~ v3_struct_0(B)
            & v3_group_1(B)
            & v4_group_1(B)
            & l1_group_1(B) )
         => ! [C] : 
              ( m1_subset_1(C,u1_struct_0(B))
             => k6_group_1(B,k6_xcmplx_0(A,1),C) = k1_group_1(B,k6_group_1(B,A,C),k6_group_1(B,k7_binop_2(1),C)) ) ) ) ),
    inference(mizar_proof,[status(thm)],[t21_xreal_1,t26_xreal_1,d1_absvalue,t138_complex1,d1_absvalue,d4_group_1,t55_group_1,t60_group_1,t49_group_1,d6_group_1,t10_xreal_1,t26_xreal_1,t26_xreal_1,t138_complex1,t56_group_1,t55_group_1,t49_group_1,d1_absvalue,d1_absvalue,d6_group_1,t62_group_1,d4_group_1,d6_group_1,d5_group_1,l50_group_1,l77_group_1,l76_group_1,d6_group_1,t14_group_1,t25_group_1,l76_group_1,t62_group_1,l76_group_1]),
    [file(group_1,l78_group_1),interesting(0.21)]).

fof(t53_group_1,theorem,(
    ! [A] : 
      ( m2_subset_1(A,k1_numbers,k5_numbers)
     => ! [B] : 
          ( m2_subset_1(B,k1_numbers,k5_numbers)
         => ! [C] : 
              ( ( ~ v3_struct_0(C)
                & v3_group_1(C)
                & v4_group_1(C)
                & l1_group_1(C) )
             => ! [D] : 
                  ( m1_subset_1(D,u1_struct_0(C))
                 => ! [E] : 
                      ( m1_subset_1(E,u1_struct_0(C))
                     => ( k1_group_1(C,D,E) = k1_group_1(C,E,D)
                       => k1_group_1(C,k6_group_1(C,A,D),k6_group_1(C,B,E)) = k1_group_1(C,k6_group_1(C,B,E),k6_group_1(C,A,D)) ) ) ) ) ) ) ),
    inference(mizar_proof,[status(thm)],[l50_group_1,d5_group_1,d5_group_1,l50_group_1,t49_group_1,d4_group_1,d4_group_1,t52_group_1,d4_group_1,t49_group_1,s1_nat_1]),
    [file(group_1,t53_group_1),interesting(0.20)]).

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

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

fof(l115_group_1,theorem,
    ( ~ v3_struct_0(g1_group_1(k1_numbers,k33_binop_2))
    & v3_group_1(g1_group_1(k1_numbers,k33_binop_2))
    & v4_group_1(g1_group_1(k1_numbers,k33_binop_2))
    & l1_group_1(g1_group_1(k1_numbers,k33_binop_2)) ),
    inference(mizar_proof,[status(thm)],[t7_group_1]),
    [file(group_1,l115_group_1),interesting(0.00)]).

fof(l2_group_1,theorem,
    ( ! [A] : 
        ( m1_subset_1(A,u1_struct_0(g1_group_1(k1_numbers,k33_binop_2)))
       => ! [B] : 
            ( m1_subset_1(B,u1_struct_0(g1_group_1(k1_numbers,k33_binop_2)))
           => ! [C] : 
                ( m1_subset_1(C,u1_struct_0(g1_group_1(k1_numbers,k33_binop_2)))
               => k1_group_1(g1_group_1(k1_numbers,k33_binop_2),k1_group_1(g1_group_1(k1_numbers,k33_binop_2),A,B),C) = k1_group_1(g1_group_1(k1_numbers,k33_binop_2),A,k1_group_1(g1_group_1(k1_numbers,k33_binop_2),B,C)) ) ) )
    & ? [A] : 
        ( m1_subset_1(A,u1_struct_0(g1_group_1(k1_numbers,k33_binop_2)))
        & ! [B] : 
            ( m1_subset_1(B,u1_struct_0(g1_group_1(k1_numbers,k33_binop_2)))
           => ( k1_group_1(g1_group_1(k1_numbers,k33_binop_2),B,A) = B
              & k1_group_1(g1_group_1(k1_numbers,k33_binop_2),A,B) = B
              & ? [C] : 
                  ( m1_subset_1(C,u1_struct_0(g1_group_1(k1_numbers,k33_binop_2)))
                  & k1_group_1(g1_group_1(k1_numbers,k33_binop_2),B,C) = A
                  & k1_group_1(g1_group_1(k1_numbers,k33_binop_2),C,B) = A ) ) ) ) ),
    inference(mizar_proof,[status(thm)],[d9_binop_2]),
    [file(group_1,l2_group_1),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(t11_group_1,theorem,(
    $true ),
    file(group_1,t11_group_1),
    [interesting(0.00)]).

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

fof(t12_group_1,theorem,(
    ! [A] : 
      ( ( ~ v3_struct_0(A)
        & v3_group_1(A)
        & v4_group_1(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_group_1(A)
                  & k1_group_1(A,C,B) = k2_group_1(A) )
               => C = k3_group_1(A,B) ) ) ) ) ),
    inference(mizar_proof,[status(thm)],[d6_group_1]),
    [file(group_1,t12_group_1),interesting(0.00)]).

fof(t13_group_1,theorem,(
    $true ),
    file(group_1,t13_group_1),
    [interesting(0.00)]).

fof(t14_group_1,theorem,(
    ! [A] : 
      ( ( ~ v3_struct_0(A)
        & v3_group_1(A)
        & v4_group_1(A)
        & l1_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,B,C) = k1_group_1(A,B,D)
                      | k1_group_1(A,C,B) = k1_group_1(A,D,B) )
                   => C = D ) ) ) ) ) ),
    inference(mizar_proof,[status(thm)],[d4_group_1,d4_group_1,d6_group_1,d5_group_1,d6_group_1,d4_group_1,d5_group_1,d6_group_1,d5_group_1,d6_group_1,d5_group_1]),
    [file(group_1,t14_group_1),interesting(0.00)]).

fof(t1_group_1,theorem,(
    $true ),
    file(group_1,t1_group_1),
    [interesting(0.00)]).

fof(t21_group_1,theorem,(
    ! [A] : 
      ( ( ~ v3_struct_0(A)
        & v3_group_1(A)
        & v4_group_1(A)
        & l1_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,B,C) = D
                  <=> C = k1_group_1(A,k3_group_1(A,B),D) ) ) ) ) ) ),
    inference(mizar_proof,[status(thm)],[d4_group_1,d6_group_1,d5_group_1,t14_group_1,d4_group_1,d6_group_1,d5_group_1]),
    [file(group_1,t21_group_1),interesting(0.00)]).

fof(t22_group_1,theorem,(
    ! [A] : 
      ( ( ~ v3_struct_0(A)
        & v3_group_1(A)
        & v4_group_1(A)
        & l1_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,B,C) = D
                  <=> B = k1_group_1(A,D,k3_group_1(A,C)) ) ) ) ) ) ),
    inference(mizar_proof,[status(thm)],[d4_group_1,d6_group_1,d5_group_1,t14_group_1,d4_group_1,d6_group_1,d5_group_1]),
    [file(group_1,t22_group_1),interesting(0.00)]).

fof(t29_group_1,theorem,(
    $true ),
    file(group_1,t29_group_1),
    [interesting(0.00)]).

fof(t2_group_1,theorem,(
    $true ),
    file(group_1,t2_group_1),
    [interesting(0.00)]).

fof(t30_group_1,theorem,(
    $true ),
    file(group_1,t30_group_1),
    [interesting(0.00)]).

fof(d14_binop_1,definition,(
    ! [A] : 
      ( ~ v1_xboole_0(A)
     => ! [B] : 
          ( ( v1_funct_1(B)
            & v1_funct_2(B,k2_zfmisc_1(A,A),A)
            & m2_relset_1(B,k2_zfmisc_1(A,A),A) )
         => ( v2_binop_1(B,A)
          <=> ! [C] : 
                ( m1_subset_1(C,A)
               => ! [D] : 
                    ( m1_subset_1(D,A)
                   => ! [E] : 
                        ( m1_subset_1(E,A)
                       => k2_binop_1(A,A,A,B,C,k2_binop_1(A,A,A,B,D,E)) = k2_binop_1(A,A,A,B,k2_binop_1(A,A,A,B,C,D),E) ) ) ) ) ) ) ),
    file(binop_1,d14_binop_1),
    [interesting(0.00)]).

fof(d2_setwiseo,definition,(
    ! [A] : 
      ( ~ v1_xboole_0(A)
     => ! [B] : 
          ( ( v1_funct_1(B)
            & v1_funct_2(B,k2_zfmisc_1(A,A),A)
            & m2_relset_1(B,k2_zfmisc_1(A,A),A) )
         => ( v1_setwiseo(B,A)
          <=> ? [C] : 
                ( m1_subset_1(C,A)
                & r3_binop_1(A,C,B) ) ) ) ) ),
    file(setwiseo,d2_setwiseo),
    [interesting(0.00)]).

fof(t11_binop_1,theorem,(
    ! [A,B] : 
      ( ( v1_funct_1(B)
        & v1_funct_2(B,k2_zfmisc_1(A,A),A)
        & m2_relset_1(B,k2_zfmisc_1(A,A),A) )
     => ! [C] : 
          ( m1_subset_1(C,A)
         => ( r3_binop_1(A,C,B)
          <=> ! [D] : 
                ( m1_subset_1(D,A)
               => ( k1_binop_1(B,C,D) = D
                  & k1_binop_1(B,D,C) = D ) ) ) ) ) ),
    file(binop_1,t11_binop_1),
    [interesting(0.00)]).

fof(d1_finseqop,definition,(
    ! [A] : 
      ( ~ v1_xboole_0(A)
     => ! [B] : 
          ( ( v1_funct_1(B)
            & v1_funct_2(B,A,A)
            & m2_relset_1(B,A,A) )
         => ! [C] : 
              ( ( v1_funct_1(C)
                & v1_funct_2(C,k2_zfmisc_1(A,A),A)
                & m2_relset_1(C,k2_zfmisc_1(A,A),A) )
             => ( r1_finseqop(A,B,C)
              <=> ! [D] : 
                    ( m1_subset_1(D,A)
                   => ( k2_binop_1(A,A,A,C,D,k8_funct_2(A,A,B,D)) = k3_binop_1(A,C)
                      & k2_binop_1(A,A,A,C,k8_funct_2(A,A,B,D),D) = k3_binop_1(A,C) ) ) ) ) ) ) ),
    file(finseqop,d1_finseqop),
    [interesting(0.00)]).

fof(d7_group_1,definition,(
    ! [A] : 
      ( ( ~ v3_struct_0(A)
        & v3_group_1(A)
        & v4_group_1(A)
        & l1_group_1(A) )
     => ! [B] : 
          ( ( v1_funct_1(B)
            & v1_funct_2(B,u1_struct_0(A),u1_struct_0(A))
            & m2_relset_1(B,u1_struct_0(A),u1_struct_0(A)) )
         => ( B = k4_group_1(A)
          <=> ! [C] : 
                ( m1_subset_1(C,u1_struct_0(A))
               => k8_funct_2(u1_struct_0(A),u1_struct_0(A),B,C) = k3_group_1(A,C) ) ) ) ) ),
    file(group_1,d7_group_1),
    [interesting(0.00)]).

fof(d8_binop_1,definition,(
    ! [A,B] : 
      ( ( v1_funct_1(B)
        & v1_funct_2(B,k2_zfmisc_1(A,A),A)
        & m2_relset_1(B,k2_zfmisc_1(A,A),A) )
     => ( ? [C] : 
            ( m1_subset_1(C,A)
            & r3_binop_1(A,C,B) )
       => ! [C] : 
            ( m1_subset_1(C,A)
           => ( C = k3_binop_1(A,B)
            <=> r3_binop_1(A,C,B) ) ) ) ) ),
    file(binop_1,d8_binop_1),
    [interesting(0.00)]).

fof(d2_finseqop,definition,(
    ! [A] : 
      ( ~ v1_xboole_0(A)
     => ! [B] : 
          ( ( v1_funct_1(B)
            & v1_funct_2(B,k2_zfmisc_1(A,A),A)
            & m2_relset_1(B,k2_zfmisc_1(A,A),A) )
         => ( v1_finseqop(B,A)
          <=> ? [C] : 
                ( v1_funct_1(C)
                & v1_funct_2(C,A,A)
                & m2_relset_1(C,A,A)
                & r1_finseqop(A,C,B) ) ) ) ) ),
    file(finseqop,d2_finseqop),
    [interesting(0.00)]).

fof(d3_finseqop,definition,(
    ! [A] : 
      ( ~ v1_xboole_0(A)
     => ! [B] : 
          ( ( v1_funct_1(B)
            & v1_funct_2(B,k2_zfmisc_1(A,A),A)
            & m2_relset_1(B,k2_zfmisc_1(A,A),A) )
         => ( ( v1_setwiseo(B,A)
              & v2_binop_1(B,A)
              & v1_finseqop(B,A) )
           => ! [C] : 
                ( ( v1_funct_1(C)
                  & v1_funct_2(C,A,A)
                  & m2_relset_1(C,A,A) )
               => ( C = k6_finseqop(A,B)
                <=> r1_finseqop(A,C,B) ) ) ) ) ) ),
    file(finseqop,d3_finseqop),
    [interesting(0.00)]).

fof(t38_group_1,theorem,(
    $true ),
    file(group_1,t38_group_1),
    [interesting(0.00)]).

fof(t39_group_1,theorem,(
    $true ),
    file(group_1,t39_group_1),
    [interesting(0.00)]).

fof(t3_group_1,theorem,(
    $true ),
    file(group_1,t3_group_1),
    [interesting(0.00)]).

fof(t40_group_1,theorem,(
    $true ),
    file(group_1,t40_group_1),
    [interesting(0.00)]).

fof(t41_group_1,theorem,(
    $true ),
    file(group_1,t41_group_1),
    [interesting(0.00)]).

fof(d8_group_1,definition,(
    ! [A] : 
      ( ( ~ v3_struct_0(A)
        & l1_group_1(A) )
     => ! [B] : 
          ( ( v1_funct_1(B)
            & v1_funct_2(B,k2_zfmisc_1(u1_struct_0(A),k5_numbers),u1_struct_0(A))
            & m2_relset_1(B,k2_zfmisc_1(u1_struct_0(A),k5_numbers),u1_struct_0(A)) )
         => ( B = k5_group_1(A)
          <=> ! [C] : 
                ( m1_subset_1(C,u1_struct_0(A))
               => ( k2_binop_1(u1_struct_0(A),k5_numbers,u1_struct_0(A),B,C,0) = k2_group_1(A)
                  & ! [D] : 
                      ( m2_subset_1(D,k1_numbers,k5_numbers)
                     => k2_binop_1(u1_struct_0(A),k5_numbers,u1_struct_0(A),B,C,k1_nat_1(D,1)) = k1_group_1(A,k2_binop_1(u1_struct_0(A),k5_numbers,u1_struct_0(A),B,C,D),C) ) ) ) ) ) ) ),
    file(group_1,d8_group_1),
    [interesting(0.00)]).

fof(t20_group_1,theorem,(
    ! [A] : 
      ( ( ~ v3_struct_0(A)
        & v3_group_1(A)
        & v4_group_1(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_group_1(A)
                  | k1_group_1(A,C,B) = k2_group_1(A) )
               => ( B = k3_group_1(A,C)
                  & C = k3_group_1(A,B) ) ) ) ) ) ),
    inference(mizar_proof,[status(thm)],[d6_group_1,t14_group_1]),
    [file(group_1,t20_group_1),interesting(0.00)]).

fof(t4_group_1,theorem,(
    $true ),
    file(group_1,t4_group_1),
    [interesting(0.00)]).

fof(t57_group_1,theorem,(
    $true ),
    file(group_1,t57_group_1),
    [interesting(0.00)]).

fof(t58_group_1,theorem,(
    $true ),
    file(group_1,t58_group_1),
    [interesting(0.00)]).

fof(t5_group_1,theorem,(
    ! [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))
               => ! [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) = C
                      & k1_group_1(A,B,C) = C
                      & ? [D] : 
                          ( m1_subset_1(D,u1_struct_0(A))
                          & k1_group_1(A,C,D) = B
                          & k1_group_1(A,D,C) = B ) ) ) )
          | ( ~ v3_struct_0(A)
            & v3_group_1(A)
            & v4_group_1(A)
            & l1_group_1(A) ) ) ) ) ),
    inference(mizar_proof,[status(thm)],[d3_group_1,d4_group_1]),
    [file(group_1,t5_group_1),interesting(0.00)]).

fof(d9_group_1,definition,(
    ! [A] : 
      ( ( ~ v3_struct_0(A)
        & v3_group_1(A)
        & v4_group_1(A)
        & l1_group_1(A) )
     => ! [B] : 
          ( v1_int_1(B)
         => ! [C] : 
              ( m1_subset_1(C,u1_struct_0(A))
             => ( ( r1_xreal_0(0,B)
                 => k6_group_1(A,B,C) = k2_binop_1(u1_struct_0(A),k5_numbers,u1_struct_0(A),k5_group_1(A),C,k1_int_2(B)) )
                & ( ~ r1_xreal_0(0,B)
                 => k6_group_1(A,B,C) = k3_group_1(A,k2_binop_1(u1_struct_0(A),k5_numbers,u1_struct_0(A),k5_group_1(A),C,k1_int_2(B))) ) ) ) ) ) ),
    file(group_1,d9_group_1),
    [interesting(0.00)]).

fof(s1_nat_1,theorem,
    ( ( p1_s1_nat_1(0)
      & ! [A] : 
          ( m2_subset_1(A,k1_numbers,k5_numbers)
         => ( p1_s1_nat_1(A)
           => p1_s1_nat_1(k1_nat_1(A,1)) ) ) )
   => ! [A] : 
        ( m2_subset_1(A,k1_numbers,k5_numbers)
       => p1_s1_nat_1(A) ) ),
    file(nat_1,s1_nat_1),
    [interesting(0.00)]).

fof(t21_xreal_1,theorem,(
    ! [A] : 
      ( v1_xreal_0(A)
     => ! [B] : 
          ( v1_xreal_0(B)
         => ! [C] : 
              ( v1_xreal_0(C)
             => ( r1_xreal_0(k2_xcmplx_0(A,B),C)
              <=> r1_xreal_0(A,k6_xcmplx_0(C,B)) ) ) ) ) ),
    file(xreal_1,t21_xreal_1),
    [interesting(0.00)]).

fof(t26_xreal_1,theorem,(
    ! [A] : 
      ( v1_xreal_0(A)
     => ! [B] : 
          ( v1_xreal_0(B)
         => ( r1_xreal_0(A,B)
          <=> r1_xreal_0(k4_xcmplx_0(B),k4_xcmplx_0(A)) ) ) ) ),
    file(xreal_1,t26_xreal_1),
    [interesting(0.00)]).

fof(d1_absvalue,definition,(
    ! [A] : 
      ( v1_xreal_0(A)
     => ( ( r1_xreal_0(0,A)
         => k16_complex1(A) = A )
        & ( ~ r1_xreal_0(0,A)
         => k16_complex1(A) = k4_xcmplx_0(A) ) ) ) ),
    file(absvalue,d1_absvalue),
    [interesting(0.00)]).

fof(t138_complex1,theorem,(
    ! [A] : 
      ( v1_xcmplx_0(A)
     => k17_complex1(k4_xcmplx_0(A)) = k17_complex1(A) ) ),
    file(complex1,t138_complex1),
    [interesting(0.00)]).

fof(t10_xreal_1,theorem,(
    ! [A] : 
      ( v1_xreal_0(A)
     => ! [B] : 
          ( v1_xreal_0(B)
         => ! [C] : 
              ( v1_xreal_0(C)
             => ! [D] : 
                  ( v1_xreal_0(D)
                 => ~ ( ~ r1_xreal_0(B,A)
                      & r1_xreal_0(C,D)
                      & r1_xreal_0(k2_xcmplx_0(B,D),k2_xcmplx_0(A,C)) ) ) ) ) ) ),
    file(xreal_1,t10_xreal_1),
    [interesting(0.00)]).

fof(t16_int_1,theorem,(
    ! [A] : 
      ( v1_int_1(A)
     => ( r1_xreal_0(0,A)
       => r2_hidden(A,k5_numbers) ) ) ),
    file(int_1,t16_int_1),
    [interesting(0.00)]).

fof(t39_nat_1,theorem,(
    ! [A] : 
      ( v4_ordinal2(A)
     => ( ~ r1_xreal_0(1,A)
       => A = 0 ) ) ),
    file(nat_1,t39_nat_1),
    [interesting(0.00)]).

fof(t8_xreal_1,theorem,(
    ! [A] : 
      ( v1_xreal_0(A)
     => ! [B] : 
          ( v1_xreal_0(B)
         => ! [C] : 
              ( v1_xreal_0(C)
             => ( r1_xreal_0(A,B)
              <=> r1_xreal_0(k2_xcmplx_0(A,C),k2_xcmplx_0(B,C)) ) ) ) ) ),
    file(xreal_1,t8_xreal_1),
    [interesting(0.00)]).

fof(d5_real_1,definition,(
    ! [A] : 
      ( v1_xreal_0(A)
     => ! [B] : 
          ( v1_xreal_0(B)
         => ( r1_xreal_0(A,B)
          <=> ~ ( r1_xreal_0(B,A)
                & B != A ) ) ) ) ),
    file(real_1,d5_real_1),
    [interesting(0.00)]).

fof(s4_int_1,theorem,
    ( ( p1_s4_int_1(f1_s4_int_1)
      & ! [A] : 
          ( v1_int_1(A)
         => ( p1_s4_int_1(A)
           => ( p1_s4_int_1(k6_xcmplx_0(A,1))
              & p1_s4_int_1(k2_xcmplx_0(A,1)) ) ) ) )
   => ! [A] : 
        ( v1_int_1(A)
       => p1_s4_int_1(A) ) ),
    file(int_1,s4_int_1),
    [interesting(0.00)]).

fof(t50_group_1,theorem,(
    ! [A] : 
      ( m2_subset_1(A,k1_numbers,k5_numbers)
     => ! [B] : 
          ( m2_subset_1(B,k1_numbers,k5_numbers)
         => ! [C] : 
              ( ( ~ v3_struct_0(C)
                & v3_group_1(C)
                & v4_group_1(C)
                & l1_group_1(C) )
             => ! [D] : 
                  ( m1_subset_1(D,u1_struct_0(C))
                 => k6_group_1(C,k2_nat_1(A,B),D) = k6_group_1(C,B,k6_group_1(C,A,D)) ) ) ) ) ),
    inference(mizar_proof,[status(thm)],[l50_group_1,l50_group_1,t48_group_1,t44_group_1,t48_group_1,s1_nat_1]),
    [file(group_1,t50_group_1),interesting(0.00)]).

fof(t6_group_1,theorem,(
    ! [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))
                 => ! [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,D) = C )
                    & ? [D] : 
                        ( m1_subset_1(D,u1_struct_0(A))
                        & k1_group_1(A,D,B) = C ) ) ) ) )
       => ( v4_group_1(A)
          & v3_group_1(A) ) ) ) ),
    inference(mizar_proof,[status(thm)],[d4_group_1,d3_group_1]),
    [file(group_1,t6_group_1),interesting(0.00)]).

fof(t26_group_1,theorem,(
    ! [A] : 
      ( ( ~ v3_struct_0(A)
        & v3_group_1(A)
        & v4_group_1(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) = k1_group_1(A,C,B)
              <=> k3_group_1(A,k1_group_1(A,B,C)) = k1_group_1(A,k3_group_1(A,B),k3_group_1(A,C)) ) ) ) ) ),
    inference(mizar_proof,[status(thm)],[t25_group_1,d6_group_1,d4_group_1,d4_group_1,d6_group_1,d5_group_1,d6_group_1,t14_group_1]),
    [file(group_1,t26_group_1),interesting(0.00)]).

fof(t27_group_1,theorem,(
    ! [A] : 
      ( ( ~ v3_struct_0(A)
        & v3_group_1(A)
        & v4_group_1(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) = k1_group_1(A,C,B)
              <=> k1_group_1(A,k3_group_1(A,B),k3_group_1(A,C)) = k1_group_1(A,k3_group_1(A,C),k3_group_1(A,B)) ) ) ) ) ),
    inference(mizar_proof,[status(thm)],[t25_group_1,t26_group_1,t19_group_1,t25_group_1,t25_group_1,t19_group_1,t19_group_1]),
    [file(group_1,t27_group_1),interesting(0.00)]).

fof(t28_group_1,theorem,(
    ! [A] : 
      ( ( ~ v3_struct_0(A)
        & v3_group_1(A)
        & v4_group_1(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) = k1_group_1(A,C,B)
              <=> k1_group_1(A,B,k3_group_1(A,C)) = k1_group_1(A,k3_group_1(A,C),B) ) ) ) ) ),
    inference(mizar_proof,[status(thm)],[d4_group_1,d4_group_1,t27_group_1,d4_group_1,d6_group_1,d5_group_1,d6_group_1,t20_group_1,t25_group_1,t19_group_1,d4_group_1,d6_group_1,d5_group_1,d4_group_1,d4_group_1,d6_group_1,d5_group_1]),
    [file(group_1,t28_group_1),interesting(0.00)]).

fof(t74_group_1,theorem,(
    ! [A] : 
      ( v1_int_1(A)
     => ! [B] : 
          ( v1_int_1(B)
         => ! [C] : 
              ( ( ~ v3_struct_0(C)
                & v3_group_1(C)
                & v4_group_1(C)
                & l1_group_1(C) )
             => ! [D] : 
                  ( m1_subset_1(D,u1_struct_0(C))
                 => ! [E] : 
                      ( m1_subset_1(E,u1_struct_0(C))
                     => ( k1_group_1(C,D,E) = k1_group_1(C,E,D)
                       => k1_group_1(C,k6_group_1(C,A,D),k6_group_1(C,B,E)) = k1_group_1(C,k6_group_1(C,B,E),k6_group_1(C,A,D)) ) ) ) ) ) ) ),
    inference(mizar_proof,[status(thm)],[t55_group_1,t53_group_1,t55_group_1,t56_group_1,t53_group_1,t28_group_1,t55_group_1,t56_group_1,t53_group_1,t28_group_1,t56_group_1,t25_group_1,t53_group_1,t25_group_1]),
    [file(group_1,t74_group_1),interesting(0.00)]).

fof(t76_group_1,theorem,(
    $true ),
    file(group_1,t76_group_1),
    [interesting(0.00)]).

fof(t77_group_1,theorem,(
    ! [A] : 
      ( v1_int_1(A)
     => ! [B] : 
          ( ( ~ v3_struct_0(B)
            & v3_group_1(B)
            & v4_group_1(B)
            & l1_group_1(B) )
         => ! [C] : 
              ( m1_subset_1(C,u1_struct_0(B))
             => ! [D] : 
                  ( m1_subset_1(D,u1_struct_0(B))
                 => ( k1_group_1(B,C,D) = k1_group_1(B,D,C)
                   => k1_group_1(B,C,k6_group_1(B,A,D)) = k1_group_1(B,k6_group_1(B,A,D),C) ) ) ) ) ) ),
    inference(mizar_proof,[status(thm)],[t44_group_1,t74_group_1,t44_group_1]),
    [file(group_1,t77_group_1),interesting(0.00)]).

fof(t78_group_1,theorem,(
    $true ),
    file(group_1,t78_group_1),
    [interesting(0.00)]).

fof(t80_group_1,theorem,(
    $true ),
    file(group_1,t80_group_1),
    [interesting(0.00)]).

fof(t81_group_1,theorem,(
    $true ),
    file(group_1,t81_group_1),
    [interesting(0.00)]).

fof(t83_group_1,theorem,(
    $true ),
    file(group_1,t83_group_1),
    [interesting(0.00)]).

fof(d11_group_1,definition,(
    ! [A] : 
      ( ( ~ v3_struct_0(A)
        & v3_group_1(A)
        & v4_group_1(A)
        & l1_group_1(A) )
     => ! [B] : 
          ( m1_subset_1(B,u1_struct_0(A))
         => ( v5_group_1(B,A)
          <=> ! [C] : 
                ( m2_subset_1(C,k1_numbers,k5_numbers)
               => ( k6_group_1(A,C,B) = k2_group_1(A)
                 => C = 0 ) ) ) ) ) ),
    file(group_1,d11_group_1),
    [interesting(0.00)]).

fof(d12_group_1,definition,(
    ! [A] : 
      ( ( ~ v3_struct_0(A)
        & v3_group_1(A)
        & v4_group_1(A)
        & l1_group_1(A) )
     => ! [B] : 
          ( m1_subset_1(B,u1_struct_0(A))
         => ! [C] : 
              ( m2_subset_1(C,k1_numbers,k5_numbers)
             => ( ( v5_group_1(B,A)
                 => ( C = k7_group_1(A,B)
                  <=> C = 0 ) )
                & ( ~ v5_group_1(B,A)
                 => ( C = k7_group_1(A,B)
                  <=> ( k6_group_1(A,C,B) = k2_group_1(A)
                      & C != 0
                      & ! [D] : 
                          ( m2_subset_1(D,k1_numbers,k5_numbers)
                         => ( k6_group_1(A,D,B) = k2_group_1(A)
                           => ( D = 0
                              | r1_xreal_0(C,D) ) ) ) ) ) ) ) ) ) ) ),
    file(group_1,d12_group_1),
    [interesting(0.00)]).

fof(t53_nat_1,theorem,(
    ! [A] : 
      ( v4_ordinal2(A)
     => ( r1_nat_1(A,0)
        & r1_nat_1(1,A) ) ) ),
    file(nat_1,t53_nat_1),
    [interesting(0.00)]).

fof(t28_nat_1,theorem,(
    ! [A] : 
      ( v4_ordinal2(A)
     => ! [B] : 
          ( v4_ordinal2(B)
         => ~ ( r1_xreal_0(A,B)
              & ! [C] : 
                  ( m2_subset_1(C,k1_numbers,k5_numbers)
                 => B != k2_xcmplx_0(A,C) ) ) ) ) ),
    file(nat_1,t28_nat_1),
    [interesting(0.00)]).

fof(t41_nat_1,theorem,(
    ! [A] : 
      ( v4_ordinal2(A)
     => ! [B] : 
          ( v4_ordinal2(B)
         => ~ ( A != 0
              & r1_xreal_0(k2_xcmplx_0(B,A),B) ) ) ) ),
    file(nat_1,t41_nat_1),
    [interesting(0.00)]).

fof(d3_nat_1,definition,(
    ! [A] : 
      ( v4_ordinal2(A)
     => ! [B] : 
          ( v4_ordinal2(B)
         => ( r1_nat_1(A,B)
          <=> ? [C] : 
                ( m2_subset_1(C,k1_numbers,k5_numbers)
                & B = k3_xcmplx_0(A,C) ) ) ) ) ),
    file(nat_1,d3_nat_1),
    [interesting(0.00)]).

fof(s4_nat_1,theorem,
    ( ! [A] : 
        ( m2_subset_1(A,k1_numbers,k5_numbers)
       => ( ! [B] : 
              ( m2_subset_1(B,k1_numbers,k5_numbers)
             => ( ~ r1_xreal_0(A,B)
               => p1_s4_nat_1(B) ) )
         => p1_s4_nat_1(A) ) )
   => ! [A] : 
        ( m2_subset_1(A,k1_numbers,k5_numbers)
       => p1_s4_nat_1(A) ) ),
    file(nat_1,s4_nat_1),
    [interesting(0.00)]).

fof(t87_group_1,theorem,(
    $true ),
    file(group_1,t87_group_1),
    [interesting(0.00)]).

fof(t88_group_1,theorem,(
    $true ),
    file(group_1,t88_group_1),
    [interesting(0.00)]).

fof(t89_group_1,theorem,(
    $true ),
    file(group_1,t89_group_1),
    [interesting(0.00)]).

fof(t8_group_1,theorem,(
    $true ),
    file(group_1,t8_group_1),
    [interesting(0.00)]).

fof(d14_group_1,definition,(
    ! [A] : 
      ( l1_struct_0(A)
     => ( v6_group_1(A)
      <=> v1_finset_1(u1_struct_0(A)) ) ) ),
    file(group_1,d14_group_1),
    [interesting(0.00)]).

fof(t79_card_1,theorem,(
    ! [A] : k4_card_1(k1_tarski(A)) = 1 ),
    file(card_1,t79_card_1),
    [interesting(0.00)]).

fof(t37_zfmisc_1,theorem,(
    ! [A,B] : 
      ( r1_tarski(k1_tarski(A),B)
    <=> r2_hidden(A,B) ) ),
    file(zfmisc_1,t37_zfmisc_1),
    [interesting(0.00)]).

fof(t80_card_1,theorem,(
    ! [A] : 
      ( v1_finset_1(A)
     => ! [B] : 
          ( v1_finset_1(B)
         => ( r1_tarski(A,B)
           => r1_xreal_0(k4_card_1(A),k4_card_1(B)) ) ) ) ),
    file(card_1,t80_card_1),
    [interesting(0.00)]).

fof(d15_group_1,definition,(
    ! [A] : 
      ( ( ~ v3_struct_0(A)
        & v3_group_1(A)
        & v4_group_1(A)
        & l1_group_1(A) )
     => ( v6_group_1(A)
       => ! [B] : 
            ( m2_subset_1(B,k1_numbers,k5_numbers)
           => ( B = k9_group_1(A)
            <=> ? [C] : 
                  ( v1_finset_1(C)
                  & C = u1_struct_0(A)
                  & B = k4_card_1(C) ) ) ) ) ) ),
    file(group_1,d15_group_1),
    [interesting(0.00)]).

fof(t91_group_1,theorem,(
    $true ),
    file(group_1,t91_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(t92_group_1,theorem,
    ( ~ v3_struct_0(g1_group_1(k1_numbers,k33_binop_2))
    & v3_group_1(g1_group_1(k1_numbers,k33_binop_2))
    & v4_group_1(g1_group_1(k1_numbers,k33_binop_2))
    & v7_group_1(g1_group_1(k1_numbers,k33_binop_2))
    & l1_group_1(g1_group_1(k1_numbers,k33_binop_2)) ),
    inference(mizar_proof,[status(thm)],[t7_group_1,d16_group_1,d9_binop_2,d9_binop_2]),
    [file(group_1,t92_group_1),interesting(0.00)]).

fof(t93_group_1,theorem,(
    $true ),
    file(group_1,t93_group_1),
    [interesting(0.00)]).

fof(t94_group_1,theorem,(
    ! [A] : 
      ( ( ~ v3_struct_0(A)
        & v3_group_1(A)
        & v4_group_1(A)
        & v7_group_1(A)
        & l1_group_1(A) )
     => ! [B] : 
          ( m1_subset_1(B,u1_struct_0(A))
         => ! [C] : 
              ( m1_subset_1(C,u1_struct_0(A))
             => k3_group_1(A,k10_group_1(A,B,C)) = k10_group_1(A,k3_group_1(A,B),k3_group_1(A,C)) ) ) ) ),
    inference(mizar_proof,[status(thm)],[t25_group_1]),
    [file(group_1,t94_group_1),interesting(0.00)]).

fof(t73_group_1,theorem,(
    ! [A] : 
      ( v1_int_1(A)
     => ! [B] : 
          ( ( ~ v3_struct_0(B)
            & v3_group_1(B)
            & v4_group_1(B)
            & l1_group_1(B) )
         => ! [C] : 
              ( m1_subset_1(C,u1_struct_0(B))
             => ! [D] : 
                  ( m1_subset_1(D,u1_struct_0(B))
                 => ( k1_group_1(B,C,D) = k1_group_1(B,D,C)
                   => k6_group_1(B,A,k1_group_1(B,C,D)) = k1_group_1(B,k6_group_1(B,A,C),k6_group_1(B,A,D)) ) ) ) ) ) ),
    inference(mizar_proof,[status(thm)],[t55_group_1,t54_group_1,t56_group_1,t54_group_1,t25_group_1,t56_group_1,t56_group_1]),
    [file(group_1,t73_group_1),interesting(0.00)]).

fof(t96_group_1,theorem,(
    ! [A] : 
      ( v1_int_1(A)
     => ! [B] : 
          ( ( ~ v3_struct_0(B)
            & v3_group_1(B)
            & v4_group_1(B)
            & v7_group_1(B)
            & l1_group_1(B) )
         => ! [C] : 
              ( m1_subset_1(C,u1_struct_0(B))
             => ! [D] : 
                  ( m1_subset_1(D,u1_struct_0(B))
                 => k6_group_1(B,A,k10_group_1(B,C,D)) = k10_group_1(B,k6_group_1(B,A,C),k6_group_1(B,A,D)) ) ) ) ) ),
    inference(mizar_proof,[status(thm)],[t73_group_1]),
    [file(group_1,t96_group_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(t5_rlvect_1,theorem,(
    ! [A] : 
      ( ( ~ v3_struct_0(A)
        & l1_rlvect_1(A) )
     => ! [B] : 
          ( m1_subset_1(B,u1_struct_0(A))
         => ! [C] : 
              ( m1_subset_1(C,u1_struct_0(A))
             => k2_rlvect_1(A,B,C) = k2_binop_1(u1_struct_0(A),u1_struct_0(A),u1_struct_0(A),u1_rlvect_1(A),B,C) ) ) ) ),
    file(rlvect_1,t5_rlvect_1),
    [interesting(0.00)]).

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

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

fof(t97_group_1,theorem,(
    ! [A] : 
      ( ( ~ v3_struct_0(A)
        & v3_group_1(A)
        & v4_group_1(A)
        & v7_group_1(A)
        & l1_group_1(A) )
     => ( v3_rlvect_1(g1_rlvect_1(u1_struct_0(A),u1_group_1(A),k2_group_1(A)))
        & v4_rlvect_1(g1_rlvect_1(u1_struct_0(A),u1_group_1(A),k2_group_1(A)))
        & v5_rlvect_1(g1_rlvect_1(u1_struct_0(A),u1_group_1(A),k2_group_1(A)))
        & v6_rlvect_1(g1_rlvect_1(u1_struct_0(A),u1_group_1(A),k2_group_1(A))) ) ) ),
    inference(mizar_proof,[status(thm)],[d5_rlvect_1,t5_rlvect_1,t5_rlvect_1,d4_group_1,d6_rlvect_1,d5_group_1,d7_rlvect_1,d8_rlvect_1,d7_group_1,d6_group_1]),
    [file(group_1,t97_group_1),interesting(0.00)]).

fof(t9_group_1,theorem,(
    $true ),
    file(group_1,t9_group_1),
    [interesting(0.00)]).