:: PRALG_3 semantic presentation begin registrationlet "I" be ($#m1_hidden :::"set"::: ) ; let "S" be ($#~v2_struct_0 "non" ($#v2_struct_0 :::"empty"::: ) ) ($#~v11_struct_0 "non" ($#v11_struct_0 :::"void"::: ) ) ($#l1_msualg_1 :::"ManySortedSign"::: ) ; let "AF" be ($#m1_pralg_2 :::"MSAlgebra-Family"::: ) "of" (Set (Const "I")) "," (Set (Const "S")); cluster (Set ($#k14_pralg_2 :::"product"::: ) "AF") -> ($#v4_msualg_1 :::"non-empty"::: ) ; end; registrationlet "X" be ($#v1_setfam_1 :::"with_non-empty_elements"::: ) ($#m1_hidden :::"set"::: ) ; cluster (Set ($#k4_relat_1 :::"id"::: ) "X") -> ($#v2_relat_1 :::"non-empty"::: ) ; end; theorem :: PRALG_3:1 (Bool "for" (Set (Var "f")) "," (Set (Var "F")) "being" ($#m1_hidden :::"Function":::) (Bool "for" (Set (Var "A")) "being" ($#m1_hidden :::"set"::: ) "st" (Bool (Bool (Set (Var "f")) ($#r2_hidden :::"in"::: ) (Set ($#k4_card_3 :::"product"::: ) (Set (Var "F"))))) "holds" (Bool (Set (Set (Var "f")) ($#k5_relat_1 :::"|"::: ) (Set (Var "A"))) ($#r2_hidden :::"in"::: ) (Set ($#k4_card_3 :::"product"::: ) (Set "(" (Set (Var "F")) ($#k5_relat_1 :::"|"::: ) (Set (Var "A")) ")" ))))) ; theorem :: PRALG_3:2 (Bool "for" (Set (Var "I")) "being" ($#~v1_xboole_0 "non" ($#v1_xboole_0 :::"empty"::: ) ) ($#m1_hidden :::"set"::: ) (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" ($#m1_pralg_2 :::"MSAlgebra-Family"::: ) "of" (Set (Var "I")) "," (Set (Var "S")) (Bool "for" (Set (Var "s")) "being" ($#m1_subset_1 :::"SortSymbol":::) "of" (Set (Var "S")) (Bool "for" (Set (Var "a")) "being" ($#~v1_xboole_0 "non" ($#v1_xboole_0 :::"empty"::: ) ) ($#m1_subset_1 :::"Subset":::) "of" (Set (Var "I")) (Bool "for" (Set (Var "Aa")) "being" ($#m1_pralg_2 :::"MSAlgebra-Family"::: ) "of" (Set (Var "a")) "," (Set (Var "S")) "st" (Bool (Bool (Set (Set (Var "A")) ($#k5_relat_1 :::"|"::: ) (Set (Var "a"))) ($#r1_hidden :::"="::: ) (Set (Var "Aa")))) "holds" (Bool (Set ($#k9_pralg_2 :::"Carrier"::: ) "(" (Set (Var "Aa")) "," (Set (Var "s")) ")" ) ($#r1_hidden :::"="::: ) (Set (Set "(" ($#k9_pralg_2 :::"Carrier"::: ) "(" (Set (Var "A")) "," (Set (Var "s")) ")" ")" ) ($#k5_relat_1 :::"|"::: ) (Set (Var "a")))))))))) ; theorem :: PRALG_3:3 (Bool "for" (Set (Var "i")) "being" ($#m1_hidden :::"set"::: ) (Bool "for" (Set (Var "I")) "being" ($#~v1_xboole_0 "non" ($#v1_xboole_0 :::"empty"::: ) ) ($#m1_hidden :::"set"::: ) (Bool "for" (Set (Var "EqR")) "being" ($#m1_subset_1 :::"Equivalence_Relation":::) "of" (Set (Var "I")) (Bool "for" (Set (Var "c1")) "," (Set (Var "c2")) "being" ($#m2_subset_1 :::"Element"::: ) "of" (Set ($#k8_eqrel_1 :::"Class"::: ) (Set (Var "EqR"))) "st" (Bool (Bool (Set (Var "i")) ($#r2_hidden :::"in"::: ) (Set (Var "c1"))) & (Bool (Set (Var "i")) ($#r2_hidden :::"in"::: ) (Set (Var "c2")))) "holds" (Bool (Set (Var "c1")) ($#r1_hidden :::"="::: ) (Set (Var "c2"))))))) ; theorem :: PRALG_3:4 (Bool "for" (Set (Var "D")) "being" ($#~v1_xboole_0 "non" ($#v1_xboole_0 :::"empty"::: ) ) ($#m1_hidden :::"set"::: ) (Bool "for" (Set (Var "F")) "being" ($#m1_hidden :::"ManySortedFunction":::) "of" (Set (Var "D")) (Bool "for" (Set (Var "C")) "being" ($#~v1_xboole_0 "non" ($#v1_xboole_0 :::"empty"::: ) ) ($#v4_funct_1 :::"functional"::: ) ($#v2_card_3 :::"with_common_domain"::: ) ($#m1_hidden :::"set"::: ) "st" (Bool (Bool (Set (Var "C")) ($#r1_hidden :::"="::: ) (Set ($#k10_xtuple_0 :::"rng"::: ) (Set (Var "F"))))) "holds" (Bool "for" (Set (Var "d")) "being" ($#m1_subset_1 :::"Element"::: ) "of" (Set (Var "D")) (Bool "for" (Set (Var "e")) "being" ($#m1_hidden :::"set"::: ) "st" (Bool (Bool (Set (Var "e")) ($#r2_hidden :::"in"::: ) (Set ($#k9_card_3 :::"DOM"::: ) (Set (Var "C"))))) "holds" (Bool (Set (Set "(" (Set (Var "F")) ($#k1_funct_1 :::"."::: ) (Set (Var "d")) ")" ) ($#k1_funct_1 :::"."::: ) (Set (Var "e"))) ($#r1_hidden :::"="::: ) (Set (Set "(" (Set "(" ($#k10_funct_6 :::"commute"::: ) (Set (Var "F")) ")" ) ($#k1_funct_1 :::"."::: ) (Set (Var "e")) ")" ) ($#k1_funct_1 :::"."::: ) (Set (Var "d"))))))))) ; 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 "U0" be ($#l3_msualg_1 :::"MSAlgebra"::: ) "over" (Set (Const "S")); let "o" be ($#m1_subset_1 :::"OperSymbol":::) "of" (Set (Const "S")); func :::"const"::: "(" "o" "," "U0" ")" -> ($#m1_hidden :::"set"::: ) equals :: PRALG_3:def 1 (Set (Set "(" ($#k5_msualg_1 :::"Den"::: ) "(" "o" "," "U0" ")" ")" ) ($#k1_funct_1 :::"."::: ) (Set ($#k1_xboole_0 :::"{}"::: ) )); end; :: deftheorem defines :::"const"::: PRALG_3:def 1 : (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 "U0")) "being" ($#l3_msualg_1 :::"MSAlgebra"::: ) "over" (Set (Var "S")) (Bool "for" (Set (Var "o")) "being" ($#m1_subset_1 :::"OperSymbol":::) "of" (Set (Var "S")) "holds" (Bool (Set ($#k1_pralg_3 :::"const"::: ) "(" (Set (Var "o")) "," (Set (Var "U0")) ")" ) ($#r1_hidden :::"="::: ) (Set (Set "(" ($#k5_msualg_1 :::"Den"::: ) "(" (Set (Var "o")) "," (Set (Var "U0")) ")" ")" ) ($#k1_funct_1 :::"."::: ) (Set ($#k1_xboole_0 :::"{}"::: ) )))))); theorem :: PRALG_3: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 "U0")) "being" ($#l3_msualg_1 :::"MSAlgebra"::: ) "over" (Set (Var "S")) (Bool "for" (Set (Var "o")) "being" ($#m1_subset_1 :::"OperSymbol":::) "of" (Set (Var "S")) "st" (Bool (Bool (Set ($#k1_msualg_1 :::"the_arity_of"::: ) (Set (Var "o"))) ($#r1_hidden :::"="::: ) (Set ($#k1_xboole_0 :::"{}"::: ) )) & (Bool (Set ($#k4_msualg_1 :::"Result"::: ) "(" (Set (Var "o")) "," (Set (Var "U0")) ")" ) ($#r1_hidden :::"<>"::: ) (Set ($#k1_xboole_0 :::"{}"::: ) ))) "holds" (Bool (Set ($#k1_pralg_3 :::"const"::: ) "(" (Set (Var "o")) "," (Set (Var "U0")) ")" ) ($#r2_hidden :::"in"::: ) (Set ($#k4_msualg_1 :::"Result"::: ) "(" (Set (Var "o")) "," (Set (Var "U0")) ")" ))))) ; theorem :: PRALG_3: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 "U0")) "being" ($#l3_msualg_1 :::"MSAlgebra"::: ) "over" (Set (Var "S")) (Bool "for" (Set (Var "s")) "being" ($#m1_subset_1 :::"SortSymbol":::) "of" (Set (Var "S")) "st" (Bool (Bool (Set (Set "the" ($#u3_msualg_1 :::"Sorts"::: ) "of" (Set (Var "U0"))) ($#k1_funct_1 :::"."::: ) (Set (Var "s"))) ($#r1_hidden :::"<>"::: ) (Set ($#k1_xboole_0 :::"{}"::: ) ))) "holds" (Bool (Set ($#k1_msualg_2 :::"Constants"::: ) "(" (Set (Var "U0")) "," (Set (Var "s")) ")" ) ($#r1_hidden :::"="::: ) "{" (Set "(" ($#k1_pralg_3 :::"const"::: ) "(" (Set (Var "o")) "," (Set (Var "U0")) ")" ")" ) where o "is" ($#m1_subset_1 :::"Element"::: ) "of" (Set "the" ($#u4_struct_0 :::"carrier'"::: ) "of" (Set (Var "S"))) : (Bool "(" (Bool (Set ($#k2_msualg_1 :::"the_result_sort_of"::: ) (Set (Var "o"))) ($#r1_hidden :::"="::: ) (Set (Var "s"))) & (Bool (Set ($#k1_msualg_1 :::"the_arity_of"::: ) (Set (Var "o"))) ($#r1_hidden :::"="::: ) (Set ($#k1_xboole_0 :::"{}"::: ) )) ")" ) "}" )))) ; theorem :: PRALG_3:7 (Bool "for" (Set (Var "I")) "being" ($#~v1_xboole_0 "non" ($#v1_xboole_0 :::"empty"::: ) ) ($#m1_hidden :::"set"::: ) (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" ($#m1_pralg_2 :::"MSAlgebra-Family"::: ) "of" (Set (Var "I")) "," (Set (Var "S")) (Bool "for" (Set (Var "o")) "being" ($#m1_subset_1 :::"OperSymbol":::) "of" (Set (Var "S")) "st" (Bool (Bool (Set ($#k1_msualg_1 :::"the_arity_of"::: ) (Set (Var "o"))) ($#r1_hidden :::"="::: ) (Set ($#k1_xboole_0 :::"{}"::: ) ))) "holds" (Bool (Set (Set "(" ($#k10_funct_6 :::"commute"::: ) (Set "(" ($#k11_pralg_2 :::"OPER"::: ) (Set (Var "A")) ")" ) ")" ) ($#k1_funct_1 :::"."::: ) (Set (Var "o"))) ($#r2_hidden :::"in"::: ) (Set ($#k1_funct_2 :::"Funcs"::: ) "(" (Set (Var "I")) "," (Set "(" ($#k1_funct_2 :::"Funcs"::: ) "(" (Set ($#k1_tarski :::"{"::: ) (Set ($#k1_xboole_0 :::"{}"::: ) ) ($#k1_tarski :::"}"::: ) ) "," (Set "(" ($#k3_tarski :::"union"::: ) "{" (Set "(" ($#k4_msualg_1 :::"Result"::: ) "(" (Set (Var "o")) "," (Set "(" (Set (Var "A")) ($#k5_pralg_2 :::"."::: ) (Set (Var "i9")) ")" ) ")" ")" ) where i9 "is" ($#m1_subset_1 :::"Element"::: ) "of" (Set (Var "I")) : (Bool verum) "}" ")" ) ")" ")" ) ")" )))))) ; theorem :: PRALG_3:8 (Bool "for" (Set (Var "I")) "being" ($#~v1_xboole_0 "non" ($#v1_xboole_0 :::"empty"::: ) ) ($#m1_hidden :::"set"::: ) (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" ($#m1_pralg_2 :::"MSAlgebra-Family"::: ) "of" (Set (Var "I")) "," (Set (Var "S")) (Bool "for" (Set (Var "o")) "being" ($#m1_subset_1 :::"OperSymbol":::) "of" (Set (Var "S")) "st" (Bool (Bool (Set ($#k1_msualg_1 :::"the_arity_of"::: ) (Set (Var "o"))) ($#r1_hidden :::"="::: ) (Set ($#k1_xboole_0 :::"{}"::: ) ))) "holds" (Bool (Set ($#k1_pralg_3 :::"const"::: ) "(" (Set (Var "o")) "," (Set "(" ($#k14_pralg_2 :::"product"::: ) (Set (Var "A")) ")" ) ")" ) ($#r2_hidden :::"in"::: ) (Set ($#k1_funct_2 :::"Funcs"::: ) "(" (Set (Var "I")) "," (Set "(" ($#k3_tarski :::"union"::: ) "{" (Set "(" ($#k4_msualg_1 :::"Result"::: ) "(" (Set (Var "o")) "," (Set "(" (Set (Var "A")) ($#k5_pralg_2 :::"."::: ) (Set (Var "i9")) ")" ) ")" ")" ) where i9 "is" ($#m1_subset_1 :::"Element"::: ) "of" (Set (Var "I")) : (Bool verum) "}" ")" ) ")" )))))) ; 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 ($#~v1_xboole_0 "non" ($#v1_xboole_0 :::"empty"::: ) ) ($#m1_hidden :::"set"::: ) ; let "o" be ($#m1_subset_1 :::"OperSymbol":::) "of" (Set (Const "S")); let "A" be ($#m1_pralg_2 :::"MSAlgebra-Family"::: ) "of" (Set (Const "I")) "," (Set (Const "S")); cluster (Set ($#k1_pralg_3 :::"const"::: ) "(" "o" "," (Set "(" ($#k14_pralg_2 :::"product"::: ) "A" ")" ) ")" ) -> ($#v1_relat_1 :::"Relation-like"::: ) ($#v1_funct_1 :::"Function-like"::: ) ; end; theorem :: PRALG_3:9 (Bool "for" (Set (Var "I")) "being" ($#~v1_xboole_0 "non" ($#v1_xboole_0 :::"empty"::: ) ) ($#m1_hidden :::"set"::: ) (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" ($#m1_subset_1 :::"Element"::: ) "of" (Set (Var "I")) (Bool "for" (Set (Var "A")) "being" ($#m1_pralg_2 :::"MSAlgebra-Family"::: ) "of" (Set (Var "I")) "," (Set (Var "S")) (Bool "for" (Set (Var "o")) "being" ($#m1_subset_1 :::"OperSymbol":::) "of" (Set (Var "S")) "st" (Bool (Bool (Set ($#k1_msualg_1 :::"the_arity_of"::: ) (Set (Var "o"))) ($#r1_hidden :::"="::: ) (Set ($#k1_xboole_0 :::"{}"::: ) ))) "holds" (Bool (Set (Set "(" ($#k1_pralg_3 :::"const"::: ) "(" (Set (Var "o")) "," (Set "(" ($#k14_pralg_2 :::"product"::: ) (Set (Var "A")) ")" ) ")" ")" ) ($#k1_funct_1 :::"."::: ) (Set (Var "i"))) ($#r1_hidden :::"="::: ) (Set ($#k1_pralg_3 :::"const"::: ) "(" (Set (Var "o")) "," (Set "(" (Set (Var "A")) ($#k5_pralg_2 :::"."::: ) (Set (Var "i")) ")" ) ")" ))))))) ; theorem :: PRALG_3:10 (Bool "for" (Set (Var "I")) "being" ($#~v1_xboole_0 "non" ($#v1_xboole_0 :::"empty"::: ) ) ($#m1_hidden :::"set"::: ) (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" ($#m1_pralg_2 :::"MSAlgebra-Family"::: ) "of" (Set (Var "I")) "," (Set (Var "S")) (Bool "for" (Set (Var "o")) "being" ($#m1_subset_1 :::"OperSymbol":::) "of" (Set (Var "S")) (Bool "for" (Set (Var "f")) "being" ($#m1_hidden :::"Function":::) "st" (Bool (Bool (Set ($#k1_msualg_1 :::"the_arity_of"::: ) (Set (Var "o"))) ($#r1_hidden :::"="::: ) (Set ($#k1_xboole_0 :::"{}"::: ) )) & (Bool (Set ($#k9_xtuple_0 :::"dom"::: ) (Set (Var "f"))) ($#r1_hidden :::"="::: ) (Set (Var "I"))) & (Bool "(" "for" (Set (Var "i")) "being" ($#m1_subset_1 :::"Element"::: ) "of" (Set (Var "I")) "holds" (Bool (Set (Set (Var "f")) ($#k1_funct_1 :::"."::: ) (Set (Var "i"))) ($#r1_hidden :::"="::: ) (Set ($#k1_pralg_3 :::"const"::: ) "(" (Set (Var "o")) "," (Set "(" (Set (Var "A")) ($#k5_pralg_2 :::"."::: ) (Set (Var "i")) ")" ) ")" )) ")" )) "holds" (Bool (Set (Var "f")) ($#r1_hidden :::"="::: ) (Set ($#k1_pralg_3 :::"const"::: ) "(" (Set (Var "o")) "," (Set "(" ($#k14_pralg_2 :::"product"::: ) (Set (Var "A")) ")" ) ")" ))))))) ; theorem :: PRALG_3:11 (Bool "for" (Set (Var "S")) "being" ($#~v2_struct_0 "non" ($#v2_struct_0 :::"empty"::: ) ) ($#~v11_struct_0 "non" ($#v11_struct_0 :::"void"::: ) ) ($#l1_msualg_1 :::"ManySortedSign"::: ) (Bool "for" (Set (Var "U1")) "," (Set (Var "U2")) "being" ($#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 "e")) "being" ($#m1_subset_1 :::"Element"::: ) "of" (Set ($#k3_msualg_1 :::"Args"::: ) "(" (Set (Var "o")) "," (Set (Var "U1")) ")" ) "st" (Bool (Bool (Set (Var "e")) ($#r1_hidden :::"="::: ) (Set ($#k1_xboole_0 :::"{}"::: ) )) & (Bool (Set ($#k1_msualg_1 :::"the_arity_of"::: ) (Set (Var "o"))) ($#r1_hidden :::"="::: ) (Set ($#k1_xboole_0 :::"{}"::: ) )) & (Bool (Set ($#k3_msualg_1 :::"Args"::: ) "(" (Set (Var "o")) "," (Set (Var "U1")) ")" ) ($#r1_hidden :::"<>"::: ) (Set ($#k1_xboole_0 :::"{}"::: ) )) & (Bool (Set ($#k3_msualg_1 :::"Args"::: ) "(" (Set (Var "o")) "," (Set (Var "U2")) ")" ) ($#r1_hidden :::"<>"::: ) (Set ($#k1_xboole_0 :::"{}"::: ) ))) "holds" (Bool "for" (Set (Var "F")) "being" ($#m2_pboole :::"ManySortedFunction":::) "of" (Set (Var "U1")) "," (Set (Var "U2")) "holds" (Bool (Set (Set (Var "F")) ($#k5_msualg_3 :::"#"::: ) (Set (Var "e"))) ($#r1_hidden :::"="::: ) (Set ($#k1_xboole_0 :::"{}"::: ) ))))))) ; begin theorem :: PRALG_3:12 (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 "o")) "being" ($#m1_subset_1 :::"OperSymbol":::) "of" (Set (Var "S")) (Bool "for" (Set (Var "U1")) "," (Set (Var "U2")) "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 "U1")) "," (Set (Var "U2")) (Bool "for" (Set (Var "x")) "being" ($#m1_subset_1 :::"Element"::: ) "of" (Set ($#k3_msualg_1 :::"Args"::: ) "(" (Set (Var "o")) "," (Set (Var "U1")) ")" ) "holds" (Bool (Set (Var "x")) ($#r2_hidden :::"in"::: ) (Set ($#k4_card_3 :::"product"::: ) (Set "(" ($#k2_funct_6 :::"doms"::: ) (Set "(" (Set (Var "F")) ($#k3_relat_1 :::"*"::: ) (Set "(" ($#k1_msualg_1 :::"the_arity_of"::: ) (Set (Var "o")) ")" ) ")" ) ")" )))))))) ; theorem :: PRALG_3:13 (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 "o")) "being" ($#m1_subset_1 :::"OperSymbol":::) "of" (Set (Var "S")) (Bool "for" (Set (Var "U1")) "," (Set (Var "U2")) "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 "U1")) "," (Set (Var "U2")) (Bool "for" (Set (Var "x")) "being" ($#m1_subset_1 :::"Element"::: ) "of" (Set ($#k3_msualg_1 :::"Args"::: ) "(" (Set (Var "o")) "," (Set (Var "U1")) ")" ) (Bool "for" (Set (Var "n")) "being" ($#m1_hidden :::"set"::: ) "st" (Bool (Bool (Set (Var "n")) ($#r2_hidden :::"in"::: ) (Set ($#k1_relset_1 :::"dom"::: ) (Set "(" ($#k1_msualg_1 :::"the_arity_of"::: ) (Set (Var "o")) ")" )))) "holds" (Bool (Set (Set "(" (Set (Var "F")) ($#k5_msualg_3 :::"#"::: ) (Set (Var "x")) ")" ) ($#k1_funct_1 :::"."::: ) (Set (Var "n"))) ($#r1_hidden :::"="::: ) (Set (Set "(" (Set (Var "F")) ($#k1_msualg_3 :::"."::: ) (Set "(" (Set "(" ($#k1_msualg_1 :::"the_arity_of"::: ) (Set (Var "o")) ")" ) ($#k7_partfun1 :::"/."::: ) (Set (Var "n")) ")" ) ")" ) ($#k1_funct_1 :::"."::: ) (Set "(" (Set (Var "x")) ($#k1_funct_1 :::"."::: ) (Set (Var "n")) ")" ))))))))) ; theorem :: PRALG_3:14 (Bool "for" (Set (Var "I")) "being" ($#~v1_xboole_0 "non" ($#v1_xboole_0 :::"empty"::: ) ) ($#m1_hidden :::"set"::: ) (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" ($#m1_pralg_2 :::"MSAlgebra-Family"::: ) "of" (Set (Var "I")) "," (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 "(" ($#k14_pralg_2 :::"product"::: ) (Set (Var "A")) ")" ) ")" ) "holds" (Bool (Set (Var "x")) ($#r2_hidden :::"in"::: ) (Set ($#k1_funct_2 :::"Funcs"::: ) "(" (Set "(" ($#k1_relset_1 :::"dom"::: ) (Set "(" ($#k1_msualg_1 :::"the_arity_of"::: ) (Set (Var "o")) ")" ) ")" ) "," (Set "(" ($#k1_funct_2 :::"Funcs"::: ) "(" (Set (Var "I")) "," (Set "(" ($#k3_tarski :::"union"::: ) "{" (Set "(" (Set "the" ($#u3_msualg_1 :::"Sorts"::: ) "of" (Set "(" (Set (Var "A")) ($#k5_pralg_2 :::"."::: ) (Set (Var "i9")) ")" )) ($#k1_funct_1 :::"."::: ) (Set (Var "s9")) ")" ) where i9 "is" ($#m1_subset_1 :::"Element"::: ) "of" (Set (Var "I")), s9 "is" ($#m1_subset_1 :::"Element"::: ) "of" (Set "the" ($#u1_struct_0 :::"carrier"::: ) "of" (Set (Var "S"))) : (Bool verum) "}" ")" ) ")" ")" ) ")" ))))))) ; theorem :: PRALG_3:15 (Bool "for" (Set (Var "I")) "being" ($#~v1_xboole_0 "non" ($#v1_xboole_0 :::"empty"::: ) ) ($#m1_hidden :::"set"::: ) (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" ($#m1_pralg_2 :::"MSAlgebra-Family"::: ) "of" (Set (Var "I")) "," (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 "(" ($#k14_pralg_2 :::"product"::: ) (Set (Var "A")) ")" ) ")" ) (Bool "for" (Set (Var "n")) "being" ($#m1_hidden :::"set"::: ) "st" (Bool (Bool (Set (Var "n")) ($#r2_hidden :::"in"::: ) (Set ($#k1_relset_1 :::"dom"::: ) (Set "(" ($#k1_msualg_1 :::"the_arity_of"::: ) (Set (Var "o")) ")" )))) "holds" (Bool (Set (Set (Var "x")) ($#k1_funct_1 :::"."::: ) (Set (Var "n"))) ($#r2_hidden :::"in"::: ) (Set ($#k4_card_3 :::"product"::: ) (Set "(" ($#k9_pralg_2 :::"Carrier"::: ) "(" (Set (Var "A")) "," (Set "(" (Set "(" ($#k1_msualg_1 :::"the_arity_of"::: ) (Set (Var "o")) ")" ) ($#k7_partfun1 :::"/."::: ) (Set (Var "n")) ")" ) ")" ")" ))))))))) ; theorem :: PRALG_3:16 (Bool "for" (Set (Var "I")) "being" ($#~v1_xboole_0 "non" ($#v1_xboole_0 :::"empty"::: ) ) ($#m1_hidden :::"set"::: ) (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" ($#m1_pralg_2 :::"MSAlgebra-Family"::: ) "of" (Set (Var "I")) "," (Set (Var "S")) (Bool "for" (Set (Var "o")) "being" ($#m1_subset_1 :::"OperSymbol":::) "of" (Set (Var "S")) (Bool "for" (Set (Var "i")) "being" ($#m1_subset_1 :::"Element"::: ) "of" (Set (Var "I")) (Bool "for" (Set (Var "n")) "being" ($#m1_hidden :::"set"::: ) "st" (Bool (Bool (Set (Var "n")) ($#r2_hidden :::"in"::: ) (Set ($#k1_relset_1 :::"dom"::: ) (Set "(" ($#k1_msualg_1 :::"the_arity_of"::: ) (Set (Var "o")) ")" )))) "holds" (Bool "for" (Set (Var "s")) "being" ($#m1_subset_1 :::"SortSymbol":::) "of" (Set (Var "S")) "st" (Bool (Bool (Set (Var "s")) ($#r1_hidden :::"="::: ) (Set (Set "(" ($#k1_msualg_1 :::"the_arity_of"::: ) (Set (Var "o")) ")" ) ($#k1_funct_1 :::"."::: ) (Set (Var "n"))))) "holds" (Bool "for" (Set (Var "y")) "being" ($#m1_subset_1 :::"Element"::: ) "of" (Set ($#k3_msualg_1 :::"Args"::: ) "(" (Set (Var "o")) "," (Set "(" ($#k14_pralg_2 :::"product"::: ) (Set (Var "A")) ")" ) ")" ) (Bool "for" (Set (Var "g")) "being" ($#m1_hidden :::"Function":::) "st" (Bool (Bool (Set (Var "g")) ($#r1_hidden :::"="::: ) (Set (Set (Var "y")) ($#k1_funct_1 :::"."::: ) (Set (Var "n"))))) "holds" (Bool (Set (Set (Var "g")) ($#k1_funct_1 :::"."::: ) (Set (Var "i"))) ($#r2_hidden :::"in"::: ) (Set (Set "the" ($#u3_msualg_1 :::"Sorts"::: ) "of" (Set "(" (Set (Var "A")) ($#k5_pralg_2 :::"."::: ) (Set (Var "i")) ")" )) ($#k1_funct_1 :::"."::: ) (Set (Var "s"))))))))))))) ; theorem :: PRALG_3:17 (Bool "for" (Set (Var "I")) "being" ($#~v1_xboole_0 "non" ($#v1_xboole_0 :::"empty"::: ) ) ($#m1_hidden :::"set"::: ) (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" ($#m1_pralg_2 :::"MSAlgebra-Family"::: ) "of" (Set (Var "I")) "," (Set (Var "S")) (Bool "for" (Set (Var "o")) "being" ($#m1_subset_1 :::"OperSymbol":::) "of" (Set (Var "S")) (Bool "for" (Set (Var "y")) "being" ($#m1_subset_1 :::"Element"::: ) "of" (Set ($#k3_msualg_1 :::"Args"::: ) "(" (Set (Var "o")) "," (Set "(" ($#k14_pralg_2 :::"product"::: ) (Set (Var "A")) ")" ) ")" ) "st" (Bool (Bool (Set ($#k1_msualg_1 :::"the_arity_of"::: ) (Set (Var "o"))) ($#r1_hidden :::"<>"::: ) (Set ($#k1_xboole_0 :::"{}"::: ) ))) "holds" (Bool (Set ($#k10_funct_6 :::"commute"::: ) (Set (Var "y"))) ($#r2_hidden :::"in"::: ) (Set ($#k4_card_3 :::"product"::: ) (Set "(" ($#k2_funct_6 :::"doms"::: ) (Set "(" (Set (Var "A")) ($#k12_pralg_2 :::"?."::: ) (Set (Var "o")) ")" ) ")" )))))))) ; theorem :: PRALG_3:18 (Bool "for" (Set (Var "I")) "being" ($#~v1_xboole_0 "non" ($#v1_xboole_0 :::"empty"::: ) ) ($#m1_hidden :::"set"::: ) (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" ($#m1_pralg_2 :::"MSAlgebra-Family"::: ) "of" (Set (Var "I")) "," (Set (Var "S")) (Bool "for" (Set (Var "o")) "being" ($#m1_subset_1 :::"OperSymbol":::) "of" (Set (Var "S")) (Bool "for" (Set (Var "y")) "being" ($#m1_subset_1 :::"Element"::: ) "of" (Set ($#k3_msualg_1 :::"Args"::: ) "(" (Set (Var "o")) "," (Set "(" ($#k14_pralg_2 :::"product"::: ) (Set (Var "A")) ")" ) ")" ) "st" (Bool (Bool (Set ($#k1_msualg_1 :::"the_arity_of"::: ) (Set (Var "o"))) ($#r1_hidden :::"<>"::: ) (Set ($#k1_xboole_0 :::"{}"::: ) ))) "holds" (Bool (Set (Var "y")) ($#r2_hidden :::"in"::: ) (Set ($#k9_xtuple_0 :::"dom"::: ) (Set "(" ($#k1_pralg_2 :::"Commute"::: ) (Set "(" ($#k2_pralg_2 :::"Frege"::: ) (Set "(" (Set (Var "A")) ($#k12_pralg_2 :::"?."::: ) (Set (Var "o")) ")" ) ")" ) ")" )))))))) ; theorem :: PRALG_3:19 (Bool "for" (Set (Var "I")) "being" ($#m1_hidden :::"set"::: ) (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" ($#m1_pralg_2 :::"MSAlgebra-Family"::: ) "of" (Set (Var "I")) "," (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 "(" ($#k14_pralg_2 :::"product"::: ) (Set (Var "A")) ")" ) ")" ) "holds" (Bool (Set (Set "(" ($#k5_msualg_1 :::"Den"::: ) "(" (Set (Var "o")) "," (Set "(" ($#k14_pralg_2 :::"product"::: ) (Set (Var "A")) ")" ) ")" ")" ) ($#k3_funct_2 :::"."::: ) (Set (Var "x"))) ($#r2_hidden :::"in"::: ) (Set ($#k4_card_3 :::"product"::: ) (Set "(" ($#k9_pralg_2 :::"Carrier"::: ) "(" (Set (Var "A")) "," (Set "(" ($#k2_msualg_1 :::"the_result_sort_of"::: ) (Set (Var "o")) ")" ) ")" ")" )))))))) ; theorem :: PRALG_3:20 (Bool "for" (Set (Var "I")) "being" ($#~v1_xboole_0 "non" ($#v1_xboole_0 :::"empty"::: ) ) ($#m1_hidden :::"set"::: ) (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" ($#m1_pralg_2 :::"MSAlgebra-Family"::: ) "of" (Set (Var "I")) "," (Set (Var "S")) (Bool "for" (Set (Var "i")) "being" ($#m1_subset_1 :::"Element"::: ) "of" (Set (Var "I")) (Bool "for" (Set (Var "o")) "being" ($#m1_subset_1 :::"OperSymbol":::) "of" (Set (Var "S")) "st" (Bool (Bool (Set ($#k1_msualg_1 :::"the_arity_of"::: ) (Set (Var "o"))) ($#r1_hidden :::"<>"::: ) (Set ($#k1_xboole_0 :::"{}"::: ) ))) "holds" (Bool "for" (Set (Var "U1")) "being" ($#v4_msualg_1 :::"non-empty"::: ) ($#l3_msualg_1 :::"MSAlgebra"::: ) "over" (Set (Var "S")) (Bool "for" (Set (Var "x")) "being" ($#m1_subset_1 :::"Element"::: ) "of" (Set ($#k3_msualg_1 :::"Args"::: ) "(" (Set (Var "o")) "," (Set "(" ($#k14_pralg_2 :::"product"::: ) (Set (Var "A")) ")" ) ")" ) "holds" (Bool (Set (Set "(" ($#k10_funct_6 :::"commute"::: ) (Set (Var "x")) ")" ) ($#k1_funct_1 :::"."::: ) (Set (Var "i"))) "is" ($#m1_subset_1 :::"Element"::: ) "of" (Set ($#k3_msualg_1 :::"Args"::: ) "(" (Set (Var "o")) "," (Set "(" (Set (Var "A")) ($#k5_pralg_2 :::"."::: ) (Set (Var "i")) ")" ) ")" ))))))))) ; theorem :: PRALG_3:21 (Bool "for" (Set (Var "I")) "being" ($#~v1_xboole_0 "non" ($#v1_xboole_0 :::"empty"::: ) ) ($#m1_hidden :::"set"::: ) (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" ($#m1_pralg_2 :::"MSAlgebra-Family"::: ) "of" (Set (Var "I")) "," (Set (Var "S")) (Bool "for" (Set (Var "i")) "being" ($#m1_subset_1 :::"Element"::: ) "of" (Set (Var "I")) (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 "(" ($#k14_pralg_2 :::"product"::: ) (Set (Var "A")) ")" ) ")" ) (Bool "for" (Set (Var "n")) "being" ($#m1_hidden :::"set"::: ) "st" (Bool (Bool (Set (Var "n")) ($#r2_hidden :::"in"::: ) (Set ($#k1_relset_1 :::"dom"::: ) (Set "(" ($#k1_msualg_1 :::"the_arity_of"::: ) (Set (Var "o")) ")" )))) "holds" (Bool "for" (Set (Var "f")) "being" ($#m1_hidden :::"Function":::) "st" (Bool (Bool (Set (Var "f")) ($#r1_hidden :::"="::: ) (Set (Set (Var "x")) ($#k1_funct_1 :::"."::: ) (Set (Var "n"))))) "holds" (Bool (Set (Set "(" (Set "(" ($#k10_funct_6 :::"commute"::: ) (Set (Var "x")) ")" ) ($#k1_funct_1 :::"."::: ) (Set (Var "i")) ")" ) ($#k1_funct_1 :::"."::: ) (Set (Var "n"))) ($#r1_hidden :::"="::: ) (Set (Set (Var "f")) ($#k1_funct_1 :::"."::: ) (Set (Var "i")))))))))))) ; theorem :: PRALG_3:22 (Bool "for" (Set (Var "I")) "being" ($#~v1_xboole_0 "non" ($#v1_xboole_0 :::"empty"::: ) ) ($#m1_hidden :::"set"::: ) (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" ($#m1_pralg_2 :::"MSAlgebra-Family"::: ) "of" (Set (Var "I")) "," (Set (Var "S")) (Bool "for" (Set (Var "o")) "being" ($#m1_subset_1 :::"OperSymbol":::) "of" (Set (Var "S")) "st" (Bool (Bool (Set ($#k1_msualg_1 :::"the_arity_of"::: ) (Set (Var "o"))) ($#r1_hidden :::"<>"::: ) (Set ($#k1_xboole_0 :::"{}"::: ) ))) "holds" (Bool "for" (Set (Var "y")) "being" ($#m1_subset_1 :::"Element"::: ) "of" (Set ($#k3_msualg_1 :::"Args"::: ) "(" (Set (Var "o")) "," (Set "(" ($#k14_pralg_2 :::"product"::: ) (Set (Var "A")) ")" ) ")" ) (Bool "for" (Set (Var "i9")) "being" ($#m1_subset_1 :::"Element"::: ) "of" (Set (Var "I")) (Bool "for" (Set (Var "g")) "being" ($#m1_hidden :::"Function":::) "st" (Bool (Bool (Set (Var "g")) ($#r1_hidden :::"="::: ) (Set (Set "(" ($#k5_msualg_1 :::"Den"::: ) "(" (Set (Var "o")) "," (Set "(" ($#k14_pralg_2 :::"product"::: ) (Set (Var "A")) ")" ) ")" ")" ) ($#k3_funct_2 :::"."::: ) (Set (Var "y"))))) "holds" (Bool (Set (Set (Var "g")) ($#k1_funct_1 :::"."::: ) (Set (Var "i9"))) ($#r1_hidden :::"="::: ) (Set (Set "(" ($#k5_msualg_1 :::"Den"::: ) "(" (Set (Var "o")) "," (Set "(" (Set (Var "A")) ($#k5_pralg_2 :::"."::: ) (Set (Var "i9")) ")" ) ")" ")" ) ($#k1_funct_1 :::"."::: ) (Set "(" (Set "(" ($#k10_funct_6 :::"commute"::: ) (Set (Var "y")) ")" ) ($#k1_funct_1 :::"."::: ) (Set (Var "i9")) ")" )))))))))) ; begin definitionlet "I" be ($#~v1_xboole_0 "non" ($#v1_xboole_0 :::"empty"::: ) ) ($#m1_hidden :::"set"::: ) ; let "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 ($#m1_pralg_2 :::"MSAlgebra-Family"::: ) "of" (Set (Const "I")) "," (Set (Const "S")); let "i" be ($#m1_subset_1 :::"Element"::: ) "of" (Set (Const "I")); func :::"proj"::: "(" "A" "," "i" ")" -> ($#m2_pboole :::"ManySortedFunction":::) "of" (Set "(" ($#k14_pralg_2 :::"product"::: ) "A" ")" ) "," (Set "(" "A" ($#k5_pralg_2 :::"."::: ) "i" ")" ) means :: PRALG_3:def 2 (Bool "for" (Set (Var "s")) "being" ($#m1_subset_1 :::"Element":::) "of" "S" "holds" (Bool (Set it ($#k1_msualg_3 :::"."::: ) (Set (Var "s"))) ($#r1_hidden :::"="::: ) (Set ($#k12_card_3 :::"proj"::: ) "(" (Set "(" ($#k9_pralg_2 :::"Carrier"::: ) "(" "A" "," (Set (Var "s")) ")" ")" ) "," "i" ")" ))); end; :: deftheorem defines :::"proj"::: PRALG_3:def 2 : (Bool "for" (Set (Var "I")) "being" ($#~v1_xboole_0 "non" ($#v1_xboole_0 :::"empty"::: ) ) ($#m1_hidden :::"set"::: ) (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" ($#m1_pralg_2 :::"MSAlgebra-Family"::: ) "of" (Set (Var "I")) "," (Set (Var "S")) (Bool "for" (Set (Var "i")) "being" ($#m1_subset_1 :::"Element"::: ) "of" (Set (Var "I")) (Bool "for" (Set (Var "b5")) "being" ($#m2_pboole :::"ManySortedFunction":::) "of" (Set "(" ($#k14_pralg_2 :::"product"::: ) (Set (Var "A")) ")" ) "," (Set "(" (Set (Var "A")) ($#k5_pralg_2 :::"."::: ) (Set (Var "i")) ")" ) "holds" (Bool "(" (Bool (Set (Var "b5")) ($#r1_hidden :::"="::: ) (Set ($#k2_pralg_3 :::"proj"::: ) "(" (Set (Var "A")) "," (Set (Var "i")) ")" )) "iff" (Bool "for" (Set (Var "s")) "being" ($#m1_subset_1 :::"Element":::) "of" (Set (Var "S")) "holds" (Bool (Set (Set (Var "b5")) ($#k1_msualg_3 :::"."::: ) (Set (Var "s"))) ($#r1_hidden :::"="::: ) (Set ($#k12_card_3 :::"proj"::: ) "(" (Set "(" ($#k9_pralg_2 :::"Carrier"::: ) "(" (Set (Var "A")) "," (Set (Var "s")) ")" ")" ) "," (Set (Var "i")) ")" ))) ")" )))))); theorem :: PRALG_3:23 (Bool "for" (Set (Var "I")) "being" ($#~v1_xboole_0 "non" ($#v1_xboole_0 :::"empty"::: ) ) ($#m1_hidden :::"set"::: ) (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" ($#m1_pralg_2 :::"MSAlgebra-Family"::: ) "of" (Set (Var "I")) "," (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 "(" ($#k14_pralg_2 :::"product"::: ) (Set (Var "A")) ")" ) ")" ) "st" (Bool (Bool (Set ($#k1_msualg_1 :::"the_arity_of"::: ) (Set (Var "o"))) ($#r1_hidden :::"<>"::: ) (Set ($#k1_xboole_0 :::"{}"::: ) ))) "holds" (Bool "for" (Set (Var "i")) "being" ($#m1_subset_1 :::"Element"::: ) "of" (Set (Var "I")) "holds" (Bool (Set (Set "(" ($#k2_pralg_3 :::"proj"::: ) "(" (Set (Var "A")) "," (Set (Var "i")) ")" ")" ) ($#k5_msualg_3 :::"#"::: ) (Set (Var "x"))) ($#r1_hidden :::"="::: ) (Set (Set "(" ($#k10_funct_6 :::"commute"::: ) (Set (Var "x")) ")" ) ($#k1_funct_1 :::"."::: ) (Set (Var "i")))))))))) ; theorem :: PRALG_3:24 (Bool "for" (Set (Var "I")) "being" ($#~v1_xboole_0 "non" ($#v1_xboole_0 :::"empty"::: ) ) ($#m1_hidden :::"set"::: ) (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" ($#m1_subset_1 :::"Element"::: ) "of" (Set (Var "I")) (Bool "for" (Set (Var "A")) "being" ($#m1_pralg_2 :::"MSAlgebra-Family"::: ) "of" (Set (Var "I")) "," (Set (Var "S")) "holds" (Bool (Set ($#k2_pralg_3 :::"proj"::: ) "(" (Set (Var "A")) "," (Set (Var "i")) ")" ) ($#r1_msualg_3 :::"is_homomorphism"::: ) (Set ($#k14_pralg_2 :::"product"::: ) (Set (Var "A"))) "," (Set (Set (Var "A")) ($#k5_pralg_2 :::"."::: ) (Set (Var "i")))))))) ; theorem :: PRALG_3:25 (Bool "for" (Set (Var "I")) "being" ($#~v1_xboole_0 "non" ($#v1_xboole_0 :::"empty"::: ) ) ($#m1_hidden :::"set"::: ) (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" ($#m1_subset_1 :::"Element"::: ) "of" (Set (Var "I")) (Bool "for" (Set (Var "A")) "being" ($#m1_pralg_2 :::"MSAlgebra-Family"::: ) "of" (Set (Var "I")) "," (Set (Var "S")) (Bool "for" (Set (Var "s")) "being" ($#m1_subset_1 :::"SortSymbol":::) "of" (Set (Var "S")) (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_hidden :::"ManySortedFunction":::) "of" (Set (Var "I")) "st" (Bool (Bool "(" "for" (Set (Var "i")) "being" ($#m1_subset_1 :::"Element"::: ) "of" (Set (Var "I")) (Bool "ex" (Set (Var "F1")) "being" ($#m2_pboole :::"ManySortedFunction":::) "of" (Set (Var "U1")) "," (Set "(" (Set (Var "A")) ($#k5_pralg_2 :::"."::: ) (Set (Var "i")) ")" ) "st" (Bool "(" (Bool (Set (Var "F1")) ($#r1_hidden :::"="::: ) (Set (Set (Var "F")) ($#k1_funct_1 :::"."::: ) (Set (Var "i")))) & (Bool (Set (Var "F1")) ($#r1_msualg_3 :::"is_homomorphism"::: ) (Set (Var "U1")) "," (Set (Set (Var "A")) ($#k5_pralg_2 :::"."::: ) (Set (Var "i")))) ")" )) ")" )) "holds" (Bool "(" (Bool (Set (Var "F")) ($#r2_hidden :::"in"::: ) (Set ($#k1_funct_2 :::"Funcs"::: ) "(" (Set (Var "I")) "," (Set "(" ($#k1_funct_2 :::"Funcs"::: ) "(" (Set "the" ($#u1_struct_0 :::"carrier"::: ) "of" (Set (Var "S"))) "," "{" (Set "(" (Set "(" (Set (Var "F")) ($#k1_funct_1 :::"."::: ) (Set (Var "i9")) ")" ) ($#k1_funct_1 :::"."::: ) (Set (Var "s1")) ")" ) where s1 "is" ($#m1_subset_1 :::"SortSymbol":::) "of" (Set (Var "S")), i9 "is" ($#m1_subset_1 :::"Element"::: ) "of" (Set (Var "I")) : (Bool verum) "}" ")" ")" ) ")" )) & (Bool (Set (Set "(" (Set "(" ($#k10_funct_6 :::"commute"::: ) (Set (Var "F")) ")" ) ($#k1_funct_1 :::"."::: ) (Set (Var "s")) ")" ) ($#k1_funct_1 :::"."::: ) (Set (Var "i"))) ($#r1_hidden :::"="::: ) (Set (Set "(" (Set (Var "F")) ($#k1_funct_1 :::"."::: ) (Set (Var "i")) ")" ) ($#k1_funct_1 :::"."::: ) (Set (Var "s")))) ")" )))))))) ; theorem :: PRALG_3:26 (Bool "for" (Set (Var "I")) "being" ($#~v1_xboole_0 "non" ($#v1_xboole_0 :::"empty"::: ) ) ($#m1_hidden :::"set"::: ) (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" ($#m1_pralg_2 :::"MSAlgebra-Family"::: ) "of" (Set (Var "I")) "," (Set (Var "S")) (Bool "for" (Set (Var "s")) "being" ($#m1_subset_1 :::"SortSymbol":::) "of" (Set (Var "S")) (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_hidden :::"ManySortedFunction":::) "of" (Set (Var "I")) "st" (Bool (Bool "(" "for" (Set (Var "i")) "being" ($#m1_subset_1 :::"Element"::: ) "of" (Set (Var "I")) (Bool "ex" (Set (Var "F1")) "being" ($#m2_pboole :::"ManySortedFunction":::) "of" (Set (Var "U1")) "," (Set "(" (Set (Var "A")) ($#k5_pralg_2 :::"."::: ) (Set (Var "i")) ")" ) "st" (Bool "(" (Bool (Set (Var "F1")) ($#r1_hidden :::"="::: ) (Set (Set (Var "F")) ($#k1_funct_1 :::"."::: ) (Set (Var "i")))) & (Bool (Set (Var "F1")) ($#r1_msualg_3 :::"is_homomorphism"::: ) (Set (Var "U1")) "," (Set (Set (Var "A")) ($#k5_pralg_2 :::"."::: ) (Set (Var "i")))) ")" )) ")" )) "holds" (Bool (Set (Set "(" ($#k10_funct_6 :::"commute"::: ) (Set (Var "F")) ")" ) ($#k1_funct_1 :::"."::: ) (Set (Var "s"))) ($#r2_hidden :::"in"::: ) (Set ($#k1_funct_2 :::"Funcs"::: ) "(" (Set (Var "I")) "," (Set "(" ($#k1_funct_2 :::"Funcs"::: ) "(" (Set "(" (Set "the" ($#u3_msualg_1 :::"Sorts"::: ) "of" (Set (Var "U1"))) ($#k1_funct_1 :::"."::: ) (Set (Var "s")) ")" ) "," (Set "(" ($#k3_tarski :::"union"::: ) "{" (Set "(" (Set "the" ($#u3_msualg_1 :::"Sorts"::: ) "of" (Set "(" (Set (Var "A")) ($#k5_pralg_2 :::"."::: ) (Set (Var "i9")) ")" )) ($#k1_funct_1 :::"."::: ) (Set (Var "s1")) ")" ) where i9 "is" ($#m1_subset_1 :::"Element"::: ) "of" (Set (Var "I")), s1 "is" ($#m1_subset_1 :::"SortSymbol":::) "of" (Set (Var "S")) : (Bool verum) "}" ")" ) ")" ")" ) ")" )))))))) ; theorem :: PRALG_3:27 (Bool "for" (Set (Var "I")) "being" ($#~v1_xboole_0 "non" ($#v1_xboole_0 :::"empty"::: ) ) ($#m1_hidden :::"set"::: ) (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" ($#m1_subset_1 :::"Element"::: ) "of" (Set (Var "I")) (Bool "for" (Set (Var "A")) "being" ($#m1_pralg_2 :::"MSAlgebra-Family"::: ) "of" (Set (Var "I")) "," (Set (Var "S")) (Bool "for" (Set (Var "s")) "being" ($#m1_subset_1 :::"SortSymbol":::) "of" (Set (Var "S")) (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_hidden :::"ManySortedFunction":::) "of" (Set (Var "I")) "st" (Bool (Bool "(" "for" (Set (Var "i")) "being" ($#m1_subset_1 :::"Element"::: ) "of" (Set (Var "I")) (Bool "ex" (Set (Var "F1")) "being" ($#m2_pboole :::"ManySortedFunction":::) "of" (Set (Var "U1")) "," (Set "(" (Set (Var "A")) ($#k5_pralg_2 :::"."::: ) (Set (Var "i")) ")" ) "st" (Bool "(" (Bool (Set (Var "F1")) ($#r1_hidden :::"="::: ) (Set (Set (Var "F")) ($#k1_funct_1 :::"."::: ) (Set (Var "i")))) & (Bool (Set (Var "F1")) ($#r1_msualg_3 :::"is_homomorphism"::: ) (Set (Var "U1")) "," (Set (Set (Var "A")) ($#k5_pralg_2 :::"."::: ) (Set (Var "i")))) ")" )) ")" )) "holds" (Bool "for" (Set (Var "F9")) "being" ($#m2_pboole :::"ManySortedFunction":::) "of" (Set (Var "U1")) "," (Set "(" (Set (Var "A")) ($#k5_pralg_2 :::"."::: ) (Set (Var "i")) ")" ) "st" (Bool (Bool (Set (Var "F9")) ($#r1_hidden :::"="::: ) (Set (Set (Var "F")) ($#k1_funct_1 :::"."::: ) (Set (Var "i"))))) "holds" (Bool "for" (Set (Var "x")) "being" ($#m1_hidden :::"set"::: ) "st" (Bool (Bool (Set (Var "x")) ($#r2_hidden :::"in"::: ) (Set (Set "the" ($#u3_msualg_1 :::"Sorts"::: ) "of" (Set (Var "U1"))) ($#k1_funct_1 :::"."::: ) (Set (Var "s"))))) "holds" (Bool "for" (Set (Var "f")) "being" ($#m1_hidden :::"Function":::) "st" (Bool (Bool (Set (Var "f")) ($#r1_hidden :::"="::: ) (Set (Set "(" ($#k10_funct_6 :::"commute"::: ) (Set "(" (Set "(" ($#k10_funct_6 :::"commute"::: ) (Set (Var "F")) ")" ) ($#k1_funct_1 :::"."::: ) (Set (Var "s")) ")" ) ")" ) ($#k1_funct_1 :::"."::: ) (Set (Var "x"))))) "holds" (Bool (Set (Set (Var "f")) ($#k1_funct_1 :::"."::: ) (Set (Var "i"))) ($#r1_hidden :::"="::: ) (Set (Set "(" (Set (Var "F9")) ($#k1_msualg_3 :::"."::: ) (Set (Var "s")) ")" ) ($#k1_funct_1 :::"."::: ) (Set (Var "x")))))))))))))) ; theorem :: PRALG_3:28 (Bool "for" (Set (Var "I")) "being" ($#~v1_xboole_0 "non" ($#v1_xboole_0 :::"empty"::: ) ) ($#m1_hidden :::"set"::: ) (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" ($#m1_pralg_2 :::"MSAlgebra-Family"::: ) "of" (Set (Var "I")) "," (Set (Var "S")) (Bool "for" (Set (Var "s")) "being" ($#m1_subset_1 :::"SortSymbol":::) "of" (Set (Var "S")) (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_hidden :::"ManySortedFunction":::) "of" (Set (Var "I")) "st" (Bool (Bool "(" "for" (Set (Var "i")) "being" ($#m1_subset_1 :::"Element"::: ) "of" (Set (Var "I")) (Bool "ex" (Set (Var "F1")) "being" ($#m2_pboole :::"ManySortedFunction":::) "of" (Set (Var "U1")) "," (Set "(" (Set (Var "A")) ($#k5_pralg_2 :::"."::: ) (Set (Var "i")) ")" ) "st" (Bool "(" (Bool (Set (Var "F1")) ($#r1_hidden :::"="::: ) (Set (Set (Var "F")) ($#k1_funct_1 :::"."::: ) (Set (Var "i")))) & (Bool (Set (Var "F1")) ($#r1_msualg_3 :::"is_homomorphism"::: ) (Set (Var "U1")) "," (Set (Set (Var "A")) ($#k5_pralg_2 :::"."::: ) (Set (Var "i")))) ")" )) ")" )) "holds" (Bool "for" (Set (Var "x")) "being" ($#m1_hidden :::"set"::: ) "st" (Bool (Bool (Set (Var "x")) ($#r2_hidden :::"in"::: ) (Set (Set "the" ($#u3_msualg_1 :::"Sorts"::: ) "of" (Set (Var "U1"))) ($#k1_funct_1 :::"."::: ) (Set (Var "s"))))) "holds" (Bool (Set (Set "(" ($#k10_funct_6 :::"commute"::: ) (Set "(" (Set "(" ($#k10_funct_6 :::"commute"::: ) (Set (Var "F")) ")" ) ($#k1_funct_1 :::"."::: ) (Set (Var "s")) ")" ) ")" ) ($#k1_funct_1 :::"."::: ) (Set (Var "x"))) ($#r2_hidden :::"in"::: ) (Set ($#k4_card_3 :::"product"::: ) (Set "(" ($#k9_pralg_2 :::"Carrier"::: ) "(" (Set (Var "A")) "," (Set (Var "s")) ")" ")" )))))))))) ; theorem :: PRALG_3:29 (Bool "for" (Set (Var "I")) "being" ($#~v1_xboole_0 "non" ($#v1_xboole_0 :::"empty"::: ) ) ($#m1_hidden :::"set"::: ) (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" ($#m1_pralg_2 :::"MSAlgebra-Family"::: ) "of" (Set (Var "I")) "," (Set (Var "S")) (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_hidden :::"ManySortedFunction":::) "of" (Set (Var "I")) "st" (Bool (Bool "(" "for" (Set (Var "i")) "being" ($#m1_subset_1 :::"Element"::: ) "of" (Set (Var "I")) (Bool "ex" (Set (Var "F1")) "being" ($#m2_pboole :::"ManySortedFunction":::) "of" (Set (Var "U1")) "," (Set "(" (Set (Var "A")) ($#k5_pralg_2 :::"."::: ) (Set (Var "i")) ")" ) "st" (Bool "(" (Bool (Set (Var "F1")) ($#r1_hidden :::"="::: ) (Set (Set (Var "F")) ($#k1_funct_1 :::"."::: ) (Set (Var "i")))) & (Bool (Set (Var "F1")) ($#r1_msualg_3 :::"is_homomorphism"::: ) (Set (Var "U1")) "," (Set (Set (Var "A")) ($#k5_pralg_2 :::"."::: ) (Set (Var "i")))) ")" )) ")" )) "holds" (Bool "ex" (Set (Var "H")) "being" ($#m2_pboole :::"ManySortedFunction":::) "of" (Set (Var "U1")) "," (Set "(" ($#k14_pralg_2 :::"product"::: ) (Set (Var "A")) ")" ) "st" (Bool "(" (Bool (Set (Var "H")) ($#r1_msualg_3 :::"is_homomorphism"::: ) (Set (Var "U1")) "," (Set ($#k14_pralg_2 :::"product"::: ) (Set (Var "A")))) & (Bool "(" "for" (Set (Var "i")) "being" ($#m1_subset_1 :::"Element"::: ) "of" (Set (Var "I")) "holds" (Bool (Set (Set "(" ($#k2_pralg_3 :::"proj"::: ) "(" (Set (Var "A")) "," (Set (Var "i")) ")" ")" ) ($#k3_msualg_3 :::"**"::: ) (Set (Var "H"))) ($#r1_hidden :::"="::: ) (Set (Set (Var "F")) ($#k1_funct_1 :::"."::: ) (Set (Var "i")))) ")" ) ")" ))))))) ; begin definitionlet "I" be ($#~v1_xboole_0 "non" ($#v1_xboole_0 :::"empty"::: ) ) ($#m1_hidden :::"set"::: ) ; let "J" be ($#m1_hidden :::"ManySortedSet":::) "of" (Set (Const "I")); let "S" be ($#~v2_struct_0 "non" ($#v2_struct_0 :::"empty"::: ) ) ($#~v11_struct_0 "non" ($#v11_struct_0 :::"void"::: ) ) ($#l1_msualg_1 :::"ManySortedSign"::: ) ; mode :::"MSAlgebra-Class"::: "of" "S" "," "J" -> ($#m1_hidden :::"ManySortedSet":::) "of" "I" means :: PRALG_3:def 3 (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"))) "is" ($#m1_pralg_2 :::"MSAlgebra-Family"::: ) "of" (Set "J" ($#k1_funct_1 :::"."::: ) (Set (Var "i"))) "," "S")); end; :: deftheorem defines :::"MSAlgebra-Class"::: PRALG_3:def 3 : (Bool "for" (Set (Var "I")) "being" ($#~v1_xboole_0 "non" ($#v1_xboole_0 :::"empty"::: ) ) ($#m1_hidden :::"set"::: ) (Bool "for" (Set (Var "J")) "being" ($#m1_hidden :::"ManySortedSet":::) "of" (Set (Var "I")) (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 "b4")) "being" ($#m1_hidden :::"ManySortedSet":::) "of" (Set (Var "I")) "holds" (Bool "(" (Bool (Set (Var "b4")) "is" ($#m1_pralg_3 :::"MSAlgebra-Class"::: ) "of" (Set (Var "S")) "," (Set (Var "J"))) "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 "b4")) ($#k1_funct_1 :::"."::: ) (Set (Var "i"))) "is" ($#m1_pralg_2 :::"MSAlgebra-Family"::: ) "of" (Set (Set (Var "J")) ($#k1_funct_1 :::"."::: ) (Set (Var "i"))) "," (Set (Var "S")))) ")" ))))); definitionlet "I" be ($#~v1_xboole_0 "non" ($#v1_xboole_0 :::"empty"::: ) ) ($#m1_hidden :::"set"::: ) ; let "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 ($#m1_pralg_2 :::"MSAlgebra-Family"::: ) "of" (Set (Const "I")) "," (Set (Const "S")); let "EqR" be ($#m1_subset_1 :::"Equivalence_Relation":::) "of" (Set (Const "I")); func "A" :::"/"::: "EqR" -> ($#m1_pralg_3 :::"MSAlgebra-Class"::: ) "of" "S" "," (Set ($#k6_partfun1 :::"id"::: ) (Set "(" ($#k8_eqrel_1 :::"Class"::: ) "EqR" ")" )) means :: PRALG_3:def 4 (Bool "for" (Set (Var "c")) "being" ($#m1_hidden :::"set"::: ) "st" (Bool (Bool (Set (Var "c")) ($#r2_hidden :::"in"::: ) (Set ($#k8_eqrel_1 :::"Class"::: ) "EqR"))) "holds" (Bool (Set it ($#k1_funct_1 :::"."::: ) (Set (Var "c"))) ($#r1_hidden :::"="::: ) (Set "A" ($#k5_relat_1 :::"|"::: ) (Set (Var "c"))))); end; :: deftheorem defines :::"/"::: PRALG_3:def 4 : (Bool "for" (Set (Var "I")) "being" ($#~v1_xboole_0 "non" ($#v1_xboole_0 :::"empty"::: ) ) ($#m1_hidden :::"set"::: ) (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" ($#m1_pralg_2 :::"MSAlgebra-Family"::: ) "of" (Set (Var "I")) "," (Set (Var "S")) (Bool "for" (Set (Var "EqR")) "being" ($#m1_subset_1 :::"Equivalence_Relation":::) "of" (Set (Var "I")) (Bool "for" (Set (Var "b5")) "being" ($#m1_pralg_3 :::"MSAlgebra-Class"::: ) "of" (Set (Var "S")) "," (Set ($#k6_partfun1 :::"id"::: ) (Set "(" ($#k8_eqrel_1 :::"Class"::: ) (Set (Var "EqR")) ")" )) "holds" (Bool "(" (Bool (Set (Var "b5")) ($#r1_hidden :::"="::: ) (Set (Set (Var "A")) ($#k3_pralg_3 :::"/"::: ) (Set (Var "EqR")))) "iff" (Bool "for" (Set (Var "c")) "being" ($#m1_hidden :::"set"::: ) "st" (Bool (Bool (Set (Var "c")) ($#r2_hidden :::"in"::: ) (Set ($#k8_eqrel_1 :::"Class"::: ) (Set (Var "EqR"))))) "holds" (Bool (Set (Set (Var "b5")) ($#k1_funct_1 :::"."::: ) (Set (Var "c"))) ($#r1_hidden :::"="::: ) (Set (Set (Var "A")) ($#k5_relat_1 :::"|"::: ) (Set (Var "c"))))) ")" )))))); definitionlet "I" be ($#~v1_xboole_0 "non" ($#v1_xboole_0 :::"empty"::: ) ) ($#m1_hidden :::"set"::: ) ; let "S" be ($#~v2_struct_0 "non" ($#v2_struct_0 :::"empty"::: ) ) ($#~v11_struct_0 "non" ($#v11_struct_0 :::"void"::: ) ) ($#l1_msualg_1 :::"ManySortedSign"::: ) ; let "J" be bbbadV2_RELAT_1() ($#m1_hidden :::"ManySortedSet":::) "of" (Set (Const "I")); let "C" be ($#m1_pralg_3 :::"MSAlgebra-Class"::: ) "of" (Set (Const "S")) "," (Set (Const "J")); func :::"product"::: "C" -> ($#m1_pralg_2 :::"MSAlgebra-Family"::: ) "of" "I" "," "S" means :: PRALG_3:def 5 (Bool "for" (Set (Var "i")) "being" ($#m1_subset_1 :::"Element"::: ) "of" "I" "st" (Bool (Bool (Set (Var "i")) ($#r2_hidden :::"in"::: ) "I")) "holds" (Bool "ex" (Set (Var "Ji")) "being" ($#~v1_xboole_0 "non" ($#v1_xboole_0 :::"empty"::: ) ) ($#m1_hidden :::"set"::: ) (Bool "ex" (Set (Var "Cs")) "being" ($#m1_pralg_2 :::"MSAlgebra-Family"::: ) "of" (Set (Var "Ji")) "," "S" "st" (Bool "(" (Bool (Set (Var "Ji")) ($#r1_hidden :::"="::: ) (Set "J" ($#k1_funct_1 :::"."::: ) (Set (Var "i")))) & (Bool (Set (Var "Cs")) ($#r1_hidden :::"="::: ) (Set "C" ($#k1_funct_1 :::"."::: ) (Set (Var "i")))) & (Bool (Set it ($#k5_pralg_2 :::"."::: ) (Set (Var "i"))) ($#r1_hidden :::"="::: ) (Set ($#k14_pralg_2 :::"product"::: ) (Set (Var "Cs")))) ")" )))); end; :: deftheorem defines :::"product"::: PRALG_3:def 5 : (Bool "for" (Set (Var "I")) "being" ($#~v1_xboole_0 "non" ($#v1_xboole_0 :::"empty"::: ) ) ($#m1_hidden :::"set"::: ) (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 "J")) "being" bbbadV2_RELAT_1() ($#m1_hidden :::"ManySortedSet":::) "of" (Set (Var "I")) (Bool "for" (Set (Var "C")) "being" ($#m1_pralg_3 :::"MSAlgebra-Class"::: ) "of" (Set (Var "S")) "," (Set (Var "J")) (Bool "for" (Set (Var "b5")) "being" ($#m1_pralg_2 :::"MSAlgebra-Family"::: ) "of" (Set (Var "I")) "," (Set (Var "S")) "holds" (Bool "(" (Bool (Set (Var "b5")) ($#r1_hidden :::"="::: ) (Set ($#k4_pralg_3 :::"product"::: ) (Set (Var "C")))) "iff" (Bool "for" (Set (Var "i")) "being" ($#m1_subset_1 :::"Element"::: ) "of" (Set (Var "I")) "st" (Bool (Bool (Set (Var "i")) ($#r2_hidden :::"in"::: ) (Set (Var "I")))) "holds" (Bool "ex" (Set (Var "Ji")) "being" ($#~v1_xboole_0 "non" ($#v1_xboole_0 :::"empty"::: ) ) ($#m1_hidden :::"set"::: ) (Bool "ex" (Set (Var "Cs")) "being" ($#m1_pralg_2 :::"MSAlgebra-Family"::: ) "of" (Set (Var "Ji")) "," (Set (Var "S")) "st" (Bool "(" (Bool (Set (Var "Ji")) ($#r1_hidden :::"="::: ) (Set (Set (Var "J")) ($#k1_funct_1 :::"."::: ) (Set (Var "i")))) & (Bool (Set (Var "Cs")) ($#r1_hidden :::"="::: ) (Set (Set (Var "C")) ($#k1_funct_1 :::"."::: ) (Set (Var "i")))) & (Bool (Set (Set (Var "b5")) ($#k5_pralg_2 :::"."::: ) (Set (Var "i"))) ($#r1_hidden :::"="::: ) (Set ($#k14_pralg_2 :::"product"::: ) (Set (Var "Cs")))) ")" )))) ")" )))))); theorem :: PRALG_3:30 (Bool "for" (Set (Var "I")) "being" ($#~v1_xboole_0 "non" ($#v1_xboole_0 :::"empty"::: ) ) ($#m1_hidden :::"set"::: ) (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" ($#m1_pralg_2 :::"MSAlgebra-Family"::: ) "of" (Set (Var "I")) "," (Set (Var "S")) (Bool "for" (Set (Var "EqR")) "being" ($#m1_subset_1 :::"Equivalence_Relation":::) "of" (Set (Var "I")) "holds" (Bool (Set ($#k14_pralg_2 :::"product"::: ) (Set (Var "A"))) "," (Set ($#k14_pralg_2 :::"product"::: ) (Set "(" ($#k4_pralg_3 :::"product"::: ) (Set "(" (Set (Var "A")) ($#k3_pralg_3 :::"/"::: ) (Set (Var "EqR")) ")" ) ")" )) ($#r6_msualg_3 :::"are_isomorphic"::: ) ))))) ;