fof(t2_msuhom_1,theorem,(
    ! [A,B] : 
      ( m1_subset_1(B,k1_zfmisc_1(A))
     => r1_tarski(k3_finseq_2(B),k3_finseq_2(A)) ) ),
    inference(mizar_proof,[status(thm)],[d3_tarski,d11_finseq_1,t1_xboole_1,d4_finseq_1,d11_finseq_1]),
    [file(msuhom_1,t2_msuhom_1),interesting(1.00)]).

fof(t4_msuhom_1,theorem,(
    ! [A,B] : 
      ( m1_subset_1(B,k1_zfmisc_1(A))
     => ! [C] : 
          ( m1_pboole(C,A)
         => k6_pboole(B,k3_pre_circ(A,C,B)) = k7_relat_1(k6_pboole(A,C),k3_finseq_2(B)) ) ) ),
    inference(mizar_proof,[status(thm)],[d3_pboole,t2_msuhom_1,t91_relat_1,d3_pboole,d3_pboole,d3_tarski,t70_funct_1,d19_pboole,d5_card_3,t1_msuhom_1,t1_msuhom_1,t1_msuhom_1,t1_msuhom_1,t1_msuhom_1,t1_msuhom_1,d5_card_3,d19_pboole,t70_funct_1,d5_card_3,d19_pboole]),
    [file(msuhom_1,t4_msuhom_1),interesting(0.99)]).

fof(t3_msuhom_1,theorem,(
    ! [A] : 
      ( ( v1_relat_1(A)
        & v1_funct_1(A) )
     => ! [B] : 
          ( v1_funcop_1(A)
         => v1_funcop_1(k7_relat_1(A,B)) ) ) ),
    inference(mizar_proof,[status(thm)],[t76_funct_1,d6_funcop_1,t70_funct_1,d6_funcop_1]),
    [file(msuhom_1,t3_msuhom_1),interesting(0.98)]).

fof(t20_msuhom_1,theorem,(
    ! [A] : 
      ( ( ~ v3_struct_0(A)
        & v6_unialg_1(A)
        & v7_unialg_1(A)
        & v8_unialg_1(A)
        & l1_unialg_1(A) )
     => ! [B] : 
          ( ( ~ v3_struct_0(B)
            & v6_unialg_1(B)
            & v7_unialg_1(B)
            & v8_unialg_1(B)
            & l1_unialg_1(B) )
         => ! [C] : 
              ( ( v1_funct_1(C)
                & v1_funct_2(C,u1_struct_0(A),u1_struct_0(B))
                & m2_relset_1(C,u1_struct_0(A),u1_struct_0(B)) )
             => ( r4_alg_1(A,B,C)
               => r4_msualg_3(k7_msualg_1(A),k10_msualg_1(A),k2_msuhom_1(k7_msualg_1(A),k7_msualg_1(B),k10_msualg_1(B)),k3_msuhom_1(A,B,C)) ) ) ) ) ),
    inference(mizar_proof,[status(thm)],[d4_alg_1,t18_msuhom_1,d12_msualg_3,d4_alg_1,t19_msuhom_1]),
    [file(msuhom_1,t20_msuhom_1),interesting(0.92)]).

fof(t9_msuhom_1,theorem,(
    ! [A] : 
      ( ( ~ v3_struct_0(A)
        & v1_msualg_1(A)
        & ~ v2_msualg_1(A)
        & l1_msualg_1(A) )
     => ! [B] : 
          ( ( v4_msualg_1(B,A)
            & v5_msualg_1(B,A)
            & l3_msualg_1(B,A) )
         => B = k2_msuhom_1(A,A,B) ) ) ),
    inference(mizar_proof,[status(thm)],[d3_pboole,d3_pboole,d2_msuhom_1,t97_relat_1,d2_msuhom_1,t97_relat_1]),
    [file(msuhom_1,t9_msuhom_1),interesting(0.86)]).

fof(t18_msuhom_1,theorem,(
    ! [A] : 
      ( ( ~ v3_struct_0(A)
        & v6_unialg_1(A)
        & v7_unialg_1(A)
        & v8_unialg_1(A)
        & l1_unialg_1(A) )
     => ! [B] : 
          ( ( ~ v3_struct_0(B)
            & v6_unialg_1(B)
            & v7_unialg_1(B)
            & v8_unialg_1(B)
            & l1_unialg_1(B) )
         => ! [C] : 
              ( ( v1_funct_1(C)
                & v1_funct_2(C,u1_struct_0(A),u1_struct_0(B))
                & m2_relset_1(C,u1_struct_0(A),u1_struct_0(B)) )
             => ( r3_alg_1(A,B,C)
               => r2_msualg_3(k7_msualg_1(A),k10_msualg_1(A),k2_msuhom_1(k7_msualg_1(A),k7_msualg_1(B),k10_msualg_1(B)),k3_msuhom_1(A,B,C)) ) ) ) ) ),
    inference(mizar_proof,[status(thm)],[d1_tarski,d3_alg_1,d1_alg_1,t10_msuhom_1,t16_msuhom_1,d10_msualg_3,d3_msualg_3,d18_pboole,d3_alg_1,d16_msualg_1,t9_msuhom_1,d14_msualg_1,t7_msualg_1,d13_msualg_1,d13_msualg_1,t13_funcop_1,d3_msuhom_1,t13_funcop_1,d1_tarski,d1_tarski]),
    [file(msuhom_1,t18_msuhom_1),interesting(0.85)]).

fof(t1_msuhom_1,theorem,(
    ! [A] : 
      ( ( v1_relat_1(A)
        & v1_funct_1(A) )
     => ! [B] : 
          ( ( v1_relat_1(B)
            & v1_funct_1(B) )
         => ! [C] : 
              ( r1_tarski(k2_relat_1(A),C)
             => k5_relat_1(A,k7_relat_1(B,C)) = k5_relat_1(A,B) ) ) ) ),
    inference(mizar_proof,[status(thm)],[t2_monoid_1,t125_relat_1]),
    [file(msuhom_1,t1_msuhom_1),interesting(0.85)]).

fof(l16_msuhom_1,theorem,(
    ! [A] : 
      ( ( ~ v3_struct_0(A)
        & v6_unialg_1(A)
        & v7_unialg_1(A)
        & v8_unialg_1(A)
        & l1_unialg_1(A) )
     => k4_finseq_1(k6_msualg_1(A)) = k4_finseq_1(u1_unialg_1(A)) ) ),
    inference(mizar_proof,[status(thm)],[d3_finseq_1,d11_unialg_1,d3_finseq_1]),
    [file(msuhom_1,l16_msuhom_1),interesting(0.82)]).

fof(t19_msuhom_1,theorem,(
    ! [A] : 
      ( ( ~ v3_struct_0(A)
        & v6_unialg_1(A)
        & v7_unialg_1(A)
        & v8_unialg_1(A)
        & l1_unialg_1(A) )
     => ! [B] : 
          ( ( ~ v3_struct_0(B)
            & v6_unialg_1(B)
            & v7_unialg_1(B)
            & v8_unialg_1(B)
            & l1_unialg_1(B) )
         => ! [C] : 
              ( ( v1_funct_1(C)
                & v1_funct_2(C,u1_struct_0(A),u1_struct_0(B))
                & m2_relset_1(C,u1_struct_0(A),u1_struct_0(B)) )
             => ( r2_alg_1(A,B,C)
               => r3_msualg_3(k7_msualg_1(A),k10_msualg_1(A),k2_msuhom_1(k7_msualg_1(A),k7_msualg_1(B),k10_msualg_1(B)),k3_msuhom_1(A,B,C)) ) ) ) ) ),
    inference(mizar_proof,[status(thm)],[d2_alg_1,d1_alg_1,t10_msuhom_1,t16_msuhom_1,d11_msualg_3,d2_msualg_3,t7_msualg_1,d13_msualg_1,d3_msuhom_1,t6_cqc_lang,d3_pboole,d1_tarski,d2_alg_1]),
    [file(msuhom_1,t19_msuhom_1),interesting(0.81)]).

