fof(t48_gr_cy_1,theorem,(
    v1_gr_cy_1(k3_gr_cy_1) ),
    inference(mizar_proof,[status(thm)],[d2_int_1,d9_gr_cy_1,d8_group_2,d1_rlvect_1,d8_group_2,d1_rlvect_1,d2_int_1,d1_tarski,t4_group_4,t39_gr_cy_1,d3_tarski,t66_group_2,d5_group_4,d8_group_2]),
    [file(gr_cy_1,t48_gr_cy_1),interesting(1.00)]).

fof(t44_gr_cy_1,theorem,(
    ! [A] : 
      ( ( ~ v3_struct_0(A)
        & v3_group_1(A)
        & v4_group_1(A)
        & l1_group_1(A) )
     => ! [B] : 
          ( ( v1_group_1(B)
            & m1_group_2(B,A) )
         => ( ( v6_group_1(A)
              & ~ v3_struct_0(A)
              & v3_group_1(A)
              & v4_group_1(A)
              & v1_gr_cy_1(A)
              & l1_group_1(A) )
           => ( ~ v3_struct_0(B)
              & v3_group_1(B)
              & v4_group_1(B)
              & v1_gr_cy_1(B)
              & l1_group_1(B) ) ) ) ) ),
    inference(mizar_proof,[status(thm)],[t42_gr_cy_1,t48_group_2,t90_group_1,t82_group_2,t40_gr_cy_1,t31_gr_cy_1,t51_group_2,t59_group_1,t53_group_2,s5_nat_1,t51_group_2,t42_nat_1,t48_group_1,t3_group_4,t57_group_2,t50_group_1,d4_group_1,d6_group_1,d5_group_1,t52_group_2,t50_group_1,t3_group_4,t42_gr_cy_1,d5_real_1]),
    [file(gr_cy_1,t44_gr_cy_1),interesting(0.89)]).

fof(t28_gr_cy_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))
         => ( v6_group_1(A)
           => r1_nat_1(k7_group_1(A,B),k9_group_1(A)) ) ) ) ),
    inference(mizar_proof,[status(thm)],[t27_gr_cy_1,t178_group_2]),
    [file(gr_cy_1,t28_gr_cy_1),interesting(0.86)]).

fof(t29_gr_cy_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))
         => ( v6_group_1(A)
           => k6_group_1(A,k9_group_1(A),B) = k2_group_1(A) ) ) ) ),
    inference(mizar_proof,[status(thm)],[t28_gr_cy_1,d3_nat_1,t50_group_1,t82_group_1,t42_group_1]),
    [file(gr_cy_1,t29_gr_cy_1),interesting(0.83)]).

fof(t35_gr_cy_1,theorem,(
    k2_group_1(k3_gr_cy_1) = 0 ),
    inference(mizar_proof,[status(thm)],[t14_gr_cy_1,d2_int_1,d2_int_1,t10_group_1]),
    [file(gr_cy_1,t35_gr_cy_1),interesting(0.82)]).

fof(t40_gr_cy_1,theorem,(
    ! [A] : 
      ( ( ~ v3_struct_0(A)
        & v3_group_1(A)
        & v4_group_1(A)
        & l1_group_1(A) )
     => v1_gr_cy_1(k5_group_2(A)) ) ),
    inference(mizar_proof,[status(thm)],[d1_tarski,d7_group_2,d9_gr_cy_1,d7_group_2,d8_group_2,d7_group_2,t66_group_2,d8_group_2,d5_group_4,d8_group_2]),
    [file(gr_cy_1,t40_gr_cy_1),interesting(0.77)]).

fof(t14_gr_cy_1,theorem,(
    ! [A] : 
      ( v1_int_1(A)
     => ! [B] : 
          ( v1_int_1(B)
         => k1_binop_1(k44_binop_2,A,B) = k2_xcmplx_0(A,B) ) ) ),
    inference(mizar_proof,[status(thm)],[d2_int_1,d20_binop_2]),
    [file(gr_cy_1,t14_gr_cy_1),interesting(0.76)]).

fof(t39_gr_cy_1,theorem,(
    ! [A] : 
      ( m1_subset_1(A,u1_struct_0(k3_gr_cy_1))
     => ! [B] : 
          ( v1_int_1(B)
         => ( A = 1
           => B = k6_group_1(k3_gr_cy_1,B,A) ) ) ) ),
    inference(mizar_proof,[status(thm)],[t8_int_1,t38_gr_cy_1,d2_int_1,t71_group_1,t38_gr_cy_1,t37_gr_cy_1]),
    [file(gr_cy_1,t39_gr_cy_1),interesting(0.76)]).

fof(t22_gr_cy_1,theorem,(
    k2_gr_cy_1(k6_finseq_1(k4_numbers)) = 0 ),
    inference(mizar_proof,[status(thm)],[t4_binop_2,t11_finsop_1]),
    [file(gr_cy_1,t22_gr_cy_1),interesting(0.75)]).

fof(t27_gr_cy_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))
         => ( v6_group_1(A)
           => k7_group_1(A,B) = k9_group_1(k5_group_4(A,k1_struct_0(A,B))) ) ) ) ),
    inference(mizar_proof,[status(thm)],[t48_group_2,s2_finseq_1,d3_finseq_1,t26_gr_cy_1,d12_group_1,t8_xreal_1,t38_nat_1,t3_finseq_1,t44_group_1,d5_funct_1,d5_funct_1,t25_gr_cy_1,d1_rlvect_1,d3_tarski,d1_funct_2,d5_group_2,t1_xboole_1,t119_zfmisc_1,t91_relat_1,d5_funct_1,t102_zfmisc_1,t106_zfmisc_1,t106_zfmisc_1,t70_funct_1,t48_group_1,t46_nat_1,t5_finseq_1,t47_nat_1,t48_group_1,t50_group_1,t82_group_1,t42_group_1,d5_group_1,t43_group_1,t82_group_1,t5_finseq_1,t8_xreal_1,t38_nat_1,t3_finseq_1,t47_nat_1,t48_group_1,t50_group_1,t82_group_1,t42_group_1,d5_group_1,d5_funct_1,d3_tarski,d1_funct_2,t11_relset_1,t72_funct_1,d3_tarski,d3_tarski,d3_tarski,d4_group_1,t5_finseq_1,d5_funct_1,t82_group_1,d3_tarski,d5_group_1,d5_group_1,d5_funct_1,t3_finseq_1,t5_finseq_1,t82_group_1,t43_group_1,t18_int_1,t11_xreal_1,t38_nat_1,t29_nat_1,t22_xreal_1,t3_finseq_1,d3_finseq_1,d5_real_1,d5_funct_1,t64_group_1,t82_group_1,t65_group_1,t82_group_1,t5_group_1,d5_group_2,t1_xboole_1,d5_group_2,t37_zfmisc_1,d5_group_4,d5_group_2,d10_xboole_0,d8_funct_1,d5_real_1,t18_int_1,d6_group_1,t43_group_1,t71_group_1,t64_group_1,t43_group_1,t3_finseq_1,t3_finseq_1,t31_xreal_1,t2_xreal_1,t11_xreal_1,t26_gr_cy_1,d12_group_1,d5_real_1,t18_int_1,d6_group_1,t43_group_1,t71_group_1,t64_group_1,t43_group_1,t3_finseq_1,t3_finseq_1,t31_xreal_1,t2_xreal_1,t11_xreal_1,t26_gr_cy_1,d12_group_1,d4_wellord2,d15_group_1,t21_card_1,t78_finseq_1]),
    [file(gr_cy_1,t27_gr_cy_1),interesting(0.75)]).

fof(t26_gr_cy_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))
         => ~ ( v6_group_1(A)
              & v5_group_1(B,A) ) ) ) ),
    inference(mizar_proof,[status(thm)],[s2_finseq_1,d3_finseq_1,d5_funct_1,d3_tarski,d1_funct_2,t11_relset_1,d15_group_1,d11_card_1,t76_finseq_1,t31_xreal_1,t73_card_1,t80_finseq_4,t18_int_1,t64_group_1,t64_group_1,t59_group_1,t18_int_1,t64_group_1,t64_group_1,t59_group_1,d5_real_1,d11_group_1]),
    [file(gr_cy_1,t26_gr_cy_1),interesting(0.74)]).

fof(t13_gr_cy_1,theorem,(
    k1_gr_cy_1(1) = k18_group_2(k5_numbers,0) ),
    inference(mizar_proof,[status(thm)],[d1_gr_cy_1,t38_nat_1,d1_tarski,d1_tarski,t10_gr_cy_1,t2_tarski]),
    [file(gr_cy_1,t13_gr_cy_1),interesting(0.74)]).

