fof(t66_finseq_5,theorem,(
    ! [A] : 
      ( ( v1_relat_1(A)
        & v1_funct_1(A)
        & v1_finseq_1(A) )
     => ! [B] : k3_finseq_5(k7_finseq_1(A,k9_finseq_1(B))) = k7_finseq_1(k9_finseq_1(B),k3_finseq_5(A)) ) ),
    inference(mizar_proof,[status(thm)],[t19_finseq_2,t35_finseq_1,t56_finseq_1,d3_finseq_5,d3_finseq_5,t3_finseq_1,t57_finseq_1,d3_finseq_1,d3_finseq_1,t4_finseq_1,d1_tarski,d3_finseq_5,t59_finseq_1,t57_finseq_1,d7_finseq_1,t60_nat_1,t1_finseq_5,t2_xreal_1,t22_nat_1,t39_nat_1,t11_xreal_1,t27_finseq_3,t11_xreal_1,t8_xreal_1,t10_xreal_1,t11_xreal_1,t8_xreal_1,t38_nat_1,t27_finseq_3,d3_finseq_5,d7_finseq_1,t61_finseq_5,t37_finseq_1,d5_real_1,t10_finseq_2]),
    [file(finseq_5,t66_finseq_5),interesting(1.00)]).

fof(t67_finseq_5,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) )
         => k3_finseq_5(k7_finseq_1(A,B)) = k7_finseq_1(k3_finseq_5(B),k3_finseq_5(A)) ) ) ),
    inference(mizar_proof,[status(thm)],[t47_finseq_1,t47_finseq_1,t45_finseq_1,t66_finseq_5,t45_finseq_1,t66_finseq_5,s3_finseq_1]),
    [file(finseq_5,t67_finseq_5),interesting(0.98)]).

fof(t59_finseq_5,theorem,(
    ! [A] : 
      ( ~ v1_xboole_0(A)
     => ! [B] : 
          ( m1_subset_1(B,A)
         => ! [C] : 
              ( m2_finseq_1(C,A)
             => ( ( r2_hidden(B,k2_relat_1(C))
                  & v2_funct_1(C) )
               => v2_funct_1(k2_finseq_5(A,C,B)) ) ) ) ) ),
    inference(mizar_proof,[status(thm)],[t52_finseq_5,l39_finseq_5]),
    [file(finseq_5,t59_finseq_5),interesting(0.89)]).

fof(t26_finseq_5,theorem,(
    ! [A,B] : 
      ( m2_finseq_1(B,A)
     => ! [C] : 
          ( m2_finseq_1(C,A)
         => k16_finseq_1(A,k8_finseq_1(A,B,C),k3_finseq_1(B)) = B ) ) ),
    inference(mizar_proof,[status(thm)],[d15_finseq_1,t23_finseq_2,t25_finseq_5]),
    [file(finseq_5,t26_finseq_5),interesting(0.86)]).

fof(t31_finseq_5,theorem,(
    ! [A] : 
      ( ~ v1_xboole_0(A)
     => ! [B] : 
          ( m2_finseq_1(B,A)
         => k1_rfinseq(A,B,0) = B ) ) ),
    inference(mizar_proof,[status(thm)],[t18_nat_1,d2_rfinseq,t27_finseq_3,d2_rfinseq,t18_finseq_1]),
    [file(finseq_5,t31_finseq_5),interesting(0.86)]).

fof(t40_finseq_5,theorem,(
    ! [A] : 
      ( ~ v1_xboole_0(A)
     => ! [B] : 
          ( m2_finseq_1(B,A)
         => ! [C] : 
              ( m2_finseq_1(C,A)
             => k1_rfinseq(A,k8_finseq_1(A,B,C),k3_finseq_1(B)) = C ) ) ) ),
    inference(mizar_proof,[status(thm)],[t39_finseq_5,t31_finseq_5]),
    [file(finseq_5,t40_finseq_5),interesting(0.85)]).

fof(t79_finseq_5,theorem,(
    ! [A] : 
      ( m2_subset_1(A,k1_numbers,k5_numbers)
     => ! [B] : 
          ( ~ v1_xboole_0(B)
         => ! [C] : 
              ( m1_subset_1(C,B)
             => ! [D] : 
                  ( m2_finseq_1(D,B)
                 => ( v2_funct_1(D)
                   => ( r2_hidden(C,k2_relat_1(D))
                      | v2_funct_1(k5_finseq_5(B,D,C,A)) ) ) ) ) ) ) ),
    inference(mizar_proof,[status(thm)],[l26_finseq_5,t102_finseq_3,t55_finseq_1,d1_tarski,t21_finseq_5,t3_xboole_0,t98_finseq_3,l39_finseq_5,t37_finseq_5,t3_xboole_0,t36_finseq_5,d1_tarski,t55_finseq_1,d2_xboole_0,t44_finseq_1,t3_xboole_0,t98_finseq_3]),
    [file(finseq_5,t79_finseq_5),interesting(0.85)]).

fof(l39_finseq_5,theorem,(
    ! [A] : 
      ( m2_subset_1(A,k1_numbers,k5_numbers)
     => ! [B] : 
          ( ~ v1_xboole_0(B)
         => ! [C] : 
              ( m2_finseq_1(C,B)
             => ( v2_funct_1(C)
               => v2_funct_1(k1_rfinseq(B,C,A)) ) ) ) ) ),
    inference(mizar_proof,[status(thm)],[t29_finseq_5,t30_finseq_5,t30_finseq_5,t17_partfun2,t16_partfun2]),
    [file(finseq_5,l39_finseq_5),interesting(0.81)]).

fof(t64_finseq_5,theorem,(
    ! [A,B] : k3_finseq_5(k10_finseq_1(A,B)) = k10_finseq_1(B,A) ),
    inference(mizar_proof,[status(thm)],[t61_finseq_1,d3_finseq_1,t61_finseq_1,t61_finseq_1,t61_finseq_1,t61_finseq_1,t4_finseq_1,d2_tarski,d3_finseq_5]),
    [file(finseq_5,t64_finseq_5),interesting(0.80)]).

fof(t58_finseq_5,theorem,(
    ! [A] : 
      ( ~ v1_xboole_0(A)
     => ! [B] : 
          ( m1_subset_1(B,A)
         => ! [C] : 
              ( m2_finseq_1(C,A)
             => ( r2_hidden(B,k2_relat_1(C))
               => r1_tarski(k2_relat_1(k2_finseq_5(A,C,B)),k2_relat_1(C)) ) ) ) ) ),
    inference(mizar_proof,[status(thm)],[t52_finseq_5,t36_finseq_5]),
    [file(finseq_5,t58_finseq_5),interesting(0.79)]).

fof(t63_finseq_5,theorem,(
    ! [A] : k3_finseq_5(k9_finseq_1(A)) = k9_finseq_1(A) ),
    inference(mizar_proof,[status(thm)],[t56_finseq_1,d3_finseq_1,t4_finseq_1,d1_tarski,t56_finseq_1,d3_finseq_5]),
    [file(finseq_5,t63_finseq_5),interesting(0.78)]).

fof(l26_finseq_5,theorem,(
    ! [A] : 
      ( m2_subset_1(A,k1_numbers,k5_numbers)
     => ! [B] : 
          ( ~ v1_xboole_0(B)
         => ! [C] : 
              ( m2_finseq_1(C,B)
             => ( v2_funct_1(C)
               => v2_funct_1(k16_finseq_1(B,C,A)) ) ) ) ) ),
    inference(mizar_proof,[status(thm)],[t20_finseq_5,t85_finseq_4,t85_finseq_4,t17_partfun2,t16_partfun2]),
    [file(finseq_5,l26_finseq_5),interesting(0.77)]).

fof(t20_finseq_5,theorem,(
    ! [A] : 
      ( m2_subset_1(A,k1_numbers,k5_numbers)
     => ! [B,C] : 
          ( m2_finseq_1(C,B)
         => r1_tarski(k4_finseq_1(k16_finseq_1(B,C,A)),k4_finseq_1(C)) ) ) ),
    inference(mizar_proof,[status(thm)],[d3_tarski,t18_finseq_5,t27_finseq_3,t2_xreal_1,t27_finseq_3,t27_finseq_3]),
    [file(finseq_5,t20_finseq_5),interesting(0.72)]).

fof(t18_finseq_5,theorem,(
    ! [A] : 
      ( m2_subset_1(A,k1_numbers,k5_numbers)
     => ! [B,C] : 
          ( m2_finseq_1(C,B)
         => r1_xreal_0(k3_finseq_1(k16_finseq_1(B,C,A)),k3_finseq_1(C)) ) ) ),
    inference(mizar_proof,[status(thm)],[t80_finseq_1,t79_finseq_1]),
    [file(finseq_5,t18_finseq_5),interesting(0.70)]).

fof(t36_finseq_5,theorem,(
    ! [A] : 
      ( m2_subset_1(A,k1_numbers,k5_numbers)
     => ! [B] : 
          ( ~ v1_xboole_0(B)
         => ! [C] : 
              ( m2_finseq_1(C,B)
             => r1_tarski(k2_relat_1(k1_rfinseq(B,C,A)),k2_relat_1(C)) ) ) ) ),
    inference(mizar_proof,[status(thm)],[d3_tarski,t4_partfun2,t29_finseq_5,t4_partfun2,t30_finseq_5]),
    [file(finseq_5,t36_finseq_5),interesting(0.70)]).

fof(t39_finseq_5,theorem,(
    ! [A] : 
      ( m2_subset_1(A,k1_numbers,k5_numbers)
     => ! [B] : 
          ( ~ v1_xboole_0(B)
         => ! [C] : 
              ( m2_finseq_1(C,B)
             => ! [D] : 
                  ( m2_finseq_1(D,B)
                 => k1_rfinseq(B,k8_finseq_1(B,C,D),k1_nat_1(k3_finseq_1(C),A)) = k1_rfinseq(B,D,A) ) ) ) ) ),
    inference(mizar_proof,[status(thm)],[t35_finseq_1,t8_xreal_1,d2_rfinseq,d2_rfinseq,t27_finseq_3,t29_finseq_5,t27_finseq_3,t30_finseq_5,t84_finseq_4,t30_finseq_5,t14_finseq_5,t8_xreal_1,d2_rfinseq,d2_rfinseq]),
    [file(finseq_5,t39_finseq_5),interesting(0.69)]).

fof(t57_finseq_5,theorem,(
    ! [A] : 
      ( ~ v1_xboole_0(A)
     => ! [B] : 
          ( m1_subset_1(B,A)
         => ! [C] : 
              ( m2_finseq_1(C,A)
             => ( r2_hidden(B,k2_relat_1(C))
               => k4_finseq_4(k5_numbers,A,k2_finseq_5(A,C,B),k3_finseq_1(k2_finseq_5(A,C,B))) = k4_finseq_4(k5_numbers,A,C,k3_finseq_1(C)) ) ) ) ) ),
    inference(mizar_proof,[status(thm)],[t31_finseq_4,t18_int_1,t53_finseq_5,t6_finseq_5,t55_finseq_5]),
    [file(finseq_5,t57_finseq_5),interesting(0.69)]).

fof(t25_finseq_5,theorem,(
    ! [A] : 
      ( m2_subset_1(A,k1_numbers,k5_numbers)
     => ! [B,C] : 
          ( m2_finseq_1(C,B)
         => ! [D] : 
              ( m2_finseq_1(D,B)
             => ( r1_xreal_0(A,k3_finseq_1(C))
               => k16_finseq_1(B,k8_finseq_1(B,C,D),A) = k16_finseq_1(B,C,A) ) ) ) ) ),
    inference(mizar_proof,[status(thm)],[t80_finseq_1,t37_nat_1,t35_finseq_1,t80_finseq_1,t3_finseq_1,t2_xreal_1,t3_finseq_1,t3_finseq_1,d3_finseq_1,d15_finseq_1,t72_funct_1,d7_finseq_1,t72_funct_1,d15_finseq_1,t10_finseq_2]),
    [file(finseq_5,t25_finseq_5),interesting(0.68)]).

