:: MSUALG_9 semantic presentation begin registrationlet "I" be ($#m1_hidden :::"set"::: ) ; let "M" be ($#m1_hidden :::"ManySortedSet":::) "of" (Set (Const "I")); cluster ($#v1_relat_1 :::"Relation-like"::: ) "I" ($#v4_relat_1 :::"-defined"::: ) ($#v1_funct_1 :::"Function-like"::: ) ($#v1_partfun1 :::"total"::: ) bbbadV2_FINSET_1() for ($#m1_subset_1 :::"Element"::: ) "of" (Set ($#k6_closure2 :::"Bool"::: ) "M"); end; registrationlet "I" be ($#m1_hidden :::"set"::: ) ; let "M" be bbbadV2_RELAT_1() ($#m1_hidden :::"ManySortedSet":::) "of" (Set (Const "I")); cluster ($#v1_relat_1 :::"Relation-like"::: ) bbbadV2_RELAT_1() "I" ($#v4_relat_1 :::"-defined"::: ) ($#v1_funct_1 :::"Function-like"::: ) ($#v1_partfun1 :::"total"::: ) bbbadV2_FINSET_1() for ($#m3_pboole :::"ManySortedSubset"::: ) "of" "M"; 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 "A" be ($#v4_msualg_1 :::"non-empty"::: ) ($#l3_msualg_1 :::"MSAlgebra"::: ) "over" (Set (Const "S")); let "o" be ($#m1_subset_1 :::"OperSymbol":::) "of" (Set (Const "S")); cluster -> ($#v1_finseq_1 :::"FinSequence-like"::: ) for ($#m1_subset_1 :::"Element"::: ) "of" (Set ($#k3_msualg_1 :::"Args"::: ) "(" "o" "," "A" ")" ); 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 "I" be ($#m1_hidden :::"set"::: ) ; let "s" be ($#m1_subset_1 :::"SortSymbol":::) "of" (Set (Const "S")); let "F" be ($#m1_pralg_2 :::"MSAlgebra-Family"::: ) "of" (Set (Const "I")) "," (Set (Const "S")); cluster -> ($#v1_relat_1 :::"Relation-like"::: ) ($#v1_funct_1 :::"Function-like"::: ) for ($#m1_subset_1 :::"Element"::: ) "of" (Set (Set "(" ($#k10_pralg_2 :::"SORTS"::: ) "F" ")" ) ($#k1_funct_1 :::"."::: ) "s"); 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 "X" be bbbadV2_RELAT_1() ($#m1_hidden :::"ManySortedSet":::) "of" (Set "the" ($#u1_struct_0 :::"carrier"::: ) "of" (Set (Const "S"))); cluster (Set ($#k13_msafree :::"FreeGen"::: ) "X") -> bbbadV2_RELAT_1() ($#v1_msafree :::"free"::: ) ; 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 "X" be bbbadV2_RELAT_1() ($#m1_hidden :::"ManySortedSet":::) "of" (Set "the" ($#u1_struct_0 :::"carrier"::: ) "of" (Set (Const "S"))); cluster (Set ($#k11_msafree :::"FreeMSA"::: ) "X") -> ($#v2_msafree :::"free"::: ) ; 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 "A", "B" be ($#v4_msualg_1 :::"non-empty"::: ) ($#l3_msualg_1 :::"MSAlgebra"::: ) "over" (Set (Const "S")); cluster (Set ($#k8_pralg_2 :::"[:"::: ) "A" "," "B" ($#k8_pralg_2 :::":]"::: ) ) -> ($#v4_msualg_1 :::"non-empty"::: ) ; end; theorem :: MSUALG_9:1 (Bool "for" (Set (Var "a")) "," (Set (Var "X")) "," (Set (Var "Y")) "being" ($#m1_hidden :::"set"::: ) (Bool "for" (Set (Var "f")) "being" ($#m1_hidden :::"Function":::) "st" (Bool (Bool (Set (Var "a")) ($#r2_hidden :::"in"::: ) (Set ($#k9_xtuple_0 :::"dom"::: ) (Set (Var "f")))) & (Bool (Set (Set (Var "f")) ($#k1_funct_1 :::"."::: ) (Set (Var "a"))) ($#r2_hidden :::"in"::: ) (Set ($#k2_zfmisc_1 :::"[:"::: ) (Set (Var "X")) "," (Set (Var "Y")) ($#k2_zfmisc_1 :::":]"::: ) ))) "holds" (Bool (Set (Set (Var "f")) ($#k1_funct_1 :::"."::: ) (Set (Var "a"))) ($#r1_hidden :::"="::: ) (Set ($#k4_tarski :::"["::: ) (Set "(" (Set "(" ($#k11_mcart_1 :::"pr1"::: ) (Set (Var "f")) ")" ) ($#k1_funct_1 :::"."::: ) (Set (Var "a")) ")" ) "," (Set "(" (Set "(" ($#k12_mcart_1 :::"pr2"::: ) (Set (Var "f")) ")" ) ($#k1_funct_1 :::"."::: ) (Set (Var "a")) ")" ) ($#k4_tarski :::"]"::: ) )))) ; theorem :: MSUALG_9:2 (Bool "for" (Set (Var "X")) "being" ($#~v1_xboole_0 "non" ($#v1_xboole_0 :::"empty"::: ) ) ($#m1_hidden :::"set"::: ) (Bool "for" (Set (Var "Y")) "being" ($#m1_hidden :::"set"::: ) (Bool "for" (Set (Var "f")) "being" ($#m1_subset_1 :::"Function":::) "of" (Set (Var "X")) "," (Set ($#k1_tarski :::"{"::: ) (Set (Var "Y")) ($#k1_tarski :::"}"::: ) ) "holds" (Bool (Set ($#k2_relset_1 :::"rng"::: ) (Set (Var "f"))) ($#r1_hidden :::"="::: ) (Set ($#k1_tarski :::"{"::: ) (Set (Var "Y")) ($#k1_tarski :::"}"::: ) ))))) ; theorem :: MSUALG_9:3 (Bool "for" (Set (Var "I")) "being" ($#m1_hidden :::"set"::: ) "holds" (Bool (Set ($#k8_eqrel_1 :::"Class"::: ) (Set "(" ($#k1_eqrel_1 :::"nabla"::: ) (Set (Var "I")) ")" )) ($#r1_tarski :::"c="::: ) (Set ($#k1_tarski :::"{"::: ) (Set (Var "I")) ($#k1_tarski :::"}"::: ) ))) ; theorem :: MSUALG_9:4 (Bool "for" (Set (Var "I")) "being" ($#~v1_xboole_0 "non" ($#v1_xboole_0 :::"empty"::: ) ) ($#m1_hidden :::"set"::: ) "holds" (Bool (Set ($#k8_eqrel_1 :::"Class"::: ) (Set "(" ($#k1_eqrel_1 :::"nabla"::: ) (Set (Var "I")) ")" )) ($#r1_hidden :::"="::: ) (Set ($#k1_tarski :::"{"::: ) (Set (Var "I")) ($#k1_tarski :::"}"::: ) ))) ; theorem :: MSUALG_9:5 (Bool "for" (Set (Var "I")) "," (Set (Var "a")) "being" ($#m1_hidden :::"set"::: ) (Bool "ex" (Set (Var "A")) "being" ($#m1_hidden :::"ManySortedSet":::) "of" (Set (Var "I")) "st" (Bool (Set ($#k1_pzfmisc1 :::"{"::: ) (Set (Var "A")) ($#k1_pzfmisc1 :::"}"::: ) ) ($#r6_pboole :::"="::: ) (Set (Set (Var "I")) ($#k7_funcop_1 :::"-->"::: ) (Set ($#k1_tarski :::"{"::: ) (Set (Var "a")) ($#k1_tarski :::"}"::: ) ))))) ; theorem :: MSUALG_9:6 (Bool "for" (Set (Var "I")) "being" ($#m1_hidden :::"set"::: ) (Bool "for" (Set (Var "A")) "being" ($#m1_hidden :::"ManySortedSet":::) "of" (Set (Var "I")) (Bool "ex" (Set (Var "B")) "being" bbbadV2_RELAT_1() ($#m1_hidden :::"ManySortedSet":::) "of" (Set (Var "I")) "st" (Bool (Set (Var "A")) ($#r2_pboole :::"c="::: ) (Set (Var "B")))))) ; theorem :: MSUALG_9:7 (Bool "for" (Set (Var "I")) "being" ($#m1_hidden :::"set"::: ) (Bool "for" (Set (Var "M")) "being" bbbadV2_RELAT_1() ($#m1_hidden :::"ManySortedSet":::) "of" (Set (Var "I")) (Bool "for" (Set (Var "B")) "being" bbbadV2_FINSET_1() ($#m3_pboole :::"ManySortedSubset"::: ) "of" (Set (Var "M")) (Bool "ex" (Set (Var "C")) "being" bbbadV2_RELAT_1() bbbadV2_FINSET_1() ($#m3_pboole :::"ManySortedSubset"::: ) "of" (Set (Var "M")) "st" (Bool (Set (Var "B")) ($#r2_pboole :::"c="::: ) (Set (Var "C"))))))) ; theorem :: MSUALG_9:8 (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")) (Bool "for" (Set (Var "F")) "," (Set (Var "G")) "being" ($#m2_pboole :::"ManySortedFunction"::: ) "of" (Set (Var "A")) "," (Set ($#k1_pzfmisc1 :::"{"::: ) (Set (Var "B")) ($#k1_pzfmisc1 :::"}"::: ) ) "holds" (Bool (Set (Var "F")) ($#r6_pboole :::"="::: ) (Set (Var "G")))))) ; theorem :: MSUALG_9:9 (Bool "for" (Set (Var "I")) "being" ($#m1_hidden :::"set"::: ) (Bool "for" (Set (Var "A")) "being" bbbadV2_RELAT_1() ($#m1_hidden :::"ManySortedSet":::) "of" (Set (Var "I")) (Bool "for" (Set (Var "B")) "being" ($#m1_hidden :::"ManySortedSet":::) "of" (Set (Var "I")) (Bool "for" (Set (Var "F")) "being" ($#m2_pboole :::"ManySortedFunction"::: ) "of" (Set (Var "A")) "," (Set ($#k1_pzfmisc1 :::"{"::: ) (Set (Var "B")) ($#k1_pzfmisc1 :::"}"::: ) ) "holds" (Bool (Set (Var "F")) "is" ($#v2_msualg_3 :::""onto""::: ) ))))) ; theorem :: MSUALG_9:10 (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")) "being" bbbadV2_RELAT_1() ($#m1_hidden :::"ManySortedSet":::) "of" (Set (Var "I")) (Bool "for" (Set (Var "F")) "being" ($#m2_pboole :::"ManySortedFunction"::: ) "of" (Set ($#k1_pzfmisc1 :::"{"::: ) (Set (Var "A")) ($#k1_pzfmisc1 :::"}"::: ) ) "," (Set (Var "B")) "holds" (Bool (Set (Var "F")) "is" ($#v1_msualg_3 :::""1-1""::: ) ))))) ; theorem :: MSUALG_9: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 "X")) "being" bbbadV2_RELAT_1() ($#m1_hidden :::"ManySortedSet":::) "of" (Set "the" ($#u1_struct_0 :::"carrier"::: ) "of" (Set (Var "S"))) "holds" (Bool (Set ($#k15_msafree :::"Reverse"::: ) (Set (Var "X"))) "is" ($#v1_msualg_3 :::""1-1""::: ) ))) ; theorem :: MSUALG_9:12 (Bool "for" (Set (Var "I")) "being" ($#m1_hidden :::"set"::: ) (Bool "for" (Set (Var "A")) "being" bbbadV2_RELAT_1() bbbadV2_FINSET_1() ($#m1_hidden :::"ManySortedSet":::) "of" (Set (Var "I")) (Bool "ex" (Set (Var "F")) "being" ($#m2_pboole :::"ManySortedFunction"::: ) "of" (Set (Set (Var "I")) ($#k7_funcop_1 :::"-->"::: ) (Set ($#k5_numbers :::"NAT"::: ) )) "," (Set (Var "A")) "st" (Bool (Set (Var "F")) "is" ($#v2_msualg_3 :::""onto""::: ) )))) ; theorem :: MSUALG_9:13 (Bool "for" (Set (Var "S")) "being" ($#~v2_struct_0 "non" ($#v2_struct_0 :::"empty"::: ) ) ($#l1_msualg_1 :::"ManySortedSign"::: ) (Bool "for" (Set (Var "A")) "being" ($#v4_msualg_1 :::"non-empty"::: ) ($#l3_msualg_1 :::"MSAlgebra"::: ) "over" (Set (Var "S")) (Bool "for" (Set (Var "f")) "," (Set (Var "g")) "being" ($#m1_subset_1 :::"Element"::: ) "of" (Set ($#k4_card_3 :::"product"::: ) (Set "the" ($#u3_msualg_1 :::"Sorts"::: ) "of" (Set (Var "A")))) "st" (Bool (Bool "(" "for" (Set (Var "i")) "being" ($#m1_hidden :::"set"::: ) "holds" (Bool (Set (Set "(" ($#k12_card_3 :::"proj"::: ) "(" (Set "the" ($#u3_msualg_1 :::"Sorts"::: ) "of" (Set (Var "A"))) "," (Set (Var "i")) ")" ")" ) ($#k1_funct_1 :::"."::: ) (Set (Var "f"))) ($#r1_hidden :::"="::: ) (Set (Set "(" ($#k12_card_3 :::"proj"::: ) "(" (Set "the" ($#u3_msualg_1 :::"Sorts"::: ) "of" (Set (Var "A"))) "," (Set (Var "i")) ")" ")" ) ($#k1_funct_1 :::"."::: ) (Set (Var "g")))) ")" )) "holds" (Bool (Set (Var "f")) ($#r8_pboole :::"="::: ) (Set (Var "g")))))) ; theorem :: MSUALG_9:14 (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 "I")) "being" ($#~v1_xboole_0 "non" ($#v1_xboole_0 :::"empty"::: ) ) ($#m1_hidden :::"set"::: ) (Bool "for" (Set (Var "s")) "being" ($#m1_subset_1 :::"Element":::) "of" (Set (Var "S")) (Bool "for" (Set (Var "A")) "being" ($#m1_pralg_2 :::"MSAlgebra-Family"::: ) "of" (Set (Var "I")) "," (Set (Var "S")) (Bool "for" (Set (Var "f")) "," (Set (Var "g")) "being" ($#m1_subset_1 :::"Element"::: ) "of" (Set ($#k4_card_3 :::"product"::: ) (Set "(" ($#k9_pralg_2 :::"Carrier"::: ) "(" (Set (Var "A")) "," (Set (Var "s")) ")" ")" )) "st" (Bool (Bool "(" "for" (Set (Var "a")) "being" ($#m1_subset_1 :::"Element"::: ) "of" (Set (Var "I")) "holds" (Bool (Set (Set "(" ($#k12_card_3 :::"proj"::: ) "(" (Set "(" ($#k9_pralg_2 :::"Carrier"::: ) "(" (Set (Var "A")) "," (Set (Var "s")) ")" ")" ) "," (Set (Var "a")) ")" ")" ) ($#k1_funct_1 :::"."::: ) (Set (Var "f"))) ($#r1_hidden :::"="::: ) (Set (Set "(" ($#k12_card_3 :::"proj"::: ) "(" (Set "(" ($#k9_pralg_2 :::"Carrier"::: ) "(" (Set (Var "A")) "," (Set (Var "s")) ")" ")" ) "," (Set (Var "a")) ")" ")" ) ($#k1_funct_1 :::"."::: ) (Set (Var "g")))) ")" )) "holds" (Bool (Set (Var "f")) ($#r8_pboole :::"="::: ) (Set (Var "g")))))))) ; theorem :: MSUALG_9:15 (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 "A")) "," (Set (Var "B")) "being" ($#v4_msualg_1 :::"non-empty"::: ) ($#l3_msualg_1 :::"MSAlgebra"::: ) "over" (Set (Var "S")) (Bool "for" (Set (Var "C")) "being" ($#v4_msualg_1 :::"non-empty"::: ) ($#m1_msualg_2 :::"MSSubAlgebra"::: ) "of" (Set (Var "A")) (Bool "for" (Set (Var "h1")) "being" ($#m2_pboole :::"ManySortedFunction":::) "of" (Set (Var "B")) "," (Set (Var "C")) "st" (Bool (Bool (Set (Var "h1")) ($#r1_msualg_3 :::"is_homomorphism"::: ) (Set (Var "B")) "," (Set (Var "C")))) "holds" (Bool "for" (Set (Var "h2")) "being" ($#m2_pboole :::"ManySortedFunction":::) "of" (Set (Var "B")) "," (Set (Var "A")) "st" (Bool (Bool (Set (Var "h1")) ($#r8_pboole :::"="::: ) (Set (Var "h2")))) "holds" (Bool (Set (Var "h2")) ($#r1_msualg_3 :::"is_homomorphism"::: ) (Set (Var "B")) "," (Set (Var "A")))))))) ; theorem :: MSUALG_9:16 (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 "A")) "," (Set (Var "B")) "being" ($#v4_msualg_1 :::"non-empty"::: ) ($#l3_msualg_1 :::"MSAlgebra"::: ) "over" (Set (Var "S")) (Bool "for" (Set (Var "F")) "being" ($#m2_pboole :::"ManySortedFunction":::) "of" (Set (Var "A")) "," (Set (Var "B")) "st" (Bool (Bool (Set (Var "F")) ($#r3_msualg_3 :::"is_monomorphism"::: ) (Set (Var "A")) "," (Set (Var "B")))) "holds" (Bool (Set (Var "A")) "," (Set ($#k6_msualg_3 :::"Image"::: ) (Set (Var "F"))) ($#r6_msualg_3 :::"are_isomorphic"::: ) )))) ; theorem :: MSUALG_9:17 (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 "A")) "," (Set (Var "B")) "being" ($#v4_msualg_1 :::"non-empty"::: ) ($#l3_msualg_1 :::"MSAlgebra"::: ) "over" (Set (Var "S")) (Bool "for" (Set (Var "F")) "being" ($#m2_pboole :::"ManySortedFunction":::) "of" (Set (Var "A")) "," (Set (Var "B")) "st" (Bool (Bool (Set (Var "F")) "is" ($#v2_msualg_3 :::""onto""::: ) )) "holds" (Bool "for" (Set (Var "o")) "being" ($#m1_subset_1 :::"OperSymbol":::) "of" (Set (Var "S")) (Bool "for" (Set (Var "x")) "being" ($#m1_subset_1 :::"Element"::: ) "of" (Set ($#k3_msualg_1 :::"Args"::: ) "(" (Set (Var "o")) "," (Set (Var "B")) ")" ) (Bool "ex" (Set (Var "y")) "being" ($#m1_subset_1 :::"Element"::: ) "of" (Set ($#k3_msualg_1 :::"Args"::: ) "(" (Set (Var "o")) "," (Set (Var "A")) ")" ) "st" (Bool (Set (Set (Var "F")) ($#k5_msualg_3 :::"#"::: ) (Set (Var "y"))) ($#r1_hidden :::"="::: ) (Set (Var "x"))))))))) ; theorem :: MSUALG_9:18 (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 "A")) "being" ($#v4_msualg_1 :::"non-empty"::: ) ($#l3_msualg_1 :::"MSAlgebra"::: ) "over" (Set (Var "S")) (Bool "for" (Set (Var "o")) "being" ($#m1_subset_1 :::"OperSymbol":::) "of" (Set (Var "S")) (Bool "for" (Set (Var "x")) "being" ($#m1_subset_1 :::"Element"::: ) "of" (Set ($#k3_msualg_1 :::"Args"::: ) "(" (Set (Var "o")) "," (Set (Var "A")) ")" ) "holds" (Bool (Set (Set "(" ($#k5_msualg_1 :::"Den"::: ) "(" (Set (Var "o")) "," (Set (Var "A")) ")" ")" ) ($#k3_funct_2 :::"."::: ) (Set (Var "x"))) ($#r2_hidden :::"in"::: ) (Set (Set "the" ($#u3_msualg_1 :::"Sorts"::: ) "of" (Set (Var "A"))) ($#k1_funct_1 :::"."::: ) (Set "(" ($#k2_msualg_1 :::"the_result_sort_of"::: ) (Set (Var "o")) ")" ))))))) ; theorem :: MSUALG_9:19 (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 "A")) "," (Set (Var "B")) "," (Set (Var "C")) "being" ($#v4_msualg_1 :::"non-empty"::: ) ($#l3_msualg_1 :::"MSAlgebra"::: ) "over" (Set (Var "S")) (Bool "for" (Set (Var "F1")) "being" ($#m2_pboole :::"ManySortedFunction":::) "of" (Set (Var "A")) "," (Set (Var "B")) (Bool "for" (Set (Var "F2")) "being" ($#m2_pboole :::"ManySortedFunction":::) "of" (Set (Var "A")) "," (Set (Var "C")) "st" (Bool (Bool (Set (Var "F1")) ($#r2_msualg_3 :::"is_epimorphism"::: ) (Set (Var "A")) "," (Set (Var "B"))) & (Bool (Set (Var "F2")) ($#r1_msualg_3 :::"is_homomorphism"::: ) (Set (Var "A")) "," (Set (Var "C")))) "holds" (Bool "for" (Set (Var "G")) "being" ($#m2_pboole :::"ManySortedFunction":::) "of" (Set (Var "B")) "," (Set (Var "C")) "st" (Bool (Bool (Set (Set (Var "G")) ($#k3_msualg_3 :::"**"::: ) (Set (Var "F1"))) ($#r8_pboole :::"="::: ) (Set (Var "F2")))) "holds" (Bool (Set (Var "G")) ($#r1_msualg_3 :::"is_homomorphism"::: ) (Set (Var "B")) "," (Set (Var "C")))))))) ; definitionlet "I" be ($#m1_hidden :::"set"::: ) ; let "A" be ($#m1_hidden :::"ManySortedSet":::) "of" (Set (Const "I")); let "B", "C" be bbbadV2_RELAT_1() ($#m1_hidden :::"ManySortedSet":::) "of" (Set (Const "I")); let "F" be ($#m2_pboole :::"ManySortedFunction"::: ) "of" (Set (Const "A")) "," (Set ($#k6_pboole :::"[|"::: ) (Set (Const "B")) "," (Set (Const "C")) ($#k6_pboole :::"|]"::: ) ); func :::"Mpr1"::: "F" -> ($#m2_pboole :::"ManySortedFunction"::: ) "of" "A" "," "B" means :: MSUALG_9:def 1 (Bool "for" (Set (Var "i")) "being" ($#m1_hidden :::"set"::: ) "st" (Bool (Bool (Set (Var "i")) ($#r2_hidden :::"in"::: ) "I")) "holds" (Bool (Set it ($#k1_funct_1 :::"."::: ) (Set (Var "i"))) ($#r1_hidden :::"="::: ) (Set ($#k11_mcart_1 :::"pr1"::: ) (Set "(" "F" ($#k1_funct_1 :::"."::: ) (Set (Var "i")) ")" )))); func :::"Mpr2"::: "F" -> ($#m2_pboole :::"ManySortedFunction"::: ) "of" "A" "," "C" means :: MSUALG_9:def 2 (Bool "for" (Set (Var "i")) "being" ($#m1_hidden :::"set"::: ) "st" (Bool (Bool (Set (Var "i")) ($#r2_hidden :::"in"::: ) "I")) "holds" (Bool (Set it ($#k1_funct_1 :::"."::: ) (Set (Var "i"))) ($#r1_hidden :::"="::: ) (Set ($#k12_mcart_1 :::"pr2"::: ) (Set "(" "F" ($#k1_funct_1 :::"."::: ) (Set (Var "i")) ")" )))); end; :: deftheorem defines :::"Mpr1"::: MSUALG_9:def 1 : (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 ($#k6_pboole :::"[|"::: ) (Set (Var "B")) "," (Set (Var "C")) ($#k6_pboole :::"|]"::: ) ) (Bool "for" (Set (Var "b6")) "being" ($#m2_pboole :::"ManySortedFunction"::: ) "of" (Set (Var "A")) "," (Set (Var "B")) "holds" (Bool "(" (Bool (Set (Var "b6")) ($#r1_hidden :::"="::: ) (Set ($#k1_msualg_9 :::"Mpr1"::: ) (Set (Var "F")))) "iff" (Bool "for" (Set (Var "i")) "being" ($#m1_hidden :::"set"::: ) "st" (Bool (Bool (Set (Var "i")) ($#r2_hidden :::"in"::: ) (Set (Var "I")))) "holds" (Bool (Set (Set (Var "b6")) ($#k1_funct_1 :::"."::: ) (Set (Var "i"))) ($#r1_hidden :::"="::: ) (Set ($#k11_mcart_1 :::"pr1"::: ) (Set "(" (Set (Var "F")) ($#k1_funct_1 :::"."::: ) (Set (Var "i")) ")" )))) ")" )))))); :: deftheorem defines :::"Mpr2"::: MSUALG_9:def 2 : (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 ($#k6_pboole :::"[|"::: ) (Set (Var "B")) "," (Set (Var "C")) ($#k6_pboole :::"|]"::: ) ) (Bool "for" (Set (Var "b6")) "being" ($#m2_pboole :::"ManySortedFunction"::: ) "of" (Set (Var "A")) "," (Set (Var "C")) "holds" (Bool "(" (Bool (Set (Var "b6")) ($#r1_hidden :::"="::: ) (Set ($#k2_msualg_9 :::"Mpr2"::: ) (Set (Var "F")))) "iff" (Bool "for" (Set (Var "i")) "being" ($#m1_hidden :::"set"::: ) "st" (Bool (Bool (Set (Var "i")) ($#r2_hidden :::"in"::: ) (Set (Var "I")))) "holds" (Bool (Set (Set (Var "b6")) ($#k1_funct_1 :::"."::: ) (Set (Var "i"))) ($#r1_hidden :::"="::: ) (Set ($#k12_mcart_1 :::"pr2"::: ) (Set "(" (Set (Var "F")) ($#k1_funct_1 :::"."::: ) (Set (Var "i")) ")" )))) ")" )))))); theorem :: MSUALG_9:20 (Bool "for" (Set (Var "I")) "," (Set (Var "a")) "being" ($#m1_hidden :::"set"::: ) (Bool "for" (Set (Var "A")) "being" ($#m1_hidden :::"ManySortedSet":::) "of" (Set (Var "I")) (Bool "for" (Set (Var "F")) "being" ($#m2_pboole :::"ManySortedFunction"::: ) "of" (Set (Var "A")) "," (Set ($#k6_pboole :::"[|"::: ) (Set "(" (Set (Var "I")) ($#k7_funcop_1 :::"-->"::: ) (Set ($#k1_tarski :::"{"::: ) (Set (Var "a")) ($#k1_tarski :::"}"::: ) ) ")" ) "," (Set "(" (Set (Var "I")) ($#k7_funcop_1 :::"-->"::: ) (Set ($#k1_tarski :::"{"::: ) (Set (Var "a")) ($#k1_tarski :::"}"::: ) ) ")" ) ($#k6_pboole :::"|]"::: ) ) "holds" (Bool (Set ($#k1_msualg_9 :::"Mpr1"::: ) (Set (Var "F"))) ($#r6_pboole :::"="::: ) (Set ($#k2_msualg_9 :::"Mpr2"::: ) (Set (Var "F"))))))) ; theorem :: MSUALG_9:21 (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 ($#k6_pboole :::"[|"::: ) (Set (Var "B")) "," (Set (Var "C")) ($#k6_pboole :::"|]"::: ) ) "st" (Bool (Bool (Set (Var "F")) "is" ($#v2_msualg_3 :::""onto""::: ) )) "holds" (Bool (Set ($#k1_msualg_9 :::"Mpr1"::: ) (Set (Var "F"))) "is" ($#v2_msualg_3 :::""onto""::: ) ))))) ; theorem :: MSUALG_9:22 (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 ($#k6_pboole :::"[|"::: ) (Set (Var "B")) "," (Set (Var "C")) ($#k6_pboole :::"|]"::: ) ) "st" (Bool (Bool (Set (Var "F")) "is" ($#v2_msualg_3 :::""onto""::: ) )) "holds" (Bool (Set ($#k2_msualg_9 :::"Mpr2"::: ) (Set (Var "F"))) "is" ($#v2_msualg_3 :::""onto""::: ) ))))) ; theorem :: MSUALG_9:23 (Bool "for" (Set (Var "I")) "being" ($#m1_hidden :::"set"::: ) (Bool "for" (Set (Var "A")) "," (Set (Var "M")) "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 ($#k6_pboole :::"[|"::: ) (Set (Var "B")) "," (Set (Var "C")) ($#k6_pboole :::"|]"::: ) ) "st" (Bool (Bool (Set (Var "M")) ($#r1_pboole :::"in"::: ) (Set ($#k2_funct_6 :::"doms"::: ) (Set (Var "F"))))) "holds" (Bool "for" (Set (Var "i")) "being" ($#m1_hidden :::"set"::: ) "st" (Bool (Bool (Set (Var "i")) ($#r2_hidden :::"in"::: ) (Set (Var "I")))) "holds" (Bool (Set (Set "(" (Set (Var "F")) ($#k16_pralg_1 :::".."::: ) (Set (Var "M")) ")" ) ($#k1_funct_1 :::"."::: ) (Set (Var "i"))) ($#r1_hidden :::"="::: ) (Set ($#k4_tarski :::"["::: ) (Set "(" (Set "(" (Set "(" ($#k1_msualg_9 :::"Mpr1"::: ) (Set (Var "F")) ")" ) ($#k16_pralg_1 :::".."::: ) (Set (Var "M")) ")" ) ($#k1_funct_1 :::"."::: ) (Set (Var "i")) ")" ) "," (Set "(" (Set "(" (Set "(" ($#k2_msualg_9 :::"Mpr2"::: ) (Set (Var "F")) ")" ) ($#k16_pralg_1 :::".."::: ) (Set (Var "M")) ")" ) ($#k1_funct_1 :::"."::: ) (Set (Var "i")) ")" ) ($#k4_tarski :::"]"::: ) ))))))) ; begin registrationlet "S" be ($#~v2_struct_0 "non" ($#v2_struct_0 :::"empty"::: ) ) ($#l1_msualg_1 :::"ManySortedSign"::: ) ; cluster (Set "the" ($#u3_msualg_1 :::"Sorts"::: ) "of" (Set "(" ($#k7_msafree2 :::"Trivial_Algebra"::: ) "S" ")" )) -> bbbadV2_RELAT_1() bbbadV2_FINSET_1() ; end; registrationlet "S" be ($#~v2_struct_0 "non" ($#v2_struct_0 :::"empty"::: ) ) ($#l1_msualg_1 :::"ManySortedSign"::: ) ; cluster (Set ($#k7_msafree2 :::"Trivial_Algebra"::: ) "S") -> ($#v4_msualg_1 :::"non-empty"::: ) ($#v4_msafree2 :::"finite-yielding"::: ) ; end; theorem :: MSUALG_9: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 "A")) "being" ($#v4_msualg_1 :::"non-empty"::: ) ($#l3_msualg_1 :::"MSAlgebra"::: ) "over" (Set (Var "S")) (Bool "for" (Set (Var "F")) "being" ($#m2_pboole :::"ManySortedFunction":::) "of" (Set (Var "A")) "," (Set "(" ($#k7_msafree2 :::"Trivial_Algebra"::: ) (Set (Var "S")) ")" ) (Bool "for" (Set (Var "o")) "being" ($#m1_subset_1 :::"OperSymbol":::) "of" (Set (Var "S")) (Bool "for" (Set (Var "x")) "being" ($#m1_subset_1 :::"Element"::: ) "of" (Set ($#k3_msualg_1 :::"Args"::: ) "(" (Set (Var "o")) "," (Set (Var "A")) ")" ) "holds" (Bool "(" (Bool (Set (Set "(" (Set (Var "F")) ($#k1_msualg_3 :::"."::: ) (Set "(" ($#k2_msualg_1 :::"the_result_sort_of"::: ) (Set (Var "o")) ")" ) ")" ) ($#k1_funct_1 :::"."::: ) (Set "(" (Set "(" ($#k5_msualg_1 :::"Den"::: ) "(" (Set (Var "o")) "," (Set (Var "A")) ")" ")" ) ($#k3_funct_2 :::"."::: ) (Set (Var "x")) ")" )) ($#r1_hidden :::"="::: ) (Set ($#k6_numbers :::"0"::: ) )) & (Bool (Set (Set "(" ($#k5_msualg_1 :::"Den"::: ) "(" (Set (Var "o")) "," (Set "(" ($#k7_msafree2 :::"Trivial_Algebra"::: ) (Set (Var "S")) ")" ) ")" ")" ) ($#k3_funct_2 :::"."::: ) (Set "(" (Set (Var "F")) ($#k5_msualg_3 :::"#"::: ) (Set (Var "x")) ")" )) ($#r1_hidden :::"="::: ) (Set ($#k6_numbers :::"0"::: ) )) ")" )))))) ; theorem :: MSUALG_9: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 "A")) "being" ($#v4_msualg_1 :::"non-empty"::: ) ($#l3_msualg_1 :::"MSAlgebra"::: ) "over" (Set (Var "S")) (Bool "for" (Set (Var "F")) "being" ($#m2_pboole :::"ManySortedFunction":::) "of" (Set (Var "A")) "," (Set "(" ($#k7_msafree2 :::"Trivial_Algebra"::: ) (Set (Var "S")) ")" ) "holds" (Bool (Set (Var "F")) ($#r2_msualg_3 :::"is_epimorphism"::: ) (Set (Var "A")) "," (Set ($#k7_msafree2 :::"Trivial_Algebra"::: ) (Set (Var "S"))))))) ; theorem :: MSUALG_9: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 "A")) "being" ($#l3_msualg_1 :::"MSAlgebra"::: ) "over" (Set (Var "S")) "st" (Bool (Bool "ex" (Set (Var "X")) "being" ($#m1_hidden :::"ManySortedSet":::) "of" (Set "the" ($#u1_struct_0 :::"carrier"::: ) "of" (Set (Var "S"))) "st" (Bool (Set "the" ($#u3_msualg_1 :::"Sorts"::: ) "of" (Set (Var "A"))) ($#r8_pboole :::"="::: ) (Set ($#k1_pzfmisc1 :::"{"::: ) (Set (Var "X")) ($#k1_pzfmisc1 :::"}"::: ) )))) "holds" (Bool (Set (Var "A")) "," (Set ($#k7_msafree2 :::"Trivial_Algebra"::: ) (Set (Var "S"))) ($#r6_msualg_3 :::"are_isomorphic"::: ) ))) ; begin theorem :: MSUALG_9:27 (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 "A")) "being" ($#v4_msualg_1 :::"non-empty"::: ) ($#l3_msualg_1 :::"MSAlgebra"::: ) "over" (Set (Var "S")) (Bool "for" (Set (Var "C")) "being" ($#m1_msualg_4 :::"MSCongruence":::) "of" (Set (Var "A")) "holds" (Bool (Set (Var "C")) "is" ($#m3_pboole :::"ManySortedSubset"::: ) "of" (Set ($#k6_pboole :::"[|"::: ) (Set "the" ($#u3_msualg_1 :::"Sorts"::: ) "of" (Set (Var "A"))) "," (Set "the" ($#u3_msualg_1 :::"Sorts"::: ) "of" (Set (Var "A"))) ($#k6_pboole :::"|]"::: ) ))))) ; theorem :: MSUALG_9: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 "A")) "being" ($#v4_msualg_1 :::"non-empty"::: ) ($#l3_msualg_1 :::"MSAlgebra"::: ) "over" (Set (Var "S")) (Bool "for" (Set (Var "R")) "being" ($#m1_subset_1 :::"Subset":::) "of" (Set "(" ($#k6_msualg_5 :::"CongrLatt"::: ) (Set (Var "A")) ")" ) (Bool "for" (Set (Var "F")) "being" ($#m1_subset_1 :::"SubsetFamily":::) "of" (Set ($#k6_pboole :::"[|"::: ) (Set "the" ($#u3_msualg_1 :::"Sorts"::: ) "of" (Set (Var "A"))) "," (Set "the" ($#u3_msualg_1 :::"Sorts"::: ) "of" (Set (Var "A"))) ($#k6_pboole :::"|]"::: ) ) "st" (Bool (Bool (Set (Var "R")) ($#r1_hidden :::"="::: ) (Set (Var "F")))) "holds" (Bool (Set ($#k4_mssubfam :::"meet"::: ) (Set ($#k5_closure2 :::"|:"::: ) (Set (Var "F")) ($#k5_closure2 :::":|"::: ) )) "is" ($#m1_msualg_4 :::"MSCongruence":::) "of" (Set (Var "A"))))))) ; theorem :: MSUALG_9: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 "A")) "being" ($#v4_msualg_1 :::"non-empty"::: ) ($#l3_msualg_1 :::"MSAlgebra"::: ) "over" (Set (Var "S")) (Bool "for" (Set (Var "C")) "being" ($#m1_msualg_4 :::"MSCongruence":::) "of" (Set (Var "A")) "st" (Bool (Bool (Set (Var "C")) ($#r8_pboole :::"="::: ) (Set ($#k6_pboole :::"[|"::: ) (Set "the" ($#u3_msualg_1 :::"Sorts"::: ) "of" (Set (Var "A"))) "," (Set "the" ($#u3_msualg_1 :::"Sorts"::: ) "of" (Set (Var "A"))) ($#k6_pboole :::"|]"::: ) ))) "holds" (Bool (Set "the" ($#u3_msualg_1 :::"Sorts"::: ) "of" (Set "(" ($#k13_msualg_4 :::"QuotMSAlg"::: ) "(" (Set (Var "A")) "," (Set (Var "C")) ")" ")" )) ($#r8_pboole :::"="::: ) (Set ($#k1_pzfmisc1 :::"{"::: ) (Set "the" ($#u3_msualg_1 :::"Sorts"::: ) "of" (Set (Var "A"))) ($#k1_pzfmisc1 :::"}"::: ) ))))) ; theorem :: MSUALG_9: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 "A")) "," (Set (Var "B")) "being" ($#v4_msualg_1 :::"non-empty"::: ) ($#l3_msualg_1 :::"MSAlgebra"::: ) "over" (Set (Var "S")) (Bool "for" (Set (Var "F")) "being" ($#m2_pboole :::"ManySortedFunction":::) "of" (Set (Var "A")) "," (Set (Var "B")) "st" (Bool (Bool (Set (Var "F")) ($#r1_msualg_3 :::"is_homomorphism"::: ) (Set (Var "A")) "," (Set (Var "B")))) "holds" (Bool (Set (Set "(" ($#k19_msualg_4 :::"MSHomQuot"::: ) (Set (Var "F")) ")" ) ($#k3_msualg_3 :::"**"::: ) (Set "(" ($#k15_msualg_4 :::"MSNat_Hom"::: ) "(" (Set (Var "A")) "," (Set "(" ($#k17_msualg_4 :::"MSCng"::: ) (Set (Var "F")) ")" ) ")" ")" )) ($#r8_pboole :::"="::: ) (Set (Var "F")))))) ; theorem :: MSUALG_9:31 (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 "A")) "being" ($#v4_msualg_1 :::"non-empty"::: ) ($#l3_msualg_1 :::"MSAlgebra"::: ) "over" (Set (Var "S")) (Bool "for" (Set (Var "C")) "being" ($#m1_msualg_4 :::"MSCongruence":::) "of" (Set (Var "A")) (Bool "for" (Set (Var "s")) "being" ($#m1_subset_1 :::"SortSymbol":::) "of" (Set (Var "S")) (Bool "for" (Set (Var "a")) "being" ($#m1_subset_1 :::"Element"::: ) "of" (Set (Set "the" ($#u3_msualg_1 :::"Sorts"::: ) "of" (Set "(" ($#k13_msualg_4 :::"QuotMSAlg"::: ) "(" (Set (Var "A")) "," (Set (Var "C")) ")" ")" )) ($#k1_funct_1 :::"."::: ) (Set (Var "s"))) (Bool "ex" (Set (Var "x")) "being" ($#m1_subset_1 :::"Element"::: ) "of" (Set (Set "the" ($#u3_msualg_1 :::"Sorts"::: ) "of" (Set (Var "A"))) ($#k1_funct_1 :::"."::: ) (Set (Var "s"))) "st" (Bool (Set (Var "a")) ($#r1_hidden :::"="::: ) (Set ($#k3_msualg_4 :::"Class"::: ) "(" (Set (Var "C")) "," (Set (Var "x")) ")" )))))))) ; theorem :: MSUALG_9:32 (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 "A")) "being" ($#l3_msualg_1 :::"MSAlgebra"::: ) "over" (Set (Var "S")) (Bool "for" (Set (Var "C1")) "," (Set (Var "C2")) "being" ($#v2_msualg_4 :::"MSEquivalence-like"::: ) ($#m1_msualg_4 :::"ManySortedRelation":::) "of" (Set (Var "A")) "st" (Bool (Bool (Set (Var "C1")) ($#r2_pboole :::"c="::: ) (Set (Var "C2")))) "holds" (Bool "for" (Set (Var "i")) "being" ($#m1_subset_1 :::"Element":::) "of" (Set (Var "S")) (Bool "for" (Set (Var "x")) "," (Set (Var "y")) "being" ($#m1_subset_1 :::"Element"::: ) "of" (Set (Set "the" ($#u3_msualg_1 :::"Sorts"::: ) "of" (Set (Var "A"))) ($#k1_funct_1 :::"."::: ) (Set (Var "i"))) "st" (Bool (Bool (Set ($#k4_tarski :::"["::: ) (Set (Var "x")) "," (Set (Var "y")) ($#k4_tarski :::"]"::: ) ) ($#r2_hidden :::"in"::: ) (Set (Set (Var "C1")) ($#k2_msualg_4 :::"."::: ) (Set (Var "i"))))) "holds" (Bool "(" (Bool (Set ($#k3_msualg_4 :::"Class"::: ) "(" (Set (Var "C1")) "," (Set (Var "x")) ")" ) ($#r1_tarski :::"c="::: ) (Set ($#k3_msualg_4 :::"Class"::: ) "(" (Set (Var "C2")) "," (Set (Var "y")) ")" )) & "(" (Bool (Bool (Set (Var "A")) "is" ($#v4_msualg_1 :::"non-empty"::: ) )) "implies" (Bool (Set ($#k3_msualg_4 :::"Class"::: ) "(" (Set (Var "C1")) "," (Set (Var "y")) ")" ) ($#r1_tarski :::"c="::: ) (Set ($#k3_msualg_4 :::"Class"::: ) "(" (Set (Var "C2")) "," (Set (Var "x")) ")" )) ")" ")" )))))) ; theorem :: MSUALG_9:33 (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 "A")) "being" ($#v4_msualg_1 :::"non-empty"::: ) ($#l3_msualg_1 :::"MSAlgebra"::: ) "over" (Set (Var "S")) (Bool "for" (Set (Var "C")) "being" ($#m1_msualg_4 :::"MSCongruence":::) "of" (Set (Var "A")) (Bool "for" (Set (Var "s")) "being" ($#m1_subset_1 :::"SortSymbol":::) "of" (Set (Var "S")) (Bool "for" (Set (Var "x")) "," (Set (Var "y")) "being" ($#m1_subset_1 :::"Element"::: ) "of" (Set (Set "the" ($#u3_msualg_1 :::"Sorts"::: ) "of" (Set (Var "A"))) ($#k1_funct_1 :::"."::: ) (Set (Var "s"))) "holds" (Bool "(" (Bool (Set (Set "(" (Set "(" ($#k15_msualg_4 :::"MSNat_Hom"::: ) "(" (Set (Var "A")) "," (Set (Var "C")) ")" ")" ) ($#k1_msualg_3 :::"."::: ) (Set (Var "s")) ")" ) ($#k3_funct_2 :::"."::: ) (Set (Var "x"))) ($#r1_hidden :::"="::: ) (Set (Set "(" (Set "(" ($#k15_msualg_4 :::"MSNat_Hom"::: ) "(" (Set (Var "A")) "," (Set (Var "C")) ")" ")" ) ($#k1_msualg_3 :::"."::: ) (Set (Var "s")) ")" ) ($#k3_funct_2 :::"."::: ) (Set (Var "y")))) "iff" (Bool (Set ($#k4_tarski :::"["::: ) (Set (Var "x")) "," (Set (Var "y")) ($#k4_tarski :::"]"::: ) ) ($#r2_hidden :::"in"::: ) (Set (Set (Var "C")) ($#k2_msualg_4 :::"."::: ) (Set (Var "s")))) ")" )))))) ; theorem :: MSUALG_9:34 (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 "A")) "being" ($#v4_msualg_1 :::"non-empty"::: ) ($#l3_msualg_1 :::"MSAlgebra"::: ) "over" (Set (Var "S")) (Bool "for" (Set (Var "C1")) "," (Set (Var "C2")) "being" ($#m1_msualg_4 :::"MSCongruence":::) "of" (Set (Var "A")) (Bool "for" (Set (Var "G")) "being" ($#m2_pboole :::"ManySortedFunction":::) "of" (Set "(" ($#k13_msualg_4 :::"QuotMSAlg"::: ) "(" (Set (Var "A")) "," (Set (Var "C1")) ")" ")" ) "," (Set "(" ($#k13_msualg_4 :::"QuotMSAlg"::: ) "(" (Set (Var "A")) "," (Set (Var "C2")) ")" ")" ) "st" (Bool (Bool "(" "for" (Set (Var "i")) "being" ($#m1_subset_1 :::"Element":::) "of" (Set (Var "S")) (Bool "for" (Set (Var "x")) "being" ($#m1_subset_1 :::"Element"::: ) "of" (Set (Set "the" ($#u3_msualg_1 :::"Sorts"::: ) "of" (Set "(" ($#k13_msualg_4 :::"QuotMSAlg"::: ) "(" (Set (Var "A")) "," (Set (Var "C1")) ")" ")" )) ($#k1_funct_1 :::"."::: ) (Set (Var "i"))) (Bool "for" (Set (Var "xx")) "being" ($#m1_subset_1 :::"Element"::: ) "of" (Set (Set "the" ($#u3_msualg_1 :::"Sorts"::: ) "of" (Set (Var "A"))) ($#k1_funct_1 :::"."::: ) (Set (Var "i"))) "st" (Bool (Bool (Set (Var "x")) ($#r1_hidden :::"="::: ) (Set ($#k3_msualg_4 :::"Class"::: ) "(" (Set (Var "C1")) "," (Set (Var "xx")) ")" ))) "holds" (Bool (Set (Set "(" (Set (Var "G")) ($#k1_msualg_3 :::"."::: ) (Set (Var "i")) ")" ) ($#k3_funct_2 :::"."::: ) (Set (Var "x"))) ($#r1_hidden :::"="::: ) (Set ($#k3_msualg_4 :::"Class"::: ) "(" (Set (Var "C2")) "," (Set (Var "xx")) ")" )))) ")" )) "holds" (Bool (Set (Set (Var "G")) ($#k3_msualg_3 :::"**"::: ) (Set "(" ($#k15_msualg_4 :::"MSNat_Hom"::: ) "(" (Set (Var "A")) "," (Set (Var "C1")) ")" ")" )) ($#r8_pboole :::"="::: ) (Set ($#k15_msualg_4 :::"MSNat_Hom"::: ) "(" (Set (Var "A")) "," (Set (Var "C2")) ")" )))))) ; theorem :: MSUALG_9:35 (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 "A")) "being" ($#v4_msualg_1 :::"non-empty"::: ) ($#l3_msualg_1 :::"MSAlgebra"::: ) "over" (Set (Var "S")) (Bool "for" (Set (Var "C1")) "," (Set (Var "C2")) "being" ($#m1_msualg_4 :::"MSCongruence":::) "of" (Set (Var "A")) (Bool "for" (Set (Var "G")) "being" ($#m2_pboole :::"ManySortedFunction":::) "of" (Set "(" ($#k13_msualg_4 :::"QuotMSAlg"::: ) "(" (Set (Var "A")) "," (Set (Var "C1")) ")" ")" ) "," (Set "(" ($#k13_msualg_4 :::"QuotMSAlg"::: ) "(" (Set (Var "A")) "," (Set (Var "C2")) ")" ")" ) "st" (Bool (Bool "(" "for" (Set (Var "i")) "being" ($#m1_subset_1 :::"Element":::) "of" (Set (Var "S")) (Bool "for" (Set (Var "x")) "being" ($#m1_subset_1 :::"Element"::: ) "of" (Set (Set "the" ($#u3_msualg_1 :::"Sorts"::: ) "of" (Set "(" ($#k13_msualg_4 :::"QuotMSAlg"::: ) "(" (Set (Var "A")) "," (Set (Var "C1")) ")" ")" )) ($#k1_funct_1 :::"."::: ) (Set (Var "i"))) (Bool "for" (Set (Var "xx")) "being" ($#m1_subset_1 :::"Element"::: ) "of" (Set (Set "the" ($#u3_msualg_1 :::"Sorts"::: ) "of" (Set (Var "A"))) ($#k1_funct_1 :::"."::: ) (Set (Var "i"))) "st" (Bool (Bool (Set (Var "x")) ($#r1_hidden :::"="::: ) (Set ($#k3_msualg_4 :::"Class"::: ) "(" (Set (Var "C1")) "," (Set (Var "xx")) ")" ))) "holds" (Bool (Set (Set "(" (Set (Var "G")) ($#k1_msualg_3 :::"."::: ) (Set (Var "i")) ")" ) ($#k3_funct_2 :::"."::: ) (Set (Var "x"))) ($#r1_hidden :::"="::: ) (Set ($#k3_msualg_4 :::"Class"::: ) "(" (Set (Var "C2")) "," (Set (Var "xx")) ")" )))) ")" )) "holds" (Bool (Set (Var "G")) ($#r2_msualg_3 :::"is_epimorphism"::: ) (Set ($#k13_msualg_4 :::"QuotMSAlg"::: ) "(" (Set (Var "A")) "," (Set (Var "C1")) ")" ) "," (Set ($#k13_msualg_4 :::"QuotMSAlg"::: ) "(" (Set (Var "A")) "," (Set (Var "C2")) ")" )))))) ; theorem :: MSUALG_9:36 (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 "A")) "," (Set (Var "B")) "being" ($#v4_msualg_1 :::"non-empty"::: ) ($#l3_msualg_1 :::"MSAlgebra"::: ) "over" (Set (Var "S")) (Bool "for" (Set (Var "F")) "being" ($#m2_pboole :::"ManySortedFunction":::) "of" (Set (Var "A")) "," (Set (Var "B")) "st" (Bool (Bool (Set (Var "F")) ($#r1_msualg_3 :::"is_homomorphism"::: ) (Set (Var "A")) "," (Set (Var "B")))) "holds" (Bool "for" (Set (Var "C1")) "being" ($#m1_msualg_4 :::"MSCongruence":::) "of" (Set (Var "A")) "st" (Bool (Bool (Set (Var "C1")) ($#r2_pboole :::"c="::: ) (Set ($#k17_msualg_4 :::"MSCng"::: ) (Set (Var "F"))))) "holds" (Bool "ex" (Set (Var "H")) "being" ($#m2_pboole :::"ManySortedFunction":::) "of" (Set "(" ($#k13_msualg_4 :::"QuotMSAlg"::: ) "(" (Set (Var "A")) "," (Set (Var "C1")) ")" ")" ) "," (Set (Var "B")) "st" (Bool "(" (Bool (Set (Var "H")) ($#r1_msualg_3 :::"is_homomorphism"::: ) (Set ($#k13_msualg_4 :::"QuotMSAlg"::: ) "(" (Set (Var "A")) "," (Set (Var "C1")) ")" ) "," (Set (Var "B"))) & (Bool (Set (Var "F")) ($#r8_pboole :::"="::: ) (Set (Set (Var "H")) ($#k3_msualg_3 :::"**"::: ) (Set "(" ($#k15_msualg_4 :::"MSNat_Hom"::: ) "(" (Set (Var "A")) "," (Set (Var "C1")) ")" ")" ))) ")" )))))) ;