:: FUNCT_2 semantic presentation begin definitionlet "X", "Y" be ($#m1_hidden :::"set"::: ) ; let "R" be ($#m1_subset_1 :::"Relation":::) "of" (Set (Const "X")) "," (Set (Const "Y")); attr "R" is :::"quasi_total"::: means :: FUNCT_2:def 1 (Bool "X" ($#r1_hidden :::"="::: ) (Set ($#k1_relset_1 :::"dom"::: ) "R")) if (Bool "Y" ($#r1_hidden :::"<>"::: ) (Set ($#k1_xboole_0 :::"{}"::: ) )) otherwise (Bool "R" ($#r1_hidden :::"="::: ) (Set ($#k1_xboole_0 :::"{}"::: ) )); end; :: deftheorem defines :::"quasi_total"::: FUNCT_2:def 1 : (Bool "for" (Set (Var "X")) "," (Set (Var "Y")) "being" ($#m1_hidden :::"set"::: ) (Bool "for" (Set (Var "R")) "being" ($#m1_subset_1 :::"Relation":::) "of" (Set (Var "X")) "," (Set (Var "Y")) "holds" (Bool "(" "(" (Bool (Bool (Set (Var "Y")) ($#r1_hidden :::"<>"::: ) (Set ($#k1_xboole_0 :::"{}"::: ) ))) "implies" (Bool "(" (Bool (Set (Var "R")) "is" ($#v1_funct_2 :::"quasi_total"::: ) ) "iff" (Bool (Set (Var "X")) ($#r1_hidden :::"="::: ) (Set ($#k1_relset_1 :::"dom"::: ) (Set (Var "R")))) ")" ) ")" & "(" (Bool (Bool (Bool "not" (Set (Var "Y")) ($#r1_hidden :::"<>"::: ) (Set ($#k1_xboole_0 :::"{}"::: ) )))) "implies" (Bool "(" (Bool (Set (Var "R")) "is" ($#v1_funct_2 :::"quasi_total"::: ) ) "iff" (Bool (Set (Var "R")) ($#r1_hidden :::"="::: ) (Set ($#k1_xboole_0 :::"{}"::: ) )) ")" ) ")" ")" ))); registrationlet "X", "Y" be ($#m1_hidden :::"set"::: ) ; cluster ($#v1_relat_1 :::"Relation-like"::: ) "X" ($#v4_relat_1 :::"-defined"::: ) "Y" ($#v5_relat_1 :::"-valued"::: ) ($#v1_funct_1 :::"Function-like"::: ) ($#v1_funct_2 :::"quasi_total"::: ) for ($#m1_subset_1 :::"Element"::: ) "of" (Set ($#k1_zfmisc_1 :::"bool"::: ) (Set ($#k2_zfmisc_1 :::"[:"::: ) "X" "," "Y" ($#k2_zfmisc_1 :::":]"::: ) )); end; registrationlet "X", "Y" be ($#m1_hidden :::"set"::: ) ; cluster ($#v1_partfun1 :::"total"::: ) -> ($#v1_funct_2 :::"quasi_total"::: ) for ($#m1_subset_1 :::"Element"::: ) "of" (Set ($#k1_zfmisc_1 :::"bool"::: ) (Set ($#k2_zfmisc_1 :::"[:"::: ) "X" "," "Y" ($#k2_zfmisc_1 :::":]"::: ) )); end; definitionlet "X", "Y" be ($#m1_hidden :::"set"::: ) ; mode Function of "X" "," "Y" is ($#v1_funct_2 :::"quasi_total"::: ) ($#m1_subset_1 :::"PartFunc":::) "of" "X" "," "Y"; end; registrationlet "X" be ($#v1_xboole_0 :::"empty"::: ) ($#m1_hidden :::"set"::: ) ; let "Y" be ($#m1_hidden :::"set"::: ) ; cluster ($#v1_funct_2 :::"quasi_total"::: ) -> ($#v1_partfun1 :::"total"::: ) for ($#m1_subset_1 :::"Element"::: ) "of" (Set ($#k1_zfmisc_1 :::"bool"::: ) (Set ($#k2_zfmisc_1 :::"[:"::: ) "X" "," "Y" ($#k2_zfmisc_1 :::":]"::: ) )); end; registrationlet "X" be ($#m1_hidden :::"set"::: ) ; let "Y" be ($#~v1_xboole_0 "non" ($#v1_xboole_0 :::"empty"::: ) ) ($#m1_hidden :::"set"::: ) ; cluster ($#v1_funct_2 :::"quasi_total"::: ) -> ($#v1_partfun1 :::"total"::: ) for ($#m1_subset_1 :::"Element"::: ) "of" (Set ($#k1_zfmisc_1 :::"bool"::: ) (Set ($#k2_zfmisc_1 :::"[:"::: ) "X" "," "Y" ($#k2_zfmisc_1 :::":]"::: ) )); end; registrationlet "X" be ($#m1_hidden :::"set"::: ) ; cluster ($#v1_funct_2 :::"quasi_total"::: ) -> ($#v1_partfun1 :::"total"::: ) for ($#m1_subset_1 :::"Element"::: ) "of" (Set ($#k1_zfmisc_1 :::"bool"::: ) (Set ($#k2_zfmisc_1 :::"[:"::: ) "X" "," "X" ($#k2_zfmisc_1 :::":]"::: ) )); end; theorem :: FUNCT_2:1 (Bool "for" (Set (Var "f")) "being" ($#m1_hidden :::"Function":::) "holds" (Bool (Set (Var "f")) "is" ($#m1_subset_1 :::"Function":::) "of" (Set "(" ($#k9_xtuple_0 :::"dom"::: ) (Set (Var "f")) ")" ) "," (Set "(" ($#k10_xtuple_0 :::"rng"::: ) (Set (Var "f")) ")" ))) ; theorem :: FUNCT_2:2 (Bool "for" (Set (Var "Y")) "being" ($#m1_hidden :::"set"::: ) (Bool "for" (Set (Var "f")) "being" ($#m1_hidden :::"Function":::) "st" (Bool (Bool (Set ($#k10_xtuple_0 :::"rng"::: ) (Set (Var "f"))) ($#r1_tarski :::"c="::: ) (Set (Var "Y")))) "holds" (Bool (Set (Var "f")) "is" ($#m1_subset_1 :::"Function":::) "of" (Set "(" ($#k9_xtuple_0 :::"dom"::: ) (Set (Var "f")) ")" ) "," (Set (Var "Y"))))) ; theorem :: FUNCT_2:3 (Bool "for" (Set (Var "X")) "," (Set (Var "Y")) "being" ($#m1_hidden :::"set"::: ) (Bool "for" (Set (Var "f")) "being" ($#m1_hidden :::"Function":::) "st" (Bool (Bool (Set ($#k9_xtuple_0 :::"dom"::: ) (Set (Var "f"))) ($#r1_hidden :::"="::: ) (Set (Var "X"))) & (Bool "(" "for" (Set (Var "x")) "being" ($#m1_hidden :::"set"::: ) "st" (Bool (Bool (Set (Var "x")) ($#r2_hidden :::"in"::: ) (Set (Var "X")))) "holds" (Bool (Set (Set (Var "f")) ($#k1_funct_1 :::"."::: ) (Set (Var "x"))) ($#r2_hidden :::"in"::: ) (Set (Var "Y"))) ")" )) "holds" (Bool (Set (Var "f")) "is" ($#m1_subset_1 :::"Function":::) "of" (Set (Var "X")) "," (Set (Var "Y"))))) ; theorem :: FUNCT_2:4 (Bool "for" (Set (Var "X")) "," (Set (Var "Y")) "," (Set (Var "x")) "being" ($#m1_hidden :::"set"::: ) (Bool "for" (Set (Var "f")) "being" ($#m1_subset_1 :::"Function":::) "of" (Set (Var "X")) "," (Set (Var "Y")) "st" (Bool (Bool (Set (Var "Y")) ($#r1_hidden :::"<>"::: ) (Set ($#k1_xboole_0 :::"{}"::: ) )) & (Bool (Set (Var "x")) ($#r2_hidden :::"in"::: ) (Set (Var "X")))) "holds" (Bool (Set (Set (Var "f")) ($#k1_funct_1 :::"."::: ) (Set (Var "x"))) ($#r2_hidden :::"in"::: ) (Set ($#k2_relset_1 :::"rng"::: ) (Set (Var "f")))))) ; theorem :: FUNCT_2:5 (Bool "for" (Set (Var "X")) "," (Set (Var "Y")) "," (Set (Var "x")) "being" ($#m1_hidden :::"set"::: ) (Bool "for" (Set (Var "f")) "being" ($#m1_subset_1 :::"Function":::) "of" (Set (Var "X")) "," (Set (Var "Y")) "st" (Bool (Bool (Set (Var "Y")) ($#r1_hidden :::"<>"::: ) (Set ($#k1_xboole_0 :::"{}"::: ) )) & (Bool (Set (Var "x")) ($#r2_hidden :::"in"::: ) (Set (Var "X")))) "holds" (Bool (Set (Set (Var "f")) ($#k1_funct_1 :::"."::: ) (Set (Var "x"))) ($#r2_hidden :::"in"::: ) (Set (Var "Y"))))) ; theorem :: FUNCT_2:6 (Bool "for" (Set (Var "X")) "," (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 (Var "Y")) "st" (Bool "(" (Bool (Bool (Set (Var "Y")) ($#r1_hidden :::"="::: ) (Set ($#k1_xboole_0 :::"{}"::: ) ))) "implies" (Bool (Set (Var "X")) ($#r1_hidden :::"="::: ) (Set ($#k1_xboole_0 :::"{}"::: ) )) ")" & (Bool (Set ($#k2_relset_1 :::"rng"::: ) (Set (Var "f"))) ($#r1_tarski :::"c="::: ) (Set (Var "Z")))) "holds" (Bool (Set (Var "f")) "is" ($#m1_subset_1 :::"Function":::) "of" (Set (Var "X")) "," (Set (Var "Z"))))) ; theorem :: FUNCT_2:7 (Bool "for" (Set (Var "X")) "," (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 (Var "Y")) "st" (Bool "(" (Bool (Bool (Set (Var "Y")) ($#r1_hidden :::"="::: ) (Set ($#k1_xboole_0 :::"{}"::: ) ))) "implies" (Bool (Set (Var "X")) ($#r1_hidden :::"="::: ) (Set ($#k1_xboole_0 :::"{}"::: ) )) ")" & (Bool (Set (Var "Y")) ($#r1_tarski :::"c="::: ) (Set (Var "Z")))) "holds" (Bool (Set (Var "f")) "is" ($#m1_subset_1 :::"Function":::) "of" (Set (Var "X")) "," (Set (Var "Z"))))) ; scheme :: FUNCT_2:sch 1 FuncEx1{ F1() -> ($#m1_hidden :::"set"::: ) , F2() -> ($#m1_hidden :::"set"::: ) , P1[ ($#m1_hidden :::"set"::: ) "," ($#m1_hidden :::"set"::: ) ] } : (Bool "ex" (Set (Var "f")) "being" ($#m1_subset_1 :::"Function":::) "of" (Set F1 "(" ")" ) "," (Set F2 "(" ")" ) "st" (Bool "for" (Set (Var "x")) "being" ($#m1_hidden :::"set"::: ) "st" (Bool (Bool (Set (Var "x")) ($#r2_hidden :::"in"::: ) (Set F1 "(" ")" ))) "holds" (Bool P1[(Set (Var "x")) "," (Set (Set (Var "f")) ($#k1_funct_1 :::"."::: ) (Set (Var "x")))]))) provided (Bool "for" (Set (Var "x")) "being" ($#m1_hidden :::"set"::: ) "st" (Bool (Bool (Set (Var "x")) ($#r2_hidden :::"in"::: ) (Set F1 "(" ")" ))) "holds" (Bool "ex" (Set (Var "y")) "being" ($#m1_hidden :::"set"::: ) "st" (Bool "(" (Bool (Set (Var "y")) ($#r2_hidden :::"in"::: ) (Set F2 "(" ")" )) & (Bool P1[(Set (Var "x")) "," (Set (Var "y"))]) ")" ))) proof end; scheme :: FUNCT_2:sch 2 Lambda1{ F1() -> ($#m1_hidden :::"set"::: ) , F2() -> ($#m1_hidden :::"set"::: ) , F3( ($#m1_hidden :::"set"::: ) ) -> ($#m1_hidden :::"set"::: ) } : (Bool "ex" (Set (Var "f")) "being" ($#m1_subset_1 :::"Function":::) "of" (Set F1 "(" ")" ) "," (Set F2 "(" ")" ) "st" (Bool "for" (Set (Var "x")) "being" ($#m1_hidden :::"set"::: ) "st" (Bool (Bool (Set (Var "x")) ($#r2_hidden :::"in"::: ) (Set F1 "(" ")" ))) "holds" (Bool (Set (Set (Var "f")) ($#k1_funct_1 :::"."::: ) (Set (Var "x"))) ($#r1_hidden :::"="::: ) (Set F3 "(" (Set (Var "x")) ")" )))) provided (Bool "for" (Set (Var "x")) "being" ($#m1_hidden :::"set"::: ) "st" (Bool (Bool (Set (Var "x")) ($#r2_hidden :::"in"::: ) (Set F1 "(" ")" ))) "holds" (Bool (Set F3 "(" (Set (Var "x")) ")" ) ($#r2_hidden :::"in"::: ) (Set F2 "(" ")" ))) proof end; definitionlet "X", "Y" be ($#m1_hidden :::"set"::: ) ; func :::"Funcs"::: "(" "X" "," "Y" ")" -> ($#m1_hidden :::"set"::: ) means :: FUNCT_2:def 2 (Bool "for" (Set (Var "x")) "being" ($#m1_hidden :::"set"::: ) "holds" (Bool "(" (Bool (Set (Var "x")) ($#r2_hidden :::"in"::: ) it) "iff" (Bool "ex" (Set (Var "f")) "being" ($#m1_hidden :::"Function":::) "st" (Bool "(" (Bool (Set (Var "x")) ($#r1_hidden :::"="::: ) (Set (Var "f"))) & (Bool (Set ($#k9_xtuple_0 :::"dom"::: ) (Set (Var "f"))) ($#r1_hidden :::"="::: ) "X") & (Bool (Set ($#k10_xtuple_0 :::"rng"::: ) (Set (Var "f"))) ($#r1_tarski :::"c="::: ) "Y") ")" )) ")" )); end; :: deftheorem defines :::"Funcs"::: FUNCT_2:def 2 : (Bool "for" (Set (Var "X")) "," (Set (Var "Y")) "," (Set (Var "b3")) "being" ($#m1_hidden :::"set"::: ) "holds" (Bool "(" (Bool (Set (Var "b3")) ($#r1_hidden :::"="::: ) (Set ($#k1_funct_2 :::"Funcs"::: ) "(" (Set (Var "X")) "," (Set (Var "Y")) ")" )) "iff" (Bool "for" (Set (Var "x")) "being" ($#m1_hidden :::"set"::: ) "holds" (Bool "(" (Bool (Set (Var "x")) ($#r2_hidden :::"in"::: ) (Set (Var "b3"))) "iff" (Bool "ex" (Set (Var "f")) "being" ($#m1_hidden :::"Function":::) "st" (Bool "(" (Bool (Set (Var "x")) ($#r1_hidden :::"="::: ) (Set (Var "f"))) & (Bool (Set ($#k9_xtuple_0 :::"dom"::: ) (Set (Var "f"))) ($#r1_hidden :::"="::: ) (Set (Var "X"))) & (Bool (Set ($#k10_xtuple_0 :::"rng"::: ) (Set (Var "f"))) ($#r1_tarski :::"c="::: ) (Set (Var "Y"))) ")" )) ")" )) ")" )); theorem :: FUNCT_2:8 (Bool "for" (Set (Var "X")) "," (Set (Var "Y")) "being" ($#m1_hidden :::"set"::: ) (Bool "for" (Set (Var "f")) "being" ($#m1_subset_1 :::"Function":::) "of" (Set (Var "X")) "," (Set (Var "Y")) "st" (Bool "(" (Bool (Bool (Set (Var "Y")) ($#r1_hidden :::"="::: ) (Set ($#k1_xboole_0 :::"{}"::: ) ))) "implies" (Bool (Set (Var "X")) ($#r1_hidden :::"="::: ) (Set ($#k1_xboole_0 :::"{}"::: ) )) ")" ) "holds" (Bool (Set (Var "f")) ($#r2_hidden :::"in"::: ) (Set ($#k1_funct_2 :::"Funcs"::: ) "(" (Set (Var "X")) "," (Set (Var "Y")) ")" )))) ; theorem :: FUNCT_2:9 (Bool "for" (Set (Var "X")) "being" ($#m1_hidden :::"set"::: ) (Bool "for" (Set (Var "f")) "being" ($#m1_subset_1 :::"Function":::) "of" (Set (Var "X")) "," (Set (Var "X")) "holds" (Bool (Set (Var "f")) ($#r2_hidden :::"in"::: ) (Set ($#k1_funct_2 :::"Funcs"::: ) "(" (Set (Var "X")) "," (Set (Var "X")) ")" )))) ; registrationlet "X" be ($#m1_hidden :::"set"::: ) ; let "Y" be ($#~v1_xboole_0 "non" ($#v1_xboole_0 :::"empty"::: ) ) ($#m1_hidden :::"set"::: ) ; cluster (Set ($#k1_funct_2 :::"Funcs"::: ) "(" "X" "," "Y" ")" ) -> ($#~v1_xboole_0 "non" ($#v1_xboole_0 :::"empty"::: ) ) ; end; registrationlet "X" be ($#m1_hidden :::"set"::: ) ; cluster (Set ($#k1_funct_2 :::"Funcs"::: ) "(" "X" "," "X" ")" ) -> ($#~v1_xboole_0 "non" ($#v1_xboole_0 :::"empty"::: ) ) ; end; registrationlet "X" be ($#~v1_xboole_0 "non" ($#v1_xboole_0 :::"empty"::: ) ) ($#m1_hidden :::"set"::: ) ; let "Y" be ($#v1_xboole_0 :::"empty"::: ) ($#m1_hidden :::"set"::: ) ; cluster (Set ($#k1_funct_2 :::"Funcs"::: ) "(" "X" "," "Y" ")" ) -> ($#v1_xboole_0 :::"empty"::: ) ; end; theorem :: FUNCT_2:10 (Bool "for" (Set (Var "X")) "," (Set (Var "Y")) "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 "y")) "being" ($#m1_hidden :::"set"::: ) "st" (Bool (Bool (Set (Var "y")) ($#r2_hidden :::"in"::: ) (Set (Var "Y")))) "holds" (Bool "ex" (Set (Var "x")) "being" ($#m1_hidden :::"set"::: ) "st" (Bool "(" (Bool (Set (Var "x")) ($#r2_hidden :::"in"::: ) (Set (Var "X"))) & (Bool (Set (Var "y")) ($#r1_hidden :::"="::: ) (Set (Set (Var "f")) ($#k1_funct_1 :::"."::: ) (Set (Var "x")))) ")" )) ")" )) "holds" (Bool (Set ($#k2_relset_1 :::"rng"::: ) (Set (Var "f"))) ($#r1_hidden :::"="::: ) (Set (Var "Y"))))) ; theorem :: FUNCT_2:11 (Bool "for" (Set (Var "X")) "," (Set (Var "Y")) "," (Set (Var "y")) "being" ($#m1_hidden :::"set"::: ) (Bool "for" (Set (Var "f")) "being" ($#m1_subset_1 :::"Function":::) "of" (Set (Var "X")) "," (Set (Var "Y")) "st" (Bool (Bool (Set (Var "y")) ($#r2_hidden :::"in"::: ) (Set ($#k2_relset_1 :::"rng"::: ) (Set (Var "f"))))) "holds" (Bool "ex" (Set (Var "x")) "being" ($#m1_hidden :::"set"::: ) "st" (Bool "(" (Bool (Set (Var "x")) ($#r2_hidden :::"in"::: ) (Set (Var "X"))) & (Bool (Set (Set (Var "f")) ($#k1_funct_1 :::"."::: ) (Set (Var "x"))) ($#r1_hidden :::"="::: ) (Set (Var "y"))) ")" )))) ; theorem :: FUNCT_2:12 (Bool "for" (Set (Var "X")) "," (Set (Var "Y")) "being" ($#m1_hidden :::"set"::: ) (Bool "for" (Set (Var "f1")) "," (Set (Var "f2")) "being" ($#m1_subset_1 :::"Function":::) "of" (Set (Var "X")) "," (Set (Var "Y")) "st" (Bool (Bool "(" "for" (Set (Var "x")) "being" ($#m1_hidden :::"set"::: ) "st" (Bool (Bool (Set (Var "x")) ($#r2_hidden :::"in"::: ) (Set (Var "X")))) "holds" (Bool (Set (Set (Var "f1")) ($#k1_funct_1 :::"."::: ) (Set (Var "x"))) ($#r1_hidden :::"="::: ) (Set (Set (Var "f2")) ($#k1_funct_1 :::"."::: ) (Set (Var "x")))) ")" )) "holds" (Bool (Set (Var "f1")) ($#r2_relset_1 :::"="::: ) (Set (Var "f2"))))) ; theorem :: FUNCT_2:13 (Bool "for" (Set (Var "X")) "," (Set (Var "Y")) "," (Set (Var "Z")) "being" ($#m1_hidden :::"set"::: ) (Bool "for" (Set (Var "f")) "being" ($#v1_funct_2 :::"quasi_total"::: ) ($#m1_subset_1 :::"Relation":::) "of" (Set (Var "X")) "," (Set (Var "Y")) (Bool "for" (Set (Var "g")) "being" ($#v1_funct_2 :::"quasi_total"::: ) ($#m1_subset_1 :::"Relation":::) "of" (Set (Var "Y")) "," (Set (Var "Z")) "st" (Bool (Bool "(" "not" (Bool (Set (Var "Y")) ($#r1_hidden :::"="::: ) (Set ($#k1_xboole_0 :::"{}"::: ) )) "or" (Bool (Set (Var "Z")) ($#r1_hidden :::"="::: ) (Set ($#k1_xboole_0 :::"{}"::: ) )) "or" (Bool (Set (Var "X")) ($#r1_hidden :::"="::: ) (Set ($#k1_xboole_0 :::"{}"::: ) )) ")" )) "holds" (Bool (Set (Set (Var "f")) ($#k4_relset_1 :::"*"::: ) (Set (Var "g"))) "is" ($#v1_funct_2 :::"quasi_total"::: ) )))) ; theorem :: FUNCT_2:14 (Bool "for" (Set (Var "X")) "," (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 (Var "Y")) (Bool "for" (Set (Var "g")) "being" ($#m1_subset_1 :::"Function":::) "of" (Set (Var "Y")) "," (Set (Var "Z")) "st" (Bool (Bool (Set (Var "Z")) ($#r1_hidden :::"<>"::: ) (Set ($#k1_xboole_0 :::"{}"::: ) )) & (Bool (Set ($#k2_relset_1 :::"rng"::: ) (Set (Var "f"))) ($#r1_hidden :::"="::: ) (Set (Var "Y"))) & (Bool (Set ($#k2_relset_1 :::"rng"::: ) (Set (Var "g"))) ($#r1_hidden :::"="::: ) (Set (Var "Z")))) "holds" (Bool (Set ($#k2_relset_1 :::"rng"::: ) (Set "(" (Set (Var "g")) ($#k1_partfun1 :::"*"::: ) (Set (Var "f")) ")" )) ($#r1_hidden :::"="::: ) (Set (Var "Z")))))) ; theorem :: FUNCT_2:15 (Bool "for" (Set (Var "X")) "," (Set (Var "Y")) "," (Set (Var "x")) "being" ($#m1_hidden :::"set"::: ) (Bool "for" (Set (Var "f")) "being" ($#m1_subset_1 :::"Function":::) "of" (Set (Var "X")) "," (Set (Var "Y")) (Bool "for" (Set (Var "g")) "being" ($#m1_hidden :::"Function":::) "st" (Bool (Bool (Set (Var "Y")) ($#r1_hidden :::"<>"::: ) (Set ($#k1_xboole_0 :::"{}"::: ) )) & (Bool (Set (Var "x")) ($#r2_hidden :::"in"::: ) (Set (Var "X")))) "holds" (Bool (Set (Set "(" (Set (Var "g")) ($#k3_relat_1 :::"*"::: ) (Set (Var "f")) ")" ) ($#k1_funct_1 :::"."::: ) (Set (Var "x"))) ($#r1_hidden :::"="::: ) (Set (Set (Var "g")) ($#k1_funct_1 :::"."::: ) (Set "(" (Set (Var "f")) ($#k1_funct_1 :::"."::: ) (Set (Var "x")) ")" )))))) ; theorem :: FUNCT_2:16 (Bool "for" (Set (Var "X")) "," (Set (Var "Y")) "being" ($#m1_hidden :::"set"::: ) (Bool "for" (Set (Var "f")) "being" ($#m1_subset_1 :::"Function":::) "of" (Set (Var "X")) "," (Set (Var "Y")) "st" (Bool (Bool (Set (Var "Y")) ($#r1_hidden :::"<>"::: ) (Set ($#k1_xboole_0 :::"{}"::: ) ))) "holds" (Bool "(" (Bool (Set ($#k2_relset_1 :::"rng"::: ) (Set (Var "f"))) ($#r1_hidden :::"="::: ) (Set (Var "Y"))) "iff" (Bool "for" (Set (Var "Z")) "being" ($#m1_hidden :::"set"::: ) "st" (Bool (Bool (Set (Var "Z")) ($#r1_hidden :::"<>"::: ) (Set ($#k1_xboole_0 :::"{}"::: ) ))) "holds" (Bool "for" (Set (Var "g")) "," (Set (Var "h")) "being" ($#m1_subset_1 :::"Function":::) "of" (Set (Var "Y")) "," (Set (Var "Z")) "st" (Bool (Bool (Set (Set (Var "g")) ($#k1_partfun1 :::"*"::: ) (Set (Var "f"))) ($#r2_relset_1 :::"="::: ) (Set (Set (Var "h")) ($#k1_partfun1 :::"*"::: ) (Set (Var "f"))))) "holds" (Bool (Set (Var "g")) ($#r2_relset_1 :::"="::: ) (Set (Var "h"))))) ")" ))) ; theorem :: FUNCT_2:17 (Bool "for" (Set (Var "X")) "," (Set (Var "Y")) "being" ($#m1_hidden :::"set"::: ) (Bool "for" (Set (Var "f")) "being" ($#m1_subset_1 :::"Relation":::) "of" (Set (Var "X")) "," (Set (Var "Y")) "holds" (Bool "(" (Bool (Set (Set "(" ($#k6_partfun1 :::"id"::: ) (Set (Var "X")) ")" ) ($#k4_relset_1 :::"*"::: ) (Set (Var "f"))) ($#r2_relset_1 :::"="::: ) (Set (Var "f"))) & (Bool (Set (Set (Var "f")) ($#k4_relset_1 :::"*"::: ) (Set "(" ($#k6_partfun1 :::"id"::: ) (Set (Var "Y")) ")" )) ($#r2_relset_1 :::"="::: ) (Set (Var "f"))) ")" ))) ; theorem :: FUNCT_2:18 (Bool "for" (Set (Var "X")) "," (Set (Var "Y")) "being" ($#m1_hidden :::"set"::: ) (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 "X")) "st" (Bool (Bool (Set (Set (Var "f")) ($#k1_partfun1 :::"*"::: ) (Set (Var "g"))) ($#r2_relset_1 :::"="::: ) (Set ($#k6_partfun1 :::"id"::: ) (Set (Var "Y"))))) "holds" (Bool (Set ($#k2_relset_1 :::"rng"::: ) (Set (Var "f"))) ($#r1_hidden :::"="::: ) (Set (Var "Y")))))) ; theorem :: FUNCT_2:19 (Bool "for" (Set (Var "X")) "," (Set (Var "Y")) "being" ($#m1_hidden :::"set"::: ) (Bool "for" (Set (Var "f")) "being" ($#m1_subset_1 :::"Function":::) "of" (Set (Var "X")) "," (Set (Var "Y")) "st" (Bool "(" (Bool (Bool (Set (Var "Y")) ($#r1_hidden :::"="::: ) (Set ($#k1_xboole_0 :::"{}"::: ) ))) "implies" (Bool (Set (Var "X")) ($#r1_hidden :::"="::: ) (Set ($#k1_xboole_0 :::"{}"::: ) )) ")" ) "holds" (Bool "(" (Bool (Set (Var "f")) "is" ($#v2_funct_1 :::"one-to-one"::: ) ) "iff" (Bool "for" (Set (Var "x1")) "," (Set (Var "x2")) "being" ($#m1_hidden :::"set"::: ) "st" (Bool (Bool (Set (Var "x1")) ($#r2_hidden :::"in"::: ) (Set (Var "X"))) & (Bool (Set (Var "x2")) ($#r2_hidden :::"in"::: ) (Set (Var "X"))) & (Bool (Set (Set (Var "f")) ($#k1_funct_1 :::"."::: ) (Set (Var "x1"))) ($#r1_hidden :::"="::: ) (Set (Set (Var "f")) ($#k1_funct_1 :::"."::: ) (Set (Var "x2"))))) "holds" (Bool (Set (Var "x1")) ($#r1_hidden :::"="::: ) (Set (Var "x2")))) ")" ))) ; theorem :: FUNCT_2:20 (Bool "for" (Set (Var "X")) "," (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 (Var "Y")) (Bool "for" (Set (Var "g")) "being" ($#m1_subset_1 :::"Function":::) "of" (Set (Var "Y")) "," (Set (Var "Z")) "st" (Bool "(" (Bool (Bool (Set (Var "Z")) ($#r1_hidden :::"="::: ) (Set ($#k1_xboole_0 :::"{}"::: ) ))) "implies" (Bool (Set (Var "Y")) ($#r1_hidden :::"="::: ) (Set ($#k1_xboole_0 :::"{}"::: ) )) ")" & (Bool (Set (Set (Var "g")) ($#k1_partfun1 :::"*"::: ) (Set (Var "f"))) "is" ($#v2_funct_1 :::"one-to-one"::: ) )) "holds" (Bool (Set (Var "f")) "is" ($#v2_funct_1 :::"one-to-one"::: ) )))) ; theorem :: FUNCT_2:21 (Bool "for" (Set (Var "X")) "," (Set (Var "Y")) "being" ($#m1_hidden :::"set"::: ) (Bool "for" (Set (Var "f")) "being" ($#m1_subset_1 :::"Function":::) "of" (Set (Var "X")) "," (Set (Var "Y")) "st" (Bool (Bool (Set (Var "X")) ($#r1_hidden :::"<>"::: ) (Set ($#k1_xboole_0 :::"{}"::: ) )) & (Bool (Set (Var "Y")) ($#r1_hidden :::"<>"::: ) (Set ($#k1_xboole_0 :::"{}"::: ) ))) "holds" (Bool "(" (Bool (Set (Var "f")) "is" ($#v2_funct_1 :::"one-to-one"::: ) ) "iff" (Bool "for" (Set (Var "Z")) "being" ($#m1_hidden :::"set"::: ) (Bool "for" (Set (Var "g")) "," (Set (Var "h")) "being" ($#m1_subset_1 :::"Function":::) "of" (Set (Var "Z")) "," (Set (Var "X")) "st" (Bool (Bool (Set (Set (Var "f")) ($#k1_partfun1 :::"*"::: ) (Set (Var "g"))) ($#r2_relset_1 :::"="::: ) (Set (Set (Var "f")) ($#k1_partfun1 :::"*"::: ) (Set (Var "h"))))) "holds" (Bool (Set (Var "g")) ($#r2_relset_1 :::"="::: ) (Set (Var "h"))))) ")" ))) ; theorem :: FUNCT_2:22 (Bool "for" (Set (Var "X")) "," (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 (Var "Y")) (Bool "for" (Set (Var "g")) "being" ($#m1_subset_1 :::"Function":::) "of" (Set (Var "Y")) "," (Set (Var "Z")) "st" (Bool (Bool (Set (Var "Z")) ($#r1_hidden :::"<>"::: ) (Set ($#k1_xboole_0 :::"{}"::: ) )) & (Bool (Set ($#k2_relset_1 :::"rng"::: ) (Set "(" (Set (Var "g")) ($#k1_partfun1 :::"*"::: ) (Set (Var "f")) ")" )) ($#r1_hidden :::"="::: ) (Set (Var "Z"))) & (Bool (Set (Var "g")) "is" ($#v2_funct_1 :::"one-to-one"::: ) )) "holds" (Bool (Set ($#k2_relset_1 :::"rng"::: ) (Set (Var "f"))) ($#r1_hidden :::"="::: ) (Set (Var "Y")))))) ; definitionlet "Y" be ($#m1_hidden :::"set"::: ) ; let "f" be (Set (Const "Y")) ($#v5_relat_1 :::"-valued"::: ) ($#m1_hidden :::"Relation":::); attr "f" is :::"onto"::: means :: FUNCT_2:def 3 (Bool (Set ($#k2_relset_1 :::"rng"::: ) "f") ($#r1_hidden :::"="::: ) "Y"); end; :: deftheorem defines :::"onto"::: FUNCT_2:def 3 : (Bool "for" (Set (Var "Y")) "being" ($#m1_hidden :::"set"::: ) (Bool "for" (Set (Var "f")) "being" (Set (Var "b1")) ($#v5_relat_1 :::"-valued"::: ) ($#m1_hidden :::"Relation":::) "holds" (Bool "(" (Bool (Set (Var "f")) "is" ($#v2_funct_2 :::"onto"::: ) ) "iff" (Bool (Set ($#k2_relset_1 :::"rng"::: ) (Set (Var "f"))) ($#r1_hidden :::"="::: ) (Set (Var "Y"))) ")" ))); theorem :: FUNCT_2:23 (Bool "for" (Set (Var "X")) "," (Set (Var "Y")) "being" ($#m1_hidden :::"set"::: ) (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 "X")) "st" (Bool (Bool (Set (Set (Var "g")) ($#k1_partfun1 :::"*"::: ) (Set (Var "f"))) ($#r2_relset_1 :::"="::: ) (Set ($#k6_partfun1 :::"id"::: ) (Set (Var "X"))))) "holds" (Bool "(" (Bool (Set (Var "f")) "is" ($#v2_funct_1 :::"one-to-one"::: ) ) & (Bool (Set (Var "g")) "is" ($#v2_funct_2 :::"onto"::: ) ) ")" )))) ; theorem :: FUNCT_2:24 (Bool "for" (Set (Var "X")) "," (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 (Var "Y")) (Bool "for" (Set (Var "g")) "being" ($#m1_subset_1 :::"Function":::) "of" (Set (Var "Y")) "," (Set (Var "Z")) "st" (Bool "(" (Bool (Bool (Set (Var "Z")) ($#r1_hidden :::"="::: ) (Set ($#k1_xboole_0 :::"{}"::: ) ))) "implies" (Bool (Set (Var "Y")) ($#r1_hidden :::"="::: ) (Set ($#k1_xboole_0 :::"{}"::: ) )) ")" & (Bool (Set (Set (Var "g")) ($#k1_partfun1 :::"*"::: ) (Set (Var "f"))) "is" ($#v2_funct_1 :::"one-to-one"::: ) ) & (Bool (Set ($#k2_relset_1 :::"rng"::: ) (Set (Var "f"))) ($#r1_hidden :::"="::: ) (Set (Var "Y")))) "holds" (Bool "(" (Bool (Set (Var "f")) "is" ($#v2_funct_1 :::"one-to-one"::: ) ) & (Bool (Set (Var "g")) "is" ($#v2_funct_1 :::"one-to-one"::: ) ) ")" )))) ; theorem :: FUNCT_2:25 (Bool "for" (Set (Var "X")) "," (Set (Var "Y")) "being" ($#m1_hidden :::"set"::: ) (Bool "for" (Set (Var "f")) "being" ($#m1_subset_1 :::"Function":::) "of" (Set (Var "X")) "," (Set (Var "Y")) "st" (Bool (Bool (Set (Var "f")) "is" ($#v2_funct_1 :::"one-to-one"::: ) ) & (Bool (Set ($#k2_relset_1 :::"rng"::: ) (Set (Var "f"))) ($#r1_hidden :::"="::: ) (Set (Var "Y")))) "holds" (Bool (Set (Set (Var "f")) ($#k2_funct_1 :::"""::: ) ) "is" ($#m1_subset_1 :::"Function":::) "of" (Set (Var "Y")) "," (Set (Var "X"))))) ; theorem :: FUNCT_2:26 (Bool "for" (Set (Var "X")) "," (Set (Var "Y")) "," (Set (Var "x")) "being" ($#m1_hidden :::"set"::: ) (Bool "for" (Set (Var "f")) "being" ($#m1_subset_1 :::"Function":::) "of" (Set (Var "X")) "," (Set (Var "Y")) "st" (Bool (Bool (Set (Var "Y")) ($#r1_hidden :::"<>"::: ) (Set ($#k1_xboole_0 :::"{}"::: ) )) & (Bool (Set (Var "f")) "is" ($#v2_funct_1 :::"one-to-one"::: ) ) & (Bool (Set (Var "x")) ($#r2_hidden :::"in"::: ) (Set (Var "X")))) "holds" (Bool (Set (Set "(" (Set (Var "f")) ($#k2_funct_1 :::"""::: ) ")" ) ($#k1_funct_1 :::"."::: ) (Set "(" (Set (Var "f")) ($#k1_funct_1 :::"."::: ) (Set (Var "x")) ")" )) ($#r1_hidden :::"="::: ) (Set (Var "x"))))) ; theorem :: FUNCT_2:27 (Bool "for" (Set (Var "X")) "being" ($#m1_hidden :::"set"::: ) (Bool "for" (Set (Var "Y")) "," (Set (Var "Z")) "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 "g")) "being" ($#m1_subset_1 :::"Function":::) "of" (Set (Var "Y")) "," (Set (Var "Z")) "st" (Bool (Bool (Set (Var "f")) "is" ($#v2_funct_2 :::"onto"::: ) ) & (Bool (Set (Var "g")) "is" ($#v2_funct_2 :::"onto"::: ) )) "holds" (Bool (Set (Set (Var "g")) ($#k1_partfun1 :::"*"::: ) (Set (Var "f"))) "is" ($#v2_funct_2 :::"onto"::: ) ))))) ; theorem :: FUNCT_2:28 (Bool "for" (Set (Var "X")) "," (Set (Var "Y")) "being" ($#m1_hidden :::"set"::: ) (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 "X")) "st" (Bool (Bool (Set (Var "X")) ($#r1_hidden :::"<>"::: ) (Set ($#k1_xboole_0 :::"{}"::: ) )) & (Bool (Set (Var "Y")) ($#r1_hidden :::"<>"::: ) (Set ($#k1_xboole_0 :::"{}"::: ) )) & (Bool (Set ($#k2_relset_1 :::"rng"::: ) (Set (Var "f"))) ($#r1_hidden :::"="::: ) (Set (Var "Y"))) & (Bool (Set (Var "f")) "is" ($#v2_funct_1 :::"one-to-one"::: ) ) & (Bool "(" "for" (Set (Var "y")) "," (Set (Var "x")) "being" ($#m1_hidden :::"set"::: ) "holds" (Bool "(" (Bool (Set (Var "y")) ($#r2_hidden :::"in"::: ) (Set (Var "Y"))) & (Bool (Set (Set (Var "g")) ($#k1_funct_1 :::"."::: ) (Set (Var "y"))) ($#r1_hidden :::"="::: ) (Set (Var "x"))) "iff" (Bool "(" (Bool (Set (Var "x")) ($#r2_hidden :::"in"::: ) (Set (Var "X"))) & (Bool (Set (Set (Var "f")) ($#k1_funct_1 :::"."::: ) (Set (Var "x"))) ($#r1_hidden :::"="::: ) (Set (Var "y"))) ")" ) ")" ) ")" )) "holds" (Bool (Set (Var "g")) ($#r1_hidden :::"="::: ) (Set (Set (Var "f")) ($#k2_funct_1 :::"""::: ) ))))) ; theorem :: FUNCT_2:29 (Bool "for" (Set (Var "X")) "," (Set (Var "Y")) "being" ($#m1_hidden :::"set"::: ) (Bool "for" (Set (Var "f")) "being" ($#m1_subset_1 :::"Function":::) "of" (Set (Var "X")) "," (Set (Var "Y")) "st" (Bool (Bool (Set (Var "Y")) ($#r1_hidden :::"<>"::: ) (Set ($#k1_xboole_0 :::"{}"::: ) )) & (Bool (Set ($#k2_relset_1 :::"rng"::: ) (Set (Var "f"))) ($#r1_hidden :::"="::: ) (Set (Var "Y"))) & (Bool (Set (Var "f")) "is" ($#v2_funct_1 :::"one-to-one"::: ) )) "holds" (Bool "(" (Bool (Set (Set "(" (Set (Var "f")) ($#k2_funct_1 :::"""::: ) ")" ) ($#k3_relat_1 :::"*"::: ) (Set (Var "f"))) ($#r1_hidden :::"="::: ) (Set ($#k6_partfun1 :::"id"::: ) (Set (Var "X")))) & (Bool (Set (Set (Var "f")) ($#k3_relat_1 :::"*"::: ) (Set "(" (Set (Var "f")) ($#k2_funct_1 :::"""::: ) ")" )) ($#r1_hidden :::"="::: ) (Set ($#k6_partfun1 :::"id"::: ) (Set (Var "Y")))) ")" ))) ; theorem :: FUNCT_2:30 (Bool "for" (Set (Var "X")) "," (Set (Var "Y")) "being" ($#m1_hidden :::"set"::: ) (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 "X")) "st" (Bool (Bool (Set (Var "X")) ($#r1_hidden :::"<>"::: ) (Set ($#k1_xboole_0 :::"{}"::: ) )) & (Bool (Set (Var "Y")) ($#r1_hidden :::"<>"::: ) (Set ($#k1_xboole_0 :::"{}"::: ) )) & (Bool (Set ($#k2_relset_1 :::"rng"::: ) (Set (Var "f"))) ($#r1_hidden :::"="::: ) (Set (Var "Y"))) & (Bool (Set (Set (Var "g")) ($#k1_partfun1 :::"*"::: ) (Set (Var "f"))) ($#r2_relset_1 :::"="::: ) (Set ($#k6_partfun1 :::"id"::: ) (Set (Var "X")))) & (Bool (Set (Var "f")) "is" ($#v2_funct_1 :::"one-to-one"::: ) )) "holds" (Bool (Set (Var "g")) ($#r1_hidden :::"="::: ) (Set (Set (Var "f")) ($#k2_funct_1 :::"""::: ) ))))) ; theorem :: FUNCT_2:31 (Bool "for" (Set (Var "X")) "," (Set (Var "Y")) "being" ($#m1_hidden :::"set"::: ) (Bool "for" (Set (Var "f")) "being" ($#m1_subset_1 :::"Function":::) "of" (Set (Var "X")) "," (Set (Var "Y")) "st" (Bool (Bool (Set (Var "Y")) ($#r1_hidden :::"<>"::: ) (Set ($#k1_xboole_0 :::"{}"::: ) )) & (Bool "ex" (Set (Var "g")) "being" ($#m1_subset_1 :::"Function":::) "of" (Set (Var "Y")) "," (Set (Var "X")) "st" (Bool (Set (Set (Var "g")) ($#k1_partfun1 :::"*"::: ) (Set (Var "f"))) ($#r2_relset_1 :::"="::: ) (Set ($#k6_partfun1 :::"id"::: ) (Set (Var "X")))))) "holds" (Bool (Set (Var "f")) "is" ($#v2_funct_1 :::"one-to-one"::: ) ))) ; theorem :: FUNCT_2:32 (Bool "for" (Set (Var "X")) "," (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 (Var "Y")) "st" (Bool "(" (Bool (Bool (Set (Var "Y")) ($#r1_hidden :::"="::: ) (Set ($#k1_xboole_0 :::"{}"::: ) ))) "implies" (Bool (Set (Var "X")) ($#r1_hidden :::"="::: ) (Set ($#k1_xboole_0 :::"{}"::: ) )) ")" & (Bool (Set (Var "Z")) ($#r1_tarski :::"c="::: ) (Set (Var "X")))) "holds" (Bool (Set (Set (Var "f")) ($#k2_partfun1 :::"|"::: ) (Set (Var "Z"))) "is" ($#m1_subset_1 :::"Function":::) "of" (Set (Var "Z")) "," (Set (Var "Y"))))) ; theorem :: FUNCT_2:33 (Bool "for" (Set (Var "X")) "," (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 (Var "Y")) "st" (Bool (Bool (Set (Var "X")) ($#r1_tarski :::"c="::: ) (Set (Var "Z")))) "holds" (Bool (Set (Set (Var "f")) ($#k2_partfun1 :::"|"::: ) (Set (Var "Z"))) ($#r2_relset_1 :::"="::: ) (Set (Var "f"))))) ; theorem :: FUNCT_2:34 (Bool "for" (Set (Var "X")) "," (Set (Var "Y")) "," (Set (Var "x")) "," (Set (Var "Z")) "being" ($#m1_hidden :::"set"::: ) (Bool "for" (Set (Var "f")) "being" ($#m1_subset_1 :::"Function":::) "of" (Set (Var "X")) "," (Set (Var "Y")) "st" (Bool (Bool (Set (Var "Y")) ($#r1_hidden :::"<>"::: ) (Set ($#k1_xboole_0 :::"{}"::: ) )) & (Bool (Set (Var "x")) ($#r2_hidden :::"in"::: ) (Set (Var "X"))) & (Bool (Set (Set (Var "f")) ($#k1_funct_1 :::"."::: ) (Set (Var "x"))) ($#r2_hidden :::"in"::: ) (Set (Var "Z")))) "holds" (Bool (Set (Set "(" (Set (Var "Z")) ($#k6_relset_1 :::"|`"::: ) (Set (Var "f")) ")" ) ($#k1_funct_1 :::"."::: ) (Set (Var "x"))) ($#r1_hidden :::"="::: ) (Set (Set (Var "f")) ($#k1_funct_1 :::"."::: ) (Set (Var "x")))))) ; theorem :: FUNCT_2:35 (Bool "for" (Set (Var "X")) "," (Set (Var "Y")) "," (Set (Var "P")) "being" ($#m1_hidden :::"set"::: ) (Bool "for" (Set (Var "f")) "being" ($#m1_subset_1 :::"Function":::) "of" (Set (Var "X")) "," (Set (Var "Y")) "st" (Bool (Bool (Set (Var "Y")) ($#r1_hidden :::"<>"::: ) (Set ($#k1_xboole_0 :::"{}"::: ) ))) "holds" (Bool "for" (Set (Var "y")) "being" ($#m1_hidden :::"set"::: ) "st" (Bool (Bool "ex" (Set (Var "x")) "being" ($#m1_hidden :::"set"::: ) "st" (Bool "(" (Bool (Set (Var "x")) ($#r2_hidden :::"in"::: ) (Set (Var "X"))) & (Bool (Set (Var "x")) ($#r2_hidden :::"in"::: ) (Set (Var "P"))) & (Bool (Set (Var "y")) ($#r1_hidden :::"="::: ) (Set (Set (Var "f")) ($#k1_funct_1 :::"."::: ) (Set (Var "x")))) ")" ))) "holds" (Bool (Set (Var "y")) ($#r2_hidden :::"in"::: ) (Set (Set (Var "f")) ($#k7_relset_1 :::".:"::: ) (Set (Var "P"))))))) ; theorem :: FUNCT_2:36 (Bool "for" (Set (Var "X")) "," (Set (Var "Y")) "," (Set (Var "P")) "being" ($#m1_hidden :::"set"::: ) (Bool "for" (Set (Var "f")) "being" ($#m1_subset_1 :::"Function":::) "of" (Set (Var "X")) "," (Set (Var "Y")) "holds" (Bool (Set (Set (Var "f")) ($#k7_relset_1 :::".:"::: ) (Set (Var "P"))) ($#r1_tarski :::"c="::: ) (Set (Var "Y"))))) ; theorem :: FUNCT_2:37 canceled; theorem :: FUNCT_2:38 (Bool "for" (Set (Var "X")) "," (Set (Var "Y")) "," (Set (Var "Q")) "being" ($#m1_hidden :::"set"::: ) (Bool "for" (Set (Var "f")) "being" ($#m1_subset_1 :::"Function":::) "of" (Set (Var "X")) "," (Set (Var "Y")) "st" (Bool (Bool (Set (Var "Y")) ($#r1_hidden :::"<>"::: ) (Set ($#k1_xboole_0 :::"{}"::: ) ))) "holds" (Bool "for" (Set (Var "x")) "being" ($#m1_hidden :::"set"::: ) "holds" (Bool "(" (Bool (Set (Var "x")) ($#r2_hidden :::"in"::: ) (Set (Set (Var "f")) ($#k8_relset_1 :::"""::: ) (Set (Var "Q")))) "iff" (Bool "(" (Bool (Set (Var "x")) ($#r2_hidden :::"in"::: ) (Set (Var "X"))) & (Bool (Set (Set (Var "f")) ($#k1_funct_1 :::"."::: ) (Set (Var "x"))) ($#r2_hidden :::"in"::: ) (Set (Var "Q"))) ")" ) ")" )))) ; theorem :: FUNCT_2:39 (Bool "for" (Set (Var "X")) "," (Set (Var "Y")) "," (Set (Var "Q")) "being" ($#m1_hidden :::"set"::: ) (Bool "for" (Set (Var "f")) "being" ($#m1_subset_1 :::"PartFunc":::) "of" (Set (Var "X")) "," (Set (Var "Y")) "holds" (Bool (Set (Set (Var "f")) ($#k8_relset_1 :::"""::: ) (Set (Var "Q"))) ($#r1_tarski :::"c="::: ) (Set (Var "X"))))) ; theorem :: FUNCT_2:40 (Bool "for" (Set (Var "X")) "," (Set (Var "Y")) "being" ($#m1_hidden :::"set"::: ) (Bool "for" (Set (Var "f")) "being" ($#m1_subset_1 :::"Function":::) "of" (Set (Var "X")) "," (Set (Var "Y")) "st" (Bool "(" (Bool (Bool (Set (Var "Y")) ($#r1_hidden :::"="::: ) (Set ($#k1_xboole_0 :::"{}"::: ) ))) "implies" (Bool (Set (Var "X")) ($#r1_hidden :::"="::: ) (Set ($#k1_xboole_0 :::"{}"::: ) )) ")" ) "holds" (Bool (Set (Set (Var "f")) ($#k8_relset_1 :::"""::: ) (Set (Var "Y"))) ($#r1_hidden :::"="::: ) (Set (Var "X"))))) ; theorem :: FUNCT_2:41 (Bool "for" (Set (Var "X")) "," (Set (Var "Y")) "being" ($#m1_hidden :::"set"::: ) (Bool "for" (Set (Var "f")) "being" ($#m1_subset_1 :::"Function":::) "of" (Set (Var "X")) "," (Set (Var "Y")) "holds" (Bool "(" (Bool "(" "for" (Set (Var "y")) "being" ($#m1_hidden :::"set"::: ) "st" (Bool (Bool (Set (Var "y")) ($#r2_hidden :::"in"::: ) (Set (Var "Y")))) "holds" (Bool (Set (Set (Var "f")) ($#k8_relset_1 :::"""::: ) (Set ($#k1_tarski :::"{"::: ) (Set (Var "y")) ($#k1_tarski :::"}"::: ) )) ($#r1_hidden :::"<>"::: ) (Set ($#k1_xboole_0 :::"{}"::: ) )) ")" ) "iff" (Bool (Set ($#k2_relset_1 :::"rng"::: ) (Set (Var "f"))) ($#r1_hidden :::"="::: ) (Set (Var "Y"))) ")" ))) ; theorem :: FUNCT_2:42 (Bool "for" (Set (Var "X")) "," (Set (Var "Y")) "," (Set (Var "P")) "being" ($#m1_hidden :::"set"::: ) (Bool "for" (Set (Var "f")) "being" ($#m1_subset_1 :::"Function":::) "of" (Set (Var "X")) "," (Set (Var "Y")) "st" (Bool "(" (Bool (Bool (Set (Var "Y")) ($#r1_hidden :::"="::: ) (Set ($#k1_xboole_0 :::"{}"::: ) ))) "implies" (Bool (Set (Var "X")) ($#r1_hidden :::"="::: ) (Set ($#k1_xboole_0 :::"{}"::: ) )) ")" & (Bool (Set (Var "P")) ($#r1_tarski :::"c="::: ) (Set (Var "X")))) "holds" (Bool (Set (Var "P")) ($#r1_tarski :::"c="::: ) (Set (Set (Var "f")) ($#k8_relset_1 :::"""::: ) (Set "(" (Set (Var "f")) ($#k7_relset_1 :::".:"::: ) (Set (Var "P")) ")" ))))) ; theorem :: FUNCT_2:43 (Bool "for" (Set (Var "X")) "," (Set (Var "Y")) "being" ($#m1_hidden :::"set"::: ) (Bool "for" (Set (Var "f")) "being" ($#m1_subset_1 :::"Function":::) "of" (Set (Var "X")) "," (Set (Var "Y")) "st" (Bool "(" (Bool (Bool (Set (Var "Y")) ($#r1_hidden :::"="::: ) (Set ($#k1_xboole_0 :::"{}"::: ) ))) "implies" (Bool (Set (Var "X")) ($#r1_hidden :::"="::: ) (Set ($#k1_xboole_0 :::"{}"::: ) )) ")" ) "holds" (Bool (Set (Set (Var "f")) ($#k8_relset_1 :::"""::: ) (Set "(" (Set (Var "f")) ($#k7_relset_1 :::".:"::: ) (Set (Var "X")) ")" )) ($#r1_hidden :::"="::: ) (Set (Var "X"))))) ; theorem :: FUNCT_2:44 (Bool "for" (Set (Var "X")) "," (Set (Var "Y")) "," (Set (Var "Z")) "," (Set (Var "Q")) "being" ($#m1_hidden :::"set"::: ) (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 (Bool (Set (Var "Z")) ($#r1_hidden :::"="::: ) (Set ($#k1_xboole_0 :::"{}"::: ) ))) "implies" (Bool (Set (Var "Y")) ($#r1_hidden :::"="::: ) (Set ($#k1_xboole_0 :::"{}"::: ) )) ")" ) "holds" (Bool (Set (Set (Var "f")) ($#k8_relset_1 :::"""::: ) (Set (Var "Q"))) ($#r1_tarski :::"c="::: ) (Set (Set "(" (Set (Var "g")) ($#k1_partfun1 :::"*"::: ) (Set (Var "f")) ")" ) ($#k8_relset_1 :::"""::: ) (Set "(" (Set (Var "g")) ($#k7_relset_1 :::".:"::: ) (Set (Var "Q")) ")" )))))) ; theorem :: FUNCT_2:45 (Bool "for" (Set (Var "Y")) "," (Set (Var "P")) "being" ($#m1_hidden :::"set"::: ) (Bool "for" (Set (Var "f")) "being" ($#m1_subset_1 :::"Function":::) "of" (Set ($#k1_xboole_0 :::"{}"::: ) ) "," (Set (Var "Y")) "holds" (Bool (Set (Set (Var "f")) ($#k7_relset_1 :::".:"::: ) (Set (Var "P"))) ($#r1_hidden :::"="::: ) (Set ($#k1_xboole_0 :::"{}"::: ) )))) ; theorem :: FUNCT_2:46 (Bool "for" (Set (Var "Y")) "," (Set (Var "Q")) "being" ($#m1_hidden :::"set"::: ) (Bool "for" (Set (Var "f")) "being" ($#m1_subset_1 :::"Function":::) "of" (Set ($#k1_xboole_0 :::"{}"::: ) ) "," (Set (Var "Y")) "holds" (Bool (Set (Set (Var "f")) ($#k8_relset_1 :::"""::: ) (Set (Var "Q"))) ($#r1_hidden :::"="::: ) (Set ($#k1_xboole_0 :::"{}"::: ) )))) ; theorem :: FUNCT_2:47 (Bool "for" (Set (Var "x")) "," (Set (Var "Y")) "being" ($#m1_hidden :::"set"::: ) (Bool "for" (Set (Var "f")) "being" ($#m1_subset_1 :::"Function":::) "of" (Set ($#k1_tarski :::"{"::: ) (Set (Var "x")) ($#k1_tarski :::"}"::: ) ) "," (Set (Var "Y")) "st" (Bool (Bool (Set (Var "Y")) ($#r1_hidden :::"<>"::: ) (Set ($#k1_xboole_0 :::"{}"::: ) ))) "holds" (Bool (Set (Set (Var "f")) ($#k1_funct_1 :::"."::: ) (Set (Var "x"))) ($#r2_hidden :::"in"::: ) (Set (Var "Y"))))) ; theorem :: FUNCT_2:48 (Bool "for" (Set (Var "x")) "," (Set (Var "Y")) "being" ($#m1_hidden :::"set"::: ) (Bool "for" (Set (Var "f")) "being" ($#m1_subset_1 :::"Function":::) "of" (Set ($#k1_tarski :::"{"::: ) (Set (Var "x")) ($#k1_tarski :::"}"::: ) ) "," (Set (Var "Y")) "st" (Bool (Bool (Set (Var "Y")) ($#r1_hidden :::"<>"::: ) (Set ($#k1_xboole_0 :::"{}"::: ) ))) "holds" (Bool (Set ($#k2_relset_1 :::"rng"::: ) (Set (Var "f"))) ($#r1_hidden :::"="::: ) (Set ($#k1_tarski :::"{"::: ) (Set "(" (Set (Var "f")) ($#k1_funct_1 :::"."::: ) (Set (Var "x")) ")" ) ($#k1_tarski :::"}"::: ) )))) ; theorem :: FUNCT_2:49 (Bool "for" (Set (Var "x")) "," (Set (Var "Y")) "," (Set (Var "P")) "being" ($#m1_hidden :::"set"::: ) (Bool "for" (Set (Var "f")) "being" ($#m1_subset_1 :::"Function":::) "of" (Set ($#k1_tarski :::"{"::: ) (Set (Var "x")) ($#k1_tarski :::"}"::: ) ) "," (Set (Var "Y")) "st" (Bool (Bool (Set (Var "Y")) ($#r1_hidden :::"<>"::: ) (Set ($#k1_xboole_0 :::"{}"::: ) ))) "holds" (Bool (Set (Set (Var "f")) ($#k7_relset_1 :::".:"::: ) (Set (Var "P"))) ($#r1_tarski :::"c="::: ) (Set ($#k1_tarski :::"{"::: ) (Set "(" (Set (Var "f")) ($#k1_funct_1 :::"."::: ) (Set (Var "x")) ")" ) ($#k1_tarski :::"}"::: ) )))) ; theorem :: FUNCT_2:50 (Bool "for" (Set (Var "X")) "," (Set (Var "y")) "," (Set (Var "x")) "being" ($#m1_hidden :::"set"::: ) (Bool "for" (Set (Var "f")) "being" ($#m1_subset_1 :::"Function":::) "of" (Set (Var "X")) "," (Set ($#k1_tarski :::"{"::: ) (Set (Var "y")) ($#k1_tarski :::"}"::: ) ) "st" (Bool (Bool (Set (Var "x")) ($#r2_hidden :::"in"::: ) (Set (Var "X")))) "holds" (Bool (Set (Set (Var "f")) ($#k1_funct_1 :::"."::: ) (Set (Var "x"))) ($#r1_hidden :::"="::: ) (Set (Var "y"))))) ; theorem :: FUNCT_2:51 (Bool "for" (Set (Var "X")) "," (Set (Var "y")) "being" ($#m1_hidden :::"set"::: ) (Bool "for" (Set (Var "f1")) "," (Set (Var "f2")) "being" ($#m1_subset_1 :::"Function":::) "of" (Set (Var "X")) "," (Set ($#k1_tarski :::"{"::: ) (Set (Var "y")) ($#k1_tarski :::"}"::: ) ) "holds" (Bool (Set (Var "f1")) ($#r2_relset_1 :::"="::: ) (Set (Var "f2"))))) ; theorem :: FUNCT_2:52 (Bool "for" (Set (Var "X")) "being" ($#m1_hidden :::"set"::: ) (Bool "for" (Set (Var "f")) "being" ($#m1_subset_1 :::"Function":::) "of" (Set (Var "X")) "," (Set (Var "X")) "holds" (Bool (Set ($#k1_relset_1 :::"dom"::: ) (Set (Var "f"))) ($#r1_hidden :::"="::: ) (Set (Var "X"))))) ; registrationlet "X", "Y" be ($#m1_hidden :::"set"::: ) ; let "f" be ($#v1_funct_2 :::"quasi_total"::: ) ($#m1_subset_1 :::"PartFunc":::) "of" (Set (Const "X")) "," (Set (Const "Y")); let "g" be ($#v1_funct_2 :::"quasi_total"::: ) ($#m1_subset_1 :::"PartFunc":::) "of" (Set (Const "X")) "," (Set (Const "X")); cluster (Set "g" ($#k3_relat_1 :::"*"::: ) "f") -> ($#v1_funct_2 :::"quasi_total"::: ) for ($#m1_subset_1 :::"PartFunc":::) "of" "X" "," "Y"; end; registrationlet "X", "Y" be ($#m1_hidden :::"set"::: ) ; let "f" be ($#v1_funct_2 :::"quasi_total"::: ) ($#m1_subset_1 :::"PartFunc":::) "of" (Set (Const "Y")) "," (Set (Const "Y")); let "g" be ($#v1_funct_2 :::"quasi_total"::: ) ($#m1_subset_1 :::"PartFunc":::) "of" (Set (Const "X")) "," (Set (Const "Y")); cluster (Set "g" ($#k3_relat_1 :::"*"::: ) "f") -> ($#v1_funct_2 :::"quasi_total"::: ) for ($#m1_subset_1 :::"PartFunc":::) "of" "X" "," "Y"; end; theorem :: FUNCT_2:53 (Bool "for" (Set (Var "X")) "being" ($#m1_hidden :::"set"::: ) (Bool "for" (Set (Var "f")) "," (Set (Var "g")) "being" ($#m1_subset_1 :::"Relation":::) "of" (Set (Var "X")) "," (Set (Var "X")) "st" (Bool (Bool (Set ($#k2_relset_1 :::"rng"::: ) (Set (Var "f"))) ($#r1_hidden :::"="::: ) (Set (Var "X"))) & (Bool (Set ($#k2_relset_1 :::"rng"::: ) (Set (Var "g"))) ($#r1_hidden :::"="::: ) (Set (Var "X")))) "holds" (Bool (Set ($#k2_relset_1 :::"rng"::: ) (Set "(" (Set (Var "g")) ($#k4_relset_1 :::"*"::: ) (Set (Var "f")) ")" )) ($#r1_hidden :::"="::: ) (Set (Var "X"))))) ; theorem :: FUNCT_2:54 (Bool "for" (Set (Var "X")) "being" ($#m1_hidden :::"set"::: ) (Bool "for" (Set (Var "f")) "," (Set (Var "g")) "being" ($#m1_subset_1 :::"Function":::) "of" (Set (Var "X")) "," (Set (Var "X")) "st" (Bool (Bool (Set (Set (Var "g")) ($#k1_partfun1 :::"*"::: ) (Set (Var "f"))) ($#r2_relset_1 :::"="::: ) (Set (Var "f"))) & (Bool (Set ($#k2_relset_1 :::"rng"::: ) (Set (Var "f"))) ($#r1_hidden :::"="::: ) (Set (Var "X")))) "holds" (Bool (Set (Var "g")) ($#r2_relset_1 :::"="::: ) (Set ($#k6_partfun1 :::"id"::: ) (Set (Var "X")))))) ; theorem :: FUNCT_2:55 (Bool "for" (Set (Var "X")) "being" ($#m1_hidden :::"set"::: ) (Bool "for" (Set (Var "f")) "," (Set (Var "g")) "being" ($#m1_subset_1 :::"Function":::) "of" (Set (Var "X")) "," (Set (Var "X")) "st" (Bool (Bool (Set (Set (Var "f")) ($#k1_partfun1 :::"*"::: ) (Set (Var "g"))) ($#r2_relset_1 :::"="::: ) (Set (Var "f"))) & (Bool (Set (Var "f")) "is" ($#v2_funct_1 :::"one-to-one"::: ) )) "holds" (Bool (Set (Var "g")) ($#r2_relset_1 :::"="::: ) (Set ($#k6_partfun1 :::"id"::: ) (Set (Var "X")))))) ; theorem :: FUNCT_2:56 (Bool "for" (Set (Var "X")) "being" ($#m1_hidden :::"set"::: ) (Bool "for" (Set (Var "f")) "being" ($#m1_subset_1 :::"Function":::) "of" (Set (Var "X")) "," (Set (Var "X")) "holds" (Bool "(" (Bool (Set (Var "f")) "is" ($#v2_funct_1 :::"one-to-one"::: ) ) "iff" (Bool "for" (Set (Var "x1")) "," (Set (Var "x2")) "being" ($#m1_hidden :::"set"::: ) "st" (Bool (Bool (Set (Var "x1")) ($#r2_hidden :::"in"::: ) (Set (Var "X"))) & (Bool (Set (Var "x2")) ($#r2_hidden :::"in"::: ) (Set (Var "X"))) & (Bool (Set (Set (Var "f")) ($#k1_funct_1 :::"."::: ) (Set (Var "x1"))) ($#r1_hidden :::"="::: ) (Set (Set (Var "f")) ($#k1_funct_1 :::"."::: ) (Set (Var "x2"))))) "holds" (Bool (Set (Var "x1")) ($#r1_hidden :::"="::: ) (Set (Var "x2")))) ")" ))) ; definitionlet "X", "Y" be ($#m1_hidden :::"set"::: ) ; let "f" be (Set (Const "X")) ($#v4_relat_1 :::"-defined"::: ) (Set (Const "Y")) ($#v5_relat_1 :::"-valued"::: ) ($#m1_hidden :::"Function":::); attr "f" is :::"bijective"::: means :: FUNCT_2:def 4 (Bool "(" (Bool "f" "is" ($#v2_funct_1 :::"one-to-one"::: ) ) & (Bool "f" "is" ($#v2_funct_2 :::"onto"::: ) ) ")" ); end; :: deftheorem defines :::"bijective"::: FUNCT_2:def 4 : (Bool "for" (Set (Var "X")) "," (Set (Var "Y")) "being" ($#m1_hidden :::"set"::: ) (Bool "for" (Set (Var "f")) "being" (Set (Var "b1")) ($#v4_relat_1 :::"-defined"::: ) (Set (Var "b2")) ($#v5_relat_1 :::"-valued"::: ) ($#m1_hidden :::"Function":::) "holds" (Bool "(" (Bool (Set (Var "f")) "is" ($#v3_funct_2 :::"bijective"::: ) ) "iff" (Bool "(" (Bool (Set (Var "f")) "is" ($#v2_funct_1 :::"one-to-one"::: ) ) & (Bool (Set (Var "f")) "is" ($#v2_funct_2 :::"onto"::: ) ) ")" ) ")" ))); registrationlet "X", "Y" be ($#m1_hidden :::"set"::: ) ; cluster ($#v1_funct_1 :::"Function-like"::: ) ($#v3_funct_2 :::"bijective"::: ) -> ($#v2_funct_1 :::"one-to-one"::: ) ($#v2_funct_2 :::"onto"::: ) for ($#m1_subset_1 :::"Element"::: ) "of" (Set ($#k1_zfmisc_1 :::"bool"::: ) (Set ($#k2_zfmisc_1 :::"[:"::: ) "X" "," "Y" ($#k2_zfmisc_1 :::":]"::: ) )); cluster ($#v1_funct_1 :::"Function-like"::: ) ($#v2_funct_1 :::"one-to-one"::: ) ($#v2_funct_2 :::"onto"::: ) -> ($#v3_funct_2 :::"bijective"::: ) for ($#m1_subset_1 :::"Element"::: ) "of" (Set ($#k1_zfmisc_1 :::"bool"::: ) (Set ($#k2_zfmisc_1 :::"[:"::: ) "X" "," "Y" ($#k2_zfmisc_1 :::":]"::: ) )); end; registrationlet "X" be ($#m1_hidden :::"set"::: ) ; cluster ($#v1_relat_1 :::"Relation-like"::: ) "X" ($#v4_relat_1 :::"-defined"::: ) "X" ($#v5_relat_1 :::"-valued"::: ) ($#v1_funct_1 :::"Function-like"::: ) ($#v1_partfun1 :::"total"::: ) ($#v1_funct_2 :::"quasi_total"::: ) ($#v3_funct_2 :::"bijective"::: ) for ($#m1_subset_1 :::"Element"::: ) "of" (Set ($#k1_zfmisc_1 :::"bool"::: ) (Set ($#k2_zfmisc_1 :::"[:"::: ) "X" "," "X" ($#k2_zfmisc_1 :::":]"::: ) )); end; definitionlet "X" be ($#m1_hidden :::"set"::: ) ; mode Permutation of "X" is ($#v3_funct_2 :::"bijective"::: ) ($#m1_subset_1 :::"Function":::) "of" "X" "," "X"; end; theorem :: FUNCT_2:57 (Bool "for" (Set (Var "X")) "being" ($#m1_hidden :::"set"::: ) (Bool "for" (Set (Var "f")) "being" ($#m1_subset_1 :::"Function":::) "of" (Set (Var "X")) "," (Set (Var "X")) "st" (Bool (Bool (Set (Var "f")) "is" ($#v2_funct_1 :::"one-to-one"::: ) ) & (Bool (Set ($#k2_relset_1 :::"rng"::: ) (Set (Var "f"))) ($#r1_hidden :::"="::: ) (Set (Var "X")))) "holds" (Bool (Set (Var "f")) "is" ($#m1_subset_1 :::"Permutation":::) "of" (Set (Var "X"))))) ; theorem :: FUNCT_2:58 (Bool "for" (Set (Var "X")) "being" ($#m1_hidden :::"set"::: ) (Bool "for" (Set (Var "f")) "being" ($#m1_subset_1 :::"Function":::) "of" (Set (Var "X")) "," (Set (Var "X")) "st" (Bool (Bool (Set (Var "f")) "is" ($#v2_funct_1 :::"one-to-one"::: ) )) "holds" (Bool "for" (Set (Var "x1")) "," (Set (Var "x2")) "being" ($#m1_hidden :::"set"::: ) "st" (Bool (Bool (Set (Var "x1")) ($#r2_hidden :::"in"::: ) (Set (Var "X"))) & (Bool (Set (Var "x2")) ($#r2_hidden :::"in"::: ) (Set (Var "X"))) & (Bool (Set (Set (Var "f")) ($#k1_funct_1 :::"."::: ) (Set (Var "x1"))) ($#r1_hidden :::"="::: ) (Set (Set (Var "f")) ($#k1_funct_1 :::"."::: ) (Set (Var "x2"))))) "holds" (Bool (Set (Var "x1")) ($#r1_hidden :::"="::: ) (Set (Var "x2")))))) ; registrationlet "X" be ($#m1_hidden :::"set"::: ) ; let "f", "g" be ($#v2_funct_2 :::"onto"::: ) ($#m1_subset_1 :::"PartFunc":::) "of" (Set (Const "X")) "," (Set (Const "X")); cluster (Set "g" ($#k3_relat_1 :::"*"::: ) "f") -> ($#v2_funct_2 :::"onto"::: ) for ($#m1_subset_1 :::"PartFunc":::) "of" "X" "," "X"; end; registrationlet "X" be ($#m1_hidden :::"set"::: ) ; let "f", "g" be ($#v3_funct_2 :::"bijective"::: ) ($#m1_subset_1 :::"Function":::) "of" (Set (Const "X")) "," (Set (Const "X")); cluster (Set "f" ($#k3_relat_1 :::"*"::: ) "g") -> ($#v3_funct_2 :::"bijective"::: ) for ($#m1_subset_1 :::"Function":::) "of" "X" "," "X"; end; registrationlet "X" be ($#m1_hidden :::"set"::: ) ; cluster ($#v1_relat_2 :::"reflexive"::: ) ($#v1_funct_1 :::"Function-like"::: ) ($#v1_partfun1 :::"total"::: ) ($#v1_funct_2 :::"quasi_total"::: ) -> ($#v3_funct_2 :::"bijective"::: ) for ($#m1_subset_1 :::"Element"::: ) "of" (Set ($#k1_zfmisc_1 :::"bool"::: ) (Set ($#k2_zfmisc_1 :::"[:"::: ) "X" "," "X" ($#k2_zfmisc_1 :::":]"::: ) )); end; definitionlet "X" be ($#m1_hidden :::"set"::: ) ; let "f" be ($#m1_subset_1 :::"Permutation":::) "of" (Set (Const "X")); :: original: :::"""::: redefine func "f" :::"""::: -> ($#m1_subset_1 :::"Permutation":::) "of" "X"; end; theorem :: FUNCT_2:59 (Bool "for" (Set (Var "X")) "being" ($#m1_hidden :::"set"::: ) (Bool "for" (Set (Var "f")) "," (Set (Var "g")) "being" ($#m1_subset_1 :::"Permutation":::) "of" (Set (Var "X")) "st" (Bool (Bool (Set (Set (Var "g")) ($#k1_partfun1 :::"*"::: ) (Set (Var "f"))) ($#r2_relset_1 :::"="::: ) (Set (Var "g")))) "holds" (Bool (Set (Var "f")) ($#r2_relset_1 :::"="::: ) (Set ($#k6_partfun1 :::"id"::: ) (Set (Var "X")))))) ; theorem :: FUNCT_2:60 (Bool "for" (Set (Var "X")) "being" ($#m1_hidden :::"set"::: ) (Bool "for" (Set (Var "f")) "," (Set (Var "g")) "being" ($#m1_subset_1 :::"Permutation":::) "of" (Set (Var "X")) "st" (Bool (Bool (Set (Set (Var "g")) ($#k1_partfun1 :::"*"::: ) (Set (Var "f"))) ($#r2_relset_1 :::"="::: ) (Set ($#k6_partfun1 :::"id"::: ) (Set (Var "X"))))) "holds" (Bool (Set (Var "g")) ($#r2_relset_1 :::"="::: ) (Set (Set (Var "f")) ($#k2_funct_2 :::"""::: ) )))) ; theorem :: FUNCT_2:61 (Bool "for" (Set (Var "X")) "being" ($#m1_hidden :::"set"::: ) (Bool "for" (Set (Var "f")) "being" ($#m1_subset_1 :::"Permutation":::) "of" (Set (Var "X")) "holds" (Bool "(" (Bool (Set (Set "(" (Set (Var "f")) ($#k2_funct_2 :::"""::: ) ")" ) ($#k1_partfun1 :::"*"::: ) (Set (Var "f"))) ($#r2_relset_1 :::"="::: ) (Set ($#k6_partfun1 :::"id"::: ) (Set (Var "X")))) & (Bool (Set (Set (Var "f")) ($#k1_partfun1 :::"*"::: ) (Set "(" (Set (Var "f")) ($#k2_funct_2 :::"""::: ) ")" )) ($#r2_relset_1 :::"="::: ) (Set ($#k6_partfun1 :::"id"::: ) (Set (Var "X")))) ")" ))) ; theorem :: FUNCT_2:62 (Bool "for" (Set (Var "X")) "," (Set (Var "P")) "being" ($#m1_hidden :::"set"::: ) (Bool "for" (Set (Var "f")) "being" ($#m1_subset_1 :::"Permutation":::) "of" (Set (Var "X")) "st" (Bool (Bool (Set (Var "P")) ($#r1_tarski :::"c="::: ) (Set (Var "X")))) "holds" (Bool "(" (Bool (Set (Set (Var "f")) ($#k7_relset_1 :::".:"::: ) (Set "(" (Set (Var "f")) ($#k8_relset_1 :::"""::: ) (Set (Var "P")) ")" )) ($#r1_hidden :::"="::: ) (Set (Var "P"))) & (Bool (Set (Set (Var "f")) ($#k8_relset_1 :::"""::: ) (Set "(" (Set (Var "f")) ($#k7_relset_1 :::".:"::: ) (Set (Var "P")) ")" )) ($#r1_hidden :::"="::: ) (Set (Var "P"))) ")" ))) ; registrationlet "X" be ($#m1_hidden :::"set"::: ) ; let "D" be ($#~v1_xboole_0 "non" ($#v1_xboole_0 :::"empty"::: ) ) ($#m1_hidden :::"set"::: ) ; let "Z" be ($#m1_hidden :::"set"::: ) ; let "f" be ($#m1_subset_1 :::"Function":::) "of" (Set (Const "X")) "," (Set (Const "D")); let "g" be ($#m1_subset_1 :::"Function":::) "of" (Set (Const "D")) "," (Set (Const "Z")); cluster (Set "f" ($#k3_relat_1 :::"*"::: ) "g") -> ($#v1_funct_2 :::"quasi_total"::: ) for ($#m1_subset_1 :::"PartFunc":::) "of" "X" "," "Z"; end; definitionlet "C" be ($#~v1_xboole_0 "non" ($#v1_xboole_0 :::"empty"::: ) ) ($#m1_hidden :::"set"::: ) ; let "D" be ($#m1_hidden :::"set"::: ) ; let "f" be ($#m1_subset_1 :::"Function":::) "of" (Set (Const "C")) "," (Set (Const "D")); let "c" be ($#m1_subset_1 :::"Element"::: ) "of" (Set (Const "C")); :: original: :::"."::: redefine func "f" :::"."::: "c" -> ($#m1_subset_1 :::"Element"::: ) "of" "D"; end; scheme :: FUNCT_2:sch 3 FuncExD{ F1() -> ($#~v1_xboole_0 "non" ($#v1_xboole_0 :::"empty"::: ) ) ($#m1_hidden :::"set"::: ) , F2() -> ($#~v1_xboole_0 "non" ($#v1_xboole_0 :::"empty"::: ) ) ($#m1_hidden :::"set"::: ) , P1[ ($#m1_hidden :::"set"::: ) "," ($#m1_hidden :::"set"::: ) ] } : (Bool "ex" (Set (Var "f")) "being" ($#m1_subset_1 :::"Function":::) "of" (Set F1 "(" ")" ) "," (Set F2 "(" ")" ) "st" (Bool "for" (Set (Var "x")) "being" ($#m1_subset_1 :::"Element"::: ) "of" (Set F1 "(" ")" ) "holds" (Bool P1[(Set (Var "x")) "," (Set (Set (Var "f")) ($#k3_funct_2 :::"."::: ) (Set (Var "x")))]))) provided (Bool "for" (Set (Var "x")) "being" ($#m1_subset_1 :::"Element"::: ) "of" (Set F1 "(" ")" ) (Bool "ex" (Set (Var "y")) "being" ($#m1_subset_1 :::"Element"::: ) "of" (Set F2 "(" ")" ) "st" (Bool P1[(Set (Var "x")) "," (Set (Var "y"))]))) proof end; scheme :: FUNCT_2:sch 4 LambdaD{ F1() -> ($#~v1_xboole_0 "non" ($#v1_xboole_0 :::"empty"::: ) ) ($#m1_hidden :::"set"::: ) , F2() -> ($#~v1_xboole_0 "non" ($#v1_xboole_0 :::"empty"::: ) ) ($#m1_hidden :::"set"::: ) , F3( ($#m1_subset_1 :::"Element"::: ) "of" (Set F1 "(" ")" )) -> ($#m1_subset_1 :::"Element"::: ) "of" (Set F2 "(" ")" ) } : (Bool "ex" (Set (Var "f")) "being" ($#m1_subset_1 :::"Function":::) "of" (Set F1 "(" ")" ) "," (Set F2 "(" ")" ) "st" (Bool "for" (Set (Var "x")) "being" ($#m1_subset_1 :::"Element"::: ) "of" (Set F1 "(" ")" ) "holds" (Bool (Set (Set (Var "f")) ($#k3_funct_2 :::"."::: ) (Set (Var "x"))) ($#r1_hidden :::"="::: ) (Set F3 "(" (Set (Var "x")) ")" )))) proof end; theorem :: FUNCT_2:63 (Bool "for" (Set (Var "X")) "," (Set (Var "Y")) "being" ($#m1_hidden :::"set"::: ) (Bool "for" (Set (Var "f1")) "," (Set (Var "f2")) "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")) "holds" (Bool (Set (Set (Var "f1")) ($#k1_funct_1 :::"."::: ) (Set (Var "x"))) ($#r1_hidden :::"="::: ) (Set (Set (Var "f2")) ($#k1_funct_1 :::"."::: ) (Set (Var "x")))) ")" )) "holds" (Bool (Set (Var "f1")) ($#r2_relset_1 :::"="::: ) (Set (Var "f2"))))) ; theorem :: FUNCT_2:64 (Bool "for" (Set (Var "X")) "," (Set (Var "Y")) "," (Set (Var "P")) "being" ($#m1_hidden :::"set"::: ) (Bool "for" (Set (Var "f")) "being" ($#m1_subset_1 :::"Function":::) "of" (Set (Var "X")) "," (Set (Var "Y")) (Bool "for" (Set (Var "y")) "being" ($#m1_hidden :::"set"::: ) "st" (Bool (Bool (Set (Var "y")) ($#r2_hidden :::"in"::: ) (Set (Set (Var "f")) ($#k7_relset_1 :::".:"::: ) (Set (Var "P"))))) "holds" (Bool "ex" (Set (Var "x")) "being" ($#m1_hidden :::"set"::: ) "st" (Bool "(" (Bool (Set (Var "x")) ($#r2_hidden :::"in"::: ) (Set (Var "X"))) & (Bool (Set (Var "x")) ($#r2_hidden :::"in"::: ) (Set (Var "P"))) & (Bool (Set (Var "y")) ($#r1_hidden :::"="::: ) (Set (Set (Var "f")) ($#k1_funct_1 :::"."::: ) (Set (Var "x")))) ")" ))))) ; theorem :: FUNCT_2:65 (Bool "for" (Set (Var "X")) "," (Set (Var "Y")) "," (Set (Var "P")) "being" ($#m1_hidden :::"set"::: ) (Bool "for" (Set (Var "f")) "being" ($#m1_subset_1 :::"Function":::) "of" (Set (Var "X")) "," (Set (Var "Y")) (Bool "for" (Set (Var "y")) "being" ($#m1_hidden :::"set"::: ) "st" (Bool (Bool (Set (Var "y")) ($#r2_hidden :::"in"::: ) (Set (Set (Var "f")) ($#k7_relset_1 :::".:"::: ) (Set (Var "P"))))) "holds" (Bool "ex" (Set (Var "c")) "being" ($#m1_subset_1 :::"Element"::: ) "of" (Set (Var "X")) "st" (Bool "(" (Bool (Set (Var "c")) ($#r2_hidden :::"in"::: ) (Set (Var "P"))) & (Bool (Set (Var "y")) ($#r1_hidden :::"="::: ) (Set (Set (Var "f")) ($#k1_funct_1 :::"."::: ) (Set (Var "c")))) ")" ))))) ; begin theorem :: FUNCT_2:66 (Bool "for" (Set (Var "X")) "," (Set (Var "Y")) "," (Set (Var "f")) "being" ($#m1_hidden :::"set"::: ) "st" (Bool (Bool (Set (Var "f")) ($#r2_hidden :::"in"::: ) (Set ($#k1_funct_2 :::"Funcs"::: ) "(" (Set (Var "X")) "," (Set (Var "Y")) ")" ))) "holds" (Bool (Set (Var "f")) "is" ($#m1_subset_1 :::"Function":::) "of" (Set (Var "X")) "," (Set (Var "Y")))) ; scheme :: FUNCT_2:sch 5 Lambda1C{ F1() -> ($#m1_hidden :::"set"::: ) , F2() -> ($#m1_hidden :::"set"::: ) , P1[ ($#m1_hidden :::"set"::: ) ], F3( ($#m1_hidden :::"set"::: ) ) -> ($#m1_hidden :::"set"::: ) , F4( ($#m1_hidden :::"set"::: ) ) -> ($#m1_hidden :::"set"::: ) } : (Bool "ex" (Set (Var "f")) "being" ($#m1_subset_1 :::"Function":::) "of" (Set F1 "(" ")" ) "," (Set F2 "(" ")" ) "st" (Bool "for" (Set (Var "x")) "being" ($#m1_hidden :::"set"::: ) "st" (Bool (Bool (Set (Var "x")) ($#r2_hidden :::"in"::: ) (Set F1 "(" ")" ))) "holds" (Bool "(" "(" (Bool (Bool P1[(Set (Var "x"))])) "implies" (Bool (Set (Set (Var "f")) ($#k1_funct_1 :::"."::: ) (Set (Var "x"))) ($#r1_hidden :::"="::: ) (Set F3 "(" (Set (Var "x")) ")" )) ")" & "(" (Bool (Bool P1[(Set (Var "x"))])) "implies" (Bool (Set (Set (Var "f")) ($#k1_funct_1 :::"."::: ) (Set (Var "x"))) ($#r1_hidden :::"="::: ) (Set F4 "(" (Set (Var "x")) ")" )) ")" ")" ))) provided (Bool "for" (Set (Var "x")) "being" ($#m1_hidden :::"set"::: ) "st" (Bool (Bool (Set (Var "x")) ($#r2_hidden :::"in"::: ) (Set F1 "(" ")" ))) "holds" (Bool "(" "(" (Bool (Bool P1[(Set (Var "x"))])) "implies" (Bool (Set F3 "(" (Set (Var "x")) ")" ) ($#r2_hidden :::"in"::: ) (Set F2 "(" ")" )) ")" & "(" (Bool (Bool P1[(Set (Var "x"))])) "implies" (Bool (Set F4 "(" (Set (Var "x")) ")" ) ($#r2_hidden :::"in"::: ) (Set F2 "(" ")" )) ")" ")" )) proof end; theorem :: FUNCT_2:67 (Bool "for" (Set (Var "X")) "," (Set (Var "Y")) "being" ($#m1_hidden :::"set"::: ) (Bool "for" (Set (Var "f")) "being" ($#m1_subset_1 :::"PartFunc":::) "of" (Set (Var "X")) "," (Set (Var "Y")) "st" (Bool (Bool (Set ($#k1_relset_1 :::"dom"::: ) (Set (Var "f"))) ($#r1_hidden :::"="::: ) (Set (Var "X")))) "holds" (Bool (Set (Var "f")) "is" ($#m1_subset_1 :::"Function":::) "of" (Set (Var "X")) "," (Set (Var "Y"))))) ; theorem :: FUNCT_2:68 (Bool "for" (Set (Var "X")) "," (Set (Var "Y")) "being" ($#m1_hidden :::"set"::: ) (Bool "for" (Set (Var "f")) "being" ($#m1_subset_1 :::"PartFunc":::) "of" (Set (Var "X")) "," (Set (Var "Y")) "st" (Bool (Bool (Set (Var "f")) "is" ($#v1_partfun1 :::"total"::: ) )) "holds" (Bool (Set (Var "f")) "is" ($#m1_subset_1 :::"Function":::) "of" (Set (Var "X")) "," (Set (Var "Y"))))) ; theorem :: FUNCT_2:69 (Bool "for" (Set (Var "X")) "," (Set (Var "Y")) "being" ($#m1_hidden :::"set"::: ) (Bool "for" (Set (Var "f")) "being" ($#m1_subset_1 :::"PartFunc":::) "of" (Set (Var "X")) "," (Set (Var "Y")) "st" (Bool "(" (Bool (Bool (Set (Var "Y")) ($#r1_hidden :::"="::: ) (Set ($#k1_xboole_0 :::"{}"::: ) ))) "implies" (Bool (Set (Var "X")) ($#r1_hidden :::"="::: ) (Set ($#k1_xboole_0 :::"{}"::: ) )) ")" & (Bool (Set (Var "f")) "is" ($#m1_subset_1 :::"Function":::) "of" (Set (Var "X")) "," (Set (Var "Y")))) "holds" (Bool (Set (Var "f")) "is" ($#v1_partfun1 :::"total"::: ) ))) ; theorem :: FUNCT_2:70 (Bool "for" (Set (Var "X")) "," (Set (Var "Y")) "being" ($#m1_hidden :::"set"::: ) (Bool "for" (Set (Var "f")) "being" ($#m1_subset_1 :::"Function":::) "of" (Set (Var "X")) "," (Set (Var "Y")) "st" (Bool "(" (Bool (Bool (Set (Var "Y")) ($#r1_hidden :::"="::: ) (Set ($#k1_xboole_0 :::"{}"::: ) ))) "implies" (Bool (Set (Var "X")) ($#r1_hidden :::"="::: ) (Set ($#k1_xboole_0 :::"{}"::: ) )) ")" ) "holds" (Bool (Set ($#k3_partfun1 :::"<:"::: ) (Set (Var "f")) "," (Set (Var "X")) "," (Set (Var "Y")) ($#k3_partfun1 :::":>"::: ) ) "is" ($#v1_partfun1 :::"total"::: ) ))) ; registrationlet "X" be ($#m1_hidden :::"set"::: ) ; let "f" be ($#m1_subset_1 :::"Function":::) "of" (Set (Const "X")) "," (Set (Const "X")); cluster (Set ($#k3_partfun1 :::"<:"::: ) "f" "," "X" "," "X" ($#k3_partfun1 :::":>"::: ) ) -> ($#v1_partfun1 :::"total"::: ) ; end; theorem :: FUNCT_2:71 (Bool "for" (Set (Var "X")) "," (Set (Var "Y")) "being" ($#m1_hidden :::"set"::: ) (Bool "for" (Set (Var "f")) "being" ($#m1_subset_1 :::"PartFunc":::) "of" (Set (Var "X")) "," (Set (Var "Y")) "st" (Bool "(" (Bool (Bool (Set (Var "Y")) ($#r1_hidden :::"="::: ) (Set ($#k1_xboole_0 :::"{}"::: ) ))) "implies" (Bool (Set (Var "X")) ($#r1_hidden :::"="::: ) (Set ($#k1_xboole_0 :::"{}"::: ) )) ")" ) "holds" (Bool "ex" (Set (Var "g")) "being" ($#m1_subset_1 :::"Function":::) "of" (Set (Var "X")) "," (Set (Var "Y")) "st" (Bool "for" (Set (Var "x")) "being" ($#m1_hidden :::"set"::: ) "st" (Bool (Bool (Set (Var "x")) ($#r2_hidden :::"in"::: ) (Set ($#k1_relset_1 :::"dom"::: ) (Set (Var "f"))))) "holds" (Bool (Set (Set (Var "g")) ($#k1_funct_1 :::"."::: ) (Set (Var "x"))) ($#r1_hidden :::"="::: ) (Set (Set (Var "f")) ($#k1_funct_1 :::"."::: ) (Set (Var "x")))))))) ; theorem :: FUNCT_2:72 (Bool "for" (Set (Var "X")) "," (Set (Var "Y")) "being" ($#m1_hidden :::"set"::: ) "holds" (Bool (Set ($#k1_funct_2 :::"Funcs"::: ) "(" (Set (Var "X")) "," (Set (Var "Y")) ")" ) ($#r1_tarski :::"c="::: ) (Set ($#k4_partfun1 :::"PFuncs"::: ) "(" (Set (Var "X")) "," (Set (Var "Y")) ")" ))) ; theorem :: FUNCT_2:73 (Bool "for" (Set (Var "X")) "," (Set (Var "Y")) "being" ($#m1_hidden :::"set"::: ) (Bool "for" (Set (Var "f")) "," (Set (Var "g")) "being" ($#m1_subset_1 :::"Function":::) "of" (Set (Var "X")) "," (Set (Var "Y")) "st" (Bool "(" (Bool (Bool (Set (Var "Y")) ($#r1_hidden :::"="::: ) (Set ($#k1_xboole_0 :::"{}"::: ) ))) "implies" (Bool (Set (Var "X")) ($#r1_hidden :::"="::: ) (Set ($#k1_xboole_0 :::"{}"::: ) )) ")" & (Bool (Set (Var "f")) ($#r1_partfun1 :::"tolerates"::: ) (Set (Var "g")))) "holds" (Bool (Set (Var "f")) ($#r2_relset_1 :::"="::: ) (Set (Var "g"))))) ; theorem :: FUNCT_2:74 (Bool "for" (Set (Var "X")) "being" ($#m1_hidden :::"set"::: ) (Bool "for" (Set (Var "f")) "," (Set (Var "g")) "being" ($#m1_subset_1 :::"Function":::) "of" (Set (Var "X")) "," (Set (Var "X")) "st" (Bool (Bool (Set (Var "f")) ($#r1_partfun1 :::"tolerates"::: ) (Set (Var "g")))) "holds" (Bool (Set (Var "f")) ($#r2_relset_1 :::"="::: ) (Set (Var "g"))))) ; theorem :: FUNCT_2:75 (Bool "for" (Set (Var "X")) "," (Set (Var "Y")) "being" ($#m1_hidden :::"set"::: ) (Bool "for" (Set (Var "f")) "being" ($#m1_subset_1 :::"PartFunc":::) "of" (Set (Var "X")) "," (Set (Var "Y")) (Bool "for" (Set (Var "g")) "being" ($#m1_subset_1 :::"Function":::) "of" (Set (Var "X")) "," (Set (Var "Y")) "st" (Bool "(" (Bool (Bool (Set (Var "Y")) ($#r1_hidden :::"="::: ) (Set ($#k1_xboole_0 :::"{}"::: ) ))) "implies" (Bool (Set (Var "X")) ($#r1_hidden :::"="::: ) (Set ($#k1_xboole_0 :::"{}"::: ) )) ")" ) "holds" (Bool "(" (Bool (Set (Var "f")) ($#r1_partfun1 :::"tolerates"::: ) (Set (Var "g"))) "iff" (Bool "for" (Set (Var "x")) "being" ($#m1_hidden :::"set"::: ) "st" (Bool (Bool (Set (Var "x")) ($#r2_hidden :::"in"::: ) (Set ($#k1_relset_1 :::"dom"::: ) (Set (Var "f"))))) "holds" (Bool (Set (Set (Var "f")) ($#k1_funct_1 :::"."::: ) (Set (Var "x"))) ($#r1_hidden :::"="::: ) (Set (Set (Var "g")) ($#k1_funct_1 :::"."::: ) (Set (Var "x"))))) ")" )))) ; theorem :: FUNCT_2:76 (Bool "for" (Set (Var "X")) "being" ($#m1_hidden :::"set"::: ) (Bool "for" (Set (Var "f")) "being" ($#m1_subset_1 :::"PartFunc":::) "of" (Set (Var "X")) "," (Set (Var "X")) (Bool "for" (Set (Var "g")) "being" ($#m1_subset_1 :::"Function":::) "of" (Set (Var "X")) "," (Set (Var "X")) "holds" (Bool "(" (Bool (Set (Var "f")) ($#r1_partfun1 :::"tolerates"::: ) (Set (Var "g"))) "iff" (Bool "for" (Set (Var "x")) "being" ($#m1_hidden :::"set"::: ) "st" (Bool (Bool (Set (Var "x")) ($#r2_hidden :::"in"::: ) (Set ($#k1_relset_1 :::"dom"::: ) (Set (Var "f"))))) "holds" (Bool (Set (Set (Var "f")) ($#k1_funct_1 :::"."::: ) (Set (Var "x"))) ($#r1_hidden :::"="::: ) (Set (Set (Var "g")) ($#k1_funct_1 :::"."::: ) (Set (Var "x"))))) ")" )))) ; theorem :: FUNCT_2:77 (Bool "for" (Set (Var "X")) "," (Set (Var "Y")) "being" ($#m1_hidden :::"set"::: ) (Bool "for" (Set (Var "f")) "being" ($#m1_subset_1 :::"PartFunc":::) "of" (Set (Var "X")) "," (Set (Var "Y")) "st" (Bool "(" (Bool (Bool (Set (Var "Y")) ($#r1_hidden :::"="::: ) (Set ($#k1_xboole_0 :::"{}"::: ) ))) "implies" (Bool (Set (Var "X")) ($#r1_hidden :::"="::: ) (Set ($#k1_xboole_0 :::"{}"::: ) )) ")" ) "holds" (Bool "ex" (Set (Var "g")) "being" ($#m1_subset_1 :::"Function":::) "of" (Set (Var "X")) "," (Set (Var "Y")) "st" (Bool (Set (Var "f")) ($#r1_partfun1 :::"tolerates"::: ) (Set (Var "g")))))) ; theorem :: FUNCT_2:78 (Bool "for" (Set (Var "X")) "being" ($#m1_hidden :::"set"::: ) (Bool "for" (Set (Var "f")) "," (Set (Var "g")) "being" ($#m1_subset_1 :::"PartFunc":::) "of" (Set (Var "X")) "," (Set (Var "X")) (Bool "for" (Set (Var "h")) "being" ($#m1_subset_1 :::"Function":::) "of" (Set (Var "X")) "," (Set (Var "X")) "st" (Bool (Bool (Set (Var "f")) ($#r1_partfun1 :::"tolerates"::: ) (Set (Var "h"))) & (Bool (Set (Var "g")) ($#r1_partfun1 :::"tolerates"::: ) (Set (Var "h")))) "holds" (Bool (Set (Var "f")) ($#r1_partfun1 :::"tolerates"::: ) (Set (Var "g")))))) ; theorem :: FUNCT_2:79 (Bool "for" (Set (Var "X")) "," (Set (Var "Y")) "being" ($#m1_hidden :::"set"::: ) (Bool "for" (Set (Var "f")) "," (Set (Var "g")) "being" ($#m1_subset_1 :::"PartFunc":::) "of" (Set (Var "X")) "," (Set (Var "Y")) "st" (Bool "(" (Bool (Bool (Set (Var "Y")) ($#r1_hidden :::"="::: ) (Set ($#k1_xboole_0 :::"{}"::: ) ))) "implies" (Bool (Set (Var "X")) ($#r1_hidden :::"="::: ) (Set ($#k1_xboole_0 :::"{}"::: ) )) ")" & (Bool (Set (Var "f")) ($#r1_partfun1 :::"tolerates"::: ) (Set (Var "g")))) "holds" (Bool "ex" (Set (Var "h")) "being" ($#m1_subset_1 :::"Function":::) "of" (Set (Var "X")) "," (Set (Var "Y")) "st" (Bool "(" (Bool (Set (Var "f")) ($#r1_partfun1 :::"tolerates"::: ) (Set (Var "h"))) & (Bool (Set (Var "g")) ($#r1_partfun1 :::"tolerates"::: ) (Set (Var "h"))) ")" )))) ; theorem :: FUNCT_2:80 (Bool "for" (Set (Var "X")) "," (Set (Var "Y")) "being" ($#m1_hidden :::"set"::: ) (Bool "for" (Set (Var "f")) "being" ($#m1_subset_1 :::"PartFunc":::) "of" (Set (Var "X")) "," (Set (Var "Y")) (Bool "for" (Set (Var "g")) "being" ($#m1_subset_1 :::"Function":::) "of" (Set (Var "X")) "," (Set (Var "Y")) "st" (Bool "(" (Bool (Bool (Set (Var "Y")) ($#r1_hidden :::"="::: ) (Set ($#k1_xboole_0 :::"{}"::: ) ))) "implies" (Bool (Set (Var "X")) ($#r1_hidden :::"="::: ) (Set ($#k1_xboole_0 :::"{}"::: ) )) ")" & (Bool (Set (Var "f")) ($#r1_partfun1 :::"tolerates"::: ) (Set (Var "g")))) "holds" (Bool (Set (Var "g")) ($#r2_hidden :::"in"::: ) (Set ($#k5_partfun1 :::"TotFuncs"::: ) (Set (Var "f"))))))) ; theorem :: FUNCT_2:81 (Bool "for" (Set (Var "X")) "being" ($#m1_hidden :::"set"::: ) (Bool "for" (Set (Var "f")) "being" ($#m1_subset_1 :::"PartFunc":::) "of" (Set (Var "X")) "," (Set (Var "X")) (Bool "for" (Set (Var "g")) "being" ($#m1_subset_1 :::"Function":::) "of" (Set (Var "X")) "," (Set (Var "X")) "st" (Bool (Bool (Set (Var "f")) ($#r1_partfun1 :::"tolerates"::: ) (Set (Var "g")))) "holds" (Bool (Set (Var "g")) ($#r2_hidden :::"in"::: ) (Set ($#k5_partfun1 :::"TotFuncs"::: ) (Set (Var "f"))))))) ; theorem :: FUNCT_2:82 (Bool "for" (Set (Var "X")) "," (Set (Var "Y")) "being" ($#m1_hidden :::"set"::: ) (Bool "for" (Set (Var "f")) "being" ($#m1_subset_1 :::"PartFunc":::) "of" (Set (Var "X")) "," (Set (Var "Y")) (Bool "for" (Set (Var "g")) "being" ($#m1_hidden :::"set"::: ) "st" (Bool (Bool (Set (Var "g")) ($#r2_hidden :::"in"::: ) (Set ($#k5_partfun1 :::"TotFuncs"::: ) (Set (Var "f"))))) "holds" (Bool (Set (Var "g")) "is" ($#m1_subset_1 :::"Function":::) "of" (Set (Var "X")) "," (Set (Var "Y")))))) ; theorem :: FUNCT_2:83 (Bool "for" (Set (Var "X")) "," (Set (Var "Y")) "being" ($#m1_hidden :::"set"::: ) (Bool "for" (Set (Var "f")) "being" ($#m1_subset_1 :::"PartFunc":::) "of" (Set (Var "X")) "," (Set (Var "Y")) "holds" (Bool (Set ($#k5_partfun1 :::"TotFuncs"::: ) (Set (Var "f"))) ($#r1_tarski :::"c="::: ) (Set ($#k1_funct_2 :::"Funcs"::: ) "(" (Set (Var "X")) "," (Set (Var "Y")) ")" )))) ; theorem :: FUNCT_2:84 (Bool "for" (Set (Var "X")) "," (Set (Var "Y")) "being" ($#m1_hidden :::"set"::: ) "holds" (Bool (Set ($#k5_partfun1 :::"TotFuncs"::: ) (Set ($#k3_partfun1 :::"<:"::: ) (Set ($#k1_xboole_0 :::"{}"::: ) ) "," (Set (Var "X")) "," (Set (Var "Y")) ($#k3_partfun1 :::":>"::: ) )) ($#r1_hidden :::"="::: ) (Set ($#k1_funct_2 :::"Funcs"::: ) "(" (Set (Var "X")) "," (Set (Var "Y")) ")" ))) ; theorem :: FUNCT_2:85 (Bool "for" (Set (Var "X")) "," (Set (Var "Y")) "being" ($#m1_hidden :::"set"::: ) (Bool "for" (Set (Var "f")) "being" ($#m1_subset_1 :::"Function":::) "of" (Set (Var "X")) "," (Set (Var "Y")) "st" (Bool "(" (Bool (Bool (Set (Var "Y")) ($#r1_hidden :::"="::: ) (Set ($#k1_xboole_0 :::"{}"::: ) ))) "implies" (Bool (Set (Var "X")) ($#r1_hidden :::"="::: ) (Set ($#k1_xboole_0 :::"{}"::: ) )) ")" ) "holds" (Bool (Set ($#k5_partfun1 :::"TotFuncs"::: ) (Set ($#k3_partfun1 :::"<:"::: ) (Set (Var "f")) "," (Set (Var "X")) "," (Set (Var "Y")) ($#k3_partfun1 :::":>"::: ) )) ($#r1_hidden :::"="::: ) (Set ($#k1_tarski :::"{"::: ) (Set (Var "f")) ($#k1_tarski :::"}"::: ) )))) ; theorem :: FUNCT_2:86 (Bool "for" (Set (Var "X")) "being" ($#m1_hidden :::"set"::: ) (Bool "for" (Set (Var "f")) "being" ($#m1_subset_1 :::"Function":::) "of" (Set (Var "X")) "," (Set (Var "X")) "holds" (Bool (Set ($#k5_partfun1 :::"TotFuncs"::: ) (Set ($#k3_partfun1 :::"<:"::: ) (Set (Var "f")) "," (Set (Var "X")) "," (Set (Var "X")) ($#k3_partfun1 :::":>"::: ) )) ($#r1_hidden :::"="::: ) (Set ($#k1_tarski :::"{"::: ) (Set (Var "f")) ($#k1_tarski :::"}"::: ) )))) ; theorem :: FUNCT_2:87 (Bool "for" (Set (Var "X")) "," (Set (Var "y")) "being" ($#m1_hidden :::"set"::: ) (Bool "for" (Set (Var "f")) "being" ($#m1_subset_1 :::"PartFunc":::) "of" (Set (Var "X")) "," (Set ($#k1_tarski :::"{"::: ) (Set (Var "y")) ($#k1_tarski :::"}"::: ) ) (Bool "for" (Set (Var "g")) "being" ($#m1_subset_1 :::"Function":::) "of" (Set (Var "X")) "," (Set ($#k1_tarski :::"{"::: ) (Set (Var "y")) ($#k1_tarski :::"}"::: ) ) "holds" (Bool (Set ($#k5_partfun1 :::"TotFuncs"::: ) (Set (Var "f"))) ($#r1_hidden :::"="::: ) (Set ($#k1_tarski :::"{"::: ) (Set (Var "g")) ($#k1_tarski :::"}"::: ) ))))) ; theorem :: FUNCT_2:88 (Bool "for" (Set (Var "X")) "," (Set (Var "Y")) "being" ($#m1_hidden :::"set"::: ) (Bool "for" (Set (Var "f")) "," (Set (Var "g")) "being" ($#m1_subset_1 :::"PartFunc":::) "of" (Set (Var "X")) "," (Set (Var "Y")) "st" (Bool (Bool (Set (Var "g")) ($#r1_relset_1 :::"c="::: ) (Set (Var "f")))) "holds" (Bool (Set ($#k5_partfun1 :::"TotFuncs"::: ) (Set (Var "f"))) ($#r1_tarski :::"c="::: ) (Set ($#k5_partfun1 :::"TotFuncs"::: ) (Set (Var "g")))))) ; theorem :: FUNCT_2:89 (Bool "for" (Set (Var "X")) "," (Set (Var "Y")) "being" ($#m1_hidden :::"set"::: ) (Bool "for" (Set (Var "f")) "," (Set (Var "g")) "being" ($#m1_subset_1 :::"PartFunc":::) "of" (Set (Var "X")) "," (Set (Var "Y")) "st" (Bool (Bool (Set ($#k1_relset_1 :::"dom"::: ) (Set (Var "g"))) ($#r1_tarski :::"c="::: ) (Set ($#k1_relset_1 :::"dom"::: ) (Set (Var "f")))) & (Bool (Set ($#k5_partfun1 :::"TotFuncs"::: ) (Set (Var "f"))) ($#r1_tarski :::"c="::: ) (Set ($#k5_partfun1 :::"TotFuncs"::: ) (Set (Var "g"))))) "holds" (Bool (Set (Var "g")) ($#r1_relset_1 :::"c="::: ) (Set (Var "f"))))) ; theorem :: FUNCT_2:90 (Bool "for" (Set (Var "X")) "," (Set (Var "Y")) "being" ($#m1_hidden :::"set"::: ) (Bool "for" (Set (Var "f")) "," (Set (Var "g")) "being" ($#m1_subset_1 :::"PartFunc":::) "of" (Set (Var "X")) "," (Set (Var "Y")) "st" (Bool (Bool (Set ($#k5_partfun1 :::"TotFuncs"::: ) (Set (Var "f"))) ($#r1_tarski :::"c="::: ) (Set ($#k5_partfun1 :::"TotFuncs"::: ) (Set (Var "g")))) & (Bool "(" "for" (Set (Var "y")) "being" ($#m1_hidden :::"set"::: ) "holds" (Bool (Set (Var "Y")) ($#r1_hidden :::"<>"::: ) (Set ($#k1_tarski :::"{"::: ) (Set (Var "y")) ($#k1_tarski :::"}"::: ) )) ")" )) "holds" (Bool (Set (Var "g")) ($#r1_relset_1 :::"c="::: ) (Set (Var "f"))))) ; theorem :: FUNCT_2:91 (Bool "for" (Set (Var "X")) "," (Set (Var "Y")) "being" ($#m1_hidden :::"set"::: ) (Bool "for" (Set (Var "f")) "," (Set (Var "g")) "being" ($#m1_subset_1 :::"PartFunc":::) "of" (Set (Var "X")) "," (Set (Var "Y")) "st" (Bool (Bool "(" "for" (Set (Var "y")) "being" ($#m1_hidden :::"set"::: ) "holds" (Bool (Set (Var "Y")) ($#r1_hidden :::"<>"::: ) (Set ($#k1_tarski :::"{"::: ) (Set (Var "y")) ($#k1_tarski :::"}"::: ) )) ")" ) & (Bool (Set ($#k5_partfun1 :::"TotFuncs"::: ) (Set (Var "f"))) ($#r1_hidden :::"="::: ) (Set ($#k5_partfun1 :::"TotFuncs"::: ) (Set (Var "g"))))) "holds" (Bool (Set (Var "f")) ($#r2_relset_1 :::"="::: ) (Set (Var "g"))))) ; registrationlet "A", "B" be ($#~v1_xboole_0 "non" ($#v1_xboole_0 :::"empty"::: ) ) ($#m1_hidden :::"set"::: ) ; cluster ($#v1_funct_1 :::"Function-like"::: ) ($#v1_funct_2 :::"quasi_total"::: ) -> ($#~v1_xboole_0 "non" ($#v1_xboole_0 :::"empty"::: ) ) for ($#m1_subset_1 :::"Element"::: ) "of" (Set ($#k1_zfmisc_1 :::"bool"::: ) (Set ($#k2_zfmisc_1 :::"[:"::: ) "A" "," "B" ($#k2_zfmisc_1 :::":]"::: ) )); end; begin scheme :: FUNCT_2:sch 6 LambdaSep1{ F1() -> ($#~v1_xboole_0 "non" ($#v1_xboole_0 :::"empty"::: ) ) ($#m1_hidden :::"set"::: ) , F2() -> ($#~v1_xboole_0 "non" ($#v1_xboole_0 :::"empty"::: ) ) ($#m1_hidden :::"set"::: ) , F3() -> ($#m1_subset_1 :::"Element"::: ) "of" (Set F1 "(" ")" ), F4() -> ($#m1_subset_1 :::"Element"::: ) "of" (Set F2 "(" ")" ), F5( ($#m1_hidden :::"set"::: ) ) -> ($#m1_subset_1 :::"Element"::: ) "of" (Set F2 "(" ")" ) } : (Bool "ex" (Set (Var "f")) "being" ($#m1_subset_1 :::"Function":::) "of" (Set F1 "(" ")" ) "," (Set F2 "(" ")" ) "st" (Bool "(" (Bool (Set (Set (Var "f")) ($#k3_funct_2 :::"."::: ) (Set F3 "(" ")" )) ($#r1_hidden :::"="::: ) (Set F4 "(" ")" )) & (Bool "(" "for" (Set (Var "x")) "being" ($#m1_subset_1 :::"Element"::: ) "of" (Set F1 "(" ")" ) "st" (Bool (Bool (Set (Var "x")) ($#r1_hidden :::"<>"::: ) (Set F3 "(" ")" ))) "holds" (Bool (Set (Set (Var "f")) ($#k3_funct_2 :::"."::: ) (Set (Var "x"))) ($#r1_hidden :::"="::: ) (Set F5 "(" (Set (Var "x")) ")" )) ")" ) ")" )) proof end; scheme :: FUNCT_2:sch 7 LambdaSep2{ F1() -> ($#~v1_xboole_0 "non" ($#v1_xboole_0 :::"empty"::: ) ) ($#m1_hidden :::"set"::: ) , F2() -> ($#~v1_xboole_0 "non" ($#v1_xboole_0 :::"empty"::: ) ) ($#m1_hidden :::"set"::: ) , F3() -> ($#m1_subset_1 :::"Element"::: ) "of" (Set F1 "(" ")" ), F4() -> ($#m1_subset_1 :::"Element"::: ) "of" (Set F1 "(" ")" ), F5() -> ($#m1_subset_1 :::"Element"::: ) "of" (Set F2 "(" ")" ), F6() -> ($#m1_subset_1 :::"Element"::: ) "of" (Set F2 "(" ")" ), F7( ($#m1_hidden :::"set"::: ) ) -> ($#m1_subset_1 :::"Element"::: ) "of" (Set F2 "(" ")" ) } : (Bool "ex" (Set (Var "f")) "being" ($#m1_subset_1 :::"Function":::) "of" (Set F1 "(" ")" ) "," (Set F2 "(" ")" ) "st" (Bool "(" (Bool (Set (Set (Var "f")) ($#k3_funct_2 :::"."::: ) (Set F3 "(" ")" )) ($#r1_hidden :::"="::: ) (Set F5 "(" ")" )) & (Bool (Set (Set (Var "f")) ($#k3_funct_2 :::"."::: ) (Set F4 "(" ")" )) ($#r1_hidden :::"="::: ) (Set F6 "(" ")" )) & (Bool "(" "for" (Set (Var "x")) "being" ($#m1_subset_1 :::"Element"::: ) "of" (Set F1 "(" ")" ) "st" (Bool (Bool (Set (Var "x")) ($#r1_hidden :::"<>"::: ) (Set F3 "(" ")" )) & (Bool (Set (Var "x")) ($#r1_hidden :::"<>"::: ) (Set F4 "(" ")" ))) "holds" (Bool (Set (Set (Var "f")) ($#k3_funct_2 :::"."::: ) (Set (Var "x"))) ($#r1_hidden :::"="::: ) (Set F7 "(" (Set (Var "x")) ")" )) ")" ) ")" )) provided (Bool (Set F3 "(" ")" ) ($#r1_hidden :::"<>"::: ) (Set F4 "(" ")" )) proof end; theorem :: FUNCT_2:92 (Bool "for" (Set (Var "A")) "," (Set (Var "B")) "being" ($#m1_hidden :::"set"::: ) (Bool "for" (Set (Var "f")) "being" ($#m1_hidden :::"Function":::) "st" (Bool (Bool (Set (Var "f")) ($#r2_hidden :::"in"::: ) (Set ($#k1_funct_2 :::"Funcs"::: ) "(" (Set (Var "A")) "," (Set (Var "B")) ")" ))) "holds" (Bool "(" (Bool (Set ($#k9_xtuple_0 :::"dom"::: ) (Set (Var "f"))) ($#r1_hidden :::"="::: ) (Set (Var "A"))) & (Bool (Set ($#k10_xtuple_0 :::"rng"::: ) (Set (Var "f"))) ($#r1_tarski :::"c="::: ) (Set (Var "B"))) ")" ))) ; scheme :: FUNCT_2:sch 8 FunctRealEx{ F1() -> ($#~v1_xboole_0 "non" ($#v1_xboole_0 :::"empty"::: ) ) ($#m1_hidden :::"set"::: ) , F2() -> ($#m1_hidden :::"set"::: ) , F3( ($#m1_hidden :::"set"::: ) ) -> ($#m1_hidden :::"set"::: ) } : (Bool "ex" (Set (Var "f")) "being" ($#m1_subset_1 :::"Function":::) "of" (Set F1 "(" ")" ) "," (Set F2 "(" ")" ) "st" (Bool "for" (Set (Var "x")) "being" ($#m1_subset_1 :::"Element"::: ) "of" (Set F1 "(" ")" ) "holds" (Bool (Set (Set (Var "f")) ($#k3_funct_2 :::"."::: ) (Set (Var "x"))) ($#r1_hidden :::"="::: ) (Set F3 "(" (Set (Var "x")) ")" )))) provided (Bool "for" (Set (Var "x")) "being" ($#m1_subset_1 :::"Element"::: ) "of" (Set F1 "(" ")" ) "holds" (Bool (Set F3 "(" (Set (Var "x")) ")" ) ($#r2_hidden :::"in"::: ) (Set F2 "(" ")" ))) proof end; scheme :: FUNCT_2:sch 9 KappaMD{ F1() -> ($#~v1_xboole_0 "non" ($#v1_xboole_0 :::"empty"::: ) ) ($#m1_hidden :::"set"::: ) , F2() -> ($#~v1_xboole_0 "non" ($#v1_xboole_0 :::"empty"::: ) ) ($#m1_hidden :::"set"::: ) , F3( ($#m1_hidden :::"set"::: ) ) -> ($#m1_hidden :::"set"::: ) } : (Bool "ex" (Set (Var "f")) "being" ($#m1_subset_1 :::"Function":::) "of" (Set F1 "(" ")" ) "," (Set F2 "(" ")" ) "st" (Bool "for" (Set (Var "x")) "being" ($#m1_subset_1 :::"Element"::: ) "of" (Set F1 "(" ")" ) "holds" (Bool (Set (Set (Var "f")) ($#k3_funct_2 :::"."::: ) (Set (Var "x"))) ($#r1_hidden :::"="::: ) (Set F3 "(" (Set (Var "x")) ")" )))) provided (Bool "for" (Set (Var "x")) "being" ($#m1_subset_1 :::"Element"::: ) "of" (Set F1 "(" ")" ) "holds" (Bool (Set F3 "(" (Set (Var "x")) ")" ) "is" ($#m1_subset_1 :::"Element"::: ) "of" (Set F2 "(" ")" ))) proof end; definitionlet "A", "B", "C" be ($#~v1_xboole_0 "non" ($#v1_xboole_0 :::"empty"::: ) ) ($#m1_hidden :::"set"::: ) ; let "f" be ($#m1_subset_1 :::"Function":::) "of" (Set (Const "A")) "," (Set ($#k2_zfmisc_1 :::"[:"::: ) (Set (Const "B")) "," (Set (Const "C")) ($#k2_zfmisc_1 :::":]"::: ) ); :: original: :::"pr1"::: redefine func :::"pr1"::: "f" -> ($#m1_subset_1 :::"Function":::) "of" "A" "," "B" means :: FUNCT_2:def 5 (Bool "for" (Set (Var "x")) "being" ($#m1_subset_1 :::"Element"::: ) "of" "A" "holds" (Bool (Set it ($#k3_funct_2 :::"."::: ) (Set (Var "x"))) ($#r1_hidden :::"="::: ) (Set (Set "(" "f" ($#k3_funct_2 :::"."::: ) (Set (Var "x")) ")" ) ($#k1_xtuple_0 :::"`1"::: ) ))); :: original: :::"pr2"::: redefine func :::"pr2"::: "f" -> ($#m1_subset_1 :::"Function":::) "of" "A" "," "C" means :: FUNCT_2:def 6 (Bool "for" (Set (Var "x")) "being" ($#m1_subset_1 :::"Element"::: ) "of" "A" "holds" (Bool (Set it ($#k3_funct_2 :::"."::: ) (Set (Var "x"))) ($#r1_hidden :::"="::: ) (Set (Set "(" "f" ($#k3_funct_2 :::"."::: ) (Set (Var "x")) ")" ) ($#k2_xtuple_0 :::"`2"::: ) ))); end; :: deftheorem defines :::"pr1"::: FUNCT_2:def 5 : (Bool "for" (Set (Var "A")) "," (Set (Var "B")) "," (Set (Var "C")) "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 ($#k2_zfmisc_1 :::"[:"::: ) (Set (Var "B")) "," (Set (Var "C")) ($#k2_zfmisc_1 :::":]"::: ) ) (Bool "for" (Set (Var "b5")) "being" ($#m1_subset_1 :::"Function":::) "of" (Set (Var "A")) "," (Set (Var "B")) "holds" (Bool "(" (Bool (Set (Var "b5")) ($#r1_hidden :::"="::: ) (Set ($#k4_funct_2 :::"pr1"::: ) (Set (Var "f")))) "iff" (Bool "for" (Set (Var "x")) "being" ($#m1_subset_1 :::"Element"::: ) "of" (Set (Var "A")) "holds" (Bool (Set (Set (Var "b5")) ($#k3_funct_2 :::"."::: ) (Set (Var "x"))) ($#r1_hidden :::"="::: ) (Set (Set "(" (Set (Var "f")) ($#k3_funct_2 :::"."::: ) (Set (Var "x")) ")" ) ($#k1_xtuple_0 :::"`1"::: ) ))) ")" )))); :: deftheorem defines :::"pr2"::: FUNCT_2:def 6 : (Bool "for" (Set (Var "A")) "," (Set (Var "B")) "," (Set (Var "C")) "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 ($#k2_zfmisc_1 :::"[:"::: ) (Set (Var "B")) "," (Set (Var "C")) ($#k2_zfmisc_1 :::":]"::: ) ) (Bool "for" (Set (Var "b5")) "being" ($#m1_subset_1 :::"Function":::) "of" (Set (Var "A")) "," (Set (Var "C")) "holds" (Bool "(" (Bool (Set (Var "b5")) ($#r1_hidden :::"="::: ) (Set ($#k5_funct_2 :::"pr2"::: ) (Set (Var "f")))) "iff" (Bool "for" (Set (Var "x")) "being" ($#m1_subset_1 :::"Element"::: ) "of" (Set (Var "A")) "holds" (Bool (Set (Set (Var "b5")) ($#k3_funct_2 :::"."::: ) (Set (Var "x"))) ($#r1_hidden :::"="::: ) (Set (Set "(" (Set (Var "f")) ($#k3_funct_2 :::"."::: ) (Set (Var "x")) ")" ) ($#k2_xtuple_0 :::"`2"::: ) ))) ")" )))); definitionlet "A1" be ($#m1_hidden :::"set"::: ) ; let "B1" be ($#~v1_xboole_0 "non" ($#v1_xboole_0 :::"empty"::: ) ) ($#m1_hidden :::"set"::: ) ; let "A2" be ($#m1_hidden :::"set"::: ) ; let "B2" be ($#~v1_xboole_0 "non" ($#v1_xboole_0 :::"empty"::: ) ) ($#m1_hidden :::"set"::: ) ; let "f1" be ($#m1_subset_1 :::"Function":::) "of" (Set (Const "A1")) "," (Set (Const "B1")); let "f2" be ($#m1_subset_1 :::"Function":::) "of" (Set (Const "A2")) "," (Set (Const "B2")); :: original: :::"="::: redefine pred "f1" :::"="::: "f2" means :: FUNCT_2:def 7 (Bool "(" (Bool "A1" ($#r1_hidden :::"="::: ) "A2") & (Bool "(" "for" (Set (Var "a")) "being" ($#m1_subset_1 :::"Element"::: ) "of" "A1" "holds" (Bool (Set "f1" ($#k1_funct_1 :::"."::: ) (Set (Var "a"))) ($#r1_hidden :::"="::: ) (Set "f2" ($#k1_funct_1 :::"."::: ) (Set (Var "a")))) ")" ) ")" ); end; :: deftheorem defines :::"="::: FUNCT_2:def 7 : (Bool "for" (Set (Var "A1")) "being" ($#m1_hidden :::"set"::: ) (Bool "for" (Set (Var "B1")) "being" ($#~v1_xboole_0 "non" ($#v1_xboole_0 :::"empty"::: ) ) ($#m1_hidden :::"set"::: ) (Bool "for" (Set (Var "A2")) "being" ($#m1_hidden :::"set"::: ) (Bool "for" (Set (Var "B2")) "being" ($#~v1_xboole_0 "non" ($#v1_xboole_0 :::"empty"::: ) ) ($#m1_hidden :::"set"::: ) (Bool "for" (Set (Var "f1")) "being" ($#m1_subset_1 :::"Function":::) "of" (Set (Var "A1")) "," (Set (Var "B1")) (Bool "for" (Set (Var "f2")) "being" ($#m1_subset_1 :::"Function":::) "of" (Set (Var "A2")) "," (Set (Var "B2")) "holds" (Bool "(" (Bool (Set (Var "f1")) ($#r1_funct_2 :::"="::: ) (Set (Var "f2"))) "iff" (Bool "(" (Bool (Set (Var "A1")) ($#r1_hidden :::"="::: ) (Set (Var "A2"))) & (Bool "(" "for" (Set (Var "a")) "being" ($#m1_subset_1 :::"Element"::: ) "of" (Set (Var "A1")) "holds" (Bool (Set (Set (Var "f1")) ($#k1_funct_1 :::"."::: ) (Set (Var "a"))) ($#r1_hidden :::"="::: ) (Set (Set (Var "f2")) ($#k1_funct_1 :::"."::: ) (Set (Var "a")))) ")" ) ")" ) ")" ))))))); definitionlet "A", "B" be ($#m1_hidden :::"set"::: ) ; let "f1", "f2" be ($#m1_subset_1 :::"Function":::) "of" (Set (Const "A")) "," (Set (Const "B")); :: original: :::"="::: redefine pred "f1" :::"="::: "f2" means :: FUNCT_2:def 8 (Bool "for" (Set (Var "a")) "being" ($#m1_subset_1 :::"Element"::: ) "of" "A" "holds" (Bool (Set "f1" ($#k1_funct_1 :::"."::: ) (Set (Var "a"))) ($#r1_hidden :::"="::: ) (Set "f2" ($#k1_funct_1 :::"."::: ) (Set (Var "a"))))); end; :: deftheorem defines :::"="::: FUNCT_2:def 8 : (Bool "for" (Set (Var "A")) "," (Set (Var "B")) "being" ($#m1_hidden :::"set"::: ) (Bool "for" (Set (Var "f1")) "," (Set (Var "f2")) "being" ($#m1_subset_1 :::"Function":::) "of" (Set (Var "A")) "," (Set (Var "B")) "holds" (Bool "(" (Bool (Set (Var "f1")) ($#r2_funct_2 :::"="::: ) (Set (Var "f2"))) "iff" (Bool "for" (Set (Var "a")) "being" ($#m1_subset_1 :::"Element"::: ) "of" (Set (Var "A")) "holds" (Bool (Set (Set (Var "f1")) ($#k1_funct_1 :::"."::: ) (Set (Var "a"))) ($#r1_hidden :::"="::: ) (Set (Set (Var "f2")) ($#k1_funct_1 :::"."::: ) (Set (Var "a"))))) ")" ))); theorem :: FUNCT_2:93 (Bool "for" (Set (Var "N")) "being" ($#m1_hidden :::"set"::: ) (Bool "for" (Set (Var "f")) "being" ($#m1_subset_1 :::"Function":::) "of" (Set (Var "N")) "," (Set "(" ($#k9_setfam_1 :::"bool"::: ) (Set (Var "N")) ")" ) (Bool "ex" (Set (Var "R")) "being" ($#m1_subset_1 :::"Relation":::) "of" (Set (Var "N")) "st" (Bool "for" (Set (Var "i")) "being" ($#m1_hidden :::"set"::: ) "st" (Bool (Bool (Set (Var "i")) ($#r2_hidden :::"in"::: ) (Set (Var "N")))) "holds" (Bool (Set ($#k9_relat_1 :::"Im"::: ) "(" (Set (Var "R")) "," (Set (Var "i")) ")" ) ($#r1_hidden :::"="::: ) (Set (Set (Var "f")) ($#k1_funct_1 :::"."::: ) (Set (Var "i")))))))) ; theorem :: FUNCT_2:94 (Bool "for" (Set (Var "X")) "being" ($#m1_hidden :::"set"::: ) (Bool "for" (Set (Var "A")) "being" ($#m1_subset_1 :::"Subset":::) "of" (Set (Var "X")) "holds" (Bool (Set (Set "(" ($#k6_partfun1 :::"id"::: ) (Set (Var "X")) ")" ) ($#k8_relset_1 :::"""::: ) (Set (Var "A"))) ($#r1_hidden :::"="::: ) (Set (Var "A"))))) ; theorem :: FUNCT_2:95 (Bool "for" (Set (Var "A")) "," (Set (Var "B")) "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 (Var "B")) (Bool "for" (Set (Var "A0")) "being" ($#m1_subset_1 :::"Subset":::) "of" (Set (Var "A")) (Bool "for" (Set (Var "B0")) "being" ($#m1_subset_1 :::"Subset":::) "of" (Set (Var "B")) "holds" (Bool "(" (Bool (Set (Set (Var "f")) ($#k7_relset_1 :::".:"::: ) (Set (Var "A0"))) ($#r1_tarski :::"c="::: ) (Set (Var "B0"))) "iff" (Bool (Set (Var "A0")) ($#r1_tarski :::"c="::: ) (Set (Set (Var "f")) ($#k8_relset_1 :::"""::: ) (Set (Var "B0")))) ")" ))))) ; theorem :: FUNCT_2:96 (Bool "for" (Set (Var "A")) "," (Set (Var "B")) "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 (Var "B")) (Bool "for" (Set (Var "A0")) "being" ($#~v1_xboole_0 "non" ($#v1_xboole_0 :::"empty"::: ) ) ($#m1_subset_1 :::"Subset":::) "of" (Set (Var "A")) (Bool "for" (Set (Var "f0")) "being" ($#m1_subset_1 :::"Function":::) "of" (Set (Var "A0")) "," (Set (Var "B")) "st" (Bool (Bool "(" "for" (Set (Var "c")) "being" ($#m1_subset_1 :::"Element"::: ) "of" (Set (Var "A")) "st" (Bool (Bool (Set (Var "c")) ($#r2_hidden :::"in"::: ) (Set (Var "A0")))) "holds" (Bool (Set (Set (Var "f")) ($#k3_funct_2 :::"."::: ) (Set (Var "c"))) ($#r1_hidden :::"="::: ) (Set (Set (Var "f0")) ($#k1_funct_1 :::"."::: ) (Set (Var "c")))) ")" )) "holds" (Bool (Set (Set (Var "f")) ($#k2_partfun1 :::"|"::: ) (Set (Var "A0"))) ($#r1_hidden :::"="::: ) (Set (Var "f0"))))))) ; theorem :: FUNCT_2:97 (Bool "for" (Set (Var "f")) "being" ($#m1_hidden :::"Function":::) (Bool "for" (Set (Var "A0")) "," (Set (Var "C")) "being" ($#m1_hidden :::"set"::: ) "st" (Bool (Bool (Set (Var "C")) ($#r1_tarski :::"c="::: ) (Set (Var "A0")))) "holds" (Bool (Set (Set (Var "f")) ($#k7_relat_1 :::".:"::: ) (Set (Var "C"))) ($#r1_hidden :::"="::: ) (Set (Set "(" (Set (Var "f")) ($#k5_relat_1 :::"|"::: ) (Set (Var "A0")) ")" ) ($#k7_relat_1 :::".:"::: ) (Set (Var "C")))))) ; theorem :: FUNCT_2:98 (Bool "for" (Set (Var "f")) "being" ($#m1_hidden :::"Function":::) (Bool "for" (Set (Var "A0")) "," (Set (Var "D")) "being" ($#m1_hidden :::"set"::: ) "st" (Bool (Bool (Set (Set (Var "f")) ($#k8_relat_1 :::"""::: ) (Set (Var "D"))) ($#r1_tarski :::"c="::: ) (Set (Var "A0")))) "holds" (Bool (Set (Set (Var "f")) ($#k8_relat_1 :::"""::: ) (Set (Var "D"))) ($#r1_hidden :::"="::: ) (Set (Set "(" (Set (Var "f")) ($#k5_relat_1 :::"|"::: ) (Set (Var "A0")) ")" ) ($#k8_relat_1 :::"""::: ) (Set (Var "D")))))) ; scheme :: FUNCT_2:sch 10 MChoice{ F1() -> ($#~v1_xboole_0 "non" ($#v1_xboole_0 :::"empty"::: ) ) ($#m1_hidden :::"set"::: ) , F2() -> ($#~v1_xboole_0 "non" ($#v1_xboole_0 :::"empty"::: ) ) ($#m1_hidden :::"set"::: ) , F3( ($#m1_hidden :::"set"::: ) ) -> ($#m1_hidden :::"set"::: ) } : (Bool "ex" (Set (Var "t")) "being" ($#m1_subset_1 :::"Function":::) "of" (Set F1 "(" ")" ) "," (Set F2 "(" ")" ) "st" (Bool "for" (Set (Var "a")) "being" ($#m1_subset_1 :::"Element"::: ) "of" (Set F1 "(" ")" ) "holds" (Bool (Set (Set (Var "t")) ($#k3_funct_2 :::"."::: ) (Set (Var "a"))) ($#r2_hidden :::"in"::: ) (Set F3 "(" (Set (Var "a")) ")" )))) provided (Bool "for" (Set (Var "a")) "being" ($#m1_subset_1 :::"Element"::: ) "of" (Set F1 "(" ")" ) "holds" (Bool (Set F2 "(" ")" ) ($#r1_xboole_0 :::"meets"::: ) (Set F3 "(" (Set (Var "a")) ")" ))) proof end; theorem :: FUNCT_2:99 (Bool "for" (Set (Var "X")) "," (Set (Var "D")) "being" ($#~v1_xboole_0 "non" ($#v1_xboole_0 :::"empty"::: ) ) ($#m1_hidden :::"set"::: ) (Bool "for" (Set (Var "p")) "being" ($#m1_subset_1 :::"Function":::) "of" (Set (Var "X")) "," (Set (Var "D")) (Bool "for" (Set (Var "i")) "being" ($#m1_subset_1 :::"Element"::: ) "of" (Set (Var "X")) "holds" (Bool (Set (Set (Var "p")) ($#k7_partfun1 :::"/."::: ) (Set (Var "i"))) ($#r1_hidden :::"="::: ) (Set (Set (Var "p")) ($#k3_funct_2 :::"."::: ) (Set (Var "i"))))))) ; registrationlet "X", "D" be ($#~v1_xboole_0 "non" ($#v1_xboole_0 :::"empty"::: ) ) ($#m1_hidden :::"set"::: ) ; let "p" be ($#m1_subset_1 :::"Function":::) "of" (Set (Const "X")) "," (Set (Const "D")); let "i" be ($#m1_subset_1 :::"Element"::: ) "of" (Set (Const "X")); identify ; end; theorem :: FUNCT_2:100 (Bool "for" (Set (Var "S")) "," (Set (Var "X")) "being" ($#m1_hidden :::"set"::: ) (Bool "for" (Set (Var "f")) "being" ($#m1_subset_1 :::"Function":::) "of" (Set (Var "S")) "," (Set (Var "X")) (Bool "for" (Set (Var "A")) "being" ($#m1_subset_1 :::"Subset":::) "of" (Set (Var "X")) "st" (Bool "(" (Bool (Bool (Set (Var "X")) ($#r1_hidden :::"="::: ) (Set ($#k1_xboole_0 :::"{}"::: ) ))) "implies" (Bool (Set (Var "S")) ($#r1_hidden :::"="::: ) (Set ($#k1_xboole_0 :::"{}"::: ) )) ")" ) "holds" (Bool (Set (Set "(" (Set (Var "f")) ($#k8_relset_1 :::"""::: ) (Set (Var "A")) ")" ) ($#k3_subset_1 :::"`"::: ) ) ($#r1_hidden :::"="::: ) (Set (Set (Var "f")) ($#k8_relset_1 :::"""::: ) (Set "(" (Set (Var "A")) ($#k3_subset_1 :::"`"::: ) ")" )))))) ; theorem :: FUNCT_2:101 (Bool "for" (Set (Var "X")) "," (Set (Var "Y")) "," (Set (Var "Z")) "being" ($#m1_hidden :::"set"::: ) (Bool "for" (Set (Var "D")) "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 "D")) "st" (Bool (Bool (Set (Var "Y")) ($#r1_tarski :::"c="::: ) (Set (Var "X"))) & (Bool (Set (Set (Var "f")) ($#k7_relset_1 :::".:"::: ) (Set (Var "Y"))) ($#r1_tarski :::"c="::: ) (Set (Var "Z")))) "holds" (Bool (Set (Set (Var "f")) ($#k2_partfun1 :::"|"::: ) (Set (Var "Y"))) "is" ($#m1_subset_1 :::"Function":::) "of" (Set (Var "Y")) "," (Set (Var "Z")))))) ; definitionlet "T", "S" be ($#~v1_xboole_0 "non" ($#v1_xboole_0 :::"empty"::: ) ) ($#m1_hidden :::"set"::: ) ; let "f" be ($#m1_subset_1 :::"Function":::) "of" (Set (Const "T")) "," (Set (Const "S")); let "G" be ($#m1_subset_1 :::"Subset-Family":::) "of" (Set (Const "S")); func "f" :::"""::: "G" -> ($#m1_subset_1 :::"Subset-Family":::) "of" "T" means :: FUNCT_2:def 9 (Bool "for" (Set (Var "A")) "being" ($#m1_subset_1 :::"Subset":::) "of" "T" "holds" (Bool "(" (Bool (Set (Var "A")) ($#r2_hidden :::"in"::: ) it) "iff" (Bool "ex" (Set (Var "B")) "being" ($#m1_subset_1 :::"Subset":::) "of" "S" "st" (Bool "(" (Bool (Set (Var "B")) ($#r2_hidden :::"in"::: ) "G") & (Bool (Set (Var "A")) ($#r1_hidden :::"="::: ) (Set "f" ($#k8_relset_1 :::"""::: ) (Set (Var "B")))) ")" )) ")" )); end; :: deftheorem defines :::"""::: FUNCT_2:def 9 : (Bool "for" (Set (Var "T")) "," (Set (Var "S")) "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 "T")) "," (Set (Var "S")) (Bool "for" (Set (Var "G")) "being" ($#m1_subset_1 :::"Subset-Family":::) "of" (Set (Var "S")) (Bool "for" (Set (Var "b5")) "being" ($#m1_subset_1 :::"Subset-Family":::) "of" (Set (Var "T")) "holds" (Bool "(" (Bool (Set (Var "b5")) ($#r1_hidden :::"="::: ) (Set (Set (Var "f")) ($#k6_funct_2 :::"""::: ) (Set (Var "G")))) "iff" (Bool "for" (Set (Var "A")) "being" ($#m1_subset_1 :::"Subset":::) "of" (Set (Var "T")) "holds" (Bool "(" (Bool (Set (Var "A")) ($#r2_hidden :::"in"::: ) (Set (Var "b5"))) "iff" (Bool "ex" (Set (Var "B")) "being" ($#m1_subset_1 :::"Subset":::) "of" (Set (Var "S")) "st" (Bool "(" (Bool (Set (Var "B")) ($#r2_hidden :::"in"::: ) (Set (Var "G"))) & (Bool (Set (Var "A")) ($#r1_hidden :::"="::: ) (Set (Set (Var "f")) ($#k8_relset_1 :::"""::: ) (Set (Var "B")))) ")" )) ")" )) ")" ))))); theorem :: FUNCT_2:102 (Bool "for" (Set (Var "T")) "," (Set (Var "S")) "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 "T")) "," (Set (Var "S")) (Bool "for" (Set (Var "A")) "," (Set (Var "B")) "being" ($#m1_subset_1 :::"Subset-Family":::) "of" (Set (Var "S")) "st" (Bool (Bool (Set (Var "A")) ($#r1_tarski :::"c="::: ) (Set (Var "B")))) "holds" (Bool (Set (Set (Var "f")) ($#k6_funct_2 :::"""::: ) (Set (Var "A"))) ($#r1_tarski :::"c="::: ) (Set (Set (Var "f")) ($#k6_funct_2 :::"""::: ) (Set (Var "B"))))))) ; definitionlet "T", "S" be ($#~v1_xboole_0 "non" ($#v1_xboole_0 :::"empty"::: ) ) ($#m1_hidden :::"set"::: ) ; let "f" be ($#m1_subset_1 :::"Function":::) "of" (Set (Const "T")) "," (Set (Const "S")); let "G" be ($#m1_subset_1 :::"Subset-Family":::) "of" (Set (Const "T")); func "f" :::".:"::: "G" -> ($#m1_subset_1 :::"Subset-Family":::) "of" "S" means :: FUNCT_2:def 10 (Bool "for" (Set (Var "A")) "being" ($#m1_subset_1 :::"Subset":::) "of" "S" "holds" (Bool "(" (Bool (Set (Var "A")) ($#r2_hidden :::"in"::: ) it) "iff" (Bool "ex" (Set (Var "B")) "being" ($#m1_subset_1 :::"Subset":::) "of" "T" "st" (Bool "(" (Bool (Set (Var "B")) ($#r2_hidden :::"in"::: ) "G") & (Bool (Set (Var "A")) ($#r1_hidden :::"="::: ) (Set "f" ($#k7_relset_1 :::".:"::: ) (Set (Var "B")))) ")" )) ")" )); end; :: deftheorem defines :::".:"::: FUNCT_2:def 10 : (Bool "for" (Set (Var "T")) "," (Set (Var "S")) "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 "T")) "," (Set (Var "S")) (Bool "for" (Set (Var "G")) "being" ($#m1_subset_1 :::"Subset-Family":::) "of" (Set (Var "T")) (Bool "for" (Set (Var "b5")) "being" ($#m1_subset_1 :::"Subset-Family":::) "of" (Set (Var "S")) "holds" (Bool "(" (Bool (Set (Var "b5")) ($#r1_hidden :::"="::: ) (Set (Set (Var "f")) ($#k7_funct_2 :::".:"::: ) (Set (Var "G")))) "iff" (Bool "for" (Set (Var "A")) "being" ($#m1_subset_1 :::"Subset":::) "of" (Set (Var "S")) "holds" (Bool "(" (Bool (Set (Var "A")) ($#r2_hidden :::"in"::: ) (Set (Var "b5"))) "iff" (Bool "ex" (Set (Var "B")) "being" ($#m1_subset_1 :::"Subset":::) "of" (Set (Var "T")) "st" (Bool "(" (Bool (Set (Var "B")) ($#r2_hidden :::"in"::: ) (Set (Var "G"))) & (Bool (Set (Var "A")) ($#r1_hidden :::"="::: ) (Set (Set (Var "f")) ($#k7_relset_1 :::".:"::: ) (Set (Var "B")))) ")" )) ")" )) ")" ))))); theorem :: FUNCT_2:103 (Bool "for" (Set (Var "T")) "," (Set (Var "S")) "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 "T")) "," (Set (Var "S")) (Bool "for" (Set (Var "A")) "," (Set (Var "B")) "being" ($#m1_subset_1 :::"Subset-Family":::) "of" (Set (Var "T")) "st" (Bool (Bool (Set (Var "A")) ($#r1_tarski :::"c="::: ) (Set (Var "B")))) "holds" (Bool (Set (Set (Var "f")) ($#k7_funct_2 :::".:"::: ) (Set (Var "A"))) ($#r1_tarski :::"c="::: ) (Set (Set (Var "f")) ($#k7_funct_2 :::".:"::: ) (Set (Var "B"))))))) ; theorem :: FUNCT_2:104 (Bool "for" (Set (Var "T")) "," (Set (Var "S")) "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 "T")) "," (Set (Var "S")) (Bool "for" (Set (Var "B")) "being" ($#m1_subset_1 :::"Subset-Family":::) "of" (Set (Var "S")) (Bool "for" (Set (Var "P")) "being" ($#m1_subset_1 :::"Subset":::) "of" (Set (Var "S")) "st" (Bool (Bool (Set (Set (Var "f")) ($#k7_funct_2 :::".:"::: ) (Set "(" (Set (Var "f")) ($#k6_funct_2 :::"""::: ) (Set (Var "B")) ")" )) "is" ($#m1_setfam_1 :::"Cover"::: ) "of" (Set (Var "P")))) "holds" (Bool (Set (Var "B")) "is" ($#m1_setfam_1 :::"Cover"::: ) "of" (Set (Var "P"))))))) ; theorem :: FUNCT_2:105 (Bool "for" (Set (Var "T")) "," (Set (Var "S")) "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 "T")) "," (Set (Var "S")) (Bool "for" (Set (Var "B")) "being" ($#m1_subset_1 :::"Subset-Family":::) "of" (Set (Var "T")) (Bool "for" (Set (Var "P")) "being" ($#m1_subset_1 :::"Subset":::) "of" (Set (Var "T")) "st" (Bool (Bool (Set (Var "B")) "is" ($#m1_setfam_1 :::"Cover"::: ) "of" (Set (Var "P")))) "holds" (Bool (Set (Set (Var "f")) ($#k6_funct_2 :::"""::: ) (Set "(" (Set (Var "f")) ($#k7_funct_2 :::".:"::: ) (Set (Var "B")) ")" )) "is" ($#m1_setfam_1 :::"Cover"::: ) "of" (Set (Var "P"))))))) ; theorem :: FUNCT_2:106 (Bool "for" (Set (Var "T")) "," (Set (Var "S")) "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 "T")) "," (Set (Var "S")) (Bool "for" (Set (Var "Q")) "being" ($#m1_subset_1 :::"Subset-Family":::) "of" (Set (Var "S")) "holds" (Bool (Set ($#k5_setfam_1 :::"union"::: ) (Set "(" (Set (Var "f")) ($#k7_funct_2 :::".:"::: ) (Set "(" (Set (Var "f")) ($#k6_funct_2 :::"""::: ) (Set (Var "Q")) ")" ) ")" )) ($#r1_tarski :::"c="::: ) (Set ($#k5_setfam_1 :::"union"::: ) (Set (Var "Q"))))))) ; theorem :: FUNCT_2:107 (Bool "for" (Set (Var "T")) "," (Set (Var "S")) "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 "T")) "," (Set (Var "S")) (Bool "for" (Set (Var "P")) "being" ($#m1_subset_1 :::"Subset-Family":::) "of" (Set (Var "T")) "holds" (Bool (Set ($#k5_setfam_1 :::"union"::: ) (Set (Var "P"))) ($#r1_tarski :::"c="::: ) (Set ($#k5_setfam_1 :::"union"::: ) (Set "(" (Set (Var "f")) ($#k6_funct_2 :::"""::: ) (Set "(" (Set (Var "f")) ($#k7_funct_2 :::".:"::: ) (Set (Var "P")) ")" ) ")" )))))) ; definitionlet "X", "Z" be ($#m1_hidden :::"set"::: ) ; let "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 "p" be (Set (Const "Z")) ($#v5_relat_1 :::"-valued"::: ) ($#m1_hidden :::"Function":::); assume (Bool (Set ($#k2_relset_1 :::"rng"::: ) (Set (Const "f"))) ($#r1_tarski :::"c="::: ) (Set ($#k9_xtuple_0 :::"dom"::: ) (Set (Const "p")))) ; func "p" :::"/*"::: "f" -> ($#m1_subset_1 :::"Function":::) "of" "X" "," "Z" equals :: FUNCT_2:def 11 (Set "p" ($#k3_relat_1 :::"*"::: ) "f"); end; :: deftheorem defines :::"/*"::: FUNCT_2:def 11 : (Bool "for" (Set (Var "X")) "," (Set (Var "Z")) "being" ($#m1_hidden :::"set"::: ) (Bool "for" (Set (Var "Y")) "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 "p")) "being" (Set (Var "b2")) ($#v5_relat_1 :::"-valued"::: ) ($#m1_hidden :::"Function":::) "st" (Bool (Bool (Set ($#k2_relset_1 :::"rng"::: ) (Set (Var "f"))) ($#r1_tarski :::"c="::: ) (Set ($#k9_xtuple_0 :::"dom"::: ) (Set (Var "p"))))) "holds" (Bool (Set (Set (Var "p")) ($#k8_funct_2 :::"/*"::: ) (Set (Var "f"))) ($#r1_hidden :::"="::: ) (Set (Set (Var "p")) ($#k3_relat_1 :::"*"::: ) (Set (Var "f")))))))); theorem :: FUNCT_2:108 (Bool "for" (Set (Var "Z")) "," (Set (Var "X")) "being" ($#m1_hidden :::"set"::: ) (Bool "for" (Set (Var "Y")) "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 "p")) "being" ($#m1_subset_1 :::"PartFunc":::) "of" (Set (Var "Y")) "," (Set (Var "Z")) (Bool "for" (Set (Var "x")) "being" ($#m1_subset_1 :::"Element"::: ) "of" (Set (Var "X")) "st" (Bool (Bool (Set (Var "X")) ($#r1_hidden :::"<>"::: ) (Set ($#k1_xboole_0 :::"{}"::: ) )) & (Bool (Set ($#k2_relset_1 :::"rng"::: ) (Set (Var "f"))) ($#r1_tarski :::"c="::: ) (Set ($#k1_relset_1 :::"dom"::: ) (Set (Var "p"))))) "holds" (Bool (Set (Set "(" (Set (Var "p")) ($#k8_funct_2 :::"/*"::: ) (Set (Var "f")) ")" ) ($#k1_funct_1 :::"."::: ) (Set (Var "x"))) ($#r1_hidden :::"="::: ) (Set (Set (Var "p")) ($#k1_funct_1 :::"."::: ) (Set "(" (Set (Var "f")) ($#k1_funct_1 :::"."::: ) (Set (Var "x")) ")" )))))))) ; theorem :: FUNCT_2:109 (Bool "for" (Set (Var "Z")) "," (Set (Var "X")) "being" ($#m1_hidden :::"set"::: ) (Bool "for" (Set (Var "Y")) "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 "p")) "being" ($#m1_subset_1 :::"PartFunc":::) "of" (Set (Var "Y")) "," (Set (Var "Z")) (Bool "for" (Set (Var "x")) "being" ($#m1_subset_1 :::"Element"::: ) "of" (Set (Var "X")) "st" (Bool (Bool (Set (Var "X")) ($#r1_hidden :::"<>"::: ) (Set ($#k1_xboole_0 :::"{}"::: ) )) & (Bool (Set ($#k2_relset_1 :::"rng"::: ) (Set (Var "f"))) ($#r1_tarski :::"c="::: ) (Set ($#k1_relset_1 :::"dom"::: ) (Set (Var "p"))))) "holds" (Bool (Set (Set "(" (Set (Var "p")) ($#k8_funct_2 :::"/*"::: ) (Set (Var "f")) ")" ) ($#k1_funct_1 :::"."::: ) (Set (Var "x"))) ($#r1_hidden :::"="::: ) (Set (Set (Var "p")) ($#k7_partfun1 :::"/."::: ) (Set "(" (Set (Var "f")) ($#k1_funct_1 :::"."::: ) (Set (Var "x")) ")" )))))))) ; theorem :: FUNCT_2:110 (Bool "for" (Set (Var "Z")) "," (Set (Var "X")) "being" ($#m1_hidden :::"set"::: ) (Bool "for" (Set (Var "Y")) "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 "p")) "being" ($#m1_subset_1 :::"PartFunc":::) "of" (Set (Var "Y")) "," (Set (Var "Z")) (Bool "for" (Set (Var "g")) "being" ($#m1_subset_1 :::"Function":::) "of" (Set (Var "X")) "," (Set (Var "X")) "st" (Bool (Bool (Set ($#k2_relset_1 :::"rng"::: ) (Set (Var "f"))) ($#r1_tarski :::"c="::: ) (Set ($#k1_relset_1 :::"dom"::: ) (Set (Var "p"))))) "holds" (Bool (Set (Set "(" (Set (Var "p")) ($#k8_funct_2 :::"/*"::: ) (Set (Var "f")) ")" ) ($#k1_partfun1 :::"*"::: ) (Set (Var "g"))) ($#r2_funct_2 :::"="::: ) (Set (Set (Var "p")) ($#k8_funct_2 :::"/*"::: ) (Set "(" (Set (Var "f")) ($#k1_partfun1 :::"*"::: ) (Set (Var "g")) ")" )))))))) ; theorem :: FUNCT_2:111 (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 :::"Function":::) "of" (Set (Var "X")) "," (Set (Var "Y")) "holds" (Bool "(" (Bool (Set (Var "f")) "is" ($#v3_funct_1 :::"constant"::: ) ) "iff" (Bool "ex" (Set (Var "y")) "being" ($#m1_subset_1 :::"Element"::: ) "of" (Set (Var "Y")) "st" (Bool (Set ($#k2_relset_1 :::"rng"::: ) (Set (Var "f"))) ($#r1_hidden :::"="::: ) (Set ($#k1_tarski :::"{"::: ) (Set (Var "y")) ($#k1_tarski :::"}"::: ) ))) ")" ))) ; theorem :: FUNCT_2:112 (Bool "for" (Set (Var "A")) "," (Set (Var "B")) "being" ($#~v1_xboole_0 "non" ($#v1_xboole_0 :::"empty"::: ) ) ($#m1_hidden :::"set"::: ) (Bool "for" (Set (Var "x")) "being" ($#m1_subset_1 :::"Element"::: ) "of" (Set (Var "A")) (Bool "for" (Set (Var "f")) "being" ($#m1_subset_1 :::"Function":::) "of" (Set (Var "A")) "," (Set (Var "B")) "holds" (Bool (Set (Set (Var "f")) ($#k3_funct_2 :::"."::: ) (Set (Var "x"))) ($#r2_hidden :::"in"::: ) (Set ($#k2_relset_1 :::"rng"::: ) (Set (Var "f"))))))) ; theorem :: FUNCT_2:113 (Bool "for" (Set (Var "y")) "," (Set (Var "A")) "," (Set (Var "B")) "being" ($#m1_hidden :::"set"::: ) (Bool "for" (Set (Var "f")) "being" ($#m1_subset_1 :::"Function":::) "of" (Set (Var "A")) "," (Set (Var "B")) "st" (Bool (Bool (Set (Var "y")) ($#r2_hidden :::"in"::: ) (Set ($#k2_relset_1 :::"rng"::: ) (Set (Var "f"))))) "holds" (Bool "ex" (Set (Var "x")) "being" ($#m1_subset_1 :::"Element"::: ) "of" (Set (Var "A")) "st" (Bool (Set (Var "y")) ($#r1_hidden :::"="::: ) (Set (Set (Var "f")) ($#k1_funct_1 :::"."::: ) (Set (Var "x"))))))) ; theorem :: FUNCT_2:114 (Bool "for" (Set (Var "Z")) "being" ($#m1_hidden :::"set"::: ) (Bool "for" (Set (Var "A")) "," (Set (Var "B")) "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 (Var "B")) "st" (Bool (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"))) ($#r2_hidden :::"in"::: ) (Set (Var "Z"))) ")" )) "holds" (Bool (Set ($#k2_relset_1 :::"rng"::: ) (Set (Var "f"))) ($#r1_tarski :::"c="::: ) (Set (Var "Z")))))) ; theorem :: FUNCT_2:115 (Bool "for" (Set (Var "Y")) "," (Set (Var "X")) "being" ($#~v1_xboole_0 "non" ($#v1_xboole_0 :::"empty"::: ) ) ($#m1_hidden :::"set"::: ) (Bool "for" (Set (Var "Z")) "being" ($#m1_hidden :::"set"::: ) (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 :::"PartFunc":::) "of" (Set (Var "Y")) "," (Set (Var "Z")) (Bool "for" (Set (Var "x")) "being" ($#m1_subset_1 :::"Element"::: ) "of" (Set (Var "X")) "st" (Bool (Bool (Set (Var "g")) "is" ($#v1_partfun1 :::"total"::: ) )) "holds" (Bool (Set (Set "(" (Set (Var "g")) ($#k8_funct_2 :::"/*"::: ) (Set (Var "f")) ")" ) ($#k3_funct_2 :::"."::: ) (Set (Var "x"))) ($#r1_hidden :::"="::: ) (Set (Set (Var "g")) ($#k1_funct_1 :::"."::: ) (Set "(" (Set (Var "f")) ($#k3_funct_2 :::"."::: ) (Set (Var "x")) ")" )))))))) ; theorem :: FUNCT_2:116 (Bool "for" (Set (Var "Y")) "," (Set (Var "X")) "being" ($#~v1_xboole_0 "non" ($#v1_xboole_0 :::"empty"::: ) ) ($#m1_hidden :::"set"::: ) (Bool "for" (Set (Var "Z")) "being" ($#m1_hidden :::"set"::: ) (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 :::"PartFunc":::) "of" (Set (Var "Y")) "," (Set (Var "Z")) (Bool "for" (Set (Var "x")) "being" ($#m1_subset_1 :::"Element"::: ) "of" (Set (Var "X")) "st" (Bool (Bool (Set (Var "g")) "is" ($#v1_partfun1 :::"total"::: ) )) "holds" (Bool (Set (Set "(" (Set (Var "g")) ($#k8_funct_2 :::"/*"::: ) (Set (Var "f")) ")" ) ($#k3_funct_2 :::"."::: ) (Set (Var "x"))) ($#r1_hidden :::"="::: ) (Set (Set (Var "g")) ($#k7_partfun1 :::"/."::: ) (Set "(" (Set (Var "f")) ($#k3_funct_2 :::"."::: ) (Set (Var "x")) ")" )))))))) ; theorem :: FUNCT_2:117 (Bool "for" (Set (Var "X")) "," (Set (Var "Y")) "being" ($#~v1_xboole_0 "non" ($#v1_xboole_0 :::"empty"::: ) ) ($#m1_hidden :::"set"::: ) (Bool "for" (Set (Var "Z")) "," (Set (Var "S")) "being" ($#m1_hidden :::"set"::: ) (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 :::"PartFunc":::) "of" (Set (Var "Y")) "," (Set (Var "Z")) "st" (Bool (Bool (Set ($#k2_relset_1 :::"rng"::: ) (Set (Var "f"))) ($#r1_tarski :::"c="::: ) (Set ($#k1_relset_1 :::"dom"::: ) (Set "(" (Set (Var "g")) ($#k2_partfun1 :::"|"::: ) (Set (Var "S")) ")" )))) "holds" (Bool (Set (Set "(" (Set (Var "g")) ($#k2_partfun1 :::"|"::: ) (Set (Var "S")) ")" ) ($#k8_funct_2 :::"/*"::: ) (Set (Var "f"))) ($#r2_funct_2 :::"="::: ) (Set (Set (Var "g")) ($#k8_funct_2 :::"/*"::: ) (Set (Var "f")))))))) ; theorem :: FUNCT_2:118 (Bool "for" (Set (Var "X")) "," (Set (Var "Y")) "being" ($#~v1_xboole_0 "non" ($#v1_xboole_0 :::"empty"::: ) ) ($#m1_hidden :::"set"::: ) (Bool "for" (Set (Var "Z")) "," (Set (Var "S")) "," (Set (Var "T")) "being" ($#m1_hidden :::"set"::: ) (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 :::"PartFunc":::) "of" (Set (Var "Y")) "," (Set (Var "Z")) "st" (Bool (Bool (Set ($#k2_relset_1 :::"rng"::: ) (Set (Var "f"))) ($#r1_tarski :::"c="::: ) (Set ($#k1_relset_1 :::"dom"::: ) (Set "(" (Set (Var "g")) ($#k2_partfun1 :::"|"::: ) (Set (Var "S")) ")" ))) & (Bool (Set (Var "S")) ($#r1_tarski :::"c="::: ) (Set (Var "T")))) "holds" (Bool (Set (Set "(" (Set (Var "g")) ($#k2_partfun1 :::"|"::: ) (Set (Var "S")) ")" ) ($#k8_funct_2 :::"/*"::: ) (Set (Var "f"))) ($#r2_funct_2 :::"="::: ) (Set (Set "(" (Set (Var "g")) ($#k2_partfun1 :::"|"::: ) (Set (Var "T")) ")" ) ($#k8_funct_2 :::"/*"::: ) (Set (Var "f")))))))) ; theorem :: FUNCT_2:119 (Bool "for" (Set (Var "D")) "," (Set (Var "A")) "," (Set (Var "B")) "being" ($#~v1_xboole_0 "non" ($#v1_xboole_0 :::"empty"::: ) ) ($#m1_hidden :::"set"::: ) (Bool "for" (Set (Var "H")) "being" ($#m1_subset_1 :::"Function":::) "of" (Set (Var "D")) "," (Set ($#k2_zfmisc_1 :::"[:"::: ) (Set (Var "A")) "," (Set (Var "B")) ($#k2_zfmisc_1 :::":]"::: ) ) (Bool "for" (Set (Var "d")) "being" ($#m1_subset_1 :::"Element"::: ) "of" (Set (Var "D")) "holds" (Bool (Set (Set (Var "H")) ($#k3_funct_2 :::"."::: ) (Set (Var "d"))) ($#r1_hidden :::"="::: ) (Set ($#k4_tarski :::"["::: ) (Set "(" (Set "(" ($#k4_funct_2 :::"pr1"::: ) (Set (Var "H")) ")" ) ($#k3_funct_2 :::"."::: ) (Set (Var "d")) ")" ) "," (Set "(" (Set "(" ($#k5_funct_2 :::"pr2"::: ) (Set (Var "H")) ")" ) ($#k3_funct_2 :::"."::: ) (Set (Var "d")) ")" ) ($#k4_tarski :::"]"::: ) ))))) ; theorem :: FUNCT_2:120 (Bool "for" (Set (Var "A1")) "," (Set (Var "A2")) "," (Set (Var "B1")) "," (Set (Var "B2")) "being" ($#m1_hidden :::"set"::: ) (Bool "for" (Set (Var "f")) "being" ($#m1_subset_1 :::"Function":::) "of" (Set (Var "A1")) "," (Set (Var "A2")) (Bool "for" (Set (Var "g")) "being" ($#m1_subset_1 :::"Function":::) "of" (Set (Var "B1")) "," (Set (Var "B2")) "st" (Bool (Bool (Set (Var "f")) ($#r1_partfun1 :::"tolerates"::: ) (Set (Var "g")))) "holds" (Bool (Set (Set (Var "f")) ($#k9_subset_1 :::"/\"::: ) (Set (Var "g"))) "is" ($#m1_subset_1 :::"Function":::) "of" (Set "(" (Set (Var "A1")) ($#k3_xboole_0 :::"/\"::: ) (Set (Var "B1")) ")" ) "," (Set "(" (Set (Var "A2")) ($#k3_xboole_0 :::"/\"::: ) (Set (Var "B2")) ")" ))))) ; registrationlet "A", "B" be ($#m1_hidden :::"set"::: ) ; cluster (Set ($#k1_funct_2 :::"Funcs"::: ) "(" "A" "," "B" ")" ) -> ($#v4_funct_1 :::"functional"::: ) ; end; definitionlet "A", "B" be ($#m1_hidden :::"set"::: ) ; mode :::"FUNCTION_DOMAIN"::: "of" "A" "," "B" -> ($#~v1_xboole_0 "non" ($#v1_xboole_0 :::"empty"::: ) ) ($#m1_hidden :::"set"::: ) means :: FUNCT_2:def 12 (Bool "for" (Set (Var "x")) "being" ($#m1_subset_1 :::"Element"::: ) "of" it "holds" (Bool (Set (Var "x")) "is" ($#m1_subset_1 :::"Function":::) "of" "A" "," "B")); end; :: deftheorem defines :::"FUNCTION_DOMAIN"::: FUNCT_2:def 12 : (Bool "for" (Set (Var "A")) "," (Set (Var "B")) "being" ($#m1_hidden :::"set"::: ) (Bool "for" (Set (Var "b3")) "being" ($#~v1_xboole_0 "non" ($#v1_xboole_0 :::"empty"::: ) ) ($#m1_hidden :::"set"::: ) "holds" (Bool "(" (Bool (Set (Var "b3")) "is" ($#m1_funct_2 :::"FUNCTION_DOMAIN"::: ) "of" (Set (Var "A")) "," (Set (Var "B"))) "iff" (Bool "for" (Set (Var "x")) "being" ($#m1_subset_1 :::"Element"::: ) "of" (Set (Var "b3")) "holds" (Bool (Set (Var "x")) "is" ($#m1_subset_1 :::"Function":::) "of" (Set (Var "A")) "," (Set (Var "B")))) ")" ))); registrationlet "A", "B" be ($#m1_hidden :::"set"::: ) ; cluster -> ($#v4_funct_1 :::"functional"::: ) for ($#m1_funct_2 :::"FUNCTION_DOMAIN"::: ) "of" "A" "," "B"; end; theorem :: FUNCT_2:121 (Bool "for" (Set (Var "P")) "," (Set (Var "Q")) "being" ($#m1_hidden :::"set"::: ) (Bool "for" (Set (Var "f")) "being" ($#m1_subset_1 :::"Function":::) "of" (Set (Var "P")) "," (Set (Var "Q")) "holds" (Bool (Set ($#k1_tarski :::"{"::: ) (Set (Var "f")) ($#k1_tarski :::"}"::: ) ) "is" ($#m1_funct_2 :::"FUNCTION_DOMAIN"::: ) "of" (Set (Var "P")) "," (Set (Var "Q"))))) ; theorem :: FUNCT_2:122 (Bool "for" (Set (Var "P")) "being" ($#m1_hidden :::"set"::: ) (Bool "for" (Set (Var "B")) "being" ($#~v1_xboole_0 "non" ($#v1_xboole_0 :::"empty"::: ) ) ($#m1_hidden :::"set"::: ) "holds" (Bool (Set ($#k1_funct_2 :::"Funcs"::: ) "(" (Set (Var "P")) "," (Set (Var "B")) ")" ) "is" ($#m1_funct_2 :::"FUNCTION_DOMAIN"::: ) "of" (Set (Var "P")) "," (Set (Var "B"))))) ; definitionlet "A" be ($#m1_hidden :::"set"::: ) ; let "B" be ($#~v1_xboole_0 "non" ($#v1_xboole_0 :::"empty"::: ) ) ($#m1_hidden :::"set"::: ) ; :: original: :::"Funcs"::: redefine func :::"Funcs"::: "(" "A" "," "B" ")" -> ($#m1_funct_2 :::"FUNCTION_DOMAIN"::: ) "of" "A" "," "B"; let "F" be ($#m1_funct_2 :::"FUNCTION_DOMAIN"::: ) "of" (Set (Const "A")) "," (Set (Const "B")); :: original: :::"Element"::: redefine mode :::"Element"::: "of" "F" -> ($#m1_subset_1 :::"Function":::) "of" "A" "," "B"; end; registrationlet "I" be ($#m1_hidden :::"set"::: ) ; cluster (Set ($#k4_relat_1 :::"id"::: ) "I") -> "I" ($#v4_relat_1 :::"-defined"::: ) ($#v1_partfun1 :::"total"::: ) for"I" ($#v4_relat_1 :::"-defined"::: ) ($#m1_hidden :::"Function":::); end; definitionlet "X", "A" 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 "A")); let "x" be ($#m1_hidden :::"set"::: ) ; assume (Bool (Set (Const "x")) ($#r2_hidden :::"in"::: ) (Set (Const "X"))) ; :: original: :::"/."::: redefine func "F" :::"/."::: "x" -> ($#m1_subset_1 :::"Element"::: ) "of" "A" equals :: FUNCT_2:def 13 (Set "F" ($#k1_funct_1 :::"."::: ) "x"); end; :: deftheorem defines :::"/."::: FUNCT_2:def 13 : (Bool "for" (Set (Var "X")) "," (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 "X")) "," (Set (Var "A")) (Bool "for" (Set (Var "x")) "being" ($#m1_hidden :::"set"::: ) "st" (Bool (Bool (Set (Var "x")) ($#r2_hidden :::"in"::: ) (Set (Var "X")))) "holds" (Bool (Set (Set (Var "F")) ($#k10_funct_2 :::"/."::: ) (Set (Var "x"))) ($#r1_hidden :::"="::: ) (Set (Set (Var "F")) ($#k1_funct_1 :::"."::: ) (Set (Var "x"))))))); theorem :: FUNCT_2:123 (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 :::"Function":::) "of" (Set (Var "X")) "," (Set (Var "X")) (Bool "for" (Set (Var "g")) "being" (Set (Var "b1")) ($#v5_relat_1 :::"-valued"::: ) ($#m1_hidden :::"Function":::) "holds" (Bool (Set ($#k9_xtuple_0 :::"dom"::: ) (Set "(" (Set (Var "f")) ($#k3_relat_1 :::"*"::: ) (Set (Var "g")) ")" )) ($#r1_hidden :::"="::: ) (Set ($#k9_xtuple_0 :::"dom"::: ) (Set (Var "g"))))))) ; theorem :: FUNCT_2:124 (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 :::"Function":::) "of" (Set (Var "X")) "," (Set (Var "X")) "st" (Bool (Bool "(" "for" (Set (Var "x")) "being" ($#m1_subset_1 :::"Element"::: ) "of" (Set (Var "X")) "holds" (Bool (Set (Set (Var "f")) ($#k3_funct_2 :::"."::: ) (Set (Var "x"))) ($#r1_hidden :::"="::: ) (Set (Var "x"))) ")" )) "holds" (Bool (Set (Var "f")) ($#r2_funct_2 :::"="::: ) (Set ($#k6_partfun1 :::"id"::: ) (Set (Var "X")))))) ; definitionlet "O", "E" be ($#m1_hidden :::"set"::: ) ; mode Action of "O" "," "E" is ($#m1_subset_1 :::"Function":::) "of" "O" "," (Set "(" ($#k1_funct_2 :::"Funcs"::: ) "(" "E" "," "E" ")" ")" ); end; theorem :: FUNCT_2:125 (Bool "for" (Set (Var "x")) "," (Set (Var "A")) "being" ($#m1_hidden :::"set"::: ) (Bool "for" (Set (Var "f")) "," (Set (Var "g")) "being" ($#m1_subset_1 :::"Function":::) "of" (Set ($#k1_tarski :::"{"::: ) (Set (Var "x")) ($#k1_tarski :::"}"::: ) ) "," (Set (Var "A")) "st" (Bool (Bool (Set (Set (Var "f")) ($#k1_funct_1 :::"."::: ) (Set (Var "x"))) ($#r1_hidden :::"="::: ) (Set (Set (Var "g")) ($#k1_funct_1 :::"."::: ) (Set (Var "x"))))) "holds" (Bool (Set (Var "f")) ($#r2_funct_2 :::"="::: ) (Set (Var "g"))))) ;