fof(t23_finseq_5,theorem,(
    ! [A,B] : 
      ( m2_finseq_1(B,A)
     => ( ~ v1_xboole_0(B)
       => k16_finseq_1(A,B,1) = k9_finseq_1(k4_finseq_4(k5_numbers,A,B,1)) ) ) ),
    inference(mizar_proof,[status(thm)],[t6_finseq_5,t27_finseq_3,t80_finseq_1,t27_finseq_3,d4_finseq_4,t85_finseq_4,t57_finseq_1]),
    [file(finseq_5,t23_finseq_5),interesting(0.68)]).

fof(t21_finseq_5,theorem,(
    ! [A] : 
      ( m2_subset_1(A,k1_numbers,k5_numbers)
     => ! [B] : 
          ( ~ v1_xboole_0(B)
         => ! [C] : 
              ( m2_finseq_1(C,B)
             => r1_tarski(k2_relat_1(k16_finseq_1(B,C,A)),k2_relat_1(C)) ) ) ) ),
    inference(mizar_proof,[status(thm)],[d3_tarski,t4_partfun2,t20_finseq_5,t4_partfun2,t85_finseq_4]),
    [file(finseq_5,t21_finseq_5),interesting(0.68)]).

fof(t60_finseq_5,theorem,(
    ! [A] : 
      ( ( v1_relat_1(A)
        & v1_funct_1(A)
        & v1_finseq_1(A) )
     => ( k4_finseq_1(A) = k4_finseq_1(k3_finseq_5(A))
        & k2_relat_1(A) = k2_relat_1(k3_finseq_5(A)) ) ) ),
    inference(mizar_proof,[status(thm)],[d3_finseq_1,d3_finseq_5,d3_finseq_1,d3_finseq_5,t11_finseq_2,t27_finseq_3,t1_finseq_5,d3_finseq_1,t2_finseq_5,d3_finseq_1,d3_finseq_5,d5_funct_1,d3_tarski,d10_xboole_0,d3_tarski,t11_finseq_2,d3_finseq_5,t27_finseq_3,t1_finseq_5,d3_finseq_1,t2_finseq_5,d3_finseq_1,d5_funct_1]),
    [file(finseq_5,t60_finseq_5),interesting(0.68)]).

fof(t37_finseq_5,theorem,(
    ! [A] : 
      ( m2_subset_1(A,k1_numbers,k5_numbers)
     => ! [B] : 
          ( ~ v1_xboole_0(B)
         => ! [C] : 
              ( m2_finseq_1(C,B)
             => ( v2_funct_1(C)
               => r1_xboole_0(k2_relat_1(k16_finseq_1(B,C,A)),k2_relat_1(k1_rfinseq(B,C,A))) ) ) ) ) ),
    inference(mizar_proof,[status(thm)],[t3_xboole_0,t4_partfun2,t4_partfun2,t20_finseq_5,t29_finseq_5,t30_finseq_5,t85_finseq_4,t27_finseq_3,t19_finseq_5,t2_xreal_1,t29_nat_1,t1_xreal_1,t27_finseq_3,t17_partfun2]),
    [file(finseq_5,t37_finseq_5),interesting(0.67)]).

fof(t51_finseq_5,theorem,(
    ! [A] : 
      ( ~ v1_xboole_0(A)
     => ! [B] : 
          ( m1_subset_1(B,A)
         => ! [C] : 
              ( m2_finseq_1(C,A)
             => r1_tarski(k2_relat_1(k1_finseq_5(A,C,B)),k2_relat_1(C)) ) ) ) ),
    inference(mizar_proof,[status(thm)],[t21_finseq_5]),
    [file(finseq_5,t51_finseq_5),interesting(0.66)]).

fof(t35_finseq_5,theorem,(
    ! [A] : 
      ( m2_subset_1(A,k1_numbers,k5_numbers)
     => ! [B,C] : 
          ( m2_finseq_1(C,B)
         => ( r1_xreal_0(k3_finseq_1(C),A)
           => v1_xboole_0(k1_rfinseq(B,C,A)) ) ) ) ),
    inference(mizar_proof,[status(thm)],[d2_rfinseq,t25_finseq_1,d5_real_1,d2_rfinseq]),
    [file(finseq_5,t35_finseq_5),interesting(0.66)]).

fof(t50_finseq_5,theorem,(
    ! [A] : 
      ( ~ v1_xboole_0(A)
     => ! [B] : 
          ( m1_subset_1(B,A)
         => ! [C] : 
              ( m2_finseq_1(C,A)
             => ~ ( r2_hidden(B,k2_relat_1(C))
                  & v1_xboole_0(k1_finseq_5(A,C,B)) ) ) ) ) ),
    inference(mizar_proof,[status(thm)],[t31_finseq_4,t45_finseq_5,t27_finseq_3,t60_relat_1]),
    [file(finseq_5,t50_finseq_5),interesting(0.65)]).

fof(t19_finseq_5,theorem,(
    ! [A] : 
      ( m2_subset_1(A,k1_numbers,k5_numbers)
     => ! [B,C] : 
          ( m2_finseq_1(C,B)
         => r1_xreal_0(k3_finseq_1(k16_finseq_1(B,C,A)),A) ) ) ),
    inference(mizar_proof,[status(thm)],[t80_finseq_1,t79_finseq_1]),
    [file(finseq_5,t19_finseq_5),interesting(0.65)]).

fof(t16_finseq_5,theorem,(
    ! [A] : 
      ( ~ v1_xboole_0(A)
     => ! [B] : 
          ( m1_subset_1(B,A)
         => ! [C] : 
              ( m2_finseq_1(C,A)
             => k4_finseq_4(k5_numbers,A,k8_finseq_1(A,k12_finseq_1(A,B),C),1) = B ) ) ) ),
    inference(mizar_proof,[status(thm)],[t8_finseq_5,t29_nat_1,t27_finseq_3,d4_finseq_4,t58_finseq_1]),
    [file(finseq_5,t16_finseq_5),interesting(0.64)]).

fof(t42_finseq_5,theorem,(
    ! [A] : 
      ( m2_subset_1(A,k1_numbers,k5_numbers)
     => ! [B] : 
          ( ~ v1_xboole_0(B)
         => ! [C] : 
              ( m2_finseq_1(C,B)
             => ( r2_hidden(A,k4_finseq_1(C))
               => r1_xreal_0(k5_finseq_4(C,k4_finseq_4(k5_numbers,B,C,A)),A) ) ) ) ) ),
    inference(mizar_proof,[status(thm)],[d5_finseq_4,t167_relat_1,d3_finseq_1,d4_finseq_4,d1_tarski,d13_funct_1,d13_finseq_1,d5_funct_1,t27_finseq_3,t46_finseq_3]),
    [file(finseq_5,t42_finseq_5),interesting(0.62)]).

fof(t41_finseq_5,theorem,(
    ! [A] : 
      ( ~ v1_xboole_0(A)
     => ! [B] : 
          ( m1_subset_1(B,A)
         => ! [C] : 
              ( m2_finseq_1(C,A)
             => ( r2_hidden(B,k2_relat_1(C))
               => k4_finseq_4(k5_numbers,A,C,k5_finseq_4(C,B)) = B ) ) ) ) ),
    inference(mizar_proof,[status(thm)],[t29_finseq_4,t30_finseq_4,d4_finseq_4]),
    [file(finseq_5,t41_finseq_5),interesting(0.59)]).

fof(t8_finseq_5,theorem,(
    ! [A,B] : 
      ( ( v1_relat_1(B)
        & v1_funct_1(B)
        & v1_finseq_1(B) )
     => k3_finseq_1(k7_finseq_1(k9_finseq_1(A),B)) = k1_nat_1(1,k3_finseq_1(B)) ) ),
    inference(mizar_proof,[status(thm)],[t35_finseq_1,t56_finseq_1]),
    [file(finseq_5,t8_finseq_5),interesting(0.59)]).

fof(t53_finseq_5,theorem,(
    ! [A] : 
      ( ~ v1_xboole_0(A)
     => ! [B] : 
          ( m1_subset_1(B,A)
         => ! [C] : 
              ( m2_finseq_1(C,A)
             => ( r2_hidden(B,k2_relat_1(C))
               => k3_finseq_1(k2_finseq_5(A,C,B)) = k2_xcmplx_0(k6_xcmplx_0(k3_finseq_1(C),k5_finseq_4(C,B)),1) ) ) ) ) ),
    inference(mizar_proof,[status(thm)],[t52_finseq_5,t31_finseq_4,t29_nat_1,t2_xreal_1,d2_rfinseq]),
    [file(finseq_5,t53_finseq_5),interesting(0.59)]).

fof(t2_finseq_5,theorem,(
    ! [A] : 
      ( m2_subset_1(A,k1_numbers,k5_numbers)
     => ! [B] : 
          ( m2_subset_1(B,k1_numbers,k5_numbers)
         => ( r2_hidden(A,k2_finseq_1(B))
           => r2_hidden(k2_xcmplx_0(k6_xcmplx_0(B,A),1),k2_finseq_1(B)) ) ) ) ),
    inference(mizar_proof,[status(thm)],[t3_finseq_1,t18_int_1,t18_nat_1,t8_xreal_1,t18_nat_1,t45_xreal_1,t8_xreal_1,t3_finseq_1,d5_real_1,t38_nat_1,t3_finseq_1]),
    [file(finseq_5,t2_finseq_5),interesting(0.59)]).

fof(t6_finseq_5,theorem,(
    ! [A] : 
      ( ( ~ v1_xboole_0(A)
        & v1_relat_1(A)
        & v1_funct_1(A)
        & v1_finseq_1(A) )
     => ( r2_hidden(1,k4_finseq_1(A))
        & r2_hidden(k3_finseq_1(A),k4_finseq_1(A)) ) ) ),
    inference(mizar_proof,[status(thm)],[t25_finseq_1,t39_nat_1,t27_finseq_3,t27_finseq_3]),
    [file(finseq_5,t6_finseq_5),interesting(0.58)]).

fof(t43_finseq_5,theorem,(
    ! [A] : 
      ( m2_subset_1(A,k1_numbers,k5_numbers)
     => ! [B] : 
          ( ~ v1_xboole_0(B)
         => ! [C] : 
              ( m1_subset_1(C,B)
             => ! [D] : 
                  ( m2_finseq_1(D,B)
                 => ( r2_hidden(C,k2_relat_1(k16_finseq_1(B,D,A)))
                   => k5_finseq_4(k16_finseq_1(B,D,A),C) = k5_finseq_4(D,C) ) ) ) ) ) ),
    inference(mizar_proof,[status(thm)],[t30_finseq_4,t20_finseq_5,t21_finseq_5,t85_finseq_4,t41_finseq_5,t42_finseq_5,t31_finseq_4,t31_finseq_4,t2_xreal_1,t27_finseq_3,t85_finseq_4,t41_finseq_5,t42_finseq_5,t1_xreal_1]),
    [file(finseq_5,t43_finseq_5),interesting(0.58)]).

fof(t45_finseq_5,theorem,(
    ! [A] : 
      ( ~ v1_xboole_0(A)
     => ! [B] : 
          ( m1_subset_1(B,A)
         => ! [C] : 
              ( m2_finseq_1(C,A)
             => ( r2_hidden(B,k2_relat_1(C))
               => k3_finseq_1(k1_finseq_5(A,C,B)) = k5_finseq_4(C,B) ) ) ) ) ),
    inference(mizar_proof,[status(thm)],[t30_finseq_4,t27_finseq_3,t80_finseq_1]),
    [file(finseq_5,t45_finseq_5),interesting(0.58)]).

