fof(t3_unialg_1,theorem,(
    ! [A] : 
      ( ~ v1_xboole_0(A)
     => ! [B] : 
          ( m1_subset_1(B,A)
         => m1_subset_1(k2_funcop_1(k1_tarski(k6_finseq_1(A)),B),k4_partfun1(k13_finseq_1(A),A)) ) ) ),
    inference(mizar_proof,[status(thm)],[t14_funcop_1,t19_funcop_1,d3_tarski,d1_tarski,d11_finseq_1,d3_tarski,d1_tarski,t11_relset_1,t119_partfun1]),
    [file(unialg_1,t3_unialg_1),interesting(1.00)]).

fof(t1_unialg_1,theorem,(
    ! [A,B] : 
      ( ( v1_funct_1(B)
        & m2_relset_1(B,k13_finseq_1(A),A) )
     => ( ~ ( ~ v1_xboole_0(B)
            & k1_relat_1(B) = k1_xboole_0 )
        & ~ ( k1_relat_1(B) != k1_xboole_0
            & v1_xboole_0(B) ) ) ) ),
    inference(mizar_proof,[status(thm)],[t60_relat_1,t64_relat_1]),
    [file(unialg_1,t1_unialg_1),interesting(0.96)]).

fof(t4_unialg_1,theorem,(
    ! [A] : 
      ( ~ v1_xboole_0(A)
     => ! [B] : 
          ( m1_subset_1(B,A)
         => ! [C] : 
              ( m1_subset_1(C,k4_partfun1(k13_finseq_1(A),A))
             => ( C = k2_funcop_1(k1_tarski(k6_finseq_1(A)),B)
               => ( v4_unialg_1(k1_unialg_1(A,C),A)
                  & v5_unialg_1(k1_unialg_1(A,C),A)
                  & v2_relat_1(k1_unialg_1(A,C)) ) ) ) ) ) ),
    inference(mizar_proof,[status(thm)],[t121_partfun1,t4_finseq_1,d8_finseq_1,d1_tarski,t2_unialg_1,d8_finseq_1,t4_finseq_1,d8_finseq_1,d1_tarski,t2_unialg_1,d8_finseq_1,t4_finseq_1,d8_finseq_1,d1_tarski,t2_unialg_1,d8_finseq_1,d4_unialg_1,d5_unialg_1,d15_funct_1]),
    [file(unialg_1,t4_unialg_1),interesting(0.83)]).

fof(t2_unialg_1,theorem,(
    ! [A] : 
      ( ~ v1_xboole_0(A)
     => ! [B] : 
          ( m1_subset_1(B,A)
         => ( ~ v1_xboole_0(k2_funcop_1(k1_tarski(k6_finseq_1(A)),B))
            & v1_funct_1(k2_funcop_1(k1_tarski(k6_finseq_1(A)),B))
            & v1_unialg_1(k2_funcop_1(k1_tarski(k6_finseq_1(A)),B),A)
            & v2_unialg_1(k2_funcop_1(k1_tarski(k6_finseq_1(A)),B),A)
            & m2_relset_1(k2_funcop_1(k1_tarski(k6_finseq_1(A)),B),k13_finseq_1(A),A) ) ) ) ),
    inference(mizar_proof,[status(thm)],[t14_funcop_1,t19_funcop_1,d3_tarski,d1_tarski,d11_finseq_1,d3_tarski,d1_tarski,t11_relset_1,d1_unialg_1,d1_tarski,d2_unialg_1,d1_tarski,t32_finseq_1,t32_finseq_1,d1_tarski,t19_funcop_1,t60_relat_1]),
    [file(unialg_1,t2_unialg_1),interesting(0.49)]).

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(t64_relat_1,theorem,(
    ! [A] : 
      ( v1_relat_1(A)
     => ( ( k1_relat_1(A) = k1_xboole_0
          | k2_relat_1(A) = k1_xboole_0 )
       => A = k1_xboole_0 ) ) ),
    file(relat_1,t64_relat_1),
    [interesting(0.00)]).

fof(t14_funcop_1,theorem,(
    ! [A,B] : 
      ( A != k1_xboole_0
     => k2_relat_1(k2_funcop_1(A,B)) = k1_tarski(B) ) ),
    file(funcop_1,t14_funcop_1),
    [interesting(0.00)]).

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

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

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