fof(t6_msuhom_1,theorem,(
    ! [A] : 
      ( ( ~ v3_struct_0(A)
        & v1_msualg_1(A)
        & l1_msualg_1(A) )
     => ! [B] : 
          ( ( ~ v3_struct_0(B)
            & v1_msualg_1(B)
            & l1_msualg_1(B) )
         => ( ( r1_msuhom_1(A,B)
              & r1_msuhom_1(B,A) )
           => A = B ) ) ) ),
    inference(mizar_proof,[status(thm)],[d1_msuhom_1,d1_msuhom_1,d1_funct_2,d1_funct_2,d10_xboole_0,t97_relat_1,t97_relat_1,d10_xboole_0]),
    [file(msuhom_1,t6_msuhom_1),interesting(0.80)]).

fof(t16_msuhom_1,theorem,(
    ! [A] : 
      ( ( ~ v3_struct_0(A)
        & v6_unialg_1(A)
        & v7_unialg_1(A)
        & v8_unialg_1(A)
        & l1_unialg_1(A) )
     => ! [B] : 
          ( ( ~ v3_struct_0(B)
            & v6_unialg_1(B)
            & v7_unialg_1(B)
            & v8_unialg_1(B)
            & l1_unialg_1(B) )
         => ! [C] : 
              ( ( v1_funct_1(C)
                & v1_funct_2(C,u1_struct_0(A),u1_struct_0(B))
                & m2_relset_1(C,u1_struct_0(A),u1_struct_0(B)) )
             => ( r1_alg_1(A,B,C)
               => r1_msualg_3(k7_msualg_1(A),k10_msualg_1(A),k2_msuhom_1(k7_msualg_1(A),k7_msualg_1(B),k10_msualg_1(B)),k3_msuhom_1(A,B,C)) ) ) ) ) ),
    inference(mizar_proof,[status(thm)],[d1_alg_1,t10_msuhom_1,d9_msualg_3,t12_msuhom_1,d16_msualg_1,d11_msualg_1,t9_msuhom_1,d15_msualg_1,t7_msualg_1,d13_msualg_1,d5_msualg_1,d12_msualg_1,l16_msuhom_1,t13_msuhom_1,d1_funct_2,l18_msuhom_1,t14_msuhom_1,d1_alg_1,t15_msuhom_1,t11_msuhom_1]),
    [file(msuhom_1,t16_msuhom_1),interesting(0.79)]).

fof(t5_msuhom_1,theorem,(
    ! [A] : 
      ( ( ~ v3_struct_0(A)
        & l1_msualg_1(A) )
     => ! [B] : 
          ( ( ~ v3_struct_0(B)
            & l1_msualg_1(B) )
         => ! [C] : 
              ( ( ~ v3_struct_0(C)
                & l1_msualg_1(C) )
             => ( ( r1_msuhom_1(A,B)
                  & r1_msuhom_1(B,C) )
               => r1_msuhom_1(A,C) ) ) ) ) ),
    inference(mizar_proof,[status(thm)],[d1_msuhom_1,d1_msuhom_1,t1_xboole_1,d1_msuhom_1,t1_xboole_1,t28_xboole_1,t100_relat_1,d1_msuhom_1,d1_msuhom_1,t28_xboole_1,t100_relat_1,d1_msuhom_1,d1_msuhom_1]),
    [file(msuhom_1,t5_msuhom_1),interesting(0.79)]).

fof(t10_msuhom_1,theorem,(
    ! [A] : 
      ( ( ~ v3_struct_0(A)
        & v6_unialg_1(A)
        & v7_unialg_1(A)
        & v8_unialg_1(A)
        & l1_unialg_1(A) )
     => ! [B] : 
          ( ( ~ v3_struct_0(B)
            & v6_unialg_1(B)
            & v7_unialg_1(B)
            & v8_unialg_1(B)
            & l1_unialg_1(B) )
         => ( r1_unialg_2(A,B)
           => k7_msualg_1(A) = k7_msualg_1(B) ) ) ) ),
    inference(mizar_proof,[status(thm)],[t7_msualg_1,d13_msualg_1,t7_msualg_1,d13_msualg_1,d2_unialg_2,d2_unialg_2]),
    [file(msuhom_1,t10_msuhom_1),interesting(0.78)]).

fof(t14_msuhom_1,theorem,(
    ! [A] : 
      ( ( ~ v3_struct_0(A)
        & v6_unialg_1(A)
        & v7_unialg_1(A)
        & v8_unialg_1(A)
        & l1_unialg_1(A) )
     => ! [B] : 
          ( m1_subset_1(B,u1_msualg_1(k7_msualg_1(A)))
         => ! [C] : 
              ( m1_subset_1(C,k3_msualg_1(k7_msualg_1(A),B,k10_msualg_1(A)))
             => m2_finseq_1(C,u1_struct_0(A)) ) ) ) ),
    inference(mizar_proof,[status(thm)],[t12_msuhom_1,t7_msualg_1,d13_msualg_1,d5_msualg_1,l16_msuhom_1,t6_unialg_2,d1_funct_2,d3_tarski,d11_finseq_1]),
    [file(msuhom_1,t14_msuhom_1),interesting(0.77)]).

fof(t13_msuhom_1,theorem,(
    ! [A] : 
      ( ( ~ v3_struct_0(A)
        & v6_unialg_1(A)
        & v7_unialg_1(A)
        & v8_unialg_1(A)
        & l1_unialg_1(A) )
     => ! [B] : 
          ( m1_subset_1(B,u1_msualg_1(k7_msualg_1(A)))
         => m2_unialg_2(k5_msualg_1(k7_msualg_1(A),B,k10_msualg_1(A)),u1_struct_0(A),k1_unialg_2(A)) ) ) ),
    inference(mizar_proof,[status(thm)],[t12_msuhom_1,d5_msualg_1,t7_msualg_1,d13_msualg_1,l16_msuhom_1,t6_unialg_2]),
    [file(msuhom_1,t13_msuhom_1),interesting(0.72)]).

fof(t22_msuhom_1,theorem,(
    ! [A] : 
      ( ( ~ v3_struct_0(A)
        & v6_unialg_1(A)
        & v7_unialg_1(A)
        & v8_unialg_1(A)
        & l1_unialg_1(A) )
     => ! [B] : 
          ( ( ~ v3_struct_0(B)
            & v6_unialg_1(B)
            & v7_unialg_1(B)
            & v8_unialg_1(B)
            & l1_unialg_1(B) )
         => ! [C] : 
              ( ( v1_funct_1(C)
                & v1_funct_2(C,u1_struct_0(A),u1_struct_0(B))
                & m2_relset_1(C,u1_struct_0(A),u1_struct_0(B)) )
             => ( ( r1_unialg_2(A,B)
                  & r2_msualg_3(k7_msualg_1(A),k10_msualg_1(A),k2_msuhom_1(k7_msualg_1(A),k7_msualg_1(B),k10_msualg_1(B)),k3_msuhom_1(A,B,C)) )
               => r3_alg_1(A,B,C) ) ) ) ) ),
    inference(mizar_proof,[status(thm)],[d10_msualg_3,t10_msuhom_1,d10_msualg_3,d13_msualg_1,d1_tarski,d3_msuhom_1,t13_funcop_1,d14_msualg_1,t13_funcop_1,t9_msuhom_1,d16_msualg_1,t21_msuhom_1,d3_alg_1,d3_msualg_3]),
    [file(msuhom_1,t22_msuhom_1),interesting(0.72)]).

fof(t8_msuhom_1,theorem,(
    ! [A,B] : 
      ( m1_subset_1(B,k1_zfmisc_1(A))
     => ! [C] : 
          ( m1_pboole(C,A)
         => ! [D] : 
              ( m1_pboole(D,A)
             => ! [E] : 
                  ( m3_pboole(E,A,C,D)
                 => ! [F] : 
                      ( m1_pboole(F,B)
                     => ! [G] : 
                          ( m1_pboole(G,B)
                         => ( ( r6_pboole(B,F,k3_pre_circ(A,C,B))
                              & r6_pboole(B,G,k3_pre_circ(A,D,B)) )
                           => m3_pboole(k3_pre_circ(A,E,B),B,F,G) ) ) ) ) ) ) ) ),
    inference(mizar_proof,[status(thm)],[d3_pboole,d3_pboole,d3_pboole,t70_funct_1,d18_pboole,d6_funcop_1,t70_funct_1,t70_funct_1,d18_pboole,d18_pboole]),
    [file(msuhom_1,t8_msuhom_1),interesting(0.71)]).

