:: ALG_1  semantic presentation begin  






















theorem :: ALG_1:1 (Bool  "for" (Set (Var "U1")) "being"   ($#l1_unialg_1 :::"Universal_Algebra":::)  (Bool  "for" (Set (Var "B")) "being"  ($#~v1_xboole_0  "non"   ($#v1_xboole_0 :::"empty"::: )   )   ($#m1_subset_1 :::"Subset":::) "of" (Set (Var "U1"))  "st" (Bool (Bool (Set (Var "B"))  ($#r1_hidden :::"="::: )  (Set  "the"  ($#u1_struct_0 :::"carrier"::: )  "of" (Set (Var "U1"))))) "holds"  (Bool (Set   ($#k3_unialg_2 :::"Opers"::: )   "(" (Set (Var "U1")) "," (Set (Var "B")) ")" )  ($#r1_hidden :::"="::: )  (Set  "the"  ($#u1_unialg_1 :::"charact"::: )  "of" (Set (Var "U1")))))) ; 
 






theorem :: ALG_1:2 (Bool  "for" (Set (Var "U1")) "," (Set (Var "U2")) "being"   ($#l1_unialg_1 :::"Universal_Algebra":::)  (Bool  "for" (Set (Var "f")) "being"   ($#m1_subset_1 :::"Function":::) "of" (Set (Var "U1")) "," (Set (Var "U2")) "holds"  (Bool (Set (Set (Var "f"))  ($#k4_finseqop :::"*"::: )  (Set  "("  ($#k6_finseq_1 :::"<*>"::: )  (Set  "the"  ($#u1_struct_0 :::"carrier"::: )  "of" (Set (Var "U1"))) ")" ))  ($#r1_hidden :::"="::: )  (Set   ($#k6_finseq_1 :::"<*>"::: )  (Set  "the"  ($#u1_struct_0 :::"carrier"::: )  "of" (Set (Var "U2"))))))) ; 
 
theorem :: ALG_1:3 (Bool  "for" (Set (Var "U1")) "being"   ($#l1_unialg_1 :::"Universal_Algebra":::)  (Bool  "for" (Set (Var "a")) "being"   ($#m2_finseq_1 :::"FinSequence":::) "of" (Set (Var "U1")) "holds"  (Bool (Set (Set  "("  ($#k6_partfun1 :::"id"::: )  (Set  "the"  ($#u1_struct_0 :::"carrier"::: )  "of" (Set (Var "U1"))) ")" )  ($#k4_finseqop :::"*"::: )  (Set (Var "a")))  ($#r1_hidden :::"="::: )  (Set (Var "a"))))) ; 
 
theorem :: ALG_1:4 (Bool  "for" (Set (Var "U1")) "," (Set (Var "U2")) "," (Set (Var "U3")) "being"   ($#l1_unialg_1 :::"Universal_Algebra":::)  (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"))  (Bool  "for" (Set (Var "a")) "being"   ($#m2_finseq_1 :::"FinSequence":::) "of" (Set (Var "U1")) "holds"  (Bool (Set (Set (Var "h2"))  ($#k4_finseqop :::"*"::: )  (Set  "(" (Set (Var "h1"))  ($#k4_finseqop :::"*"::: )  (Set (Var "a")) ")" ))  ($#r1_hidden :::"="::: )  (Set (Set  "(" (Set (Var "h2"))  ($#k1_partfun1 :::"*"::: )  (Set (Var "h1")) ")" )  ($#k4_finseqop :::"*"::: )  (Set (Var "a")))))))) ; 
 definitionlet "U1", "U2" be   ($#l1_unialg_1 :::"Universal_Algebra":::); let "f" be   ($#m1_subset_1 :::"Function":::) "of" (Set (Const "U1")) "," (Set (Const "U2")); pred "f" :::"is_homomorphism"::: "U1" "," "U2" means :: ALG_1:def 1 (Bool  "("  (Bool "U1" "," "U2"  ($#r1_unialg_2 :::"are_similar"::: )  ) & (Bool  "("   "for" (Set (Var "n")) "being"    ($#m1_subset_1 :::"Element"::: )   "of" (Set   ($#k5_numbers :::"NAT"::: )  )  "st" (Bool (Bool (Set (Var "n"))  ($#r2_hidden :::"in"::: )  (Set   ($#k4_finseq_1 :::"dom"::: )  (Set  "the"  ($#u1_unialg_1 :::"charact"::: )  "of" "U1")))) "holds"  (Bool  "for" (Set (Var "o1")) "being"   ($#m5_margrel1 :::"operation":::) "of" "U1"  (Bool  "for" (Set (Var "o2")) "being"   ($#m5_margrel1 :::"operation":::) "of" "U2"  "st" (Bool (Bool (Set (Var "o1"))  ($#r1_hidden :::"="::: )  (Set (Set  "the"  ($#u1_unialg_1 :::"charact"::: )  "of" "U1")  ($#k1_funct_1 :::"."::: )  (Set (Var "n")))) & (Bool (Set (Var "o2"))  ($#r1_hidden :::"="::: )  (Set (Set  "the"  ($#u1_unialg_1 :::"charact"::: )  "of" "U2")  ($#k1_funct_1 :::"."::: )  (Set (Var "n"))))) "holds"  (Bool  "for" (Set (Var "x")) "being"   ($#m2_finseq_1 :::"FinSequence":::) "of" "U1"  "st" (Bool (Bool (Set (Var "x"))  ($#r2_hidden :::"in"::: )  (Set   ($#k1_relset_1 :::"dom"::: )  (Set (Var "o1"))))) "holds"  (Bool (Set "f"  ($#k1_funct_1 :::"."::: )  (Set  "(" (Set (Var "o1"))  ($#k1_funct_1 :::"."::: )  (Set (Var "x")) ")" ))  ($#r1_hidden :::"="::: )  (Set (Set (Var "o2"))  ($#k1_funct_1 :::"."::: )  (Set  "(" "f"  ($#k4_finseqop :::"*"::: )  (Set (Var "x")) ")" ))))))  ")" )  ")" ); end; 






:: deftheorem    defines :::"is_homomorphism"::: ALG_1:def 1 :  (Bool  "for" (Set (Var "U1")) "," (Set (Var "U2")) "being"   ($#l1_unialg_1 :::"Universal_Algebra":::)  (Bool  "for" (Set (Var "f")) "being"   ($#m1_subset_1 :::"Function":::) "of" (Set (Var "U1")) "," (Set (Var "U2")) "holds"   (Bool  "("  (Bool (Set (Var "f"))  ($#r1_alg_1 :::"is_homomorphism"::: )  (Set (Var "U1")) "," (Set (Var "U2"))) "iff" (Bool  "("  (Bool (Set (Var "U1")) "," (Set (Var "U2"))  ($#r1_unialg_2 :::"are_similar"::: )  ) & (Bool  "("   "for" (Set (Var "n")) "being"    ($#m1_subset_1 :::"Element"::: )   "of" (Set   ($#k5_numbers :::"NAT"::: )  )  "st" (Bool (Bool (Set (Var "n"))  ($#r2_hidden :::"in"::: )  (Set   ($#k4_finseq_1 :::"dom"::: )  (Set  "the"  ($#u1_unialg_1 :::"charact"::: )  "of" (Set (Var "U1")))))) "holds"  (Bool  "for" (Set (Var "o1")) "being"   ($#m5_margrel1 :::"operation":::) "of" (Set (Var "U1"))  (Bool  "for" (Set (Var "o2")) "being"   ($#m5_margrel1 :::"operation":::) "of" (Set (Var "U2"))  "st" (Bool (Bool (Set (Var "o1"))  ($#r1_hidden :::"="::: )  (Set (Set  "the"  ($#u1_unialg_1 :::"charact"::: )  "of" (Set (Var "U1")))  ($#k1_funct_1 :::"."::: )  (Set (Var "n")))) & (Bool (Set (Var "o2"))  ($#r1_hidden :::"="::: )  (Set (Set  "the"  ($#u1_unialg_1 :::"charact"::: )  "of" (Set (Var "U2")))  ($#k1_funct_1 :::"."::: )  (Set (Var "n"))))) "holds"  (Bool  "for" (Set (Var "x")) "being"   ($#m2_finseq_1 :::"FinSequence":::) "of" (Set (Var "U1"))  "st" (Bool (Bool (Set (Var "x"))  ($#r2_hidden :::"in"::: )  (Set   ($#k1_relset_1 :::"dom"::: )  (Set (Var "o1"))))) "holds"  (Bool (Set (Set (Var "f"))  ($#k1_funct_1 :::"."::: )  (Set  "(" (Set (Var "o1"))  ($#k1_funct_1 :::"."::: )  (Set (Var "x")) ")" ))  ($#r1_hidden :::"="::: )  (Set (Set (Var "o2"))  ($#k1_funct_1 :::"."::: )  (Set  "(" (Set (Var "f"))  ($#k4_finseqop :::"*"::: )  (Set (Var "x")) ")" ))))))  ")" )  ")" )  ")" ))); 
 definitionlet "U1", "U2" be   ($#l1_unialg_1 :::"Universal_Algebra":::); let "f" be   ($#m1_subset_1 :::"Function":::) "of" (Set (Const "U1")) "," (Set (Const "U2")); pred "f" :::"is_monomorphism"::: "U1" "," "U2" means :: ALG_1:def 2 (Bool  "("  (Bool "f"  ($#r1_alg_1 :::"is_homomorphism"::: )  "U1" "," "U2") & (Bool "f" "is"   ($#v2_funct_1 :::"one-to-one"::: )  )  ")" ); pred "f" :::"is_epimorphism"::: "U1" "," "U2" means :: ALG_1:def 3 (Bool  "("  (Bool "f"  ($#r1_alg_1 :::"is_homomorphism"::: )  "U1" "," "U2") & (Bool (Set   ($#k2_relset_1 :::"rng"::: )  "f")  ($#r1_hidden :::"="::: )  (Set  "the"  ($#u1_struct_0 :::"carrier"::: )  "of" "U2"))  ")" ); end; 












:: deftheorem    defines :::"is_monomorphism"::: ALG_1:def 2 :  (Bool  "for" (Set (Var "U1")) "," (Set (Var "U2")) "being"   ($#l1_unialg_1 :::"Universal_Algebra":::)  (Bool  "for" (Set (Var "f")) "being"   ($#m1_subset_1 :::"Function":::) "of" (Set (Var "U1")) "," (Set (Var "U2")) "holds"   (Bool  "("  (Bool (Set (Var "f"))  ($#r2_alg_1 :::"is_monomorphism"::: )  (Set (Var "U1")) "," (Set (Var "U2"))) "iff" (Bool  "("  (Bool (Set (Var "f"))  ($#r1_alg_1 :::"is_homomorphism"::: )  (Set (Var "U1")) "," (Set (Var "U2"))) & (Bool (Set (Var "f")) "is"   ($#v2_funct_1 :::"one-to-one"::: )  )  ")" )  ")" ))); 
 
:: deftheorem    defines :::"is_epimorphism"::: ALG_1:def 3 :  (Bool  "for" (Set (Var "U1")) "," (Set (Var "U2")) "being"   ($#l1_unialg_1 :::"Universal_Algebra":::)  (Bool  "for" (Set (Var "f")) "being"   ($#m1_subset_1 :::"Function":::) "of" (Set (Var "U1")) "," (Set (Var "U2")) "holds"   (Bool  "("  (Bool (Set (Var "f"))  ($#r3_alg_1 :::"is_epimorphism"::: )  (Set (Var "U1")) "," (Set (Var "U2"))) "iff" (Bool  "("  (Bool (Set (Var "f"))  ($#r1_alg_1 :::"is_homomorphism"::: )  (Set (Var "U1")) "," (Set (Var "U2"))) & (Bool (Set   ($#k2_relset_1 :::"rng"::: )  (Set (Var "f")))  ($#r1_hidden :::"="::: )  (Set  "the"  ($#u1_struct_0 :::"carrier"::: )  "of" (Set (Var "U2"))))  ")" )  ")" ))); 
 definitionlet "U1", "U2" be   ($#l1_unialg_1 :::"Universal_Algebra":::); let "f" be   ($#m1_subset_1 :::"Function":::) "of" (Set (Const "U1")) "," (Set (Const "U2")); pred "f" :::"is_isomorphism"::: "U1" "," "U2" means :: ALG_1:def 4 (Bool  "("  (Bool "f"  ($#r2_alg_1 :::"is_monomorphism"::: )  "U1" "," "U2") & (Bool "f"  ($#r3_alg_1 :::"is_epimorphism"::: )  "U1" "," "U2")  ")" ); end; 






:: deftheorem    defines :::"is_isomorphism"::: ALG_1:def 4 :  (Bool  "for" (Set (Var "U1")) "," (Set (Var "U2")) "being"   ($#l1_unialg_1 :::"Universal_Algebra":::)  (Bool  "for" (Set (Var "f")) "being"   ($#m1_subset_1 :::"Function":::) "of" (Set (Var "U1")) "," (Set (Var "U2")) "holds"   (Bool  "("  (Bool (Set (Var "f"))  ($#r4_alg_1 :::"is_isomorphism"::: )  (Set (Var "U1")) "," (Set (Var "U2"))) "iff" (Bool  "("  (Bool (Set (Var "f"))  ($#r2_alg_1 :::"is_monomorphism"::: )  (Set (Var "U1")) "," (Set (Var "U2"))) & (Bool (Set (Var "f"))  ($#r3_alg_1 :::"is_epimorphism"::: )  (Set (Var "U1")) "," (Set (Var "U2")))  ")" )  ")" ))); 
 definitionlet "U1", "U2" be   ($#l1_unialg_1 :::"Universal_Algebra":::); pred "U1" "," "U2" :::"are_isomorphic":::  means :: ALG_1:def 5 (Bool  "ex" (Set (Var "f")) "being"   ($#m1_subset_1 :::"Function":::) "of" "U1" "," "U2" "st" (Bool (Set (Var "f"))  ($#r4_alg_1 :::"is_isomorphism"::: )  "U1" "," "U2")); end; 





:: deftheorem    defines :::"are_isomorphic"::: ALG_1:def 5 :  (Bool  "for" (Set (Var "U1")) "," (Set (Var "U2")) "being"   ($#l1_unialg_1 :::"Universal_Algebra":::) "holds"   (Bool  "("  (Bool (Set (Var "U1")) "," (Set (Var "U2"))  ($#r5_alg_1 :::"are_isomorphic"::: )  ) "iff" (Bool  "ex" (Set (Var "f")) "being"   ($#m1_subset_1 :::"Function":::) "of" (Set (Var "U1")) "," (Set (Var "U2")) "st" (Bool (Set (Var "f"))  ($#r4_alg_1 :::"is_isomorphism"::: )  (Set (Var "U1")) "," (Set (Var "U2"))))  ")" )); 
 
theorem :: ALG_1:5 (Bool  "for" (Set (Var "U1")) "being"   ($#l1_unialg_1 :::"Universal_Algebra":::) "holds"  (Bool (Set   ($#k6_partfun1 :::"id"::: )  (Set  "the"  ($#u1_struct_0 :::"carrier"::: )  "of" (Set (Var "U1"))))  ($#r1_alg_1 :::"is_homomorphism"::: )  (Set (Var "U1")) "," (Set (Var "U1")))) ; 
 
theorem :: ALG_1:6 (Bool  "for" (Set (Var "U1")) "," (Set (Var "U2")) "," (Set (Var "U3")) "being"   ($#l1_unialg_1 :::"Universal_Algebra":::)  (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"))  "st" (Bool (Bool (Set (Var "h1"))  ($#r1_alg_1 :::"is_homomorphism"::: )  (Set (Var "U1")) "," (Set (Var "U2"))) & (Bool (Set (Var "h2"))  ($#r1_alg_1 :::"is_homomorphism"::: )  (Set (Var "U2")) "," (Set (Var "U3")))) "holds"  (Bool (Set (Set (Var "h2"))  ($#k1_partfun1 :::"*"::: )  (Set (Var "h1")))  ($#r1_alg_1 :::"is_homomorphism"::: )  (Set (Var "U1")) "," (Set (Var "U3")))))) ; 
 
theorem :: ALG_1:7 (Bool  "for" (Set (Var "U1")) "," (Set (Var "U2")) "being"   ($#l1_unialg_1 :::"Universal_Algebra":::)  (Bool  "for" (Set (Var "f")) "being"   ($#m1_subset_1 :::"Function":::) "of" (Set (Var "U1")) "," (Set (Var "U2")) "holds"   (Bool  "("  (Bool (Set (Var "f"))  ($#r4_alg_1 :::"is_isomorphism"::: )  (Set (Var "U1")) "," (Set (Var "U2"))) "iff" (Bool  "("  (Bool (Set (Var "f"))  ($#r1_alg_1 :::"is_homomorphism"::: )  (Set (Var "U1")) "," (Set (Var "U2"))) & (Bool (Set   ($#k2_relset_1 :::"rng"::: )  (Set (Var "f")))  ($#r1_hidden :::"="::: )  (Set  "the"  ($#u1_struct_0 :::"carrier"::: )  "of" (Set (Var "U2")))) & (Bool (Set (Var "f")) "is"   ($#v2_funct_1 :::"one-to-one"::: )  )  ")" )  ")" ))) ; 
 
theorem :: ALG_1:8 (Bool  "for" (Set (Var "U1")) "," (Set (Var "U2")) "being"   ($#l1_unialg_1 :::"Universal_Algebra":::)  (Bool  "for" (Set (Var "f")) "being"   ($#m1_subset_1 :::"Function":::) "of" (Set (Var "U1")) "," (Set (Var "U2"))  "st" (Bool (Bool (Set (Var "f"))  ($#r4_alg_1 :::"is_isomorphism"::: )  (Set (Var "U1")) "," (Set (Var "U2")))) "holds"  (Bool  "("  (Bool (Set   ($#k1_relset_1 :::"dom"::: )  (Set (Var "f")))  ($#r1_hidden :::"="::: )  (Set  "the"  ($#u1_struct_0 :::"carrier"::: )  "of" (Set (Var "U1")))) & (Bool (Set   ($#k2_relset_1 :::"rng"::: )  (Set (Var "f")))  ($#r1_hidden :::"="::: )  (Set  "the"  ($#u1_struct_0 :::"carrier"::: )  "of" (Set (Var "U2"))))  ")" ))) ; 
 
theorem :: ALG_1:9 (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"))  (Bool  "for" (Set (Var "h1")) "being"   ($#m1_subset_1 :::"Function":::) "of" (Set (Var "U2")) "," (Set (Var "U1"))  "st" (Bool (Bool (Set (Var "h"))  ($#r4_alg_1 :::"is_isomorphism"::: )  (Set (Var "U1")) "," (Set (Var "U2"))) & (Bool (Set (Var "h1"))  ($#r1_hidden :::"="::: )  (Set (Set (Var "h"))  ($#k2_funct_1 :::"""::: )  ))) "holds"  (Bool (Set (Var "h1"))  ($#r1_alg_1 :::"is_homomorphism"::: )  (Set (Var "U2")) "," (Set (Var "U1")))))) ; 
 
theorem :: ALG_1:10 (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"))  (Bool  "for" (Set (Var "h1")) "being"   ($#m1_subset_1 :::"Function":::) "of" (Set (Var "U2")) "," (Set (Var "U1"))  "st" (Bool (Bool (Set (Var "h"))  ($#r4_alg_1 :::"is_isomorphism"::: )  (Set (Var "U1")) "," (Set (Var "U2"))) & (Bool (Set (Var "h1"))  ($#r1_hidden :::"="::: )  (Set (Set (Var "h"))  ($#k2_funct_1 :::"""::: )  ))) "holds"  (Bool (Set (Var "h1"))  ($#r4_alg_1 :::"is_isomorphism"::: )  (Set (Var "U2")) "," (Set (Var "U1")))))) ; 
 
theorem :: ALG_1:11 (Bool  "for" (Set (Var "U1")) "," (Set (Var "U2")) "," (Set (Var "U3")) "being"   ($#l1_unialg_1 :::"Universal_Algebra":::)  (Bool  "for" (Set (Var "h")) "being"   ($#m1_subset_1 :::"Function":::) "of" (Set (Var "U1")) "," (Set (Var "U2"))  (Bool  "for" (Set (Var "h1")) "being"   ($#m1_subset_1 :::"Function":::) "of" (Set (Var "U2")) "," (Set (Var "U3"))  "st" (Bool (Bool (Set (Var "h"))  ($#r4_alg_1 :::"is_isomorphism"::: )  (Set (Var "U1")) "," (Set (Var "U2"))) & (Bool (Set (Var "h1"))  ($#r4_alg_1 :::"is_isomorphism"::: )  (Set (Var "U2")) "," (Set (Var "U3")))) "holds"  (Bool (Set (Set (Var "h1"))  ($#k1_partfun1 :::"*"::: )  (Set (Var "h")))  ($#r4_alg_1 :::"is_isomorphism"::: )  (Set (Var "U1")) "," (Set (Var "U3")))))) ; 
 
theorem :: ALG_1:12 (Bool  "for" (Set (Var "U1")) "being"   ($#l1_unialg_1 :::"Universal_Algebra":::) "holds"  (Bool (Set (Var "U1")) "," (Set (Var "U1"))  ($#r5_alg_1 :::"are_isomorphic"::: )  )) ; 
 
theorem :: ALG_1:13 (Bool  "for" (Set (Var "U1")) "," (Set (Var "U2")) "being"   ($#l1_unialg_1 :::"Universal_Algebra":::)  "st" (Bool (Bool (Set (Var "U1")) "," (Set (Var "U2"))  ($#r5_alg_1 :::"are_isomorphic"::: )  )) "holds"  (Bool (Set (Var "U2")) "," (Set (Var "U1"))  ($#r5_alg_1 :::"are_isomorphic"::: )  )) ; 
 
theorem :: ALG_1:14 (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"))  ($#r5_alg_1 :::"are_isomorphic"::: )  ) & (Bool (Set (Var "U2")) "," (Set (Var "U3"))  ($#r5_alg_1 :::"are_isomorphic"::: )  )) "holds"  (Bool (Set (Var "U1")) "," (Set (Var "U3"))  ($#r5_alg_1 :::"are_isomorphic"::: )  )) ; 
 definitionlet "U1", "U2" be   ($#l1_unialg_1 :::"Universal_Algebra":::); let "f" be   ($#m1_subset_1 :::"Function":::) "of" (Set (Const "U1")) "," (Set (Const "U2")); assume 
(Bool (Set (Const "f"))  ($#r1_alg_1 :::"is_homomorphism"::: )  (Set (Const "U1")) "," (Set (Const "U2")))
 ; func  :::"Image"::: "f" ->   ($#v1_unialg_1 :::"strict"::: )     ($#m1_unialg_2 :::"SubAlgebra"::: )   "of" "U2" means :: ALG_1:def 6 (Bool (Set  "the"  ($#u1_struct_0 :::"carrier"::: )  "of" it)  ($#r1_hidden :::"="::: )  (Set "f"  ($#k7_relset_1 :::".:"::: )  (Set  "the"  ($#u1_struct_0 :::"carrier"::: )  "of" "U1"))); end; 








:: deftheorem    defines :::"Image"::: ALG_1:def 6 :  (Bool  "for" (Set (Var "U1")) "," (Set (Var "U2")) "being"   ($#l1_unialg_1 :::"Universal_Algebra":::)  (Bool  "for" (Set (Var "f")) "being"   ($#m1_subset_1 :::"Function":::) "of" (Set (Var "U1")) "," (Set (Var "U2"))  "st" (Bool (Bool (Set (Var "f"))  ($#r1_alg_1 :::"is_homomorphism"::: )  (Set (Var "U1")) "," (Set (Var "U2")))) "holds"  (Bool  "for" (Set (Var "b4")) "being"   ($#v1_unialg_1 :::"strict"::: )     ($#m1_unialg_2 :::"SubAlgebra"::: )   "of" (Set (Var "U2")) "holds"   (Bool  "("  (Bool (Set (Var "b4"))  ($#r1_hidden :::"="::: )  (Set   ($#k1_alg_1 :::"Image"::: )  (Set (Var "f")))) "iff" (Bool (Set  "the"  ($#u1_struct_0 :::"carrier"::: )  "of" (Set (Var "b4")))  ($#r1_hidden :::"="::: )  (Set (Set (Var "f"))  ($#k7_relset_1 :::".:"::: )  (Set  "the"  ($#u1_struct_0 :::"carrier"::: )  "of" (Set (Var "U1")))))  ")" )))); 
 
theorem :: ALG_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 "h"))  ($#r1_alg_1 :::"is_homomorphism"::: )  (Set (Var "U1")) "," (Set (Var "U2")))) "holds"  (Bool (Set   ($#k2_relset_1 :::"rng"::: )  (Set (Var "h")))  ($#r1_hidden :::"="::: )  (Set  "the"  ($#u1_struct_0 :::"carrier"::: )  "of" (Set  "("  ($#k1_alg_1 :::"Image"::: )  (Set (Var "h")) ")" ))))) ; 
 
theorem :: ALG_1:16 (Bool  "for" (Set (Var "U1")) "being"   ($#l1_unialg_1 :::"Universal_Algebra":::)  (Bool  "for" (Set (Var "U2")) "being"   ($#v1_unialg_1 :::"strict"::: )    ($#l1_unialg_1 :::"Universal_Algebra":::)  (Bool  "for" (Set (Var "f")) "being"   ($#m1_subset_1 :::"Function":::) "of" (Set (Var "U1")) "," (Set (Var "U2"))  "st" (Bool (Bool (Set (Var "f"))  ($#r1_alg_1 :::"is_homomorphism"::: )  (Set (Var "U1")) "," (Set (Var "U2")))) "holds"  (Bool  "("  (Bool (Set (Var "f"))  ($#r3_alg_1 :::"is_epimorphism"::: )  (Set (Var "U1")) "," (Set (Var "U2"))) "iff" (Bool (Set   ($#k1_alg_1 :::"Image"::: )  (Set (Var "f")))  ($#r1_hidden :::"="::: )  (Set (Var "U2")))  ")" )))) ; 
 begin  definitionlet "U1" be    ($#l1_struct_0 :::"1-sorted"::: )  ; mode Relation of "U1" is   ($#m1_subset_1 :::"Relation":::) "of" (Set  "the"  ($#u1_struct_0 :::"carrier"::: )  "of" "U1"); mode Equivalence_Relation of "U1" is   ($#m1_subset_1 :::"Equivalence_Relation":::) "of" (Set  "the"  ($#u1_struct_0 :::"carrier"::: )  "of" "U1"); end; definitionlet "U1" be   ($#l1_unialg_1 :::"Universal_Algebra":::); mode  :::"Congruence":::  "of" "U1" ->   ($#m1_subset_1 :::"Equivalence_Relation":::) "of" "U1" means :: ALG_1:def 7 (Bool  "for" (Set (Var "n")) "being"    ($#m1_subset_1 :::"Element"::: )   "of" (Set   ($#k5_numbers :::"NAT"::: )  )  (Bool  "for" (Set (Var "o1")) "being"   ($#m5_margrel1 :::"operation":::) "of" "U1"  "st" (Bool (Bool (Set (Var "n"))  ($#r2_hidden :::"in"::: )  (Set   ($#k4_finseq_1 :::"dom"::: )  (Set  "the"  ($#u1_unialg_1 :::"charact"::: )  "of" "U1"))) & (Bool (Set (Var "o1"))  ($#r1_hidden :::"="::: )  (Set (Set  "the"  ($#u1_unialg_1 :::"charact"::: )  "of" "U1")  ($#k1_funct_1 :::"."::: )  (Set (Var "n"))))) "holds"  (Bool  "for" (Set (Var "x")) "," (Set (Var "y")) "being"   ($#m2_finseq_1 :::"FinSequence":::) "of" "U1"  "st" (Bool (Bool (Set (Var "x"))  ($#r2_hidden :::"in"::: )  (Set   ($#k1_relset_1 :::"dom"::: )  (Set (Var "o1")))) & (Bool (Set (Var "y"))  ($#r2_hidden :::"in"::: )  (Set   ($#k1_relset_1 :::"dom"::: )  (Set (Var "o1")))) & (Bool (Set  ($#k4_tarski :::"["::: ) (Set (Var "x")) "," (Set (Var "y")) ($#k4_tarski :::"]"::: ) )  ($#r2_hidden :::"in"::: )  (Set   ($#k3_finseq_3 :::"ExtendRel"::: )  it))) "holds"  (Bool (Set  ($#k4_tarski :::"["::: ) (Set  "(" (Set (Var "o1"))  ($#k1_funct_1 :::"."::: )  (Set (Var "x")) ")" ) "," (Set  "(" (Set (Var "o1"))  ($#k1_funct_1 :::"."::: )  (Set (Var "y")) ")" ) ($#k4_tarski :::"]"::: ) )  ($#r2_hidden :::"in"::: )  it)))); end; 





:: deftheorem    defines :::"Congruence"::: ALG_1:def 7 :  (Bool  "for" (Set (Var "U1")) "being"   ($#l1_unialg_1 :::"Universal_Algebra":::)  (Bool  "for" (Set (Var "b2")) "being"   ($#m1_subset_1 :::"Equivalence_Relation":::) "of" (Set (Var "U1")) "holds"   (Bool  "("  (Bool (Set (Var "b2")) "is"    ($#m1_alg_1 :::"Congruence"::: )   "of" (Set (Var "U1"))) "iff" (Bool  "for" (Set (Var "n")) "being"    ($#m1_subset_1 :::"Element"::: )   "of" (Set   ($#k5_numbers :::"NAT"::: )  )  (Bool  "for" (Set (Var "o1")) "being"   ($#m5_margrel1 :::"operation":::) "of" (Set (Var "U1"))  "st" (Bool (Bool (Set (Var "n"))  ($#r2_hidden :::"in"::: )  (Set   ($#k4_finseq_1 :::"dom"::: )  (Set  "the"  ($#u1_unialg_1 :::"charact"::: )  "of" (Set (Var "U1"))))) & (Bool (Set (Var "o1"))  ($#r1_hidden :::"="::: )  (Set (Set  "the"  ($#u1_unialg_1 :::"charact"::: )  "of" (Set (Var "U1")))  ($#k1_funct_1 :::"."::: )  (Set (Var "n"))))) "holds"  (Bool  "for" (Set (Var "x")) "," (Set (Var "y")) "being"   ($#m2_finseq_1 :::"FinSequence":::) "of" (Set (Var "U1"))  "st" (Bool (Bool (Set (Var "x"))  ($#r2_hidden :::"in"::: )  (Set   ($#k1_relset_1 :::"dom"::: )  (Set (Var "o1")))) & (Bool (Set (Var "y"))  ($#r2_hidden :::"in"::: )  (Set   ($#k1_relset_1 :::"dom"::: )  (Set (Var "o1")))) & (Bool (Set  ($#k4_tarski :::"["::: ) (Set (Var "x")) "," (Set (Var "y")) ($#k4_tarski :::"]"::: ) )  ($#r2_hidden :::"in"::: )  (Set   ($#k3_finseq_3 :::"ExtendRel"::: )  (Set (Var "b2"))))) "holds"  (Bool (Set  ($#k4_tarski :::"["::: ) (Set  "(" (Set (Var "o1"))  ($#k1_funct_1 :::"."::: )  (Set (Var "x")) ")" ) "," (Set  "(" (Set (Var "o1"))  ($#k1_funct_1 :::"."::: )  (Set (Var "y")) ")" ) ($#k4_tarski :::"]"::: ) )  ($#r2_hidden :::"in"::: )  (Set (Var "b2"))))))  ")" ))); 
 


definitionlet "U1" be   ($#l1_unialg_1 :::"Universal_Algebra":::); let "E" be    ($#m1_alg_1 :::"Congruence"::: )   "of" (Set (Const "U1")); let "o" be   ($#m5_margrel1 :::"operation":::) "of" (Set (Const "U1")); func  :::"QuotOp":::  "(" "o" "," "E" ")"  ->  ($#~v1_xboole_0  "non"   ($#v1_xboole_0 :::"empty"::: )   )    ($#v2_margrel1 :::"homogeneous"::: )     ($#v3_margrel1 :::"quasi_total"::: )    ($#m1_subset_1 :::"PartFunc":::) "of" (Set  "(" (Set  "("  ($#k8_eqrel_1 :::"Class"::: )  "E" ")" )  ($#k3_finseq_2 :::"*"::: )  ")" ) "," (Set  "("  ($#k8_eqrel_1 :::"Class"::: )  "E" ")" ) means :: ALG_1:def 8 (Bool  "("  (Bool (Set   ($#k1_relset_1 :::"dom"::: )  it)  ($#r1_hidden :::"="::: )  (Set (Set  "("  ($#k19_margrel1 :::"arity"::: )  "o" ")" )  ($#k4_finseq_2 :::"-tuples_on"::: )  (Set  "("  ($#k8_eqrel_1 :::"Class"::: )  "E" ")" ))) & (Bool  "("   "for" (Set (Var "y")) "being"    ($#m2_finseq_1 :::"FinSequence"::: )   "of" (Set   ($#k8_eqrel_1 :::"Class"::: )  "E")  "st" (Bool (Bool (Set (Var "y"))  ($#r2_hidden :::"in"::: )  (Set   ($#k1_relset_1 :::"dom"::: )  it))) "holds"  (Bool  "for" (Set (Var "x")) "being"    ($#m2_finseq_1 :::"FinSequence"::: )   "of" (Set  "the"  ($#u1_struct_0 :::"carrier"::: )  "of" "U1")  "st" (Bool (Bool (Set (Var "x"))  ($#r1_finseq_3 :::"is_representatives_FS"::: )  (Set (Var "y")))) "holds"  (Bool (Set it  ($#k1_funct_1 :::"."::: )  (Set (Var "y")))  ($#r1_hidden :::"="::: )  (Set   ($#k6_eqrel_1 :::"Class"::: )   "(" "E" "," (Set  "(" "o"  ($#k1_funct_1 :::"."::: )  (Set (Var "x")) ")" ) ")" )))  ")" )  ")" ); end; 







:: deftheorem    defines :::"QuotOp"::: ALG_1:def 8 :  (Bool  "for" (Set (Var "U1")) "being"   ($#l1_unialg_1 :::"Universal_Algebra":::)  (Bool  "for" (Set (Var "E")) "being"    ($#m1_alg_1 :::"Congruence"::: )   "of" (Set (Var "U1"))  (Bool  "for" (Set (Var "o")) "being"   ($#m5_margrel1 :::"operation":::) "of" (Set (Var "U1"))  (Bool  "for" (Set (Var "b4")) "being"  ($#~v1_xboole_0  "non"   ($#v1_xboole_0 :::"empty"::: )   )    ($#v2_margrel1 :::"homogeneous"::: )     ($#v3_margrel1 :::"quasi_total"::: )    ($#m1_subset_1 :::"PartFunc":::) "of" (Set  "(" (Set  "("  ($#k8_eqrel_1 :::"Class"::: )  (Set (Var "E")) ")" )  ($#k3_finseq_2 :::"*"::: )  ")" ) "," (Set  "("  ($#k8_eqrel_1 :::"Class"::: )  (Set (Var "E")) ")" ) "holds"   (Bool  "("  (Bool (Set (Var "b4"))  ($#r1_hidden :::"="::: )  (Set   ($#k2_alg_1 :::"QuotOp"::: )   "(" (Set (Var "o")) "," (Set (Var "E")) ")" )) "iff" (Bool  "("  (Bool (Set   ($#k1_relset_1 :::"dom"::: )  (Set (Var "b4")))  ($#r1_hidden :::"="::: )  (Set (Set  "("  ($#k19_margrel1 :::"arity"::: )  (Set (Var "o")) ")" )  ($#k4_finseq_2 :::"-tuples_on"::: )  (Set  "("  ($#k8_eqrel_1 :::"Class"::: )  (Set (Var "E")) ")" ))) & (Bool  "("   "for" (Set (Var "y")) "being"    ($#m2_finseq_1 :::"FinSequence"::: )   "of" (Set   ($#k8_eqrel_1 :::"Class"::: )  (Set (Var "E")))  "st" (Bool (Bool (Set (Var "y"))  ($#r2_hidden :::"in"::: )  (Set   ($#k1_relset_1 :::"dom"::: )  (Set (Var "b4"))))) "holds"  (Bool  "for" (Set (Var "x")) "being"    ($#m2_finseq_1 :::"FinSequence"::: )   "of" (Set  "the"  ($#u1_struct_0 :::"carrier"::: )  "of" (Set (Var "U1")))  "st" (Bool (Bool (Set (Var "x"))  ($#r1_finseq_3 :::"is_representatives_FS"::: )  (Set (Var "y")))) "holds"  (Bool (Set (Set (Var "b4"))  ($#k1_funct_1 :::"."::: )  (Set (Var "y")))  ($#r1_hidden :::"="::: )  (Set   ($#k6_eqrel_1 :::"Class"::: )   "(" (Set (Var "E")) "," (Set  "(" (Set (Var "o"))  ($#k1_funct_1 :::"."::: )  (Set (Var "x")) ")" ) ")" )))  ")" )  ")" )  ")" ))))); 
 definitionlet "U1" be   ($#l1_unialg_1 :::"Universal_Algebra":::); let "E" be    ($#m1_alg_1 :::"Congruence"::: )   "of" (Set (Const "U1")); func  :::"QuotOpSeq":::  "(" "U1" "," "E" ")"  ->   ($#m2_finseq_1 :::"PFuncFinSequence":::) "of" (Set  "("  ($#k8_eqrel_1 :::"Class"::: )  "E" ")" ) means :: ALG_1:def 9 (Bool  "("  (Bool (Set   ($#k3_finseq_1 :::"len"::: )  it)  ($#r1_hidden :::"="::: )  (Set   ($#k3_finseq_1 :::"len"::: )  (Set  "the"  ($#u1_unialg_1 :::"charact"::: )  "of" "U1"))) & (Bool  "("   "for" (Set (Var "n")) "being"    ($#m1_subset_1 :::"Element"::: )   "of" (Set   ($#k5_numbers :::"NAT"::: )  )  "st" (Bool (Bool (Set (Var "n"))  ($#r2_hidden :::"in"::: )  (Set   ($#k4_finseq_1 :::"dom"::: )  it))) "holds"  (Bool  "for" (Set (Var "o1")) "being"   ($#m5_margrel1 :::"operation":::) "of" "U1"  "st" (Bool (Bool (Set (Set  "the"  ($#u1_unialg_1 :::"charact"::: )  "of" "U1")  ($#k1_funct_1 :::"."::: )  (Set (Var "n")))  ($#r1_hidden :::"="::: )  (Set (Var "o1")))) "holds"  (Bool (Set it  ($#k1_funct_1 :::"."::: )  (Set (Var "n")))  ($#r1_hidden :::"="::: )  (Set   ($#k2_alg_1 :::"QuotOp"::: )   "(" (Set (Var "o1")) "," "E" ")" )))  ")" )  ")" ); end; 






:: deftheorem    defines :::"QuotOpSeq"::: ALG_1:def 9 :  (Bool  "for" (Set (Var "U1")) "being"   ($#l1_unialg_1 :::"Universal_Algebra":::)  (Bool  "for" (Set (Var "E")) "being"    ($#m1_alg_1 :::"Congruence"::: )   "of" (Set (Var "U1"))  (Bool  "for" (Set (Var "b3")) "being"   ($#m2_finseq_1 :::"PFuncFinSequence":::) "of" (Set  "("  ($#k8_eqrel_1 :::"Class"::: )  (Set (Var "E")) ")" ) "holds"   (Bool  "("  (Bool (Set (Var "b3"))  ($#r1_hidden :::"="::: )  (Set   ($#k3_alg_1 :::"QuotOpSeq"::: )   "(" (Set (Var "U1")) "," (Set (Var "E")) ")" )) "iff" (Bool  "("  (Bool (Set   ($#k3_finseq_1 :::"len"::: )  (Set (Var "b3")))  ($#r1_hidden :::"="::: )  (Set   ($#k3_finseq_1 :::"len"::: )  (Set  "the"  ($#u1_unialg_1 :::"charact"::: )  "of" (Set (Var "U1"))))) & (Bool  "("   "for" (Set (Var "n")) "being"    ($#m1_subset_1 :::"Element"::: )   "of" (Set   ($#k5_numbers :::"NAT"::: )  )  "st" (Bool (Bool (Set (Var "n"))  ($#r2_hidden :::"in"::: )  (Set   ($#k4_finseq_1 :::"dom"::: )  (Set (Var "b3"))))) "holds"  (Bool  "for" (Set (Var "o1")) "being"   ($#m5_margrel1 :::"operation":::) "of" (Set (Var "U1"))  "st" (Bool (Bool (Set (Set  "the"  ($#u1_unialg_1 :::"charact"::: )  "of" (Set (Var "U1")))  ($#k1_funct_1 :::"."::: )  (Set (Var "n")))  ($#r1_hidden :::"="::: )  (Set (Var "o1")))) "holds"  (Bool (Set (Set (Var "b3"))  ($#k1_funct_1 :::"."::: )  (Set (Var "n")))  ($#r1_hidden :::"="::: )  (Set   ($#k2_alg_1 :::"QuotOp"::: )   "(" (Set (Var "o1")) "," (Set (Var "E")) ")" )))  ")" )  ")" )  ")" )))); 
 definitionlet "U1" be   ($#l1_unialg_1 :::"Universal_Algebra":::); let "E" be    ($#m1_alg_1 :::"Congruence"::: )   "of" (Set (Const "U1")); func  :::"QuotUnivAlg":::  "(" "U1" "," "E" ")"  ->   ($#v1_unialg_1 :::"strict"::: )    ($#l1_unialg_1 :::"Universal_Algebra":::) equals :: ALG_1:def 10 (Set   ($#g1_unialg_1 :::"UAStr"::: )  "(#"  (Set  "("  ($#k8_eqrel_1 :::"Class"::: )  "E" ")" ) "," (Set  "("  ($#k3_alg_1 :::"QuotOpSeq"::: )   "(" "U1" "," "E" ")"  ")" ) "#)" ); end; 






:: deftheorem    defines :::"QuotUnivAlg"::: ALG_1:def 10 :  (Bool  "for" (Set (Var "U1")) "being"   ($#l1_unialg_1 :::"Universal_Algebra":::)  (Bool  "for" (Set (Var "E")) "being"    ($#m1_alg_1 :::"Congruence"::: )   "of" (Set (Var "U1")) "holds"  (Bool (Set   ($#k4_alg_1 :::"QuotUnivAlg"::: )   "(" (Set (Var "U1")) "," (Set (Var "E")) ")" )  ($#r1_hidden :::"="::: )  (Set   ($#g1_unialg_1 :::"UAStr"::: )  "(#"  (Set  "("  ($#k8_eqrel_1 :::"Class"::: )  (Set (Var "E")) ")" ) "," (Set  "("  ($#k3_alg_1 :::"QuotOpSeq"::: )   "(" (Set (Var "U1")) "," (Set (Var "E")) ")"  ")" ) "#)" )))); 
 definitionlet "U1" be   ($#l1_unialg_1 :::"Universal_Algebra":::); let "E" be    ($#m1_alg_1 :::"Congruence"::: )   "of" (Set (Const "U1")); func  :::"Nat_Hom":::  "(" "U1" "," "E" ")"  ->   ($#m1_subset_1 :::"Function":::) "of" "U1" "," (Set  "("  ($#k4_alg_1 :::"QuotUnivAlg"::: )   "(" "U1" "," "E" ")"  ")" ) means :: ALG_1:def 11 (Bool  "for" (Set (Var "u")) "being"   ($#m1_subset_1 :::"Element":::) "of" "U1" "holds"  (Bool (Set it  ($#k3_funct_2 :::"."::: )  (Set (Var "u")))  ($#r1_hidden :::"="::: )  (Set   ($#k6_eqrel_1 :::"Class"::: )   "(" "E" "," (Set (Var "u")) ")" ))); end; 






:: deftheorem    defines :::"Nat_Hom"::: ALG_1:def 11 :  (Bool  "for" (Set (Var "U1")) "being"   ($#l1_unialg_1 :::"Universal_Algebra":::)  (Bool  "for" (Set (Var "E")) "being"    ($#m1_alg_1 :::"Congruence"::: )   "of" (Set (Var "U1"))  (Bool  "for" (Set (Var "b3")) "being"   ($#m1_subset_1 :::"Function":::) "of" (Set (Var "U1")) "," (Set  "("  ($#k4_alg_1 :::"QuotUnivAlg"::: )   "(" (Set (Var "U1")) "," (Set (Var "E")) ")"  ")" ) "holds"   (Bool  "("  (Bool (Set (Var "b3"))  ($#r1_hidden :::"="::: )  (Set   ($#k5_alg_1 :::"Nat_Hom"::: )   "(" (Set (Var "U1")) "," (Set (Var "E")) ")" )) "iff" (Bool  "for" (Set (Var "u")) "being"   ($#m1_subset_1 :::"Element":::) "of" (Set (Var "U1")) "holds"  (Bool (Set (Set (Var "b3"))  ($#k3_funct_2 :::"."::: )  (Set (Var "u")))  ($#r1_hidden :::"="::: )  (Set   ($#k6_eqrel_1 :::"Class"::: )   "(" (Set (Var "E")) "," (Set (Var "u")) ")" )))  ")" )))); 
 
theorem :: ALG_1:17 (Bool  "for" (Set (Var "U1")) "being"   ($#l1_unialg_1 :::"Universal_Algebra":::)  (Bool  "for" (Set (Var "E")) "being"    ($#m1_alg_1 :::"Congruence"::: )   "of" (Set (Var "U1")) "holds"  (Bool (Set   ($#k5_alg_1 :::"Nat_Hom"::: )   "(" (Set (Var "U1")) "," (Set (Var "E")) ")" )  ($#r1_alg_1 :::"is_homomorphism"::: )  (Set (Var "U1")) "," (Set   ($#k4_alg_1 :::"QuotUnivAlg"::: )   "(" (Set (Var "U1")) "," (Set (Var "E")) ")" )))) ; 
 
theorem :: ALG_1:18 (Bool  "for" (Set (Var "U1")) "being"   ($#l1_unialg_1 :::"Universal_Algebra":::)  (Bool  "for" (Set (Var "E")) "being"    ($#m1_alg_1 :::"Congruence"::: )   "of" (Set (Var "U1")) "holds"  (Bool (Set   ($#k5_alg_1 :::"Nat_Hom"::: )   "(" (Set (Var "U1")) "," (Set (Var "E")) ")" )  ($#r3_alg_1 :::"is_epimorphism"::: )  (Set (Var "U1")) "," (Set   ($#k4_alg_1 :::"QuotUnivAlg"::: )   "(" (Set (Var "U1")) "," (Set (Var "E")) ")" )))) ; 
 definitionlet "U1", "U2" be   ($#l1_unialg_1 :::"Universal_Algebra":::); let "f" be   ($#m1_subset_1 :::"Function":::) "of" (Set (Const "U1")) "," (Set (Const "U2")); assume 
(Bool (Set (Const "f"))  ($#r1_alg_1 :::"is_homomorphism"::: )  (Set (Const "U1")) "," (Set (Const "U2")))
 ; func  :::"Cng"::: "f" ->    ($#m1_alg_1 :::"Congruence"::: )   "of" "U1" means :: ALG_1:def 12 (Bool  "for" (Set (Var "a")) "," (Set (Var "b")) "being"   ($#m1_subset_1 :::"Element":::) "of" "U1" "holds"   (Bool  "("  (Bool (Set  ($#k4_tarski :::"["::: ) (Set (Var "a")) "," (Set (Var "b")) ($#k4_tarski :::"]"::: ) )  ($#r2_hidden :::"in"::: )  it) "iff" (Bool (Set "f"  ($#k3_funct_2 :::"."::: )  (Set (Var "a")))  ($#r1_hidden :::"="::: )  (Set "f"  ($#k3_funct_2 :::"."::: )  (Set (Var "b"))))  ")" )); end; 








:: deftheorem    defines :::"Cng"::: ALG_1:def 12 :  (Bool  "for" (Set (Var "U1")) "," (Set (Var "U2")) "being"   ($#l1_unialg_1 :::"Universal_Algebra":::)  (Bool  "for" (Set (Var "f")) "being"   ($#m1_subset_1 :::"Function":::) "of" (Set (Var "U1")) "," (Set (Var "U2"))  "st" (Bool (Bool (Set (Var "f"))  ($#r1_alg_1 :::"is_homomorphism"::: )  (Set (Var "U1")) "," (Set (Var "U2")))) "holds"  (Bool  "for" (Set (Var "b4")) "being"    ($#m1_alg_1 :::"Congruence"::: )   "of" (Set (Var "U1")) "holds"   (Bool  "("  (Bool (Set (Var "b4"))  ($#r1_hidden :::"="::: )  (Set   ($#k6_alg_1 :::"Cng"::: )  (Set (Var "f")))) "iff" (Bool  "for" (Set (Var "a")) "," (Set (Var "b")) "being"   ($#m1_subset_1 :::"Element":::) "of" (Set (Var "U1")) "holds"   (Bool  "("  (Bool (Set  ($#k4_tarski :::"["::: ) (Set (Var "a")) "," (Set (Var "b")) ($#k4_tarski :::"]"::: ) )  ($#r2_hidden :::"in"::: )  (Set (Var "b4"))) "iff" (Bool (Set (Set (Var "f"))  ($#k3_funct_2 :::"."::: )  (Set (Var "a")))  ($#r1_hidden :::"="::: )  (Set (Set (Var "f"))  ($#k3_funct_2 :::"."::: )  (Set (Var "b"))))  ")" ))  ")" )))); 
 definitionlet "U1", "U2" be   ($#l1_unialg_1 :::"Universal_Algebra":::); let "f" be   ($#m1_subset_1 :::"Function":::) "of" (Set (Const "U1")) "," (Set (Const "U2")); assume 
(Bool (Set (Const "f"))  ($#r1_alg_1 :::"is_homomorphism"::: )  (Set (Const "U1")) "," (Set (Const "U2")))
 ; func  :::"HomQuot"::: "f" ->   ($#m1_subset_1 :::"Function":::) "of" (Set  "("  ($#k4_alg_1 :::"QuotUnivAlg"::: )   "(" "U1" "," (Set  "("  ($#k6_alg_1 :::"Cng"::: )  "f" ")" ) ")"  ")" ) "," "U2" means :: ALG_1:def 13 (Bool  "for" (Set (Var "a")) "being"   ($#m1_subset_1 :::"Element":::) "of" "U1" "holds"  (Bool (Set it  ($#k1_funct_1 :::"."::: )  (Set  "("  ($#k6_eqrel_1 :::"Class"::: )   "(" (Set  "("  ($#k6_alg_1 :::"Cng"::: )  "f" ")" ) "," (Set (Var "a")) ")"  ")" ))  ($#r1_hidden :::"="::: )  (Set "f"  ($#k3_funct_2 :::"."::: )  (Set (Var "a"))))); end; 








:: deftheorem    defines :::"HomQuot"::: ALG_1:def 13 :  (Bool  "for" (Set (Var "U1")) "," (Set (Var "U2")) "being"   ($#l1_unialg_1 :::"Universal_Algebra":::)  (Bool  "for" (Set (Var "f")) "being"   ($#m1_subset_1 :::"Function":::) "of" (Set (Var "U1")) "," (Set (Var "U2"))  "st" (Bool (Bool (Set (Var "f"))  ($#r1_alg_1 :::"is_homomorphism"::: )  (Set (Var "U1")) "," (Set (Var "U2")))) "holds"  (Bool  "for" (Set (Var "b4")) "being"   ($#m1_subset_1 :::"Function":::) "of" (Set  "("  ($#k4_alg_1 :::"QuotUnivAlg"::: )   "(" (Set (Var "U1")) "," (Set  "("  ($#k6_alg_1 :::"Cng"::: )  (Set (Var "f")) ")" ) ")"  ")" ) "," (Set (Var "U2")) "holds"   (Bool  "("  (Bool (Set (Var "b4"))  ($#r1_hidden :::"="::: )  (Set   ($#k7_alg_1 :::"HomQuot"::: )  (Set (Var "f")))) "iff" (Bool  "for" (Set (Var "a")) "being"   ($#m1_subset_1 :::"Element":::) "of" (Set (Var "U1")) "holds"  (Bool (Set (Set (Var "b4"))  ($#k1_funct_1 :::"."::: )  (Set  "("  ($#k6_eqrel_1 :::"Class"::: )   "(" (Set  "("  ($#k6_alg_1 :::"Cng"::: )  (Set (Var "f")) ")" ) "," (Set (Var "a")) ")"  ")" ))  ($#r1_hidden :::"="::: )  (Set (Set (Var "f"))  ($#k3_funct_2 :::"."::: )  (Set (Var "a")))))  ")" )))); 
 
theorem :: ALG_1:19 (Bool  "for" (Set (Var "U1")) "," (Set (Var "U2")) "being"   ($#l1_unialg_1 :::"Universal_Algebra":::)  (Bool  "for" (Set (Var "f")) "being"   ($#m1_subset_1 :::"Function":::) "of" (Set (Var "U1")) "," (Set (Var "U2"))  "st" (Bool (Bool (Set (Var "f"))  ($#r1_alg_1 :::"is_homomorphism"::: )  (Set (Var "U1")) "," (Set (Var "U2")))) "holds"  (Bool  "("  (Bool (Set   ($#k7_alg_1 :::"HomQuot"::: )  (Set (Var "f")))  ($#r1_alg_1 :::"is_homomorphism"::: )  (Set   ($#k4_alg_1 :::"QuotUnivAlg"::: )   "(" (Set (Var "U1")) "," (Set  "("  ($#k6_alg_1 :::"Cng"::: )  (Set (Var "f")) ")" ) ")" ) "," (Set (Var "U2"))) & (Bool (Set   ($#k7_alg_1 :::"HomQuot"::: )  (Set (Var "f")))  ($#r2_alg_1 :::"is_monomorphism"::: )  (Set   ($#k4_alg_1 :::"QuotUnivAlg"::: )   "(" (Set (Var "U1")) "," (Set  "("  ($#k6_alg_1 :::"Cng"::: )  (Set (Var "f")) ")" ) ")" ) "," (Set (Var "U2")))  ")" ))) ; 
 
theorem :: ALG_1:20 (Bool  "for" (Set (Var "U1")) "," (Set (Var "U2")) "being"   ($#l1_unialg_1 :::"Universal_Algebra":::)  (Bool  "for" (Set (Var "f")) "being"   ($#m1_subset_1 :::"Function":::) "of" (Set (Var "U1")) "," (Set (Var "U2"))  "st" (Bool (Bool (Set (Var "f"))  ($#r3_alg_1 :::"is_epimorphism"::: )  (Set (Var "U1")) "," (Set (Var "U2")))) "holds"  (Bool (Set   ($#k7_alg_1 :::"HomQuot"::: )  (Set (Var "f")))  ($#r4_alg_1 :::"is_isomorphism"::: )  (Set   ($#k4_alg_1 :::"QuotUnivAlg"::: )   "(" (Set (Var "U1")) "," (Set  "("  ($#k6_alg_1 :::"Cng"::: )  (Set (Var "f")) ")" ) ")" ) "," (Set (Var "U2"))))) ; 
 
theorem :: ALG_1:21 (Bool  "for" (Set (Var "U1")) "," (Set (Var "U2")) "being"   ($#l1_unialg_1 :::"Universal_Algebra":::)  (Bool  "for" (Set (Var "f")) "being"   ($#m1_subset_1 :::"Function":::) "of" (Set (Var "U1")) "," (Set (Var "U2"))  "st" (Bool (Bool (Set (Var "f"))  ($#r3_alg_1 :::"is_epimorphism"::: )  (Set (Var "U1")) "," (Set (Var "U2")))) "holds"  (Bool (Set   ($#k4_alg_1 :::"QuotUnivAlg"::: )   "(" (Set (Var "U1")) "," (Set  "("  ($#k6_alg_1 :::"Cng"::: )  (Set (Var "f")) ")" ) ")" ) "," (Set (Var "U2"))  ($#r5_alg_1 :::"are_isomorphic"::: )  ))) ;