fof(t20_asympt_0,theorem,(
    ! [A] : 
      ( ( v1_funct_1(A)
        & v1_funct_2(A,k5_numbers,k1_numbers)
        & v2_asympt_0(A)
        & m2_relset_1(A,k5_numbers,k1_numbers) )
     => r2_hidden(A,k6_asympt_0(A)) ) ),
    inference(mizar_proof,[status(thm)],[t10_asympt_0,t19_asympt_0]),
    [file(asympt_0,t20_asympt_0),interesting(1.00)]).

fof(s2_asympt_0,theorem,
    ( ~ v1_xboole_0(a_0_1_asympt_0)
    & v1_finset_1(a_0_1_asympt_0)
    & m1_subset_1(a_0_1_asympt_0,k1_zfmisc_1(f2_s2_asympt_0)) ),
    inference(mizar_proof,[status(thm)],[s1_asympt_0,t2_tarski]),
    [file(asympt_0,s2_asympt_0),interesting(0.98)]).

fof(t17_asympt_0,theorem,(
    ! [A] : 
      ( ( v1_funct_1(A)
        & v1_funct_2(A,k5_numbers,k1_numbers)
        & v4_asympt_0(A)
        & m2_relset_1(A,k5_numbers,k1_numbers) )
     => ! [B] : 
          ( ( v1_funct_1(B)
            & v1_funct_2(B,k5_numbers,k1_numbers)
            & v4_asympt_0(B)
            & m2_relset_1(B,k5_numbers,k1_numbers) )
         => ( v1_limfunc1(k19_seq_1(A,B))
           => ( ~ r2_hidden(A,k5_asympt_0(B))
              & r2_hidden(B,k5_asympt_0(A)) ) ) ) ) ),
    inference(mizar_proof,[status(thm)],[t5_asympt_0,t16_asympt_0]),
    [file(asympt_0,t17_asympt_0),interesting(0.95)]).

fof(t4_asympt_0,theorem,(
    ! [A] : 
      ( ( v1_funct_1(A)
        & v1_funct_2(A,k5_numbers,k1_numbers)
        & m2_relset_1(A,k5_numbers,k1_numbers) )
     => ! [B] : 
          ( ( v1_funct_1(B)
            & v1_funct_2(B,k5_numbers,k1_numbers)
            & m2_relset_1(B,k5_numbers,k1_numbers) )
         => ( ( v4_seq_2(A)
              & v4_seq_2(B)
              & r1_asympt_0(A,B) )
           => r1_xreal_0(k2_seq_2(A),k2_seq_2(B)) ) ) ) ),
    inference(mizar_proof,[status(thm)],[d11_asympt_0,t25_seq_2,t11_xreal_1,t15_seq_1,t11_seq_1,t14_seq_1,d4_asympt_0,t3_asympt_0,t26_seq_2,t8_xreal_1]),
    [file(asympt_0,t4_asympt_0),interesting(0.93)]).

fof(t28_asympt_0,theorem,(
    ! [A] : 
      ( ( v1_funct_1(A)
        & v1_funct_2(A,k5_numbers,k1_numbers)
        & v2_asympt_0(A)
        & m2_relset_1(A,k5_numbers,k1_numbers) )
     => r2_hidden(A,k7_asympt_0(A)) ) ),
    inference(mizar_proof,[status(thm)],[t10_asympt_0,t20_asympt_0,d3_xboole_0]),
    [file(asympt_0,t28_asympt_0),interesting(0.93)]).

fof(t3_asympt_0,theorem,(
    ! [A] : 
      ( ( v1_funct_1(A)
        & v1_funct_2(A,k5_numbers,k1_numbers)
        & v2_asympt_0(A)
        & m2_relset_1(A,k5_numbers,k1_numbers) )
     => ( v4_seq_2(A)
       => r1_xreal_0(0,k2_seq_2(A)) ) ) ),
    inference(mizar_proof,[status(thm)],[d4_asympt_0,t60_xreal_1,d7_seq_2,t46_square_1,t12_absvalue,t8_xreal_1,d1_absvalue]),
    [file(asympt_0,t3_asympt_0),interesting(0.91)]).

fof(t10_asympt_0,theorem,(
    ! [A] : 
      ( ( v1_funct_1(A)
        & v1_funct_2(A,k5_numbers,k1_numbers)
        & v2_asympt_0(A)
        & m2_relset_1(A,k5_numbers,k1_numbers) )
     => r2_hidden(A,k5_asympt_0(A)) ) ),
    inference(mizar_proof,[status(thm)],[t11_funct_2,d4_asympt_0]),
    [file(asympt_0,t10_asympt_0),interesting(0.89)]).

fof(t22_asympt_0,theorem,(
    ! [A] : 
      ( ( v1_funct_1(A)
        & v1_funct_2(A,k5_numbers,k1_numbers)
        & v4_asympt_0(A)
        & m2_relset_1(A,k5_numbers,k1_numbers) )
     => ! [B] : 
          ( ( v1_funct_1(B)
            & v1_funct_2(B,k5_numbers,k1_numbers)
            & v4_asympt_0(B)
            & m2_relset_1(B,k5_numbers,k1_numbers) )
         => ( v4_seq_2(k19_seq_1(A,B))
           => ( r1_xreal_0(k2_seq_2(k19_seq_1(A,B)),0)
              | k6_asympt_0(A) = k6_asympt_0(B) ) ) ) ) ),
    inference(mizar_proof,[status(thm)],[d4_asympt_0,t10_asympt_0,t15_asympt_0,t19_asympt_0,t21_asympt_0,d4_asympt_0,t10_asympt_0,t15_asympt_0,t19_asympt_0,t21_asympt_0,t2_tarski]),
    [file(asympt_0,t22_asympt_0),interesting(0.89)]).

fof(t24_asympt_0,theorem,(
    ! [A] : 
      ( ( v1_funct_1(A)
        & v1_funct_2(A,k5_numbers,k1_numbers)
        & v4_asympt_0(A)
        & m2_relset_1(A,k5_numbers,k1_numbers) )
     => ! [B] : 
          ( ( v1_funct_1(B)
            & v1_funct_2(B,k5_numbers,k1_numbers)
            & v4_asympt_0(B)
            & m2_relset_1(B,k5_numbers,k1_numbers) )
         => ( v1_limfunc1(k19_seq_1(A,B))
           => ( ~ r2_hidden(B,k6_asympt_0(A))
              & r2_hidden(A,k6_asympt_0(B)) ) ) ) ) ),
    inference(mizar_proof,[status(thm)],[t5_asympt_0,t23_asympt_0]),
    [file(asympt_0,t24_asympt_0),interesting(0.86)]).

fof(t37_asympt_0,theorem,(
    ! [A] : 
      ( ( v1_funct_1(A)
        & v1_funct_2(A,k5_numbers,k1_numbers)
        & v2_asympt_0(A)
        & m2_relset_1(A,k5_numbers,k1_numbers) )
     => ( ? [B] : 
            ( m2_subset_1(B,k1_numbers,k5_numbers)
            & r1_xreal_0(2,B)
            & r2_asympt_0(A,B) )
       => v7_asympt_0(A) ) ) ),
    inference(mizar_proof,[status(thm)],[d19_asympt_0,d8_asympt_0,t46_square_1,t11_funct_2,t2_xreal_1,t2_xreal_1,t65_power,t59_power,d5_int_1,t16_int_1,t48_power,t39_power,t99_newton,t2_xreal_1,d3_power,t10_pre_ff,t48_power,t66_xreal_1,t2_xreal_1,t66_xreal_1,t2_xreal_1,t1_asympt_0,d18_asympt_0,d18_asympt_0,t48_power,t29_power,t29_power,t48_power,t48_power,t32_power,t30_power,t48_power,t99_newton,t48_power,t29_power,t2_xreal_1,t40_power,t48_power,t66_xreal_1,t2_xreal_1,d18_asympt_0,t66_xreal_1,t48_power,t30_power,t32_power,t48_power,t2_xreal_1,s1_nat_1,d18_asympt_0,t2_xreal_1,t70_xreal_1,t1_asympt_0,d18_asympt_0,d19_asympt_0,d20_asympt_0]),
    [file(asympt_0,t37_asympt_0),interesting(0.85)]).

fof(s3_asympt_0,theorem,
    ( ~ r1_xreal_0(f1_s3_asympt_0,0)
   => ( ~ v1_xboole_0(a_0_2_asympt_0)
      & v1_finset_1(a_0_2_asympt_0)
      & m1_subset_1(a_0_2_asympt_0,k1_zfmisc_1(f2_s3_asympt_0)) ) ),
    inference(mizar_proof,[status(thm)],[t22_nat_1,s2_asympt_0,t38_nat_1,t38_nat_1,t2_tarski]),
    [file(asympt_0,s3_asympt_0),interesting(0.84)]).

fof(t27_asympt_0,theorem,(
    ! [A] : 
      ( ( v1_funct_1(A)
        & v1_funct_2(A,k5_numbers,k1_numbers)
        & v2_asympt_0(A)
        & m2_relset_1(A,k5_numbers,k1_numbers) )
     => k7_asympt_0(A) = a_1_2_asympt_0(A) ) ),
    inference(mizar_proof,[status(thm)],[d3_xboole_0,t46_square_1,t2_xreal_1,d4_asympt_0,t46_square_1,t2_xreal_1,t66_xreal_1,t2_xreal_1,t66_xreal_1,d3_xboole_0,t2_tarski]),
    [file(asympt_0,t27_asympt_0),interesting(0.84)]).

fof(s1_asympt_0,theorem,
    ( r1_xreal_0(f1_s1_asympt_0,f2_s1_asympt_0)
   => ( ~ v1_xboole_0(a_0_0_asympt_0)
      & v1_finset_1(a_0_0_asympt_0)
      & m1_subset_1(a_0_0_asympt_0,k1_zfmisc_1(f3_s1_asympt_0)) ) ),
    inference(mizar_proof,[status(thm)],[s1_graph_2,d3_tarski,t2_tarski]),
    [file(asympt_0,s1_asympt_0),interesting(0.83)]).

fof(t35_asympt_0,theorem,(
    ! [A] : 
      ( ( v1_funct_1(A)
        & v1_funct_2(A,k5_numbers,k1_numbers)
        & v4_asympt_0(A)
        & m2_relset_1(A,k5_numbers,k1_numbers) )
     => ! [B] : 
          ( ( v1_funct_1(B)
            & v1_funct_2(B,k5_numbers,k1_numbers)
            & v4_asympt_0(B)
            & m2_relset_1(B,k5_numbers,k1_numbers) )
         => ( v1_limfunc1(k19_seq_1(A,B))
           => ( r2_hidden(A,k6_asympt_0(B))
              & ~ r2_hidden(A,k7_asympt_0(B)) ) ) ) ) ),
    inference(mizar_proof,[status(thm)],[t17_asympt_0,d3_xboole_0,t19_asympt_0]),
    [file(asympt_0,t35_asympt_0),interesting(0.82)]).

fof(t15_asympt_0,theorem,(
    ! [A] : 
      ( ( v1_funct_1(A)
        & v1_funct_2(A,k5_numbers,k1_numbers)
        & v4_asympt_0(A)
        & m2_relset_1(A,k5_numbers,k1_numbers) )
     => ! [B] : 
          ( ( v1_funct_1(B)
            & v1_funct_2(B,k5_numbers,k1_numbers)
            & v4_asympt_0(B)
            & m2_relset_1(B,k5_numbers,k1_numbers) )
         => ( v4_seq_2(k19_seq_1(A,B))
           => ( r1_xreal_0(k2_seq_2(k19_seq_1(A,B)),0)
              | k5_asympt_0(A) = k5_asympt_0(B) ) ) ) ) ),
    inference(mizar_proof,[status(thm)],[l29_asympt_0,t2_asympt_0,t124_xreal_1,l29_asympt_0,l26_asympt_0]),
    [file(asympt_0,t15_asympt_0),interesting(0.80)]).