fof(t36_gr_cy_1,theorem,(
    ! [A] : 
      ( v4_ordinal2(A)
     => ( ~ r1_xreal_0(A,0)
       => k2_group_1(k5_gr_cy_1(A)) = 0 ) ) ),
    inference(mizar_proof,[status(thm)],[d6_gr_cy_1,d5_gr_cy_1,t10_gr_cy_1,t10_gr_cy_1,t76_nat_1,t76_nat_1,t10_group_1]),
    [file(gr_cy_1,t36_gr_cy_1),interesting(0.73)]).

fof(t37_gr_cy_1,theorem,(
    ! [A] : 
      ( m1_subset_1(A,u1_struct_0(k3_gr_cy_1))
     => k3_group_1(k3_gr_cy_1,A) = k4_xcmplx_0(k6_gr_cy_1(A)) ) ),
    inference(mizar_proof,[status(thm)],[t14_gr_cy_1,d2_int_1,t35_gr_cy_1,t20_group_1]),
    [file(gr_cy_1,t37_gr_cy_1),interesting(0.72)]).

fof(t10_gr_cy_1,theorem,(
    ! [A] : 
      ( v4_ordinal2(A)
     => ! [B] : 
          ( v4_ordinal2(B)
         => ( ~ r1_xreal_0(A,0)
           => ( r2_hidden(B,k1_gr_cy_1(A))
            <=> ~ r1_xreal_0(A,B) ) ) ) ) ),
    inference(mizar_proof,[status(thm)],[d21_ordinal2,d1_gr_cy_1]),
    [file(gr_cy_1,t10_gr_cy_1),interesting(0.72)]).

fof(t42_gr_cy_1,theorem,(
    ! [A] : 
      ( ( ~ v3_struct_0(A)
        & v3_group_1(A)
        & v4_group_1(A)
        & l1_group_1(A) )
     => ( v6_group_1(A)
       => ( ( ~ v3_struct_0(A)
            & v3_group_1(A)
            & v4_group_1(A)
            & v1_gr_cy_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] : 
                      ( m2_subset_1(D,k1_numbers,k5_numbers)
                      & C = k6_group_1(A,D,B) ) ) ) ) ) ) ),
    inference(mizar_proof,[status(thm)],[t41_gr_cy_1,t8_int_1,t90_group_1,t46_nat_1,t18_int_1,t71_group_1,t30_gr_cy_1,t41_gr_cy_1]),
    [file(gr_cy_1,t42_gr_cy_1),interesting(0.68)]).

fof(t43_gr_cy_1,theorem,(
    ! [A] : 
      ( ( ~ v3_struct_0(A)
        & v1_group_1(A)
        & v3_group_1(A)
        & v4_group_1(A)
        & l1_group_1(A) )
     => ( v6_group_1(A)
       => ( ( ~ v3_struct_0(A)
            & v3_group_1(A)
            & v4_group_1(A)
            & v1_gr_cy_1(A)
            & l1_group_1(A) )
        <=> ? [B] : 
              ( m1_subset_1(B,u1_struct_0(A))
              & k7_group_1(A,B) = k9_group_1(A) ) ) ) ) ),
    inference(mizar_proof,[status(thm)],[d9_gr_cy_1,t27_gr_cy_1,t27_gr_cy_1,t85_group_2,d9_gr_cy_1]),
    [file(gr_cy_1,t43_gr_cy_1),interesting(0.68)]).

fof(t46_gr_cy_1,theorem,(
    ! [A] : 
      ( m2_subset_1(A,k1_numbers,k5_numbers)
     => ~ ( ~ r1_xreal_0(A,0)
          & ! [B] : 
              ( m1_subset_1(B,u1_struct_0(k5_gr_cy_1(A)))
             => ? [C] : 
                  ( m1_subset_1(C,u1_struct_0(k5_gr_cy_1(A)))
                  & ! [D] : 
                      ( v1_int_1(D)
                     => C != k6_group_1(k5_gr_cy_1(A),D,B) ) ) ) ) ) ),
    inference(mizar_proof,[status(thm)],[d6_gr_cy_1,d5_gr_cy_1,t8_xreal_1,t38_nat_1,t13_gr_cy_1,t36_gr_cy_1,d7_group_2,t70_group_2,t40_gr_cy_1,t41_gr_cy_1,t10_gr_cy_1,l2_gr_cy_1,t43_group_1,t36_gr_cy_1,t78_nat_1,t46_nat_1,t10_gr_cy_1,t48_group_1,t44_group_1,t74_nat_1,s1_nat_1,t10_gr_cy_1,t76_nat_1,d5_real_1]),
    [file(gr_cy_1,t46_gr_cy_1),interesting(0.68)]).

fof(t50_gr_cy_1,theorem,
    ( ~ v3_struct_0(k3_gr_cy_1)
    & v3_group_1(k3_gr_cy_1)
    & v4_group_1(k3_gr_cy_1)
    & v7_group_1(k3_gr_cy_1)
    & l1_group_1(k3_gr_cy_1) ),
    inference(mizar_proof,[status(thm)],[t48_gr_cy_1]),
    [file(gr_cy_1,t50_gr_cy_1),interesting(0.66)]).

fof(t38_gr_cy_1,theorem,(
    ! [A] : 
      ( m1_subset_1(A,u1_struct_0(k3_gr_cy_1))
     => ( A = 1
       => ! [B] : 
            ( m2_subset_1(B,k1_numbers,k5_numbers)
           => k6_group_1(k3_gr_cy_1,B,A) = B ) ) ) ),
    inference(mizar_proof,[status(thm)],[t35_gr_cy_1,t43_group_1,l49_gr_cy_1,t49_group_1,s1_nat_1]),
    [file(gr_cy_1,t38_gr_cy_1),interesting(0.63)]).

fof(t41_gr_cy_1,theorem,(
    ! [A] : 
      ( ( ~ v3_struct_0(A)
        & v3_group_1(A)
        & v4_group_1(A)
        & l1_group_1(A) )
     => ( ( ~ v3_struct_0(A)
          & v3_group_1(A)
          & v4_group_1(A)
          & v1_gr_cy_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] : 
                    ( v1_int_1(D)
                    & C = k6_group_1(A,D,B) ) ) ) ) ) ),
    inference(mizar_proof,[status(thm)],[d9_gr_cy_1,d1_rlvect_1,t25_gr_cy_1,t25_gr_cy_1,t71_group_2,d9_gr_cy_1]),
    [file(gr_cy_1,t41_gr_cy_1),interesting(0.63)]).

fof(t33_gr_cy_1,theorem,
    ( v4_group_1(g1_group_1(k4_numbers,k44_binop_2))
    & v3_group_1(g1_group_1(k4_numbers,k44_binop_2)) ),
    inference(mizar_proof,[status(thm)],[t14_gr_cy_1,d2_int_1,d4_group_1,d2_int_1,d3_group_1,d2_int_1,d2_int_1]),
    [file(gr_cy_1,t33_gr_cy_1),interesting(0.62)]).

fof(l49_gr_cy_1,theorem,(
    ! [A] : 
      ( m1_subset_1(A,u1_struct_0(k3_gr_cy_1))
     => ! [B] : 
          ( m1_subset_1(B,u1_struct_0(k3_gr_cy_1))
         => ! [C] : 
              ( v1_int_1(C)
             => ! [D] : 
                  ( v1_int_1(D)
                 => ( ( A = C
                      & B = D )
                   => k1_group_1(k3_gr_cy_1,A,B) = k2_xcmplx_0(C,D) ) ) ) ) ) ),
    inference(mizar_proof,[status(thm)],[t14_gr_cy_1]),
    [file(gr_cy_1,l49_gr_cy_1),interesting(0.61)]).

fof(t12_gr_cy_1,theorem,(
    ! [A] : 
      ( v4_ordinal2(A)
     => ( ~ r1_xreal_0(A,0)
       => r2_hidden(0,k1_gr_cy_1(A)) ) ) ),
    inference(mizar_proof,[status(thm)],[t10_gr_cy_1]),
    [file(gr_cy_1,t12_gr_cy_1),interesting(0.60)]).

fof(t21_gr_cy_1,theorem,(
    ! [A] : 
      ( m1_subset_1(A,k4_numbers)
     => k2_gr_cy_1(k12_finseq_1(k4_numbers,A)) = A ) ),
    inference(mizar_proof,[status(thm)],[t12_finsop_1]),
    [file(gr_cy_1,t21_gr_cy_1),interesting(0.59)]).

fof(t49_gr_cy_1,theorem,(
    ! [A] : 
      ( m2_subset_1(A,k1_numbers,k5_numbers)
     => ( ~ r1_xreal_0(A,0)
       => ( ~ v3_struct_0(k5_gr_cy_1(A))
          & v3_group_1(k5_gr_cy_1(A))
          & v4_group_1(k5_gr_cy_1(A))
          & v1_gr_cy_1(k5_gr_cy_1(A))
          & l1_group_1(k5_gr_cy_1(A)) ) ) ) ),
    inference(mizar_proof,[status(thm)],[t46_gr_cy_1,t41_gr_cy_1]),
    [file(gr_cy_1,t49_gr_cy_1),interesting(0.59)]).

