:: PARTFUN2 semantic presentation begin theorem :: PARTFUN2:1 (Bool "for" (Set (Var "D")) "," (Set (Var "C")) "being" ($#~v1_xboole_0 "non" ($#v1_xboole_0 :::"empty"::: ) ) ($#m1_hidden :::"set"::: ) (Bool "for" (Set (Var "f")) "," (Set (Var "g")) "being" ($#m1_subset_1 :::"PartFunc":::) "of" (Set (Var "C")) "," (Set (Var "D")) "st" (Bool (Bool (Set ($#k1_relset_1 :::"dom"::: ) (Set (Var "f"))) ($#r1_hidden :::"="::: ) (Set ($#k1_relset_1 :::"dom"::: ) (Set (Var "g")))) & (Bool "(" "for" (Set (Var "c")) "being" ($#m1_subset_1 :::"Element"::: ) "of" (Set (Var "C")) "st" (Bool (Bool (Set (Var "c")) ($#r2_hidden :::"in"::: ) (Set ($#k1_relset_1 :::"dom"::: ) (Set (Var "f"))))) "holds" (Bool (Set (Set (Var "f")) ($#k7_partfun1 :::"/."::: ) (Set (Var "c"))) ($#r1_hidden :::"="::: ) (Set (Set (Var "g")) ($#k7_partfun1 :::"/."::: ) (Set (Var "c")))) ")" )) "holds" (Bool (Set (Var "f")) ($#r2_relset_1 :::"="::: ) (Set (Var "g"))))) ; theorem :: PARTFUN2:2 (Bool "for" (Set (Var "y")) "being" ($#m1_hidden :::"set"::: ) (Bool "for" (Set (Var "D")) "," (Set (Var "C")) "being" ($#~v1_xboole_0 "non" ($#v1_xboole_0 :::"empty"::: ) ) ($#m1_hidden :::"set"::: ) (Bool "for" (Set (Var "f")) "being" ($#m1_subset_1 :::"PartFunc":::) "of" (Set (Var "C")) "," (Set (Var "D")) "holds" (Bool "(" (Bool (Set (Var "y")) ($#r2_hidden :::"in"::: ) (Set ($#k2_relset_1 :::"rng"::: ) (Set (Var "f")))) "iff" (Bool "ex" (Set (Var "c")) "being" ($#m1_subset_1 :::"Element"::: ) "of" (Set (Var "C")) "st" (Bool "(" (Bool (Set (Var "c")) ($#r2_hidden :::"in"::: ) (Set ($#k1_relset_1 :::"dom"::: ) (Set (Var "f")))) & (Bool (Set (Var "y")) ($#r1_hidden :::"="::: ) (Set (Set (Var "f")) ($#k7_partfun1 :::"/."::: ) (Set (Var "c")))) ")" )) ")" )))) ; theorem :: PARTFUN2:3 (Bool "for" (Set (Var "D")) "," (Set (Var "E")) "," (Set (Var "C")) "being" ($#~v1_xboole_0 "non" ($#v1_xboole_0 :::"empty"::: ) ) ($#m1_hidden :::"set"::: ) (Bool "for" (Set (Var "f")) "being" ($#m1_subset_1 :::"PartFunc":::) "of" (Set (Var "C")) "," (Set (Var "D")) (Bool "for" (Set (Var "s")) "being" ($#m1_subset_1 :::"PartFunc":::) "of" (Set (Var "D")) "," (Set (Var "E")) (Bool "for" (Set (Var "h")) "being" ($#m1_subset_1 :::"PartFunc":::) "of" (Set (Var "C")) "," (Set (Var "E")) "holds" (Bool "(" (Bool (Set (Var "h")) ($#r2_relset_1 :::"="::: ) (Set (Set (Var "s")) ($#k1_partfun1 :::"*"::: ) (Set (Var "f")))) "iff" (Bool "(" (Bool "(" "for" (Set (Var "c")) "being" ($#m1_subset_1 :::"Element"::: ) "of" (Set (Var "C")) "holds" (Bool "(" (Bool (Set (Var "c")) ($#r2_hidden :::"in"::: ) (Set ($#k1_relset_1 :::"dom"::: ) (Set (Var "h")))) "iff" (Bool "(" (Bool (Set (Var "c")) ($#r2_hidden :::"in"::: ) (Set ($#k1_relset_1 :::"dom"::: ) (Set (Var "f")))) & (Bool (Set (Set (Var "f")) ($#k7_partfun1 :::"/."::: ) (Set (Var "c"))) ($#r2_hidden :::"in"::: ) (Set ($#k1_relset_1 :::"dom"::: ) (Set (Var "s")))) ")" ) ")" ) ")" ) & (Bool "(" "for" (Set (Var "c")) "being" ($#m1_subset_1 :::"Element"::: ) "of" (Set (Var "C")) "st" (Bool (Bool (Set (Var "c")) ($#r2_hidden :::"in"::: ) (Set ($#k1_relset_1 :::"dom"::: ) (Set (Var "h"))))) "holds" (Bool (Set (Set (Var "h")) ($#k7_partfun1 :::"/."::: ) (Set (Var "c"))) ($#r1_hidden :::"="::: ) (Set (Set (Var "s")) ($#k7_partfun1 :::"/."::: ) (Set "(" (Set (Var "f")) ($#k7_partfun1 :::"/."::: ) (Set (Var "c")) ")" ))) ")" ) ")" ) ")" ))))) ; theorem :: PARTFUN2:4 (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 "f")) "being" ($#m1_subset_1 :::"PartFunc":::) "of" (Set (Var "C")) "," (Set (Var "D")) (Bool "for" (Set (Var "s")) "being" ($#m1_subset_1 :::"PartFunc":::) "of" (Set (Var "D")) "," (Set (Var "E")) "st" (Bool (Bool (Set (Var "c")) ($#r2_hidden :::"in"::: ) (Set ($#k1_relset_1 :::"dom"::: ) (Set (Var "f")))) & (Bool (Set (Set (Var "f")) ($#k7_partfun1 :::"/."::: ) (Set (Var "c"))) ($#r2_hidden :::"in"::: ) (Set ($#k1_relset_1 :::"dom"::: ) (Set (Var "s"))))) "holds" (Bool (Set (Set "(" (Set (Var "s")) ($#k1_partfun1 :::"*"::: ) (Set (Var "f")) ")" ) ($#k7_partfun1 :::"/."::: ) (Set (Var "c"))) ($#r1_hidden :::"="::: ) (Set (Set (Var "s")) ($#k7_partfun1 :::"/."::: ) (Set "(" (Set (Var "f")) ($#k7_partfun1 :::"/."::: ) (Set (Var "c")) ")" ))))))) ; theorem :: PARTFUN2:5 (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 "f")) "being" ($#m1_subset_1 :::"PartFunc":::) "of" (Set (Var "C")) "," (Set (Var "D")) (Bool "for" (Set (Var "s")) "being" ($#m1_subset_1 :::"PartFunc":::) "of" (Set (Var "D")) "," (Set (Var "E")) "st" (Bool (Bool (Set ($#k2_relset_1 :::"rng"::: ) (Set (Var "f"))) ($#r1_tarski :::"c="::: ) (Set ($#k1_relset_1 :::"dom"::: ) (Set (Var "s")))) & (Bool (Set (Var "c")) ($#r2_hidden :::"in"::: ) (Set ($#k1_relset_1 :::"dom"::: ) (Set (Var "f"))))) "holds" (Bool (Set (Set "(" (Set (Var "s")) ($#k1_partfun1 :::"*"::: ) (Set (Var "f")) ")" ) ($#k7_partfun1 :::"/."::: ) (Set (Var "c"))) ($#r1_hidden :::"="::: ) (Set (Set (Var "s")) ($#k7_partfun1 :::"/."::: ) (Set "(" (Set (Var "f")) ($#k7_partfun1 :::"/."::: ) (Set (Var "c")) ")" ))))))) ; definitionlet "D" be ($#~v1_xboole_0 "non" ($#v1_xboole_0 :::"empty"::: ) ) ($#m1_hidden :::"set"::: ) ; let "SD" be ($#m1_subset_1 :::"Subset":::) "of" (Set (Const "D")); :: original: :::"id"::: redefine func :::"id"::: "SD" -> ($#m1_subset_1 :::"PartFunc":::) "of" "D" "," "D"; end; theorem :: PARTFUN2:6 (Bool "for" (Set (Var "D")) "being" ($#~v1_xboole_0 "non" ($#v1_xboole_0 :::"empty"::: ) ) ($#m1_hidden :::"set"::: ) (Bool "for" (Set (Var "SD")) "being" ($#m1_subset_1 :::"Subset":::) "of" (Set (Var "D")) (Bool "for" (Set (Var "F")) "being" ($#m1_subset_1 :::"PartFunc":::) "of" (Set (Var "D")) "," (Set (Var "D")) "holds" (Bool "(" (Bool (Set (Var "F")) ($#r2_relset_1 :::"="::: ) (Set ($#k1_partfun2 :::"id"::: ) (Set (Var "SD")))) "iff" (Bool "(" (Bool (Set ($#k1_relset_1 :::"dom"::: ) (Set (Var "F"))) ($#r1_hidden :::"="::: ) (Set (Var "SD"))) & (Bool "(" "for" (Set (Var "d")) "being" ($#m1_subset_1 :::"Element"::: ) "of" (Set (Var "D")) "st" (Bool (Bool (Set (Var "d")) ($#r2_hidden :::"in"::: ) (Set (Var "SD")))) "holds" (Bool (Set (Set (Var "F")) ($#k7_partfun1 :::"/."::: ) (Set (Var "d"))) ($#r1_hidden :::"="::: ) (Set (Var "d"))) ")" ) ")" ) ")" )))) ; theorem :: PARTFUN2:7 (Bool "for" (Set (Var "D")) "being" ($#~v1_xboole_0 "non" ($#v1_xboole_0 :::"empty"::: ) ) ($#m1_hidden :::"set"::: ) (Bool "for" (Set (Var "SD")) "being" ($#m1_subset_1 :::"Subset":::) "of" (Set (Var "D")) (Bool "for" (Set (Var "d")) "being" ($#m1_subset_1 :::"Element"::: ) "of" (Set (Var "D")) (Bool "for" (Set (Var "F")) "being" ($#m1_subset_1 :::"PartFunc":::) "of" (Set (Var "D")) "," (Set (Var "D")) "st" (Bool (Bool (Set (Var "d")) ($#r2_hidden :::"in"::: ) (Set (Set "(" ($#k1_relset_1 :::"dom"::: ) (Set (Var "F")) ")" ) ($#k9_subset_1 :::"/\"::: ) (Set (Var "SD"))))) "holds" (Bool (Set (Set (Var "F")) ($#k7_partfun1 :::"/."::: ) (Set (Var "d"))) ($#r1_hidden :::"="::: ) (Set (Set "(" (Set (Var "F")) ($#k1_partfun1 :::"*"::: ) (Set "(" ($#k1_partfun2 :::"id"::: ) (Set (Var "SD")) ")" ) ")" ) ($#k7_partfun1 :::"/."::: ) (Set (Var "d")))))))) ; theorem :: PARTFUN2:8 (Bool "for" (Set (Var "D")) "being" ($#~v1_xboole_0 "non" ($#v1_xboole_0 :::"empty"::: ) ) ($#m1_hidden :::"set"::: ) (Bool "for" (Set (Var "SD")) "being" ($#m1_subset_1 :::"Subset":::) "of" (Set (Var "D")) (Bool "for" (Set (Var "d")) "being" ($#m1_subset_1 :::"Element"::: ) "of" (Set (Var "D")) (Bool "for" (Set (Var "F")) "being" ($#m1_subset_1 :::"PartFunc":::) "of" (Set (Var "D")) "," (Set (Var "D")) "holds" (Bool "(" (Bool (Set (Var "d")) ($#r2_hidden :::"in"::: ) (Set ($#k1_relset_1 :::"dom"::: ) (Set "(" (Set "(" ($#k1_partfun2 :::"id"::: ) (Set (Var "SD")) ")" ) ($#k1_partfun1 :::"*"::: ) (Set (Var "F")) ")" ))) "iff" (Bool "(" (Bool (Set (Var "d")) ($#r2_hidden :::"in"::: ) (Set ($#k1_relset_1 :::"dom"::: ) (Set (Var "F")))) & (Bool (Set (Set (Var "F")) ($#k7_partfun1 :::"/."::: ) (Set (Var "d"))) ($#r2_hidden :::"in"::: ) (Set (Var "SD"))) ")" ) ")" ))))) ; theorem :: PARTFUN2:9 (Bool "for" (Set (Var "D")) "," (Set (Var "C")) "being" ($#~v1_xboole_0 "non" ($#v1_xboole_0 :::"empty"::: ) ) ($#m1_hidden :::"set"::: ) (Bool "for" (Set (Var "f")) "being" ($#m1_subset_1 :::"PartFunc":::) "of" (Set (Var "C")) "," (Set (Var "D")) "st" (Bool (Bool "(" "for" (Set (Var "c1")) "," (Set (Var "c2")) "being" ($#m1_subset_1 :::"Element"::: ) "of" (Set (Var "C")) "st" (Bool (Bool (Set (Var "c1")) ($#r2_hidden :::"in"::: ) (Set ($#k1_relset_1 :::"dom"::: ) (Set (Var "f")))) & (Bool (Set (Var "c2")) ($#r2_hidden :::"in"::: ) (Set ($#k1_relset_1 :::"dom"::: ) (Set (Var "f")))) & (Bool (Set (Set (Var "f")) ($#k7_partfun1 :::"/."::: ) (Set (Var "c1"))) ($#r1_hidden :::"="::: ) (Set (Set (Var "f")) ($#k7_partfun1 :::"/."::: ) (Set (Var "c2"))))) "holds" (Bool (Set (Var "c1")) ($#r1_hidden :::"="::: ) (Set (Var "c2"))) ")" )) "holds" (Bool (Set (Var "f")) "is" ($#v2_funct_1 :::"one-to-one"::: ) ))) ; theorem :: PARTFUN2:10 (Bool "for" (Set (Var "x")) "," (Set (Var "y")) "being" ($#m1_hidden :::"set"::: ) (Bool "for" (Set (Var "C")) "," (Set (Var "D")) "being" ($#~v1_xboole_0 "non" ($#v1_xboole_0 :::"empty"::: ) ) ($#m1_hidden :::"set"::: ) (Bool "for" (Set (Var "f")) "being" ($#m1_subset_1 :::"PartFunc":::) "of" (Set (Var "C")) "," (Set (Var "D")) "st" (Bool (Bool (Set (Var "f")) "is" ($#v2_funct_1 :::"one-to-one"::: ) ) & (Bool (Set (Var "x")) ($#r2_hidden :::"in"::: ) (Set ($#k1_relset_1 :::"dom"::: ) (Set (Var "f")))) & (Bool (Set (Var "y")) ($#r2_hidden :::"in"::: ) (Set ($#k1_relset_1 :::"dom"::: ) (Set (Var "f")))) & (Bool (Set (Set (Var "f")) ($#k7_partfun1 :::"/."::: ) (Set (Var "x"))) ($#r1_hidden :::"="::: ) (Set (Set (Var "f")) ($#k7_partfun1 :::"/."::: ) (Set (Var "y"))))) "holds" (Bool (Set (Var "x")) ($#r1_hidden :::"="::: ) (Set (Var "y")))))) ; definitionlet "X", "Y" be ($#m1_hidden :::"set"::: ) ; let "f" be ($#v2_funct_1 :::"one-to-one"::: ) ($#m1_subset_1 :::"PartFunc":::) "of" (Set (Const "X")) "," (Set (Const "Y")); :: original: :::"""::: redefine func "f" :::"""::: -> ($#m1_subset_1 :::"PartFunc":::) "of" "Y" "," "X"; end; theorem :: PARTFUN2:11 (Bool "for" (Set (Var "C")) "," (Set (Var "D")) "being" ($#~v1_xboole_0 "non" ($#v1_xboole_0 :::"empty"::: ) ) ($#m1_hidden :::"set"::: ) (Bool "for" (Set (Var "f")) "being" ($#v2_funct_1 :::"one-to-one"::: ) ($#m1_subset_1 :::"PartFunc":::) "of" (Set (Var "C")) "," (Set (Var "D")) (Bool "for" (Set (Var "g")) "being" ($#m1_subset_1 :::"PartFunc":::) "of" (Set (Var "D")) "," (Set (Var "C")) "holds" (Bool "(" (Bool (Set (Var "g")) ($#r2_relset_1 :::"="::: ) (Set (Set (Var "f")) ($#k2_partfun2 :::"""::: ) )) "iff" (Bool "(" (Bool (Set ($#k1_relset_1 :::"dom"::: ) (Set (Var "g"))) ($#r1_hidden :::"="::: ) (Set ($#k2_relset_1 :::"rng"::: ) (Set (Var "f")))) & (Bool "(" "for" (Set (Var "d")) "being" ($#m1_subset_1 :::"Element"::: ) "of" (Set (Var "D")) (Bool "for" (Set (Var "c")) "being" ($#m1_subset_1 :::"Element"::: ) "of" (Set (Var "C")) "holds" (Bool "(" (Bool (Set (Var "d")) ($#r2_hidden :::"in"::: ) (Set ($#k2_relset_1 :::"rng"::: ) (Set (Var "f")))) & (Bool (Set (Var "c")) ($#r1_hidden :::"="::: ) (Set (Set (Var "g")) ($#k7_partfun1 :::"/."::: ) (Set (Var "d")))) "iff" (Bool "(" (Bool (Set (Var "c")) ($#r2_hidden :::"in"::: ) (Set ($#k1_relset_1 :::"dom"::: ) (Set (Var "f")))) & (Bool (Set (Var "d")) ($#r1_hidden :::"="::: ) (Set (Set (Var "f")) ($#k7_partfun1 :::"/."::: ) (Set (Var "c")))) ")" ) ")" )) ")" ) ")" ) ")" )))) ; theorem :: PARTFUN2:12 (Bool "for" (Set (Var "C")) "," (Set (Var "D")) "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 "f")) "being" ($#v2_funct_1 :::"one-to-one"::: ) ($#m1_subset_1 :::"PartFunc":::) "of" (Set (Var "C")) "," (Set (Var "D")) "st" (Bool (Bool (Set (Var "c")) ($#r2_hidden :::"in"::: ) (Set ($#k1_relset_1 :::"dom"::: ) (Set (Var "f"))))) "holds" (Bool "(" (Bool (Set (Var "c")) ($#r1_hidden :::"="::: ) (Set (Set "(" (Set (Var "f")) ($#k2_partfun2 :::"""::: ) ")" ) ($#k7_partfun1 :::"/."::: ) (Set "(" (Set (Var "f")) ($#k7_partfun1 :::"/."::: ) (Set (Var "c")) ")" ))) & (Bool (Set (Var "c")) ($#r1_hidden :::"="::: ) (Set (Set "(" (Set "(" (Set (Var "f")) ($#k2_partfun2 :::"""::: ) ")" ) ($#k1_partfun1 :::"*"::: ) (Set (Var "f")) ")" ) ($#k7_partfun1 :::"/."::: ) (Set (Var "c")))) ")" )))) ; theorem :: PARTFUN2:13 (Bool "for" (Set (Var "C")) "," (Set (Var "D")) "being" ($#~v1_xboole_0 "non" ($#v1_xboole_0 :::"empty"::: ) ) ($#m1_hidden :::"set"::: ) (Bool "for" (Set (Var "d")) "being" ($#m1_subset_1 :::"Element"::: ) "of" (Set (Var "D")) (Bool "for" (Set (Var "f")) "being" ($#v2_funct_1 :::"one-to-one"::: ) ($#m1_subset_1 :::"PartFunc":::) "of" (Set (Var "C")) "," (Set (Var "D")) "st" (Bool (Bool (Set (Var "d")) ($#r2_hidden :::"in"::: ) (Set ($#k2_relset_1 :::"rng"::: ) (Set (Var "f"))))) "holds" (Bool "(" (Bool (Set (Var "d")) ($#r1_hidden :::"="::: ) (Set (Set (Var "f")) ($#k7_partfun1 :::"/."::: ) (Set "(" (Set "(" (Set (Var "f")) ($#k2_partfun2 :::"""::: ) ")" ) ($#k7_partfun1 :::"/."::: ) (Set (Var "d")) ")" ))) & (Bool (Set (Var "d")) ($#r1_hidden :::"="::: ) (Set (Set "(" (Set (Var "f")) ($#k1_partfun1 :::"*"::: ) (Set "(" (Set (Var "f")) ($#k2_partfun2 :::"""::: ) ")" ) ")" ) ($#k7_partfun1 :::"/."::: ) (Set (Var "d")))) ")" )))) ; theorem :: PARTFUN2:14 (Bool "for" (Set (Var "C")) "," (Set (Var "D")) "being" ($#~v1_xboole_0 "non" ($#v1_xboole_0 :::"empty"::: ) ) ($#m1_hidden :::"set"::: ) (Bool "for" (Set (Var "f")) "being" ($#m1_subset_1 :::"PartFunc":::) "of" (Set (Var "C")) "," (Set (Var "D")) (Bool "for" (Set (Var "t")) "being" ($#m1_subset_1 :::"PartFunc":::) "of" (Set (Var "D")) "," (Set (Var "C")) "st" (Bool (Bool (Set (Var "f")) "is" ($#v2_funct_1 :::"one-to-one"::: ) ) & (Bool (Set ($#k1_relset_1 :::"dom"::: ) (Set (Var "f"))) ($#r1_hidden :::"="::: ) (Set ($#k2_relset_1 :::"rng"::: ) (Set (Var "t")))) & (Bool (Set ($#k2_relset_1 :::"rng"::: ) (Set (Var "f"))) ($#r1_hidden :::"="::: ) (Set ($#k1_relset_1 :::"dom"::: ) (Set (Var "t")))) & (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")) "st" (Bool (Bool (Set (Var "c")) ($#r2_hidden :::"in"::: ) (Set ($#k1_relset_1 :::"dom"::: ) (Set (Var "f")))) & (Bool (Set (Var "d")) ($#r2_hidden :::"in"::: ) (Set ($#k1_relset_1 :::"dom"::: ) (Set (Var "t"))))) "holds" (Bool "(" (Bool (Set (Set (Var "f")) ($#k7_partfun1 :::"/."::: ) (Set (Var "c"))) ($#r1_hidden :::"="::: ) (Set (Var "d"))) "iff" (Bool (Set (Set (Var "t")) ($#k7_partfun1 :::"/."::: ) (Set (Var "d"))) ($#r1_hidden :::"="::: ) (Set (Var "c"))) ")" )) ")" )) "holds" (Bool (Set (Var "t")) ($#r1_hidden :::"="::: ) (Set (Set (Var "f")) ($#k2_funct_1 :::"""::: ) ))))) ; theorem :: PARTFUN2:15 (Bool "for" (Set (Var "X")) "being" ($#m1_hidden :::"set"::: ) (Bool "for" (Set (Var "D")) "," (Set (Var "C")) "being" ($#~v1_xboole_0 "non" ($#v1_xboole_0 :::"empty"::: ) ) ($#m1_hidden :::"set"::: ) (Bool "for" (Set (Var "g")) "," (Set (Var "f")) "being" ($#m1_subset_1 :::"PartFunc":::) "of" (Set (Var "C")) "," (Set (Var "D")) "holds" (Bool "(" (Bool (Set (Var "g")) ($#r2_relset_1 :::"="::: ) (Set (Set (Var "f")) ($#k2_partfun1 :::"|"::: ) (Set (Var "X")))) "iff" (Bool "(" (Bool (Set ($#k1_relset_1 :::"dom"::: ) (Set (Var "g"))) ($#r1_hidden :::"="::: ) (Set (Set "(" ($#k1_relset_1 :::"dom"::: ) (Set (Var "f")) ")" ) ($#k8_subset_1 :::"/\"::: ) (Set (Var "X")))) & (Bool "(" "for" (Set (Var "c")) "being" ($#m1_subset_1 :::"Element"::: ) "of" (Set (Var "C")) "st" (Bool (Bool (Set (Var "c")) ($#r2_hidden :::"in"::: ) (Set ($#k1_relset_1 :::"dom"::: ) (Set (Var "g"))))) "holds" (Bool (Set (Set (Var "g")) ($#k7_partfun1 :::"/."::: ) (Set (Var "c"))) ($#r1_hidden :::"="::: ) (Set (Set (Var "f")) ($#k7_partfun1 :::"/."::: ) (Set (Var "c")))) ")" ) ")" ) ")" )))) ; theorem :: PARTFUN2:16 (Bool "for" (Set (Var "X")) "being" ($#m1_hidden :::"set"::: ) (Bool "for" (Set (Var "C")) "," (Set (Var "D")) "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 "f")) "being" ($#m1_subset_1 :::"PartFunc":::) "of" (Set (Var "C")) "," (Set (Var "D")) "st" (Bool (Bool (Set (Var "c")) ($#r2_hidden :::"in"::: ) (Set (Set "(" ($#k1_relset_1 :::"dom"::: ) (Set (Var "f")) ")" ) ($#k8_subset_1 :::"/\"::: ) (Set (Var "X"))))) "holds" (Bool (Set (Set "(" (Set (Var "f")) ($#k2_partfun1 :::"|"::: ) (Set (Var "X")) ")" ) ($#k7_partfun1 :::"/."::: ) (Set (Var "c"))) ($#r1_hidden :::"="::: ) (Set (Set (Var "f")) ($#k7_partfun1 :::"/."::: ) (Set (Var "c")))))))) ; theorem :: PARTFUN2:17 (Bool "for" (Set (Var "X")) "being" ($#m1_hidden :::"set"::: ) (Bool "for" (Set (Var "C")) "," (Set (Var "D")) "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 "f")) "being" ($#m1_subset_1 :::"PartFunc":::) "of" (Set (Var "C")) "," (Set (Var "D")) "st" (Bool (Bool (Set (Var "c")) ($#r2_hidden :::"in"::: ) (Set ($#k1_relset_1 :::"dom"::: ) (Set (Var "f")))) & (Bool (Set (Var "c")) ($#r2_hidden :::"in"::: ) (Set (Var "X")))) "holds" (Bool (Set (Set "(" (Set (Var "f")) ($#k2_partfun1 :::"|"::: ) (Set (Var "X")) ")" ) ($#k7_partfun1 :::"/."::: ) (Set (Var "c"))) ($#r1_hidden :::"="::: ) (Set (Set (Var "f")) ($#k7_partfun1 :::"/."::: ) (Set (Var "c")))))))) ; theorem :: PARTFUN2:18 (Bool "for" (Set (Var "X")) "being" ($#m1_hidden :::"set"::: ) (Bool "for" (Set (Var "C")) "," (Set (Var "D")) "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 "f")) "being" ($#m1_subset_1 :::"PartFunc":::) "of" (Set (Var "C")) "," (Set (Var "D")) "st" (Bool (Bool (Set (Var "c")) ($#r2_hidden :::"in"::: ) (Set ($#k1_relset_1 :::"dom"::: ) (Set (Var "f")))) & (Bool (Set (Var "c")) ($#r2_hidden :::"in"::: ) (Set (Var "X")))) "holds" (Bool (Set (Set (Var "f")) ($#k7_partfun1 :::"/."::: ) (Set (Var "c"))) ($#r2_hidden :::"in"::: ) (Set ($#k2_relset_1 :::"rng"::: ) (Set "(" (Set (Var "f")) ($#k2_partfun1 :::"|"::: ) (Set (Var "X")) ")" ))))))) ; definitionlet "C", "D" be ($#~v1_xboole_0 "non" ($#v1_xboole_0 :::"empty"::: ) ) ($#m1_hidden :::"set"::: ) ; let "X" be ($#m1_hidden :::"set"::: ) ; let "f" be ($#m1_subset_1 :::"PartFunc":::) "of" (Set (Const "C")) "," (Set (Const "D")); :: original: :::"|`"::: redefine func "X" :::"|`"::: "f" -> ($#m1_subset_1 :::"PartFunc":::) "of" "C" "," "D"; end; theorem :: PARTFUN2:19 (Bool "for" (Set (Var "X")) "being" ($#m1_hidden :::"set"::: ) (Bool "for" (Set (Var "D")) "," (Set (Var "C")) "being" ($#~v1_xboole_0 "non" ($#v1_xboole_0 :::"empty"::: ) ) ($#m1_hidden :::"set"::: ) (Bool "for" (Set (Var "g")) "," (Set (Var "f")) "being" ($#m1_subset_1 :::"PartFunc":::) "of" (Set (Var "C")) "," (Set (Var "D")) "holds" (Bool "(" (Bool (Set (Var "g")) ($#r2_relset_1 :::"="::: ) (Set (Set (Var "X")) ($#k3_partfun2 :::"|`"::: ) (Set (Var "f")))) "iff" (Bool "(" (Bool "(" "for" (Set (Var "c")) "being" ($#m1_subset_1 :::"Element"::: ) "of" (Set (Var "C")) "holds" (Bool "(" (Bool (Set (Var "c")) ($#r2_hidden :::"in"::: ) (Set ($#k1_relset_1 :::"dom"::: ) (Set (Var "g")))) "iff" (Bool "(" (Bool (Set (Var "c")) ($#r2_hidden :::"in"::: ) (Set ($#k1_relset_1 :::"dom"::: ) (Set (Var "f")))) & (Bool (Set (Set (Var "f")) ($#k7_partfun1 :::"/."::: ) (Set (Var "c"))) ($#r2_hidden :::"in"::: ) (Set (Var "X"))) ")" ) ")" ) ")" ) & (Bool "(" "for" (Set (Var "c")) "being" ($#m1_subset_1 :::"Element"::: ) "of" (Set (Var "C")) "st" (Bool (Bool (Set (Var "c")) ($#r2_hidden :::"in"::: ) (Set ($#k1_relset_1 :::"dom"::: ) (Set (Var "g"))))) "holds" (Bool (Set (Set (Var "g")) ($#k7_partfun1 :::"/."::: ) (Set (Var "c"))) ($#r1_hidden :::"="::: ) (Set (Set (Var "f")) ($#k7_partfun1 :::"/."::: ) (Set (Var "c")))) ")" ) ")" ) ")" )))) ; theorem :: PARTFUN2:20 (Bool "for" (Set (Var "X")) "being" ($#m1_hidden :::"set"::: ) (Bool "for" (Set (Var "C")) "," (Set (Var "D")) "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 "f")) "being" ($#m1_subset_1 :::"PartFunc":::) "of" (Set (Var "C")) "," (Set (Var "D")) "holds" (Bool "(" (Bool (Set (Var "c")) ($#r2_hidden :::"in"::: ) (Set ($#k1_relset_1 :::"dom"::: ) (Set "(" (Set (Var "X")) ($#k3_partfun2 :::"|`"::: ) (Set (Var "f")) ")" ))) "iff" (Bool "(" (Bool (Set (Var "c")) ($#r2_hidden :::"in"::: ) (Set ($#k1_relset_1 :::"dom"::: ) (Set (Var "f")))) & (Bool (Set (Set (Var "f")) ($#k7_partfun1 :::"/."::: ) (Set (Var "c"))) ($#r2_hidden :::"in"::: ) (Set (Var "X"))) ")" ) ")" ))))) ; theorem :: PARTFUN2:21 (Bool "for" (Set (Var "X")) "being" ($#m1_hidden :::"set"::: ) (Bool "for" (Set (Var "C")) "," (Set (Var "D")) "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 "f")) "being" ($#m1_subset_1 :::"PartFunc":::) "of" (Set (Var "C")) "," (Set (Var "D")) "st" (Bool (Bool (Set (Var "c")) ($#r2_hidden :::"in"::: ) (Set ($#k1_relset_1 :::"dom"::: ) (Set "(" (Set (Var "X")) ($#k3_partfun2 :::"|`"::: ) (Set (Var "f")) ")" )))) "holds" (Bool (Set (Set "(" (Set (Var "X")) ($#k3_partfun2 :::"|`"::: ) (Set (Var "f")) ")" ) ($#k7_partfun1 :::"/."::: ) (Set (Var "c"))) ($#r1_hidden :::"="::: ) (Set (Set (Var "f")) ($#k7_partfun1 :::"/."::: ) (Set (Var "c")))))))) ; theorem :: PARTFUN2:22 (Bool "for" (Set (Var "X")) "being" ($#m1_hidden :::"set"::: ) (Bool "for" (Set (Var "D")) "," (Set (Var "C")) "being" ($#~v1_xboole_0 "non" ($#v1_xboole_0 :::"empty"::: ) ) ($#m1_hidden :::"set"::: ) (Bool "for" (Set (Var "SD")) "being" ($#m1_subset_1 :::"Subset":::) "of" (Set (Var "D")) (Bool "for" (Set (Var "f")) "being" ($#m1_subset_1 :::"PartFunc":::) "of" (Set (Var "C")) "," (Set (Var "D")) "holds" (Bool "(" (Bool (Set (Var "SD")) ($#r1_hidden :::"="::: ) (Set (Set (Var "f")) ($#k7_relset_1 :::".:"::: ) (Set (Var "X")))) "iff" (Bool "for" (Set (Var "d")) "being" ($#m1_subset_1 :::"Element"::: ) "of" (Set (Var "D")) "holds" (Bool "(" (Bool (Set (Var "d")) ($#r2_hidden :::"in"::: ) (Set (Var "SD"))) "iff" (Bool "ex" (Set (Var "c")) "being" ($#m1_subset_1 :::"Element"::: ) "of" (Set (Var "C")) "st" (Bool "(" (Bool (Set (Var "c")) ($#r2_hidden :::"in"::: ) (Set ($#k1_relset_1 :::"dom"::: ) (Set (Var "f")))) & (Bool (Set (Var "c")) ($#r2_hidden :::"in"::: ) (Set (Var "X"))) & (Bool (Set (Var "d")) ($#r1_hidden :::"="::: ) (Set (Set (Var "f")) ($#k7_partfun1 :::"/."::: ) (Set (Var "c")))) ")" )) ")" )) ")" ))))) ; theorem :: PARTFUN2:23 (Bool "for" (Set (Var "X")) "being" ($#m1_hidden :::"set"::: ) (Bool "for" (Set (Var "C")) "," (Set (Var "D")) "being" ($#~v1_xboole_0 "non" ($#v1_xboole_0 :::"empty"::: ) ) ($#m1_hidden :::"set"::: ) (Bool "for" (Set (Var "d")) "being" ($#m1_subset_1 :::"Element"::: ) "of" (Set (Var "D")) (Bool "for" (Set (Var "f")) "being" ($#m1_subset_1 :::"PartFunc":::) "of" (Set (Var "C")) "," (Set (Var "D")) "holds" (Bool "(" (Bool (Set (Var "d")) ($#r2_hidden :::"in"::: ) (Set (Set (Var "f")) ($#k7_relset_1 :::".:"::: ) (Set (Var "X")))) "iff" (Bool "ex" (Set (Var "c")) "being" ($#m1_subset_1 :::"Element"::: ) "of" (Set (Var "C")) "st" (Bool "(" (Bool (Set (Var "c")) ($#r2_hidden :::"in"::: ) (Set ($#k1_relset_1 :::"dom"::: ) (Set (Var "f")))) & (Bool (Set (Var "c")) ($#r2_hidden :::"in"::: ) (Set (Var "X"))) & (Bool (Set (Var "d")) ($#r1_hidden :::"="::: ) (Set (Set (Var "f")) ($#k7_partfun1 :::"/."::: ) (Set (Var "c")))) ")" )) ")" ))))) ; theorem :: PARTFUN2:24 (Bool "for" (Set (Var "C")) "," (Set (Var "D")) "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 "f")) "being" ($#m1_subset_1 :::"PartFunc":::) "of" (Set (Var "C")) "," (Set (Var "D")) "st" (Bool (Bool (Set (Var "c")) ($#r2_hidden :::"in"::: ) (Set ($#k1_relset_1 :::"dom"::: ) (Set (Var "f"))))) "holds" (Bool (Set ($#k9_relat_1 :::"Im"::: ) "(" (Set (Var "f")) "," (Set (Var "c")) ")" ) ($#r1_hidden :::"="::: ) (Set ($#k1_tarski :::"{"::: ) (Set "(" (Set (Var "f")) ($#k7_partfun1 :::"/."::: ) (Set (Var "c")) ")" ) ($#k1_tarski :::"}"::: ) ))))) ; theorem :: PARTFUN2:25 (Bool "for" (Set (Var "C")) "," (Set (Var "D")) "being" ($#~v1_xboole_0 "non" ($#v1_xboole_0 :::"empty"::: ) ) ($#m1_hidden :::"set"::: ) (Bool "for" (Set (Var "c1")) "," (Set (Var "c2")) "being" ($#m1_subset_1 :::"Element"::: ) "of" (Set (Var "C")) (Bool "for" (Set (Var "f")) "being" ($#m1_subset_1 :::"PartFunc":::) "of" (Set (Var "C")) "," (Set (Var "D")) "st" (Bool (Bool (Set (Var "c1")) ($#r2_hidden :::"in"::: ) (Set ($#k1_relset_1 :::"dom"::: ) (Set (Var "f")))) & (Bool (Set (Var "c2")) ($#r2_hidden :::"in"::: ) (Set ($#k1_relset_1 :::"dom"::: ) (Set (Var "f"))))) "holds" (Bool (Set (Set (Var "f")) ($#k7_relset_1 :::".:"::: ) (Set ($#k2_tarski :::"{"::: ) (Set (Var "c1")) "," (Set (Var "c2")) ($#k2_tarski :::"}"::: ) )) ($#r1_hidden :::"="::: ) (Set ($#k2_tarski :::"{"::: ) (Set "(" (Set (Var "f")) ($#k7_partfun1 :::"/."::: ) (Set (Var "c1")) ")" ) "," (Set "(" (Set (Var "f")) ($#k7_partfun1 :::"/."::: ) (Set (Var "c2")) ")" ) ($#k2_tarski :::"}"::: ) ))))) ; theorem :: PARTFUN2:26 (Bool "for" (Set (Var "X")) "being" ($#m1_hidden :::"set"::: ) (Bool "for" (Set (Var "D")) "," (Set (Var "C")) "being" ($#~v1_xboole_0 "non" ($#v1_xboole_0 :::"empty"::: ) ) ($#m1_hidden :::"set"::: ) (Bool "for" (Set (Var "SC")) "being" ($#m1_subset_1 :::"Subset":::) "of" (Set (Var "C")) (Bool "for" (Set (Var "f")) "being" ($#m1_subset_1 :::"PartFunc":::) "of" (Set (Var "C")) "," (Set (Var "D")) "holds" (Bool "(" (Bool (Set (Var "SC")) ($#r1_hidden :::"="::: ) (Set (Set (Var "f")) ($#k8_relset_1 :::"""::: ) (Set (Var "X")))) "iff" (Bool "for" (Set (Var "c")) "being" ($#m1_subset_1 :::"Element"::: ) "of" (Set (Var "C")) "holds" (Bool "(" (Bool (Set (Var "c")) ($#r2_hidden :::"in"::: ) (Set (Var "SC"))) "iff" (Bool "(" (Bool (Set (Var "c")) ($#r2_hidden :::"in"::: ) (Set ($#k1_relset_1 :::"dom"::: ) (Set (Var "f")))) & (Bool (Set (Set (Var "f")) ($#k7_partfun1 :::"/."::: ) (Set (Var "c"))) ($#r2_hidden :::"in"::: ) (Set (Var "X"))) ")" ) ")" )) ")" ))))) ; theorem :: PARTFUN2:27 (Bool "for" (Set (Var "D")) "," (Set (Var "C")) "being" ($#~v1_xboole_0 "non" ($#v1_xboole_0 :::"empty"::: ) ) ($#m1_hidden :::"set"::: ) (Bool "for" (Set (Var "f")) "being" ($#m1_subset_1 :::"PartFunc":::) "of" (Set (Var "C")) "," (Set (Var "D")) (Bool "ex" (Set (Var "g")) "being" ($#m1_subset_1 :::"Function":::) "of" (Set (Var "C")) "," (Set (Var "D")) "st" (Bool "for" (Set (Var "c")) "being" ($#m1_subset_1 :::"Element"::: ) "of" (Set (Var "C")) "st" (Bool (Bool (Set (Var "c")) ($#r2_hidden :::"in"::: ) (Set ($#k1_relset_1 :::"dom"::: ) (Set (Var "f"))))) "holds" (Bool (Set (Set (Var "g")) ($#k3_funct_2 :::"."::: ) (Set (Var "c"))) ($#r1_hidden :::"="::: ) (Set (Set (Var "f")) ($#k7_partfun1 :::"/."::: ) (Set (Var "c")))))))) ; theorem :: PARTFUN2:28 (Bool "for" (Set (Var "D")) "," (Set (Var "C")) "being" ($#~v1_xboole_0 "non" ($#v1_xboole_0 :::"empty"::: ) ) ($#m1_hidden :::"set"::: ) (Bool "for" (Set (Var "f")) "," (Set (Var "g")) "being" ($#m1_subset_1 :::"PartFunc":::) "of" (Set (Var "C")) "," (Set (Var "D")) "holds" (Bool "(" (Bool (Set (Var "f")) ($#r1_partfun1 :::"tolerates"::: ) (Set (Var "g"))) "iff" (Bool "for" (Set (Var "c")) "being" ($#m1_subset_1 :::"Element"::: ) "of" (Set (Var "C")) "st" (Bool (Bool (Set (Var "c")) ($#r2_hidden :::"in"::: ) (Set (Set "(" ($#k1_relset_1 :::"dom"::: ) (Set (Var "f")) ")" ) ($#k9_subset_1 :::"/\"::: ) (Set "(" ($#k1_relset_1 :::"dom"::: ) (Set (Var "g")) ")" )))) "holds" (Bool (Set (Set (Var "f")) ($#k7_partfun1 :::"/."::: ) (Set (Var "c"))) ($#r1_hidden :::"="::: ) (Set (Set (Var "g")) ($#k7_partfun1 :::"/."::: ) (Set (Var "c"))))) ")" ))) ; scheme :: PARTFUN2:sch 1 PartFuncExD{ F1() -> ($#~v1_xboole_0 "non" ($#v1_xboole_0 :::"empty"::: ) ) ($#m1_hidden :::"set"::: ) , F2() -> ($#~v1_xboole_0 "non" ($#v1_xboole_0 :::"empty"::: ) ) ($#m1_hidden :::"set"::: ) , P1[ ($#m1_hidden :::"set"::: ) "," ($#m1_hidden :::"set"::: ) ] } : (Bool "ex" (Set (Var "f")) "being" ($#m1_subset_1 :::"PartFunc":::) "of" (Set F1 "(" ")" ) "," (Set F2 "(" ")" ) "st" (Bool "(" (Bool "(" "for" (Set (Var "d")) "being" ($#m1_subset_1 :::"Element"::: ) "of" (Set F1 "(" ")" ) "holds" (Bool "(" (Bool (Set (Var "d")) ($#r2_hidden :::"in"::: ) (Set ($#k1_relset_1 :::"dom"::: ) (Set (Var "f")))) "iff" (Bool "ex" (Set (Var "c")) "being" ($#m1_subset_1 :::"Element"::: ) "of" (Set F2 "(" ")" ) "st" (Bool P1[(Set (Var "d")) "," (Set (Var "c"))])) ")" ) ")" ) & (Bool "(" "for" (Set (Var "d")) "being" ($#m1_subset_1 :::"Element"::: ) "of" (Set F1 "(" ")" ) "st" (Bool (Bool (Set (Var "d")) ($#r2_hidden :::"in"::: ) (Set ($#k1_relset_1 :::"dom"::: ) (Set (Var "f"))))) "holds" (Bool P1[(Set (Var "d")) "," (Set (Set (Var "f")) ($#k7_partfun1 :::"/."::: ) (Set (Var "d")))]) ")" ) ")" )) proof end; scheme :: PARTFUN2:sch 2 LambdaPFD{ F1() -> ($#~v1_xboole_0 "non" ($#v1_xboole_0 :::"empty"::: ) ) ($#m1_hidden :::"set"::: ) , F2() -> ($#~v1_xboole_0 "non" ($#v1_xboole_0 :::"empty"::: ) ) ($#m1_hidden :::"set"::: ) , F3( ($#m1_hidden :::"set"::: ) ) -> ($#m1_subset_1 :::"Element"::: ) "of" (Set F2 "(" ")" ), 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 "d")) "being" ($#m1_subset_1 :::"Element"::: ) "of" (Set F1 "(" ")" ) "holds" (Bool "(" (Bool (Set (Var "d")) ($#r2_hidden :::"in"::: ) (Set ($#k1_relset_1 :::"dom"::: ) (Set (Var "f")))) "iff" (Bool P1[(Set (Var "d"))]) ")" ) ")" ) & (Bool "(" "for" (Set (Var "d")) "being" ($#m1_subset_1 :::"Element"::: ) "of" (Set F1 "(" ")" ) "st" (Bool (Bool (Set (Var "d")) ($#r2_hidden :::"in"::: ) (Set ($#k1_relset_1 :::"dom"::: ) (Set (Var "f"))))) "holds" (Bool (Set (Set (Var "f")) ($#k7_partfun1 :::"/."::: ) (Set (Var "d"))) ($#r1_hidden :::"="::: ) (Set F3 "(" (Set (Var "d")) ")" )) ")" ) ")" )) proof end; scheme :: PARTFUN2:sch 3 UnPartFuncD{ F1() -> ($#~v1_xboole_0 "non" ($#v1_xboole_0 :::"empty"::: ) ) ($#m1_hidden :::"set"::: ) , F2() -> ($#~v1_xboole_0 "non" ($#v1_xboole_0 :::"empty"::: ) ) ($#m1_hidden :::"set"::: ) , F3() -> ($#m1_hidden :::"set"::: ) , F4( ($#m1_hidden :::"set"::: ) ) -> ($#m1_subset_1 :::"Element"::: ) "of" (Set F2 "(" ")" ) } : (Bool "for" (Set (Var "f")) "," (Set (Var "g")) "being" ($#m1_subset_1 :::"PartFunc":::) "of" (Set F1 "(" ")" ) "," (Set F2 "(" ")" ) "st" (Bool (Bool (Set ($#k1_relset_1 :::"dom"::: ) (Set (Var "f"))) ($#r1_hidden :::"="::: ) (Set F3 "(" ")" )) & (Bool "(" "for" (Set (Var "c")) "being" ($#m1_subset_1 :::"Element"::: ) "of" (Set F1 "(" ")" ) "st" (Bool (Bool (Set (Var "c")) ($#r2_hidden :::"in"::: ) (Set ($#k1_relset_1 :::"dom"::: ) (Set (Var "f"))))) "holds" (Bool (Set (Set (Var "f")) ($#k7_partfun1 :::"/."::: ) (Set (Var "c"))) ($#r1_hidden :::"="::: ) (Set F4 "(" (Set (Var "c")) ")" )) ")" ) & (Bool (Set ($#k1_relset_1 :::"dom"::: ) (Set (Var "g"))) ($#r1_hidden :::"="::: ) (Set F3 "(" ")" )) & (Bool "(" "for" (Set (Var "c")) "being" ($#m1_subset_1 :::"Element"::: ) "of" (Set F1 "(" ")" ) "st" (Bool (Bool (Set (Var "c")) ($#r2_hidden :::"in"::: ) (Set ($#k1_relset_1 :::"dom"::: ) (Set (Var "g"))))) "holds" (Bool (Set (Set (Var "g")) ($#k7_partfun1 :::"/."::: ) (Set (Var "c"))) ($#r1_hidden :::"="::: ) (Set F4 "(" (Set (Var "c")) ")" )) ")" )) "holds" (Bool (Set (Var "f")) ($#r2_relset_1 :::"="::: ) (Set (Var "g")))) proof end; definitionlet "C", "D" be ($#~v1_xboole_0 "non" ($#v1_xboole_0 :::"empty"::: ) ) ($#m1_hidden :::"set"::: ) ; let "SC" be ($#m1_subset_1 :::"Subset":::) "of" (Set (Const "C")); let "d" be ($#m1_subset_1 :::"Element"::: ) "of" (Set (Const "D")); :: original: :::"-->"::: redefine func "SC" :::"-->"::: "d" -> ($#m1_subset_1 :::"PartFunc":::) "of" "C" "," "D"; end; theorem :: PARTFUN2:29 (Bool "for" (Set (Var "C")) "," (Set (Var "D")) "being" ($#~v1_xboole_0 "non" ($#v1_xboole_0 :::"empty"::: ) ) ($#m1_hidden :::"set"::: ) (Bool "for" (Set (Var "SC")) "being" ($#m1_subset_1 :::"Subset":::) "of" (Set (Var "C")) (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")) "st" (Bool (Bool (Set (Var "c")) ($#r2_hidden :::"in"::: ) (Set (Var "SC")))) "holds" (Bool (Set (Set "(" (Set (Var "SC")) ($#k4_partfun2 :::"-->"::: ) (Set (Var "d")) ")" ) ($#k7_partfun1 :::"/."::: ) (Set (Var "c"))) ($#r1_hidden :::"="::: ) (Set (Var "d"))))))) ; theorem :: PARTFUN2:30 (Bool "for" (Set (Var "D")) "," (Set (Var "C")) "being" ($#~v1_xboole_0 "non" ($#v1_xboole_0 :::"empty"::: ) ) ($#m1_hidden :::"set"::: ) (Bool "for" (Set (Var "d")) "being" ($#m1_subset_1 :::"Element"::: ) "of" (Set (Var "D")) (Bool "for" (Set (Var "f")) "being" ($#m1_subset_1 :::"PartFunc":::) "of" (Set (Var "C")) "," (Set (Var "D")) "st" (Bool (Bool "(" "for" (Set (Var "c")) "being" ($#m1_subset_1 :::"Element"::: ) "of" (Set (Var "C")) "st" (Bool (Bool (Set (Var "c")) ($#r2_hidden :::"in"::: ) (Set ($#k1_relset_1 :::"dom"::: ) (Set (Var "f"))))) "holds" (Bool (Set (Set (Var "f")) ($#k7_partfun1 :::"/."::: ) (Set (Var "c"))) ($#r1_hidden :::"="::: ) (Set (Var "d"))) ")" )) "holds" (Bool (Set (Var "f")) ($#r2_relset_1 :::"="::: ) (Set (Set "(" ($#k1_relset_1 :::"dom"::: ) (Set (Var "f")) ")" ) ($#k4_partfun2 :::"-->"::: ) (Set (Var "d"))))))) ; theorem :: PARTFUN2:31 (Bool "for" (Set (Var "E")) "," (Set (Var "C")) "," (Set (Var "D")) "being" ($#~v1_xboole_0 "non" ($#v1_xboole_0 :::"empty"::: ) ) ($#m1_hidden :::"set"::: ) (Bool "for" (Set (Var "SE")) "being" ($#m1_subset_1 :::"Subset":::) "of" (Set (Var "E")) (Bool "for" (Set (Var "c")) "being" ($#m1_subset_1 :::"Element"::: ) "of" (Set (Var "C")) (Bool "for" (Set (Var "f")) "being" ($#m1_subset_1 :::"PartFunc":::) "of" (Set (Var "C")) "," (Set (Var "D")) "st" (Bool (Bool (Set (Var "c")) ($#r2_hidden :::"in"::: ) (Set ($#k1_relset_1 :::"dom"::: ) (Set (Var "f"))))) "holds" (Bool (Set (Set (Var "f")) ($#k1_partfun1 :::"*"::: ) (Set "(" (Set (Var "SE")) ($#k4_partfun2 :::"-->"::: ) (Set (Var "c")) ")" )) ($#r2_relset_1 :::"="::: ) (Set (Set (Var "SE")) ($#k4_partfun2 :::"-->"::: ) (Set "(" (Set (Var "f")) ($#k7_partfun1 :::"/."::: ) (Set (Var "c")) ")" ))))))) ; theorem :: PARTFUN2:32 (Bool "for" (Set (Var "C")) "being" ($#~v1_xboole_0 "non" ($#v1_xboole_0 :::"empty"::: ) ) ($#m1_hidden :::"set"::: ) (Bool "for" (Set (Var "SC")) "being" ($#m1_subset_1 :::"Subset":::) "of" (Set (Var "C")) "holds" (Bool "(" (Bool (Set ($#k1_partfun2 :::"id"::: ) (Set (Var "SC"))) "is" ($#v1_partfun1 :::"total"::: ) ) "iff" (Bool (Set (Var "SC")) ($#r1_hidden :::"="::: ) (Set (Var "C"))) ")" ))) ; theorem :: PARTFUN2:33 (Bool "for" (Set (Var "C")) "," (Set (Var "D")) "being" ($#~v1_xboole_0 "non" ($#v1_xboole_0 :::"empty"::: ) ) ($#m1_hidden :::"set"::: ) (Bool "for" (Set (Var "SC")) "being" ($#m1_subset_1 :::"Subset":::) "of" (Set (Var "C")) (Bool "for" (Set (Var "d")) "being" ($#m1_subset_1 :::"Element"::: ) "of" (Set (Var "D")) "st" (Bool (Bool (Set (Set (Var "SC")) ($#k4_partfun2 :::"-->"::: ) (Set (Var "d"))) "is" ($#v1_partfun1 :::"total"::: ) )) "holds" (Bool (Set (Var "SC")) ($#r1_hidden :::"<>"::: ) (Set ($#k1_xboole_0 :::"{}"::: ) ))))) ; theorem :: PARTFUN2:34 (Bool "for" (Set (Var "D")) "," (Set (Var "C")) "being" ($#~v1_xboole_0 "non" ($#v1_xboole_0 :::"empty"::: ) ) ($#m1_hidden :::"set"::: ) (Bool "for" (Set (Var "SC")) "being" ($#m1_subset_1 :::"Subset":::) "of" (Set (Var "C")) (Bool "for" (Set (Var "d")) "being" ($#m1_subset_1 :::"Element"::: ) "of" (Set (Var "D")) "holds" (Bool "(" (Bool (Set (Set (Var "SC")) ($#k4_partfun2 :::"-->"::: ) (Set (Var "d"))) "is" ($#v1_partfun1 :::"total"::: ) ) "iff" (Bool (Set (Var "SC")) ($#r1_hidden :::"="::: ) (Set (Var "C"))) ")" )))) ; definitionlet "C", "D" be ($#~v1_xboole_0 "non" ($#v1_xboole_0 :::"empty"::: ) ) ($#m1_hidden :::"set"::: ) ; let "f" be ($#m1_subset_1 :::"PartFunc":::) "of" (Set (Const "C")) "," (Set (Const "D")); :: original: :::"constant"::: redefine attr "f" is :::"constant"::: means :: PARTFUN2:def 1 (Bool "ex" (Set (Var "d")) "being" ($#m1_subset_1 :::"Element"::: ) "of" "D" "st" (Bool "for" (Set (Var "c")) "being" ($#m1_subset_1 :::"Element"::: ) "of" "C" "st" (Bool (Bool (Set (Var "c")) ($#r2_hidden :::"in"::: ) (Set ($#k1_relset_1 :::"dom"::: ) "f"))) "holds" (Bool (Set "f" ($#k1_funct_1 :::"."::: ) (Set (Var "c"))) ($#r1_hidden :::"="::: ) (Set (Var "d"))))); end; :: deftheorem defines :::"constant"::: PARTFUN2:def 1 : (Bool "for" (Set (Var "C")) "," (Set (Var "D")) "being" ($#~v1_xboole_0 "non" ($#v1_xboole_0 :::"empty"::: ) ) ($#m1_hidden :::"set"::: ) (Bool "for" (Set (Var "f")) "being" ($#m1_subset_1 :::"PartFunc":::) "of" (Set (Var "C")) "," (Set (Var "D")) "holds" (Bool "(" (Bool (Set (Var "f")) "is" ($#v3_funct_1 :::"constant"::: ) ) "iff" (Bool "ex" (Set (Var "d")) "being" ($#m1_subset_1 :::"Element"::: ) "of" (Set (Var "D")) "st" (Bool "for" (Set (Var "c")) "being" ($#m1_subset_1 :::"Element"::: ) "of" (Set (Var "C")) "st" (Bool (Bool (Set (Var "c")) ($#r2_hidden :::"in"::: ) (Set ($#k1_relset_1 :::"dom"::: ) (Set (Var "f"))))) "holds" (Bool (Set (Set (Var "f")) ($#k1_funct_1 :::"."::: ) (Set (Var "c"))) ($#r1_hidden :::"="::: ) (Set (Var "d"))))) ")" ))); theorem :: PARTFUN2:35 (Bool "for" (Set (Var "X")) "being" ($#m1_hidden :::"set"::: ) (Bool "for" (Set (Var "D")) "," (Set (Var "C")) "being" ($#~v1_xboole_0 "non" ($#v1_xboole_0 :::"empty"::: ) ) ($#m1_hidden :::"set"::: ) (Bool "for" (Set (Var "f")) "being" ($#m1_subset_1 :::"PartFunc":::) "of" (Set (Var "C")) "," (Set (Var "D")) "holds" (Bool "(" (Bool (Set (Set (Var "f")) ($#k2_partfun1 :::"|"::: ) (Set (Var "X"))) "is" bbbadV3_FUNCT_1()) "iff" (Bool "ex" (Set (Var "d")) "being" ($#m1_subset_1 :::"Element"::: ) "of" (Set (Var "D")) "st" (Bool "for" (Set (Var "c")) "being" ($#m1_subset_1 :::"Element"::: ) "of" (Set (Var "C")) "st" (Bool (Bool (Set (Var "c")) ($#r2_hidden :::"in"::: ) (Set (Set (Var "X")) ($#k9_subset_1 :::"/\"::: ) (Set "(" ($#k1_relset_1 :::"dom"::: ) (Set (Var "f")) ")" )))) "holds" (Bool (Set (Set (Var "f")) ($#k7_partfun1 :::"/."::: ) (Set (Var "c"))) ($#r1_hidden :::"="::: ) (Set (Var "d"))))) ")" )))) ; theorem :: PARTFUN2:36 (Bool "for" (Set (Var "X")) "being" ($#m1_hidden :::"set"::: ) (Bool "for" (Set (Var "D")) "," (Set (Var "C")) "being" ($#~v1_xboole_0 "non" ($#v1_xboole_0 :::"empty"::: ) ) ($#m1_hidden :::"set"::: ) (Bool "for" (Set (Var "f")) "being" ($#m1_subset_1 :::"PartFunc":::) "of" (Set (Var "C")) "," (Set (Var "D")) "holds" (Bool "(" (Bool (Set (Set (Var "f")) ($#k2_partfun1 :::"|"::: ) (Set (Var "X"))) "is" bbbadV3_FUNCT_1()) "iff" (Bool "for" (Set (Var "c1")) "," (Set (Var "c2")) "being" ($#m1_subset_1 :::"Element"::: ) "of" (Set (Var "C")) "st" (Bool (Bool (Set (Var "c1")) ($#r2_hidden :::"in"::: ) (Set (Set (Var "X")) ($#k9_subset_1 :::"/\"::: ) (Set "(" ($#k1_relset_1 :::"dom"::: ) (Set (Var "f")) ")" ))) & (Bool (Set (Var "c2")) ($#r2_hidden :::"in"::: ) (Set (Set (Var "X")) ($#k9_subset_1 :::"/\"::: ) (Set "(" ($#k1_relset_1 :::"dom"::: ) (Set (Var "f")) ")" )))) "holds" (Bool (Set (Set (Var "f")) ($#k7_partfun1 :::"/."::: ) (Set (Var "c1"))) ($#r1_hidden :::"="::: ) (Set (Set (Var "f")) ($#k7_partfun1 :::"/."::: ) (Set (Var "c2"))))) ")" )))) ; theorem :: PARTFUN2:37 (Bool "for" (Set (Var "X")) "being" ($#m1_hidden :::"set"::: ) (Bool "for" (Set (Var "C")) "," (Set (Var "D")) "being" ($#~v1_xboole_0 "non" ($#v1_xboole_0 :::"empty"::: ) ) ($#m1_hidden :::"set"::: ) (Bool "for" (Set (Var "f")) "being" ($#m1_subset_1 :::"PartFunc":::) "of" (Set (Var "C")) "," (Set (Var "D")) "st" (Bool (Bool (Set (Var "X")) ($#r1_xboole_0 :::"meets"::: ) (Set ($#k1_relset_1 :::"dom"::: ) (Set (Var "f"))))) "holds" (Bool "(" (Bool (Set (Set (Var "f")) ($#k2_partfun1 :::"|"::: ) (Set (Var "X"))) "is" bbbadV3_FUNCT_1()) "iff" (Bool "ex" (Set (Var "d")) "being" ($#m1_subset_1 :::"Element"::: ) "of" (Set (Var "D")) "st" (Bool (Set ($#k2_relset_1 :::"rng"::: ) (Set "(" (Set (Var "f")) ($#k2_partfun1 :::"|"::: ) (Set (Var "X")) ")" )) ($#r1_hidden :::"="::: ) (Set ($#k1_tarski :::"{"::: ) (Set (Var "d")) ($#k1_tarski :::"}"::: ) ))) ")" )))) ; theorem :: PARTFUN2:38 (Bool "for" (Set (Var "X")) "," (Set (Var "Y")) "being" ($#m1_hidden :::"set"::: ) (Bool "for" (Set (Var "C")) "," (Set (Var "D")) "being" ($#~v1_xboole_0 "non" ($#v1_xboole_0 :::"empty"::: ) ) ($#m1_hidden :::"set"::: ) (Bool "for" (Set (Var "f")) "being" ($#m1_subset_1 :::"PartFunc":::) "of" (Set (Var "C")) "," (Set (Var "D")) "st" (Bool (Bool (Set (Set (Var "f")) ($#k2_partfun1 :::"|"::: ) (Set (Var "X"))) "is" bbbadV3_FUNCT_1()) & (Bool (Set (Var "Y")) ($#r1_tarski :::"c="::: ) (Set (Var "X")))) "holds" (Bool (Set (Set (Var "f")) ($#k2_partfun1 :::"|"::: ) (Set (Var "Y"))) "is" bbbadV3_FUNCT_1())))) ; theorem :: PARTFUN2:39 (Bool "for" (Set (Var "X")) "being" ($#m1_hidden :::"set"::: ) (Bool "for" (Set (Var "C")) "," (Set (Var "D")) "being" ($#~v1_xboole_0 "non" ($#v1_xboole_0 :::"empty"::: ) ) ($#m1_hidden :::"set"::: ) (Bool "for" (Set (Var "f")) "being" ($#m1_subset_1 :::"PartFunc":::) "of" (Set (Var "C")) "," (Set (Var "D")) "st" (Bool (Bool (Set (Var "X")) ($#r1_xboole_0 :::"misses"::: ) (Set ($#k1_relset_1 :::"dom"::: ) (Set (Var "f"))))) "holds" (Bool (Set (Set (Var "f")) ($#k2_partfun1 :::"|"::: ) (Set (Var "X"))) "is" bbbadV3_FUNCT_1())))) ; theorem :: PARTFUN2:40 (Bool "for" (Set (Var "C")) "," (Set (Var "D")) "being" ($#~v1_xboole_0 "non" ($#v1_xboole_0 :::"empty"::: ) ) ($#m1_hidden :::"set"::: ) (Bool "for" (Set (Var "SC")) "being" ($#m1_subset_1 :::"Subset":::) "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 :::"PartFunc":::) "of" (Set (Var "C")) "," (Set (Var "D")) "st" (Bool (Bool (Set (Set (Var "f")) ($#k2_partfun1 :::"|"::: ) (Set (Var "SC"))) ($#r2_relset_1 :::"="::: ) (Set (Set "(" ($#k1_relset_1 :::"dom"::: ) (Set "(" (Set (Var "f")) ($#k2_partfun1 :::"|"::: ) (Set (Var "SC")) ")" ) ")" ) ($#k4_partfun2 :::"-->"::: ) (Set (Var "d"))))) "holds" (Bool (Set (Set (Var "f")) ($#k2_partfun1 :::"|"::: ) (Set (Var "SC"))) "is" bbbadV3_FUNCT_1()))))) ; theorem :: PARTFUN2:41 (Bool "for" (Set (Var "x")) "being" ($#m1_hidden :::"set"::: ) (Bool "for" (Set (Var "C")) "," (Set (Var "D")) "being" ($#~v1_xboole_0 "non" ($#v1_xboole_0 :::"empty"::: ) ) ($#m1_hidden :::"set"::: ) (Bool "for" (Set (Var "f")) "being" ($#m1_subset_1 :::"PartFunc":::) "of" (Set (Var "C")) "," (Set (Var "D")) "holds" (Bool (Set (Set (Var "f")) ($#k2_partfun1 :::"|"::: ) (Set ($#k1_tarski :::"{"::: ) (Set (Var "x")) ($#k1_tarski :::"}"::: ) )) "is" bbbadV3_FUNCT_1())))) ; theorem :: PARTFUN2:42 (Bool "for" (Set (Var "X")) "," (Set (Var "Y")) "being" ($#m1_hidden :::"set"::: ) (Bool "for" (Set (Var "C")) "," (Set (Var "D")) "being" ($#~v1_xboole_0 "non" ($#v1_xboole_0 :::"empty"::: ) ) ($#m1_hidden :::"set"::: ) (Bool "for" (Set (Var "f")) "being" ($#m1_subset_1 :::"PartFunc":::) "of" (Set (Var "C")) "," (Set (Var "D")) "st" (Bool (Bool (Set (Set (Var "f")) ($#k2_partfun1 :::"|"::: ) (Set (Var "X"))) "is" bbbadV3_FUNCT_1()) & (Bool (Set (Set (Var "f")) ($#k2_partfun1 :::"|"::: ) (Set (Var "Y"))) "is" bbbadV3_FUNCT_1()) & (Bool (Set (Set (Var "X")) ($#k3_xboole_0 :::"/\"::: ) (Set (Var "Y"))) ($#r1_xboole_0 :::"meets"::: ) (Set ($#k1_relset_1 :::"dom"::: ) (Set (Var "f"))))) "holds" (Bool (Set (Set (Var "f")) ($#k2_partfun1 :::"|"::: ) (Set "(" (Set (Var "X")) ($#k2_xboole_0 :::"\/"::: ) (Set (Var "Y")) ")" )) "is" bbbadV3_FUNCT_1())))) ; theorem :: PARTFUN2:43 (Bool "for" (Set (Var "Y")) "," (Set (Var "X")) "being" ($#m1_hidden :::"set"::: ) (Bool "for" (Set (Var "C")) "," (Set (Var "D")) "being" ($#~v1_xboole_0 "non" ($#v1_xboole_0 :::"empty"::: ) ) ($#m1_hidden :::"set"::: ) (Bool "for" (Set (Var "f")) "being" ($#m1_subset_1 :::"PartFunc":::) "of" (Set (Var "C")) "," (Set (Var "D")) "st" (Bool (Bool (Set (Set (Var "f")) ($#k2_partfun1 :::"|"::: ) (Set (Var "Y"))) "is" bbbadV3_FUNCT_1())) "holds" (Bool (Set (Set "(" (Set (Var "f")) ($#k2_partfun1 :::"|"::: ) (Set (Var "X")) ")" ) ($#k2_partfun1 :::"|"::: ) (Set (Var "Y"))) "is" bbbadV3_FUNCT_1())))) ; theorem :: PARTFUN2:44 (Bool "for" (Set (Var "C")) "," (Set (Var "D")) "being" ($#~v1_xboole_0 "non" ($#v1_xboole_0 :::"empty"::: ) ) ($#m1_hidden :::"set"::: ) (Bool "for" (Set (Var "SC")) "being" ($#m1_subset_1 :::"Subset":::) "of" (Set (Var "C")) (Bool "for" (Set (Var "d")) "being" ($#m1_subset_1 :::"Element"::: ) "of" (Set (Var "D")) "holds" (Bool (Set (Set "(" (Set (Var "SC")) ($#k4_partfun2 :::"-->"::: ) (Set (Var "d")) ")" ) ($#k2_partfun1 :::"|"::: ) (Set (Var "SC"))) "is" bbbadV3_FUNCT_1())))) ; theorem :: PARTFUN2:45 (Bool "for" (Set (Var "D")) "," (Set (Var "C")) "being" ($#~v1_xboole_0 "non" ($#v1_xboole_0 :::"empty"::: ) ) ($#m1_hidden :::"set"::: ) (Bool "for" (Set (Var "f")) "," (Set (Var "g")) "being" ($#m1_subset_1 :::"PartFunc":::) "of" (Set (Var "C")) "," (Set (Var "D")) "st" (Bool (Bool (Set ($#k1_relset_1 :::"dom"::: ) (Set (Var "f"))) ($#r1_tarski :::"c="::: ) (Set ($#k1_relset_1 :::"dom"::: ) (Set (Var "g")))) & (Bool "(" "for" (Set (Var "c")) "being" ($#m1_subset_1 :::"Element"::: ) "of" (Set (Var "C")) "st" (Bool (Bool (Set (Var "c")) ($#r2_hidden :::"in"::: ) (Set ($#k1_relset_1 :::"dom"::: ) (Set (Var "f"))))) "holds" (Bool (Set (Set (Var "f")) ($#k7_partfun1 :::"/."::: ) (Set (Var "c"))) ($#r1_hidden :::"="::: ) (Set (Set (Var "g")) ($#k7_partfun1 :::"/."::: ) (Set (Var "c")))) ")" )) "holds" (Bool (Set (Var "f")) ($#r1_relset_1 :::"c="::: ) (Set (Var "g"))))) ; theorem :: PARTFUN2:46 (Bool "for" (Set (Var "C")) "," (Set (Var "D")) "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 :::"PartFunc":::) "of" (Set (Var "C")) "," (Set (Var "D")) "holds" (Bool "(" (Bool "(" (Bool (Set (Var "c")) ($#r2_hidden :::"in"::: ) (Set ($#k1_relset_1 :::"dom"::: ) (Set (Var "f")))) & (Bool (Set (Var "d")) ($#r1_hidden :::"="::: ) (Set (Set (Var "f")) ($#k7_partfun1 :::"/."::: ) (Set (Var "c")))) ")" ) "iff" (Bool (Set ($#k4_tarski :::"["::: ) (Set (Var "c")) "," (Set (Var "d")) ($#k4_tarski :::"]"::: ) ) ($#r2_hidden :::"in"::: ) (Set (Var "f"))) ")" ))))) ; theorem :: PARTFUN2:47 (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 "e")) "being" ($#m1_subset_1 :::"Element"::: ) "of" (Set (Var "E")) (Bool "for" (Set (Var "f")) "being" ($#m1_subset_1 :::"PartFunc":::) "of" (Set (Var "C")) "," (Set (Var "D")) (Bool "for" (Set (Var "s")) "being" ($#m1_subset_1 :::"PartFunc":::) "of" (Set (Var "D")) "," (Set (Var "E")) "st" (Bool (Bool (Set ($#k4_tarski :::"["::: ) (Set (Var "c")) "," (Set (Var "e")) ($#k4_tarski :::"]"::: ) ) ($#r2_hidden :::"in"::: ) (Set (Set (Var "s")) ($#k1_partfun1 :::"*"::: ) (Set (Var "f"))))) "holds" (Bool "(" (Bool (Set ($#k4_tarski :::"["::: ) (Set (Var "c")) "," (Set "(" (Set (Var "f")) ($#k7_partfun1 :::"/."::: ) (Set (Var "c")) ")" ) ($#k4_tarski :::"]"::: ) ) ($#r2_hidden :::"in"::: ) (Set (Var "f"))) & (Bool (Set ($#k4_tarski :::"["::: ) (Set "(" (Set (Var "f")) ($#k7_partfun1 :::"/."::: ) (Set (Var "c")) ")" ) "," (Set (Var "e")) ($#k4_tarski :::"]"::: ) ) ($#r2_hidden :::"in"::: ) (Set (Var "s"))) ")" )))))) ; theorem :: PARTFUN2:48 (Bool "for" (Set (Var "C")) "," (Set (Var "D")) "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 :::"PartFunc":::) "of" (Set (Var "C")) "," (Set (Var "D")) "st" (Bool (Bool (Set (Var "f")) ($#r1_hidden :::"="::: ) (Set ($#k1_tarski :::"{"::: ) (Set ($#k4_tarski :::"["::: ) (Set (Var "c")) "," (Set (Var "d")) ($#k4_tarski :::"]"::: ) ) ($#k1_tarski :::"}"::: ) ))) "holds" (Bool (Set (Set (Var "f")) ($#k7_partfun1 :::"/."::: ) (Set (Var "c"))) ($#r1_hidden :::"="::: ) (Set (Var "d"))))))) ; theorem :: PARTFUN2:49 (Bool "for" (Set (Var "C")) "," (Set (Var "D")) "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 "f")) "being" ($#m1_subset_1 :::"PartFunc":::) "of" (Set (Var "C")) "," (Set (Var "D")) "st" (Bool (Bool (Set ($#k1_relset_1 :::"dom"::: ) (Set (Var "f"))) ($#r1_hidden :::"="::: ) (Set ($#k1_tarski :::"{"::: ) (Set (Var "c")) ($#k1_tarski :::"}"::: ) ))) "holds" (Bool (Set (Var "f")) ($#r1_hidden :::"="::: ) (Set ($#k1_tarski :::"{"::: ) (Set ($#k4_tarski :::"["::: ) (Set (Var "c")) "," (Set "(" (Set (Var "f")) ($#k7_partfun1 :::"/."::: ) (Set (Var "c")) ")" ) ($#k4_tarski :::"]"::: ) ) ($#k1_tarski :::"}"::: ) ))))) ; theorem :: PARTFUN2:50 (Bool "for" (Set (Var "C")) "," (Set (Var "D")) "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 "f1")) "," (Set (Var "f")) "," (Set (Var "g")) "being" ($#m1_subset_1 :::"PartFunc":::) "of" (Set (Var "C")) "," (Set (Var "D")) "st" (Bool (Bool (Set (Var "f1")) ($#r2_relset_1 :::"="::: ) (Set (Set (Var "f")) ($#k9_subset_1 :::"/\"::: ) (Set (Var "g")))) & (Bool (Set (Var "c")) ($#r2_hidden :::"in"::: ) (Set ($#k1_relset_1 :::"dom"::: ) (Set (Var "f1"))))) "holds" (Bool "(" (Bool (Set (Set (Var "f1")) ($#k7_partfun1 :::"/."::: ) (Set (Var "c"))) ($#r1_hidden :::"="::: ) (Set (Set (Var "f")) ($#k7_partfun1 :::"/."::: ) (Set (Var "c")))) & (Bool (Set (Set (Var "f1")) ($#k7_partfun1 :::"/."::: ) (Set (Var "c"))) ($#r1_hidden :::"="::: ) (Set (Set (Var "g")) ($#k7_partfun1 :::"/."::: ) (Set (Var "c")))) ")" )))) ; theorem :: PARTFUN2:51 (Bool "for" (Set (Var "C")) "," (Set (Var "D")) "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 "f")) "," (Set (Var "f1")) "," (Set (Var "g")) "being" ($#m1_subset_1 :::"PartFunc":::) "of" (Set (Var "C")) "," (Set (Var "D")) "st" (Bool (Bool (Set (Var "c")) ($#r2_hidden :::"in"::: ) (Set ($#k1_relset_1 :::"dom"::: ) (Set (Var "f")))) & (Bool (Set (Var "f1")) ($#r2_relset_1 :::"="::: ) (Set (Set (Var "f")) ($#k4_subset_1 :::"\/"::: ) (Set (Var "g"))))) "holds" (Bool (Set (Set (Var "f1")) ($#k7_partfun1 :::"/."::: ) (Set (Var "c"))) ($#r1_hidden :::"="::: ) (Set (Set (Var "f")) ($#k7_partfun1 :::"/."::: ) (Set (Var "c"))))))) ; theorem :: PARTFUN2:52 (Bool "for" (Set (Var "C")) "," (Set (Var "D")) "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 "g")) "," (Set (Var "f1")) "," (Set (Var "f")) "being" ($#m1_subset_1 :::"PartFunc":::) "of" (Set (Var "C")) "," (Set (Var "D")) "st" (Bool (Bool (Set (Var "c")) ($#r2_hidden :::"in"::: ) (Set ($#k1_relset_1 :::"dom"::: ) (Set (Var "g")))) & (Bool (Set (Var "f1")) ($#r2_relset_1 :::"="::: ) (Set (Set (Var "f")) ($#k4_subset_1 :::"\/"::: ) (Set (Var "g"))))) "holds" (Bool (Set (Set (Var "f1")) ($#k7_partfun1 :::"/."::: ) (Set (Var "c"))) ($#r1_hidden :::"="::: ) (Set (Set (Var "g")) ($#k7_partfun1 :::"/."::: ) (Set (Var "c"))))))) ; theorem :: PARTFUN2:53 (Bool "for" (Set (Var "C")) "," (Set (Var "D")) "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 "f1")) "," (Set (Var "f")) "," (Set (Var "g")) "being" ($#m1_subset_1 :::"PartFunc":::) "of" (Set (Var "C")) "," (Set (Var "D")) "st" (Bool (Bool (Set (Var "c")) ($#r2_hidden :::"in"::: ) (Set ($#k1_relset_1 :::"dom"::: ) (Set (Var "f1")))) & (Bool (Set (Var "f1")) ($#r2_relset_1 :::"="::: ) (Set (Set (Var "f")) ($#k4_subset_1 :::"\/"::: ) (Set (Var "g")))) & (Bool (Bool "not" (Set (Set (Var "f1")) ($#k7_partfun1 :::"/."::: ) (Set (Var "c"))) ($#r1_hidden :::"="::: ) (Set (Set (Var "f")) ($#k7_partfun1 :::"/."::: ) (Set (Var "c")))))) "holds" (Bool (Set (Set (Var "f1")) ($#k7_partfun1 :::"/."::: ) (Set (Var "c"))) ($#r1_hidden :::"="::: ) (Set (Set (Var "g")) ($#k7_partfun1 :::"/."::: ) (Set (Var "c"))))))) ; theorem :: PARTFUN2:54 (Bool "for" (Set (Var "C")) "," (Set (Var "D")) "being" ($#~v1_xboole_0 "non" ($#v1_xboole_0 :::"empty"::: ) ) ($#m1_hidden :::"set"::: ) (Bool "for" (Set (Var "SC")) "being" ($#m1_subset_1 :::"Subset":::) "of" (Set (Var "C")) (Bool "for" (Set (Var "c")) "being" ($#m1_subset_1 :::"Element"::: ) "of" (Set (Var "C")) (Bool "for" (Set (Var "f")) "being" ($#m1_subset_1 :::"PartFunc":::) "of" (Set (Var "C")) "," (Set (Var "D")) "holds" (Bool "(" (Bool "(" (Bool (Set (Var "c")) ($#r2_hidden :::"in"::: ) (Set ($#k1_relset_1 :::"dom"::: ) (Set (Var "f")))) & (Bool (Set (Var "c")) ($#r2_hidden :::"in"::: ) (Set (Var "SC"))) ")" ) "iff" (Bool (Set ($#k4_tarski :::"["::: ) (Set (Var "c")) "," (Set "(" (Set (Var "f")) ($#k7_partfun1 :::"/."::: ) (Set (Var "c")) ")" ) ($#k4_tarski :::"]"::: ) ) ($#r2_hidden :::"in"::: ) (Set (Set (Var "f")) ($#k2_partfun1 :::"|"::: ) (Set (Var "SC")))) ")" ))))) ; theorem :: PARTFUN2:55 (Bool "for" (Set (Var "C")) "," (Set (Var "D")) "being" ($#~v1_xboole_0 "non" ($#v1_xboole_0 :::"empty"::: ) ) ($#m1_hidden :::"set"::: ) (Bool "for" (Set (Var "SD")) "being" ($#m1_subset_1 :::"Subset":::) "of" (Set (Var "D")) (Bool "for" (Set (Var "c")) "being" ($#m1_subset_1 :::"Element"::: ) "of" (Set (Var "C")) (Bool "for" (Set (Var "f")) "being" ($#m1_subset_1 :::"PartFunc":::) "of" (Set (Var "C")) "," (Set (Var "D")) "holds" (Bool "(" (Bool "(" (Bool (Set (Var "c")) ($#r2_hidden :::"in"::: ) (Set ($#k1_relset_1 :::"dom"::: ) (Set (Var "f")))) & (Bool (Set (Set (Var "f")) ($#k7_partfun1 :::"/."::: ) (Set (Var "c"))) ($#r2_hidden :::"in"::: ) (Set (Var "SD"))) ")" ) "iff" (Bool (Set ($#k4_tarski :::"["::: ) (Set (Var "c")) "," (Set "(" (Set (Var "f")) ($#k7_partfun1 :::"/."::: ) (Set (Var "c")) ")" ) ($#k4_tarski :::"]"::: ) ) ($#r2_hidden :::"in"::: ) (Set (Set (Var "SD")) ($#k3_partfun2 :::"|`"::: ) (Set (Var "f")))) ")" ))))) ; theorem :: PARTFUN2:56 (Bool "for" (Set (Var "C")) "," (Set (Var "D")) "being" ($#~v1_xboole_0 "non" ($#v1_xboole_0 :::"empty"::: ) ) ($#m1_hidden :::"set"::: ) (Bool "for" (Set (Var "SD")) "being" ($#m1_subset_1 :::"Subset":::) "of" (Set (Var "D")) (Bool "for" (Set (Var "c")) "being" ($#m1_subset_1 :::"Element"::: ) "of" (Set (Var "C")) (Bool "for" (Set (Var "f")) "being" ($#m1_subset_1 :::"PartFunc":::) "of" (Set (Var "C")) "," (Set (Var "D")) "holds" (Bool "(" (Bool (Set (Var "c")) ($#r2_hidden :::"in"::: ) (Set (Set (Var "f")) ($#k8_relset_1 :::"""::: ) (Set (Var "SD")))) "iff" (Bool "(" (Bool (Set ($#k4_tarski :::"["::: ) (Set (Var "c")) "," (Set "(" (Set (Var "f")) ($#k7_partfun1 :::"/."::: ) (Set (Var "c")) ")" ) ($#k4_tarski :::"]"::: ) ) ($#r2_hidden :::"in"::: ) (Set (Var "f"))) & (Bool (Set (Set (Var "f")) ($#k7_partfun1 :::"/."::: ) (Set (Var "c"))) ($#r2_hidden :::"in"::: ) (Set (Var "SD"))) ")" ) ")" ))))) ; theorem :: PARTFUN2:57 (Bool "for" (Set (Var "X")) "being" ($#m1_hidden :::"set"::: ) (Bool "for" (Set (Var "D")) "," (Set (Var "C")) "being" ($#~v1_xboole_0 "non" ($#v1_xboole_0 :::"empty"::: ) ) ($#m1_hidden :::"set"::: ) (Bool "for" (Set (Var "f")) "being" ($#m1_subset_1 :::"PartFunc":::) "of" (Set (Var "C")) "," (Set (Var "D")) "holds" (Bool "(" (Bool (Set (Set (Var "f")) ($#k2_partfun1 :::"|"::: ) (Set (Var "X"))) "is" bbbadV3_FUNCT_1()) "iff" (Bool "ex" (Set (Var "d")) "being" ($#m1_subset_1 :::"Element"::: ) "of" (Set (Var "D")) "st" (Bool "for" (Set (Var "c")) "being" ($#m1_subset_1 :::"Element"::: ) "of" (Set (Var "C")) "st" (Bool (Bool (Set (Var "c")) ($#r2_hidden :::"in"::: ) (Set (Set (Var "X")) ($#k9_subset_1 :::"/\"::: ) (Set "(" ($#k1_relset_1 :::"dom"::: ) (Set (Var "f")) ")" )))) "holds" (Bool (Set (Set (Var "f")) ($#k1_funct_1 :::"."::: ) (Set (Var "c"))) ($#r1_hidden :::"="::: ) (Set (Var "d"))))) ")" )))) ; theorem :: PARTFUN2:58 (Bool "for" (Set (Var "X")) "being" ($#m1_hidden :::"set"::: ) (Bool "for" (Set (Var "D")) "," (Set (Var "C")) "being" ($#~v1_xboole_0 "non" ($#v1_xboole_0 :::"empty"::: ) ) ($#m1_hidden :::"set"::: ) (Bool "for" (Set (Var "f")) "being" ($#m1_subset_1 :::"PartFunc":::) "of" (Set (Var "C")) "," (Set (Var "D")) "holds" (Bool "(" (Bool (Set (Set (Var "f")) ($#k2_partfun1 :::"|"::: ) (Set (Var "X"))) "is" bbbadV3_FUNCT_1()) "iff" (Bool "for" (Set (Var "c1")) "," (Set (Var "c2")) "being" ($#m1_subset_1 :::"Element"::: ) "of" (Set (Var "C")) "st" (Bool (Bool (Set (Var "c1")) ($#r2_hidden :::"in"::: ) (Set (Set (Var "X")) ($#k9_subset_1 :::"/\"::: ) (Set "(" ($#k1_relset_1 :::"dom"::: ) (Set (Var "f")) ")" ))) & (Bool (Set (Var "c2")) ($#r2_hidden :::"in"::: ) (Set (Set (Var "X")) ($#k9_subset_1 :::"/\"::: ) (Set "(" ($#k1_relset_1 :::"dom"::: ) (Set (Var "f")) ")" )))) "holds" (Bool (Set (Set (Var "f")) ($#k1_funct_1 :::"."::: ) (Set (Var "c1"))) ($#r1_hidden :::"="::: ) (Set (Set (Var "f")) ($#k1_funct_1 :::"."::: ) (Set (Var "c2"))))) ")" )))) ; theorem :: PARTFUN2:59 (Bool "for" (Set (Var "X")) "being" ($#m1_hidden :::"set"::: ) (Bool "for" (Set (Var "D")) "," (Set (Var "C")) "being" ($#~v1_xboole_0 "non" ($#v1_xboole_0 :::"empty"::: ) ) ($#m1_hidden :::"set"::: ) (Bool "for" (Set (Var "d")) "being" ($#m1_subset_1 :::"Element"::: ) "of" (Set (Var "D")) (Bool "for" (Set (Var "f")) "being" ($#m1_subset_1 :::"PartFunc":::) "of" (Set (Var "C")) "," (Set (Var "D")) "st" (Bool (Bool (Set (Var "d")) ($#r2_hidden :::"in"::: ) (Set (Set (Var "f")) ($#k7_relset_1 :::".:"::: ) (Set (Var "X"))))) "holds" (Bool "ex" (Set (Var "c")) "being" ($#m1_subset_1 :::"Element"::: ) "of" (Set (Var "C")) "st" (Bool "(" (Bool (Set (Var "c")) ($#r2_hidden :::"in"::: ) (Set ($#k1_relset_1 :::"dom"::: ) (Set (Var "f")))) & (Bool (Set (Var "c")) ($#r2_hidden :::"in"::: ) (Set (Var "X"))) & (Bool (Set (Var "d")) ($#r1_hidden :::"="::: ) (Set (Set (Var "f")) ($#k1_funct_1 :::"."::: ) (Set (Var "c")))) ")" )))))) ; theorem :: PARTFUN2:60 (Bool "for" (Set (Var "C")) "," (Set (Var "D")) "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 :::"PartFunc":::) "of" (Set (Var "C")) "," (Set (Var "D")) "st" (Bool (Bool (Set (Var "f")) "is" ($#v2_funct_1 :::"one-to-one"::: ) )) "holds" (Bool "(" (Bool (Set (Var "d")) ($#r2_hidden :::"in"::: ) (Set ($#k2_relset_1 :::"rng"::: ) (Set (Var "f")))) & (Bool (Set (Var "c")) ($#r1_hidden :::"="::: ) (Set (Set "(" (Set (Var "f")) ($#k2_funct_1 :::"""::: ) ")" ) ($#k1_funct_1 :::"."::: ) (Set (Var "d")))) "iff" (Bool "(" (Bool (Set (Var "c")) ($#r2_hidden :::"in"::: ) (Set ($#k1_relset_1 :::"dom"::: ) (Set (Var "f")))) & (Bool (Set (Var "d")) ($#r1_hidden :::"="::: ) (Set (Set (Var "f")) ($#k1_funct_1 :::"."::: ) (Set (Var "c")))) ")" ) ")" ))))) ; theorem :: PARTFUN2:61 (Bool "for" (Set (Var "Y")) "being" ($#m1_hidden :::"set"::: ) (Bool "for" (Set (Var "f")) "," (Set (Var "g")) "being" (Set (Var "b1")) ($#v5_relat_1 :::"-valued"::: ) ($#m1_hidden :::"Function":::) "st" (Bool (Bool (Set (Var "f")) ($#r1_tarski :::"c="::: ) (Set (Var "g")))) "holds" (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")) ($#k7_partfun1 :::"/."::: ) (Set (Var "x"))) ($#r1_hidden :::"="::: ) (Set (Set (Var "g")) ($#k7_partfun1 :::"/."::: ) (Set (Var "x"))))))) ;