fof(l18_finsop_1,theorem,(
    ! [A] : 
      ( ~ v1_xboole_0(A)
     => ! [B] : 
          ( m2_finseq_1(B,A)
         => ! [C] : 
              ( m2_finseq_1(C,A)
             => ! [D] : 
                  ( ( v1_funct_1(D)
                    & v1_funct_2(D,k2_zfmisc_1(A,A),A)
                    & m2_relset_1(D,k2_zfmisc_1(A,A),A) )
                 => ( ( v2_binop_1(D,A)
                      & v1_binop_1(D,A)
                      & v2_funct_1(B)
                      & v2_funct_1(C)
                      & k2_relat_1(B) = k2_relat_1(C)
                      & r1_xreal_0(1,k3_finseq_1(B)) )
                   => k2_finsop_1(A,B,D) = k2_finsop_1(A,C,D) ) ) ) ) ) ),
    inference(mizar_proof,[status(thm)],[t65_finseq_1,t55_funct_1,t46_relat_1,d3_finseq_1,d3_finseq_1,t55_funct_1,t45_relat_1,d3_finseq_1,t5_finseq_1,d1_funct_2,t11_relset_1,t47_relat_1,t55_funct_1,t62_funct_1,t46_funct_1,t83_funct_2,t55_relat_1,t61_funct_1,t42_funct_1,t8_finsop_1]),
    [file(finsop_1,l18_finsop_1),interesting(1.00)]).

fof(t9_finsop_1,theorem,(
    ! [A] : 
      ( ~ v1_xboole_0(A)
     => ! [B] : 
          ( m2_finseq_1(B,A)
         => ! [C] : 
              ( m2_finseq_1(C,A)
             => ! [D] : 
                  ( ( v1_funct_1(D)
                    & v1_funct_2(D,k2_zfmisc_1(A,A),A)
                    & m2_relset_1(D,k2_zfmisc_1(A,A),A) )
                 => ( ( v2_binop_1(D,A)
                      & v1_binop_1(D,A)
                      & v2_funct_1(B)
                      & v2_funct_1(C)
                      & k2_relat_1(B) = k2_relat_1(C) )
                   => ( ( ~ v1_setwiseo(D,A)
                        & ~ r1_xreal_0(1,k3_finseq_1(B)) )
                      | k2_finsop_1(A,B,D) = k2_finsop_1(A,C,D) ) ) ) ) ) ) ),
    inference(mizar_proof,[status(thm)],[t39_nat_1,l18_finsop_1,l19_finsop_1]),
    [file(finsop_1,t9_finsop_1),interesting(0.89)]).

fof(t13_finsop_1,theorem,(
    ! [A] : 
      ( ~ v1_xboole_0(A)
     => ! [B] : 
          ( m1_subset_1(B,A)
         => ! [C] : 
              ( m1_subset_1(C,A)
             => ! [D] : 
                  ( ( v1_funct_1(D)
                    & v1_funct_2(D,k2_zfmisc_1(A,A),A)
                    & m2_relset_1(D,k2_zfmisc_1(A,A),A) )
                 => k2_finsop_1(A,k2_finseq_4(A,B,C),D) = k2_binop_1(A,A,A,D,B,C) ) ) ) ) ),
    inference(mizar_proof,[status(thm)],[t56_finseq_1,d9_finseq_1,t5_finsop_1,l9_finsop_1]),
    [file(finsop_1,t13_finsop_1),interesting(0.88)]).

fof(l9_finsop_1,theorem,(
    ! [A] : 
      ( ~ v1_xboole_0(A)
     => ! [B] : 
          ( m1_subset_1(B,A)
         => ! [C] : 
              ( ( v1_funct_1(C)
                & v1_funct_2(C,k2_zfmisc_1(A,A),A)
                & m2_relset_1(C,k2_zfmisc_1(A,A),A) )
             => k2_finsop_1(A,k12_finseq_1(A,B),C) = B ) ) ) ),
    inference(mizar_proof,[status(thm)],[t56_finseq_1,t2_finsop_1,d8_finseq_1]),
    [file(finsop_1,l9_finsop_1),interesting(0.82)]).

fof(t17_finsop_1,theorem,(
    ! [A] : 
      ( ~ v1_xboole_0(A)
     => ! [B] : 
          ( m1_subset_1(B,A)
         => ! [C] : 
              ( ( v1_funct_1(C)
                & v1_funct_2(C,k2_zfmisc_1(A,A),A)
                & m2_relset_1(C,k2_zfmisc_1(A,A),A) )
             => k2_finsop_1(A,k1_finsop_1(A,1,B),C) = B ) ) ) ),
    inference(mizar_proof,[status(thm)],[t73_finseq_2,l9_finsop_1]),
    [file(finsop_1,t17_finsop_1),interesting(0.80)]).

fof(l8_finsop_1,theorem,(
    ! [A] : 
      ( ~ v1_xboole_0(A)
     => ! [B] : 
          ( ( v1_funct_1(B)
            & v1_funct_2(B,k2_zfmisc_1(A,A),A)
            & m2_relset_1(B,k2_zfmisc_1(A,A),A) )
         => ( v1_setwiseo(B,A)
           => k2_finsop_1(A,k6_finseq_1(A),B) = k3_binop_1(A,B) ) ) ) ),
    inference(mizar_proof,[status(thm)],[t32_finseq_1,d1_finsop_1]),
    [file(finsop_1,l8_finsop_1),interesting(0.79)]).

fof(t14_finsop_1,theorem,(
    ! [A] : 
      ( ~ v1_xboole_0(A)
     => ! [B] : 
          ( m1_subset_1(B,A)
         => ! [C] : 
              ( m1_subset_1(C,A)
             => ! [D] : 
                  ( ( v1_funct_1(D)
                    & v1_funct_2(D,k2_zfmisc_1(A,A),A)
                    & m2_relset_1(D,k2_zfmisc_1(A,A),A) )
                 => ( v1_binop_1(D,A)
                   => k2_finsop_1(A,k2_finseq_4(A,B,C),D) = k2_finsop_1(A,k2_finseq_4(A,C,B),D) ) ) ) ) ) ),
    inference(mizar_proof,[status(thm)],[t13_finsop_1,d2_binop_1,t13_finsop_1]),
    [file(finsop_1,t14_finsop_1),interesting(0.78)]).

fof(t18_finsop_1,theorem,(
    ! [A] : 
      ( ~ v1_xboole_0(A)
     => ! [B] : 
          ( m1_subset_1(B,A)
         => ! [C] : 
              ( ( v1_funct_1(C)
                & v1_funct_2(C,k2_zfmisc_1(A,A),A)
                & m2_relset_1(C,k2_zfmisc_1(A,A),A) )
             => k2_finsop_1(A,k1_finsop_1(A,2,B),C) = k2_binop_1(A,A,A,C,B,B) ) ) ) ),
    inference(mizar_proof,[status(thm)],[t75_finseq_2,t13_finsop_1]),
    [file(finsop_1,t18_finsop_1),interesting(0.77)]).

fof(l21_finsop_1,theorem,(
    ! [A] : 
      ( ~ v1_xboole_0(A)
     => ! [B] : 
          ( m2_finseq_1(B,A)
         => ! [C] : 
              ( ( v1_funct_1(C)
                & v1_funct_2(C,k2_zfmisc_1(A,A),A)
                & m2_relset_1(C,k2_zfmisc_1(A,A),A) )
             => ( k3_finseq_1(B) = 1
               => k2_finsop_1(A,B,C) = k1_funct_1(B,1) ) ) ) ) ),
    inference(mizar_proof,[status(thm)],[t57_finseq_1,t24_finseq_4,l9_finsop_1,t24_finseq_4]),
    [file(finsop_1,l21_finsop_1),interesting(0.74)]).