fof(t70_finseq_5,theorem,(
    ! [A] : 
      ( ~ v1_xboole_0(A)
     => ! [B] : 
          ( m1_subset_1(B,A)
         => ! [C] : 
              ( m2_finseq_1(C,A)
             => k5_finseq_5(A,C,B,0) = k8_finseq_1(A,k12_finseq_1(A,B),C) ) ) ) ),
    inference(mizar_proof,[status(thm)],[t47_finseq_1,t31_finseq_5]),
    [file(finseq_5,t70_finseq_5),interesting(0.58)]).

fof(t56_finseq_5,theorem,(
    ! [A] : 
      ( ~ v1_xboole_0(A)
     => ! [B] : 
          ( m1_subset_1(B,A)
         => ! [C] : 
              ( m2_finseq_1(C,A)
             => k4_finseq_4(k5_numbers,A,k2_finseq_5(A,C,B),1) = B ) ) ) ),
    inference(mizar_proof,[status(thm)],[t16_finseq_5]),
    [file(finseq_5,t56_finseq_5),interesting(0.57)]).

fof(t1_finseq_5,theorem,(
    ! [A] : 
      ( m2_subset_1(A,k1_numbers,k5_numbers)
     => ! [B] : 
          ( m2_subset_1(B,k1_numbers,k5_numbers)
         => ( r1_xreal_0(A,B)
           => m2_subset_1(k2_xcmplx_0(k6_xcmplx_0(B,A),1),k1_numbers,k5_numbers) ) ) ) ),
    inference(mizar_proof,[status(thm)],[t18_int_1]),
    [file(finseq_5,t1_finseq_5),interesting(0.57)]).

fof(t3_finseq_5,theorem,(
    ! [A] : 
      ( ( v1_relat_1(A)
        & v1_funct_1(A) )
     => ! [B,C] : 
          ( k10_relat_1(A,k1_tarski(C)) = k1_tarski(B)
         => ( r2_hidden(B,k1_relat_1(A))
            & r2_hidden(C,k2_relat_1(A))
            & k1_funct_1(A,B) = C ) ) ) ),
    inference(mizar_proof,[status(thm)],[d1_tarski,d13_funct_1,d13_funct_1,d1_tarski,d5_funct_1]),
    [file(finseq_5,t3_finseq_5),interesting(0.55)]).

fof(t38_finseq_5,theorem,(
    ! [A] : 
      ( ~ v1_xboole_0(A)
     => ! [B] : 
          ( m1_subset_1(B,A)
         => ! [C] : 
              ( m2_finseq_1(C,A)
             => ( r2_hidden(B,k2_relat_1(C))
               => k7_finseq_4(C,B) = k1_rfinseq(A,C,k5_finseq_4(C,B)) ) ) ) ) ),
    inference(mizar_proof,[status(thm)],[d7_finseq_4,t31_finseq_4,d2_rfinseq,d3_finseq_1,d7_finseq_4,d2_rfinseq,t10_finseq_2]),
    [file(finseq_5,t38_finseq_5),interesting(0.54)]).

fof(t81_finseq_5,theorem,(
    ! [A] : 
      ( m2_subset_1(A,k1_numbers,k5_numbers)
     => ! [B] : 
          ( ~ v1_xboole_0(B)
         => k16_finseq_1(B,k6_finseq_1(B),A) = k6_finseq_1(B) ) ) ),
    inference(mizar_proof,[status(thm)],[t32_finseq_1,t18_nat_1,t79_finseq_1]),
    [file(finseq_5,t81_finseq_5),interesting(0.52)]).

fof(t28_finseq_5,theorem,(
    ! [A] : 
      ( m2_subset_1(A,k1_numbers,k5_numbers)
     => ! [B] : 
          ( ~ v1_xboole_0(B)
         => ! [C] : 
              ( m2_finseq_1(C,B)
             => r1_xreal_0(k3_finseq_1(k1_rfinseq(B,C,A)),k3_finseq_1(C)) ) ) ) ),
    inference(mizar_proof,[status(thm)],[d2_rfinseq,t29_nat_1,d2_rfinseq,t32_finseq_1,t18_nat_1]),
    [file(finseq_5,t28_finseq_5),interesting(0.49)]).

fof(t15_finseq_5,theorem,(
    ! [A] : 
      ( ~ v1_xboole_0(A)
     => ! [B] : 
          ( m2_finseq_1(B,A)
         => ( k3_finseq_1(B) = 1
           => B = k12_finseq_1(A,k4_finseq_4(k5_numbers,A,B,1)) ) ) ) ),
    inference(mizar_proof,[status(thm)],[t25_finseq_1,t6_finseq_5,d4_finseq_4,t57_finseq_1]),
    [file(finseq_5,t15_finseq_5),interesting(0.49)]).

fof(t29_finseq_5,theorem,(
    ! [A] : 
      ( m2_subset_1(A,k1_numbers,k5_numbers)
     => ! [B] : 
          ( m2_subset_1(B,k1_numbers,k5_numbers)
         => ! [C] : 
              ( ~ v1_xboole_0(C)
             => ! [D] : 
                  ( m2_finseq_1(D,C)
                 => ( r2_hidden(A,k4_finseq_1(k1_rfinseq(C,D,B)))
                   => r2_hidden(k1_nat_1(B,A),k4_finseq_1(D)) ) ) ) ) ) ),
    inference(mizar_proof,[status(thm)],[t27_finseq_3,t29_nat_1,t2_xreal_1,t27_finseq_3,d2_rfinseq,t21_xreal_1,t27_finseq_3,d2_rfinseq,t26_finseq_1]),
    [file(finseq_5,t29_finseq_5),interesting(0.49)]).

fof(t49_finseq_5,theorem,(
    ! [A] : 
      ( ~ v1_xboole_0(A)
     => ! [B] : 
          ( m1_subset_1(B,A)
         => ! [C] : 
              ( m2_finseq_1(C,A)
             => ! [D] : 
                  ( ( r2_hidden(D,k2_relat_1(C))
                    & r2_hidden(B,k2_relat_1(C))
                    & r1_xreal_0(k5_finseq_4(C,D),k5_finseq_4(C,B)) )
                 => r2_hidden(D,k2_relat_1(k1_finseq_5(A,C,B))) ) ) ) ) ),
    inference(mizar_proof,[status(thm)],[t30_finseq_4,t31_finseq_4,t3_finseq_1,d3_finseq_1,t45_finseq_5,d5_funct_1,d4_finseq_4,t46_finseq_5,d4_finseq_4,t29_finseq_4]),
    [file(finseq_5,t49_finseq_5),interesting(0.49)]).

fof(l17_finseq_5,theorem,(
    ! [A] : 
      ( m2_subset_1(A,k1_numbers,k5_numbers)
     => ! [B] : 
          ( ~ v1_xboole_0(B)
         => ! [C] : 
              ( m2_finseq_1(C,B)
             => ! [D] : 
                  ( m2_finseq_1(D,B)
                 => ( r2_hidden(A,k4_finseq_1(C))
                   => k4_finseq_4(k5_numbers,B,k8_finseq_1(B,C,D),A) = k4_finseq_4(k5_numbers,B,C,A) ) ) ) ) ) ),
    inference(mizar_proof,[status(thm)],[t39_finseq_1,d4_finseq_4,d7_finseq_1,d4_finseq_4]),
    [file(finseq_5,l17_finseq_5),interesting(0.49)]).

fof(t54_finseq_5,theorem,(
    ! [A] : 
      ( m2_subset_1(A,k1_numbers,k5_numbers)
     => ! [B] : 
          ( ~ v1_xboole_0(B)
         => ! [C] : 
              ( m1_subset_1(C,B)
             => ! [D] : 
                  ( m2_finseq_1(D,B)
                 => ( ( r2_hidden(C,k2_relat_1(D))
                      & r2_hidden(k1_nat_1(A,1),k4_finseq_1(k2_finseq_5(B,D,C))) )
                   => r2_hidden(k1_nat_1(A,k5_finseq_4(D,C)),k4_finseq_1(D)) ) ) ) ) ) ),
    inference(mizar_proof,[status(thm)],[t27_finseq_3,t53_finseq_5,t8_xreal_1,t21_xreal_1,t31_finseq_4,t29_nat_1,t2_xreal_1,t27_finseq_3]),
    [file(finseq_5,t54_finseq_5),interesting(0.48)]).

fof(t27_finseq_5,theorem,(
    ! [A] : 
      ( ~ v1_xboole_0(A)
     => ! [B] : 
          ( m1_subset_1(B,A)
         => ! [C,D] : 
              ( m2_finseq_1(D,C)
             => ( r2_hidden(B,k2_relat_1(D))
               => k7_finseq_1(k6_finseq_4(D,B),k12_finseq_1(A,B)) = k16_finseq_1(C,D,k5_finseq_4(D,B)) ) ) ) ) ),
    inference(mizar_proof,[status(thm)],[d6_finseq_4,t29_finseq_4,t30_finseq_4,t11_finseq_5,d15_finseq_1]),
    [file(finseq_5,t27_finseq_5),interesting(0.46)]).

fof(t74_finseq_5,theorem,(
    ! [A] : 
      ( m2_subset_1(A,k1_numbers,k5_numbers)
     => ! [B] : 
          ( ~ v1_xboole_0(B)
         => ! [C] : 
              ( m1_subset_1(C,B)
             => ! [D] : 
                  ( m2_finseq_1(D,B)
                 => r2_hidden(C,k2_relat_1(k5_finseq_5(B,D,C,A))) ) ) ) ) ),
    inference(mizar_proof,[status(thm)],[d1_tarski,d2_xboole_0,t73_finseq_5]),
    [file(finseq_5,t74_finseq_5),interesting(0.46)]).

fof(t12_finseq_5,theorem,(
    ! [A] : 
      ( m2_subset_1(A,k1_numbers,k5_numbers)
     => ! [B] : 
          ( ( v1_relat_1(B)
            & v1_funct_1(B)
            & v2_funct_1(B)
            & v1_finseq_1(B) )
         => ( r2_hidden(A,k4_finseq_1(B))
           => k5_finseq_4(B,k1_funct_1(B,A)) = A ) ) ) ),
    inference(mizar_proof,[status(thm)],[d5_funct_1,t10_finseq_4,t35_finseq_4,d3_finseq_4]),
    [file(finseq_5,t12_finseq_5),interesting(0.45)]).

fof(t10_finseq_5,theorem,(
    ! [A] : 
      ( ( v1_relat_1(A)
        & v1_funct_1(A)
        & v1_finseq_1(A) )
     => ! [B,C] : 
          ( ( r2_hidden(B,k2_relat_1(A))
            & r2_hidden(C,k2_relat_1(A))
            & k5_finseq_4(A,B) = k5_finseq_4(A,C) )
         => B = C ) ) ),
    inference(mizar_proof,[status(thm)],[t29_finseq_4,t29_finseq_4]),
    [file(finseq_5,t10_finseq_5),interesting(0.44)]).

fof(t32_finseq_5,theorem,(
    ! [A] : 
      ( ~ v1_xboole_0(A)
     => ! [B] : 
          ( m2_finseq_1(B,A)
         => ( ~ v1_xboole_0(B)
           => B = k8_finseq_1(A,k12_finseq_1(A,k4_finseq_4(k5_numbers,A,B,1)),k1_rfinseq(A,B,1)) ) ) ) ),
    inference(mizar_proof,[status(thm)],[t23_finseq_5,t21_rfinseq]),
    [file(finseq_5,t32_finseq_5),interesting(0.44)]).

