:: MSUHOM_1  semantic presentation begin  


















theorem :: MSUHOM_1:1 (Bool  "for" (Set (Var "f")) "," (Set (Var "g")) "being"   ($#m1_hidden :::"Function":::)  (Bool  "for" (Set (Var "C")) "being"    ($#m1_hidden :::"set"::: )    "st" (Bool (Bool (Set   ($#k10_xtuple_0 :::"rng"::: )  (Set (Var "f")))  ($#r1_tarski :::"c="::: )  (Set (Var "C")))) "holds"  (Bool (Set (Set  "(" (Set (Var "g"))  ($#k5_relat_1 :::"|"::: )  (Set (Var "C")) ")" )  ($#k3_relat_1 :::"*"::: )  (Set (Var "f")))  ($#r1_hidden :::"="::: )  (Set (Set (Var "g"))  ($#k3_relat_1 :::"*"::: )  (Set (Var "f")))))) ; 
 
theorem :: MSUHOM_1:2 (Bool  "for" (Set (Var "I")) "being"    ($#m1_hidden :::"set"::: )    (Bool  "for" (Set (Var "C")) "being"   ($#m1_subset_1 :::"Subset":::) "of" (Set (Var "I")) "holds"  (Bool (Set (Set (Var "C"))  ($#k3_finseq_2 :::"*"::: )  )  ($#r1_tarski :::"c="::: )  (Set (Set (Var "I"))  ($#k3_finseq_2 :::"*"::: )  )))) ; 
 
theorem :: MSUHOM_1:3 (Bool  "for" (Set (Var "f")) "being"   ($#m1_hidden :::"Function":::)  (Bool  "for" (Set (Var "C")) "being"    ($#m1_hidden :::"set"::: )    "st" (Bool (Bool (Set (Var "f")) "is"   ($#v1_funcop_1 :::"Function-yielding"::: )  )) "holds"  (Bool (Set (Set (Var "f"))  ($#k5_relat_1 :::"|"::: )  (Set (Var "C"))) "is"   ($#v1_funcop_1 :::"Function-yielding"::: )  ))) ; 
 
theorem :: MSUHOM_1:4 (Bool  "for" (Set (Var "I")) "being"    ($#m1_hidden :::"set"::: )    (Bool  "for" (Set (Var "C")) "being"   ($#m1_subset_1 :::"Subset":::) "of" (Set (Var "I"))  (Bool  "for" (Set (Var "M")) "being"   ($#m1_hidden :::"ManySortedSet":::) "of" (Set (Var "I")) "holds"  (Bool (Set (Set  "(" (Set (Var "M"))  ($#k5_relat_1 :::"|"::: )  (Set (Var "C")) ")" )  ($#k6_finseq_2 :::"#"::: )  )  ($#r1_hidden :::"="::: )  (Set (Set  "(" (Set (Var "M"))  ($#k6_finseq_2 :::"#"::: )  ")" )  ($#k5_relat_1 :::"|"::: )  (Set  "(" (Set (Var "C"))  ($#k3_finseq_2 :::"*"::: )  ")" )))))) ; 
 definitionlet "S", "S9" be  ($#~v2_struct_0  "non"   ($#v2_struct_0 :::"empty"::: )   )    ($#l1_msualg_1 :::"ManySortedSign"::: )  ; pred "S" :::"<="::: "S9" means :: MSUHOM_1:def 1 (Bool  "("  (Bool (Set  "the"  ($#u1_struct_0 :::"carrier"::: )  "of" "S")  ($#r1_tarski :::"c="::: )  (Set  "the"  ($#u1_struct_0 :::"carrier"::: )  "of" "S9")) & (Bool (Set  "the"  ($#u4_struct_0 :::"carrier'"::: )  "of" "S")  ($#r1_tarski :::"c="::: )  (Set  "the"  ($#u4_struct_0 :::"carrier'"::: )  "of" "S9")) & (Bool (Set (Set  "the"  ($#u1_msualg_1 :::"Arity"::: )  "of" "S9")  ($#k2_partfun1 :::"|"::: )  (Set  "the"  ($#u4_struct_0 :::"carrier'"::: )  "of" "S"))  ($#r1_hidden :::"="::: )  (Set  "the"  ($#u1_msualg_1 :::"Arity"::: )  "of" "S")) & (Bool (Set (Set  "the"  ($#u2_msualg_1 :::"ResultSort"::: )  "of" "S9")  ($#k2_partfun1 :::"|"::: )  (Set  "the"  ($#u4_struct_0 :::"carrier'"::: )  "of" "S"))  ($#r1_hidden :::"="::: )  (Set  "the"  ($#u2_msualg_1 :::"ResultSort"::: )  "of" "S"))  ")" ); reflexivity  
(Bool  "for" (Set (Var "S")) "being"  ($#~v2_struct_0  "non"   ($#v2_struct_0 :::"empty"::: )   )    ($#l1_msualg_1 :::"ManySortedSign"::: )   "holds"   (Bool  "("  (Bool (Set  "the"  ($#u1_struct_0 :::"carrier"::: )  "of" (Set (Var "S")))  ($#r1_tarski :::"c="::: )  (Set  "the"  ($#u1_struct_0 :::"carrier"::: )  "of" (Set (Var "S")))) & (Bool (Set  "the"  ($#u4_struct_0 :::"carrier'"::: )  "of" (Set (Var "S")))  ($#r1_tarski :::"c="::: )  (Set  "the"  ($#u4_struct_0 :::"carrier'"::: )  "of" (Set (Var "S")))) & (Bool (Set (Set  "the"  ($#u1_msualg_1 :::"Arity"::: )  "of" (Set (Var "S")))  ($#k2_partfun1 :::"|"::: )  (Set  "the"  ($#u4_struct_0 :::"carrier'"::: )  "of" (Set (Var "S"))))  ($#r1_hidden :::"="::: )  (Set  "the"  ($#u1_msualg_1 :::"Arity"::: )  "of" (Set (Var "S")))) & (Bool (Set (Set  "the"  ($#u2_msualg_1 :::"ResultSort"::: )  "of" (Set (Var "S")))  ($#k2_partfun1 :::"|"::: )  (Set  "the"  ($#u4_struct_0 :::"carrier'"::: )  "of" (Set (Var "S"))))  ($#r1_hidden :::"="::: )  (Set  "the"  ($#u2_msualg_1 :::"ResultSort"::: )  "of" (Set (Var "S"))))  ")" ))
 ; end; 





:: deftheorem    defines :::"<="::: MSUHOM_1:def 1 :  (Bool  "for" (Set (Var "S")) "," (Set (Var "S9")) "being"  ($#~v2_struct_0  "non"   ($#v2_struct_0 :::"empty"::: )   )    ($#l1_msualg_1 :::"ManySortedSign"::: )   "holds"   (Bool  "("  (Bool (Set (Var "S"))  ($#r1_msuhom_1 :::"<="::: )  (Set (Var "S9"))) "iff" (Bool  "("  (Bool (Set  "the"  ($#u1_struct_0 :::"carrier"::: )  "of" (Set (Var "S")))  ($#r1_tarski :::"c="::: )  (Set  "the"  ($#u1_struct_0 :::"carrier"::: )  "of" (Set (Var "S9")))) & (Bool (Set  "the"  ($#u4_struct_0 :::"carrier'"::: )  "of" (Set (Var "S")))  ($#r1_tarski :::"c="::: )  (Set  "the"  ($#u4_struct_0 :::"carrier'"::: )  "of" (Set (Var "S9")))) & (Bool (Set (Set  "the"  ($#u1_msualg_1 :::"Arity"::: )  "of" (Set (Var "S9")))  ($#k2_partfun1 :::"|"::: )  (Set  "the"  ($#u4_struct_0 :::"carrier'"::: )  "of" (Set (Var "S"))))  ($#r1_hidden :::"="::: )  (Set  "the"  ($#u1_msualg_1 :::"Arity"::: )  "of" (Set (Var "S")))) & (Bool (Set (Set  "the"  ($#u2_msualg_1 :::"ResultSort"::: )  "of" (Set (Var "S9")))  ($#k2_partfun1 :::"|"::: )  (Set  "the"  ($#u4_struct_0 :::"carrier'"::: )  "of" (Set (Var "S"))))  ($#r1_hidden :::"="::: )  (Set  "the"  ($#u2_msualg_1 :::"ResultSort"::: )  "of" (Set (Var "S"))))  ")" )  ")" )); 
 
theorem :: MSUHOM_1:5 (Bool  "for" (Set (Var "S")) "," (Set (Var "S9")) "," (Set (Var "S99")) "being"  ($#~v2_struct_0  "non"   ($#v2_struct_0 :::"empty"::: )   )    ($#l1_msualg_1 :::"ManySortedSign"::: )    "st" (Bool (Bool (Set (Var "S"))  ($#r1_msuhom_1 :::"<="::: )  (Set (Var "S9"))) & (Bool (Set (Var "S9"))  ($#r1_msuhom_1 :::"<="::: )  (Set (Var "S99")))) "holds"  (Bool (Set (Var "S"))  ($#r1_msuhom_1 :::"<="::: )  (Set (Var "S99")))) ; 
 
theorem :: MSUHOM_1:6 (Bool  "for" (Set (Var "S")) "," (Set (Var "S9")) "being"  ($#~v2_struct_0  "non"   ($#v2_struct_0 :::"empty"::: )   )    ($#v1_msualg_1 :::"strict"::: )     ($#l1_msualg_1 :::"ManySortedSign"::: )    "st" (Bool (Bool (Set (Var "S"))  ($#r1_msuhom_1 :::"<="::: )  (Set (Var "S9"))) & (Bool (Set (Var "S9"))  ($#r1_msuhom_1 :::"<="::: )  (Set (Var "S")))) "holds"  (Bool (Set (Var "S"))  ($#r1_hidden :::"="::: )  (Set (Var "S9")))) ; 
 
theorem :: MSUHOM_1:7 (Bool  "for" (Set (Var "n")) "being"   ($#m1_hidden :::"Nat":::)  (Bool  "for" (Set (Var "A")) "being"  ($#~v1_xboole_0  "non"   ($#v1_xboole_0 :::"empty"::: )   )    ($#m1_hidden :::"set"::: )    (Bool  "for" (Set (Var "g")) "being"   ($#m1_hidden :::"Function":::)  (Bool  "for" (Set (Var "a")) "being"    ($#m1_subset_1 :::"Element"::: )   "of" (Set (Var "A"))  (Bool  "for" (Set (Var "k")) "being"   ($#m1_hidden :::"Nat":::)  "st" (Bool (Bool (Num 1)  ($#r1_xxreal_0 :::"<="::: )  (Set (Var "k"))) & (Bool (Set (Var "k"))  ($#r1_xxreal_0 :::"<="::: )  (Set (Var "n")))) "holds"  (Bool (Set (Set  "(" (Set (Var "a"))  ($#k16_funcop_1 :::".-->"::: )  (Set (Var "g")) ")" )  ($#k1_funct_1 :::"."::: )  (Set  "(" (Set  "(" (Set (Var "n"))  ($#k5_finseq_2 :::"|->"::: )  (Set (Var "a")) ")" )  ($#k7_partfun1 :::"/."::: )  (Set (Var "k")) ")" ))  ($#r1_hidden :::"="::: )  (Set (Var "g")))))))) ; 
 
theorem :: MSUHOM_1:8 (Bool  "for" (Set (Var "I")) "being"    ($#m1_hidden :::"set"::: )    (Bool  "for" (Set (Var "I0")) "being"   ($#m1_subset_1 :::"Subset":::) "of" (Set (Var "I"))  (Bool  "for" (Set (Var "A")) "," (Set (Var "B")) "being"   ($#m1_hidden :::"ManySortedSet":::) "of" (Set (Var "I"))  (Bool  "for" (Set (Var "F")) "being"    ($#m2_pboole :::"ManySortedFunction"::: )   "of" (Set (Var "A")) "," (Set (Var "B"))  (Bool  "for" (Set (Var "A0")) "," (Set (Var "B0")) "being"   ($#m1_hidden :::"ManySortedSet":::) "of" (Set (Var "I0"))  "st" (Bool (Bool (Set (Var "A0"))  ($#r6_pboole :::"="::: )  (Set (Set (Var "A"))  ($#k5_relat_1 :::"|"::: )  (Set (Var "I0")))) & (Bool (Set (Var "B0"))  ($#r6_pboole :::"="::: )  (Set (Set (Var "B"))  ($#k5_relat_1 :::"|"::: )  (Set (Var "I0"))))) "holds"  (Bool (Set (Set (Var "F"))  ($#k5_relat_1 :::"|"::: )  (Set (Var "I0"))) "is"    ($#m2_pboole :::"ManySortedFunction"::: )   "of" (Set (Var "A0")) "," (Set (Var "B0")))))))) ; 
 definitionlet "S", "S9" be  ($#~v2_struct_0  "non"   ($#v2_struct_0 :::"empty"::: )   )   ($#~v11_struct_0  "non"   ($#v11_struct_0 :::"void"::: )   )    ($#v1_msualg_1 :::"strict"::: )     ($#l1_msualg_1 :::"ManySortedSign"::: )  ; let "A" be   ($#v3_msualg_1 :::"strict"::: )     ($#v4_msualg_1 :::"non-empty"::: )     ($#l3_msualg_1 :::"MSAlgebra"::: )   "over" (Set (Const "S9")); assume 
(Bool (Set (Const "S"))  ($#r1_msuhom_1 :::"<="::: )  (Set (Const "S9")))
 ; func "A" :::"Over"::: "S" ->   ($#v3_msualg_1 :::"strict"::: )     ($#v4_msualg_1 :::"non-empty"::: )     ($#l3_msualg_1 :::"MSAlgebra"::: )   "over" "S" means :: MSUHOM_1:def 2 (Bool  "("  (Bool (Set  "the"  ($#u3_msualg_1 :::"Sorts"::: )  "of" it)  ($#r1_hidden :::"="::: )  (Set (Set  "the"  ($#u3_msualg_1 :::"Sorts"::: )  "of" "A")  ($#k5_relat_1 :::"|"::: )  (Set  "the"  ($#u1_struct_0 :::"carrier"::: )  "of" "S"))) & (Bool (Set  "the"  ($#u4_msualg_1 :::"Charact"::: )  "of" it)  ($#r1_hidden :::"="::: )  (Set (Set  "the"  ($#u4_msualg_1 :::"Charact"::: )  "of" "A")  ($#k5_relat_1 :::"|"::: )  (Set  "the"  ($#u4_struct_0 :::"carrier'"::: )  "of" "S")))  ")" ); end; 








:: deftheorem    defines :::"Over"::: MSUHOM_1:def 2 :  (Bool  "for" (Set (Var "S")) "," (Set (Var "S9")) "being"  ($#~v2_struct_0  "non"   ($#v2_struct_0 :::"empty"::: )   )   ($#~v11_struct_0  "non"   ($#v11_struct_0 :::"void"::: )   )    ($#v1_msualg_1 :::"strict"::: )     ($#l1_msualg_1 :::"ManySortedSign"::: )    (Bool  "for" (Set (Var "A")) "being"   ($#v3_msualg_1 :::"strict"::: )     ($#v4_msualg_1 :::"non-empty"::: )     ($#l3_msualg_1 :::"MSAlgebra"::: )   "over" (Set (Var "S9"))  "st" (Bool (Bool (Set (Var "S"))  ($#r1_msuhom_1 :::"<="::: )  (Set (Var "S9")))) "holds"  (Bool  "for" (Set (Var "b4")) "being"   ($#v3_msualg_1 :::"strict"::: )     ($#v4_msualg_1 :::"non-empty"::: )     ($#l3_msualg_1 :::"MSAlgebra"::: )   "over" (Set (Var "S")) "holds"   (Bool  "("  (Bool (Set (Var "b4"))  ($#r1_hidden :::"="::: )  (Set (Set (Var "A"))  ($#k1_msuhom_1 :::"Over"::: )  (Set (Var "S")))) "iff" (Bool  "("  (Bool (Set  "the"  ($#u3_msualg_1 :::"Sorts"::: )  "of" (Set (Var "b4")))  ($#r1_hidden :::"="::: )  (Set (Set  "the"  ($#u3_msualg_1 :::"Sorts"::: )  "of" (Set (Var "A")))  ($#k5_relat_1 :::"|"::: )  (Set  "the"  ($#u1_struct_0 :::"carrier"::: )  "of" (Set (Var "S"))))) & (Bool (Set  "the"  ($#u4_msualg_1 :::"Charact"::: )  "of" (Set (Var "b4")))  ($#r1_hidden :::"="::: )  (Set (Set  "the"  ($#u4_msualg_1 :::"Charact"::: )  "of" (Set (Var "A")))  ($#k5_relat_1 :::"|"::: )  (Set  "the"  ($#u4_struct_0 :::"carrier'"::: )  "of" (Set (Var "S")))))  ")" )  ")" )))); 
 
theorem :: MSUHOM_1:9 (Bool  "for" (Set (Var "S")) "being"  ($#~v2_struct_0  "non"   ($#v2_struct_0 :::"empty"::: )   )   ($#~v11_struct_0  "non"   ($#v11_struct_0 :::"void"::: )   )    ($#v1_msualg_1 :::"strict"::: )     ($#l1_msualg_1 :::"ManySortedSign"::: )    (Bool  "for" (Set (Var "A")) "being"   ($#v3_msualg_1 :::"strict"::: )     ($#v4_msualg_1 :::"non-empty"::: )     ($#l3_msualg_1 :::"MSAlgebra"::: )   "over" (Set (Var "S")) "holds"  (Bool (Set (Var "A"))  ($#r1_hidden :::"="::: )  (Set (Set (Var "A"))  ($#k1_msuhom_1 :::"Over"::: )  (Set (Var "S")))))) ; 
 
theorem :: MSUHOM_1:10 (Bool  "for" (Set (Var "U1")) "," (Set (Var "U2")) "being"   ($#l1_unialg_1 :::"Universal_Algebra":::)  "st" (Bool (Bool (Set (Var "U1")) "," (Set (Var "U2"))  ($#r1_unialg_2 :::"are_similar"::: )  )) "holds"  (Bool (Set   ($#k6_msualg_1 :::"MSSign"::: )  (Set (Var "U1")))  ($#r1_hidden :::"="::: )  (Set   ($#k6_msualg_1 :::"MSSign"::: )  (Set (Var "U2"))))) ; 
 definitionlet "U1", "U2" be   ($#l1_unialg_1 :::"Universal_Algebra":::); let "h" be   ($#m1_subset_1 :::"Function":::) "of" (Set (Const "U1")) "," (Set (Const "U2")); assume 
(Bool (Set   ($#k6_msualg_1 :::"MSSign"::: )  (Set (Const "U1")))  ($#r1_hidden :::"="::: )  (Set   ($#k6_msualg_1 :::"MSSign"::: )  (Set (Const "U2"))))
 ; func  :::"MSAlg"::: "h" ->   ($#m2_pboole :::"ManySortedFunction":::) "of" (Set  "("  ($#k9_msualg_1 :::"MSAlg"::: )  "U1" ")" ) "," (Set  "(" (Set  "("  ($#k9_msualg_1 :::"MSAlg"::: )  "U2" ")" )  ($#k1_msuhom_1 :::"Over"::: )  (Set  "("  ($#k6_msualg_1 :::"MSSign"::: )  "U1" ")" ) ")" ) equals :: MSUHOM_1:def 3 (Set (Set  ($#k6_numbers :::"0"::: ) )  ($#k16_funcop_1 :::".-->"::: )  "h"); end; 








:: deftheorem    defines :::"MSAlg"::: MSUHOM_1:def 3 :  (Bool  "for" (Set (Var "U1")) "," (Set (Var "U2")) "being"   ($#l1_unialg_1 :::"Universal_Algebra":::)  (Bool  "for" (Set (Var "h")) "being"   ($#m1_subset_1 :::"Function":::) "of" (Set (Var "U1")) "," (Set (Var "U2"))  "st" (Bool (Bool (Set   ($#k6_msualg_1 :::"MSSign"::: )  (Set (Var "U1")))  ($#r1_hidden :::"="::: )  (Set   ($#k6_msualg_1 :::"MSSign"::: )  (Set (Var "U2"))))) "holds"  (Bool (Set   ($#k2_msuhom_1 :::"MSAlg"::: )  (Set (Var "h")))  ($#r1_hidden :::"="::: )  (Set (Set  ($#k6_numbers :::"0"::: ) )  ($#k16_funcop_1 :::".-->"::: )  (Set (Var "h")))))); 
 
theorem :: MSUHOM_1:11 (Bool  "for" (Set (Var "U1")) "," (Set (Var "U2")) "being"   ($#l1_unialg_1 :::"Universal_Algebra":::)  (Bool  "for" (Set (Var "h")) "being"   ($#m1_subset_1 :::"Function":::) "of" (Set (Var "U1")) "," (Set (Var "U2"))  "st" (Bool (Bool (Set (Var "U1")) "," (Set (Var "U2"))  ($#r1_unialg_2 :::"are_similar"::: )  )) "holds"  (Bool  "for" (Set (Var "o")) "being"   ($#m1_subset_1 :::"OperSymbol":::) "of" (Set  "("  ($#k6_msualg_1 :::"MSSign"::: )  (Set (Var "U1")) ")" ) "holds"  (Bool (Set (Set  "("  ($#k2_msuhom_1 :::"MSAlg"::: )  (Set (Var "h")) ")" )  ($#k1_msualg_3 :::"."::: )  (Set  "("  ($#k2_msualg_1 :::"the_result_sort_of"::: )  (Set (Var "o")) ")" ))  ($#r1_funct_2 :::"="::: )  (Set (Var "h")))))) ; 
 
theorem :: MSUHOM_1:12 (Bool  "for" (Set (Var "U1")) "being"   ($#l1_unialg_1 :::"Universal_Algebra":::)  (Bool  "for" (Set (Var "o")) "being"   ($#m1_subset_1 :::"OperSymbol":::) "of" (Set  "("  ($#k6_msualg_1 :::"MSSign"::: )  (Set (Var "U1")) ")" ) "holds"  (Bool (Set   ($#k5_msualg_1 :::"Den"::: )   "(" (Set (Var "o")) "," (Set  "("  ($#k9_msualg_1 :::"MSAlg"::: )  (Set (Var "U1")) ")" ) ")" )  ($#r1_hidden :::"="::: )  (Set (Set  "the"  ($#u1_unialg_1 :::"charact"::: )  "of" (Set (Var "U1")))  ($#k1_funct_1 :::"."::: )  (Set (Var "o")))))) ; 
 
theorem :: MSUHOM_1:13 (Bool  "for" (Set (Var "U1")) "being"   ($#l1_unialg_1 :::"Universal_Algebra":::)  (Bool  "for" (Set (Var "o")) "being"   ($#m1_subset_1 :::"OperSymbol":::) "of" (Set  "("  ($#k6_msualg_1 :::"MSSign"::: )  (Set (Var "U1")) ")" ) "holds"  (Bool (Set   ($#k5_msualg_1 :::"Den"::: )   "(" (Set (Var "o")) "," (Set  "("  ($#k9_msualg_1 :::"MSAlg"::: )  (Set (Var "U1")) ")" ) ")" ) "is"   ($#m5_margrel1 :::"operation":::) "of" (Set (Var "U1"))))) ; 
 
theorem :: MSUHOM_1:14 (Bool  "for" (Set (Var "U1")) "being"   ($#l1_unialg_1 :::"Universal_Algebra":::)  (Bool  "for" (Set (Var "o")) "being"   ($#m1_subset_1 :::"OperSymbol":::) "of" (Set  "("  ($#k6_msualg_1 :::"MSSign"::: )  (Set (Var "U1")) ")" )  (Bool  "for" (Set (Var "y")) "being"    ($#m1_subset_1 :::"Element"::: )   "of" (Set   ($#k3_msualg_1 :::"Args"::: )   "(" (Set (Var "o")) "," (Set  "("  ($#k9_msualg_1 :::"MSAlg"::: )  (Set (Var "U1")) ")" ) ")" ) "holds"  (Bool (Set (Var "y")) "is"    ($#m2_finseq_1 :::"FinSequence"::: )   "of" (Set  "the"  ($#u1_struct_0 :::"carrier"::: )  "of" (Set (Var "U1"))))))) ; 
 
theorem :: MSUHOM_1:15 (Bool  "for" (Set (Var "U1")) "," (Set (Var "U2")) "being"   ($#l1_unialg_1 :::"Universal_Algebra":::)  (Bool  "for" (Set (Var "h")) "being"   ($#m1_subset_1 :::"Function":::) "of" (Set (Var "U1")) "," (Set (Var "U2"))  "st" (Bool (Bool (Set (Var "U1")) "," (Set (Var "U2"))  ($#r1_unialg_2 :::"are_similar"::: )  )) "holds"  (Bool  "for" (Set (Var "o")) "being"   ($#m1_subset_1 :::"OperSymbol":::) "of" (Set  "("  ($#k6_msualg_1 :::"MSSign"::: )  (Set (Var "U1")) ")" )  (Bool  "for" (Set (Var "y")) "being"    ($#m1_subset_1 :::"Element"::: )   "of" (Set   ($#k3_msualg_1 :::"Args"::: )   "(" (Set (Var "o")) "," (Set  "("  ($#k9_msualg_1 :::"MSAlg"::: )  (Set (Var "U1")) ")" ) ")" ) "holds"  (Bool (Set (Set  "("  ($#k2_msuhom_1 :::"MSAlg"::: )  (Set (Var "h")) ")" )  ($#k5_msualg_3 :::"#"::: )  (Set (Var "y")))  ($#r1_hidden :::"="::: )  (Set (Set (Var "h"))  ($#k3_relat_1 :::"*"::: )  (Set (Var "y")))))))) ; 
 
theorem :: MSUHOM_1:16 (Bool  "for" (Set (Var "U1")) "," (Set (Var "U2")) "being"   ($#l1_unialg_1 :::"Universal_Algebra":::)  (Bool  "for" (Set (Var "h")) "being"   ($#m1_subset_1 :::"Function":::) "of" (Set (Var "U1")) "," (Set (Var "U2"))  "st" (Bool (Bool (Set (Var "h"))  ($#r1_alg_1 :::"is_homomorphism"::: )  (Set (Var "U1")) "," (Set (Var "U2")))) "holds"  (Bool (Set   ($#k2_msuhom_1 :::"MSAlg"::: )  (Set (Var "h")))  ($#r1_msualg_3 :::"is_homomorphism"::: )  (Set   ($#k9_msualg_1 :::"MSAlg"::: )  (Set (Var "U1"))) "," (Set (Set  "("  ($#k9_msualg_1 :::"MSAlg"::: )  (Set (Var "U2")) ")" )  ($#k1_msuhom_1 :::"Over"::: )  (Set  "("  ($#k6_msualg_1 :::"MSSign"::: )  (Set (Var "U1")) ")" ))))) ; 
 
theorem :: MSUHOM_1:17 (Bool  "for" (Set (Var "U1")) "," (Set (Var "U2")) "being"   ($#l1_unialg_1 :::"Universal_Algebra":::)  (Bool  "for" (Set (Var "h")) "being"   ($#m1_subset_1 :::"Function":::) "of" (Set (Var "U1")) "," (Set (Var "U2"))  "st" (Bool (Bool (Set (Var "U1")) "," (Set (Var "U2"))  ($#r1_unialg_2 :::"are_similar"::: )  )) "holds"  (Bool (Set   ($#k2_msuhom_1 :::"MSAlg"::: )  (Set (Var "h"))) "is"   ($#m1_hidden :::"ManySortedSet":::) "of" (Set  ($#k1_tarski :::"{"::: ) (Set  ($#k6_numbers :::"0"::: ) ) ($#k1_tarski :::"}"::: ) )))) ; 
 
theorem :: MSUHOM_1:18 (Bool  "for" (Set (Var "U1")) "," (Set (Var "U2")) "being"   ($#l1_unialg_1 :::"Universal_Algebra":::)  (Bool  "for" (Set (Var "h")) "being"   ($#m1_subset_1 :::"Function":::) "of" (Set (Var "U1")) "," (Set (Var "U2"))  "st" (Bool (Bool (Set (Var "h"))  ($#r3_alg_1 :::"is_epimorphism"::: )  (Set (Var "U1")) "," (Set (Var "U2")))) "holds"  (Bool (Set   ($#k2_msuhom_1 :::"MSAlg"::: )  (Set (Var "h")))  ($#r2_msualg_3 :::"is_epimorphism"::: )  (Set   ($#k9_msualg_1 :::"MSAlg"::: )  (Set (Var "U1"))) "," (Set (Set  "("  ($#k9_msualg_1 :::"MSAlg"::: )  (Set (Var "U2")) ")" )  ($#k1_msuhom_1 :::"Over"::: )  (Set  "("  ($#k6_msualg_1 :::"MSSign"::: )  (Set (Var "U1")) ")" ))))) ; 
 
theorem :: MSUHOM_1:19 (Bool  "for" (Set (Var "U1")) "," (Set (Var "U2")) "being"   ($#l1_unialg_1 :::"Universal_Algebra":::)  (Bool  "for" (Set (Var "h")) "being"   ($#m1_subset_1 :::"Function":::) "of" (Set (Var "U1")) "," (Set (Var "U2"))  "st" (Bool (Bool (Set (Var "h"))  ($#r2_alg_1 :::"is_monomorphism"::: )  (Set (Var "U1")) "," (Set (Var "U2")))) "holds"  (Bool (Set   ($#k2_msuhom_1 :::"MSAlg"::: )  (Set (Var "h")))  ($#r3_msualg_3 :::"is_monomorphism"::: )  (Set   ($#k9_msualg_1 :::"MSAlg"::: )  (Set (Var "U1"))) "," (Set (Set  "("  ($#k9_msualg_1 :::"MSAlg"::: )  (Set (Var "U2")) ")" )  ($#k1_msuhom_1 :::"Over"::: )  (Set  "("  ($#k6_msualg_1 :::"MSSign"::: )  (Set (Var "U1")) ")" ))))) ; 
 
theorem :: MSUHOM_1:20 (Bool  "for" (Set (Var "U1")) "," (Set (Var "U2")) "being"   ($#l1_unialg_1 :::"Universal_Algebra":::)  (Bool  "for" (Set (Var "h")) "being"   ($#m1_subset_1 :::"Function":::) "of" (Set (Var "U1")) "," (Set (Var "U2"))  "st" (Bool (Bool (Set (Var "h"))  ($#r4_alg_1 :::"is_isomorphism"::: )  (Set (Var "U1")) "," (Set (Var "U2")))) "holds"  (Bool (Set   ($#k2_msuhom_1 :::"MSAlg"::: )  (Set (Var "h")))  ($#r4_msualg_3 :::"is_isomorphism"::: )  (Set   ($#k9_msualg_1 :::"MSAlg"::: )  (Set (Var "U1"))) "," (Set (Set  "("  ($#k9_msualg_1 :::"MSAlg"::: )  (Set (Var "U2")) ")" )  ($#k1_msuhom_1 :::"Over"::: )  (Set  "("  ($#k6_msualg_1 :::"MSSign"::: )  (Set (Var "U1")) ")" ))))) ; 
 
theorem :: MSUHOM_1:21 (Bool  "for" (Set (Var "U1")) "," (Set (Var "U2")) "being"   ($#l1_unialg_1 :::"Universal_Algebra":::)  (Bool  "for" (Set (Var "h")) "being"   ($#m1_subset_1 :::"Function":::) "of" (Set (Var "U1")) "," (Set (Var "U2"))  "st" (Bool (Bool (Set (Var "U1")) "," (Set (Var "U2"))  ($#r1_unialg_2 :::"are_similar"::: )  ) & (Bool (Set   ($#k2_msuhom_1 :::"MSAlg"::: )  (Set (Var "h")))  ($#r1_msualg_3 :::"is_homomorphism"::: )  (Set   ($#k9_msualg_1 :::"MSAlg"::: )  (Set (Var "U1"))) "," (Set (Set  "("  ($#k9_msualg_1 :::"MSAlg"::: )  (Set (Var "U2")) ")" )  ($#k1_msuhom_1 :::"Over"::: )  (Set  "("  ($#k6_msualg_1 :::"MSSign"::: )  (Set (Var "U1")) ")" )))) "holds"  (Bool (Set (Var "h"))  ($#r1_alg_1 :::"is_homomorphism"::: )  (Set (Var "U1")) "," (Set (Var "U2"))))) ; 
 
theorem :: MSUHOM_1:22 (Bool  "for" (Set (Var "U1")) "," (Set (Var "U2")) "being"   ($#l1_unialg_1 :::"Universal_Algebra":::)  (Bool  "for" (Set (Var "h")) "being"   ($#m1_subset_1 :::"Function":::) "of" (Set (Var "U1")) "," (Set (Var "U2"))  "st" (Bool (Bool (Set (Var "U1")) "," (Set (Var "U2"))  ($#r1_unialg_2 :::"are_similar"::: )  ) & (Bool (Set   ($#k2_msuhom_1 :::"MSAlg"::: )  (Set (Var "h")))  ($#r2_msualg_3 :::"is_epimorphism"::: )  (Set   ($#k9_msualg_1 :::"MSAlg"::: )  (Set (Var "U1"))) "," (Set (Set  "("  ($#k9_msualg_1 :::"MSAlg"::: )  (Set (Var "U2")) ")" )  ($#k1_msuhom_1 :::"Over"::: )  (Set  "("  ($#k6_msualg_1 :::"MSSign"::: )  (Set (Var "U1")) ")" )))) "holds"  (Bool (Set (Var "h"))  ($#r3_alg_1 :::"is_epimorphism"::: )  (Set (Var "U1")) "," (Set (Var "U2"))))) ; 
 
theorem :: MSUHOM_1:23 (Bool  "for" (Set (Var "U1")) "," (Set (Var "U2")) "being"   ($#l1_unialg_1 :::"Universal_Algebra":::)  (Bool  "for" (Set (Var "h")) "being"   ($#m1_subset_1 :::"Function":::) "of" (Set (Var "U1")) "," (Set (Var "U2"))  "st" (Bool (Bool (Set (Var "U1")) "," (Set (Var "U2"))  ($#r1_unialg_2 :::"are_similar"::: )  ) & (Bool (Set   ($#k2_msuhom_1 :::"MSAlg"::: )  (Set (Var "h")))  ($#r3_msualg_3 :::"is_monomorphism"::: )  (Set   ($#k9_msualg_1 :::"MSAlg"::: )  (Set (Var "U1"))) "," (Set (Set  "("  ($#k9_msualg_1 :::"MSAlg"::: )  (Set (Var "U2")) ")" )  ($#k1_msuhom_1 :::"Over"::: )  (Set  "("  ($#k6_msualg_1 :::"MSSign"::: )  (Set (Var "U1")) ")" )))) "holds"  (Bool (Set (Var "h"))  ($#r2_alg_1 :::"is_monomorphism"::: )  (Set (Var "U1")) "," (Set (Var "U2"))))) ; 
 
theorem :: MSUHOM_1:24 (Bool  "for" (Set (Var "U1")) "," (Set (Var "U2")) "being"   ($#l1_unialg_1 :::"Universal_Algebra":::)  (Bool  "for" (Set (Var "h")) "being"   ($#m1_subset_1 :::"Function":::) "of" (Set (Var "U1")) "," (Set (Var "U2"))  "st" (Bool (Bool (Set (Var "U1")) "," (Set (Var "U2"))  ($#r1_unialg_2 :::"are_similar"::: )  ) & (Bool (Set   ($#k2_msuhom_1 :::"MSAlg"::: )  (Set (Var "h")))  ($#r4_msualg_3 :::"is_isomorphism"::: )  (Set   ($#k9_msualg_1 :::"MSAlg"::: )  (Set (Var "U1"))) "," (Set (Set  "("  ($#k9_msualg_1 :::"MSAlg"::: )  (Set (Var "U2")) ")" )  ($#k1_msuhom_1 :::"Over"::: )  (Set  "("  ($#k6_msualg_1 :::"MSSign"::: )  (Set (Var "U1")) ")" )))) "holds"  (Bool (Set (Var "h"))  ($#r4_alg_1 :::"is_isomorphism"::: )  (Set (Var "U1")) "," (Set (Var "U2"))))) ; 
 
theorem :: MSUHOM_1:25 (Bool  "for" (Set (Var "U1")) "being"   ($#l1_unialg_1 :::"Universal_Algebra":::) "holds"  (Bool (Set   ($#k2_msuhom_1 :::"MSAlg"::: )  (Set  "("  ($#k6_partfun1 :::"id"::: )  (Set  "the"  ($#u1_struct_0 :::"carrier"::: )  "of" (Set (Var "U1"))) ")" ))  ($#r8_pboole :::"="::: )  (Set   ($#k2_msualg_3 :::"id"::: )  (Set  "the"  ($#u3_msualg_1 :::"Sorts"::: )  "of" (Set  "("  ($#k9_msualg_1 :::"MSAlg"::: )  (Set (Var "U1")) ")" ))))) ; 
 
theorem :: MSUHOM_1:26 (Bool  "for" (Set (Var "U1")) "," (Set (Var "U2")) "," (Set (Var "U3")) "being"   ($#l1_unialg_1 :::"Universal_Algebra":::)  "st" (Bool (Bool (Set (Var "U1")) "," (Set (Var "U2"))  ($#r1_unialg_2 :::"are_similar"::: )  ) & (Bool (Set (Var "U2")) "," (Set (Var "U3"))  ($#r1_unialg_2 :::"are_similar"::: )  )) "holds"  (Bool  "for" (Set (Var "h1")) "being"   ($#m1_subset_1 :::"Function":::) "of" (Set (Var "U1")) "," (Set (Var "U2"))  (Bool  "for" (Set (Var "h2")) "being"   ($#m1_subset_1 :::"Function":::) "of" (Set (Var "U2")) "," (Set (Var "U3")) "holds"  (Bool (Set (Set  "("  ($#k2_msuhom_1 :::"MSAlg"::: )  (Set (Var "h2")) ")" )  ($#k8_pboole :::"**"::: )  (Set  "("  ($#k2_msuhom_1 :::"MSAlg"::: )  (Set (Var "h1")) ")" ))  ($#r1_hidden :::"="::: )  (Set   ($#k2_msuhom_1 :::"MSAlg"::: )  (Set  "(" (Set (Var "h2"))  ($#k1_partfun1 :::"*"::: )  (Set (Var "h1")) ")" )))))) ;