:: FUNCT_4 semantic presentation begin theorem :: FUNCT_4:1 (Bool "for" (Set (Var "Z")) "being" ($#m1_hidden :::"set"::: ) "st" (Bool (Bool "(" "for" (Set (Var "z")) "being" ($#m1_hidden :::"set"::: ) "st" (Bool (Bool (Set (Var "z")) ($#r2_hidden :::"in"::: ) (Set (Var "Z")))) "holds" (Bool "ex" (Set (Var "x")) "," (Set (Var "y")) "being" ($#m1_hidden :::"set"::: ) "st" (Bool (Set (Var "z")) ($#r1_hidden :::"="::: ) (Set ($#k4_tarski :::"["::: ) (Set (Var "x")) "," (Set (Var "y")) ($#k4_tarski :::"]"::: ) ))) ")" )) "holds" (Bool "ex" (Set (Var "X")) "," (Set (Var "Y")) "being" ($#m1_hidden :::"set"::: ) "st" (Bool (Set (Var "Z")) ($#r1_tarski :::"c="::: ) (Set ($#k2_zfmisc_1 :::"[:"::: ) (Set (Var "X")) "," (Set (Var "Y")) ($#k2_zfmisc_1 :::":]"::: ) )))) ; theorem :: FUNCT_4:2 (Bool "for" (Set (Var "g")) "," (Set (Var "f")) "being" ($#m1_hidden :::"Function":::) "holds" (Bool (Set (Set (Var "g")) ($#k3_relat_1 :::"*"::: ) (Set (Var "f"))) ($#r1_hidden :::"="::: ) (Set (Set "(" (Set (Var "g")) ($#k5_relat_1 :::"|"::: ) (Set "(" ($#k10_xtuple_0 :::"rng"::: ) (Set (Var "f")) ")" ) ")" ) ($#k3_relat_1 :::"*"::: ) (Set (Var "f"))))) ; theorem :: FUNCT_4:3 (Bool "for" (Set (Var "X")) "," (Set (Var "Y")) "being" ($#m1_hidden :::"set"::: ) "holds" (Bool "(" (Bool (Set ($#k6_partfun1 :::"id"::: ) (Set (Var "X"))) ($#r1_relset_1 :::"c="::: ) (Set ($#k6_partfun1 :::"id"::: ) (Set (Var "Y")))) "iff" (Bool (Set (Var "X")) ($#r1_tarski :::"c="::: ) (Set (Var "Y"))) ")" )) ; theorem :: FUNCT_4:4 (Bool "for" (Set (Var "X")) "," (Set (Var "Y")) "," (Set (Var "a")) "being" ($#m1_hidden :::"set"::: ) "st" (Bool (Bool (Set (Var "X")) ($#r1_tarski :::"c="::: ) (Set (Var "Y")))) "holds" (Bool (Set (Set (Var "X")) ($#k7_funcop_1 :::"-->"::: ) (Set (Var "a"))) ($#r1_relset_1 :::"c="::: ) (Set (Set (Var "Y")) ($#k7_funcop_1 :::"-->"::: ) (Set (Var "a"))))) ; theorem :: FUNCT_4:5 (Bool "for" (Set (Var "X")) "," (Set (Var "a")) "," (Set (Var "Y")) "," (Set (Var "b")) "being" ($#m1_hidden :::"set"::: ) "st" (Bool (Bool (Set (Set (Var "X")) ($#k7_funcop_1 :::"-->"::: ) (Set (Var "a"))) ($#r1_relset_1 :::"c="::: ) (Set (Set (Var "Y")) ($#k7_funcop_1 :::"-->"::: ) (Set (Var "b"))))) "holds" (Bool (Set (Var "X")) ($#r1_tarski :::"c="::: ) (Set (Var "Y")))) ; theorem :: FUNCT_4:6 (Bool "for" (Set (Var "X")) "," (Set (Var "a")) "," (Set (Var "Y")) "," (Set (Var "b")) "being" ($#m1_hidden :::"set"::: ) "st" (Bool (Bool (Set (Var "X")) ($#r1_hidden :::"<>"::: ) (Set ($#k1_xboole_0 :::"{}"::: ) )) & (Bool (Set (Set (Var "X")) ($#k7_funcop_1 :::"-->"::: ) (Set (Var "a"))) ($#r1_relset_1 :::"c="::: ) (Set (Set (Var "Y")) ($#k7_funcop_1 :::"-->"::: ) (Set (Var "b"))))) "holds" (Bool (Set (Var "a")) ($#r1_hidden :::"="::: ) (Set (Var "b")))) ; theorem :: FUNCT_4:7 (Bool "for" (Set (Var "x")) "being" ($#m1_hidden :::"set"::: ) (Bool "for" (Set (Var "f")) "being" ($#m1_hidden :::"Function":::) "st" (Bool (Bool (Set (Var "x")) ($#r2_hidden :::"in"::: ) (Set ($#k9_xtuple_0 :::"dom"::: ) (Set (Var "f"))))) "holds" (Bool (Set (Set (Var "x")) ($#k16_funcop_1 :::".-->"::: ) (Set "(" (Set (Var "f")) ($#k1_funct_1 :::"."::: ) (Set (Var "x")) ")" )) ($#r1_tarski :::"c="::: ) (Set (Var "f"))))) ; theorem :: FUNCT_4:8 (Bool "for" (Set (Var "Y")) "," (Set (Var "X")) "being" ($#m1_hidden :::"set"::: ) (Bool "for" (Set (Var "f")) "being" ($#m1_hidden :::"Function":::) "holds" (Bool (Set (Set "(" (Set (Var "Y")) ($#k6_relat_1 :::"|`"::: ) (Set (Var "f")) ")" ) ($#k5_relat_1 :::"|"::: ) (Set (Var "X"))) ($#r1_tarski :::"c="::: ) (Set (Var "f"))))) ; theorem :: FUNCT_4:9 (Bool "for" (Set (Var "Y")) "," (Set (Var "X")) "being" ($#m1_hidden :::"set"::: ) (Bool "for" (Set (Var "f")) "," (Set (Var "g")) "being" ($#m1_hidden :::"Function":::) "st" (Bool (Bool (Set (Var "f")) ($#r1_tarski :::"c="::: ) (Set (Var "g")))) "holds" (Bool (Set (Set "(" (Set (Var "Y")) ($#k6_relat_1 :::"|`"::: ) (Set (Var "f")) ")" ) ($#k5_relat_1 :::"|"::: ) (Set (Var "X"))) ($#r1_tarski :::"c="::: ) (Set (Set "(" (Set (Var "Y")) ($#k6_relat_1 :::"|`"::: ) (Set (Var "g")) ")" ) ($#k5_relat_1 :::"|"::: ) (Set (Var "X")))))) ; definitionlet "f", "g" be ($#m1_hidden :::"Function":::); func "f" :::"+*"::: "g" -> ($#m1_hidden :::"Function":::) means :: FUNCT_4:def 1 (Bool "(" (Bool (Set ($#k9_xtuple_0 :::"dom"::: ) it) ($#r1_hidden :::"="::: ) (Set (Set "(" ($#k9_xtuple_0 :::"dom"::: ) "f" ")" ) ($#k2_xboole_0 :::"\/"::: ) (Set "(" ($#k9_xtuple_0 :::"dom"::: ) "g" ")" ))) & (Bool "(" "for" (Set (Var "x")) "being" ($#m1_hidden :::"set"::: ) "st" (Bool (Bool (Set (Var "x")) ($#r2_hidden :::"in"::: ) (Set (Set "(" ($#k9_xtuple_0 :::"dom"::: ) "f" ")" ) ($#k2_xboole_0 :::"\/"::: ) (Set "(" ($#k9_xtuple_0 :::"dom"::: ) "g" ")" )))) "holds" (Bool "(" "(" (Bool (Bool (Set (Var "x")) ($#r2_hidden :::"in"::: ) (Set ($#k9_xtuple_0 :::"dom"::: ) "g"))) "implies" (Bool (Set it ($#k1_funct_1 :::"."::: ) (Set (Var "x"))) ($#r1_hidden :::"="::: ) (Set "g" ($#k1_funct_1 :::"."::: ) (Set (Var "x")))) ")" & "(" (Bool (Bool (Bool "not" (Set (Var "x")) ($#r2_hidden :::"in"::: ) (Set ($#k9_xtuple_0 :::"dom"::: ) "g")))) "implies" (Bool (Set it ($#k1_funct_1 :::"."::: ) (Set (Var "x"))) ($#r1_hidden :::"="::: ) (Set "f" ($#k1_funct_1 :::"."::: ) (Set (Var "x")))) ")" ")" ) ")" ) ")" ); idempotence (Bool "for" (Set (Var "f")) "being" ($#m1_hidden :::"Function":::) "holds" (Bool "(" (Bool (Set ($#k9_xtuple_0 :::"dom"::: ) (Set (Var "f"))) ($#r1_hidden :::"="::: ) (Set (Set "(" ($#k9_xtuple_0 :::"dom"::: ) (Set (Var "f")) ")" ) ($#k2_xboole_0 :::"\/"::: ) (Set "(" ($#k9_xtuple_0 :::"dom"::: ) (Set (Var "f")) ")" ))) & (Bool "(" "for" (Set (Var "x")) "being" ($#m1_hidden :::"set"::: ) "st" (Bool (Bool (Set (Var "x")) ($#r2_hidden :::"in"::: ) (Set (Set "(" ($#k9_xtuple_0 :::"dom"::: ) (Set (Var "f")) ")" ) ($#k2_xboole_0 :::"\/"::: ) (Set "(" ($#k9_xtuple_0 :::"dom"::: ) (Set (Var "f")) ")" )))) "holds" (Bool "(" "(" (Bool (Bool (Set (Var "x")) ($#r2_hidden :::"in"::: ) (Set ($#k9_xtuple_0 :::"dom"::: ) (Set (Var "f"))))) "implies" (Bool (Set (Set (Var "f")) ($#k1_funct_1 :::"."::: ) (Set (Var "x"))) ($#r1_hidden :::"="::: ) (Set (Set (Var "f")) ($#k1_funct_1 :::"."::: ) (Set (Var "x")))) ")" & "(" (Bool (Bool (Bool "not" (Set (Var "x")) ($#r2_hidden :::"in"::: ) (Set ($#k9_xtuple_0 :::"dom"::: ) (Set (Var "f")))))) "implies" (Bool (Set (Set (Var "f")) ($#k1_funct_1 :::"."::: ) (Set (Var "x"))) ($#r1_hidden :::"="::: ) (Set (Set (Var "f")) ($#k1_funct_1 :::"."::: ) (Set (Var "x")))) ")" ")" ) ")" ) ")" )) ; end; :: deftheorem defines :::"+*"::: FUNCT_4:def 1 : (Bool "for" (Set (Var "f")) "," (Set (Var "g")) "," (Set (Var "b3")) "being" ($#m1_hidden :::"Function":::) "holds" (Bool "(" (Bool (Set (Var "b3")) ($#r1_hidden :::"="::: ) (Set (Set (Var "f")) ($#k1_funct_4 :::"+*"::: ) (Set (Var "g")))) "iff" (Bool "(" (Bool (Set ($#k9_xtuple_0 :::"dom"::: ) (Set (Var "b3"))) ($#r1_hidden :::"="::: ) (Set (Set "(" ($#k9_xtuple_0 :::"dom"::: ) (Set (Var "f")) ")" ) ($#k2_xboole_0 :::"\/"::: ) (Set "(" ($#k9_xtuple_0 :::"dom"::: ) (Set (Var "g")) ")" ))) & (Bool "(" "for" (Set (Var "x")) "being" ($#m1_hidden :::"set"::: ) "st" (Bool (Bool (Set (Var "x")) ($#r2_hidden :::"in"::: ) (Set (Set "(" ($#k9_xtuple_0 :::"dom"::: ) (Set (Var "f")) ")" ) ($#k2_xboole_0 :::"\/"::: ) (Set "(" ($#k9_xtuple_0 :::"dom"::: ) (Set (Var "g")) ")" )))) "holds" (Bool "(" "(" (Bool (Bool (Set (Var "x")) ($#r2_hidden :::"in"::: ) (Set ($#k9_xtuple_0 :::"dom"::: ) (Set (Var "g"))))) "implies" (Bool (Set (Set (Var "b3")) ($#k1_funct_1 :::"."::: ) (Set (Var "x"))) ($#r1_hidden :::"="::: ) (Set (Set (Var "g")) ($#k1_funct_1 :::"."::: ) (Set (Var "x")))) ")" & "(" (Bool (Bool (Bool "not" (Set (Var "x")) ($#r2_hidden :::"in"::: ) (Set ($#k9_xtuple_0 :::"dom"::: ) (Set (Var "g")))))) "implies" (Bool (Set (Set (Var "b3")) ($#k1_funct_1 :::"."::: ) (Set (Var "x"))) ($#r1_hidden :::"="::: ) (Set (Set (Var "f")) ($#k1_funct_1 :::"."::: ) (Set (Var "x")))) ")" ")" ) ")" ) ")" ) ")" )); theorem :: FUNCT_4:10 (Bool "for" (Set (Var "f")) "," (Set (Var "g")) "being" ($#m1_hidden :::"Function":::) "holds" (Bool "(" (Bool (Set ($#k9_xtuple_0 :::"dom"::: ) (Set (Var "f"))) ($#r1_tarski :::"c="::: ) (Set ($#k9_xtuple_0 :::"dom"::: ) (Set "(" (Set (Var "f")) ($#k1_funct_4 :::"+*"::: ) (Set (Var "g")) ")" ))) & (Bool (Set ($#k9_xtuple_0 :::"dom"::: ) (Set (Var "g"))) ($#r1_tarski :::"c="::: ) (Set ($#k9_xtuple_0 :::"dom"::: ) (Set "(" (Set (Var "f")) ($#k1_funct_4 :::"+*"::: ) (Set (Var "g")) ")" ))) ")" )) ; theorem :: FUNCT_4:11 (Bool "for" (Set (Var "x")) "being" ($#m1_hidden :::"set"::: ) (Bool "for" (Set (Var "g")) "," (Set (Var "f")) "being" ($#m1_hidden :::"Function":::) "st" (Bool (Bool (Bool "not" (Set (Var "x")) ($#r2_hidden :::"in"::: ) (Set ($#k9_xtuple_0 :::"dom"::: ) (Set (Var "g")))))) "holds" (Bool (Set (Set "(" (Set (Var "f")) ($#k1_funct_4 :::"+*"::: ) (Set (Var "g")) ")" ) ($#k1_funct_1 :::"."::: ) (Set (Var "x"))) ($#r1_hidden :::"="::: ) (Set (Set (Var "f")) ($#k1_funct_1 :::"."::: ) (Set (Var "x")))))) ; theorem :: FUNCT_4:12 (Bool "for" (Set (Var "x")) "being" ($#m1_hidden :::"set"::: ) (Bool "for" (Set (Var "f")) "," (Set (Var "g")) "being" ($#m1_hidden :::"Function":::) "holds" (Bool "(" (Bool (Set (Var "x")) ($#r2_hidden :::"in"::: ) (Set ($#k9_xtuple_0 :::"dom"::: ) (Set "(" (Set (Var "f")) ($#k1_funct_4 :::"+*"::: ) (Set (Var "g")) ")" ))) "iff" (Bool "(" (Bool (Set (Var "x")) ($#r2_hidden :::"in"::: ) (Set ($#k9_xtuple_0 :::"dom"::: ) (Set (Var "f")))) "or" (Bool (Set (Var "x")) ($#r2_hidden :::"in"::: ) (Set ($#k9_xtuple_0 :::"dom"::: ) (Set (Var "g")))) ")" ) ")" ))) ; theorem :: FUNCT_4:13 (Bool "for" (Set (Var "x")) "being" ($#m1_hidden :::"set"::: ) (Bool "for" (Set (Var "g")) "," (Set (Var "f")) "being" ($#m1_hidden :::"Function":::) "st" (Bool (Bool (Set (Var "x")) ($#r2_hidden :::"in"::: ) (Set ($#k9_xtuple_0 :::"dom"::: ) (Set (Var "g"))))) "holds" (Bool (Set (Set "(" (Set (Var "f")) ($#k1_funct_4 :::"+*"::: ) (Set (Var "g")) ")" ) ($#k1_funct_1 :::"."::: ) (Set (Var "x"))) ($#r1_hidden :::"="::: ) (Set (Set (Var "g")) ($#k1_funct_1 :::"."::: ) (Set (Var "x")))))) ; theorem :: FUNCT_4:14 (Bool "for" (Set (Var "f")) "," (Set (Var "g")) "," (Set (Var "h")) "being" ($#m1_hidden :::"Function":::) "holds" (Bool (Set (Set "(" (Set (Var "f")) ($#k1_funct_4 :::"+*"::: ) (Set (Var "g")) ")" ) ($#k1_funct_4 :::"+*"::: ) (Set (Var "h"))) ($#r1_hidden :::"="::: ) (Set (Set (Var "f")) ($#k1_funct_4 :::"+*"::: ) (Set "(" (Set (Var "g")) ($#k1_funct_4 :::"+*"::: ) (Set (Var "h")) ")" )))) ; theorem :: FUNCT_4:15 (Bool "for" (Set (Var "x")) "being" ($#m1_hidden :::"set"::: ) (Bool "for" (Set (Var "f")) "," (Set (Var "g")) "being" ($#m1_hidden :::"Function":::) "st" (Bool (Bool (Set (Var "f")) ($#r1_partfun1 :::"tolerates"::: ) (Set (Var "g"))) & (Bool (Set (Var "x")) ($#r2_hidden :::"in"::: ) (Set ($#k9_xtuple_0 :::"dom"::: ) (Set (Var "f"))))) "holds" (Bool (Set (Set "(" (Set (Var "f")) ($#k1_funct_4 :::"+*"::: ) (Set (Var "g")) ")" ) ($#k1_funct_1 :::"."::: ) (Set (Var "x"))) ($#r1_hidden :::"="::: ) (Set (Set (Var "f")) ($#k1_funct_1 :::"."::: ) (Set (Var "x")))))) ; theorem :: FUNCT_4:16 (Bool "for" (Set (Var "x")) "being" ($#m1_hidden :::"set"::: ) (Bool "for" (Set (Var "f")) "," (Set (Var "g")) "being" ($#m1_hidden :::"Function":::) "st" (Bool (Bool (Set ($#k9_xtuple_0 :::"dom"::: ) (Set (Var "f"))) ($#r1_xboole_0 :::"misses"::: ) (Set ($#k9_xtuple_0 :::"dom"::: ) (Set (Var "g")))) & (Bool (Set (Var "x")) ($#r2_hidden :::"in"::: ) (Set ($#k9_xtuple_0 :::"dom"::: ) (Set (Var "f"))))) "holds" (Bool (Set (Set "(" (Set (Var "f")) ($#k1_funct_4 :::"+*"::: ) (Set (Var "g")) ")" ) ($#k1_funct_1 :::"."::: ) (Set (Var "x"))) ($#r1_hidden :::"="::: ) (Set (Set (Var "f")) ($#k1_funct_1 :::"."::: ) (Set (Var "x")))))) ; theorem :: FUNCT_4:17 (Bool "for" (Set (Var "f")) "," (Set (Var "g")) "being" ($#m1_hidden :::"Function":::) "holds" (Bool (Set ($#k10_xtuple_0 :::"rng"::: ) (Set "(" (Set (Var "f")) ($#k1_funct_4 :::"+*"::: ) (Set (Var "g")) ")" )) ($#r1_tarski :::"c="::: ) (Set (Set "(" ($#k10_xtuple_0 :::"rng"::: ) (Set (Var "f")) ")" ) ($#k2_xboole_0 :::"\/"::: ) (Set "(" ($#k10_xtuple_0 :::"rng"::: ) (Set (Var "g")) ")" )))) ; theorem :: FUNCT_4:18 (Bool "for" (Set (Var "g")) "," (Set (Var "f")) "being" ($#m1_hidden :::"Function":::) "holds" (Bool (Set ($#k10_xtuple_0 :::"rng"::: ) (Set (Var "g"))) ($#r1_tarski :::"c="::: ) (Set ($#k10_xtuple_0 :::"rng"::: ) (Set "(" (Set (Var "f")) ($#k1_funct_4 :::"+*"::: ) (Set (Var "g")) ")" )))) ; theorem :: FUNCT_4:19 (Bool "for" (Set (Var "f")) "," (Set (Var "g")) "being" ($#m1_hidden :::"Function":::) "st" (Bool (Bool (Set ($#k9_xtuple_0 :::"dom"::: ) (Set (Var "f"))) ($#r1_tarski :::"c="::: ) (Set ($#k9_xtuple_0 :::"dom"::: ) (Set (Var "g"))))) "holds" (Bool (Set (Set (Var "f")) ($#k1_funct_4 :::"+*"::: ) (Set (Var "g"))) ($#r1_hidden :::"="::: ) (Set (Var "g")))) ; registrationlet "f" be ($#m1_hidden :::"Function":::); let "g" be ($#v1_xboole_0 :::"empty"::: ) ($#m1_hidden :::"Function":::); reduce ; reduce ; end; theorem :: FUNCT_4:20 (Bool "for" (Set (Var "f")) "being" ($#m1_hidden :::"Function":::) "holds" (Bool (Set (Set ($#k1_xboole_0 :::"{}"::: ) ) ($#k1_funct_4 :::"+*"::: ) (Set (Var "f"))) ($#r1_hidden :::"="::: ) (Set (Var "f")))) ; theorem :: FUNCT_4:21 (Bool "for" (Set (Var "f")) "being" ($#m1_hidden :::"Function":::) "holds" (Bool (Set (Set (Var "f")) ($#k1_funct_4 :::"+*"::: ) (Set ($#k1_xboole_0 :::"{}"::: ) )) ($#r1_hidden :::"="::: ) (Set (Var "f")))) ; theorem :: FUNCT_4:22 (Bool "for" (Set (Var "X")) "," (Set (Var "Y")) "being" ($#m1_hidden :::"set"::: ) "holds" (Bool (Set (Set "(" ($#k6_partfun1 :::"id"::: ) (Set (Var "X")) ")" ) ($#k1_funct_4 :::"+*"::: ) (Set "(" ($#k6_partfun1 :::"id"::: ) (Set (Var "Y")) ")" )) ($#r1_hidden :::"="::: ) (Set ($#k6_partfun1 :::"id"::: ) (Set "(" (Set (Var "X")) ($#k2_xboole_0 :::"\/"::: ) (Set (Var "Y")) ")" )))) ; theorem :: FUNCT_4:23 (Bool "for" (Set (Var "f")) "," (Set (Var "g")) "being" ($#m1_hidden :::"Function":::) "holds" (Bool (Set (Set "(" (Set (Var "f")) ($#k1_funct_4 :::"+*"::: ) (Set (Var "g")) ")" ) ($#k5_relat_1 :::"|"::: ) (Set "(" ($#k9_xtuple_0 :::"dom"::: ) (Set (Var "g")) ")" )) ($#r1_hidden :::"="::: ) (Set (Var "g")))) ; theorem :: FUNCT_4:24 (Bool "for" (Set (Var "f")) "," (Set (Var "g")) "being" ($#m1_hidden :::"Function":::) "holds" (Bool (Set (Set "(" (Set (Var "f")) ($#k1_funct_4 :::"+*"::: ) (Set (Var "g")) ")" ) ($#k5_relat_1 :::"|"::: ) (Set "(" (Set "(" ($#k9_xtuple_0 :::"dom"::: ) (Set (Var "f")) ")" ) ($#k6_subset_1 :::"\"::: ) (Set "(" ($#k9_xtuple_0 :::"dom"::: ) (Set (Var "g")) ")" ) ")" )) ($#r1_tarski :::"c="::: ) (Set (Var "f")))) ; theorem :: FUNCT_4:25 (Bool "for" (Set (Var "g")) "," (Set (Var "f")) "being" ($#m1_hidden :::"Function":::) "holds" (Bool (Set (Var "g")) ($#r1_tarski :::"c="::: ) (Set (Set (Var "f")) ($#k1_funct_4 :::"+*"::: ) (Set (Var "g"))))) ; theorem :: FUNCT_4:26 (Bool "for" (Set (Var "f")) "," (Set (Var "g")) "," (Set (Var "h")) "being" ($#m1_hidden :::"Function":::) "st" (Bool (Bool (Set (Var "f")) ($#r1_partfun1 :::"tolerates"::: ) (Set (Set (Var "g")) ($#k1_funct_4 :::"+*"::: ) (Set (Var "h"))))) "holds" (Bool (Set (Set (Var "f")) ($#k5_relat_1 :::"|"::: ) (Set "(" (Set "(" ($#k9_xtuple_0 :::"dom"::: ) (Set (Var "f")) ")" ) ($#k6_subset_1 :::"\"::: ) (Set "(" ($#k9_xtuple_0 :::"dom"::: ) (Set (Var "h")) ")" ) ")" )) ($#r1_partfun1 :::"tolerates"::: ) (Set (Var "g")))) ; theorem :: FUNCT_4:27 (Bool "for" (Set (Var "f")) "," (Set (Var "g")) "," (Set (Var "h")) "being" ($#m1_hidden :::"Function":::) "st" (Bool (Bool (Set (Var "f")) ($#r1_partfun1 :::"tolerates"::: ) (Set (Set (Var "g")) ($#k1_funct_4 :::"+*"::: ) (Set (Var "h"))))) "holds" (Bool (Set (Var "f")) ($#r1_partfun1 :::"tolerates"::: ) (Set (Var "h")))) ; theorem :: FUNCT_4:28 (Bool "for" (Set (Var "f")) "," (Set (Var "g")) "being" ($#m1_hidden :::"Function":::) "holds" (Bool "(" (Bool (Set (Var "f")) ($#r1_partfun1 :::"tolerates"::: ) (Set (Var "g"))) "iff" (Bool (Set (Var "f")) ($#r1_tarski :::"c="::: ) (Set (Set (Var "f")) ($#k1_funct_4 :::"+*"::: ) (Set (Var "g")))) ")" )) ; theorem :: FUNCT_4:29 (Bool "for" (Set (Var "f")) "," (Set (Var "g")) "being" ($#m1_hidden :::"Function":::) "holds" (Bool (Set (Set (Var "f")) ($#k1_funct_4 :::"+*"::: ) (Set (Var "g"))) ($#r1_tarski :::"c="::: ) (Set (Set (Var "f")) ($#k2_xboole_0 :::"\/"::: ) (Set (Var "g"))))) ; theorem :: FUNCT_4:30 (Bool "for" (Set (Var "f")) "," (Set (Var "g")) "being" ($#m1_hidden :::"Function":::) "holds" (Bool "(" (Bool (Set (Var "f")) ($#r1_partfun1 :::"tolerates"::: ) (Set (Var "g"))) "iff" (Bool (Set (Set (Var "f")) ($#k2_xboole_0 :::"\/"::: ) (Set (Var "g"))) ($#r1_hidden :::"="::: ) (Set (Set (Var "f")) ($#k1_funct_4 :::"+*"::: ) (Set (Var "g")))) ")" )) ; theorem :: FUNCT_4:31 (Bool "for" (Set (Var "f")) "," (Set (Var "g")) "being" ($#m1_hidden :::"Function":::) "st" (Bool (Bool (Set ($#k9_xtuple_0 :::"dom"::: ) (Set (Var "f"))) ($#r1_xboole_0 :::"misses"::: ) (Set ($#k9_xtuple_0 :::"dom"::: ) (Set (Var "g"))))) "holds" (Bool (Set (Set (Var "f")) ($#k2_xboole_0 :::"\/"::: ) (Set (Var "g"))) ($#r1_hidden :::"="::: ) (Set (Set (Var "f")) ($#k1_funct_4 :::"+*"::: ) (Set (Var "g"))))) ; theorem :: FUNCT_4:32 (Bool "for" (Set (Var "f")) "," (Set (Var "g")) "being" ($#m1_hidden :::"Function":::) "st" (Bool (Bool (Set ($#k9_xtuple_0 :::"dom"::: ) (Set (Var "f"))) ($#r1_xboole_0 :::"misses"::: ) (Set ($#k9_xtuple_0 :::"dom"::: ) (Set (Var "g"))))) "holds" (Bool (Set (Var "f")) ($#r1_tarski :::"c="::: ) (Set (Set (Var "f")) ($#k1_funct_4 :::"+*"::: ) (Set (Var "g"))))) ; theorem :: FUNCT_4:33 (Bool "for" (Set (Var "f")) "," (Set (Var "g")) "being" ($#m1_hidden :::"Function":::) "st" (Bool (Bool (Set ($#k9_xtuple_0 :::"dom"::: ) (Set (Var "f"))) ($#r1_xboole_0 :::"misses"::: ) (Set ($#k9_xtuple_0 :::"dom"::: ) (Set (Var "g"))))) "holds" (Bool (Set (Set "(" (Set (Var "f")) ($#k1_funct_4 :::"+*"::: ) (Set (Var "g")) ")" ) ($#k5_relat_1 :::"|"::: ) (Set "(" ($#k9_xtuple_0 :::"dom"::: ) (Set (Var "f")) ")" )) ($#r1_hidden :::"="::: ) (Set (Var "f")))) ; theorem :: FUNCT_4:34 (Bool "for" (Set (Var "f")) "," (Set (Var "g")) "being" ($#m1_hidden :::"Function":::) "holds" (Bool "(" (Bool (Set (Var "f")) ($#r1_partfun1 :::"tolerates"::: ) (Set (Var "g"))) "iff" (Bool (Set (Set (Var "f")) ($#k1_funct_4 :::"+*"::: ) (Set (Var "g"))) ($#r1_hidden :::"="::: ) (Set (Set (Var "g")) ($#k1_funct_4 :::"+*"::: ) (Set (Var "f")))) ")" )) ; theorem :: FUNCT_4:35 (Bool "for" (Set (Var "f")) "," (Set (Var "g")) "being" ($#m1_hidden :::"Function":::) "st" (Bool (Bool (Set ($#k9_xtuple_0 :::"dom"::: ) (Set (Var "f"))) ($#r1_xboole_0 :::"misses"::: ) (Set ($#k9_xtuple_0 :::"dom"::: ) (Set (Var "g"))))) "holds" (Bool (Set (Set (Var "f")) ($#k1_funct_4 :::"+*"::: ) (Set (Var "g"))) ($#r1_hidden :::"="::: ) (Set (Set (Var "g")) ($#k1_funct_4 :::"+*"::: ) (Set (Var "f"))))) ; theorem :: FUNCT_4:36 (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")) "is" ($#v1_partfun1 :::"total"::: ) )) "holds" (Bool (Set (Set (Var "f")) ($#k1_funct_4 :::"+*"::: ) (Set (Var "g"))) ($#r1_hidden :::"="::: ) (Set (Var "g"))))) ; theorem :: FUNCT_4:37 (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 :::"{}"::: ) )) ")" ) "holds" (Bool (Set (Set (Var "f")) ($#k1_funct_4 :::"+*"::: ) (Set (Var "g"))) ($#r1_hidden :::"="::: ) (Set (Var "g"))))) ; theorem :: FUNCT_4:38 (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")) "holds" (Bool (Set (Set (Var "f")) ($#k1_funct_4 :::"+*"::: ) (Set (Var "g"))) ($#r1_hidden :::"="::: ) (Set (Var "g"))))) ; theorem :: FUNCT_4:39 (Bool "for" (Set (Var "X")) "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")) "," (Set (Var "g")) "being" ($#m1_subset_1 :::"Function":::) "of" (Set (Var "X")) "," (Set (Var "D")) "holds" (Bool (Set (Set (Var "f")) ($#k1_funct_4 :::"+*"::: ) (Set (Var "g"))) ($#r1_hidden :::"="::: ) (Set (Var "g")))))) ; theorem :: FUNCT_4:40 (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")) "holds" (Bool (Set (Set (Var "f")) ($#k1_funct_4 :::"+*"::: ) (Set (Var "g"))) "is" ($#m1_subset_1 :::"PartFunc":::) "of" (Set (Var "X")) "," (Set (Var "Y"))))) ; definitionlet "f" be ($#m1_hidden :::"Function":::); func :::"~"::: "f" -> ($#m1_hidden :::"Function":::) means :: FUNCT_4:def 2 (Bool "(" (Bool "(" "for" (Set (Var "x")) "being" ($#m1_hidden :::"set"::: ) "holds" (Bool "(" (Bool (Set (Var "x")) ($#r2_hidden :::"in"::: ) (Set ($#k9_xtuple_0 :::"dom"::: ) it)) "iff" (Bool "ex" (Set (Var "y")) "," (Set (Var "z")) "being" ($#m1_hidden :::"set"::: ) "st" (Bool "(" (Bool (Set (Var "x")) ($#r1_hidden :::"="::: ) (Set ($#k4_tarski :::"["::: ) (Set (Var "z")) "," (Set (Var "y")) ($#k4_tarski :::"]"::: ) )) & (Bool (Set ($#k4_tarski :::"["::: ) (Set (Var "y")) "," (Set (Var "z")) ($#k4_tarski :::"]"::: ) ) ($#r2_hidden :::"in"::: ) (Set ($#k9_xtuple_0 :::"dom"::: ) "f")) ")" )) ")" ) ")" ) & (Bool "(" "for" (Set (Var "y")) "," (Set (Var "z")) "being" ($#m1_hidden :::"set"::: ) "st" (Bool (Bool (Set ($#k4_tarski :::"["::: ) (Set (Var "y")) "," (Set (Var "z")) ($#k4_tarski :::"]"::: ) ) ($#r2_hidden :::"in"::: ) (Set ($#k9_xtuple_0 :::"dom"::: ) "f"))) "holds" (Bool (Set it ($#k1_binop_1 :::"."::: ) "(" (Set (Var "z")) "," (Set (Var "y")) ")" ) ($#r1_hidden :::"="::: ) (Set "f" ($#k1_binop_1 :::"."::: ) "(" (Set (Var "y")) "," (Set (Var "z")) ")" )) ")" ) ")" ); end; :: deftheorem defines :::"~"::: FUNCT_4:def 2 : (Bool "for" (Set (Var "f")) "," (Set (Var "b2")) "being" ($#m1_hidden :::"Function":::) "holds" (Bool "(" (Bool (Set (Var "b2")) ($#r1_hidden :::"="::: ) (Set ($#k2_funct_4 :::"~"::: ) (Set (Var "f")))) "iff" (Bool "(" (Bool "(" "for" (Set (Var "x")) "being" ($#m1_hidden :::"set"::: ) "holds" (Bool "(" (Bool (Set (Var "x")) ($#r2_hidden :::"in"::: ) (Set ($#k9_xtuple_0 :::"dom"::: ) (Set (Var "b2")))) "iff" (Bool "ex" (Set (Var "y")) "," (Set (Var "z")) "being" ($#m1_hidden :::"set"::: ) "st" (Bool "(" (Bool (Set (Var "x")) ($#r1_hidden :::"="::: ) (Set ($#k4_tarski :::"["::: ) (Set (Var "z")) "," (Set (Var "y")) ($#k4_tarski :::"]"::: ) )) & (Bool (Set ($#k4_tarski :::"["::: ) (Set (Var "y")) "," (Set (Var "z")) ($#k4_tarski :::"]"::: ) ) ($#r2_hidden :::"in"::: ) (Set ($#k9_xtuple_0 :::"dom"::: ) (Set (Var "f")))) ")" )) ")" ) ")" ) & (Bool "(" "for" (Set (Var "y")) "," (Set (Var "z")) "being" ($#m1_hidden :::"set"::: ) "st" (Bool (Bool (Set ($#k4_tarski :::"["::: ) (Set (Var "y")) "," (Set (Var "z")) ($#k4_tarski :::"]"::: ) ) ($#r2_hidden :::"in"::: ) (Set ($#k9_xtuple_0 :::"dom"::: ) (Set (Var "f"))))) "holds" (Bool (Set (Set (Var "b2")) ($#k1_binop_1 :::"."::: ) "(" (Set (Var "z")) "," (Set (Var "y")) ")" ) ($#r1_hidden :::"="::: ) (Set (Set (Var "f")) ($#k1_binop_1 :::"."::: ) "(" (Set (Var "y")) "," (Set (Var "z")) ")" )) ")" ) ")" ) ")" )); theorem :: FUNCT_4:41 (Bool "for" (Set (Var "f")) "being" ($#m1_hidden :::"Function":::) "holds" (Bool (Set ($#k10_xtuple_0 :::"rng"::: ) (Set "(" ($#k2_funct_4 :::"~"::: ) (Set (Var "f")) ")" )) ($#r1_tarski :::"c="::: ) (Set ($#k10_xtuple_0 :::"rng"::: ) (Set (Var "f"))))) ; theorem :: FUNCT_4:42 (Bool "for" (Set (Var "x")) "," (Set (Var "y")) "being" ($#m1_hidden :::"set"::: ) (Bool "for" (Set (Var "f")) "being" ($#m1_hidden :::"Function":::) "holds" (Bool "(" (Bool (Set ($#k4_tarski :::"["::: ) (Set (Var "x")) "," (Set (Var "y")) ($#k4_tarski :::"]"::: ) ) ($#r2_hidden :::"in"::: ) (Set ($#k9_xtuple_0 :::"dom"::: ) (Set (Var "f")))) "iff" (Bool (Set ($#k4_tarski :::"["::: ) (Set (Var "y")) "," (Set (Var "x")) ($#k4_tarski :::"]"::: ) ) ($#r2_hidden :::"in"::: ) (Set ($#k9_xtuple_0 :::"dom"::: ) (Set "(" ($#k2_funct_4 :::"~"::: ) (Set (Var "f")) ")" ))) ")" ))) ; theorem :: FUNCT_4:43 (Bool "for" (Set (Var "y")) "," (Set (Var "x")) "being" ($#m1_hidden :::"set"::: ) (Bool "for" (Set (Var "f")) "being" ($#m1_hidden :::"Function":::) "st" (Bool (Bool (Set ($#k4_tarski :::"["::: ) (Set (Var "y")) "," (Set (Var "x")) ($#k4_tarski :::"]"::: ) ) ($#r2_hidden :::"in"::: ) (Set ($#k9_xtuple_0 :::"dom"::: ) (Set "(" ($#k2_funct_4 :::"~"::: ) (Set (Var "f")) ")" )))) "holds" (Bool (Set (Set "(" ($#k2_funct_4 :::"~"::: ) (Set (Var "f")) ")" ) ($#k1_binop_1 :::"."::: ) "(" (Set (Var "y")) "," (Set (Var "x")) ")" ) ($#r1_hidden :::"="::: ) (Set (Set (Var "f")) ($#k1_binop_1 :::"."::: ) "(" (Set (Var "x")) "," (Set (Var "y")) ")" )))) ; theorem :: FUNCT_4:44 (Bool "for" (Set (Var "f")) "being" ($#m1_hidden :::"Function":::) (Bool "ex" (Set (Var "X")) "," (Set (Var "Y")) "being" ($#m1_hidden :::"set"::: ) "st" (Bool (Set ($#k9_xtuple_0 :::"dom"::: ) (Set "(" ($#k2_funct_4 :::"~"::: ) (Set (Var "f")) ")" )) ($#r1_tarski :::"c="::: ) (Set ($#k2_zfmisc_1 :::"[:"::: ) (Set (Var "X")) "," (Set (Var "Y")) ($#k2_zfmisc_1 :::":]"::: ) )))) ; theorem :: FUNCT_4:45 (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_tarski :::"c="::: ) (Set ($#k2_zfmisc_1 :::"[:"::: ) (Set (Var "X")) "," (Set (Var "Y")) ($#k2_zfmisc_1 :::":]"::: ) ))) "holds" (Bool (Set ($#k9_xtuple_0 :::"dom"::: ) (Set "(" ($#k2_funct_4 :::"~"::: ) (Set (Var "f")) ")" )) ($#r1_tarski :::"c="::: ) (Set ($#k2_zfmisc_1 :::"[:"::: ) (Set (Var "Y")) "," (Set (Var "X")) ($#k2_zfmisc_1 :::":]"::: ) )))) ; theorem :: FUNCT_4:46 (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 ($#k2_zfmisc_1 :::"[:"::: ) (Set (Var "X")) "," (Set (Var "Y")) ($#k2_zfmisc_1 :::":]"::: ) ))) "holds" (Bool (Set ($#k9_xtuple_0 :::"dom"::: ) (Set "(" ($#k2_funct_4 :::"~"::: ) (Set (Var "f")) ")" )) ($#r1_hidden :::"="::: ) (Set ($#k2_zfmisc_1 :::"[:"::: ) (Set (Var "Y")) "," (Set (Var "X")) ($#k2_zfmisc_1 :::":]"::: ) )))) ; theorem :: FUNCT_4:47 (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_tarski :::"c="::: ) (Set ($#k2_zfmisc_1 :::"[:"::: ) (Set (Var "X")) "," (Set (Var "Y")) ($#k2_zfmisc_1 :::":]"::: ) ))) "holds" (Bool (Set ($#k10_xtuple_0 :::"rng"::: ) (Set "(" ($#k2_funct_4 :::"~"::: ) (Set (Var "f")) ")" )) ($#r1_hidden :::"="::: ) (Set ($#k10_xtuple_0 :::"rng"::: ) (Set (Var "f")))))) ; theorem :: FUNCT_4:48 (Bool "for" (Set (Var "X")) "," (Set (Var "Y")) "," (Set (Var "Z")) "being" ($#m1_hidden :::"set"::: ) (Bool "for" (Set (Var "f")) "being" ($#m1_subset_1 :::"PartFunc":::) "of" (Set ($#k2_zfmisc_1 :::"[:"::: ) (Set (Var "X")) "," (Set (Var "Y")) ($#k2_zfmisc_1 :::":]"::: ) ) "," (Set (Var "Z")) "holds" (Bool (Set ($#k2_funct_4 :::"~"::: ) (Set (Var "f"))) "is" ($#m1_subset_1 :::"PartFunc":::) "of" (Set ($#k2_zfmisc_1 :::"[:"::: ) (Set (Var "Y")) "," (Set (Var "X")) ($#k2_zfmisc_1 :::":]"::: ) ) "," (Set (Var "Z"))))) ; theorem :: FUNCT_4:49 (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 ($#k2_zfmisc_1 :::"[:"::: ) (Set (Var "X")) "," (Set (Var "Y")) ($#k2_zfmisc_1 :::":]"::: ) ) "," (Set (Var "Z")) "st" (Bool (Bool (Set (Var "Z")) ($#r1_hidden :::"<>"::: ) (Set ($#k1_xboole_0 :::"{}"::: ) ))) "holds" (Bool (Set ($#k2_funct_4 :::"~"::: ) (Set (Var "f"))) "is" ($#m1_subset_1 :::"Function":::) "of" (Set ($#k2_zfmisc_1 :::"[:"::: ) (Set (Var "Y")) "," (Set (Var "X")) ($#k2_zfmisc_1 :::":]"::: ) ) "," (Set (Var "Z"))))) ; theorem :: FUNCT_4:50 (Bool "for" (Set (Var "X")) "," (Set (Var "Y")) "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 ($#k2_zfmisc_1 :::"[:"::: ) (Set (Var "X")) "," (Set (Var "Y")) ($#k2_zfmisc_1 :::":]"::: ) ) "," (Set (Var "D")) "holds" (Bool (Set ($#k2_funct_4 :::"~"::: ) (Set (Var "f"))) "is" ($#m1_subset_1 :::"Function":::) "of" (Set ($#k2_zfmisc_1 :::"[:"::: ) (Set (Var "Y")) "," (Set (Var "X")) ($#k2_zfmisc_1 :::":]"::: ) ) "," (Set (Var "D")))))) ; theorem :: FUNCT_4:51 (Bool "for" (Set (Var "f")) "being" ($#m1_hidden :::"Function":::) "holds" (Bool (Set ($#k2_funct_4 :::"~"::: ) (Set "(" ($#k2_funct_4 :::"~"::: ) (Set (Var "f")) ")" )) ($#r1_tarski :::"c="::: ) (Set (Var "f")))) ; theorem :: FUNCT_4:52 (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_tarski :::"c="::: ) (Set ($#k2_zfmisc_1 :::"[:"::: ) (Set (Var "X")) "," (Set (Var "Y")) ($#k2_zfmisc_1 :::":]"::: ) ))) "holds" (Bool (Set ($#k2_funct_4 :::"~"::: ) (Set "(" ($#k2_funct_4 :::"~"::: ) (Set (Var "f")) ")" )) ($#r1_hidden :::"="::: ) (Set (Var "f"))))) ; theorem :: FUNCT_4:53 (Bool "for" (Set (Var "X")) "," (Set (Var "Y")) "," (Set (Var "Z")) "being" ($#m1_hidden :::"set"::: ) (Bool "for" (Set (Var "f")) "being" ($#m1_subset_1 :::"PartFunc":::) "of" (Set ($#k2_zfmisc_1 :::"[:"::: ) (Set (Var "X")) "," (Set (Var "Y")) ($#k2_zfmisc_1 :::":]"::: ) ) "," (Set (Var "Z")) "holds" (Bool (Set ($#k2_funct_4 :::"~"::: ) (Set "(" ($#k2_funct_4 :::"~"::: ) (Set (Var "f")) ")" )) ($#r1_hidden :::"="::: ) (Set (Var "f"))))) ; definitionlet "f", "g" be ($#m1_hidden :::"Function":::); func :::"|:":::"f" "," "g":::":|"::: -> ($#m1_hidden :::"Function":::) means :: FUNCT_4:def 3 (Bool "(" (Bool "(" "for" (Set (Var "z")) "being" ($#m1_hidden :::"set"::: ) "holds" (Bool "(" (Bool (Set (Var "z")) ($#r2_hidden :::"in"::: ) (Set ($#k9_xtuple_0 :::"dom"::: ) it)) "iff" (Bool "ex" (Set (Var "x")) "," (Set (Var "y")) "," (Set (Var "x9")) "," (Set (Var "y9")) "being" ($#m1_hidden :::"set"::: ) "st" (Bool "(" (Bool (Set (Var "z")) ($#r1_hidden :::"="::: ) (Set ($#k4_tarski :::"["::: ) (Set ($#k4_tarski :::"["::: ) (Set (Var "x")) "," (Set (Var "x9")) ($#k4_tarski :::"]"::: ) ) "," (Set ($#k4_tarski :::"["::: ) (Set (Var "y")) "," (Set (Var "y9")) ($#k4_tarski :::"]"::: ) ) ($#k4_tarski :::"]"::: ) )) & (Bool (Set ($#k4_tarski :::"["::: ) (Set (Var "x")) "," (Set (Var "y")) ($#k4_tarski :::"]"::: ) ) ($#r2_hidden :::"in"::: ) (Set ($#k9_xtuple_0 :::"dom"::: ) "f")) & (Bool (Set ($#k4_tarski :::"["::: ) (Set (Var "x9")) "," (Set (Var "y9")) ($#k4_tarski :::"]"::: ) ) ($#r2_hidden :::"in"::: ) (Set ($#k9_xtuple_0 :::"dom"::: ) "g")) ")" )) ")" ) ")" ) & (Bool "(" "for" (Set (Var "x")) "," (Set (Var "y")) "," (Set (Var "x9")) "," (Set (Var "y9")) "being" ($#m1_hidden :::"set"::: ) "st" (Bool (Bool (Set ($#k4_tarski :::"["::: ) (Set (Var "x")) "," (Set (Var "y")) ($#k4_tarski :::"]"::: ) ) ($#r2_hidden :::"in"::: ) (Set ($#k9_xtuple_0 :::"dom"::: ) "f")) & (Bool (Set ($#k4_tarski :::"["::: ) (Set (Var "x9")) "," (Set (Var "y9")) ($#k4_tarski :::"]"::: ) ) ($#r2_hidden :::"in"::: ) (Set ($#k9_xtuple_0 :::"dom"::: ) "g"))) "holds" (Bool (Set it ($#k1_binop_1 :::"."::: ) "(" (Set ($#k4_tarski :::"["::: ) (Set (Var "x")) "," (Set (Var "x9")) ($#k4_tarski :::"]"::: ) ) "," (Set ($#k4_tarski :::"["::: ) (Set (Var "y")) "," (Set (Var "y9")) ($#k4_tarski :::"]"::: ) ) ")" ) ($#r1_hidden :::"="::: ) (Set ($#k4_tarski :::"["::: ) (Set "(" "f" ($#k1_binop_1 :::"."::: ) "(" (Set (Var "x")) "," (Set (Var "y")) ")" ")" ) "," (Set "(" "g" ($#k1_binop_1 :::"."::: ) "(" (Set (Var "x9")) "," (Set (Var "y9")) ")" ")" ) ($#k4_tarski :::"]"::: ) )) ")" ) ")" ); end; :: deftheorem defines :::"|:"::: FUNCT_4:def 3 : (Bool "for" (Set (Var "f")) "," (Set (Var "g")) "," (Set (Var "b3")) "being" ($#m1_hidden :::"Function":::) "holds" (Bool "(" (Bool (Set (Var "b3")) ($#r1_hidden :::"="::: ) (Set ($#k3_funct_4 :::"|:"::: ) (Set (Var "f")) "," (Set (Var "g")) ($#k3_funct_4 :::":|"::: ) )) "iff" (Bool "(" (Bool "(" "for" (Set (Var "z")) "being" ($#m1_hidden :::"set"::: ) "holds" (Bool "(" (Bool (Set (Var "z")) ($#r2_hidden :::"in"::: ) (Set ($#k9_xtuple_0 :::"dom"::: ) (Set (Var "b3")))) "iff" (Bool "ex" (Set (Var "x")) "," (Set (Var "y")) "," (Set (Var "x9")) "," (Set (Var "y9")) "being" ($#m1_hidden :::"set"::: ) "st" (Bool "(" (Bool (Set (Var "z")) ($#r1_hidden :::"="::: ) (Set ($#k4_tarski :::"["::: ) (Set ($#k4_tarski :::"["::: ) (Set (Var "x")) "," (Set (Var "x9")) ($#k4_tarski :::"]"::: ) ) "," (Set ($#k4_tarski :::"["::: ) (Set (Var "y")) "," (Set (Var "y9")) ($#k4_tarski :::"]"::: ) ) ($#k4_tarski :::"]"::: ) )) & (Bool (Set ($#k4_tarski :::"["::: ) (Set (Var "x")) "," (Set (Var "y")) ($#k4_tarski :::"]"::: ) ) ($#r2_hidden :::"in"::: ) (Set ($#k9_xtuple_0 :::"dom"::: ) (Set (Var "f")))) & (Bool (Set ($#k4_tarski :::"["::: ) (Set (Var "x9")) "," (Set (Var "y9")) ($#k4_tarski :::"]"::: ) ) ($#r2_hidden :::"in"::: ) (Set ($#k9_xtuple_0 :::"dom"::: ) (Set (Var "g")))) ")" )) ")" ) ")" ) & (Bool "(" "for" (Set (Var "x")) "," (Set (Var "y")) "," (Set (Var "x9")) "," (Set (Var "y9")) "being" ($#m1_hidden :::"set"::: ) "st" (Bool (Bool (Set ($#k4_tarski :::"["::: ) (Set (Var "x")) "," (Set (Var "y")) ($#k4_tarski :::"]"::: ) ) ($#r2_hidden :::"in"::: ) (Set ($#k9_xtuple_0 :::"dom"::: ) (Set (Var "f")))) & (Bool (Set ($#k4_tarski :::"["::: ) (Set (Var "x9")) "," (Set (Var "y9")) ($#k4_tarski :::"]"::: ) ) ($#r2_hidden :::"in"::: ) (Set ($#k9_xtuple_0 :::"dom"::: ) (Set (Var "g"))))) "holds" (Bool (Set (Set (Var "b3")) ($#k1_binop_1 :::"."::: ) "(" (Set ($#k4_tarski :::"["::: ) (Set (Var "x")) "," (Set (Var "x9")) ($#k4_tarski :::"]"::: ) ) "," (Set ($#k4_tarski :::"["::: ) (Set (Var "y")) "," (Set (Var "y9")) ($#k4_tarski :::"]"::: ) ) ")" ) ($#r1_hidden :::"="::: ) (Set ($#k4_tarski :::"["::: ) (Set "(" (Set (Var "f")) ($#k1_binop_1 :::"."::: ) "(" (Set (Var "x")) "," (Set (Var "y")) ")" ")" ) "," (Set "(" (Set (Var "g")) ($#k1_binop_1 :::"."::: ) "(" (Set (Var "x9")) "," (Set (Var "y9")) ")" ")" ) ($#k4_tarski :::"]"::: ) )) ")" ) ")" ) ")" )); theorem :: FUNCT_4:54 (Bool "for" (Set (Var "x")) "," (Set (Var "x9")) "," (Set (Var "y")) "," (Set (Var "y9")) "being" ($#m1_hidden :::"set"::: ) (Bool "for" (Set (Var "f")) "," (Set (Var "g")) "being" ($#m1_hidden :::"Function":::) "holds" (Bool "(" (Bool (Set ($#k4_tarski :::"["::: ) (Set ($#k4_tarski :::"["::: ) (Set (Var "x")) "," (Set (Var "x9")) ($#k4_tarski :::"]"::: ) ) "," (Set ($#k4_tarski :::"["::: ) (Set (Var "y")) "," (Set (Var "y9")) ($#k4_tarski :::"]"::: ) ) ($#k4_tarski :::"]"::: ) ) ($#r2_hidden :::"in"::: ) (Set ($#k9_xtuple_0 :::"dom"::: ) (Set ($#k3_funct_4 :::"|:"::: ) (Set (Var "f")) "," (Set (Var "g")) ($#k3_funct_4 :::":|"::: ) ))) "iff" (Bool "(" (Bool (Set ($#k4_tarski :::"["::: ) (Set (Var "x")) "," (Set (Var "y")) ($#k4_tarski :::"]"::: ) ) ($#r2_hidden :::"in"::: ) (Set ($#k9_xtuple_0 :::"dom"::: ) (Set (Var "f")))) & (Bool (Set ($#k4_tarski :::"["::: ) (Set (Var "x9")) "," (Set (Var "y9")) ($#k4_tarski :::"]"::: ) ) ($#r2_hidden :::"in"::: ) (Set ($#k9_xtuple_0 :::"dom"::: ) (Set (Var "g")))) ")" ) ")" ))) ; theorem :: FUNCT_4:55 (Bool "for" (Set (Var "x")) "," (Set (Var "x9")) "," (Set (Var "y")) "," (Set (Var "y9")) "being" ($#m1_hidden :::"set"::: ) (Bool "for" (Set (Var "f")) "," (Set (Var "g")) "being" ($#m1_hidden :::"Function":::) "st" (Bool (Bool (Set ($#k4_tarski :::"["::: ) (Set ($#k4_tarski :::"["::: ) (Set (Var "x")) "," (Set (Var "x9")) ($#k4_tarski :::"]"::: ) ) "," (Set ($#k4_tarski :::"["::: ) (Set (Var "y")) "," (Set (Var "y9")) ($#k4_tarski :::"]"::: ) ) ($#k4_tarski :::"]"::: ) ) ($#r2_hidden :::"in"::: ) (Set ($#k9_xtuple_0 :::"dom"::: ) (Set ($#k3_funct_4 :::"|:"::: ) (Set (Var "f")) "," (Set (Var "g")) ($#k3_funct_4 :::":|"::: ) )))) "holds" (Bool (Set (Set ($#k3_funct_4 :::"|:"::: ) (Set (Var "f")) "," (Set (Var "g")) ($#k3_funct_4 :::":|"::: ) ) ($#k1_binop_1 :::"."::: ) "(" (Set ($#k4_tarski :::"["::: ) (Set (Var "x")) "," (Set (Var "x9")) ($#k4_tarski :::"]"::: ) ) "," (Set ($#k4_tarski :::"["::: ) (Set (Var "y")) "," (Set (Var "y9")) ($#k4_tarski :::"]"::: ) ) ")" ) ($#r1_hidden :::"="::: ) (Set ($#k4_tarski :::"["::: ) (Set "(" (Set (Var "f")) ($#k1_binop_1 :::"."::: ) "(" (Set (Var "x")) "," (Set (Var "y")) ")" ")" ) "," (Set "(" (Set (Var "g")) ($#k1_binop_1 :::"."::: ) "(" (Set (Var "x9")) "," (Set (Var "y9")) ")" ")" ) ($#k4_tarski :::"]"::: ) )))) ; theorem :: FUNCT_4:56 (Bool "for" (Set (Var "f")) "," (Set (Var "g")) "being" ($#m1_hidden :::"Function":::) "holds" (Bool (Set ($#k10_xtuple_0 :::"rng"::: ) (Set ($#k3_funct_4 :::"|:"::: ) (Set (Var "f")) "," (Set (Var "g")) ($#k3_funct_4 :::":|"::: ) )) ($#r1_tarski :::"c="::: ) (Set ($#k2_zfmisc_1 :::"[:"::: ) (Set "(" ($#k10_xtuple_0 :::"rng"::: ) (Set (Var "f")) ")" ) "," (Set "(" ($#k10_xtuple_0 :::"rng"::: ) (Set (Var "g")) ")" ) ($#k2_zfmisc_1 :::":]"::: ) ))) ; theorem :: FUNCT_4:57 (Bool "for" (Set (Var "X")) "," (Set (Var "Y")) "," (Set (Var "X9")) "," (Set (Var "Y9")) "being" ($#m1_hidden :::"set"::: ) (Bool "for" (Set (Var "f")) "," (Set (Var "g")) "being" ($#m1_hidden :::"Function":::) "st" (Bool (Bool (Set ($#k9_xtuple_0 :::"dom"::: ) (Set (Var "f"))) ($#r1_tarski :::"c="::: ) (Set ($#k2_zfmisc_1 :::"[:"::: ) (Set (Var "X")) "," (Set (Var "Y")) ($#k2_zfmisc_1 :::":]"::: ) )) & (Bool (Set ($#k9_xtuple_0 :::"dom"::: ) (Set (Var "g"))) ($#r1_tarski :::"c="::: ) (Set ($#k2_zfmisc_1 :::"[:"::: ) (Set (Var "X9")) "," (Set (Var "Y9")) ($#k2_zfmisc_1 :::":]"::: ) ))) "holds" (Bool (Set ($#k9_xtuple_0 :::"dom"::: ) (Set ($#k3_funct_4 :::"|:"::: ) (Set (Var "f")) "," (Set (Var "g")) ($#k3_funct_4 :::":|"::: ) )) ($#r1_tarski :::"c="::: ) (Set ($#k2_zfmisc_1 :::"[:"::: ) (Set ($#k2_zfmisc_1 :::"[:"::: ) (Set (Var "X")) "," (Set (Var "X9")) ($#k2_zfmisc_1 :::":]"::: ) ) "," (Set ($#k2_zfmisc_1 :::"[:"::: ) (Set (Var "Y")) "," (Set (Var "Y9")) ($#k2_zfmisc_1 :::":]"::: ) ) ($#k2_zfmisc_1 :::":]"::: ) )))) ; theorem :: FUNCT_4:58 (Bool "for" (Set (Var "X")) "," (Set (Var "Y")) "," (Set (Var "X9")) "," (Set (Var "Y9")) "being" ($#m1_hidden :::"set"::: ) (Bool "for" (Set (Var "f")) "," (Set (Var "g")) "being" ($#m1_hidden :::"Function":::) "st" (Bool (Bool (Set ($#k9_xtuple_0 :::"dom"::: ) (Set (Var "f"))) ($#r1_hidden :::"="::: ) (Set ($#k2_zfmisc_1 :::"[:"::: ) (Set (Var "X")) "," (Set (Var "Y")) ($#k2_zfmisc_1 :::":]"::: ) )) & (Bool (Set ($#k9_xtuple_0 :::"dom"::: ) (Set (Var "g"))) ($#r1_hidden :::"="::: ) (Set ($#k2_zfmisc_1 :::"[:"::: ) (Set (Var "X9")) "," (Set (Var "Y9")) ($#k2_zfmisc_1 :::":]"::: ) ))) "holds" (Bool (Set ($#k9_xtuple_0 :::"dom"::: ) (Set ($#k3_funct_4 :::"|:"::: ) (Set (Var "f")) "," (Set (Var "g")) ($#k3_funct_4 :::":|"::: ) )) ($#r1_hidden :::"="::: ) (Set ($#k2_zfmisc_1 :::"[:"::: ) (Set ($#k2_zfmisc_1 :::"[:"::: ) (Set (Var "X")) "," (Set (Var "X9")) ($#k2_zfmisc_1 :::":]"::: ) ) "," (Set ($#k2_zfmisc_1 :::"[:"::: ) (Set (Var "Y")) "," (Set (Var "Y9")) ($#k2_zfmisc_1 :::":]"::: ) ) ($#k2_zfmisc_1 :::":]"::: ) )))) ; theorem :: FUNCT_4:59 (Bool "for" (Set (Var "X")) "," (Set (Var "Y")) "," (Set (Var "Z")) "," (Set (Var "X9")) "," (Set (Var "Y9")) "," (Set (Var "Z9")) "being" ($#m1_hidden :::"set"::: ) (Bool "for" (Set (Var "f")) "being" ($#m1_subset_1 :::"PartFunc":::) "of" (Set ($#k2_zfmisc_1 :::"[:"::: ) (Set (Var "X")) "," (Set (Var "Y")) ($#k2_zfmisc_1 :::":]"::: ) ) "," (Set (Var "Z")) (Bool "for" (Set (Var "g")) "being" ($#m1_subset_1 :::"PartFunc":::) "of" (Set ($#k2_zfmisc_1 :::"[:"::: ) (Set (Var "X9")) "," (Set (Var "Y9")) ($#k2_zfmisc_1 :::":]"::: ) ) "," (Set (Var "Z9")) "holds" (Bool (Set ($#k3_funct_4 :::"|:"::: ) (Set (Var "f")) "," (Set (Var "g")) ($#k3_funct_4 :::":|"::: ) ) "is" ($#m1_subset_1 :::"PartFunc":::) "of" (Set ($#k2_zfmisc_1 :::"[:"::: ) (Set ($#k2_zfmisc_1 :::"[:"::: ) (Set (Var "X")) "," (Set (Var "X9")) ($#k2_zfmisc_1 :::":]"::: ) ) "," (Set ($#k2_zfmisc_1 :::"[:"::: ) (Set (Var "Y")) "," (Set (Var "Y9")) ($#k2_zfmisc_1 :::":]"::: ) ) ($#k2_zfmisc_1 :::":]"::: ) ) "," (Set ($#k2_zfmisc_1 :::"[:"::: ) (Set (Var "Z")) "," (Set (Var "Z9")) ($#k2_zfmisc_1 :::":]"::: ) ))))) ; theorem :: FUNCT_4:60 (Bool "for" (Set (Var "X")) "," (Set (Var "Y")) "," (Set (Var "Z")) "," (Set (Var "X9")) "," (Set (Var "Y9")) "," (Set (Var "Z9")) "being" ($#m1_hidden :::"set"::: ) (Bool "for" (Set (Var "f")) "being" ($#m1_subset_1 :::"Function":::) "of" (Set ($#k2_zfmisc_1 :::"[:"::: ) (Set (Var "X")) "," (Set (Var "Y")) ($#k2_zfmisc_1 :::":]"::: ) ) "," (Set (Var "Z")) (Bool "for" (Set (Var "g")) "being" ($#m1_subset_1 :::"Function":::) "of" (Set ($#k2_zfmisc_1 :::"[:"::: ) (Set (Var "X9")) "," (Set (Var "Y9")) ($#k2_zfmisc_1 :::":]"::: ) ) "," (Set (Var "Z9")) "st" (Bool (Bool (Set (Var "Z")) ($#r1_hidden :::"<>"::: ) (Set ($#k1_xboole_0 :::"{}"::: ) )) & (Bool (Set (Var "Z9")) ($#r1_hidden :::"<>"::: ) (Set ($#k1_xboole_0 :::"{}"::: ) ))) "holds" (Bool (Set ($#k3_funct_4 :::"|:"::: ) (Set (Var "f")) "," (Set (Var "g")) ($#k3_funct_4 :::":|"::: ) ) "is" ($#m1_subset_1 :::"Function":::) "of" (Set ($#k2_zfmisc_1 :::"[:"::: ) (Set ($#k2_zfmisc_1 :::"[:"::: ) (Set (Var "X")) "," (Set (Var "X9")) ($#k2_zfmisc_1 :::":]"::: ) ) "," (Set ($#k2_zfmisc_1 :::"[:"::: ) (Set (Var "Y")) "," (Set (Var "Y9")) ($#k2_zfmisc_1 :::":]"::: ) ) ($#k2_zfmisc_1 :::":]"::: ) ) "," (Set ($#k2_zfmisc_1 :::"[:"::: ) (Set (Var "Z")) "," (Set (Var "Z9")) ($#k2_zfmisc_1 :::":]"::: ) ))))) ; theorem :: FUNCT_4:61 (Bool "for" (Set (Var "X")) "," (Set (Var "Y")) "," (Set (Var "X9")) "," (Set (Var "Y9")) "being" ($#m1_hidden :::"set"::: ) (Bool "for" (Set (Var "D")) "," (Set (Var "D9")) "being" ($#~v1_xboole_0 "non" ($#v1_xboole_0 :::"empty"::: ) ) ($#m1_hidden :::"set"::: ) (Bool "for" (Set (Var "f")) "being" ($#m1_subset_1 :::"Function":::) "of" (Set ($#k2_zfmisc_1 :::"[:"::: ) (Set (Var "X")) "," (Set (Var "Y")) ($#k2_zfmisc_1 :::":]"::: ) ) "," (Set (Var "D")) (Bool "for" (Set (Var "g")) "being" ($#m1_subset_1 :::"Function":::) "of" (Set ($#k2_zfmisc_1 :::"[:"::: ) (Set (Var "X9")) "," (Set (Var "Y9")) ($#k2_zfmisc_1 :::":]"::: ) ) "," (Set (Var "D9")) "holds" (Bool (Set ($#k3_funct_4 :::"|:"::: ) (Set (Var "f")) "," (Set (Var "g")) ($#k3_funct_4 :::":|"::: ) ) "is" ($#m1_subset_1 :::"Function":::) "of" (Set ($#k2_zfmisc_1 :::"[:"::: ) (Set ($#k2_zfmisc_1 :::"[:"::: ) (Set (Var "X")) "," (Set (Var "X9")) ($#k2_zfmisc_1 :::":]"::: ) ) "," (Set ($#k2_zfmisc_1 :::"[:"::: ) (Set (Var "Y")) "," (Set (Var "Y9")) ($#k2_zfmisc_1 :::":]"::: ) ) ($#k2_zfmisc_1 :::":]"::: ) ) "," (Set ($#k2_zfmisc_1 :::"[:"::: ) (Set (Var "D")) "," (Set (Var "D9")) ($#k2_zfmisc_1 :::":]"::: ) )))))) ; definitionlet "x", "y", "a", "b" be ($#m1_hidden :::"set"::: ) ; func "(" "x" "," "y" ")" :::"-->"::: "(" "a" "," "b" ")" -> ($#m1_hidden :::"set"::: ) equals :: FUNCT_4:def 4 (Set (Set "(" "x" ($#k16_funcop_1 :::".-->"::: ) "a" ")" ) ($#k1_funct_4 :::"+*"::: ) (Set "(" "y" ($#k16_funcop_1 :::".-->"::: ) "b" ")" )); end; :: deftheorem defines :::"-->"::: FUNCT_4:def 4 : (Bool "for" (Set (Var "x")) "," (Set (Var "y")) "," (Set (Var "a")) "," (Set (Var "b")) "being" ($#m1_hidden :::"set"::: ) "holds" (Bool (Set "(" (Set (Var "x")) "," (Set (Var "y")) ")" ($#k4_funct_4 :::"-->"::: ) "(" (Set (Var "a")) "," (Set (Var "b")) ")" ) ($#r1_hidden :::"="::: ) (Set (Set "(" (Set (Var "x")) ($#k16_funcop_1 :::".-->"::: ) (Set (Var "a")) ")" ) ($#k1_funct_4 :::"+*"::: ) (Set "(" (Set (Var "y")) ($#k16_funcop_1 :::".-->"::: ) (Set (Var "b")) ")" )))); registrationlet "x", "y", "a", "b" be ($#m1_hidden :::"set"::: ) ; cluster (Set "(" "x" "," "y" ")" ($#k4_funct_4 :::"-->"::: ) "(" "a" "," "b" ")" ) -> ($#v1_relat_1 :::"Relation-like"::: ) ($#v1_funct_1 :::"Function-like"::: ) ; end; theorem :: FUNCT_4:62 (Bool "for" (Set (Var "x1")) "," (Set (Var "x2")) "," (Set (Var "y1")) "," (Set (Var "y2")) "being" ($#m1_hidden :::"set"::: ) "holds" (Bool "(" (Bool (Set ($#k9_xtuple_0 :::"dom"::: ) (Set "(" "(" (Set (Var "x1")) "," (Set (Var "x2")) ")" ($#k4_funct_4 :::"-->"::: ) "(" (Set (Var "y1")) "," (Set (Var "y2")) ")" ")" )) ($#r1_hidden :::"="::: ) (Set ($#k2_tarski :::"{"::: ) (Set (Var "x1")) "," (Set (Var "x2")) ($#k2_tarski :::"}"::: ) )) & (Bool (Set ($#k10_xtuple_0 :::"rng"::: ) (Set "(" "(" (Set (Var "x1")) "," (Set (Var "x2")) ")" ($#k4_funct_4 :::"-->"::: ) "(" (Set (Var "y1")) "," (Set (Var "y2")) ")" ")" )) ($#r1_tarski :::"c="::: ) (Set ($#k2_tarski :::"{"::: ) (Set (Var "y1")) "," (Set (Var "y2")) ($#k2_tarski :::"}"::: ) )) ")" )) ; theorem :: FUNCT_4:63 (Bool "for" (Set (Var "x1")) "," (Set (Var "x2")) "," (Set (Var "y1")) "," (Set (Var "y2")) "being" ($#m1_hidden :::"set"::: ) "holds" (Bool "(" "(" (Bool (Bool (Set (Var "x1")) ($#r1_hidden :::"<>"::: ) (Set (Var "x2")))) "implies" (Bool (Set (Set "(" "(" (Set (Var "x1")) "," (Set (Var "x2")) ")" ($#k4_funct_4 :::"-->"::: ) "(" (Set (Var "y1")) "," (Set (Var "y2")) ")" ")" ) ($#k1_funct_1 :::"."::: ) (Set (Var "x1"))) ($#r1_hidden :::"="::: ) (Set (Var "y1"))) ")" & (Bool (Set (Set "(" "(" (Set (Var "x1")) "," (Set (Var "x2")) ")" ($#k4_funct_4 :::"-->"::: ) "(" (Set (Var "y1")) "," (Set (Var "y2")) ")" ")" ) ($#k1_funct_1 :::"."::: ) (Set (Var "x2"))) ($#r1_hidden :::"="::: ) (Set (Var "y2"))) ")" )) ; theorem :: FUNCT_4:64 (Bool "for" (Set (Var "x1")) "," (Set (Var "x2")) "," (Set (Var "y1")) "," (Set (Var "y2")) "being" ($#m1_hidden :::"set"::: ) "st" (Bool (Bool (Set (Var "x1")) ($#r1_hidden :::"<>"::: ) (Set (Var "x2")))) "holds" (Bool (Set ($#k10_xtuple_0 :::"rng"::: ) (Set "(" "(" (Set (Var "x1")) "," (Set (Var "x2")) ")" ($#k4_funct_4 :::"-->"::: ) "(" (Set (Var "y1")) "," (Set (Var "y2")) ")" ")" )) ($#r1_hidden :::"="::: ) (Set ($#k2_tarski :::"{"::: ) (Set (Var "y1")) "," (Set (Var "y2")) ($#k2_tarski :::"}"::: ) ))) ; theorem :: FUNCT_4:65 (Bool "for" (Set (Var "x1")) "," (Set (Var "x2")) "," (Set (Var "y")) "being" ($#m1_hidden :::"set"::: ) "holds" (Bool (Set "(" (Set (Var "x1")) "," (Set (Var "x2")) ")" ($#k4_funct_4 :::"-->"::: ) "(" (Set (Var "y")) "," (Set (Var "y")) ")" ) ($#r1_hidden :::"="::: ) (Set (Set ($#k2_tarski :::"{"::: ) (Set (Var "x1")) "," (Set (Var "x2")) ($#k2_tarski :::"}"::: ) ) ($#k7_funcop_1 :::"-->"::: ) (Set (Var "y"))))) ; definitionlet "A" be ($#~v1_xboole_0 "non" ($#v1_xboole_0 :::"empty"::: ) ) ($#m1_hidden :::"set"::: ) ; let "x1", "x2" be ($#m1_hidden :::"set"::: ) ; let "y1", "y2" be ($#m1_subset_1 :::"Element"::: ) "of" (Set (Const "A")); :: original: :::"-->"::: redefine func "(" "x1" "," "x2" ")" :::"-->"::: "(" "y1" "," "y2" ")" -> ($#m1_subset_1 :::"Function":::) "of" (Set ($#k2_tarski :::"{"::: ) "x1" "," "x2" ($#k2_tarski :::"}"::: ) ) "," "A"; end; theorem :: FUNCT_4:66 (Bool "for" (Set (Var "a")) "," (Set (Var "b")) "," (Set (Var "c")) "," (Set (Var "d")) "being" ($#m1_hidden :::"set"::: ) (Bool "for" (Set (Var "g")) "being" ($#m1_hidden :::"Function":::) "st" (Bool (Bool (Set ($#k9_xtuple_0 :::"dom"::: ) (Set (Var "g"))) ($#r1_hidden :::"="::: ) (Set ($#k2_tarski :::"{"::: ) (Set (Var "a")) "," (Set (Var "b")) ($#k2_tarski :::"}"::: ) )) & (Bool (Set (Set (Var "g")) ($#k1_funct_1 :::"."::: ) (Set (Var "a"))) ($#r1_hidden :::"="::: ) (Set (Var "c"))) & (Bool (Set (Set (Var "g")) ($#k1_funct_1 :::"."::: ) (Set (Var "b"))) ($#r1_hidden :::"="::: ) (Set (Var "d")))) "holds" (Bool (Set (Var "g")) ($#r1_hidden :::"="::: ) (Set "(" (Set (Var "a")) "," (Set (Var "b")) ")" ($#k4_funct_4 :::"-->"::: ) "(" (Set (Var "c")) "," (Set (Var "d")) ")" )))) ; theorem :: FUNCT_4:67 (Bool "for" (Set (Var "a")) "," (Set (Var "b")) "," (Set (Var "c")) "," (Set (Var "d")) "being" ($#m1_hidden :::"set"::: ) "st" (Bool (Bool (Set (Var "a")) ($#r1_hidden :::"<>"::: ) (Set (Var "c")))) "holds" (Bool (Set "(" (Set (Var "a")) "," (Set (Var "c")) ")" ($#k4_funct_4 :::"-->"::: ) "(" (Set (Var "b")) "," (Set (Var "d")) ")" ) ($#r1_hidden :::"="::: ) (Set ($#k2_tarski :::"{"::: ) (Set ($#k4_tarski :::"["::: ) (Set (Var "a")) "," (Set (Var "b")) ($#k4_tarski :::"]"::: ) ) "," (Set ($#k4_tarski :::"["::: ) (Set (Var "c")) "," (Set (Var "d")) ($#k4_tarski :::"]"::: ) ) ($#k2_tarski :::"}"::: ) ))) ; theorem :: FUNCT_4:68 (Bool "for" (Set (Var "a")) "," (Set (Var "b")) "," (Set (Var "x")) "," (Set (Var "y")) "," (Set (Var "x9")) "," (Set (Var "y9")) "being" ($#m1_hidden :::"set"::: ) "st" (Bool (Bool (Set (Var "a")) ($#r1_hidden :::"<>"::: ) (Set (Var "b"))) & (Bool (Set "(" (Set (Var "a")) "," (Set (Var "b")) ")" ($#k4_funct_4 :::"-->"::: ) "(" (Set (Var "x")) "," (Set (Var "y")) ")" ) ($#r1_hidden :::"="::: ) (Set "(" (Set (Var "a")) "," (Set (Var "b")) ")" ($#k4_funct_4 :::"-->"::: ) "(" (Set (Var "x9")) "," (Set (Var "y9")) ")" ))) "holds" (Bool "(" (Bool (Set (Var "x")) ($#r1_hidden :::"="::: ) (Set (Var "x9"))) & (Bool (Set (Var "y")) ($#r1_hidden :::"="::: ) (Set (Var "y9"))) ")" )) ; begin theorem :: FUNCT_4:69 (Bool "for" (Set (Var "f1")) "," (Set (Var "f2")) "," (Set (Var "g1")) "," (Set (Var "g2")) "being" ($#m1_hidden :::"Function":::) "st" (Bool (Bool (Set ($#k10_xtuple_0 :::"rng"::: ) (Set (Var "g1"))) ($#r1_tarski :::"c="::: ) (Set ($#k9_xtuple_0 :::"dom"::: ) (Set (Var "f1")))) & (Bool (Set ($#k10_xtuple_0 :::"rng"::: ) (Set (Var "g2"))) ($#r1_tarski :::"c="::: ) (Set ($#k9_xtuple_0 :::"dom"::: ) (Set (Var "f2")))) & (Bool (Set (Var "f1")) ($#r1_partfun1 :::"tolerates"::: ) (Set (Var "f2")))) "holds" (Bool (Set (Set "(" (Set (Var "f1")) ($#k1_funct_4 :::"+*"::: ) (Set (Var "f2")) ")" ) ($#k3_relat_1 :::"*"::: ) (Set "(" (Set (Var "g1")) ($#k1_funct_4 :::"+*"::: ) (Set (Var "g2")) ")" )) ($#r1_hidden :::"="::: ) (Set (Set "(" (Set (Var "f1")) ($#k3_relat_1 :::"*"::: ) (Set (Var "g1")) ")" ) ($#k1_funct_4 :::"+*"::: ) (Set "(" (Set (Var "f2")) ($#k3_relat_1 :::"*"::: ) (Set (Var "g2")) ")" )))) ; theorem :: FUNCT_4:70 (Bool "for" (Set (Var "f")) "being" ($#m1_hidden :::"Function":::) (Bool "for" (Set (Var "A")) "," (Set (Var "B")) "being" ($#m1_hidden :::"set"::: ) "st" (Bool (Bool (Set ($#k9_xtuple_0 :::"dom"::: ) (Set (Var "f"))) ($#r1_tarski :::"c="::: ) (Set (Set (Var "A")) ($#k2_xboole_0 :::"\/"::: ) (Set (Var "B"))))) "holds" (Bool (Set (Set "(" (Set (Var "f")) ($#k5_relat_1 :::"|"::: ) (Set (Var "A")) ")" ) ($#k1_funct_4 :::"+*"::: ) (Set "(" (Set (Var "f")) ($#k5_relat_1 :::"|"::: ) (Set (Var "B")) ")" )) ($#r1_hidden :::"="::: ) (Set (Var "f"))))) ; theorem :: FUNCT_4:71 (Bool "for" (Set (Var "p")) "," (Set (Var "q")) "being" ($#m1_hidden :::"Function":::) (Bool "for" (Set (Var "A")) "being" ($#m1_hidden :::"set"::: ) "holds" (Bool (Set (Set "(" (Set (Var "p")) ($#k1_funct_4 :::"+*"::: ) (Set (Var "q")) ")" ) ($#k5_relat_1 :::"|"::: ) (Set (Var "A"))) ($#r1_hidden :::"="::: ) (Set (Set "(" (Set (Var "p")) ($#k5_relat_1 :::"|"::: ) (Set (Var "A")) ")" ) ($#k1_funct_4 :::"+*"::: ) (Set "(" (Set (Var "q")) ($#k5_relat_1 :::"|"::: ) (Set (Var "A")) ")" ))))) ; theorem :: FUNCT_4:72 (Bool "for" (Set (Var "f")) "," (Set (Var "g")) "being" ($#m1_hidden :::"Function":::) (Bool "for" (Set (Var "A")) "being" ($#m1_hidden :::"set"::: ) "st" (Bool (Bool (Set (Var "A")) ($#r1_xboole_0 :::"misses"::: ) (Set ($#k9_xtuple_0 :::"dom"::: ) (Set (Var "g"))))) "holds" (Bool (Set (Set "(" (Set (Var "f")) ($#k1_funct_4 :::"+*"::: ) (Set (Var "g")) ")" ) ($#k5_relat_1 :::"|"::: ) (Set (Var "A"))) ($#r1_hidden :::"="::: ) (Set (Set (Var "f")) ($#k5_relat_1 :::"|"::: ) (Set (Var "A")))))) ; theorem :: FUNCT_4:73 (Bool "for" (Set (Var "f")) "," (Set (Var "g")) "being" ($#m1_hidden :::"Function":::) (Bool "for" (Set (Var "A")) "being" ($#m1_hidden :::"set"::: ) "st" (Bool (Bool (Set ($#k9_xtuple_0 :::"dom"::: ) (Set (Var "f"))) ($#r1_xboole_0 :::"misses"::: ) (Set (Var "A")))) "holds" (Bool (Set (Set "(" (Set (Var "f")) ($#k1_funct_4 :::"+*"::: ) (Set (Var "g")) ")" ) ($#k5_relat_1 :::"|"::: ) (Set (Var "A"))) ($#r1_hidden :::"="::: ) (Set (Set (Var "g")) ($#k5_relat_1 :::"|"::: ) (Set (Var "A")))))) ; theorem :: FUNCT_4:74 (Bool "for" (Set (Var "f")) "," (Set (Var "g")) "," (Set (Var "h")) "being" ($#m1_hidden :::"Function":::) "st" (Bool (Bool (Set ($#k9_xtuple_0 :::"dom"::: ) (Set (Var "g"))) ($#r1_hidden :::"="::: ) (Set ($#k9_xtuple_0 :::"dom"::: ) (Set (Var "h"))))) "holds" (Bool (Set (Set "(" (Set (Var "f")) ($#k1_funct_4 :::"+*"::: ) (Set (Var "g")) ")" ) ($#k1_funct_4 :::"+*"::: ) (Set (Var "h"))) ($#r1_hidden :::"="::: ) (Set (Set (Var "f")) ($#k1_funct_4 :::"+*"::: ) (Set (Var "h"))))) ; theorem :: FUNCT_4:75 (Bool "for" (Set (Var "f")) "being" ($#m1_hidden :::"Function":::) (Bool "for" (Set (Var "A")) "being" ($#m1_hidden :::"set"::: ) "holds" (Bool (Set (Set (Var "f")) ($#k1_funct_4 :::"+*"::: ) (Set "(" (Set (Var "f")) ($#k5_relat_1 :::"|"::: ) (Set (Var "A")) ")" )) ($#r1_hidden :::"="::: ) (Set (Var "f"))))) ; theorem :: FUNCT_4:76 (Bool "for" (Set (Var "f")) "," (Set (Var "g")) "being" ($#m1_hidden :::"Function":::) (Bool "for" (Set (Var "B")) "," (Set (Var "C")) "being" ($#m1_hidden :::"set"::: ) "st" (Bool (Bool (Set ($#k9_xtuple_0 :::"dom"::: ) (Set (Var "f"))) ($#r1_tarski :::"c="::: ) (Set (Var "B"))) & (Bool (Set ($#k9_xtuple_0 :::"dom"::: ) (Set (Var "g"))) ($#r1_tarski :::"c="::: ) (Set (Var "C"))) & (Bool (Set (Var "B")) ($#r1_xboole_0 :::"misses"::: ) (Set (Var "C")))) "holds" (Bool "(" (Bool (Set (Set "(" (Set (Var "f")) ($#k1_funct_4 :::"+*"::: ) (Set (Var "g")) ")" ) ($#k5_relat_1 :::"|"::: ) (Set (Var "B"))) ($#r1_hidden :::"="::: ) (Set (Var "f"))) & (Bool (Set (Set "(" (Set (Var "f")) ($#k1_funct_4 :::"+*"::: ) (Set (Var "g")) ")" ) ($#k5_relat_1 :::"|"::: ) (Set (Var "C"))) ($#r1_hidden :::"="::: ) (Set (Var "g"))) ")" ))) ; theorem :: FUNCT_4:77 (Bool "for" (Set (Var "p")) "," (Set (Var "q")) "being" ($#m1_hidden :::"Function":::) (Bool "for" (Set (Var "A")) "being" ($#m1_hidden :::"set"::: ) "st" (Bool (Bool (Set ($#k9_xtuple_0 :::"dom"::: ) (Set (Var "p"))) ($#r1_tarski :::"c="::: ) (Set (Var "A"))) & (Bool (Set ($#k9_xtuple_0 :::"dom"::: ) (Set (Var "q"))) ($#r1_xboole_0 :::"misses"::: ) (Set (Var "A")))) "holds" (Bool (Set (Set "(" (Set (Var "p")) ($#k1_funct_4 :::"+*"::: ) (Set (Var "q")) ")" ) ($#k5_relat_1 :::"|"::: ) (Set (Var "A"))) ($#r1_hidden :::"="::: ) (Set (Var "p"))))) ; theorem :: FUNCT_4:78 (Bool "for" (Set (Var "f")) "being" ($#m1_hidden :::"Function":::) (Bool "for" (Set (Var "A")) "," (Set (Var "B")) "being" ($#m1_hidden :::"set"::: ) "holds" (Bool (Set (Set (Var "f")) ($#k5_relat_1 :::"|"::: ) (Set "(" (Set (Var "A")) ($#k2_xboole_0 :::"\/"::: ) (Set (Var "B")) ")" )) ($#r1_hidden :::"="::: ) (Set (Set "(" (Set (Var "f")) ($#k5_relat_1 :::"|"::: ) (Set (Var "A")) ")" ) ($#k1_funct_4 :::"+*"::: ) (Set "(" (Set (Var "f")) ($#k5_relat_1 :::"|"::: ) (Set (Var "B")) ")" ))))) ; theorem :: FUNCT_4:79 (Bool "for" (Set (Var "i")) "," (Set (Var "j")) "," (Set (Var "k")) "being" ($#m1_hidden :::"set"::: ) "holds" (Bool (Set "(" (Set (Var "i")) "," (Set (Var "j")) ")" ($#k17_funcop_1 :::":->"::: ) (Set (Var "k"))) ($#r1_hidden :::"="::: ) (Set (Set ($#k4_tarski :::"["::: ) (Set (Var "i")) "," (Set (Var "j")) ($#k4_tarski :::"]"::: ) ) ($#k16_funcop_1 :::".-->"::: ) (Set (Var "k"))))) ; theorem :: FUNCT_4:80 (Bool "for" (Set (Var "i")) "," (Set (Var "j")) "," (Set (Var "k")) "being" ($#m1_hidden :::"set"::: ) "holds" (Bool (Set (Set "(" "(" (Set (Var "i")) "," (Set (Var "j")) ")" ($#k17_funcop_1 :::":->"::: ) (Set (Var "k")) ")" ) ($#k1_binop_1 :::"."::: ) "(" (Set (Var "i")) "," (Set (Var "j")) ")" ) ($#r1_hidden :::"="::: ) (Set (Var "k")))) ; theorem :: FUNCT_4:81 (Bool "for" (Set (Var "a")) "," (Set (Var "b")) "," (Set (Var "c")) "being" ($#m1_hidden :::"set"::: ) "holds" (Bool (Set "(" (Set (Var "a")) "," (Set (Var "a")) ")" ($#k4_funct_4 :::"-->"::: ) "(" (Set (Var "b")) "," (Set (Var "c")) ")" ) ($#r1_hidden :::"="::: ) (Set (Set (Var "a")) ($#k16_funcop_1 :::".-->"::: ) (Set (Var "c"))))) ; theorem :: FUNCT_4:82 (Bool "for" (Set (Var "x")) "," (Set (Var "y")) "being" ($#m1_hidden :::"set"::: ) "holds" (Bool (Set (Set (Var "x")) ($#k16_funcop_1 :::".-->"::: ) (Set (Var "y"))) ($#r1_hidden :::"="::: ) (Set ($#k1_tarski :::"{"::: ) (Set ($#k4_tarski :::"["::: ) (Set (Var "x")) "," (Set (Var "y")) ($#k4_tarski :::"]"::: ) ) ($#k1_tarski :::"}"::: ) ))) ; theorem :: FUNCT_4:83 (Bool "for" (Set (Var "f")) "being" ($#m1_hidden :::"Function":::) (Bool "for" (Set (Var "a")) "," (Set (Var "b")) "," (Set (Var "c")) "being" ($#m1_hidden :::"set"::: ) "st" (Bool (Bool (Set (Var "a")) ($#r1_hidden :::"<>"::: ) (Set (Var "c")))) "holds" (Bool (Set (Set "(" (Set (Var "f")) ($#k1_funct_4 :::"+*"::: ) (Set "(" (Set (Var "a")) ($#k16_funcop_1 :::".-->"::: ) (Set (Var "b")) ")" ) ")" ) ($#k1_funct_1 :::"."::: ) (Set (Var "c"))) ($#r1_hidden :::"="::: ) (Set (Set (Var "f")) ($#k1_funct_1 :::"."::: ) (Set (Var "c")))))) ; theorem :: FUNCT_4:84 (Bool "for" (Set (Var "f")) "being" ($#m1_hidden :::"Function":::) (Bool "for" (Set (Var "a")) "," (Set (Var "b")) "," (Set (Var "c")) "," (Set (Var "d")) "being" ($#m1_hidden :::"set"::: ) "st" (Bool (Bool (Set (Var "a")) ($#r1_hidden :::"<>"::: ) (Set (Var "b")))) "holds" (Bool "(" (Bool (Set (Set "(" (Set (Var "f")) ($#k1_funct_4 :::"+*"::: ) (Set "(" "(" (Set (Var "a")) "," (Set (Var "b")) ")" ($#k4_funct_4 :::"-->"::: ) "(" (Set (Var "c")) "," (Set (Var "d")) ")" ")" ) ")" ) ($#k1_funct_1 :::"."::: ) (Set (Var "a"))) ($#r1_hidden :::"="::: ) (Set (Var "c"))) & (Bool (Set (Set "(" (Set (Var "f")) ($#k1_funct_4 :::"+*"::: ) (Set "(" "(" (Set (Var "a")) "," (Set (Var "b")) ")" ($#k4_funct_4 :::"-->"::: ) "(" (Set (Var "c")) "," (Set (Var "d")) ")" ")" ) ")" ) ($#k1_funct_1 :::"."::: ) (Set (Var "b"))) ($#r1_hidden :::"="::: ) (Set (Var "d"))) ")" ))) ; theorem :: FUNCT_4:85 (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 "a")) ($#r2_hidden :::"in"::: ) (Set ($#k9_xtuple_0 :::"dom"::: ) (Set (Var "f")))) & (Bool (Set (Set (Var "f")) ($#k1_funct_1 :::"."::: ) (Set (Var "a"))) ($#r1_hidden :::"="::: ) (Set (Var "b")))) "holds" (Bool (Set (Set (Var "a")) ($#k16_funcop_1 :::".-->"::: ) (Set (Var "b"))) ($#r1_tarski :::"c="::: ) (Set (Var "f"))))) ; theorem :: FUNCT_4:86 (Bool "for" (Set (Var "a")) "," (Set (Var "b")) "," (Set (Var "c")) "," (Set (Var "d")) "being" ($#m1_hidden :::"set"::: ) (Bool "for" (Set (Var "f")) "being" ($#m1_hidden :::"Function":::) "st" (Bool (Bool (Set (Var "a")) ($#r2_hidden :::"in"::: ) (Set ($#k9_xtuple_0 :::"dom"::: ) (Set (Var "f")))) & (Bool (Set (Var "c")) ($#r2_hidden :::"in"::: ) (Set ($#k9_xtuple_0 :::"dom"::: ) (Set (Var "f")))) & (Bool (Set (Set (Var "f")) ($#k1_funct_1 :::"."::: ) (Set (Var "a"))) ($#r1_hidden :::"="::: ) (Set (Var "b"))) & (Bool (Set (Set (Var "f")) ($#k1_funct_1 :::"."::: ) (Set (Var "c"))) ($#r1_hidden :::"="::: ) (Set (Var "d")))) "holds" (Bool (Set "(" (Set (Var "a")) "," (Set (Var "c")) ")" ($#k4_funct_4 :::"-->"::: ) "(" (Set (Var "b")) "," (Set (Var "d")) ")" ) ($#r1_tarski :::"c="::: ) (Set (Var "f"))))) ; theorem :: FUNCT_4:87 (Bool "for" (Set (Var "f")) "," (Set (Var "g")) "," (Set (Var "h")) "being" ($#m1_hidden :::"Function":::) "st" (Bool (Bool (Set (Var "f")) ($#r1_tarski :::"c="::: ) (Set (Var "h"))) & (Bool (Set (Var "g")) ($#r1_tarski :::"c="::: ) (Set (Var "h")))) "holds" (Bool (Set (Set (Var "f")) ($#k1_funct_4 :::"+*"::: ) (Set (Var "g"))) ($#r1_tarski :::"c="::: ) (Set (Var "h")))) ; theorem :: FUNCT_4:88 (Bool "for" (Set (Var "f")) "," (Set (Var "g")) "being" ($#m1_hidden :::"Function":::) (Bool "for" (Set (Var "A")) "being" ($#m1_hidden :::"set"::: ) "st" (Bool (Bool (Set (Set (Var "A")) ($#k3_xboole_0 :::"/\"::: ) (Set "(" ($#k9_xtuple_0 :::"dom"::: ) (Set (Var "f")) ")" )) ($#r1_tarski :::"c="::: ) (Set (Set (Var "A")) ($#k3_xboole_0 :::"/\"::: ) (Set "(" ($#k9_xtuple_0 :::"dom"::: ) (Set (Var "g")) ")" )))) "holds" (Bool (Set (Set "(" (Set (Var "f")) ($#k1_funct_4 :::"+*"::: ) (Set "(" (Set (Var "g")) ($#k5_relat_1 :::"|"::: ) (Set (Var "A")) ")" ) ")" ) ($#k5_relat_1 :::"|"::: ) (Set (Var "A"))) ($#r1_hidden :::"="::: ) (Set (Set (Var "g")) ($#k5_relat_1 :::"|"::: ) (Set (Var "A")))))) ; theorem :: FUNCT_4:89 (Bool "for" (Set (Var "f")) "being" ($#m1_hidden :::"Function":::) (Bool "for" (Set (Var "a")) "," (Set (Var "b")) "," (Set (Var "n")) "," (Set (Var "m")) "being" ($#m1_hidden :::"set"::: ) "holds" (Bool (Set (Set "(" (Set "(" (Set (Var "f")) ($#k1_funct_4 :::"+*"::: ) (Set "(" (Set (Var "a")) ($#k16_funcop_1 :::".-->"::: ) (Set (Var "b")) ")" ) ")" ) ($#k1_funct_4 :::"+*"::: ) (Set "(" (Set (Var "m")) ($#k16_funcop_1 :::".-->"::: ) (Set (Var "n")) ")" ) ")" ) ($#k1_funct_1 :::"."::: ) (Set (Var "m"))) ($#r1_hidden :::"="::: ) (Set (Var "n"))))) ; theorem :: FUNCT_4:90 (Bool "for" (Set (Var "f")) "being" ($#m1_hidden :::"Function":::) (Bool "for" (Set (Var "n")) "," (Set (Var "m")) "being" ($#m1_hidden :::"set"::: ) "holds" (Bool (Set (Set "(" (Set "(" (Set (Var "f")) ($#k1_funct_4 :::"+*"::: ) (Set "(" (Set (Var "n")) ($#k16_funcop_1 :::".-->"::: ) (Set (Var "m")) ")" ) ")" ) ($#k1_funct_4 :::"+*"::: ) (Set "(" (Set (Var "m")) ($#k16_funcop_1 :::".-->"::: ) (Set (Var "n")) ")" ) ")" ) ($#k1_funct_1 :::"."::: ) (Set (Var "n"))) ($#r1_hidden :::"="::: ) (Set (Var "m"))))) ; theorem :: FUNCT_4:91 (Bool "for" (Set (Var "f")) "being" ($#m1_hidden :::"Function":::) (Bool "for" (Set (Var "a")) "," (Set (Var "b")) "," (Set (Var "n")) "," (Set (Var "m")) "," (Set (Var "x")) "being" ($#m1_hidden :::"set"::: ) "st" (Bool (Bool (Set (Var "x")) ($#r1_hidden :::"<>"::: ) (Set (Var "m"))) & (Bool (Set (Var "x")) ($#r1_hidden :::"<>"::: ) (Set (Var "a")))) "holds" (Bool (Set (Set "(" (Set "(" (Set (Var "f")) ($#k1_funct_4 :::"+*"::: ) (Set "(" (Set (Var "a")) ($#k16_funcop_1 :::".-->"::: ) (Set (Var "b")) ")" ) ")" ) ($#k1_funct_4 :::"+*"::: ) (Set "(" (Set (Var "m")) ($#k16_funcop_1 :::".-->"::: ) (Set (Var "n")) ")" ) ")" ) ($#k1_funct_1 :::"."::: ) (Set (Var "x"))) ($#r1_hidden :::"="::: ) (Set (Set (Var "f")) ($#k1_funct_1 :::"."::: ) (Set (Var "x")))))) ; theorem :: FUNCT_4:92 (Bool "for" (Set (Var "f")) "," (Set (Var "g")) "being" ($#m1_hidden :::"Function":::) "st" (Bool (Bool (Set (Var "f")) "is" ($#v2_funct_1 :::"one-to-one"::: ) ) & (Bool (Set (Var "g")) "is" ($#v2_funct_1 :::"one-to-one"::: ) ) & (Bool (Set ($#k10_xtuple_0 :::"rng"::: ) (Set (Var "f"))) ($#r1_xboole_0 :::"misses"::: ) (Set ($#k10_xtuple_0 :::"rng"::: ) (Set (Var "g"))))) "holds" (Bool (Set (Set (Var "f")) ($#k1_funct_4 :::"+*"::: ) (Set (Var "g"))) "is" ($#v2_funct_1 :::"one-to-one"::: ) )) ; registrationlet "f", "g" be ($#m1_hidden :::"Function":::); reduce ; end; theorem :: FUNCT_4:93 (Bool "for" (Set (Var "f")) "," (Set (Var "g")) "being" ($#m1_hidden :::"Function":::) "holds" (Bool (Set (Set "(" (Set (Var "f")) ($#k1_funct_4 :::"+*"::: ) (Set (Var "g")) ")" ) ($#k1_funct_4 :::"+*"::: ) (Set (Var "g"))) ($#r1_hidden :::"="::: ) (Set (Set (Var "f")) ($#k1_funct_4 :::"+*"::: ) (Set (Var "g"))))) ; theorem :: FUNCT_4:94 (Bool "for" (Set (Var "f")) "," (Set (Var "g")) "," (Set (Var "h")) "being" ($#m1_hidden :::"Function":::) (Bool "for" (Set (Var "D")) "being" ($#m1_hidden :::"set"::: ) "st" (Bool (Bool (Set (Set "(" (Set (Var "f")) ($#k1_funct_4 :::"+*"::: ) (Set (Var "g")) ")" ) ($#k5_relat_1 :::"|"::: ) (Set (Var "D"))) ($#r1_hidden :::"="::: ) (Set (Set (Var "h")) ($#k5_relat_1 :::"|"::: ) (Set (Var "D"))))) "holds" (Bool (Set (Set "(" (Set (Var "h")) ($#k1_funct_4 :::"+*"::: ) (Set (Var "g")) ")" ) ($#k5_relat_1 :::"|"::: ) (Set (Var "D"))) ($#r1_hidden :::"="::: ) (Set (Set "(" (Set (Var "f")) ($#k1_funct_4 :::"+*"::: ) (Set (Var "g")) ")" ) ($#k5_relat_1 :::"|"::: ) (Set (Var "D")))))) ; theorem :: FUNCT_4:95 (Bool "for" (Set (Var "f")) "," (Set (Var "g")) "," (Set (Var "h")) "being" ($#m1_hidden :::"Function":::) (Bool "for" (Set (Var "D")) "being" ($#m1_hidden :::"set"::: ) "st" (Bool (Bool (Set (Set (Var "f")) ($#k5_relat_1 :::"|"::: ) (Set (Var "D"))) ($#r1_hidden :::"="::: ) (Set (Set (Var "h")) ($#k5_relat_1 :::"|"::: ) (Set (Var "D"))))) "holds" (Bool (Set (Set "(" (Set (Var "h")) ($#k1_funct_4 :::"+*"::: ) (Set (Var "g")) ")" ) ($#k5_relat_1 :::"|"::: ) (Set (Var "D"))) ($#r1_hidden :::"="::: ) (Set (Set "(" (Set (Var "f")) ($#k1_funct_4 :::"+*"::: ) (Set (Var "g")) ")" ) ($#k5_relat_1 :::"|"::: ) (Set (Var "D")))))) ; theorem :: FUNCT_4:96 (Bool "for" (Set (Var "x")) "being" ($#m1_hidden :::"set"::: ) "holds" (Bool (Set (Set (Var "x")) ($#k16_funcop_1 :::".-->"::: ) (Set (Var "x"))) ($#r1_hidden :::"="::: ) (Set ($#k6_partfun1 :::"id"::: ) (Set ($#k1_tarski :::"{"::: ) (Set (Var "x")) ($#k1_tarski :::"}"::: ) )))) ; theorem :: FUNCT_4:97 (Bool "for" (Set (Var "f")) "," (Set (Var "g")) "being" ($#m1_hidden :::"Function":::) "st" (Bool (Bool (Set (Var "f")) ($#r1_tarski :::"c="::: ) (Set (Var "g")))) "holds" (Bool (Set (Set (Var "f")) ($#k1_funct_4 :::"+*"::: ) (Set (Var "g"))) ($#r1_hidden :::"="::: ) (Set (Var "g")))) ; theorem :: FUNCT_4:98 (Bool "for" (Set (Var "f")) "," (Set (Var "g")) "being" ($#m1_hidden :::"Function":::) "st" (Bool (Bool (Set (Var "f")) ($#r1_tarski :::"c="::: ) (Set (Var "g")))) "holds" (Bool (Set (Set (Var "g")) ($#k1_funct_4 :::"+*"::: ) (Set (Var "f"))) ($#r1_hidden :::"="::: ) (Set (Var "g")))) ; begin definitionlet "f" be ($#m1_hidden :::"Function":::); let "x", "y" be ($#m1_hidden :::"set"::: ) ; func "f" :::"+~"::: "(" "x" "," "y" ")" -> ($#m1_hidden :::"set"::: ) equals :: FUNCT_4:def 5 (Set "f" ($#k1_funct_4 :::"+*"::: ) (Set "(" (Set "(" "x" ($#k16_funcop_1 :::".-->"::: ) "y" ")" ) ($#k3_relat_1 :::"*"::: ) "f" ")" )); end; :: deftheorem defines :::"+~"::: FUNCT_4:def 5 : (Bool "for" (Set (Var "f")) "being" ($#m1_hidden :::"Function":::) (Bool "for" (Set (Var "x")) "," (Set (Var "y")) "being" ($#m1_hidden :::"set"::: ) "holds" (Bool (Set (Set (Var "f")) ($#k6_funct_4 :::"+~"::: ) "(" (Set (Var "x")) "," (Set (Var "y")) ")" ) ($#r1_hidden :::"="::: ) (Set (Set (Var "f")) ($#k1_funct_4 :::"+*"::: ) (Set "(" (Set "(" (Set (Var "x")) ($#k16_funcop_1 :::".-->"::: ) (Set (Var "y")) ")" ) ($#k3_relat_1 :::"*"::: ) (Set (Var "f")) ")" ))))); registrationlet "f" be ($#m1_hidden :::"Function":::); let "x", "y" be ($#m1_hidden :::"set"::: ) ; cluster (Set "f" ($#k6_funct_4 :::"+~"::: ) "(" "x" "," "y" ")" ) -> ($#v1_relat_1 :::"Relation-like"::: ) ($#v1_funct_1 :::"Function-like"::: ) ; end; theorem :: FUNCT_4:99 (Bool "for" (Set (Var "f")) "being" ($#m1_hidden :::"Function":::) (Bool "for" (Set (Var "x")) "," (Set (Var "y")) "being" ($#m1_hidden :::"set"::: ) "holds" (Bool (Set ($#k9_xtuple_0 :::"dom"::: ) (Set "(" (Set (Var "f")) ($#k6_funct_4 :::"+~"::: ) "(" (Set (Var "x")) "," (Set (Var "y")) ")" ")" )) ($#r1_hidden :::"="::: ) (Set ($#k9_xtuple_0 :::"dom"::: ) (Set (Var "f")))))) ; theorem :: FUNCT_4:100 (Bool "for" (Set (Var "f")) "being" ($#m1_hidden :::"Function":::) (Bool "for" (Set (Var "x")) "," (Set (Var "y")) "being" ($#m1_hidden :::"set"::: ) "st" (Bool (Bool (Set (Var "x")) ($#r1_hidden :::"<>"::: ) (Set (Var "y")))) "holds" (Bool "not" (Bool (Set (Var "x")) ($#r2_hidden :::"in"::: ) (Set ($#k10_xtuple_0 :::"rng"::: ) (Set "(" (Set (Var "f")) ($#k6_funct_4 :::"+~"::: ) "(" (Set (Var "x")) "," (Set (Var "y")) ")" ")" )))))) ; theorem :: FUNCT_4:101 (Bool "for" (Set (Var "f")) "being" ($#m1_hidden :::"Function":::) (Bool "for" (Set (Var "x")) "," (Set (Var "y")) "being" ($#m1_hidden :::"set"::: ) "st" (Bool (Bool (Set (Var "x")) ($#r2_hidden :::"in"::: ) (Set ($#k10_xtuple_0 :::"rng"::: ) (Set (Var "f"))))) "holds" (Bool (Set (Var "y")) ($#r2_hidden :::"in"::: ) (Set ($#k10_xtuple_0 :::"rng"::: ) (Set "(" (Set (Var "f")) ($#k6_funct_4 :::"+~"::: ) "(" (Set (Var "x")) "," (Set (Var "y")) ")" ")" ))))) ; theorem :: FUNCT_4:102 (Bool "for" (Set (Var "f")) "being" ($#m1_hidden :::"Function":::) (Bool "for" (Set (Var "x")) "being" ($#m1_hidden :::"set"::: ) "holds" (Bool (Set (Set (Var "f")) ($#k6_funct_4 :::"+~"::: ) "(" (Set (Var "x")) "," (Set (Var "x")) ")" ) ($#r1_hidden :::"="::: ) (Set (Var "f"))))) ; theorem :: FUNCT_4:103 (Bool "for" (Set (Var "f")) "being" ($#m1_hidden :::"Function":::) (Bool "for" (Set (Var "x")) "," (Set (Var "y")) "being" ($#m1_hidden :::"set"::: ) "st" (Bool (Bool (Bool "not" (Set (Var "x")) ($#r2_hidden :::"in"::: ) (Set ($#k10_xtuple_0 :::"rng"::: ) (Set (Var "f")))))) "holds" (Bool (Set (Set (Var "f")) ($#k6_funct_4 :::"+~"::: ) "(" (Set (Var "x")) "," (Set (Var "y")) ")" ) ($#r1_hidden :::"="::: ) (Set (Var "f"))))) ; theorem :: FUNCT_4:104 (Bool "for" (Set (Var "f")) "being" ($#m1_hidden :::"Function":::) (Bool "for" (Set (Var "x")) "," (Set (Var "y")) "being" ($#m1_hidden :::"set"::: ) "holds" (Bool (Set ($#k10_xtuple_0 :::"rng"::: ) (Set "(" (Set (Var "f")) ($#k6_funct_4 :::"+~"::: ) "(" (Set (Var "x")) "," (Set (Var "y")) ")" ")" )) ($#r1_tarski :::"c="::: ) (Set (Set "(" (Set "(" ($#k10_xtuple_0 :::"rng"::: ) (Set (Var "f")) ")" ) ($#k6_subset_1 :::"\"::: ) (Set ($#k1_tarski :::"{"::: ) (Set (Var "x")) ($#k1_tarski :::"}"::: ) ) ")" ) ($#k2_xboole_0 :::"\/"::: ) (Set ($#k1_tarski :::"{"::: ) (Set (Var "y")) ($#k1_tarski :::"}"::: ) ))))) ; theorem :: FUNCT_4:105 (Bool "for" (Set (Var "z")) "being" ($#m1_hidden :::"set"::: ) (Bool "for" (Set (Var "f")) "being" ($#m1_hidden :::"Function":::) (Bool "for" (Set (Var "x")) "," (Set (Var "y")) "being" ($#m1_hidden :::"set"::: ) "st" (Bool (Bool (Set (Set (Var "f")) ($#k1_funct_1 :::"."::: ) (Set (Var "z"))) ($#r1_hidden :::"<>"::: ) (Set (Var "x")))) "holds" (Bool (Set (Set "(" (Set (Var "f")) ($#k6_funct_4 :::"+~"::: ) "(" (Set (Var "x")) "," (Set (Var "y")) ")" ")" ) ($#k1_funct_1 :::"."::: ) (Set (Var "z"))) ($#r1_hidden :::"="::: ) (Set (Set (Var "f")) ($#k1_funct_1 :::"."::: ) (Set (Var "z"))))))) ; theorem :: FUNCT_4:106 (Bool "for" (Set (Var "z")) "being" ($#m1_hidden :::"set"::: ) (Bool "for" (Set (Var "f")) "being" ($#m1_hidden :::"Function":::) (Bool "for" (Set (Var "x")) "," (Set (Var "y")) "being" ($#m1_hidden :::"set"::: ) "st" (Bool (Bool (Set (Var "z")) ($#r2_hidden :::"in"::: ) (Set ($#k9_xtuple_0 :::"dom"::: ) (Set (Var "f")))) & (Bool (Set (Set (Var "f")) ($#k1_funct_1 :::"."::: ) (Set (Var "z"))) ($#r1_hidden :::"="::: ) (Set (Var "x")))) "holds" (Bool (Set (Set "(" (Set (Var "f")) ($#k6_funct_4 :::"+~"::: ) "(" (Set (Var "x")) "," (Set (Var "y")) ")" ")" ) ($#k1_funct_1 :::"."::: ) (Set (Var "z"))) ($#r1_hidden :::"="::: ) (Set (Var "y")))))) ; theorem :: FUNCT_4:107 (Bool "for" (Set (Var "f")) "being" ($#m1_hidden :::"Function":::) (Bool "for" (Set (Var "x")) "," (Set (Var "y")) "being" ($#m1_hidden :::"set"::: ) "st" (Bool (Bool (Bool "not" (Set (Var "x")) ($#r2_hidden :::"in"::: ) (Set ($#k9_xtuple_0 :::"dom"::: ) (Set (Var "f")))))) "holds" (Bool (Set (Var "f")) ($#r1_tarski :::"c="::: ) (Set (Set (Var "f")) ($#k1_funct_4 :::"+*"::: ) (Set "(" (Set (Var "x")) ($#k16_funcop_1 :::".-->"::: ) (Set (Var "y")) ")" ))))) ; theorem :: FUNCT_4:108 (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 "x")) "," (Set (Var "y")) "being" ($#m1_hidden :::"set"::: ) "st" (Bool (Bool (Set (Var "x")) ($#r2_hidden :::"in"::: ) (Set (Var "X"))) & (Bool (Set (Var "y")) ($#r2_hidden :::"in"::: ) (Set (Var "Y")))) "holds" (Bool (Set (Set (Var "f")) ($#k1_funct_4 :::"+*"::: ) (Set "(" (Set (Var "x")) ($#k16_funcop_1 :::".-->"::: ) (Set (Var "y")) ")" )) "is" ($#m1_subset_1 :::"PartFunc":::) "of" (Set (Var "X")) "," (Set (Var "Y")))))) ; registrationlet "f" be ($#m1_hidden :::"Function":::); let "g" be ($#~v1_xboole_0 "non" ($#v1_xboole_0 :::"empty"::: ) ) ($#m1_hidden :::"Function":::); cluster (Set "f" ($#k1_funct_4 :::"+*"::: ) "g") -> ($#~v1_xboole_0 "non" ($#v1_xboole_0 :::"empty"::: ) ) ; cluster (Set "g" ($#k1_funct_4 :::"+*"::: ) "f") -> ($#~v1_xboole_0 "non" ($#v1_xboole_0 :::"empty"::: ) ) ; end; registrationlet "f", "g" be ($#v2_relat_1 :::"non-empty"::: ) ($#m1_hidden :::"Function":::); cluster (Set "f" ($#k1_funct_4 :::"+*"::: ) "g") -> ($#v2_relat_1 :::"non-empty"::: ) ; end; definitionlet "X", "Y" be ($#m1_hidden :::"set"::: ) ; let "f", "g" be ($#m1_subset_1 :::"PartFunc":::) "of" (Set (Const "X")) "," (Set (Const "Y")); :: original: :::"+*"::: redefine func "f" :::"+*"::: "g" -> ($#m1_subset_1 :::"PartFunc":::) "of" "X" "," "Y"; end; theorem :: FUNCT_4:109 (Bool "for" (Set (Var "z")) "," (Set (Var "x")) "," (Set (Var "y")) "being" ($#m1_hidden :::"set"::: ) "holds" (Bool (Set ($#k9_xtuple_0 :::"dom"::: ) (Set "(" (Set "(" (Set (Var "x")) ($#k7_funcop_1 :::"-->"::: ) (Set (Var "y")) ")" ) ($#k1_funct_4 :::"+*"::: ) (Set "(" (Set (Var "x")) ($#k16_funcop_1 :::".-->"::: ) (Set (Var "z")) ")" ) ")" )) ($#r1_hidden :::"="::: ) (Set ($#k1_ordinal1 :::"succ"::: ) (Set (Var "x"))))) ; theorem :: FUNCT_4:110 (Bool "for" (Set (Var "z")) "," (Set (Var "x")) "," (Set (Var "y")) "being" ($#m1_hidden :::"set"::: ) "holds" (Bool (Set ($#k9_xtuple_0 :::"dom"::: ) (Set "(" (Set "(" (Set "(" (Set (Var "x")) ($#k7_funcop_1 :::"-->"::: ) (Set (Var "y")) ")" ) ($#k1_funct_4 :::"+*"::: ) (Set "(" (Set (Var "x")) ($#k16_funcop_1 :::".-->"::: ) (Set (Var "z")) ")" ) ")" ) ($#k1_funct_4 :::"+*"::: ) (Set "(" (Set "(" ($#k1_ordinal1 :::"succ"::: ) (Set (Var "x")) ")" ) ($#k16_funcop_1 :::".-->"::: ) (Set (Var "z")) ")" ) ")" )) ($#r1_hidden :::"="::: ) (Set ($#k1_ordinal1 :::"succ"::: ) (Set "(" ($#k1_ordinal1 :::"succ"::: ) (Set (Var "x")) ")" )))) ; registrationlet "f", "g" be ($#v1_funcop_1 :::"Function-yielding"::: ) ($#m1_hidden :::"Function":::); cluster (Set "f" ($#k1_funct_4 :::"+*"::: ) "g") -> ($#v1_funcop_1 :::"Function-yielding"::: ) ; end; registrationlet "I" be ($#m1_hidden :::"set"::: ) ; let "f", "g" be (Set (Const "I")) ($#v4_relat_1 :::"-defined"::: ) ($#m1_hidden :::"Function":::); cluster (Set "f" ($#k1_funct_4 :::"+*"::: ) "g") -> "I" ($#v4_relat_1 :::"-defined"::: ) ; end; registrationlet "I" be ($#m1_hidden :::"set"::: ) ; let "f" be (Set (Const "I")) ($#v4_relat_1 :::"-defined"::: ) ($#v1_partfun1 :::"total"::: ) ($#m1_hidden :::"Function":::); let "g" be (Set (Const "I")) ($#v4_relat_1 :::"-defined"::: ) ($#m1_hidden :::"Function":::); cluster (Set "f" ($#k1_funct_4 :::"+*"::: ) "g") -> "I" ($#v4_relat_1 :::"-defined"::: ) ($#v1_partfun1 :::"total"::: ) for"I" ($#v4_relat_1 :::"-defined"::: ) ($#m1_hidden :::"Function":::); cluster (Set "g" ($#k1_funct_4 :::"+*"::: ) "f") -> "I" ($#v4_relat_1 :::"-defined"::: ) ($#v1_partfun1 :::"total"::: ) for"I" ($#v4_relat_1 :::"-defined"::: ) ($#m1_hidden :::"Function":::); end; registrationlet "I" be ($#m1_hidden :::"set"::: ) ; let "g", "h" be (Set (Const "I")) ($#v5_relat_1 :::"-valued"::: ) ($#m1_hidden :::"Function":::); cluster (Set "g" ($#k1_funct_4 :::"+*"::: ) "h") -> "I" ($#v5_relat_1 :::"-valued"::: ) ; end; registrationlet "f" be ($#m1_hidden :::"Function":::); let "g", "h" be (Set (Const "f")) ($#v5_funct_1 :::"-compatible"::: ) ($#m1_hidden :::"Function":::); cluster (Set "g" ($#k1_funct_4 :::"+*"::: ) "h") -> "f" ($#v5_funct_1 :::"-compatible"::: ) ; end; theorem :: FUNCT_4:111 (Bool "for" (Set (Var "f")) "being" ($#m1_hidden :::"Function":::) (Bool "for" (Set (Var "A")) "being" ($#m1_hidden :::"set"::: ) "holds" (Bool (Set (Set "(" (Set (Var "f")) ($#k5_relat_1 :::"|"::: ) (Set (Var "A")) ")" ) ($#k1_funct_4 :::"+*"::: ) (Set (Var "f"))) ($#r1_hidden :::"="::: ) (Set (Var "f"))))) ; theorem :: FUNCT_4:112 (Bool "for" (Set (Var "x")) "," (Set (Var "y")) "being" ($#m1_hidden :::"set"::: ) (Bool "for" (Set (Var "R")) "being" ($#m1_hidden :::"Relation":::) "st" (Bool (Bool (Set ($#k9_xtuple_0 :::"dom"::: ) (Set (Var "R"))) ($#r1_hidden :::"="::: ) (Set ($#k1_tarski :::"{"::: ) (Set (Var "x")) ($#k1_tarski :::"}"::: ) )) & (Bool (Set ($#k10_xtuple_0 :::"rng"::: ) (Set (Var "R"))) ($#r1_hidden :::"="::: ) (Set ($#k1_tarski :::"{"::: ) (Set (Var "y")) ($#k1_tarski :::"}"::: ) ))) "holds" (Bool (Set (Var "R")) ($#r1_hidden :::"="::: ) (Set (Set (Var "x")) ($#k16_funcop_1 :::".-->"::: ) (Set (Var "y")))))) ; theorem :: FUNCT_4:113 (Bool "for" (Set (Var "f")) "being" ($#m1_hidden :::"Function":::) (Bool "for" (Set (Var "x")) "," (Set (Var "y")) "being" ($#m1_hidden :::"set"::: ) "holds" (Bool (Set (Set "(" (Set (Var "f")) ($#k1_funct_4 :::"+*"::: ) (Set "(" (Set (Var "x")) ($#k16_funcop_1 :::".-->"::: ) (Set (Var "y")) ")" ) ")" ) ($#k1_funct_1 :::"."::: ) (Set (Var "x"))) ($#r1_hidden :::"="::: ) (Set (Var "y"))))) ; theorem :: FUNCT_4:114 (Bool "for" (Set (Var "z1")) "," (Set (Var "z2")) "being" ($#m1_hidden :::"set"::: ) (Bool "for" (Set (Var "f")) "being" ($#m1_hidden :::"Function":::) (Bool "for" (Set (Var "x")) "being" ($#m1_hidden :::"set"::: ) "holds" (Bool (Set (Set "(" (Set (Var "f")) ($#k1_funct_4 :::"+*"::: ) (Set "(" (Set (Var "x")) ($#k16_funcop_1 :::".-->"::: ) (Set (Var "z1")) ")" ) ")" ) ($#k1_funct_4 :::"+*"::: ) (Set "(" (Set (Var "x")) ($#k16_funcop_1 :::".-->"::: ) (Set (Var "z2")) ")" )) ($#r1_hidden :::"="::: ) (Set (Set (Var "f")) ($#k1_funct_4 :::"+*"::: ) (Set "(" (Set (Var "x")) ($#k16_funcop_1 :::".-->"::: ) (Set (Var "z2")) ")" )))))) ; registrationlet "A" be ($#~v1_xboole_0 "non" ($#v1_xboole_0 :::"empty"::: ) ) ($#m1_hidden :::"set"::: ) ; let "a", "b" be ($#m1_subset_1 :::"Element"::: ) "of" (Set (Const "A")); let "x", "y" be ($#m1_hidden :::"set"::: ) ; cluster (Set "(" "a" "," "b" ")" ($#k4_funct_4 :::"-->"::: ) "(" "x" "," "y" ")" ) -> "A" ($#v4_relat_1 :::"-defined"::: ) ; end; theorem :: FUNCT_4:115 (Bool "for" (Set (Var "g")) "," (Set (Var "h")) "," (Set (Var "f")) "being" ($#m1_hidden :::"Function":::) "st" (Bool (Bool (Set ($#k9_xtuple_0 :::"dom"::: ) (Set (Var "g"))) ($#r1_xboole_0 :::"misses"::: ) (Set ($#k9_xtuple_0 :::"dom"::: ) (Set (Var "h"))))) "holds" (Bool (Set (Set "(" (Set "(" (Set (Var "f")) ($#k1_funct_4 :::"+*"::: ) (Set (Var "g")) ")" ) ($#k1_funct_4 :::"+*"::: ) (Set (Var "h")) ")" ) ($#k1_funct_4 :::"+*"::: ) (Set (Var "g"))) ($#r1_hidden :::"="::: ) (Set (Set "(" (Set (Var "f")) ($#k1_funct_4 :::"+*"::: ) (Set (Var "g")) ")" ) ($#k1_funct_4 :::"+*"::: ) (Set (Var "h"))))) ; theorem :: FUNCT_4:116 (Bool "for" (Set (Var "f")) "," (Set (Var "h")) "," (Set (Var "g")) "being" ($#m1_hidden :::"Function":::) "st" (Bool (Bool (Set ($#k9_xtuple_0 :::"dom"::: ) (Set (Var "f"))) ($#r1_xboole_0 :::"misses"::: ) (Set ($#k9_xtuple_0 :::"dom"::: ) (Set (Var "h")))) & (Bool (Set (Var "f")) ($#r1_tarski :::"c="::: ) (Set (Set (Var "g")) ($#k1_funct_4 :::"+*"::: ) (Set (Var "h"))))) "holds" (Bool (Set (Var "f")) ($#r1_tarski :::"c="::: ) (Set (Var "g")))) ; theorem :: FUNCT_4:117 (Bool "for" (Set (Var "f")) "," (Set (Var "h")) "," (Set (Var "g")) "being" ($#m1_hidden :::"Function":::) "st" (Bool (Bool (Set ($#k9_xtuple_0 :::"dom"::: ) (Set (Var "f"))) ($#r1_xboole_0 :::"misses"::: ) (Set ($#k9_xtuple_0 :::"dom"::: ) (Set (Var "h")))) & (Bool (Set (Var "f")) ($#r1_tarski :::"c="::: ) (Set (Var "g")))) "holds" (Bool (Set (Var "f")) ($#r1_tarski :::"c="::: ) (Set (Set (Var "g")) ($#k1_funct_4 :::"+*"::: ) (Set (Var "h"))))) ; theorem :: FUNCT_4:118 (Bool "for" (Set (Var "g")) "," (Set (Var "h")) "," (Set (Var "f")) "being" ($#m1_hidden :::"Function":::) "st" (Bool (Bool (Set ($#k9_xtuple_0 :::"dom"::: ) (Set (Var "g"))) ($#r1_xboole_0 :::"misses"::: ) (Set ($#k9_xtuple_0 :::"dom"::: ) (Set (Var "h"))))) "holds" (Bool (Set (Set "(" (Set (Var "f")) ($#k1_funct_4 :::"+*"::: ) (Set (Var "g")) ")" ) ($#k1_funct_4 :::"+*"::: ) (Set (Var "h"))) ($#r1_hidden :::"="::: ) (Set (Set "(" (Set (Var "f")) ($#k1_funct_4 :::"+*"::: ) (Set (Var "h")) ")" ) ($#k1_funct_4 :::"+*"::: ) (Set (Var "g"))))) ; theorem :: FUNCT_4:119 (Bool "for" (Set (Var "f")) "," (Set (Var "g")) "being" ($#m1_hidden :::"Function":::) "st" (Bool (Bool (Set ($#k9_xtuple_0 :::"dom"::: ) (Set (Var "f"))) ($#r1_xboole_0 :::"misses"::: ) (Set ($#k9_xtuple_0 :::"dom"::: ) (Set (Var "g"))))) "holds" (Bool (Set (Set "(" (Set (Var "f")) ($#k1_funct_4 :::"+*"::: ) (Set (Var "g")) ")" ) ($#k6_subset_1 :::"\"::: ) (Set (Var "g"))) ($#r1_hidden :::"="::: ) (Set (Var "f")))) ; theorem :: FUNCT_4:120 (Bool "for" (Set (Var "f")) "," (Set (Var "g")) "being" ($#m1_hidden :::"Function":::) "st" (Bool (Bool (Set ($#k9_xtuple_0 :::"dom"::: ) (Set (Var "f"))) ($#r1_xboole_0 :::"misses"::: ) (Set ($#k9_xtuple_0 :::"dom"::: ) (Set (Var "g"))))) "holds" (Bool (Set (Set (Var "f")) ($#k6_subset_1 :::"\"::: ) (Set (Var "g"))) ($#r1_hidden :::"="::: ) (Set (Var "f")))) ; theorem :: FUNCT_4:121 (Bool "for" (Set (Var "g")) "," (Set (Var "h")) "," (Set (Var "f")) "being" ($#m1_hidden :::"Function":::) "st" (Bool (Bool (Set ($#k9_xtuple_0 :::"dom"::: ) (Set (Var "g"))) ($#r1_xboole_0 :::"misses"::: ) (Set ($#k9_xtuple_0 :::"dom"::: ) (Set (Var "h"))))) "holds" (Bool (Set (Set "(" (Set (Var "f")) ($#k6_subset_1 :::"\"::: ) (Set (Var "g")) ")" ) ($#k1_funct_4 :::"+*"::: ) (Set (Var "h"))) ($#r1_hidden :::"="::: ) (Set (Set "(" (Set (Var "f")) ($#k1_funct_4 :::"+*"::: ) (Set (Var "h")) ")" ) ($#k6_subset_1 :::"\"::: ) (Set (Var "g"))))) ; theorem :: FUNCT_4:122 (Bool "for" (Set (Var "f1")) "," (Set (Var "f2")) "," (Set (Var "g1")) "," (Set (Var "g2")) "being" ($#m1_hidden :::"Function":::) "st" (Bool (Bool (Set (Var "f1")) ($#r1_tarski :::"c="::: ) (Set (Var "g1"))) & (Bool (Set (Var "f2")) ($#r1_tarski :::"c="::: ) (Set (Var "g2"))) & (Bool (Set ($#k9_xtuple_0 :::"dom"::: ) (Set (Var "f1"))) ($#r1_xboole_0 :::"misses"::: ) (Set ($#k9_xtuple_0 :::"dom"::: ) (Set (Var "g2"))))) "holds" (Bool (Set (Set (Var "f1")) ($#k1_funct_4 :::"+*"::: ) (Set (Var "f2"))) ($#r1_tarski :::"c="::: ) (Set (Set (Var "g1")) ($#k1_funct_4 :::"+*"::: ) (Set (Var "g2"))))) ; theorem :: FUNCT_4:123 (Bool "for" (Set (Var "f")) "," (Set (Var "g")) "," (Set (Var "h")) "being" ($#m1_hidden :::"Function":::) "st" (Bool (Bool (Set (Var "f")) ($#r1_tarski :::"c="::: ) (Set (Var "g")))) "holds" (Bool (Set (Set (Var "f")) ($#k1_funct_4 :::"+*"::: ) (Set (Var "h"))) ($#r1_tarski :::"c="::: ) (Set (Set (Var "g")) ($#k1_funct_4 :::"+*"::: ) (Set (Var "h"))))) ; theorem :: FUNCT_4:124 (Bool "for" (Set (Var "f")) "," (Set (Var "g")) "," (Set (Var "h")) "being" ($#m1_hidden :::"Function":::) "st" (Bool (Bool (Set (Var "f")) ($#r1_tarski :::"c="::: ) (Set (Var "g"))) & (Bool (Set ($#k9_xtuple_0 :::"dom"::: ) (Set (Var "f"))) ($#r1_xboole_0 :::"misses"::: ) (Set ($#k9_xtuple_0 :::"dom"::: ) (Set (Var "h"))))) "holds" (Bool (Set (Var "f")) ($#r1_tarski :::"c="::: ) (Set (Set (Var "g")) ($#k1_funct_4 :::"+*"::: ) (Set (Var "h"))))) ; registrationlet "x", "y" be ($#m1_hidden :::"set"::: ) ; cluster (Set "x" ($#k16_funcop_1 :::".-->"::: ) "y") -> ($#v1_zfmisc_1 :::"trivial"::: ) ; end; theorem :: FUNCT_4:125 (Bool "for" (Set (Var "f")) "," (Set (Var "g")) "," (Set (Var "h")) "being" ($#m1_hidden :::"Function":::) "st" (Bool (Bool (Set (Var "f")) ($#r1_partfun1 :::"tolerates"::: ) (Set (Var "g"))) & (Bool (Set (Var "g")) ($#r1_partfun1 :::"tolerates"::: ) (Set (Var "h"))) & (Bool (Set (Var "h")) ($#r1_partfun1 :::"tolerates"::: ) (Set (Var "f")))) "holds" (Bool (Set (Set (Var "f")) ($#k1_funct_4 :::"+*"::: ) (Set (Var "g"))) ($#r1_partfun1 :::"tolerates"::: ) (Set (Var "h")))) ;