fof(t36_asympt_0,theorem,(
    ! [A] : 
      ( ( v1_funct_1(A)
        & v1_funct_2(A,k5_numbers,k1_numbers)
        & v2_asympt_0(A)
        & m2_relset_1(A,k5_numbers,k1_numbers) )
     => ! [B] : k10_asympt_0(A,B) = k3_xboole_0(k8_asympt_0(A,B),k9_asympt_0(A,B)) ) ),
    inference(mizar_proof,[status(thm)],[d4_asympt_0,t46_square_1,t2_xreal_1,t66_xreal_1,t2_xreal_1,t66_xreal_1,d3_xboole_0,d3_xboole_0,t46_square_1,t2_xreal_1,t2_tarski]),
    [file(asympt_0,t36_asympt_0),interesting(0.78)]).

fof(t5_asympt_0,theorem,(
    ! [A] : 
      ( ( v1_funct_1(A)
        & v1_funct_2(A,k5_numbers,k1_numbers)
        & m2_relset_1(A,k5_numbers,k1_numbers) )
     => ! [B] : 
          ( ( v1_funct_1(B)
            & v1_funct_2(B,k5_numbers,k1_numbers)
            & v5_asympt_0(B)
            & m2_relset_1(B,k5_numbers,k1_numbers) )
         => ( v1_limfunc1(k19_seq_1(A,B))
           => ( v4_seq_2(k19_seq_1(B,A))
              & k2_seq_2(k19_seq_1(B,A)) = 0 ) ) ) ) ),
    inference(mizar_proof,[status(thm)],[d7_asympt_0,d1_xreal_0,d4_limfunc1,t46_square_1,t2_xreal_1,t70_xreal_1,t107_xcmplx_1,l12_asympt_0,d9_xcmplx_0,d8_seq_1,t12_seq_1,d7_xcmplx_0,d9_seq_1,d8_seq_1,t12_seq_1,d9_seq_1,t70_xreal_1,d7_xcmplx_0,t66_xreal_1,t124_xreal_1,d1_absvalue,t70_xreal_1,t71_xreal_1,d7_xcmplx_0,t66_xreal_1,t203_xcmplx_1,t71_xreal_1,d7_xcmplx_0,d1_absvalue,t71_xreal_1,d6_seq_2,d7_seq_2]),
    [file(asympt_0,t5_asympt_0),interesting(0.75)]).

fof(t23_asympt_0,theorem,(
    ! [A] : 
      ( ( v1_funct_1(A)
        & v1_funct_2(A,k5_numbers,k1_numbers)
        & v4_asympt_0(A)
        & m2_relset_1(A,k5_numbers,k1_numbers) )
     => ! [B] : 
          ( ( v1_funct_1(B)
            & v1_funct_2(B,k5_numbers,k1_numbers)
            & v4_asympt_0(B)
            & m2_relset_1(B,k5_numbers,k1_numbers) )
         => ( ( v4_seq_2(k19_seq_1(A,B))
              & k2_seq_2(k19_seq_1(A,B)) = 0 )
           => ( r2_hidden(B,k6_asympt_0(A))
              & ~ r2_hidden(A,k6_asympt_0(B)) ) ) ) ) ),
    inference(mizar_proof,[status(thm)],[t16_asympt_0,t19_asympt_0]),
    [file(asympt_0,t23_asympt_0),interesting(0.74)]).

fof(t16_asympt_0,theorem,(
    ! [A] : 
      ( ( v1_funct_1(A)
        & v1_funct_2(A,k5_numbers,k1_numbers)
        & v4_asympt_0(A)
        & m2_relset_1(A,k5_numbers,k1_numbers) )
     => ! [B] : 
          ( ( v1_funct_1(B)
            & v1_funct_2(B,k5_numbers,k1_numbers)
            & v4_asympt_0(B)
            & m2_relset_1(B,k5_numbers,k1_numbers) )
         => ( ( v4_seq_2(k19_seq_1(A,B))
              & k2_seq_2(k19_seq_1(A,B)) = 0 )
           => ( r2_hidden(A,k5_asympt_0(B))
              & ~ r2_hidden(B,k5_asympt_0(A)) ) ) ) ) ),
    inference(mizar_proof,[status(thm)],[t11_funct_2,d7_seq_2,d4_asympt_0,d6_asympt_0,t46_square_1,t2_xreal_1,t46_square_1,t2_xreal_1,t2_xreal_1,t12_absvalue,d9_seq_1,t12_seq_1,d8_seq_1,t66_xreal_1,d7_xcmplx_0,t46_square_1,t57_funcop_1,t13_funcop_1,t2_xreal_1,t124_xreal_1,t124_xreal_1,t66_xreal_1,d7_xcmplx_0,t66_xreal_1,d7_xcmplx_0,d9_xcmplx_0,d9_xcmplx_0,l12_asympt_0,d11_asympt_0,t7_absvalue,d6_seq_2,t7_absvalue,d7_seq_2,t4_asympt_0,t66_xreal_1,t107_xcmplx_1]),
    [file(asympt_0,t16_asympt_0),interesting(0.72)]).

fof(t2_asympt_0,theorem,(
    ! [A] : 
      ( ( v1_funct_1(A)
        & v1_funct_2(A,k5_numbers,k1_numbers)
        & v4_asympt_0(A)
        & m2_relset_1(A,k5_numbers,k1_numbers) )
     => ! [B] : 
          ( ( v1_funct_1(B)
            & v1_funct_2(B,k5_numbers,k1_numbers)
            & v4_asympt_0(B)
            & m2_relset_1(B,k5_numbers,k1_numbers) )
         => ( v4_seq_2(k19_seq_1(A,B))
           => ( k2_seq_2(k19_seq_1(A,B)) = 0
              | ( v4_seq_2(k19_seq_1(B,A))
                & k2_seq_2(k19_seq_1(B,A)) = k2_real_1(k2_seq_2(k19_seq_1(A,B))) ) ) ) ) ) ),
    inference(mizar_proof,[status(thm)],[d6_asympt_0,d6_asympt_0,t133_complex1,t133_complex1,t30_seq_2,t98_xreal_1,t3_seq_2,t98_xreal_1,d7_seq_2,t37_nat_1,t37_nat_1,t37_nat_1,t2_xreal_1,t50_xcmplx_1,l12_asympt_0,t6_xcmplx_1,t133_complex1,t151_complex1,t73_real_1,d9_xcmplx_0,d9_xcmplx_0,t4_xcmplx_1,t205_xcmplx_1,d7_xcmplx_0,d9_xcmplx_0,d9_xcmplx_0,l12_asympt_0,t215_xcmplx_1,l12_asympt_0,t11_seq_2,t3_seq_2,t98_xreal_1,t78_xreal_1,d9_xcmplx_0,d7_xcmplx_0,t2_xreal_1,d6_seq_2,d7_seq_2]),
    [file(asympt_0,t2_asympt_0),interesting(0.71)]).

fof(t33_asympt_0,theorem,(
    ! [A] : 
      ( ( v1_funct_1(A)
        & v1_funct_2(A,k5_numbers,k1_numbers)
        & v4_asympt_0(A)
        & m2_relset_1(A,k5_numbers,k1_numbers) )
     => ! [B] : 
          ( ( v1_funct_1(B)
            & v1_funct_2(B,k5_numbers,k1_numbers)
            & v4_asympt_0(B)
            & m2_relset_1(B,k5_numbers,k1_numbers) )
         => ( v4_seq_2(k19_seq_1(A,B))
           => ( r1_xreal_0(k2_seq_2(k19_seq_1(A,B)),0)
              | r2_hidden(A,k7_asympt_0(B)) ) ) ) ) ),
    inference(mizar_proof,[status(thm)],[t15_asympt_0,t10_asympt_0,t10_asympt_0,t19_asympt_0,d3_xboole_0]),
    [file(asympt_0,t33_asympt_0),interesting(0.71)]).

fof(l29_asympt_0,theorem,(
    ! [A] : 
      ( ( v1_funct_1(A)
        & v1_funct_2(A,k5_numbers,k1_numbers)
        & v4_asympt_0(A)
        & m2_relset_1(A,k5_numbers,k1_numbers) )
     => ! [B] : 
          ( ( v1_funct_1(B)
            & v1_funct_2(B,k5_numbers,k1_numbers)
            & v4_asympt_0(B)
            & m2_relset_1(B,k5_numbers,k1_numbers) )
         => ( v4_seq_2(k19_seq_1(A,B))
           => ( r1_xreal_0(k2_seq_2(k19_seq_1(A,B)),0)
              | r2_hidden(A,k5_asympt_0(B)) ) ) ) ) ),
    inference(mizar_proof,[status(thm)],[t70_xreal_1,d7_seq_2,t11_funct_2,d4_asympt_0,d6_asympt_0,t46_square_1,t46_square_1,t2_xreal_1,t2_xreal_1,t12_absvalue,t22_xreal_1,d9_seq_1,t12_seq_1,d8_seq_1,t66_xreal_1,d7_xcmplx_0]),
    [file(asympt_0,l29_asympt_0),interesting(0.63)]).

fof(t34_asympt_0,theorem,(
    ! [A] : 
      ( ( v1_funct_1(A)
        & v1_funct_2(A,k5_numbers,k1_numbers)
        & v4_asympt_0(A)
        & m2_relset_1(A,k5_numbers,k1_numbers) )
     => ! [B] : 
          ( ( v1_funct_1(B)
            & v1_funct_2(B,k5_numbers,k1_numbers)
            & v4_asympt_0(B)
            & m2_relset_1(B,k5_numbers,k1_numbers) )
         => ( ( v4_seq_2(k19_seq_1(A,B))
              & k2_seq_2(k19_seq_1(A,B)) = 0 )
           => ( r2_hidden(A,k5_asympt_0(B))
              & ~ r2_hidden(A,k7_asympt_0(B)) ) ) ) ) ),
    inference(mizar_proof,[status(thm)],[d3_xboole_0,t19_asympt_0,t16_asympt_0,t16_asympt_0]),
    [file(asympt_0,t34_asympt_0),interesting(0.56)]).

fof(t38_asympt_0,theorem,(
    ! [A] : 
      ( ( v1_funct_1(A)
        & v1_funct_2(A,k5_numbers,k1_numbers)
        & v2_asympt_0(A)
        & m2_relset_1(A,k5_numbers,k1_numbers) )
     => ! [B] : 
          ( ( v1_funct_1(B)
            & v1_funct_2(B,k5_numbers,k1_numbers)
            & v2_asympt_0(B)
            & v6_asympt_0(B)
            & m2_relset_1(B,k5_numbers,k1_numbers) )
         => ! [C] : 
              ( m2_subset_1(C,k1_numbers,k5_numbers)
             => ( ( v7_asympt_0(A)
                  & r1_xreal_0(2,C)
                  & r2_hidden(B,k8_asympt_0(A,a_1_3_asympt_0(C))) )
               => r2_hidden(B,k5_asympt_0(A)) ) ) ) ) ),
    inference(mizar_proof,[status(thm)],[d20_asympt_0,d19_asympt_0,d8_asympt_0,d8_asympt_0,d4_asympt_0,t46_square_1,t2_xreal_1,t46_square_1,t2_xreal_1,t2_xreal_1,t66_xreal_1,t2_xreal_1,t70_xreal_1,t11_funct_2,t2_xreal_1,t2_xreal_1,t2_xreal_1,t12_pre_ff,t59_power,t21_int_1,d4_int_1,t8_xreal_1,t8_xreal_1,t16_int_1,t48_power,t99_newton,d3_power,d4_int_1,t10_pre_ff,t30_power,t32_power,t52_int_1,t10_pre_ff,t66_xreal_1,d7_xcmplx_0,d9_xcmplx_0,t9_xreal_1,t16_int_1,t48_power,t2_xreal_1,t1_asympt_0,d18_asympt_0,t66_xreal_1,d7_xcmplx_0,t66_xreal_1,t2_xreal_1,d9_xcmplx_0,t2_xreal_1,t2_xreal_1,t66_xreal_1,t2_xreal_1,t1_asympt_0,t66_xreal_1,t2_xreal_1,t2_xreal_1,t2_xreal_1,t2_xreal_1]),
    [file(asympt_0,t38_asympt_0),interesting(0.52)]).