fof(t52_finseq_5,theorem,(
    ! [A] : 
      ( ~ v1_xboole_0(A)
     => ! [B] : 
          ( m1_subset_1(B,A)
         => ! [C] : 
              ( m2_finseq_1(C,A)
             => ~ ( r2_hidden(B,k2_relat_1(C))
                  & ! [D] : 
                      ( m2_subset_1(D,k1_numbers,k5_numbers)
                     => ~ ( k1_nat_1(D,1) = k5_finseq_4(C,B)
                          & k2_finseq_5(A,C,B) = k1_rfinseq(A,C,D) ) ) ) ) ) ) ),
    inference(mizar_proof,[status(thm)],[t31_finseq_4,t18_int_1,t30_finseq_4,t41_finseq_5,t34_finseq_5]),
    [file(finseq_5,t52_finseq_5),interesting(0.44)]).

fof(t71_finseq_5,theorem,(
    ! [A] : 
      ( m2_subset_1(A,k1_numbers,k5_numbers)
     => ! [B] : 
          ( ~ v1_xboole_0(B)
         => ! [C] : 
              ( m1_subset_1(C,B)
             => ! [D] : 
                  ( m2_finseq_1(D,B)
                 => ( r1_xreal_0(k3_finseq_1(D),A)
                   => k5_finseq_5(B,D,C,A) = k8_finseq_1(B,D,k12_finseq_1(B,C)) ) ) ) ) ) ),
    inference(mizar_proof,[status(thm)],[t35_finseq_5,t47_finseq_1,t79_finseq_1]),
    [file(finseq_5,t71_finseq_5),interesting(0.44)]).

fof(t5_finseq_5,theorem,(
    ! [A] : 
      ( ( v1_relat_1(A)
        & v1_funct_1(A) )
     => ! [B,C] : 
          ( ( v2_funct_1(A)
            & r2_hidden(B,k2_relat_1(A))
            & r2_hidden(C,k2_relat_1(A))
            & k10_relat_1(A,k1_tarski(B)) = k10_relat_1(A,k1_tarski(C)) )
         => B = C ) ) ),
    inference(mizar_proof,[status(thm)],[t144_funct_1,t144_funct_1,t3_finseq_5,t6_zfmisc_1]),
    [file(finseq_5,t5_finseq_5),interesting(0.43)]).

fof(t73_finseq_5,theorem,(
    ! [A] : 
      ( m2_subset_1(A,k1_numbers,k5_numbers)
     => ! [B] : 
          ( ~ v1_xboole_0(B)
         => ! [C] : 
              ( m1_subset_1(C,B)
             => ! [D] : 
                  ( m2_finseq_1(D,B)
                 => k2_relat_1(k5_finseq_5(B,D,C,A)) = k2_xboole_0(k1_tarski(C),k2_relat_1(D)) ) ) ) ) ),
    inference(mizar_proof,[status(thm)],[t44_finseq_1,t44_finseq_1,t4_xboole_1,t44_finseq_1,t21_rfinseq,t55_finseq_1]),
    [file(finseq_5,t73_finseq_5),interesting(0.43)]).

fof(t48_finseq_5,theorem,(
    ! [A] : 
      ( ~ v1_xboole_0(A)
     => ! [B] : 
          ( m1_subset_1(B,A)
         => ! [C] : 
              ( m2_finseq_1(C,A)
             => ( r2_hidden(B,k2_relat_1(C))
               => k4_finseq_4(k5_numbers,A,k1_finseq_5(A,C,B),k5_finseq_4(C,B)) = B ) ) ) ) ),
    inference(mizar_proof,[status(thm)],[t31_finseq_4,t3_finseq_1,t30_finseq_4,t46_finseq_5,d4_finseq_4,t29_finseq_4]),
    [file(finseq_5,t48_finseq_5),interesting(0.42)]).

fof(t62_finseq_5,theorem,(
    ! [A] : 
      ( ( v1_relat_1(A)
        & v1_funct_1(A)
        & v1_finseq_1(A) )
     => ! [B] : 
          ( m2_subset_1(B,k1_numbers,k5_numbers)
         => ! [C] : 
              ( m2_subset_1(C,k1_numbers,k5_numbers)
             => ( ( r2_hidden(B,k4_finseq_1(A))
                  & k1_nat_1(B,C) = k1_nat_1(k3_finseq_1(A),1) )
               => r2_hidden(C,k4_finseq_1(k3_finseq_5(A))) ) ) ) ) ),
    inference(mizar_proof,[status(thm)],[d3_finseq_1,t60_finseq_5,t2_finseq_5]),
    [file(finseq_5,t62_finseq_5),interesting(0.41)]).

fof(t4_finseq_5,theorem,(
    ! [A] : 
      ( ( v1_relat_1(A)
        & v1_funct_1(A) )
     => ( v2_funct_1(A)
      <=> ! [B] : 
            ( r2_hidden(B,k1_relat_1(A))
           => k10_relat_1(A,k1_tarski(k1_funct_1(A,B))) = k1_tarski(B) ) ) ) ),
    inference(mizar_proof,[status(thm)],[t3_finseq_4,t3_finseq_4,t5_finseq_4]),
    [file(finseq_5,t4_finseq_5),interesting(0.38)]).

fof(t72_finseq_5,theorem,(
    ! [A] : 
      ( m2_subset_1(A,k1_numbers,k5_numbers)
     => ! [B] : 
          ( ~ v1_xboole_0(B)
         => ! [C] : 
              ( m1_subset_1(C,B)
             => ! [D] : 
                  ( m2_finseq_1(D,B)
                 => k3_finseq_1(k5_finseq_5(B,D,C,A)) = k1_nat_1(k3_finseq_1(D),1) ) ) ) ) ),
    inference(mizar_proof,[status(thm)],[t35_finseq_1,d2_rfinseq,t35_finseq_1,t56_finseq_1,t80_finseq_1,t71_finseq_5,t19_finseq_2]),
    [file(finseq_5,t72_finseq_5),interesting(0.37)]).

fof(t47_finseq_5,theorem,(
    ! [A] : 
      ( ~ v1_xboole_0(A)
     => ! [B] : 
          ( m1_subset_1(B,A)
         => ! [C] : 
              ( m2_finseq_1(C,A)
             => ( r2_hidden(B,k2_relat_1(C))
               => k4_finseq_4(k5_numbers,A,k1_finseq_5(A,C,B),1) = k4_finseq_4(k5_numbers,A,C,1) ) ) ) ) ),
    inference(mizar_proof,[status(thm)],[t31_finseq_4,t3_finseq_1,t46_finseq_5]),
    [file(finseq_5,t47_finseq_5),interesting(0.32)]).

fof(t44_finseq_5,theorem,(
    ! [A] : 
      ( m2_subset_1(A,k1_numbers,k5_numbers)
     => ! [B] : 
          ( ~ v1_xboole_0(B)
         => ! [C] : 
              ( m2_finseq_1(C,B)
             => ( ( r2_hidden(A,k4_finseq_1(C))
                  & v2_funct_1(C) )
               => k5_finseq_4(C,k4_finseq_4(k5_numbers,B,C,A)) = A ) ) ) ) ),
    inference(mizar_proof,[status(thm)],[t12_finseq_5,d4_finseq_4]),
    [file(finseq_5,t44_finseq_5),interesting(0.31)]).

fof(t55_finseq_5,theorem,(
    ! [A] : 
      ( m2_subset_1(A,k1_numbers,k5_numbers)
     => ! [B] : 
          ( ~ v1_xboole_0(B)
         => ! [C] : 
              ( m1_subset_1(C,B)
             => ! [D] : 
                  ( m2_finseq_1(D,B)
                 => ( ( r2_hidden(C,k2_relat_1(D))
                      & r2_hidden(k1_nat_1(A,1),k4_finseq_1(k2_finseq_5(B,D,C))) )
                   => k4_finseq_4(k5_numbers,B,k2_finseq_5(B,D,C),k1_nat_1(A,1)) = k4_finseq_4(k5_numbers,B,D,k1_nat_1(A,k5_finseq_4(D,C))) ) ) ) ) ) ),
    inference(mizar_proof,[status(thm)],[t52_finseq_5,t31_finseq_4,t29_nat_1,t2_xreal_1,t54_finseq_5,d4_finseq_4,d2_rfinseq,d4_finseq_4]),
    [file(finseq_5,t55_finseq_5),interesting(0.31)]).

fof(t61_finseq_5,theorem,(
    ! [A] : 
      ( m2_subset_1(A,k1_numbers,k5_numbers)
     => ! [B] : 
          ( ( v1_relat_1(B)
            & v1_funct_1(B)
            & v1_finseq_1(B) )
         => ( r2_hidden(A,k4_finseq_1(B))
           => k1_funct_1(k3_finseq_5(B),A) = k1_funct_1(B,k2_xcmplx_0(k6_xcmplx_0(k3_finseq_1(B),A),1)) ) ) ) ),
    inference(mizar_proof,[status(thm)],[t60_finseq_5,d3_finseq_5]),
    [file(finseq_5,t61_finseq_5),interesting(0.30)]).

fof(t46_finseq_5,theorem,(
    ! [A] : 
      ( m2_subset_1(A,k1_numbers,k5_numbers)
     => ! [B] : 
          ( ~ v1_xboole_0(B)
         => ! [C] : 
              ( m1_subset_1(C,B)
             => ! [D] : 
                  ( m2_finseq_1(D,B)
                 => ( ( r2_hidden(C,k2_relat_1(D))
                      & r2_hidden(A,k2_finseq_1(k5_finseq_4(D,C))) )
                   => k4_finseq_4(k5_numbers,B,k1_finseq_5(B,D,C),A) = k4_finseq_4(k5_numbers,B,D,A) ) ) ) ) ) ),
    inference(mizar_proof,[status(thm)],[t30_finseq_4,t86_finseq_4]),
    [file(finseq_5,t46_finseq_5),interesting(0.26)]).

fof(t34_finseq_5,theorem,(
    ! [A] : 
      ( m2_subset_1(A,k1_numbers,k5_numbers)
     => ! [B] : 
          ( m2_subset_1(B,k1_numbers,k5_numbers)
         => ! [C] : 
              ( ~ v1_xboole_0(C)
             => ! [D] : 
                  ( m2_finseq_1(D,C)
                 => ( ( k1_nat_1(A,1) = B
                      & r2_hidden(B,k4_finseq_1(D)) )
                   => k8_finseq_1(C,k12_finseq_1(C,k4_finseq_4(k5_numbers,C,D,B)),k1_rfinseq(C,D,B)) = k1_rfinseq(C,D,A) ) ) ) ) ) ),
    inference(mizar_proof,[status(thm)],[t27_finseq_3,t29_nat_1,t2_xreal_1,t8_finseq_5,d2_rfinseq,d2_rfinseq,t27_finseq_3,t58_finseq_1,d4_finseq_4,d2_rfinseq,d5_real_1,t18_int_1,t38_nat_1,t11_xreal_1,t27_finseq_3,t56_finseq_1,t37_finseq_1,d2_rfinseq,d2_rfinseq,t18_finseq_1]),
    [file(finseq_5,t34_finseq_5),interesting(0.26)]).

fof(t7_finseq_5,theorem,(
    ! [A] : 
      ( ( ~ v1_xboole_0(A)
        & v1_relat_1(A)
        & v1_funct_1(A)
        & v1_finseq_1(A) )
     => ? [B] : 
          ( m2_subset_1(B,k1_numbers,k5_numbers)
          & k1_nat_1(B,1) = k3_finseq_1(A) ) ) ),
    inference(mizar_proof,[status(thm)],[t25_finseq_1,t22_nat_1]),
    [file(finseq_5,t7_finseq_5),interesting(0.26)]).