fof(t25_gr_cy_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))
             => ( r1_rlvect_1(k5_group_4(A,k1_struct_0(A,C)),B)
              <=> ? [D] : 
                    ( v1_int_1(D)
                    & B = k6_group_1(A,D,C) ) ) ) ) ) ),
    inference(mizar_proof,[status(thm)],[t37_group_4,t68_finseq_2,d3_finseq_1,d3_finseq_1,d5_funct_1,d1_tarski,t70_finseq_2,t17_finseq_1,t24_gr_cy_1,t8_int_1,t69_finseq_2,t69_finseq_2,d2_finseq_2,t19_funcop_1,t69_finseq_2,t31_group_4,t15_group_4,t37_group_4,t70_group_1,t69_finseq_2,t69_finseq_2,d2_finseq_2,t19_funcop_1,t69_finseq_2,t31_group_4,t15_group_4,t37_group_4,t60_group_2,t19_group_1]),
    [file(gr_cy_1,t25_gr_cy_1),interesting(0.57)]).

fof(t15_gr_cy_1,theorem,(
    ! [A] : 
      ( m1_subset_1(A,k4_numbers)
     => ( A = 0
       => r3_binop_1(k4_numbers,A,k44_binop_2) ) ) ),
    inference(mizar_proof,[status(thm)],[t4_binop_2,t22_setwiseo]),
    [file(gr_cy_1,t15_gr_cy_1),interesting(0.55)]).

fof(t20_gr_cy_1,theorem,(
    ! [A] : 
      ( m1_subset_1(A,k4_numbers)
     => ! [B] : 
          ( m2_finseq_1(B,k4_numbers)
         => k2_gr_cy_1(k8_finseq_1(k4_numbers,B,k12_finseq_1(k4_numbers,A))) = k2_xcmplx_0(k2_gr_cy_1(B),k2_group_4(A)) ) ) ),
    inference(mizar_proof,[status(thm)],[t5_finsop_1,d2_group_4,t14_gr_cy_1]),
    [file(gr_cy_1,t20_gr_cy_1),interesting(0.55)]).

fof(l52_gr_cy_1,theorem,(
    ? [A] : 
      ( m1_subset_1(A,u1_struct_0(k3_gr_cy_1))
      & g1_group_1(u1_struct_0(k3_gr_cy_1),u1_group_1(k3_gr_cy_1)) = k5_group_4(k3_gr_cy_1,k1_struct_0(k3_gr_cy_1,A)) ) ),
    inference(mizar_proof,[status(thm)],[d2_int_1,d3_tarski,d1_rlvect_1,d8_group_2,d1_rlvect_1,d2_int_1,d1_tarski,t4_group_4,t39_gr_cy_1,t66_group_2,d8_group_2,d5_group_4,d8_group_2]),
    [file(gr_cy_1,l52_gr_cy_1),interesting(0.54)]).

fof(t34_gr_cy_1,theorem,(
    ! [A] : 
      ( v4_ordinal2(A)
     => ( ~ r1_xreal_0(A,0)
       => ( v4_group_1(g1_group_1(k1_gr_cy_1(A),k4_gr_cy_1(A)))
          & v3_group_1(g1_group_1(k1_gr_cy_1(A),k4_gr_cy_1(A))) ) ) ) ),
    inference(mizar_proof,[status(thm)],[d5_gr_cy_1,t74_nat_1,t74_nat_1,d4_group_1,t10_gr_cy_1,d3_group_1,t10_gr_cy_1,t76_nat_1,t76_nat_1,t28_nat_1,t37_nat_1,t46_nat_1,t10_gr_cy_1,t77_nat_1,t63_nat_1,t76_nat_1,t77_nat_1,d5_real_1,t77_nat_1,t63_nat_1,t76_nat_1,t77_nat_1,d5_real_1]),
    [file(gr_cy_1,t34_gr_cy_1),interesting(0.51)]).

fof(t45_gr_cy_1,theorem,(
    ! [A] : 
      ( m2_subset_1(A,k1_numbers,k5_numbers)
     => ! [B] : 
          ( ( ~ v3_struct_0(B)
            & v1_group_1(B)
            & v3_group_1(B)
            & v4_group_1(B)
            & l1_group_1(B) )
         => ( ( v6_group_1(B)
              & k9_group_1(B) = A
              & v1_int_2(A) )
           => ( ~ v3_struct_0(B)
              & v3_group_1(B)
              & v4_group_1(B)
              & v1_gr_cy_1(B)
              & l1_group_1(B) ) ) ) ) ),
    inference(mizar_proof,[status(thm)],[t28_gr_cy_1,d5_int_2,t85_group_1,d1_tarski,d7_group_2,d3_tarski,d5_group_2,d10_xboole_0,t70_group_2,t81_group_2,d5_int_2,t43_gr_cy_1]),
    [file(gr_cy_1,t45_gr_cy_1),interesting(0.51)]).

fof(t30_gr_cy_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))
             => ( v6_group_1(B)
               => k3_group_1(B,k6_group_1(B,A,C)) = k6_group_1(B,k10_binop_2(k9_group_1(B),k4_nat_1(A,k9_group_1(B))),C) ) ) ) ) ),
    inference(mizar_proof,[status(thm)],[t90_group_1,t46_nat_1,t18_int_1,t48_group_1,t47_nat_1,t64_group_1,t65_group_1,t71_group_1,d6_group_1,d5_group_1,t50_group_1,t29_gr_cy_1,t42_group_1,t20_group_1]),
    [file(gr_cy_1,t30_gr_cy_1),interesting(0.50)]).

fof(t31_gr_cy_1,theorem,(
    ! [A] : 
      ( ( ~ v3_struct_0(A)
        & v1_group_1(A)
        & v3_group_1(A)
        & v4_group_1(A)
        & l1_group_1(A) )
     => ~ ( ~ r1_xreal_0(k9_group_1(A),1)
          & ! [B] : 
              ( m1_subset_1(B,u1_struct_0(A))
             => B = k2_group_1(A) ) ) ) ),
    inference(mizar_proof,[status(thm)],[d1_tarski,d7_group_2,d1_rlvect_1,t71_group_2,t81_group_2]),
    [file(gr_cy_1,t31_gr_cy_1),interesting(0.48)]).

fof(t51_gr_cy_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)
           => ( r1_xreal_0(A,0)
              | r1_tarski(k1_gr_cy_1(A),k1_gr_cy_1(B)) ) ) ) ) ),
    inference(mizar_proof,[status(thm)],[d3_tarski,t10_gr_cy_1,t2_xreal_1,t10_gr_cy_1]),
    [file(gr_cy_1,t51_gr_cy_1),interesting(0.47)]).

fof(t24_gr_cy_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] : 
              ( m2_finseq_1(C,k4_numbers)
             => k3_group_4(A,k4_group_4(A,C,k1_finsop_1(u1_struct_0(A),k3_finseq_1(C),B))) = k6_group_1(A,k2_gr_cy_1(C),B) ) ) ) ),
    inference(mizar_proof,[status(thm)],[l27_gr_cy_1,l28_gr_cy_1,s2_finseq_2]),
    [file(gr_cy_1,t24_gr_cy_1),interesting(0.39)]).

fof(l27_gr_cy_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_4(A,k4_group_4(A,k6_finseq_1(k4_numbers),k1_finsop_1(u1_struct_0(A),k3_finseq_1(k6_finseq_1(k4_numbers)),B))) = k6_group_1(A,k2_gr_cy_1(k6_finseq_1(k4_numbers)),B) ) ) ),
    inference(mizar_proof,[status(thm)],[t27_group_4,t32_finseq_1,t72_finseq_2,t11_group_4,t22_gr_cy_1,t59_group_1]),
    [file(gr_cy_1,l27_gr_cy_1),interesting(0.25)]).

fof(t32_gr_cy_1,theorem,(
    ! [A] : 
      ( m2_subset_1(A,k1_numbers,k5_numbers)
     => ! [B] : 
          ( ( ~ v3_struct_0(B)
            & v1_group_1(B)
            & v3_group_1(B)
            & v4_group_1(B)
            & l1_group_1(B) )
         => ( ( v6_group_1(B)
              & k9_group_1(B) = A
              & v1_int_2(A) )
           => ! [C] : 
                ( ( v1_group_1(C)
                  & m1_group_2(C,B) )
               => ( r1_group_2(B,C,k5_group_2(B))
                  | C = B ) ) ) ) ) ),
    inference(mizar_proof,[status(thm)],[t48_group_2,t178_group_2,d5_int_2,t82_group_2,t85_group_2]),
    [file(gr_cy_1,t32_gr_cy_1),interesting(0.06)]).