fof(t12_finsop_1,theorem,(
    ! [A] : 
      ( ~ v1_xboole_0(A)
     => ! [B] : 
          ( m1_subset_1(B,A)
         => ! [C] : 
              ( ( v1_funct_1(C)
                & v1_funct_2(C,k2_zfmisc_1(A,A),A)
                & m2_relset_1(C,k2_zfmisc_1(A,A),A) )
             => k2_finsop_1(A,k12_finseq_1(A,B),C) = B ) ) ) ),
    inference(mizar_proof,[status(thm)],[l9_finsop_1]),
    [file(finsop_1,t12_finsop_1),interesting(0.74)]).

fof(t15_finsop_1,theorem,(
    ! [A] : 
      ( ~ v1_xboole_0(A)
     => ! [B] : 
          ( m1_subset_1(B,A)
         => ! [C] : 
              ( m1_subset_1(C,A)
             => ! [D] : 
                  ( m1_subset_1(D,A)
                 => ! [E] : 
                      ( ( v1_funct_1(E)
                        & v1_funct_2(E,k2_zfmisc_1(A,A),A)
                        & m2_relset_1(E,k2_zfmisc_1(A,A),A) )
                     => k2_finsop_1(A,k3_finseq_4(A,B,C,D),E) = k2_binop_1(A,A,A,E,k2_binop_1(A,A,A,E,B,C),D) ) ) ) ) ) ),
    inference(mizar_proof,[status(thm)],[t56_finseq_1,t61_finseq_1,t60_finseq_1,t5_finsop_1,t13_finsop_1]),
    [file(finsop_1,t15_finsop_1),interesting(0.73)]).

fof(t11_finsop_1,theorem,(
    ! [A] : 
      ( ~ v1_xboole_0(A)
     => ! [B] : 
          ( ( v1_funct_1(B)
            & v1_funct_2(B,k2_zfmisc_1(A,A),A)
            & m2_relset_1(B,k2_zfmisc_1(A,A),A) )
         => ( v1_setwiseo(B,A)
           => k2_finsop_1(A,k6_finseq_1(A),B) = k3_binop_1(A,B) ) ) ) ),
    inference(mizar_proof,[status(thm)],[l8_finsop_1]),
    [file(finsop_1,t11_finsop_1),interesting(0.69)]).

fof(t8_finsop_1,theorem,(
    ! [A] : 
      ( ~ v1_xboole_0(A)
     => ! [B] : 
          ( m2_finseq_1(B,A)
         => ! [C] : 
              ( m2_finseq_1(C,A)
             => ! [D] : 
                  ( ( v1_funct_1(D)
                    & v1_funct_2(D,k2_zfmisc_1(A,A),A)
                    & m2_relset_1(D,k2_zfmisc_1(A,A),A) )
                 => ! [E] : 
                      ( ( v1_funct_1(E)
                        & v1_funct_2(E,k4_relset_1(k5_numbers,A,B),k4_relset_1(k5_numbers,A,B))
                        & v3_funct_2(E,k4_relset_1(k5_numbers,A,B),k4_relset_1(k5_numbers,A,B))
                        & m2_relset_1(E,k4_relset_1(k5_numbers,A,B),k4_relset_1(k5_numbers,A,B)) )
                     => ( ( v1_binop_1(D,A)
                          & v2_binop_1(D,A)
                          & C = k5_relat_1(E,B) )
                       => ( ( ~ v1_setwiseo(D,A)
                            & ~ r1_xreal_0(1,k3_finseq_1(B)) )
                          | k2_finsop_1(A,B,D) = k2_finsop_1(A,C,D) ) ) ) ) ) ) ) ),
    inference(mizar_proof,[status(thm)],[l16_finsop_1,t39_nat_1,t48_finseq_2,t22_funct_1,l15_finsop_1]),
    [file(finsop_1,t8_finsop_1),interesting(0.65)]).

fof(l10_finsop_1,theorem,(
    ! [A] : 
      ( ~ v1_xboole_0(A)
     => ! [B] : 
          ( m1_subset_1(B,A)
         => ! [C] : 
              ( m2_finseq_1(C,A)
             => ! [D] : 
                  ( ( v1_funct_1(D)
                    & v1_funct_2(D,k2_zfmisc_1(A,A),A)
                    & m2_relset_1(D,k2_zfmisc_1(A,A),A) )
                 => ( r1_xreal_0(1,k3_finseq_1(C))
                   => k2_finsop_1(A,k8_finseq_1(A,C,k12_finseq_1(A,B)),D) = k2_binop_1(A,A,A,D,k2_finsop_1(A,C,D),B) ) ) ) ) ) ),
    inference(mizar_proof,[status(thm)],[t2_finsop_1,t35_finseq_1,t56_finseq_1,t37_nat_1,t2_finsop_1,t31_xreal_1,t59_finseq_1,t39_nat_1,t27_finseq_3,d7_finseq_1,t37_nat_1,t38_nat_1,t38_nat_1,t37_nat_1,t27_finseq_3,d7_finseq_1,d5_real_1,s1_nat_1]),
    [file(finsop_1,l10_finsop_1),interesting(0.63)]).

fof(t6_finsop_1,theorem,(
    ! [A] : 
      ( ~ v1_xboole_0(A)
     => ! [B] : 
          ( m2_finseq_1(B,A)
         => ! [C] : 
              ( m2_finseq_1(C,A)
             => ! [D] : 
                  ( ( v1_funct_1(D)
                    & v1_funct_2(D,k2_zfmisc_1(A,A),A)
                    & m2_relset_1(D,k2_zfmisc_1(A,A),A) )
                 => ( v2_binop_1(D,A)
                   => ( ( ~ v1_setwiseo(D,A)
                        & ~ ( r1_xreal_0(1,k3_finseq_1(B))
                            & r1_xreal_0(1,k3_finseq_1(C)) ) )
                      | k2_finsop_1(A,k8_finseq_1(A,B,C),D) = k2_binop_1(A,A,A,D,k2_finsop_1(A,B,D),k2_finsop_1(A,C,D)) ) ) ) ) ) ) ),
    inference(mizar_proof,[status(thm)],[t32_finseq_1,t47_finseq_1,t23_setwiseo,l8_finsop_1,t35_finseq_1,t37_nat_1,t2_xreal_1,t45_finseq_1,t5_finsop_1,t39_nat_1,d3_binop_1,t5_finsop_1,t25_finseq_1,t47_finseq_1,t5_finsop_1,l9_finsop_1,t47_finseq_1,s2_finseq_2]),
    [file(finsop_1,t6_finsop_1),interesting(0.63)]).

fof(t21_finsop_1,theorem,(
    ! [A] : 
      ( ~ v1_xboole_0(A)
     => ! [B] : 
          ( m2_finseq_1(B,A)
         => ! [C] : 
              ( ( v1_funct_1(C)
                & v1_funct_2(C,k2_zfmisc_1(A,A),A)
                & m2_relset_1(C,k2_zfmisc_1(A,A),A) )
             => ( k3_finseq_1(B) = 1
               => k2_finsop_1(A,B,C) = k1_funct_1(B,1) ) ) ) ) ),
    inference(mizar_proof,[status(thm)],[l21_finsop_1]),
    [file(finsop_1,t21_finsop_1),interesting(0.63)]).

