:: PARTFUN1 semantic presentation begin theorem :: PARTFUN1:1 (Bool "for" (Set (Var "f")) "," (Set (Var "g")) "being" ($#m1_hidden :::"Function":::) "st" (Bool (Bool "(" "for" (Set (Var "x")) "being" ($#m1_hidden :::"set"::: ) "st" (Bool (Bool (Set (Var "x")) ($#r2_hidden :::"in"::: ) (Set (Set "(" ($#k9_xtuple_0 :::"dom"::: ) (Set (Var "f")) ")" ) ($#k3_xboole_0 :::"/\"::: ) (Set "(" ($#k9_xtuple_0 :::"dom"::: ) (Set (Var "g")) ")" )))) "holds" (Bool (Set (Set (Var "f")) ($#k1_funct_1 :::"."::: ) (Set (Var "x"))) ($#r1_hidden :::"="::: ) (Set (Set (Var "g")) ($#k1_funct_1 :::"."::: ) (Set (Var "x")))) ")" )) "holds" (Bool "ex" (Set (Var "h")) "being" ($#m1_hidden :::"Function":::) "st" (Bool (Set (Set (Var "f")) ($#k2_xboole_0 :::"\/"::: ) (Set (Var "g"))) ($#r1_hidden :::"="::: ) (Set (Var "h"))))) ; theorem :: PARTFUN1:2 (Bool "for" (Set (Var "f")) "," (Set (Var "g")) "," (Set (Var "h")) "being" ($#m1_hidden :::"Function":::) "st" (Bool (Bool (Set (Set (Var "f")) ($#k2_xboole_0 :::"\/"::: ) (Set (Var "g"))) ($#r1_hidden :::"="::: ) (Set (Var "h")))) "holds" (Bool "for" (Set (Var "x")) "being" ($#m1_hidden :::"set"::: ) "st" (Bool (Bool (Set (Var "x")) ($#r2_hidden :::"in"::: ) (Set (Set "(" ($#k9_xtuple_0 :::"dom"::: ) (Set (Var "f")) ")" ) ($#k3_xboole_0 :::"/\"::: ) (Set "(" ($#k9_xtuple_0 :::"dom"::: ) (Set (Var "g")) ")" )))) "holds" (Bool (Set (Set (Var "f")) ($#k1_funct_1 :::"."::: ) (Set (Var "x"))) ($#r1_hidden :::"="::: ) (Set (Set (Var "g")) ($#k1_funct_1 :::"."::: ) (Set (Var "x")))))) ; scheme :: PARTFUN1:sch 1 LambdaC{ F1() -> ($#m1_hidden :::"set"::: ) , P1[ ($#m1_hidden :::"set"::: ) ], F2( ($#m1_hidden :::"set"::: ) ) -> ($#m1_hidden :::"set"::: ) , F3( ($#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 "x")) "being" ($#m1_hidden :::"set"::: ) "st" (Bool (Bool (Set (Var "x")) ($#r2_hidden :::"in"::: ) (Set F1 "(" ")" ))) "holds" (Bool "(" "(" (Bool (Bool P1[(Set (Var "x"))])) "implies" (Bool (Set (Set (Var "f")) ($#k1_funct_1 :::"."::: ) (Set (Var "x"))) ($#r1_hidden :::"="::: ) (Set F2 "(" (Set (Var "x")) ")" )) ")" & "(" (Bool (Bool P1[(Set (Var "x"))])) "implies" (Bool (Set (Set (Var "f")) ($#k1_funct_1 :::"."::: ) (Set (Var "x"))) ($#r1_hidden :::"="::: ) (Set F3 "(" (Set (Var "x")) ")" )) ")" ")" ) ")" ) ")" )) proof end; registrationlet "X", "Y" be ($#m1_hidden :::"set"::: ) ; cluster ($#v1_relat_1 :::"Relation-like"::: ) "X" ($#v4_relat_1 :::"-defined"::: ) "Y" ($#v5_relat_1 :::"-valued"::: ) ($#v1_funct_1 :::"Function-like"::: ) for ($#m1_subset_1 :::"Element"::: ) "of" (Set ($#k1_zfmisc_1 :::"bool"::: ) (Set ($#k2_zfmisc_1 :::"[:"::: ) "X" "," "Y" ($#k2_zfmisc_1 :::":]"::: ) )); end; definitionlet "X", "Y" be ($#m1_hidden :::"set"::: ) ; mode PartFunc of "X" "," "Y" is ($#v1_funct_1 :::"Function-like"::: ) ($#m1_subset_1 :::"Relation":::) "of" "X" "," "Y"; end; theorem :: PARTFUN1:3 (Bool "for" (Set (Var "X")) "," (Set (Var "Y")) "," (Set (Var "y")) "being" ($#m1_hidden :::"set"::: ) (Bool "for" (Set (Var "f")) "being" ($#m1_subset_1 :::"PartFunc":::) "of" (Set (Var "X")) "," (Set (Var "Y")) "st" (Bool (Bool (Set (Var "y")) ($#r2_hidden :::"in"::: ) (Set ($#k10_xtuple_0 :::"rng"::: ) (Set (Var "f"))))) "holds" (Bool "ex" (Set (Var "x")) "being" ($#m1_subset_1 :::"Element"::: ) "of" (Set (Var "X")) "st" (Bool "(" (Bool (Set (Var "x")) ($#r2_hidden :::"in"::: ) (Set ($#k1_relset_1 :::"dom"::: ) (Set (Var "f")))) & (Bool (Set (Var "y")) ($#r1_hidden :::"="::: ) (Set (Set (Var "f")) ($#k1_funct_1 :::"."::: ) (Set (Var "x")))) ")" )))) ; theorem :: PARTFUN1:4 (Bool "for" (Set (Var "Y")) "," (Set (Var "x")) "being" ($#m1_hidden :::"set"::: ) (Bool "for" (Set (Var "f")) "being" (Set (Var "b1")) ($#v5_relat_1 :::"-valued"::: ) ($#m1_hidden :::"Function":::) "st" (Bool (Bool (Set (Var "x")) ($#r2_hidden :::"in"::: ) (Set ($#k9_xtuple_0 :::"dom"::: ) (Set (Var "f"))))) "holds" (Bool (Set (Set (Var "f")) ($#k1_funct_1 :::"."::: ) (Set (Var "x"))) ($#r2_hidden :::"in"::: ) (Set (Var "Y"))))) ; theorem :: PARTFUN1:5 (Bool "for" (Set (Var "X")) "," (Set (Var "Y")) "being" ($#m1_hidden :::"set"::: ) (Bool "for" (Set (Var "f1")) "," (Set (Var "f2")) "being" ($#m1_subset_1 :::"PartFunc":::) "of" (Set (Var "X")) "," (Set (Var "Y")) "st" (Bool (Bool (Set ($#k1_relset_1 :::"dom"::: ) (Set (Var "f1"))) ($#r1_hidden :::"="::: ) (Set ($#k1_relset_1 :::"dom"::: ) (Set (Var "f2")))) & (Bool "(" "for" (Set (Var "x")) "being" ($#m1_subset_1 :::"Element"::: ) "of" (Set (Var "X")) "st" (Bool (Bool (Set (Var "x")) ($#r2_hidden :::"in"::: ) (Set ($#k1_relset_1 :::"dom"::: ) (Set (Var "f1"))))) "holds" (Bool (Set (Set (Var "f1")) ($#k1_funct_1 :::"."::: ) (Set (Var "x"))) ($#r1_hidden :::"="::: ) (Set (Set (Var "f2")) ($#k1_funct_1 :::"."::: ) (Set (Var "x")))) ")" )) "holds" (Bool (Set (Var "f1")) ($#r1_hidden :::"="::: ) (Set (Var "f2"))))) ; scheme :: PARTFUN1:sch 2 PartFuncEx{ F1() -> ($#m1_hidden :::"set"::: ) , F2() -> ($#m1_hidden :::"set"::: ) , P1[ ($#m1_hidden :::"set"::: ) "," ($#m1_hidden :::"set"::: ) ] } : (Bool "ex" (Set (Var "f")) "being" ($#m1_subset_1 :::"PartFunc":::) "of" (Set F1 "(" ")" ) "," (Set F2 "(" ")" ) "st" (Bool "(" (Bool "(" "for" (Set (Var "x")) "being" ($#m1_hidden :::"set"::: ) "holds" (Bool "(" (Bool (Set (Var "x")) ($#r2_hidden :::"in"::: ) (Set ($#k1_relset_1 :::"dom"::: ) (Set (Var "f")))) "iff" (Bool "(" (Bool (Set (Var "x")) ($#r2_hidden :::"in"::: ) (Set F1 "(" ")" )) & (Bool "ex" (Set (Var "y")) "being" ($#m1_hidden :::"set"::: ) "st" (Bool P1[(Set (Var "x")) "," (Set (Var "y"))])) ")" ) ")" ) ")" ) & (Bool "(" "for" (Set (Var "x")) "being" ($#m1_hidden :::"set"::: ) "st" (Bool (Bool (Set (Var "x")) ($#r2_hidden :::"in"::: ) (Set ($#k1_relset_1 :::"dom"::: ) (Set (Var "f"))))) "holds" (Bool P1[(Set (Var "x")) "," (Set (Set (Var "f")) ($#k1_funct_1 :::"."::: ) (Set (Var "x")))]) ")" ) ")" )) provided (Bool "for" (Set (Var "x")) "," (Set (Var "y")) "being" ($#m1_hidden :::"set"::: ) "st" (Bool (Bool (Set (Var "x")) ($#r2_hidden :::"in"::: ) (Set F1 "(" ")" )) & (Bool P1[(Set (Var "x")) "," (Set (Var "y"))])) "holds" (Bool (Set (Var "y")) ($#r2_hidden :::"in"::: ) (Set F2 "(" ")" ))) and (Bool "for" (Set (Var "x")) "," (Set (Var "y1")) "," (Set (Var "y2")) "being" ($#m1_hidden :::"set"::: ) "st" (Bool (Bool (Set (Var "x")) ($#r2_hidden :::"in"::: ) (Set F1 "(" ")" )) & (Bool P1[(Set (Var "x")) "," (Set (Var "y1"))]) & (Bool P1[(Set (Var "x")) "," (Set (Var "y2"))])) "holds" (Bool (Set (Var "y1")) ($#r1_hidden :::"="::: ) (Set (Var "y2")))) proof end; scheme :: PARTFUN1:sch 3 LambdaR{ F1() -> ($#m1_hidden :::"set"::: ) , F2() -> ($#m1_hidden :::"set"::: ) , F3( ($#m1_hidden :::"set"::: ) ) -> ($#m1_hidden :::"set"::: ) , P1[ ($#m1_hidden :::"set"::: ) ] } : (Bool "ex" (Set (Var "f")) "being" ($#m1_subset_1 :::"PartFunc":::) "of" (Set F1 "(" ")" ) "," (Set F2 "(" ")" ) "st" (Bool "(" (Bool "(" "for" (Set (Var "x")) "being" ($#m1_hidden :::"set"::: ) "holds" (Bool "(" (Bool (Set (Var "x")) ($#r2_hidden :::"in"::: ) (Set ($#k1_relset_1 :::"dom"::: ) (Set (Var "f")))) "iff" (Bool "(" (Bool (Set (Var "x")) ($#r2_hidden :::"in"::: ) (Set F1 "(" ")" )) & (Bool P1[(Set (Var "x"))]) ")" ) ")" ) ")" ) & (Bool "(" "for" (Set (Var "x")) "being" ($#m1_hidden :::"set"::: ) "st" (Bool (Bool (Set (Var "x")) ($#r2_hidden :::"in"::: ) (Set ($#k1_relset_1 :::"dom"::: ) (Set (Var "f"))))) "holds" (Bool (Set (Set (Var "f")) ($#k1_funct_1 :::"."::: ) (Set (Var "x"))) ($#r1_hidden :::"="::: ) (Set F3 "(" (Set (Var "x")) ")" )) ")" ) ")" )) provided (Bool "for" (Set (Var "x")) "being" ($#m1_hidden :::"set"::: ) "st" (Bool (Bool P1[(Set (Var "x"))])) "holds" (Bool (Set F3 "(" (Set (Var "x")) ")" ) ($#r2_hidden :::"in"::: ) (Set F2 "(" ")" ))) proof end; definitionlet "X", "Y", "V", "Z" be ($#m1_hidden :::"set"::: ) ; let "f" be ($#m1_subset_1 :::"PartFunc":::) "of" (Set (Const "X")) "," (Set (Const "Y")); let "g" be ($#m1_subset_1 :::"PartFunc":::) "of" (Set (Const "V")) "," (Set (Const "Z")); :: original: :::"*"::: redefine func "g" :::"*"::: "f" -> ($#m1_subset_1 :::"PartFunc":::) "of" "X" "," "Z"; end; theorem :: PARTFUN1:6 (Bool "for" (Set (Var "X")) "," (Set (Var "Y")) "being" ($#m1_hidden :::"set"::: ) (Bool "for" (Set (Var "f")) "being" ($#m1_subset_1 :::"Relation":::) "of" (Set (Var "X")) "," (Set (Var "Y")) "holds" (Bool (Set (Set "(" ($#k4_relat_1 :::"id"::: ) (Set (Var "X")) ")" ) ($#k3_relat_1 :::"*"::: ) (Set (Var "f"))) ($#r1_hidden :::"="::: ) (Set (Var "f"))))) ; theorem :: PARTFUN1:7 (Bool "for" (Set (Var "X")) "," (Set (Var "Y")) "being" ($#m1_hidden :::"set"::: ) (Bool "for" (Set (Var "f")) "being" ($#m1_subset_1 :::"Relation":::) "of" (Set (Var "X")) "," (Set (Var "Y")) "holds" (Bool (Set (Set (Var "f")) ($#k3_relat_1 :::"*"::: ) (Set "(" ($#k4_relat_1 :::"id"::: ) (Set (Var "Y")) ")" )) ($#r1_hidden :::"="::: ) (Set (Var "f"))))) ; theorem :: PARTFUN1:8 (Bool "for" (Set (Var "X")) "," (Set (Var "Y")) "being" ($#m1_hidden :::"set"::: ) (Bool "for" (Set (Var "f")) "being" ($#m1_subset_1 :::"PartFunc":::) "of" (Set (Var "X")) "," (Set (Var "Y")) "st" (Bool (Bool "(" "for" (Set (Var "x1")) "," (Set (Var "x2")) "being" ($#m1_subset_1 :::"Element"::: ) "of" (Set (Var "X")) "st" (Bool (Bool (Set (Var "x1")) ($#r2_hidden :::"in"::: ) (Set ($#k1_relset_1 :::"dom"::: ) (Set (Var "f")))) & (Bool (Set (Var "x2")) ($#r2_hidden :::"in"::: ) (Set ($#k1_relset_1 :::"dom"::: ) (Set (Var "f")))) & (Bool (Set (Set (Var "f")) ($#k1_funct_1 :::"."::: ) (Set (Var "x1"))) ($#r1_hidden :::"="::: ) (Set (Set (Var "f")) ($#k1_funct_1 :::"."::: ) (Set (Var "x2"))))) "holds" (Bool (Set (Var "x1")) ($#r1_hidden :::"="::: ) (Set (Var "x2"))) ")" )) "holds" (Bool (Set (Var "f")) "is" ($#v2_funct_1 :::"one-to-one"::: ) ))) ; theorem :: PARTFUN1:9 (Bool "for" (Set (Var "X")) "," (Set (Var "Y")) "being" ($#m1_hidden :::"set"::: ) (Bool "for" (Set (Var "f")) "being" ($#m1_subset_1 :::"PartFunc":::) "of" (Set (Var "X")) "," (Set (Var "Y")) "st" (Bool (Bool (Set (Var "f")) "is" ($#v2_funct_1 :::"one-to-one"::: ) )) "holds" (Bool (Set (Set (Var "f")) ($#k2_funct_1 :::"""::: ) ) "is" ($#m1_subset_1 :::"PartFunc":::) "of" (Set (Var "Y")) "," (Set (Var "X"))))) ; theorem :: PARTFUN1:10 (Bool "for" (Set (Var "X")) "," (Set (Var "Y")) "," (Set (Var "Z")) "being" ($#m1_hidden :::"set"::: ) (Bool "for" (Set (Var "f")) "being" ($#m1_subset_1 :::"PartFunc":::) "of" (Set (Var "X")) "," (Set (Var "Y")) "holds" (Bool (Set (Set (Var "f")) ($#k5_relset_1 :::"|"::: ) (Set (Var "Z"))) "is" ($#m1_subset_1 :::"PartFunc":::) "of" (Set (Var "Z")) "," (Set (Var "Y"))))) ; theorem :: PARTFUN1:11 (Bool "for" (Set (Var "X")) "," (Set (Var "Y")) "," (Set (Var "Z")) "being" ($#m1_hidden :::"set"::: ) (Bool "for" (Set (Var "f")) "being" ($#m1_subset_1 :::"PartFunc":::) "of" (Set (Var "X")) "," (Set (Var "Y")) "holds" (Bool (Set (Set (Var "f")) ($#k5_relset_1 :::"|"::: ) (Set (Var "Z"))) "is" ($#m1_subset_1 :::"PartFunc":::) "of" (Set (Var "X")) "," (Set (Var "Y"))))) ; definitionlet "X", "Y" be ($#m1_hidden :::"set"::: ) ; let "f" be ($#m1_subset_1 :::"PartFunc":::) "of" (Set (Const "X")) "," (Set (Const "Y")); let "Z" be ($#m1_hidden :::"set"::: ) ; :: original: :::"|"::: redefine func "f" :::"|"::: "Z" -> ($#m1_subset_1 :::"PartFunc":::) "of" "X" "," "Y"; end; theorem :: PARTFUN1:12 (Bool "for" (Set (Var "X")) "," (Set (Var "Y")) "," (Set (Var "Z")) "being" ($#m1_hidden :::"set"::: ) (Bool "for" (Set (Var "f")) "being" ($#m1_subset_1 :::"PartFunc":::) "of" (Set (Var "X")) "," (Set (Var "Y")) "holds" (Bool (Set (Set (Var "Z")) ($#k6_relset_1 :::"|`"::: ) (Set (Var "f"))) "is" ($#m1_subset_1 :::"PartFunc":::) "of" (Set (Var "X")) "," (Set (Var "Z"))))) ; theorem :: PARTFUN1:13 (Bool "for" (Set (Var "X")) "," (Set (Var "Y")) "," (Set (Var "Z")) "being" ($#m1_hidden :::"set"::: ) (Bool "for" (Set (Var "f")) "being" ($#m1_subset_1 :::"PartFunc":::) "of" (Set (Var "X")) "," (Set (Var "Y")) "holds" (Bool (Set (Set (Var "Z")) ($#k6_relset_1 :::"|`"::: ) (Set (Var "f"))) "is" ($#m1_subset_1 :::"PartFunc":::) "of" (Set (Var "X")) "," (Set (Var "Y"))))) ; theorem :: PARTFUN1:14 (Bool "for" (Set (Var "Y")) "," (Set (Var "X")) "being" ($#m1_hidden :::"set"::: ) (Bool "for" (Set (Var "f")) "being" ($#m1_hidden :::"Function":::) "holds" (Bool (Set (Set "(" (Set (Var "Y")) ($#k6_relat_1 :::"|`"::: ) (Set (Var "f")) ")" ) ($#k5_relat_1 :::"|"::: ) (Set (Var "X"))) "is" ($#m1_subset_1 :::"PartFunc":::) "of" (Set (Var "X")) "," (Set (Var "Y"))))) ; theorem :: PARTFUN1:15 (Bool "for" (Set (Var "X")) "," (Set (Var "Y")) "," (Set (Var "y")) "being" ($#m1_hidden :::"set"::: ) (Bool "for" (Set (Var "f")) "being" ($#m1_subset_1 :::"PartFunc":::) "of" (Set (Var "X")) "," (Set (Var "Y")) "st" (Bool (Bool (Set (Var "y")) ($#r2_hidden :::"in"::: ) (Set (Set (Var "f")) ($#k7_relat_1 :::".:"::: ) (Set (Var "X"))))) "holds" (Bool "ex" (Set (Var "x")) "being" ($#m1_subset_1 :::"Element"::: ) "of" (Set (Var "X")) "st" (Bool "(" (Bool (Set (Var "x")) ($#r2_hidden :::"in"::: ) (Set ($#k1_relset_1 :::"dom"::: ) (Set (Var "f")))) & (Bool (Set (Var "y")) ($#r1_hidden :::"="::: ) (Set (Set (Var "f")) ($#k1_funct_1 :::"."::: ) (Set (Var "x")))) ")" )))) ; theorem :: PARTFUN1:16 (Bool "for" (Set (Var "x")) "," (Set (Var "Y")) "being" ($#m1_hidden :::"set"::: ) (Bool "for" (Set (Var "f")) "being" ($#m1_subset_1 :::"PartFunc":::) "of" (Set ($#k1_tarski :::"{"::: ) (Set (Var "x")) ($#k1_tarski :::"}"::: ) ) "," (Set (Var "Y")) "holds" (Bool (Set ($#k10_xtuple_0 :::"rng"::: ) (Set (Var "f"))) ($#r1_tarski :::"c="::: ) (Set ($#k1_tarski :::"{"::: ) (Set "(" (Set (Var "f")) ($#k1_funct_1 :::"."::: ) (Set (Var "x")) ")" ) ($#k1_tarski :::"}"::: ) )))) ; theorem :: PARTFUN1:17 (Bool "for" (Set (Var "x")) "," (Set (Var "Y")) "being" ($#m1_hidden :::"set"::: ) (Bool "for" (Set (Var "f")) "being" ($#m1_subset_1 :::"PartFunc":::) "of" (Set ($#k1_tarski :::"{"::: ) (Set (Var "x")) ($#k1_tarski :::"}"::: ) ) "," (Set (Var "Y")) "holds" (Bool (Set (Var "f")) "is" ($#v2_funct_1 :::"one-to-one"::: ) ))) ; theorem :: PARTFUN1:18 (Bool "for" (Set (Var "x")) "," (Set (Var "Y")) "," (Set (Var "P")) "being" ($#m1_hidden :::"set"::: ) (Bool "for" (Set (Var "f")) "being" ($#m1_subset_1 :::"PartFunc":::) "of" (Set ($#k1_tarski :::"{"::: ) (Set (Var "x")) ($#k1_tarski :::"}"::: ) ) "," (Set (Var "Y")) "holds" (Bool (Set (Set (Var "f")) ($#k7_relat_1 :::".:"::: ) (Set (Var "P"))) ($#r1_tarski :::"c="::: ) (Set ($#k1_tarski :::"{"::: ) (Set "(" (Set (Var "f")) ($#k1_funct_1 :::"."::: ) (Set (Var "x")) ")" ) ($#k1_tarski :::"}"::: ) )))) ; theorem :: PARTFUN1:19 (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 ($#k9_xtuple_0 :::"dom"::: ) (Set (Var "f"))) ($#r1_hidden :::"="::: ) (Set ($#k1_tarski :::"{"::: ) (Set (Var "x")) ($#k1_tarski :::"}"::: ) )) & (Bool (Set (Var "x")) ($#r2_hidden :::"in"::: ) (Set (Var "X"))) & (Bool (Set (Set (Var "f")) ($#k1_funct_1 :::"."::: ) (Set (Var "x"))) ($#r2_hidden :::"in"::: ) (Set (Var "Y")))) "holds" (Bool (Set (Var "f")) "is" ($#m1_subset_1 :::"PartFunc":::) "of" (Set (Var "X")) "," (Set (Var "Y"))))) ; theorem :: PARTFUN1:20 (Bool "for" (Set (Var "X")) "," (Set (Var "y")) "," (Set (Var "x")) "being" ($#m1_hidden :::"set"::: ) (Bool "for" (Set (Var "f")) "being" ($#m1_subset_1 :::"PartFunc":::) "of" (Set (Var "X")) "," (Set ($#k1_tarski :::"{"::: ) (Set (Var "y")) ($#k1_tarski :::"}"::: ) ) "st" (Bool (Bool (Set (Var "x")) ($#r2_hidden :::"in"::: ) (Set ($#k1_relset_1 :::"dom"::: ) (Set (Var "f"))))) "holds" (Bool (Set (Set (Var "f")) ($#k1_funct_1 :::"."::: ) (Set (Var "x"))) ($#r1_hidden :::"="::: ) (Set (Var "y"))))) ; theorem :: PARTFUN1:21 (Bool "for" (Set (Var "X")) "," (Set (Var "y")) "being" ($#m1_hidden :::"set"::: ) (Bool "for" (Set (Var "f1")) "," (Set (Var "f2")) "being" ($#m1_subset_1 :::"PartFunc":::) "of" (Set (Var "X")) "," (Set ($#k1_tarski :::"{"::: ) (Set (Var "y")) ($#k1_tarski :::"}"::: ) ) "st" (Bool (Bool (Set ($#k1_relset_1 :::"dom"::: ) (Set (Var "f1"))) ($#r1_hidden :::"="::: ) (Set ($#k1_relset_1 :::"dom"::: ) (Set (Var "f2"))))) "holds" (Bool (Set (Var "f1")) ($#r1_hidden :::"="::: ) (Set (Var "f2"))))) ; definitionlet "f" be ($#m1_hidden :::"Function":::); let "X", "Y" be ($#m1_hidden :::"set"::: ) ; func :::"<:":::"f" "," "X" "," "Y":::":>"::: -> ($#m1_subset_1 :::"PartFunc":::) "of" "X" "," "Y" equals :: PARTFUN1:def 1 (Set (Set "(" "Y" ($#k6_relat_1 :::"|`"::: ) "f" ")" ) ($#k5_relat_1 :::"|"::: ) "X"); end; :: deftheorem defines :::"<:"::: PARTFUN1:def 1 : (Bool "for" (Set (Var "f")) "being" ($#m1_hidden :::"Function":::) (Bool "for" (Set (Var "X")) "," (Set (Var "Y")) "being" ($#m1_hidden :::"set"::: ) "holds" (Bool (Set ($#k3_partfun1 :::"<:"::: ) (Set (Var "f")) "," (Set (Var "X")) "," (Set (Var "Y")) ($#k3_partfun1 :::":>"::: ) ) ($#r1_hidden :::"="::: ) (Set (Set "(" (Set (Var "Y")) ($#k6_relat_1 :::"|`"::: ) (Set (Var "f")) ")" ) ($#k5_relat_1 :::"|"::: ) (Set (Var "X")))))); theorem :: PARTFUN1:22 (Bool "for" (Set (Var "X")) "," (Set (Var "Y")) "being" ($#m1_hidden :::"set"::: ) (Bool "for" (Set (Var "f")) "being" ($#m1_hidden :::"Function":::) "holds" (Bool (Set ($#k3_partfun1 :::"<:"::: ) (Set (Var "f")) "," (Set (Var "X")) "," (Set (Var "Y")) ($#k3_partfun1 :::":>"::: ) ) ($#r1_relset_1 :::"c="::: ) (Set (Var "f"))))) ; theorem :: PARTFUN1:23 (Bool "for" (Set (Var "X")) "," (Set (Var "Y")) "being" ($#m1_hidden :::"set"::: ) (Bool "for" (Set (Var "f")) "being" ($#m1_hidden :::"Function":::) "holds" (Bool "(" (Bool (Set ($#k1_relset_1 :::"dom"::: ) (Set ($#k3_partfun1 :::"<:"::: ) (Set (Var "f")) "," (Set (Var "X")) "," (Set (Var "Y")) ($#k3_partfun1 :::":>"::: ) )) ($#r1_tarski :::"c="::: ) (Set ($#k9_xtuple_0 :::"dom"::: ) (Set (Var "f")))) & (Bool (Set ($#k10_xtuple_0 :::"rng"::: ) (Set ($#k3_partfun1 :::"<:"::: ) (Set (Var "f")) "," (Set (Var "X")) "," (Set (Var "Y")) ($#k3_partfun1 :::":>"::: ) )) ($#r1_tarski :::"c="::: ) (Set ($#k10_xtuple_0 :::"rng"::: ) (Set (Var "f")))) ")" ))) ; theorem :: PARTFUN1:24 (Bool "for" (Set (Var "x")) "," (Set (Var "X")) "," (Set (Var "Y")) "being" ($#m1_hidden :::"set"::: ) (Bool "for" (Set (Var "f")) "being" ($#m1_hidden :::"Function":::) "holds" (Bool "(" (Bool (Set (Var "x")) ($#r2_hidden :::"in"::: ) (Set ($#k1_relset_1 :::"dom"::: ) (Set ($#k3_partfun1 :::"<:"::: ) (Set (Var "f")) "," (Set (Var "X")) "," (Set (Var "Y")) ($#k3_partfun1 :::":>"::: ) ))) "iff" (Bool "(" (Bool (Set (Var "x")) ($#r2_hidden :::"in"::: ) (Set ($#k9_xtuple_0 :::"dom"::: ) (Set (Var "f")))) & (Bool (Set (Var "x")) ($#r2_hidden :::"in"::: ) (Set (Var "X"))) & (Bool (Set (Set (Var "f")) ($#k1_funct_1 :::"."::: ) (Set (Var "x"))) ($#r2_hidden :::"in"::: ) (Set (Var "Y"))) ")" ) ")" ))) ; theorem :: PARTFUN1:25 (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 ($#k9_xtuple_0 :::"dom"::: ) (Set (Var "f")))) & (Bool (Set (Var "x")) ($#r2_hidden :::"in"::: ) (Set (Var "X"))) & (Bool (Set (Set (Var "f")) ($#k1_funct_1 :::"."::: ) (Set (Var "x"))) ($#r2_hidden :::"in"::: ) (Set (Var "Y")))) "holds" (Bool (Set (Set ($#k3_partfun1 :::"<:"::: ) (Set (Var "f")) "," (Set (Var "X")) "," (Set (Var "Y")) ($#k3_partfun1 :::":>"::: ) ) ($#k1_funct_1 :::"."::: ) (Set (Var "x"))) ($#r1_hidden :::"="::: ) (Set (Set (Var "f")) ($#k1_funct_1 :::"."::: ) (Set (Var "x")))))) ; theorem :: PARTFUN1:26 (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 ($#k1_relset_1 :::"dom"::: ) (Set ($#k3_partfun1 :::"<:"::: ) (Set (Var "f")) "," (Set (Var "X")) "," (Set (Var "Y")) ($#k3_partfun1 :::":>"::: ) )))) "holds" (Bool (Set (Set ($#k3_partfun1 :::"<:"::: ) (Set (Var "f")) "," (Set (Var "X")) "," (Set (Var "Y")) ($#k3_partfun1 :::":>"::: ) ) ($#k1_funct_1 :::"."::: ) (Set (Var "x"))) ($#r1_hidden :::"="::: ) (Set (Set (Var "f")) ($#k1_funct_1 :::"."::: ) (Set (Var "x")))))) ; theorem :: PARTFUN1:27 (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 "f")) ($#r1_tarski :::"c="::: ) (Set (Var "g")))) "holds" (Bool (Set ($#k3_partfun1 :::"<:"::: ) (Set (Var "f")) "," (Set (Var "X")) "," (Set (Var "Y")) ($#k3_partfun1 :::":>"::: ) ) ($#r1_relset_1 :::"c="::: ) (Set ($#k3_partfun1 :::"<:"::: ) (Set (Var "g")) "," (Set (Var "X")) "," (Set (Var "Y")) ($#k3_partfun1 :::":>"::: ) )))) ; theorem :: PARTFUN1:28 (Bool "for" (Set (Var "Z")) "," (Set (Var "X")) "," (Set (Var "Y")) "being" ($#m1_hidden :::"set"::: ) (Bool "for" (Set (Var "f")) "being" ($#m1_hidden :::"Function":::) "st" (Bool (Bool (Set (Var "Z")) ($#r1_tarski :::"c="::: ) (Set (Var "X")))) "holds" (Bool (Set ($#k3_partfun1 :::"<:"::: ) (Set (Var "f")) "," (Set (Var "Z")) "," (Set (Var "Y")) ($#k3_partfun1 :::":>"::: ) ) ($#r1_relset_1 :::"c="::: ) (Set ($#k3_partfun1 :::"<:"::: ) (Set (Var "f")) "," (Set (Var "X")) "," (Set (Var "Y")) ($#k3_partfun1 :::":>"::: ) )))) ; theorem :: PARTFUN1:29 (Bool "for" (Set (Var "Z")) "," (Set (Var "Y")) "," (Set (Var "X")) "being" ($#m1_hidden :::"set"::: ) (Bool "for" (Set (Var "f")) "being" ($#m1_hidden :::"Function":::) "st" (Bool (Bool (Set (Var "Z")) ($#r1_tarski :::"c="::: ) (Set (Var "Y")))) "holds" (Bool (Set ($#k3_partfun1 :::"<:"::: ) (Set (Var "f")) "," (Set (Var "X")) "," (Set (Var "Z")) ($#k3_partfun1 :::":>"::: ) ) ($#r1_relset_1 :::"c="::: ) (Set ($#k3_partfun1 :::"<:"::: ) (Set (Var "f")) "," (Set (Var "X")) "," (Set (Var "Y")) ($#k3_partfun1 :::":>"::: ) )))) ; theorem :: PARTFUN1:30 (Bool "for" (Set (Var "X1")) "," (Set (Var "X2")) "," (Set (Var "Y1")) "," (Set (Var "Y2")) "being" ($#m1_hidden :::"set"::: ) (Bool "for" (Set (Var "f")) "being" ($#m1_hidden :::"Function":::) "st" (Bool (Bool (Set (Var "X1")) ($#r1_tarski :::"c="::: ) (Set (Var "X2"))) & (Bool (Set (Var "Y1")) ($#r1_tarski :::"c="::: ) (Set (Var "Y2")))) "holds" (Bool (Set ($#k3_partfun1 :::"<:"::: ) (Set (Var "f")) "," (Set (Var "X1")) "," (Set (Var "Y1")) ($#k3_partfun1 :::":>"::: ) ) ($#r1_relset_1 :::"c="::: ) (Set ($#k3_partfun1 :::"<:"::: ) (Set (Var "f")) "," (Set (Var "X2")) "," (Set (Var "Y2")) ($#k3_partfun1 :::":>"::: ) )))) ; theorem :: PARTFUN1:31 (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 (Var "X"))) & (Bool (Set ($#k10_xtuple_0 :::"rng"::: ) (Set (Var "f"))) ($#r1_tarski :::"c="::: ) (Set (Var "Y")))) "holds" (Bool (Set (Var "f")) ($#r1_hidden :::"="::: ) (Set ($#k3_partfun1 :::"<:"::: ) (Set (Var "f")) "," (Set (Var "X")) "," (Set (Var "Y")) ($#k3_partfun1 :::":>"::: ) )))) ; theorem :: PARTFUN1:32 (Bool "for" (Set (Var "f")) "being" ($#m1_hidden :::"Function":::) "holds" (Bool (Set (Var "f")) ($#r1_hidden :::"="::: ) (Set ($#k3_partfun1 :::"<:"::: ) (Set (Var "f")) "," (Set "(" ($#k9_xtuple_0 :::"dom"::: ) (Set (Var "f")) ")" ) "," (Set "(" ($#k10_xtuple_0 :::"rng"::: ) (Set (Var "f")) ")" ) ($#k3_partfun1 :::":>"::: ) ))) ; theorem :: PARTFUN1:33 (Bool "for" (Set (Var "X")) "," (Set (Var "Y")) "being" ($#m1_hidden :::"set"::: ) (Bool "for" (Set (Var "f")) "being" ($#m1_subset_1 :::"PartFunc":::) "of" (Set (Var "X")) "," (Set (Var "Y")) "holds" (Bool (Set ($#k3_partfun1 :::"<:"::: ) (Set (Var "f")) "," (Set (Var "X")) "," (Set (Var "Y")) ($#k3_partfun1 :::":>"::: ) ) ($#r1_hidden :::"="::: ) (Set (Var "f"))))) ; theorem :: PARTFUN1:34 (Bool "for" (Set (Var "X")) "," (Set (Var "Y")) "being" ($#m1_hidden :::"set"::: ) "holds" (Bool (Set ($#k3_partfun1 :::"<:"::: ) (Set ($#k1_xboole_0 :::"{}"::: ) ) "," (Set (Var "X")) "," (Set (Var "Y")) ($#k3_partfun1 :::":>"::: ) ) ($#r1_hidden :::"="::: ) (Set ($#k1_xboole_0 :::"{}"::: ) ))) ; theorem :: PARTFUN1:35 (Bool "for" (Set (Var "Y")) "," (Set (Var "Z")) "," (Set (Var "X")) "being" ($#m1_hidden :::"set"::: ) (Bool "for" (Set (Var "f")) "," (Set (Var "g")) "being" ($#m1_hidden :::"Function":::) "holds" (Bool (Set (Set ($#k3_partfun1 :::"<:"::: ) (Set (Var "g")) "," (Set (Var "Y")) "," (Set (Var "Z")) ($#k3_partfun1 :::":>"::: ) ) ($#k1_partfun1 :::"*"::: ) (Set ($#k3_partfun1 :::"<:"::: ) (Set (Var "f")) "," (Set (Var "X")) "," (Set (Var "Y")) ($#k3_partfun1 :::":>"::: ) )) ($#r1_relset_1 :::"c="::: ) (Set ($#k3_partfun1 :::"<:"::: ) (Set "(" (Set (Var "g")) ($#k3_relat_1 :::"*"::: ) (Set (Var "f")) ")" ) "," (Set (Var "X")) "," (Set (Var "Z")) ($#k3_partfun1 :::":>"::: ) )))) ; theorem :: PARTFUN1:36 (Bool "for" (Set (Var "Y")) "," (Set (Var "Z")) "," (Set (Var "X")) "being" ($#m1_hidden :::"set"::: ) (Bool "for" (Set (Var "f")) "," (Set (Var "g")) "being" ($#m1_hidden :::"Function":::) "st" (Bool (Bool (Set (Set "(" ($#k10_xtuple_0 :::"rng"::: ) (Set (Var "f")) ")" ) ($#k3_xboole_0 :::"/\"::: ) (Set "(" ($#k9_xtuple_0 :::"dom"::: ) (Set (Var "g")) ")" )) ($#r1_tarski :::"c="::: ) (Set (Var "Y")))) "holds" (Bool (Set (Set ($#k3_partfun1 :::"<:"::: ) (Set (Var "g")) "," (Set (Var "Y")) "," (Set (Var "Z")) ($#k3_partfun1 :::":>"::: ) ) ($#k1_partfun1 :::"*"::: ) (Set ($#k3_partfun1 :::"<:"::: ) (Set (Var "f")) "," (Set (Var "X")) "," (Set (Var "Y")) ($#k3_partfun1 :::":>"::: ) )) ($#r1_hidden :::"="::: ) (Set ($#k3_partfun1 :::"<:"::: ) (Set "(" (Set (Var "g")) ($#k3_relat_1 :::"*"::: ) (Set (Var "f")) ")" ) "," (Set (Var "X")) "," (Set (Var "Z")) ($#k3_partfun1 :::":>"::: ) )))) ; theorem :: PARTFUN1: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 (Var "f")) "is" ($#v2_funct_1 :::"one-to-one"::: ) )) "holds" (Bool (Set ($#k3_partfun1 :::"<:"::: ) (Set (Var "f")) "," (Set (Var "X")) "," (Set (Var "Y")) ($#k3_partfun1 :::":>"::: ) ) "is" ($#v2_funct_1 :::"one-to-one"::: ) ))) ; theorem :: PARTFUN1:38 (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 "f")) "is" ($#v2_funct_1 :::"one-to-one"::: ) )) "holds" (Bool (Set (Set ($#k3_partfun1 :::"<:"::: ) (Set (Var "f")) "," (Set (Var "X")) "," (Set (Var "Y")) ($#k3_partfun1 :::":>"::: ) ) ($#k2_funct_1 :::"""::: ) ) ($#r1_hidden :::"="::: ) (Set ($#k3_partfun1 :::"<:"::: ) (Set "(" (Set (Var "f")) ($#k2_funct_1 :::"""::: ) ")" ) "," (Set (Var "Y")) "," (Set (Var "X")) ($#k3_partfun1 :::":>"::: ) )))) ; theorem :: PARTFUN1:39 (Bool "for" (Set (Var "Z")) "," (Set (Var "X")) "," (Set (Var "Y")) "being" ($#m1_hidden :::"set"::: ) (Bool "for" (Set (Var "f")) "being" ($#m1_hidden :::"Function":::) "holds" (Bool (Set (Set (Var "Z")) ($#k6_relset_1 :::"|`"::: ) (Set ($#k3_partfun1 :::"<:"::: ) (Set (Var "f")) "," (Set (Var "X")) "," (Set (Var "Y")) ($#k3_partfun1 :::":>"::: ) )) ($#r1_hidden :::"="::: ) (Set ($#k3_partfun1 :::"<:"::: ) (Set (Var "f")) "," (Set (Var "X")) "," (Set "(" (Set (Var "Z")) ($#k3_xboole_0 :::"/\"::: ) (Set (Var "Y")) ")" ) ($#k3_partfun1 :::":>"::: ) )))) ; definitionlet "X" be ($#m1_hidden :::"set"::: ) ; let "f" be (Set (Const "X")) ($#v4_relat_1 :::"-defined"::: ) ($#m1_hidden :::"Relation":::); attr "f" is :::"total"::: means :: PARTFUN1:def 2 (Bool (Set ($#k1_relset_1 :::"dom"::: ) "f") ($#r1_hidden :::"="::: ) "X"); end; :: deftheorem defines :::"total"::: PARTFUN1:def 2 : (Bool "for" (Set (Var "X")) "being" ($#m1_hidden :::"set"::: ) (Bool "for" (Set (Var "f")) "being" (Set (Var "b1")) ($#v4_relat_1 :::"-defined"::: ) ($#m1_hidden :::"Relation":::) "holds" (Bool "(" (Bool (Set (Var "f")) "is" ($#v1_partfun1 :::"total"::: ) ) "iff" (Bool (Set ($#k1_relset_1 :::"dom"::: ) (Set (Var "f"))) ($#r1_hidden :::"="::: ) (Set (Var "X"))) ")" ))); registrationlet "X" be ($#v1_xboole_0 :::"empty"::: ) ($#m1_hidden :::"set"::: ) ; let "Y" be ($#m1_hidden :::"set"::: ) ; cluster -> ($#v1_partfun1 :::"total"::: ) for ($#m1_subset_1 :::"Element"::: ) "of" (Set ($#k1_zfmisc_1 :::"bool"::: ) (Set ($#k2_zfmisc_1 :::"[:"::: ) "X" "," "Y" ($#k2_zfmisc_1 :::":]"::: ) )); end; registrationlet "X" be ($#~v1_xboole_0 "non" ($#v1_xboole_0 :::"empty"::: ) ) ($#m1_hidden :::"set"::: ) ; let "Y" be ($#v1_xboole_0 :::"empty"::: ) ($#m1_hidden :::"set"::: ) ; cluster -> ($#~v1_partfun1 "non" ($#v1_partfun1 :::"total"::: ) ) for ($#m1_subset_1 :::"Element"::: ) "of" (Set ($#k1_zfmisc_1 :::"bool"::: ) (Set ($#k2_zfmisc_1 :::"[:"::: ) "X" "," "Y" ($#k2_zfmisc_1 :::":]"::: ) )); end; theorem :: PARTFUN1: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 ($#k3_partfun1 :::"<:"::: ) (Set (Var "f")) "," (Set (Var "X")) "," (Set (Var "Y")) ($#k3_partfun1 :::":>"::: ) ) "is" ($#v1_partfun1 :::"total"::: ) )) "holds" (Bool (Set (Var "X")) ($#r1_tarski :::"c="::: ) (Set ($#k9_xtuple_0 :::"dom"::: ) (Set (Var "f")))))) ; theorem :: PARTFUN1:41 (Bool "for" (Set (Var "X")) "," (Set (Var "Y")) "being" ($#m1_hidden :::"set"::: ) "st" (Bool (Bool (Set ($#k3_partfun1 :::"<:"::: ) (Set ($#k1_xboole_0 :::"{}"::: ) ) "," (Set (Var "X")) "," (Set (Var "Y")) ($#k3_partfun1 :::":>"::: ) ) "is" ($#v1_partfun1 :::"total"::: ) )) "holds" (Bool (Set (Var "X")) ($#r1_hidden :::"="::: ) (Set ($#k1_xboole_0 :::"{}"::: ) ))) ; theorem :: PARTFUN1:42 (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")) ($#r1_tarski :::"c="::: ) (Set ($#k9_xtuple_0 :::"dom"::: ) (Set (Var "f")))) & (Bool (Set ($#k10_xtuple_0 :::"rng"::: ) (Set (Var "f"))) ($#r1_tarski :::"c="::: ) (Set (Var "Y")))) "holds" (Bool (Set ($#k3_partfun1 :::"<:"::: ) (Set (Var "f")) "," (Set (Var "X")) "," (Set (Var "Y")) ($#k3_partfun1 :::":>"::: ) ) "is" ($#v1_partfun1 :::"total"::: ) ))) ; theorem :: PARTFUN1:43 (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 ($#k3_partfun1 :::"<:"::: ) (Set (Var "f")) "," (Set (Var "X")) "," (Set (Var "Y")) ($#k3_partfun1 :::":>"::: ) ) "is" ($#v1_partfun1 :::"total"::: ) )) "holds" (Bool (Set (Set (Var "f")) ($#k7_relat_1 :::".:"::: ) (Set (Var "X"))) ($#r1_tarski :::"c="::: ) (Set (Var "Y"))))) ; theorem :: PARTFUN1:44 (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")) ($#r1_tarski :::"c="::: ) (Set ($#k9_xtuple_0 :::"dom"::: ) (Set (Var "f")))) & (Bool (Set (Set (Var "f")) ($#k7_relat_1 :::".:"::: ) (Set (Var "X"))) ($#r1_tarski :::"c="::: ) (Set (Var "Y")))) "holds" (Bool (Set ($#k3_partfun1 :::"<:"::: ) (Set (Var "f")) "," (Set (Var "X")) "," (Set (Var "Y")) ($#k3_partfun1 :::":>"::: ) ) "is" ($#v1_partfun1 :::"total"::: ) ))) ; definitionlet "X", "Y" be ($#m1_hidden :::"set"::: ) ; func :::"PFuncs"::: "(" "X" "," "Y" ")" -> ($#m1_hidden :::"set"::: ) means :: PARTFUN1:def 3 (Bool "for" (Set (Var "x")) "being" ($#m1_hidden :::"set"::: ) "holds" (Bool "(" (Bool (Set (Var "x")) ($#r2_hidden :::"in"::: ) it) "iff" (Bool "ex" (Set (Var "f")) "being" ($#m1_hidden :::"Function":::) "st" (Bool "(" (Bool (Set (Var "x")) ($#r1_hidden :::"="::: ) (Set (Var "f"))) & (Bool (Set ($#k9_xtuple_0 :::"dom"::: ) (Set (Var "f"))) ($#r1_tarski :::"c="::: ) "X") & (Bool (Set ($#k10_xtuple_0 :::"rng"::: ) (Set (Var "f"))) ($#r1_tarski :::"c="::: ) "Y") ")" )) ")" )); end; :: deftheorem defines :::"PFuncs"::: PARTFUN1:def 3 : (Bool "for" (Set (Var "X")) "," (Set (Var "Y")) "," (Set (Var "b3")) "being" ($#m1_hidden :::"set"::: ) "holds" (Bool "(" (Bool (Set (Var "b3")) ($#r1_hidden :::"="::: ) (Set ($#k4_partfun1 :::"PFuncs"::: ) "(" (Set (Var "X")) "," (Set (Var "Y")) ")" )) "iff" (Bool "for" (Set (Var "x")) "being" ($#m1_hidden :::"set"::: ) "holds" (Bool "(" (Bool (Set (Var "x")) ($#r2_hidden :::"in"::: ) (Set (Var "b3"))) "iff" (Bool "ex" (Set (Var "f")) "being" ($#m1_hidden :::"Function":::) "st" (Bool "(" (Bool (Set (Var "x")) ($#r1_hidden :::"="::: ) (Set (Var "f"))) & (Bool (Set ($#k9_xtuple_0 :::"dom"::: ) (Set (Var "f"))) ($#r1_tarski :::"c="::: ) (Set (Var "X"))) & (Bool (Set ($#k10_xtuple_0 :::"rng"::: ) (Set (Var "f"))) ($#r1_tarski :::"c="::: ) (Set (Var "Y"))) ")" )) ")" )) ")" )); registrationlet "X", "Y" be ($#m1_hidden :::"set"::: ) ; cluster (Set ($#k4_partfun1 :::"PFuncs"::: ) "(" "X" "," "Y" ")" ) -> ($#~v1_xboole_0 "non" ($#v1_xboole_0 :::"empty"::: ) ) ; end; theorem :: PARTFUN1:45 (Bool "for" (Set (Var "X")) "," (Set (Var "Y")) "being" ($#m1_hidden :::"set"::: ) (Bool "for" (Set (Var "f")) "being" ($#m1_subset_1 :::"PartFunc":::) "of" (Set (Var "X")) "," (Set (Var "Y")) "holds" (Bool (Set (Var "f")) ($#r2_hidden :::"in"::: ) (Set ($#k4_partfun1 :::"PFuncs"::: ) "(" (Set (Var "X")) "," (Set (Var "Y")) ")" )))) ; theorem :: PARTFUN1:46 (Bool "for" (Set (Var "X")) "," (Set (Var "Y")) "," (Set (Var "f")) "being" ($#m1_hidden :::"set"::: ) "st" (Bool (Bool (Set (Var "f")) ($#r2_hidden :::"in"::: ) (Set ($#k4_partfun1 :::"PFuncs"::: ) "(" (Set (Var "X")) "," (Set (Var "Y")) ")" ))) "holds" (Bool (Set (Var "f")) "is" ($#m1_subset_1 :::"PartFunc":::) "of" (Set (Var "X")) "," (Set (Var "Y")))) ; theorem :: PARTFUN1:47 (Bool "for" (Set (Var "X")) "," (Set (Var "Y")) "being" ($#m1_hidden :::"set"::: ) (Bool "for" (Set (Var "f")) "being" ($#m1_subset_1 :::"Element"::: ) "of" (Set ($#k4_partfun1 :::"PFuncs"::: ) "(" (Set (Var "X")) "," (Set (Var "Y")) ")" ) "holds" (Bool (Set (Var "f")) "is" ($#m1_subset_1 :::"PartFunc":::) "of" (Set (Var "X")) "," (Set (Var "Y"))))) ; theorem :: PARTFUN1:48 (Bool "for" (Set (Var "Y")) "being" ($#m1_hidden :::"set"::: ) "holds" (Bool (Set ($#k4_partfun1 :::"PFuncs"::: ) "(" (Set ($#k1_xboole_0 :::"{}"::: ) ) "," (Set (Var "Y")) ")" ) ($#r1_hidden :::"="::: ) (Set ($#k1_tarski :::"{"::: ) (Set ($#k1_xboole_0 :::"{}"::: ) ) ($#k1_tarski :::"}"::: ) ))) ; theorem :: PARTFUN1:49 (Bool "for" (Set (Var "X")) "being" ($#m1_hidden :::"set"::: ) "holds" (Bool (Set ($#k4_partfun1 :::"PFuncs"::: ) "(" (Set (Var "X")) "," (Set ($#k1_xboole_0 :::"{}"::: ) ) ")" ) ($#r1_hidden :::"="::: ) (Set ($#k1_tarski :::"{"::: ) (Set ($#k1_xboole_0 :::"{}"::: ) ) ($#k1_tarski :::"}"::: ) ))) ; theorem :: PARTFUN1:50 (Bool "for" (Set (Var "X1")) "," (Set (Var "X2")) "," (Set (Var "Y1")) "," (Set (Var "Y2")) "being" ($#m1_hidden :::"set"::: ) "st" (Bool (Bool (Set (Var "X1")) ($#r1_tarski :::"c="::: ) (Set (Var "X2"))) & (Bool (Set (Var "Y1")) ($#r1_tarski :::"c="::: ) (Set (Var "Y2")))) "holds" (Bool (Set ($#k4_partfun1 :::"PFuncs"::: ) "(" (Set (Var "X1")) "," (Set (Var "Y1")) ")" ) ($#r1_tarski :::"c="::: ) (Set ($#k4_partfun1 :::"PFuncs"::: ) "(" (Set (Var "X2")) "," (Set (Var "Y2")) ")" ))) ; definitionlet "f", "g" be ($#m1_hidden :::"Function":::); pred "f" :::"tolerates"::: "g" means :: PARTFUN1:def 4 (Bool "for" (Set (Var "x")) "being" ($#m1_hidden :::"set"::: ) "st" (Bool (Bool (Set (Var "x")) ($#r2_hidden :::"in"::: ) (Set (Set "(" ($#k9_xtuple_0 :::"dom"::: ) "f" ")" ) ($#k3_xboole_0 :::"/\"::: ) (Set "(" ($#k9_xtuple_0 :::"dom"::: ) "g" ")" )))) "holds" (Bool (Set "f" ($#k1_funct_1 :::"."::: ) (Set (Var "x"))) ($#r1_hidden :::"="::: ) (Set "g" ($#k1_funct_1 :::"."::: ) (Set (Var "x"))))); reflexivity (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 (Set "(" ($#k9_xtuple_0 :::"dom"::: ) (Set (Var "f")) ")" ) ($#k3_xboole_0 :::"/\"::: ) (Set "(" ($#k9_xtuple_0 :::"dom"::: ) (Set (Var "f")) ")" )))) "holds" (Bool (Set (Set (Var "f")) ($#k1_funct_1 :::"."::: ) (Set (Var "x"))) ($#r1_hidden :::"="::: ) (Set (Set (Var "f")) ($#k1_funct_1 :::"."::: ) (Set (Var "x")))))) ; symmetry (Bool "for" (Set (Var "f")) "," (Set (Var "g")) "being" ($#m1_hidden :::"Function":::) "st" (Bool (Bool "(" "for" (Set (Var "x")) "being" ($#m1_hidden :::"set"::: ) "st" (Bool (Bool (Set (Var "x")) ($#r2_hidden :::"in"::: ) (Set (Set "(" ($#k9_xtuple_0 :::"dom"::: ) (Set (Var "f")) ")" ) ($#k3_xboole_0 :::"/\"::: ) (Set "(" ($#k9_xtuple_0 :::"dom"::: ) (Set (Var "g")) ")" )))) "holds" (Bool (Set (Set (Var "f")) ($#k1_funct_1 :::"."::: ) (Set (Var "x"))) ($#r1_hidden :::"="::: ) (Set (Set (Var "g")) ($#k1_funct_1 :::"."::: ) (Set (Var "x")))) ")" )) "holds" (Bool "for" (Set (Var "x")) "being" ($#m1_hidden :::"set"::: ) "st" (Bool (Bool (Set (Var "x")) ($#r2_hidden :::"in"::: ) (Set (Set "(" ($#k9_xtuple_0 :::"dom"::: ) (Set (Var "g")) ")" ) ($#k3_xboole_0 :::"/\"::: ) (Set "(" ($#k9_xtuple_0 :::"dom"::: ) (Set (Var "f")) ")" )))) "holds" (Bool (Set (Set (Var "g")) ($#k1_funct_1 :::"."::: ) (Set (Var "x"))) ($#r1_hidden :::"="::: ) (Set (Set (Var "f")) ($#k1_funct_1 :::"."::: ) (Set (Var "x")))))) ; end; :: deftheorem defines :::"tolerates"::: PARTFUN1:def 4 : (Bool "for" (Set (Var "f")) "," (Set (Var "g")) "being" ($#m1_hidden :::"Function":::) "holds" (Bool "(" (Bool (Set (Var "f")) ($#r1_partfun1 :::"tolerates"::: ) (Set (Var "g"))) "iff" (Bool "for" (Set (Var "x")) "being" ($#m1_hidden :::"set"::: ) "st" (Bool (Bool (Set (Var "x")) ($#r2_hidden :::"in"::: ) (Set (Set "(" ($#k9_xtuple_0 :::"dom"::: ) (Set (Var "f")) ")" ) ($#k3_xboole_0 :::"/\"::: ) (Set "(" ($#k9_xtuple_0 :::"dom"::: ) (Set (Var "g")) ")" )))) "holds" (Bool (Set (Set (Var "f")) ($#k1_funct_1 :::"."::: ) (Set (Var "x"))) ($#r1_hidden :::"="::: ) (Set (Set (Var "g")) ($#k1_funct_1 :::"."::: ) (Set (Var "x"))))) ")" )); theorem :: PARTFUN1:51 (Bool "for" (Set (Var "f")) "," (Set (Var "g")) "being" ($#m1_hidden :::"Function":::) "holds" (Bool "(" (Bool (Set (Var "f")) ($#r1_partfun1 :::"tolerates"::: ) (Set (Var "g"))) "iff" (Bool "ex" (Set (Var "h")) "being" ($#m1_hidden :::"Function":::) "st" (Bool (Set (Set (Var "f")) ($#k2_xboole_0 :::"\/"::: ) (Set (Var "g"))) ($#r1_hidden :::"="::: ) (Set (Var "h")))) ")" )) ; theorem :: PARTFUN1:52 (Bool "for" (Set (Var "f")) "," (Set (Var "g")) "being" ($#m1_hidden :::"Function":::) "holds" (Bool "(" (Bool (Set (Var "f")) ($#r1_partfun1 :::"tolerates"::: ) (Set (Var "g"))) "iff" (Bool "ex" (Set (Var "h")) "being" ($#m1_hidden :::"Function":::) "st" (Bool "(" (Bool (Set (Var "f")) ($#r1_tarski :::"c="::: ) (Set (Var "h"))) & (Bool (Set (Var "g")) ($#r1_tarski :::"c="::: ) (Set (Var "h"))) ")" )) ")" )) ; theorem :: PARTFUN1:53 (Bool "for" (Set (Var "f")) "," (Set (Var "g")) "being" ($#m1_hidden :::"Function":::) "st" (Bool (Bool (Set ($#k9_xtuple_0 :::"dom"::: ) (Set (Var "f"))) ($#r1_tarski :::"c="::: ) (Set ($#k9_xtuple_0 :::"dom"::: ) (Set (Var "g"))))) "holds" (Bool "(" (Bool (Set (Var "f")) ($#r1_partfun1 :::"tolerates"::: ) (Set (Var "g"))) "iff" (Bool "for" (Set (Var "x")) "being" ($#m1_hidden :::"set"::: ) "st" (Bool (Bool (Set (Var "x")) ($#r2_hidden :::"in"::: ) (Set ($#k9_xtuple_0 :::"dom"::: ) (Set (Var "f"))))) "holds" (Bool (Set (Set (Var "f")) ($#k1_funct_1 :::"."::: ) (Set (Var "x"))) ($#r1_hidden :::"="::: ) (Set (Set (Var "g")) ($#k1_funct_1 :::"."::: ) (Set (Var "x"))))) ")" )) ; theorem :: PARTFUN1:54 (Bool "for" (Set (Var "f")) "," (Set (Var "g")) "being" ($#m1_hidden :::"Function":::) "st" (Bool (Bool (Set (Var "f")) ($#r1_tarski :::"c="::: ) (Set (Var "g")))) "holds" (Bool (Set (Var "f")) ($#r1_partfun1 :::"tolerates"::: ) (Set (Var "g")))) ; theorem :: PARTFUN1:55 (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 ($#k9_xtuple_0 :::"dom"::: ) (Set (Var "g")))) & (Bool (Set (Var "f")) ($#r1_partfun1 :::"tolerates"::: ) (Set (Var "g")))) "holds" (Bool (Set (Var "f")) ($#r1_hidden :::"="::: ) (Set (Var "g")))) ; theorem :: PARTFUN1:56 (Bool "for" (Set (Var "f")) "," (Set (Var "g")) "being" ($#m1_hidden :::"Function":::) "st" (Bool (Bool (Set ($#k9_xtuple_0 :::"dom"::: ) (Set (Var "f"))) ($#r1_xboole_0 :::"misses"::: ) (Set ($#k9_xtuple_0 :::"dom"::: ) (Set (Var "g"))))) "holds" (Bool (Set (Var "f")) ($#r1_partfun1 :::"tolerates"::: ) (Set (Var "g")))) ; theorem :: PARTFUN1:57 (Bool "for" (Set (Var "f")) "," (Set (Var "g")) "," (Set (Var "h")) "being" ($#m1_hidden :::"Function":::) "st" (Bool (Bool (Set (Var "f")) ($#r1_tarski :::"c="::: ) (Set (Var "h"))) & (Bool (Set (Var "g")) ($#r1_tarski :::"c="::: ) (Set (Var "h")))) "holds" (Bool (Set (Var "f")) ($#r1_partfun1 :::"tolerates"::: ) (Set (Var "g")))) ; theorem :: PARTFUN1:58 (Bool "for" (Set (Var "X")) "," (Set (Var "Y")) "being" ($#m1_hidden :::"set"::: ) (Bool "for" (Set (Var "f")) "," (Set (Var "g")) "being" ($#m1_subset_1 :::"PartFunc":::) "of" (Set (Var "X")) "," (Set (Var "Y")) (Bool "for" (Set (Var "h")) "being" ($#m1_hidden :::"Function":::) "st" (Bool (Bool (Set (Var "f")) ($#r1_partfun1 :::"tolerates"::: ) (Set (Var "h"))) & (Bool (Set (Var "g")) ($#r1_relset_1 :::"c="::: ) (Set (Var "f")))) "holds" (Bool (Set (Var "g")) ($#r1_partfun1 :::"tolerates"::: ) (Set (Var "h")))))) ; theorem :: PARTFUN1:59 (Bool "for" (Set (Var "f")) "being" ($#m1_hidden :::"Function":::) "holds" (Bool (Set ($#k1_xboole_0 :::"{}"::: ) ) ($#r1_partfun1 :::"tolerates"::: ) (Set (Var "f")))) ; theorem :: PARTFUN1:60 (Bool "for" (Set (Var "X")) "," (Set (Var "Y")) "being" ($#m1_hidden :::"set"::: ) (Bool "for" (Set (Var "f")) "being" ($#m1_hidden :::"Function":::) "holds" (Bool (Set ($#k3_partfun1 :::"<:"::: ) (Set ($#k1_xboole_0 :::"{}"::: ) ) "," (Set (Var "X")) "," (Set (Var "Y")) ($#k3_partfun1 :::":>"::: ) ) ($#r1_partfun1 :::"tolerates"::: ) (Set (Var "f"))))) ; theorem :: PARTFUN1:61 (Bool "for" (Set (Var "X")) "," (Set (Var "y")) "being" ($#m1_hidden :::"set"::: ) (Bool "for" (Set (Var "f")) "," (Set (Var "g")) "being" ($#m1_subset_1 :::"PartFunc":::) "of" (Set (Var "X")) "," (Set ($#k1_tarski :::"{"::: ) (Set (Var "y")) ($#k1_tarski :::"}"::: ) ) "holds" (Bool (Set (Var "f")) ($#r1_partfun1 :::"tolerates"::: ) (Set (Var "g"))))) ; theorem :: PARTFUN1:62 (Bool "for" (Set (Var "X")) "being" ($#m1_hidden :::"set"::: ) (Bool "for" (Set (Var "f")) "being" ($#m1_hidden :::"Function":::) "holds" (Bool (Set (Set (Var "f")) ($#k5_relat_1 :::"|"::: ) (Set (Var "X"))) ($#r1_partfun1 :::"tolerates"::: ) (Set (Var "f"))))) ; theorem :: PARTFUN1:63 (Bool "for" (Set (Var "Y")) "being" ($#m1_hidden :::"set"::: ) (Bool "for" (Set (Var "f")) "being" ($#m1_hidden :::"Function":::) "holds" (Bool (Set (Set (Var "Y")) ($#k6_relat_1 :::"|`"::: ) (Set (Var "f"))) ($#r1_partfun1 :::"tolerates"::: ) (Set (Var "f"))))) ; theorem :: PARTFUN1:64 (Bool "for" (Set (Var "Y")) "," (Set (Var "X")) "being" ($#m1_hidden :::"set"::: ) (Bool "for" (Set (Var "f")) "being" ($#m1_hidden :::"Function":::) "holds" (Bool (Set (Set "(" (Set (Var "Y")) ($#k6_relat_1 :::"|`"::: ) (Set (Var "f")) ")" ) ($#k5_relat_1 :::"|"::: ) (Set (Var "X"))) ($#r1_partfun1 :::"tolerates"::: ) (Set (Var "f"))))) ; theorem :: PARTFUN1:65 (Bool "for" (Set (Var "X")) "," (Set (Var "Y")) "being" ($#m1_hidden :::"set"::: ) (Bool "for" (Set (Var "f")) "being" ($#m1_hidden :::"Function":::) "holds" (Bool (Set ($#k3_partfun1 :::"<:"::: ) (Set (Var "f")) "," (Set (Var "X")) "," (Set (Var "Y")) ($#k3_partfun1 :::":>"::: ) ) ($#r1_partfun1 :::"tolerates"::: ) (Set (Var "f"))))) ; theorem :: PARTFUN1:66 (Bool "for" (Set (Var "X")) "," (Set (Var "Y")) "being" ($#m1_hidden :::"set"::: ) (Bool "for" (Set (Var "f")) "," (Set (Var "g")) "being" ($#m1_subset_1 :::"PartFunc":::) "of" (Set (Var "X")) "," (Set (Var "Y")) "st" (Bool (Bool (Set (Var "f")) "is" ($#v1_partfun1 :::"total"::: ) ) & (Bool (Set (Var "g")) "is" ($#v1_partfun1 :::"total"::: ) ) & (Bool (Set (Var "f")) ($#r1_partfun1 :::"tolerates"::: ) (Set (Var "g")))) "holds" (Bool (Set (Var "f")) ($#r1_hidden :::"="::: ) (Set (Var "g"))))) ; theorem :: PARTFUN1:67 (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_subset_1 :::"PartFunc":::) "of" (Set (Var "X")) "," (Set (Var "Y")) "st" (Bool (Bool (Set (Var "f")) ($#r1_partfun1 :::"tolerates"::: ) (Set (Var "h"))) & (Bool (Set (Var "g")) ($#r1_partfun1 :::"tolerates"::: ) (Set (Var "h"))) & (Bool (Set (Var "h")) "is" ($#v1_partfun1 :::"total"::: ) )) "holds" (Bool (Set (Var "f")) ($#r1_partfun1 :::"tolerates"::: ) (Set (Var "g"))))) ; theorem :: PARTFUN1:68 (Bool "for" (Set (Var "X")) "," (Set (Var "Y")) "being" ($#m1_hidden :::"set"::: ) (Bool "for" (Set (Var "f")) "," (Set (Var "g")) "being" ($#m1_subset_1 :::"PartFunc":::) "of" (Set (Var "X")) "," (Set (Var "Y")) "st" (Bool "(" (Bool (Bool (Set (Var "Y")) ($#r1_hidden :::"="::: ) (Set ($#k1_xboole_0 :::"{}"::: ) ))) "implies" (Bool (Set (Var "X")) ($#r1_hidden :::"="::: ) (Set ($#k1_xboole_0 :::"{}"::: ) )) ")" & (Bool (Set (Var "f")) ($#r1_partfun1 :::"tolerates"::: ) (Set (Var "g")))) "holds" (Bool "ex" (Set (Var "h")) "being" ($#m1_subset_1 :::"PartFunc":::) "of" (Set (Var "X")) "," (Set (Var "Y")) "st" (Bool "(" (Bool (Set (Var "h")) "is" ($#v1_partfun1 :::"total"::: ) ) & (Bool (Set (Var "f")) ($#r1_partfun1 :::"tolerates"::: ) (Set (Var "h"))) & (Bool (Set (Var "g")) ($#r1_partfun1 :::"tolerates"::: ) (Set (Var "h"))) ")" )))) ; definitionlet "X", "Y" be ($#m1_hidden :::"set"::: ) ; let "f" be ($#m1_subset_1 :::"PartFunc":::) "of" (Set (Const "X")) "," (Set (Const "Y")); func :::"TotFuncs"::: "f" -> ($#m1_hidden :::"set"::: ) means :: PARTFUN1:def 5 (Bool "for" (Set (Var "x")) "being" ($#m1_hidden :::"set"::: ) "holds" (Bool "(" (Bool (Set (Var "x")) ($#r2_hidden :::"in"::: ) it) "iff" (Bool "ex" (Set (Var "g")) "being" ($#m1_subset_1 :::"PartFunc":::) "of" "X" "," "Y" "st" (Bool "(" (Bool (Set (Var "g")) ($#r1_hidden :::"="::: ) (Set (Var "x"))) & (Bool (Set (Var "g")) "is" ($#v1_partfun1 :::"total"::: ) ) & (Bool "f" ($#r1_partfun1 :::"tolerates"::: ) (Set (Var "g"))) ")" )) ")" )); end; :: deftheorem defines :::"TotFuncs"::: PARTFUN1:def 5 : (Bool "for" (Set (Var "X")) "," (Set (Var "Y")) "being" ($#m1_hidden :::"set"::: ) (Bool "for" (Set (Var "f")) "being" ($#m1_subset_1 :::"PartFunc":::) "of" (Set (Var "X")) "," (Set (Var "Y")) (Bool "for" (Set (Var "b4")) "being" ($#m1_hidden :::"set"::: ) "holds" (Bool "(" (Bool (Set (Var "b4")) ($#r1_hidden :::"="::: ) (Set ($#k5_partfun1 :::"TotFuncs"::: ) (Set (Var "f")))) "iff" (Bool "for" (Set (Var "x")) "being" ($#m1_hidden :::"set"::: ) "holds" (Bool "(" (Bool (Set (Var "x")) ($#r2_hidden :::"in"::: ) (Set (Var "b4"))) "iff" (Bool "ex" (Set (Var "g")) "being" ($#m1_subset_1 :::"PartFunc":::) "of" (Set (Var "X")) "," (Set (Var "Y")) "st" (Bool "(" (Bool (Set (Var "g")) ($#r1_hidden :::"="::: ) (Set (Var "x"))) & (Bool (Set (Var "g")) "is" ($#v1_partfun1 :::"total"::: ) ) & (Bool (Set (Var "f")) ($#r1_partfun1 :::"tolerates"::: ) (Set (Var "g"))) ")" )) ")" )) ")" )))); theorem :: PARTFUN1:69 (Bool "for" (Set (Var "X")) "," (Set (Var "Y")) "being" ($#m1_hidden :::"set"::: ) (Bool "for" (Set (Var "f")) "being" ($#m1_subset_1 :::"PartFunc":::) "of" (Set (Var "X")) "," (Set (Var "Y")) (Bool "for" (Set (Var "g")) "being" ($#m1_hidden :::"set"::: ) "st" (Bool (Bool (Set (Var "g")) ($#r2_hidden :::"in"::: ) (Set ($#k5_partfun1 :::"TotFuncs"::: ) (Set (Var "f"))))) "holds" (Bool (Set (Var "g")) "is" ($#m1_subset_1 :::"PartFunc":::) "of" (Set (Var "X")) "," (Set (Var "Y")))))) ; theorem :: PARTFUN1:70 (Bool "for" (Set (Var "X")) "," (Set (Var "Y")) "being" ($#m1_hidden :::"set"::: ) (Bool "for" (Set (Var "f")) "," (Set (Var "g")) "being" ($#m1_subset_1 :::"PartFunc":::) "of" (Set (Var "X")) "," (Set (Var "Y")) "st" (Bool (Bool (Set (Var "g")) ($#r2_hidden :::"in"::: ) (Set ($#k5_partfun1 :::"TotFuncs"::: ) (Set (Var "f"))))) "holds" (Bool (Set (Var "g")) "is" ($#v1_partfun1 :::"total"::: ) ))) ; theorem :: PARTFUN1:71 (Bool "for" (Set (Var "X")) "," (Set (Var "Y")) "being" ($#m1_hidden :::"set"::: ) (Bool "for" (Set (Var "f")) "being" ($#m1_subset_1 :::"PartFunc":::) "of" (Set (Var "X")) "," (Set (Var "Y")) (Bool "for" (Set (Var "g")) "being" ($#m1_hidden :::"Function":::) "st" (Bool (Bool (Set (Var "g")) ($#r2_hidden :::"in"::: ) (Set ($#k5_partfun1 :::"TotFuncs"::: ) (Set (Var "f"))))) "holds" (Bool (Set (Var "f")) ($#r1_partfun1 :::"tolerates"::: ) (Set (Var "g")))))) ; registrationlet "X" be ($#~v1_xboole_0 "non" ($#v1_xboole_0 :::"empty"::: ) ) ($#m1_hidden :::"set"::: ) ; let "Y" be ($#v1_xboole_0 :::"empty"::: ) ($#m1_hidden :::"set"::: ) ; let "f" be ($#m1_subset_1 :::"PartFunc":::) "of" (Set (Const "X")) "," (Set (Const "Y")); cluster (Set ($#k5_partfun1 :::"TotFuncs"::: ) "f") -> ($#v1_xboole_0 :::"empty"::: ) ; end; theorem :: PARTFUN1:72 (Bool "for" (Set (Var "X")) "," (Set (Var "Y")) "being" ($#m1_hidden :::"set"::: ) (Bool "for" (Set (Var "f")) "being" ($#m1_subset_1 :::"PartFunc":::) "of" (Set (Var "X")) "," (Set (Var "Y")) "holds" (Bool "(" (Bool (Set (Var "f")) "is" ($#v1_partfun1 :::"total"::: ) ) "iff" (Bool (Set ($#k5_partfun1 :::"TotFuncs"::: ) (Set (Var "f"))) ($#r1_hidden :::"="::: ) (Set ($#k1_tarski :::"{"::: ) (Set (Var "f")) ($#k1_tarski :::"}"::: ) )) ")" ))) ; theorem :: PARTFUN1:73 (Bool "for" (Set (Var "Y")) "being" ($#m1_hidden :::"set"::: ) (Bool "for" (Set (Var "f")) "being" ($#m1_subset_1 :::"PartFunc":::) "of" (Set ($#k1_xboole_0 :::"{}"::: ) ) "," (Set (Var "Y")) "holds" (Bool (Set ($#k5_partfun1 :::"TotFuncs"::: ) (Set (Var "f"))) ($#r1_hidden :::"="::: ) (Set ($#k1_tarski :::"{"::: ) (Set (Var "f")) ($#k1_tarski :::"}"::: ) )))) ; theorem :: PARTFUN1:74 (Bool "for" (Set (Var "Y")) "being" ($#m1_hidden :::"set"::: ) (Bool "for" (Set (Var "f")) "being" ($#m1_subset_1 :::"PartFunc":::) "of" (Set ($#k1_xboole_0 :::"{}"::: ) ) "," (Set (Var "Y")) "holds" (Bool (Set ($#k5_partfun1 :::"TotFuncs"::: ) (Set (Var "f"))) ($#r1_hidden :::"="::: ) (Set ($#k1_tarski :::"{"::: ) (Set ($#k1_xboole_0 :::"{}"::: ) ) ($#k1_tarski :::"}"::: ) )))) ; theorem :: PARTFUN1:75 (Bool "for" (Set (Var "X")) "," (Set (Var "Y")) "being" ($#m1_hidden :::"set"::: ) (Bool "for" (Set (Var "f")) "," (Set (Var "g")) "being" ($#m1_subset_1 :::"PartFunc":::) "of" (Set (Var "X")) "," (Set (Var "Y")) "st" (Bool (Bool (Set ($#k5_partfun1 :::"TotFuncs"::: ) (Set (Var "f"))) ($#r1_xboole_0 :::"meets"::: ) (Set ($#k5_partfun1 :::"TotFuncs"::: ) (Set (Var "g"))))) "holds" (Bool (Set (Var "f")) ($#r1_partfun1 :::"tolerates"::: ) (Set (Var "g"))))) ; theorem :: PARTFUN1:76 (Bool "for" (Set (Var "X")) "," (Set (Var "Y")) "being" ($#m1_hidden :::"set"::: ) (Bool "for" (Set (Var "f")) "," (Set (Var "g")) "being" ($#m1_subset_1 :::"PartFunc":::) "of" (Set (Var "X")) "," (Set (Var "Y")) "st" (Bool "(" (Bool (Bool (Set (Var "Y")) ($#r1_hidden :::"="::: ) (Set ($#k1_xboole_0 :::"{}"::: ) ))) "implies" (Bool (Set (Var "X")) ($#r1_hidden :::"="::: ) (Set ($#k1_xboole_0 :::"{}"::: ) )) ")" & (Bool (Set (Var "f")) ($#r1_partfun1 :::"tolerates"::: ) (Set (Var "g")))) "holds" (Bool (Set ($#k5_partfun1 :::"TotFuncs"::: ) (Set (Var "f"))) ($#r1_xboole_0 :::"meets"::: ) (Set ($#k5_partfun1 :::"TotFuncs"::: ) (Set (Var "g")))))) ; begin registrationlet "X" be ($#m1_hidden :::"set"::: ) ; cluster ($#v1_relat_1 :::"Relation-like"::: ) "X" ($#v4_relat_1 :::"-defined"::: ) "X" ($#v5_relat_1 :::"-valued"::: ) ($#v1_relat_2 :::"reflexive"::: ) ($#v3_relat_2 :::"symmetric"::: ) ($#v4_relat_2 :::"antisymmetric"::: ) ($#v8_relat_2 :::"transitive"::: ) ($#v1_partfun1 :::"total"::: ) for ($#m1_subset_1 :::"Element"::: ) "of" (Set ($#k1_zfmisc_1 :::"bool"::: ) (Set ($#k2_zfmisc_1 :::"[:"::: ) "X" "," "X" ($#k2_zfmisc_1 :::":]"::: ) )); end; registration cluster ($#v1_relat_1 :::"Relation-like"::: ) ($#v3_relat_2 :::"symmetric"::: ) ($#v8_relat_2 :::"transitive"::: ) -> ($#v1_relat_2 :::"reflexive"::: ) for ($#m1_hidden :::"set"::: ) ; end; registrationlet "X" be ($#m1_hidden :::"set"::: ) ; cluster (Set ($#k4_relat_1 :::"id"::: ) "X") -> ($#v3_relat_2 :::"symmetric"::: ) ($#v4_relat_2 :::"antisymmetric"::: ) ($#v8_relat_2 :::"transitive"::: ) ; end; definitionlet "X" be ($#m1_hidden :::"set"::: ) ; :: original: :::"id"::: redefine func :::"id"::: "X" -> ($#v1_partfun1 :::"total"::: ) ($#m1_subset_1 :::"Relation":::) "of" "X"; end; scheme :: PARTFUN1:sch 4 LambdaC9{ F1() -> ($#~v1_xboole_0 "non" ($#v1_xboole_0 :::"empty"::: ) ) ($#m1_hidden :::"set"::: ) , P1[ ($#m1_hidden :::"set"::: ) ], F2( ($#m1_hidden :::"set"::: ) ) -> ($#m1_hidden :::"set"::: ) , F3( ($#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 "x")) "being" ($#m1_subset_1 :::"Element"::: ) "of" (Set F1 "(" ")" ) "holds" (Bool "(" "(" (Bool (Bool P1[(Set (Var "x"))])) "implies" (Bool (Set (Set (Var "f")) ($#k1_funct_1 :::"."::: ) (Set (Var "x"))) ($#r1_hidden :::"="::: ) (Set F2 "(" (Set (Var "x")) ")" )) ")" & "(" (Bool (Bool P1[(Set (Var "x"))])) "implies" (Bool (Set (Set (Var "f")) ($#k1_funct_1 :::"."::: ) (Set (Var "x"))) ($#r1_hidden :::"="::: ) (Set F3 "(" (Set (Var "x")) ")" )) ")" ")" ) ")" ) ")" )) proof end; begin theorem :: PARTFUN1:77 (Bool "for" (Set (Var "x")) "," (Set (Var "y")) "," (Set (Var "z")) "being" ($#m1_hidden :::"set"::: ) (Bool "for" (Set (Var "f")) "," (Set (Var "g")) "being" ($#m1_hidden :::"Function":::) "st" (Bool (Bool (Set (Var "f")) ($#r1_partfun1 :::"tolerates"::: ) (Set (Var "g"))) & (Bool (Set ($#k4_tarski :::"["::: ) (Set (Var "x")) "," (Set (Var "y")) ($#k4_tarski :::"]"::: ) ) ($#r2_hidden :::"in"::: ) (Set (Var "f"))) & (Bool (Set ($#k4_tarski :::"["::: ) (Set (Var "x")) "," (Set (Var "z")) ($#k4_tarski :::"]"::: ) ) ($#r2_hidden :::"in"::: ) (Set (Var "g")))) "holds" (Bool (Set (Var "y")) ($#r1_hidden :::"="::: ) (Set (Var "z"))))) ; theorem :: PARTFUN1:78 (Bool "for" (Set (Var "A")) "being" ($#m1_hidden :::"set"::: ) "st" (Bool (Bool (Set (Var "A")) "is" ($#v4_funct_1 :::"functional"::: ) ) & (Bool "(" "for" (Set (Var "f")) "," (Set (Var "g")) "being" ($#m1_hidden :::"Function":::) "st" (Bool (Bool (Set (Var "f")) ($#r2_hidden :::"in"::: ) (Set (Var "A"))) & (Bool (Set (Var "g")) ($#r2_hidden :::"in"::: ) (Set (Var "A")))) "holds" (Bool (Set (Var "f")) ($#r1_partfun1 :::"tolerates"::: ) (Set (Var "g"))) ")" )) "holds" (Bool (Set ($#k3_tarski :::"union"::: ) (Set (Var "A"))) "is" ($#m1_hidden :::"Function":::))) ; definitionlet "D" be ($#m1_hidden :::"set"::: ) ; let "p" be (Set (Const "D")) ($#v5_relat_1 :::"-valued"::: ) ($#m1_hidden :::"Function":::); let "i" be ($#m1_hidden :::"set"::: ) ; assume (Bool (Set (Const "i")) ($#r2_hidden :::"in"::: ) (Set ($#k9_xtuple_0 :::"dom"::: ) (Set (Const "p")))) ; func "p" :::"/."::: "i" -> ($#m1_subset_1 :::"Element"::: ) "of" "D" equals :: PARTFUN1:def 6 (Set "p" ($#k1_funct_1 :::"."::: ) "i"); end; :: deftheorem defines :::"/."::: PARTFUN1:def 6 : (Bool "for" (Set (Var "D")) "being" ($#m1_hidden :::"set"::: ) (Bool "for" (Set (Var "p")) "being" (Set (Var "b1")) ($#v5_relat_1 :::"-valued"::: ) ($#m1_hidden :::"Function":::) (Bool "for" (Set (Var "i")) "being" ($#m1_hidden :::"set"::: ) "st" (Bool (Bool (Set (Var "i")) ($#r2_hidden :::"in"::: ) (Set ($#k9_xtuple_0 :::"dom"::: ) (Set (Var "p"))))) "holds" (Bool (Set (Set (Var "p")) ($#k7_partfun1 :::"/."::: ) (Set (Var "i"))) ($#r1_hidden :::"="::: ) (Set (Set (Var "p")) ($#k1_funct_1 :::"."::: ) (Set (Var "i"))))))); registrationlet "X", "Y" be ($#~v1_xboole_0 "non" ($#v1_xboole_0 :::"empty"::: ) ) ($#m1_hidden :::"set"::: ) ; cluster ($#v1_relat_1 :::"Relation-like"::: ) "X" ($#v4_relat_1 :::"-defined"::: ) "Y" ($#v5_relat_1 :::"-valued"::: ) ($#v1_funct_1 :::"Function-like"::: ) ($#~v1_xboole_0 "non" ($#v1_xboole_0 :::"empty"::: ) ) for ($#m1_subset_1 :::"Element"::: ) "of" (Set ($#k1_zfmisc_1 :::"bool"::: ) (Set ($#k2_zfmisc_1 :::"[:"::: ) "X" "," "Y" ($#k2_zfmisc_1 :::":]"::: ) )); end; registrationlet "A", "B" be ($#m1_hidden :::"set"::: ) ; cluster (Set ($#k4_partfun1 :::"PFuncs"::: ) "(" "A" "," "B" ")" ) -> ($#v4_funct_1 :::"functional"::: ) ; end; theorem :: PARTFUN1:79 (Bool "for" (Set (Var "f1")) "," (Set (Var "f2")) "," (Set (Var "g")) "being" ($#m1_hidden :::"Function":::) "st" (Bool (Bool (Set ($#k10_xtuple_0 :::"rng"::: ) (Set (Var "g"))) ($#r1_tarski :::"c="::: ) (Set ($#k9_xtuple_0 :::"dom"::: ) (Set (Var "f1")))) & (Bool (Set ($#k10_xtuple_0 :::"rng"::: ) (Set (Var "g"))) ($#r1_tarski :::"c="::: ) (Set ($#k9_xtuple_0 :::"dom"::: ) (Set (Var "f2")))) & (Bool (Set (Var "f1")) ($#r1_partfun1 :::"tolerates"::: ) (Set (Var "f2")))) "holds" (Bool (Set (Set (Var "f1")) ($#k3_relat_1 :::"*"::: ) (Set (Var "g"))) ($#r1_hidden :::"="::: ) (Set (Set (Var "f2")) ($#k3_relat_1 :::"*"::: ) (Set (Var "g"))))) ; theorem :: PARTFUN1:80 (Bool "for" (Set (Var "Y")) "," (Set (Var "x")) "," (Set (Var "X")) "being" ($#m1_hidden :::"set"::: ) (Bool "for" (Set (Var "f")) "being" (Set (Var "b1")) ($#v5_relat_1 :::"-valued"::: ) ($#m1_hidden :::"Function":::) "st" (Bool (Bool (Set (Var "x")) ($#r2_hidden :::"in"::: ) (Set ($#k9_xtuple_0 :::"dom"::: ) (Set "(" (Set (Var "f")) ($#k5_relat_1 :::"|"::: ) (Set (Var "X")) ")" )))) "holds" (Bool (Set (Set "(" (Set (Var "f")) ($#k5_relat_1 :::"|"::: ) (Set (Var "X")) ")" ) ($#k7_partfun1 :::"/."::: ) (Set (Var "x"))) ($#r1_hidden :::"="::: ) (Set (Set (Var "f")) ($#k7_partfun1 :::"/."::: ) (Set (Var "x")))))) ;