:: FUNCT_5 semantic presentation begin scheme :: FUNCT_5:sch 1 LambdaFS{ F1() -> ($#m1_hidden :::"set"::: ) , F2( ($#m1_hidden :::"set"::: ) ) -> ($#m1_hidden :::"set"::: ) } : (Bool "ex" (Set (Var "f")) "being" ($#m1_hidden :::"Function":::) "st" (Bool "(" (Bool (Set ($#k9_xtuple_0 :::"dom"::: ) (Set (Var "f"))) ($#r1_hidden :::"="::: ) (Set F1 "(" ")" )) & (Bool "(" "for" (Set (Var "g")) "being" ($#m1_hidden :::"Function":::) "st" (Bool (Bool (Set (Var "g")) ($#r2_hidden :::"in"::: ) (Set F1 "(" ")" ))) "holds" (Bool (Set (Set (Var "f")) ($#k1_funct_1 :::"."::: ) (Set (Var "g"))) ($#r1_hidden :::"="::: ) (Set F2 "(" (Set (Var "g")) ")" )) ")" ) ")" )) proof end; theorem :: FUNCT_5:1 (Bool (Set ($#k2_funct_4 :::"~"::: ) (Set ($#k1_xboole_0 :::"{}"::: ) )) ($#r1_hidden :::"="::: ) (Set ($#k1_xboole_0 :::"{}"::: ) )) ; theorem :: FUNCT_5:2 canceled; theorem :: FUNCT_5:3 canceled; theorem :: FUNCT_5:4 canceled; theorem :: FUNCT_5:5 canceled; theorem :: FUNCT_5:6 canceled; theorem :: FUNCT_5:7 canceled; theorem :: FUNCT_5:8 (Bool "(" (Bool (Set ($#k9_xtuple_0 :::"proj1"::: ) (Set ($#k1_xboole_0 :::"{}"::: ) )) ($#r1_hidden :::"="::: ) (Set ($#k1_xboole_0 :::"{}"::: ) )) & (Bool (Set ($#k10_xtuple_0 :::"proj2"::: ) (Set ($#k1_xboole_0 :::"{}"::: ) )) ($#r1_hidden :::"="::: ) (Set ($#k1_xboole_0 :::"{}"::: ) )) ")" ) ; theorem :: FUNCT_5:9 (Bool "for" (Set (Var "Y")) "," (Set (Var "X")) "being" ($#m1_hidden :::"set"::: ) "st" (Bool (Bool "(" (Bool (Set (Var "Y")) ($#r1_hidden :::"<>"::: ) (Set ($#k1_xboole_0 :::"{}"::: ) )) "or" (Bool (Set ($#k2_zfmisc_1 :::"[:"::: ) (Set (Var "X")) "," (Set (Var "Y")) ($#k2_zfmisc_1 :::":]"::: ) ) ($#r1_hidden :::"<>"::: ) (Set ($#k1_xboole_0 :::"{}"::: ) )) "or" (Bool (Set ($#k2_zfmisc_1 :::"[:"::: ) (Set (Var "Y")) "," (Set (Var "X")) ($#k2_zfmisc_1 :::":]"::: ) ) ($#r1_hidden :::"<>"::: ) (Set ($#k1_xboole_0 :::"{}"::: ) )) ")" )) "holds" (Bool "(" (Bool (Set ($#k9_xtuple_0 :::"proj1"::: ) (Set ($#k2_zfmisc_1 :::"[:"::: ) (Set (Var "X")) "," (Set (Var "Y")) ($#k2_zfmisc_1 :::":]"::: ) )) ($#r1_hidden :::"="::: ) (Set (Var "X"))) & (Bool (Set ($#k10_xtuple_0 :::"proj2"::: ) (Set ($#k2_zfmisc_1 :::"[:"::: ) (Set (Var "Y")) "," (Set (Var "X")) ($#k2_zfmisc_1 :::":]"::: ) )) ($#r1_hidden :::"="::: ) (Set (Var "X"))) ")" )) ; theorem :: FUNCT_5:10 (Bool "for" (Set (Var "X")) "," (Set (Var "Y")) "being" ($#m1_hidden :::"set"::: ) "holds" (Bool "(" (Bool (Set ($#k9_xtuple_0 :::"proj1"::: ) (Set ($#k2_zfmisc_1 :::"[:"::: ) (Set (Var "X")) "," (Set (Var "Y")) ($#k2_zfmisc_1 :::":]"::: ) )) ($#r1_tarski :::"c="::: ) (Set (Var "X"))) & (Bool (Set ($#k10_xtuple_0 :::"proj2"::: ) (Set ($#k2_zfmisc_1 :::"[:"::: ) (Set (Var "X")) "," (Set (Var "Y")) ($#k2_zfmisc_1 :::":]"::: ) )) ($#r1_tarski :::"c="::: ) (Set (Var "Y"))) ")" )) ; theorem :: FUNCT_5:11 (Bool "for" (Set (Var "Z")) "," (Set (Var "X")) "," (Set (Var "Y")) "being" ($#m1_hidden :::"set"::: ) "st" (Bool (Bool (Set (Var "Z")) ($#r1_tarski :::"c="::: ) (Set ($#k2_zfmisc_1 :::"[:"::: ) (Set (Var "X")) "," (Set (Var "Y")) ($#k2_zfmisc_1 :::":]"::: ) ))) "holds" (Bool "(" (Bool (Set ($#k9_xtuple_0 :::"proj1"::: ) (Set (Var "Z"))) ($#r1_tarski :::"c="::: ) (Set (Var "X"))) & (Bool (Set ($#k10_xtuple_0 :::"proj2"::: ) (Set (Var "Z"))) ($#r1_tarski :::"c="::: ) (Set (Var "Y"))) ")" )) ; theorem :: FUNCT_5:12 (Bool "for" (Set (Var "x")) "," (Set (Var "y")) "being" ($#m1_hidden :::"set"::: ) "holds" (Bool "(" (Bool (Set ($#k9_xtuple_0 :::"proj1"::: ) (Set ($#k1_tarski :::"{"::: ) (Set ($#k4_tarski :::"["::: ) (Set (Var "x")) "," (Set (Var "y")) ($#k4_tarski :::"]"::: ) ) ($#k1_tarski :::"}"::: ) )) ($#r1_hidden :::"="::: ) (Set ($#k1_tarski :::"{"::: ) (Set (Var "x")) ($#k1_tarski :::"}"::: ) )) & (Bool (Set ($#k10_xtuple_0 :::"proj2"::: ) (Set ($#k1_tarski :::"{"::: ) (Set ($#k4_tarski :::"["::: ) (Set (Var "x")) "," (Set (Var "y")) ($#k4_tarski :::"]"::: ) ) ($#k1_tarski :::"}"::: ) )) ($#r1_hidden :::"="::: ) (Set ($#k1_tarski :::"{"::: ) (Set (Var "y")) ($#k1_tarski :::"}"::: ) )) ")" )) ; theorem :: FUNCT_5:13 (Bool "for" (Set (Var "x")) "," (Set (Var "y")) "," (Set (Var "z")) "," (Set (Var "t")) "being" ($#m1_hidden :::"set"::: ) "holds" (Bool "(" (Bool (Set ($#k9_xtuple_0 :::"proj1"::: ) (Set ($#k2_tarski :::"{"::: ) (Set ($#k4_tarski :::"["::: ) (Set (Var "x")) "," (Set (Var "y")) ($#k4_tarski :::"]"::: ) ) "," (Set ($#k4_tarski :::"["::: ) (Set (Var "z")) "," (Set (Var "t")) ($#k4_tarski :::"]"::: ) ) ($#k2_tarski :::"}"::: ) )) ($#r1_hidden :::"="::: ) (Set ($#k2_tarski :::"{"::: ) (Set (Var "x")) "," (Set (Var "z")) ($#k2_tarski :::"}"::: ) )) & (Bool (Set ($#k10_xtuple_0 :::"proj2"::: ) (Set ($#k2_tarski :::"{"::: ) (Set ($#k4_tarski :::"["::: ) (Set (Var "x")) "," (Set (Var "y")) ($#k4_tarski :::"]"::: ) ) "," (Set ($#k4_tarski :::"["::: ) (Set (Var "z")) "," (Set (Var "t")) ($#k4_tarski :::"]"::: ) ) ($#k2_tarski :::"}"::: ) )) ($#r1_hidden :::"="::: ) (Set ($#k2_tarski :::"{"::: ) (Set (Var "y")) "," (Set (Var "t")) ($#k2_tarski :::"}"::: ) )) ")" )) ; theorem :: FUNCT_5:14 (Bool "for" (Set (Var "X")) "being" ($#m1_hidden :::"set"::: ) "st" (Bool (Bool "(" "for" (Set (Var "x")) "," (Set (Var "y")) "being" ($#m1_hidden :::"set"::: ) "holds" (Bool (Bool "not" (Set ($#k4_tarski :::"["::: ) (Set (Var "x")) "," (Set (Var "y")) ($#k4_tarski :::"]"::: ) ) ($#r2_hidden :::"in"::: ) (Set (Var "X")))) ")" )) "holds" (Bool "(" (Bool (Set ($#k9_xtuple_0 :::"proj1"::: ) (Set (Var "X"))) ($#r1_hidden :::"="::: ) (Set ($#k1_xboole_0 :::"{}"::: ) )) & (Bool (Set ($#k10_xtuple_0 :::"proj2"::: ) (Set (Var "X"))) ($#r1_hidden :::"="::: ) (Set ($#k1_xboole_0 :::"{}"::: ) )) ")" )) ; theorem :: FUNCT_5:15 (Bool "for" (Set (Var "X")) "being" ($#m1_hidden :::"set"::: ) "st" (Bool (Bool "(" (Bool (Set ($#k9_xtuple_0 :::"proj1"::: ) (Set (Var "X"))) ($#r1_hidden :::"="::: ) (Set ($#k1_xboole_0 :::"{}"::: ) )) "or" (Bool (Set ($#k10_xtuple_0 :::"proj2"::: ) (Set (Var "X"))) ($#r1_hidden :::"="::: ) (Set ($#k1_xboole_0 :::"{}"::: ) )) ")" )) "holds" (Bool "for" (Set (Var "x")) "," (Set (Var "y")) "being" ($#m1_hidden :::"set"::: ) "holds" (Bool (Bool "not" (Set ($#k4_tarski :::"["::: ) (Set (Var "x")) "," (Set (Var "y")) ($#k4_tarski :::"]"::: ) ) ($#r2_hidden :::"in"::: ) (Set (Var "X")))))) ; theorem :: FUNCT_5:16 (Bool "for" (Set (Var "X")) "being" ($#m1_hidden :::"set"::: ) "holds" (Bool "(" (Bool (Set ($#k9_xtuple_0 :::"proj1"::: ) (Set (Var "X"))) ($#r1_hidden :::"="::: ) (Set ($#k1_xboole_0 :::"{}"::: ) )) "iff" (Bool (Set ($#k10_xtuple_0 :::"proj2"::: ) (Set (Var "X"))) ($#r1_hidden :::"="::: ) (Set ($#k1_xboole_0 :::"{}"::: ) )) ")" )) ; theorem :: FUNCT_5:17 (Bool "for" (Set (Var "f")) "being" ($#m1_hidden :::"Function":::) "holds" (Bool "(" (Bool (Set ($#k9_xtuple_0 :::"proj1"::: ) (Set "(" ($#k9_xtuple_0 :::"dom"::: ) (Set (Var "f")) ")" )) ($#r1_hidden :::"="::: ) (Set ($#k10_xtuple_0 :::"proj2"::: ) (Set "(" ($#k9_xtuple_0 :::"dom"::: ) (Set "(" ($#k2_funct_4 :::"~"::: ) (Set (Var "f")) ")" ) ")" ))) & (Bool (Set ($#k10_xtuple_0 :::"proj2"::: ) (Set "(" ($#k9_xtuple_0 :::"dom"::: ) (Set (Var "f")) ")" )) ($#r1_hidden :::"="::: ) (Set ($#k9_xtuple_0 :::"proj1"::: ) (Set "(" ($#k9_xtuple_0 :::"dom"::: ) (Set "(" ($#k2_funct_4 :::"~"::: ) (Set (Var "f")) ")" ) ")" ))) ")" )) ; theorem :: FUNCT_5:18 (Bool "for" (Set (Var "f")) "being" ($#m1_hidden :::"Relation":::) "holds" (Bool "(" (Bool (Set ($#k9_xtuple_0 :::"proj1"::: ) (Set (Var "f"))) ($#r1_hidden :::"="::: ) (Set ($#k9_xtuple_0 :::"dom"::: ) (Set (Var "f")))) & (Bool (Set ($#k10_xtuple_0 :::"proj2"::: ) (Set (Var "f"))) ($#r1_hidden :::"="::: ) (Set ($#k10_xtuple_0 :::"rng"::: ) (Set (Var "f")))) ")" )) ; definitionlet "f" be ($#m1_hidden :::"Function":::); func :::"curry"::: "f" -> ($#m1_hidden :::"Function":::) means :: FUNCT_5:def 1 (Bool "(" (Bool (Set ($#k9_xtuple_0 :::"dom"::: ) it) ($#r1_hidden :::"="::: ) (Set ($#k9_xtuple_0 :::"proj1"::: ) (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 :::"proj1"::: ) (Set "(" ($#k9_xtuple_0 :::"dom"::: ) "f" ")" )))) "holds" (Bool "ex" (Set (Var "g")) "being" ($#m1_hidden :::"Function":::) "st" (Bool "(" (Bool (Set it ($#k1_funct_1 :::"."::: ) (Set (Var "x"))) ($#r1_hidden :::"="::: ) (Set (Var "g"))) & (Bool (Set ($#k9_xtuple_0 :::"dom"::: ) (Set (Var "g"))) ($#r1_hidden :::"="::: ) (Set ($#k10_xtuple_0 :::"proj2"::: ) (Set "(" (Set "(" ($#k9_xtuple_0 :::"dom"::: ) "f" ")" ) ($#k3_xboole_0 :::"/\"::: ) (Set ($#k2_zfmisc_1 :::"[:"::: ) (Set ($#k1_tarski :::"{"::: ) (Set (Var "x")) ($#k1_tarski :::"}"::: ) ) "," (Set "(" ($#k10_xtuple_0 :::"proj2"::: ) (Set "(" ($#k9_xtuple_0 :::"dom"::: ) "f" ")" ) ")" ) ($#k2_zfmisc_1 :::":]"::: ) ) ")" ))) & (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 (Set (Set (Var "g")) ($#k1_funct_1 :::"."::: ) (Set (Var "y"))) ($#r1_hidden :::"="::: ) (Set "f" ($#k1_binop_1 :::"."::: ) "(" (Set (Var "x")) "," (Set (Var "y")) ")" )) ")" ) ")" )) ")" ) ")" ); func :::"uncurry"::: "f" -> ($#m1_hidden :::"Function":::) means :: FUNCT_5:def 2 (Bool "(" (Bool "(" "for" (Set (Var "t")) "being" ($#m1_hidden :::"set"::: ) "holds" (Bool "(" (Bool (Set (Var "t")) ($#r2_hidden :::"in"::: ) (Set ($#k9_xtuple_0 :::"dom"::: ) it)) "iff" (Bool "ex" (Set (Var "x")) "being" ($#m1_hidden :::"set"::: ) (Bool "ex" (Set (Var "g")) "being" ($#m1_hidden :::"Function":::)(Bool "ex" (Set (Var "y")) "being" ($#m1_hidden :::"set"::: ) "st" (Bool "(" (Bool (Set (Var "t")) ($#r1_hidden :::"="::: ) (Set ($#k4_tarski :::"["::: ) (Set (Var "x")) "," (Set (Var "y")) ($#k4_tarski :::"]"::: ) )) & (Bool (Set (Var "x")) ($#r2_hidden :::"in"::: ) (Set ($#k9_xtuple_0 :::"dom"::: ) "f")) & (Bool (Set (Var "g")) ($#r1_hidden :::"="::: ) (Set "f" ($#k1_funct_1 :::"."::: ) (Set (Var "x")))) & (Bool (Set (Var "y")) ($#r2_hidden :::"in"::: ) (Set ($#k9_xtuple_0 :::"dom"::: ) (Set (Var "g")))) ")" )))) ")" ) ")" ) & (Bool "(" "for" (Set (Var "x")) "being" ($#m1_hidden :::"set"::: ) (Bool "for" (Set (Var "g")) "being" ($#m1_hidden :::"Function":::) "st" (Bool (Bool (Set (Var "x")) ($#r2_hidden :::"in"::: ) (Set ($#k9_xtuple_0 :::"dom"::: ) it)) & (Bool (Set (Var "g")) ($#r1_hidden :::"="::: ) (Set "f" ($#k1_funct_1 :::"."::: ) (Set "(" (Set (Var "x")) ($#k1_xtuple_0 :::"`1"::: ) ")" )))) "holds" (Bool (Set it ($#k1_funct_1 :::"."::: ) (Set (Var "x"))) ($#r1_hidden :::"="::: ) (Set (Set (Var "g")) ($#k1_funct_1 :::"."::: ) (Set "(" (Set (Var "x")) ($#k2_xtuple_0 :::"`2"::: ) ")" )))) ")" ) ")" ); end; :: deftheorem defines :::"curry"::: FUNCT_5:def 1 : (Bool "for" (Set (Var "f")) "," (Set (Var "b2")) "being" ($#m1_hidden :::"Function":::) "holds" (Bool "(" (Bool (Set (Var "b2")) ($#r1_hidden :::"="::: ) (Set ($#k1_funct_5 :::"curry"::: ) (Set (Var "f")))) "iff" (Bool "(" (Bool (Set ($#k9_xtuple_0 :::"dom"::: ) (Set (Var "b2"))) ($#r1_hidden :::"="::: ) (Set ($#k9_xtuple_0 :::"proj1"::: ) (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 :::"proj1"::: ) (Set "(" ($#k9_xtuple_0 :::"dom"::: ) (Set (Var "f")) ")" )))) "holds" (Bool "ex" (Set (Var "g")) "being" ($#m1_hidden :::"Function":::) "st" (Bool "(" (Bool (Set (Set (Var "b2")) ($#k1_funct_1 :::"."::: ) (Set (Var "x"))) ($#r1_hidden :::"="::: ) (Set (Var "g"))) & (Bool (Set ($#k9_xtuple_0 :::"dom"::: ) (Set (Var "g"))) ($#r1_hidden :::"="::: ) (Set ($#k10_xtuple_0 :::"proj2"::: ) (Set "(" (Set "(" ($#k9_xtuple_0 :::"dom"::: ) (Set (Var "f")) ")" ) ($#k3_xboole_0 :::"/\"::: ) (Set ($#k2_zfmisc_1 :::"[:"::: ) (Set ($#k1_tarski :::"{"::: ) (Set (Var "x")) ($#k1_tarski :::"}"::: ) ) "," (Set "(" ($#k10_xtuple_0 :::"proj2"::: ) (Set "(" ($#k9_xtuple_0 :::"dom"::: ) (Set (Var "f")) ")" ) ")" ) ($#k2_zfmisc_1 :::":]"::: ) ) ")" ))) & (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 (Set (Set (Var "g")) ($#k1_funct_1 :::"."::: ) (Set (Var "y"))) ($#r1_hidden :::"="::: ) (Set (Set (Var "f")) ($#k1_binop_1 :::"."::: ) "(" (Set (Var "x")) "," (Set (Var "y")) ")" )) ")" ) ")" )) ")" ) ")" ) ")" )); :: deftheorem defines :::"uncurry"::: FUNCT_5: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_5 :::"uncurry"::: ) (Set (Var "f")))) "iff" (Bool "(" (Bool "(" "for" (Set (Var "t")) "being" ($#m1_hidden :::"set"::: ) "holds" (Bool "(" (Bool (Set (Var "t")) ($#r2_hidden :::"in"::: ) (Set ($#k9_xtuple_0 :::"dom"::: ) (Set (Var "b2")))) "iff" (Bool "ex" (Set (Var "x")) "being" ($#m1_hidden :::"set"::: ) (Bool "ex" (Set (Var "g")) "being" ($#m1_hidden :::"Function":::)(Bool "ex" (Set (Var "y")) "being" ($#m1_hidden :::"set"::: ) "st" (Bool "(" (Bool (Set (Var "t")) ($#r1_hidden :::"="::: ) (Set ($#k4_tarski :::"["::: ) (Set (Var "x")) "," (Set (Var "y")) ($#k4_tarski :::"]"::: ) )) & (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 (Var "g")))) ")" )))) ")" ) ")" ) & (Bool "(" "for" (Set (Var "x")) "being" ($#m1_hidden :::"set"::: ) (Bool "for" (Set (Var "g")) "being" ($#m1_hidden :::"Function":::) "st" (Bool (Bool (Set (Var "x")) ($#r2_hidden :::"in"::: ) (Set ($#k9_xtuple_0 :::"dom"::: ) (Set (Var "b2")))) & (Bool (Set (Var "g")) ($#r1_hidden :::"="::: ) (Set (Set (Var "f")) ($#k1_funct_1 :::"."::: ) (Set "(" (Set (Var "x")) ($#k1_xtuple_0 :::"`1"::: ) ")" )))) "holds" (Bool (Set (Set (Var "b2")) ($#k1_funct_1 :::"."::: ) (Set (Var "x"))) ($#r1_hidden :::"="::: ) (Set (Set (Var "g")) ($#k1_funct_1 :::"."::: ) (Set "(" (Set (Var "x")) ($#k2_xtuple_0 :::"`2"::: ) ")" )))) ")" ) ")" ) ")" )); definitionlet "f" be ($#m1_hidden :::"Function":::); func :::"curry'"::: "f" -> ($#m1_hidden :::"Function":::) equals :: FUNCT_5:def 3 (Set ($#k1_funct_5 :::"curry"::: ) (Set "(" ($#k2_funct_4 :::"~"::: ) "f" ")" )); func :::"uncurry'"::: "f" -> ($#m1_hidden :::"Function":::) equals :: FUNCT_5:def 4 (Set ($#k2_funct_4 :::"~"::: ) (Set "(" ($#k2_funct_5 :::"uncurry"::: ) "f" ")" )); end; :: deftheorem defines :::"curry'"::: FUNCT_5:def 3 : (Bool "for" (Set (Var "f")) "being" ($#m1_hidden :::"Function":::) "holds" (Bool (Set ($#k3_funct_5 :::"curry'"::: ) (Set (Var "f"))) ($#r1_hidden :::"="::: ) (Set ($#k1_funct_5 :::"curry"::: ) (Set "(" ($#k2_funct_4 :::"~"::: ) (Set (Var "f")) ")" )))); :: deftheorem defines :::"uncurry'"::: FUNCT_5:def 4 : (Bool "for" (Set (Var "f")) "being" ($#m1_hidden :::"Function":::) "holds" (Bool (Set ($#k4_funct_5 :::"uncurry'"::: ) (Set (Var "f"))) ($#r1_hidden :::"="::: ) (Set ($#k2_funct_4 :::"~"::: ) (Set "(" ($#k2_funct_5 :::"uncurry"::: ) (Set (Var "f")) ")" )))); theorem :: FUNCT_5:19 (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 ($#k4_tarski :::"["::: ) (Set (Var "x")) "," (Set (Var "y")) ($#k4_tarski :::"]"::: ) ) ($#r2_hidden :::"in"::: ) (Set ($#k9_xtuple_0 :::"dom"::: ) (Set (Var "f"))))) "holds" (Bool "(" (Bool (Set (Var "x")) ($#r2_hidden :::"in"::: ) (Set ($#k9_xtuple_0 :::"dom"::: ) (Set "(" ($#k1_funct_5 :::"curry"::: ) (Set (Var "f")) ")" ))) & (Bool (Set (Set "(" ($#k1_funct_5 :::"curry"::: ) (Set (Var "f")) ")" ) ($#k1_funct_1 :::"."::: ) (Set (Var "x"))) "is" ($#m1_hidden :::"Function":::)) ")" ))) ; theorem :: FUNCT_5:20 (Bool "for" (Set (Var "x")) "," (Set (Var "y")) "being" ($#m1_hidden :::"set"::: ) (Bool "for" (Set (Var "f")) "," (Set (Var "g")) "being" ($#m1_hidden :::"Function":::) "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 (Var "g")) ($#r1_hidden :::"="::: ) (Set (Set "(" ($#k1_funct_5 :::"curry"::: ) (Set (Var "f")) ")" ) ($#k1_funct_1 :::"."::: ) (Set (Var "x"))))) "holds" (Bool "(" (Bool (Set (Var "y")) ($#r2_hidden :::"in"::: ) (Set ($#k9_xtuple_0 :::"dom"::: ) (Set (Var "g")))) & (Bool (Set (Set (Var "g")) ($#k1_funct_1 :::"."::: ) (Set (Var "y"))) ($#r1_hidden :::"="::: ) (Set (Set (Var "f")) ($#k1_binop_1 :::"."::: ) "(" (Set (Var "x")) "," (Set (Var "y")) ")" )) ")" ))) ; theorem :: FUNCT_5:21 (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 ($#k4_tarski :::"["::: ) (Set (Var "x")) "," (Set (Var "y")) ($#k4_tarski :::"]"::: ) ) ($#r2_hidden :::"in"::: ) (Set ($#k9_xtuple_0 :::"dom"::: ) (Set (Var "f"))))) "holds" (Bool "(" (Bool (Set (Var "y")) ($#r2_hidden :::"in"::: ) (Set ($#k9_xtuple_0 :::"dom"::: ) (Set "(" ($#k3_funct_5 :::"curry'"::: ) (Set (Var "f")) ")" ))) & (Bool (Set (Set "(" ($#k3_funct_5 :::"curry'"::: ) (Set (Var "f")) ")" ) ($#k1_funct_1 :::"."::: ) (Set (Var "y"))) "is" ($#m1_hidden :::"Function":::)) ")" ))) ; theorem :: FUNCT_5:22 (Bool "for" (Set (Var "x")) "," (Set (Var "y")) "being" ($#m1_hidden :::"set"::: ) (Bool "for" (Set (Var "f")) "," (Set (Var "g")) "being" ($#m1_hidden :::"Function":::) "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 (Var "g")) ($#r1_hidden :::"="::: ) (Set (Set "(" ($#k3_funct_5 :::"curry'"::: ) (Set (Var "f")) ")" ) ($#k1_funct_1 :::"."::: ) (Set (Var "y"))))) "holds" (Bool "(" (Bool (Set (Var "x")) ($#r2_hidden :::"in"::: ) (Set ($#k9_xtuple_0 :::"dom"::: ) (Set (Var "g")))) & (Bool (Set (Set (Var "g")) ($#k1_funct_1 :::"."::: ) (Set (Var "x"))) ($#r1_hidden :::"="::: ) (Set (Set (Var "f")) ($#k1_binop_1 :::"."::: ) "(" (Set (Var "x")) "," (Set (Var "y")) ")" )) ")" ))) ; theorem :: FUNCT_5:23 (Bool "for" (Set (Var "f")) "being" ($#m1_hidden :::"Function":::) "holds" (Bool (Set ($#k9_xtuple_0 :::"dom"::: ) (Set "(" ($#k3_funct_5 :::"curry'"::: ) (Set (Var "f")) ")" )) ($#r1_hidden :::"="::: ) (Set ($#k10_xtuple_0 :::"proj2"::: ) (Set "(" ($#k9_xtuple_0 :::"dom"::: ) (Set (Var "f")) ")" )))) ; theorem :: FUNCT_5:24 (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 ($#k2_zfmisc_1 :::"[:"::: ) (Set (Var "X")) "," (Set (Var "Y")) ($#k2_zfmisc_1 :::":]"::: ) ) ($#r1_hidden :::"<>"::: ) (Set ($#k1_xboole_0 :::"{}"::: ) )) & (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 "(" (Bool (Set ($#k9_xtuple_0 :::"dom"::: ) (Set "(" ($#k1_funct_5 :::"curry"::: ) (Set (Var "f")) ")" )) ($#r1_hidden :::"="::: ) (Set (Var "X"))) & (Bool (Set ($#k9_xtuple_0 :::"dom"::: ) (Set "(" ($#k3_funct_5 :::"curry'"::: ) (Set (Var "f")) ")" )) ($#r1_hidden :::"="::: ) (Set (Var "Y"))) ")" ))) ; theorem :: FUNCT_5:25 (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 "(" (Bool (Set ($#k9_xtuple_0 :::"dom"::: ) (Set "(" ($#k1_funct_5 :::"curry"::: ) (Set (Var "f")) ")" )) ($#r1_tarski :::"c="::: ) (Set (Var "X"))) & (Bool (Set ($#k9_xtuple_0 :::"dom"::: ) (Set "(" ($#k3_funct_5 :::"curry'"::: ) (Set (Var "f")) ")" )) ($#r1_tarski :::"c="::: ) (Set (Var "Y"))) ")" ))) ; theorem :: FUNCT_5:26 (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 ($#k10_xtuple_0 :::"rng"::: ) (Set (Var "f"))) ($#r1_tarski :::"c="::: ) (Set ($#k1_funct_2 :::"Funcs"::: ) "(" (Set (Var "X")) "," (Set (Var "Y")) ")" ))) "holds" (Bool "(" (Bool (Set ($#k9_xtuple_0 :::"dom"::: ) (Set "(" ($#k2_funct_5 :::"uncurry"::: ) (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 ($#k9_xtuple_0 :::"dom"::: ) (Set "(" ($#k4_funct_5 :::"uncurry'"::: ) (Set (Var "f")) ")" )) ($#r1_hidden :::"="::: ) (Set ($#k2_zfmisc_1 :::"[:"::: ) (Set (Var "X")) "," (Set "(" ($#k9_xtuple_0 :::"dom"::: ) (Set (Var "f")) ")" ) ($#k2_zfmisc_1 :::":]"::: ) )) ")" ))) ; theorem :: FUNCT_5:27 (Bool "for" (Set (Var "f")) "being" ($#m1_hidden :::"Function":::) "st" (Bool (Bool "(" "for" (Set (Var "x")) "," (Set (Var "y")) "being" ($#m1_hidden :::"set"::: ) "holds" (Bool (Bool "not" (Set ($#k4_tarski :::"["::: ) (Set (Var "x")) "," (Set (Var "y")) ($#k4_tarski :::"]"::: ) ) ($#r2_hidden :::"in"::: ) (Set ($#k9_xtuple_0 :::"dom"::: ) (Set (Var "f"))))) ")" )) "holds" (Bool "(" (Bool (Set ($#k1_funct_5 :::"curry"::: ) (Set (Var "f"))) ($#r1_hidden :::"="::: ) (Set ($#k1_xboole_0 :::"{}"::: ) )) & (Bool (Set ($#k3_funct_5 :::"curry'"::: ) (Set (Var "f"))) ($#r1_hidden :::"="::: ) (Set ($#k1_xboole_0 :::"{}"::: ) )) ")" )) ; theorem :: FUNCT_5:28 (Bool "for" (Set (Var "f")) "being" ($#m1_hidden :::"Function":::) "st" (Bool (Bool "(" "for" (Set (Var "x")) "being" ($#m1_hidden :::"set"::: ) "holds" (Bool "(" "not" (Bool (Set (Var "x")) ($#r2_hidden :::"in"::: ) (Set ($#k9_xtuple_0 :::"dom"::: ) (Set (Var "f")))) "or" "not" (Bool (Set (Set (Var "f")) ($#k1_funct_1 :::"."::: ) (Set (Var "x"))) "is" ($#m1_hidden :::"Function":::)) ")" ) ")" )) "holds" (Bool "(" (Bool (Set ($#k2_funct_5 :::"uncurry"::: ) (Set (Var "f"))) ($#r1_hidden :::"="::: ) (Set ($#k1_xboole_0 :::"{}"::: ) )) & (Bool (Set ($#k4_funct_5 :::"uncurry'"::: ) (Set (Var "f"))) ($#r1_hidden :::"="::: ) (Set ($#k1_xboole_0 :::"{}"::: ) )) ")" )) ; theorem :: FUNCT_5:29 (Bool "for" (Set (Var "X")) "," (Set (Var "Y")) "," (Set (Var "x")) "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 ($#k9_xtuple_0 :::"dom"::: ) (Set (Var "f"))) ($#r1_hidden :::"="::: ) (Set ($#k2_zfmisc_1 :::"[:"::: ) (Set (Var "X")) "," (Set (Var "Y")) ($#k2_zfmisc_1 :::":]"::: ) )) & (Bool (Set (Var "x")) ($#r2_hidden :::"in"::: ) (Set (Var "X")))) "holds" (Bool "ex" (Set (Var "g")) "being" ($#m1_hidden :::"Function":::) "st" (Bool "(" (Bool (Set (Set "(" ($#k1_funct_5 :::"curry"::: ) (Set (Var "f")) ")" ) ($#k1_funct_1 :::"."::: ) (Set (Var "x"))) ($#r1_hidden :::"="::: ) (Set (Var "g"))) & (Bool (Set ($#k9_xtuple_0 :::"dom"::: ) (Set (Var "g"))) ($#r1_hidden :::"="::: ) (Set (Var "Y"))) & (Bool (Set ($#k10_xtuple_0 :::"rng"::: ) (Set (Var "g"))) ($#r1_tarski :::"c="::: ) (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 (Var "Y")))) "holds" (Bool (Set (Set (Var "g")) ($#k1_funct_1 :::"."::: ) (Set (Var "y"))) ($#r1_hidden :::"="::: ) (Set (Set (Var "f")) ($#k1_binop_1 :::"."::: ) "(" (Set (Var "x")) "," (Set (Var "y")) ")" )) ")" ) ")" )))) ; theorem :: FUNCT_5: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 "(" ($#k1_funct_5 :::"curry"::: ) (Set (Var "f")) ")" )))) "holds" (Bool (Set (Set "(" ($#k1_funct_5 :::"curry"::: ) (Set (Var "f")) ")" ) ($#k1_funct_1 :::"."::: ) (Set (Var "x"))) "is" ($#m1_hidden :::"Function":::)))) ; theorem :: FUNCT_5: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 "(" ($#k1_funct_5 :::"curry"::: ) (Set (Var "f")) ")" ))) & (Bool (Set (Var "g")) ($#r1_hidden :::"="::: ) (Set (Set "(" ($#k1_funct_5 :::"curry"::: ) (Set (Var "f")) ")" ) ($#k1_funct_1 :::"."::: ) (Set (Var "x"))))) "holds" (Bool "(" (Bool (Set ($#k9_xtuple_0 :::"dom"::: ) (Set (Var "g"))) ($#r1_hidden :::"="::: ) (Set ($#k10_xtuple_0 :::"proj2"::: ) (Set "(" (Set "(" ($#k9_xtuple_0 :::"dom"::: ) (Set (Var "f")) ")" ) ($#k3_xboole_0 :::"/\"::: ) (Set ($#k2_zfmisc_1 :::"[:"::: ) (Set ($#k1_tarski :::"{"::: ) (Set (Var "x")) ($#k1_tarski :::"}"::: ) ) "," (Set "(" ($#k10_xtuple_0 :::"proj2"::: ) (Set "(" ($#k9_xtuple_0 :::"dom"::: ) (Set (Var "f")) ")" ) ")" ) ($#k2_zfmisc_1 :::":]"::: ) ) ")" ))) & (Bool (Set ($#k9_xtuple_0 :::"dom"::: ) (Set (Var "g"))) ($#r1_tarski :::"c="::: ) (Set ($#k10_xtuple_0 :::"proj2"::: ) (Set "(" ($#k9_xtuple_0 :::"dom"::: ) (Set (Var "f")) ")" ))) & (Bool (Set ($#k10_xtuple_0 :::"rng"::: ) (Set (Var "g"))) ($#r1_tarski :::"c="::: ) (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 (Set (Var "g")) ($#k1_funct_1 :::"."::: ) (Set (Var "y"))) ($#r1_hidden :::"="::: ) (Set (Set (Var "f")) ($#k1_binop_1 :::"."::: ) "(" (Set (Var "x")) "," (Set (Var "y")) ")" )) & (Bool (Set ($#k4_tarski :::"["::: ) (Set (Var "x")) "," (Set (Var "y")) ($#k4_tarski :::"]"::: ) ) ($#r2_hidden :::"in"::: ) (Set ($#k9_xtuple_0 :::"dom"::: ) (Set (Var "f")))) ")" ) ")" ) ")" ))) ; theorem :: FUNCT_5:32 (Bool "for" (Set (Var "X")) "," (Set (Var "Y")) "," (Set (Var "y")) "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 ($#k9_xtuple_0 :::"dom"::: ) (Set (Var "f"))) ($#r1_hidden :::"="::: ) (Set ($#k2_zfmisc_1 :::"[:"::: ) (Set (Var "X")) "," (Set (Var "Y")) ($#k2_zfmisc_1 :::":]"::: ) )) & (Bool (Set (Var "y")) ($#r2_hidden :::"in"::: ) (Set (Var "Y")))) "holds" (Bool "ex" (Set (Var "g")) "being" ($#m1_hidden :::"Function":::) "st" (Bool "(" (Bool (Set (Set "(" ($#k3_funct_5 :::"curry'"::: ) (Set (Var "f")) ")" ) ($#k1_funct_1 :::"."::: ) (Set (Var "y"))) ($#r1_hidden :::"="::: ) (Set (Var "g"))) & (Bool (Set ($#k9_xtuple_0 :::"dom"::: ) (Set (Var "g"))) ($#r1_hidden :::"="::: ) (Set (Var "X"))) & (Bool (Set ($#k10_xtuple_0 :::"rng"::: ) (Set (Var "g"))) ($#r1_tarski :::"c="::: ) (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 (Var "X")))) "holds" (Bool (Set (Set (Var "g")) ($#k1_funct_1 :::"."::: ) (Set (Var "x"))) ($#r1_hidden :::"="::: ) (Set (Set (Var "f")) ($#k1_binop_1 :::"."::: ) "(" (Set (Var "x")) "," (Set (Var "y")) ")" )) ")" ) ")" )))) ; theorem :: FUNCT_5:33 (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 "(" ($#k3_funct_5 :::"curry'"::: ) (Set (Var "f")) ")" )))) "holds" (Bool (Set (Set "(" ($#k3_funct_5 :::"curry'"::: ) (Set (Var "f")) ")" ) ($#k1_funct_1 :::"."::: ) (Set (Var "x"))) "is" ($#m1_hidden :::"Function":::)))) ; theorem :: FUNCT_5:34 (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 "(" ($#k3_funct_5 :::"curry'"::: ) (Set (Var "f")) ")" ))) & (Bool (Set (Var "g")) ($#r1_hidden :::"="::: ) (Set (Set "(" ($#k3_funct_5 :::"curry'"::: ) (Set (Var "f")) ")" ) ($#k1_funct_1 :::"."::: ) (Set (Var "x"))))) "holds" (Bool "(" (Bool (Set ($#k9_xtuple_0 :::"dom"::: ) (Set (Var "g"))) ($#r1_hidden :::"="::: ) (Set ($#k9_xtuple_0 :::"proj1"::: ) (Set "(" (Set "(" ($#k9_xtuple_0 :::"dom"::: ) (Set (Var "f")) ")" ) ($#k3_xboole_0 :::"/\"::: ) (Set ($#k2_zfmisc_1 :::"[:"::: ) (Set "(" ($#k9_xtuple_0 :::"proj1"::: ) (Set "(" ($#k9_xtuple_0 :::"dom"::: ) (Set (Var "f")) ")" ) ")" ) "," (Set ($#k1_tarski :::"{"::: ) (Set (Var "x")) ($#k1_tarski :::"}"::: ) ) ($#k2_zfmisc_1 :::":]"::: ) ) ")" ))) & (Bool (Set ($#k9_xtuple_0 :::"dom"::: ) (Set (Var "g"))) ($#r1_tarski :::"c="::: ) (Set ($#k9_xtuple_0 :::"proj1"::: ) (Set "(" ($#k9_xtuple_0 :::"dom"::: ) (Set (Var "f")) ")" ))) & (Bool (Set ($#k10_xtuple_0 :::"rng"::: ) (Set (Var "g"))) ($#r1_tarski :::"c="::: ) (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 (Set (Var "g")) ($#k1_funct_1 :::"."::: ) (Set (Var "y"))) ($#r1_hidden :::"="::: ) (Set (Set (Var "f")) ($#k1_binop_1 :::"."::: ) "(" (Set (Var "y")) "," (Set (Var "x")) ")" )) & (Bool (Set ($#k4_tarski :::"["::: ) (Set (Var "y")) "," (Set (Var "x")) ($#k4_tarski :::"]"::: ) ) ($#r2_hidden :::"in"::: ) (Set ($#k9_xtuple_0 :::"dom"::: ) (Set (Var "f")))) ")" ) ")" ) ")" ))) ; theorem :: FUNCT_5: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 ($#k9_xtuple_0 :::"dom"::: ) (Set (Var "f"))) ($#r1_hidden :::"="::: ) (Set ($#k2_zfmisc_1 :::"[:"::: ) (Set (Var "X")) "," (Set (Var "Y")) ($#k2_zfmisc_1 :::":]"::: ) ))) "holds" (Bool "(" (Bool (Set ($#k10_xtuple_0 :::"rng"::: ) (Set "(" ($#k1_funct_5 :::"curry"::: ) (Set (Var "f")) ")" )) ($#r1_tarski :::"c="::: ) (Set ($#k1_funct_2 :::"Funcs"::: ) "(" (Set (Var "Y")) "," (Set "(" ($#k10_xtuple_0 :::"rng"::: ) (Set (Var "f")) ")" ) ")" )) & (Bool (Set ($#k10_xtuple_0 :::"rng"::: ) (Set "(" ($#k3_funct_5 :::"curry'"::: ) (Set (Var "f")) ")" )) ($#r1_tarski :::"c="::: ) (Set ($#k1_funct_2 :::"Funcs"::: ) "(" (Set (Var "X")) "," (Set "(" ($#k10_xtuple_0 :::"rng"::: ) (Set (Var "f")) ")" ) ")" )) ")" ))) ; theorem :: FUNCT_5:36 (Bool "for" (Set (Var "f")) "being" ($#m1_hidden :::"Function":::) "holds" (Bool "(" (Bool (Set ($#k10_xtuple_0 :::"rng"::: ) (Set "(" ($#k1_funct_5 :::"curry"::: ) (Set (Var "f")) ")" )) ($#r1_tarski :::"c="::: ) (Set ($#k4_partfun1 :::"PFuncs"::: ) "(" (Set "(" ($#k10_xtuple_0 :::"proj2"::: ) (Set "(" ($#k9_xtuple_0 :::"dom"::: ) (Set (Var "f")) ")" ) ")" ) "," (Set "(" ($#k10_xtuple_0 :::"rng"::: ) (Set (Var "f")) ")" ) ")" )) & (Bool (Set ($#k10_xtuple_0 :::"rng"::: ) (Set "(" ($#k3_funct_5 :::"curry'"::: ) (Set (Var "f")) ")" )) ($#r1_tarski :::"c="::: ) (Set ($#k4_partfun1 :::"PFuncs"::: ) "(" (Set "(" ($#k9_xtuple_0 :::"proj1"::: ) (Set "(" ($#k9_xtuple_0 :::"dom"::: ) (Set (Var "f")) ")" ) ")" ) "," (Set "(" ($#k10_xtuple_0 :::"rng"::: ) (Set (Var "f")) ")" ) ")" )) ")" )) ; theorem :: FUNCT_5:37 (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 ($#k10_xtuple_0 :::"rng"::: ) (Set (Var "f"))) ($#r1_tarski :::"c="::: ) (Set ($#k4_partfun1 :::"PFuncs"::: ) "(" (Set (Var "X")) "," (Set (Var "Y")) ")" ))) "holds" (Bool "(" (Bool (Set ($#k9_xtuple_0 :::"dom"::: ) (Set "(" ($#k2_funct_5 :::"uncurry"::: ) (Set (Var "f")) ")" )) ($#r1_tarski :::"c="::: ) (Set ($#k2_zfmisc_1 :::"[:"::: ) (Set "(" ($#k9_xtuple_0 :::"dom"::: ) (Set (Var "f")) ")" ) "," (Set (Var "X")) ($#k2_zfmisc_1 :::":]"::: ) )) & (Bool (Set ($#k9_xtuple_0 :::"dom"::: ) (Set "(" ($#k4_funct_5 :::"uncurry'"::: ) (Set (Var "f")) ")" )) ($#r1_tarski :::"c="::: ) (Set ($#k2_zfmisc_1 :::"[:"::: ) (Set (Var "X")) "," (Set "(" ($#k9_xtuple_0 :::"dom"::: ) (Set (Var "f")) ")" ) ($#k2_zfmisc_1 :::":]"::: ) )) ")" ))) ; theorem :: FUNCT_5:38 (Bool "for" (Set (Var "x")) "," (Set (Var "y")) "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")))) & (Bool (Set (Var "y")) ($#r2_hidden :::"in"::: ) (Set ($#k9_xtuple_0 :::"dom"::: ) (Set (Var "g"))))) "holds" (Bool "(" (Bool (Set ($#k4_tarski :::"["::: ) (Set (Var "x")) "," (Set (Var "y")) ($#k4_tarski :::"]"::: ) ) ($#r2_hidden :::"in"::: ) (Set ($#k9_xtuple_0 :::"dom"::: ) (Set "(" ($#k2_funct_5 :::"uncurry"::: ) (Set (Var "f")) ")" ))) & (Bool (Set (Set "(" ($#k2_funct_5 :::"uncurry"::: ) (Set (Var "f")) ")" ) ($#k1_binop_1 :::"."::: ) "(" (Set (Var "x")) "," (Set (Var "y")) ")" ) ($#r1_hidden :::"="::: ) (Set (Set (Var "g")) ($#k1_funct_1 :::"."::: ) (Set (Var "y")))) & (Bool (Set (Set (Var "g")) ($#k1_funct_1 :::"."::: ) (Set (Var "y"))) ($#r2_hidden :::"in"::: ) (Set ($#k10_xtuple_0 :::"rng"::: ) (Set "(" ($#k2_funct_5 :::"uncurry"::: ) (Set (Var "f")) ")" ))) ")" ))) ; theorem :: FUNCT_5:39 (Bool "for" (Set (Var "x")) "," (Set (Var "y")) "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")))) & (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 "(" ($#k4_funct_5 :::"uncurry'"::: ) (Set (Var "f")) ")" ))) & (Bool (Set (Set "(" ($#k4_funct_5 :::"uncurry'"::: ) (Set (Var "f")) ")" ) ($#k1_binop_1 :::"."::: ) "(" (Set (Var "y")) "," (Set (Var "x")) ")" ) ($#r1_hidden :::"="::: ) (Set (Set (Var "g")) ($#k1_funct_1 :::"."::: ) (Set (Var "y")))) & (Bool (Set (Set (Var "g")) ($#k1_funct_1 :::"."::: ) (Set (Var "y"))) ($#r2_hidden :::"in"::: ) (Set ($#k10_xtuple_0 :::"rng"::: ) (Set "(" ($#k4_funct_5 :::"uncurry'"::: ) (Set (Var "f")) ")" ))) ")" ))) ; theorem :: FUNCT_5:40 (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 ($#k10_xtuple_0 :::"rng"::: ) (Set (Var "f"))) ($#r1_tarski :::"c="::: ) (Set ($#k4_partfun1 :::"PFuncs"::: ) "(" (Set (Var "X")) "," (Set (Var "Y")) ")" ))) "holds" (Bool "(" (Bool (Set ($#k10_xtuple_0 :::"rng"::: ) (Set "(" ($#k2_funct_5 :::"uncurry"::: ) (Set (Var "f")) ")" )) ($#r1_tarski :::"c="::: ) (Set (Var "Y"))) & (Bool (Set ($#k10_xtuple_0 :::"rng"::: ) (Set "(" ($#k4_funct_5 :::"uncurry'"::: ) (Set (Var "f")) ")" )) ($#r1_tarski :::"c="::: ) (Set (Var "Y"))) ")" ))) ; theorem :: FUNCT_5:41 (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 ($#k10_xtuple_0 :::"rng"::: ) (Set (Var "f"))) ($#r1_tarski :::"c="::: ) (Set ($#k1_funct_2 :::"Funcs"::: ) "(" (Set (Var "X")) "," (Set (Var "Y")) ")" ))) "holds" (Bool "(" (Bool (Set ($#k10_xtuple_0 :::"rng"::: ) (Set "(" ($#k2_funct_5 :::"uncurry"::: ) (Set (Var "f")) ")" )) ($#r1_tarski :::"c="::: ) (Set (Var "Y"))) & (Bool (Set ($#k10_xtuple_0 :::"rng"::: ) (Set "(" ($#k4_funct_5 :::"uncurry'"::: ) (Set (Var "f")) ")" )) ($#r1_tarski :::"c="::: ) (Set (Var "Y"))) ")" ))) ; theorem :: FUNCT_5:42 (Bool "(" (Bool (Set ($#k1_funct_5 :::"curry"::: ) (Set ($#k1_xboole_0 :::"{}"::: ) )) ($#r1_hidden :::"="::: ) (Set ($#k1_xboole_0 :::"{}"::: ) )) & (Bool (Set ($#k3_funct_5 :::"curry'"::: ) (Set ($#k1_xboole_0 :::"{}"::: ) )) ($#r1_hidden :::"="::: ) (Set ($#k1_xboole_0 :::"{}"::: ) )) ")" ) ; theorem :: FUNCT_5:43 (Bool "(" (Bool (Set ($#k2_funct_5 :::"uncurry"::: ) (Set ($#k1_xboole_0 :::"{}"::: ) )) ($#r1_hidden :::"="::: ) (Set ($#k1_xboole_0 :::"{}"::: ) )) & (Bool (Set ($#k4_funct_5 :::"uncurry'"::: ) (Set ($#k1_xboole_0 :::"{}"::: ) )) ($#r1_hidden :::"="::: ) (Set ($#k1_xboole_0 :::"{}"::: ) )) ")" ) ; theorem :: FUNCT_5:44 (Bool "for" (Set (Var "X")) "," (Set (Var "Y")) "being" ($#m1_hidden :::"set"::: ) (Bool "for" (Set (Var "f1")) "," (Set (Var "f2")) "being" ($#m1_hidden :::"Function":::) "st" (Bool (Bool (Set ($#k9_xtuple_0 :::"dom"::: ) (Set (Var "f1"))) ($#r1_hidden :::"="::: ) (Set ($#k2_zfmisc_1 :::"[:"::: ) (Set (Var "X")) "," (Set (Var "Y")) ($#k2_zfmisc_1 :::":]"::: ) )) & (Bool (Set ($#k9_xtuple_0 :::"dom"::: ) (Set (Var "f2"))) ($#r1_hidden :::"="::: ) (Set ($#k2_zfmisc_1 :::"[:"::: ) (Set (Var "X")) "," (Set (Var "Y")) ($#k2_zfmisc_1 :::":]"::: ) )) & (Bool (Set ($#k1_funct_5 :::"curry"::: ) (Set (Var "f1"))) ($#r1_hidden :::"="::: ) (Set ($#k1_funct_5 :::"curry"::: ) (Set (Var "f2"))))) "holds" (Bool (Set (Var "f1")) ($#r1_hidden :::"="::: ) (Set (Var "f2"))))) ; theorem :: FUNCT_5:45 (Bool "for" (Set (Var "X")) "," (Set (Var "Y")) "being" ($#m1_hidden :::"set"::: ) (Bool "for" (Set (Var "f1")) "," (Set (Var "f2")) "being" ($#m1_hidden :::"Function":::) "st" (Bool (Bool (Set ($#k9_xtuple_0 :::"dom"::: ) (Set (Var "f1"))) ($#r1_hidden :::"="::: ) (Set ($#k2_zfmisc_1 :::"[:"::: ) (Set (Var "X")) "," (Set (Var "Y")) ($#k2_zfmisc_1 :::":]"::: ) )) & (Bool (Set ($#k9_xtuple_0 :::"dom"::: ) (Set (Var "f2"))) ($#r1_hidden :::"="::: ) (Set ($#k2_zfmisc_1 :::"[:"::: ) (Set (Var "X")) "," (Set (Var "Y")) ($#k2_zfmisc_1 :::":]"::: ) )) & (Bool (Set ($#k3_funct_5 :::"curry'"::: ) (Set (Var "f1"))) ($#r1_hidden :::"="::: ) (Set ($#k3_funct_5 :::"curry'"::: ) (Set (Var "f2"))))) "holds" (Bool (Set (Var "f1")) ($#r1_hidden :::"="::: ) (Set (Var "f2"))))) ; theorem :: FUNCT_5:46 (Bool "for" (Set (Var "X")) "," (Set (Var "Y")) "being" ($#m1_hidden :::"set"::: ) (Bool "for" (Set (Var "f1")) "," (Set (Var "f2")) "being" ($#m1_hidden :::"Function":::) "st" (Bool (Bool (Set ($#k10_xtuple_0 :::"rng"::: ) (Set (Var "f1"))) ($#r1_tarski :::"c="::: ) (Set ($#k1_funct_2 :::"Funcs"::: ) "(" (Set (Var "X")) "," (Set (Var "Y")) ")" )) & (Bool (Set ($#k10_xtuple_0 :::"rng"::: ) (Set (Var "f2"))) ($#r1_tarski :::"c="::: ) (Set ($#k1_funct_2 :::"Funcs"::: ) "(" (Set (Var "X")) "," (Set (Var "Y")) ")" )) & (Bool (Set (Var "X")) ($#r1_hidden :::"<>"::: ) (Set ($#k1_xboole_0 :::"{}"::: ) )) & (Bool (Set ($#k2_funct_5 :::"uncurry"::: ) (Set (Var "f1"))) ($#r1_hidden :::"="::: ) (Set ($#k2_funct_5 :::"uncurry"::: ) (Set (Var "f2"))))) "holds" (Bool (Set (Var "f1")) ($#r1_hidden :::"="::: ) (Set (Var "f2"))))) ; theorem :: FUNCT_5:47 (Bool "for" (Set (Var "X")) "," (Set (Var "Y")) "being" ($#m1_hidden :::"set"::: ) (Bool "for" (Set (Var "f1")) "," (Set (Var "f2")) "being" ($#m1_hidden :::"Function":::) "st" (Bool (Bool (Set ($#k10_xtuple_0 :::"rng"::: ) (Set (Var "f1"))) ($#r1_tarski :::"c="::: ) (Set ($#k1_funct_2 :::"Funcs"::: ) "(" (Set (Var "X")) "," (Set (Var "Y")) ")" )) & (Bool (Set ($#k10_xtuple_0 :::"rng"::: ) (Set (Var "f2"))) ($#r1_tarski :::"c="::: ) (Set ($#k1_funct_2 :::"Funcs"::: ) "(" (Set (Var "X")) "," (Set (Var "Y")) ")" )) & (Bool (Set (Var "X")) ($#r1_hidden :::"<>"::: ) (Set ($#k1_xboole_0 :::"{}"::: ) )) & (Bool (Set ($#k4_funct_5 :::"uncurry'"::: ) (Set (Var "f1"))) ($#r1_hidden :::"="::: ) (Set ($#k4_funct_5 :::"uncurry'"::: ) (Set (Var "f2"))))) "holds" (Bool (Set (Var "f1")) ($#r1_hidden :::"="::: ) (Set (Var "f2"))))) ; theorem :: FUNCT_5:48 (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 ($#k10_xtuple_0 :::"rng"::: ) (Set (Var "f"))) ($#r1_tarski :::"c="::: ) (Set ($#k1_funct_2 :::"Funcs"::: ) "(" (Set (Var "X")) "," (Set (Var "Y")) ")" )) & (Bool (Set (Var "X")) ($#r1_hidden :::"<>"::: ) (Set ($#k1_xboole_0 :::"{}"::: ) ))) "holds" (Bool "(" (Bool (Set ($#k1_funct_5 :::"curry"::: ) (Set "(" ($#k2_funct_5 :::"uncurry"::: ) (Set (Var "f")) ")" )) ($#r1_hidden :::"="::: ) (Set (Var "f"))) & (Bool (Set ($#k3_funct_5 :::"curry'"::: ) (Set "(" ($#k4_funct_5 :::"uncurry'"::: ) (Set (Var "f")) ")" )) ($#r1_hidden :::"="::: ) (Set (Var "f"))) ")" ))) ; theorem :: FUNCT_5:49 (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 "(" (Bool (Set ($#k2_funct_5 :::"uncurry"::: ) (Set "(" ($#k1_funct_5 :::"curry"::: ) (Set (Var "f")) ")" )) ($#r1_hidden :::"="::: ) (Set (Var "f"))) & (Bool (Set ($#k4_funct_5 :::"uncurry'"::: ) (Set "(" ($#k3_funct_5 :::"curry'"::: ) (Set (Var "f")) ")" )) ($#r1_hidden :::"="::: ) (Set (Var "f"))) ")" ))) ; theorem :: FUNCT_5:50 (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 "(" (Bool (Set ($#k2_funct_5 :::"uncurry"::: ) (Set "(" ($#k1_funct_5 :::"curry"::: ) (Set (Var "f")) ")" )) ($#r1_hidden :::"="::: ) (Set (Var "f"))) & (Bool (Set ($#k4_funct_5 :::"uncurry'"::: ) (Set "(" ($#k3_funct_5 :::"curry'"::: ) (Set (Var "f")) ")" )) ($#r1_hidden :::"="::: ) (Set (Var "f"))) ")" ))) ; theorem :: FUNCT_5:51 (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 ($#k10_xtuple_0 :::"rng"::: ) (Set (Var "f"))) ($#r1_tarski :::"c="::: ) (Set ($#k4_partfun1 :::"PFuncs"::: ) "(" (Set (Var "X")) "," (Set (Var "Y")) ")" )) & (Bool (Bool "not" (Set ($#k1_xboole_0 :::"{}"::: ) ) ($#r2_hidden :::"in"::: ) (Set ($#k10_xtuple_0 :::"rng"::: ) (Set (Var "f")))))) "holds" (Bool "(" (Bool (Set ($#k1_funct_5 :::"curry"::: ) (Set "(" ($#k2_funct_5 :::"uncurry"::: ) (Set (Var "f")) ")" )) ($#r1_hidden :::"="::: ) (Set (Var "f"))) & (Bool (Set ($#k3_funct_5 :::"curry'"::: ) (Set "(" ($#k4_funct_5 :::"uncurry'"::: ) (Set (Var "f")) ")" )) ($#r1_hidden :::"="::: ) (Set (Var "f"))) ")" ))) ; theorem :: FUNCT_5:52 (Bool "for" (Set (Var "X")) "," (Set (Var "Y")) "being" ($#m1_hidden :::"set"::: ) (Bool "for" (Set (Var "f1")) "," (Set (Var "f2")) "being" ($#m1_hidden :::"Function":::) "st" (Bool (Bool (Set ($#k9_xtuple_0 :::"dom"::: ) (Set (Var "f1"))) ($#r1_tarski :::"c="::: ) (Set ($#k2_zfmisc_1 :::"[:"::: ) (Set (Var "X")) "," (Set (Var "Y")) ($#k2_zfmisc_1 :::":]"::: ) )) & (Bool (Set ($#k9_xtuple_0 :::"dom"::: ) (Set (Var "f2"))) ($#r1_tarski :::"c="::: ) (Set ($#k2_zfmisc_1 :::"[:"::: ) (Set (Var "X")) "," (Set (Var "Y")) ($#k2_zfmisc_1 :::":]"::: ) )) & (Bool (Set ($#k1_funct_5 :::"curry"::: ) (Set (Var "f1"))) ($#r1_hidden :::"="::: ) (Set ($#k1_funct_5 :::"curry"::: ) (Set (Var "f2"))))) "holds" (Bool (Set (Var "f1")) ($#r1_hidden :::"="::: ) (Set (Var "f2"))))) ; theorem :: FUNCT_5:53 (Bool "for" (Set (Var "X")) "," (Set (Var "Y")) "being" ($#m1_hidden :::"set"::: ) (Bool "for" (Set (Var "f1")) "," (Set (Var "f2")) "being" ($#m1_hidden :::"Function":::) "st" (Bool (Bool (Set ($#k9_xtuple_0 :::"dom"::: ) (Set (Var "f1"))) ($#r1_tarski :::"c="::: ) (Set ($#k2_zfmisc_1 :::"[:"::: ) (Set (Var "X")) "," (Set (Var "Y")) ($#k2_zfmisc_1 :::":]"::: ) )) & (Bool (Set ($#k9_xtuple_0 :::"dom"::: ) (Set (Var "f2"))) ($#r1_tarski :::"c="::: ) (Set ($#k2_zfmisc_1 :::"[:"::: ) (Set (Var "X")) "," (Set (Var "Y")) ($#k2_zfmisc_1 :::":]"::: ) )) & (Bool (Set ($#k3_funct_5 :::"curry'"::: ) (Set (Var "f1"))) ($#r1_hidden :::"="::: ) (Set ($#k3_funct_5 :::"curry'"::: ) (Set (Var "f2"))))) "holds" (Bool (Set (Var "f1")) ($#r1_hidden :::"="::: ) (Set (Var "f2"))))) ; theorem :: FUNCT_5:54 (Bool "for" (Set (Var "X")) "," (Set (Var "Y")) "being" ($#m1_hidden :::"set"::: ) (Bool "for" (Set (Var "f1")) "," (Set (Var "f2")) "being" ($#m1_hidden :::"Function":::) "st" (Bool (Bool (Set ($#k10_xtuple_0 :::"rng"::: ) (Set (Var "f1"))) ($#r1_tarski :::"c="::: ) (Set ($#k4_partfun1 :::"PFuncs"::: ) "(" (Set (Var "X")) "," (Set (Var "Y")) ")" )) & (Bool (Set ($#k10_xtuple_0 :::"rng"::: ) (Set (Var "f2"))) ($#r1_tarski :::"c="::: ) (Set ($#k4_partfun1 :::"PFuncs"::: ) "(" (Set (Var "X")) "," (Set (Var "Y")) ")" )) & (Bool (Bool "not" (Set ($#k1_xboole_0 :::"{}"::: ) ) ($#r2_hidden :::"in"::: ) (Set ($#k10_xtuple_0 :::"rng"::: ) (Set (Var "f1"))))) & (Bool (Bool "not" (Set ($#k1_xboole_0 :::"{}"::: ) ) ($#r2_hidden :::"in"::: ) (Set ($#k10_xtuple_0 :::"rng"::: ) (Set (Var "f2"))))) & (Bool (Set ($#k2_funct_5 :::"uncurry"::: ) (Set (Var "f1"))) ($#r1_hidden :::"="::: ) (Set ($#k2_funct_5 :::"uncurry"::: ) (Set (Var "f2"))))) "holds" (Bool (Set (Var "f1")) ($#r1_hidden :::"="::: ) (Set (Var "f2"))))) ; theorem :: FUNCT_5:55 (Bool "for" (Set (Var "X")) "," (Set (Var "Y")) "being" ($#m1_hidden :::"set"::: ) (Bool "for" (Set (Var "f1")) "," (Set (Var "f2")) "being" ($#m1_hidden :::"Function":::) "st" (Bool (Bool (Set ($#k10_xtuple_0 :::"rng"::: ) (Set (Var "f1"))) ($#r1_tarski :::"c="::: ) (Set ($#k4_partfun1 :::"PFuncs"::: ) "(" (Set (Var "X")) "," (Set (Var "Y")) ")" )) & (Bool (Set ($#k10_xtuple_0 :::"rng"::: ) (Set (Var "f2"))) ($#r1_tarski :::"c="::: ) (Set ($#k4_partfun1 :::"PFuncs"::: ) "(" (Set (Var "X")) "," (Set (Var "Y")) ")" )) & (Bool (Bool "not" (Set ($#k1_xboole_0 :::"{}"::: ) ) ($#r2_hidden :::"in"::: ) (Set ($#k10_xtuple_0 :::"rng"::: ) (Set (Var "f1"))))) & (Bool (Bool "not" (Set ($#k1_xboole_0 :::"{}"::: ) ) ($#r2_hidden :::"in"::: ) (Set ($#k10_xtuple_0 :::"rng"::: ) (Set (Var "f2"))))) & (Bool (Set ($#k4_funct_5 :::"uncurry'"::: ) (Set (Var "f1"))) ($#r1_hidden :::"="::: ) (Set ($#k4_funct_5 :::"uncurry'"::: ) (Set (Var "f2"))))) "holds" (Bool (Set (Var "f1")) ($#r1_hidden :::"="::: ) (Set (Var "f2"))))) ; theorem :: FUNCT_5:56 (Bool "for" (Set (Var "X")) "," (Set (Var "Y")) "," (Set (Var "Z")) "being" ($#m1_hidden :::"set"::: ) "st" (Bool (Bool (Set (Var "X")) ($#r1_tarski :::"c="::: ) (Set (Var "Y")))) "holds" (Bool (Set ($#k1_funct_2 :::"Funcs"::: ) "(" (Set (Var "Z")) "," (Set (Var "X")) ")" ) ($#r1_tarski :::"c="::: ) (Set ($#k1_funct_2 :::"Funcs"::: ) "(" (Set (Var "Z")) "," (Set (Var "Y")) ")" ))) ; theorem :: FUNCT_5:57 (Bool "for" (Set (Var "X")) "being" ($#m1_hidden :::"set"::: ) "holds" (Bool (Set ($#k1_funct_2 :::"Funcs"::: ) "(" (Set ($#k1_xboole_0 :::"{}"::: ) ) "," (Set (Var "X")) ")" ) ($#r1_hidden :::"="::: ) (Set ($#k1_tarski :::"{"::: ) (Set ($#k1_xboole_0 :::"{}"::: ) ) ($#k1_tarski :::"}"::: ) ))) ; theorem :: FUNCT_5:58 (Bool "for" (Set (Var "X")) "," (Set (Var "x")) "being" ($#m1_hidden :::"set"::: ) "holds" (Bool "(" (Bool (Set (Var "X")) "," (Set ($#k1_funct_2 :::"Funcs"::: ) "(" (Set ($#k1_tarski :::"{"::: ) (Set (Var "x")) ($#k1_tarski :::"}"::: ) ) "," (Set (Var "X")) ")" ) ($#r2_wellord2 :::"are_equipotent"::: ) ) & (Bool (Set ($#k1_card_1 :::"card"::: ) (Set (Var "X"))) ($#r1_hidden :::"="::: ) (Set ($#k1_card_1 :::"card"::: ) (Set "(" ($#k1_funct_2 :::"Funcs"::: ) "(" (Set ($#k1_tarski :::"{"::: ) (Set (Var "x")) ($#k1_tarski :::"}"::: ) ) "," (Set (Var "X")) ")" ")" ))) ")" )) ; theorem :: FUNCT_5:59 (Bool "for" (Set (Var "X")) "," (Set (Var "x")) "being" ($#m1_hidden :::"set"::: ) "holds" (Bool (Set ($#k9_funct_2 :::"Funcs"::: ) "(" (Set (Var "X")) "," (Set ($#k1_tarski :::"{"::: ) (Set (Var "x")) ($#k1_tarski :::"}"::: ) ) ")" ) ($#r1_hidden :::"="::: ) (Set ($#k6_domain_1 :::"{"::: ) (Set "(" (Set (Var "X")) ($#k7_funcop_1 :::"-->"::: ) (Set (Var "x")) ")" ) ($#k6_domain_1 :::"}"::: ) ))) ; theorem :: FUNCT_5:60 (Bool "for" (Set (Var "X1")) "," (Set (Var "Y1")) "," (Set (Var "X2")) "," (Set (Var "Y2")) "being" ($#m1_hidden :::"set"::: ) "st" (Bool (Bool (Set (Var "X1")) "," (Set (Var "Y1")) ($#r2_wellord2 :::"are_equipotent"::: ) ) & (Bool (Set (Var "X2")) "," (Set (Var "Y2")) ($#r2_wellord2 :::"are_equipotent"::: ) )) "holds" (Bool "(" (Bool (Set ($#k1_funct_2 :::"Funcs"::: ) "(" (Set (Var "X1")) "," (Set (Var "X2")) ")" ) "," (Set ($#k1_funct_2 :::"Funcs"::: ) "(" (Set (Var "Y1")) "," (Set (Var "Y2")) ")" ) ($#r2_wellord2 :::"are_equipotent"::: ) ) & (Bool (Set ($#k1_card_1 :::"card"::: ) (Set "(" ($#k1_funct_2 :::"Funcs"::: ) "(" (Set (Var "X1")) "," (Set (Var "X2")) ")" ")" )) ($#r1_hidden :::"="::: ) (Set ($#k1_card_1 :::"card"::: ) (Set "(" ($#k1_funct_2 :::"Funcs"::: ) "(" (Set (Var "Y1")) "," (Set (Var "Y2")) ")" ")" ))) ")" )) ; theorem :: FUNCT_5:61 (Bool "for" (Set (Var "X1")) "," (Set (Var "Y1")) "," (Set (Var "X2")) "," (Set (Var "Y2")) "being" ($#m1_hidden :::"set"::: ) "st" (Bool (Bool (Set ($#k1_card_1 :::"card"::: ) (Set (Var "X1"))) ($#r1_hidden :::"="::: ) (Set ($#k1_card_1 :::"card"::: ) (Set (Var "Y1")))) & (Bool (Set ($#k1_card_1 :::"card"::: ) (Set (Var "X2"))) ($#r1_hidden :::"="::: ) (Set ($#k1_card_1 :::"card"::: ) (Set (Var "Y2"))))) "holds" (Bool (Set ($#k1_card_1 :::"card"::: ) (Set "(" ($#k1_funct_2 :::"Funcs"::: ) "(" (Set (Var "X1")) "," (Set (Var "X2")) ")" ")" )) ($#r1_hidden :::"="::: ) (Set ($#k1_card_1 :::"card"::: ) (Set "(" ($#k1_funct_2 :::"Funcs"::: ) "(" (Set (Var "Y1")) "," (Set (Var "Y2")) ")" ")" )))) ; theorem :: FUNCT_5:62 (Bool "for" (Set (Var "X1")) "," (Set (Var "X2")) "," (Set (Var "X")) "being" ($#m1_hidden :::"set"::: ) "st" (Bool (Bool (Set (Var "X1")) ($#r1_xboole_0 :::"misses"::: ) (Set (Var "X2")))) "holds" (Bool "(" (Bool (Set ($#k1_funct_2 :::"Funcs"::: ) "(" (Set "(" (Set (Var "X1")) ($#k2_xboole_0 :::"\/"::: ) (Set (Var "X2")) ")" ) "," (Set (Var "X")) ")" ) "," (Set ($#k2_zfmisc_1 :::"[:"::: ) (Set "(" ($#k1_funct_2 :::"Funcs"::: ) "(" (Set (Var "X1")) "," (Set (Var "X")) ")" ")" ) "," (Set "(" ($#k1_funct_2 :::"Funcs"::: ) "(" (Set (Var "X2")) "," (Set (Var "X")) ")" ")" ) ($#k2_zfmisc_1 :::":]"::: ) ) ($#r2_wellord2 :::"are_equipotent"::: ) ) & (Bool (Set ($#k1_card_1 :::"card"::: ) (Set "(" ($#k1_funct_2 :::"Funcs"::: ) "(" (Set "(" (Set (Var "X1")) ($#k2_xboole_0 :::"\/"::: ) (Set (Var "X2")) ")" ) "," (Set (Var "X")) ")" ")" )) ($#r1_hidden :::"="::: ) (Set ($#k1_card_1 :::"card"::: ) (Set ($#k2_zfmisc_1 :::"[:"::: ) (Set "(" ($#k1_funct_2 :::"Funcs"::: ) "(" (Set (Var "X1")) "," (Set (Var "X")) ")" ")" ) "," (Set "(" ($#k1_funct_2 :::"Funcs"::: ) "(" (Set (Var "X2")) "," (Set (Var "X")) ")" ")" ) ($#k2_zfmisc_1 :::":]"::: ) ))) ")" )) ; theorem :: FUNCT_5:63 (Bool "for" (Set (Var "X")) "," (Set (Var "Y")) "," (Set (Var "Z")) "being" ($#m1_hidden :::"set"::: ) "holds" (Bool "(" (Bool (Set ($#k1_funct_2 :::"Funcs"::: ) "(" (Set ($#k2_zfmisc_1 :::"[:"::: ) (Set (Var "X")) "," (Set (Var "Y")) ($#k2_zfmisc_1 :::":]"::: ) ) "," (Set (Var "Z")) ")" ) "," (Set ($#k1_funct_2 :::"Funcs"::: ) "(" (Set (Var "X")) "," (Set "(" ($#k1_funct_2 :::"Funcs"::: ) "(" (Set (Var "Y")) "," (Set (Var "Z")) ")" ")" ) ")" ) ($#r2_wellord2 :::"are_equipotent"::: ) ) & (Bool (Set ($#k1_card_1 :::"card"::: ) (Set "(" ($#k1_funct_2 :::"Funcs"::: ) "(" (Set ($#k2_zfmisc_1 :::"[:"::: ) (Set (Var "X")) "," (Set (Var "Y")) ($#k2_zfmisc_1 :::":]"::: ) ) "," (Set (Var "Z")) ")" ")" )) ($#r1_hidden :::"="::: ) (Set ($#k1_card_1 :::"card"::: ) (Set "(" ($#k1_funct_2 :::"Funcs"::: ) "(" (Set (Var "X")) "," (Set "(" ($#k1_funct_2 :::"Funcs"::: ) "(" (Set (Var "Y")) "," (Set (Var "Z")) ")" ")" ) ")" ")" ))) ")" )) ; theorem :: FUNCT_5:64 (Bool "for" (Set (Var "Z")) "," (Set (Var "X")) "," (Set (Var "Y")) "being" ($#m1_hidden :::"set"::: ) "holds" (Bool "(" (Bool (Set ($#k1_funct_2 :::"Funcs"::: ) "(" (Set (Var "Z")) "," (Set ($#k2_zfmisc_1 :::"[:"::: ) (Set (Var "X")) "," (Set (Var "Y")) ($#k2_zfmisc_1 :::":]"::: ) ) ")" ) "," (Set ($#k2_zfmisc_1 :::"[:"::: ) (Set "(" ($#k1_funct_2 :::"Funcs"::: ) "(" (Set (Var "Z")) "," (Set (Var "X")) ")" ")" ) "," (Set "(" ($#k1_funct_2 :::"Funcs"::: ) "(" (Set (Var "Z")) "," (Set (Var "Y")) ")" ")" ) ($#k2_zfmisc_1 :::":]"::: ) ) ($#r2_wellord2 :::"are_equipotent"::: ) ) & (Bool (Set ($#k1_card_1 :::"card"::: ) (Set "(" ($#k1_funct_2 :::"Funcs"::: ) "(" (Set (Var "Z")) "," (Set ($#k2_zfmisc_1 :::"[:"::: ) (Set (Var "X")) "," (Set (Var "Y")) ($#k2_zfmisc_1 :::":]"::: ) ) ")" ")" )) ($#r1_hidden :::"="::: ) (Set ($#k1_card_1 :::"card"::: ) (Set ($#k2_zfmisc_1 :::"[:"::: ) (Set "(" ($#k1_funct_2 :::"Funcs"::: ) "(" (Set (Var "Z")) "," (Set (Var "X")) ")" ")" ) "," (Set "(" ($#k1_funct_2 :::"Funcs"::: ) "(" (Set (Var "Z")) "," (Set (Var "Y")) ")" ")" ) ($#k2_zfmisc_1 :::":]"::: ) ))) ")" )) ; theorem :: FUNCT_5:65 (Bool "for" (Set (Var "x")) "," (Set (Var "y")) "," (Set (Var "X")) "being" ($#m1_hidden :::"set"::: ) "st" (Bool (Bool (Set (Var "x")) ($#r1_hidden :::"<>"::: ) (Set (Var "y")))) "holds" (Bool "(" (Bool (Set ($#k9_funct_2 :::"Funcs"::: ) "(" (Set (Var "X")) "," (Set ($#k2_tarski :::"{"::: ) (Set (Var "x")) "," (Set (Var "y")) ($#k2_tarski :::"}"::: ) ) ")" ) "," (Set ($#k1_zfmisc_1 :::"bool"::: ) (Set (Var "X"))) ($#r2_wellord2 :::"are_equipotent"::: ) ) & (Bool (Set ($#k1_card_1 :::"card"::: ) (Set "(" ($#k9_funct_2 :::"Funcs"::: ) "(" (Set (Var "X")) "," (Set ($#k2_tarski :::"{"::: ) (Set (Var "x")) "," (Set (Var "y")) ($#k2_tarski :::"}"::: ) ) ")" ")" )) ($#r1_hidden :::"="::: ) (Set ($#k1_card_1 :::"card"::: ) (Set "(" ($#k1_zfmisc_1 :::"bool"::: ) (Set (Var "X")) ")" ))) ")" )) ; theorem :: FUNCT_5:66 (Bool "for" (Set (Var "x")) "," (Set (Var "y")) "," (Set (Var "X")) "being" ($#m1_hidden :::"set"::: ) "st" (Bool (Bool (Set (Var "x")) ($#r1_hidden :::"<>"::: ) (Set (Var "y")))) "holds" (Bool "(" (Bool (Set ($#k1_funct_2 :::"Funcs"::: ) "(" (Set ($#k2_tarski :::"{"::: ) (Set (Var "x")) "," (Set (Var "y")) ($#k2_tarski :::"}"::: ) ) "," (Set (Var "X")) ")" ) "," (Set ($#k2_zfmisc_1 :::"[:"::: ) (Set (Var "X")) "," (Set (Var "X")) ($#k2_zfmisc_1 :::":]"::: ) ) ($#r2_wellord2 :::"are_equipotent"::: ) ) & (Bool (Set ($#k1_card_1 :::"card"::: ) (Set "(" ($#k1_funct_2 :::"Funcs"::: ) "(" (Set ($#k2_tarski :::"{"::: ) (Set (Var "x")) "," (Set (Var "y")) ($#k2_tarski :::"}"::: ) ) "," (Set (Var "X")) ")" ")" )) ($#r1_hidden :::"="::: ) (Set ($#k1_card_1 :::"card"::: ) (Set ($#k2_zfmisc_1 :::"[:"::: ) (Set (Var "X")) "," (Set (Var "X")) ($#k2_zfmisc_1 :::":]"::: ) ))) ")" )) ; begin notationsynonym :::"op0"::: for :::"0"::: ; end; definition:: original: :::"op0"::: redefine func :::"op0"::: -> ($#m1_subset_1 :::"Element"::: ) "of" (Num 1); end; definitionfunc :::"op1"::: -> ($#m1_hidden :::"set"::: ) equals :: FUNCT_5:def 5 (Set (Set ($#k1_xboole_0 :::"0"::: ) ) ($#k16_funcop_1 :::".-->"::: ) (Set ($#k1_xboole_0 :::"0"::: ) )); func :::"op2"::: -> ($#m1_hidden :::"set"::: ) equals :: FUNCT_5:def 6 (Set "(" (Set ($#k1_xboole_0 :::"0"::: ) ) "," (Set ($#k1_xboole_0 :::"0"::: ) ) ")" ($#k17_funcop_1 :::":->"::: ) (Set ($#k1_xboole_0 :::"0"::: ) )); end; :: deftheorem defines :::"op1"::: FUNCT_5:def 5 : (Bool (Set ($#k6_funct_5 :::"op1"::: ) ) ($#r1_hidden :::"="::: ) (Set (Set ($#k1_xboole_0 :::"0"::: ) ) ($#k16_funcop_1 :::".-->"::: ) (Set ($#k1_xboole_0 :::"0"::: ) ))); :: deftheorem defines :::"op2"::: FUNCT_5:def 6 : (Bool (Set ($#k7_funct_5 :::"op2"::: ) ) ($#r1_hidden :::"="::: ) (Set "(" (Set ($#k1_xboole_0 :::"0"::: ) ) "," (Set ($#k1_xboole_0 :::"0"::: ) ) ")" ($#k17_funcop_1 :::":->"::: ) (Set ($#k1_xboole_0 :::"0"::: ) ))); definition:: original: :::"op1"::: redefine func :::"op1"::: -> ($#m1_subset_1 :::"UnOp":::) "of" (Num 1); :: original: :::"op2"::: redefine func :::"op2"::: -> ($#m1_subset_1 :::"BinOp":::) "of" (Num 1); end; definitionlet "D" be ($#~v1_xboole_0 "non" ($#v1_xboole_0 :::"empty"::: ) ) ($#m1_hidden :::"set"::: ) ; let "X" be ($#m1_hidden :::"set"::: ) ; let "E" be ($#~v1_xboole_0 "non" ($#v1_xboole_0 :::"empty"::: ) ) ($#m1_hidden :::"set"::: ) ; let "F" be ($#m1_funct_2 :::"FUNCTION_DOMAIN"::: ) "of" (Set (Const "X")) "," (Set (Const "E")); let "f" be ($#m1_subset_1 :::"Function":::) "of" (Set (Const "D")) "," (Set (Const "F")); let "d" be ($#m1_subset_1 :::"Element"::: ) "of" (Set (Const "D")); :: original: :::"."::: redefine func "f" :::"."::: "d" -> ($#m2_funct_2 :::"Element"::: ) "of" "F"; end; theorem :: FUNCT_5:67 (Bool "for" (Set (Var "C")) "," (Set (Var "D")) "," (Set (Var "E")) "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 "C")) "," (Set (Var "D")) ($#k2_zfmisc_1 :::":]"::: ) ) "," (Set (Var "E")) "holds" (Bool (Set ($#k1_funct_5 :::"curry"::: ) (Set (Var "f"))) "is" ($#m1_subset_1 :::"Function":::) "of" (Set (Var "C")) "," (Set "(" ($#k9_funct_2 :::"Funcs"::: ) "(" (Set (Var "D")) "," (Set (Var "E")) ")" ")" )))) ; theorem :: FUNCT_5:68 (Bool "for" (Set (Var "D")) "," (Set (Var "C")) "," (Set (Var "E")) "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 "C")) "," (Set (Var "D")) ($#k2_zfmisc_1 :::":]"::: ) ) "," (Set (Var "E")) "holds" (Bool (Set ($#k3_funct_5 :::"curry'"::: ) (Set (Var "f"))) "is" ($#m1_subset_1 :::"Function":::) "of" (Set (Var "D")) "," (Set "(" ($#k9_funct_2 :::"Funcs"::: ) "(" (Set (Var "C")) "," (Set (Var "E")) ")" ")" )))) ; definitionlet "C", "D", "E" be ($#~v1_xboole_0 "non" ($#v1_xboole_0 :::"empty"::: ) ) ($#m1_hidden :::"set"::: ) ; let "f" be ($#m1_subset_1 :::"Function":::) "of" (Set ($#k2_zfmisc_1 :::"[:"::: ) (Set (Const "C")) "," (Set (Const "D")) ($#k2_zfmisc_1 :::":]"::: ) ) "," (Set (Const "E")); :: original: :::"curry"::: redefine func :::"curry"::: "f" -> ($#m1_subset_1 :::"Function":::) "of" "C" "," (Set "(" ($#k9_funct_2 :::"Funcs"::: ) "(" "D" "," "E" ")" ")" ); :: original: :::"curry'"::: redefine func :::"curry'"::: "f" -> ($#m1_subset_1 :::"Function":::) "of" "D" "," (Set "(" ($#k9_funct_2 :::"Funcs"::: ) "(" "C" "," "E" ")" ")" ); end; theorem :: FUNCT_5:69 (Bool "for" (Set (Var "C")) "," (Set (Var "D")) "," (Set (Var "E")) "being" ($#~v1_xboole_0 "non" ($#v1_xboole_0 :::"empty"::: ) ) ($#m1_hidden :::"set"::: ) (Bool "for" (Set (Var "c")) "being" ($#m1_subset_1 :::"Element"::: ) "of" (Set (Var "C")) (Bool "for" (Set (Var "d")) "being" ($#m1_subset_1 :::"Element"::: ) "of" (Set (Var "D")) (Bool "for" (Set (Var "f")) "being" ($#m1_subset_1 :::"Function":::) "of" (Set ($#k2_zfmisc_1 :::"[:"::: ) (Set (Var "C")) "," (Set (Var "D")) ($#k2_zfmisc_1 :::":]"::: ) ) "," (Set (Var "E")) "holds" (Bool (Set (Set (Var "f")) ($#k2_binop_1 :::"."::: ) "(" (Set (Var "c")) "," (Set (Var "d")) ")" ) ($#r1_hidden :::"="::: ) (Set (Set "(" (Set "(" ($#k11_funct_5 :::"curry"::: ) (Set (Var "f")) ")" ) ($#k10_funct_5 :::"."::: ) (Set (Var "c")) ")" ) ($#k3_funct_2 :::"."::: ) (Set (Var "d")))))))) ; theorem :: FUNCT_5:70 (Bool "for" (Set (Var "C")) "," (Set (Var "D")) "," (Set (Var "E")) "being" ($#~v1_xboole_0 "non" ($#v1_xboole_0 :::"empty"::: ) ) ($#m1_hidden :::"set"::: ) (Bool "for" (Set (Var "c")) "being" ($#m1_subset_1 :::"Element"::: ) "of" (Set (Var "C")) (Bool "for" (Set (Var "d")) "being" ($#m1_subset_1 :::"Element"::: ) "of" (Set (Var "D")) (Bool "for" (Set (Var "f")) "being" ($#m1_subset_1 :::"Function":::) "of" (Set ($#k2_zfmisc_1 :::"[:"::: ) (Set (Var "C")) "," (Set (Var "D")) ($#k2_zfmisc_1 :::":]"::: ) ) "," (Set (Var "E")) "holds" (Bool (Set (Set (Var "f")) ($#k2_binop_1 :::"."::: ) "(" (Set (Var "c")) "," (Set (Var "d")) ")" ) ($#r1_hidden :::"="::: ) (Set (Set "(" (Set "(" ($#k12_funct_5 :::"curry'"::: ) (Set (Var "f")) ")" ) ($#k10_funct_5 :::"."::: ) (Set (Var "d")) ")" ) ($#k3_funct_2 :::"."::: ) (Set (Var "c")))))))) ; definitionlet "A", "B", "C" be ($#~v1_xboole_0 "non" ($#v1_xboole_0 :::"empty"::: ) ) ($#m1_hidden :::"set"::: ) ; let "f" be ($#m1_subset_1 :::"Function":::) "of" (Set (Const "A")) "," (Set "(" ($#k9_funct_2 :::"Funcs"::: ) "(" (Set (Const "B")) "," (Set (Const "C")) ")" ")" ); :: original: :::"uncurry"::: redefine func :::"uncurry"::: "f" -> ($#m1_subset_1 :::"Function":::) "of" (Set ($#k2_zfmisc_1 :::"[:"::: ) "A" "," "B" ($#k2_zfmisc_1 :::":]"::: ) ) "," "C"; end; theorem :: FUNCT_5:71 (Bool "for" (Set (Var "A")) "," (Set (Var "B")) "," (Set (Var "C")) "being" ($#~v1_xboole_0 "non" ($#v1_xboole_0 :::"empty"::: ) ) ($#m1_hidden :::"set"::: ) (Bool "for" (Set (Var "f")) "being" ($#m1_subset_1 :::"Function":::) "of" (Set (Var "A")) "," (Set "(" ($#k9_funct_2 :::"Funcs"::: ) "(" (Set (Var "B")) "," (Set (Var "C")) ")" ")" ) "holds" (Bool (Set ($#k11_funct_5 :::"curry"::: ) (Set "(" ($#k13_funct_5 :::"uncurry"::: ) (Set (Var "f")) ")" )) ($#r2_funct_2 :::"="::: ) (Set (Var "f"))))) ; theorem :: FUNCT_5:72 (Bool "for" (Set (Var "A")) "," (Set (Var "B")) "," (Set (Var "C")) "being" ($#~v1_xboole_0 "non" ($#v1_xboole_0 :::"empty"::: ) ) ($#m1_hidden :::"set"::: ) (Bool "for" (Set (Var "f")) "being" ($#m1_subset_1 :::"Function":::) "of" (Set (Var "A")) "," (Set "(" ($#k9_funct_2 :::"Funcs"::: ) "(" (Set (Var "B")) "," (Set (Var "C")) ")" ")" ) (Bool "for" (Set (Var "a")) "being" ($#m1_subset_1 :::"Element"::: ) "of" (Set (Var "A")) (Bool "for" (Set (Var "b")) "being" ($#m1_subset_1 :::"Element"::: ) "of" (Set (Var "B")) "holds" (Bool (Set (Set "(" ($#k13_funct_5 :::"uncurry"::: ) (Set (Var "f")) ")" ) ($#k2_binop_1 :::"."::: ) "(" (Set (Var "a")) "," (Set (Var "b")) ")" ) ($#r1_hidden :::"="::: ) (Set (Set "(" (Set (Var "f")) ($#k10_funct_5 :::"."::: ) (Set (Var "a")) ")" ) ($#k3_funct_2 :::"."::: ) (Set (Var "b")))))))) ;