fof(t24_finseq_5,theorem,(
    ! [A] : 
      ( m2_subset_1(A,k1_numbers,k5_numbers)
     => ! [B] : 
          ( ~ v1_xboole_0(B)
         => ! [C] : 
              ( m2_finseq_1(C,B)
             => ( k1_nat_1(A,1) = k3_finseq_1(C)
               => C = k8_finseq_1(B,k16_finseq_1(B,C,A),k12_finseq_1(B,k4_finseq_4(k5_numbers,B,C,k3_finseq_1(C)))) ) ) ) ) ),
    inference(mizar_proof,[status(thm)],[t25_finseq_1,t6_finseq_5,d15_finseq_1,d3_finseq_1,t97_relat_1,t11_finseq_5,d4_finseq_4]),
    [file(finseq_5,t24_finseq_5),interesting(0.23)]).

fof(t75_finseq_5,theorem,(
    ! [A] : 
      ( m2_subset_1(A,k1_numbers,k5_numbers)
     => ! [B] : 
          ( m2_subset_1(B,k1_numbers,k5_numbers)
         => ! [C] : 
              ( ~ v1_xboole_0(C)
             => ! [D] : 
                  ( m1_subset_1(D,C)
                 => ! [E] : 
                      ( m2_finseq_1(E,C)
                     => ( r2_hidden(A,k4_finseq_1(k16_finseq_1(C,E,B)))
                       => k4_finseq_4(k5_numbers,C,k5_finseq_5(C,E,D,B),A) = k4_finseq_4(k5_numbers,C,E,A) ) ) ) ) ) ) ),
    inference(mizar_proof,[status(thm)],[t45_finseq_1,l17_finseq_5,t85_finseq_4]),
    [file(finseq_5,t75_finseq_5),interesting(0.21)]).

fof(t76_finseq_5,theorem,(
    ! [A] : 
      ( m2_subset_1(A,k1_numbers,k5_numbers)
     => ! [B] : 
          ( ~ v1_xboole_0(B)
         => ! [C] : 
              ( m1_subset_1(C,B)
             => ! [D] : 
                  ( m2_finseq_1(D,B)
                 => ( r1_xreal_0(A,k3_finseq_1(D))
                   => k4_finseq_4(k5_numbers,B,k5_finseq_5(B,D,C,A),k1_nat_1(A,1)) = C ) ) ) ) ) ),
    inference(mizar_proof,[status(thm)],[t80_finseq_1,t19_finseq_2,t29_nat_1,t27_finseq_3,l17_finseq_5,t82_finseq_4]),
    [file(finseq_5,t76_finseq_5),interesting(0.17)]).

fof(t69_finseq_5,theorem,(
    ! [A] : 
      ( m2_subset_1(A,k1_numbers,k5_numbers)
     => ! [B] : 
          ( m2_subset_1(B,k1_numbers,k5_numbers)
         => ! [C] : 
              ( ~ v1_xboole_0(C)
             => ! [D] : 
                  ( m2_finseq_1(D,C)
                 => ( ( r2_hidden(A,k4_finseq_1(D))
                      & k1_nat_1(A,B) = k1_nat_1(k3_finseq_1(D),1) )
                   => k4_finseq_4(k5_numbers,C,D,A) = k4_finseq_4(k5_numbers,C,k4_finseq_5(C,D),B) ) ) ) ) ) ),
    inference(mizar_proof,[status(thm)],[t62_finseq_5,d4_finseq_4,d3_finseq_5,d4_finseq_4]),
    [file(finseq_5,t69_finseq_5),interesting(0.15)]).

fof(s1_finseq_5,theorem,(
    ? [A] : 
      ( v1_relat_1(A)
      & v1_funct_1(A)
      & v1_finseq_1(A)
      & k3_finseq_1(A) = f1_s1_finseq_5
      & ! [B] : 
          ( m2_subset_1(B,k1_numbers,k5_numbers)
         => ( r2_hidden(B,k4_finseq_1(A))
           => k1_funct_1(A,B) = f2_s1_finseq_5(B) ) ) ) ),
    inference(mizar_proof,[status(thm)],[s2_finseq_1,d3_finseq_1]),
    [file(finseq_5,s1_finseq_5),interesting(0.14)]).

fof(t11_finseq_5,theorem,(
    ! [A] : 
      ( m2_subset_1(A,k1_numbers,k5_numbers)
     => ! [B] : 
          ( ( v1_relat_1(B)
            & v1_funct_1(B)
            & v1_finseq_1(B) )
         => ! [C] : 
              ( ( v1_relat_1(C)
                & v1_funct_1(C)
                & v1_finseq_1(C) )
             => ( ( r2_hidden(k1_nat_1(A,1),k4_finseq_1(B))
                  & C = k7_relat_1(B,k2_finseq_1(A)) )
               => k7_relat_1(B,k2_finseq_1(k1_nat_1(A,1))) = k7_finseq_1(C,k9_finseq_1(k1_funct_1(B,k1_nat_1(A,1)))) ) ) ) ) ),
    inference(mizar_proof,[status(thm)],[t19_finseq_1,t6_finseq_1,t72_funct_1,t29_nat_1,t7_finseq_1,t82_funct_1,t27_finseq_3,t21_finseq_1,t61_finseq_3]),
    [file(finseq_5,t11_finseq_5),interesting(0.06)]).

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(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(t29_finseq_4,theorem,(
    ! [A] : 
      ( ( v1_relat_1(A)
        & v1_funct_1(A)
        & v1_finseq_1(A) )
     => ! [B] : 
          ( r2_hidden(B,k2_relat_1(A))
         => k1_funct_1(A,k5_finseq_4(A,B)) = B ) ) ),
    file(finseq_4,t29_finseq_4),
    [interesting(0.00)]).

fof(d4_finseq_4,definition,(
    ! [A,B,C] : 
      ( ( v1_funct_1(C)
        & m2_relset_1(C,A,B) )
     => ! [D] : 
          ( r2_hidden(D,k1_relat_1(C))
         => k4_finseq_4(A,B,C,D) = k1_funct_1(C,D) ) ) ),
    file(finseq_4,d4_finseq_4),
    [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(t13_finseq_5,theorem,(
    ! [A] : 
      ( ~ v1_xboole_0(A)
     => ! [B] : 
          ( m2_finseq_1(B,A)
         => ! [C] : 
              ( m2_finseq_1(C,A)
             => ( ( k4_finseq_1(B) = k4_finseq_1(C)
                  & ! [D] : 
                      ( m2_subset_1(D,k1_numbers,k5_numbers)
                     => ( r2_hidden(D,k4_finseq_1(B))
                       => k4_finseq_4(k5_numbers,A,B,D) = k4_finseq_4(k5_numbers,A,C,D) ) ) )
               => B = C ) ) ) ) ),
    inference(mizar_proof,[status(thm)],[d4_finseq_4,d4_finseq_4,t17_finseq_1]),
    [file(finseq_5,t13_finseq_5),interesting(0.00)]).

fof(t17_finseq_5,theorem,(
    $true ),
    file(finseq_5,t17_finseq_5),
    [interesting(0.00)]).

fof(t22_finseq_5,theorem,(
    $true ),
    file(finseq_5,t22_finseq_5),
    [interesting(0.00)]).

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

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

fof(t27_finseq_3,theorem,(
    ! [A] : 
      ( ( v1_relat_1(A)
        & v1_funct_1(A)
        & v1_finseq_1(A) )
     => ! [B] : 
          ( v4_ordinal2(B)
         => ( r2_hidden(B,k4_finseq_1(A))
          <=> ( r1_xreal_0(1,B)
              & r1_xreal_0(B,k3_finseq_1(A)) ) ) ) ) ),
    file(finseq_3,t27_finseq_3),
    [interesting(0.00)]).

fof(d15_finseq_1,definition,(
    ! [A,B] : 
      ( m2_finseq_1(B,A)
     => ! [C] : 
          ( v4_ordinal2(C)
         => k16_finseq_1(A,B,C) = k7_relat_1(B,k2_finseq_1(C)) ) ) ),
    file(finseq_1,d15_finseq_1),
    [interesting(0.00)]).

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

fof(t19_finseq_1,theorem,(
    ! [A] : 
      ( v4_ordinal2(A)
     => ! [B] : 
          ( ( v1_relat_1(B)
            & v1_funct_1(B)
            & v1_finseq_1(B) )
         => ( v1_relat_1(k7_relat_1(B,k2_finseq_1(A)))
            & v1_funct_1(k7_relat_1(B,k2_finseq_1(A)))
            & v1_finseq_1(k7_relat_1(B,k2_finseq_1(A))) ) ) ) ),
    file(finseq_1,t19_finseq_1),
    [interesting(0.00)]).

fof(t6_finseq_1,theorem,(
    ! [A] : 
      ( v4_ordinal2(A)
     => r2_hidden(k2_xcmplx_0(A,1),k2_finseq_1(k2_xcmplx_0(A,1))) ) ),
    file(finseq_1,t6_finseq_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(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(t7_finseq_1,theorem,(
    ! [A] : 
      ( v4_ordinal2(A)
     => ! [B] : 
          ( v4_ordinal2(B)
         => ( r1_xreal_0(A,B)
          <=> r1_tarski(k2_finseq_1(A),k2_finseq_1(B)) ) ) ) ),
    file(finseq_1,t7_finseq_1),
    [interesting(0.00)]).

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

fof(t21_finseq_1,theorem,(
    ! [A] : 
      ( v4_ordinal2(A)
     => ! [B] : 
          ( ( v1_relat_1(B)
            & v1_funct_1(B)
            & v1_finseq_1(B) )
         => ! [C] : 
              ( ( v1_relat_1(C)
                & v1_funct_1(C)
                & v1_finseq_1(C) )
             => ( ( r1_xreal_0(A,k3_finseq_1(B))
                  & C = k7_relat_1(B,k2_finseq_1(A)) )
               => ( k3_finseq_1(C) = A
                  & k4_finseq_1(C) = k2_finseq_1(A) ) ) ) ) ) ),
    file(finseq_1,t21_finseq_1),
    [interesting(0.00)]).

fof(t61_finseq_3,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) )
         => ! [C] : 
              ( v4_ordinal2(C)
             => ( ( k3_finseq_1(A) = k2_xcmplx_0(C,1)
                  & B = k7_relat_1(A,k2_finseq_1(C)) )
               => A = k7_finseq_1(B,k9_finseq_1(k1_funct_1(A,k2_xcmplx_0(C,1)))) ) ) ) ) ),
    file(finseq_3,t61_finseq_3),
    [interesting(0.00)]).

fof(t23_finseq_2,theorem,(
    ! [A] : 
      ( m2_subset_1(A,k1_numbers,k5_numbers)
     => ! [B] : 
          ( ( v1_relat_1(B)
            & v1_funct_1(B)
            & v1_finseq_1(B) )
         => ! [C] : 
              ( ( v1_relat_1(C)
                & v1_funct_1(C)
                & v1_finseq_1(C) )
             => ( ( B = k7_relat_1(C,k2_finseq_1(A))
                  & r1_xreal_0(k3_finseq_1(C),A) )
               => C = B ) ) ) ) ),
    file(finseq_2,t23_finseq_2),
    [interesting(0.00)]).

fof(t80_finseq_1,theorem,(
    ! [A,B] : 
      ( m2_finseq_1(B,A)
     => ! [C] : 
          ( v4_ordinal2(C)
         => ( r1_xreal_0(C,k3_finseq_1(B))
           => k3_finseq_1(k16_finseq_1(A,B,C)) = C ) ) ) ),
    file(finseq_1,t80_finseq_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(t35_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) )
         => k3_finseq_1(k7_finseq_1(A,B)) = k1_nat_1(k3_finseq_1(A),k3_finseq_1(B)) ) ) ),
    file(finseq_1,t35_finseq_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(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(d7_finseq_1,definition,(
    ! [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) )
         => ! [C] : 
              ( ( v1_relat_1(C)
                & v1_funct_1(C)
                & v1_finseq_1(C) )
             => ( C = k7_finseq_1(A,B)
              <=> ( k4_finseq_1(C) = k2_finseq_1(k1_nat_1(k3_finseq_1(A),k3_finseq_1(B)))
                  & ! [D] : 
                      ( m2_subset_1(D,k1_numbers,k5_numbers)
                     => ( r2_hidden(D,k4_finseq_1(A))
                       => k1_funct_1(C,D) = k1_funct_1(A,D) ) )
                  & ! [D] : 
                      ( m2_subset_1(D,k1_numbers,k5_numbers)
                     => ( r2_hidden(D,k4_finseq_1(B))
                       => k1_funct_1(C,k1_nat_1(k3_finseq_1(A),D)) = k1_funct_1(B,D) ) ) ) ) ) ) ) ),
    file(finseq_1,d7_finseq_1),
    [interesting(0.00)]).