fof(d2_int_1,definition,(
    ! [A] : 
      ( v1_int_1(A)
    <=> r2_hidden(A,k4_numbers) ) ),
    file(int_1,d2_int_1),
    [interesting(0.00)]).

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

fof(d1_rlvect_1,definition,(
    ! [A] : 
      ( l1_struct_0(A)
     => ! [B] : 
          ( r1_rlvect_1(A,B)
        <=> r2_hidden(B,u1_struct_0(A)) ) ) ),
    file(rlvect_1,d1_rlvect_1),
    [interesting(0.00)]).

fof(d8_group_2,definition,(
    ! [A] : 
      ( ( ~ v3_struct_0(A)
        & v3_group_1(A)
        & v4_group_1(A)
        & l1_group_1(A) )
     => k6_group_2(A) = g1_group_1(u1_struct_0(A),u1_group_1(A)) ) ),
    file(group_2,d8_group_2),
    [interesting(0.00)]).

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(t4_group_4,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_group_2(D,B)
                 => ! [E] : 
                      ( m1_subset_1(E,u1_struct_0(D))
                     => ( C = E
                       => k6_group_1(B,A,C) = k6_group_1(D,A,E) ) ) ) ) ) ) ),
    file(group_4,t4_group_4),
    [interesting(0.00)]).

fof(t8_int_1,theorem,(
    ! [A] : 
      ( v1_xreal_0(A)
     => ~ ( v1_int_1(A)
          & ! [B] : 
              ( m2_subset_1(B,k1_numbers,k5_numbers)
             => ( A != B
                & A != k1_real_1(B) ) ) ) ) ),
    file(int_1,t8_int_1),
    [interesting(0.00)]).

fof(d20_binop_2,definition,(
    ! [A] : 
      ( ( v1_funct_1(A)
        & v1_funct_2(A,k2_zfmisc_1(k4_numbers,k4_numbers),k4_numbers)
        & m2_relset_1(A,k2_zfmisc_1(k4_numbers,k4_numbers),k4_numbers) )
     => ( A = k44_binop_2
      <=> ! [B] : 
            ( m1_subset_1(B,k4_numbers)
           => ! [C] : 
                ( m1_subset_1(C,k4_numbers)
               => k2_binop_1(k4_numbers,k4_numbers,k4_numbers,A,B,C) = k20_binop_2(B,C) ) ) ) ) ),
    file(binop_2,d20_binop_2),
    [interesting(0.00)]).

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

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

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)) ) ) ) ) ),
    file(group_1,t49_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(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)) ) ) ) ),
    file(group_1,t71_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) ) ) ) ) ) ),
    file(group_1,t20_group_1),
    [interesting(0.00)]).

fof(t66_group_2,theorem,(
    ! [A] : 
      ( ( ~ v3_struct_0(A)
        & v3_group_1(A)
        & v4_group_1(A)
        & l1_group_1(A) )
     => ! [B] : 
          ( m1_group_2(B,A)
         => ! [C] : 
              ( m1_group_2(C,A)
             => ( r1_tarski(u1_struct_0(B),u1_struct_0(C))
               => m1_group_2(B,C) ) ) ) ) ),
    file(group_2,t66_group_2),
    [interesting(0.00)]).

fof(d5_group_4,definition,(
    ! [A] : 
      ( ( ~ v3_struct_0(A)
        & v3_group_1(A)
        & v4_group_1(A)
        & l1_group_1(A) )
     => ! [B] : 
          ( m1_subset_1(B,k1_zfmisc_1(u1_struct_0(A)))
         => ! [C] : 
              ( ( v1_group_1(C)
                & m1_group_2(C,A) )
             => ( C = k5_group_4(A,B)
              <=> ( r1_tarski(B,u1_struct_0(C))
                  & ! [D] : 
                      ( ( v1_group_1(D)
                        & m1_group_2(D,A) )
                     => ( r1_tarski(B,u1_struct_0(D))
                       => m1_group_2(C,D) ) ) ) ) ) ) ) ),
    file(group_4,d5_group_4),
    [interesting(0.00)]).

fof(t11_gr_cy_1,theorem,(
    $true ),
    file(gr_cy_1,t11_gr_cy_1),
    [interesting(0.00)]).

fof(d21_ordinal2,definition,(
    ! [A] : 
      ( v4_ordinal2(A)
    <=> r2_hidden(A,k5_ordinal2) ) ),
    file(ordinal2,d21_ordinal2),
    [interesting(0.00)]).

fof(d1_gr_cy_1,definition,(
    ! [A] : 
      ( v4_ordinal2(A)
     => ( ~ r1_xreal_0(A,0)
       => k1_gr_cy_1(A) = a_1_0_gr_cy_1(A) ) ) ),
    file(gr_cy_1,d1_gr_cy_1),
    [interesting(0.00)]).

fof(t4_binop_2,theorem,(
    k3_binop_1(k4_numbers,k44_binop_2) = 0 ),
    file(binop_2,t4_binop_2),
    [interesting(0.00)]).

fof(t22_setwiseo,theorem,(
    ! [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)
          <=> r3_binop_1(A,k3_binop_1(A,B),B) ) ) ) ),
    file(setwiseo,t22_setwiseo),
    [interesting(0.00)]).

fof(t16_gr_cy_1,theorem,(
    $true ),
    file(gr_cy_1,t16_gr_cy_1),
    [interesting(0.00)]).

fof(t17_gr_cy_1,theorem,(
    $true ),
    file(gr_cy_1,t17_gr_cy_1),
    [interesting(0.00)]).

fof(t18_gr_cy_1,theorem,(
    $true ),
    file(gr_cy_1,t18_gr_cy_1),
    [interesting(0.00)]).

fof(t19_gr_cy_1,theorem,(
    $true ),
    file(gr_cy_1,t19_gr_cy_1),
    [interesting(0.00)]).

fof(t1_gr_cy_1,theorem,(
    $true ),
    file(gr_cy_1,t1_gr_cy_1),
    [interesting(0.00)]).

fof(t12_finsop_1,theorem,(
    ! [A] : 
      ( ~ v1_xboole_0(A)
     => ! [B] : 
          ( m1_subset_1(B,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) )
             => k2_finsop_1(A,k12_finseq_1(A,B),C) = B ) ) ) ),
    file(finsop_1,t12_finsop_1),
    [interesting(0.00)]).

fof(t23_gr_cy_1,theorem,(
    $true ),
    file(gr_cy_1,t23_gr_cy_1),
    [interesting(0.00)]).

fof(t2_gr_cy_1,theorem,(
    $true ),
    file(gr_cy_1,t2_gr_cy_1),
    [interesting(0.00)]).

fof(t48_group_2,theorem,(
    ! [A] : 
      ( ( ~ v3_struct_0(A)
        & v3_group_1(A)
        & l1_group_1(A) )
     => ! [B] : 
          ( m1_group_2(B,A)
         => ( v6_group_1(A)
           => v6_group_1(B) ) ) ) ),
    file(group_2,t48_group_2),
    [interesting(0.00)]).

fof(t178_group_2,theorem,(
    ! [A] : 
      ( ( ~ v3_struct_0(A)
        & v3_group_1(A)
        & v4_group_1(A)
        & l1_group_1(A) )
     => ! [B] : 
          ( m1_group_2(B,A)
         => ( v6_group_1(A)
           => r1_nat_1(k9_group_1(B),k9_group_1(A)) ) ) ) ),
    file(group_2,t178_group_2),
    [interesting(0.00)]).

fof(d5_int_2,definition,(
    ! [A] : 
      ( m2_subset_1(A,k1_numbers,k5_numbers)
     => ( v1_int_2(A)
      <=> ( ~ r1_xreal_0(A,1)
          & ! [B] : 
              ( m2_subset_1(B,k1_numbers,k5_numbers)
             => ~ ( r1_nat_1(B,A)
                  & B != 1
                  & B != A ) ) ) ) ) ),
    file(int_2,d5_int_2),
    [interesting(0.00)]).

fof(t82_group_2,theorem,(
    ! [A] : 
      ( ( ~ v3_struct_0(A)
        & v3_group_1(A)
        & v4_group_1(A)
        & l1_group_1(A) )
     => ! [B] : 
          ( ( v1_group_1(B)
            & m1_group_2(B,A) )
         => ( ( v6_group_1(B)
              & k9_group_1(B) = 1 )
           => r1_group_2(A,B,k5_group_2(A)) ) ) ) ),
    file(group_2,t82_group_2),
    [interesting(0.00)]).

