:: PRALG_2  semantic presentation begin  









registrationlet "X" be   ($#v4_funct_1 :::"functional"::: )    ($#~v1_xboole_0  "non"   ($#v1_xboole_0 :::"empty"::: )   )    ($#v2_card_3 :::"with_common_domain"::: )     ($#m1_hidden :::"set"::: )  ; 
cluster   -> (Set   ($#k9_card_3 :::"DOM"::: )  "X")  ($#v4_relat_1 :::"-defined"::: )    for    ($#m1_subset_1 :::"Element"::: )   "of" "X"; 
end; registrationlet "X" be   ($#v4_funct_1 :::"functional"::: )    ($#~v1_xboole_0  "non"   ($#v1_xboole_0 :::"empty"::: )   )    ($#v2_card_3 :::"with_common_domain"::: )     ($#m1_hidden :::"set"::: )  ; 
cluster   ->   ($#v1_partfun1 :::"total"::: )    for    ($#m1_subset_1 :::"Element"::: )   "of" "X"; 
end; begin  definitionlet "F" be   ($#m1_hidden :::"Function":::); func  :::"Commute"::: "F" ->   ($#m1_hidden :::"Function":::) means :: PRALG_2:def 1 (Bool  "("  (Bool  "("   "for" (Set (Var "x")) "being"    ($#m1_hidden :::"set"::: )   "holds"   (Bool  "("  (Bool (Set (Var "x"))  ($#r2_hidden :::"in"::: )  (Set   ($#k9_xtuple_0 :::"dom"::: )  it)) "iff" (Bool  "ex" (Set (Var "f")) "being"   ($#m1_hidden :::"Function":::) "st"  (Bool  "("  (Bool (Set (Var "f"))  ($#r2_hidden :::"in"::: )  (Set   ($#k9_xtuple_0 :::"dom"::: )  "F")) & (Bool (Set (Var "x"))  ($#r1_hidden :::"="::: )  (Set   ($#k10_funct_6 :::"commute"::: )  (Set (Var "f"))))  ")" ))  ")" )  ")" ) & (Bool  "("   "for" (Set (Var "f")) "being"   ($#m1_hidden :::"Function":::)  "st" (Bool (Bool (Set (Var "f"))  ($#r2_hidden :::"in"::: )  (Set   ($#k9_xtuple_0 :::"dom"::: )  it))) "holds"  (Bool (Set it  ($#k1_funct_1 :::"."::: )  (Set (Var "f")))  ($#r1_hidden :::"="::: )  (Set "F"  ($#k1_funct_1 :::"."::: )  (Set  "("  ($#k10_funct_6 :::"commute"::: )  (Set (Var "f")) ")" )))  ")" )  ")" ); end; 





:: deftheorem    defines :::"Commute"::: PRALG_2:def 1 :  (Bool  "for" (Set (Var "F")) "," (Set (Var "b2")) "being"   ($#m1_hidden :::"Function":::) "holds"   (Bool  "("  (Bool (Set (Var "b2"))  ($#r1_hidden :::"="::: )  (Set   ($#k1_pralg_2 :::"Commute"::: )  (Set (Var "F")))) "iff" (Bool  "("  (Bool  "("   "for" (Set (Var "x")) "being"    ($#m1_hidden :::"set"::: )   "holds"   (Bool  "("  (Bool (Set (Var "x"))  ($#r2_hidden :::"in"::: )  (Set   ($#k9_xtuple_0 :::"dom"::: )  (Set (Var "b2")))) "iff" (Bool  "ex" (Set (Var "f")) "being"   ($#m1_hidden :::"Function":::) "st"  (Bool  "("  (Bool (Set (Var "f"))  ($#r2_hidden :::"in"::: )  (Set   ($#k9_xtuple_0 :::"dom"::: )  (Set (Var "F")))) & (Bool (Set (Var "x"))  ($#r1_hidden :::"="::: )  (Set   ($#k10_funct_6 :::"commute"::: )  (Set (Var "f"))))  ")" ))  ")" )  ")" ) & (Bool  "("   "for" (Set (Var "f")) "being"   ($#m1_hidden :::"Function":::)  "st" (Bool (Bool (Set (Var "f"))  ($#r2_hidden :::"in"::: )  (Set   ($#k9_xtuple_0 :::"dom"::: )  (Set (Var "b2"))))) "holds"  (Bool (Set (Set (Var "b2"))  ($#k1_funct_1 :::"."::: )  (Set (Var "f")))  ($#r1_hidden :::"="::: )  (Set (Set (Var "F"))  ($#k1_funct_1 :::"."::: )  (Set  "("  ($#k10_funct_6 :::"commute"::: )  (Set (Var "f")) ")" )))  ")" )  ")" )  ")" )); 
 
theorem :: PRALG_2:1 (Bool  "for" (Set (Var "F")) "being"   ($#m1_hidden :::"Function":::)  "st" (Bool (Bool (Set   ($#k9_xtuple_0 :::"dom"::: )  (Set (Var "F")))  ($#r1_hidden :::"="::: )  (Set  ($#k1_tarski :::"{"::: ) (Set  ($#k1_xboole_0 :::"{}"::: ) ) ($#k1_tarski :::"}"::: ) ))) "holds"  (Bool (Set   ($#k1_pralg_2 :::"Commute"::: )  (Set (Var "F")))  ($#r1_hidden :::"="::: )  (Set (Var "F")))) ; 
 definitionlet "f" be   ($#v1_funcop_1 :::"Function-yielding"::: )    ($#m1_hidden :::"Function":::); :: original: :::"Frege"::: redefine func  :::"Frege"::: "f" ->   ($#m1_hidden :::"ManySortedFunction":::) "of" (Set   ($#k4_card_3 :::"product"::: )  (Set  "("  ($#k2_funct_6 :::"doms"::: )  "f" ")" )) means :: PRALG_2:def 2 (Bool  "for" (Set (Var "g")) "being"   ($#m1_hidden :::"Function":::)  "st" (Bool (Bool (Set (Var "g"))  ($#r2_hidden :::"in"::: )  (Set   ($#k4_card_3 :::"product"::: )  (Set  "("  ($#k2_funct_6 :::"doms"::: )  "f" ")" )))) "holds"  (Bool (Set it  ($#k1_funct_1 :::"."::: )  (Set (Var "g")))  ($#r1_hidden :::"="::: )  (Set "f"  ($#k15_pralg_1 :::".."::: )  (Set (Var "g"))))); end; 





:: deftheorem    defines :::"Frege"::: PRALG_2:def 2 :  (Bool  "for" (Set (Var "f")) "being"   ($#v1_funcop_1 :::"Function-yielding"::: )    ($#m1_hidden :::"Function":::)  (Bool  "for" (Set (Var "b2")) "being"   ($#m1_hidden :::"ManySortedFunction":::) "of" (Set   ($#k4_card_3 :::"product"::: )  (Set  "("  ($#k2_funct_6 :::"doms"::: )  (Set (Var "f")) ")" )) "holds"   (Bool  "("  (Bool (Set (Var "b2"))  ($#r1_hidden :::"="::: )  (Set   ($#k2_pralg_2 :::"Frege"::: )  (Set (Var "f")))) "iff" (Bool  "for" (Set (Var "g")) "being"   ($#m1_hidden :::"Function":::)  "st" (Bool (Bool (Set (Var "g"))  ($#r2_hidden :::"in"::: )  (Set   ($#k4_card_3 :::"product"::: )  (Set  "("  ($#k2_funct_6 :::"doms"::: )  (Set (Var "f")) ")" )))) "holds"  (Bool (Set (Set (Var "b2"))  ($#k1_funct_1 :::"."::: )  (Set (Var "g")))  ($#r1_hidden :::"="::: )  (Set (Set (Var "f"))  ($#k15_pralg_1 :::".."::: )  (Set (Var "g")))))  ")" ))); 
 registrationlet "I" be    ($#m1_hidden :::"set"::: )  ; let "A", "B" be bbbadV2_RELAT_1()  ($#m1_hidden :::"ManySortedSet":::) "of" (Set (Const "I")); 
cluster (Set  ($#k6_pboole :::"[|"::: ) "A" "," "B" ($#k6_pboole :::"|]"::: ) ) -> bbbadV2_RELAT_1() ; 
end; 
theorem :: PRALG_2:2 (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 :::"set"::: )    (Bool  "for" (Set (Var "A")) "," (Set (Var "B")) "being"   ($#m1_hidden :::"ManySortedSet":::) "of" (Set (Var "I"))  (Bool  "for" (Set (Var "f")) "being"   ($#m1_subset_1 :::"Function":::) "of" (Set (Var "J")) "," (Set (Var "I")) "holds"  (Bool (Set (Set  ($#k6_pboole :::"[|"::: ) (Set (Var "A")) "," (Set (Var "B")) ($#k6_pboole :::"|]"::: ) )  ($#k3_relat_1 :::"*"::: )  (Set (Var "f")))  ($#r6_pboole :::"="::: )  (Set  ($#k6_pboole :::"[|"::: ) (Set  "(" (Set (Var "A"))  ($#k3_relat_1 :::"*"::: )  (Set (Var "f")) ")" ) "," (Set  "(" (Set (Var "B"))  ($#k3_relat_1 :::"*"::: )  (Set (Var "f")) ")" ) ($#k6_pboole :::"|]"::: ) )))))) ; 
 definitionlet "I" be  ($#~v1_xboole_0  "non"   ($#v1_xboole_0 :::"empty"::: )   )    ($#m1_hidden :::"set"::: )  ; let "A", "B" be bbbadV2_RELAT_1()  ($#m1_hidden :::"ManySortedSet":::) "of" (Set (Const "I")); let "pj" be    ($#m2_finseq_2 :::"Element"::: )   "of" (Set (Set (Const "I"))  ($#k3_finseq_2 :::"*"::: )  ); let "rj" be    ($#m1_subset_1 :::"Element"::: )   "of" (Set (Const "I")); let "f" be   ($#m1_subset_1 :::"Function":::) "of" (Set  "(" (Set  "(" (Set (Const "A"))  ($#k6_finseq_2 :::"#"::: )  ")" )  ($#k1_funct_1 :::"."::: )  (Set (Const "pj")) ")" ) "," (Set  "(" (Set (Const "A"))  ($#k1_funct_1 :::"."::: )  (Set (Const "rj")) ")" ); let "g" be   ($#m1_subset_1 :::"Function":::) "of" (Set  "(" (Set  "(" (Set (Const "B"))  ($#k6_finseq_2 :::"#"::: )  ")" )  ($#k1_funct_1 :::"."::: )  (Set (Const "pj")) ")" ) "," (Set  "(" (Set (Const "B"))  ($#k1_funct_1 :::"."::: )  (Set (Const "rj")) ")" ); func :::"[[:":::"f" "," "g":::":]]"::: ->   ($#m1_subset_1 :::"Function":::) "of" (Set  "(" (Set  "(" (Set  ($#k6_pboole :::"[|"::: ) "A" "," "B" ($#k6_pboole :::"|]"::: ) )  ($#k6_finseq_2 :::"#"::: )  ")" )  ($#k1_funct_1 :::"."::: )  "pj" ")" ) "," (Set  "(" (Set  ($#k6_pboole :::"[|"::: ) "A" "," "B" ($#k6_pboole :::"|]"::: ) )  ($#k1_funct_1 :::"."::: )  "rj" ")" ) means :: PRALG_2:def 3 (Bool  "for" (Set (Var "h")) "being"   ($#m1_hidden :::"Function":::)  "st" (Bool (Bool (Set (Var "h"))  ($#r2_hidden :::"in"::: )  (Set (Set  "(" (Set  ($#k6_pboole :::"[|"::: ) "A" "," "B" ($#k6_pboole :::"|]"::: ) )  ($#k6_finseq_2 :::"#"::: )  ")" )  ($#k1_funct_1 :::"."::: )  "pj"))) "holds"  (Bool (Set it  ($#k1_funct_1 :::"."::: )  (Set (Var "h")))  ($#r1_hidden :::"="::: )  (Set  ($#k4_tarski :::"["::: ) (Set  "(" "f"  ($#k1_funct_1 :::"."::: )  (Set  "("  ($#k11_mcart_1 :::"pr1"::: )  (Set (Var "h")) ")" ) ")" ) "," (Set  "(" "g"  ($#k1_funct_1 :::"."::: )  (Set  "("  ($#k12_mcart_1 :::"pr2"::: )  (Set (Var "h")) ")" ) ")" ) ($#k4_tarski :::"]"::: ) ))); end; 











:: deftheorem    defines :::"[[:"::: PRALG_2:def 3 :  (Bool  "for" (Set (Var "I")) "being"  ($#~v1_xboole_0  "non"   ($#v1_xboole_0 :::"empty"::: )   )    ($#m1_hidden :::"set"::: )    (Bool  "for" (Set (Var "A")) "," (Set (Var "B")) "being" bbbadV2_RELAT_1()  ($#m1_hidden :::"ManySortedSet":::) "of" (Set (Var "I"))  (Bool  "for" (Set (Var "pj")) "being"    ($#m2_finseq_2 :::"Element"::: )   "of" (Set (Set (Var "I"))  ($#k3_finseq_2 :::"*"::: )  )  (Bool  "for" (Set (Var "rj")) "being"    ($#m1_subset_1 :::"Element"::: )   "of" (Set (Var "I"))  (Bool  "for" (Set (Var "f")) "being"   ($#m1_subset_1 :::"Function":::) "of" (Set  "(" (Set  "(" (Set (Var "A"))  ($#k6_finseq_2 :::"#"::: )  ")" )  ($#k1_funct_1 :::"."::: )  (Set (Var "pj")) ")" ) "," (Set  "(" (Set (Var "A"))  ($#k1_funct_1 :::"."::: )  (Set (Var "rj")) ")" )  (Bool  "for" (Set (Var "g")) "being"   ($#m1_subset_1 :::"Function":::) "of" (Set  "(" (Set  "(" (Set (Var "B"))  ($#k6_finseq_2 :::"#"::: )  ")" )  ($#k1_funct_1 :::"."::: )  (Set (Var "pj")) ")" ) "," (Set  "(" (Set (Var "B"))  ($#k1_funct_1 :::"."::: )  (Set (Var "rj")) ")" )  (Bool  "for" (Set (Var "b8")) "being"   ($#m1_subset_1 :::"Function":::) "of" (Set  "(" (Set  "(" (Set  ($#k6_pboole :::"[|"::: ) (Set (Var "A")) "," (Set (Var "B")) ($#k6_pboole :::"|]"::: ) )  ($#k6_finseq_2 :::"#"::: )  ")" )  ($#k1_funct_1 :::"."::: )  (Set (Var "pj")) ")" ) "," (Set  "(" (Set  ($#k6_pboole :::"[|"::: ) (Set (Var "A")) "," (Set (Var "B")) ($#k6_pboole :::"|]"::: ) )  ($#k1_funct_1 :::"."::: )  (Set (Var "rj")) ")" ) "holds"   (Bool  "("  (Bool (Set (Var "b8"))  ($#r1_hidden :::"="::: )  (Set  ($#k3_pralg_2 :::"[[:"::: ) (Set (Var "f")) "," (Set (Var "g")) ($#k3_pralg_2 :::":]]"::: ) )) "iff" (Bool  "for" (Set (Var "h")) "being"   ($#m1_hidden :::"Function":::)  "st" (Bool (Bool (Set (Var "h"))  ($#r2_hidden :::"in"::: )  (Set (Set  "(" (Set  ($#k6_pboole :::"[|"::: ) (Set (Var "A")) "," (Set (Var "B")) ($#k6_pboole :::"|]"::: ) )  ($#k6_finseq_2 :::"#"::: )  ")" )  ($#k1_funct_1 :::"."::: )  (Set (Var "pj"))))) "holds"  (Bool (Set (Set (Var "b8"))  ($#k1_funct_1 :::"."::: )  (Set (Var "h")))  ($#r1_hidden :::"="::: )  (Set  ($#k4_tarski :::"["::: ) (Set  "(" (Set (Var "f"))  ($#k1_funct_1 :::"."::: )  (Set  "("  ($#k11_mcart_1 :::"pr1"::: )  (Set (Var "h")) ")" ) ")" ) "," (Set  "(" (Set (Var "g"))  ($#k1_funct_1 :::"."::: )  (Set  "("  ($#k12_mcart_1 :::"pr2"::: )  (Set (Var "h")) ")" ) ")" ) ($#k4_tarski :::"]"::: ) )))  ")" )))))))); 
 definitionlet "I" be  ($#~v1_xboole_0  "non"   ($#v1_xboole_0 :::"empty"::: )   )    ($#m1_hidden :::"set"::: )  ; let "J" be    ($#m1_hidden :::"set"::: )  ; let "A", "B" be bbbadV2_RELAT_1()  ($#m1_hidden :::"ManySortedSet":::) "of" (Set (Const "I")); let "p" be   ($#m1_subset_1 :::"Function":::) "of" (Set (Const "J")) "," (Set  "(" (Set (Const "I"))  ($#k3_finseq_2 :::"*"::: )  ")" ); let "r" be   ($#m1_subset_1 :::"Function":::) "of" (Set (Const "J")) "," (Set (Const "I")); let "F" be    ($#m2_pboole :::"ManySortedFunction"::: )   "of" (Set (Set  "(" (Set (Const "A"))  ($#k6_finseq_2 :::"#"::: )  ")" )  ($#k3_relat_1 :::"*"::: )  (Set (Const "p"))) "," (Set (Set (Const "A"))  ($#k3_relat_1 :::"*"::: )  (Set (Const "r"))); let "G" be    ($#m2_pboole :::"ManySortedFunction"::: )   "of" (Set (Set  "(" (Set (Const "B"))  ($#k6_finseq_2 :::"#"::: )  ")" )  ($#k3_relat_1 :::"*"::: )  (Set (Const "p"))) "," (Set (Set (Const "B"))  ($#k3_relat_1 :::"*"::: )  (Set (Const "r"))); func :::"[[:":::"F" "," "G":::":]]"::: ->    ($#m2_pboole :::"ManySortedFunction"::: )   "of" (Set (Set  "(" (Set  ($#k6_pboole :::"[|"::: ) "A" "," "B" ($#k6_pboole :::"|]"::: ) )  ($#k6_finseq_2 :::"#"::: )  ")" )  ($#k3_relat_1 :::"*"::: )  "p") "," (Set (Set  ($#k6_pboole :::"[|"::: ) "A" "," "B" ($#k6_pboole :::"|]"::: ) )  ($#k3_relat_1 :::"*"::: )  "r") means :: PRALG_2:def 4 (Bool  "for" (Set (Var "j")) "being"    ($#m1_hidden :::"set"::: )    "st" (Bool (Bool (Set (Var "j"))  ($#r2_hidden :::"in"::: )  "J")) "holds"  (Bool  "for" (Set (Var "pj")) "being"    ($#m2_finseq_2 :::"Element"::: )   "of" (Set "I"  ($#k3_finseq_2 :::"*"::: )  )  (Bool  "for" (Set (Var "rj")) "being"    ($#m1_subset_1 :::"Element"::: )   "of" "I"  "st" (Bool (Bool (Set (Var "pj"))  ($#r1_hidden :::"="::: )  (Set "p"  ($#k1_funct_1 :::"."::: )  (Set (Var "j")))) & (Bool (Set (Var "rj"))  ($#r1_hidden :::"="::: )  (Set "r"  ($#k1_funct_1 :::"."::: )  (Set (Var "j"))))) "holds"  (Bool  "for" (Set (Var "f")) "being"   ($#m1_subset_1 :::"Function":::) "of" (Set  "(" (Set  "(" "A"  ($#k6_finseq_2 :::"#"::: )  ")" )  ($#k1_funct_1 :::"."::: )  (Set (Var "pj")) ")" ) "," (Set  "(" "A"  ($#k1_funct_1 :::"."::: )  (Set (Var "rj")) ")" )  (Bool  "for" (Set (Var "g")) "being"   ($#m1_subset_1 :::"Function":::) "of" (Set  "(" (Set  "(" "B"  ($#k6_finseq_2 :::"#"::: )  ")" )  ($#k1_funct_1 :::"."::: )  (Set (Var "pj")) ")" ) "," (Set  "(" "B"  ($#k1_funct_1 :::"."::: )  (Set (Var "rj")) ")" )  "st" (Bool (Bool (Set (Var "f"))  ($#r1_hidden :::"="::: )  (Set "F"  ($#k1_funct_1 :::"."::: )  (Set (Var "j")))) & (Bool (Set (Var "g"))  ($#r1_hidden :::"="::: )  (Set "G"  ($#k1_funct_1 :::"."::: )  (Set (Var "j"))))) "holds"  (Bool (Set it  ($#k1_funct_1 :::"."::: )  (Set (Var "j")))  ($#r1_hidden :::"="::: )  (Set  ($#k3_pralg_2 :::"[[:"::: ) (Set (Var "f")) "," (Set (Var "g")) ($#k3_pralg_2 :::":]]"::: ) ))))))); end; 












:: deftheorem    defines :::"[[:"::: PRALG_2:def 4 :  (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 :::"set"::: )    (Bool  "for" (Set (Var "A")) "," (Set (Var "B")) "being" bbbadV2_RELAT_1()  ($#m1_hidden :::"ManySortedSet":::) "of" (Set (Var "I"))  (Bool  "for" (Set (Var "p")) "being"   ($#m1_subset_1 :::"Function":::) "of" (Set (Var "J")) "," (Set  "(" (Set (Var "I"))  ($#k3_finseq_2 :::"*"::: )  ")" )  (Bool  "for" (Set (Var "r")) "being"   ($#m1_subset_1 :::"Function":::) "of" (Set (Var "J")) "," (Set (Var "I"))  (Bool  "for" (Set (Var "F")) "being"    ($#m2_pboole :::"ManySortedFunction"::: )   "of" (Set (Set  "(" (Set (Var "A"))  ($#k6_finseq_2 :::"#"::: )  ")" )  ($#k3_relat_1 :::"*"::: )  (Set (Var "p"))) "," (Set (Set (Var "A"))  ($#k3_relat_1 :::"*"::: )  (Set (Var "r")))  (Bool  "for" (Set (Var "G")) "being"    ($#m2_pboole :::"ManySortedFunction"::: )   "of" (Set (Set  "(" (Set (Var "B"))  ($#k6_finseq_2 :::"#"::: )  ")" )  ($#k3_relat_1 :::"*"::: )  (Set (Var "p"))) "," (Set (Set (Var "B"))  ($#k3_relat_1 :::"*"::: )  (Set (Var "r")))  (Bool  "for" (Set (Var "b9")) "being"    ($#m2_pboole :::"ManySortedFunction"::: )   "of" (Set (Set  "(" (Set  ($#k6_pboole :::"[|"::: ) (Set (Var "A")) "," (Set (Var "B")) ($#k6_pboole :::"|]"::: ) )  ($#k6_finseq_2 :::"#"::: )  ")" )  ($#k3_relat_1 :::"*"::: )  (Set (Var "p"))) "," (Set (Set  ($#k6_pboole :::"[|"::: ) (Set (Var "A")) "," (Set (Var "B")) ($#k6_pboole :::"|]"::: ) )  ($#k3_relat_1 :::"*"::: )  (Set (Var "r"))) "holds"   (Bool  "("  (Bool (Set (Var "b9"))  ($#r1_hidden :::"="::: )  (Set  ($#k4_pralg_2 :::"[[:"::: ) (Set (Var "F")) "," (Set (Var "G")) ($#k4_pralg_2 :::":]]"::: ) )) "iff" (Bool  "for" (Set (Var "j")) "being"    ($#m1_hidden :::"set"::: )    "st" (Bool (Bool (Set (Var "j"))  ($#r2_hidden :::"in"::: )  (Set (Var "J")))) "holds"  (Bool  "for" (Set (Var "pj")) "being"    ($#m2_finseq_2 :::"Element"::: )   "of" (Set (Set (Var "I"))  ($#k3_finseq_2 :::"*"::: )  )  (Bool  "for" (Set (Var "rj")) "being"    ($#m1_subset_1 :::"Element"::: )   "of" (Set (Var "I"))  "st" (Bool (Bool (Set (Var "pj"))  ($#r1_hidden :::"="::: )  (Set (Set (Var "p"))  ($#k1_funct_1 :::"."::: )  (Set (Var "j")))) & (Bool (Set (Var "rj"))  ($#r1_hidden :::"="::: )  (Set (Set (Var "r"))  ($#k1_funct_1 :::"."::: )  (Set (Var "j"))))) "holds"  (Bool  "for" (Set (Var "f")) "being"   ($#m1_subset_1 :::"Function":::) "of" (Set  "(" (Set  "(" (Set (Var "A"))  ($#k6_finseq_2 :::"#"::: )  ")" )  ($#k1_funct_1 :::"."::: )  (Set (Var "pj")) ")" ) "," (Set  "(" (Set (Var "A"))  ($#k1_funct_1 :::"."::: )  (Set (Var "rj")) ")" )  (Bool  "for" (Set (Var "g")) "being"   ($#m1_subset_1 :::"Function":::) "of" (Set  "(" (Set  "(" (Set (Var "B"))  ($#k6_finseq_2 :::"#"::: )  ")" )  ($#k1_funct_1 :::"."::: )  (Set (Var "pj")) ")" ) "," (Set  "(" (Set (Var "B"))  ($#k1_funct_1 :::"."::: )  (Set (Var "rj")) ")" )  "st" (Bool (Bool (Set (Var "f"))  ($#r1_hidden :::"="::: )  (Set (Set (Var "F"))  ($#k1_funct_1 :::"."::: )  (Set (Var "j")))) & (Bool (Set (Var "g"))  ($#r1_hidden :::"="::: )  (Set (Set (Var "G"))  ($#k1_funct_1 :::"."::: )  (Set (Var "j"))))) "holds"  (Bool (Set (Set (Var "b9"))  ($#k1_funct_1 :::"."::: )  (Set (Var "j")))  ($#r1_hidden :::"="::: )  (Set  ($#k3_pralg_2 :::"[[:"::: ) (Set (Var "f")) "," (Set (Var "g")) ($#k3_pralg_2 :::":]]"::: ) )))))))  ")" ))))))))); 
 begin  definitionlet "I" be    ($#m1_hidden :::"set"::: )  ; let "S" be  ($#~v2_struct_0  "non"   ($#v2_struct_0 :::"empty"::: )   )    ($#l1_msualg_1 :::"ManySortedSign"::: )  ; mode  :::"MSAlgebra-Family":::  "of" "I" "," "S" ->   ($#m1_hidden :::"ManySortedSet":::) "of" "I" means :: PRALG_2:def 5 (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"   ($#v4_msualg_1 :::"non-empty"::: )     ($#l3_msualg_1 :::"MSAlgebra"::: )   "over" "S")); end; 






:: deftheorem    defines :::"MSAlgebra-Family"::: PRALG_2:def 5 :  (Bool  "for" (Set (Var "I")) "being"    ($#m1_hidden :::"set"::: )    (Bool  "for" (Set (Var "S")) "being"  ($#~v2_struct_0  "non"   ($#v2_struct_0 :::"empty"::: )   )    ($#l1_msualg_1 :::"ManySortedSign"::: )    (Bool  "for" (Set (Var "b3")) "being"   ($#m1_hidden :::"ManySortedSet":::) "of" (Set (Var "I")) "holds"   (Bool  "("  (Bool (Set (Var "b3")) "is"    ($#m1_pralg_2 :::"MSAlgebra-Family"::: )   "of" (Set (Var "I")) "," (Set (Var "S"))) "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 "b3"))  ($#k1_funct_1 :::"."::: )  (Set (Var "i"))) "is"   ($#v4_msualg_1 :::"non-empty"::: )     ($#l3_msualg_1 :::"MSAlgebra"::: )   "over" (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"::: )   )    ($#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")); :: original: :::"."::: redefine func "A" :::"."::: "i" ->   ($#v4_msualg_1 :::"non-empty"::: )     ($#l3_msualg_1 :::"MSAlgebra"::: )   "over" "S"; end; definitionlet "S" be  ($#~v2_struct_0  "non"   ($#v2_struct_0 :::"empty"::: )   )    ($#l1_msualg_1 :::"ManySortedSign"::: )  ; let "U1" be    ($#l3_msualg_1 :::"MSAlgebra"::: )   "over" (Set (Const "S")); func :::"|.":::"U1":::".|"::: ->    ($#m1_hidden :::"set"::: )   equals :: PRALG_2:def 6 (Set   ($#k3_tarski :::"union"::: )  (Set  "("  ($#k10_xtuple_0 :::"rng"::: )  (Set  "the"  ($#u3_msualg_1 :::"Sorts"::: )  "of" "U1") ")" )); end; 






:: deftheorem    defines :::"|."::: PRALG_2:def 6 :  (Bool  "for" (Set (Var "S")) "being"  ($#~v2_struct_0  "non"   ($#v2_struct_0 :::"empty"::: )   )    ($#l1_msualg_1 :::"ManySortedSign"::: )    (Bool  "for" (Set (Var "U1")) "being"    ($#l3_msualg_1 :::"MSAlgebra"::: )   "over" (Set (Var "S")) "holds"  (Bool (Set  ($#k6_pralg_2 :::"|."::: ) (Set (Var "U1")) ($#k6_pralg_2 :::".|"::: ) )  ($#r1_hidden :::"="::: )  (Set   ($#k3_tarski :::"union"::: )  (Set  "("  ($#k10_xtuple_0 :::"rng"::: )  (Set  "the"  ($#u3_msualg_1 :::"Sorts"::: )  "of" (Set (Var "U1"))) ")" ))))); 
 registrationlet "S" be  ($#~v2_struct_0  "non"   ($#v2_struct_0 :::"empty"::: )   )    ($#l1_msualg_1 :::"ManySortedSign"::: )  ; let "U1" be   ($#v4_msualg_1 :::"non-empty"::: )     ($#l3_msualg_1 :::"MSAlgebra"::: )   "over" (Set (Const "S")); 
cluster (Set  ($#k6_pralg_2 :::"|."::: ) "U1" ($#k6_pralg_2 :::".|"::: ) ) ->  ($#~v1_xboole_0  "non"   ($#v1_xboole_0 :::"empty"::: )   )  ; 
end; 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"::: )   )    ($#l1_msualg_1 :::"ManySortedSign"::: )  ; let "A" be    ($#m1_pralg_2 :::"MSAlgebra-Family"::: )   "of" (Set (Const "I")) "," (Set (Const "S")); func :::"|.":::"A":::".|"::: ->    ($#m1_hidden :::"set"::: )   equals :: PRALG_2:def 7 (Set   ($#k3_tarski :::"union"::: )   "{"  (Set  ($#k6_pralg_2 :::"|."::: ) (Set  "(" "A"  ($#k5_pralg_2 :::"."::: )  (Set (Var "i")) ")" ) ($#k6_pralg_2 :::".|"::: ) ) where i "is"    ($#m1_subset_1 :::"Element"::: )   "of" "I" : (Bool verum)  "}"  ); end; 







:: deftheorem    defines :::"|."::: PRALG_2:def 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"::: )   )    ($#l1_msualg_1 :::"ManySortedSign"::: )    (Bool  "for" (Set (Var "A")) "being"    ($#m1_pralg_2 :::"MSAlgebra-Family"::: )   "of" (Set (Var "I")) "," (Set (Var "S")) "holds"  (Bool (Set  ($#k7_pralg_2 :::"|."::: ) (Set (Var "A")) ($#k7_pralg_2 :::".|"::: ) )  ($#r1_hidden :::"="::: )  (Set   ($#k3_tarski :::"union"::: )   "{"  (Set  ($#k6_pralg_2 :::"|."::: ) (Set  "(" (Set (Var "A"))  ($#k5_pralg_2 :::"."::: )  (Set (Var "i")) ")" ) ($#k6_pralg_2 :::".|"::: ) ) where i "is"    ($#m1_subset_1 :::"Element"::: )   "of" (Set (Var "I")) : (Bool verum)  "}"  ))))); 
 registrationlet "I" be  ($#~v1_xboole_0  "non"   ($#v1_xboole_0 :::"empty"::: )   )    ($#m1_hidden :::"set"::: )  ; let "S" be  ($#~v2_struct_0  "non"   ($#v2_struct_0 :::"empty"::: )   )    ($#l1_msualg_1 :::"ManySortedSign"::: )  ; let "A" be    ($#m1_pralg_2 :::"MSAlgebra-Family"::: )   "of" (Set (Const "I")) "," (Set (Const "S")); 
cluster (Set  ($#k7_pralg_2 :::"|."::: ) "A" ($#k7_pralg_2 :::".|"::: ) ) ->  ($#~v1_xboole_0  "non"   ($#v1_xboole_0 :::"empty"::: )   )  ; 
end; begin  
theorem :: PRALG_2:3 (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  "("  (Bool (Set   ($#k3_msualg_1 :::"Args"::: )   "(" (Set (Var "o")) "," (Set (Var "U0")) ")" )  ($#r1_hidden :::"="::: )  (Set   ($#k4_card_3 :::"product"::: )  (Set  "(" (Set  "the"  ($#u3_msualg_1 :::"Sorts"::: )  "of" (Set (Var "U0")))  ($#k3_relat_1 :::"*"::: )  (Set  "("  ($#k1_msualg_1 :::"the_arity_of"::: )  (Set (Var "o")) ")" ) ")" ))) & (Bool (Set   ($#k9_xtuple_0 :::"dom"::: )  (Set  "(" (Set  "the"  ($#u3_msualg_1 :::"Sorts"::: )  "of" (Set (Var "U0")))  ($#k3_relat_1 :::"*"::: )  (Set  "("  ($#k1_msualg_1 :::"the_arity_of"::: )  (Set (Var "o")) ")" ) ")" ))  ($#r1_hidden :::"="::: )  (Set   ($#k9_xtuple_0 :::"dom"::: )  (Set  "("  ($#k1_msualg_1 :::"the_arity_of"::: )  (Set (Var "o")) ")" ))) & (Bool (Set   ($#k4_msualg_1 :::"Result"::: )   "(" (Set (Var "o")) "," (Set (Var "U0")) ")" )  ($#r1_hidden :::"="::: )  (Set (Set  "the"  ($#u3_msualg_1 :::"Sorts"::: )  "of" (Set (Var "U0")))  ($#k1_funct_1 :::"."::: )  (Set  "("  ($#k2_msualg_1 :::"the_result_sort_of"::: )  (Set (Var "o")) ")" )))  ")" )))) ; 
 
theorem :: PRALG_2:4 (Bool  "for" (Set (Var "S")) "being"  ($#~v2_struct_0  "non"   ($#v2_struct_0 :::"empty"::: )   )   ($#~v11_struct_0  "non"   ($#v11_struct_0 :::"void"::: )   )    ($#l1_msualg_1 :::"ManySortedSign"::: )    (Bool  "for" (Set (Var "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 :::"{}"::: )  ))) "holds"  (Bool (Set   ($#k3_msualg_1 :::"Args"::: )   "(" (Set (Var "o")) "," (Set (Var "U0")) ")" )  ($#r1_hidden :::"="::: )  (Set  ($#k1_tarski :::"{"::: ) (Set  ($#k1_xboole_0 :::"{}"::: ) ) ($#k1_tarski :::"}"::: ) ))))) ; 
 definitionlet "S" be  ($#~v2_struct_0  "non"   ($#v2_struct_0 :::"empty"::: )   )    ($#l1_msualg_1 :::"ManySortedSign"::: )  ; let "U1", "U2" be   ($#v4_msualg_1 :::"non-empty"::: )     ($#l3_msualg_1 :::"MSAlgebra"::: )   "over" (Set (Const "S")); func :::"[:":::"U1" "," "U2":::":]"::: ->    ($#l3_msualg_1 :::"MSAlgebra"::: )   "over" "S" equals :: PRALG_2:def 8 (Set   ($#g3_msualg_1 :::"MSAlgebra"::: )  "(#"  (Set  ($#k6_pboole :::"[|"::: ) (Set  "the"  ($#u3_msualg_1 :::"Sorts"::: )  "of" "U1") "," (Set  "the"  ($#u3_msualg_1 :::"Sorts"::: )  "of" "U2") ($#k6_pboole :::"|]"::: ) ) "," (Set  ($#k4_pralg_2 :::"[[:"::: ) (Set  "the"  ($#u4_msualg_1 :::"Charact"::: )  "of" "U1") "," (Set  "the"  ($#u4_msualg_1 :::"Charact"::: )  "of" "U2") ($#k4_pralg_2 :::":]]"::: ) ) "#)" ); end; 







:: deftheorem    defines :::"[:"::: PRALG_2:def 8 :  (Bool  "for" (Set (Var "S")) "being"  ($#~v2_struct_0  "non"   ($#v2_struct_0 :::"empty"::: )   )    ($#l1_msualg_1 :::"ManySortedSign"::: )    (Bool  "for" (Set (Var "U1")) "," (Set (Var "U2")) "being"   ($#v4_msualg_1 :::"non-empty"::: )     ($#l3_msualg_1 :::"MSAlgebra"::: )   "over" (Set (Var "S")) "holds"  (Bool (Set  ($#k8_pralg_2 :::"[:"::: ) (Set (Var "U1")) "," (Set (Var "U2")) ($#k8_pralg_2 :::":]"::: ) )  ($#r1_hidden :::"="::: )  (Set   ($#g3_msualg_1 :::"MSAlgebra"::: )  "(#"  (Set  ($#k6_pboole :::"[|"::: ) (Set  "the"  ($#u3_msualg_1 :::"Sorts"::: )  "of" (Set (Var "U1"))) "," (Set  "the"  ($#u3_msualg_1 :::"Sorts"::: )  "of" (Set (Var "U2"))) ($#k6_pboole :::"|]"::: ) ) "," (Set  ($#k4_pralg_2 :::"[[:"::: ) (Set  "the"  ($#u4_msualg_1 :::"Charact"::: )  "of" (Set (Var "U1"))) "," (Set  "the"  ($#u4_msualg_1 :::"Charact"::: )  "of" (Set (Var "U2"))) ($#k4_pralg_2 :::":]]"::: ) ) "#)" )))); 
 registrationlet "S" be  ($#~v2_struct_0  "non"   ($#v2_struct_0 :::"empty"::: )   )    ($#l1_msualg_1 :::"ManySortedSign"::: )  ; let "U1", "U2" be   ($#v4_msualg_1 :::"non-empty"::: )     ($#l3_msualg_1 :::"MSAlgebra"::: )   "over" (Set (Const "S")); 
cluster (Set  ($#k8_pralg_2 :::"[:"::: ) "U1" "," "U2" ($#k8_pralg_2 :::":]"::: ) ) ->   ($#v3_msualg_1 :::"strict"::: )   ; 
end; definitionlet "I" be    ($#m1_hidden :::"set"::: )  ; let "S" be  ($#~v2_struct_0  "non"   ($#v2_struct_0 :::"empty"::: )   )    ($#l1_msualg_1 :::"ManySortedSign"::: )  ; let "s" be   ($#m1_subset_1 :::"SortSymbol":::) "of" (Set (Const "S")); let "A" be    ($#m1_pralg_2 :::"MSAlgebra-Family"::: )   "of" (Set (Const "I")) "," (Set (Const "S")); func  :::"Carrier":::  "(" "A" "," "s" ")"  ->   ($#m1_hidden :::"ManySortedSet":::) "of" "I" means :: PRALG_2:def 9 (Bool  "for" (Set (Var "i")) "being"    ($#m1_hidden :::"set"::: )    "st" (Bool (Bool (Set (Var "i"))  ($#r2_hidden :::"in"::: )  "I")) "holds"  (Bool  "ex" (Set (Var "U0")) "being"    ($#l3_msualg_1 :::"MSAlgebra"::: )   "over" "S" "st"  (Bool  "("  (Bool (Set (Var "U0"))  ($#r1_hidden :::"="::: )  (Set "A"  ($#k1_funct_1 :::"."::: )  (Set (Var "i")))) & (Bool (Set it  ($#k1_funct_1 :::"."::: )  (Set (Var "i")))  ($#r1_hidden :::"="::: )  (Set (Set  "the"  ($#u3_msualg_1 :::"Sorts"::: )  "of" (Set (Var "U0")))  ($#k1_funct_1 :::"."::: )  "s"))  ")" ))) if (Bool "I"  ($#r1_hidden :::"<>"::: )  (Set   ($#k1_xboole_0 :::"{}"::: )  ))  otherwise (Bool it  ($#r1_hidden :::"="::: )  (Set   ($#k1_xboole_0 :::"{}"::: )  )); end; 








:: deftheorem    defines :::"Carrier"::: PRALG_2:def 9 :  (Bool  "for" (Set (Var "I")) "being"    ($#m1_hidden :::"set"::: )    (Bool  "for" (Set (Var "S")) "being"  ($#~v2_struct_0  "non"   ($#v2_struct_0 :::"empty"::: )   )    ($#l1_msualg_1 :::"ManySortedSign"::: )    (Bool  "for" (Set (Var "s")) "being"   ($#m1_subset_1 :::"SortSymbol":::) "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 "b5")) "being"   ($#m1_hidden :::"ManySortedSet":::) "of" (Set (Var "I")) "holds"   (Bool  "("   "("  (Bool (Bool (Set (Var "I"))  ($#r1_hidden :::"<>"::: )  (Set   ($#k1_xboole_0 :::"{}"::: )  ))) "implies" (Bool  "("  (Bool (Set (Var "b5"))  ($#r1_hidden :::"="::: )  (Set   ($#k9_pralg_2 :::"Carrier"::: )   "(" (Set (Var "A")) "," (Set (Var "s")) ")" )) "iff" (Bool  "for" (Set (Var "i")) "being"    ($#m1_hidden :::"set"::: )    "st" (Bool (Bool (Set (Var "i"))  ($#r2_hidden :::"in"::: )  (Set (Var "I")))) "holds"  (Bool  "ex" (Set (Var "U0")) "being"    ($#l3_msualg_1 :::"MSAlgebra"::: )   "over" (Set (Var "S")) "st"  (Bool  "("  (Bool (Set (Var "U0"))  ($#r1_hidden :::"="::: )  (Set (Set (Var "A"))  ($#k1_funct_1 :::"."::: )  (Set (Var "i")))) & (Bool (Set (Set (Var "b5"))  ($#k1_funct_1 :::"."::: )  (Set (Var "i")))  ($#r1_hidden :::"="::: )  (Set (Set  "the"  ($#u3_msualg_1 :::"Sorts"::: )  "of" (Set (Var "U0")))  ($#k1_funct_1 :::"."::: )  (Set (Var "s"))))  ")" )))  ")" )  ")"  &  "("  (Bool (Bool (Bool  "not" (Set (Var "I"))  ($#r1_hidden :::"<>"::: )  (Set   ($#k1_xboole_0 :::"{}"::: )  )))) "implies" (Bool  "("  (Bool (Set (Var "b5"))  ($#r1_hidden :::"="::: )  (Set   ($#k9_pralg_2 :::"Carrier"::: )   "(" (Set (Var "A")) "," (Set (Var "s")) ")" )) "iff" (Bool (Set (Var "b5"))  ($#r1_hidden :::"="::: )  (Set   ($#k1_xboole_0 :::"{}"::: )  ))  ")" )  ")"   ")" )))))); 
 registrationlet "I" be    ($#m1_hidden :::"set"::: )  ; let "S" be  ($#~v2_struct_0  "non"   ($#v2_struct_0 :::"empty"::: )   )    ($#l1_msualg_1 :::"ManySortedSign"::: )  ; let "s" be   ($#m1_subset_1 :::"SortSymbol":::) "of" (Set (Const "S")); let "A" be    ($#m1_pralg_2 :::"MSAlgebra-Family"::: )   "of" (Set (Const "I")) "," (Set (Const "S")); 
cluster (Set   ($#k9_pralg_2 :::"Carrier"::: )   "(" "A" "," "s" ")" ) -> bbbadV2_RELAT_1() ; 
end; definitionlet "I" be    ($#m1_hidden :::"set"::: )  ; let "S" be  ($#~v2_struct_0  "non"   ($#v2_struct_0 :::"empty"::: )   )    ($#l1_msualg_1 :::"ManySortedSign"::: )  ; let "A" be    ($#m1_pralg_2 :::"MSAlgebra-Family"::: )   "of" (Set (Const "I")) "," (Set (Const "S")); func  :::"SORTS"::: "A" ->   ($#m1_hidden :::"ManySortedSet":::) "of" (Set  "the"  ($#u1_struct_0 :::"carrier"::: )  "of" "S") means :: PRALG_2:def 10 (Bool  "for" (Set (Var "s")) "being"   ($#m1_subset_1 :::"SortSymbol":::) "of" "S" "holds"  (Bool (Set it  ($#k1_funct_1 :::"."::: )  (Set (Var "s")))  ($#r1_hidden :::"="::: )  (Set   ($#k4_card_3 :::"product"::: )  (Set  "("  ($#k9_pralg_2 :::"Carrier"::: )   "(" "A" "," (Set (Var "s")) ")"  ")" )))); end; 







:: deftheorem    defines :::"SORTS"::: PRALG_2:def 10 :  (Bool  "for" (Set (Var "I")) "being"    ($#m1_hidden :::"set"::: )    (Bool  "for" (Set (Var "S")) "being"  ($#~v2_struct_0  "non"   ($#v2_struct_0 :::"empty"::: )   )    ($#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 "b4")) "being"   ($#m1_hidden :::"ManySortedSet":::) "of" (Set  "the"  ($#u1_struct_0 :::"carrier"::: )  "of" (Set (Var "S"))) "holds"   (Bool  "("  (Bool (Set (Var "b4"))  ($#r1_hidden :::"="::: )  (Set   ($#k10_pralg_2 :::"SORTS"::: )  (Set (Var "A")))) "iff" (Bool  "for" (Set (Var "s")) "being"   ($#m1_subset_1 :::"SortSymbol":::) "of" (Set (Var "S")) "holds"  (Bool (Set (Set (Var "b4"))  ($#k1_funct_1 :::"."::: )  (Set (Var "s")))  ($#r1_hidden :::"="::: )  (Set   ($#k4_card_3 :::"product"::: )  (Set  "("  ($#k9_pralg_2 :::"Carrier"::: )   "(" (Set (Var "A")) "," (Set (Var "s")) ")"  ")" ))))  ")" ))))); 
 registrationlet "I" be    ($#m1_hidden :::"set"::: )  ; let "S" be  ($#~v2_struct_0  "non"   ($#v2_struct_0 :::"empty"::: )   )    ($#l1_msualg_1 :::"ManySortedSign"::: )  ; let "A" be    ($#m1_pralg_2 :::"MSAlgebra-Family"::: )   "of" (Set (Const "I")) "," (Set (Const "S")); 
cluster (Set   ($#k10_pralg_2 :::"SORTS"::: )  "A") -> bbbadV2_RELAT_1() ; 
end; definitionlet "I" be    ($#m1_hidden :::"set"::: )  ; let "S" be  ($#~v2_struct_0  "non"   ($#v2_struct_0 :::"empty"::: )   )    ($#l1_msualg_1 :::"ManySortedSign"::: )  ; let "A" be    ($#m1_pralg_2 :::"MSAlgebra-Family"::: )   "of" (Set (Const "I")) "," (Set (Const "S")); func  :::"OPER"::: "A" ->   ($#m1_hidden :::"ManySortedFunction":::) "of" "I" means :: PRALG_2:def 11 (Bool  "for" (Set (Var "i")) "being"    ($#m1_hidden :::"set"::: )    "st" (Bool (Bool (Set (Var "i"))  ($#r2_hidden :::"in"::: )  "I")) "holds"  (Bool  "ex" (Set (Var "U0")) "being"    ($#l3_msualg_1 :::"MSAlgebra"::: )   "over" "S" "st"  (Bool  "("  (Bool (Set (Var "U0"))  ($#r1_hidden :::"="::: )  (Set "A"  ($#k1_funct_1 :::"."::: )  (Set (Var "i")))) & (Bool (Set it  ($#k1_funct_1 :::"."::: )  (Set (Var "i")))  ($#r1_hidden :::"="::: )  (Set  "the"  ($#u4_msualg_1 :::"Charact"::: )  "of" (Set (Var "U0"))))  ")" ))) if (Bool "I"  ($#r1_hidden :::"<>"::: )  (Set   ($#k1_xboole_0 :::"{}"::: )  ))  otherwise (Bool it  ($#r1_hidden :::"="::: )  (Set   ($#k1_xboole_0 :::"{}"::: )  )); end; 







:: deftheorem    defines :::"OPER"::: PRALG_2:def 11 :  (Bool  "for" (Set (Var "I")) "being"    ($#m1_hidden :::"set"::: )    (Bool  "for" (Set (Var "S")) "being"  ($#~v2_struct_0  "non"   ($#v2_struct_0 :::"empty"::: )   )    ($#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 "b4")) "being"   ($#m1_hidden :::"ManySortedFunction":::) "of" (Set (Var "I")) "holds"   (Bool  "("   "("  (Bool (Bool (Set (Var "I"))  ($#r1_hidden :::"<>"::: )  (Set   ($#k1_xboole_0 :::"{}"::: )  ))) "implies" (Bool  "("  (Bool (Set (Var "b4"))  ($#r1_hidden :::"="::: )  (Set   ($#k11_pralg_2 :::"OPER"::: )  (Set (Var "A")))) "iff" (Bool  "for" (Set (Var "i")) "being"    ($#m1_hidden :::"set"::: )    "st" (Bool (Bool (Set (Var "i"))  ($#r2_hidden :::"in"::: )  (Set (Var "I")))) "holds"  (Bool  "ex" (Set (Var "U0")) "being"    ($#l3_msualg_1 :::"MSAlgebra"::: )   "over" (Set (Var "S")) "st"  (Bool  "("  (Bool (Set (Var "U0"))  ($#r1_hidden :::"="::: )  (Set (Set (Var "A"))  ($#k1_funct_1 :::"."::: )  (Set (Var "i")))) & (Bool (Set (Set (Var "b4"))  ($#k1_funct_1 :::"."::: )  (Set (Var "i")))  ($#r1_hidden :::"="::: )  (Set  "the"  ($#u4_msualg_1 :::"Charact"::: )  "of" (Set (Var "U0"))))  ")" )))  ")" )  ")"  &  "("  (Bool (Bool (Bool  "not" (Set (Var "I"))  ($#r1_hidden :::"<>"::: )  (Set   ($#k1_xboole_0 :::"{}"::: )  )))) "implies" (Bool  "("  (Bool (Set (Var "b4"))  ($#r1_hidden :::"="::: )  (Set   ($#k11_pralg_2 :::"OPER"::: )  (Set (Var "A")))) "iff" (Bool (Set (Var "b4"))  ($#r1_hidden :::"="::: )  (Set   ($#k1_xboole_0 :::"{}"::: )  ))  ")" )  ")"   ")" ))))); 
 
theorem :: PRALG_2:5 (Bool  "for" (Set (Var "I")) "being"    ($#m1_hidden :::"set"::: )    (Bool  "for" (Set (Var "S")) "being"  ($#~v2_struct_0  "non"   ($#v2_struct_0 :::"empty"::: )   )    ($#l1_msualg_1 :::"ManySortedSign"::: )    (Bool  "for" (Set (Var "A")) "being"    ($#m1_pralg_2 :::"MSAlgebra-Family"::: )   "of" (Set (Var "I")) "," (Set (Var "S")) "holds"  (Bool (Set   ($#k9_xtuple_0 :::"dom"::: )  (Set  "("  ($#k2_funct_5 :::"uncurry"::: )  (Set  "("  ($#k11_pralg_2 :::"OPER"::: )  (Set (Var "A")) ")" ) ")" ))  ($#r1_hidden :::"="::: )  (Set  ($#k2_zfmisc_1 :::"[:"::: ) (Set (Var "I")) "," (Set  "the"  ($#u4_struct_0 :::"carrier'"::: )  "of" (Set (Var "S"))) ($#k2_zfmisc_1 :::":]"::: ) ))))) ; 
 
theorem :: PRALG_2:6 (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")) "holds"  (Bool (Set   ($#k10_funct_6 :::"commute"::: )  (Set  "("  ($#k11_pralg_2 :::"OPER"::: )  (Set (Var "A")) ")" ))  ($#r2_hidden :::"in"::: )  (Set   ($#k1_funct_2 :::"Funcs"::: )   "(" (Set  "the"  ($#u4_struct_0 :::"carrier'"::: )  "of" (Set (Var "S"))) "," (Set  "("  ($#k1_funct_2 :::"Funcs"::: )   "(" (Set (Var "I")) "," (Set  "("  ($#k10_xtuple_0 :::"rng"::: )  (Set  "("  ($#k2_funct_5 :::"uncurry"::: )  (Set  "("  ($#k11_pralg_2 :::"OPER"::: )  (Set (Var "A")) ")" ) ")" ) ")" ) ")"  ")" ) ")" )))))) ; 
 definitionlet "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 "A" be    ($#m1_pralg_2 :::"MSAlgebra-Family"::: )   "of" (Set (Const "I")) "," (Set (Const "S")); let "o" be   ($#m1_subset_1 :::"OperSymbol":::) "of" (Set (Const "S")); func "A" :::"?."::: "o" ->   ($#m1_hidden :::"ManySortedFunction":::) "of" "I" equals :: PRALG_2:def 12 (Set (Set  "("  ($#k10_funct_6 :::"commute"::: )  (Set  "("  ($#k11_pralg_2 :::"OPER"::: )  "A" ")" ) ")" )  ($#k1_funct_1 :::"."::: )  "o"); end; 








:: deftheorem    defines :::"?."::: PRALG_2:def 12 :  (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")) "holds"  (Bool (Set (Set (Var "A"))  ($#k12_pralg_2 :::"?."::: )  (Set (Var "o")))  ($#r1_hidden :::"="::: )  (Set (Set  "("  ($#k10_funct_6 :::"commute"::: )  (Set  "("  ($#k11_pralg_2 :::"OPER"::: )  (Set (Var "A")) ")" ) ")" )  ($#k1_funct_1 :::"."::: )  (Set (Var "o")))))))); 
 
theorem :: PRALG_2:7 (Bool  "for" (Set (Var "I")) "being"  ($#~v1_xboole_0  "non"   ($#v1_xboole_0 :::"empty"::: )   )    ($#m1_hidden :::"set"::: )    (Bool  "for" (Set (Var "i")) "being"    ($#m1_subset_1 :::"Element"::: )   "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 "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")) "holds"  (Bool (Set (Set  "(" (Set (Var "A"))  ($#k12_pralg_2 :::"?."::: )  (Set (Var "o")) ")" )  ($#k1_funct_1 :::"."::: )  (Set (Var "i")))  ($#r1_hidden :::"="::: )  (Set   ($#k5_msualg_1 :::"Den"::: )   "(" (Set (Var "o")) "," (Set  "(" (Set (Var "A"))  ($#k5_pralg_2 :::"."::: )  (Set (Var "i")) ")" ) ")" ))))))) ; 
 
theorem :: PRALG_2: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"))  (Bool  "for" (Set (Var "x")) "being"    ($#m1_hidden :::"set"::: )    "st" (Bool (Bool (Set (Var "x"))  ($#r2_hidden :::"in"::: )  (Set   ($#k10_xtuple_0 :::"rng"::: )  (Set  "("  ($#k2_pralg_2 :::"Frege"::: )  (Set  "(" (Set (Var "A"))  ($#k12_pralg_2 :::"?."::: )  (Set (Var "o")) ")" ) ")" )))) "holds"  (Bool (Set (Var "x")) "is"   ($#m1_hidden :::"Function":::))))))) ; 
 
theorem :: PRALG_2: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 "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 (Var "f"))  ($#r2_hidden :::"in"::: )  (Set   ($#k10_xtuple_0 :::"rng"::: )  (Set  "("  ($#k2_pralg_2 :::"Frege"::: )  (Set  "(" (Set (Var "A"))  ($#k12_pralg_2 :::"?."::: )  (Set (Var "o")) ")" ) ")" )))) "holds"  (Bool  "("  (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")))  ($#r2_hidden :::"in"::: )  (Set   ($#k4_msualg_1 :::"Result"::: )   "(" (Set (Var "o")) "," (Set  "(" (Set (Var "A"))  ($#k5_pralg_2 :::"."::: )  (Set (Var "i")) ")" ) ")" ))  ")" )  ")" )))))) ; 
 
theorem :: PRALG_2: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 (Var "f"))  ($#r2_hidden :::"in"::: )  (Set   ($#k9_xtuple_0 :::"dom"::: )  (Set  "("  ($#k2_pralg_2 :::"Frege"::: )  (Set  "(" (Set (Var "A"))  ($#k12_pralg_2 :::"?."::: )  (Set (Var "o")) ")" ) ")" )))) "holds"  (Bool  "("  (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")))  ($#r2_hidden :::"in"::: )  (Set   ($#k3_msualg_1 :::"Args"::: )   "(" (Set (Var "o")) "," (Set  "(" (Set (Var "A"))  ($#k5_pralg_2 :::"."::: )  (Set (Var "i")) ")" ) ")" ))  ")" ) & (Bool (Set   ($#k10_xtuple_0 :::"rng"::: )  (Set (Var "f")))  ($#r1_tarski :::"c="::: )  (Set   ($#k9_funct_2 :::"Funcs"::: )   "(" (Set  "("  ($#k9_xtuple_0 :::"dom"::: )  (Set  "("  ($#k1_msualg_1 :::"the_arity_of"::: )  (Set (Var "o")) ")" ) ")" ) "," (Set  ($#k7_pralg_2 :::"|."::: ) (Set (Var "A")) ($#k7_pralg_2 :::".|"::: ) ) ")" ))  ")" )))))) ; 
 
theorem :: PRALG_2:11 (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")) "holds"   (Bool  "("  (Bool (Set   ($#k9_xtuple_0 :::"dom"::: )  (Set  "("  ($#k2_funct_6 :::"doms"::: )  (Set  "(" (Set (Var "A"))  ($#k12_pralg_2 :::"?."::: )  (Set (Var "o")) ")" ) ")" ))  ($#r1_hidden :::"="::: )  (Set (Var "I"))) & (Bool  "("   "for" (Set (Var "i")) "being"    ($#m1_subset_1 :::"Element"::: )   "of" (Set (Var "I")) "holds"  (Bool (Set (Set  "("  ($#k2_funct_6 :::"doms"::: )  (Set  "(" (Set (Var "A"))  ($#k12_pralg_2 :::"?."::: )  (Set (Var "o")) ")" ) ")" )  ($#k1_funct_1 :::"."::: )  (Set (Var "i")))  ($#r1_hidden :::"="::: )  (Set   ($#k3_msualg_1 :::"Args"::: )   "(" (Set (Var "o")) "," (Set  "(" (Set (Var "A"))  ($#k5_pralg_2 :::"."::: )  (Set (Var "i")) ")" ) ")" ))  ")" )  ")" ))))) ; 
 definitionlet "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 "A" be    ($#m1_pralg_2 :::"MSAlgebra-Family"::: )   "of" (Set (Const "I")) "," (Set (Const "S")); func  :::"OPS"::: "A" ->    ($#m2_pboole :::"ManySortedFunction"::: )   "of" (Set (Set  "(" (Set  "("  ($#k10_pralg_2 :::"SORTS"::: )  "A" ")" )  ($#k6_finseq_2 :::"#"::: )  ")" )  ($#k3_relat_1 :::"*"::: )  (Set  "the"  ($#u1_msualg_1 :::"Arity"::: )  "of" "S")) "," (Set (Set  "("  ($#k10_pralg_2 :::"SORTS"::: )  "A" ")" )  ($#k3_relat_1 :::"*"::: )  (Set  "the"  ($#u2_msualg_1 :::"ResultSort"::: )  "of" "S")) means :: PRALG_2:def 13 (Bool  "for" (Set (Var "o")) "being"   ($#m1_subset_1 :::"OperSymbol":::) "of" "S" "holds"  (Bool (Set it  ($#k1_funct_1 :::"."::: )  (Set (Var "o")))  ($#r1_hidden :::"="::: )  (Set   ($#k14_funcop_1 :::"IFEQ"::: )   "(" (Set  "("  ($#k1_msualg_1 :::"the_arity_of"::: )  (Set (Var "o")) ")" ) "," (Set  ($#k1_xboole_0 :::"{}"::: ) ) "," (Set  "("  ($#k10_funct_6 :::"commute"::: )  (Set  "(" "A"  ($#k12_pralg_2 :::"?."::: )  (Set (Var "o")) ")" ) ")" ) "," (Set  "("  ($#k1_pralg_2 :::"Commute"::: )  (Set  "("  ($#k2_pralg_2 :::"Frege"::: )  (Set  "(" "A"  ($#k12_pralg_2 :::"?."::: )  (Set (Var "o")) ")" ) ")" ) ")" ) ")" ))) if (Bool "I"  ($#r1_hidden :::"<>"::: )  (Set   ($#k1_xboole_0 :::"{}"::: )  ))  otherwise (Bool verum); end; 







:: deftheorem    defines :::"OPS"::: PRALG_2:def 13 :  (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 "b4")) "being"    ($#m2_pboole :::"ManySortedFunction"::: )   "of" (Set (Set  "(" (Set  "("  ($#k10_pralg_2 :::"SORTS"::: )  (Set (Var "A")) ")" )  ($#k6_finseq_2 :::"#"::: )  ")" )  ($#k3_relat_1 :::"*"::: )  (Set  "the"  ($#u1_msualg_1 :::"Arity"::: )  "of" (Set (Var "S")))) "," (Set (Set  "("  ($#k10_pralg_2 :::"SORTS"::: )  (Set (Var "A")) ")" )  ($#k3_relat_1 :::"*"::: )  (Set  "the"  ($#u2_msualg_1 :::"ResultSort"::: )  "of" (Set (Var "S")))) "holds"   (Bool  "("   "("  (Bool (Bool (Set (Var "I"))  ($#r1_hidden :::"<>"::: )  (Set   ($#k1_xboole_0 :::"{}"::: )  ))) "implies" (Bool  "("  (Bool (Set (Var "b4"))  ($#r1_hidden :::"="::: )  (Set   ($#k13_pralg_2 :::"OPS"::: )  (Set (Var "A")))) "iff" (Bool  "for" (Set (Var "o")) "being"   ($#m1_subset_1 :::"OperSymbol":::) "of" (Set (Var "S")) "holds"  (Bool (Set (Set (Var "b4"))  ($#k1_funct_1 :::"."::: )  (Set (Var "o")))  ($#r1_hidden :::"="::: )  (Set   ($#k14_funcop_1 :::"IFEQ"::: )   "(" (Set  "("  ($#k1_msualg_1 :::"the_arity_of"::: )  (Set (Var "o")) ")" ) "," (Set  ($#k1_xboole_0 :::"{}"::: ) ) "," (Set  "("  ($#k10_funct_6 :::"commute"::: )  (Set  "(" (Set (Var "A"))  ($#k12_pralg_2 :::"?."::: )  (Set (Var "o")) ")" ) ")" ) "," (Set  "("  ($#k1_pralg_2 :::"Commute"::: )  (Set  "("  ($#k2_pralg_2 :::"Frege"::: )  (Set  "(" (Set (Var "A"))  ($#k12_pralg_2 :::"?."::: )  (Set (Var "o")) ")" ) ")" ) ")" ) ")" )))  ")" )  ")"  &  "("  (Bool (Bool (Bool  "not" (Set (Var "I"))  ($#r1_hidden :::"<>"::: )  (Set   ($#k1_xboole_0 :::"{}"::: )  )))) "implies" (Bool  "("  (Bool (Set (Var "b4"))  ($#r1_hidden :::"="::: )  (Set   ($#k13_pralg_2 :::"OPS"::: )  (Set (Var "A")))) "iff" (Bool verum)  ")" )  ")"   ")" ))))); 
 definitionlet "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 "A" be    ($#m1_pralg_2 :::"MSAlgebra-Family"::: )   "of" (Set (Const "I")) "," (Set (Const "S")); func  :::"product"::: "A" ->    ($#l3_msualg_1 :::"MSAlgebra"::: )   "over" "S" equals :: PRALG_2:def 14 (Set   ($#g3_msualg_1 :::"MSAlgebra"::: )  "(#"  (Set  "("  ($#k10_pralg_2 :::"SORTS"::: )  "A" ")" ) "," (Set  "("  ($#k13_pralg_2 :::"OPS"::: )  "A" ")" ) "#)" ); end; 







:: deftheorem    defines :::"product"::: PRALG_2:def 14 :  (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")) "holds"  (Bool (Set   ($#k14_pralg_2 :::"product"::: )  (Set (Var "A")))  ($#r1_hidden :::"="::: )  (Set   ($#g3_msualg_1 :::"MSAlgebra"::: )  "(#"  (Set  "("  ($#k10_pralg_2 :::"SORTS"::: )  (Set (Var "A")) ")" ) "," (Set  "("  ($#k13_pralg_2 :::"OPS"::: )  (Set (Var "A")) ")" ) "#)" ))))); 
 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 "A" be    ($#m1_pralg_2 :::"MSAlgebra-Family"::: )   "of" (Set (Const "I")) "," (Set (Const "S")); 
cluster (Set   ($#k14_pralg_2 :::"product"::: )  "A") ->   ($#v3_msualg_1 :::"strict"::: )   ; 
end; 
theorem :: PRALG_2:12 (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")) "holds"   (Bool  "("  (Bool (Set  "the"  ($#u3_msualg_1 :::"Sorts"::: )  "of" (Set  "("  ($#k14_pralg_2 :::"product"::: )  (Set (Var "A")) ")" ))  ($#r8_pboole :::"="::: )  (Set   ($#k10_pralg_2 :::"SORTS"::: )  (Set (Var "A")))) & (Bool (Set  "the"  ($#u4_msualg_1 :::"Charact"::: )  "of" (Set  "("  ($#k14_pralg_2 :::"product"::: )  (Set (Var "A")) ")" ))  ($#r8_pboole :::"="::: )  (Set   ($#k13_pralg_2 :::"OPS"::: )  (Set (Var "A"))))  ")" )))) ;