fof(t10_finseq_2,theorem,(
    ! [A] : 
      ( m2_subset_1(A,k1_numbers,k5_numbers)
     => ! [B] : 
          ( ( v1_relat_1(B)
            & v1_funct_1(B)
            & v1_finseq_1(B) )
         => ! [C] : 
              ( ( v1_relat_1(C)
                & v1_funct_1(C)
                & v1_finseq_1(C) )
             => ( ( k3_finseq_1(B) = A
                  & k3_finseq_1(C) = A
                  & ! [D] : 
                      ( m2_subset_1(D,k1_numbers,k5_numbers)
                     => ( r2_hidden(D,k2_finseq_1(A))
                       => k1_funct_1(B,D) = k1_funct_1(C,D) ) ) )
               => B = C ) ) ) ) ),
    file(finseq_2,t10_finseq_2),
    [interesting(0.00)]).

fof(d6_finseq_4,definition,(
    ! [A] : 
      ( ( v1_relat_1(A)
        & v1_funct_1(A)
        & v1_finseq_1(A) )
     => ! [B] : 
          ( r2_hidden(B,k2_relat_1(A))
         => ! [C] : 
              ( ( v1_relat_1(C)
                & v1_funct_1(C)
                & v1_finseq_1(C) )
             => ( C = k6_finseq_4(A,B)
              <=> ? [D] : 
                    ( m2_subset_1(D,k1_numbers,k5_numbers)
                    & D = k6_xcmplx_0(k5_finseq_4(A,B),1)
                    & C = k7_relat_1(A,k2_finseq_1(D)) ) ) ) ) ) ),
    file(finseq_4,d6_finseq_4),
    [interesting(0.00)]).

fof(t30_finseq_4,theorem,(
    ! [A] : 
      ( ( v1_relat_1(A)
        & v1_funct_1(A)
        & v1_finseq_1(A) )
     => ! [B] : 
          ( r2_hidden(B,k2_relat_1(A))
         => r2_hidden(k5_finseq_4(A,B),k4_finseq_1(A)) ) ) ),
    file(finseq_4,t30_finseq_4),
    [interesting(0.00)]).