fof(t85_group_2,theorem,(
    ! [A] : 
      ( ( ~ v3_struct_0(A)
        & v1_group_1(A)
        & v3_group_1(A)
        & v4_group_1(A)
        & l1_group_1(A) )
     => ! [B] : 
          ( ( v1_group_1(B)
            & m1_group_2(B,A) )
         => ( ( v6_group_1(A)
              & k9_group_1(A) = k9_group_1(B) )
           => B = A ) ) ) ),
    file(group_2,t85_group_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(d5_gr_cy_1,definition,(
    ! [A] : 
      ( v4_ordinal2(A)
     => ( ~ r1_xreal_0(A,0)
       => ! [B] : 
            ( ( v1_funct_1(B)
              & v1_funct_2(B,k2_zfmisc_1(k1_gr_cy_1(A),k1_gr_cy_1(A)),k1_gr_cy_1(A))
              & m2_relset_1(B,k2_zfmisc_1(k1_gr_cy_1(A),k1_gr_cy_1(A)),k1_gr_cy_1(A)) )
           => ( B = k4_gr_cy_1(A)
            <=> ! [C] : 
                  ( m2_subset_1(C,k5_numbers,k1_gr_cy_1(A))
                 => ! [D] : 
                      ( m2_subset_1(D,k5_numbers,k1_gr_cy_1(A))
                     => k2_binop_1(k1_gr_cy_1(A),k1_gr_cy_1(A),k1_gr_cy_1(A),B,C,D) = k4_nat_1(k1_nat_1(C,D),A) ) ) ) ) ) ) ),
    file(gr_cy_1,d5_gr_cy_1),
    [interesting(0.00)]).

fof(t74_nat_1,theorem,(
    ! [A] : 
      ( v4_ordinal2(A)
     => ! [B] : 
          ( v4_ordinal2(B)
         => ! [C] : 
              ( v4_ordinal2(C)
             => k4_nat_1(k2_xcmplx_0(A,B),C) = k4_nat_1(k2_xcmplx_0(k4_nat_1(A,C),B),C) ) ) ) ),
    file(nat_1,t74_nat_1),
    [interesting(0.00)]).

fof(t76_nat_1,theorem,(
    ! [A] : 
      ( v4_ordinal2(A)
     => ! [B] : 
          ( v4_ordinal2(B)
         => ( ~ r1_xreal_0(A,B)
           => k4_nat_1(B,A) = B ) ) ) ),
    file(nat_1,t76_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(t37_nat_1,theorem,(
    ! [A] : 
      ( v4_ordinal2(A)
     => ! [B] : 
          ( v4_ordinal2(B)
         => ! [C] : 
              ( v4_ordinal2(C)
             => ( r1_xreal_0(A,B)
               => r1_xreal_0(A,k2_xcmplx_0(B,C)) ) ) ) ) ),
    file(nat_1,t37_nat_1),
    [interesting(0.00)]).

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

fof(t77_nat_1,theorem,(
    ! [A] : 
      ( v4_ordinal2(A)
     => k4_nat_1(A,A) = 0 ) ),
    file(nat_1,t77_nat_1),
    [interesting(0.00)]).

fof(t63_nat_1,theorem,(
    ! [A] : 
      ( v4_ordinal2(A)
     => ! [B] : 
          ( v4_ordinal2(B)
         => k4_nat_1(k3_xcmplx_0(A,B),A) = 0 ) ) ),
    file(nat_1,t63_nat_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(t3_gr_cy_1,theorem,(
    $true ),
    file(gr_cy_1,t3_gr_cy_1),
    [interesting(0.00)]).

fof(d9_gr_cy_1,definition,(
    ! [A] : 
      ( ( ~ v3_struct_0(A)
        & v3_group_1(A)
        & v4_group_1(A)
        & l1_group_1(A) )
     => ( v1_gr_cy_1(A)
      <=> ? [B] : 
            ( m1_subset_1(B,u1_struct_0(A))
            & g1_group_1(u1_struct_0(A),u1_group_1(A)) = k5_group_4(A,k1_struct_0(A,B)) ) ) ) ),
    file(gr_cy_1,d9_gr_cy_1),
    [interesting(0.00)]).

fof(t37_group_4,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,k1_zfmisc_1(u1_struct_0(A)))
             => ( r1_rlvect_1(k5_group_4(A,C),B)
              <=> ? [D] : 
                    ( m2_finseq_1(D,u1_struct_0(A))
                    & ? [E] : 
                        ( m2_finseq_1(E,k4_numbers)
                        & k3_finseq_1(D) = k3_finseq_1(E)
                        & r1_tarski(k2_relat_1(D),C)
                        & k3_group_4(A,k4_group_4(A,E,D)) = B ) ) ) ) ) ) ),
    file(group_4,t37_group_4),
    [interesting(0.00)]).

fof(t68_finseq_2,theorem,(
    ! [A] : 
      ( v4_ordinal2(A)
     => ! [B] : k4_finseq_1(k2_finseq_2(A,B)) = k2_finseq_1(A) ) ),
    file(finseq_2,t68_finseq_2),
    [interesting(0.00)]).

fof(d3_finseq_1,definition,(
    ! [A] : 
      ( ( v1_relat_1(A)
        & v1_funct_1(A)
        & v1_finseq_1(A) )
     => ! [B] : 
          ( m2_subset_1(B,k1_numbers,k5_numbers)
         => ( B = k3_finseq_1(A)
          <=> k2_finseq_1(B) = k1_relat_1(A) ) ) ) ),
    file(finseq_1,d3_finseq_1),
    [interesting(0.00)]).

fof(d5_funct_1,definition,(
    ! [A] : 
      ( ( v1_relat_1(A)
        & v1_funct_1(A) )
     => ! [B] : 
          ( B = k2_relat_1(A)
        <=> ! [C] : 
              ( r2_hidden(C,B)
            <=> ? [D] : 
                  ( r2_hidden(D,k1_relat_1(A))
                  & C = k1_funct_1(A,D) ) ) ) ) ),
    file(funct_1,d5_funct_1),
    [interesting(0.00)]).

fof(t70_finseq_2,theorem,(
    ! [A] : 
      ( v4_ordinal2(A)
     => ! [B,C] : 
          ( r2_hidden(B,k2_finseq_1(A))
         => k1_funct_1(k2_finseq_2(A,C),B) = C ) ) ),
    file(finseq_2,t70_finseq_2),
    [interesting(0.00)]).

fof(t17_finseq_1,theorem,(
    ! [A] : 
      ( ( v1_relat_1(A)
        & v1_funct_1(A)
        & v1_finseq_1(A) )
     => ! [B] : 
          ( ( v1_relat_1(B)
            & v1_funct_1(B)
            & v1_finseq_1(B) )
         => ( ( k4_finseq_1(A) = k4_finseq_1(B)
              & ! [C] : 
                  ( m2_subset_1(C,k1_numbers,k5_numbers)
                 => ( r2_hidden(C,k4_finseq_1(A))
                   => k1_funct_1(A,C) = k1_funct_1(B,C) ) ) )
           => A = B ) ) ) ),
    file(finseq_1,t17_finseq_1),
    [interesting(0.00)]).

fof(t27_group_4,theorem,(
    ! [A] : 
      ( ( ~ v3_struct_0(A)
        & v3_group_1(A)
        & v4_group_1(A)
        & l1_group_1(A) )
     => k4_group_4(A,k6_finseq_1(k4_numbers),k6_finseq_1(u1_struct_0(A))) = k1_xboole_0 ) ),
    file(group_4,t27_group_4),
    [interesting(0.00)]).

fof(t32_finseq_1,theorem,(
    ! [A] : 
      ( ( v1_relat_1(A)
        & v1_funct_1(A)
        & v1_finseq_1(A) )
     => ! [B] : 
          ( A = k6_finseq_1(B)
        <=> k3_finseq_1(A) = 0 ) ) ),
    file(finseq_1,t32_finseq_1),
    [interesting(0.00)]).

fof(t72_finseq_2,theorem,(
    ! [A] : k2_finseq_2(0,A) = k1_xboole_0 ),
    file(finseq_2,t72_finseq_2),
    [interesting(0.00)]).

fof(t11_group_4,theorem,(
    ! [A] : 
      ( ( ~ v3_struct_0(A)
        & v2_group_1(A)
        & l1_group_1(A) )
     => k3_group_4(A,k6_finseq_1(u1_struct_0(A))) = k2_group_1(A) ) ),
    file(group_4,t11_group_4),
    [interesting(0.00)]).

fof(t11_finsop_1,theorem,(
    ! [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)
           => k2_finsop_1(A,k6_finseq_1(A),B) = k3_binop_1(A,B) ) ) ) ),
    file(finsop_1,t11_finsop_1),
    [interesting(0.00)]).

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

fof(d2_group_4,definition,(
    ! [A] : 
      ( v1_int_1(A)
     => k2_group_4(A) = A ) ),
    file(group_4,d2_group_4),
    [interesting(0.00)]).

fof(t69_finseq_2,theorem,(
    ! [A] : 
      ( v4_ordinal2(A)
     => ! [B] : k3_finseq_1(k2_finseq_2(A,B)) = A ) ),
    file(finseq_2,t69_finseq_2),
    [interesting(0.00)]).