fof(t23_msuhom_1,theorem,(
    ! [A] : 
      ( ( ~ v3_struct_0(A)
        & v6_unialg_1(A)
        & v7_unialg_1(A)
        & v8_unialg_1(A)
        & l1_unialg_1(A) )
     => ! [B] : 
          ( ( ~ v3_struct_0(B)
            & v6_unialg_1(B)
            & v7_unialg_1(B)
            & v8_unialg_1(B)
            & l1_unialg_1(B) )
         => ! [C] : 
              ( ( v1_funct_1(C)
                & v1_funct_2(C,u1_struct_0(A),u1_struct_0(B))
                & m2_relset_1(C,u1_struct_0(A),u1_struct_0(B)) )
             => ( ( r1_unialg_2(A,B)
                  & r3_msualg_3(k7_msualg_1(A),k10_msualg_1(A),k2_msuhom_1(k7_msualg_1(A),k7_msualg_1(B),k10_msualg_1(B)),k3_msuhom_1(A,B,C)) )
               => r2_alg_1(A,B,C) ) ) ) ) ),
    inference(mizar_proof,[status(thm)],[t10_msuhom_1,d11_msualg_3,t21_msuhom_1,d11_msualg_3,t7_msualg_1,d13_msualg_1,d1_tarski,d3_msuhom_1,t13_funcop_1,t1_msualg_3,d2_alg_1]),
    [file(msuhom_1,t23_msuhom_1),interesting(0.68)]).

fof(t21_msuhom_1,theorem,(
    ! [A] : 
      ( ( ~ v3_struct_0(A)
        & v6_unialg_1(A)
        & v7_unialg_1(A)
        & v8_unialg_1(A)
        & l1_unialg_1(A) )
     => ! [B] : 
          ( ( ~ v3_struct_0(B)
            & v6_unialg_1(B)
            & v7_unialg_1(B)
            & v8_unialg_1(B)
            & l1_unialg_1(B) )
         => ! [C] : 
              ( ( v1_funct_1(C)
                & v1_funct_2(C,u1_struct_0(A),u1_struct_0(B))
                & m2_relset_1(C,u1_struct_0(A),u1_struct_0(B)) )
             => ( ( r1_unialg_2(A,B)
                  & r1_msualg_3(k7_msualg_1(A),k10_msualg_1(A),k2_msuhom_1(k7_msualg_1(A),k7_msualg_1(B),k10_msualg_1(B)),k3_msuhom_1(A,B,C)) )
               => r1_alg_1(A,B,C) ) ) ) ) ),
    inference(mizar_proof,[status(thm)],[t10_msuhom_1,d1_alg_1,l22_msuhom_1,t12_msuhom_1,d1_funct_2,t11_msuhom_1,d9_msualg_3,d16_msualg_1,d11_msualg_1,t9_msuhom_1,d15_msualg_1,t15_msuhom_1]),
    [file(msuhom_1,t21_msuhom_1),interesting(0.67)]).

fof(t24_msuhom_1,theorem,(
    ! [A] : 
      ( ( ~ v3_struct_0(A)
        & v6_unialg_1(A)
        & v7_unialg_1(A)
        & v8_unialg_1(A)
        & l1_unialg_1(A) )
     => ! [B] : 
          ( ( ~ v3_struct_0(B)
            & v6_unialg_1(B)
            & v7_unialg_1(B)
            & v8_unialg_1(B)
            & l1_unialg_1(B) )
         => ! [C] : 
              ( ( v1_funct_1(C)
                & v1_funct_2(C,u1_struct_0(A),u1_struct_0(B))
                & m2_relset_1(C,u1_struct_0(A),u1_struct_0(B)) )
             => ( ( r1_unialg_2(A,B)
                  & r4_msualg_3(k7_msualg_1(A),k10_msualg_1(A),k2_msuhom_1(k7_msualg_1(A),k7_msualg_1(B),k10_msualg_1(B)),k3_msuhom_1(A,B,C)) )
               => r4_alg_1(A,B,C) ) ) ) ) ),
    inference(mizar_proof,[status(thm)],[d12_msualg_3,d12_msualg_3,t23_msuhom_1,d4_alg_1,t22_msuhom_1]),
    [file(msuhom_1,t24_msuhom_1),interesting(0.67)]).

fof(l22_msuhom_1,theorem,(
    ! [A] : 
      ( ( ~ v3_struct_0(A)
        & v6_unialg_1(A)
        & v7_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)))
           => m1_subset_1(B,u1_msualg_1(k7_msualg_1(A))) ) ) ) ),
    inference(mizar_proof,[status(thm)],[l16_msuhom_1,d13_msualg_1]),
    [file(msuhom_1,l22_msuhom_1),interesting(0.61)]).

fof(t12_msuhom_1,theorem,(
    ! [A] : 
      ( ( ~ v3_struct_0(A)
        & v6_unialg_1(A)
        & v7_unialg_1(A)
        & v8_unialg_1(A)
        & l1_unialg_1(A) )
     => ! [B] : 
          ( m1_subset_1(B,u1_msualg_1(k7_msualg_1(A)))
         => k5_msualg_1(k7_msualg_1(A),B,k10_msualg_1(A)) = k1_funct_1(u1_unialg_1(A),B) ) ) ),
    inference(mizar_proof,[status(thm)],[d16_msualg_1,d11_msualg_1,d15_msualg_1]),
    [file(msuhom_1,t12_msuhom_1),interesting(0.58)]).

fof(t17_msuhom_1,theorem,(
    ! [A] : 
      ( ( ~ v3_struct_0(A)
        & v6_unialg_1(A)
        & v7_unialg_1(A)
        & v8_unialg_1(A)
        & l1_unialg_1(A) )
     => ! [B] : 
          ( ( ~ v3_struct_0(B)
            & v6_unialg_1(B)
            & v7_unialg_1(B)
            & v8_unialg_1(B)
            & l1_unialg_1(B) )
         => ! [C] : 
              ( ( v1_funct_1(C)
                & v1_funct_2(C,u1_struct_0(A),u1_struct_0(B))
                & m2_relset_1(C,u1_struct_0(A),u1_struct_0(B)) )
             => ( r1_unialg_2(A,B)
               => m1_pboole(k3_msuhom_1(A,B,C),k1_tarski(0)) ) ) ) ) ),
    inference(mizar_proof,[status(thm)],[t10_msuhom_1,d3_msuhom_1,t5_cqc_lang,d3_pboole]),
    [file(msuhom_1,t17_msuhom_1),interesting(0.51)]).

fof(l18_msuhom_1,theorem,(
    ! [A] : 
      ( ( ~ v3_struct_0(A)
        & v6_unialg_1(A)
        & v7_unialg_1(A)
        & v8_unialg_1(A)
        & l1_unialg_1(A) )
     => ! [B] : 
          ( ( ~ v3_struct_0(B)
            & v6_unialg_1(B)
            & v7_unialg_1(B)
            & v8_unialg_1(B)
            & l1_unialg_1(B) )
         => ( r1_unialg_2(A,B)
           => ! [C] : 
                ( m1_subset_1(C,u1_msualg_1(k7_msualg_1(A)))
               => m2_unialg_2(k5_msualg_1(k7_msualg_1(A),C,k2_msuhom_1(k7_msualg_1(A),k7_msualg_1(B),k10_msualg_1(B))),u1_struct_0(B),k1_unialg_2(B)) ) ) ) ) ),
    inference(mizar_proof,[status(thm)],[d2_unialg_2,t10_msuhom_1,d16_msualg_1,d11_msualg_1,t9_msuhom_1,d15_msualg_1,d5_msualg_1,t7_msualg_1,d13_msualg_1,l16_msuhom_1,l16_msuhom_1,t6_unialg_2]),
    [file(msuhom_1,l18_msuhom_1),interesting(0.49)]).