fof(d2_rfinseq,definition,(
    ! [A,B] : 
      ( m2_finseq_1(B,A)
     => ! [C] : 
          ( m2_subset_1(C,k1_numbers,k5_numbers)
         => ! [D] : 
              ( m2_finseq_1(D,A)
             => ( ( r1_xreal_0(C,k3_finseq_1(B))
                 => ( D = k1_rfinseq(A,B,C)
                  <=> ( k3_finseq_1(D) = k5_real_1(k3_finseq_1(B),C)
                      & ! [E] : 
                          ( m2_subset_1(E,k1_numbers,k5_numbers)
                         => ( r2_hidden(E,k4_finseq_1(D))
                           => k1_funct_1(D,E) = k1_funct_1(B,k1_nat_1(E,C)) ) ) ) ) )
                & ( ~ r1_xreal_0(C,k3_finseq_1(B))
                 => ( D = k1_rfinseq(A,B,C)
                  <=> D = k6_finseq_1(A) ) ) ) ) ) ) ),
    file(rfinseq,d2_rfinseq),
    [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(t18_nat_1,theorem,(
    ! [A] : 
      ( v4_ordinal2(A)
     => r1_xreal_0(0,A) ) ),
    file(nat_1,t18_nat_1),
    [interesting(0.00)]).

fof(t85_finseq_4,theorem,(
    ! [A] : 
      ( m2_subset_1(A,k1_numbers,k5_numbers)
     => ! [B] : 
          ( v4_ordinal2(B)
         => ! [C,D] : 
              ( m2_finseq_1(D,C)
             => ( r2_hidden(B,k4_finseq_1(k16_finseq_1(C,D,A)))
               => k4_finseq_4(k5_numbers,C,k16_finseq_1(C,D,A),B) = k4_finseq_4(k5_numbers,C,D,B) ) ) ) ) ),
    file(finseq_4,t85_finseq_4),
    [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(t21_rfinseq,theorem,(
    ! [A] : 
      ( ~ v1_xboole_0(A)
     => ! [B] : 
          ( m2_finseq_1(B,A)
         => ! [C] : 
              ( m2_subset_1(C,k1_numbers,k5_numbers)
             => k8_finseq_1(A,k16_finseq_1(A,B,C),k1_rfinseq(A,B,C)) = B ) ) ) ),
    file(rfinseq,t21_rfinseq),
    [interesting(0.00)]).

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

fof(t26_finseq_1,theorem,(
    ! [A] : 
      ( ( v1_relat_1(A)
        & v1_funct_1(A)
        & v1_finseq_1(A) )
     => ( A = k1_xboole_0
      <=> k4_finseq_1(A) = k1_xboole_0 ) ) ),
    file(finseq_1,t26_finseq_1),
    [interesting(0.00)]).

fof(t30_finseq_5,theorem,(
    ! [A] : 
      ( m2_subset_1(A,k1_numbers,k5_numbers)
     => ! [B] : 
          ( m2_subset_1(B,k1_numbers,k5_numbers)
         => ! [C] : 
              ( ~ v1_xboole_0(C)
             => ! [D] : 
                  ( m2_finseq_1(D,C)
                 => ( r2_hidden(A,k4_finseq_1(k1_rfinseq(C,D,B)))
                   => k4_finseq_4(k5_numbers,C,k1_rfinseq(C,D,B),A) = k4_finseq_4(k5_numbers,C,D,k1_nat_1(B,A)) ) ) ) ) ) ),
    inference(mizar_proof,[status(thm)],[t29_finseq_5,d4_finseq_4,d2_rfinseq,d4_finseq_4,d2_rfinseq,t26_finseq_1]),
    [file(finseq_5,t30_finseq_5),interesting(0.00)]).

fof(t33_finseq_5,theorem,(
    ! [A] : 
      ( m2_subset_1(A,k1_numbers,k5_numbers)
     => ! [B] : 
          ( ~ v1_xboole_0(B)
         => ! [C] : 
              ( m2_finseq_1(C,B)
             => ( k1_nat_1(A,1) = k3_finseq_1(C)
               => k1_rfinseq(B,C,A) = k12_finseq_1(B,k4_finseq_4(k5_numbers,B,C,k3_finseq_1(C))) ) ) ) ) ),
    inference(mizar_proof,[status(thm)],[t29_nat_1,d2_rfinseq,t27_finseq_3,t15_finseq_5,t30_finseq_5]),
    [file(finseq_5,t33_finseq_5),interesting(0.00)]).

fof(d7_finseq_4,definition,(
    ! [A] : 
      ( ( v1_relat_1(A)
        & v1_funct_1(A)
        & v1_finseq_1(A) )
     => ! [B] : 
          ( r2_hidden(B,k2_relat_1(A))
         => ! [C] : 
              ( ( v1_relat_1(C)
                & v1_funct_1(C)
                & v1_finseq_1(C) )
             => ( C = k7_finseq_4(A,B)
              <=> ( k3_finseq_1(C) = k6_xcmplx_0(k3_finseq_1(A),k5_finseq_4(A,B))
                  & ! [D] : 
                      ( m2_subset_1(D,k1_numbers,k5_numbers)
                     => ( r2_hidden(D,k4_finseq_1(C))
                       => k1_funct_1(C,D) = k1_funct_1(A,k1_nat_1(D,k5_finseq_4(A,B))) ) ) ) ) ) ) ) ),
    file(finseq_4,d7_finseq_4),
    [interesting(0.00)]).

fof(t31_finseq_4,theorem,(
    ! [A] : 
      ( ( v1_relat_1(A)
        & v1_funct_1(A)
        & v1_finseq_1(A) )
     => ! [B] : 
          ( r2_hidden(B,k2_relat_1(A))
         => ( r1_xreal_0(1,k5_finseq_4(A,B))
            & r1_xreal_0(k5_finseq_4(A,B),k3_finseq_1(A)) ) ) ) ),
    file(finseq_4,t31_finseq_4),
    [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(t84_finseq_4,theorem,(
    ! [A] : 
      ( m2_subset_1(A,k1_numbers,k5_numbers)
     => ! [B] : 
          ( ~ v1_xboole_0(B)
         => ! [C] : 
              ( m2_finseq_1(C,B)
             => ! [D] : 
                  ( m2_finseq_1(D,B)
                 => ( r2_hidden(A,k4_finseq_1(D))
                   => k4_finseq_4(k5_numbers,B,k8_finseq_1(B,C,D),k1_nat_1(k3_finseq_1(C),A)) = k4_finseq_4(k5_numbers,B,D,A) ) ) ) ) ) ),
    file(finseq_4,t84_finseq_4),
    [interesting(0.00)]).

fof(t24_finseq_4,theorem,(
    ! [A,B] : 
      ( m2_finseq_1(B,A)
     => ! [C] : 
          ( m2_subset_1(C,k1_numbers,k5_numbers)
         => ( ( r1_xreal_0(1,C)
              & r1_xreal_0(C,k3_finseq_1(B)) )
           => k4_finseq_4(k5_numbers,A,B,C) = k1_funct_1(B,C) ) ) ) ),
    file(finseq_4,t24_finseq_4),
    [interesting(0.00)]).

fof(t18_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) )
         => ( ( k3_finseq_1(A) = k3_finseq_1(B)
              & ! [C] : 
                  ( m2_subset_1(C,k1_numbers,k5_numbers)
                 => ( ( r1_xreal_0(1,C)
                      & r1_xreal_0(C,k3_finseq_1(A)) )
                   => k1_funct_1(A,C) = k1_funct_1(B,C) ) ) )
           => A = B ) ) ) ),
    file(finseq_1,t18_finseq_1),
    [interesting(0.00)]).

fof(t14_finseq_5,theorem,(
    ! [A] : 
      ( ~ v1_xboole_0(A)
     => ! [B] : 
          ( m2_finseq_1(B,A)
         => ! [C] : 
              ( m2_finseq_1(C,A)
             => ( ( k3_finseq_1(B) = k3_finseq_1(C)
                  & ! [D] : 
                      ( m2_subset_1(D,k1_numbers,k5_numbers)
                     => ( ( r1_xreal_0(1,D)
                          & r1_xreal_0(D,k3_finseq_1(B)) )
                       => k4_finseq_4(k5_numbers,A,B,D) = k4_finseq_4(k5_numbers,A,C,D) ) ) )
               => B = C ) ) ) ) ),
    inference(mizar_proof,[status(thm)],[t24_finseq_4,t24_finseq_4,t18_finseq_1]),
    [file(finseq_5,t14_finseq_5),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(t79_finseq_1,theorem,(
    ! [A,B] : 
      ( m2_finseq_1(B,A)
     => ! [C] : 
          ( v4_ordinal2(C)
         => ( r1_xreal_0(k3_finseq_1(B),C)
           => k16_finseq_1(A,B,C) = B ) ) ) ),
    file(finseq_1,t79_finseq_1),
    [interesting(0.00)]).

fof(t4_partfun2,theorem,(
    ! [A,B] : 
      ( ~ v1_xboole_0(B)
     => ! [C] : 
          ( ~ v1_xboole_0(C)
         => ! [D] : 
              ( ( v1_funct_1(D)
                & m2_relset_1(D,C,B) )
             => ( r2_hidden(A,k2_relat_1(D))
              <=> ? [E] : 
                    ( m1_subset_1(E,C)
                    & r2_hidden(E,k4_relset_1(C,B,D))
                    & A = k4_finseq_4(C,B,D,E) ) ) ) ) ) ),
    file(partfun2,t4_partfun2),
    [interesting(0.00)]).

fof(d5_finseq_4,definition,(
    ! [A] : 
      ( ( v1_relat_1(A)
        & v1_funct_1(A)
        & v1_finseq_1(A) )
     => ! [B] : k5_finseq_4(A,B) = k1_funct_1(k14_finseq_1(k10_relat_1(A,k1_tarski(B))),1) ) ),
    file(finseq_4,d5_finseq_4),
    [interesting(0.00)]).

fof(t167_relat_1,theorem,(
    ! [A,B] : 
      ( v1_relat_1(B)
     => r1_tarski(k10_relat_1(B,A),k1_relat_1(B)) ) ),
    file(relat_1,t167_relat_1),
    [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(d13_funct_1,definition,(
    ! [A] : 
      ( ( v1_relat_1(A)
        & v1_funct_1(A) )
     => ! [B,C] : 
          ( C = k10_relat_1(A,B)
        <=> ! [D] : 
              ( r2_hidden(D,C)
            <=> ( r2_hidden(D,k1_relat_1(A))
                & r2_hidden(k1_funct_1(A,D),B) ) ) ) ) ),
    file(funct_1,d13_funct_1),
    [interesting(0.00)]).

fof(d13_finseq_1,definition,(
    ! [A] : 
      ( ? [B] : 
          ( v4_ordinal2(B)
          & r1_tarski(A,k2_finseq_1(B)) )
     => ! [B] : 
          ( m2_finseq_1(B,k5_numbers)
         => ( B = k14_finseq_1(A)
          <=> ( k2_relat_1(B) = A
              & ! [C] : 
                  ( v4_ordinal2(C)
                 => ! [D] : 
                      ( v4_ordinal2(D)
                     => ! [E] : 
                          ( v4_ordinal2(E)
                         => ! [F] : 
                              ( v4_ordinal2(F)
                             => ~ ( r1_xreal_0(1,C)
                                  & ~ r1_xreal_0(D,C)
                                  & r1_xreal_0(D,k3_finseq_1(B))
                                  & E = k1_funct_1(B,C)
                                  & F = k1_funct_1(B,D)
                                  & r1_xreal_0(F,E) ) ) ) ) ) ) ) ) ) ),
    file(finseq_1,d13_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(t46_finseq_3,theorem,(
    ! [A,B] : 
      ( v4_ordinal2(B)
     => ! [C] : 
          ( v4_ordinal2(C)
         => ! [D] : 
              ( v4_ordinal2(D)
             => ! [E] : 
                  ( v4_ordinal2(E)
                 => ! [F] : 
                      ( v4_ordinal2(F)
                     => ~ ( r1_tarski(A,k2_finseq_1(B))
                          & ~ r1_xreal_0(D,C)
                          & r1_xreal_0(1,E)
                          & r1_xreal_0(F,k3_finseq_1(k14_finseq_1(A)))
                          & k1_funct_1(k14_finseq_1(A),F) = C
                          & k1_funct_1(k14_finseq_1(A),E) = D
                          & r1_xreal_0(E,F) ) ) ) ) ) ) ),
    file(finseq_3,t46_finseq_3),
    [interesting(0.00)]).

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

fof(t10_finseq_4,theorem,(
    ! [A] : 
      ( ( v1_relat_1(A)
        & v1_funct_1(A) )
     => ( v2_funct_1(A)
      <=> ! [B] : 
            ( r2_hidden(B,k2_relat_1(A))
           => r2_finseq_4(A,B) ) ) ) ),
    file(finseq_4,t10_finseq_4),
    [interesting(0.00)]).

fof(t35_finseq_4,theorem,(
    ! [A] : 
      ( ( v1_relat_1(A)
        & v1_funct_1(A)
        & v1_finseq_1(A) )
     => ! [B] : 
          ( r2_finseq_4(A,B)
         => k1_finseq_4(A,B) = k5_finseq_4(A,B) ) ) ),
    file(finseq_4,t35_finseq_4),
    [interesting(0.00)]).

fof(d3_finseq_4,definition,(
    ! [A] : 
      ( ( v1_relat_1(A)
        & v1_funct_1(A) )
     => ! [B] : 
          ( r2_finseq_4(A,B)
         => ! [C] : 
              ( C = k1_finseq_4(A,B)
            <=> ( r2_hidden(C,k1_relat_1(A))
                & k1_funct_1(A,C) = B ) ) ) ) ),
    file(finseq_4,d3_finseq_4),
    [interesting(0.00)]).

fof(t86_finseq_4,theorem,(
    ! [A,B] : 
      ( m2_finseq_1(B,A)
     => ! [C] : 
          ( m2_subset_1(C,k1_numbers,k5_numbers)
         => ! [D] : 
              ( m2_subset_1(D,k1_numbers,k5_numbers)
             => ( ( r2_hidden(C,k4_finseq_1(B))
                  & r2_hidden(D,k2_finseq_1(C)) )
               => ( r2_hidden(D,k4_finseq_1(B))
                  & k4_finseq_4(k5_numbers,A,k16_finseq_1(A,B,C),D) = k4_finseq_4(k5_numbers,A,B,D) ) ) ) ) ) ),
    file(finseq_4,t86_finseq_4),
    [interesting(0.00)]).

fof(t3_finseq_4,theorem,(
    ! [A] : 
      ( ( v1_relat_1(A)
        & v1_funct_1(A) )
     => ! [B] : 
          ( r1_finseq_4(A,B)
        <=> ( r2_hidden(B,k1_relat_1(A))
            & k10_relat_1(A,k1_tarski(k1_funct_1(A,B))) = k1_tarski(B) ) ) ) ),
    file(finseq_4,t3_finseq_4),
    [interesting(0.00)]).

fof(t5_finseq_4,theorem,(
    ! [A] : 
      ( ( v1_relat_1(A)
        & v1_funct_1(A) )
     => ( ! [B] : 
            ( r2_hidden(B,k1_relat_1(A))
           => r1_finseq_4(A,B) )
      <=> v2_funct_1(A) ) ) ),
    file(finseq_4,t5_finseq_4),
    [interesting(0.00)]).

fof(t60_relat_1,theorem,
    ( k1_relat_1(k1_xboole_0) = k1_xboole_0
    & k2_relat_1(k1_xboole_0) = k1_xboole_0 ),
    file(relat_1,t60_relat_1),
    [interesting(0.00)]).

fof(t56_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
          & k2_relat_1(B) = k1_tarski(A) ) ) ) ),
    file(finseq_1,t56_finseq_1),
    [interesting(0.00)]).

fof(t58_finseq_1,theorem,(
    ! [A,B] : 
      ( ( v1_relat_1(B)
        & v1_funct_1(B)
        & v1_finseq_1(B) )
     => k1_funct_1(k7_finseq_1(k9_finseq_1(A),B),1) = A ) ),
    file(finseq_1,t58_finseq_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(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(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(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(t37_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) )
         => ! [C] : 
              ( v4_ordinal2(C)
             => ( r1_xreal_0(C,k3_finseq_1(k7_finseq_1(A,B)))
               => ( r1_xreal_0(C,k3_finseq_1(A))
                  | k1_funct_1(k7_finseq_1(A,B),C) = k1_funct_1(B,k6_xcmplx_0(C,k3_finseq_1(A))) ) ) ) ) ) ),
    file(finseq_1,t37_finseq_1),
    [interesting(0.00)]).

fof(t17_partfun2,theorem,(
    ! [A,B,C] : 
      ( ~ v1_xboole_0(C)
     => ! [D] : 
          ( ~ v1_xboole_0(D)
         => ! [E] : 
              ( ( v1_funct_1(E)
                & m2_relset_1(E,C,D) )
             => ( ( v2_funct_1(E)
                  & r2_hidden(A,k4_relset_1(C,D,E))
                  & r2_hidden(B,k4_relset_1(C,D,E))
                  & k4_finseq_4(C,D,E,A) = k4_finseq_4(C,D,E,B) )
               => A = B ) ) ) ) ),
    file(partfun2,t17_partfun2),
    [interesting(0.00)]).

fof(t16_partfun2,theorem,(
    ! [A] : 
      ( ~ v1_xboole_0(A)
     => ! [B] : 
          ( ~ v1_xboole_0(B)
         => ! [C] : 
              ( ( v1_funct_1(C)
                & m2_relset_1(C,B,A) )
             => ( ! [D] : 
                    ( m1_subset_1(D,B)
                   => ! [E] : 
                        ( m1_subset_1(E,B)
                       => ( ( r2_hidden(D,k4_relset_1(B,A,C))
                            & r2_hidden(E,k4_relset_1(B,A,C))
                            & k4_finseq_4(B,A,C,D) = k4_finseq_4(B,A,C,E) )
                         => D = E ) ) )
               => v2_funct_1(C) ) ) ) ) ),
    file(partfun2,t16_partfun2),
    [interesting(0.00)]).

fof(t144_funct_1,theorem,(
    ! [A] : 
      ( ( v1_relat_1(A)
        & v1_funct_1(A) )
     => ( ! [B] : ~ ( r2_hidden(B,k2_relat_1(A))
            & ! [C] : k10_relat_1(A,k1_tarski(B)) != k1_tarski(C) )
      <=> v2_funct_1(A) ) ) ),
    file(funct_1,t144_funct_1),
    [interesting(0.00)]).

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

fof(t4_finseq_1,theorem,
    ( k2_finseq_1(0) = k1_xboole_0
    & k2_finseq_1(1) = k1_tarski(1)
    & k2_finseq_1(2) = k2_tarski(1,2) ),
    file(finseq_1,t4_finseq_1),
    [interesting(0.00)]).

fof(d3_finseq_5,definition,(
    ! [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) )
         => ( B = k3_finseq_5(A)
          <=> ( k3_finseq_1(B) = k3_finseq_1(A)
              & ! [C] : 
                  ( m2_subset_1(C,k1_numbers,k5_numbers)
                 => ( r2_hidden(C,k4_finseq_1(B))
                   => k1_funct_1(B,C) = k1_funct_1(A,k2_xcmplx_0(k6_xcmplx_0(k3_finseq_1(A),C),1)) ) ) ) ) ) ) ),
    file(finseq_5,d3_finseq_5),
    [interesting(0.00)]).

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

fof(d2_tarski,definition,(
    ! [A,B,C] : 
      ( C = k2_tarski(A,B)
    <=> ! [D] : 
          ( r2_hidden(D,C)
        <=> ( D = A
            | D = B ) ) ) ),
    file(tarski,d2_tarski),
    [interesting(0.00)]).

fof(t47_finseq_1,theorem,(
    ! [A] : 
      ( ( v1_relat_1(A)
        & v1_funct_1(A)
        & v1_finseq_1(A) )
     => ( k7_finseq_1(A,k1_xboole_0) = A
        & k7_finseq_1(k1_xboole_0,A) = A ) ) ),
    file(finseq_1,t47_finseq_1),
    [interesting(0.00)]).