fof(t39_asympt_0,theorem,(
    ! [A] : 
      ( ( v1_funct_1(A)
        & v1_funct_2(A,k5_numbers,k1_numbers)
        & v2_asympt_0(A)
        & m2_relset_1(A,k5_numbers,k1_numbers) )
     => ! [B] : 
          ( ( v1_funct_1(B)
            & v1_funct_2(B,k5_numbers,k1_numbers)
            & v2_asympt_0(B)
            & v6_asympt_0(B)
            & m2_relset_1(B,k5_numbers,k1_numbers) )
         => ! [C] : 
              ( m2_subset_1(C,k1_numbers,k5_numbers)
             => ( ( v7_asympt_0(A)
                  & r1_xreal_0(2,C)
                  & r2_hidden(B,k9_asympt_0(A,a_1_3_asympt_0(C))) )
               => r2_hidden(B,k6_asympt_0(A)) ) ) ) ) ),
    inference(mizar_proof,[status(thm)],[d20_asympt_0,d19_asympt_0,d8_asympt_0,d8_asympt_0,d4_asympt_0,t46_square_1,t2_xreal_1,t46_square_1,t2_xreal_1,t2_xreal_1,t66_xreal_1,t2_xreal_1,t124_xreal_1,t70_xreal_1,t11_funct_2,t2_xreal_1,t2_xreal_1,t2_xreal_1,t12_pre_ff,t21_int_1,d4_int_1,t8_xreal_1,t8_xreal_1,t59_power,t16_int_1,t48_power,t99_newton,d3_power,d4_int_1,t10_pre_ff,t30_power,t32_power,t52_int_1,t10_pre_ff,t66_xreal_1,d7_xcmplx_0,d9_xcmplx_0,t66_xreal_1,d7_xcmplx_0,t66_xreal_1,t2_xreal_1,d9_xcmplx_0,t2_xreal_1,t2_xreal_1,t1_asympt_0,t2_xreal_1,t2_xreal_1,t66_xreal_1,d7_xcmplx_0,d18_asympt_0,t66_xreal_1,t1_asympt_0,t66_xreal_1,t2_xreal_1,t2_xreal_1,t2_xreal_1,t2_xreal_1]),
    [file(asympt_0,t39_asympt_0),interesting(0.52)]).

fof(t40_asympt_0,theorem,(
    ! [A] : 
      ( ( v1_funct_1(A)
        & v1_funct_2(A,k5_numbers,k1_numbers)
        & v2_asympt_0(A)
        & m2_relset_1(A,k5_numbers,k1_numbers) )
     => ! [B] : 
          ( ( v1_funct_1(B)
            & v1_funct_2(B,k5_numbers,k1_numbers)
            & v2_asympt_0(B)
            & v6_asympt_0(B)
            & m2_relset_1(B,k5_numbers,k1_numbers) )
         => ! [C] : 
              ( m2_subset_1(C,k1_numbers,k5_numbers)
             => ( ( v7_asympt_0(A)
                  & r1_xreal_0(2,C)
                  & r2_hidden(B,k10_asympt_0(A,a_1_3_asympt_0(C))) )
               => r2_hidden(B,k7_asympt_0(A)) ) ) ) ) ),
    inference(mizar_proof,[status(thm)],[t36_asympt_0,d3_xboole_0,t38_asympt_0,t39_asympt_0,d3_xboole_0]),
    [file(asympt_0,t40_asympt_0),interesting(0.39)]).

fof(t25_asympt_0,theorem,(
    ! [A] : 
      ( ( v1_funct_1(A)
        & v1_funct_2(A,k5_numbers,k1_numbers)
        & v3_asympt_0(A)
        & m2_relset_1(A,k5_numbers,k1_numbers) )
     => ! [B] : 
          ( ( v1_funct_1(B)
            & v1_funct_2(B,k5_numbers,k1_numbers)
            & v3_asympt_0(B)
            & m2_relset_1(B,k5_numbers,k1_numbers) )
         => ( r2_hidden(B,k6_asympt_0(A))
          <=> ? [C] : 
                ( m1_subset_1(C,k1_numbers)
                & ~ r1_xreal_0(C,0)
                & ! [D] : 
                    ( m2_subset_1(D,k1_numbers,k5_numbers)
                   => r1_xreal_0(k4_real_1(C,k2_seq_1(k5_numbers,k1_numbers,A,D)),k2_seq_1(k5_numbers,k1_numbers,B,D)) ) ) ) ) ) ),
    inference(mizar_proof,[status(thm)],[s3_asympt_0,d1_sfmastr3,d5_asympt_0,t66_xreal_1,t88_xcmplx_1,d1_xreal_0,d1_sfmastr3,d5_asympt_0,t124_xreal_1,t70_xreal_1,d9_xcmplx_0,d5_asympt_0,t66_xreal_1,t2_xreal_1,d5_asympt_0,t66_xreal_1,t2_xreal_1,t11_funct_2,d5_asympt_0]),
    [file(asympt_0,t25_asympt_0),interesting(0.22)]).

fof(t7_asympt_0,theorem,(
    ! [A] : 
      ( ( v1_funct_1(A)
        & v1_funct_2(A,k5_numbers,k1_numbers)
        & v3_asympt_0(A)
        & m2_relset_1(A,k5_numbers,k1_numbers) )
     => ! [B] : 
          ( ( v1_funct_1(B)
            & v1_funct_2(B,k5_numbers,k1_numbers)
            & v2_asympt_0(B)
            & m2_relset_1(B,k5_numbers,k1_numbers) )
         => ( r2_hidden(B,k5_asympt_0(A))
          <=> ? [C] : 
                ( m1_subset_1(C,k1_numbers)
                & ~ r1_xreal_0(C,0)
                & ! [D] : 
                    ( m2_subset_1(D,k1_numbers,k5_numbers)
                   => r1_xreal_0(k2_seq_1(k5_numbers,k1_numbers,B,D),k4_real_1(C,k2_seq_1(k5_numbers,k1_numbers,A,D))) ) ) ) ) ) ),
    inference(mizar_proof,[status(thm)],[s3_asympt_0,d1_pre_circ,d5_asympt_0,t66_xreal_1,t88_xcmplx_1,d5_asympt_0,t66_xreal_1,t2_xreal_1,d1_xreal_0,d5_asympt_0,t66_xreal_1,t2_xreal_1,t11_funct_2,d4_asympt_0]),
    [file(asympt_0,t7_asympt_0),interesting(0.14)]).

fof(t31_asympt_0,theorem,(
    ! [A] : 
      ( ( v1_funct_1(A)
        & v1_funct_2(A,k5_numbers,k1_numbers)
        & v3_asympt_0(A)
        & m2_relset_1(A,k5_numbers,k1_numbers) )
     => ! [B] : 
          ( ( v1_funct_1(B)
            & v1_funct_2(B,k5_numbers,k1_numbers)
            & v3_asympt_0(B)
            & m2_relset_1(B,k5_numbers,k1_numbers) )
         => ( r2_hidden(B,k7_asympt_0(A))
          <=> ? [C] : 
                ( m1_subset_1(C,k1_numbers)
                & ? [D] : 
                    ( m1_subset_1(D,k1_numbers)
                    & ~ r1_xreal_0(C,0)
                    & ~ r1_xreal_0(D,0)
                    & ! [E] : 
                        ( m2_subset_1(E,k1_numbers,k5_numbers)
                       => ( r1_xreal_0(k4_real_1(D,k2_seq_1(k5_numbers,k1_numbers,A,E)),k2_seq_1(k5_numbers,k1_numbers,B,E))
                          & r1_xreal_0(k2_seq_1(k5_numbers,k1_numbers,B,E),k4_real_1(C,k2_seq_1(k5_numbers,k1_numbers,A,E))) ) ) ) ) ) ) ) ),
    inference(mizar_proof,[status(thm)],[t27_asympt_0,s3_asympt_0,d1_pre_circ,d5_asympt_0,t66_xreal_1,t88_xcmplx_1,d1_sfmastr3,d5_asympt_0,t66_xreal_1,t88_xcmplx_1,t46_square_1,t35_square_1,d5_asympt_0,t124_xreal_1,t70_xreal_1,d9_xcmplx_0,d1_sfmastr3,d1_xreal_0,t46_square_1,t38_square_1,d5_asympt_0,t66_xreal_1,t2_xreal_1,t66_xreal_1,t2_xreal_1,t66_xreal_1,t2_xreal_1,t66_xreal_1,t2_xreal_1,t11_funct_2]),
    [file(asympt_0,t31_asympt_0),interesting(0.12)]).

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

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

fof(d7_xcmplx_0,definition,(
    ! [A] : 
      ( v1_xcmplx_0(A)
     => ! [B] : 
          ( v1_xcmplx_0(B)
         => ( ( A != 0
             => ( B = k5_xcmplx_0(A)
              <=> k3_xcmplx_0(A,B) = 1 ) )
            & ( A = 0
             => ( B = k5_xcmplx_0(A)
              <=> B = 0 ) ) ) ) ) ),
    file(xcmplx_0,d7_xcmplx_0),
    [interesting(0.00)]).

fof(t13_seq_1,theorem,(
    ! [A] : 
      ( v1_xreal_0(A)
     => ! [B] : 
          ( ( v1_funct_1(B)
            & v1_funct_2(B,k5_numbers,k1_numbers)
            & m2_relset_1(B,k5_numbers,k1_numbers) )
         => ! [C] : 
              ( ( v1_funct_1(C)
                & v1_funct_2(C,k5_numbers,k1_numbers)
                & m2_relset_1(C,k5_numbers,k1_numbers) )
             => ( B = k14_seq_1(C,A)
              <=> ! [D] : 
                    ( m2_subset_1(D,k1_numbers,k5_numbers)
                   => k2_seq_1(k5_numbers,k1_numbers,B,D) = k3_xcmplx_0(A,k2_seq_1(k5_numbers,k1_numbers,C,D)) ) ) ) ) ) ),
    file(seq_1,t13_seq_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(t13_asympt_0,theorem,(
    ! [A] : 
      ( ( v1_funct_1(A)
        & v1_funct_2(A,k5_numbers,k1_numbers)
        & v2_asympt_0(A)
        & m2_relset_1(A,k5_numbers,k1_numbers) )
     => ! [B] : 
          ( ( v2_xreal_0(B)
            & m1_subset_1(B,k1_numbers) )
         => k5_asympt_0(A) = k5_asympt_0(k3_asympt_0(A,B)) ) ) ),
    inference(mizar_proof,[status(thm)],[t124_xreal_1,t70_xreal_1,d7_xcmplx_0,t13_seq_1,t70_xreal_1,t13_seq_1,t2_tarski]),
    [file(asympt_0,t13_asympt_0),interesting(0.00)]).

fof(t9_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(A,B)
                      & r1_xreal_0(C,D) )
                   => r1_xreal_0(k2_xcmplx_0(A,C),k2_xcmplx_0(B,D)) ) ) ) ) ) ),
    file(xreal_1,t9_xreal_1),
    [interesting(0.00)]).