fof(t25_msuhom_1,theorem,(
    ! [A] : 
      ( ( ~ v3_struct_0(A)
        & v6_unialg_1(A)
        & v7_unialg_1(A)
        & v8_unialg_1(A)
        & l1_unialg_1(A) )
     => r6_pboole(u1_struct_0(k7_msualg_1(A)),k3_msuhom_1(A,A,k6_partfun1(u1_struct_0(A))),k2_msualg_3(u1_struct_0(k7_msualg_1(A)),u4_msualg_1(k7_msualg_1(A),k10_msualg_1(A)))) ) ),
    inference(mizar_proof,[status(thm)],[d3_msuhom_1,t7_msualg_1,d13_msualg_1,d13_msualg_1,d1_tarski,d16_msualg_1,d14_msualg_1,t6_cqc_lang,d1_msualg_3,t6_cqc_lang,d1_tarski,t3_pboole]),
    [file(msuhom_1,t25_msuhom_1),interesting(0.45)]).

fof(t7_msuhom_1,theorem,(
    ! [A] : 
      ( m2_subset_1(A,k1_numbers,k5_numbers)
     => ! [B] : 
          ( ~ v1_xboole_0(B)
         => ! [C] : 
              ( ( v1_relat_1(C)
                & v1_funct_1(C) )
             => ! [D] : 
                  ( m1_subset_1(D,B)
                 => ! [E] : 
                      ( m2_subset_1(E,k1_numbers,k5_numbers)
                     => ( ( r1_xreal_0(1,E)
                          & r1_xreal_0(E,A) )
                       => k1_funct_1(k3_cqc_lang(D,C),k4_finseq_4(k5_numbers,B,k1_msuhom_1(B,A,D),E)) = C ) ) ) ) ) ) ),
    inference(mizar_proof,[status(thm)],[t3_finseq_1,t68_finseq_2,d4_finseq_4,t70_finseq_2,t6_cqc_lang]),
    [file(msuhom_1,t7_msuhom_1),interesting(0.24)]).

fof(t15_msuhom_1,theorem,(
    ! [A] : 
      ( ( ~ v3_struct_0(A)
        & v6_unialg_1(A)
        & v7_unialg_1(A)
        & v8_unialg_1(A)
        & l1_unialg_1(A) )
     => ! [B] : 
          ( ( ~ v3_struct_0(B)
            & v6_unialg_1(B)
            & v7_unialg_1(B)
            & v8_unialg_1(B)
            & l1_unialg_1(B) )
         => ! [C] : 
              ( ( v1_funct_1(C)
                & v1_funct_2(C,u1_struct_0(A),u1_struct_0(B))
                & m2_relset_1(C,u1_struct_0(A),u1_struct_0(B)) )
             => ( r1_unialg_2(A,B)
               => ! [D] : 
                    ( m1_subset_1(D,u1_msualg_1(k7_msualg_1(A)))
                   => ! [E] : 
                        ( m1_subset_1(E,k3_msualg_1(k7_msualg_1(A),D,k10_msualg_1(A)))
                       => k6_msualg_3(k7_msualg_1(A),k10_msualg_1(A),k2_msuhom_1(k7_msualg_1(A),k7_msualg_1(B),k10_msualg_1(B)),D,k3_msuhom_1(A,B,C),E) = k5_relat_1(E,C) ) ) ) ) ) ) ),
    inference(mizar_proof,[status(thm)],[t10_msuhom_1,d1_tarski,t7_msualg_1,d13_msualg_1,d6_msualg_1,t7_msualg_1,d13_msualg_1,d5_msualg_1,d2_unialg_2,d1_funct_2,t22_funct_1,d5_funct_1,t6_msualg_3,d1_tarski,t77_finseq_2,d11_finseq_1,d20_pboole,d20_pboole,d4_finseq_4,t68_finseq_2,t70_finseq_2,d3_msuhom_1,t13_funcop_1,t14_msuhom_1,d4_finseq_1,t6_msualg_3,d20_pboole,t68_finseq_2,t6_msualg_3,d20_pboole,t68_finseq_2,t1_alg_1,t6_msualg_3,d20_pboole,t68_finseq_2,d2_finseq_1,d1_funct_2,t20_finseq_1,t1_alg_1,d8_msualg_3,t1_alg_1,t1_alg_1,t17_finseq_1]),
    [file(msuhom_1,t15_msuhom_1),interesting(0.20)]).

fof(t26_msuhom_1,theorem,(
    ! [A] : 
      ( ( ~ v3_struct_0(A)
        & v6_unialg_1(A)
        & v7_unialg_1(A)
        & v8_unialg_1(A)
        & l1_unialg_1(A) )
     => ! [B] : 
          ( ( ~ v3_struct_0(B)
            & v6_unialg_1(B)
            & v7_unialg_1(B)
            & v8_unialg_1(B)
            & l1_unialg_1(B) )
         => ! [C] : 
              ( ( ~ v3_struct_0(C)
                & v6_unialg_1(C)
                & v7_unialg_1(C)
                & v8_unialg_1(C)
                & l1_unialg_1(C) )
             => ( ( r1_unialg_2(A,B)
                  & r1_unialg_2(B,C) )
               => ! [D] : 
                    ( ( v1_funct_1(D)
                      & v1_funct_2(D,u1_struct_0(A),u1_struct_0(B))
                      & m2_relset_1(D,u1_struct_0(A),u1_struct_0(B)) )
                   => ! [E] : 
                        ( ( v1_funct_1(E)
                          & v1_funct_2(E,u1_struct_0(B),u1_struct_0(C))
                          & m2_relset_1(E,u1_struct_0(B),u1_struct_0(C)) )
                       => k13_pboole(k3_msuhom_1(A,B,D),k3_msuhom_1(B,C,E)) = k3_msuhom_1(A,C,k7_funct_2(u1_struct_0(A),u1_struct_0(B),u1_struct_0(C),D,E)) ) ) ) ) ) ) ),
    inference(mizar_proof,[status(thm)],[t4_unialg_2,t10_msuhom_1,t10_msuhom_1,t17_msuhom_1,t17_msuhom_1,d3_pboole,d24_pboole,d3_pboole,d1_tarski,d3_msuhom_1,t6_cqc_lang,d1_tarski,d3_msuhom_1,t6_cqc_lang,d24_pboole,d3_pboole,t17_msuhom_1,d3_pboole,d3_pboole,d3_msuhom_1,t6_cqc_lang,d1_tarski,d3_pboole,d3_msuhom_1,t6_cqc_lang,d1_tarski,d3_msuhom_1,t6_cqc_lang,d1_tarski,t3_pboole]),
    [file(msuhom_1,t26_msuhom_1),interesting(0.03)]).