fof(t7_finsop_1,theorem,(
    ! [A] : 
      ( ~ v1_xboole_0(A)
     => ! [B] : 
          ( m1_subset_1(B,A)
         => ! [C] : 
              ( m2_finseq_1(C,A)
             => ! [D] : 
                  ( ( v1_funct_1(D)
                    & v1_funct_2(D,k2_zfmisc_1(A,A),A)
                    & m2_relset_1(D,k2_zfmisc_1(A,A),A) )
                 => ( v2_binop_1(D,A)
                   => ( ( ~ v1_setwiseo(D,A)
                        & ~ r1_xreal_0(1,k3_finseq_1(C)) )
                      | k2_finsop_1(A,k8_finseq_1(A,k12_finseq_1(A,B),C),D) = k2_binop_1(A,A,A,D,B,k2_finsop_1(A,C,D)) ) ) ) ) ) ) ),
    inference(mizar_proof,[status(thm)],[t56_finseq_1,t6_finsop_1,l9_finsop_1]),
    [file(finsop_1,t7_finsop_1),interesting(0.63)]).

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

fof(t22_finsop_1,theorem,(
    ! [A] : 
      ( ~ v1_xboole_0(A)
     => ! [B] : 
          ( m2_finseq_1(B,A)
         => ! [C] : 
              ( ( v1_funct_1(C)
                & v1_funct_2(C,k2_zfmisc_1(A,A),A)
                & m2_relset_1(C,k2_zfmisc_1(A,A),A) )
             => ( k3_finseq_1(B) = 2
               => k2_finsop_1(A,B,C) = k1_binop_1(C,k1_funct_1(B,1),k1_funct_1(B,2)) ) ) ) ) ),
    inference(mizar_proof,[status(thm)],[t61_finseq_1,t24_finseq_4,t24_finseq_4,t13_finsop_1,t24_finseq_4,t24_finseq_4]),
    [file(finsop_1,t22_finsop_1),interesting(0.61)]).

fof(l15_finsop_1,theorem,(
    ! [A] : 
      ( ~ v1_xboole_0(A)
     => ! [B] : 
          ( m2_finseq_1(B,A)
         => ! [C] : 
              ( m2_finseq_1(C,A)
             => ! [D] : 
                  ( ( v1_funct_1(D)
                    & v1_funct_2(D,k2_zfmisc_1(A,A),A)
                    & m2_relset_1(D,k2_zfmisc_1(A,A),A) )
                 => ( ( v2_binop_1(D,A)
                      & v1_binop_1(D,A) )
                   => ! [E] : 
                        ( ( v1_funct_1(E)
                          & v1_funct_2(E,k5_finsop_1(B),k5_finsop_1(B))
                          & v3_funct_2(E,k5_finsop_1(B),k5_finsop_1(B))
                          & m2_relset_1(E,k5_finsop_1(B),k5_finsop_1(B)) )
                       => ( ( r1_xreal_0(1,k3_finseq_1(B))
                            & k3_finseq_1(B) = k3_finseq_1(C)
                            & ! [F] : 
                                ( m2_subset_1(F,k1_numbers,k5_numbers)
                               => ( r2_hidden(F,k5_finsop_1(C))
                                 => k1_funct_1(C,F) = k1_funct_1(B,k1_funct_1(E,F)) ) ) )
                         => k2_finsop_1(A,B,D) = k2_finsop_1(A,C,D) ) ) ) ) ) ) ) ),
    inference(mizar_proof,[status(thm)],[t23_finseq_1,t6_finseq_1,d3_finseq_1,d1_funct_2,d3_funct_2,d5_funct_1,d4_finseq_1,d5_funct_1,t3_finseq_1,t28_nat_1,t3_finseq_1,t28_nat_1,t23_finseq_1,s1_finseq_1,d3_tarski,d5_funct_1,t14_setwiseo,t3_finseq_1,t37_nat_1,t2_xreal_1,t3_finseq_1,t9_xreal_1,t3_finseq_1,d3_finseq_1,d4_finseq_1,d5_funct_1,d4_finseq_1,t37_nat_1,t21_finseq_1,t29_nat_1,t2_xreal_1,t21_finseq_1,d3_finseq_1,t35_finseq_1,t35_finseq_1,t57_finseq_1,d3_finseq_1,t35_finseq_1,t57_finseq_1,d3_finseq_1,t11_finseq_1,t21_finseq_1,t70_funct_1,d7_finseq_1,d1_tarski,t3_finseq_1,t56_finseq_1,d3_finseq_1,d7_finseq_1,t57_finseq_1,d2_xboole_0,t35_finseq_1,t56_finseq_1,d7_finseq_1,t29_nat_1,t7_finseq_1,d5_funct_1,t21_finseq_1,t21_finseq_1,d3_finseq_1,d5_funct_1,d5_funct_1,s1_finseq_1,d5_funct_1,t3_finseq_1,t3_finseq_1,t38_nat_1,d8_funct_1,t3_finseq_1,t8_xreal_1,d5_real_1,t38_nat_1,d3_tarski,d5_funct_1,t14_setwiseo,t7_finseq_1,t3_finseq_1,d5_funct_1,t39_nat_1,t3_finseq_1,t60_nat_1,t11_xreal_1,t37_nat_1,t2_xreal_1,t3_finseq_1,t11_xreal_1,t3_finseq_1,d1_funct_2,t11_relset_1,d10_xboole_0,d3_tarski,d5_funct_1,t14_setwiseo,d5_funct_1,t3_finseq_1,t37_nat_1,t9_xreal_1,t3_finseq_1,d5_funct_1,d4_xboole_0,t16_finseq_3,d1_tarski,t3_finseq_1,t3_finseq_1,t3_finseq_1,t3_finseq_1,t38_nat_1,t3_finseq_1,d5_funct_1,d4_xboole_0,t16_finseq_3,d1_tarski,t3_finseq_1,t37_nat_1,t9_xreal_1,t3_finseq_1,d5_funct_1,d4_xboole_0,t16_finseq_3,d1_tarski,t31_xreal_1,t38_nat_1,t3_finseq_1,d5_funct_1,d8_funct_1,d5_funct_1,d8_funct_1,t3_finseq_1,t8_xreal_1,t3_finseq_1,t21_finseq_1,d4_xboole_0,t16_finseq_3,d1_tarski,d8_funct_1,t9_finseq_3,t3_finseq_1,t8_xreal_1,t3_finseq_1,t21_finseq_1,d4_xboole_0,t16_finseq_3,d1_tarski,d8_funct_1,t9_finseq_3,t2_xcmplx_1,d8_funct_1,t83_funct_2,d5_funct_1,d7_finseq_1,t70_funct_1,t70_funct_1,d5_funct_1,t11_xreal_1,t31_xreal_1,t2_xreal_1,t148_xreal_1,t2_xreal_1,t60_nat_1,t3_finseq_1,t38_finseq_1,t45_finseq_1,d5_funct_1,t38_finseq_1,d7_finseq_1,t56_finseq_1,d7_finseq_1,t39_nat_1,t61_finseq_3,t5_finsop_1,t39_nat_1,t35_finseq_1,t57_finseq_1,t37_nat_1,t6_finsop_1,d3_binop_1,d2_binop_1,t7_finsop_1,t6_finsop_1,t45_finseq_1,t25_finseq_1,t47_finseq_1,t47_finseq_1,d2_binop_1,t7_finsop_1,t25_finseq_1,t47_finseq_1,t47_finseq_1,t5_finsop_1,t35_finseq_1,t21_finseq_1,t4_finseq_1,d3_finseq_1,d1_funct_2,d3_funct_2,d1_tarski,d5_funct_1,d1_tarski,l9_finsop_1,t57_finseq_1,s1_nat_1]),
    [file(finsop_1,l15_finsop_1),interesting(0.52)]).