fof(d9_asympt_0,definition,(
    ! [A] : 
      ( ( v1_funct_1(A)
        & v1_funct_2(A,k5_numbers,k1_numbers)
        & m2_relset_1(A,k5_numbers,k1_numbers) )
     => ! [B] : 
          ( v1_xreal_0(B)
         => ! [C] : 
              ( ( v1_funct_1(C)
                & v1_funct_2(C,k5_numbers,k1_numbers)
                & m2_relset_1(C,k5_numbers,k1_numbers) )
             => ( C = k2_asympt_0(A,B)
              <=> ! [D] : 
                    ( m2_subset_1(D,k1_numbers,k5_numbers)
                   => k2_seq_1(k5_numbers,k1_numbers,C,D) = k2_xcmplx_0(B,k2_seq_1(k5_numbers,k1_numbers,A,D)) ) ) ) ) ) ),
    file(asympt_0,d9_asympt_0),
    [interesting(0.00)]).

fof(t66_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(0,C) )
               => r1_xreal_0(k3_xcmplx_0(A,C),k3_xcmplx_0(B,C)) ) ) ) ) ),
    file(xreal_1,t66_xreal_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(t14_asympt_0,theorem,(
    ! [A] : 
      ( ( ~ v3_xreal_0(A)
        & m1_subset_1(A,k1_numbers) )
     => ! [B] : 
          ( ( v1_funct_1(B)
            & v1_funct_2(B,k5_numbers,k1_numbers)
            & v2_asympt_0(B)
            & m2_relset_1(B,k5_numbers,k1_numbers) )
         => ! [C] : 
              ( ( v1_funct_1(C)
                & v1_funct_2(C,k5_numbers,k1_numbers)
                & v2_asympt_0(C)
                & m2_relset_1(C,k5_numbers,k1_numbers) )
             => ( r2_hidden(B,k5_asympt_0(C))
               => r2_hidden(B,k5_asympt_0(k2_asympt_0(C,A))) ) ) ) ) ),
    inference(mizar_proof,[status(thm)],[t9_xreal_1,d9_asympt_0,t66_xreal_1,t2_xreal_1]),
    [file(asympt_0,t14_asympt_0),interesting(0.00)]).

fof(d4_asympt_0,definition,(
    ! [A] : 
      ( ( v1_funct_1(A)
        & v1_funct_2(A,k5_numbers,k1_numbers)
        & m2_relset_1(A,k5_numbers,k1_numbers) )
     => ( v2_asympt_0(A)
      <=> ? [B] : 
            ( m2_subset_1(B,k1_numbers,k5_numbers)
            & ! [C] : 
                ( m2_subset_1(C,k1_numbers,k5_numbers)
               => ( r1_xreal_0(B,C)
                 => r1_xreal_0(0,k2_seq_1(k5_numbers,k1_numbers,A,C)) ) ) ) ) ) ),
    file(asympt_0,d4_asympt_0),
    [interesting(0.00)]).

fof(t18_asympt_0,theorem,(
    ! [A,B] : 
      ( ( v1_funct_1(B)
        & v1_funct_2(B,k5_numbers,k1_numbers)
        & v2_asympt_0(B)
        & m2_relset_1(B,k5_numbers,k1_numbers) )
     => ( r2_hidden(A,k6_asympt_0(B))
       => ( v1_funct_1(A)
          & v1_funct_2(A,k5_numbers,k1_numbers)
          & v2_asympt_0(A)
          & m2_relset_1(A,k5_numbers,k1_numbers) ) ) ) ),
    inference(mizar_proof,[status(thm)],[d4_asympt_0]),
    [file(asympt_0,t18_asympt_0),interesting(0.00)]).

fof(t11_funct_2,theorem,(
    ! [A,B,C] : 
      ( ( v1_funct_1(C)
        & v1_funct_2(C,A,B)
        & m2_relset_1(C,A,B) )
     => ( ( B = k1_xboole_0
         => A = k1_xboole_0 )
       => r2_hidden(C,k1_funct_2(A,B)) ) ) ),
    file(funct_2,t11_funct_2),
    [interesting(0.00)]).

fof(d7_seq_2,definition,(
    ! [A] : 
      ( ( v1_funct_1(A)
        & v1_funct_2(A,k5_numbers,k1_numbers)
        & m2_relset_1(A,k5_numbers,k1_numbers) )
     => ( v4_seq_2(A)
       => ! [B] : 
            ( v1_xreal_0(B)
           => ( B = k1_seq_2(A)
            <=> ! [C] : 
                  ( v1_xreal_0(C)
                 => ~ ( ~ r1_xreal_0(C,0)
                      & ! [D] : 
                          ( m2_subset_1(D,k1_numbers,k5_numbers)
                         => ? [E] : 
                              ( m2_subset_1(E,k1_numbers,k5_numbers)
                              & r1_xreal_0(D,E)
                              & r1_xreal_0(C,k18_complex1(k6_xcmplx_0(k2_seq_1(k5_numbers,k1_numbers,A,E),B))) ) ) ) ) ) ) ) ) ),
    file(seq_2,d7_seq_2),
    [interesting(0.00)]).

fof(d6_asympt_0,definition,(
    ! [A] : 
      ( ( v1_funct_1(A)
        & v1_funct_2(A,k5_numbers,k1_numbers)
        & m2_relset_1(A,k5_numbers,k1_numbers) )
     => ( v4_asympt_0(A)
      <=> ? [B] : 
            ( m2_subset_1(B,k1_numbers,k5_numbers)
            & ! [C] : 
                ( m2_subset_1(C,k1_numbers,k5_numbers)
               => ~ ( r1_xreal_0(B,C)
                    & r1_xreal_0(k2_seq_1(k5_numbers,k1_numbers,A,C),0) ) ) ) ) ) ),
    file(asympt_0,d6_asympt_0),
    [interesting(0.00)]).

fof(t46_square_1,theorem,(
    ! [A] : 
      ( v1_xreal_0(A)
     => ! [B] : 
          ( v1_xreal_0(B)
         => r1_xreal_0(A,k2_square_1(A,B)) ) ) ),
    file(square_1,t46_square_1),
    [interesting(0.00)]).

fof(t12_absvalue,theorem,(
    ! [A] : 
      ( v1_xreal_0(A)
     => ! [B] : 
          ( v1_xreal_0(B)
         => ( ( r1_xreal_0(k4_xcmplx_0(A),B)
              & r1_xreal_0(B,A) )
          <=> r1_xreal_0(k18_complex1(B),A) ) ) ) ),
    file(absvalue,t12_absvalue),
    [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(d9_seq_1,definition,(
    ! [A] : 
      ( ( v1_funct_1(A)
        & v1_funct_2(A,k5_numbers,k1_numbers)
        & m2_relset_1(A,k5_numbers,k1_numbers) )
     => ! [B] : 
          ( ( v1_funct_1(B)
            & v1_funct_2(B,k5_numbers,k1_numbers)
            & m2_relset_1(B,k5_numbers,k1_numbers) )
         => k19_seq_1(A,B) = k11_seq_1(A,k18_seq_1(B)) ) ) ),
    file(seq_1,d9_seq_1),
    [interesting(0.00)]).

fof(t12_seq_1,theorem,(
    ! [A] : 
      ( ( v1_funct_1(A)
        & v1_funct_2(A,k5_numbers,k1_numbers)
        & m2_relset_1(A,k5_numbers,k1_numbers) )
     => ! [B] : 
          ( ( v1_funct_1(B)
            & v1_funct_2(B,k5_numbers,k1_numbers)
            & m2_relset_1(B,k5_numbers,k1_numbers) )
         => ! [C] : 
              ( ( v1_funct_1(C)
                & v1_funct_2(C,k5_numbers,k1_numbers)
                & m2_relset_1(C,k5_numbers,k1_numbers) )
             => ( A = k8_seq_1(k5_numbers,k1_numbers,B,C)
              <=> ! [D] : 
                    ( m2_subset_1(D,k1_numbers,k5_numbers)
                   => k2_seq_1(k5_numbers,k1_numbers,A,D) = k4_real_1(k2_seq_1(k5_numbers,k1_numbers,B,D),k2_seq_1(k5_numbers,k1_numbers,C,D)) ) ) ) ) ) ),
    file(seq_1,t12_seq_1),
    [interesting(0.00)]).

fof(d8_seq_1,definition,(
    ! [A] : 
      ( ( v1_funct_1(A)
        & v1_funct_2(A,k5_numbers,k1_numbers)
        & m2_relset_1(A,k5_numbers,k1_numbers) )
     => ! [B] : 
          ( ( v1_funct_1(B)
            & v1_funct_2(B,k5_numbers,k1_numbers)
            & m2_relset_1(B,k5_numbers,k1_numbers) )
         => ( B = k18_seq_1(A)
          <=> ! [C] : 
                ( m2_subset_1(C,k1_numbers,k5_numbers)
               => k2_seq_1(k5_numbers,k1_numbers,B,C) = k2_real_1(k2_seq_1(k5_numbers,k1_numbers,A,C)) ) ) ) ) ),
    file(seq_1,d8_seq_1),
    [interesting(0.00)]).

fof(t133_complex1,theorem,(
    ! [A] : 
      ( v1_xcmplx_0(A)
     => ( ~ ( A != 0
            & r1_xreal_0(k17_complex1(A),0) )
        & ~ ( ~ r1_xreal_0(k17_complex1(A),0)
            & A = 0 ) ) ) ),
    file(complex1,t133_complex1),
    [interesting(0.00)]).

fof(t30_seq_2,theorem,(
    ! [A] : 
      ( ( v1_funct_1(A)
        & v1_funct_2(A,k5_numbers,k1_numbers)
        & m2_relset_1(A,k5_numbers,k1_numbers) )
     => ~ ( v4_seq_2(A)
          & k2_seq_2(A) != 0
          & ! [B] : 
              ( m2_subset_1(B,k1_numbers,k5_numbers)
             => ? [C] : 
                  ( m2_subset_1(C,k1_numbers,k5_numbers)
                  & r1_xreal_0(B,C)
                  & r1_xreal_0(k18_complex1(k2_seq_1(k5_numbers,k1_numbers,A,C)),k6_real_1(k18_complex1(k2_seq_2(A)),2)) ) ) ) ) ),
    file(seq_2,t30_seq_2),
    [interesting(0.00)]).

fof(t98_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(0,A)
                      & r1_xreal_0(0,B)
                      & ~ r1_xreal_0(C,A)
                      & ~ r1_xreal_0(D,B)
                      & r1_xreal_0(k3_xcmplx_0(C,D),k3_xcmplx_0(A,B)) ) ) ) ) ) ),
    file(xreal_1,t98_xreal_1),
    [interesting(0.00)]).

