:: SETWISEO semantic presentation begin theorem :: SETWISEO:1 (Bool "for" (Set (Var "x")) "," (Set (Var "y")) "," (Set (Var "z")) "being" ($#m1_hidden :::"set"::: ) "holds" (Bool (Set ($#k1_tarski :::"{"::: ) (Set (Var "x")) ($#k1_tarski :::"}"::: ) ) ($#r1_tarski :::"c="::: ) (Set ($#k1_enumset1 :::"{"::: ) (Set (Var "x")) "," (Set (Var "y")) "," (Set (Var "z")) ($#k1_enumset1 :::"}"::: ) ))) ; theorem :: SETWISEO:2 (Bool "for" (Set (Var "x")) "," (Set (Var "y")) "," (Set (Var "z")) "being" ($#m1_hidden :::"set"::: ) "holds" (Bool (Set ($#k2_tarski :::"{"::: ) (Set (Var "x")) "," (Set (Var "y")) ($#k2_tarski :::"}"::: ) ) ($#r1_tarski :::"c="::: ) (Set ($#k1_enumset1 :::"{"::: ) (Set (Var "x")) "," (Set (Var "y")) "," (Set (Var "z")) ($#k1_enumset1 :::"}"::: ) ))) ; theorem :: SETWISEO:3 canceled; theorem :: SETWISEO:4 canceled; theorem :: SETWISEO:5 canceled; theorem :: SETWISEO:6 (Bool "for" (Set (Var "X")) "," (Set (Var "Y")) "being" ($#m1_hidden :::"set"::: ) (Bool "for" (Set (Var "f")) "being" ($#m1_hidden :::"Function":::) "holds" (Bool (Set (Set (Var "f")) ($#k7_relat_1 :::".:"::: ) (Set "(" (Set (Var "Y")) ($#k6_subset_1 :::"\"::: ) (Set "(" (Set (Var "f")) ($#k8_relat_1 :::"""::: ) (Set (Var "X")) ")" ) ")" )) ($#r1_hidden :::"="::: ) (Set (Set "(" (Set (Var "f")) ($#k7_relat_1 :::".:"::: ) (Set (Var "Y")) ")" ) ($#k6_subset_1 :::"\"::: ) (Set (Var "X")))))) ; theorem :: SETWISEO:7 (Bool "for" (Set (Var "Y")) "," (Set (Var "X")) "being" ($#~v1_xboole_0 "non" ($#v1_xboole_0 :::"empty"::: ) ) ($#m1_hidden :::"set"::: ) (Bool "for" (Set (Var "f")) "being" ($#m1_subset_1 :::"Function":::) "of" (Set (Var "X")) "," (Set (Var "Y")) (Bool "for" (Set (Var "x")) "being" ($#m1_subset_1 :::"Element"::: ) "of" (Set (Var "X")) "holds" (Bool (Set (Var "x")) ($#r2_hidden :::"in"::: ) (Set (Set (Var "f")) ($#k8_relset_1 :::"""::: ) (Set ($#k1_tarski :::"{"::: ) (Set "(" (Set (Var "f")) ($#k3_funct_2 :::"."::: ) (Set (Var "x")) ")" ) ($#k1_tarski :::"}"::: ) )))))) ; theorem :: SETWISEO:8 (Bool "for" (Set (Var "Y")) "," (Set (Var "X")) "being" ($#~v1_xboole_0 "non" ($#v1_xboole_0 :::"empty"::: ) ) ($#m1_hidden :::"set"::: ) (Bool "for" (Set (Var "f")) "being" ($#m1_subset_1 :::"Function":::) "of" (Set (Var "X")) "," (Set (Var "Y")) (Bool "for" (Set (Var "x")) "being" ($#m1_subset_1 :::"Element"::: ) "of" (Set (Var "X")) "holds" (Bool (Set ($#k9_relat_1 :::"Im"::: ) "(" (Set (Var "f")) "," (Set (Var "x")) ")" ) ($#r1_hidden :::"="::: ) (Set ($#k1_tarski :::"{"::: ) (Set "(" (Set (Var "f")) ($#k3_funct_2 :::"."::: ) (Set (Var "x")) ")" ) ($#k1_tarski :::"}"::: ) ))))) ; theorem :: SETWISEO:9 (Bool "for" (Set (Var "X")) "being" ($#~v1_xboole_0 "non" ($#v1_xboole_0 :::"empty"::: ) ) ($#m1_hidden :::"set"::: ) (Bool "for" (Set (Var "B")) "being" ($#m1_subset_1 :::"Element"::: ) "of" (Set ($#k5_finsub_1 :::"Fin"::: ) (Set (Var "X"))) (Bool "for" (Set (Var "x")) "being" ($#m1_hidden :::"set"::: ) "st" (Bool (Bool (Set (Var "x")) ($#r2_hidden :::"in"::: ) (Set (Var "B")))) "holds" (Bool (Set (Var "x")) "is" ($#m1_subset_1 :::"Element"::: ) "of" (Set (Var "X")))))) ; theorem :: SETWISEO:10 (Bool "for" (Set (Var "X")) "," (Set (Var "Y")) "being" ($#~v1_xboole_0 "non" ($#v1_xboole_0 :::"empty"::: ) ) ($#m1_hidden :::"set"::: ) (Bool "for" (Set (Var "A")) "being" ($#m1_subset_1 :::"Element"::: ) "of" (Set ($#k5_finsub_1 :::"Fin"::: ) (Set (Var "X"))) (Bool "for" (Set (Var "B")) "being" ($#m1_hidden :::"set"::: ) (Bool "for" (Set (Var "f")) "being" ($#m1_subset_1 :::"Function":::) "of" (Set (Var "X")) "," (Set (Var "Y")) "st" (Bool (Bool "(" "for" (Set (Var "x")) "being" ($#m1_subset_1 :::"Element"::: ) "of" (Set (Var "X")) "st" (Bool (Bool (Set (Var "x")) ($#r2_hidden :::"in"::: ) (Set (Var "A")))) "holds" (Bool (Set (Set (Var "f")) ($#k3_funct_2 :::"."::: ) (Set (Var "x"))) ($#r2_hidden :::"in"::: ) (Set (Var "B"))) ")" )) "holds" (Bool (Set (Set (Var "f")) ($#k7_relset_1 :::".:"::: ) (Set (Var "A"))) ($#r1_tarski :::"c="::: ) (Set (Var "B"))))))) ; theorem :: SETWISEO:11 (Bool "for" (Set (Var "X")) "being" ($#m1_hidden :::"set"::: ) (Bool "for" (Set (Var "B")) "being" ($#m1_subset_1 :::"Element"::: ) "of" (Set ($#k5_finsub_1 :::"Fin"::: ) (Set (Var "X"))) (Bool "for" (Set (Var "A")) "being" ($#m1_hidden :::"set"::: ) "st" (Bool (Bool (Set (Var "A")) ($#r1_tarski :::"c="::: ) (Set (Var "B")))) "holds" (Bool (Set (Var "A")) "is" ($#m1_subset_1 :::"Element"::: ) "of" (Set ($#k5_finsub_1 :::"Fin"::: ) (Set (Var "X"))))))) ; theorem :: SETWISEO:12 (Bool "for" (Set (Var "X")) "being" ($#~v1_xboole_0 "non" ($#v1_xboole_0 :::"empty"::: ) ) ($#m1_hidden :::"set"::: ) (Bool "for" (Set (Var "B")) "being" ($#m1_subset_1 :::"Element"::: ) "of" (Set ($#k5_finsub_1 :::"Fin"::: ) (Set (Var "X"))) "st" (Bool (Bool (Set (Var "B")) ($#r1_hidden :::"<>"::: ) (Set ($#k1_xboole_0 :::"{}"::: ) ))) "holds" (Bool "ex" (Set (Var "x")) "being" ($#m1_subset_1 :::"Element"::: ) "of" (Set (Var "X")) "st" (Bool (Set (Var "x")) ($#r2_hidden :::"in"::: ) (Set (Var "B")))))) ; theorem :: SETWISEO:13 (Bool "for" (Set (Var "Y")) "," (Set (Var "X")) "being" ($#~v1_xboole_0 "non" ($#v1_xboole_0 :::"empty"::: ) ) ($#m1_hidden :::"set"::: ) (Bool "for" (Set (Var "f")) "being" ($#m1_subset_1 :::"Function":::) "of" (Set (Var "X")) "," (Set (Var "Y")) (Bool "for" (Set (Var "A")) "being" ($#m1_subset_1 :::"Element"::: ) "of" (Set ($#k5_finsub_1 :::"Fin"::: ) (Set (Var "X"))) "st" (Bool (Bool (Set (Set (Var "f")) ($#k7_relset_1 :::".:"::: ) (Set (Var "A"))) ($#r1_hidden :::"="::: ) (Set ($#k1_xboole_0 :::"{}"::: ) ))) "holds" (Bool (Set (Var "A")) ($#r1_hidden :::"="::: ) (Set ($#k1_xboole_0 :::"{}"::: ) ))))) ; registrationlet "X" be ($#m1_hidden :::"set"::: ) ; cluster ($#v1_xboole_0 :::"empty"::: ) ($#v1_finset_1 :::"finite"::: ) for ($#m1_subset_1 :::"Element"::: ) "of" (Set ($#k5_finsub_1 :::"Fin"::: ) "X"); end; definitionlet "X" be ($#m1_hidden :::"set"::: ) ; func :::"{}."::: "X" -> ($#v1_xboole_0 :::"empty"::: ) ($#m1_subset_1 :::"Element"::: ) "of" (Set ($#k5_finsub_1 :::"Fin"::: ) "X") equals :: SETWISEO:def 1 (Set ($#k1_xboole_0 :::"{}"::: ) ); end; :: deftheorem defines :::"{}."::: SETWISEO:def 1 : (Bool "for" (Set (Var "X")) "being" ($#m1_hidden :::"set"::: ) "holds" (Bool (Set ($#k1_setwiseo :::"{}."::: ) (Set (Var "X"))) ($#r1_hidden :::"="::: ) (Set ($#k1_xboole_0 :::"{}"::: ) ))); scheme :: SETWISEO:sch 1 FinSubFuncEx{ F1() -> ($#~v1_xboole_0 "non" ($#v1_xboole_0 :::"empty"::: ) ) ($#m1_hidden :::"set"::: ) , F2() -> ($#m1_subset_1 :::"Element"::: ) "of" (Set ($#k5_finsub_1 :::"Fin"::: ) (Set F1 "(" ")" )), P1[ ($#m1_hidden :::"set"::: ) "," ($#m1_hidden :::"set"::: ) ] } : (Bool "ex" (Set (Var "f")) "being" ($#m1_subset_1 :::"Function":::) "of" (Set F1 "(" ")" ) "," (Set "(" ($#k5_finsub_1 :::"Fin"::: ) (Set F1 "(" ")" ) ")" ) "st" (Bool "for" (Set (Var "b")) "," (Set (Var "a")) "being" ($#m1_subset_1 :::"Element"::: ) "of" (Set F1 "(" ")" ) "holds" (Bool "(" (Bool (Set (Var "a")) ($#r2_hidden :::"in"::: ) (Set (Set (Var "f")) ($#k3_funct_2 :::"."::: ) (Set (Var "b")))) "iff" (Bool "(" (Bool (Set (Var "a")) ($#r2_hidden :::"in"::: ) (Set F2 "(" ")" )) & (Bool P1[(Set (Var "a")) "," (Set (Var "b"))]) ")" ) ")" ))) proof end; definitionlet "X" be ($#~v1_xboole_0 "non" ($#v1_xboole_0 :::"empty"::: ) ) ($#m1_hidden :::"set"::: ) ; let "F" be ($#m1_subset_1 :::"BinOp":::) "of" (Set (Const "X")); attr "F" is :::"having_a_unity"::: means :: SETWISEO:def 2 (Bool "ex" (Set (Var "x")) "being" ($#m1_subset_1 :::"Element"::: ) "of" "X" "st" (Bool (Set (Var "x")) ($#r3_binop_1 :::"is_a_unity_wrt"::: ) "F")); end; :: deftheorem defines :::"having_a_unity"::: SETWISEO:def 2 : (Bool "for" (Set (Var "X")) "being" ($#~v1_xboole_0 "non" ($#v1_xboole_0 :::"empty"::: ) ) ($#m1_hidden :::"set"::: ) (Bool "for" (Set (Var "F")) "being" ($#m1_subset_1 :::"BinOp":::) "of" (Set (Var "X")) "holds" (Bool "(" (Bool (Set (Var "F")) "is" ($#v1_setwiseo :::"having_a_unity"::: ) ) "iff" (Bool "ex" (Set (Var "x")) "being" ($#m1_subset_1 :::"Element"::: ) "of" (Set (Var "X")) "st" (Bool (Set (Var "x")) ($#r3_binop_1 :::"is_a_unity_wrt"::: ) (Set (Var "F")))) ")" ))); theorem :: SETWISEO:14 (Bool "for" (Set (Var "X")) "being" ($#~v1_xboole_0 "non" ($#v1_xboole_0 :::"empty"::: ) ) ($#m1_hidden :::"set"::: ) (Bool "for" (Set (Var "F")) "being" ($#m1_subset_1 :::"BinOp":::) "of" (Set (Var "X")) "holds" (Bool "(" (Bool (Set (Var "F")) "is" ($#v1_setwiseo :::"having_a_unity"::: ) ) "iff" (Bool (Set ($#k4_binop_1 :::"the_unity_wrt"::: ) (Set (Var "F"))) ($#r3_binop_1 :::"is_a_unity_wrt"::: ) (Set (Var "F"))) ")" ))) ; theorem :: SETWISEO:15 (Bool "for" (Set (Var "X")) "being" ($#~v1_xboole_0 "non" ($#v1_xboole_0 :::"empty"::: ) ) ($#m1_hidden :::"set"::: ) (Bool "for" (Set (Var "F")) "being" ($#m1_subset_1 :::"BinOp":::) "of" (Set (Var "X")) "st" (Bool (Bool (Set (Var "F")) "is" ($#v1_setwiseo :::"having_a_unity"::: ) )) "holds" (Bool "for" (Set (Var "x")) "being" ($#m1_subset_1 :::"Element"::: ) "of" (Set (Var "X")) "holds" (Bool "(" (Bool (Set (Set (Var "F")) ($#k5_binop_1 :::"."::: ) "(" (Set "(" ($#k4_binop_1 :::"the_unity_wrt"::: ) (Set (Var "F")) ")" ) "," (Set (Var "x")) ")" ) ($#r1_hidden :::"="::: ) (Set (Var "x"))) & (Bool (Set (Set (Var "F")) ($#k5_binop_1 :::"."::: ) "(" (Set (Var "x")) "," (Set "(" ($#k4_binop_1 :::"the_unity_wrt"::: ) (Set (Var "F")) ")" ) ")" ) ($#r1_hidden :::"="::: ) (Set (Var "x"))) ")" )))) ; registrationlet "X" be ($#~v1_xboole_0 "non" ($#v1_xboole_0 :::"empty"::: ) ) ($#m1_hidden :::"set"::: ) ; cluster ($#~v1_xboole_0 "non" ($#v1_xboole_0 :::"empty"::: ) ) ($#v1_finset_1 :::"finite"::: ) for ($#m1_subset_1 :::"Element"::: ) "of" (Set ($#k5_finsub_1 :::"Fin"::: ) "X"); end; notationlet "X" be ($#~v1_xboole_0 "non" ($#v1_xboole_0 :::"empty"::: ) ) ($#m1_hidden :::"set"::: ) ; let "x" be ($#m1_subset_1 :::"Element"::: ) "of" (Set (Const "X")); synonym :::"{.":::"x":::".}"::: for :::"{":::"X":::"}":::; let "y" be ($#m1_subset_1 :::"Element"::: ) "of" (Set (Const "X")); synonym :::"{.":::"x" "," "y":::".}"::: for :::"{":::"X" "," "x":::"}":::; let "z" be ($#m1_subset_1 :::"Element"::: ) "of" (Set (Const "X")); synonym :::"{.":::"x" "," "y" "," "z":::".}"::: for :::"{":::"X" "," "x" "," "y":::"}":::; end; definitionlet "X" be ($#~v1_xboole_0 "non" ($#v1_xboole_0 :::"empty"::: ) ) ($#m1_hidden :::"set"::: ) ; let "x" be ($#m1_subset_1 :::"Element"::: ) "of" (Set (Const "X")); :: original: :::"{."::: redefine func :::"{.":::"x":::".}"::: -> ($#m1_subset_1 :::"Element"::: ) "of" (Set ($#k5_finsub_1 :::"Fin"::: ) "X"); let "y" be ($#m1_subset_1 :::"Element"::: ) "of" (Set (Const "X")); :: original: :::"{."::: redefine func :::"{.":::"x" "," "y":::".}"::: -> ($#m1_subset_1 :::"Element"::: ) "of" (Set ($#k5_finsub_1 :::"Fin"::: ) "X"); let "z" be ($#m1_subset_1 :::"Element"::: ) "of" (Set (Const "X")); :: original: :::"{."::: redefine func :::"{.":::"x" "," "y" "," "z":::".}"::: -> ($#m1_subset_1 :::"Element"::: ) "of" (Set ($#k5_finsub_1 :::"Fin"::: ) "X"); end; definitionlet "X" be ($#m1_hidden :::"set"::: ) ; let "A", "B" be ($#m1_subset_1 :::"Element"::: ) "of" (Set ($#k5_finsub_1 :::"Fin"::: ) (Set (Const "X"))); :: original: :::"\/"::: redefine func "A" :::"\/"::: "B" -> ($#m1_subset_1 :::"Element"::: ) "of" (Set ($#k5_finsub_1 :::"Fin"::: ) "X"); end; definitionlet "X" be ($#m1_hidden :::"set"::: ) ; let "A", "B" be ($#m1_subset_1 :::"Element"::: ) "of" (Set ($#k5_finsub_1 :::"Fin"::: ) (Set (Const "X"))); :: original: :::"\"::: redefine func "A" :::"\"::: "B" -> ($#m1_subset_1 :::"Element"::: ) "of" (Set ($#k5_finsub_1 :::"Fin"::: ) "X"); end; scheme :: SETWISEO:sch 2 FinSubInd1{ F1() -> ($#~v1_xboole_0 "non" ($#v1_xboole_0 :::"empty"::: ) ) ($#m1_hidden :::"set"::: ) , P1[ ($#m1_hidden :::"set"::: ) ] } : (Bool "for" (Set (Var "B")) "being" ($#m1_subset_1 :::"Element"::: ) "of" (Set ($#k5_finsub_1 :::"Fin"::: ) (Set F1 "(" ")" )) "holds" (Bool P1[(Set (Var "B"))])) provided (Bool P1[(Set ($#k1_setwiseo :::"{}."::: ) (Set F1 "(" ")" ))]) and (Bool "for" (Set (Var "B9")) "being" ($#m1_subset_1 :::"Element"::: ) "of" (Set ($#k5_finsub_1 :::"Fin"::: ) (Set F1 "(" ")" )) (Bool "for" (Set (Var "b")) "being" ($#m1_subset_1 :::"Element"::: ) "of" (Set F1 "(" ")" ) "st" (Bool (Bool P1[(Set (Var "B9"))]) & (Bool (Bool "not" (Set (Var "b")) ($#r2_hidden :::"in"::: ) (Set (Var "B9"))))) "holds" (Bool P1[(Set (Set (Var "B9")) ($#k2_xboole_0 :::"\/"::: ) (Set ($#k1_tarski :::"{"::: ) (Set (Var "b")) ($#k1_tarski :::"}"::: ) ))]))) proof end; scheme :: SETWISEO:sch 3 FinSubInd2{ F1() -> ($#~v1_xboole_0 "non" ($#v1_xboole_0 :::"empty"::: ) ) ($#m1_hidden :::"set"::: ) , P1[ ($#m1_subset_1 :::"Element"::: ) "of" (Set ($#k5_finsub_1 :::"Fin"::: ) (Set F1 "(" ")" ))] } : (Bool "for" (Set (Var "B")) "being" ($#~v1_xboole_0 "non" ($#v1_xboole_0 :::"empty"::: ) ) ($#m1_subset_1 :::"Element"::: ) "of" (Set ($#k5_finsub_1 :::"Fin"::: ) (Set F1 "(" ")" )) "holds" (Bool P1[(Set (Var "B"))])) provided (Bool "for" (Set (Var "x")) "being" ($#m1_subset_1 :::"Element"::: ) "of" (Set F1 "(" ")" ) "holds" (Bool P1[(Set ($#k2_setwiseo :::"{."::: ) (Set (Var "x")) ($#k2_setwiseo :::".}"::: ) )])) and (Bool "for" (Set (Var "B1")) "," (Set (Var "B2")) "being" ($#~v1_xboole_0 "non" ($#v1_xboole_0 :::"empty"::: ) ) ($#m1_subset_1 :::"Element"::: ) "of" (Set ($#k5_finsub_1 :::"Fin"::: ) (Set F1 "(" ")" )) "st" (Bool (Bool P1[(Set (Var "B1"))]) & (Bool P1[(Set (Var "B2"))])) "holds" (Bool P1[(Set (Set (Var "B1")) ($#k5_setwiseo :::"\/"::: ) (Set (Var "B2")))])) proof end; scheme :: SETWISEO:sch 4 FinSubInd3{ F1() -> ($#~v1_xboole_0 "non" ($#v1_xboole_0 :::"empty"::: ) ) ($#m1_hidden :::"set"::: ) , P1[ ($#m1_hidden :::"set"::: ) ] } : (Bool "for" (Set (Var "B")) "being" ($#m1_subset_1 :::"Element"::: ) "of" (Set ($#k5_finsub_1 :::"Fin"::: ) (Set F1 "(" ")" )) "holds" (Bool P1[(Set (Var "B"))])) provided (Bool P1[(Set ($#k1_setwiseo :::"{}."::: ) (Set F1 "(" ")" ))]) and (Bool "for" (Set (Var "B9")) "being" ($#m1_subset_1 :::"Element"::: ) "of" (Set ($#k5_finsub_1 :::"Fin"::: ) (Set F1 "(" ")" )) (Bool "for" (Set (Var "b")) "being" ($#m1_subset_1 :::"Element"::: ) "of" (Set F1 "(" ")" ) "st" (Bool (Bool P1[(Set (Var "B9"))])) "holds" (Bool P1[(Set (Set (Var "B9")) ($#k2_xboole_0 :::"\/"::: ) (Set ($#k1_tarski :::"{"::: ) (Set (Var "b")) ($#k1_tarski :::"}"::: ) ))]))) proof end; definitionlet "X", "Y" be ($#~v1_xboole_0 "non" ($#v1_xboole_0 :::"empty"::: ) ) ($#m1_hidden :::"set"::: ) ; let "F" be ($#m1_subset_1 :::"BinOp":::) "of" (Set (Const "Y")); let "B" be ($#m1_subset_1 :::"Element"::: ) "of" (Set ($#k5_finsub_1 :::"Fin"::: ) (Set (Const "X"))); let "f" be ($#m1_subset_1 :::"Function":::) "of" (Set (Const "X")) "," (Set (Const "Y")); assume that (Bool "(" (Bool (Set (Const "B")) ($#r1_hidden :::"<>"::: ) (Set ($#k1_xboole_0 :::"{}"::: ) )) "or" (Bool (Set (Const "F")) "is" ($#v1_setwiseo :::"having_a_unity"::: ) ) ")" ) and (Bool (Set (Const "F")) "is" ($#v1_binop_1 :::"commutative"::: ) ) and (Bool (Set (Const "F")) "is" ($#v2_binop_1 :::"associative"::: ) ) ; func "F" :::"$$"::: "(" "B" "," "f" ")" -> ($#m1_subset_1 :::"Element"::: ) "of" "Y" means :: SETWISEO:def 3 (Bool "ex" (Set (Var "G")) "being" ($#m1_subset_1 :::"Function":::) "of" (Set "(" ($#k5_finsub_1 :::"Fin"::: ) "X" ")" ) "," "Y" "st" (Bool "(" (Bool it ($#r1_hidden :::"="::: ) (Set (Set (Var "G")) ($#k3_funct_2 :::"."::: ) "B")) & (Bool "(" "for" (Set (Var "e")) "being" ($#m1_subset_1 :::"Element"::: ) "of" "Y" "st" (Bool (Bool (Set (Var "e")) ($#r3_binop_1 :::"is_a_unity_wrt"::: ) "F")) "holds" (Bool (Set (Set (Var "G")) ($#k1_funct_1 :::"."::: ) (Set ($#k1_xboole_0 :::"{}"::: ) )) ($#r1_hidden :::"="::: ) (Set (Var "e"))) ")" ) & (Bool "(" "for" (Set (Var "x")) "being" ($#m1_subset_1 :::"Element"::: ) "of" "X" "holds" (Bool (Set (Set (Var "G")) ($#k1_funct_1 :::"."::: ) (Set ($#k1_tarski :::"{"::: ) (Set (Var "x")) ($#k1_tarski :::"}"::: ) )) ($#r1_hidden :::"="::: ) (Set "f" ($#k3_funct_2 :::"."::: ) (Set (Var "x")))) ")" ) & (Bool "(" "for" (Set (Var "B9")) "being" ($#m1_subset_1 :::"Element"::: ) "of" (Set ($#k5_finsub_1 :::"Fin"::: ) "X") "st" (Bool (Bool (Set (Var "B9")) ($#r1_tarski :::"c="::: ) "B") & (Bool (Set (Var "B9")) ($#r1_hidden :::"<>"::: ) (Set ($#k1_xboole_0 :::"{}"::: ) ))) "holds" (Bool "for" (Set (Var "x")) "being" ($#m1_subset_1 :::"Element"::: ) "of" "X" "st" (Bool (Bool (Set (Var "x")) ($#r2_hidden :::"in"::: ) (Set "B" ($#k6_setwiseo :::"\"::: ) (Set (Var "B9"))))) "holds" (Bool (Set (Set (Var "G")) ($#k1_funct_1 :::"."::: ) (Set "(" (Set (Var "B9")) ($#k2_xboole_0 :::"\/"::: ) (Set ($#k1_tarski :::"{"::: ) (Set (Var "x")) ($#k1_tarski :::"}"::: ) ) ")" )) ($#r1_hidden :::"="::: ) (Set "F" ($#k5_binop_1 :::"."::: ) "(" (Set "(" (Set (Var "G")) ($#k3_funct_2 :::"."::: ) (Set (Var "B9")) ")" ) "," (Set "(" "f" ($#k3_funct_2 :::"."::: ) (Set (Var "x")) ")" ) ")" ))) ")" ) ")" )); end; :: deftheorem defines :::"$$"::: SETWISEO:def 3 : (Bool "for" (Set (Var "X")) "," (Set (Var "Y")) "being" ($#~v1_xboole_0 "non" ($#v1_xboole_0 :::"empty"::: ) ) ($#m1_hidden :::"set"::: ) (Bool "for" (Set (Var "F")) "being" ($#m1_subset_1 :::"BinOp":::) "of" (Set (Var "Y")) (Bool "for" (Set (Var "B")) "being" ($#m1_subset_1 :::"Element"::: ) "of" (Set ($#k5_finsub_1 :::"Fin"::: ) (Set (Var "X"))) (Bool "for" (Set (Var "f")) "being" ($#m1_subset_1 :::"Function":::) "of" (Set (Var "X")) "," (Set (Var "Y")) "st" (Bool (Bool "(" (Bool (Set (Var "B")) ($#r1_hidden :::"<>"::: ) (Set ($#k1_xboole_0 :::"{}"::: ) )) "or" (Bool (Set (Var "F")) "is" ($#v1_setwiseo :::"having_a_unity"::: ) ) ")" ) & (Bool (Set (Var "F")) "is" ($#v1_binop_1 :::"commutative"::: ) ) & (Bool (Set (Var "F")) "is" ($#v2_binop_1 :::"associative"::: ) )) "holds" (Bool "for" (Set (Var "b6")) "being" ($#m1_subset_1 :::"Element"::: ) "of" (Set (Var "Y")) "holds" (Bool "(" (Bool (Set (Var "b6")) ($#r1_hidden :::"="::: ) (Set (Set (Var "F")) ($#k7_setwiseo :::"$$"::: ) "(" (Set (Var "B")) "," (Set (Var "f")) ")" )) "iff" (Bool "ex" (Set (Var "G")) "being" ($#m1_subset_1 :::"Function":::) "of" (Set "(" ($#k5_finsub_1 :::"Fin"::: ) (Set (Var "X")) ")" ) "," (Set (Var "Y")) "st" (Bool "(" (Bool (Set (Var "b6")) ($#r1_hidden :::"="::: ) (Set (Set (Var "G")) ($#k3_funct_2 :::"."::: ) (Set (Var "B")))) & (Bool "(" "for" (Set (Var "e")) "being" ($#m1_subset_1 :::"Element"::: ) "of" (Set (Var "Y")) "st" (Bool (Bool (Set (Var "e")) ($#r3_binop_1 :::"is_a_unity_wrt"::: ) (Set (Var "F")))) "holds" (Bool (Set (Set (Var "G")) ($#k1_funct_1 :::"."::: ) (Set ($#k1_xboole_0 :::"{}"::: ) )) ($#r1_hidden :::"="::: ) (Set (Var "e"))) ")" ) & (Bool "(" "for" (Set (Var "x")) "being" ($#m1_subset_1 :::"Element"::: ) "of" (Set (Var "X")) "holds" (Bool (Set (Set (Var "G")) ($#k1_funct_1 :::"."::: ) (Set ($#k1_tarski :::"{"::: ) (Set (Var "x")) ($#k1_tarski :::"}"::: ) )) ($#r1_hidden :::"="::: ) (Set (Set (Var "f")) ($#k3_funct_2 :::"."::: ) (Set (Var "x")))) ")" ) & (Bool "(" "for" (Set (Var "B9")) "being" ($#m1_subset_1 :::"Element"::: ) "of" (Set ($#k5_finsub_1 :::"Fin"::: ) (Set (Var "X"))) "st" (Bool (Bool (Set (Var "B9")) ($#r1_tarski :::"c="::: ) (Set (Var "B"))) & (Bool (Set (Var "B9")) ($#r1_hidden :::"<>"::: ) (Set ($#k1_xboole_0 :::"{}"::: ) ))) "holds" (Bool "for" (Set (Var "x")) "being" ($#m1_subset_1 :::"Element"::: ) "of" (Set (Var "X")) "st" (Bool (Bool (Set (Var "x")) ($#r2_hidden :::"in"::: ) (Set (Set (Var "B")) ($#k6_setwiseo :::"\"::: ) (Set (Var "B9"))))) "holds" (Bool (Set (Set (Var "G")) ($#k1_funct_1 :::"."::: ) (Set "(" (Set (Var "B9")) ($#k2_xboole_0 :::"\/"::: ) (Set ($#k1_tarski :::"{"::: ) (Set (Var "x")) ($#k1_tarski :::"}"::: ) ) ")" )) ($#r1_hidden :::"="::: ) (Set (Set (Var "F")) ($#k5_binop_1 :::"."::: ) "(" (Set "(" (Set (Var "G")) ($#k3_funct_2 :::"."::: ) (Set (Var "B9")) ")" ) "," (Set "(" (Set (Var "f")) ($#k3_funct_2 :::"."::: ) (Set (Var "x")) ")" ) ")" ))) ")" ) ")" )) ")" )))))); theorem :: SETWISEO:16 (Bool "for" (Set (Var "X")) "," (Set (Var "Y")) "being" ($#~v1_xboole_0 "non" ($#v1_xboole_0 :::"empty"::: ) ) ($#m1_hidden :::"set"::: ) (Bool "for" (Set (Var "F")) "being" ($#m1_subset_1 :::"BinOp":::) "of" (Set (Var "Y")) (Bool "for" (Set (Var "B")) "being" ($#m1_subset_1 :::"Element"::: ) "of" (Set ($#k5_finsub_1 :::"Fin"::: ) (Set (Var "X"))) (Bool "for" (Set (Var "f")) "being" ($#m1_subset_1 :::"Function":::) "of" (Set (Var "X")) "," (Set (Var "Y")) "st" (Bool (Bool "(" (Bool (Set (Var "B")) ($#r1_hidden :::"<>"::: ) (Set ($#k1_xboole_0 :::"{}"::: ) )) "or" (Bool (Set (Var "F")) "is" ($#v1_setwiseo :::"having_a_unity"::: ) ) ")" ) & (Bool (Set (Var "F")) "is" ($#v3_binop_1 :::"idempotent"::: ) ) & (Bool (Set (Var "F")) "is" ($#v1_binop_1 :::"commutative"::: ) ) & (Bool (Set (Var "F")) "is" ($#v2_binop_1 :::"associative"::: ) )) "holds" (Bool "for" (Set (Var "IT")) "being" ($#m1_subset_1 :::"Element"::: ) "of" (Set (Var "Y")) "holds" (Bool "(" (Bool (Set (Var "IT")) ($#r1_hidden :::"="::: ) (Set (Set (Var "F")) ($#k7_setwiseo :::"$$"::: ) "(" (Set (Var "B")) "," (Set (Var "f")) ")" )) "iff" (Bool "ex" (Set (Var "G")) "being" ($#m1_subset_1 :::"Function":::) "of" (Set "(" ($#k5_finsub_1 :::"Fin"::: ) (Set (Var "X")) ")" ) "," (Set (Var "Y")) "st" (Bool "(" (Bool (Set (Var "IT")) ($#r1_hidden :::"="::: ) (Set (Set (Var "G")) ($#k3_funct_2 :::"."::: ) (Set (Var "B")))) & (Bool "(" "for" (Set (Var "e")) "being" ($#m1_subset_1 :::"Element"::: ) "of" (Set (Var "Y")) "st" (Bool (Bool (Set (Var "e")) ($#r3_binop_1 :::"is_a_unity_wrt"::: ) (Set (Var "F")))) "holds" (Bool (Set (Set (Var "G")) ($#k1_funct_1 :::"."::: ) (Set ($#k1_xboole_0 :::"{}"::: ) )) ($#r1_hidden :::"="::: ) (Set (Var "e"))) ")" ) & (Bool "(" "for" (Set (Var "x")) "being" ($#m1_subset_1 :::"Element"::: ) "of" (Set (Var "X")) "holds" (Bool (Set (Set (Var "G")) ($#k1_funct_1 :::"."::: ) (Set ($#k1_tarski :::"{"::: ) (Set (Var "x")) ($#k1_tarski :::"}"::: ) )) ($#r1_hidden :::"="::: ) (Set (Set (Var "f")) ($#k3_funct_2 :::"."::: ) (Set (Var "x")))) ")" ) & (Bool "(" "for" (Set (Var "B9")) "being" ($#m1_subset_1 :::"Element"::: ) "of" (Set ($#k5_finsub_1 :::"Fin"::: ) (Set (Var "X"))) "st" (Bool (Bool (Set (Var "B9")) ($#r1_tarski :::"c="::: ) (Set (Var "B"))) & (Bool (Set (Var "B9")) ($#r1_hidden :::"<>"::: ) (Set ($#k1_xboole_0 :::"{}"::: ) ))) "holds" (Bool "for" (Set (Var "x")) "being" ($#m1_subset_1 :::"Element"::: ) "of" (Set (Var "X")) "st" (Bool (Bool (Set (Var "x")) ($#r2_hidden :::"in"::: ) (Set (Var "B")))) "holds" (Bool (Set (Set (Var "G")) ($#k1_funct_1 :::"."::: ) (Set "(" (Set (Var "B9")) ($#k2_xboole_0 :::"\/"::: ) (Set ($#k1_tarski :::"{"::: ) (Set (Var "x")) ($#k1_tarski :::"}"::: ) ) ")" )) ($#r1_hidden :::"="::: ) (Set (Set (Var "F")) ($#k5_binop_1 :::"."::: ) "(" (Set "(" (Set (Var "G")) ($#k3_funct_2 :::"."::: ) (Set (Var "B9")) ")" ) "," (Set "(" (Set (Var "f")) ($#k3_funct_2 :::"."::: ) (Set (Var "x")) ")" ) ")" ))) ")" ) ")" )) ")" )))))) ; theorem :: SETWISEO:17 (Bool "for" (Set (Var "Y")) "," (Set (Var "X")) "being" ($#~v1_xboole_0 "non" ($#v1_xboole_0 :::"empty"::: ) ) ($#m1_hidden :::"set"::: ) (Bool "for" (Set (Var "F")) "being" ($#m1_subset_1 :::"BinOp":::) "of" (Set (Var "Y")) (Bool "for" (Set (Var "f")) "being" ($#m1_subset_1 :::"Function":::) "of" (Set (Var "X")) "," (Set (Var "Y")) "st" (Bool (Bool (Set (Var "F")) "is" ($#v1_binop_1 :::"commutative"::: ) ) & (Bool (Set (Var "F")) "is" ($#v2_binop_1 :::"associative"::: ) )) "holds" (Bool "for" (Set (Var "b")) "being" ($#m1_subset_1 :::"Element"::: ) "of" (Set (Var "X")) "holds" (Bool (Set (Set (Var "F")) ($#k7_setwiseo :::"$$"::: ) "(" (Set ($#k2_setwiseo :::"{."::: ) (Set (Var "b")) ($#k2_setwiseo :::".}"::: ) ) "," (Set (Var "f")) ")" ) ($#r1_hidden :::"="::: ) (Set (Set (Var "f")) ($#k3_funct_2 :::"."::: ) (Set (Var "b")))))))) ; theorem :: SETWISEO:18 (Bool "for" (Set (Var "Y")) "," (Set (Var "X")) "being" ($#~v1_xboole_0 "non" ($#v1_xboole_0 :::"empty"::: ) ) ($#m1_hidden :::"set"::: ) (Bool "for" (Set (Var "F")) "being" ($#m1_subset_1 :::"BinOp":::) "of" (Set (Var "Y")) (Bool "for" (Set (Var "f")) "being" ($#m1_subset_1 :::"Function":::) "of" (Set (Var "X")) "," (Set (Var "Y")) "st" (Bool (Bool (Set (Var "F")) "is" ($#v3_binop_1 :::"idempotent"::: ) ) & (Bool (Set (Var "F")) "is" ($#v1_binop_1 :::"commutative"::: ) ) & (Bool (Set (Var "F")) "is" ($#v2_binop_1 :::"associative"::: ) )) "holds" (Bool "for" (Set (Var "a")) "," (Set (Var "b")) "being" ($#m1_subset_1 :::"Element"::: ) "of" (Set (Var "X")) "holds" (Bool (Set (Set (Var "F")) ($#k7_setwiseo :::"$$"::: ) "(" (Set ($#k3_setwiseo :::"{."::: ) (Set (Var "a")) "," (Set (Var "b")) ($#k3_setwiseo :::".}"::: ) ) "," (Set (Var "f")) ")" ) ($#r1_hidden :::"="::: ) (Set (Set (Var "F")) ($#k5_binop_1 :::"."::: ) "(" (Set "(" (Set (Var "f")) ($#k3_funct_2 :::"."::: ) (Set (Var "a")) ")" ) "," (Set "(" (Set (Var "f")) ($#k3_funct_2 :::"."::: ) (Set (Var "b")) ")" ) ")" )))))) ; theorem :: SETWISEO:19 (Bool "for" (Set (Var "Y")) "," (Set (Var "X")) "being" ($#~v1_xboole_0 "non" ($#v1_xboole_0 :::"empty"::: ) ) ($#m1_hidden :::"set"::: ) (Bool "for" (Set (Var "F")) "being" ($#m1_subset_1 :::"BinOp":::) "of" (Set (Var "Y")) (Bool "for" (Set (Var "f")) "being" ($#m1_subset_1 :::"Function":::) "of" (Set (Var "X")) "," (Set (Var "Y")) "st" (Bool (Bool (Set (Var "F")) "is" ($#v3_binop_1 :::"idempotent"::: ) ) & (Bool (Set (Var "F")) "is" ($#v1_binop_1 :::"commutative"::: ) ) & (Bool (Set (Var "F")) "is" ($#v2_binop_1 :::"associative"::: ) )) "holds" (Bool "for" (Set (Var "a")) "," (Set (Var "b")) "," (Set (Var "c")) "being" ($#m1_subset_1 :::"Element"::: ) "of" (Set (Var "X")) "holds" (Bool (Set (Set (Var "F")) ($#k7_setwiseo :::"$$"::: ) "(" (Set ($#k4_setwiseo :::"{."::: ) (Set (Var "a")) "," (Set (Var "b")) "," (Set (Var "c")) ($#k4_setwiseo :::".}"::: ) ) "," (Set (Var "f")) ")" ) ($#r1_hidden :::"="::: ) (Set (Set (Var "F")) ($#k5_binop_1 :::"."::: ) "(" (Set "(" (Set (Var "F")) ($#k5_binop_1 :::"."::: ) "(" (Set "(" (Set (Var "f")) ($#k3_funct_2 :::"."::: ) (Set (Var "a")) ")" ) "," (Set "(" (Set (Var "f")) ($#k3_funct_2 :::"."::: ) (Set (Var "b")) ")" ) ")" ")" ) "," (Set "(" (Set (Var "f")) ($#k3_funct_2 :::"."::: ) (Set (Var "c")) ")" ) ")" )))))) ; theorem :: SETWISEO:20 (Bool "for" (Set (Var "Y")) "," (Set (Var "X")) "being" ($#~v1_xboole_0 "non" ($#v1_xboole_0 :::"empty"::: ) ) ($#m1_hidden :::"set"::: ) (Bool "for" (Set (Var "F")) "being" ($#m1_subset_1 :::"BinOp":::) "of" (Set (Var "Y")) (Bool "for" (Set (Var "B")) "being" ($#m1_subset_1 :::"Element"::: ) "of" (Set ($#k5_finsub_1 :::"Fin"::: ) (Set (Var "X"))) (Bool "for" (Set (Var "f")) "being" ($#m1_subset_1 :::"Function":::) "of" (Set (Var "X")) "," (Set (Var "Y")) "st" (Bool (Bool (Set (Var "F")) "is" ($#v3_binop_1 :::"idempotent"::: ) ) & (Bool (Set (Var "F")) "is" ($#v1_binop_1 :::"commutative"::: ) ) & (Bool (Set (Var "F")) "is" ($#v2_binop_1 :::"associative"::: ) ) & (Bool (Set (Var "B")) ($#r1_hidden :::"<>"::: ) (Set ($#k1_xboole_0 :::"{}"::: ) ))) "holds" (Bool "for" (Set (Var "x")) "being" ($#m1_subset_1 :::"Element"::: ) "of" (Set (Var "X")) "holds" (Bool (Set (Set (Var "F")) ($#k7_setwiseo :::"$$"::: ) "(" (Set "(" (Set (Var "B")) ($#k5_setwiseo :::"\/"::: ) (Set ($#k2_setwiseo :::"{."::: ) (Set (Var "x")) ($#k2_setwiseo :::".}"::: ) ) ")" ) "," (Set (Var "f")) ")" ) ($#r1_hidden :::"="::: ) (Set (Set (Var "F")) ($#k5_binop_1 :::"."::: ) "(" (Set "(" (Set (Var "F")) ($#k7_setwiseo :::"$$"::: ) "(" (Set (Var "B")) "," (Set (Var "f")) ")" ")" ) "," (Set "(" (Set (Var "f")) ($#k3_funct_2 :::"."::: ) (Set (Var "x")) ")" ) ")" ))))))) ; theorem :: SETWISEO:21 (Bool "for" (Set (Var "Y")) "," (Set (Var "X")) "being" ($#~v1_xboole_0 "non" ($#v1_xboole_0 :::"empty"::: ) ) ($#m1_hidden :::"set"::: ) (Bool "for" (Set (Var "F")) "being" ($#m1_subset_1 :::"BinOp":::) "of" (Set (Var "Y")) (Bool "for" (Set (Var "f")) "being" ($#m1_subset_1 :::"Function":::) "of" (Set (Var "X")) "," (Set (Var "Y")) "st" (Bool (Bool (Set (Var "F")) "is" ($#v3_binop_1 :::"idempotent"::: ) ) & (Bool (Set (Var "F")) "is" ($#v1_binop_1 :::"commutative"::: ) ) & (Bool (Set (Var "F")) "is" ($#v2_binop_1 :::"associative"::: ) )) "holds" (Bool "for" (Set (Var "B1")) "," (Set (Var "B2")) "being" ($#m1_subset_1 :::"Element"::: ) "of" (Set ($#k5_finsub_1 :::"Fin"::: ) (Set (Var "X"))) "st" (Bool (Bool (Set (Var "B1")) ($#r1_hidden :::"<>"::: ) (Set ($#k1_xboole_0 :::"{}"::: ) )) & (Bool (Set (Var "B2")) ($#r1_hidden :::"<>"::: ) (Set ($#k1_xboole_0 :::"{}"::: ) ))) "holds" (Bool (Set (Set (Var "F")) ($#k7_setwiseo :::"$$"::: ) "(" (Set "(" (Set (Var "B1")) ($#k5_setwiseo :::"\/"::: ) (Set (Var "B2")) ")" ) "," (Set (Var "f")) ")" ) ($#r1_hidden :::"="::: ) (Set (Set (Var "F")) ($#k5_binop_1 :::"."::: ) "(" (Set "(" (Set (Var "F")) ($#k7_setwiseo :::"$$"::: ) "(" (Set (Var "B1")) "," (Set (Var "f")) ")" ")" ) "," (Set "(" (Set (Var "F")) ($#k7_setwiseo :::"$$"::: ) "(" (Set (Var "B2")) "," (Set (Var "f")) ")" ")" ) ")" )))))) ; theorem :: SETWISEO:22 (Bool "for" (Set (Var "Y")) "," (Set (Var "X")) "being" ($#~v1_xboole_0 "non" ($#v1_xboole_0 :::"empty"::: ) ) ($#m1_hidden :::"set"::: ) (Bool "for" (Set (Var "F")) "being" ($#m1_subset_1 :::"BinOp":::) "of" (Set (Var "Y")) (Bool "for" (Set (Var "B")) "being" ($#m1_subset_1 :::"Element"::: ) "of" (Set ($#k5_finsub_1 :::"Fin"::: ) (Set (Var "X"))) (Bool "for" (Set (Var "f")) "being" ($#m1_subset_1 :::"Function":::) "of" (Set (Var "X")) "," (Set (Var "Y")) "st" (Bool (Bool (Set (Var "F")) "is" ($#v1_binop_1 :::"commutative"::: ) ) & (Bool (Set (Var "F")) "is" ($#v2_binop_1 :::"associative"::: ) ) & (Bool (Set (Var "F")) "is" ($#v3_binop_1 :::"idempotent"::: ) )) "holds" (Bool "for" (Set (Var "x")) "being" ($#m1_subset_1 :::"Element"::: ) "of" (Set (Var "X")) "st" (Bool (Bool (Set (Var "x")) ($#r2_hidden :::"in"::: ) (Set (Var "B")))) "holds" (Bool (Set (Set (Var "F")) ($#k5_binop_1 :::"."::: ) "(" (Set "(" (Set (Var "f")) ($#k3_funct_2 :::"."::: ) (Set (Var "x")) ")" ) "," (Set "(" (Set (Var "F")) ($#k7_setwiseo :::"$$"::: ) "(" (Set (Var "B")) "," (Set (Var "f")) ")" ")" ) ")" ) ($#r1_hidden :::"="::: ) (Set (Set (Var "F")) ($#k7_setwiseo :::"$$"::: ) "(" (Set (Var "B")) "," (Set (Var "f")) ")" ))))))) ; theorem :: SETWISEO:23 (Bool "for" (Set (Var "Y")) "," (Set (Var "X")) "being" ($#~v1_xboole_0 "non" ($#v1_xboole_0 :::"empty"::: ) ) ($#m1_hidden :::"set"::: ) (Bool "for" (Set (Var "F")) "being" ($#m1_subset_1 :::"BinOp":::) "of" (Set (Var "Y")) (Bool "for" (Set (Var "f")) "being" ($#m1_subset_1 :::"Function":::) "of" (Set (Var "X")) "," (Set (Var "Y")) "st" (Bool (Bool (Set (Var "F")) "is" ($#v1_binop_1 :::"commutative"::: ) ) & (Bool (Set (Var "F")) "is" ($#v2_binop_1 :::"associative"::: ) ) & (Bool (Set (Var "F")) "is" ($#v3_binop_1 :::"idempotent"::: ) )) "holds" (Bool "for" (Set (Var "B")) "," (Set (Var "C")) "being" ($#m1_subset_1 :::"Element"::: ) "of" (Set ($#k5_finsub_1 :::"Fin"::: ) (Set (Var "X"))) "st" (Bool (Bool (Set (Var "B")) ($#r1_hidden :::"<>"::: ) (Set ($#k1_xboole_0 :::"{}"::: ) )) & (Bool (Set (Var "B")) ($#r1_tarski :::"c="::: ) (Set (Var "C")))) "holds" (Bool (Set (Set (Var "F")) ($#k5_binop_1 :::"."::: ) "(" (Set "(" (Set (Var "F")) ($#k7_setwiseo :::"$$"::: ) "(" (Set (Var "B")) "," (Set (Var "f")) ")" ")" ) "," (Set "(" (Set (Var "F")) ($#k7_setwiseo :::"$$"::: ) "(" (Set (Var "C")) "," (Set (Var "f")) ")" ")" ) ")" ) ($#r1_hidden :::"="::: ) (Set (Set (Var "F")) ($#k7_setwiseo :::"$$"::: ) "(" (Set (Var "C")) "," (Set (Var "f")) ")" )))))) ; theorem :: SETWISEO:24 (Bool "for" (Set (Var "Y")) "," (Set (Var "X")) "being" ($#~v1_xboole_0 "non" ($#v1_xboole_0 :::"empty"::: ) ) ($#m1_hidden :::"set"::: ) (Bool "for" (Set (Var "F")) "being" ($#m1_subset_1 :::"BinOp":::) "of" (Set (Var "Y")) (Bool "for" (Set (Var "B")) "being" ($#m1_subset_1 :::"Element"::: ) "of" (Set ($#k5_finsub_1 :::"Fin"::: ) (Set (Var "X"))) (Bool "for" (Set (Var "f")) "being" ($#m1_subset_1 :::"Function":::) "of" (Set (Var "X")) "," (Set (Var "Y")) "st" (Bool (Bool (Set (Var "B")) ($#r1_hidden :::"<>"::: ) (Set ($#k1_xboole_0 :::"{}"::: ) )) & (Bool (Set (Var "F")) "is" ($#v1_binop_1 :::"commutative"::: ) ) & (Bool (Set (Var "F")) "is" ($#v2_binop_1 :::"associative"::: ) ) & (Bool (Set (Var "F")) "is" ($#v3_binop_1 :::"idempotent"::: ) )) "holds" (Bool "for" (Set (Var "a")) "being" ($#m1_subset_1 :::"Element"::: ) "of" (Set (Var "Y")) "st" (Bool (Bool "(" "for" (Set (Var "b")) "being" ($#m1_subset_1 :::"Element"::: ) "of" (Set (Var "X")) "st" (Bool (Bool (Set (Var "b")) ($#r2_hidden :::"in"::: ) (Set (Var "B")))) "holds" (Bool (Set (Set (Var "f")) ($#k3_funct_2 :::"."::: ) (Set (Var "b"))) ($#r1_hidden :::"="::: ) (Set (Var "a"))) ")" )) "holds" (Bool (Set (Set (Var "F")) ($#k7_setwiseo :::"$$"::: ) "(" (Set (Var "B")) "," (Set (Var "f")) ")" ) ($#r1_hidden :::"="::: ) (Set (Var "a")))))))) ; theorem :: SETWISEO:25 (Bool "for" (Set (Var "X")) "," (Set (Var "Y")) "being" ($#~v1_xboole_0 "non" ($#v1_xboole_0 :::"empty"::: ) ) ($#m1_hidden :::"set"::: ) (Bool "for" (Set (Var "F")) "being" ($#m1_subset_1 :::"BinOp":::) "of" (Set (Var "Y")) (Bool "for" (Set (Var "B")) "being" ($#m1_subset_1 :::"Element"::: ) "of" (Set ($#k5_finsub_1 :::"Fin"::: ) (Set (Var "X"))) (Bool "for" (Set (Var "f")) "being" ($#m1_subset_1 :::"Function":::) "of" (Set (Var "X")) "," (Set (Var "Y")) "st" (Bool (Bool (Set (Var "F")) "is" ($#v1_binop_1 :::"commutative"::: ) ) & (Bool (Set (Var "F")) "is" ($#v2_binop_1 :::"associative"::: ) ) & (Bool (Set (Var "F")) "is" ($#v3_binop_1 :::"idempotent"::: ) )) "holds" (Bool "for" (Set (Var "a")) "being" ($#m1_subset_1 :::"Element"::: ) "of" (Set (Var "Y")) "st" (Bool (Bool (Set (Set (Var "f")) ($#k7_relset_1 :::".:"::: ) (Set (Var "B"))) ($#r1_hidden :::"="::: ) (Set ($#k1_tarski :::"{"::: ) (Set (Var "a")) ($#k1_tarski :::"}"::: ) ))) "holds" (Bool (Set (Set (Var "F")) ($#k7_setwiseo :::"$$"::: ) "(" (Set (Var "B")) "," (Set (Var "f")) ")" ) ($#r1_hidden :::"="::: ) (Set (Var "a")))))))) ; theorem :: SETWISEO:26 (Bool "for" (Set (Var "X")) "," (Set (Var "Y")) "being" ($#~v1_xboole_0 "non" ($#v1_xboole_0 :::"empty"::: ) ) ($#m1_hidden :::"set"::: ) (Bool "for" (Set (Var "F")) "being" ($#m1_subset_1 :::"BinOp":::) "of" (Set (Var "Y")) "st" (Bool (Bool (Set (Var "F")) "is" ($#v1_binop_1 :::"commutative"::: ) ) & (Bool (Set (Var "F")) "is" ($#v2_binop_1 :::"associative"::: ) ) & (Bool (Set (Var "F")) "is" ($#v3_binop_1 :::"idempotent"::: ) )) "holds" (Bool "for" (Set (Var "f")) "," (Set (Var "g")) "being" ($#m1_subset_1 :::"Function":::) "of" (Set (Var "X")) "," (Set (Var "Y")) (Bool "for" (Set (Var "A")) "," (Set (Var "B")) "being" ($#m1_subset_1 :::"Element"::: ) "of" (Set ($#k5_finsub_1 :::"Fin"::: ) (Set (Var "X"))) "st" (Bool (Bool (Set (Var "A")) ($#r1_hidden :::"<>"::: ) (Set ($#k1_xboole_0 :::"{}"::: ) )) & (Bool (Set (Set (Var "f")) ($#k7_relset_1 :::".:"::: ) (Set (Var "A"))) ($#r1_hidden :::"="::: ) (Set (Set (Var "g")) ($#k7_relset_1 :::".:"::: ) (Set (Var "B"))))) "holds" (Bool (Set (Set (Var "F")) ($#k7_setwiseo :::"$$"::: ) "(" (Set (Var "A")) "," (Set (Var "f")) ")" ) ($#r1_hidden :::"="::: ) (Set (Set (Var "F")) ($#k7_setwiseo :::"$$"::: ) "(" (Set (Var "B")) "," (Set (Var "g")) ")" )))))) ; theorem :: SETWISEO:27 (Bool "for" (Set (Var "Y")) "," (Set (Var "X")) "being" ($#~v1_xboole_0 "non" ($#v1_xboole_0 :::"empty"::: ) ) ($#m1_hidden :::"set"::: ) (Bool "for" (Set (Var "F")) "," (Set (Var "G")) "being" ($#m1_subset_1 :::"BinOp":::) "of" (Set (Var "Y")) "st" (Bool (Bool (Set (Var "F")) "is" ($#v3_binop_1 :::"idempotent"::: ) ) & (Bool (Set (Var "F")) "is" ($#v1_binop_1 :::"commutative"::: ) ) & (Bool (Set (Var "F")) "is" ($#v2_binop_1 :::"associative"::: ) ) & (Bool (Set (Var "G")) ($#r6_binop_1 :::"is_distributive_wrt"::: ) (Set (Var "F")))) "holds" (Bool "for" (Set (Var "B")) "being" ($#m1_subset_1 :::"Element"::: ) "of" (Set ($#k5_finsub_1 :::"Fin"::: ) (Set (Var "X"))) "st" (Bool (Bool (Set (Var "B")) ($#r1_hidden :::"<>"::: ) (Set ($#k1_xboole_0 :::"{}"::: ) ))) "holds" (Bool "for" (Set (Var "f")) "being" ($#m1_subset_1 :::"Function":::) "of" (Set (Var "X")) "," (Set (Var "Y")) (Bool "for" (Set (Var "a")) "being" ($#m1_subset_1 :::"Element"::: ) "of" (Set (Var "Y")) "holds" (Bool (Set (Set (Var "G")) ($#k5_binop_1 :::"."::: ) "(" (Set (Var "a")) "," (Set "(" (Set (Var "F")) ($#k7_setwiseo :::"$$"::: ) "(" (Set (Var "B")) "," (Set (Var "f")) ")" ")" ) ")" ) ($#r1_hidden :::"="::: ) (Set (Set (Var "F")) ($#k7_setwiseo :::"$$"::: ) "(" (Set (Var "B")) "," (Set "(" (Set (Var "G")) ($#k10_funcop_1 :::"[;]"::: ) "(" (Set (Var "a")) "," (Set (Var "f")) ")" ")" ) ")" ))))))) ; theorem :: SETWISEO:28 (Bool "for" (Set (Var "Y")) "," (Set (Var "X")) "being" ($#~v1_xboole_0 "non" ($#v1_xboole_0 :::"empty"::: ) ) ($#m1_hidden :::"set"::: ) (Bool "for" (Set (Var "F")) "," (Set (Var "G")) "being" ($#m1_subset_1 :::"BinOp":::) "of" (Set (Var "Y")) "st" (Bool (Bool (Set (Var "F")) "is" ($#v3_binop_1 :::"idempotent"::: ) ) & (Bool (Set (Var "F")) "is" ($#v1_binop_1 :::"commutative"::: ) ) & (Bool (Set (Var "F")) "is" ($#v2_binop_1 :::"associative"::: ) ) & (Bool (Set (Var "G")) ($#r6_binop_1 :::"is_distributive_wrt"::: ) (Set (Var "F")))) "holds" (Bool "for" (Set (Var "B")) "being" ($#m1_subset_1 :::"Element"::: ) "of" (Set ($#k5_finsub_1 :::"Fin"::: ) (Set (Var "X"))) "st" (Bool (Bool (Set (Var "B")) ($#r1_hidden :::"<>"::: ) (Set ($#k1_xboole_0 :::"{}"::: ) ))) "holds" (Bool "for" (Set (Var "f")) "being" ($#m1_subset_1 :::"Function":::) "of" (Set (Var "X")) "," (Set (Var "Y")) (Bool "for" (Set (Var "a")) "being" ($#m1_subset_1 :::"Element"::: ) "of" (Set (Var "Y")) "holds" (Bool (Set (Set (Var "G")) ($#k5_binop_1 :::"."::: ) "(" (Set "(" (Set (Var "F")) ($#k7_setwiseo :::"$$"::: ) "(" (Set (Var "B")) "," (Set (Var "f")) ")" ")" ) "," (Set (Var "a")) ")" ) ($#r1_hidden :::"="::: ) (Set (Set (Var "F")) ($#k7_setwiseo :::"$$"::: ) "(" (Set (Var "B")) "," (Set "(" (Set (Var "G")) ($#k9_funcop_1 :::"[:]"::: ) "(" (Set (Var "f")) "," (Set (Var "a")) ")" ")" ) ")" ))))))) ; definitionlet "X", "Y" be ($#~v1_xboole_0 "non" ($#v1_xboole_0 :::"empty"::: ) ) ($#m1_hidden :::"set"::: ) ; let "f" be ($#m1_subset_1 :::"Function":::) "of" (Set (Const "X")) "," (Set (Const "Y")); let "A" be ($#m1_subset_1 :::"Element"::: ) "of" (Set ($#k5_finsub_1 :::"Fin"::: ) (Set (Const "X"))); :: original: :::".:"::: redefine func "f" :::".:"::: "A" -> ($#m1_subset_1 :::"Element"::: ) "of" (Set ($#k5_finsub_1 :::"Fin"::: ) "Y"); end; theorem :: SETWISEO:29 (Bool "for" (Set (Var "A")) "," (Set (Var "X")) "," (Set (Var "Y")) "being" ($#~v1_xboole_0 "non" ($#v1_xboole_0 :::"empty"::: ) ) ($#m1_hidden :::"set"::: ) (Bool "for" (Set (Var "F")) "being" ($#m1_subset_1 :::"BinOp":::) "of" (Set (Var "A")) "st" (Bool (Bool (Set (Var "F")) "is" ($#v3_binop_1 :::"idempotent"::: ) ) & (Bool (Set (Var "F")) "is" ($#v1_binop_1 :::"commutative"::: ) ) & (Bool (Set (Var "F")) "is" ($#v2_binop_1 :::"associative"::: ) )) "holds" (Bool "for" (Set (Var "B")) "being" ($#m1_subset_1 :::"Element"::: ) "of" (Set ($#k5_finsub_1 :::"Fin"::: ) (Set (Var "X"))) "st" (Bool (Bool (Set (Var "B")) ($#r1_hidden :::"<>"::: ) (Set ($#k1_xboole_0 :::"{}"::: ) ))) "holds" (Bool "for" (Set (Var "f")) "being" ($#m1_subset_1 :::"Function":::) "of" (Set (Var "X")) "," (Set (Var "Y")) (Bool "for" (Set (Var "g")) "being" ($#m1_subset_1 :::"Function":::) "of" (Set (Var "Y")) "," (Set (Var "A")) "holds" (Bool (Set (Set (Var "F")) ($#k7_setwiseo :::"$$"::: ) "(" (Set "(" (Set (Var "f")) ($#k8_setwiseo :::".:"::: ) (Set (Var "B")) ")" ) "," (Set (Var "g")) ")" ) ($#r1_hidden :::"="::: ) (Set (Set (Var "F")) ($#k7_setwiseo :::"$$"::: ) "(" (Set (Var "B")) "," (Set "(" (Set (Var "g")) ($#k1_partfun1 :::"*"::: ) (Set (Var "f")) ")" ) ")" ))))))) ; theorem :: SETWISEO:30 (Bool "for" (Set (Var "X")) "," (Set (Var "Y")) "being" ($#~v1_xboole_0 "non" ($#v1_xboole_0 :::"empty"::: ) ) ($#m1_hidden :::"set"::: ) (Bool "for" (Set (Var "F")) "being" ($#m1_subset_1 :::"BinOp":::) "of" (Set (Var "Y")) "st" (Bool (Bool (Set (Var "F")) "is" ($#v1_binop_1 :::"commutative"::: ) ) & (Bool (Set (Var "F")) "is" ($#v2_binop_1 :::"associative"::: ) ) & (Bool (Set (Var "F")) "is" ($#v3_binop_1 :::"idempotent"::: ) )) "holds" (Bool "for" (Set (Var "Z")) "being" ($#~v1_xboole_0 "non" ($#v1_xboole_0 :::"empty"::: ) ) ($#m1_hidden :::"set"::: ) (Bool "for" (Set (Var "G")) "being" ($#m1_subset_1 :::"BinOp":::) "of" (Set (Var "Z")) "st" (Bool (Bool (Set (Var "G")) "is" ($#v1_binop_1 :::"commutative"::: ) ) & (Bool (Set (Var "G")) "is" ($#v2_binop_1 :::"associative"::: ) ) & (Bool (Set (Var "G")) "is" ($#v3_binop_1 :::"idempotent"::: ) )) "holds" (Bool "for" (Set (Var "f")) "being" ($#m1_subset_1 :::"Function":::) "of" (Set (Var "X")) "," (Set (Var "Y")) (Bool "for" (Set (Var "g")) "being" ($#m1_subset_1 :::"Function":::) "of" (Set (Var "Y")) "," (Set (Var "Z")) "st" (Bool (Bool "(" "for" (Set (Var "x")) "," (Set (Var "y")) "being" ($#m1_subset_1 :::"Element"::: ) "of" (Set (Var "Y")) "holds" (Bool (Set (Set (Var "g")) ($#k3_funct_2 :::"."::: ) (Set "(" (Set (Var "F")) ($#k5_binop_1 :::"."::: ) "(" (Set (Var "x")) "," (Set (Var "y")) ")" ")" )) ($#r1_hidden :::"="::: ) (Set (Set (Var "G")) ($#k5_binop_1 :::"."::: ) "(" (Set "(" (Set (Var "g")) ($#k3_funct_2 :::"."::: ) (Set (Var "x")) ")" ) "," (Set "(" (Set (Var "g")) ($#k3_funct_2 :::"."::: ) (Set (Var "y")) ")" ) ")" )) ")" )) "holds" (Bool "for" (Set (Var "B")) "being" ($#m1_subset_1 :::"Element"::: ) "of" (Set ($#k5_finsub_1 :::"Fin"::: ) (Set (Var "X"))) "st" (Bool (Bool (Set (Var "B")) ($#r1_hidden :::"<>"::: ) (Set ($#k1_xboole_0 :::"{}"::: ) ))) "holds" (Bool (Set (Set (Var "g")) ($#k3_funct_2 :::"."::: ) (Set "(" (Set (Var "F")) ($#k7_setwiseo :::"$$"::: ) "(" (Set (Var "B")) "," (Set (Var "f")) ")" ")" )) ($#r1_hidden :::"="::: ) (Set (Set (Var "G")) ($#k7_setwiseo :::"$$"::: ) "(" (Set (Var "B")) "," (Set "(" (Set (Var "g")) ($#k1_partfun1 :::"*"::: ) (Set (Var "f")) ")" ) ")" ))))))))) ; theorem :: SETWISEO:31 (Bool "for" (Set (Var "Y")) "," (Set (Var "X")) "being" ($#~v1_xboole_0 "non" ($#v1_xboole_0 :::"empty"::: ) ) ($#m1_hidden :::"set"::: ) (Bool "for" (Set (Var "F")) "being" ($#m1_subset_1 :::"BinOp":::) "of" (Set (Var "Y")) "st" (Bool (Bool (Set (Var "F")) "is" ($#v1_binop_1 :::"commutative"::: ) ) & (Bool (Set (Var "F")) "is" ($#v2_binop_1 :::"associative"::: ) ) & (Bool (Set (Var "F")) "is" ($#v1_setwiseo :::"having_a_unity"::: ) )) "holds" (Bool "for" (Set (Var "f")) "being" ($#m1_subset_1 :::"Function":::) "of" (Set (Var "X")) "," (Set (Var "Y")) "holds" (Bool (Set (Set (Var "F")) ($#k7_setwiseo :::"$$"::: ) "(" (Set "(" ($#k1_setwiseo :::"{}."::: ) (Set (Var "X")) ")" ) "," (Set (Var "f")) ")" ) ($#r1_hidden :::"="::: ) (Set ($#k4_binop_1 :::"the_unity_wrt"::: ) (Set (Var "F"))))))) ; theorem :: SETWISEO:32 (Bool "for" (Set (Var "Y")) "," (Set (Var "X")) "being" ($#~v1_xboole_0 "non" ($#v1_xboole_0 :::"empty"::: ) ) ($#m1_hidden :::"set"::: ) (Bool "for" (Set (Var "F")) "being" ($#m1_subset_1 :::"BinOp":::) "of" (Set (Var "Y")) (Bool "for" (Set (Var "B")) "being" ($#m1_subset_1 :::"Element"::: ) "of" (Set ($#k5_finsub_1 :::"Fin"::: ) (Set (Var "X"))) (Bool "for" (Set (Var "f")) "being" ($#m1_subset_1 :::"Function":::) "of" (Set (Var "X")) "," (Set (Var "Y")) "st" (Bool (Bool (Set (Var "F")) "is" ($#v3_binop_1 :::"idempotent"::: ) ) & (Bool (Set (Var "F")) "is" ($#v1_binop_1 :::"commutative"::: ) ) & (Bool (Set (Var "F")) "is" ($#v2_binop_1 :::"associative"::: ) ) & (Bool (Set (Var "F")) "is" ($#v1_setwiseo :::"having_a_unity"::: ) )) "holds" (Bool "for" (Set (Var "x")) "being" ($#m1_subset_1 :::"Element"::: ) "of" (Set (Var "X")) "holds" (Bool (Set (Set (Var "F")) ($#k7_setwiseo :::"$$"::: ) "(" (Set "(" (Set (Var "B")) ($#k5_setwiseo :::"\/"::: ) (Set ($#k2_setwiseo :::"{."::: ) (Set (Var "x")) ($#k2_setwiseo :::".}"::: ) ) ")" ) "," (Set (Var "f")) ")" ) ($#r1_hidden :::"="::: ) (Set (Set (Var "F")) ($#k5_binop_1 :::"."::: ) "(" (Set "(" (Set (Var "F")) ($#k7_setwiseo :::"$$"::: ) "(" (Set (Var "B")) "," (Set (Var "f")) ")" ")" ) "," (Set "(" (Set (Var "f")) ($#k3_funct_2 :::"."::: ) (Set (Var "x")) ")" ) ")" ))))))) ; theorem :: SETWISEO:33 (Bool "for" (Set (Var "Y")) "," (Set (Var "X")) "being" ($#~v1_xboole_0 "non" ($#v1_xboole_0 :::"empty"::: ) ) ($#m1_hidden :::"set"::: ) (Bool "for" (Set (Var "F")) "being" ($#m1_subset_1 :::"BinOp":::) "of" (Set (Var "Y")) (Bool "for" (Set (Var "f")) "being" ($#m1_subset_1 :::"Function":::) "of" (Set (Var "X")) "," (Set (Var "Y")) "st" (Bool (Bool (Set (Var "F")) "is" ($#v3_binop_1 :::"idempotent"::: ) ) & (Bool (Set (Var "F")) "is" ($#v1_binop_1 :::"commutative"::: ) ) & (Bool (Set (Var "F")) "is" ($#v2_binop_1 :::"associative"::: ) ) & (Bool (Set (Var "F")) "is" ($#v1_setwiseo :::"having_a_unity"::: ) )) "holds" (Bool "for" (Set (Var "B1")) "," (Set (Var "B2")) "being" ($#m1_subset_1 :::"Element"::: ) "of" (Set ($#k5_finsub_1 :::"Fin"::: ) (Set (Var "X"))) "holds" (Bool (Set (Set (Var "F")) ($#k7_setwiseo :::"$$"::: ) "(" (Set "(" (Set (Var "B1")) ($#k5_setwiseo :::"\/"::: ) (Set (Var "B2")) ")" ) "," (Set (Var "f")) ")" ) ($#r1_hidden :::"="::: ) (Set (Set (Var "F")) ($#k5_binop_1 :::"."::: ) "(" (Set "(" (Set (Var "F")) ($#k7_setwiseo :::"$$"::: ) "(" (Set (Var "B1")) "," (Set (Var "f")) ")" ")" ) "," (Set "(" (Set (Var "F")) ($#k7_setwiseo :::"$$"::: ) "(" (Set (Var "B2")) "," (Set (Var "f")) ")" ")" ) ")" )))))) ; theorem :: SETWISEO:34 (Bool "for" (Set (Var "X")) "," (Set (Var "Y")) "being" ($#~v1_xboole_0 "non" ($#v1_xboole_0 :::"empty"::: ) ) ($#m1_hidden :::"set"::: ) (Bool "for" (Set (Var "F")) "being" ($#m1_subset_1 :::"BinOp":::) "of" (Set (Var "Y")) "st" (Bool (Bool (Set (Var "F")) "is" ($#v1_binop_1 :::"commutative"::: ) ) & (Bool (Set (Var "F")) "is" ($#v2_binop_1 :::"associative"::: ) ) & (Bool (Set (Var "F")) "is" ($#v3_binop_1 :::"idempotent"::: ) ) & (Bool (Set (Var "F")) "is" ($#v1_setwiseo :::"having_a_unity"::: ) )) "holds" (Bool "for" (Set (Var "f")) "," (Set (Var "g")) "being" ($#m1_subset_1 :::"Function":::) "of" (Set (Var "X")) "," (Set (Var "Y")) (Bool "for" (Set (Var "A")) "," (Set (Var "B")) "being" ($#m1_subset_1 :::"Element"::: ) "of" (Set ($#k5_finsub_1 :::"Fin"::: ) (Set (Var "X"))) "st" (Bool (Bool (Set (Set (Var "f")) ($#k8_setwiseo :::".:"::: ) (Set (Var "A"))) ($#r1_hidden :::"="::: ) (Set (Set (Var "g")) ($#k8_setwiseo :::".:"::: ) (Set (Var "B"))))) "holds" (Bool (Set (Set (Var "F")) ($#k7_setwiseo :::"$$"::: ) "(" (Set (Var "A")) "," (Set (Var "f")) ")" ) ($#r1_hidden :::"="::: ) (Set (Set (Var "F")) ($#k7_setwiseo :::"$$"::: ) "(" (Set (Var "B")) "," (Set (Var "g")) ")" )))))) ; theorem :: SETWISEO:35 (Bool "for" (Set (Var "A")) "," (Set (Var "X")) "," (Set (Var "Y")) "being" ($#~v1_xboole_0 "non" ($#v1_xboole_0 :::"empty"::: ) ) ($#m1_hidden :::"set"::: ) (Bool "for" (Set (Var "F")) "being" ($#m1_subset_1 :::"BinOp":::) "of" (Set (Var "A")) "st" (Bool (Bool (Set (Var "F")) "is" ($#v3_binop_1 :::"idempotent"::: ) ) & (Bool (Set (Var "F")) "is" ($#v1_binop_1 :::"commutative"::: ) ) & (Bool (Set (Var "F")) "is" ($#v2_binop_1 :::"associative"::: ) ) & (Bool (Set (Var "F")) "is" ($#v1_setwiseo :::"having_a_unity"::: ) )) "holds" (Bool "for" (Set (Var "B")) "being" ($#m1_subset_1 :::"Element"::: ) "of" (Set ($#k5_finsub_1 :::"Fin"::: ) (Set (Var "X"))) (Bool "for" (Set (Var "f")) "being" ($#m1_subset_1 :::"Function":::) "of" (Set (Var "X")) "," (Set (Var "Y")) (Bool "for" (Set (Var "g")) "being" ($#m1_subset_1 :::"Function":::) "of" (Set (Var "Y")) "," (Set (Var "A")) "holds" (Bool (Set (Set (Var "F")) ($#k7_setwiseo :::"$$"::: ) "(" (Set "(" (Set (Var "f")) ($#k8_setwiseo :::".:"::: ) (Set (Var "B")) ")" ) "," (Set (Var "g")) ")" ) ($#r1_hidden :::"="::: ) (Set (Set (Var "F")) ($#k7_setwiseo :::"$$"::: ) "(" (Set (Var "B")) "," (Set "(" (Set (Var "g")) ($#k1_partfun1 :::"*"::: ) (Set (Var "f")) ")" ) ")" ))))))) ; theorem :: SETWISEO:36 (Bool "for" (Set (Var "X")) "," (Set (Var "Y")) "being" ($#~v1_xboole_0 "non" ($#v1_xboole_0 :::"empty"::: ) ) ($#m1_hidden :::"set"::: ) (Bool "for" (Set (Var "F")) "being" ($#m1_subset_1 :::"BinOp":::) "of" (Set (Var "Y")) "st" (Bool (Bool (Set (Var "F")) "is" ($#v1_binop_1 :::"commutative"::: ) ) & (Bool (Set (Var "F")) "is" ($#v2_binop_1 :::"associative"::: ) ) & (Bool (Set (Var "F")) "is" ($#v3_binop_1 :::"idempotent"::: ) ) & (Bool (Set (Var "F")) "is" ($#v1_setwiseo :::"having_a_unity"::: ) )) "holds" (Bool "for" (Set (Var "Z")) "being" ($#~v1_xboole_0 "non" ($#v1_xboole_0 :::"empty"::: ) ) ($#m1_hidden :::"set"::: ) (Bool "for" (Set (Var "G")) "being" ($#m1_subset_1 :::"BinOp":::) "of" (Set (Var "Z")) "st" (Bool (Bool (Set (Var "G")) "is" ($#v1_binop_1 :::"commutative"::: ) ) & (Bool (Set (Var "G")) "is" ($#v2_binop_1 :::"associative"::: ) ) & (Bool (Set (Var "G")) "is" ($#v3_binop_1 :::"idempotent"::: ) ) & (Bool (Set (Var "G")) "is" ($#v1_setwiseo :::"having_a_unity"::: ) )) "holds" (Bool "for" (Set (Var "f")) "being" ($#m1_subset_1 :::"Function":::) "of" (Set (Var "X")) "," (Set (Var "Y")) (Bool "for" (Set (Var "g")) "being" ($#m1_subset_1 :::"Function":::) "of" (Set (Var "Y")) "," (Set (Var "Z")) "st" (Bool (Bool (Set (Set (Var "g")) ($#k3_funct_2 :::"."::: ) (Set "(" ($#k4_binop_1 :::"the_unity_wrt"::: ) (Set (Var "F")) ")" )) ($#r1_hidden :::"="::: ) (Set ($#k4_binop_1 :::"the_unity_wrt"::: ) (Set (Var "G")))) & (Bool "(" "for" (Set (Var "x")) "," (Set (Var "y")) "being" ($#m1_subset_1 :::"Element"::: ) "of" (Set (Var "Y")) "holds" (Bool (Set (Set (Var "g")) ($#k3_funct_2 :::"."::: ) (Set "(" (Set (Var "F")) ($#k5_binop_1 :::"."::: ) "(" (Set (Var "x")) "," (Set (Var "y")) ")" ")" )) ($#r1_hidden :::"="::: ) (Set (Set (Var "G")) ($#k5_binop_1 :::"."::: ) "(" (Set "(" (Set (Var "g")) ($#k3_funct_2 :::"."::: ) (Set (Var "x")) ")" ) "," (Set "(" (Set (Var "g")) ($#k3_funct_2 :::"."::: ) (Set (Var "y")) ")" ) ")" )) ")" )) "holds" (Bool "for" (Set (Var "B")) "being" ($#m1_subset_1 :::"Element"::: ) "of" (Set ($#k5_finsub_1 :::"Fin"::: ) (Set (Var "X"))) "holds" (Bool (Set (Set (Var "g")) ($#k3_funct_2 :::"."::: ) (Set "(" (Set (Var "F")) ($#k7_setwiseo :::"$$"::: ) "(" (Set (Var "B")) "," (Set (Var "f")) ")" ")" )) ($#r1_hidden :::"="::: ) (Set (Set (Var "G")) ($#k7_setwiseo :::"$$"::: ) "(" (Set (Var "B")) "," (Set "(" (Set (Var "g")) ($#k1_partfun1 :::"*"::: ) (Set (Var "f")) ")" ) ")" ))))))))) ; definitionlet "A" be ($#m1_hidden :::"set"::: ) ; func :::"FinUnion"::: "A" -> ($#m1_subset_1 :::"BinOp":::) "of" (Set "(" ($#k5_finsub_1 :::"Fin"::: ) "A" ")" ) means :: SETWISEO:def 4 (Bool "for" (Set (Var "x")) "," (Set (Var "y")) "being" ($#m1_subset_1 :::"Element"::: ) "of" (Set ($#k5_finsub_1 :::"Fin"::: ) "A") "holds" (Bool (Set it ($#k5_binop_1 :::"."::: ) "(" (Set (Var "x")) "," (Set (Var "y")) ")" ) ($#r1_hidden :::"="::: ) (Set (Set (Var "x")) ($#k5_setwiseo :::"\/"::: ) (Set (Var "y"))))); end; :: deftheorem defines :::"FinUnion"::: SETWISEO:def 4 : (Bool "for" (Set (Var "A")) "being" ($#m1_hidden :::"set"::: ) (Bool "for" (Set (Var "b2")) "being" ($#m1_subset_1 :::"BinOp":::) "of" (Set "(" ($#k5_finsub_1 :::"Fin"::: ) (Set (Var "A")) ")" ) "holds" (Bool "(" (Bool (Set (Var "b2")) ($#r1_hidden :::"="::: ) (Set ($#k9_setwiseo :::"FinUnion"::: ) (Set (Var "A")))) "iff" (Bool "for" (Set (Var "x")) "," (Set (Var "y")) "being" ($#m1_subset_1 :::"Element"::: ) "of" (Set ($#k5_finsub_1 :::"Fin"::: ) (Set (Var "A"))) "holds" (Bool (Set (Set (Var "b2")) ($#k5_binop_1 :::"."::: ) "(" (Set (Var "x")) "," (Set (Var "y")) ")" ) ($#r1_hidden :::"="::: ) (Set (Set (Var "x")) ($#k5_setwiseo :::"\/"::: ) (Set (Var "y"))))) ")" ))); theorem :: SETWISEO:37 (Bool "for" (Set (Var "A")) "being" ($#m1_hidden :::"set"::: ) "holds" (Bool (Set ($#k9_setwiseo :::"FinUnion"::: ) (Set (Var "A"))) "is" ($#v3_binop_1 :::"idempotent"::: ) )) ; theorem :: SETWISEO:38 (Bool "for" (Set (Var "A")) "being" ($#m1_hidden :::"set"::: ) "holds" (Bool (Set ($#k9_setwiseo :::"FinUnion"::: ) (Set (Var "A"))) "is" ($#v1_binop_1 :::"commutative"::: ) )) ; theorem :: SETWISEO:39 (Bool "for" (Set (Var "A")) "being" ($#m1_hidden :::"set"::: ) "holds" (Bool (Set ($#k9_setwiseo :::"FinUnion"::: ) (Set (Var "A"))) "is" ($#v2_binop_1 :::"associative"::: ) )) ; theorem :: SETWISEO:40 (Bool "for" (Set (Var "A")) "being" ($#m1_hidden :::"set"::: ) "holds" (Bool (Set ($#k1_setwiseo :::"{}."::: ) (Set (Var "A"))) ($#r3_binop_1 :::"is_a_unity_wrt"::: ) (Set ($#k9_setwiseo :::"FinUnion"::: ) (Set (Var "A"))))) ; theorem :: SETWISEO:41 (Bool "for" (Set (Var "A")) "being" ($#m1_hidden :::"set"::: ) "holds" (Bool (Set ($#k9_setwiseo :::"FinUnion"::: ) (Set (Var "A"))) "is" ($#v1_setwiseo :::"having_a_unity"::: ) )) ; theorem :: SETWISEO:42 (Bool "for" (Set (Var "A")) "being" ($#m1_hidden :::"set"::: ) "holds" (Bool (Set ($#k4_binop_1 :::"the_unity_wrt"::: ) (Set "(" ($#k9_setwiseo :::"FinUnion"::: ) (Set (Var "A")) ")" )) ($#r3_binop_1 :::"is_a_unity_wrt"::: ) (Set ($#k9_setwiseo :::"FinUnion"::: ) (Set (Var "A"))))) ; theorem :: SETWISEO:43 (Bool "for" (Set (Var "A")) "being" ($#m1_hidden :::"set"::: ) "holds" (Bool (Set ($#k4_binop_1 :::"the_unity_wrt"::: ) (Set "(" ($#k9_setwiseo :::"FinUnion"::: ) (Set (Var "A")) ")" )) ($#r1_hidden :::"="::: ) (Set ($#k1_xboole_0 :::"{}"::: ) ))) ; definitionlet "X" be ($#~v1_xboole_0 "non" ($#v1_xboole_0 :::"empty"::: ) ) ($#m1_hidden :::"set"::: ) ; let "A" be ($#m1_hidden :::"set"::: ) ; let "B" be ($#m1_subset_1 :::"Element"::: ) "of" (Set ($#k5_finsub_1 :::"Fin"::: ) (Set (Const "X"))); let "f" be ($#m1_subset_1 :::"Function":::) "of" (Set (Const "X")) "," (Set "(" ($#k5_finsub_1 :::"Fin"::: ) (Set (Const "A")) ")" ); func :::"FinUnion"::: "(" "B" "," "f" ")" -> ($#m1_subset_1 :::"Element"::: ) "of" (Set ($#k5_finsub_1 :::"Fin"::: ) "A") equals :: SETWISEO:def 5 (Set (Set "(" ($#k9_setwiseo :::"FinUnion"::: ) "A" ")" ) ($#k7_setwiseo :::"$$"::: ) "(" "B" "," "f" ")" ); end; :: deftheorem defines :::"FinUnion"::: SETWISEO:def 5 : (Bool "for" (Set (Var "X")) "being" ($#~v1_xboole_0 "non" ($#v1_xboole_0 :::"empty"::: ) ) ($#m1_hidden :::"set"::: ) (Bool "for" (Set (Var "A")) "being" ($#m1_hidden :::"set"::: ) (Bool "for" (Set (Var "B")) "being" ($#m1_subset_1 :::"Element"::: ) "of" (Set ($#k5_finsub_1 :::"Fin"::: ) (Set (Var "X"))) (Bool "for" (Set (Var "f")) "being" ($#m1_subset_1 :::"Function":::) "of" (Set (Var "X")) "," (Set "(" ($#k5_finsub_1 :::"Fin"::: ) (Set (Var "A")) ")" ) "holds" (Bool (Set ($#k10_setwiseo :::"FinUnion"::: ) "(" (Set (Var "B")) "," (Set (Var "f")) ")" ) ($#r1_hidden :::"="::: ) (Set (Set "(" ($#k9_setwiseo :::"FinUnion"::: ) (Set (Var "A")) ")" ) ($#k7_setwiseo :::"$$"::: ) "(" (Set (Var "B")) "," (Set (Var "f")) ")" )))))); theorem :: SETWISEO:44 (Bool "for" (Set (Var "X")) "being" ($#~v1_xboole_0 "non" ($#v1_xboole_0 :::"empty"::: ) ) ($#m1_hidden :::"set"::: ) (Bool "for" (Set (Var "A")) "being" ($#m1_hidden :::"set"::: ) (Bool "for" (Set (Var "f")) "being" ($#m1_subset_1 :::"Function":::) "of" (Set (Var "X")) "," (Set "(" ($#k5_finsub_1 :::"Fin"::: ) (Set (Var "A")) ")" ) (Bool "for" (Set (Var "i")) "being" ($#m1_subset_1 :::"Element"::: ) "of" (Set (Var "X")) "holds" (Bool (Set ($#k10_setwiseo :::"FinUnion"::: ) "(" (Set ($#k2_setwiseo :::"{."::: ) (Set (Var "i")) ($#k2_setwiseo :::".}"::: ) ) "," (Set (Var "f")) ")" ) ($#r1_hidden :::"="::: ) (Set (Set (Var "f")) ($#k3_funct_2 :::"."::: ) (Set (Var "i")))))))) ; theorem :: SETWISEO:45 (Bool "for" (Set (Var "X")) "being" ($#~v1_xboole_0 "non" ($#v1_xboole_0 :::"empty"::: ) ) ($#m1_hidden :::"set"::: ) (Bool "for" (Set (Var "A")) "being" ($#m1_hidden :::"set"::: ) (Bool "for" (Set (Var "f")) "being" ($#m1_subset_1 :::"Function":::) "of" (Set (Var "X")) "," (Set "(" ($#k5_finsub_1 :::"Fin"::: ) (Set (Var "A")) ")" ) (Bool "for" (Set (Var "i")) "," (Set (Var "j")) "being" ($#m1_subset_1 :::"Element"::: ) "of" (Set (Var "X")) "holds" (Bool (Set ($#k10_setwiseo :::"FinUnion"::: ) "(" (Set ($#k3_setwiseo :::"{."::: ) (Set (Var "i")) "," (Set (Var "j")) ($#k3_setwiseo :::".}"::: ) ) "," (Set (Var "f")) ")" ) ($#r1_hidden :::"="::: ) (Set (Set "(" (Set (Var "f")) ($#k3_funct_2 :::"."::: ) (Set (Var "i")) ")" ) ($#k5_setwiseo :::"\/"::: ) (Set "(" (Set (Var "f")) ($#k3_funct_2 :::"."::: ) (Set (Var "j")) ")" ))))))) ; theorem :: SETWISEO:46 (Bool "for" (Set (Var "X")) "being" ($#~v1_xboole_0 "non" ($#v1_xboole_0 :::"empty"::: ) ) ($#m1_hidden :::"set"::: ) (Bool "for" (Set (Var "A")) "being" ($#m1_hidden :::"set"::: ) (Bool "for" (Set (Var "f")) "being" ($#m1_subset_1 :::"Function":::) "of" (Set (Var "X")) "," (Set "(" ($#k5_finsub_1 :::"Fin"::: ) (Set (Var "A")) ")" ) (Bool "for" (Set (Var "i")) "," (Set (Var "j")) "," (Set (Var "k")) "being" ($#m1_subset_1 :::"Element"::: ) "of" (Set (Var "X")) "holds" (Bool (Set ($#k10_setwiseo :::"FinUnion"::: ) "(" (Set ($#k4_setwiseo :::"{."::: ) (Set (Var "i")) "," (Set (Var "j")) "," (Set (Var "k")) ($#k4_setwiseo :::".}"::: ) ) "," (Set (Var "f")) ")" ) ($#r1_hidden :::"="::: ) (Set (Set "(" (Set "(" (Set (Var "f")) ($#k3_funct_2 :::"."::: ) (Set (Var "i")) ")" ) ($#k5_setwiseo :::"\/"::: ) (Set "(" (Set (Var "f")) ($#k3_funct_2 :::"."::: ) (Set (Var "j")) ")" ) ")" ) ($#k5_setwiseo :::"\/"::: ) (Set "(" (Set (Var "f")) ($#k3_funct_2 :::"."::: ) (Set (Var "k")) ")" ))))))) ; theorem :: SETWISEO:47 (Bool "for" (Set (Var "X")) "being" ($#~v1_xboole_0 "non" ($#v1_xboole_0 :::"empty"::: ) ) ($#m1_hidden :::"set"::: ) (Bool "for" (Set (Var "A")) "being" ($#m1_hidden :::"set"::: ) (Bool "for" (Set (Var "f")) "being" ($#m1_subset_1 :::"Function":::) "of" (Set (Var "X")) "," (Set "(" ($#k5_finsub_1 :::"Fin"::: ) (Set (Var "A")) ")" ) "holds" (Bool (Set ($#k10_setwiseo :::"FinUnion"::: ) "(" (Set "(" ($#k1_setwiseo :::"{}."::: ) (Set (Var "X")) ")" ) "," (Set (Var "f")) ")" ) ($#r1_hidden :::"="::: ) (Set ($#k1_xboole_0 :::"{}"::: ) ))))) ; theorem :: SETWISEO:48 (Bool "for" (Set (Var "X")) "being" ($#~v1_xboole_0 "non" ($#v1_xboole_0 :::"empty"::: ) ) ($#m1_hidden :::"set"::: ) (Bool "for" (Set (Var "A")) "being" ($#m1_hidden :::"set"::: ) (Bool "for" (Set (Var "f")) "being" ($#m1_subset_1 :::"Function":::) "of" (Set (Var "X")) "," (Set "(" ($#k5_finsub_1 :::"Fin"::: ) (Set (Var "A")) ")" ) (Bool "for" (Set (Var "i")) "being" ($#m1_subset_1 :::"Element"::: ) "of" (Set (Var "X")) (Bool "for" (Set (Var "B")) "being" ($#m1_subset_1 :::"Element"::: ) "of" (Set ($#k5_finsub_1 :::"Fin"::: ) (Set (Var "X"))) "holds" (Bool (Set ($#k10_setwiseo :::"FinUnion"::: ) "(" (Set "(" (Set (Var "B")) ($#k5_setwiseo :::"\/"::: ) (Set ($#k2_setwiseo :::"{."::: ) (Set (Var "i")) ($#k2_setwiseo :::".}"::: ) ) ")" ) "," (Set (Var "f")) ")" ) ($#r1_hidden :::"="::: ) (Set (Set "(" ($#k10_setwiseo :::"FinUnion"::: ) "(" (Set (Var "B")) "," (Set (Var "f")) ")" ")" ) ($#k5_setwiseo :::"\/"::: ) (Set "(" (Set (Var "f")) ($#k3_funct_2 :::"."::: ) (Set (Var "i")) ")" )))))))) ; theorem :: SETWISEO:49 (Bool "for" (Set (Var "X")) "being" ($#~v1_xboole_0 "non" ($#v1_xboole_0 :::"empty"::: ) ) ($#m1_hidden :::"set"::: ) (Bool "for" (Set (Var "A")) "being" ($#m1_hidden :::"set"::: ) (Bool "for" (Set (Var "f")) "being" ($#m1_subset_1 :::"Function":::) "of" (Set (Var "X")) "," (Set "(" ($#k5_finsub_1 :::"Fin"::: ) (Set (Var "A")) ")" ) (Bool "for" (Set (Var "B")) "being" ($#m1_subset_1 :::"Element"::: ) "of" (Set ($#k5_finsub_1 :::"Fin"::: ) (Set (Var "X"))) "holds" (Bool (Set ($#k10_setwiseo :::"FinUnion"::: ) "(" (Set (Var "B")) "," (Set (Var "f")) ")" ) ($#r1_hidden :::"="::: ) (Set ($#k3_tarski :::"union"::: ) (Set "(" (Set (Var "f")) ($#k8_setwiseo :::".:"::: ) (Set (Var "B")) ")" ))))))) ; theorem :: SETWISEO:50 (Bool "for" (Set (Var "X")) "being" ($#~v1_xboole_0 "non" ($#v1_xboole_0 :::"empty"::: ) ) ($#m1_hidden :::"set"::: ) (Bool "for" (Set (Var "A")) "being" ($#m1_hidden :::"set"::: ) (Bool "for" (Set (Var "f")) "being" ($#m1_subset_1 :::"Function":::) "of" (Set (Var "X")) "," (Set "(" ($#k5_finsub_1 :::"Fin"::: ) (Set (Var "A")) ")" ) (Bool "for" (Set (Var "B1")) "," (Set (Var "B2")) "being" ($#m1_subset_1 :::"Element"::: ) "of" (Set ($#k5_finsub_1 :::"Fin"::: ) (Set (Var "X"))) "holds" (Bool (Set ($#k10_setwiseo :::"FinUnion"::: ) "(" (Set "(" (Set (Var "B1")) ($#k5_setwiseo :::"\/"::: ) (Set (Var "B2")) ")" ) "," (Set (Var "f")) ")" ) ($#r1_hidden :::"="::: ) (Set (Set "(" ($#k10_setwiseo :::"FinUnion"::: ) "(" (Set (Var "B1")) "," (Set (Var "f")) ")" ")" ) ($#k5_setwiseo :::"\/"::: ) (Set "(" ($#k10_setwiseo :::"FinUnion"::: ) "(" (Set (Var "B2")) "," (Set (Var "f")) ")" ")" ))))))) ; theorem :: SETWISEO:51 (Bool "for" (Set (Var "X")) "," (Set (Var "Y")) "being" ($#~v1_xboole_0 "non" ($#v1_xboole_0 :::"empty"::: ) ) ($#m1_hidden :::"set"::: ) (Bool "for" (Set (Var "A")) "being" ($#m1_hidden :::"set"::: ) (Bool "for" (Set (Var "B")) "being" ($#m1_subset_1 :::"Element"::: ) "of" (Set ($#k5_finsub_1 :::"Fin"::: ) (Set (Var "X"))) (Bool "for" (Set (Var "f")) "being" ($#m1_subset_1 :::"Function":::) "of" (Set (Var "X")) "," (Set (Var "Y")) (Bool "for" (Set (Var "g")) "being" ($#m1_subset_1 :::"Function":::) "of" (Set (Var "Y")) "," (Set "(" ($#k5_finsub_1 :::"Fin"::: ) (Set (Var "A")) ")" ) "holds" (Bool (Set ($#k10_setwiseo :::"FinUnion"::: ) "(" (Set "(" (Set (Var "f")) ($#k8_setwiseo :::".:"::: ) (Set (Var "B")) ")" ) "," (Set (Var "g")) ")" ) ($#r1_hidden :::"="::: ) (Set ($#k10_setwiseo :::"FinUnion"::: ) "(" (Set (Var "B")) "," (Set "(" (Set (Var "g")) ($#k1_partfun1 :::"*"::: ) (Set (Var "f")) ")" ) ")" ))))))) ; theorem :: SETWISEO:52 (Bool "for" (Set (Var "A")) "," (Set (Var "X")) "being" ($#~v1_xboole_0 "non" ($#v1_xboole_0 :::"empty"::: ) ) ($#m1_hidden :::"set"::: ) (Bool "for" (Set (Var "Y")) "being" ($#m1_hidden :::"set"::: ) (Bool "for" (Set (Var "G")) "being" ($#m1_subset_1 :::"BinOp":::) "of" (Set (Var "A")) "st" (Bool (Bool (Set (Var "G")) "is" ($#v1_binop_1 :::"commutative"::: ) ) & (Bool (Set (Var "G")) "is" ($#v2_binop_1 :::"associative"::: ) ) & (Bool (Set (Var "G")) "is" ($#v3_binop_1 :::"idempotent"::: ) )) "holds" (Bool "for" (Set (Var "B")) "being" ($#m1_subset_1 :::"Element"::: ) "of" (Set ($#k5_finsub_1 :::"Fin"::: ) (Set (Var "X"))) "st" (Bool (Bool (Set (Var "B")) ($#r1_hidden :::"<>"::: ) (Set ($#k1_xboole_0 :::"{}"::: ) ))) "holds" (Bool "for" (Set (Var "f")) "being" ($#m1_subset_1 :::"Function":::) "of" (Set (Var "X")) "," (Set "(" ($#k5_finsub_1 :::"Fin"::: ) (Set (Var "Y")) ")" ) (Bool "for" (Set (Var "g")) "being" ($#m1_subset_1 :::"Function":::) "of" (Set "(" ($#k5_finsub_1 :::"Fin"::: ) (Set (Var "Y")) ")" ) "," (Set (Var "A")) "st" (Bool (Bool "(" "for" (Set (Var "x")) "," (Set (Var "y")) "being" ($#m1_subset_1 :::"Element"::: ) "of" (Set ($#k5_finsub_1 :::"Fin"::: ) (Set (Var "Y"))) "holds" (Bool (Set (Set (Var "g")) ($#k3_funct_2 :::"."::: ) (Set "(" (Set (Var "x")) ($#k5_setwiseo :::"\/"::: ) (Set (Var "y")) ")" )) ($#r1_hidden :::"="::: ) (Set (Set (Var "G")) ($#k5_binop_1 :::"."::: ) "(" (Set "(" (Set (Var "g")) ($#k3_funct_2 :::"."::: ) (Set (Var "x")) ")" ) "," (Set "(" (Set (Var "g")) ($#k3_funct_2 :::"."::: ) (Set (Var "y")) ")" ) ")" )) ")" )) "holds" (Bool (Set (Set (Var "g")) ($#k3_funct_2 :::"."::: ) (Set "(" ($#k10_setwiseo :::"FinUnion"::: ) "(" (Set (Var "B")) "," (Set (Var "f")) ")" ")" )) ($#r1_hidden :::"="::: ) (Set (Set (Var "G")) ($#k7_setwiseo :::"$$"::: ) "(" (Set (Var "B")) "," (Set "(" (Set (Var "g")) ($#k1_partfun1 :::"*"::: ) (Set (Var "f")) ")" ) ")" )))))))) ; theorem :: SETWISEO:53 (Bool "for" (Set (Var "X")) "," (Set (Var "Z")) "being" ($#~v1_xboole_0 "non" ($#v1_xboole_0 :::"empty"::: ) ) ($#m1_hidden :::"set"::: ) (Bool "for" (Set (Var "Y")) "being" ($#m1_hidden :::"set"::: ) (Bool "for" (Set (Var "G")) "being" ($#m1_subset_1 :::"BinOp":::) "of" (Set (Var "Z")) "st" (Bool (Bool (Set (Var "G")) "is" ($#v1_binop_1 :::"commutative"::: ) ) & (Bool (Set (Var "G")) "is" ($#v2_binop_1 :::"associative"::: ) ) & (Bool (Set (Var "G")) "is" ($#v3_binop_1 :::"idempotent"::: ) ) & (Bool (Set (Var "G")) "is" ($#v1_setwiseo :::"having_a_unity"::: ) )) "holds" (Bool "for" (Set (Var "f")) "being" ($#m1_subset_1 :::"Function":::) "of" (Set (Var "X")) "," (Set "(" ($#k5_finsub_1 :::"Fin"::: ) (Set (Var "Y")) ")" ) (Bool "for" (Set (Var "g")) "being" ($#m1_subset_1 :::"Function":::) "of" (Set "(" ($#k5_finsub_1 :::"Fin"::: ) (Set (Var "Y")) ")" ) "," (Set (Var "Z")) "st" (Bool (Bool (Set (Set (Var "g")) ($#k3_funct_2 :::"."::: ) (Set "(" ($#k1_setwiseo :::"{}."::: ) (Set (Var "Y")) ")" )) ($#r1_hidden :::"="::: ) (Set ($#k4_binop_1 :::"the_unity_wrt"::: ) (Set (Var "G")))) & (Bool "(" "for" (Set (Var "x")) "," (Set (Var "y")) "being" ($#m1_subset_1 :::"Element"::: ) "of" (Set ($#k5_finsub_1 :::"Fin"::: ) (Set (Var "Y"))) "holds" (Bool (Set (Set (Var "g")) ($#k3_funct_2 :::"."::: ) (Set "(" (Set (Var "x")) ($#k5_setwiseo :::"\/"::: ) (Set (Var "y")) ")" )) ($#r1_hidden :::"="::: ) (Set (Set (Var "G")) ($#k5_binop_1 :::"."::: ) "(" (Set "(" (Set (Var "g")) ($#k3_funct_2 :::"."::: ) (Set (Var "x")) ")" ) "," (Set "(" (Set (Var "g")) ($#k3_funct_2 :::"."::: ) (Set (Var "y")) ")" ) ")" )) ")" )) "holds" (Bool "for" (Set (Var "B")) "being" ($#m1_subset_1 :::"Element"::: ) "of" (Set ($#k5_finsub_1 :::"Fin"::: ) (Set (Var "X"))) "holds" (Bool (Set (Set (Var "g")) ($#k3_funct_2 :::"."::: ) (Set "(" ($#k10_setwiseo :::"FinUnion"::: ) "(" (Set (Var "B")) "," (Set (Var "f")) ")" ")" )) ($#r1_hidden :::"="::: ) (Set (Set (Var "G")) ($#k7_setwiseo :::"$$"::: ) "(" (Set (Var "B")) "," (Set "(" (Set (Var "g")) ($#k1_partfun1 :::"*"::: ) (Set (Var "f")) ")" ) ")" )))))))) ; definitionlet "A" be ($#m1_hidden :::"set"::: ) ; func :::"singleton"::: "A" -> ($#m1_subset_1 :::"Function":::) "of" "A" "," (Set "(" ($#k5_finsub_1 :::"Fin"::: ) "A" ")" ) means :: SETWISEO:def 6 (Bool "for" (Set (Var "x")) "being" ($#m1_hidden :::"set"::: ) "st" (Bool (Bool (Set (Var "x")) ($#r2_hidden :::"in"::: ) "A")) "holds" (Bool (Set it ($#k1_funct_1 :::"."::: ) (Set (Var "x"))) ($#r1_hidden :::"="::: ) (Set ($#k1_tarski :::"{"::: ) (Set (Var "x")) ($#k1_tarski :::"}"::: ) ))); end; :: deftheorem defines :::"singleton"::: SETWISEO:def 6 : (Bool "for" (Set (Var "A")) "being" ($#m1_hidden :::"set"::: ) (Bool "for" (Set (Var "b2")) "being" ($#m1_subset_1 :::"Function":::) "of" (Set (Var "A")) "," (Set "(" ($#k5_finsub_1 :::"Fin"::: ) (Set (Var "A")) ")" ) "holds" (Bool "(" (Bool (Set (Var "b2")) ($#r1_hidden :::"="::: ) (Set ($#k11_setwiseo :::"singleton"::: ) (Set (Var "A")))) "iff" (Bool "for" (Set (Var "x")) "being" ($#m1_hidden :::"set"::: ) "st" (Bool (Bool (Set (Var "x")) ($#r2_hidden :::"in"::: ) (Set (Var "A")))) "holds" (Bool (Set (Set (Var "b2")) ($#k1_funct_1 :::"."::: ) (Set (Var "x"))) ($#r1_hidden :::"="::: ) (Set ($#k1_tarski :::"{"::: ) (Set (Var "x")) ($#k1_tarski :::"}"::: ) ))) ")" ))); theorem :: SETWISEO:54 (Bool "for" (Set (Var "A")) "being" ($#~v1_xboole_0 "non" ($#v1_xboole_0 :::"empty"::: ) ) ($#m1_hidden :::"set"::: ) (Bool "for" (Set (Var "f")) "being" ($#m1_subset_1 :::"Function":::) "of" (Set (Var "A")) "," (Set "(" ($#k5_finsub_1 :::"Fin"::: ) (Set (Var "A")) ")" ) "holds" (Bool "(" (Bool (Set (Var "f")) ($#r2_funct_2 :::"="::: ) (Set ($#k11_setwiseo :::"singleton"::: ) (Set (Var "A")))) "iff" (Bool "for" (Set (Var "x")) "being" ($#m1_subset_1 :::"Element"::: ) "of" (Set (Var "A")) "holds" (Bool (Set (Set (Var "f")) ($#k3_funct_2 :::"."::: ) (Set (Var "x"))) ($#r1_hidden :::"="::: ) (Set ($#k1_tarski :::"{"::: ) (Set (Var "x")) ($#k1_tarski :::"}"::: ) ))) ")" ))) ; theorem :: SETWISEO:55 (Bool "for" (Set (Var "X")) "being" ($#~v1_xboole_0 "non" ($#v1_xboole_0 :::"empty"::: ) ) ($#m1_hidden :::"set"::: ) (Bool "for" (Set (Var "x")) "being" ($#m1_hidden :::"set"::: ) (Bool "for" (Set (Var "y")) "being" ($#m1_subset_1 :::"Element"::: ) "of" (Set (Var "X")) "holds" (Bool "(" (Bool (Set (Var "x")) ($#r2_hidden :::"in"::: ) (Set (Set "(" ($#k11_setwiseo :::"singleton"::: ) (Set (Var "X")) ")" ) ($#k3_funct_2 :::"."::: ) (Set (Var "y")))) "iff" (Bool (Set (Var "x")) ($#r1_hidden :::"="::: ) (Set (Var "y"))) ")" )))) ; theorem :: SETWISEO:56 (Bool "for" (Set (Var "X")) "being" ($#~v1_xboole_0 "non" ($#v1_xboole_0 :::"empty"::: ) ) ($#m1_hidden :::"set"::: ) (Bool "for" (Set (Var "x")) "," (Set (Var "y")) "," (Set (Var "z")) "being" ($#m1_subset_1 :::"Element"::: ) "of" (Set (Var "X")) "st" (Bool (Bool (Set (Var "x")) ($#r2_hidden :::"in"::: ) (Set (Set "(" ($#k11_setwiseo :::"singleton"::: ) (Set (Var "X")) ")" ) ($#k3_funct_2 :::"."::: ) (Set (Var "z")))) & (Bool (Set (Var "y")) ($#r2_hidden :::"in"::: ) (Set (Set "(" ($#k11_setwiseo :::"singleton"::: ) (Set (Var "X")) ")" ) ($#k3_funct_2 :::"."::: ) (Set (Var "z"))))) "holds" (Bool (Set (Var "x")) ($#r1_hidden :::"="::: ) (Set (Var "y"))))) ; theorem :: SETWISEO:57 (Bool "for" (Set (Var "X")) "being" ($#~v1_xboole_0 "non" ($#v1_xboole_0 :::"empty"::: ) ) ($#m1_hidden :::"set"::: ) (Bool "for" (Set (Var "A")) "being" ($#m1_hidden :::"set"::: ) (Bool "for" (Set (Var "f")) "being" ($#m1_subset_1 :::"Function":::) "of" (Set (Var "X")) "," (Set "(" ($#k5_finsub_1 :::"Fin"::: ) (Set (Var "A")) ")" ) (Bool "for" (Set (Var "B")) "being" ($#m1_subset_1 :::"Element"::: ) "of" (Set ($#k5_finsub_1 :::"Fin"::: ) (Set (Var "X"))) (Bool "for" (Set (Var "x")) "being" ($#m1_hidden :::"set"::: ) "holds" (Bool "(" (Bool (Set (Var "x")) ($#r2_hidden :::"in"::: ) (Set ($#k10_setwiseo :::"FinUnion"::: ) "(" (Set (Var "B")) "," (Set (Var "f")) ")" )) "iff" (Bool "ex" (Set (Var "i")) "being" ($#m1_subset_1 :::"Element"::: ) "of" (Set (Var "X")) "st" (Bool "(" (Bool (Set (Var "i")) ($#r2_hidden :::"in"::: ) (Set (Var "B"))) & (Bool (Set (Var "x")) ($#r2_hidden :::"in"::: ) (Set (Set (Var "f")) ($#k3_funct_2 :::"."::: ) (Set (Var "i")))) ")" )) ")" )))))) ; theorem :: SETWISEO:58 (Bool "for" (Set (Var "X")) "being" ($#~v1_xboole_0 "non" ($#v1_xboole_0 :::"empty"::: ) ) ($#m1_hidden :::"set"::: ) (Bool "for" (Set (Var "B")) "being" ($#m1_subset_1 :::"Element"::: ) "of" (Set ($#k5_finsub_1 :::"Fin"::: ) (Set (Var "X"))) "holds" (Bool (Set ($#k10_setwiseo :::"FinUnion"::: ) "(" (Set (Var "B")) "," (Set "(" ($#k11_setwiseo :::"singleton"::: ) (Set (Var "X")) ")" ) ")" ) ($#r1_hidden :::"="::: ) (Set (Var "B"))))) ; theorem :: SETWISEO:59 (Bool "for" (Set (Var "X")) "being" ($#~v1_xboole_0 "non" ($#v1_xboole_0 :::"empty"::: ) ) ($#m1_hidden :::"set"::: ) (Bool "for" (Set (Var "Y")) "," (Set (Var "Z")) "being" ($#m1_hidden :::"set"::: ) (Bool "for" (Set (Var "f")) "being" ($#m1_subset_1 :::"Function":::) "of" (Set (Var "X")) "," (Set "(" ($#k5_finsub_1 :::"Fin"::: ) (Set (Var "Y")) ")" ) (Bool "for" (Set (Var "g")) "being" ($#m1_subset_1 :::"Function":::) "of" (Set "(" ($#k5_finsub_1 :::"Fin"::: ) (Set (Var "Y")) ")" ) "," (Set "(" ($#k5_finsub_1 :::"Fin"::: ) (Set (Var "Z")) ")" ) "st" (Bool (Bool (Set (Set (Var "g")) ($#k3_funct_2 :::"."::: ) (Set "(" ($#k1_setwiseo :::"{}."::: ) (Set (Var "Y")) ")" )) ($#r1_hidden :::"="::: ) (Set ($#k1_setwiseo :::"{}."::: ) (Set (Var "Z")))) & (Bool "(" "for" (Set (Var "x")) "," (Set (Var "y")) "being" ($#m1_subset_1 :::"Element"::: ) "of" (Set ($#k5_finsub_1 :::"Fin"::: ) (Set (Var "Y"))) "holds" (Bool (Set (Set (Var "g")) ($#k3_funct_2 :::"."::: ) (Set "(" (Set (Var "x")) ($#k5_setwiseo :::"\/"::: ) (Set (Var "y")) ")" )) ($#r1_hidden :::"="::: ) (Set (Set "(" (Set (Var "g")) ($#k3_funct_2 :::"."::: ) (Set (Var "x")) ")" ) ($#k5_setwiseo :::"\/"::: ) (Set "(" (Set (Var "g")) ($#k3_funct_2 :::"."::: ) (Set (Var "y")) ")" ))) ")" )) "holds" (Bool "for" (Set (Var "B")) "being" ($#m1_subset_1 :::"Element"::: ) "of" (Set ($#k5_finsub_1 :::"Fin"::: ) (Set (Var "X"))) "holds" (Bool (Set (Set (Var "g")) ($#k3_funct_2 :::"."::: ) (Set "(" ($#k10_setwiseo :::"FinUnion"::: ) "(" (Set (Var "B")) "," (Set (Var "f")) ")" ")" )) ($#r1_hidden :::"="::: ) (Set ($#k10_setwiseo :::"FinUnion"::: ) "(" (Set (Var "B")) "," (Set "(" (Set (Var "g")) ($#k1_partfun1 :::"*"::: ) (Set (Var "f")) ")" ) ")" ))))))) ;