fof(t57_finseq_1,theorem,(
    ! [A,B] : 
      ( ( v1_relat_1(B)
        & v1_funct_1(B)
        & v1_finseq_1(B) )
     => ( B = k9_finseq_1(A)
      <=> ( k3_finseq_1(B) = 1
          & k1_funct_1(B,1) = A ) ) ) ),
    file(finseq_1,t57_finseq_1),
    [interesting(0.00)]).

fof(t19_finseq_2,theorem,(
    ! [A,B] : 
      ( ( v1_relat_1(B)
        & v1_funct_1(B)
        & v1_finseq_1(B) )
     => k3_finseq_1(k7_finseq_1(B,k9_finseq_1(A))) = k1_nat_1(k3_finseq_1(B),1) ) ),
    file(finseq_2,t19_finseq_2),
    [interesting(0.00)]).

fof(t74_finseq_2,theorem,(
    ! [A] : 
      ( m2_subset_1(A,k1_numbers,k5_numbers)
     => ! [B] : k2_finseq_2(k1_nat_1(A,1),B) = k7_finseq_1(k2_finseq_2(A,B),k9_finseq_1(B)) ) ),
    file(finseq_2,t74_finseq_2),
    [interesting(0.00)]).

fof(t25_group_4,theorem,(
    ! [A] : 
      ( ( ~ v3_struct_0(A)
        & v3_group_1(A)
        & v4_group_1(A)
        & l1_group_1(A) )
     => ! [B] : 
          ( m2_finseq_1(B,u1_struct_0(A))
         => ! [C] : 
              ( m2_finseq_1(C,u1_struct_0(A))
             => ! [D] : 
                  ( m2_finseq_1(D,k4_numbers)
                 => ! [E] : 
                      ( m2_finseq_1(E,k4_numbers)
                     => ( ( k3_finseq_1(B) = k3_finseq_1(D)
                          & k3_finseq_1(C) = k3_finseq_1(E) )
                       => k4_group_4(A,k8_finseq_1(k4_numbers,D,E),k8_finseq_1(u1_struct_0(A),B,C)) = k8_finseq_1(u1_struct_0(A),k4_group_4(A,D,B),k4_group_4(A,E,C)) ) ) ) ) ) ) ),
    file(group_4,t25_group_4),
    [interesting(0.00)]).

fof(t8_group_4,theorem,(
    ! [A] : 
      ( ( ~ v3_struct_0(A)
        & v2_group_1(A)
        & v4_group_1(A)
        & l1_group_1(A) )
     => ! [B] : 
          ( m2_finseq_1(B,u1_struct_0(A))
         => ! [C] : 
              ( m2_finseq_1(C,u1_struct_0(A))
             => k3_group_4(A,k8_finseq_1(u1_struct_0(A),B,C)) = k1_group_1(A,k3_group_4(A,B),k3_group_4(A,C)) ) ) ) ),
    file(group_4,t8_group_4),
    [interesting(0.00)]).

fof(t28_group_4,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))
             => k4_group_4(B,k12_finseq_1(k4_numbers,k2_group_4(A)),k12_finseq_1(u1_struct_0(B),C)) = k12_finseq_1(u1_struct_0(B),k6_group_1(B,A,C)) ) ) ) ),
    file(group_4,t28_group_4),
    [interesting(0.00)]).

fof(t12_group_4,theorem,(
    ! [A] : 
      ( ( ~ v3_struct_0(A)
        & l1_group_1(A) )
     => ! [B] : 
          ( m1_subset_1(B,u1_struct_0(A))
         => k3_group_4(A,k12_finseq_1(u1_struct_0(A),B)) = B ) ) ),
    file(group_4,t12_group_4),
    [interesting(0.00)]).

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

fof(t5_finsop_1,theorem,(
    ! [A] : 
      ( ~ v1_xboole_0(A)
     => ! [B] : 
          ( m1_subset_1(B,A)
         => ! [C] : 
              ( m2_finseq_1(C,A)
             => ! [D] : 
                  ( ( v1_funct_1(D)
                    & v1_funct_2(D,k2_zfmisc_1(A,A),A)
                    & m2_relset_1(D,k2_zfmisc_1(A,A),A) )
                 => ( ( v1_setwiseo(D,A)
                      | r1_xreal_0(1,k3_finseq_1(C)) )
                   => k2_finsop_1(A,k8_finseq_1(A,C,k12_finseq_1(A,B)),D) = k2_binop_1(A,A,A,D,k2_finsop_1(A,C,D),B) ) ) ) ) ) ),
    file(finsop_1,t5_finsop_1),
    [interesting(0.00)]).

fof(l28_gr_cy_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] : 
              ( m2_finseq_1(C,k4_numbers)
             => ! [D] : 
                  ( m1_subset_1(D,k4_numbers)
                 => ( k3_group_4(A,k4_group_4(A,C,k1_finsop_1(u1_struct_0(A),k3_finseq_1(C),B))) = k6_group_1(A,k2_gr_cy_1(C),B)
                   => k3_group_4(A,k4_group_4(A,k8_finseq_1(k4_numbers,C,k12_finseq_1(k4_numbers,D)),k1_finsop_1(u1_struct_0(A),k3_finseq_1(k8_finseq_1(k4_numbers,C,k12_finseq_1(k4_numbers,D))),B))) = k6_group_1(A,k2_gr_cy_1(k8_finseq_1(k4_numbers,C,k12_finseq_1(k4_numbers,D))),B) ) ) ) ) ) ),
    inference(mizar_proof,[status(thm)],[d2_group_4,d2_group_4,t69_finseq_2,t57_finseq_1,t57_finseq_1,t19_finseq_2,t74_finseq_2,t25_group_4,t8_group_4,t28_group_4,t12_group_4,t63_group_1,t20_gr_cy_1]),
    [file(gr_cy_1,l28_gr_cy_1),interesting(0.00)]).

fof(s2_finseq_2,theorem,
    ( ( p1_s2_finseq_2(k6_finseq_1(f1_s2_finseq_2))
      & ! [A] : 
          ( m2_finseq_1(A,f1_s2_finseq_2)
         => ! [B] : 
              ( m1_subset_1(B,f1_s2_finseq_2)
             => ( p1_s2_finseq_2(A)
               => p1_s2_finseq_2(k8_finseq_1(f1_s2_finseq_2,A,k12_finseq_1(f1_s2_finseq_2,B))) ) ) ) )
   => ! [A] : 
        ( m2_finseq_1(A,f1_s2_finseq_2)
       => p1_s2_finseq_2(A) ) ),
    file(finseq_2,s2_finseq_2),
    [interesting(0.00)]).

fof(d2_finseq_2,definition,(
    ! [A] : 
      ( v4_ordinal2(A)
     => ! [B] : k2_finseq_2(A,B) = k2_funcop_1(k2_finseq_1(A),B) ) ),
    file(finseq_2,d2_finseq_2),
    [interesting(0.00)]).

fof(t19_funcop_1,theorem,(
    ! [A,B] : 
      ( k1_relat_1(k2_funcop_1(A,B)) = A
      & r1_tarski(k2_relat_1(k2_funcop_1(A,B)),k1_tarski(B)) ) ),
    file(funcop_1,t19_funcop_1),
    [interesting(0.00)]).

fof(t31_group_4,theorem,(
    ! [A] : 
      ( ( ~ v3_struct_0(A)
        & v3_group_1(A)
        & v4_group_1(A)
        & l1_group_1(A) )
     => ! [B] : 
          ( m2_finseq_1(B,u1_struct_0(A))
         => k4_group_4(A,k1_finsop_1(k4_numbers,k3_finseq_1(B),k2_group_4(1)),B) = B ) ) ),
    file(group_4,t31_group_4),
    [interesting(0.00)]).

fof(t15_group_4,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))
             => k3_group_4(B,k1_finsop_1(u1_struct_0(B),A,C)) = k6_group_1(B,A,C) ) ) ) ),
    file(group_4,t15_group_4),
    [interesting(0.00)]).

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

fof(t60_group_2,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_group_2(C,A)
             => ( r1_rlvect_1(C,B)
               => r1_rlvect_1(C,k3_group_1(A,B)) ) ) ) ) ),
    file(group_2,t60_group_2),
    [interesting(0.00)]).

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

fof(t71_group_2,theorem,(
    ! [A] : 
      ( ( ~ v3_struct_0(A)
        & v3_group_1(A)
        & v4_group_1(A)
        & l1_group_1(A) )
     => ! [B] : 
          ( m1_group_2(B,A)
         => ( ! [C] : 
                ( m1_subset_1(C,u1_struct_0(A))
               => r1_rlvect_1(B,C) )
           => g1_group_1(u1_struct_0(B),u1_group_1(B)) = g1_group_1(u1_struct_0(A),u1_group_1(A)) ) ) ) ),
    file(group_2,t71_group_2),
    [interesting(0.00)]).

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

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

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

