:: FUNCT_6 semantic presentation begin theorem :: FUNCT_6:1 (Bool "for" (Set (Var "f")) "being" ($#m1_hidden :::"Function":::) "holds" (Bool (Set ($#k4_card_3 :::"product"::: ) (Set (Var "f"))) ($#r1_tarski :::"c="::: ) (Set ($#k1_funct_2 :::"Funcs"::: ) "(" (Set "(" ($#k9_xtuple_0 :::"dom"::: ) (Set (Var "f")) ")" ) "," (Set "(" ($#k3_card_3 :::"Union"::: ) (Set (Var "f")) ")" ) ")" ))) ; begin theorem :: FUNCT_6:2 (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 "(" ($#k2_funct_4 :::"~"::: ) (Set (Var "f")) ")" )))) "holds" (Bool "ex" (Set (Var "y")) "," (Set (Var "z")) "being" ($#m1_hidden :::"set"::: ) "st" (Bool (Set (Var "x")) ($#r1_hidden :::"="::: ) (Set ($#k4_tarski :::"["::: ) (Set (Var "y")) "," (Set (Var "z")) ($#k4_tarski :::"]"::: ) ))))) ; theorem :: FUNCT_6:3 (Bool "for" (Set (Var "X")) "," (Set (Var "Y")) "," (Set (Var "z")) "being" ($#m1_hidden :::"set"::: ) "holds" (Bool (Set ($#k2_funct_4 :::"~"::: ) (Set "(" (Set ($#k2_zfmisc_1 :::"[:"::: ) (Set (Var "X")) "," (Set (Var "Y")) ($#k2_zfmisc_1 :::":]"::: ) ) ($#k7_funcop_1 :::"-->"::: ) (Set (Var "z")) ")" )) ($#r1_hidden :::"="::: ) (Set (Set ($#k2_zfmisc_1 :::"[:"::: ) (Set (Var "Y")) "," (Set (Var "X")) ($#k2_zfmisc_1 :::":]"::: ) ) ($#k7_funcop_1 :::"-->"::: ) (Set (Var "z"))))) ; theorem :: FUNCT_6:4 (Bool "for" (Set (Var "f")) "being" ($#m1_hidden :::"Function":::) "holds" (Bool "(" (Bool (Set ($#k1_funct_5 :::"curry"::: ) (Set (Var "f"))) ($#r1_hidden :::"="::: ) (Set ($#k3_funct_5 :::"curry'"::: ) (Set "(" ($#k2_funct_4 :::"~"::: ) (Set (Var "f")) ")" ))) & (Bool (Set ($#k2_funct_5 :::"uncurry"::: ) (Set (Var "f"))) ($#r1_hidden :::"="::: ) (Set ($#k2_funct_4 :::"~"::: ) (Set "(" ($#k4_funct_5 :::"uncurry'"::: ) (Set (Var "f")) ")" ))) ")" )) ; theorem :: FUNCT_6:5 (Bool "for" (Set (Var "X")) "," (Set (Var "Y")) "," (Set (Var "z")) "being" ($#m1_hidden :::"set"::: ) "st" (Bool (Bool (Set ($#k2_zfmisc_1 :::"[:"::: ) (Set (Var "X")) "," (Set (Var "Y")) ($#k2_zfmisc_1 :::":]"::: ) ) ($#r1_hidden :::"<>"::: ) (Set ($#k1_xboole_0 :::"{}"::: ) ))) "holds" (Bool "(" (Bool (Set ($#k1_funct_5 :::"curry"::: ) (Set "(" (Set ($#k2_zfmisc_1 :::"[:"::: ) (Set (Var "X")) "," (Set (Var "Y")) ($#k2_zfmisc_1 :::":]"::: ) ) ($#k7_funcop_1 :::"-->"::: ) (Set (Var "z")) ")" )) ($#r1_hidden :::"="::: ) (Set (Set (Var "X")) ($#k7_funcop_1 :::"-->"::: ) (Set "(" (Set (Var "Y")) ($#k7_funcop_1 :::"-->"::: ) (Set (Var "z")) ")" ))) & (Bool (Set ($#k3_funct_5 :::"curry'"::: ) (Set "(" (Set ($#k2_zfmisc_1 :::"[:"::: ) (Set (Var "X")) "," (Set (Var "Y")) ($#k2_zfmisc_1 :::":]"::: ) ) ($#k7_funcop_1 :::"-->"::: ) (Set (Var "z")) ")" )) ($#r1_hidden :::"="::: ) (Set (Set (Var "Y")) ($#k7_funcop_1 :::"-->"::: ) (Set "(" (Set (Var "X")) ($#k7_funcop_1 :::"-->"::: ) (Set (Var "z")) ")" ))) ")" )) ; theorem :: FUNCT_6:6 (Bool "for" (Set (Var "X")) "," (Set (Var "Y")) "," (Set (Var "z")) "being" ($#m1_hidden :::"set"::: ) "holds" (Bool "(" (Bool (Set ($#k2_funct_5 :::"uncurry"::: ) (Set "(" (Set (Var "X")) ($#k7_funcop_1 :::"-->"::: ) (Set "(" (Set (Var "Y")) ($#k7_funcop_1 :::"-->"::: ) (Set (Var "z")) ")" ) ")" )) ($#r1_hidden :::"="::: ) (Set (Set ($#k2_zfmisc_1 :::"[:"::: ) (Set (Var "X")) "," (Set (Var "Y")) ($#k2_zfmisc_1 :::":]"::: ) ) ($#k7_funcop_1 :::"-->"::: ) (Set (Var "z")))) & (Bool (Set ($#k4_funct_5 :::"uncurry'"::: ) (Set "(" (Set (Var "X")) ($#k7_funcop_1 :::"-->"::: ) (Set "(" (Set (Var "Y")) ($#k7_funcop_1 :::"-->"::: ) (Set (Var "z")) ")" ) ")" )) ($#r1_hidden :::"="::: ) (Set (Set ($#k2_zfmisc_1 :::"[:"::: ) (Set (Var "Y")) "," (Set (Var "X")) ($#k2_zfmisc_1 :::":]"::: ) ) ($#k7_funcop_1 :::"-->"::: ) (Set (Var "z")))) ")" )) ; theorem :: FUNCT_6:7 (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 "x")) ($#r2_hidden :::"in"::: ) (Set ($#k9_xtuple_0 :::"dom"::: ) (Set (Var "f")))) & (Bool (Set (Var "g")) ($#r1_hidden :::"="::: ) (Set (Set (Var "f")) ($#k1_funct_1 :::"."::: ) (Set (Var "x"))))) "holds" (Bool "(" (Bool (Set ($#k10_xtuple_0 :::"rng"::: ) (Set (Var "g"))) ($#r1_tarski :::"c="::: ) (Set ($#k10_xtuple_0 :::"rng"::: ) (Set "(" ($#k2_funct_5 :::"uncurry"::: ) (Set (Var "f")) ")" ))) & (Bool (Set ($#k10_xtuple_0 :::"rng"::: ) (Set (Var "g"))) ($#r1_tarski :::"c="::: ) (Set ($#k10_xtuple_0 :::"rng"::: ) (Set "(" ($#k4_funct_5 :::"uncurry'"::: ) (Set (Var "f")) ")" ))) ")" ))) ; theorem :: FUNCT_6:8 (Bool "for" (Set (Var "X")) "being" ($#m1_hidden :::"set"::: ) (Bool "for" (Set (Var "f")) "being" ($#m1_hidden :::"Function":::) "holds" (Bool "(" (Bool (Set ($#k9_xtuple_0 :::"dom"::: ) (Set "(" ($#k2_funct_5 :::"uncurry"::: ) (Set "(" (Set (Var "X")) ($#k7_funcop_1 :::"-->"::: ) (Set (Var "f")) ")" ) ")" )) ($#r1_hidden :::"="::: ) (Set ($#k2_zfmisc_1 :::"[:"::: ) (Set (Var "X")) "," (Set "(" ($#k9_xtuple_0 :::"dom"::: ) (Set (Var "f")) ")" ) ($#k2_zfmisc_1 :::":]"::: ) )) & (Bool (Set ($#k10_xtuple_0 :::"rng"::: ) (Set "(" ($#k2_funct_5 :::"uncurry"::: ) (Set "(" (Set (Var "X")) ($#k7_funcop_1 :::"-->"::: ) (Set (Var "f")) ")" ) ")" )) ($#r1_tarski :::"c="::: ) (Set ($#k10_xtuple_0 :::"rng"::: ) (Set (Var "f")))) & (Bool (Set ($#k9_xtuple_0 :::"dom"::: ) (Set "(" ($#k4_funct_5 :::"uncurry'"::: ) (Set "(" (Set (Var "X")) ($#k7_funcop_1 :::"-->"::: ) (Set (Var "f")) ")" ) ")" )) ($#r1_hidden :::"="::: ) (Set ($#k2_zfmisc_1 :::"[:"::: ) (Set "(" ($#k9_xtuple_0 :::"dom"::: ) (Set (Var "f")) ")" ) "," (Set (Var "X")) ($#k2_zfmisc_1 :::":]"::: ) )) & (Bool (Set ($#k10_xtuple_0 :::"rng"::: ) (Set "(" ($#k4_funct_5 :::"uncurry'"::: ) (Set "(" (Set (Var "X")) ($#k7_funcop_1 :::"-->"::: ) (Set (Var "f")) ")" ) ")" )) ($#r1_tarski :::"c="::: ) (Set ($#k10_xtuple_0 :::"rng"::: ) (Set (Var "f")))) ")" ))) ; theorem :: FUNCT_6:9 (Bool "for" (Set (Var "X")) "being" ($#m1_hidden :::"set"::: ) (Bool "for" (Set (Var "f")) "being" ($#m1_hidden :::"Function":::) "st" (Bool (Bool (Set (Var "X")) ($#r1_hidden :::"<>"::: ) (Set ($#k1_xboole_0 :::"{}"::: ) ))) "holds" (Bool "(" (Bool (Set ($#k10_xtuple_0 :::"rng"::: ) (Set "(" ($#k2_funct_5 :::"uncurry"::: ) (Set "(" (Set (Var "X")) ($#k7_funcop_1 :::"-->"::: ) (Set (Var "f")) ")" ) ")" )) ($#r1_hidden :::"="::: ) (Set ($#k10_xtuple_0 :::"rng"::: ) (Set (Var "f")))) & (Bool (Set ($#k10_xtuple_0 :::"rng"::: ) (Set "(" ($#k4_funct_5 :::"uncurry'"::: ) (Set "(" (Set (Var "X")) ($#k7_funcop_1 :::"-->"::: ) (Set (Var "f")) ")" ) ")" )) ($#r1_hidden :::"="::: ) (Set ($#k10_xtuple_0 :::"rng"::: ) (Set (Var "f")))) ")" ))) ; theorem :: FUNCT_6:10 (Bool "for" (Set (Var "X")) "," (Set (Var "Y")) "," (Set (Var "Z")) "being" ($#m1_hidden :::"set"::: ) (Bool "for" (Set (Var "f")) "being" ($#m1_hidden :::"Function":::) "st" (Bool (Bool (Set ($#k2_zfmisc_1 :::"[:"::: ) (Set (Var "X")) "," (Set (Var "Y")) ($#k2_zfmisc_1 :::":]"::: ) ) ($#r1_hidden :::"<>"::: ) (Set ($#k1_xboole_0 :::"{}"::: ) )) & (Bool (Set (Var "f")) ($#r2_hidden :::"in"::: ) (Set ($#k1_funct_2 :::"Funcs"::: ) "(" (Set ($#k2_zfmisc_1 :::"[:"::: ) (Set (Var "X")) "," (Set (Var "Y")) ($#k2_zfmisc_1 :::":]"::: ) ) "," (Set (Var "Z")) ")" ))) "holds" (Bool "(" (Bool (Set ($#k1_funct_5 :::"curry"::: ) (Set (Var "f"))) ($#r2_hidden :::"in"::: ) (Set ($#k1_funct_2 :::"Funcs"::: ) "(" (Set (Var "X")) "," (Set "(" ($#k1_funct_2 :::"Funcs"::: ) "(" (Set (Var "Y")) "," (Set (Var "Z")) ")" ")" ) ")" )) & (Bool (Set ($#k3_funct_5 :::"curry'"::: ) (Set (Var "f"))) ($#r2_hidden :::"in"::: ) (Set ($#k1_funct_2 :::"Funcs"::: ) "(" (Set (Var "Y")) "," (Set "(" ($#k1_funct_2 :::"Funcs"::: ) "(" (Set (Var "X")) "," (Set (Var "Z")) ")" ")" ) ")" )) ")" ))) ; theorem :: FUNCT_6:11 (Bool "for" (Set (Var "X")) "," (Set (Var "Y")) "," (Set (Var "Z")) "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 "X")) "," (Set "(" ($#k1_funct_2 :::"Funcs"::: ) "(" (Set (Var "Y")) "," (Set (Var "Z")) ")" ")" ) ")" ))) "holds" (Bool "(" (Bool (Set ($#k2_funct_5 :::"uncurry"::: ) (Set (Var "f"))) ($#r2_hidden :::"in"::: ) (Set ($#k1_funct_2 :::"Funcs"::: ) "(" (Set ($#k2_zfmisc_1 :::"[:"::: ) (Set (Var "X")) "," (Set (Var "Y")) ($#k2_zfmisc_1 :::":]"::: ) ) "," (Set (Var "Z")) ")" )) & (Bool (Set ($#k4_funct_5 :::"uncurry'"::: ) (Set (Var "f"))) ($#r2_hidden :::"in"::: ) (Set ($#k1_funct_2 :::"Funcs"::: ) "(" (Set ($#k2_zfmisc_1 :::"[:"::: ) (Set (Var "Y")) "," (Set (Var "X")) ($#k2_zfmisc_1 :::":]"::: ) ) "," (Set (Var "Z")) ")" )) ")" ))) ; theorem :: FUNCT_6:12 (Bool "for" (Set (Var "X")) "," (Set (Var "Y")) "," (Set (Var "Z")) "," (Set (Var "V1")) "," (Set (Var "V2")) "being" ($#m1_hidden :::"set"::: ) (Bool "for" (Set (Var "f")) "being" ($#m1_hidden :::"Function":::) "st" (Bool (Bool "(" (Bool (Set ($#k1_funct_5 :::"curry"::: ) (Set (Var "f"))) ($#r2_hidden :::"in"::: ) (Set ($#k1_funct_2 :::"Funcs"::: ) "(" (Set (Var "X")) "," (Set "(" ($#k1_funct_2 :::"Funcs"::: ) "(" (Set (Var "Y")) "," (Set (Var "Z")) ")" ")" ) ")" )) "or" (Bool (Set ($#k3_funct_5 :::"curry'"::: ) (Set (Var "f"))) ($#r2_hidden :::"in"::: ) (Set ($#k1_funct_2 :::"Funcs"::: ) "(" (Set (Var "Y")) "," (Set "(" ($#k1_funct_2 :::"Funcs"::: ) "(" (Set (Var "X")) "," (Set (Var "Z")) ")" ")" ) ")" )) ")" ) & (Bool (Set ($#k9_xtuple_0 :::"dom"::: ) (Set (Var "f"))) ($#r1_tarski :::"c="::: ) (Set ($#k2_zfmisc_1 :::"[:"::: ) (Set (Var "V1")) "," (Set (Var "V2")) ($#k2_zfmisc_1 :::":]"::: ) ))) "holds" (Bool (Set (Var "f")) ($#r2_hidden :::"in"::: ) (Set ($#k1_funct_2 :::"Funcs"::: ) "(" (Set ($#k2_zfmisc_1 :::"[:"::: ) (Set (Var "X")) "," (Set (Var "Y")) ($#k2_zfmisc_1 :::":]"::: ) ) "," (Set (Var "Z")) ")" )))) ; theorem :: FUNCT_6:13 (Bool "for" (Set (Var "X")) "," (Set (Var "Y")) "," (Set (Var "Z")) "," (Set (Var "V1")) "," (Set (Var "V2")) "being" ($#m1_hidden :::"set"::: ) (Bool "for" (Set (Var "f")) "being" ($#m1_hidden :::"Function":::) "st" (Bool (Bool "(" (Bool (Set ($#k2_funct_5 :::"uncurry"::: ) (Set (Var "f"))) ($#r2_hidden :::"in"::: ) (Set ($#k1_funct_2 :::"Funcs"::: ) "(" (Set ($#k2_zfmisc_1 :::"[:"::: ) (Set (Var "X")) "," (Set (Var "Y")) ($#k2_zfmisc_1 :::":]"::: ) ) "," (Set (Var "Z")) ")" )) "or" (Bool (Set ($#k4_funct_5 :::"uncurry'"::: ) (Set (Var "f"))) ($#r2_hidden :::"in"::: ) (Set ($#k1_funct_2 :::"Funcs"::: ) "(" (Set ($#k2_zfmisc_1 :::"[:"::: ) (Set (Var "Y")) "," (Set (Var "X")) ($#k2_zfmisc_1 :::":]"::: ) ) "," (Set (Var "Z")) ")" )) ")" ) & (Bool (Set ($#k10_xtuple_0 :::"rng"::: ) (Set (Var "f"))) ($#r1_tarski :::"c="::: ) (Set ($#k4_partfun1 :::"PFuncs"::: ) "(" (Set (Var "V1")) "," (Set (Var "V2")) ")" )) & (Bool (Set ($#k9_xtuple_0 :::"dom"::: ) (Set (Var "f"))) ($#r1_hidden :::"="::: ) (Set (Var "X")))) "holds" (Bool (Set (Var "f")) ($#r2_hidden :::"in"::: ) (Set ($#k1_funct_2 :::"Funcs"::: ) "(" (Set (Var "X")) "," (Set "(" ($#k1_funct_2 :::"Funcs"::: ) "(" (Set (Var "Y")) "," (Set (Var "Z")) ")" ")" ) ")" )))) ; theorem :: FUNCT_6:14 (Bool "for" (Set (Var "X")) "," (Set (Var "Y")) "," (Set (Var "Z")) "being" ($#m1_hidden :::"set"::: ) (Bool "for" (Set (Var "f")) "being" ($#m1_hidden :::"Function":::) "st" (Bool (Bool (Set (Var "f")) ($#r2_hidden :::"in"::: ) (Set ($#k4_partfun1 :::"PFuncs"::: ) "(" (Set ($#k2_zfmisc_1 :::"[:"::: ) (Set (Var "X")) "," (Set (Var "Y")) ($#k2_zfmisc_1 :::":]"::: ) ) "," (Set (Var "Z")) ")" ))) "holds" (Bool "(" (Bool (Set ($#k1_funct_5 :::"curry"::: ) (Set (Var "f"))) ($#r2_hidden :::"in"::: ) (Set ($#k4_partfun1 :::"PFuncs"::: ) "(" (Set (Var "X")) "," (Set "(" ($#k4_partfun1 :::"PFuncs"::: ) "(" (Set (Var "Y")) "," (Set (Var "Z")) ")" ")" ) ")" )) & (Bool (Set ($#k3_funct_5 :::"curry'"::: ) (Set (Var "f"))) ($#r2_hidden :::"in"::: ) (Set ($#k4_partfun1 :::"PFuncs"::: ) "(" (Set (Var "Y")) "," (Set "(" ($#k4_partfun1 :::"PFuncs"::: ) "(" (Set (Var "X")) "," (Set (Var "Z")) ")" ")" ) ")" )) ")" ))) ; theorem :: FUNCT_6:15 (Bool "for" (Set (Var "X")) "," (Set (Var "Y")) "," (Set (Var "Z")) "being" ($#m1_hidden :::"set"::: ) (Bool "for" (Set (Var "f")) "being" ($#m1_hidden :::"Function":::) "st" (Bool (Bool (Set (Var "f")) ($#r2_hidden :::"in"::: ) (Set ($#k4_partfun1 :::"PFuncs"::: ) "(" (Set (Var "X")) "," (Set "(" ($#k4_partfun1 :::"PFuncs"::: ) "(" (Set (Var "Y")) "," (Set (Var "Z")) ")" ")" ) ")" ))) "holds" (Bool "(" (Bool (Set ($#k2_funct_5 :::"uncurry"::: ) (Set (Var "f"))) ($#r2_hidden :::"in"::: ) (Set ($#k4_partfun1 :::"PFuncs"::: ) "(" (Set ($#k2_zfmisc_1 :::"[:"::: ) (Set (Var "X")) "," (Set (Var "Y")) ($#k2_zfmisc_1 :::":]"::: ) ) "," (Set (Var "Z")) ")" )) & (Bool (Set ($#k4_funct_5 :::"uncurry'"::: ) (Set (Var "f"))) ($#r2_hidden :::"in"::: ) (Set ($#k4_partfun1 :::"PFuncs"::: ) "(" (Set ($#k2_zfmisc_1 :::"[:"::: ) (Set (Var "Y")) "," (Set (Var "X")) ($#k2_zfmisc_1 :::":]"::: ) ) "," (Set (Var "Z")) ")" )) ")" ))) ; theorem :: FUNCT_6:16 (Bool "for" (Set (Var "X")) "," (Set (Var "Y")) "," (Set (Var "Z")) "," (Set (Var "V1")) "," (Set (Var "V2")) "being" ($#m1_hidden :::"set"::: ) (Bool "for" (Set (Var "f")) "being" ($#m1_hidden :::"Function":::) "st" (Bool (Bool "(" (Bool (Set ($#k1_funct_5 :::"curry"::: ) (Set (Var "f"))) ($#r2_hidden :::"in"::: ) (Set ($#k4_partfun1 :::"PFuncs"::: ) "(" (Set (Var "X")) "," (Set "(" ($#k4_partfun1 :::"PFuncs"::: ) "(" (Set (Var "Y")) "," (Set (Var "Z")) ")" ")" ) ")" )) "or" (Bool (Set ($#k3_funct_5 :::"curry'"::: ) (Set (Var "f"))) ($#r2_hidden :::"in"::: ) (Set ($#k4_partfun1 :::"PFuncs"::: ) "(" (Set (Var "Y")) "," (Set "(" ($#k4_partfun1 :::"PFuncs"::: ) "(" (Set (Var "X")) "," (Set (Var "Z")) ")" ")" ) ")" )) ")" ) & (Bool (Set ($#k9_xtuple_0 :::"dom"::: ) (Set (Var "f"))) ($#r1_tarski :::"c="::: ) (Set ($#k2_zfmisc_1 :::"[:"::: ) (Set (Var "V1")) "," (Set (Var "V2")) ($#k2_zfmisc_1 :::":]"::: ) ))) "holds" (Bool (Set (Var "f")) ($#r2_hidden :::"in"::: ) (Set ($#k4_partfun1 :::"PFuncs"::: ) "(" (Set ($#k2_zfmisc_1 :::"[:"::: ) (Set (Var "X")) "," (Set (Var "Y")) ($#k2_zfmisc_1 :::":]"::: ) ) "," (Set (Var "Z")) ")" )))) ; theorem :: FUNCT_6:17 (Bool "for" (Set (Var "X")) "," (Set (Var "Y")) "," (Set (Var "Z")) "," (Set (Var "V1")) "," (Set (Var "V2")) "being" ($#m1_hidden :::"set"::: ) (Bool "for" (Set (Var "f")) "being" ($#m1_hidden :::"Function":::) "st" (Bool (Bool "(" (Bool (Set ($#k2_funct_5 :::"uncurry"::: ) (Set (Var "f"))) ($#r2_hidden :::"in"::: ) (Set ($#k4_partfun1 :::"PFuncs"::: ) "(" (Set ($#k2_zfmisc_1 :::"[:"::: ) (Set (Var "X")) "," (Set (Var "Y")) ($#k2_zfmisc_1 :::":]"::: ) ) "," (Set (Var "Z")) ")" )) "or" (Bool (Set ($#k4_funct_5 :::"uncurry'"::: ) (Set (Var "f"))) ($#r2_hidden :::"in"::: ) (Set ($#k4_partfun1 :::"PFuncs"::: ) "(" (Set ($#k2_zfmisc_1 :::"[:"::: ) (Set (Var "Y")) "," (Set (Var "X")) ($#k2_zfmisc_1 :::":]"::: ) ) "," (Set (Var "Z")) ")" )) ")" ) & (Bool (Set ($#k10_xtuple_0 :::"rng"::: ) (Set (Var "f"))) ($#r1_tarski :::"c="::: ) (Set ($#k4_partfun1 :::"PFuncs"::: ) "(" (Set (Var "V1")) "," (Set (Var "V2")) ")" )) & (Bool (Set ($#k9_xtuple_0 :::"dom"::: ) (Set (Var "f"))) ($#r1_tarski :::"c="::: ) (Set (Var "X")))) "holds" (Bool (Set (Var "f")) ($#r2_hidden :::"in"::: ) (Set ($#k4_partfun1 :::"PFuncs"::: ) "(" (Set (Var "X")) "," (Set "(" ($#k4_partfun1 :::"PFuncs"::: ) "(" (Set (Var "Y")) "," (Set (Var "Z")) ")" ")" ) ")" )))) ; begin definitionlet "X" be ($#m1_hidden :::"set"::: ) ; func :::"SubFuncs"::: "X" -> ($#m1_hidden :::"set"::: ) means :: FUNCT_6:def 1 (Bool "for" (Set (Var "x")) "being" ($#m1_hidden :::"set"::: ) "holds" (Bool "(" (Bool (Set (Var "x")) ($#r2_hidden :::"in"::: ) it) "iff" (Bool "(" (Bool (Set (Var "x")) ($#r2_hidden :::"in"::: ) "X") & (Bool (Set (Var "x")) "is" ($#m1_hidden :::"Function":::)) ")" ) ")" )); end; :: deftheorem defines :::"SubFuncs"::: FUNCT_6:def 1 : (Bool "for" (Set (Var "X")) "being" ($#m1_hidden :::"set"::: ) (Bool "for" (Set (Var "b2")) "being" ($#m1_hidden :::"set"::: ) "holds" (Bool "(" (Bool (Set (Var "b2")) ($#r1_hidden :::"="::: ) (Set ($#k1_funct_6 :::"SubFuncs"::: ) (Set (Var "X")))) "iff" (Bool "for" (Set (Var "x")) "being" ($#m1_hidden :::"set"::: ) "holds" (Bool "(" (Bool (Set (Var "x")) ($#r2_hidden :::"in"::: ) (Set (Var "b2"))) "iff" (Bool "(" (Bool (Set (Var "x")) ($#r2_hidden :::"in"::: ) (Set (Var "X"))) & (Bool (Set (Var "x")) "is" ($#m1_hidden :::"Function":::)) ")" ) ")" )) ")" ))); theorem :: FUNCT_6:18 (Bool "for" (Set (Var "X")) "being" ($#m1_hidden :::"set"::: ) "holds" (Bool (Set ($#k1_funct_6 :::"SubFuncs"::: ) (Set (Var "X"))) ($#r1_tarski :::"c="::: ) (Set (Var "X")))) ; theorem :: FUNCT_6:19 (Bool "for" (Set (Var "x")) "being" ($#m1_hidden :::"set"::: ) (Bool "for" (Set (Var "f")) "being" ($#m1_hidden :::"Function":::) "holds" (Bool "(" (Bool (Set (Var "x")) ($#r2_hidden :::"in"::: ) (Set (Set (Var "f")) ($#k8_relat_1 :::"""::: ) (Set "(" ($#k1_funct_6 :::"SubFuncs"::: ) (Set "(" ($#k10_xtuple_0 :::"rng"::: ) (Set (Var "f")) ")" ) ")" ))) "iff" (Bool "(" (Bool (Set (Var "x")) ($#r2_hidden :::"in"::: ) (Set ($#k9_xtuple_0 :::"dom"::: ) (Set (Var "f")))) & (Bool (Set (Set (Var "f")) ($#k1_funct_1 :::"."::: ) (Set (Var "x"))) "is" ($#m1_hidden :::"Function":::)) ")" ) ")" ))) ; theorem :: FUNCT_6:20 (Bool "for" (Set (Var "f")) "," (Set (Var "g")) "," (Set (Var "h")) "being" ($#m1_hidden :::"Function":::) "holds" (Bool "(" (Bool (Set ($#k1_funct_6 :::"SubFuncs"::: ) (Set ($#k1_xboole_0 :::"{}"::: ) )) ($#r1_hidden :::"="::: ) (Set ($#k1_xboole_0 :::"{}"::: ) )) & (Bool (Set ($#k1_funct_6 :::"SubFuncs"::: ) (Set ($#k1_tarski :::"{"::: ) (Set (Var "f")) ($#k1_tarski :::"}"::: ) )) ($#r1_hidden :::"="::: ) (Set ($#k1_tarski :::"{"::: ) (Set (Var "f")) ($#k1_tarski :::"}"::: ) )) & (Bool (Set ($#k1_funct_6 :::"SubFuncs"::: ) (Set ($#k2_tarski :::"{"::: ) (Set (Var "f")) "," (Set (Var "g")) ($#k2_tarski :::"}"::: ) )) ($#r1_hidden :::"="::: ) (Set ($#k2_tarski :::"{"::: ) (Set (Var "f")) "," (Set (Var "g")) ($#k2_tarski :::"}"::: ) )) & (Bool (Set ($#k1_funct_6 :::"SubFuncs"::: ) (Set ($#k1_enumset1 :::"{"::: ) (Set (Var "f")) "," (Set (Var "g")) "," (Set (Var "h")) ($#k1_enumset1 :::"}"::: ) )) ($#r1_hidden :::"="::: ) (Set ($#k1_enumset1 :::"{"::: ) (Set (Var "f")) "," (Set (Var "g")) "," (Set (Var "h")) ($#k1_enumset1 :::"}"::: ) )) ")" )) ; theorem :: FUNCT_6:21 (Bool "for" (Set (Var "Y")) "," (Set (Var "X")) "being" ($#m1_hidden :::"set"::: ) "st" (Bool (Bool (Set (Var "Y")) ($#r1_tarski :::"c="::: ) (Set ($#k1_funct_6 :::"SubFuncs"::: ) (Set (Var "X"))))) "holds" (Bool (Set ($#k1_funct_6 :::"SubFuncs"::: ) (Set (Var "Y"))) ($#r1_hidden :::"="::: ) (Set (Var "Y")))) ; definitionlet "f" be ($#m1_hidden :::"Function":::); func :::"doms"::: "f" -> ($#m1_hidden :::"Function":::) means :: FUNCT_6:def 2 (Bool "(" (Bool (Set ($#k9_xtuple_0 :::"dom"::: ) it) ($#r1_hidden :::"="::: ) (Set "f" ($#k8_relat_1 :::"""::: ) (Set "(" ($#k1_funct_6 :::"SubFuncs"::: ) (Set "(" ($#k10_xtuple_0 :::"rng"::: ) "f" ")" ) ")" ))) & (Bool "(" "for" (Set (Var "x")) "being" ($#m1_hidden :::"set"::: ) "st" (Bool (Bool (Set (Var "x")) ($#r2_hidden :::"in"::: ) (Set "f" ($#k8_relat_1 :::"""::: ) (Set "(" ($#k1_funct_6 :::"SubFuncs"::: ) (Set "(" ($#k10_xtuple_0 :::"rng"::: ) "f" ")" ) ")" )))) "holds" (Bool (Set it ($#k1_funct_1 :::"."::: ) (Set (Var "x"))) ($#r1_hidden :::"="::: ) (Set ($#k9_xtuple_0 :::"proj1"::: ) (Set "(" "f" ($#k1_funct_1 :::"."::: ) (Set (Var "x")) ")" ))) ")" ) ")" ); func :::"rngs"::: "f" -> ($#m1_hidden :::"Function":::) means :: FUNCT_6:def 3 (Bool "(" (Bool (Set ($#k9_xtuple_0 :::"dom"::: ) it) ($#r1_hidden :::"="::: ) (Set "f" ($#k8_relat_1 :::"""::: ) (Set "(" ($#k1_funct_6 :::"SubFuncs"::: ) (Set "(" ($#k10_xtuple_0 :::"rng"::: ) "f" ")" ) ")" ))) & (Bool "(" "for" (Set (Var "x")) "being" ($#m1_hidden :::"set"::: ) "st" (Bool (Bool (Set (Var "x")) ($#r2_hidden :::"in"::: ) (Set "f" ($#k8_relat_1 :::"""::: ) (Set "(" ($#k1_funct_6 :::"SubFuncs"::: ) (Set "(" ($#k10_xtuple_0 :::"rng"::: ) "f" ")" ) ")" )))) "holds" (Bool (Set it ($#k1_funct_1 :::"."::: ) (Set (Var "x"))) ($#r1_hidden :::"="::: ) (Set ($#k10_xtuple_0 :::"proj2"::: ) (Set "(" "f" ($#k1_funct_1 :::"."::: ) (Set (Var "x")) ")" ))) ")" ) ")" ); func :::"meet"::: "f" -> ($#m1_hidden :::"set"::: ) equals :: FUNCT_6:def 4 (Set ($#k1_setfam_1 :::"meet"::: ) (Set "(" ($#k10_xtuple_0 :::"rng"::: ) "f" ")" )); end; :: deftheorem defines :::"doms"::: FUNCT_6: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_6 :::"doms"::: ) (Set (Var "f")))) "iff" (Bool "(" (Bool (Set ($#k9_xtuple_0 :::"dom"::: ) (Set (Var "b2"))) ($#r1_hidden :::"="::: ) (Set (Set (Var "f")) ($#k8_relat_1 :::"""::: ) (Set "(" ($#k1_funct_6 :::"SubFuncs"::: ) (Set "(" ($#k10_xtuple_0 :::"rng"::: ) (Set (Var "f")) ")" ) ")" ))) & (Bool "(" "for" (Set (Var "x")) "being" ($#m1_hidden :::"set"::: ) "st" (Bool (Bool (Set (Var "x")) ($#r2_hidden :::"in"::: ) (Set (Set (Var "f")) ($#k8_relat_1 :::"""::: ) (Set "(" ($#k1_funct_6 :::"SubFuncs"::: ) (Set "(" ($#k10_xtuple_0 :::"rng"::: ) (Set (Var "f")) ")" ) ")" )))) "holds" (Bool (Set (Set (Var "b2")) ($#k1_funct_1 :::"."::: ) (Set (Var "x"))) ($#r1_hidden :::"="::: ) (Set ($#k9_xtuple_0 :::"proj1"::: ) (Set "(" (Set (Var "f")) ($#k1_funct_1 :::"."::: ) (Set (Var "x")) ")" ))) ")" ) ")" ) ")" )); :: deftheorem defines :::"rngs"::: FUNCT_6:def 3 : (Bool "for" (Set (Var "f")) "," (Set (Var "b2")) "being" ($#m1_hidden :::"Function":::) "holds" (Bool "(" (Bool (Set (Var "b2")) ($#r1_hidden :::"="::: ) (Set ($#k3_funct_6 :::"rngs"::: ) (Set (Var "f")))) "iff" (Bool "(" (Bool (Set ($#k9_xtuple_0 :::"dom"::: ) (Set (Var "b2"))) ($#r1_hidden :::"="::: ) (Set (Set (Var "f")) ($#k8_relat_1 :::"""::: ) (Set "(" ($#k1_funct_6 :::"SubFuncs"::: ) (Set "(" ($#k10_xtuple_0 :::"rng"::: ) (Set (Var "f")) ")" ) ")" ))) & (Bool "(" "for" (Set (Var "x")) "being" ($#m1_hidden :::"set"::: ) "st" (Bool (Bool (Set (Var "x")) ($#r2_hidden :::"in"::: ) (Set (Set (Var "f")) ($#k8_relat_1 :::"""::: ) (Set "(" ($#k1_funct_6 :::"SubFuncs"::: ) (Set "(" ($#k10_xtuple_0 :::"rng"::: ) (Set (Var "f")) ")" ) ")" )))) "holds" (Bool (Set (Set (Var "b2")) ($#k1_funct_1 :::"."::: ) (Set (Var "x"))) ($#r1_hidden :::"="::: ) (Set ($#k10_xtuple_0 :::"proj2"::: ) (Set "(" (Set (Var "f")) ($#k1_funct_1 :::"."::: ) (Set (Var "x")) ")" ))) ")" ) ")" ) ")" )); :: deftheorem defines :::"meet"::: FUNCT_6:def 4 : (Bool "for" (Set (Var "f")) "being" ($#m1_hidden :::"Function":::) "holds" (Bool (Set ($#k4_funct_6 :::"meet"::: ) (Set (Var "f"))) ($#r1_hidden :::"="::: ) (Set ($#k1_setfam_1 :::"meet"::: ) (Set "(" ($#k10_xtuple_0 :::"rng"::: ) (Set (Var "f")) ")" )))); theorem :: FUNCT_6:22 (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 "x")) ($#r2_hidden :::"in"::: ) (Set ($#k9_xtuple_0 :::"dom"::: ) (Set (Var "f")))) & (Bool (Set (Var "g")) ($#r1_hidden :::"="::: ) (Set (Set (Var "f")) ($#k1_funct_1 :::"."::: ) (Set (Var "x"))))) "holds" (Bool "(" (Bool (Set (Var "x")) ($#r2_hidden :::"in"::: ) (Set ($#k9_xtuple_0 :::"dom"::: ) (Set "(" ($#k2_funct_6 :::"doms"::: ) (Set (Var "f")) ")" ))) & (Bool (Set (Set "(" ($#k2_funct_6 :::"doms"::: ) (Set (Var "f")) ")" ) ($#k1_funct_1 :::"."::: ) (Set (Var "x"))) ($#r1_hidden :::"="::: ) (Set ($#k9_xtuple_0 :::"dom"::: ) (Set (Var "g")))) & (Bool (Set (Var "x")) ($#r2_hidden :::"in"::: ) (Set ($#k9_xtuple_0 :::"dom"::: ) (Set "(" ($#k3_funct_6 :::"rngs"::: ) (Set (Var "f")) ")" ))) & (Bool (Set (Set "(" ($#k3_funct_6 :::"rngs"::: ) (Set (Var "f")) ")" ) ($#k1_funct_1 :::"."::: ) (Set (Var "x"))) ($#r1_hidden :::"="::: ) (Set ($#k10_xtuple_0 :::"rng"::: ) (Set (Var "g")))) ")" ))) ; theorem :: FUNCT_6:23 (Bool "(" (Bool (Set ($#k2_funct_6 :::"doms"::: ) (Set ($#k1_xboole_0 :::"{}"::: ) )) ($#r1_hidden :::"="::: ) (Set ($#k1_xboole_0 :::"{}"::: ) )) & (Bool (Set ($#k3_funct_6 :::"rngs"::: ) (Set ($#k1_xboole_0 :::"{}"::: ) )) ($#r1_hidden :::"="::: ) (Set ($#k1_xboole_0 :::"{}"::: ) )) ")" ) ; theorem :: FUNCT_6:24 (Bool "for" (Set (Var "X")) "being" ($#m1_hidden :::"set"::: ) (Bool "for" (Set (Var "f")) "being" ($#m1_hidden :::"Function":::) "holds" (Bool "(" (Bool (Set ($#k2_funct_6 :::"doms"::: ) (Set "(" (Set (Var "X")) ($#k7_funcop_1 :::"-->"::: ) (Set (Var "f")) ")" )) ($#r1_hidden :::"="::: ) (Set (Set (Var "X")) ($#k7_funcop_1 :::"-->"::: ) (Set "(" ($#k9_xtuple_0 :::"dom"::: ) (Set (Var "f")) ")" ))) & (Bool (Set ($#k3_funct_6 :::"rngs"::: ) (Set "(" (Set (Var "X")) ($#k7_funcop_1 :::"-->"::: ) (Set (Var "f")) ")" )) ($#r1_hidden :::"="::: ) (Set (Set (Var "X")) ($#k7_funcop_1 :::"-->"::: ) (Set "(" ($#k10_xtuple_0 :::"rng"::: ) (Set (Var "f")) ")" ))) ")" ))) ; theorem :: FUNCT_6:25 (Bool "for" (Set (Var "x")) "being" ($#m1_hidden :::"set"::: ) (Bool "for" (Set (Var "f")) "being" ($#m1_hidden :::"Function":::) "st" (Bool (Bool (Set (Var "f")) ($#r1_hidden :::"<>"::: ) (Set ($#k1_xboole_0 :::"{}"::: ) ))) "holds" (Bool "(" (Bool (Set (Var "x")) ($#r2_hidden :::"in"::: ) (Set ($#k4_funct_6 :::"meet"::: ) (Set (Var "f")))) "iff" (Bool "for" (Set (Var "y")) "being" ($#m1_hidden :::"set"::: ) "st" (Bool (Bool (Set (Var "y")) ($#r2_hidden :::"in"::: ) (Set ($#k9_xtuple_0 :::"dom"::: ) (Set (Var "f"))))) "holds" (Bool (Set (Var "x")) ($#r2_hidden :::"in"::: ) (Set (Set (Var "f")) ($#k1_funct_1 :::"."::: ) (Set (Var "y"))))) ")" ))) ; theorem :: FUNCT_6:26 (Bool "for" (Set (Var "Y")) "being" ($#m1_hidden :::"set"::: ) "holds" (Bool "(" (Bool (Set ($#k3_card_3 :::"Union"::: ) (Set "(" (Set ($#k1_xboole_0 :::"{}"::: ) ) ($#k7_funcop_1 :::"-->"::: ) (Set (Var "Y")) ")" )) ($#r1_hidden :::"="::: ) (Set ($#k1_xboole_0 :::"{}"::: ) )) & (Bool (Set ($#k4_funct_6 :::"meet"::: ) (Set "(" (Set ($#k1_xboole_0 :::"{}"::: ) ) ($#k7_funcop_1 :::"-->"::: ) (Set (Var "Y")) ")" )) ($#r1_hidden :::"="::: ) (Set ($#k1_xboole_0 :::"{}"::: ) )) ")" )) ; theorem :: FUNCT_6:27 (Bool "for" (Set (Var "X")) "," (Set (Var "Y")) "being" ($#m1_hidden :::"set"::: ) "st" (Bool (Bool (Set (Var "X")) ($#r1_hidden :::"<>"::: ) (Set ($#k1_xboole_0 :::"{}"::: ) ))) "holds" (Bool "(" (Bool (Set ($#k3_card_3 :::"Union"::: ) (Set "(" (Set (Var "X")) ($#k7_funcop_1 :::"-->"::: ) (Set (Var "Y")) ")" )) ($#r1_hidden :::"="::: ) (Set (Var "Y"))) & (Bool (Set ($#k4_funct_6 :::"meet"::: ) (Set "(" (Set (Var "X")) ($#k7_funcop_1 :::"-->"::: ) (Set (Var "Y")) ")" )) ($#r1_hidden :::"="::: ) (Set (Var "Y"))) ")" )) ; definitionlet "f" be ($#m1_hidden :::"Function":::); let "x", "y" be ($#m1_hidden :::"set"::: ) ; func "f" :::".."::: "(" "x" "," "y" ")" -> ($#m1_hidden :::"set"::: ) equals :: FUNCT_6:def 5 (Set (Set "(" ($#k2_funct_5 :::"uncurry"::: ) "f" ")" ) ($#k1_binop_1 :::"."::: ) "(" "x" "," "y" ")" ); end; :: deftheorem defines :::".."::: FUNCT_6: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")) ($#k5_funct_6 :::".."::: ) "(" (Set (Var "x")) "," (Set (Var "y")) ")" ) ($#r1_hidden :::"="::: ) (Set (Set "(" ($#k2_funct_5 :::"uncurry"::: ) (Set (Var "f")) ")" ) ($#k1_binop_1 :::"."::: ) "(" (Set (Var "x")) "," (Set (Var "y")) ")" )))); theorem :: FUNCT_6:28 (Bool "for" (Set (Var "x")) "," (Set (Var "X")) "," (Set (Var "y")) "being" ($#m1_hidden :::"set"::: ) (Bool "for" (Set (Var "f")) "being" ($#m1_hidden :::"Function":::) "st" (Bool (Bool (Set (Var "x")) ($#r2_hidden :::"in"::: ) (Set (Var "X"))) & (Bool (Set (Var "y")) ($#r2_hidden :::"in"::: ) (Set ($#k9_xtuple_0 :::"dom"::: ) (Set (Var "f"))))) "holds" (Bool (Set (Set "(" (Set (Var "X")) ($#k7_funcop_1 :::"-->"::: ) (Set (Var "f")) ")" ) ($#k5_funct_6 :::".."::: ) "(" (Set (Var "x")) "," (Set (Var "y")) ")" ) ($#r1_hidden :::"="::: ) (Set (Set (Var "f")) ($#k1_funct_1 :::"."::: ) (Set (Var "y")))))) ; begin definitionlet "f" be ($#m1_hidden :::"Function":::); func :::"<:":::"f":::":>"::: -> ($#m1_hidden :::"Function":::) equals :: FUNCT_6:def 6 (Set ($#k1_funct_5 :::"curry"::: ) (Set "(" (Set "(" ($#k4_funct_5 :::"uncurry'"::: ) "f" ")" ) ($#k5_relat_1 :::"|"::: ) (Set ($#k2_zfmisc_1 :::"[:"::: ) (Set "(" ($#k4_funct_6 :::"meet"::: ) (Set "(" ($#k2_funct_6 :::"doms"::: ) "f" ")" ) ")" ) "," (Set "(" ($#k9_xtuple_0 :::"dom"::: ) "f" ")" ) ($#k2_zfmisc_1 :::":]"::: ) ) ")" )); end; :: deftheorem defines :::"<:"::: FUNCT_6:def 6 : (Bool "for" (Set (Var "f")) "being" ($#m1_hidden :::"Function":::) "holds" (Bool (Set ($#k6_funct_6 :::"<:"::: ) (Set (Var "f")) ($#k6_funct_6 :::":>"::: ) ) ($#r1_hidden :::"="::: ) (Set ($#k1_funct_5 :::"curry"::: ) (Set "(" (Set "(" ($#k4_funct_5 :::"uncurry'"::: ) (Set (Var "f")) ")" ) ($#k5_relat_1 :::"|"::: ) (Set ($#k2_zfmisc_1 :::"[:"::: ) (Set "(" ($#k4_funct_6 :::"meet"::: ) (Set "(" ($#k2_funct_6 :::"doms"::: ) (Set (Var "f")) ")" ) ")" ) "," (Set "(" ($#k9_xtuple_0 :::"dom"::: ) (Set (Var "f")) ")" ) ($#k2_zfmisc_1 :::":]"::: ) ) ")" )))); theorem :: FUNCT_6:29 (Bool "for" (Set (Var "f")) "being" ($#m1_hidden :::"Function":::) "holds" (Bool "(" (Bool (Set ($#k9_xtuple_0 :::"dom"::: ) (Set ($#k6_funct_6 :::"<:"::: ) (Set (Var "f")) ($#k6_funct_6 :::":>"::: ) )) ($#r1_hidden :::"="::: ) (Set ($#k4_funct_6 :::"meet"::: ) (Set "(" ($#k2_funct_6 :::"doms"::: ) (Set (Var "f")) ")" ))) & (Bool (Set ($#k10_xtuple_0 :::"rng"::: ) (Set ($#k6_funct_6 :::"<:"::: ) (Set (Var "f")) ($#k6_funct_6 :::":>"::: ) )) ($#r1_tarski :::"c="::: ) (Set ($#k4_card_3 :::"product"::: ) (Set "(" ($#k3_funct_6 :::"rngs"::: ) (Set (Var "f")) ")" ))) ")" )) ; theorem :: FUNCT_6:30 (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 ($#k6_funct_6 :::"<:"::: ) (Set (Var "f")) ($#k6_funct_6 :::":>"::: ) )))) "holds" (Bool (Set (Set ($#k6_funct_6 :::"<:"::: ) (Set (Var "f")) ($#k6_funct_6 :::":>"::: ) ) ($#k1_funct_1 :::"."::: ) (Set (Var "x"))) "is" ($#m1_hidden :::"Function":::)))) ; theorem :: FUNCT_6:31 (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 "x")) ($#r2_hidden :::"in"::: ) (Set ($#k9_xtuple_0 :::"dom"::: ) (Set ($#k6_funct_6 :::"<:"::: ) (Set (Var "f")) ($#k6_funct_6 :::":>"::: ) ))) & (Bool (Set (Var "g")) ($#r1_hidden :::"="::: ) (Set (Set ($#k6_funct_6 :::"<:"::: ) (Set (Var "f")) ($#k6_funct_6 :::":>"::: ) ) ($#k1_funct_1 :::"."::: ) (Set (Var "x"))))) "holds" (Bool "(" (Bool (Set ($#k9_xtuple_0 :::"dom"::: ) (Set (Var "g"))) ($#r1_hidden :::"="::: ) (Set (Set (Var "f")) ($#k8_relat_1 :::"""::: ) (Set "(" ($#k1_funct_6 :::"SubFuncs"::: ) (Set "(" ($#k10_xtuple_0 :::"rng"::: ) (Set (Var "f")) ")" ) ")" ))) & (Bool "(" "for" (Set (Var "y")) "being" ($#m1_hidden :::"set"::: ) "st" (Bool (Bool (Set (Var "y")) ($#r2_hidden :::"in"::: ) (Set ($#k9_xtuple_0 :::"dom"::: ) (Set (Var "g"))))) "holds" (Bool "(" (Bool (Set ($#k4_tarski :::"["::: ) (Set (Var "y")) "," (Set (Var "x")) ($#k4_tarski :::"]"::: ) ) ($#r2_hidden :::"in"::: ) (Set ($#k9_xtuple_0 :::"dom"::: ) (Set "(" ($#k2_funct_5 :::"uncurry"::: ) (Set (Var "f")) ")" ))) & (Bool (Set (Set (Var "g")) ($#k1_funct_1 :::"."::: ) (Set (Var "y"))) ($#r1_hidden :::"="::: ) (Set (Set "(" ($#k2_funct_5 :::"uncurry"::: ) (Set (Var "f")) ")" ) ($#k1_binop_1 :::"."::: ) "(" (Set (Var "y")) "," (Set (Var "x")) ")" )) ")" ) ")" ) ")" ))) ; theorem :: FUNCT_6:32 (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 ($#k6_funct_6 :::"<:"::: ) (Set (Var "f")) ($#k6_funct_6 :::":>"::: ) )))) "holds" (Bool "for" (Set (Var "g")) "being" ($#m1_hidden :::"Function":::) "st" (Bool (Bool (Set (Var "g")) ($#r2_hidden :::"in"::: ) (Set ($#k10_xtuple_0 :::"rng"::: ) (Set (Var "f"))))) "holds" (Bool (Set (Var "x")) ($#r2_hidden :::"in"::: ) (Set ($#k9_xtuple_0 :::"dom"::: ) (Set (Var "g"))))))) ; theorem :: FUNCT_6:33 (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 "g")) ($#r2_hidden :::"in"::: ) (Set ($#k10_xtuple_0 :::"rng"::: ) (Set (Var "f")))) & (Bool "(" "for" (Set (Var "g")) "being" ($#m1_hidden :::"Function":::) "st" (Bool (Bool (Set (Var "g")) ($#r2_hidden :::"in"::: ) (Set ($#k10_xtuple_0 :::"rng"::: ) (Set (Var "f"))))) "holds" (Bool (Set (Var "x")) ($#r2_hidden :::"in"::: ) (Set ($#k9_xtuple_0 :::"dom"::: ) (Set (Var "g")))) ")" )) "holds" (Bool (Set (Var "x")) ($#r2_hidden :::"in"::: ) (Set ($#k9_xtuple_0 :::"dom"::: ) (Set ($#k6_funct_6 :::"<:"::: ) (Set (Var "f")) ($#k6_funct_6 :::":>"::: ) ))))) ; theorem :: FUNCT_6:34 (Bool "for" (Set (Var "x")) "," (Set (Var "y")) "being" ($#m1_hidden :::"set"::: ) (Bool "for" (Set (Var "f")) "," (Set (Var "g")) "," (Set (Var "h")) "being" ($#m1_hidden :::"Function":::) "st" (Bool (Bool (Set (Var "x")) ($#r2_hidden :::"in"::: ) (Set ($#k9_xtuple_0 :::"dom"::: ) (Set (Var "f")))) & (Bool (Set (Var "g")) ($#r1_hidden :::"="::: ) (Set (Set (Var "f")) ($#k1_funct_1 :::"."::: ) (Set (Var "x")))) & (Bool (Set (Var "y")) ($#r2_hidden :::"in"::: ) (Set ($#k9_xtuple_0 :::"dom"::: ) (Set ($#k6_funct_6 :::"<:"::: ) (Set (Var "f")) ($#k6_funct_6 :::":>"::: ) ))) & (Bool (Set (Var "h")) ($#r1_hidden :::"="::: ) (Set (Set ($#k6_funct_6 :::"<:"::: ) (Set (Var "f")) ($#k6_funct_6 :::":>"::: ) ) ($#k1_funct_1 :::"."::: ) (Set (Var "y"))))) "holds" (Bool (Set (Set (Var "g")) ($#k1_funct_1 :::"."::: ) (Set (Var "y"))) ($#r1_hidden :::"="::: ) (Set (Set (Var "h")) ($#k1_funct_1 :::"."::: ) (Set (Var "x")))))) ; theorem :: FUNCT_6:35 (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 (Var "x")) ($#r2_hidden :::"in"::: ) (Set ($#k9_xtuple_0 :::"dom"::: ) (Set (Var "f")))) & (Bool (Set (Set (Var "f")) ($#k1_funct_1 :::"."::: ) (Set (Var "x"))) "is" ($#m1_hidden :::"Function":::)) & (Bool (Set (Var "y")) ($#r2_hidden :::"in"::: ) (Set ($#k9_xtuple_0 :::"dom"::: ) (Set ($#k6_funct_6 :::"<:"::: ) (Set (Var "f")) ($#k6_funct_6 :::":>"::: ) )))) "holds" (Bool (Set (Set (Var "f")) ($#k5_funct_6 :::".."::: ) "(" (Set (Var "x")) "," (Set (Var "y")) ")" ) ($#r1_hidden :::"="::: ) (Set (Set ($#k6_funct_6 :::"<:"::: ) (Set (Var "f")) ($#k6_funct_6 :::":>"::: ) ) ($#k5_funct_6 :::".."::: ) "(" (Set (Var "y")) "," (Set (Var "x")) ")" )))) ; definitionlet "f" be ($#m1_hidden :::"Function":::); func :::"Frege"::: "f" -> ($#m1_hidden :::"Function":::) means :: FUNCT_6:def 7 (Bool "(" (Bool (Set ($#k9_xtuple_0 :::"dom"::: ) it) ($#r1_hidden :::"="::: ) (Set ($#k4_card_3 :::"product"::: ) (Set "(" ($#k2_funct_6 :::"doms"::: ) "f" ")" ))) & (Bool "(" "for" (Set (Var "g")) "being" ($#m1_hidden :::"Function":::) "st" (Bool (Bool (Set (Var "g")) ($#r2_hidden :::"in"::: ) (Set ($#k4_card_3 :::"product"::: ) (Set "(" ($#k2_funct_6 :::"doms"::: ) "f" ")" )))) "holds" (Bool "ex" (Set (Var "h")) "being" ($#m1_hidden :::"Function":::) "st" (Bool "(" (Bool (Set it ($#k1_funct_1 :::"."::: ) (Set (Var "g"))) ($#r1_hidden :::"="::: ) (Set (Var "h"))) & (Bool (Set ($#k9_xtuple_0 :::"dom"::: ) (Set (Var "h"))) ($#r1_hidden :::"="::: ) (Set "f" ($#k8_relat_1 :::"""::: ) (Set "(" ($#k1_funct_6 :::"SubFuncs"::: ) (Set "(" ($#k10_xtuple_0 :::"rng"::: ) "f" ")" ) ")" ))) & (Bool "(" "for" (Set (Var "x")) "being" ($#m1_hidden :::"set"::: ) "st" (Bool (Bool (Set (Var "x")) ($#r2_hidden :::"in"::: ) (Set ($#k9_xtuple_0 :::"dom"::: ) (Set (Var "h"))))) "holds" (Bool (Set (Set (Var "h")) ($#k1_funct_1 :::"."::: ) (Set (Var "x"))) ($#r1_hidden :::"="::: ) (Set (Set "(" ($#k2_funct_5 :::"uncurry"::: ) "f" ")" ) ($#k1_binop_1 :::"."::: ) "(" (Set (Var "x")) "," (Set "(" (Set (Var "g")) ($#k1_funct_1 :::"."::: ) (Set (Var "x")) ")" ) ")" )) ")" ) ")" )) ")" ) ")" ); end; :: deftheorem defines :::"Frege"::: FUNCT_6:def 7 : (Bool "for" (Set (Var "f")) "," (Set (Var "b2")) "being" ($#m1_hidden :::"Function":::) "holds" (Bool "(" (Bool (Set (Var "b2")) ($#r1_hidden :::"="::: ) (Set ($#k7_funct_6 :::"Frege"::: ) (Set (Var "f")))) "iff" (Bool "(" (Bool (Set ($#k9_xtuple_0 :::"dom"::: ) (Set (Var "b2"))) ($#r1_hidden :::"="::: ) (Set ($#k4_card_3 :::"product"::: ) (Set "(" ($#k2_funct_6 :::"doms"::: ) (Set (Var "f")) ")" ))) & (Bool "(" "for" (Set (Var "g")) "being" ($#m1_hidden :::"Function":::) "st" (Bool (Bool (Set (Var "g")) ($#r2_hidden :::"in"::: ) (Set ($#k4_card_3 :::"product"::: ) (Set "(" ($#k2_funct_6 :::"doms"::: ) (Set (Var "f")) ")" )))) "holds" (Bool "ex" (Set (Var "h")) "being" ($#m1_hidden :::"Function":::) "st" (Bool "(" (Bool (Set (Set (Var "b2")) ($#k1_funct_1 :::"."::: ) (Set (Var "g"))) ($#r1_hidden :::"="::: ) (Set (Var "h"))) & (Bool (Set ($#k9_xtuple_0 :::"dom"::: ) (Set (Var "h"))) ($#r1_hidden :::"="::: ) (Set (Set (Var "f")) ($#k8_relat_1 :::"""::: ) (Set "(" ($#k1_funct_6 :::"SubFuncs"::: ) (Set "(" ($#k10_xtuple_0 :::"rng"::: ) (Set (Var "f")) ")" ) ")" ))) & (Bool "(" "for" (Set (Var "x")) "being" ($#m1_hidden :::"set"::: ) "st" (Bool (Bool (Set (Var "x")) ($#r2_hidden :::"in"::: ) (Set ($#k9_xtuple_0 :::"dom"::: ) (Set (Var "h"))))) "holds" (Bool (Set (Set (Var "h")) ($#k1_funct_1 :::"."::: ) (Set (Var "x"))) ($#r1_hidden :::"="::: ) (Set (Set "(" ($#k2_funct_5 :::"uncurry"::: ) (Set (Var "f")) ")" ) ($#k1_binop_1 :::"."::: ) "(" (Set (Var "x")) "," (Set "(" (Set (Var "g")) ($#k1_funct_1 :::"."::: ) (Set (Var "x")) ")" ) ")" )) ")" ) ")" )) ")" ) ")" ) ")" )); theorem :: FUNCT_6:36 (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 "g")) ($#r2_hidden :::"in"::: ) (Set ($#k4_card_3 :::"product"::: ) (Set "(" ($#k2_funct_6 :::"doms"::: ) (Set (Var "f")) ")" ))) & (Bool (Set (Var "x")) ($#r2_hidden :::"in"::: ) (Set ($#k9_xtuple_0 :::"dom"::: ) (Set (Var "g"))))) "holds" (Bool (Set (Set "(" ($#k7_funct_6 :::"Frege"::: ) (Set (Var "f")) ")" ) ($#k5_funct_6 :::".."::: ) "(" (Set (Var "g")) "," (Set (Var "x")) ")" ) ($#r1_hidden :::"="::: ) (Set (Set (Var "f")) ($#k5_funct_6 :::".."::: ) "(" (Set (Var "x")) "," (Set "(" (Set (Var "g")) ($#k1_funct_1 :::"."::: ) (Set (Var "x")) ")" ) ")" )))) ; theorem :: FUNCT_6:37 (Bool "for" (Set (Var "x")) "being" ($#m1_hidden :::"set"::: ) (Bool "for" (Set (Var "f")) "," (Set (Var "g")) "," (Set (Var "h")) "," (Set (Var "h9")) "being" ($#m1_hidden :::"Function":::) "st" (Bool (Bool (Set (Var "x")) ($#r2_hidden :::"in"::: ) (Set ($#k9_xtuple_0 :::"dom"::: ) (Set (Var "f")))) & (Bool (Set (Var "g")) ($#r1_hidden :::"="::: ) (Set (Set (Var "f")) ($#k1_funct_1 :::"."::: ) (Set (Var "x")))) & (Bool (Set (Var "h")) ($#r2_hidden :::"in"::: ) (Set ($#k4_card_3 :::"product"::: ) (Set "(" ($#k2_funct_6 :::"doms"::: ) (Set (Var "f")) ")" ))) & (Bool (Set (Var "h9")) ($#r1_hidden :::"="::: ) (Set (Set "(" ($#k7_funct_6 :::"Frege"::: ) (Set (Var "f")) ")" ) ($#k1_funct_1 :::"."::: ) (Set (Var "h"))))) "holds" (Bool "(" (Bool (Set (Set (Var "h")) ($#k1_funct_1 :::"."::: ) (Set (Var "x"))) ($#r2_hidden :::"in"::: ) (Set ($#k9_xtuple_0 :::"dom"::: ) (Set (Var "g")))) & (Bool (Set (Set (Var "h9")) ($#k1_funct_1 :::"."::: ) (Set (Var "x"))) ($#r1_hidden :::"="::: ) (Set (Set (Var "g")) ($#k1_funct_1 :::"."::: ) (Set "(" (Set (Var "h")) ($#k1_funct_1 :::"."::: ) (Set (Var "x")) ")" ))) & (Bool (Set (Var "h9")) ($#r2_hidden :::"in"::: ) (Set ($#k4_card_3 :::"product"::: ) (Set "(" ($#k3_funct_6 :::"rngs"::: ) (Set (Var "f")) ")" ))) ")" ))) ; theorem :: FUNCT_6:38 (Bool "for" (Set (Var "f")) "being" ($#m1_hidden :::"Function":::) "holds" (Bool (Set ($#k10_xtuple_0 :::"rng"::: ) (Set "(" ($#k7_funct_6 :::"Frege"::: ) (Set (Var "f")) ")" )) ($#r1_hidden :::"="::: ) (Set ($#k4_card_3 :::"product"::: ) (Set "(" ($#k3_funct_6 :::"rngs"::: ) (Set (Var "f")) ")" )))) ; theorem :: FUNCT_6:39 (Bool "for" (Set (Var "f")) "being" ($#m1_hidden :::"Function":::) "st" (Bool (Bool (Bool "not" (Set ($#k1_xboole_0 :::"{}"::: ) ) ($#r2_hidden :::"in"::: ) (Set ($#k10_xtuple_0 :::"rng"::: ) (Set (Var "f")))))) "holds" (Bool "(" (Bool (Set ($#k7_funct_6 :::"Frege"::: ) (Set (Var "f"))) "is" ($#v2_funct_1 :::"one-to-one"::: ) ) "iff" (Bool "for" (Set (Var "g")) "being" ($#m1_hidden :::"Function":::) "st" (Bool (Bool (Set (Var "g")) ($#r2_hidden :::"in"::: ) (Set ($#k10_xtuple_0 :::"rng"::: ) (Set (Var "f"))))) "holds" (Bool (Set (Var "g")) "is" ($#v2_funct_1 :::"one-to-one"::: ) )) ")" )) ; begin theorem :: FUNCT_6:40 (Bool "(" (Bool (Set ($#k6_funct_6 :::"<:"::: ) (Set ($#k1_xboole_0 :::"{}"::: ) ) ($#k6_funct_6 :::":>"::: ) ) ($#r1_hidden :::"="::: ) (Set ($#k1_xboole_0 :::"{}"::: ) )) & (Bool (Set ($#k7_funct_6 :::"Frege"::: ) (Set ($#k1_xboole_0 :::"{}"::: ) )) ($#r1_hidden :::"="::: ) (Set (Set ($#k1_xboole_0 :::"{}"::: ) ) ($#k16_funcop_1 :::".-->"::: ) (Set ($#k1_xboole_0 :::"{}"::: ) ))) ")" ) ; theorem :: FUNCT_6:41 (Bool "for" (Set (Var "X")) "being" ($#m1_hidden :::"set"::: ) (Bool "for" (Set (Var "f")) "being" ($#m1_hidden :::"Function":::) "st" (Bool (Bool (Set (Var "X")) ($#r1_hidden :::"<>"::: ) (Set ($#k1_xboole_0 :::"{}"::: ) ))) "holds" (Bool "(" (Bool (Set ($#k9_xtuple_0 :::"dom"::: ) (Set ($#k6_funct_6 :::"<:"::: ) (Set "(" (Set (Var "X")) ($#k7_funcop_1 :::"-->"::: ) (Set (Var "f")) ")" ) ($#k6_funct_6 :::":>"::: ) )) ($#r1_hidden :::"="::: ) (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 ($#k9_xtuple_0 :::"dom"::: ) (Set (Var "f"))))) "holds" (Bool (Set (Set ($#k6_funct_6 :::"<:"::: ) (Set "(" (Set (Var "X")) ($#k7_funcop_1 :::"-->"::: ) (Set (Var "f")) ")" ) ($#k6_funct_6 :::":>"::: ) ) ($#k1_funct_1 :::"."::: ) (Set (Var "x"))) ($#r1_hidden :::"="::: ) (Set (Set (Var "X")) ($#k7_funcop_1 :::"-->"::: ) (Set "(" (Set (Var "f")) ($#k1_funct_1 :::"."::: ) (Set (Var "x")) ")" ))) ")" ) ")" ))) ; theorem :: FUNCT_6:42 (Bool "for" (Set (Var "X")) "being" ($#m1_hidden :::"set"::: ) (Bool "for" (Set (Var "f")) "being" ($#m1_hidden :::"Function":::) "holds" (Bool "(" (Bool (Set ($#k9_xtuple_0 :::"dom"::: ) (Set "(" ($#k7_funct_6 :::"Frege"::: ) (Set "(" (Set (Var "X")) ($#k7_funcop_1 :::"-->"::: ) (Set (Var "f")) ")" ) ")" )) ($#r1_hidden :::"="::: ) (Set ($#k1_funct_2 :::"Funcs"::: ) "(" (Set (Var "X")) "," (Set "(" ($#k9_xtuple_0 :::"dom"::: ) (Set (Var "f")) ")" ) ")" )) & (Bool (Set ($#k10_xtuple_0 :::"rng"::: ) (Set "(" ($#k7_funct_6 :::"Frege"::: ) (Set "(" (Set (Var "X")) ($#k7_funcop_1 :::"-->"::: ) (Set (Var "f")) ")" ) ")" )) ($#r1_hidden :::"="::: ) (Set ($#k1_funct_2 :::"Funcs"::: ) "(" (Set (Var "X")) "," (Set "(" ($#k10_xtuple_0 :::"rng"::: ) (Set (Var "f")) ")" ) ")" )) & (Bool "(" "for" (Set (Var "g")) "being" ($#m1_hidden :::"Function":::) "st" (Bool (Bool (Set (Var "g")) ($#r2_hidden :::"in"::: ) (Set ($#k1_funct_2 :::"Funcs"::: ) "(" (Set (Var "X")) "," (Set "(" ($#k9_xtuple_0 :::"dom"::: ) (Set (Var "f")) ")" ) ")" ))) "holds" (Bool (Set (Set "(" ($#k7_funct_6 :::"Frege"::: ) (Set "(" (Set (Var "X")) ($#k7_funcop_1 :::"-->"::: ) (Set (Var "f")) ")" ) ")" ) ($#k1_funct_1 :::"."::: ) (Set (Var "g"))) ($#r1_hidden :::"="::: ) (Set (Set (Var "f")) ($#k3_relat_1 :::"*"::: ) (Set (Var "g")))) ")" ) ")" ))) ; theorem :: FUNCT_6:43 (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_hidden :::"="::: ) (Set (Var "X"))) & (Bool (Set ($#k9_xtuple_0 :::"dom"::: ) (Set (Var "g"))) ($#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"))) "," (Set (Set (Var "g")) ($#k1_funct_1 :::"."::: ) (Set (Var "x"))) ($#r2_wellord2 :::"are_equipotent"::: ) ) ")" )) "holds" (Bool (Set ($#k4_card_3 :::"product"::: ) (Set (Var "f"))) "," (Set ($#k4_card_3 :::"product"::: ) (Set (Var "g"))) ($#r2_wellord2 :::"are_equipotent"::: ) ))) ; theorem :: FUNCT_6:44 (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_hidden :::"="::: ) (Set ($#k9_xtuple_0 :::"dom"::: ) (Set (Var "h")))) & (Bool (Set ($#k9_xtuple_0 :::"dom"::: ) (Set (Var "g"))) ($#r1_hidden :::"="::: ) (Set ($#k10_xtuple_0 :::"rng"::: ) (Set (Var "h")))) & (Bool (Set (Var "h")) "is" ($#v2_funct_1 :::"one-to-one"::: ) ) & (Bool "(" "for" (Set (Var "x")) "being" ($#m1_hidden :::"set"::: ) "st" (Bool (Bool (Set (Var "x")) ($#r2_hidden :::"in"::: ) (Set ($#k9_xtuple_0 :::"dom"::: ) (Set (Var "h"))))) "holds" (Bool (Set (Set (Var "f")) ($#k1_funct_1 :::"."::: ) (Set (Var "x"))) "," (Set (Set (Var "g")) ($#k1_funct_1 :::"."::: ) (Set "(" (Set (Var "h")) ($#k1_funct_1 :::"."::: ) (Set (Var "x")) ")" )) ($#r2_wellord2 :::"are_equipotent"::: ) ) ")" )) "holds" (Bool (Set ($#k4_card_3 :::"product"::: ) (Set (Var "f"))) "," (Set ($#k4_card_3 :::"product"::: ) (Set (Var "g"))) ($#r2_wellord2 :::"are_equipotent"::: ) )) ; theorem :: FUNCT_6:45 (Bool "for" (Set (Var "X")) "being" ($#m1_hidden :::"set"::: ) (Bool "for" (Set (Var "f")) "being" ($#m1_hidden :::"Function":::) (Bool "for" (Set (Var "P")) "being" ($#m1_subset_1 :::"Permutation":::) "of" (Set (Var "X")) "st" (Bool (Bool (Set ($#k9_xtuple_0 :::"dom"::: ) (Set (Var "f"))) ($#r1_hidden :::"="::: ) (Set (Var "X")))) "holds" (Bool (Set ($#k4_card_3 :::"product"::: ) (Set (Var "f"))) "," (Set ($#k4_card_3 :::"product"::: ) (Set "(" (Set (Var "f")) ($#k3_relat_1 :::"*"::: ) (Set (Var "P")) ")" )) ($#r2_wellord2 :::"are_equipotent"::: ) )))) ; begin definitionlet "f" be ($#m1_hidden :::"Function":::); let "X" be ($#m1_hidden :::"set"::: ) ; func :::"Funcs"::: "(" "f" "," "X" ")" -> ($#m1_hidden :::"Function":::) means :: FUNCT_6:def 8 (Bool "(" (Bool (Set ($#k9_xtuple_0 :::"dom"::: ) it) ($#r1_hidden :::"="::: ) (Set ($#k9_xtuple_0 :::"dom"::: ) "f")) & (Bool "(" "for" (Set (Var "x")) "being" ($#m1_hidden :::"set"::: ) "st" (Bool (Bool (Set (Var "x")) ($#r2_hidden :::"in"::: ) (Set ($#k9_xtuple_0 :::"dom"::: ) "f"))) "holds" (Bool (Set it ($#k1_funct_1 :::"."::: ) (Set (Var "x"))) ($#r1_hidden :::"="::: ) (Set ($#k1_funct_2 :::"Funcs"::: ) "(" (Set "(" "f" ($#k1_funct_1 :::"."::: ) (Set (Var "x")) ")" ) "," "X" ")" )) ")" ) ")" ); end; :: deftheorem defines :::"Funcs"::: FUNCT_6:def 8 : (Bool "for" (Set (Var "f")) "being" ($#m1_hidden :::"Function":::) (Bool "for" (Set (Var "X")) "being" ($#m1_hidden :::"set"::: ) (Bool "for" (Set (Var "b3")) "being" ($#m1_hidden :::"Function":::) "holds" (Bool "(" (Bool (Set (Var "b3")) ($#r1_hidden :::"="::: ) (Set ($#k8_funct_6 :::"Funcs"::: ) "(" (Set (Var "f")) "," (Set (Var "X")) ")" )) "iff" (Bool "(" (Bool (Set ($#k9_xtuple_0 :::"dom"::: ) (Set (Var "b3"))) ($#r1_hidden :::"="::: ) (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 ($#k9_xtuple_0 :::"dom"::: ) (Set (Var "f"))))) "holds" (Bool (Set (Set (Var "b3")) ($#k1_funct_1 :::"."::: ) (Set (Var "x"))) ($#r1_hidden :::"="::: ) (Set ($#k1_funct_2 :::"Funcs"::: ) "(" (Set "(" (Set (Var "f")) ($#k1_funct_1 :::"."::: ) (Set (Var "x")) ")" ) "," (Set (Var "X")) ")" )) ")" ) ")" ) ")" )))); theorem :: FUNCT_6:46 (Bool "for" (Set (Var "f")) "being" ($#m1_hidden :::"Function":::) "st" (Bool (Bool (Bool "not" (Set ($#k1_xboole_0 :::"{}"::: ) ) ($#r2_hidden :::"in"::: ) (Set ($#k10_xtuple_0 :::"rng"::: ) (Set (Var "f")))))) "holds" (Bool (Set ($#k8_funct_6 :::"Funcs"::: ) "(" (Set (Var "f")) "," (Set ($#k1_xboole_0 :::"{}"::: ) ) ")" ) ($#r1_hidden :::"="::: ) (Set (Set "(" ($#k9_xtuple_0 :::"dom"::: ) (Set (Var "f")) ")" ) ($#k7_funcop_1 :::"-->"::: ) (Set ($#k1_xboole_0 :::"{}"::: ) )))) ; theorem :: FUNCT_6:47 (Bool "for" (Set (Var "X")) "being" ($#m1_hidden :::"set"::: ) "holds" (Bool (Set ($#k8_funct_6 :::"Funcs"::: ) "(" (Set ($#k1_xboole_0 :::"{}"::: ) ) "," (Set (Var "X")) ")" ) ($#r1_hidden :::"="::: ) (Set ($#k1_xboole_0 :::"{}"::: ) ))) ; theorem :: FUNCT_6:48 (Bool "for" (Set (Var "X")) "," (Set (Var "Y")) "," (Set (Var "Z")) "being" ($#m1_hidden :::"set"::: ) "holds" (Bool (Set ($#k8_funct_6 :::"Funcs"::: ) "(" (Set "(" (Set (Var "X")) ($#k7_funcop_1 :::"-->"::: ) (Set (Var "Y")) ")" ) "," (Set (Var "Z")) ")" ) ($#r1_hidden :::"="::: ) (Set (Set (Var "X")) ($#k7_funcop_1 :::"-->"::: ) (Set "(" ($#k1_funct_2 :::"Funcs"::: ) "(" (Set (Var "Y")) "," (Set (Var "Z")) ")" ")" )))) ; theorem :: FUNCT_6:49 (Bool "for" (Set (Var "X")) "being" ($#m1_hidden :::"set"::: ) (Bool "for" (Set (Var "f")) "being" ($#m1_hidden :::"Function":::) "holds" (Bool (Set ($#k1_funct_2 :::"Funcs"::: ) "(" (Set "(" ($#k3_card_3 :::"Union"::: ) (Set "(" ($#k2_card_3 :::"disjoin"::: ) (Set (Var "f")) ")" ) ")" ) "," (Set (Var "X")) ")" ) "," (Set ($#k4_card_3 :::"product"::: ) (Set "(" ($#k8_funct_6 :::"Funcs"::: ) "(" (Set (Var "f")) "," (Set (Var "X")) ")" ")" )) ($#r2_wellord2 :::"are_equipotent"::: ) ))) ; definitionlet "X" be ($#m1_hidden :::"set"::: ) ; let "f" be ($#m1_hidden :::"Function":::); func :::"Funcs"::: "(" "X" "," "f" ")" -> ($#m1_hidden :::"Function":::) means :: FUNCT_6:def 9 (Bool "(" (Bool (Set ($#k9_xtuple_0 :::"dom"::: ) it) ($#r1_hidden :::"="::: ) (Set ($#k9_xtuple_0 :::"dom"::: ) "f")) & (Bool "(" "for" (Set (Var "x")) "being" ($#m1_hidden :::"set"::: ) "st" (Bool (Bool (Set (Var "x")) ($#r2_hidden :::"in"::: ) (Set ($#k9_xtuple_0 :::"dom"::: ) "f"))) "holds" (Bool (Set it ($#k1_funct_1 :::"."::: ) (Set (Var "x"))) ($#r1_hidden :::"="::: ) (Set ($#k1_funct_2 :::"Funcs"::: ) "(" "X" "," (Set "(" "f" ($#k1_funct_1 :::"."::: ) (Set (Var "x")) ")" ) ")" )) ")" ) ")" ); end; :: deftheorem defines :::"Funcs"::: FUNCT_6:def 9 : (Bool "for" (Set (Var "X")) "being" ($#m1_hidden :::"set"::: ) (Bool "for" (Set (Var "f")) "," (Set (Var "b3")) "being" ($#m1_hidden :::"Function":::) "holds" (Bool "(" (Bool (Set (Var "b3")) ($#r1_hidden :::"="::: ) (Set ($#k9_funct_6 :::"Funcs"::: ) "(" (Set (Var "X")) "," (Set (Var "f")) ")" )) "iff" (Bool "(" (Bool (Set ($#k9_xtuple_0 :::"dom"::: ) (Set (Var "b3"))) ($#r1_hidden :::"="::: ) (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 ($#k9_xtuple_0 :::"dom"::: ) (Set (Var "f"))))) "holds" (Bool (Set (Set (Var "b3")) ($#k1_funct_1 :::"."::: ) (Set (Var "x"))) ($#r1_hidden :::"="::: ) (Set ($#k1_funct_2 :::"Funcs"::: ) "(" (Set (Var "X")) "," (Set "(" (Set (Var "f")) ($#k1_funct_1 :::"."::: ) (Set (Var "x")) ")" ) ")" )) ")" ) ")" ) ")" ))); theorem :: FUNCT_6:50 (Bool "for" (Set (Var "f")) "being" ($#m1_hidden :::"Function":::) "holds" (Bool (Set ($#k9_funct_6 :::"Funcs"::: ) "(" (Set ($#k1_xboole_0 :::"{}"::: ) ) "," (Set (Var "f")) ")" ) ($#r1_hidden :::"="::: ) (Set (Set "(" ($#k9_xtuple_0 :::"dom"::: ) (Set (Var "f")) ")" ) ($#k7_funcop_1 :::"-->"::: ) (Set ($#k1_tarski :::"{"::: ) (Set ($#k1_xboole_0 :::"{}"::: ) ) ($#k1_tarski :::"}"::: ) )))) ; theorem :: FUNCT_6:51 (Bool "for" (Set (Var "X")) "being" ($#m1_hidden :::"set"::: ) "holds" (Bool (Set ($#k9_funct_6 :::"Funcs"::: ) "(" (Set (Var "X")) "," (Set ($#k1_xboole_0 :::"{}"::: ) ) ")" ) ($#r1_hidden :::"="::: ) (Set ($#k1_xboole_0 :::"{}"::: ) ))) ; theorem :: FUNCT_6:52 (Bool "for" (Set (Var "X")) "," (Set (Var "Y")) "," (Set (Var "Z")) "being" ($#m1_hidden :::"set"::: ) "holds" (Bool (Set ($#k9_funct_6 :::"Funcs"::: ) "(" (Set (Var "X")) "," (Set "(" (Set (Var "Y")) ($#k7_funcop_1 :::"-->"::: ) (Set (Var "Z")) ")" ) ")" ) ($#r1_hidden :::"="::: ) (Set (Set (Var "Y")) ($#k7_funcop_1 :::"-->"::: ) (Set "(" ($#k1_funct_2 :::"Funcs"::: ) "(" (Set (Var "X")) "," (Set (Var "Z")) ")" ")" )))) ; theorem :: FUNCT_6:53 (Bool "for" (Set (Var "X")) "being" ($#m1_hidden :::"set"::: ) (Bool "for" (Set (Var "f")) "being" ($#m1_hidden :::"Function":::) "holds" (Bool (Set ($#k4_card_3 :::"product"::: ) (Set "(" ($#k9_funct_6 :::"Funcs"::: ) "(" (Set (Var "X")) "," (Set (Var "f")) ")" ")" )) "," (Set ($#k1_funct_2 :::"Funcs"::: ) "(" (Set (Var "X")) "," (Set "(" ($#k4_card_3 :::"product"::: ) (Set (Var "f")) ")" ) ")" ) ($#r2_wellord2 :::"are_equipotent"::: ) ))) ; begin definitionlet "f" be ($#m1_hidden :::"Function":::); func :::"commute"::: "f" -> ($#v1_funcop_1 :::"Function-yielding"::: ) ($#m1_hidden :::"Function":::) equals :: FUNCT_6:def 10 (Set ($#k3_funct_5 :::"curry'"::: ) (Set "(" ($#k2_funct_5 :::"uncurry"::: ) "f" ")" )); end; :: deftheorem defines :::"commute"::: FUNCT_6:def 10 : (Bool "for" (Set (Var "f")) "being" ($#m1_hidden :::"Function":::) "holds" (Bool (Set ($#k10_funct_6 :::"commute"::: ) (Set (Var "f"))) ($#r1_hidden :::"="::: ) (Set ($#k3_funct_5 :::"curry'"::: ) (Set "(" ($#k2_funct_5 :::"uncurry"::: ) (Set (Var "f")) ")" )))); theorem :: FUNCT_6:54 (Bool "for" (Set (Var "f")) "being" ($#m1_hidden :::"Function":::) (Bool "for" (Set (Var "x")) "being" ($#m1_hidden :::"set"::: ) "st" (Bool (Bool (Set (Var "x")) ($#r2_hidden :::"in"::: ) (Set ($#k9_xtuple_0 :::"dom"::: ) (Set "(" ($#k10_funct_6 :::"commute"::: ) (Set (Var "f")) ")" )))) "holds" (Bool (Set (Set "(" ($#k10_funct_6 :::"commute"::: ) (Set (Var "f")) ")" ) ($#k1_funct_1 :::"."::: ) (Set (Var "x"))) "is" ($#m1_hidden :::"Function":::)))) ; theorem :: FUNCT_6:55 (Bool "for" (Set (Var "A")) "," (Set (Var "B")) "," (Set (Var "C")) "being" ($#m1_hidden :::"set"::: ) (Bool "for" (Set (Var "f")) "being" ($#m1_hidden :::"Function":::) "st" (Bool (Bool (Set (Var "A")) ($#r1_hidden :::"<>"::: ) (Set ($#k1_xboole_0 :::"{}"::: ) )) & (Bool (Set (Var "B")) ($#r1_hidden :::"<>"::: ) (Set ($#k1_xboole_0 :::"{}"::: ) )) & (Bool (Set (Var "f")) ($#r2_hidden :::"in"::: ) (Set ($#k1_funct_2 :::"Funcs"::: ) "(" (Set (Var "A")) "," (Set "(" ($#k1_funct_2 :::"Funcs"::: ) "(" (Set (Var "B")) "," (Set (Var "C")) ")" ")" ) ")" ))) "holds" (Bool (Set ($#k10_funct_6 :::"commute"::: ) (Set (Var "f"))) ($#r2_hidden :::"in"::: ) (Set ($#k1_funct_2 :::"Funcs"::: ) "(" (Set (Var "B")) "," (Set "(" ($#k1_funct_2 :::"Funcs"::: ) "(" (Set (Var "A")) "," (Set (Var "C")) ")" ")" ) ")" )))) ; theorem :: FUNCT_6:56 (Bool "for" (Set (Var "A")) "," (Set (Var "B")) "," (Set (Var "C")) "being" ($#m1_hidden :::"set"::: ) (Bool "for" (Set (Var "f")) "being" ($#m1_hidden :::"Function":::) "st" (Bool (Bool (Set (Var "A")) ($#r1_hidden :::"<>"::: ) (Set ($#k1_xboole_0 :::"{}"::: ) )) & (Bool (Set (Var "B")) ($#r1_hidden :::"<>"::: ) (Set ($#k1_xboole_0 :::"{}"::: ) )) & (Bool (Set (Var "f")) ($#r2_hidden :::"in"::: ) (Set ($#k1_funct_2 :::"Funcs"::: ) "(" (Set (Var "A")) "," (Set "(" ($#k1_funct_2 :::"Funcs"::: ) "(" (Set (Var "B")) "," (Set (Var "C")) ")" ")" ) ")" ))) "holds" (Bool "for" (Set (Var "g")) "," (Set (Var "h")) "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 (Var "A"))) & (Bool (Set (Var "y")) ($#r2_hidden :::"in"::: ) (Set (Var "B"))) & (Bool (Set (Set (Var "f")) ($#k1_funct_1 :::"."::: ) (Set (Var "x"))) ($#r1_hidden :::"="::: ) (Set (Var "g"))) & (Bool (Set (Set "(" ($#k10_funct_6 :::"commute"::: ) (Set (Var "f")) ")" ) ($#k1_funct_1 :::"."::: ) (Set (Var "y"))) ($#r1_hidden :::"="::: ) (Set (Var "h")))) "holds" (Bool "(" (Bool (Set (Set (Var "h")) ($#k1_funct_1 :::"."::: ) (Set (Var "x"))) ($#r1_hidden :::"="::: ) (Set (Set (Var "g")) ($#k1_funct_1 :::"."::: ) (Set (Var "y")))) & (Bool (Set ($#k9_xtuple_0 :::"dom"::: ) (Set (Var "h"))) ($#r1_hidden :::"="::: ) (Set (Var "A"))) & (Bool (Set ($#k9_xtuple_0 :::"dom"::: ) (Set (Var "g"))) ($#r1_hidden :::"="::: ) (Set (Var "B"))) & (Bool (Set ($#k10_xtuple_0 :::"rng"::: ) (Set (Var "h"))) ($#r1_tarski :::"c="::: ) (Set (Var "C"))) & (Bool (Set ($#k10_xtuple_0 :::"rng"::: ) (Set (Var "g"))) ($#r1_tarski :::"c="::: ) (Set (Var "C"))) ")" ))))) ; theorem :: FUNCT_6:57 (Bool "for" (Set (Var "A")) "," (Set (Var "B")) "," (Set (Var "C")) "being" ($#m1_hidden :::"set"::: ) (Bool "for" (Set (Var "f")) "being" ($#m1_hidden :::"Function":::) "st" (Bool (Bool (Set (Var "A")) ($#r1_hidden :::"<>"::: ) (Set ($#k1_xboole_0 :::"{}"::: ) )) & (Bool (Set (Var "B")) ($#r1_hidden :::"<>"::: ) (Set ($#k1_xboole_0 :::"{}"::: ) )) & (Bool (Set (Var "f")) ($#r2_hidden :::"in"::: ) (Set ($#k1_funct_2 :::"Funcs"::: ) "(" (Set (Var "A")) "," (Set "(" ($#k1_funct_2 :::"Funcs"::: ) "(" (Set (Var "B")) "," (Set (Var "C")) ")" ")" ) ")" ))) "holds" (Bool (Set ($#k10_funct_6 :::"commute"::: ) (Set "(" ($#k10_funct_6 :::"commute"::: ) (Set (Var "f")) ")" )) ($#r1_hidden :::"="::: ) (Set (Var "f"))))) ; theorem :: FUNCT_6:58 (Bool (Set ($#k10_funct_6 :::"commute"::: ) (Set ($#k1_xboole_0 :::"{}"::: ) )) ($#r1_hidden :::"="::: ) (Set ($#k1_xboole_0 :::"{}"::: ) )) ; theorem :: FUNCT_6:59 (Bool "for" (Set (Var "f")) "being" ($#v1_funcop_1 :::"Function-yielding"::: ) ($#m1_hidden :::"Function":::) "holds" (Bool (Set ($#k9_xtuple_0 :::"dom"::: ) (Set "(" ($#k2_funct_6 :::"doms"::: ) (Set (Var "f")) ")" )) ($#r1_hidden :::"="::: ) (Set ($#k9_xtuple_0 :::"dom"::: ) (Set (Var "f"))))) ; theorem :: FUNCT_6:60 (Bool "for" (Set (Var "f")) "being" ($#v1_funcop_1 :::"Function-yielding"::: ) ($#m1_hidden :::"Function":::) "holds" (Bool (Set ($#k9_xtuple_0 :::"dom"::: ) (Set "(" ($#k3_funct_6 :::"rngs"::: ) (Set (Var "f")) ")" )) ($#r1_hidden :::"="::: ) (Set ($#k9_xtuple_0 :::"dom"::: ) (Set (Var "f"))))) ;