fof(d11_finseq_1,definition,(
    ! [A,B] : 
      ( B = k13_finseq_1(A)
    <=> ! [C] : 
          ( r2_hidden(C,B)
        <=> m2_finseq_1(C,A) ) ) ),
    file(finseq_1,d11_finseq_1),
    [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(t119_partfun1,theorem,(
    ! [A,B,C] : 
      ( ( v1_funct_1(C)
        & m2_relset_1(C,A,B) )
     => r2_hidden(C,k4_partfun1(A,B)) ) ),
    file(partfun1,t119_partfun1),
    [interesting(0.00)]).

fof(t121_partfun1,theorem,(
    ! [A,B,C] : 
      ( m1_subset_1(C,k4_partfun1(A,B))
     => ( v1_funct_1(C)
        & m2_relset_1(C,A,B) ) ) ),
    file(partfun1,t121_partfun1),
    [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(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(d1_unialg_1,definition,(
    ! [A,B] : 
      ( ( v1_funct_1(B)
        & m2_relset_1(B,k13_finseq_1(A),A) )
     => ( v1_unialg_1(B,A)
      <=> ! [C] : 
            ( m2_finseq_1(C,A)
           => ! [D] : 
                ( m2_finseq_1(D,A)
               => ( ( r2_hidden(C,k1_relat_1(B))
                    & r2_hidden(D,k1_relat_1(B)) )
                 => k3_finseq_1(C) = k3_finseq_1(D) ) ) ) ) ) ),
    file(unialg_1,d1_unialg_1),
    [interesting(0.00)]).

fof(d2_unialg_1,definition,(
    ! [A,B] : 
      ( ( v1_funct_1(B)
        & m2_relset_1(B,k13_finseq_1(A),A) )
     => ( v2_unialg_1(B,A)
      <=> ! [C] : 
            ( m2_finseq_1(C,A)
           => ! [D] : 
                ( m2_finseq_1(D,A)
               => ( ( k3_finseq_1(C) = k3_finseq_1(D)
                    & r2_hidden(C,k1_relat_1(B)) )
                 => r2_hidden(D,k1_relat_1(B)) ) ) ) ) ) ),
    file(unialg_1,d2_unialg_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(d4_unialg_1,definition,(
    ! [A,B] : 
      ( m2_finseq_1(B,k4_partfun1(k13_finseq_1(A),A))
     => ( v4_unialg_1(B,A)
      <=> ! [C] : 
            ( m2_subset_1(C,k1_numbers,k5_numbers)
           => ! [D] : 
                ( ( v1_funct_1(D)
                  & m2_relset_1(D,k13_finseq_1(A),A) )
               => ( ( r2_hidden(C,k4_finseq_1(B))
                    & D = k1_funct_1(B,C) )
                 => v1_unialg_1(D,A) ) ) ) ) ) ),
    file(unialg_1,d4_unialg_1),
    [interesting(0.00)]).

fof(d5_unialg_1,definition,(
    ! [A,B] : 
      ( m2_finseq_1(B,k4_partfun1(k13_finseq_1(A),A))
     => ( v5_unialg_1(B,A)
      <=> ! [C] : 
            ( m2_subset_1(C,k1_numbers,k5_numbers)
           => ! [D] : 
                ( ( v1_funct_1(D)
                  & m2_relset_1(D,k13_finseq_1(A),A) )
               => ( ( r2_hidden(C,k4_finseq_1(B))
                    & D = k1_funct_1(B,C) )
                 => v2_unialg_1(D,A) ) ) ) ) ) ),
    file(unialg_1,d5_unialg_1),
    [interesting(0.00)]).

fof(d15_funct_1,definition,(
    ! [A] : 
      ( ( v1_relat_1(A)
        & v1_funct_1(A) )
     => ( v2_relat_1(A)
      <=> ! [B] : ~ ( r2_hidden(B,k1_relat_1(A))
            & v1_xboole_0(k1_funct_1(A,B)) ) ) ) ),
    file(funct_1,d15_funct_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(t5_unialg_1,theorem,(
    ! [A] : 
      ( ( ~ v3_struct_0(A)
        & v6_unialg_1(A)
        & v8_unialg_1(A)
        & l1_unialg_1(A) )
     => ! [B] : 
          ( m2_subset_1(B,k1_numbers,k5_numbers)
         => ( r2_hidden(B,k4_finseq_1(u1_unialg_1(A)))
           => ( v1_funct_1(k1_funct_1(u1_unialg_1(A),B))
              & m2_relset_1(k1_funct_1(u1_unialg_1(A),B),k13_finseq_1(u1_struct_0(A)),u1_struct_0(A)) ) ) ) ) ),
    inference(mizar_proof,[status(thm)],[d4_finseq_1,d5_funct_1,t121_partfun1]),
    [file(unialg_1,t5_unialg_1),interesting(0.00)]).