fof(t47_nat_1,theorem,(
    ! [A] : 
      ( v4_ordinal2(A)
     => ! [B] : 
          ( v4_ordinal2(B)
         => ( ~ r1_xreal_0(A,0)
           => B = k2_xcmplx_0(k3_xcmplx_0(A,k3_nat_1(B,A)),k4_nat_1(B,A)) ) ) ) ),
    file(nat_1,t47_nat_1),
    [interesting(0.00)]).

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

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)) ) ) ) ) ),
    file(group_1,t65_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(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(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)) ) ) ) ) ),
    file(group_1,t50_group_1),
    [interesting(0.00)]).

fof(s2_finseq_1,theorem,(
    ? [A] : 
      ( v1_relat_1(A)
      & v1_funct_1(A)
      & v1_finseq_1(A)
      & k3_finseq_1(A) = f1_s2_finseq_1
      & ! [B] : 
          ( m2_subset_1(B,k1_numbers,k5_numbers)
         => ( r2_hidden(B,k2_finseq_1(f1_s2_finseq_1))
           => k1_funct_1(A,B) = f2_s2_finseq_1(B) ) ) ) ),
    file(finseq_1,s2_finseq_1),
    [interesting(0.00)]).

fof(d1_funct_2,definition,(
    ! [A,B,C] : 
      ( m2_relset_1(C,A,B)
     => ( ( ( B = k1_xboole_0
           => A = k1_xboole_0 )
         => ( v1_funct_2(C,A,B)
          <=> A = k4_relset_1(A,B,C) ) )
        & ( B = k1_xboole_0
         => ( A = k1_xboole_0
            | ( v1_funct_2(C,A,B)
            <=> C = k1_xboole_0 ) ) ) ) ) ),
    file(funct_2,d1_funct_2),
    [interesting(0.00)]).

fof(t11_relset_1,theorem,(
    ! [A,B,C] : 
      ( v1_relat_1(C)
     => ( ( r1_tarski(k1_relat_1(C),A)
          & r1_tarski(k2_relat_1(C),B) )
       => m2_relset_1(C,A,B) ) ) ),
    file(relset_1,t11_relset_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(d11_card_1,definition,(
    ! [A] : 
      ( v1_finset_1(A)
     => ! [B] : 
          ( m2_subset_1(B,k1_numbers,k5_numbers)
         => ( B = k4_card_1(A)
          <=> k1_card_1(B) = k1_card_1(A) ) ) ) ),
    file(card_1,d11_card_1),
    [interesting(0.00)]).

fof(t76_finseq_1,theorem,(
    ! [A] : 
      ( m2_subset_1(A,k1_numbers,k5_numbers)
     => k1_card_1(k2_finseq_1(A)) = k1_card_1(A) ) ),
    file(finseq_1,t76_finseq_1),
    [interesting(0.00)]).

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

fof(t73_card_1,theorem,(
    ! [A] : 
      ( m2_subset_1(A,k1_numbers,k5_numbers)
     => ! [B] : 
          ( m2_subset_1(B,k1_numbers,k5_numbers)
         => ( r2_hidden(k1_card_1(A),k1_card_1(B))
          <=> ~ r1_xreal_0(B,A) ) ) ) ),
    file(card_1,t73_card_1),
    [interesting(0.00)]).

fof(t80_finseq_4,theorem,(
    ! [A,B,C] : 
      ( ( v1_funct_1(C)
        & v1_funct_2(C,B,A)
        & m2_relset_1(C,B,A) )
     => ~ ( r2_hidden(k1_card_1(A),k1_card_1(B))
          & A != k1_xboole_0
          & ! [D,E] : ~ ( r2_hidden(D,B)
              & r2_hidden(E,B)
              & D != E
              & k1_funct_1(C,D) = k1_funct_1(C,E) ) ) ) ),
    file(finseq_4,t80_finseq_4),
    [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(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(t38_nat_1,theorem,(
    ! [A] : 
      ( v4_ordinal2(A)
     => ! [B] : 
          ( v4_ordinal2(B)
         => ( ~ r1_xreal_0(k2_xcmplx_0(B,1),A)
          <=> r1_xreal_0(A,B) ) ) ) ),
    file(nat_1,t38_nat_1),
    [interesting(0.00)]).

fof(t3_finseq_1,theorem,(
    ! [A] : 
      ( v4_ordinal2(A)
     => ! [B] : 
          ( v4_ordinal2(B)
         => ( r2_hidden(A,k2_finseq_1(B))
          <=> ( r1_xreal_0(1,A)
              & r1_xreal_0(A,B) ) ) ) ) ),
    file(finseq_1,t3_finseq_1),
    [interesting(0.00)]).

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

fof(d5_group_2,definition,(
    ! [A] : 
      ( ( ~ v3_struct_0(A)
        & v3_group_1(A)
        & l1_group_1(A) )
     => ! [B] : 
          ( ( ~ v3_struct_0(B)
            & v3_group_1(B)
            & l1_group_1(B) )
         => ( m1_group_2(B,A)
          <=> ( r1_tarski(u1_struct_0(B),u1_struct_0(A))
              & u1_group_1(B) = k1_realset1(u1_group_1(A),u1_struct_0(B)) ) ) ) ) ),
    file(group_2,d5_group_2),
    [interesting(0.00)]).

fof(t1_xboole_1,theorem,(
    ! [A,B,C] : 
      ( ( r1_tarski(A,B)
        & r1_tarski(B,C) )
     => r1_tarski(A,C) ) ),
    file(xboole_1,t1_xboole_1),
    [interesting(0.00)]).

fof(t119_zfmisc_1,theorem,(
    ! [A,B,C,D] : 
      ( ( r1_tarski(A,B)
        & r1_tarski(C,D) )
     => r1_tarski(k2_zfmisc_1(A,C),k2_zfmisc_1(B,D)) ) ),
    file(zfmisc_1,t119_zfmisc_1),
    [interesting(0.00)]).

fof(t91_relat_1,theorem,(
    ! [A,B] : 
      ( v1_relat_1(B)
     => ( r1_tarski(A,k1_relat_1(B))
       => k1_relat_1(k7_relat_1(B,A)) = A ) ) ),
    file(relat_1,t91_relat_1),
    [interesting(0.00)]).

fof(t102_zfmisc_1,theorem,(
    ! [A,B,C] : ~ ( r2_hidden(A,k2_zfmisc_1(B,C))
      & ! [D,E] : k4_tarski(D,E) != A ) ),
    file(zfmisc_1,t102_zfmisc_1),
    [interesting(0.00)]).

fof(t106_zfmisc_1,theorem,(
    ! [A,B,C,D] : 
      ( r2_hidden(k4_tarski(A,B),k2_zfmisc_1(C,D))
    <=> ( r2_hidden(A,C)
        & r2_hidden(B,D) ) ) ),
    file(zfmisc_1,t106_zfmisc_1),
    [interesting(0.00)]).

fof(t70_funct_1,theorem,(
    ! [A,B,C] : 
      ( ( v1_relat_1(C)
        & v1_funct_1(C) )
     => ( r2_hidden(B,k1_relat_1(k7_relat_1(C,A)))
       => k1_funct_1(k7_relat_1(C,A),B) = k1_funct_1(C,B) ) ) ),
    file(funct_1,t70_funct_1),
    [interesting(0.00)]).

fof(t5_finseq_1,theorem,(
    ! [A] : 
      ( v4_ordinal2(A)
     => ( A = 0
        | r2_hidden(A,k2_finseq_1(A)) ) ) ),
    file(finseq_1,t5_finseq_1),
    [interesting(0.00)]).

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

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

fof(t72_funct_1,theorem,(
    ! [A,B,C] : 
      ( ( v1_relat_1(C)
        & v1_funct_1(C) )
     => ( r2_hidden(B,A)
       => k1_funct_1(k7_relat_1(C,A),B) = k1_funct_1(C,B) ) ) ),
    file(funct_1,t72_funct_1),
    [interesting(0.00)]).

fof(t11_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(k6_xcmplx_0(A,C),k6_xcmplx_0(B,C)) ) ) ) ) ),
    file(xreal_1,t11_xreal_1),
    [interesting(0.00)]).

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

