:: AUTALG_1  semantic presentation begin  







theorem :: AUTALG_1:1 (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"))))  ($#r4_alg_1 :::"is_isomorphism"::: )  (Set (Var "UA")) "," (Set (Var "UA")))) ; 
 definitionlet "UA" be   ($#l1_unialg_1 :::"Universal_Algebra":::); func  :::"UAAut"::: "UA" ->    ($#m1_funct_2 :::"FUNCTION_DOMAIN"::: )   "of" (Set  "the"  ($#u1_struct_0 :::"carrier"::: )  "of" "UA") "," (Set  "the"  ($#u1_struct_0 :::"carrier"::: )  "of" "UA") means :: AUTALG_1: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"))  ($#r4_alg_1 :::"is_isomorphism"::: )  "UA" "," "UA")  ")" )); end; 





:: deftheorem    defines :::"UAAut"::: AUTALG_1: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_autalg_1 :::"UAAut"::: )  (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"))  ($#r4_alg_1 :::"is_isomorphism"::: )  (Set (Var "UA")) "," (Set (Var "UA")))  ")" ))  ")" ))); 
 
theorem :: AUTALG_1:2 (Bool  "for" (Set (Var "UA")) "being"   ($#l1_unialg_1 :::"Universal_Algebra":::) "holds"  (Bool (Set   ($#k1_autalg_1 :::"UAAut"::: )  (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 :: AUTALG_1:3 (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_autalg_1 :::"UAAut"::: )  (Set (Var "UA"))))) ; 
 
theorem :: AUTALG_1:4 (Bool  "for" (Set (Var "UA")) "being"   ($#l1_unialg_1 :::"Universal_Algebra":::)  (Bool  "for" (Set (Var "f")) "," (Set (Var "g")) "being"   ($#m1_subset_1 :::"Function":::) "of" (Set (Var "UA")) "," (Set (Var "UA"))  "st" (Bool (Bool (Set (Var "f")) "is"    ($#m2_funct_2 :::"Element"::: )   "of" (Set   ($#k1_autalg_1 :::"UAAut"::: )  (Set (Var "UA")))) & (Bool (Set (Var "g"))  ($#r1_hidden :::"="::: )  (Set (Set (Var "f"))  ($#k2_funct_1 :::"""::: )  ))) "holds"  (Bool (Set (Var "g"))  ($#r4_alg_1 :::"is_isomorphism"::: )  (Set (Var "UA")) "," (Set (Var "UA"))))) ; 
 
theorem :: AUTALG_1:5 (Bool  "for" (Set (Var "UA")) "being"   ($#l1_unialg_1 :::"Universal_Algebra":::)  (Bool  "for" (Set (Var "f")) "being"    ($#m2_funct_2 :::"Element"::: )   "of" (Set   ($#k1_autalg_1 :::"UAAut"::: )  (Set (Var "UA"))) "holds"  (Bool (Set (Set (Var "f"))  ($#k2_funct_1 :::"""::: )  )  ($#r2_hidden :::"in"::: )  (Set   ($#k1_autalg_1 :::"UAAut"::: )  (Set (Var "UA")))))) ; 
 
theorem :: AUTALG_1:6 (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_autalg_1 :::"UAAut"::: )  (Set (Var "UA"))) "holds"  (Bool (Set (Set (Var "f1"))  ($#k1_partfun1 :::"*"::: )  (Set (Var "f2")))  ($#r2_hidden :::"in"::: )  (Set   ($#k1_autalg_1 :::"UAAut"::: )  (Set (Var "UA")))))) ; 
 definitionlet "UA" be   ($#l1_unialg_1 :::"Universal_Algebra":::); func  :::"UAAutComp"::: "UA" ->   ($#m1_subset_1 :::"BinOp":::) "of" (Set  "("  ($#k1_autalg_1 :::"UAAut"::: )  "UA" ")" ) means :: AUTALG_1:def 2 (Bool  "for" (Set (Var "x")) "," (Set (Var "y")) "being"    ($#m2_funct_2 :::"Element"::: )   "of" (Set   ($#k1_autalg_1 :::"UAAut"::: )  "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 :::"UAAutComp"::: AUTALG_1: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_autalg_1 :::"UAAut"::: )  (Set (Var "UA")) ")" ) "holds"   (Bool  "("  (Bool (Set (Var "b2"))  ($#r1_hidden :::"="::: )  (Set   ($#k2_autalg_1 :::"UAAutComp"::: )  (Set (Var "UA")))) "iff" (Bool  "for" (Set (Var "x")) "," (Set (Var "y")) "being"    ($#m2_funct_2 :::"Element"::: )   "of" (Set   ($#k1_autalg_1 :::"UAAut"::: )  (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  :::"UAAutGroup"::: "UA" ->   ($#l3_algstr_0 :::"Group":::) equals :: AUTALG_1:def 3 (Set   ($#g3_algstr_0 :::"multMagma"::: )  "(#"  (Set  "("  ($#k1_autalg_1 :::"UAAut"::: )  "UA" ")" ) "," (Set  "("  ($#k2_autalg_1 :::"UAAutComp"::: )  "UA" ")" ) "#)" ); end; 





:: deftheorem    defines :::"UAAutGroup"::: AUTALG_1:def 3 :  (Bool  "for" (Set (Var "UA")) "being"   ($#l1_unialg_1 :::"Universal_Algebra":::) "holds"  (Bool (Set   ($#k3_autalg_1 :::"UAAutGroup"::: )  (Set (Var "UA")))  ($#r1_hidden :::"="::: )  (Set   ($#g3_algstr_0 :::"multMagma"::: )  "(#"  (Set  "("  ($#k1_autalg_1 :::"UAAut"::: )  (Set (Var "UA")) ")" ) "," (Set  "("  ($#k2_autalg_1 :::"UAAutComp"::: )  (Set (Var "UA")) ")" ) "#)" ))); 
 registrationlet "UA" be   ($#l1_unialg_1 :::"Universal_Algebra":::); 
cluster (Set   ($#k3_autalg_1 :::"UAAutGroup"::: )  "UA") ->   ($#v15_algstr_0 :::"strict"::: )   ; 
end; 
theorem :: AUTALG_1:7 (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_autalg_1 :::"UAAutGroup"::: )  (Set (Var "UA")) ")" )  (Bool  "for" (Set (Var "f")) "," (Set (Var "g")) "being"    ($#m2_funct_2 :::"Element"::: )   "of" (Set   ($#k1_autalg_1 :::"UAAut"::: )  (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 :: AUTALG_1:8 (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_autalg_1 :::"UAAutGroup"::: )  (Set (Var "UA")) ")" )))) ; 
 
theorem :: AUTALG_1:9 (Bool  "for" (Set (Var "UA")) "being"   ($#l1_unialg_1 :::"Universal_Algebra":::)  (Bool  "for" (Set (Var "f")) "being"    ($#m2_funct_2 :::"Element"::: )   "of" (Set   ($#k1_autalg_1 :::"UAAut"::: )  (Set (Var "UA")))  (Bool  "for" (Set (Var "g")) "being"   ($#m1_subset_1 :::"Element":::) "of" (Set  "("  ($#k3_autalg_1 :::"UAAutGroup"::: )  (Set (Var "UA")) ")" )  "st" (Bool (Bool (Set (Var "f"))  ($#r1_hidden :::"="::: )  (Set (Var "g")))) "holds"  (Bool (Set (Set (Var "f"))  ($#k2_funct_1 :::"""::: )  )  ($#r1_hidden :::"="::: )  (Set (Set (Var "g"))  ($#k2_group_1 :::"""::: )  ))))) ; 
 begin  








theorem :: AUTALG_1:10 (Bool  "for" (Set (Var "I")) "being"    ($#m1_hidden :::"set"::: )    (Bool  "for" (Set (Var "A")) "," (Set (Var "B")) "," (Set (Var "C")) "being"   ($#m1_hidden :::"ManySortedSet":::) "of" (Set (Var "I"))  "st" (Bool (Bool (Set (Var "A"))  ($#r1_pzfmisc1 :::"is_transformable_to"::: )  (Set (Var "B"))) & (Bool (Set (Var "B"))  ($#r1_pzfmisc1 :::"is_transformable_to"::: )  (Set (Var "C")))) "holds"  (Bool (Set (Var "A"))  ($#r1_pzfmisc1 :::"is_transformable_to"::: )  (Set (Var "C"))))) ; 
 
theorem :: AUTALG_1:11 (Bool  "for" (Set (Var "x")) "being"    ($#m1_hidden :::"set"::: )    (Bool  "for" (Set (Var "A")) "being"   ($#m1_hidden :::"ManySortedSet":::) "of" (Set  ($#k1_tarski :::"{"::: ) (Set (Var "x")) ($#k1_tarski :::"}"::: ) ) "holds"  (Bool (Set (Var "A"))  ($#r1_hidden :::"="::: )  (Set (Set (Var "x"))  ($#k16_funcop_1 :::".-->"::: )  (Set  "(" (Set (Var "A"))  ($#k1_funct_1 :::"."::: )  (Set (Var "x")) ")" ))))) ; 
 
theorem :: AUTALG_1:12 (Bool  "for" (Set (Var "I")) "being"    ($#m1_hidden :::"set"::: )    (Bool  "for" (Set (Var "A")) "," (Set (Var "B")) "being" bbbadV2_RELAT_1()  ($#m1_hidden :::"ManySortedSet":::) "of" (Set (Var "I"))  (Bool  "for" (Set (Var "F")) "being"    ($#m2_pboole :::"ManySortedFunction"::: )   "of" (Set (Var "A")) "," (Set (Var "B"))  "st" (Bool (Bool (Set (Var "F")) "is"   ($#v1_msualg_3 :::""1-1""::: )  ) & (Bool (Set (Var "F")) "is"   ($#v2_msualg_3 :::""onto""::: )  )) "holds"  (Bool  "("  (Bool (Set (Set (Var "F"))  ($#k4_msualg_3 :::""""::: )  ) "is"   ($#v1_msualg_3 :::""1-1""::: )  ) & (Bool (Set (Set (Var "F"))  ($#k4_msualg_3 :::""""::: )  ) "is"   ($#v2_msualg_3 :::""onto""::: )  )  ")" )))) ; 
 
theorem :: AUTALG_1:13 (Bool  "for" (Set (Var "I")) "being"    ($#m1_hidden :::"set"::: )    (Bool  "for" (Set (Var "A")) "," (Set (Var "B")) "being" bbbadV2_RELAT_1()  ($#m1_hidden :::"ManySortedSet":::) "of" (Set (Var "I"))  (Bool  "for" (Set (Var "F")) "being"    ($#m2_pboole :::"ManySortedFunction"::: )   "of" (Set (Var "A")) "," (Set (Var "B"))  "st" (Bool (Bool (Set (Var "F")) "is"   ($#v1_msualg_3 :::""1-1""::: )  ) & (Bool (Set (Var "F")) "is"   ($#v2_msualg_3 :::""onto""::: )  )) "holds"  (Bool (Set (Set  "(" (Set (Var "F"))  ($#k4_msualg_3 :::""""::: )  ")" )  ($#k4_msualg_3 :::""""::: )  )  ($#r6_pboole :::"="::: )  (Set (Var "F")))))) ; 
 
theorem :: AUTALG_1:14 (Bool  "for" (Set (Var "F")) "," (Set (Var "G")) "being"   ($#v1_funcop_1 :::"Function-yielding"::: )    ($#m1_hidden :::"Function":::)  "st" (Bool (Bool (Set (Var "F")) "is"   ($#v1_msualg_3 :::""1-1""::: )  ) & (Bool (Set (Var "G")) "is"   ($#v1_msualg_3 :::""1-1""::: )  )) "holds"  (Bool (Set (Set (Var "G"))  ($#k8_pboole :::"**"::: )  (Set (Var "F"))) "is"   ($#v1_msualg_3 :::""1-1""::: )  )) ; 
 
theorem :: AUTALG_1:15 (Bool  "for" (Set (Var "I")) "being"    ($#m1_hidden :::"set"::: )    (Bool  "for" (Set (Var "A")) "being"   ($#m1_hidden :::"ManySortedSet":::) "of" (Set (Var "I"))  (Bool  "for" (Set (Var "B")) "," (Set (Var "C")) "being" bbbadV2_RELAT_1()  ($#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 "G")) "being"    ($#m2_pboole :::"ManySortedFunction"::: )   "of" (Set (Var "B")) "," (Set (Var "C"))  "st" (Bool (Bool (Set (Var "F")) "is"   ($#v2_msualg_3 :::""onto""::: )  ) & (Bool (Set (Var "G")) "is"   ($#v2_msualg_3 :::""onto""::: )  )) "holds"  (Bool (Set (Set (Var "G"))  ($#k3_msualg_3 :::"**"::: )  (Set (Var "F"))) "is"   ($#v2_msualg_3 :::""onto""::: )  )))))) ; 
 
theorem :: AUTALG_1:16 (Bool  "for" (Set (Var "I")) "being"    ($#m1_hidden :::"set"::: )    (Bool  "for" (Set (Var "A")) "," (Set (Var "B")) "," (Set (Var "C")) "being" bbbadV2_RELAT_1()  ($#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 "G")) "being"    ($#m2_pboole :::"ManySortedFunction"::: )   "of" (Set (Var "B")) "," (Set (Var "C"))  "st" (Bool (Bool (Set (Var "F")) "is"   ($#v1_msualg_3 :::""1-1""::: )  ) & (Bool (Set (Var "F")) "is"   ($#v2_msualg_3 :::""onto""::: )  ) & (Bool (Set (Var "G")) "is"   ($#v1_msualg_3 :::""1-1""::: )  ) & (Bool (Set (Var "G")) "is"   ($#v2_msualg_3 :::""onto""::: )  )) "holds"  (Bool (Set (Set  "(" (Set (Var "G"))  ($#k3_msualg_3 :::"**"::: )  (Set (Var "F")) ")" )  ($#k4_msualg_3 :::""""::: )  )  ($#r6_pboole :::"="::: )  (Set (Set  "(" (Set (Var "F"))  ($#k4_msualg_3 :::""""::: )  ")" )  ($#k3_msualg_3 :::"**"::: )  (Set  "(" (Set (Var "G"))  ($#k4_msualg_3 :::""""::: )  ")" ))))))) ; 
 
theorem :: AUTALG_1:17 (Bool  "for" (Set (Var "I")) "being"    ($#m1_hidden :::"set"::: )    (Bool  "for" (Set (Var "A")) "," (Set (Var "B")) "being" bbbadV2_RELAT_1()  ($#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 "G")) "being"    ($#m2_pboole :::"ManySortedFunction"::: )   "of" (Set (Var "B")) "," (Set (Var "A"))  "st" (Bool (Bool (Set (Var "F")) "is"   ($#v1_msualg_3 :::""1-1""::: )  ) & (Bool (Set (Var "F")) "is"   ($#v2_msualg_3 :::""onto""::: )  ) & (Bool (Set (Set (Var "G"))  ($#k3_msualg_3 :::"**"::: )  (Set (Var "F")))  ($#r6_pboole :::"="::: )  (Set   ($#k2_msualg_3 :::"id"::: )  (Set (Var "A"))))) "holds"  (Bool (Set (Var "G"))  ($#r6_pboole :::"="::: )  (Set (Set (Var "F"))  ($#k4_msualg_3 :::""""::: )  )))))) ; 
 
theorem :: AUTALG_1:18 (Bool  "for" (Set (Var "I")) "being"    ($#m1_hidden :::"set"::: )    (Bool  "for" (Set (Var "A")) "," (Set (Var "B")) "being"   ($#m1_hidden :::"ManySortedSet":::) "of" (Set (Var "I"))  "st" (Bool (Bool (Set (Var "A"))  ($#r1_pzfmisc1 :::"is_transformable_to"::: )  (Set (Var "B")))) "holds"  (Bool (Set   ($#k7_pboole :::"(Funcs)"::: )   "(" (Set (Var "A")) "," (Set (Var "B")) ")" ) "is" bbbadV2_RELAT_1()))) ; 
 definitionlet "I" be    ($#m1_hidden :::"set"::: )  ; let "A", "B" be   ($#m1_hidden :::"ManySortedSet":::) "of" (Set (Const "I")); assume 
(Bool (Set (Const "A"))  ($#r1_pzfmisc1 :::"is_transformable_to"::: )  (Set (Const "B")))
 ; func  :::"MSFuncs":::  "(" "A" "," "B" ")"  ->  ($#~v1_xboole_0  "non"   ($#v1_xboole_0 :::"empty"::: )   )    ($#m1_hidden :::"set"::: )   equals :: AUTALG_1:def 4 (Set   ($#k4_card_3 :::"product"::: )  (Set  "("  ($#k7_pboole :::"(Funcs)"::: )   "(" "A" "," "B" ")"  ")" )); end; 








:: deftheorem    defines :::"MSFuncs"::: AUTALG_1:def 4 :  (Bool  "for" (Set (Var "I")) "being"    ($#m1_hidden :::"set"::: )    (Bool  "for" (Set (Var "A")) "," (Set (Var "B")) "being"   ($#m1_hidden :::"ManySortedSet":::) "of" (Set (Var "I"))  "st" (Bool (Bool (Set (Var "A"))  ($#r1_pzfmisc1 :::"is_transformable_to"::: )  (Set (Var "B")))) "holds"  (Bool (Set   ($#k4_autalg_1 :::"MSFuncs"::: )   "(" (Set (Var "A")) "," (Set (Var "B")) ")" )  ($#r1_hidden :::"="::: )  (Set   ($#k4_card_3 :::"product"::: )  (Set  "("  ($#k7_pboole :::"(Funcs)"::: )   "(" (Set (Var "A")) "," (Set (Var "B")) ")"  ")" ))))); 
 
theorem :: AUTALG_1:19 (Bool  "for" (Set (Var "I")) "being"    ($#m1_hidden :::"set"::: )    (Bool  "for" (Set (Var "A")) "," (Set (Var "B")) "being"   ($#m1_hidden :::"ManySortedSet":::) "of" (Set (Var "I"))  "st" (Bool (Bool (Set (Var "A"))  ($#r1_pzfmisc1 :::"is_transformable_to"::: )  (Set (Var "B")))) "holds"  (Bool  "for" (Set (Var "x")) "being"    ($#m1_hidden :::"set"::: )    "st" (Bool (Bool (Set (Var "x"))  ($#r2_hidden :::"in"::: )  (Set   ($#k4_autalg_1 :::"MSFuncs"::: )   "(" (Set (Var "A")) "," (Set (Var "B")) ")" ))) "holds"  (Bool (Set (Var "x")) "is"    ($#m2_pboole :::"ManySortedFunction"::: )   "of" (Set (Var "A")) "," (Set (Var "B")))))) ; 
 
theorem :: AUTALG_1:20 (Bool  "for" (Set (Var "I")) "being"    ($#m1_hidden :::"set"::: )    (Bool  "for" (Set (Var "A")) "," (Set (Var "B")) "being"   ($#m1_hidden :::"ManySortedSet":::) "of" (Set (Var "I"))  "st" (Bool (Bool (Set (Var "A"))  ($#r1_pzfmisc1 :::"is_transformable_to"::: )  (Set (Var "B")))) "holds"  (Bool  "for" (Set (Var "g")) "being"    ($#m2_pboole :::"ManySortedFunction"::: )   "of" (Set (Var "A")) "," (Set (Var "B")) "holds"  (Bool (Set (Var "g"))  ($#r2_hidden :::"in"::: )  (Set   ($#k4_autalg_1 :::"MSFuncs"::: )   "(" (Set (Var "A")) "," (Set (Var "B")) ")" ))))) ; 
 registrationlet "I" be    ($#m1_hidden :::"set"::: )  ; let "A" be   ($#m1_hidden :::"ManySortedSet":::) "of" (Set (Const "I")); 
cluster (Set   ($#k7_pboole :::"(Funcs)"::: )   "(" "A" "," "A" ")" ) -> bbbadV2_RELAT_1() ; 
end; definitionlet "I" be    ($#m1_hidden :::"set"::: )  ; let "D" be   ($#m1_hidden :::"ManySortedSet":::) "of" (Set (Const "I")); let "A" be  ($#~v1_xboole_0  "non"   ($#v1_xboole_0 :::"empty"::: )   )   ($#m1_subset_1 :::"Subset":::) "of" (Set  "("  ($#k4_autalg_1 :::"MSFuncs"::: )   "(" (Set (Const "D")) "," (Set (Const "D")) ")"  ")" ); :: original: :::"Element"::: redefine mode  :::"Element":::  "of" "A" ->    ($#m2_pboole :::"ManySortedFunction"::: )   "of" "D" "," "D"; end; registrationlet "I" be    ($#m1_hidden :::"set"::: )  ; let "A" be   ($#m1_hidden :::"ManySortedSet":::) "of" (Set (Const "I")); 
cluster (Set   ($#k2_msualg_3 :::"id"::: )  "A") ->   ($#v2_msualg_3 :::""onto""::: )   ; 

cluster (Set   ($#k2_msualg_3 :::"id"::: )  "A") ->   ($#v1_msualg_3 :::""1-1""::: )   ; 
end; begin  






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", "U2" be   ($#v4_msualg_1 :::"non-empty"::: )     ($#l3_msualg_1 :::"MSAlgebra"::: )   "over" (Set (Const "S")); mode MSFunctionSet of "U1" "," "U2" is  ($#~v1_xboole_0  "non"   ($#v1_xboole_0 :::"empty"::: )   )   ($#m1_subset_1 :::"Subset":::) "of" (Set  "("  ($#k4_autalg_1 :::"MSFuncs"::: )   "(" (Set  "the"  ($#u3_msualg_1 :::"Sorts"::: )  "of" "U1") "," (Set  "the"  ($#u3_msualg_1 :::"Sorts"::: )  "of" "U2") ")"  ")" ); end; 
theorem :: AUTALG_1:21 (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_autalg_1 :::"MSFuncs"::: )   "(" (Set  "the"  ($#u3_msualg_1 :::"Sorts"::: )  "of" (Set (Var "U1"))) "," (Set  "the"  ($#u3_msualg_1 :::"Sorts"::: )  "of" (Set (Var "U1"))) ")" )))) ; 
 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  :::"MSAAut"::: "U1" ->   ($#m1_subset_1 :::"MSFunctionSet":::) "of" "U1" "," "U1" means :: AUTALG_1:def 5 (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"))  ($#r4_msualg_3 :::"is_isomorphism"::: )  "U1" "," "U1")  ")" )); end; 






:: deftheorem    defines :::"MSAAut"::: AUTALG_1: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 :::"MSFunctionSet":::) "of" (Set (Var "U1")) "," (Set (Var "U1")) "holds"   (Bool  "("  (Bool (Set (Var "b3"))  ($#r1_hidden :::"="::: )  (Set   ($#k5_autalg_1 :::"MSAAut"::: )  (Set (Var "U1")))) "iff" (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"))  ($#r4_msualg_3 :::"is_isomorphism"::: )  (Set (Var "U1")) "," (Set (Var "U1")))  ")" ))  ")" )))); 
 
theorem :: AUTALG_1:22 (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 "f")) "being"    ($#m1_autalg_1 :::"Element"::: )   "of" (Set   ($#k5_autalg_1 :::"MSAAut"::: )  (Set (Var "U1"))) "holds"  (Bool (Set (Var "f"))  ($#r2_hidden :::"in"::: )  (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 :: AUTALG_1:23 (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   ($#k5_autalg_1 :::"MSAAut"::: )  (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 :: AUTALG_1:24 (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   ($#k5_autalg_1 :::"MSAAut"::: )  (Set (Var "U1")))))) ; 
 
theorem :: AUTALG_1:25 (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 "f")) "being"    ($#m1_autalg_1 :::"Element"::: )   "of" (Set   ($#k5_autalg_1 :::"MSAAut"::: )  (Set (Var "U1"))) "holds"  (Bool (Set (Set (Var "f"))  ($#k4_msualg_3 :::""""::: )  )  ($#r2_hidden :::"in"::: )  (Set   ($#k5_autalg_1 :::"MSAAut"::: )  (Set (Var "U1"))))))) ; 
 
theorem :: AUTALG_1:26 (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   ($#k5_autalg_1 :::"MSAAut"::: )  (Set (Var "U1"))) "holds"  (Bool (Set (Set (Var "f1"))  ($#k3_msualg_3 :::"**"::: )  (Set (Var "f2")))  ($#r2_hidden :::"in"::: )  (Set   ($#k5_autalg_1 :::"MSAAut"::: )  (Set (Var "U1"))))))) ; 
 
theorem :: AUTALG_1:27 (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_autalg_1 :::"UAAut"::: )  (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   ($#k5_autalg_1 :::"MSAAut"::: )  (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  :::"MSAAutComp"::: "U1" ->   ($#m1_subset_1 :::"BinOp":::) "of" (Set  "("  ($#k5_autalg_1 :::"MSAAut"::: )  "U1" ")" ) means :: AUTALG_1:def 6 (Bool  "for" (Set (Var "x")) "," (Set (Var "y")) "being"    ($#m1_autalg_1 :::"Element"::: )   "of" (Set   ($#k5_autalg_1 :::"MSAAut"::: )  "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 :::"MSAAutComp"::: AUTALG_1: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"   ($#m1_subset_1 :::"BinOp":::) "of" (Set  "("  ($#k5_autalg_1 :::"MSAAut"::: )  (Set (Var "U1")) ")" ) "holds"   (Bool  "("  (Bool (Set (Var "b3"))  ($#r1_hidden :::"="::: )  (Set   ($#k6_autalg_1 :::"MSAAutComp"::: )  (Set (Var "U1")))) "iff" (Bool  "for" (Set (Var "x")) "," (Set (Var "y")) "being"    ($#m1_autalg_1 :::"Element"::: )   "of" (Set   ($#k5_autalg_1 :::"MSAAut"::: )  (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  :::"MSAAutGroup"::: "U1" ->   ($#l3_algstr_0 :::"Group":::) equals :: AUTALG_1:def 7 (Set   ($#g3_algstr_0 :::"multMagma"::: )  "(#"  (Set  "("  ($#k5_autalg_1 :::"MSAAut"::: )  "U1" ")" ) "," (Set  "("  ($#k6_autalg_1 :::"MSAAutComp"::: )  "U1" ")" ) "#)" ); end; 






:: deftheorem    defines :::"MSAAutGroup"::: AUTALG_1:def 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   ($#k7_autalg_1 :::"MSAAutGroup"::: )  (Set (Var "U1")))  ($#r1_hidden :::"="::: )  (Set   ($#g3_algstr_0 :::"multMagma"::: )  "(#"  (Set  "("  ($#k5_autalg_1 :::"MSAAut"::: )  (Set (Var "U1")) ")" ) "," (Set  "("  ($#k6_autalg_1 :::"MSAAutComp"::: )  (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   ($#k7_autalg_1 :::"MSAAutGroup"::: )  "U1") ->   ($#v15_algstr_0 :::"strict"::: )   ; 
end; 
theorem :: AUTALG_1:28 (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  "("  ($#k7_autalg_1 :::"MSAAutGroup"::: )  (Set (Var "U1")) ")" )  (Bool  "for" (Set (Var "f")) "," (Set (Var "g")) "being"    ($#m1_autalg_1 :::"Element"::: )   "of" (Set   ($#k5_autalg_1 :::"MSAAut"::: )  (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 :: AUTALG_1:29 (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  "("  ($#k7_autalg_1 :::"MSAAutGroup"::: )  (Set (Var "U1")) ")" ))))) ; 
 
theorem :: AUTALG_1:30 (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 "f")) "being"    ($#m1_autalg_1 :::"Element"::: )   "of" (Set   ($#k5_autalg_1 :::"MSAAut"::: )  (Set (Var "U1")))  (Bool  "for" (Set (Var "g")) "being"   ($#m1_subset_1 :::"Element":::) "of" (Set  "("  ($#k7_autalg_1 :::"MSAAutGroup"::: )  (Set (Var "U1")) ")" )  "st" (Bool (Bool (Set (Var "f"))  ($#r1_hidden :::"="::: )  (Set (Var "g")))) "holds"  (Bool (Set (Set (Var "f"))  ($#k4_msualg_3 :::""""::: )  )  ($#r1_hidden :::"="::: )  (Set (Set (Var "g"))  ($#k2_group_1 :::"""::: )  )))))) ; 
 begin  
theorem :: AUTALG_1:31 (Bool  "for" (Set (Var "UA1")) "," (Set (Var "UA2")) "being"   ($#l1_unialg_1 :::"Universal_Algebra":::)  "st" (Bool (Bool (Set (Var "UA1")) "," (Set (Var "UA2"))  ($#r1_unialg_2 :::"are_similar"::: )  )) "holds"  (Bool  "for" (Set (Var "F")) "being"   ($#m2_pboole :::"ManySortedFunction":::) "of" (Set  "("  ($#k9_msualg_1 :::"MSAlg"::: )  (Set (Var "UA1")) ")" ) "," (Set  "(" (Set  "("  ($#k9_msualg_1 :::"MSAlg"::: )  (Set (Var "UA2")) ")" )  ($#k1_msuhom_1 :::"Over"::: )  (Set  "("  ($#k6_msualg_1 :::"MSSign"::: )  (Set (Var "UA1")) ")" ) ")" ) "holds"  (Bool (Set (Set (Var "F"))  ($#k1_funct_1 :::"."::: )  (Set  ($#k6_numbers :::"0"::: ) )) "is"   ($#m1_subset_1 :::"Function":::) "of" (Set (Var "UA1")) "," (Set (Var "UA2"))))) ; 
 
theorem :: AUTALG_1:32 (Bool  "for" (Set (Var "UA")) "being"   ($#l1_unialg_1 :::"Universal_Algebra":::)  (Bool  "for" (Set (Var "f")) "being"    ($#m2_funct_2 :::"Element"::: )   "of" (Set   ($#k1_autalg_1 :::"UAAut"::: )  (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")) ")" )))) ; 
 
theorem :: AUTALG_1:33 (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_autalg_1 :::"UAAut"::: )  (Set (Var "UA")))) & (Bool  "("   "for" (Set (Var "x")) "being"    ($#m1_hidden :::"set"::: )    "st" (Bool (Bool (Set (Var "x"))  ($#r2_hidden :::"in"::: )  (Set   ($#k1_autalg_1 :::"UAAut"::: )  (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_autalg_1 :::"UAAutGroup"::: )  (Set (Var "UA")) ")" ) "," (Set  "("  ($#k7_autalg_1 :::"MSAAutGroup"::: )  (Set  "("  ($#k9_msualg_1 :::"MSAlg"::: )  (Set (Var "UA")) ")" ) ")" )))) ; 
 
theorem :: AUTALG_1:34 (Bool  "for" (Set (Var "UA")) "being"   ($#l1_unialg_1 :::"Universal_Algebra":::)  (Bool  "for" (Set (Var "h")) "being"   ($#m1_subset_1 :::"Homomorphism":::) "of" (Set  "("  ($#k3_autalg_1 :::"UAAutGroup"::: )  (Set (Var "UA")) ")" ) "," (Set  "("  ($#k7_autalg_1 :::"MSAAutGroup"::: )  (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_autalg_1 :::"UAAut"::: )  (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 :: AUTALG_1:35 (Bool  "for" (Set (Var "UA")) "being"   ($#l1_unialg_1 :::"Universal_Algebra":::) "holds"  (Bool (Set   ($#k3_autalg_1 :::"UAAutGroup"::: )  (Set (Var "UA"))) "," (Set   ($#k7_autalg_1 :::"MSAAutGroup"::: )  (Set  "("  ($#k9_msualg_1 :::"MSAlg"::: )  (Set (Var "UA")) ")" ))  ($#r2_group_6 :::"are_isomorphic"::: )  )) ;