fof(t3_seq_2,theorem,(
    ! [A] : 
      ( v1_xreal_0(A)
     => ( ~ r1_xreal_0(A,0)
       => ( ~ r1_xreal_0(k7_xcmplx_0(A,2),0)
          & ~ r1_xreal_0(k7_xcmplx_0(A,4),0) ) ) ) ),
    file(seq_2,t3_seq_2),
    [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(t50_xcmplx_1,theorem,(
    ! [A] : 
      ( v1_xcmplx_0(A)
     => ! [B] : 
          ( v1_xcmplx_0(B)
         => ~ ( A != 0
              & B != 0
              & k7_xcmplx_0(A,B) = 0 ) ) ) ),
    file(xcmplx_1,t50_xcmplx_1),
    [interesting(0.00)]).

fof(d9_xcmplx_0,definition,(
    ! [A] : 
      ( v1_xcmplx_0(A)
     => ! [B] : 
          ( v1_xcmplx_0(B)
         => k7_xcmplx_0(A,B) = k3_xcmplx_0(A,k5_xcmplx_0(B)) ) ) ),
    file(xcmplx_0,d9_xcmplx_0),
    [interesting(0.00)]).

fof(l12_asympt_0,theorem,(
    ! [A] : 
      ( ( v1_funct_1(A)
        & v1_funct_2(A,k5_numbers,k1_numbers)
        & m2_relset_1(A,k5_numbers,k1_numbers) )
     => ! [B] : 
          ( ( v1_funct_1(B)
            & v1_funct_2(B,k5_numbers,k1_numbers)
            & m2_relset_1(B,k5_numbers,k1_numbers) )
         => ! [C] : 
              ( m2_subset_1(C,k1_numbers,k5_numbers)
             => k2_seq_1(k5_numbers,k1_numbers,k19_seq_1(A,B),C) = k6_real_1(k2_seq_1(k5_numbers,k1_numbers,A,C),k2_seq_1(k5_numbers,k1_numbers,B,C)) ) ) ) ),
    inference(mizar_proof,[status(thm)],[d9_seq_1,t12_seq_1,d8_seq_1,d9_xcmplx_0]),
    [file(asympt_0,l12_asympt_0),interesting(0.00)]).

fof(t6_xcmplx_1,theorem,(
    ! [A] : 
      ( v1_xcmplx_0(A)
     => ! [B] : 
          ( v1_xcmplx_0(B)
         => ~ ( k3_xcmplx_0(A,B) = 0
              & A != 0
              & B != 0 ) ) ) ),
    file(xcmplx_1,t6_xcmplx_1),
    [interesting(0.00)]).

fof(t151_complex1,theorem,(
    ! [A] : 
      ( v1_xcmplx_0(A)
     => ! [B] : 
          ( v1_xcmplx_0(B)
         => k17_complex1(k3_xcmplx_0(A,B)) = k4_real_1(k17_complex1(A),k17_complex1(B)) ) ) ),
    file(complex1,t151_complex1),
    [interesting(0.00)]).

fof(t73_real_1,theorem,(
    ! [A] : 
      ( v1_xreal_0(A)
     => ! [B] : 
          ( v1_xreal_0(B)
         => ! [C] : 
              ( v1_xreal_0(C)
             => ( ~ r1_xreal_0(A,0)
               => ( ~ ( ~ r1_xreal_0(C,B)
                      & r1_xreal_0(k7_xcmplx_0(C,A),k7_xcmplx_0(B,A)) )
                  & ~ ( ~ r1_xreal_0(k7_xcmplx_0(C,A),k7_xcmplx_0(B,A))
                      & r1_xreal_0(C,B) ) ) ) ) ) ) ),
    file(real_1,t73_real_1),
    [interesting(0.00)]).

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

fof(t205_xcmplx_1,theorem,(
    ! [A] : 
      ( v1_xcmplx_0(A)
     => ! [B] : 
          ( v1_xcmplx_0(B)
         => k3_xcmplx_0(k5_xcmplx_0(A),k5_xcmplx_0(B)) = k5_xcmplx_0(k3_xcmplx_0(A,B)) ) ) ),
    file(xcmplx_1,t205_xcmplx_1),
    [interesting(0.00)]).

fof(t215_xcmplx_1,theorem,(
    ! [A] : 
      ( v1_xcmplx_0(A)
     => ! [B] : 
          ( v1_xcmplx_0(B)
         => k5_xcmplx_0(k7_xcmplx_0(A,B)) = k7_xcmplx_0(B,A) ) ) ),
    file(xcmplx_1,t215_xcmplx_1),
    [interesting(0.00)]).

fof(t11_seq_2,theorem,(
    ! [A] : 
      ( v1_xreal_0(A)
     => ! [B] : 
          ( v1_xreal_0(B)
         => ~ ( A != 0
              & B != 0
              & k18_complex1(k6_xcmplx_0(k5_xcmplx_0(A),k5_xcmplx_0(B))) != k6_real_1(k18_complex1(k6_xcmplx_0(A,B)),k4_real_1(k18_complex1(A),k18_complex1(B))) ) ) ) ),
    file(seq_2,t11_seq_2),
    [interesting(0.00)]).

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

fof(d6_seq_2,definition,(
    ! [A] : 
      ( ( v1_funct_1(A)
        & v1_funct_2(A,k5_numbers,k1_numbers)
        & m2_relset_1(A,k5_numbers,k1_numbers) )
     => ( v4_seq_2(A)
      <=> ? [B] : 
            ( v1_xreal_0(B)
            & ! [C] : 
                ( v1_xreal_0(C)
               => ~ ( ~ r1_xreal_0(C,0)
                    & ! [D] : 
                        ( m2_subset_1(D,k1_numbers,k5_numbers)
                       => ? [E] : 
                            ( m2_subset_1(E,k1_numbers,k5_numbers)
                            & r1_xreal_0(D,E)
                            & r1_xreal_0(C,k18_complex1(k6_xcmplx_0(k2_seq_1(k5_numbers,k1_numbers,A,E),B))) ) ) ) ) ) ) ) ),
    file(seq_2,d6_seq_2),
    [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(t11_asympt_0,theorem,(
    ! [A] : 
      ( ( v1_funct_1(A)
        & v1_funct_2(A,k5_numbers,k1_numbers)
        & v2_asympt_0(A)
        & m2_relset_1(A,k5_numbers,k1_numbers) )
     => ! [B] : 
          ( ( v1_funct_1(B)
            & v1_funct_2(B,k5_numbers,k1_numbers)
            & v2_asympt_0(B)
            & m2_relset_1(B,k5_numbers,k1_numbers) )
         => ( r2_hidden(A,k5_asympt_0(B))
           => r1_tarski(k5_asympt_0(A),k5_asympt_0(B)) ) ) ) ),
    inference(mizar_proof,[status(thm)],[d3_tarski,d4_asympt_0,t46_square_1,t2_xreal_1,t46_square_1,t46_square_1,t2_xreal_1,t46_square_1,t2_xreal_1,t66_xreal_1,t66_xreal_1,t2_xreal_1,t2_xreal_1]),
    [file(asympt_0,t11_asympt_0),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(l26_asympt_0,theorem,(
    ! [A] : 
      ( ( v1_funct_1(A)
        & v1_funct_2(A,k5_numbers,k1_numbers)
        & v2_asympt_0(A)
        & m2_relset_1(A,k5_numbers,k1_numbers) )
     => ! [B] : 
          ( ( v1_funct_1(B)
            & v1_funct_2(B,k5_numbers,k1_numbers)
            & v2_asympt_0(B)
            & m2_relset_1(B,k5_numbers,k1_numbers) )
         => ( ( r2_hidden(A,k5_asympt_0(B))
              & r2_hidden(B,k5_asympt_0(A)) )
          <=> k5_asympt_0(A) = k5_asympt_0(B) ) ) ) ),
    inference(mizar_proof,[status(thm)],[t11_asympt_0,d10_xboole_0,t10_asympt_0]),
    [file(asympt_0,l26_asympt_0),interesting(0.00)]).

fof(t19_asympt_0,theorem,(
    ! [A] : 
      ( ( v1_funct_1(A)
        & v1_funct_2(A,k5_numbers,k1_numbers)
        & v2_asympt_0(A)
        & m2_relset_1(A,k5_numbers,k1_numbers) )
     => ! [B] : 
          ( ( v1_funct_1(B)
            & v1_funct_2(B,k5_numbers,k1_numbers)
            & v2_asympt_0(B)
            & m2_relset_1(B,k5_numbers,k1_numbers) )
         => ( r2_hidden(A,k6_asympt_0(B))
          <=> r2_hidden(B,k5_asympt_0(A)) ) ) ) ),
    inference(mizar_proof,[status(thm)],[t11_funct_2,t11_funct_2,t124_xreal_1,d4_asympt_0,t46_square_1,t2_xreal_1,t66_xreal_1,d7_xcmplx_0,t124_xreal_1,d4_asympt_0,t46_square_1,t2_xreal_1,t66_xreal_1,d7_xcmplx_0]),
    [file(asympt_0,t19_asympt_0),interesting(0.00)]).

fof(t12_asympt_0,theorem,(
    ! [A] : 
      ( ( v1_funct_1(A)
        & v1_funct_2(A,k5_numbers,k1_numbers)
        & v2_asympt_0(A)
        & m2_relset_1(A,k5_numbers,k1_numbers) )
     => ! [B] : 
          ( ( v1_funct_1(B)
            & v1_funct_2(B,k5_numbers,k1_numbers)
            & v2_asympt_0(B)
            & m2_relset_1(B,k5_numbers,k1_numbers) )
         => ! [C] : 
              ( ( v1_funct_1(C)
                & v1_funct_2(C,k5_numbers,k1_numbers)
                & v2_asympt_0(C)
                & m2_relset_1(C,k5_numbers,k1_numbers) )
             => ( ( r2_hidden(A,k5_asympt_0(B))
                  & r2_hidden(B,k5_asympt_0(C)) )
               => r2_hidden(A,k5_asympt_0(C)) ) ) ) ) ),
    inference(mizar_proof,[status(thm)],[t11_asympt_0]),
    [file(asympt_0,t12_asympt_0),interesting(0.00)]).

fof(t21_asympt_0,theorem,(
    ! [A] : 
      ( ( v1_funct_1(A)
        & v1_funct_2(A,k5_numbers,k1_numbers)
        & v2_asympt_0(A)
        & m2_relset_1(A,k5_numbers,k1_numbers) )
     => ! [B] : 
          ( ( v1_funct_1(B)
            & v1_funct_2(B,k5_numbers,k1_numbers)
            & v2_asympt_0(B)
            & m2_relset_1(B,k5_numbers,k1_numbers) )
         => ! [C] : 
              ( ( v1_funct_1(C)
                & v1_funct_2(C,k5_numbers,k1_numbers)
                & v2_asympt_0(C)
                & m2_relset_1(C,k5_numbers,k1_numbers) )
             => ( ( r2_hidden(A,k6_asympt_0(B))
                  & r2_hidden(B,k6_asympt_0(C)) )
               => r2_hidden(A,k6_asympt_0(C)) ) ) ) ) ),
    inference(mizar_proof,[status(thm)],[t19_asympt_0,t12_asympt_0,t19_asympt_0]),
    [file(asympt_0,t21_asympt_0),interesting(0.00)]).

fof(d7_asympt_0,definition,(
    ! [A] : 
      ( ( v1_funct_1(A)
        & v1_funct_2(A,k5_numbers,k1_numbers)
        & m2_relset_1(A,k5_numbers,k1_numbers) )
     => ( v5_asympt_0(A)
      <=> ? [B] : 
            ( m2_subset_1(B,k1_numbers,k5_numbers)
            & ! [C] : 
                ( m2_subset_1(C,k1_numbers,k5_numbers)
               => ~ ( r1_xreal_0(B,C)
                    & k2_seq_1(k5_numbers,k1_numbers,A,C) = 0 ) ) ) ) ) ),
    file(asympt_0,d7_asympt_0),
    [interesting(0.00)]).

fof(d1_xreal_0,definition,(
    ! [A] : 
      ( v1_xreal_0(A)
    <=> r2_hidden(A,k1_numbers) ) ),
    file(xreal_0,d1_xreal_0),
    [interesting(0.00)]).

fof(d4_limfunc1,definition,(
    ! [A] : 
      ( ( v1_funct_1(A)
        & v1_funct_2(A,k5_numbers,k1_numbers)
        & m2_relset_1(A,k5_numbers,k1_numbers) )
     => ( v1_limfunc1(A)
      <=> ! [B] : 
            ( m1_subset_1(B,k1_numbers)
           => ? [C] : 
                ( m2_subset_1(C,k1_numbers,k5_numbers)
                & ! [D] : 
                    ( m2_subset_1(D,k1_numbers,k5_numbers)
                   => ~ ( r1_xreal_0(C,D)
                        & r1_xreal_0(k2_seq_1(k5_numbers,k1_numbers,A,D),B) ) ) ) ) ) ) ),
    file(limfunc1,d4_limfunc1),
    [interesting(0.00)]).

fof(t107_xcmplx_1,theorem,(
    ! [A] : 
      ( v1_xcmplx_0(A)
     => ( A != 0
       => k3_xcmplx_0(A,k7_xcmplx_0(1,A)) = 1 ) ) ),
    file(xcmplx_1,t107_xcmplx_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(t71_xreal_1,theorem,(
    ! [A] : 
      ( v1_xreal_0(A)
     => ! [B] : 
          ( v1_xreal_0(B)
         => ! [C] : 
              ( v1_xreal_0(C)
             => ~ ( ~ r1_xreal_0(0,A)
                  & ~ r1_xreal_0(C,B)
                  & r1_xreal_0(k3_xcmplx_0(B,A),k3_xcmplx_0(C,A)) ) ) ) ) ),
    file(xreal_1,t71_xreal_1),
    [interesting(0.00)]).

fof(t203_xcmplx_1,theorem,(
    k5_xcmplx_0(0) = 0 ),
    file(xcmplx_1,t203_xcmplx_1),
    [interesting(0.00)]).

fof(t57_funcop_1,theorem,(
    ! [A,B,C] : 
      ( r2_hidden(C,B)
     => ( v1_funct_1(k2_funcop_1(A,C))
        & v1_funct_2(k2_funcop_1(A,C),A,B)
        & m2_relset_1(k2_funcop_1(A,C),A,B) ) ) ),
    file(funcop_1,t57_funcop_1),
    [interesting(0.00)]).

fof(t13_funcop_1,theorem,(
    ! [A,B,C] : 
      ( r2_hidden(B,A)
     => k1_funct_1(k2_funcop_1(A,C),B) = C ) ),
    file(funcop_1,t13_funcop_1),
    [interesting(0.00)]).

fof(d11_asympt_0,definition,(
    ! [A] : 
      ( ( v1_funct_1(A)
        & v1_funct_2(A,k5_numbers,k1_numbers)
        & m2_relset_1(A,k5_numbers,k1_numbers) )
     => ! [B] : 
          ( ( v1_funct_1(B)
            & v1_funct_2(B,k5_numbers,k1_numbers)
            & m2_relset_1(B,k5_numbers,k1_numbers) )
         => ( r1_asympt_0(A,B)
          <=> ? [C] : 
                ( m2_subset_1(C,k1_numbers,k5_numbers)
                & ! [D] : 
                    ( m2_subset_1(D,k1_numbers,k5_numbers)
                   => ( r1_xreal_0(C,D)
                     => r1_xreal_0(k2_seq_1(k5_numbers,k1_numbers,A,D),k2_seq_1(k5_numbers,k1_numbers,B,D)) ) ) ) ) ) ) ),
    file(asympt_0,d11_asympt_0),
    [interesting(0.00)]).

fof(t7_absvalue,theorem,(
    ! [A] : 
      ( v1_xreal_0(A)
     => ( A = 0
      <=> k18_complex1(A) = 0 ) ) ),
    file(absvalue,t7_absvalue),
    [interesting(0.00)]).

fof(t25_seq_2,theorem,(
    ! [A] : 
      ( ( v1_funct_1(A)
        & v1_funct_2(A,k5_numbers,k1_numbers)
        & m2_relset_1(A,k5_numbers,k1_numbers) )
     => ! [B] : 
          ( ( v1_funct_1(B)
            & v1_funct_2(B,k5_numbers,k1_numbers)
            & m2_relset_1(B,k5_numbers,k1_numbers) )
         => ( ( v4_seq_2(A)
              & v4_seq_2(B) )
           => v4_seq_2(k10_seq_1(A,B)) ) ) ) ),
    file(seq_2,t25_seq_2),
    [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(t15_seq_1,theorem,(
    ! [A] : 
      ( ( v1_funct_1(A)
        & v1_funct_2(A,k5_numbers,k1_numbers)
        & m2_relset_1(A,k5_numbers,k1_numbers) )
     => ! [B] : 
          ( ( v1_funct_1(B)
            & v1_funct_2(B,k5_numbers,k1_numbers)
            & m2_relset_1(B,k5_numbers,k1_numbers) )
         => k10_seq_1(A,B) = k9_seq_1(A,k17_seq_1(B)) ) ) ),
    file(seq_1,t15_seq_1),
    [interesting(0.00)]).

fof(t11_seq_1,theorem,(
    ! [A] : 
      ( ( v1_funct_1(A)
        & v1_funct_2(A,k5_numbers,k1_numbers)
        & m2_relset_1(A,k5_numbers,k1_numbers) )
     => ! [B] : 
          ( ( v1_funct_1(B)
            & v1_funct_2(B,k5_numbers,k1_numbers)
            & m2_relset_1(B,k5_numbers,k1_numbers) )
         => ! [C] : 
              ( ( v1_funct_1(C)
                & v1_funct_2(C,k5_numbers,k1_numbers)
                & m2_relset_1(C,k5_numbers,k1_numbers) )
             => ( A = k6_seq_1(k5_numbers,k1_numbers,B,C)
              <=> ! [D] : 
                    ( m2_subset_1(D,k1_numbers,k5_numbers)
                   => k2_seq_1(k5_numbers,k1_numbers,A,D) = k3_real_1(k2_seq_1(k5_numbers,k1_numbers,B,D),k2_seq_1(k5_numbers,k1_numbers,C,D)) ) ) ) ) ) ),
    file(seq_1,t11_seq_1),
    [interesting(0.00)]).

fof(t14_seq_1,theorem,(
    ! [A] : 
      ( ( v1_funct_1(A)
        & v1_funct_2(A,k5_numbers,k1_numbers)
        & m2_relset_1(A,k5_numbers,k1_numbers) )
     => ! [B] : 
          ( ( v1_funct_1(B)
            & v1_funct_2(B,k5_numbers,k1_numbers)
            & m2_relset_1(B,k5_numbers,k1_numbers) )
         => ( A = k17_seq_1(B)
          <=> ! [C] : 
                ( m2_subset_1(C,k1_numbers,k5_numbers)
               => k2_seq_1(k5_numbers,k1_numbers,A,C) = k1_real_1(k2_seq_1(k5_numbers,k1_numbers,B,C)) ) ) ) ) ),
    file(seq_1,t14_seq_1),
    [interesting(0.00)]).

fof(t60_xreal_1,theorem,(
    ! [A] : 
      ( v1_xreal_0(A)
     => ( ~ ( ~ r1_xreal_0(0,A)
            & r1_xreal_0(k4_xcmplx_0(A),0) )
        & ~ ( ~ r1_xreal_0(k4_xcmplx_0(A),0)
            & r1_xreal_0(0,A) ) ) ) ),
    file(xreal_1,t60_xreal_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(t26_seq_2,theorem,(
    ! [A] : 
      ( ( v1_funct_1(A)
        & v1_funct_2(A,k5_numbers,k1_numbers)
        & m2_relset_1(A,k5_numbers,k1_numbers) )
     => ! [B] : 
          ( ( v1_funct_1(B)
            & v1_funct_2(B,k5_numbers,k1_numbers)
            & m2_relset_1(B,k5_numbers,k1_numbers) )
         => ( ( v4_seq_2(A)
              & v4_seq_2(B) )
           => k2_seq_2(k10_seq_1(A,B)) = k5_real_1(k2_seq_2(A),k2_seq_2(B)) ) ) ) ),
    file(seq_2,t26_seq_2),
    [interesting(0.00)]).

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

fof(s1_graph_2,theorem,(
    v1_finset_1(a_0_0_graph_2) ),
    file(graph_2,s1_graph_2),
    [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(d1_sfmastr3,definition,(
    ! [A] : 
      ( ( ~ v1_xboole_0(A)
        & v1_finset_1(A)
        & v2_membered(A) )
     => ! [B] : 
          ( v1_xreal_0(B)
         => ( B = k3_seq_4(A)
          <=> ( r2_hidden(B,A)
              & ! [C] : 
                  ( v1_xreal_0(C)
                 => ( r2_hidden(C,A)
                   => r1_xreal_0(B,C) ) ) ) ) ) ) ),
    file(sfmastr3,d1_sfmastr3),
    [interesting(0.00)]).

fof(d5_asympt_0,definition,(
    ! [A] : 
      ( ( v1_funct_1(A)
        & v1_funct_2(A,k5_numbers,k1_numbers)
        & m2_relset_1(A,k5_numbers,k1_numbers) )
     => ( v3_asympt_0(A)
      <=> ! [B] : 
            ( m2_subset_1(B,k1_numbers,k5_numbers)
           => ~ r1_xreal_0(k2_seq_1(k5_numbers,k1_numbers,A,B),0) ) ) ) ),
    file(asympt_0,d5_asympt_0),
    [interesting(0.00)]).

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

fof(d10_asympt_0,definition,(
    ! [A] : 
      ( ( v1_funct_1(A)
        & v1_funct_2(A,k5_numbers,k1_numbers)
        & m2_relset_1(A,k5_numbers,k1_numbers) )
     => ! [B] : 
          ( ( v1_funct_1(B)
            & v1_funct_2(B,k5_numbers,k1_numbers)
            & m2_relset_1(B,k5_numbers,k1_numbers) )
         => ! [C] : 
              ( ( v1_funct_1(C)
                & v1_funct_2(C,k5_numbers,k1_numbers)
                & m2_relset_1(C,k5_numbers,k1_numbers) )
             => ( C = k4_asympt_0(A,B)
              <=> ! [D] : 
                    ( m2_subset_1(D,k1_numbers,k5_numbers)
                   => k2_seq_1(k5_numbers,k1_numbers,C,D) = k4_square_1(k2_seq_1(k5_numbers,k1_numbers,A,D),k2_seq_1(k5_numbers,k1_numbers,B,D)) ) ) ) ) ) ),
    file(asympt_0,d10_asympt_0),
    [interesting(0.00)]).

fof(t49_square_1,theorem,(
    ! [A] : 
      ( v1_xreal_0(A)
     => ! [B] : 
          ( v1_xreal_0(B)
         => ( k2_square_1(A,B) = A
            | k2_square_1(A,B) = B ) ) ) ),
    file(square_1,t49_square_1),
    [interesting(0.00)]).

fof(t26_asympt_0,theorem,(
    ! [A] : 
      ( ( v1_funct_1(A)
        & v1_funct_2(A,k5_numbers,k1_numbers)
        & v2_asympt_0(A)
        & m2_relset_1(A,k5_numbers,k1_numbers) )
     => ! [B] : 
          ( ( v1_funct_1(B)
            & v1_funct_2(B,k5_numbers,k1_numbers)
            & v2_asympt_0(B)
            & m2_relset_1(B,k5_numbers,k1_numbers) )
         => k6_asympt_0(k1_asympt_0(A,B)) = k6_asympt_0(k4_asympt_0(A,B)) ) ) ),
    inference(mizar_proof,[status(thm)],[d4_asympt_0,d4_asympt_0,t46_square_1,t2_xreal_1,t2_xreal_1,d10_asympt_0,t9_xreal_1,t11_seq_1,t9_xreal_1,t11_seq_1,t49_square_1,t66_xreal_1,t2_xreal_1,t70_xreal_1,t46_square_1,t2_xreal_1,t46_square_1,t2_xreal_1,t46_square_1,t9_xreal_1,t66_xreal_1,t11_seq_1,t66_xreal_1,d10_asympt_0,t2_xreal_1,t2_tarski]),
    [file(asympt_0,t26_asympt_0),interesting(0.00)]).

fof(d3_xboole_0,definition,(
    ! [A,B,C] : 
      ( C = k3_xboole_0(A,B)
    <=> ! [D] : 
          ( r2_hidden(D,C)
        <=> ( r2_hidden(D,A)
            & r2_hidden(D,B) ) ) ) ),
    file(xboole_0,d3_xboole_0),
    [interesting(0.00)]).

fof(t29_asympt_0,theorem,(
    ! [A] : 
      ( ( v1_funct_1(A)
        & v1_funct_2(A,k5_numbers,k1_numbers)
        & v2_asympt_0(A)
        & m2_relset_1(A,k5_numbers,k1_numbers) )
     => ! [B] : 
          ( ( v1_funct_1(B)
            & v1_funct_2(B,k5_numbers,k1_numbers)
            & v2_asympt_0(B)
            & m2_relset_1(B,k5_numbers,k1_numbers) )
         => ( r2_hidden(A,k7_asympt_0(B))
           => r2_hidden(B,k7_asympt_0(A)) ) ) ) ),
    inference(mizar_proof,[status(thm)],[d3_xboole_0,t19_asympt_0,d3_xboole_0]),
    [file(asympt_0,t29_asympt_0),interesting(0.00)]).

fof(t30_asympt_0,theorem,(
    ! [A] : 
      ( ( v1_funct_1(A)
        & v1_funct_2(A,k5_numbers,k1_numbers)
        & v2_asympt_0(A)
        & m2_relset_1(A,k5_numbers,k1_numbers) )
     => ! [B] : 
          ( ( v1_funct_1(B)
            & v1_funct_2(B,k5_numbers,k1_numbers)
            & v2_asympt_0(B)
            & m2_relset_1(B,k5_numbers,k1_numbers) )
         => ! [C] : 
              ( ( v1_funct_1(C)
                & v1_funct_2(C,k5_numbers,k1_numbers)
                & v2_asympt_0(C)
                & m2_relset_1(C,k5_numbers,k1_numbers) )
             => ( ( r2_hidden(A,k7_asympt_0(B))
                  & r2_hidden(B,k7_asympt_0(C)) )
               => r2_hidden(A,k7_asympt_0(C)) ) ) ) ) ),
    inference(mizar_proof,[status(thm)],[d3_xboole_0,d3_xboole_0,t12_asympt_0,t21_asympt_0,d3_xboole_0]),
    [file(asympt_0,t30_asympt_0),interesting(0.00)]).

fof(d1_pre_circ,definition,(
    ! [A] : 
      ( ( ~ v1_xboole_0(A)
        & v1_finset_1(A)
        & v2_membered(A) )
     => ! [B] : 
          ( v1_xreal_0(B)
         => ( B = k1_pre_circ(A)
          <=> ( r2_hidden(B,A)
              & ! [C] : 
                  ( v1_xreal_0(C)
                 => ( r2_hidden(C,A)
                   => r1_xreal_0(C,B) ) ) ) ) ) ) ),
    file(pre_circ,d1_pre_circ),
    [interesting(0.00)]).

fof(t35_square_1,theorem,(
    ! [A] : 
      ( v1_xreal_0(A)
     => ! [B] : 
          ( v1_xreal_0(B)
         => r1_xreal_0(k1_square_1(A,B),A) ) ) ),
    file(square_1,t35_square_1),
    [interesting(0.00)]).

fof(t38_square_1,theorem,(
    ! [A] : 
      ( v1_xreal_0(A)
     => ! [B] : 
          ( v1_xreal_0(B)
         => ( k1_square_1(A,B) = A
            | k1_square_1(A,B) = B ) ) ) ),
    file(square_1,t38_square_1),
    [interesting(0.00)]).

fof(t32_asympt_0,theorem,(
    ! [A] : 
      ( ( v1_funct_1(A)
        & v1_funct_2(A,k5_numbers,k1_numbers)
        & v2_asympt_0(A)
        & m2_relset_1(A,k5_numbers,k1_numbers) )
     => ! [B] : 
          ( ( v1_funct_1(B)
            & v1_funct_2(B,k5_numbers,k1_numbers)
            & v2_asympt_0(B)
            & m2_relset_1(B,k5_numbers,k1_numbers) )
         => k7_asympt_0(k1_asympt_0(A,B)) = k7_asympt_0(k4_asympt_0(A,B)) ) ) ),
    inference(mizar_proof,[status(thm)],[t27_asympt_0,t27_asympt_0,d4_asympt_0,d4_asympt_0,t70_xreal_1,t46_square_1,t46_square_1,t2_xreal_1,t2_xreal_1,t11_seq_1,d10_asympt_0,t46_square_1,t9_xreal_1,t66_xreal_1,t9_xreal_1,t11_seq_1,t9_xreal_1,t11_seq_1,t49_square_1,t66_xreal_1,t2_xreal_1,d4_asympt_0,d4_asympt_0,t70_xreal_1,t46_square_1,t2_xreal_1,t46_square_1,t2_xreal_1,d10_asympt_0,t11_seq_1,t9_xreal_1,t49_square_1,t66_xreal_1,t46_square_1,t9_xreal_1,t66_xreal_1,t11_seq_1,t66_xreal_1,d10_asympt_0,t2_xreal_1,t2_tarski]),
    [file(asympt_0,t32_asympt_0),interesting(0.00)]).

fof(d19_asympt_0,definition,(
    ! [A] : 
      ( ( v1_funct_1(A)
        & v1_funct_2(A,k5_numbers,k1_numbers)
        & v2_asympt_0(A)
        & m2_relset_1(A,k5_numbers,k1_numbers) )
     => ! [B] : 
          ( m2_subset_1(B,k1_numbers,k5_numbers)
         => ( r2_asympt_0(A,B)
          <=> ( v6_asympt_0(A)
              & r2_hidden(k11_asympt_0(A,B),k5_asympt_0(A)) ) ) ) ) ),
    file(asympt_0,d19_asympt_0),
    [interesting(0.00)]).

fof(d8_asympt_0,definition,(
    ! [A] : 
      ( ( v1_funct_1(A)
        & v1_funct_2(A,k5_numbers,k1_numbers)
        & m2_relset_1(A,k5_numbers,k1_numbers) )
     => ( v6_asympt_0(A)
      <=> ? [B] : 
            ( m2_subset_1(B,k1_numbers,k5_numbers)
            & ! [C] : 
                ( m2_subset_1(C,k1_numbers,k5_numbers)
               => ( r1_xreal_0(B,C)
                 => r1_xreal_0(k2_seq_1(k5_numbers,k1_numbers,A,C),k2_seq_1(k5_numbers,k1_numbers,A,k1_nat_1(C,1))) ) ) ) ) ) ),
    file(asympt_0,d8_asympt_0),
    [interesting(0.00)]).

fof(t65_power,theorem,(
    ! [A] : 
      ( v1_xreal_0(A)
     => ! [B] : 
          ( v1_xreal_0(B)
         => ! [C] : 
              ( v1_xreal_0(C)
             => ~ ( ~ r1_xreal_0(A,1)
                  & ~ r1_xreal_0(B,0)
                  & ~ r1_xreal_0(C,B)
                  & r1_xreal_0(k5_power(A,C),k5_power(A,B)) ) ) ) ) ),
    file(power,t65_power),
    [interesting(0.00)]).

fof(t59_power,theorem,(
    ! [A] : 
      ( v1_xreal_0(A)
     => ~ ( ~ r1_xreal_0(A,0)
          & A != 1
          & k5_power(A,1) != 0 ) ) ),
    file(power,t59_power),
    [interesting(0.00)]).

fof(d5_int_1,definition,(
    ! [A] : 
      ( v1_xreal_0(A)
     => ! [B] : 
          ( v1_int_1(B)
         => ( B = k2_int_1(A)
          <=> ( r1_xreal_0(A,B)
              & ~ r1_xreal_0(k2_xcmplx_0(A,1),B) ) ) ) ) ),
    file(int_1,d5_int_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(t48_power,theorem,(
    ! [A] : 
      ( v1_xreal_0(A)
     => ! [B] : 
          ( m2_subset_1(B,k1_numbers,k5_numbers)
         => ( A != 0
           => k3_power(A,B) = k2_newton(A,B) ) ) ) ),
    file(power,t48_power),
    [interesting(0.00)]).

fof(t39_power,theorem,(
    ! [A] : 
      ( v1_xreal_0(A)
     => ! [B] : 
          ( v1_xreal_0(B)
         => ~ ( ~ r1_xreal_0(A,0)
              & r1_xreal_0(k3_power(A,B),0) ) ) ) ),
    file(power,t39_power),
    [interesting(0.00)]).

fof(t99_newton,theorem,(
    ! [A] : 
      ( m2_subset_1(A,k1_numbers,k5_numbers)
     => ! [B] : 
          ( m2_subset_1(B,k1_numbers,k5_numbers)
         => m2_subset_1(k3_newton(B,A),k1_numbers,k5_numbers) ) ) ),
    file(newton,t99_newton),
    [interesting(0.00)]).

fof(d3_power,definition,(
    ! [A] : 
      ( v1_xreal_0(A)
     => ! [B] : 
          ( v1_xreal_0(B)
         => ~ ( ~ r1_xreal_0(A,0)
              & A != 1
              & ~ r1_xreal_0(B,0)
              & ~ ! [C] : 
                    ( v1_xreal_0(C)
                   => ( C = k5_power(A,B)
                    <=> k3_power(A,C) = B ) ) ) ) ) ),
    file(power,d3_power),
    [interesting(0.00)]).

fof(t10_pre_ff,theorem,(
    ! [A] : 
      ( v1_xreal_0(A)
     => ! [B] : 
          ( v1_xreal_0(B)
         => ! [C] : 
              ( v1_xreal_0(C)
             => ( r1_xreal_0(A,B)
               => ( r1_xreal_0(C,1)
                  | r1_xreal_0(k3_power(C,A),k3_power(C,B)) ) ) ) ) ) ),
    file(pre_ff,t10_pre_ff),
    [interesting(0.00)]).

fof(s1_int_2,theorem,
    ( ( p1_s1_int_2(f1_s1_int_2)
      & ! [A] : 
          ( m2_subset_1(A,k1_numbers,k5_numbers)
         => ( ( r1_xreal_0(f1_s1_int_2,A)
              & p1_s1_int_2(A) )
           => p1_s1_int_2(k1_nat_1(A,1)) ) ) )
   => ! [A] : 
        ( m2_subset_1(A,k1_numbers,k5_numbers)
       => ( r1_xreal_0(f1_s1_int_2,A)
         => p1_s1_int_2(A) ) ) ),
    file(int_2,s1_int_2),
    [interesting(0.00)]).

fof(t1_asympt_0,theorem,(
    ! [A] : 
      ( ( v1_funct_1(A)
        & v1_funct_2(A,k5_numbers,k1_numbers)
        & m2_relset_1(A,k5_numbers,k1_numbers) )
     => ! [B] : 
          ( m2_subset_1(B,k1_numbers,k5_numbers)
         => ( ! [C] : 
                ( m2_subset_1(C,k1_numbers,k5_numbers)
               => ( r1_xreal_0(B,C)
                 => r1_xreal_0(k2_seq_1(k5_numbers,k1_numbers,A,C),k2_seq_1(k5_numbers,k1_numbers,A,k1_nat_1(C,1))) ) )
           => ! [C] : 
                ( m2_subset_1(C,k1_numbers,k5_numbers)
               => ! [D] : 
                    ( m2_subset_1(D,k1_numbers,k5_numbers)
                   => ( ( r1_xreal_0(B,C)
                        & r1_xreal_0(C,D) )
                     => r1_xreal_0(k2_seq_1(k5_numbers,k1_numbers,A,C),k2_seq_1(k5_numbers,k1_numbers,A,D)) ) ) ) ) ) ) ),
    inference(mizar_proof,[status(thm)],[t2_xreal_1,t2_xreal_1,s1_int_2]),
    [file(asympt_0,t1_asympt_0),interesting(0.00)]).

fof(d18_asympt_0,definition,(
    ! [A] : 
      ( ( v1_funct_1(A)
        & v1_funct_2(A,k5_numbers,k1_numbers)
        & m2_relset_1(A,k5_numbers,k1_numbers) )
     => ! [B] : 
          ( m2_subset_1(B,k1_numbers,k5_numbers)
         => ! [C] : 
              ( ( v1_funct_1(C)
                & v1_funct_2(C,k5_numbers,k1_numbers)
                & m2_relset_1(C,k5_numbers,k1_numbers) )
             => ( C = k11_asympt_0(A,B)
              <=> ! [D] : 
                    ( m2_subset_1(D,k1_numbers,k5_numbers)
                   => k2_seq_1(k5_numbers,k1_numbers,C,D) = k2_seq_1(k5_numbers,k1_numbers,A,k2_nat_1(B,D)) ) ) ) ) ) ),
    file(asympt_0,d18_asympt_0),
    [interesting(0.00)]).

fof(t29_power,theorem,(
    ! [A] : 
      ( v1_xreal_0(A)
     => k3_power(A,0) = 1 ) ),
    file(power,t29_power),
    [interesting(0.00)]).

fof(t32_power,theorem,(
    ! [A] : 
      ( v1_xreal_0(A)
     => ! [B] : 
          ( v1_xreal_0(B)
         => ! [C] : 
              ( v1_xreal_0(C)
             => ( ~ r1_xreal_0(A,0)
               => k3_power(A,k2_xcmplx_0(B,C)) = k3_xcmplx_0(k3_power(A,B),k3_power(A,C)) ) ) ) ) ),
    file(power,t32_power),
    [interesting(0.00)]).

fof(t30_power,theorem,(
    ! [A] : 
      ( v1_xreal_0(A)
     => k3_power(A,1) = A ) ),
    file(power,t30_power),
    [interesting(0.00)]).

fof(t40_power,theorem,(
    ! [A] : 
      ( v1_xreal_0(A)
     => ! [B] : 
          ( v1_xreal_0(B)
         => ~ ( ~ r1_xreal_0(A,1)
              & ~ r1_xreal_0(B,0)
              & r1_xreal_0(k3_power(A,B),1) ) ) ) ),
    file(power,t40_power),
    [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(d20_asympt_0,definition,(
    ! [A] : 
      ( ( v1_funct_1(A)
        & v1_funct_2(A,k5_numbers,k1_numbers)
        & v2_asympt_0(A)
        & m2_relset_1(A,k5_numbers,k1_numbers) )
     => ( v7_asympt_0(A)
      <=> ! [B] : 
            ( m2_subset_1(B,k1_numbers,k5_numbers)
           => ( r1_xreal_0(2,B)
             => r2_asympt_0(A,B) ) ) ) ) ),
    file(asympt_0,d20_asympt_0),
    [interesting(0.00)]).

fof(t12_pre_ff,theorem,(
    ! [A] : 
      ( v1_xreal_0(A)
     => ! [B] : 
          ( v1_xreal_0(B)
         => ! [C] : 
              ( v1_xreal_0(C)
             => ( r1_xreal_0(B,C)
               => ( r1_xreal_0(A,1)
                  | r1_xreal_0(B,0)
                  | r1_xreal_0(k5_power(A,B),k5_power(A,C)) ) ) ) ) ) ),
    file(pre_ff,t12_pre_ff),
    [interesting(0.00)]).

fof(t21_int_1,theorem,(
    ! [A] : 
      ( v1_int_1(A)
     => ( ~ r1_xreal_0(0,A)
       => r1_xreal_0(A,k1_real_1(1)) ) ) ),
    file(int_1,t21_int_1),
    [interesting(0.00)]).

fof(d4_int_1,definition,(
    ! [A] : 
      ( v1_xreal_0(A)
     => ! [B] : 
          ( v1_int_1(B)
         => ( B = k1_int_1(A)
          <=> ( r1_xreal_0(B,A)
              & ~ r1_xreal_0(B,k6_xcmplx_0(A,1)) ) ) ) ) ),
    file(int_1,d4_int_1),
    [interesting(0.00)]).

fof(t52_int_1,theorem,(
    ! [A] : 
      ( v1_xreal_0(A)
     => ~ r1_xreal_0(k2_xcmplx_0(k1_int_1(A),1),A) ) ),
    file(int_1,t52_int_1),
    [interesting(0.00)]).

fof(s3_funct_2,theorem,
    ( ! [A] : 
        ( m1_subset_1(A,f1_s3_funct_2)
       => ? [B] : 
            ( m1_subset_1(B,f2_s3_funct_2)
            & p1_s3_funct_2(A,B) ) )
   => ? [A] : 
        ( v1_funct_1(A)
        & v1_funct_2(A,f1_s3_funct_2,f2_s3_funct_2)
        & m2_relset_1(A,f1_s3_funct_2,f2_s3_funct_2)
        & ! [B] : 
            ( m1_subset_1(B,f1_s3_funct_2)
           => p1_s3_funct_2(B,k8_funct_2(f1_s3_funct_2,f2_s3_funct_2,A,B)) ) ) ),
    file(funct_2,s3_funct_2),
    [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(t41_asympt_0,theorem,(
    ! [A] : 
      ( ( v1_funct_1(A)
        & v1_funct_2(A,k5_numbers,k1_numbers)
        & v2_asympt_0(A)
        & m2_relset_1(A,k5_numbers,k1_numbers) )
     => ! [B] : 
          ( ( v1_funct_1(B)
            & v1_funct_2(B,k5_numbers,k1_numbers)
            & v2_asympt_0(B)
            & m2_relset_1(B,k5_numbers,k1_numbers) )
         => k12_asympt_0(k5_numbers,k5_asympt_0(A),k5_asympt_0(B)) = k5_asympt_0(k1_asympt_0(A,B)) ) ) ),
    inference(mizar_proof,[status(thm)],[t46_square_1,t46_square_1,t46_square_1,t2_xreal_1,t70_xreal_1,t66_xreal_1,t2_xreal_1,t8_xreal_1,t2_xreal_1,t11_seq_1,t8_xreal_1,d4_asympt_0,d4_asympt_0,t46_square_1,t2_xreal_1,s3_funct_2,s3_funct_2,t11_funct_2,t2_xreal_1,t66_xreal_1,t2_xreal_1,t66_xreal_1,t21_xreal_1,t11_seq_1,t22_xreal_1,t2_tarski]),
    [file(asympt_0,t41_asympt_0),interesting(0.00)]).

fof(t50_square_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(C,B) )
              <=> r1_xreal_0(k2_square_1(A,C),B) ) ) ) ) ),
    file(square_1,t50_square_1),
    [interesting(0.00)]).

fof(d2_square_1,definition,(
    ! [A] : 
      ( v1_xreal_0(A)
     => ! [B] : 
          ( v1_xreal_0(B)
         => ( ( r1_xreal_0(B,A)
             => k2_square_1(A,B) = A )
            & ( ~ r1_xreal_0(B,A)
             => k2_square_1(A,B) = B ) ) ) ) ),
    file(square_1,d2_square_1),
    [interesting(0.00)]).

fof(t42_asympt_0,theorem,(
    ! [A] : 
      ( ( v1_funct_1(A)
        & v1_funct_2(A,k5_numbers,k1_numbers)
        & v2_asympt_0(A)
        & m2_relset_1(A,k5_numbers,k1_numbers) )
     => ! [B] : 
          ( ( v1_funct_1(B)
            & v1_funct_2(B,k5_numbers,k1_numbers)
            & v2_asympt_0(B)
            & m2_relset_1(B,k5_numbers,k1_numbers) )
         => k13_asympt_0(k5_numbers,k5_asympt_0(A),k5_asympt_0(B)) = k5_asympt_0(k4_asympt_0(A,B)) ) ) ),
    inference(mizar_proof,[status(thm)],[t46_square_1,t46_square_1,t46_square_1,t2_xreal_1,t70_xreal_1,t66_xreal_1,t2_xreal_1,t46_square_1,t66_xreal_1,t2_xreal_1,t50_square_1,d10_asympt_0,t46_square_1,d4_asympt_0,d4_asympt_0,t46_square_1,t2_xreal_1,s3_funct_2,s3_funct_2,t11_funct_2,t2_xreal_1,t66_xreal_1,d2_square_1,d10_asympt_0,t2_xreal_1,t66_xreal_1,d2_square_1,d10_asympt_0,t2_xreal_1,d2_square_1,d2_square_1,t2_tarski]),
    [file(asympt_0,t42_asympt_0),interesting(0.00)]).

fof(t6_asympt_0,theorem,(
    ! [A,B] : 
      ( ( v1_funct_1(B)
        & v1_funct_2(B,k5_numbers,k1_numbers)
        & v2_asympt_0(B)
        & m2_relset_1(B,k5_numbers,k1_numbers) )
     => ( r2_hidden(A,k5_asympt_0(B))
       => ( v1_funct_1(A)
          & v1_funct_2(A,k5_numbers,k1_numbers)
          & v2_asympt_0(A)
          & m2_relset_1(A,k5_numbers,k1_numbers) ) ) ) ),
    inference(mizar_proof,[status(thm)],[d4_asympt_0]),
    [file(asympt_0,t6_asympt_0),interesting(0.00)]).

fof(t8_asympt_0,theorem,(
    ! [A] : 
      ( ( v1_funct_1(A)
        & v1_funct_2(A,k5_numbers,k1_numbers)
        & v4_asympt_0(A)
        & m2_relset_1(A,k5_numbers,k1_numbers) )
     => ! [B] : 
          ( ( v1_funct_1(B)
            & v1_funct_2(B,k5_numbers,k1_numbers)
            & v2_asympt_0(B)
            & m2_relset_1(B,k5_numbers,k1_numbers) )
         => ! [C] : 
              ( m2_subset_1(C,k1_numbers,k5_numbers)
             => ~ ( r2_hidden(B,k5_asympt_0(A))
                  & ! [D] : 
                      ( m2_subset_1(D,k1_numbers,k5_numbers)
                     => ~ ( r1_xreal_0(C,D)
                          & r1_xreal_0(k2_seq_1(k5_numbers,k1_numbers,A,D),0) ) )
                  & ! [D] : 
                      ( m1_subset_1(D,k1_numbers)
                     => ~ ( ~ r1_xreal_0(D,0)
                          & ! [E] : 
                              ( m2_subset_1(E,k1_numbers,k5_numbers)
                             => ( r1_xreal_0(C,E)
                               => r1_xreal_0(k2_seq_1(k5_numbers,k1_numbers,B,E),k4_real_1(D,k2_seq_1(k5_numbers,k1_numbers,A,E))) ) ) ) ) ) ) ) ) ),
    inference(mizar_proof,[status(thm)],[t46_square_1,t46_square_1,s1_asympt_0,s1_asympt_0,d1_sfmastr3,d1_xreal_0,t46_square_1,t46_square_1,t2_xreal_1,t66_xreal_1,t2_xreal_1,t2_xreal_1,d1_pre_circ,d1_pre_circ,t70_xreal_1,t88_xcmplx_1,d1_sfmastr3,t66_xreal_1,t70_xreal_1,t88_xcmplx_1,t2_xreal_1,t88_xcmplx_1,t66_xreal_1,t88_xcmplx_1,t66_xreal_1,t2_xreal_1,t66_xreal_1,t2_xreal_1]),
    [file(asympt_0,t8_asympt_0),interesting(0.00)]).

fof(t9_asympt_0,theorem,(
    ! [A] : 
      ( ( v1_funct_1(A)
        & v1_funct_2(A,k5_numbers,k1_numbers)
        & v2_asympt_0(A)
        & m2_relset_1(A,k5_numbers,k1_numbers) )
     => ! [B] : 
          ( ( v1_funct_1(B)
            & v1_funct_2(B,k5_numbers,k1_numbers)
            & v2_asympt_0(B)
            & m2_relset_1(B,k5_numbers,k1_numbers) )
         => k5_asympt_0(k1_asympt_0(A,B)) = k5_asympt_0(k4_asympt_0(A,B)) ) ) ),
    inference(mizar_proof,[status(thm)],[t70_xreal_1,t11_seq_1,d10_asympt_0,t46_square_1,t9_xreal_1,t66_xreal_1,t2_xreal_1,d4_asympt_0,d4_asympt_0,t46_square_1,t2_xreal_1,t46_square_1,t2_xreal_1,d10_asympt_0,t11_seq_1,t9_xreal_1,t49_square_1,t66_xreal_1,t2_xreal_1,t2_tarski]),
    [file(asympt_0,t9_asympt_0),interesting(0.00)]).