fof(t45_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) )
         => ! [C] : 
              ( ( v1_relat_1(C)
                & v1_funct_1(C)
                & v1_finseq_1(C) )
             => k7_finseq_1(k7_finseq_1(A,B),C) = k7_finseq_1(A,k7_finseq_1(B,C)) ) ) ) ),
    file(finseq_1,t45_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(t59_finseq_1,theorem,(
    ! [A,B] : 
      ( ( v1_relat_1(B)
        & v1_funct_1(B)
        & v1_finseq_1(B) )
     => k1_funct_1(k7_finseq_1(B,k9_finseq_1(A)),k1_nat_1(k3_finseq_1(B),1)) = A ) ),
    file(finseq_1,t59_finseq_1),
    [interesting(0.00)]).

fof(t60_nat_1,theorem,(
    ! [A] : 
      ( v4_ordinal2(A)
     => ! [B] : 
          ( v4_ordinal2(B)
         => ( ~ r1_xreal_0(B,A)
           => m2_subset_1(k6_xcmplx_0(B,1),k1_numbers,k5_numbers) ) ) ) ),
    file(nat_1,t60_nat_1),
    [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(t10_xreal_1,theorem,(
    ! [A] : 
      ( v1_xreal_0(A)
     => ! [B] : 
          ( v1_xreal_0(B)
         => ! [C] : 
              ( v1_xreal_0(C)
             => ! [D] : 
                  ( v1_xreal_0(D)
                 => ~ ( ~ r1_xreal_0(B,A)
                      & r1_xreal_0(C,D)
                      & r1_xreal_0(k2_xcmplx_0(B,D),k2_xcmplx_0(A,C)) ) ) ) ) ) ),
    file(xreal_1,t10_xreal_1),
    [interesting(0.00)]).

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

fof(t45_xreal_1,theorem,(
    ! [A] : 
      ( v1_xreal_0(A)
     => ! [B] : 
          ( v1_xreal_0(B)
         => ( r1_xreal_0(0,A)
           => r1_xreal_0(k6_xcmplx_0(B,A),B) ) ) ) ),
    file(xreal_1,t45_xreal_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(s3_finseq_1,theorem,
    ( ( p1_s3_finseq_1(k1_xboole_0)
      & ! [A] : 
          ( ( v1_relat_1(A)
            & v1_funct_1(A)
            & v1_finseq_1(A) )
         => ! [B] : 
              ( p1_s3_finseq_1(A)
             => p1_s3_finseq_1(k7_finseq_1(A,k9_finseq_1(B))) ) ) )
   => ! [A] : 
        ( ( v1_relat_1(A)
          & v1_funct_1(A)
          & v1_finseq_1(A) )
       => p1_s3_finseq_1(A) ) ),
    file(finseq_1,s3_finseq_1),
    [interesting(0.00)]).

fof(d4_funct_1,definition,(
    ! [A] : 
      ( ( v1_relat_1(A)
        & v1_funct_1(A) )
     => ! [B,C] : 
          ( ( r2_hidden(B,k1_relat_1(A))
           => ( C = k1_funct_1(A,B)
            <=> r2_hidden(k4_tarski(B,C),A) ) )
          & ( ~ r2_hidden(B,k1_relat_1(A))
           => ( C = k1_funct_1(A,B)
            <=> C = k1_xboole_0 ) ) ) ) ),
    file(funct_1,d4_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(t65_finseq_5,theorem,(
    ! [A] : 
      ( ( v1_relat_1(A)
        & v1_funct_1(A)
        & v1_finseq_1(A) )
     => ( k1_funct_1(A,1) = k1_funct_1(k3_finseq_5(A),k3_finseq_1(A))
        & k1_funct_1(A,k3_finseq_1(A)) = k1_funct_1(k3_finseq_5(A),1) ) ) ),
    inference(mizar_proof,[status(thm)],[t60_finseq_5,t60_relat_1,d4_funct_1,t60_relat_1,d4_funct_1,d4_funct_1,t60_relat_1,d4_funct_1,t25_finseq_1,t5_finseq_1,d3_finseq_1,t61_finseq_5,t39_nat_1,t27_finseq_3,t61_finseq_5]),
    [file(finseq_5,t65_finseq_5),interesting(0.00)]).

fof(t68_finseq_5,theorem,(
    ! [A] : 
      ( ~ v1_xboole_0(A)
     => ! [B] : 
          ( m2_finseq_1(B,A)
         => ( ~ v1_xboole_0(B)
           => ( k4_finseq_4(k5_numbers,A,B,1) = k4_finseq_4(k5_numbers,A,k4_finseq_5(A,B),k3_finseq_1(B))
              & k4_finseq_4(k5_numbers,A,B,k3_finseq_1(B)) = k4_finseq_4(k5_numbers,A,k4_finseq_5(A,B),1) ) ) ) ) ),
    inference(mizar_proof,[status(thm)],[t6_finseq_5,t6_finseq_5,t60_finseq_5,d4_finseq_4,t65_finseq_5,d4_finseq_4,d4_finseq_4,t65_finseq_5,d4_finseq_4]),
    [file(finseq_5,t68_finseq_5),interesting(0.00)]).

fof(d2_xboole_0,definition,(
    ! [A,B,C] : 
      ( C = k2_xboole_0(A,B)
    <=> ! [D] : 
          ( r2_hidden(D,C)
        <=> ( r2_hidden(D,A)
            | r2_hidden(D,B) ) ) ) ),
    file(xboole_0,d2_xboole_0),
    [interesting(0.00)]).

fof(t44_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) )
         => k2_relat_1(k7_finseq_1(A,B)) = k2_xboole_0(k2_relat_1(A),k2_relat_1(B)) ) ) ),
    file(finseq_1,t44_finseq_1),
    [interesting(0.00)]).

fof(t4_xboole_1,theorem,(
    ! [A,B,C] : k2_xboole_0(k2_xboole_0(A,B),C) = k2_xboole_0(A,k2_xboole_0(B,C)) ),
    file(xboole_1,t4_xboole_1),
    [interesting(0.00)]).

fof(t55_finseq_1,theorem,(
    ! [A,B] : 
      ( ( v1_relat_1(B)
        & v1_funct_1(B)
        & v1_finseq_1(B) )
     => ( B = k9_finseq_1(A)
      <=> ( k4_finseq_1(B) = k2_finseq_1(1)
          & k2_relat_1(B) = k1_tarski(A) ) ) ) ),
    file(finseq_1,t55_finseq_1),
    [interesting(0.00)]).

fof(t39_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) )
         => r1_tarski(k4_finseq_1(A),k4_finseq_1(k7_finseq_1(A,B))) ) ) ),
    file(finseq_1,t39_finseq_1),
    [interesting(0.00)]).

fof(t82_finseq_4,theorem,(
    ! [A] : 
      ( ~ v1_xboole_0(A)
     => ! [B] : 
          ( m2_finseq_1(B,A)
         => ! [C] : 
              ( m1_subset_1(C,A)
             => k4_finseq_4(k5_numbers,A,k8_finseq_1(A,B,k12_finseq_1(A,C)),k1_nat_1(k3_finseq_1(B),1)) = C ) ) ) ),
    file(finseq_4,t82_finseq_4),
    [interesting(0.00)]).

fof(t77_finseq_5,theorem,(
    ! [A] : 
      ( m2_subset_1(A,k1_numbers,k5_numbers)
     => ! [B] : 
          ( m2_subset_1(B,k1_numbers,k5_numbers)
         => ! [C] : 
              ( ~ v1_xboole_0(C)
             => ! [D] : 
                  ( m1_subset_1(D,C)
                 => ! [E] : 
                      ( m2_finseq_1(E,C)
                     => ( ( r1_xreal_0(k1_nat_1(A,1),B)
                          & r1_xreal_0(B,k3_finseq_1(E)) )
                       => k4_finseq_4(k5_numbers,C,k5_finseq_5(C,E,D,A),k1_nat_1(B,1)) = k4_finseq_4(k5_numbers,C,E,B) ) ) ) ) ) ) ),
    inference(mizar_proof,[status(thm)],[t29_nat_1,t2_xreal_1,t2_xreal_1,t80_finseq_1,t19_finseq_2,t18_int_1,t29_nat_1,t21_xreal_1,d2_rfinseq,t27_finseq_3,t84_finseq_4,t30_finseq_5]),
    [file(finseq_5,t77_finseq_5),interesting(0.00)]).

fof(t78_finseq_5,theorem,(
    ! [A] : 
      ( m2_subset_1(A,k1_numbers,k5_numbers)
     => ! [B] : 
          ( ~ v1_xboole_0(B)
         => ! [C] : 
              ( m1_subset_1(C,B)
             => ! [D] : 
                  ( m2_finseq_1(D,B)
                 => ( r1_xreal_0(1,A)
                   => ( v1_xboole_0(D)
                      | k4_finseq_4(k5_numbers,B,k5_finseq_5(B,D,C,A),1) = k4_finseq_4(k5_numbers,B,D,1) ) ) ) ) ) ) ),
    inference(mizar_proof,[status(thm)],[t25_finseq_1,t39_nat_1,t80_finseq_1,t79_finseq_1,t27_finseq_3,t75_finseq_5]),
    [file(finseq_5,t78_finseq_5),interesting(0.00)]).

fof(t102_finseq_3,theorem,(
    ! [A] : v2_funct_1(k9_finseq_1(A)) ),
    file(finseq_3,t102_finseq_3),
    [interesting(0.00)]).

fof(t3_xboole_0,theorem,(
    ! [A,B] : 
      ( ~ ( ~ r1_xboole_0(A,B)
          & ! [C] : ~ ( r2_hidden(C,A)
              & r2_hidden(C,B) ) )
      & ~ ( ? [C] : 
              ( r2_hidden(C,A)
              & r2_hidden(C,B) )
          & r1_xboole_0(A,B) ) ) ),
    file(xboole_0,t3_xboole_0),
    [interesting(0.00)]).

fof(t98_finseq_3,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) )
         => ( ( r1_xboole_0(k2_relat_1(A),k2_relat_1(B))
              & v2_funct_1(A)
              & v2_funct_1(B) )
          <=> v2_funct_1(k7_finseq_1(A,B)) ) ) ) ),
    file(finseq_3,t98_finseq_3),
    [interesting(0.00)]).

fof(t80_finseq_5,theorem,(
    ! [A] : 
      ( ~ v1_xboole_0(A)
     => ! [B] : 
          ( m2_finseq_1(B,A)
         => ! [C] : 
              ( m2_subset_1(C,k1_numbers,k5_numbers)
             => ! [D] : 
                  ( m2_subset_1(D,k1_numbers,k5_numbers)
                 => ( r1_xreal_0(C,D)
                   => ( k16_finseq_1(A,k16_finseq_1(A,B,C),D) = k16_finseq_1(A,B,C)
                      & k16_finseq_1(A,k16_finseq_1(A,B,D),C) = k16_finseq_1(A,B,C) ) ) ) ) ) ) ),
    inference(mizar_proof,[status(thm)],[t19_finseq_5,t2_xreal_1,t79_finseq_1,d15_finseq_1,d15_finseq_1,d15_finseq_1,t7_finseq_1,t82_funct_1]),
    [file(finseq_5,t80_finseq_5),interesting(0.00)]).

fof(t82_finseq_5,theorem,(
    ! [A] : 
      ( ~ v1_xboole_0(A)
     => k4_finseq_5(A,k6_finseq_1(A)) = k6_finseq_1(A) ) ),
    file(finseq_5,t82_finseq_5),
    [interesting(0.00)]).

fof(t9_finseq_5,theorem,(
    $true ),
    file(finseq_5,t9_finseq_5),
    [interesting(0.00)]).