fof(t19_finsop_1,theorem,(
    ! [A] : 
      ( ~ v1_xboole_0(A)
     => ! [B] : 
          ( m1_subset_1(B,A)
         => ! [C] : 
              ( ( v1_funct_1(C)
                & v1_funct_2(C,k2_zfmisc_1(A,A),A)
                & m2_relset_1(C,k2_zfmisc_1(A,A),A) )
             => ! [D] : 
                  ( m2_subset_1(D,k1_numbers,k5_numbers)
                 => ! [E] : 
                      ( m2_subset_1(E,k1_numbers,k5_numbers)
                     => ( v2_binop_1(C,A)
                       => ( ( ~ v1_setwiseo(C,A)
                            & ~ ( D != 0
                                & E != 0 ) )
                          | k2_finsop_1(A,k1_finsop_1(A,k1_nat_1(D,E),B),C) = k2_binop_1(A,A,A,C,k2_finsop_1(A,k1_finsop_1(A,D,B),C),k2_finsop_1(A,k1_finsop_1(A,E,B),C)) ) ) ) ) ) ) ) ),
    inference(mizar_proof,[status(thm)],[t69_finseq_2,t39_nat_1,t143_finseq_2,t6_finsop_1]),
    [file(finsop_1,t19_finsop_1),interesting(0.51)]).

fof(t20_finsop_1,theorem,(
    ! [A] : 
      ( ~ v1_xboole_0(A)
     => ! [B] : 
          ( m1_subset_1(B,A)
         => ! [C] : 
              ( ( v1_funct_1(C)
                & v1_funct_2(C,k2_zfmisc_1(A,A),A)
                & m2_relset_1(C,k2_zfmisc_1(A,A),A) )
             => ! [D] : 
                  ( m2_subset_1(D,k1_numbers,k5_numbers)
                 => ! [E] : 
                      ( m2_subset_1(E,k1_numbers,k5_numbers)
                     => ( v2_binop_1(C,A)
                       => ( ( ~ v1_setwiseo(C,A)
                            & ~ ( D != 0
                                & E != 0 ) )
                          | k2_finsop_1(A,k1_finsop_1(A,k2_nat_1(D,E),B),C) = k2_finsop_1(A,k1_finsop_1(A,E,k2_finsop_1(A,k1_finsop_1(A,D,B),C)),C) ) ) ) ) ) ) ) ),
    inference(mizar_proof,[status(thm)],[t72_finseq_2,t72_finseq_2,t17_finsop_1,t6_xcmplx_1,t19_finsop_1,t17_finsop_1,t19_finsop_1,s1_nat_1]),
    [file(finsop_1,t20_finsop_1),interesting(0.48)]).

fof(l5_finsop_1,theorem,(
    ! [A] : 
      ( ~ v1_xboole_0(A)
     => ! [B] : 
          ( m2_finseq_1(B,A)
         => ! [C] : 
              ( ( v1_funct_1(C)
                & v1_funct_2(C,k2_zfmisc_1(A,A),A)
                & m2_relset_1(C,k2_zfmisc_1(A,A),A) )
             => ( ( r1_xreal_0(1,k3_finseq_1(B))
                  & v2_binop_1(C,A)
                  & v1_binop_1(C,A) )
               => k2_finsop_1(A,B,C) = k7_setwiseo(k5_numbers,A,C,k5_finsop_1(B),k4_finsop_1(A,k3_finsop_1(A,k5_numbers,k3_binop_1(A,C)),B)) ) ) ) ) ),
    inference(mizar_proof,[status(thm)],[t2_finsop_1,d3_finseq_1,t5_finseq_1,d3_setwiseo,t3_finseq_1,t14_funct_4,t4_finseq_1,t38_nat_1,t5_finseq_1,t7_finseq_1,t37_nat_1,t27_finseq_3,d5_finsub_1,t11_finseq_3,d4_xboole_0,t11_finseq_1,t14_funct_4,t38_nat_1,s1_nat_1]),
    [file(finsop_1,l5_finsop_1),interesting(0.42)]).

fof(l22_finsop_1,theorem,(
    ! [A] : 
      ( ~ v1_xboole_0(A)
     => ! [B] : 
          ( m2_finseq_1(B,A)
         => ! [C] : 
              ( m2_finseq_1(C,A)
             => ! [D] : 
                  ( m2_finseq_1(D,A)
                 => ! [E] : 
                      ( ( v1_funct_1(E)
                        & v1_funct_2(E,k2_zfmisc_1(A,A),A)
                        & m2_relset_1(E,k2_zfmisc_1(A,A),A) )
                     => ( ( v2_binop_1(E,A)
                          & v1_binop_1(E,A)
                          & r1_xreal_0(1,k3_finseq_1(B))
                          & k3_finseq_1(B) = k3_finseq_1(C)
                          & k3_finseq_1(B) = k3_finseq_1(D)
                          & ! [F] : 
                              ( m2_subset_1(F,k1_numbers,k5_numbers)
                             => ( r2_hidden(F,k5_finsop_1(B))
                               => k1_funct_1(D,F) = k1_binop_1(E,k1_funct_1(B,F),k1_funct_1(C,F)) ) ) )
                       => k2_finsop_1(A,D,E) = k2_binop_1(A,A,A,E,k2_finsop_1(A,B,E),k2_finsop_1(A,C,E)) ) ) ) ) ) ) ),
    inference(mizar_proof,[status(thm)],[t23_finseq_1,t59_finseq_3,d3_finseq_1,d3_finseq_1,t70_funct_1,t37_nat_1,t7_finseq_1,d3_finseq_1,d3_finseq_1,t6_finseq_1,d3_finseq_1,d4_finseq_1,d5_funct_1,t61_finseq_3,l9_finsop_1,t5_finsop_1,t5_finsop_1,d3_binop_1,d3_binop_1,d2_binop_1,d3_binop_1,d3_binop_1,l21_finsop_1,t27_finseq_3,t39_nat_1,s1_nat_1]),
    [file(finsop_1,l22_finsop_1),interesting(0.27)]).

fof(t4_finsop_1,theorem,(
    ! [A] : 
      ( ~ v1_xboole_0(A)
     => ! [B] : 
          ( m2_finseq_1(B,A)
         => ! [C] : 
              ( ( v1_funct_1(C)
                & v1_funct_2(C,k2_zfmisc_1(A,A),A)
                & m2_relset_1(C,k2_zfmisc_1(A,A),A) )
             => ( ( v2_binop_1(C,A)
                  & v1_binop_1(C,A) )
               => ( ( ~ v1_setwiseo(C,A)
                    & ~ r1_xreal_0(1,k3_finseq_1(B)) )
                  | k2_finsop_1(A,B,C) = k7_setwiseo(k5_numbers,A,C,k5_finsop_1(B),k4_finsop_1(A,k3_finsop_1(A,k5_numbers,k3_binop_1(A,C)),B)) ) ) ) ) ) ),
    inference(mizar_proof,[status(thm)],[t39_nat_1,l5_finsop_1,l6_finsop_1]),
    [file(finsop_1,t4_finsop_1),interesting(0.21)]).

fof(t2_finsop_1,theorem,(
    ! [A] : 
      ( ~ v1_xboole_0(A)
     => ! [B] : 
          ( m2_finseq_1(B,A)
         => ! [C] : 
              ( ( v1_funct_1(C)
                & v1_funct_2(C,k2_zfmisc_1(A,A),A)
                & m2_relset_1(C,k2_zfmisc_1(A,A),A) )
             => ~ ( r1_xreal_0(1,k3_finseq_1(B))
                  & ! [D] : 
                      ( ( v1_funct_1(D)
                        & v1_funct_2(D,k5_numbers,A)
                        & m2_relset_1(D,k5_numbers,A) )
                     => ~ ( k8_funct_2(k5_numbers,A,D,1) = k1_funct_1(B,1)
                          & ! [E] : 
                              ( m2_subset_1(E,k1_numbers,k5_numbers)
                             => ~ ( 0 != E
                                  & ~ r1_xreal_0(k3_finseq_1(B),E)
                                  & k8_funct_2(k5_numbers,A,D,k1_nat_1(E,1)) != k1_binop_1(C,k8_funct_2(k5_numbers,A,D,E),k1_funct_1(B,k1_nat_1(E,1))) ) )
                          & k2_finsop_1(A,B,C) = k8_funct_2(k5_numbers,A,D,k3_finseq_1(B)) ) ) ) ) ) ) ),
    inference(mizar_proof,[status(thm)],[d1_finsop_1]),
    [file(finsop_1,t2_finsop_1),interesting(0.13)]).

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(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(t23_finseq_1,theorem,(
    ! [A] : 
      ( v4_ordinal2(A)
     => ! [B,C] : 
          ( m2_finseq_1(C,B)
         => m2_finseq_1(k7_relat_1(C,k2_finseq_1(A)),B) ) ) ),
    file(finseq_1,t23_finseq_1),
    [interesting(0.00)]).

fof(t59_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)
             => ! [D] : 
                  ( v4_ordinal2(D)
                 => ( ( k3_finseq_1(A) = k2_xcmplx_0(C,D)
                      & B = k7_relat_1(A,k2_finseq_1(C)) )
                   => k3_finseq_1(B) = C ) ) ) ) ) ),
    file(finseq_3,t59_finseq_3),
    [interesting(0.00)]).

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

