:: ENDALG  semantic presentation begin  


definitionlet "UA" be   ($#l1_unialg_1 :::"Universal_Algebra":::); func  :::"UAEnd"::: "UA" ->    ($#m1_funct_2 :::"FUNCTION_DOMAIN"::: )   "of" (Set  "the"  ($#u1_struct_0 :::"carrier"::: )  "of" "UA") "," (Set  "the"  ($#u1_struct_0 :::"carrier"::: )  "of" "UA") means :: ENDALG:def 1 (Bool  "for" (Set (Var "h")) "being"   ($#m1_subset_1 :::"Function":::) "of" "UA" "," "UA" "holds"   (Bool  "("  (Bool (Set (Var "h"))  ($#r2_hidden :::"in"::: )  it) "iff" (Bool (Set (Var "h"))  ($#r1_alg_1 :::"is_homomorphism"::: )  "UA" "," "UA")  ")" )); end; 





:: deftheorem    defines :::"UAEnd"::: ENDALG:def 1 :  (Bool  "for" (Set (Var "UA")) "being"   ($#l1_unialg_1 :::"Universal_Algebra":::)  (Bool  "for" (Set (Var "b2")) "being"    ($#m1_funct_2 :::"FUNCTION_DOMAIN"::: )   "of" (Set  "the"  ($#u1_struct_0 :::"carrier"::: )  "of" (Set (Var "UA"))) "," (Set  "the"  ($#u1_struct_0 :::"carrier"::: )  "of" (Set (Var "UA"))) "holds"   (Bool  "("  (Bool (Set (Var "b2"))  ($#r1_hidden :::"="::: )  (Set   ($#k1_endalg :::"UAEnd"::: )  (Set (Var "UA")))) "iff" (Bool  "for" (Set (Var "h")) "being"   ($#m1_subset_1 :::"Function":::) "of" (Set (Var "UA")) "," (Set (Var "UA")) "holds"   (Bool  "("  (Bool (Set (Var "h"))  ($#r2_hidden :::"in"::: )  (Set (Var "b2"))) "iff" (Bool (Set (Var "h"))  ($#r1_alg_1 :::"is_homomorphism"::: )  (Set (Var "UA")) "," (Set (Var "UA")))  ")" ))  ")" ))); 
 
theorem :: ENDALG:1 (Bool  "for" (Set (Var "UA")) "being"   ($#l1_unialg_1 :::"Universal_Algebra":::) "holds"  (Bool (Set   ($#k1_endalg :::"UAEnd"::: )  (Set (Var "UA")))  ($#r1_tarski :::"c="::: )  (Set   ($#k9_funct_2 :::"Funcs"::: )   "(" (Set  "the"  ($#u1_struct_0 :::"carrier"::: )  "of" (Set (Var "UA"))) "," (Set  "the"  ($#u1_struct_0 :::"carrier"::: )  "of" (Set (Var "UA"))) ")" ))) ; 
 
theorem :: ENDALG:2 (Bool  "for" (Set (Var "UA")) "being"   ($#l1_unialg_1 :::"Universal_Algebra":::) "holds"  (Bool (Set   ($#k6_partfun1 :::"id"::: )  (Set  "the"  ($#u1_struct_0 :::"carrier"::: )  "of" (Set (Var "UA"))))  ($#r2_hidden :::"in"::: )  (Set   ($#k1_endalg :::"UAEnd"::: )  (Set (Var "UA"))))) ; 
 
theorem :: ENDALG:3 (Bool  "for" (Set (Var "UA")) "being"   ($#l1_unialg_1 :::"Universal_Algebra":::)  (Bool  "for" (Set (Var "f1")) "," (Set (Var "f2")) "being"    ($#m2_funct_2 :::"Element"::: )   "of" (Set   ($#k1_endalg :::"UAEnd"::: )  (Set (Var "UA"))) "holds"  (Bool (Set (Set (Var "f1"))  ($#k1_partfun1 :::"*"::: )  (Set (Var "f2")))  ($#r2_hidden :::"in"::: )  (Set   ($#k1_endalg :::"UAEnd"::: )  (Set (Var "UA")))))) ; 
 definitionlet "UA" be   ($#l1_unialg_1 :::"Universal_Algebra":::); func  :::"UAEndComp"::: "UA" ->   ($#m1_subset_1 :::"BinOp":::) "of" (Set  "("  ($#k1_endalg :::"UAEnd"::: )  "UA" ")" ) means :: ENDALG:def 2 (Bool  "for" (Set (Var "x")) "," (Set (Var "y")) "being"    ($#m2_funct_2 :::"Element"::: )   "of" (Set   ($#k1_endalg :::"UAEnd"::: )  "UA") "holds"  (Bool (Set it  ($#k5_binop_1 :::"."::: )   "(" (Set (Var "x")) "," (Set (Var "y")) ")" )  ($#r1_hidden :::"="::: )  (Set (Set (Var "y"))  ($#k1_partfun1 :::"*"::: )  (Set (Var "x"))))); end; 





:: deftheorem    defines :::"UAEndComp"::: ENDALG:def 2 :  (Bool  "for" (Set (Var "UA")) "being"   ($#l1_unialg_1 :::"Universal_Algebra":::)  (Bool  "for" (Set (Var "b2")) "being"   ($#m1_subset_1 :::"BinOp":::) "of" (Set  "("  ($#k1_endalg :::"UAEnd"::: )  (Set (Var "UA")) ")" ) "holds"   (Bool  "("  (Bool (Set (Var "b2"))  ($#r1_hidden :::"="::: )  (Set   ($#k2_endalg :::"UAEndComp"::: )  (Set (Var "UA")))) "iff" (Bool  "for" (Set (Var "x")) "," (Set (Var "y")) "being"    ($#m2_funct_2 :::"Element"::: )   "of" (Set   ($#k1_endalg :::"UAEnd"::: )  (Set (Var "UA"))) "holds"  (Bool (Set (Set (Var "b2"))  ($#k5_binop_1 :::"."::: )   "(" (Set (Var "x")) "," (Set (Var "y")) ")" )  ($#r1_hidden :::"="::: )  (Set (Set (Var "y"))  ($#k1_partfun1 :::"*"::: )  (Set (Var "x")))))  ")" ))); 
 definitionlet "UA" be   ($#l1_unialg_1 :::"Universal_Algebra":::); func  :::"UAEndMonoid"::: "UA" ->   ($#v22_algstr_0 :::"strict"::: )     ($#l4_algstr_0 :::"multLoopStr"::: )   means :: ENDALG:def 3 (Bool  "("  (Bool (Set  "the"  ($#u1_struct_0 :::"carrier"::: )  "of" it)  ($#r1_hidden :::"="::: )  (Set   ($#k1_endalg :::"UAEnd"::: )  "UA")) & (Bool (Set  "the"  ($#u2_algstr_0 :::"multF"::: )  "of" it)  ($#r1_hidden :::"="::: )  (Set   ($#k2_endalg :::"UAEndComp"::: )  "UA")) & (Bool (Set   ($#k5_struct_0 :::"1."::: )  it)  ($#r1_hidden :::"="::: )  (Set   ($#k6_partfun1 :::"id"::: )  (Set  "the"  ($#u1_struct_0 :::"carrier"::: )  "of" "UA")))  ")" ); end; 





:: deftheorem    defines :::"UAEndMonoid"::: ENDALG:def 3 :  (Bool  "for" (Set (Var "UA")) "being"   ($#l1_unialg_1 :::"Universal_Algebra":::)  (Bool  "for" (Set (Var "b2")) "being"   ($#v22_algstr_0 :::"strict"::: )     ($#l4_algstr_0 :::"multLoopStr"::: )   "holds"   (Bool  "("  (Bool (Set (Var "b2"))  ($#r1_hidden :::"="::: )  (Set   ($#k3_endalg :::"UAEndMonoid"::: )  (Set (Var "UA")))) "iff" (Bool  "("  (Bool (Set  "the"  ($#u1_struct_0 :::"carrier"::: )  "of" (Set (Var "b2")))  ($#r1_hidden :::"="::: )  (Set   ($#k1_endalg :::"UAEnd"::: )  (Set (Var "UA")))) & (Bool (Set  "the"  ($#u2_algstr_0 :::"multF"::: )  "of" (Set (Var "b2")))  ($#r1_hidden :::"="::: )  (Set   ($#k2_endalg :::"UAEndComp"::: )  (Set (Var "UA")))) & (Bool (Set   ($#k5_struct_0 :::"1."::: )  (Set (Var "b2")))  ($#r1_hidden :::"="::: )  (Set   ($#k6_partfun1 :::"id"::: )  (Set  "the"  ($#u1_struct_0 :::"carrier"::: )  "of" (Set (Var "UA")))))  ")" )  ")" ))); 
 registrationlet "UA" be   ($#l1_unialg_1 :::"Universal_Algebra":::); 
cluster (Set   ($#k3_endalg :::"UAEndMonoid"::: )  "UA") ->  ($#~v2_struct_0  "non"   ($#v2_struct_0 :::"empty"::: )   )    ($#v22_algstr_0 :::"strict"::: )   ; 
end; registrationlet "UA" be   ($#l1_unialg_1 :::"Universal_Algebra":::); 
cluster (Set   ($#k3_endalg :::"UAEndMonoid"::: )  "UA") ->   ($#v22_algstr_0 :::"strict"::: )     ($#v3_group_1 :::"associative"::: )     ($#v4_vectsp_1 :::"well-unital"::: )   ; 
end; 
theorem :: ENDALG:4 (Bool  "for" (Set (Var "UA")) "being"   ($#l1_unialg_1 :::"Universal_Algebra":::)  (Bool  "for" (Set (Var "x")) "," (Set (Var "y")) "being"   ($#m1_subset_1 :::"Element":::) "of" (Set  "("  ($#k3_endalg :::"UAEndMonoid"::: )  (Set (Var "UA")) ")" )  (Bool  "for" (Set (Var "f")) "," (Set (Var "g")) "being"    ($#m2_funct_2 :::"Element"::: )   "of" (Set   ($#k1_endalg :::"UAEnd"::: )  (Set (Var "UA")))  "st" (Bool (Bool (Set (Var "x"))  ($#r1_hidden :::"="::: )  (Set (Var "f"))) & (Bool (Set (Var "y"))  ($#r1_hidden :::"="::: )  (Set (Var "g")))) "holds"  (Bool (Set (Set (Var "x"))  ($#k6_algstr_0 :::"*"::: )  (Set (Var "y")))  ($#r1_hidden :::"="::: )  (Set (Set (Var "g"))  ($#k1_partfun1 :::"*"::: )  (Set (Var "f"))))))) ; 
 
theorem :: ENDALG:5 (Bool  "for" (Set (Var "UA")) "being"   ($#l1_unialg_1 :::"Universal_Algebra":::) "holds"  (Bool (Set   ($#k6_partfun1 :::"id"::: )  (Set  "the"  ($#u1_struct_0 :::"carrier"::: )  "of" (Set (Var "UA"))))  ($#r1_hidden :::"="::: )  (Set   ($#k1_group_1 :::"1_"::: )  (Set  "("  ($#k3_endalg :::"UAEndMonoid"::: )  (Set (Var "UA")) ")" )))) ; 
 





definitionlet "S" be  ($#~v2_struct_0  "non"   ($#v2_struct_0 :::"empty"::: )   )   ($#~v11_struct_0  "non"   ($#v11_struct_0 :::"void"::: )   )    ($#l1_msualg_1 :::"ManySortedSign"::: )  ; let "U1" be   ($#v4_msualg_1 :::"non-empty"::: )     ($#l3_msualg_1 :::"MSAlgebra"::: )   "over" (Set (Const "S")); func  :::"MSAEnd"::: "U1" ->   ($#m1_subset_1 :::"MSFunctionSet":::) "of" "U1" "," "U1" means :: ENDALG:def 4 (Bool  "("  (Bool  "("   "for" (Set (Var "f")) "being"    ($#m1_autalg_1 :::"Element"::: )   "of" it "holds"  (Bool (Set (Var "f")) "is"   ($#m2_pboole :::"ManySortedFunction":::) "of" "U1" "," "U1")  ")" ) & (Bool  "("   "for" (Set (Var "h")) "being"   ($#m2_pboole :::"ManySortedFunction":::) "of" "U1" "," "U1" "holds"   (Bool  "("  (Bool (Set (Var "h"))  ($#r2_hidden :::"in"::: )  it) "iff" (Bool (Set (Var "h"))  ($#r1_msualg_3 :::"is_homomorphism"::: )  "U1" "," "U1")  ")" )  ")" )  ")" ); end; 






:: deftheorem    defines :::"MSAEnd"::: ENDALG:def 4 :  (Bool  "for" (Set (Var "S")) "being"  ($#~v2_struct_0  "non"   ($#v2_struct_0 :::"empty"::: )   )   ($#~v11_struct_0  "non"   ($#v11_struct_0 :::"void"::: )   )    ($#l1_msualg_1 :::"ManySortedSign"::: )    (Bool  "for" (Set (Var "U1")) "being"   ($#v4_msualg_1 :::"non-empty"::: )     ($#l3_msualg_1 :::"MSAlgebra"::: )   "over" (Set (Var "S"))  (Bool  "for" (Set (Var "b3")) "being"   ($#m1_subset_1 :::"MSFunctionSet":::) "of" (Set (Var "U1")) "," (Set (Var "U1")) "holds"   (Bool  "("  (Bool (Set (Var "b3"))  ($#r1_hidden :::"="::: )  (Set   ($#k4_endalg :::"MSAEnd"::: )  (Set (Var "U1")))) "iff" (Bool  "("  (Bool  "("   "for" (Set (Var "f")) "being"    ($#m1_autalg_1 :::"Element"::: )   "of" (Set (Var "b3")) "holds"  (Bool (Set (Var "f")) "is"   ($#m2_pboole :::"ManySortedFunction":::) "of" (Set (Var "U1")) "," (Set (Var "U1")))  ")" ) & (Bool  "("   "for" (Set (Var "h")) "being"   ($#m2_pboole :::"ManySortedFunction":::) "of" (Set (Var "U1")) "," (Set (Var "U1")) "holds"   (Bool  "("  (Bool (Set (Var "h"))  ($#r2_hidden :::"in"::: )  (Set (Var "b3"))) "iff" (Bool (Set (Var "h"))  ($#r1_msualg_3 :::"is_homomorphism"::: )  (Set (Var "U1")) "," (Set (Var "U1")))  ")" )  ")" )  ")" )  ")" )))); 
 
theorem :: ENDALG:6 (Bool  "for" (Set (Var "S")) "being"  ($#~v2_struct_0  "non"   ($#v2_struct_0 :::"empty"::: )   )   ($#~v11_struct_0  "non"   ($#v11_struct_0 :::"void"::: )   )    ($#l1_msualg_1 :::"ManySortedSign"::: )    (Bool  "for" (Set (Var "U1")) "being"   ($#v4_msualg_1 :::"non-empty"::: )     ($#l3_msualg_1 :::"MSAlgebra"::: )   "over" (Set (Var "S")) "holds"  (Bool (Set   ($#k4_endalg :::"MSAEnd"::: )  (Set (Var "U1")))  ($#r1_tarski :::"c="::: )  (Set   ($#k4_autalg_1 :::"MSFuncs"::: )   "(" (Set  "the"  ($#u3_msualg_1 :::"Sorts"::: )  "of" (Set (Var "U1"))) "," (Set  "the"  ($#u3_msualg_1 :::"Sorts"::: )  "of" (Set (Var "U1"))) ")" )))) ; 
 
theorem :: ENDALG:7 (Bool  "for" (Set (Var "S")) "being"  ($#~v2_struct_0  "non"   ($#v2_struct_0 :::"empty"::: )   )   ($#~v11_struct_0  "non"   ($#v11_struct_0 :::"void"::: )   )    ($#l1_msualg_1 :::"ManySortedSign"::: )    (Bool  "for" (Set (Var "U1")) "being"   ($#v4_msualg_1 :::"non-empty"::: )     ($#l3_msualg_1 :::"MSAlgebra"::: )   "over" (Set (Var "S")) "holds"  (Bool (Set   ($#k2_msualg_3 :::"id"::: )  (Set  "the"  ($#u3_msualg_1 :::"Sorts"::: )  "of" (Set (Var "U1"))))  ($#r2_hidden :::"in"::: )  (Set   ($#k4_endalg :::"MSAEnd"::: )  (Set (Var "U1")))))) ; 
 
theorem :: ENDALG:8 (Bool  "for" (Set (Var "S")) "being"  ($#~v2_struct_0  "non"   ($#v2_struct_0 :::"empty"::: )   )   ($#~v11_struct_0  "non"   ($#v11_struct_0 :::"void"::: )   )    ($#l1_msualg_1 :::"ManySortedSign"::: )    (Bool  "for" (Set (Var "U1")) "being"   ($#v4_msualg_1 :::"non-empty"::: )     ($#l3_msualg_1 :::"MSAlgebra"::: )   "over" (Set (Var "S"))  (Bool  "for" (Set (Var "f1")) "," (Set (Var "f2")) "being"    ($#m1_autalg_1 :::"Element"::: )   "of" (Set   ($#k4_endalg :::"MSAEnd"::: )  (Set (Var "U1"))) "holds"  (Bool (Set (Set (Var "f1"))  ($#k3_msualg_3 :::"**"::: )  (Set (Var "f2")))  ($#r2_hidden :::"in"::: )  (Set   ($#k4_endalg :::"MSAEnd"::: )  (Set (Var "U1"))))))) ; 
 
theorem :: ENDALG:9 (Bool  "for" (Set (Var "UA")) "being"   ($#l1_unialg_1 :::"Universal_Algebra":::)  (Bool  "for" (Set (Var "F")) "being"   ($#m2_pboole :::"ManySortedFunction":::) "of" (Set  "("  ($#k9_msualg_1 :::"MSAlg"::: )  (Set (Var "UA")) ")" ) "," (Set  "("  ($#k9_msualg_1 :::"MSAlg"::: )  (Set (Var "UA")) ")" )  (Bool  "for" (Set (Var "f")) "being"    ($#m2_funct_2 :::"Element"::: )   "of" (Set   ($#k1_endalg :::"UAEnd"::: )  (Set (Var "UA")))  "st" (Bool (Bool (Set (Var "F"))  ($#r1_hidden :::"="::: )  (Set (Set  ($#k6_numbers :::"0"::: ) )  ($#k16_funcop_1 :::".-->"::: )  (Set (Var "f"))))) "holds"  (Bool (Set (Var "F"))  ($#r2_hidden :::"in"::: )  (Set   ($#k4_endalg :::"MSAEnd"::: )  (Set  "("  ($#k9_msualg_1 :::"MSAlg"::: )  (Set (Var "UA")) ")" )))))) ; 
 definitionlet "S" be  ($#~v2_struct_0  "non"   ($#v2_struct_0 :::"empty"::: )   )   ($#~v11_struct_0  "non"   ($#v11_struct_0 :::"void"::: )   )    ($#l1_msualg_1 :::"ManySortedSign"::: )  ; let "U1" be   ($#v4_msualg_1 :::"non-empty"::: )     ($#l3_msualg_1 :::"MSAlgebra"::: )   "over" (Set (Const "S")); func  :::"MSAEndComp"::: "U1" ->   ($#m1_subset_1 :::"BinOp":::) "of" (Set  "("  ($#k4_endalg :::"MSAEnd"::: )  "U1" ")" ) means :: ENDALG:def 5 (Bool  "for" (Set (Var "x")) "," (Set (Var "y")) "being"    ($#m1_autalg_1 :::"Element"::: )   "of" (Set   ($#k4_endalg :::"MSAEnd"::: )  "U1") "holds"  (Bool (Set it  ($#k5_binop_1 :::"."::: )   "(" (Set (Var "x")) "," (Set (Var "y")) ")" )  ($#r1_hidden :::"="::: )  (Set (Set (Var "y"))  ($#k3_msualg_3 :::"**"::: )  (Set (Var "x"))))); end; 






:: deftheorem    defines :::"MSAEndComp"::: ENDALG:def 5 :  (Bool  "for" (Set (Var "S")) "being"  ($#~v2_struct_0  "non"   ($#v2_struct_0 :::"empty"::: )   )   ($#~v11_struct_0  "non"   ($#v11_struct_0 :::"void"::: )   )    ($#l1_msualg_1 :::"ManySortedSign"::: )    (Bool  "for" (Set (Var "U1")) "being"   ($#v4_msualg_1 :::"non-empty"::: )     ($#l3_msualg_1 :::"MSAlgebra"::: )   "over" (Set (Var "S"))  (Bool  "for" (Set (Var "b3")) "being"   ($#m1_subset_1 :::"BinOp":::) "of" (Set  "("  ($#k4_endalg :::"MSAEnd"::: )  (Set (Var "U1")) ")" ) "holds"   (Bool  "("  (Bool (Set (Var "b3"))  ($#r1_hidden :::"="::: )  (Set   ($#k5_endalg :::"MSAEndComp"::: )  (Set (Var "U1")))) "iff" (Bool  "for" (Set (Var "x")) "," (Set (Var "y")) "being"    ($#m1_autalg_1 :::"Element"::: )   "of" (Set   ($#k4_endalg :::"MSAEnd"::: )  (Set (Var "U1"))) "holds"  (Bool (Set (Set (Var "b3"))  ($#k5_binop_1 :::"."::: )   "(" (Set (Var "x")) "," (Set (Var "y")) ")" )  ($#r1_hidden :::"="::: )  (Set (Set (Var "y"))  ($#k3_msualg_3 :::"**"::: )  (Set (Var "x")))))  ")" )))); 
 definitionlet "S" be  ($#~v2_struct_0  "non"   ($#v2_struct_0 :::"empty"::: )   )   ($#~v11_struct_0  "non"   ($#v11_struct_0 :::"void"::: )   )    ($#l1_msualg_1 :::"ManySortedSign"::: )  ; let "U1" be   ($#v4_msualg_1 :::"non-empty"::: )     ($#l3_msualg_1 :::"MSAlgebra"::: )   "over" (Set (Const "S")); func  :::"MSAEndMonoid"::: "U1" ->   ($#v22_algstr_0 :::"strict"::: )     ($#l4_algstr_0 :::"multLoopStr"::: )   means :: ENDALG:def 6 (Bool  "("  (Bool (Set  "the"  ($#u1_struct_0 :::"carrier"::: )  "of" it)  ($#r1_hidden :::"="::: )  (Set   ($#k4_endalg :::"MSAEnd"::: )  "U1")) & (Bool (Set  "the"  ($#u2_algstr_0 :::"multF"::: )  "of" it)  ($#r1_hidden :::"="::: )  (Set   ($#k5_endalg :::"MSAEndComp"::: )  "U1")) & (Bool (Set   ($#k5_struct_0 :::"1."::: )  it)  ($#r1_hidden :::"="::: )  (Set   ($#k2_msualg_3 :::"id"::: )  (Set  "the"  ($#u3_msualg_1 :::"Sorts"::: )  "of" "U1")))  ")" ); end; 






:: deftheorem    defines :::"MSAEndMonoid"::: ENDALG:def 6 :  (Bool  "for" (Set (Var "S")) "being"  ($#~v2_struct_0  "non"   ($#v2_struct_0 :::"empty"::: )   )   ($#~v11_struct_0  "non"   ($#v11_struct_0 :::"void"::: )   )    ($#l1_msualg_1 :::"ManySortedSign"::: )    (Bool  "for" (Set (Var "U1")) "being"   ($#v4_msualg_1 :::"non-empty"::: )     ($#l3_msualg_1 :::"MSAlgebra"::: )   "over" (Set (Var "S"))  (Bool  "for" (Set (Var "b3")) "being"   ($#v22_algstr_0 :::"strict"::: )     ($#l4_algstr_0 :::"multLoopStr"::: )   "holds"   (Bool  "("  (Bool (Set (Var "b3"))  ($#r1_hidden :::"="::: )  (Set   ($#k6_endalg :::"MSAEndMonoid"::: )  (Set (Var "U1")))) "iff" (Bool  "("  (Bool (Set  "the"  ($#u1_struct_0 :::"carrier"::: )  "of" (Set (Var "b3")))  ($#r1_hidden :::"="::: )  (Set   ($#k4_endalg :::"MSAEnd"::: )  (Set (Var "U1")))) & (Bool (Set  "the"  ($#u2_algstr_0 :::"multF"::: )  "of" (Set (Var "b3")))  ($#r1_hidden :::"="::: )  (Set   ($#k5_endalg :::"MSAEndComp"::: )  (Set (Var "U1")))) & (Bool (Set   ($#k5_struct_0 :::"1."::: )  (Set (Var "b3")))  ($#r1_hidden :::"="::: )  (Set   ($#k2_msualg_3 :::"id"::: )  (Set  "the"  ($#u3_msualg_1 :::"Sorts"::: )  "of" (Set (Var "U1")))))  ")" )  ")" )))); 
 registrationlet "S" be  ($#~v2_struct_0  "non"   ($#v2_struct_0 :::"empty"::: )   )   ($#~v11_struct_0  "non"   ($#v11_struct_0 :::"void"::: )   )    ($#l1_msualg_1 :::"ManySortedSign"::: )  ; let "U1" be   ($#v4_msualg_1 :::"non-empty"::: )     ($#l3_msualg_1 :::"MSAlgebra"::: )   "over" (Set (Const "S")); 
cluster (Set   ($#k6_endalg :::"MSAEndMonoid"::: )  "U1") ->  ($#~v2_struct_0  "non"   ($#v2_struct_0 :::"empty"::: )   )    ($#v22_algstr_0 :::"strict"::: )   ; 
end; registrationlet "S" be  ($#~v2_struct_0  "non"   ($#v2_struct_0 :::"empty"::: )   )   ($#~v11_struct_0  "non"   ($#v11_struct_0 :::"void"::: )   )    ($#l1_msualg_1 :::"ManySortedSign"::: )  ; let "U1" be   ($#v4_msualg_1 :::"non-empty"::: )     ($#l3_msualg_1 :::"MSAlgebra"::: )   "over" (Set (Const "S")); 
cluster (Set   ($#k6_endalg :::"MSAEndMonoid"::: )  "U1") ->   ($#v22_algstr_0 :::"strict"::: )     ($#v3_group_1 :::"associative"::: )     ($#v4_vectsp_1 :::"well-unital"::: )   ; 
end; 
theorem :: ENDALG:10 (Bool  "for" (Set (Var "S")) "being"  ($#~v2_struct_0  "non"   ($#v2_struct_0 :::"empty"::: )   )   ($#~v11_struct_0  "non"   ($#v11_struct_0 :::"void"::: )   )    ($#l1_msualg_1 :::"ManySortedSign"::: )    (Bool  "for" (Set (Var "U1")) "being"   ($#v4_msualg_1 :::"non-empty"::: )     ($#l3_msualg_1 :::"MSAlgebra"::: )   "over" (Set (Var "S"))  (Bool  "for" (Set (Var "x")) "," (Set (Var "y")) "being"   ($#m1_subset_1 :::"Element":::) "of" (Set  "("  ($#k6_endalg :::"MSAEndMonoid"::: )  (Set (Var "U1")) ")" )  (Bool  "for" (Set (Var "f")) "," (Set (Var "g")) "being"    ($#m1_autalg_1 :::"Element"::: )   "of" (Set   ($#k4_endalg :::"MSAEnd"::: )  (Set (Var "U1")))  "st" (Bool (Bool (Set (Var "x"))  ($#r1_hidden :::"="::: )  (Set (Var "f"))) & (Bool (Set (Var "y"))  ($#r1_hidden :::"="::: )  (Set (Var "g")))) "holds"  (Bool (Set (Set (Var "x"))  ($#k6_algstr_0 :::"*"::: )  (Set (Var "y")))  ($#r1_hidden :::"="::: )  (Set (Set (Var "g"))  ($#k3_msualg_3 :::"**"::: )  (Set (Var "f")))))))) ; 
 
theorem :: ENDALG:11 (Bool  "for" (Set (Var "S")) "being"  ($#~v2_struct_0  "non"   ($#v2_struct_0 :::"empty"::: )   )   ($#~v11_struct_0  "non"   ($#v11_struct_0 :::"void"::: )   )    ($#l1_msualg_1 :::"ManySortedSign"::: )    (Bool  "for" (Set (Var "U1")) "being"   ($#v4_msualg_1 :::"non-empty"::: )     ($#l3_msualg_1 :::"MSAlgebra"::: )   "over" (Set (Var "S")) "holds"  (Bool (Set   ($#k2_msualg_3 :::"id"::: )  (Set  "the"  ($#u3_msualg_1 :::"Sorts"::: )  "of" (Set (Var "U1"))))  ($#r1_hidden :::"="::: )  (Set   ($#k1_group_1 :::"1_"::: )  (Set  "("  ($#k6_endalg :::"MSAEndMonoid"::: )  (Set (Var "U1")) ")" ))))) ; 
 
theorem :: ENDALG:12 (Bool  "for" (Set (Var "UA")) "being"   ($#l1_unialg_1 :::"Universal_Algebra":::)  (Bool  "for" (Set (Var "f")) "being"    ($#m2_funct_2 :::"Element"::: )   "of" (Set   ($#k1_endalg :::"UAEnd"::: )  (Set (Var "UA"))) "holds"  (Bool (Set (Set  ($#k6_numbers :::"0"::: ) )  ($#k16_funcop_1 :::".-->"::: )  (Set (Var "f"))) "is"   ($#m2_pboole :::"ManySortedFunction":::) "of" (Set  "("  ($#k9_msualg_1 :::"MSAlg"::: )  (Set (Var "UA")) ")" ) "," (Set  "("  ($#k9_msualg_1 :::"MSAlg"::: )  (Set (Var "UA")) ")" )))) ; 
 registration
cluster  ($#~v2_struct_0  "non"   ($#v2_struct_0 :::"empty"::: )   )    ($#v6_vectsp_1 :::"left_unital"::: )    for    ($#l4_algstr_0 :::"multLoopStr"::: )  ; 
end; registrationlet "G", "H" be  ($#~v2_struct_0  "non"   ($#v2_struct_0 :::"empty"::: )   )    ($#v4_vectsp_1 :::"well-unital"::: )     ($#l4_algstr_0 :::"multLoopStr"::: )  ; 
cluster   ($#v1_relat_1 :::"Relation-like"::: )   (Set  "the"  ($#u1_struct_0 :::"carrier"::: )  "of" "G")  ($#v4_relat_1 :::"-defined"::: )   (Set  "the"  ($#u1_struct_0 :::"carrier"::: )  "of" "H")  ($#v5_relat_1 :::"-valued"::: )     ($#v1_funct_1 :::"Function-like"::: )    ($#~v1_xboole_0  "non"   ($#v1_xboole_0 :::"empty"::: )   )  bbbadV1_PARTFUN1((Set  "the"  ($#u1_struct_0 :::"carrier"::: )  "of" "G"))   ($#v1_funct_2 :::"quasi_total"::: )     ($#v6_group_1 :::"unity-preserving"::: )     ($#v1_group_6 :::"multiplicative"::: )    for    ($#m1_subset_1 :::"Element"::: )   "of" (Set   ($#k1_zfmisc_1 :::"bool"::: )  (Set  ($#k2_zfmisc_1 :::"[:"::: ) (Set  "the"  ($#u1_struct_0 :::"carrier"::: )  "of" "G") "," (Set  "the"  ($#u1_struct_0 :::"carrier"::: )  "of" "H") ($#k2_zfmisc_1 :::":]"::: ) )); 
end; definitionlet "G", "H" be  ($#~v2_struct_0  "non"   ($#v2_struct_0 :::"empty"::: )   )    ($#v4_vectsp_1 :::"well-unital"::: )     ($#l4_algstr_0 :::"multLoopStr"::: )  ; mode Homomorphism of "G" "," "H" is   ($#v6_group_1 :::"unity-preserving"::: )     ($#v1_group_6 :::"multiplicative"::: )    ($#m1_subset_1 :::"Function":::) "of" "G" "," "H"; end; 
theorem :: ENDALG:13 (Bool  "for" (Set (Var "G")) "being"  ($#~v2_struct_0  "non"   ($#v2_struct_0 :::"empty"::: )   )    ($#v4_vectsp_1 :::"well-unital"::: )     ($#l4_algstr_0 :::"multLoopStr"::: )   "holds"  (Bool (Set   ($#k6_partfun1 :::"id"::: )  (Set  "the"  ($#u1_struct_0 :::"carrier"::: )  "of" (Set (Var "G")))) "is"   ($#m1_subset_1 :::"Homomorphism":::) "of" (Set (Var "G")) "," (Set (Var "G")))) ; 
 definitionlet "G", "H" be  ($#~v2_struct_0  "non"   ($#v2_struct_0 :::"empty"::: )   )    ($#v4_vectsp_1 :::"well-unital"::: )     ($#l4_algstr_0 :::"multLoopStr"::: )  ; pred "G" "," "H" :::"are_isomorphic":::  means :: ENDALG:def 7 (Bool  "ex" (Set (Var "h")) "being"   ($#m1_subset_1 :::"Homomorphism":::) "of" "G" "," "H" "st" (Bool (Set (Var "h")) "is"   ($#v3_funct_2 :::"bijective"::: )  )); reflexivity  
(Bool  "for" (Set (Var "G")) "being"  ($#~v2_struct_0  "non"   ($#v2_struct_0 :::"empty"::: )   )    ($#v4_vectsp_1 :::"well-unital"::: )     ($#l4_algstr_0 :::"multLoopStr"::: )   (Bool  "ex" (Set (Var "h")) "being"   ($#m1_subset_1 :::"Homomorphism":::) "of" (Set (Var "G")) "," (Set (Var "G")) "st" (Bool (Set (Var "h")) "is"   ($#v3_funct_2 :::"bijective"::: )  )))
 ; end; 





:: deftheorem    defines :::"are_isomorphic"::: ENDALG:def 7 :  (Bool  "for" (Set (Var "G")) "," (Set (Var "H")) "being"  ($#~v2_struct_0  "non"   ($#v2_struct_0 :::"empty"::: )   )    ($#v4_vectsp_1 :::"well-unital"::: )     ($#l4_algstr_0 :::"multLoopStr"::: )   "holds"   (Bool  "("  (Bool (Set (Var "G")) "," (Set (Var "H"))  ($#r1_endalg :::"are_isomorphic"::: )  ) "iff" (Bool  "ex" (Set (Var "h")) "being"   ($#m1_subset_1 :::"Homomorphism":::) "of" (Set (Var "G")) "," (Set (Var "H")) "st" (Bool (Set (Var "h")) "is"   ($#v3_funct_2 :::"bijective"::: )  ))  ")" )); 
 
theorem :: ENDALG:14 (Bool  "for" (Set (Var "UA")) "being"   ($#l1_unialg_1 :::"Universal_Algebra":::)  (Bool  "for" (Set (Var "h")) "being"   ($#m1_hidden :::"Function":::)  "st" (Bool (Bool (Set   ($#k9_xtuple_0 :::"dom"::: )  (Set (Var "h")))  ($#r1_hidden :::"="::: )  (Set   ($#k1_endalg :::"UAEnd"::: )  (Set (Var "UA")))) & (Bool  "("   "for" (Set (Var "x")) "being"    ($#m1_hidden :::"set"::: )    "st" (Bool (Bool (Set (Var "x"))  ($#r2_hidden :::"in"::: )  (Set   ($#k1_endalg :::"UAEnd"::: )  (Set (Var "UA"))))) "holds"  (Bool (Set (Set (Var "h"))  ($#k1_funct_1 :::"."::: )  (Set (Var "x")))  ($#r1_hidden :::"="::: )  (Set (Set  ($#k6_numbers :::"0"::: ) )  ($#k16_funcop_1 :::".-->"::: )  (Set (Var "x"))))  ")" )) "holds"  (Bool (Set (Var "h")) "is"   ($#m1_subset_1 :::"Homomorphism":::) "of" (Set  "("  ($#k3_endalg :::"UAEndMonoid"::: )  (Set (Var "UA")) ")" ) "," (Set  "("  ($#k6_endalg :::"MSAEndMonoid"::: )  (Set  "("  ($#k9_msualg_1 :::"MSAlg"::: )  (Set (Var "UA")) ")" ) ")" )))) ; 
 
theorem :: ENDALG:15 (Bool  "for" (Set (Var "UA")) "being"   ($#l1_unialg_1 :::"Universal_Algebra":::)  (Bool  "for" (Set (Var "h")) "being"   ($#m1_subset_1 :::"Homomorphism":::) "of" (Set  "("  ($#k3_endalg :::"UAEndMonoid"::: )  (Set (Var "UA")) ")" ) "," (Set  "("  ($#k6_endalg :::"MSAEndMonoid"::: )  (Set  "("  ($#k9_msualg_1 :::"MSAlg"::: )  (Set (Var "UA")) ")" ) ")" )  "st" (Bool (Bool  "("   "for" (Set (Var "x")) "being"    ($#m1_hidden :::"set"::: )    "st" (Bool (Bool (Set (Var "x"))  ($#r2_hidden :::"in"::: )  (Set   ($#k1_endalg :::"UAEnd"::: )  (Set (Var "UA"))))) "holds"  (Bool (Set (Set (Var "h"))  ($#k1_funct_1 :::"."::: )  (Set (Var "x")))  ($#r1_hidden :::"="::: )  (Set (Set  ($#k6_numbers :::"0"::: ) )  ($#k16_funcop_1 :::".-->"::: )  (Set (Var "x"))))  ")" )) "holds"  (Bool (Set (Var "h")) "is"   ($#v3_funct_2 :::"bijective"::: )  ))) ; 
 
theorem :: ENDALG:16 (Bool  "for" (Set (Var "UA")) "being"   ($#l1_unialg_1 :::"Universal_Algebra":::) "holds"  (Bool (Set   ($#k3_endalg :::"UAEndMonoid"::: )  (Set (Var "UA"))) "," (Set   ($#k6_endalg :::"MSAEndMonoid"::: )  (Set  "("  ($#k9_msualg_1 :::"MSAlg"::: )  (Set (Var "UA")) ")" ))  ($#r1_endalg :::"are_isomorphic"::: )  )) ;