fof(d4_alg_1,definition,(
    ! [A] : 
      ( ( ~ v3_struct_0(A)
        & v6_unialg_1(A)
        & v7_unialg_1(A)
        & v8_unialg_1(A)
        & l1_unialg_1(A) )
     => ! [B] : 
          ( ( ~ v3_struct_0(B)
            & v6_unialg_1(B)
            & v7_unialg_1(B)
            & v8_unialg_1(B)
            & l1_unialg_1(B) )
         => ! [C] : 
              ( ( v1_funct_1(C)
                & v1_funct_2(C,u1_struct_0(A),u1_struct_0(B))
                & m2_relset_1(C,u1_struct_0(A),u1_struct_0(B)) )
             => ( r4_alg_1(A,B,C)
              <=> ( r2_alg_1(A,B,C)
                  & r3_alg_1(A,B,C) ) ) ) ) ) ),
    file(alg_1,d4_alg_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(d3_alg_1,definition,(
    ! [A] : 
      ( ( ~ v3_struct_0(A)
        & v6_unialg_1(A)
        & v7_unialg_1(A)
        & v8_unialg_1(A)
        & l1_unialg_1(A) )
     => ! [B] : 
          ( ( ~ v3_struct_0(B)
            & v6_unialg_1(B)
            & v7_unialg_1(B)
            & v8_unialg_1(B)
            & l1_unialg_1(B) )
         => ! [C] : 
              ( ( v1_funct_1(C)
                & v1_funct_2(C,u1_struct_0(A),u1_struct_0(B))
                & m2_relset_1(C,u1_struct_0(A),u1_struct_0(B)) )
             => ( r3_alg_1(A,B,C)
              <=> ( r1_alg_1(A,B,C)
                  & k2_relat_1(C) = u1_struct_0(B) ) ) ) ) ) ),
    file(alg_1,d3_alg_1),
    [interesting(0.00)]).

fof(d1_alg_1,definition,(
    ! [A] : 
      ( ( ~ v3_struct_0(A)
        & v6_unialg_1(A)
        & v7_unialg_1(A)
        & v8_unialg_1(A)
        & l1_unialg_1(A) )
     => ! [B] : 
          ( ( ~ v3_struct_0(B)
            & v6_unialg_1(B)
            & v7_unialg_1(B)
            & v8_unialg_1(B)
            & l1_unialg_1(B) )
         => ! [C] : 
              ( ( v1_funct_1(C)
                & v1_funct_2(C,u1_struct_0(A),u1_struct_0(B))
                & m2_relset_1(C,u1_struct_0(A),u1_struct_0(B)) )
             => ( r1_alg_1(A,B,C)
              <=> ( r1_unialg_2(A,B)
                  & ! [D] : 
                      ( m2_subset_1(D,k1_numbers,k5_numbers)
                     => ( r2_hidden(D,k4_finseq_1(u1_unialg_1(A)))
                       => ! [E] : 
                            ( m2_unialg_2(E,u1_struct_0(A),k1_unialg_2(A))
                           => ! [F] : 
                                ( m2_unialg_2(F,u1_struct_0(B),k1_unialg_2(B))
                               => ( ( E = k1_funct_1(u1_unialg_1(A),D)
                                    & F = k1_funct_1(u1_unialg_1(B),D) )
                                 => ! [G] : 
                                      ( m2_finseq_1(G,u1_struct_0(A))
                                     => ( r2_hidden(G,k4_relset_1(k3_finseq_2(u1_struct_0(A)),u1_struct_0(A),E))
                                       => k1_funct_1(C,k1_funct_1(E,G)) = k1_funct_1(F,k5_finseqop(u1_struct_0(A),u1_struct_0(B),G,C)) ) ) ) ) ) ) ) ) ) ) ) ) ),
    file(alg_1,d1_alg_1),
    [interesting(0.00)]).

fof(t7_msualg_1,theorem,(
    ! [A,B] : 
      ( ~ v1_xboole_0(B)
     => ! [C] : 
          ( ~ v1_xboole_0(C)
         => ! [D] : 
              ( ( v1_funct_1(D)
                & m2_relset_1(D,A,B) )
             => ! [E] : 
                  ( ( v1_funct_1(E)
                    & v1_funct_2(E,B,C)
                    & m2_relset_1(E,B,C) )
                 => ( v1_funct_1(k1_partfun1(A,B,B,C,D,E))
                    & v1_funct_2(k1_partfun1(A,B,B,C,D,E),k1_relat_1(D),C)
                    & m2_relset_1(k1_partfun1(A,B,B,C,D,E),k1_relat_1(D),C) ) ) ) ) ) ),
    file(msualg_1,t7_msualg_1),
    [interesting(0.00)]).

fof(d13_msualg_1,definition,(
    ! [A] : 
      ( ( ~ v3_struct_0(A)
        & v6_unialg_1(A)
        & v7_unialg_1(A)
        & v8_unialg_1(A)
        & l1_unialg_1(A) )
     => ! [B] : 
          ( ( v3_realset2(B)
            & v1_msualg_1(B)
            & ~ v2_msualg_1(B)
            & v6_msualg_1(B)
            & l1_msualg_1(B) )
         => ( B = k7_msualg_1(A)
          <=> ( u1_struct_0(B) = k1_tarski(0)
              & u1_msualg_1(B) = k4_finseq_1(k6_msualg_1(A))
              & u2_msualg_1(B) = k1_partfun1(k5_numbers,k5_numbers,k5_numbers,k3_finseq_2(k1_tarski(0)),k6_msualg_1(A),k9_pboole(0))
              & u3_msualg_1(B) = k10_pboole(k4_finseq_1(k6_msualg_1(A)),0) ) ) ) ) ),
    file(msualg_1,d13_msualg_1),
    [interesting(0.00)]).

fof(d2_unialg_2,definition,(
    ! [A] : 
      ( ( ~ v3_struct_0(A)
        & v6_unialg_1(A)
        & v7_unialg_1(A)
        & v8_unialg_1(A)
        & l1_unialg_1(A) )
     => ! [B] : 
          ( ( ~ v3_struct_0(B)
            & v6_unialg_1(B)
            & v7_unialg_1(B)
            & v8_unialg_1(B)
            & l1_unialg_1(B) )
         => ( r1_unialg_2(A,B)
          <=> k3_unialg_1(A) = k3_unialg_1(B) ) ) ) ),
    file(unialg_2,d2_unialg_2),
    [interesting(0.00)]).

fof(d9_msualg_3,definition,(
    ! [A] : 
      ( ( ~ v3_struct_0(A)
        & ~ v2_msualg_1(A)
        & l1_msualg_1(A) )
     => ! [B] : 
          ( l3_msualg_1(B,A)
         => ! [C] : 
              ( l3_msualg_1(C,A)
             => ! [D] : 
                  ( m3_pboole(D,u1_struct_0(A),u4_msualg_1(A,B),u4_msualg_1(A,C))
                 => ( r1_msualg_3(A,B,C,D)
                  <=> ! [E] : 
                        ( m1_subset_1(E,u1_msualg_1(A))
                       => ( k3_msualg_1(A,E,B) != k1_xboole_0
                         => ! [F] : 
                              ( m1_subset_1(F,k3_msualg_1(A,E,B))
                             => k1_funct_1(k1_msualg_3(u1_struct_0(A),u4_msualg_1(A,B),u4_msualg_1(A,C),D,k2_msualg_1(A,E)),k1_funct_1(k5_msualg_1(A,E,B),F)) = k1_funct_1(k5_msualg_1(A,E,C),k5_msualg_3(A,B,C,E,D,F)) ) ) ) ) ) ) ) ) ),
    file(msualg_3,d9_msualg_3),
    [interesting(0.00)]).

fof(d16_msualg_1,definition,(
    ! [A] : 
      ( ( ~ v3_struct_0(A)
        & v6_unialg_1(A)
        & v7_unialg_1(A)
        & v8_unialg_1(A)
        & l1_unialg_1(A) )
     => k10_msualg_1(A) = g3_msualg_1(k7_msualg_1(A),k8_msualg_1(A),k9_msualg_1(A)) ) ),
    file(msualg_1,d16_msualg_1),
    [interesting(0.00)]).

fof(d11_msualg_1,definition,(
    ! [A] : 
      ( ( ~ v3_struct_0(A)
        & ~ v2_msualg_1(A)
        & l1_msualg_1(A) )
     => ! [B] : 
          ( m1_subset_1(B,u1_msualg_1(A))
         => ! [C] : 
              ( l3_msualg_1(C,A)
             => k5_msualg_1(A,B,C) = k1_funct_1(u5_msualg_1(A,C),B) ) ) ) ),
    file(msualg_1,d11_msualg_1),
    [interesting(0.00)]).

fof(d15_msualg_1,definition,(
    ! [A] : 
      ( ( ~ v3_struct_0(A)
        & v6_unialg_1(A)
        & v7_unialg_1(A)
        & v8_unialg_1(A)
        & l1_unialg_1(A) )
     => k9_msualg_1(A) = u1_unialg_1(A) ) ),
    file(msualg_1,d15_msualg_1),
    [interesting(0.00)]).

fof(d3_pboole,definition,(
    ! [A,B] : 
      ( ( v1_relat_1(B)
        & v1_funct_1(B) )
     => ( m1_pboole(B,A)
      <=> k1_relat_1(B) = A ) ) ),
    file(pboole,d3_pboole),
    [interesting(0.00)]).

fof(d2_msuhom_1,definition,(
    ! [A] : 
      ( ( ~ v3_struct_0(A)
        & v1_msualg_1(A)
        & ~ v2_msualg_1(A)
        & l1_msualg_1(A) )
     => ! [B] : 
          ( ( ~ v3_struct_0(B)
            & v1_msualg_1(B)
            & ~ v2_msualg_1(B)
            & l1_msualg_1(B) )
         => ! [C] : 
              ( ( v4_msualg_1(C,B)
                & v5_msualg_1(C,B)
                & l3_msualg_1(C,B) )
             => ( r1_msuhom_1(A,B)
               => ! [D] : 
                    ( ( v4_msualg_1(D,A)
                      & v5_msualg_1(D,A)
                      & l3_msualg_1(D,A) )
                   => ( D = k2_msuhom_1(A,B,C)
                    <=> ( u4_msualg_1(A,D) = k7_relat_1(u4_msualg_1(B,C),u1_struct_0(A))
                        & u5_msualg_1(A,D) = k7_relat_1(u5_msualg_1(B,C),u1_msualg_1(A)) ) ) ) ) ) ) ) ),
    file(msuhom_1,d2_msuhom_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(d5_msualg_1,definition,(
    ! [A] : 
      ( l1_msualg_1(A)
     => ( v2_msualg_1(A)
      <=> u1_msualg_1(A) = k1_xboole_0 ) ) ),
    file(msualg_1,d5_msualg_1),
    [interesting(0.00)]).

fof(d12_msualg_1,definition,(
    ! [A] : 
      ( l1_msualg_1(A)
     => ( v6_msualg_1(A)
      <=> ? [B] : 
            ( m2_subset_1(B,k1_numbers,k5_numbers)
            & u1_msualg_1(A) = k2_finseq_1(B) ) ) ) ),
    file(msualg_1,d12_msualg_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(d11_unialg_1,definition,(
    ! [A] : 
      ( ( ~ v3_struct_0(A)
        & v6_unialg_1(A)
        & v8_unialg_1(A)
        & l1_unialg_1(A) )
     => ! [B] : 
          ( m2_finseq_1(B,k5_numbers)
         => ( B = k3_unialg_1(A)
          <=> ( k3_finseq_1(B) = k3_finseq_1(u1_unialg_1(A))
              & ! [C] : 
                  ( m2_subset_1(C,k1_numbers,k5_numbers)
                 => ( r2_hidden(C,k4_finseq_1(B))
                   => ! [D] : 
                        ( ( ~ v1_xboole_0(D)
                          & v1_funct_1(D)
                          & v1_unialg_1(D,u1_struct_0(A))
                          & m2_relset_1(D,k13_finseq_1(u1_struct_0(A)),u1_struct_0(A)) )
                       => ( D = k1_funct_1(u1_unialg_1(A),C)
                         => k1_funct_1(B,C) = k2_unialg_1(u1_struct_0(A),D) ) ) ) ) ) ) ) ) ),
    file(unialg_1,d11_unialg_1),
    [interesting(0.00)]).

fof(t6_unialg_2,theorem,(
    ! [A] : 
      ( ( ~ v3_struct_0(A)
        & v6_unialg_1(A)
        & v7_unialg_1(A)
        & v8_unialg_1(A)
        & l1_unialg_1(A) )
     => ! [B] : 
          ( r2_hidden(B,k4_finseq_1(u1_unialg_1(A)))
         => m2_unialg_2(k1_funct_1(u1_unialg_1(A),B),u1_struct_0(A),k1_unialg_2(A)) ) ) ),
    file(unialg_2,t6_unialg_2),
    [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(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(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(d6_msualg_1,definition,(
    ! [A] : 
      ( ( ~ v3_struct_0(A)
        & ~ v2_msualg_1(A)
        & l1_msualg_1(A) )
     => ! [B] : 
          ( m1_subset_1(B,u1_msualg_1(A))
         => k1_msualg_1(A,B) = k1_funct_1(u2_msualg_1(A),B) ) ) ),
    file(msualg_1,d6_msualg_1),
    [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(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(t6_msualg_3,theorem,(
    ! [A] : 
      ( ( ~ v3_struct_0(A)
        & ~ v2_msualg_1(A)
        & l1_msualg_1(A) )
     => ! [B] : 
          ( m1_subset_1(B,u1_msualg_1(A))
         => ! [C] : 
              ( l3_msualg_1(C,A)
             => ! [D] : 
                  ( ( v1_relat_1(D)
                    & v1_funct_1(D) )
                 => ( r2_hidden(D,k3_msualg_1(A,B,C))
                   => ( k1_relat_1(D) = k4_finseq_1(k1_msualg_1(A,B))
                      & ! [E] : 
                          ( r2_hidden(E,k1_relat_1(k5_relat_1(k1_msualg_1(A,B),u4_msualg_1(A,C))))
                         => r2_hidden(k1_funct_1(D,E),k1_funct_1(k5_relat_1(k1_msualg_1(A,B),u4_msualg_1(A,C)),E)) ) ) ) ) ) ) ) ),
    file(msualg_3,t6_msualg_3),
    [interesting(0.00)]).

fof(t77_finseq_2,theorem,(
    ! [A] : 
      ( v4_ordinal2(A)
     => ! [B] : 
          ( ~ v1_xboole_0(B)
         => ! [C] : 
              ( m1_subset_1(C,B)
             => m2_finseq_1(k2_finseq_2(A,C),B) ) ) ) ),
    file(finseq_2,t77_finseq_2),
    [interesting(0.00)]).

fof(d20_pboole,definition,(
    ! [A,B] : 
      ( ( v1_funct_1(B)
        & v1_funct_2(B,k5_numbers,k3_finseq_2(k1_tarski(A)))
        & m2_relset_1(B,k5_numbers,k3_finseq_2(k1_tarski(A))) )
     => ( B = k9_pboole(A)
      <=> ! [C] : 
            ( m2_subset_1(C,k1_numbers,k5_numbers)
           => k8_funct_2(k5_numbers,k3_finseq_2(k1_tarski(A)),B,C) = k2_finseq_2(C,A) ) ) ) ),
    file(pboole,d20_pboole),
    [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(t68_finseq_2,theorem,(
    ! [A] : 
      ( v4_ordinal2(A)
     => ! [B] : k4_finseq_1(k2_finseq_2(A,B)) = k2_finseq_1(A) ) ),
    file(finseq_2,t68_finseq_2),
    [interesting(0.00)]).

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

fof(d3_msuhom_1,definition,(
    ! [A] : 
      ( ( ~ v3_struct_0(A)
        & v6_unialg_1(A)
        & v7_unialg_1(A)
        & v8_unialg_1(A)
        & l1_unialg_1(A) )
     => ! [B] : 
          ( ( ~ v3_struct_0(B)
            & v6_unialg_1(B)
            & v7_unialg_1(B)
            & v8_unialg_1(B)
            & l1_unialg_1(B) )
         => ! [C] : 
              ( ( v1_funct_1(C)
                & v1_funct_2(C,u1_struct_0(A),u1_struct_0(B))
                & m2_relset_1(C,u1_struct_0(A),u1_struct_0(B)) )
             => ( k7_msualg_1(A) = k7_msualg_1(B)
               => k3_msuhom_1(A,B,C) = k2_pre_circ(k1_tarski(0),C) ) ) ) ) ),
    file(msuhom_1,d3_msuhom_1),
    [interesting(0.00)]).

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

fof(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(t1_alg_1,theorem,(
    ! [A] : 
      ( ~ v1_xboole_0(A)
     => ! [B] : 
          ( ~ v1_xboole_0(B)
         => ! [C] : 
              ( m2_finseq_1(C,A)
             => ! [D] : 
                  ( ( v1_funct_1(D)
                    & v1_funct_2(D,A,B)
                    & m2_relset_1(D,A,B) )
                 => ( k4_finseq_1(k5_finseqop(A,B,C,D)) = k4_finseq_1(C)
                    & k3_finseq_1(k5_finseqop(A,B,C,D)) = k3_finseq_1(C)
                    & ! [E] : 
                        ( m2_subset_1(E,k1_numbers,k5_numbers)
                       => ( r2_hidden(E,k4_finseq_1(k5_finseqop(A,B,C,D)))
                         => k1_funct_1(k5_finseqop(A,B,C,D),E) = k1_funct_1(D,k1_funct_1(C,E)) ) ) ) ) ) ) ) ),
    file(alg_1,t1_alg_1),
    [interesting(0.00)]).

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

fof(t20_finseq_1,theorem,(
    ! [A] : 
      ( ( v1_relat_1(A)
        & v1_funct_1(A) )
     => ! [B] : 
          ( ( v1_relat_1(B)
            & v1_funct_1(B)
            & v1_finseq_1(B) )
         => ( r1_tarski(k2_relat_1(B),k1_relat_1(A))
           => ( v1_relat_1(k5_relat_1(B,A))
              & v1_funct_1(k5_relat_1(B,A))
              & v1_finseq_1(k5_relat_1(B,A)) ) ) ) ) ),
    file(finseq_1,t20_finseq_1),
    [interesting(0.00)]).

fof(d8_msualg_3,definition,(
    ! [A] : 
      ( ( ~ v3_struct_0(A)
        & ~ v2_msualg_1(A)
        & l1_msualg_1(A) )
     => ! [B] : 
          ( ( v5_msualg_1(B,A)
            & l3_msualg_1(B,A) )
         => ! [C] : 
              ( ( v5_msualg_1(C,A)
                & l3_msualg_1(C,A) )
             => ! [D] : 
                  ( m1_subset_1(D,u1_msualg_1(A))
                 => ! [E] : 
                      ( m3_pboole(E,u1_struct_0(A),u4_msualg_1(A,B),u4_msualg_1(A,C))
                     => ! [F] : 
                          ( m1_subset_1(F,k3_msualg_1(A,D,B))
                         => ! [G] : 
                              ( m1_subset_1(G,k3_msualg_1(A,D,C))
                             => ( G = k6_msualg_3(A,B,C,D,E,F)
                              <=> ! [H] : 
                                    ( m2_subset_1(H,k1_numbers,k5_numbers)
                                   => ( r2_hidden(H,k1_relat_1(F))
                                     => k1_funct_1(G,H) = k1_funct_1(k1_msualg_3(u1_struct_0(A),u4_msualg_1(A,B),u4_msualg_1(A,C),E,k4_finseq_4(k5_numbers,u1_struct_0(A),k1_msualg_1(A,D),H)),k1_funct_1(F,H)) ) ) ) ) ) ) ) ) ) ) ),
    file(msualg_3,d8_msualg_3),
    [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(d7_msualg_1,definition,(
    ! [A] : 
      ( ( ~ v3_struct_0(A)
        & ~ v2_msualg_1(A)
        & l1_msualg_1(A) )
     => ! [B] : 
          ( m1_subset_1(B,u1_msualg_1(A))
         => k2_msualg_1(A,B) = k1_funct_1(u3_msualg_1(A),B) ) ) ),
    file(msualg_1,d7_msualg_1),
    [interesting(0.00)]).

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

fof(t11_msuhom_1,theorem,(
    ! [A] : 
      ( ( ~ v3_struct_0(A)
        & v6_unialg_1(A)
        & v7_unialg_1(A)
        & v8_unialg_1(A)
        & l1_unialg_1(A) )
     => ! [B] : 
          ( ( ~ v3_struct_0(B)
            & v6_unialg_1(B)
            & v7_unialg_1(B)
            & v8_unialg_1(B)
            & l1_unialg_1(B) )
         => ! [C] : 
              ( ( v1_funct_1(C)
                & v1_funct_2(C,u1_struct_0(A),u1_struct_0(B))
                & m2_relset_1(C,u1_struct_0(A),u1_struct_0(B)) )
             => ( r1_unialg_2(A,B)
               => ! [D] : 
                    ( m1_subset_1(D,u1_msualg_1(k7_msualg_1(A)))
                   => k1_msualg_3(u1_struct_0(k7_msualg_1(A)),u4_msualg_1(k7_msualg_1(A),k10_msualg_1(A)),u4_msualg_1(k7_msualg_1(A),k2_msuhom_1(k7_msualg_1(A),k7_msualg_1(B),k10_msualg_1(B))),k3_msuhom_1(A,B,C),k2_msualg_1(k7_msualg_1(A),D)) = C ) ) ) ) ) ),
    inference(mizar_proof,[status(thm)],[t10_msuhom_1,d1_tarski,t7_msualg_1,d13_msualg_1,t7_msualg_1,d13_msualg_1,d5_msualg_1,t10_msuhom_1,d12_msualg_1,d2_unialg_2,t70_finseq_2,d7_msualg_1,d3_msuhom_1,d2_finseq_2,t13_funcop_1]),
    [file(msuhom_1,t11_msuhom_1),interesting(0.00)]).

fof(d10_msualg_3,definition,(
    ! [A] : 
      ( ( ~ v3_struct_0(A)
        & ~ v2_msualg_1(A)
        & l1_msualg_1(A) )
     => ! [B] : 
          ( l3_msualg_1(B,A)
         => ! [C] : 
              ( l3_msualg_1(C,A)
             => ! [D] : 
                  ( m3_pboole(D,u1_struct_0(A),u4_msualg_1(A,B),u4_msualg_1(A,C))
                 => ( r2_msualg_3(A,B,C,D)
                  <=> ( r1_msualg_3(A,B,C,D)
                      & v2_msualg_3(D,u1_struct_0(A),u4_msualg_1(A,B),u4_msualg_1(A,C)) ) ) ) ) ) ) ),
    file(msualg_3,d10_msualg_3),
    [interesting(0.00)]).

fof(d3_msualg_3,definition,(
    ! [A,B] : 
      ( m1_pboole(B,A)
     => ! [C] : 
          ( m1_pboole(C,A)
         => ! [D] : 
              ( m3_pboole(D,A,B,C)
             => ( v2_msualg_3(D,A,B,C)
              <=> ! [E] : 
                    ( r2_hidden(E,A)
                   => k2_relat_1(k1_funct_1(D,E)) = k1_funct_1(C,E) ) ) ) ) ) ),
    file(msualg_3,d3_msualg_3),
    [interesting(0.00)]).

fof(d18_pboole,definition,(
    ! [A,B] : 
      ( m1_pboole(B,A)
     => ! [C] : 
          ( m1_pboole(C,A)
         => ! [D] : 
              ( m1_pboole(D,A)
             => ( m3_pboole(D,A,B,C)
              <=> ! [E] : 
                    ( r2_hidden(E,A)
                   => ( v1_funct_1(k1_funct_1(D,E))
                      & v1_funct_2(k1_funct_1(D,E),k1_funct_1(B,E),k1_funct_1(C,E))
                      & m2_relset_1(k1_funct_1(D,E),k1_funct_1(B,E),k1_funct_1(C,E)) ) ) ) ) ) ) ),
    file(pboole,d18_pboole),
    [interesting(0.00)]).

fof(d14_msualg_1,definition,(
    ! [A] : 
      ( ( ~ v3_struct_0(A)
        & v6_unialg_1(A)
        & v7_unialg_1(A)
        & v8_unialg_1(A)
        & l1_unialg_1(A) )
     => k8_msualg_1(A) = k10_pboole(k1_tarski(0),u1_struct_0(A)) ) ),
    file(msualg_1,d14_msualg_1),
    [interesting(0.00)]).

fof(d12_msualg_3,definition,(
    ! [A] : 
      ( ( ~ v3_struct_0(A)
        & ~ v2_msualg_1(A)
        & l1_msualg_1(A) )
     => ! [B] : 
          ( l3_msualg_1(B,A)
         => ! [C] : 
              ( l3_msualg_1(C,A)
             => ! [D] : 
                  ( m3_pboole(D,u1_struct_0(A),u4_msualg_1(A,B),u4_msualg_1(A,C))
                 => ( r4_msualg_3(A,B,C,D)
                  <=> ( r2_msualg_3(A,B,C,D)
                      & r3_msualg_3(A,B,C,D) ) ) ) ) ) ) ),
    file(msualg_3,d12_msualg_3),
    [interesting(0.00)]).

fof(d2_alg_1,definition,(
    ! [A] : 
      ( ( ~ v3_struct_0(A)
        & v6_unialg_1(A)
        & v7_unialg_1(A)
        & v8_unialg_1(A)
        & l1_unialg_1(A) )
     => ! [B] : 
          ( ( ~ v3_struct_0(B)
            & v6_unialg_1(B)
            & v7_unialg_1(B)
            & v8_unialg_1(B)
            & l1_unialg_1(B) )
         => ! [C] : 
              ( ( v1_funct_1(C)
                & v1_funct_2(C,u1_struct_0(A),u1_struct_0(B))
                & m2_relset_1(C,u1_struct_0(A),u1_struct_0(B)) )
             => ( r2_alg_1(A,B,C)
              <=> ( r1_alg_1(A,B,C)
                  & v2_funct_1(C) ) ) ) ) ) ),
    file(alg_1,d2_alg_1),
    [interesting(0.00)]).

fof(d11_msualg_3,definition,(
    ! [A] : 
      ( ( ~ v3_struct_0(A)
        & ~ v2_msualg_1(A)
        & l1_msualg_1(A) )
     => ! [B] : 
          ( l3_msualg_1(B,A)
         => ! [C] : 
              ( l3_msualg_1(C,A)
             => ! [D] : 
                  ( m3_pboole(D,u1_struct_0(A),u4_msualg_1(A,B),u4_msualg_1(A,C))
                 => ( r3_msualg_3(A,B,C,D)
                  <=> ( r1_msualg_3(A,B,C,D)
                      & v1_msualg_3(D) ) ) ) ) ) ) ),
    file(msualg_3,d11_msualg_3),
    [interesting(0.00)]).

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

fof(t6_cqc_lang,theorem,(
    ! [A,B] : k1_funct_1(k3_cqc_lang(A,B),A) = B ),
    file(cqc_lang,t6_cqc_lang),
    [interesting(0.00)]).

fof(t1_msualg_3,theorem,(
    ! [A,B] : 
      ( ( v1_funcop_1(B)
        & m1_pboole(B,A) )
     => ( v1_msualg_3(B)
      <=> ! [C] : 
            ( r2_hidden(C,A)
           => v2_funct_1(k1_funct_1(B,C)) ) ) ) ),
    file(msualg_3,t1_msualg_3),
    [interesting(0.00)]).

fof(d1_msualg_3,definition,(
    ! [A,B] : 
      ( m1_pboole(B,A)
     => ! [C] : 
          ( m3_pboole(C,A,B,B)
         => ( C = k2_msualg_3(A,B)
          <=> ! [D] : 
                ( r2_hidden(D,A)
               => k1_funct_1(C,D) = k6_partfun1(k1_funct_1(B,D)) ) ) ) ) ),
    file(msualg_3,d1_msualg_3),
    [interesting(0.00)]).

fof(t3_pboole,theorem,(
    ! [A,B] : 
      ( m1_pboole(B,A)
     => ! [C] : 
          ( m1_pboole(C,A)
         => ( ! [D] : 
                ( r2_hidden(D,A)
               => k1_funct_1(B,D) = k1_funct_1(C,D) )
           => B = C ) ) ) ),
    file(pboole,t3_pboole),
    [interesting(0.00)]).

fof(t4_unialg_2,theorem,(
    ! [A] : 
      ( ( ~ v3_struct_0(A)
        & v6_unialg_1(A)
        & v7_unialg_1(A)
        & v8_unialg_1(A)
        & l1_unialg_1(A) )
     => ! [B] : 
          ( ( ~ v3_struct_0(B)
            & v6_unialg_1(B)
            & v7_unialg_1(B)
            & v8_unialg_1(B)
            & l1_unialg_1(B) )
         => ! [C] : 
              ( ( ~ v3_struct_0(C)
                & v6_unialg_1(C)
                & v7_unialg_1(C)
                & v8_unialg_1(C)
                & l1_unialg_1(C) )
             => ( ( r1_unialg_2(A,B)
                  & r1_unialg_2(B,C) )
               => r1_unialg_2(A,C) ) ) ) ) ),
    file(unialg_2,t4_unialg_2),
    [interesting(0.00)]).

fof(t5_cqc_lang,theorem,(
    ! [A,B] : 
      ( k1_relat_1(k3_cqc_lang(A,B)) = k1_tarski(A)
      & k2_relat_1(k3_cqc_lang(A,B)) = k1_tarski(B) ) ),
    file(cqc_lang,t5_cqc_lang),
    [interesting(0.00)]).

fof(d24_pboole,definition,(
    ! [A] : 
      ( ( v1_relat_1(A)
        & v1_funct_1(A)
        & v1_funcop_1(A) )
     => ! [B] : 
          ( ( v1_relat_1(B)
            & v1_funct_1(B)
            & v1_funcop_1(B) )
         => ! [C] : 
              ( ( v1_relat_1(C)
                & v1_funct_1(C)
                & v1_funcop_1(C) )
             => ( C = k13_pboole(A,B)
              <=> ( k1_relat_1(C) = k3_xboole_0(k1_relat_1(A),k1_relat_1(B))
                  & ! [D] : 
                      ( r2_hidden(D,k1_relat_1(C))
                     => k1_funct_1(C,D) = k5_relat_1(k1_funct_1(A,D),k1_funct_1(B,D)) ) ) ) ) ) ) ),
    file(pboole,d24_pboole),
    [interesting(0.00)]).

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

fof(d6_funcop_1,definition,(
    ! [A] : 
      ( ( v1_relat_1(A)
        & v1_funct_1(A) )
     => ( v1_funcop_1(A)
      <=> ! [B] : 
            ( r2_hidden(B,k1_relat_1(A))
           => ( v1_relat_1(k1_funct_1(A,B))
              & v1_funct_1(k1_funct_1(A,B)) ) ) ) ) ),
    file(funcop_1,d6_funcop_1),
    [interesting(0.00)]).

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

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

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

fof(d19_pboole,definition,(
    ! [A,B] : 
      ( m1_pboole(B,A)
     => ! [C] : 
          ( m1_pboole(C,k3_finseq_2(A))
         => ( C = k6_pboole(A,B)
          <=> ! [D] : 
                ( m2_finseq_2(D,A,k3_finseq_2(A))
               => k1_funct_1(C,D) = k4_card_3(k5_relat_1(D,B)) ) ) ) ) ),
    file(pboole,d19_pboole),
    [interesting(0.00)]).

fof(d5_card_3,definition,(
    ! [A] : 
      ( ( v1_relat_1(A)
        & v1_funct_1(A) )
     => ! [B] : 
          ( B = k4_card_3(A)
        <=> ! [C] : 
              ( r2_hidden(C,B)
            <=> ? [D] : 
                  ( v1_relat_1(D)
                  & v1_funct_1(D)
                  & C = D
                  & k1_relat_1(D) = k1_relat_1(A)
                  & ! [E] : 
                      ( r2_hidden(E,k1_relat_1(A))
                     => r2_hidden(k1_funct_1(D,E),k1_funct_1(A,E)) ) ) ) ) ) ),
    file(card_3,d5_card_3),
    [interesting(0.00)]).

fof(t2_monoid_1,theorem,(
    ! [A] : 
      ( ( v1_relat_1(A)
        & v1_funct_1(A) )
     => ! [B] : 
          ( ( v1_relat_1(B)
            & v1_funct_1(B) )
         => ! [C] : k5_relat_1(B,k7_relat_1(A,C)) = k5_relat_1(k8_relat_1(C,B),A) ) ) ),
    file(monoid_1,t2_monoid_1),
    [interesting(0.00)]).

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

fof(d1_msuhom_1,definition,(
    ! [A] : 
      ( ( ~ v3_struct_0(A)
        & l1_msualg_1(A) )
     => ! [B] : 
          ( ( ~ v3_struct_0(B)
            & l1_msualg_1(B) )
         => ( r1_msuhom_1(A,B)
          <=> ( r1_tarski(u1_struct_0(A),u1_struct_0(B))
              & r1_tarski(u1_msualg_1(A),u1_msualg_1(B))
              & k2_partfun1(u1_msualg_1(B),k3_finseq_2(u1_struct_0(B)),u2_msualg_1(B),u1_msualg_1(A)) = u2_msualg_1(A)
              & k2_partfun1(u1_msualg_1(B),u1_struct_0(B),u3_msualg_1(B),u1_msualg_1(A)) = u3_msualg_1(A) ) ) ) ) ),
    file(msuhom_1,d1_msuhom_1),
    [interesting(0.00)]).

fof(t28_xboole_1,theorem,(
    ! [A,B] : 
      ( r1_tarski(A,B)
     => k3_xboole_0(A,B) = A ) ),
    file(xboole_1,t28_xboole_1),
    [interesting(0.00)]).

fof(t100_relat_1,theorem,(
    ! [A,B,C] : 
      ( v1_relat_1(C)
     => k7_relat_1(k7_relat_1(C,A),B) = k7_relat_1(C,k3_xboole_0(A,B)) ) ),
    file(relat_1,t100_relat_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(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)]).