fof(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(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(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(d4_finseq_1,definition,(
    ! [A,B] : 
      ( ( v1_relat_1(B)
        & v1_funct_1(B)
        & v1_finseq_1(B) )
     => ( m1_finseq_1(B,A)
      <=> r1_tarski(k2_relat_1(B),A) ) ) ),
    file(finseq_1,d4_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(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(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(d1_finsop_1,definition,(
    ! [A] : 
      ( ~ v1_xboole_0(A)
     => ! [B] : 
          ( m2_finseq_1(B,A)
         => ! [C] : 
              ( ( v1_funct_1(C)
                & v1_funct_2(C,k2_zfmisc_1(A,A),A)
                & m2_relset_1(C,k2_zfmisc_1(A,A),A) )
             => ( ( v1_setwiseo(C,A)
                  | r1_xreal_0(1,k3_finseq_1(B)) )
               => ! [D] : 
                    ( m1_subset_1(D,A)
                   => ( ( ( v1_setwiseo(C,A)
                          & k3_finseq_1(B) = 0 )
                       => ( D = k2_finsop_1(A,B,C)
                        <=> D = k3_binop_1(A,C) ) )
                      & ( ~ ( v1_setwiseo(C,A)
                            & k3_finseq_1(B) = 0 )
                       => ( D = k2_finsop_1(A,B,C)
                        <=> ? [E] : 
                              ( v1_funct_1(E)
                              & v1_funct_2(E,k5_numbers,A)
                              & m2_relset_1(E,k5_numbers,A)
                              & k8_funct_2(k5_numbers,A,E,1) = k1_funct_1(B,1)
                              & ! [F] : 
                                  ( m2_subset_1(F,k1_numbers,k5_numbers)
                                 => ~ ( 0 != F
                                      & ~ r1_xreal_0(k3_finseq_1(B),F)
                                      & k8_funct_2(k5_numbers,A,E,k1_nat_1(F,1)) != k1_binop_1(C,k8_funct_2(k5_numbers,A,E,F),k1_funct_1(B,k1_nat_1(F,1))) ) )
                              & D = k8_funct_2(k5_numbers,A,E,k3_finseq_1(B)) ) ) ) ) ) ) ) ) ) ),
    file(finsop_1,d1_finsop_1),
    [interesting(0.00)]).

fof(d8_finseq_1,definition,(
    ! [A,B] : 
      ( ( v1_relat_1(B)
        & v1_funct_1(B) )
     => ( B = k9_finseq_1(A)
      <=> ( k1_relat_1(B) = k2_finseq_1(1)
          & k1_funct_1(B,1) = A ) ) ) ),
    file(finseq_1,d8_finseq_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(t31_xreal_1,theorem,(
    ! [A] : 
      ( v1_xreal_0(A)
     => ! [B] : 
          ( v1_xreal_0(B)
         => ~ ( ~ r1_xreal_0(A,0)
              & r1_xreal_0(k2_xcmplx_0(B,A),B) ) ) ) ),
    file(xreal_1,t31_xreal_1),
    [interesting(0.00)]).

fof(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(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(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(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(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(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(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(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(t23_setwiseo,theorem,(
    ! [A] : 
      ( ~ v1_xboole_0(A)
     => ! [B] : 
          ( ( v1_funct_1(B)
            & v1_funct_2(B,k2_zfmisc_1(A,A),A)
            & m2_relset_1(B,k2_zfmisc_1(A,A),A) )
         => ( v1_setwiseo(B,A)
           => ! [C] : 
                ( m1_subset_1(C,A)
               => ( k2_binop_1(A,A,A,B,k3_binop_1(A,B),C) = C
                  & k2_binop_1(A,A,A,B,C,k3_binop_1(A,B)) = C ) ) ) ) ) ),
    file(setwiseo,t23_setwiseo),
    [interesting(0.00)]).

fof(l11_finsop_1,theorem,(
    ! [A] : 
      ( ~ v1_xboole_0(A)
     => ! [B] : 
          ( m1_subset_1(B,A)
         => ! [C] : 
              ( m2_finseq_1(C,A)
             => ! [D] : 
                  ( ( v1_funct_1(D)
                    & v1_funct_2(D,k2_zfmisc_1(A,A),A)
                    & m2_relset_1(D,k2_zfmisc_1(A,A),A) )
                 => ( ( v1_setwiseo(D,A)
                      & k3_finseq_1(C) = 0 )
                   => k2_finsop_1(A,k8_finseq_1(A,C,k12_finseq_1(A,B)),D) = k2_binop_1(A,A,A,D,k2_finsop_1(A,C,D),B) ) ) ) ) ) ),
    inference(mizar_proof,[status(thm)],[t32_finseq_1,t47_finseq_1,l9_finsop_1,t23_setwiseo,d1_finsop_1]),
    [file(finsop_1,l11_finsop_1),interesting(0.00)]).

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

fof(d2_binop_1,definition,(
    ! [A,B] : 
      ( ( v1_funct_1(B)
        & v1_funct_2(B,k2_zfmisc_1(A,A),A)
        & m2_relset_1(B,k2_zfmisc_1(A,A),A) )
     => ( v1_binop_1(B,A)
      <=> ! [C] : 
            ( m1_subset_1(C,A)
           => ! [D] : 
                ( m1_subset_1(D,A)
               => k1_binop_1(B,C,D) = k1_binop_1(B,D,C) ) ) ) ) ),
    file(binop_1,d2_binop_1),
    [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(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(l23_finsop_1,theorem,(
    ! [A] : 
      ( ~ v1_xboole_0(A)
     => ! [B] : 
          ( m2_finseq_1(B,A)
         => ! [C] : 
              ( m2_finseq_1(C,A)
             => ! [D] : 
                  ( m2_finseq_1(D,A)
                 => ! [E] : 
                      ( ( v1_funct_1(E)
                        & v1_funct_2(E,k2_zfmisc_1(A,A),A)
                        & m2_relset_1(E,k2_zfmisc_1(A,A),A) )
                     => ( ( v1_setwiseo(E,A)
                          & k3_finseq_1(B) = 0
                          & k3_finseq_1(B) = k3_finseq_1(C)
                          & k3_finseq_1(B) = k3_finseq_1(D) )
                       => k2_finsop_1(A,B,E) = k2_binop_1(A,A,A,E,k2_finsop_1(A,C,E),k2_finsop_1(A,D,E)) ) ) ) ) ) ) ),
    inference(mizar_proof,[status(thm)],[d1_finsop_1,t23_setwiseo,d1_finsop_1,d1_finsop_1]),
    [file(finsop_1,l23_finsop_1),interesting(0.00)]).

fof(t10_finsop_1,theorem,(
    ! [A] : 
      ( ~ v1_xboole_0(A)
     => ! [B] : 
          ( m2_finseq_1(B,A)
         => ! [C] : 
              ( m2_finseq_1(C,A)
             => ! [D] : 
                  ( m2_finseq_1(D,A)
                 => ! [E] : 
                      ( ( v1_funct_1(E)
                        & v1_funct_2(E,k2_zfmisc_1(A,A),A)
                        & m2_relset_1(E,k2_zfmisc_1(A,A),A) )
                     => ( ( v2_binop_1(E,A)
                          & v1_binop_1(E,A)
                          & k3_finseq_1(B) = k3_finseq_1(C)
                          & k3_finseq_1(B) = k3_finseq_1(D)
                          & ! [F] : 
                              ( m2_subset_1(F,k1_numbers,k5_numbers)
                             => ( r2_hidden(F,k5_finsop_1(B))
                               => k1_funct_1(B,F) = k1_binop_1(E,k1_funct_1(C,F),k1_funct_1(D,F)) ) ) )
                       => ( ( ~ v1_setwiseo(E,A)
                            & ~ r1_xreal_0(1,k3_finseq_1(B)) )
                          | k2_finsop_1(A,B,E) = k2_binop_1(A,A,A,E,k2_finsop_1(A,C,E),k2_finsop_1(A,D,E)) ) ) ) ) ) ) ) ),
    inference(mizar_proof,[status(thm)],[d3_finseq_1,t39_nat_1,l22_finsop_1,l23_finsop_1]),
    [file(finsop_1,t10_finsop_1),interesting(0.00)]).

fof(d9_finseq_1,definition,(
    ! [A,B] : k10_finseq_1(A,B) = k7_finseq_1(k9_finseq_1(A),k9_finseq_1(B)) ),
    file(finseq_1,d9_finseq_1),
    [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(t60_finseq_1,theorem,(
    ! [A,B,C] : 
      ( k11_finseq_1(A,B,C) = k7_finseq_1(k9_finseq_1(A),k10_finseq_1(B,C))
      & k11_finseq_1(A,B,C) = k7_finseq_1(k10_finseq_1(A,B),k9_finseq_1(C)) ) ),
    file(finseq_1,t60_finseq_1),
    [interesting(0.00)]).

fof(t16_finsop_1,theorem,(
    ! [A] : 
      ( ~ v1_xboole_0(A)
     => ! [B] : 
          ( m1_subset_1(B,A)
         => ! [C] : 
              ( m1_subset_1(C,A)
             => ! [D] : 
                  ( m1_subset_1(D,A)
                 => ! [E] : 
                      ( ( v1_funct_1(E)
                        & v1_funct_2(E,k2_zfmisc_1(A,A),A)
                        & m2_relset_1(E,k2_zfmisc_1(A,A),A) )
                     => ( v1_binop_1(E,A)
                       => k2_finsop_1(A,k3_finseq_4(A,B,C,D),E) = k2_finsop_1(A,k3_finseq_4(A,C,B,D),E) ) ) ) ) ) ) ),
    inference(mizar_proof,[status(thm)],[t15_finsop_1,d2_binop_1,t15_finsop_1]),
    [file(finsop_1,t16_finsop_1),interesting(0.00)]).

fof(t75_finseq_2,theorem,(
    ! [A] : k2_finseq_2(2,A) = k10_finseq_1(A,A) ),
    file(finseq_2,t75_finseq_2),
    [interesting(0.00)]).

fof(t1_finsop_1,theorem,(
    $true ),
    file(finsop_1,t1_finsop_1),
    [interesting(0.00)]).

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

fof(t73_finseq_2,theorem,(
    ! [A] : k2_finseq_2(1,A) = k9_finseq_1(A) ),
    file(finseq_2,t73_finseq_2),
    [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(t69_finseq_2,theorem,(
    ! [A] : 
      ( v4_ordinal2(A)
     => ! [B] : k3_finseq_1(k2_finseq_2(A,B)) = A ) ),
    file(finseq_2,t69_finseq_2),
    [interesting(0.00)]).

fof(t143_finseq_2,theorem,(
    ! [A] : 
      ( m2_subset_1(A,k1_numbers,k5_numbers)
     => ! [B] : 
          ( m2_subset_1(B,k1_numbers,k5_numbers)
         => ! [C] : k2_finseq_2(k1_nat_1(A,B),C) = k7_finseq_1(k2_finseq_2(A,C),k2_finseq_2(B,C)) ) ) ),
    file(finseq_2,t143_finseq_2),
    [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(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(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(s2_finseq_2,theorem,
    ( ( p1_s2_finseq_2(k6_finseq_1(f1_s2_finseq_2))
      & ! [A] : 
          ( m2_finseq_1(A,f1_s2_finseq_2)
         => ! [B] : 
              ( m1_subset_1(B,f1_s2_finseq_2)
             => ( p1_s2_finseq_2(A)
               => p1_s2_finseq_2(k8_finseq_1(f1_s2_finseq_2,A,k12_finseq_1(f1_s2_finseq_2,B))) ) ) ) )
   => ! [A] : 
        ( m2_finseq_1(A,f1_s2_finseq_2)
       => p1_s2_finseq_2(A) ) ),
    file(finseq_2,s2_finseq_2),
    [interesting(0.00)]).

fof(t3_finsop_1,theorem,(
    ! [A] : 
      ( ~ v1_xboole_0(A)
     => ! [B] : 
          ( m1_subset_1(B,A)
         => ! [C] : 
              ( m2_finseq_1(C,A)
             => ! [D] : 
                  ( ( v1_funct_1(D)
                    & v1_funct_2(D,k2_zfmisc_1(A,A),A)
                    & m2_relset_1(D,k2_zfmisc_1(A,A),A) )
                 => ( r1_xreal_0(1,k3_finseq_1(C))
                   => ( ! [E] : 
                          ( ( v1_funct_1(E)
                            & v1_funct_2(E,k5_numbers,A)
                            & m2_relset_1(E,k5_numbers,A) )
                         => ~ ( k8_funct_2(k5_numbers,A,E,1) = k1_funct_1(C,1)
                              & ! [F] : 
                                  ( m2_subset_1(F,k1_numbers,k5_numbers)
                                 => ~ ( 0 != F
                                      & ~ r1_xreal_0(k3_finseq_1(C),F)
                                      & k8_funct_2(k5_numbers,A,E,k1_nat_1(F,1)) != k1_binop_1(D,k8_funct_2(k5_numbers,A,E,F),k1_funct_1(C,k1_nat_1(F,1))) ) )
                              & B = k8_funct_2(k5_numbers,A,E,k3_finseq_1(C)) ) )
                      | B = k2_finsop_1(A,C,D) ) ) ) ) ) ) ),
    inference(mizar_proof,[status(thm)],[d1_finsop_1]),
    [file(finsop_1,t3_finsop_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(d3_setwiseo,definition,(
    ! [A] : 
      ( ~ v1_xboole_0(A)
     => ! [B] : 
          ( ~ v1_xboole_0(B)
         => ! [C] : 
              ( ( v1_funct_1(C)
                & v1_funct_2(C,k2_zfmisc_1(B,B),B)
                & m2_relset_1(C,k2_zfmisc_1(B,B),B) )
             => ! [D] : 
                  ( m1_subset_1(D,k5_finsub_1(A))
                 => ! [E] : 
                      ( ( v1_funct_1(E)
                        & v1_funct_2(E,A,B)
                        & m2_relset_1(E,A,B) )
                     => ( ( v1_binop_1(C,B)
                          & v2_binop_1(C,B) )
                       => ( ( D = k1_xboole_0
                            & ~ v1_setwiseo(C,B) )
                          | ! [F] : 
                              ( m1_subset_1(F,B)
                             => ( F = k7_setwiseo(A,B,C,D,E)
                              <=> ? [G] : 
                                    ( v1_funct_1(G)
                                    & v1_funct_2(G,k5_finsub_1(A),B)
                                    & m2_relset_1(G,k5_finsub_1(A),B)
                                    & F = k8_funct_2(k5_finsub_1(A),B,G,D)
                                    & ! [H] : 
                                        ( m1_subset_1(H,B)
                                       => ( r3_binop_1(B,H,C)
                                         => k1_funct_1(G,k1_xboole_0) = H ) )
                                    & ! [H] : 
                                        ( m1_subset_1(H,A)
                                       => k8_funct_2(k5_finsub_1(A),B,G,k2_setwiseo(A,H)) = k8_funct_2(A,B,E,H) )
                                    & ! [H] : 
                                        ( m1_subset_1(H,k5_finsub_1(A))
                                       => ( r1_tarski(H,D)
                                         => ( H = k1_xboole_0
                                            | ! [I] : 
                                                ( m1_subset_1(I,A)
                                               => ( r2_hidden(I,k6_setwiseo(A,D,H))
                                                 => k8_funct_2(k5_finsub_1(A),B,G,k5_setwiseo(A,H,k2_setwiseo(A,I))) = k2_binop_1(B,B,B,C,k8_funct_2(k5_finsub_1(A),B,G,H),k8_funct_2(A,B,E,I)) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ),
    file(setwiseo,d3_setwiseo),
    [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(t14_funct_4,theorem,(
    ! [A,B] : 
      ( ( v1_relat_1(B)
        & v1_funct_1(B) )
     => ! [C] : 
          ( ( v1_relat_1(C)
            & v1_funct_1(C) )
         => ( r2_hidden(A,k1_relat_1(B))
           => k1_funct_1(k1_funct_4(C,B),A) = k1_funct_1(B,A) ) ) ) ),
    file(funct_4,t14_funct_4),
    [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(d5_finsub_1,definition,(
    ! [A,B] : 
      ( v4_finsub_1(B)
     => ( B = k5_finsub_1(A)
      <=> ! [C] : 
            ( r2_hidden(C,B)
          <=> ( r1_tarski(C,A)
              & v1_finset_1(C) ) ) ) ) ),
    file(finsub_1,d5_finsub_1),
    [interesting(0.00)]).

fof(t11_finseq_3,theorem,(
    ! [A] : 
      ( v4_ordinal2(A)
     => ! [B] : 
          ( v4_ordinal2(B)
         => ( r2_hidden(k2_xcmplx_0(A,B),k2_finseq_1(A))
           => B = 0 ) ) ) ),
    file(finseq_3,t11_finseq_3),
    [interesting(0.00)]).

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

fof(t11_finseq_1,theorem,(
    ! [A] : 
      ( v4_ordinal2(A)
     => k2_xboole_0(k2_finseq_1(A),k1_tarski(k2_xcmplx_0(A,1))) = k2_finseq_1(k2_xcmplx_0(A,1)) ) ),
    file(finseq_1,t11_finseq_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(t40_setwiseo,theorem,(
    ! [A] : 
      ( ~ v1_xboole_0(A)
     => ! [B] : 
          ( ~ v1_xboole_0(B)
         => ! [C] : 
              ( ( v1_funct_1(C)
                & v1_funct_2(C,k2_zfmisc_1(A,A),A)
                & m2_relset_1(C,k2_zfmisc_1(A,A),A) )
             => ( ( v1_binop_1(C,A)
                  & v2_binop_1(C,A)
                  & v1_setwiseo(C,A) )
               => ! [D] : 
                    ( ( v1_funct_1(D)
                      & v1_funct_2(D,B,A)
                      & m2_relset_1(D,B,A) )
                   => k7_setwiseo(B,A,C,k1_setwiseo(B),D) = k3_binop_1(A,C) ) ) ) ) ) ),
    file(setwiseo,t40_setwiseo),
    [interesting(0.00)]).

fof(l6_finsop_1,theorem,(
    ! [A] : 
      ( ~ v1_xboole_0(A)
     => ! [B] : 
          ( m2_finseq_1(B,A)
         => ! [C] : 
              ( ( v1_funct_1(C)
                & v1_funct_2(C,k2_zfmisc_1(A,A),A)
                & m2_relset_1(C,k2_zfmisc_1(A,A),A) )
             => ( ( k3_finseq_1(B) = 0
                  & v1_setwiseo(C,A)
                  & v2_binop_1(C,A)
                  & v1_binop_1(C,A) )
               => k2_finsop_1(A,B,C) = k7_setwiseo(k5_numbers,A,C,k5_finsop_1(B),k4_finsop_1(A,k3_finsop_1(A,k5_numbers,k3_binop_1(A,C)),B)) ) ) ) ) ),
    inference(mizar_proof,[status(thm)],[t25_finseq_1,t26_finseq_1,d1_finsop_1,t40_setwiseo]),
    [file(finsop_1,l6_finsop_1),interesting(0.00)]).

fof(t65_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(A) = k2_relat_1(B)
              & v2_funct_1(A)
              & v2_funct_1(B) )
           => k3_finseq_1(A) = k3_finseq_1(B) ) ) ) ),
    file(finseq_1,t65_finseq_1),
    [interesting(0.00)]).

fof(t55_funct_1,theorem,(
    ! [A] : 
      ( ( v1_relat_1(A)
        & v1_funct_1(A) )
     => ( v2_funct_1(A)
       => ( k2_relat_1(A) = k1_relat_1(k2_funct_1(A))
          & k1_relat_1(A) = k2_relat_1(k2_funct_1(A)) ) ) ) ),
    file(funct_1,t55_funct_1),
    [interesting(0.00)]).

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

fof(t45_relat_1,theorem,(
    ! [A] : 
      ( v1_relat_1(A)
     => ! [B] : 
          ( v1_relat_1(B)
         => r1_tarski(k2_relat_1(k5_relat_1(A,B)),k2_relat_1(B)) ) ) ),
    file(relat_1,t45_relat_1),
    [interesting(0.00)]).

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

fof(t11_relset_1,theorem,(
    ! [A,B,C] : 
      ( v1_relat_1(C)
     => ( ( r1_tarski(k1_relat_1(C),A)
          & r1_tarski(k2_relat_1(C),B) )
       => m2_relset_1(C,A,B) ) ) ),
    file(relset_1,t11_relset_1),
    [interesting(0.00)]).

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

fof(t62_funct_1,theorem,(
    ! [A] : 
      ( ( v1_relat_1(A)
        & v1_funct_1(A) )
     => ( v2_funct_1(A)
       => v2_funct_1(k2_funct_1(A)) ) ) ),
    file(funct_1,t62_funct_1),
    [interesting(0.00)]).

fof(t46_funct_1,theorem,(
    ! [A] : 
      ( ( v1_relat_1(A)
        & v1_funct_1(A) )
     => ! [B] : 
          ( ( v1_relat_1(B)
            & v1_funct_1(B) )
         => ( ( v2_funct_1(A)
              & v2_funct_1(B) )
           => v2_funct_1(k5_relat_1(A,B)) ) ) ) ),
    file(funct_1,t46_funct_1),
    [interesting(0.00)]).

fof(t83_funct_2,theorem,(
    ! [A,B] : 
      ( ( v1_funct_1(B)
        & v1_funct_2(B,A,A)
        & m2_relset_1(B,A,A) )
     => ( ( v2_funct_1(B)
          & k2_relat_1(B) = A )
       => ( v1_funct_1(B)
          & v1_funct_2(B,A,A)
          & v3_funct_2(B,A,A)
          & m2_relset_1(B,A,A) ) ) ) ),
    file(funct_2,t83_funct_2),
    [interesting(0.00)]).

fof(t55_relat_1,theorem,(
    ! [A] : 
      ( v1_relat_1(A)
     => ! [B] : 
          ( v1_relat_1(B)
         => ! [C] : 
              ( v1_relat_1(C)
             => k5_relat_1(k5_relat_1(A,B),C) = k5_relat_1(A,k5_relat_1(B,C)) ) ) ) ),
    file(relat_1,t55_relat_1),
    [interesting(0.00)]).

fof(t61_funct_1,theorem,(
    ! [A] : 
      ( ( v1_relat_1(A)
        & v1_funct_1(A) )
     => ( v2_funct_1(A)
       => ( k5_relat_1(A,k2_funct_1(A)) = k6_relat_1(k1_relat_1(A))
          & k5_relat_1(k2_funct_1(A),A) = k6_relat_1(k2_relat_1(A)) ) ) ) ),
    file(funct_1,t61_funct_1),
    [interesting(0.00)]).

fof(t42_funct_1,theorem,(
    ! [A] : 
      ( ( v1_relat_1(A)
        & v1_funct_1(A) )
     => ( k5_relat_1(k6_relat_1(k1_relat_1(A)),A) = A
        & k5_relat_1(A,k6_relat_1(k2_relat_1(A))) = A ) ) ),
    file(funct_1,t42_funct_1),
    [interesting(0.00)]).

fof(t62_relat_1,theorem,(
    ! [A] : 
      ( v1_relat_1(A)
     => ( k5_relat_1(k1_xboole_0,A) = k1_xboole_0
        & k5_relat_1(A,k1_xboole_0) = k1_xboole_0 ) ) ),
    file(relat_1,t62_relat_1),
    [interesting(0.00)]).

fof(l16_finsop_1,theorem,(
    ! [A] : 
      ( ~ v1_xboole_0(A)
     => ! [B] : 
          ( m2_finseq_1(B,A)
         => ! [C] : 
              ( m2_finseq_1(C,A)
             => ! [D] : 
                  ( ( v1_funct_1(D)
                    & v1_funct_2(D,k2_zfmisc_1(A,A),A)
                    & m2_relset_1(D,k2_zfmisc_1(A,A),A) )
                 => ! [E] : 
                      ( ( v1_funct_1(E)
                        & v1_funct_2(E,k4_relset_1(k5_numbers,A,B),k4_relset_1(k5_numbers,A,B))
                        & v3_funct_2(E,k4_relset_1(k5_numbers,A,B),k4_relset_1(k5_numbers,A,B))
                        & m2_relset_1(E,k4_relset_1(k5_numbers,A,B),k4_relset_1(k5_numbers,A,B)) )
                     => ( ( v1_setwiseo(D,A)
                          & k3_finseq_1(B) = 0
                          & C = k5_relat_1(E,B) )
                       => k2_finsop_1(A,B,D) = k2_finsop_1(A,C,D) ) ) ) ) ) ) ),
    inference(mizar_proof,[status(thm)],[t25_finseq_1,t62_relat_1,t25_finseq_1,d1_finsop_1,d1_finsop_1]),
    [file(finsop_1,l16_finsop_1),interesting(0.00)]).

fof(t48_finseq_2,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_funct_1(C)
                & v1_funct_2(C,k4_finseq_1(A),k4_finseq_1(A))
                & v3_funct_2(C,k4_finseq_1(A),k4_finseq_1(A))
                & m2_relset_1(C,k4_finseq_1(A),k4_finseq_1(A)) )
             => ( B = k5_relat_1(C,A)
               => k3_finseq_1(B) = k3_finseq_1(A) ) ) ) ) ),
    file(finseq_2,t48_finseq_2),
    [interesting(0.00)]).

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

fof(d3_funct_2,definition,(
    ! [A,B,C] : 
      ( ( v1_funct_1(C)
        & v1_funct_2(C,A,B)
        & m2_relset_1(C,A,B) )
     => ( v2_funct_2(C,A,B)
      <=> k2_relat_1(C) = B ) ) ),
    file(funct_2,d3_funct_2),
    [interesting(0.00)]).

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

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

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

fof(t14_setwiseo,theorem,(
    ! [A] : 
      ( ~ v1_xboole_0(A)
     => ! [B] : 
          ( m1_subset_1(B,k5_finsub_1(A))
         => ! [C] : 
              ( r2_hidden(C,B)
             => m1_subset_1(C,A) ) ) ) ),
    file(setwiseo,t14_setwiseo),
    [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(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(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(d1_tarski,definition,(
    ! [A,B] : 
      ( B = k1_tarski(A)
    <=> ! [C] : 
          ( r2_hidden(C,B)
        <=> C = A ) ) ),
    file(tarski,d1_tarski),
    [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(d8_funct_1,definition,(
    ! [A] : 
      ( ( v1_relat_1(A)
        & v1_funct_1(A) )
     => ( v2_funct_1(A)
      <=> ! [B,C] : 
            ( ( r2_hidden(B,k1_relat_1(A))
              & r2_hidden(C,k1_relat_1(A))
              & k1_funct_1(A,B) = k1_funct_1(A,C) )
           => B = C ) ) ) ),
    file(funct_1,d8_funct_1),
    [interesting(0.00)]).

fof(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(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(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(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(t16_finseq_3,theorem,(
    ! [A] : 
      ( v4_ordinal2(A)
     => k6_subset_1(k5_numbers,k2_finseq_1(k2_xcmplx_0(A,1)),k2_finseq_1(A)) = k1_tarski(k2_xcmplx_0(A,1)) ) ),
    file(finseq_3,t16_finseq_3),
    [interesting(0.00)]).

fof(t9_finseq_3,theorem,(
    ! [A] : 
      ( v4_ordinal2(A)
     => ~ r2_hidden(k2_xcmplx_0(A,1),k2_finseq_1(A)) ) ),
    file(finseq_3,t9_finseq_3),
    [interesting(0.00)]).

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

fof(t148_xreal_1,theorem,(
    ! [A] : 
      ( v1_xreal_0(A)
     => ~ r1_xreal_0(A,k6_xcmplx_0(A,1)) ) ),
    file(xreal_1,t148_xreal_1),
    [interesting(0.00)]).

fof(t38_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] : 
              ( m2_subset_1(C,k1_numbers,k5_numbers)
             => ~ ( r2_hidden(C,k4_finseq_1(k7_finseq_1(A,B)))
                  & ~ r2_hidden(C,k4_finseq_1(A))
                  & ! [D] : 
                      ( m2_subset_1(D,k1_numbers,k5_numbers)
                     => ~ ( r2_hidden(D,k4_finseq_1(B))
                          & C = k1_nat_1(k3_finseq_1(A),D) ) ) ) ) ) ) ),
    file(finseq_1,t38_finseq_1),
    [interesting(0.00)]).

fof(l19_finsop_1,theorem,(
    ! [A] : 
      ( ~ v1_xboole_0(A)
     => ! [B] : 
          ( m2_finseq_1(B,A)
         => ! [C] : 
              ( m2_finseq_1(C,A)
             => ! [D] : 
                  ( ( v1_funct_1(D)
                    & v1_funct_2(D,k2_zfmisc_1(A,A),A)
                    & m2_relset_1(D,k2_zfmisc_1(A,A),A) )
                 => ( ( k3_finseq_1(B) = 0
                      & v1_setwiseo(D,A)
                      & v2_funct_1(B)
                      & v2_funct_1(C)
                      & k2_relat_1(B) = k2_relat_1(C) )
                   => k2_finsop_1(A,B,D) = k2_finsop_1(A,C,D) ) ) ) ) ) ),
    inference(mizar_proof,[status(thm)],[t65_finseq_1,d1_finsop_1]),
    [file(finsop_1,l19_finsop_1),interesting(0.00)]).