fof(t22_xreal_1,theorem,(
    ! [A] : 
      ( v1_xreal_0(A)
     => ! [B] : 
          ( v1_xreal_0(B)
         => ! [C] : 
              ( v1_xreal_0(C)
             => ( r1_xreal_0(A,k2_xcmplx_0(B,C))
              <=> r1_xreal_0(k6_xcmplx_0(A,B),C) ) ) ) ) ),
    file(xreal_1,t22_xreal_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) ) ) ) ) ),
    file(group_1,t5_group_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(d10_xboole_0,definition,(
    ! [A,B] : 
      ( A = B
    <=> ( r1_tarski(A,B)
        & r1_tarski(B,A) ) ) ),
    file(xboole_0,d10_xboole_0),
    [interesting(0.00)]).

fof(d8_funct_1,definition,(
    ! [A] : 
      ( ( v1_relat_1(A)
        & v1_funct_1(A) )
     => ( v2_funct_1(A)
      <=> ! [B,C] : 
            ( ( r2_hidden(B,k1_relat_1(A))
              & r2_hidden(C,k1_relat_1(A))
              & k1_funct_1(A,B) = k1_funct_1(A,C) )
           => B = C ) ) ) ),
    file(funct_1,d8_funct_1),
    [interesting(0.00)]).

fof(t2_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(B,C) )
               => r1_xreal_0(A,C) ) ) ) ) ),
    file(xreal_1,t2_xreal_1),
    [interesting(0.00)]).

fof(d4_wellord2,definition,(
    ! [A,B] : 
      ( r2_wellord2(A,B)
    <=> ? [C] : 
          ( v1_relat_1(C)
          & v1_funct_1(C)
          & v2_funct_1(C)
          & k1_relat_1(C) = A
          & k2_relat_1(C) = B ) ) ),
    file(wellord2,d4_wellord2),
    [interesting(0.00)]).

fof(t21_card_1,theorem,(
    ! [A,B] : 
      ( r2_wellord2(A,B)
    <=> k1_card_1(A) = k1_card_1(B) ) ),
    file(card_1,t21_card_1),
    [interesting(0.00)]).

fof(t78_finseq_1,theorem,
    ( ! [A] : 
        ( v4_ordinal2(A)
       => k4_card_1(k2_finseq_1(A)) = A )
    & ! [A] : 
        ( m2_subset_1(A,k1_numbers,k5_numbers)
       => ( k4_card_1(A) = A
          & k4_card_1(k1_card_1(A)) = A ) ) ),
    file(finseq_1,t78_finseq_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(d7_group_2,definition,(
    ! [A] : 
      ( ( ~ v3_struct_0(A)
        & v3_group_1(A)
        & v4_group_1(A)
        & l1_group_1(A) )
     => ! [B] : 
          ( ( v1_group_1(B)
            & m1_group_2(B,A) )
         => ( B = k5_group_2(A)
          <=> u1_struct_0(B) = k6_domain_1(u1_struct_0(A),k2_group_1(A)) ) ) ) ),
    file(group_2,d7_group_2),
    [interesting(0.00)]).

fof(t81_group_2,theorem,(
    ! [A] : 
      ( ( ~ v3_struct_0(A)
        & v3_group_1(A)
        & v4_group_1(A)
        & l1_group_1(A) )
     => k9_group_1(k5_group_2(A)) = 1 ) ),
    file(group_2,t81_group_2),
    [interesting(0.00)]).

fof(t51_group_2,theorem,(
    ! [A] : 
      ( ( ~ v3_struct_0(A)
        & v3_group_1(A)
        & l1_group_1(A) )
     => ! [B] : 
          ( m1_group_2(B,A)
         => ! [C] : 
              ( m1_subset_1(C,u1_struct_0(B))
             => m1_subset_1(C,u1_struct_0(A)) ) ) ) ),
    file(group_2,t51_group_2),
    [interesting(0.00)]).

fof(t53_group_2,theorem,(
    ! [A] : 
      ( ( ~ v3_struct_0(A)
        & v3_group_1(A)
        & v4_group_1(A)
        & l1_group_1(A) )
     => ! [B] : 
          ( m1_group_2(B,A)
         => k2_group_1(B) = k2_group_1(A) ) ) ),
    file(group_2,t53_group_2),
    [interesting(0.00)]).

fof(s5_nat_1,theorem,
    ( ? [A] : 
        ( m2_subset_1(A,k1_numbers,k5_numbers)
        & p1_s5_nat_1(A) )
   => ? [A] : 
        ( m2_subset_1(A,k1_numbers,k5_numbers)
        & p1_s5_nat_1(A)
        & ! [B] : 
            ( m2_subset_1(B,k1_numbers,k5_numbers)
           => ( p1_s5_nat_1(B)
             => r1_xreal_0(A,B) ) ) ) ),
    file(nat_1,s5_nat_1),
    [interesting(0.00)]).

fof(t42_nat_1,theorem,(
    ! [A] : 
      ( m2_subset_1(A,k1_numbers,k5_numbers)
     => ( ~ r1_xreal_0(A,0)
       => ! [B] : 
            ( m2_subset_1(B,k1_numbers,k5_numbers)
           => ? [C] : 
                ( m2_subset_1(C,k1_numbers,k5_numbers)
                & ? [D] : 
                    ( m2_subset_1(D,k1_numbers,k5_numbers)
                    & B = k1_nat_1(k2_nat_1(A,C),D)
                    & ~ r1_xreal_0(A,D) ) ) ) ) ) ),
    file(nat_1,t42_nat_1),
    [interesting(0.00)]).

fof(t3_group_4,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_group_2(D,B)
                 => ! [E] : 
                      ( m1_subset_1(E,u1_struct_0(D))
                     => ( C = E
                       => k6_group_1(B,A,C) = k6_group_1(D,A,E) ) ) ) ) ) ) ),
    file(group_4,t3_group_4),
    [interesting(0.00)]).

fof(t57_group_2,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_group_2(C,A)
             => ! [D] : 
                  ( m1_subset_1(D,u1_struct_0(C))
                 => ( D = B
                   => k3_group_1(C,D) = k3_group_1(A,B) ) ) ) ) ) ),
    file(group_2,t57_group_2),
    [interesting(0.00)]).

fof(t52_group_2,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))
             => ! [D] : 
                  ( m1_group_2(D,A)
                 => ! [E] : 
                      ( m1_subset_1(E,u1_struct_0(D))
                     => ! [F] : 
                          ( m1_subset_1(F,u1_struct_0(D))
                         => ( ( E = B
                              & F = C )
                           => k1_group_1(D,E,F) = k1_group_1(A,B,C) ) ) ) ) ) ) ) ),
    file(group_2,t52_group_2),
    [interesting(0.00)]).

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

fof(t70_group_2,theorem,(
    ! [A] : 
      ( ( ~ v3_struct_0(A)
        & v1_group_1(A)
        & v3_group_1(A)
        & v4_group_1(A)
        & l1_group_1(A) )
     => ! [B] : 
          ( ( v1_group_1(B)
            & m1_group_2(B,A) )
         => ( u1_struct_0(B) = u1_struct_0(A)
           => B = A ) ) ) ),
    file(group_2,t70_group_2),
    [interesting(0.00)]).

fof(t47_gr_cy_1,theorem,(
    $true ),
    file(gr_cy_1,t47_gr_cy_1),
    [interesting(0.00)]).

fof(d6_gr_cy_1,definition,(
    ! [A] : 
      ( v4_ordinal2(A)
     => ( ~ r1_xreal_0(A,0)
       => k5_gr_cy_1(A) = g1_group_1(k1_gr_cy_1(A),k4_gr_cy_1(A)) ) ) ),
    file(gr_cy_1,d6_gr_cy_1),
    [interesting(0.00)]).

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

fof(l2_gr_cy_1,theorem,(
    ! [A,B] : 
      ( m2_subset_1(B,k1_numbers,k5_numbers)
     => ( r2_hidden(A,k1_gr_cy_1(B))
       => ( r1_xreal_0(B,0)
          | m2_subset_1(A,k1_numbers,k5_numbers) ) ) ) ),
    file(gr_cy_1,l2_gr_cy_1),
    [interesting(0.00)]).

fof(t78_nat_1,theorem,(
    ! [A] : 
      ( v4_ordinal2(A)
     => 0 = k4_nat_1(0,A) ) ),
    file(nat_1,t78_nat_1),
    [interesting(0.00)]).

fof(t4_gr_cy_1,theorem,(
    $true ),
    file(gr_cy_1,t4_gr_cy_1),
    [interesting(0.00)]).

fof(t5_gr_cy_1,theorem,(
    $true ),
    file(gr_cy_1,t5_gr_cy_1),
    [interesting(0.00)]).

fof(t6_gr_cy_1,theorem,(
    $true ),
    file(gr_cy_1,t6_gr_cy_1),
    [interesting(0.00)]).

fof(t7_gr_cy_1,theorem,(
    $true ),
    file(gr_cy_1,t7_gr_cy_1),
    [interesting(0.00)]).

fof(t8_gr_cy_1,theorem,(
    $true ),
    file(gr_cy_1,t8_gr_cy_1),
    [interesting(0.00)]).

fof(t9_gr_cy_1,theorem,(
    $true ),
    file(gr_cy_1,t9_gr_cy_1),
    [interesting(0.00)]).