:: GRFUNC_1  semantic presentation begin  



















theorem :: GRFUNC_1:1 (Bool  "for" (Set (Var "f")) "being"   ($#m1_hidden :::"Function":::)  (Bool  "for" (Set (Var "G")) "being"    ($#m1_hidden :::"set"::: )    "st" (Bool (Bool (Set (Var "G"))  ($#r1_tarski :::"c="::: )  (Set (Var "f")))) "holds"  (Bool (Set (Var "G")) "is"   ($#m1_hidden :::"Function":::)))) ; 
 
theorem :: GRFUNC_1:2 (Bool  "for" (Set (Var "f")) "," (Set (Var "g")) "being"   ($#m1_hidden :::"Function":::) "holds"   (Bool  "("  (Bool (Set (Var "f"))  ($#r1_tarski :::"c="::: )  (Set (Var "g"))) "iff" (Bool  "("  (Bool (Set   ($#k9_xtuple_0 :::"dom"::: )  (Set (Var "f")))  ($#r1_tarski :::"c="::: )  (Set   ($#k9_xtuple_0 :::"dom"::: )  (Set (Var "g")))) & (Bool  "("   "for" (Set (Var "x")) "being"    ($#m1_hidden :::"set"::: )    "st" (Bool (Bool (Set (Var "x"))  ($#r2_hidden :::"in"::: )  (Set   ($#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 :: GRFUNC_1:3 (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_tarski :::"c="::: )  (Set (Var "g")))) "holds"  (Bool (Set (Var "f"))  ($#r1_hidden :::"="::: )  (Set (Var "g")))) ; 
 
theorem :: GRFUNC_1:4 (Bool  "for" (Set (Var "x")) "," (Set (Var "z")) "being"    ($#m1_hidden :::"set"::: )    (Bool  "for" (Set (Var "g")) "," (Set (Var "f")) "being"   ($#m1_hidden :::"Function":::)  "st" (Bool (Bool (Set  ($#k4_tarski :::"["::: ) (Set (Var "x")) "," (Set (Var "z")) ($#k4_tarski :::"]"::: ) )  ($#r2_hidden :::"in"::: )  (Set (Set (Var "g"))  ($#k3_relat_1 :::"*"::: )  (Set (Var "f"))))) "holds"  (Bool  "("  (Bool (Set  ($#k4_tarski :::"["::: ) (Set (Var "x")) "," (Set  "(" (Set (Var "f"))  ($#k1_funct_1 :::"."::: )  (Set (Var "x")) ")" ) ($#k4_tarski :::"]"::: ) )  ($#r2_hidden :::"in"::: )  (Set (Var "f"))) & (Bool (Set  ($#k4_tarski :::"["::: ) (Set  "(" (Set (Var "f"))  ($#k1_funct_1 :::"."::: )  (Set (Var "x")) ")" ) "," (Set (Var "z")) ($#k4_tarski :::"]"::: ) )  ($#r2_hidden :::"in"::: )  (Set (Var "g")))  ")" ))) ; 
 
theorem :: GRFUNC_1:5 (Bool  "for" (Set (Var "x")) "," (Set (Var "y")) "being"    ($#m1_hidden :::"set"::: )   "holds"  (Bool (Set  ($#k1_tarski :::"{"::: ) (Set  ($#k4_tarski :::"["::: ) (Set (Var "x")) "," (Set (Var "y")) ($#k4_tarski :::"]"::: ) ) ($#k1_tarski :::"}"::: ) ) "is"   ($#m1_hidden :::"Function":::))) ; 
 
theorem :: GRFUNC_1:6 (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"))  ($#r1_hidden :::"="::: )  (Set  ($#k1_tarski :::"{"::: ) (Set  ($#k4_tarski :::"["::: ) (Set (Var "x")) "," (Set (Var "y")) ($#k4_tarski :::"]"::: ) ) ($#k1_tarski :::"}"::: ) ))) "holds"  (Bool (Set (Set (Var "f"))  ($#k1_funct_1 :::"."::: )  (Set (Var "x")))  ($#r1_hidden :::"="::: )  (Set (Var "y"))))) ; 
 
theorem :: GRFUNC_1:7 (Bool  "for" (Set (Var "x")) "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 :::"}"::: ) ))) "holds"  (Bool (Set (Var "f"))  ($#r1_hidden :::"="::: )  (Set  ($#k1_tarski :::"{"::: ) (Set  ($#k4_tarski :::"["::: ) (Set (Var "x")) "," (Set  "(" (Set (Var "f"))  ($#k1_funct_1 :::"."::: )  (Set (Var "x")) ")" ) ($#k4_tarski :::"]"::: ) ) ($#k1_tarski :::"}"::: ) )))) ; 
 
theorem :: GRFUNC_1:8 (Bool  "for" (Set (Var "x1")) "," (Set (Var "y1")) "," (Set (Var "x2")) "," (Set (Var "y2")) "being"    ($#m1_hidden :::"set"::: )   "holds"   (Bool  "("  (Bool (Set  ($#k2_tarski :::"{"::: ) (Set  ($#k4_tarski :::"["::: ) (Set (Var "x1")) "," (Set (Var "y1")) ($#k4_tarski :::"]"::: ) ) "," (Set  ($#k4_tarski :::"["::: ) (Set (Var "x2")) "," (Set (Var "y2")) ($#k4_tarski :::"]"::: ) ) ($#k2_tarski :::"}"::: ) ) "is"   ($#m1_hidden :::"Function":::)) "iff"  "("  (Bool (Bool (Set (Var "x1"))  ($#r1_hidden :::"="::: )  (Set (Var "x2")))) "implies" (Bool (Set (Var "y1"))  ($#r1_hidden :::"="::: )  (Set (Var "y2")))  ")"   ")" )) ; 
 
theorem :: GRFUNC_1:9 (Bool  "for" (Set (Var "f")) "being"   ($#m1_hidden :::"Function":::) "holds"   (Bool  "("  (Bool (Set (Var "f")) "is"   ($#v2_funct_1 :::"one-to-one"::: )  ) "iff" (Bool  "for" (Set (Var "x1")) "," (Set (Var "x2")) "," (Set (Var "y")) "being"    ($#m1_hidden :::"set"::: )    "st" (Bool (Bool (Set  ($#k4_tarski :::"["::: ) (Set (Var "x1")) "," (Set (Var "y")) ($#k4_tarski :::"]"::: ) )  ($#r2_hidden :::"in"::: )  (Set (Var "f"))) & (Bool (Set  ($#k4_tarski :::"["::: ) (Set (Var "x2")) "," (Set (Var "y")) ($#k4_tarski :::"]"::: ) )  ($#r2_hidden :::"in"::: )  (Set (Var "f")))) "holds"  (Bool (Set (Var "x1"))  ($#r1_hidden :::"="::: )  (Set (Var "x2"))))  ")" )) ; 
 
theorem :: GRFUNC_1:10 (Bool  "for" (Set (Var "g")) "," (Set (Var "f")) "being"   ($#m1_hidden :::"Function":::)  "st" (Bool (Bool (Set (Var "g"))  ($#r1_tarski :::"c="::: )  (Set (Var "f"))) & (Bool (Set (Var "f")) "is"   ($#v2_funct_1 :::"one-to-one"::: )  )) "holds"  (Bool (Set (Var "g")) "is"   ($#v2_funct_1 :::"one-to-one"::: )  )) ; 
 registrationlet "f" be   ($#m1_hidden :::"Function":::); let "X" be    ($#m1_hidden :::"set"::: )  ; 
cluster (Set "f"  ($#k3_xboole_0 :::"/\"::: )  "X") ->   ($#v1_funct_1 :::"Function-like"::: )   ; 
end; 
theorem :: GRFUNC_1:11 (Bool  "for" (Set (Var "x")) "being"    ($#m1_hidden :::"set"::: )    (Bool  "for" (Set (Var "f")) "," (Set (Var "g")) "being"   ($#m1_hidden :::"Function":::)  "st" (Bool (Bool (Set (Var "x"))  ($#r2_hidden :::"in"::: )  (Set   ($#k9_xtuple_0 :::"dom"::: )  (Set  "(" (Set (Var "f"))  ($#k3_xboole_0 :::"/\"::: )  (Set (Var "g")) ")" )))) "holds"  (Bool (Set (Set  "(" (Set (Var "f"))  ($#k3_xboole_0 :::"/\"::: )  (Set (Var "g")) ")" )  ($#k1_funct_1 :::"."::: )  (Set (Var "x")))  ($#r1_hidden :::"="::: )  (Set (Set (Var "f"))  ($#k1_funct_1 :::"."::: )  (Set (Var "x")))))) ; 
 
theorem :: GRFUNC_1:12 (Bool  "for" (Set (Var "f")) "," (Set (Var "g")) "being"   ($#m1_hidden :::"Function":::)  "st" (Bool (Bool (Set (Var "f")) "is"   ($#v2_funct_1 :::"one-to-one"::: )  )) "holds"  (Bool (Set (Set (Var "f"))  ($#k3_xboole_0 :::"/\"::: )  (Set (Var "g"))) "is"   ($#v2_funct_1 :::"one-to-one"::: )  )) ; 
 
theorem :: GRFUNC_1:13 (Bool  "for" (Set (Var "f")) "," (Set (Var "g")) "being"   ($#m1_hidden :::"Function":::)  "st" (Bool (Bool (Set   ($#k9_xtuple_0 :::"dom"::: )  (Set (Var "f")))  ($#r1_xboole_0 :::"misses"::: )  (Set   ($#k9_xtuple_0 :::"dom"::: )  (Set (Var "g"))))) "holds"  (Bool (Set (Set (Var "f"))  ($#k2_xboole_0 :::"\/"::: )  (Set (Var "g"))) "is"   ($#m1_hidden :::"Function":::))) ; 
 
theorem :: GRFUNC_1:14 (Bool  "for" (Set (Var "f")) "," (Set (Var "h")) "," (Set (Var "g")) "being"   ($#m1_hidden :::"Function":::)  "st" (Bool (Bool (Set (Var "f"))  ($#r1_tarski :::"c="::: )  (Set (Var "h"))) & (Bool (Set (Var "g"))  ($#r1_tarski :::"c="::: )  (Set (Var "h")))) "holds"  (Bool (Set (Set (Var "f"))  ($#k2_xboole_0 :::"\/"::: )  (Set (Var "g"))) "is"   ($#m1_hidden :::"Function":::))) ; 
 
theorem :: GRFUNC_1:15 (Bool  "for" (Set (Var "x")) "being"    ($#m1_hidden :::"set"::: )    (Bool  "for" (Set (Var "g")) "," (Set (Var "h")) "," (Set (Var "f")) "being"   ($#m1_hidden :::"Function":::)  "st" (Bool (Bool (Set (Var "x"))  ($#r2_hidden :::"in"::: )  (Set   ($#k9_xtuple_0 :::"dom"::: )  (Set (Var "g")))) & (Bool (Set (Var "h"))  ($#r1_hidden :::"="::: )  (Set (Set (Var "f"))  ($#k2_xboole_0 :::"\/"::: )  (Set (Var "g"))))) "holds"  (Bool (Set (Set (Var "h"))  ($#k1_funct_1 :::"."::: )  (Set (Var "x")))  ($#r1_hidden :::"="::: )  (Set (Set (Var "g"))  ($#k1_funct_1 :::"."::: )  (Set (Var "x")))))) ; 
 
theorem :: GRFUNC_1:16 (Bool  "for" (Set (Var "x")) "being"    ($#m1_hidden :::"set"::: )    (Bool  "for" (Set (Var "h")) "," (Set (Var "f")) "," (Set (Var "g")) "being"   ($#m1_hidden :::"Function":::)  "st" (Bool (Bool (Set (Var "x"))  ($#r2_hidden :::"in"::: )  (Set   ($#k9_xtuple_0 :::"dom"::: )  (Set (Var "h")))) & (Bool (Set (Var "h"))  ($#r1_hidden :::"="::: )  (Set (Set (Var "f"))  ($#k2_xboole_0 :::"\/"::: )  (Set (Var "g")))) & (Bool (Bool  "not" (Set (Set (Var "h"))  ($#k1_funct_1 :::"."::: )  (Set (Var "x")))  ($#r1_hidden :::"="::: )  (Set (Set (Var "f"))  ($#k1_funct_1 :::"."::: )  (Set (Var "x")))))) "holds"  (Bool (Set (Set (Var "h"))  ($#k1_funct_1 :::"."::: )  (Set (Var "x")))  ($#r1_hidden :::"="::: )  (Set (Set (Var "g"))  ($#k1_funct_1 :::"."::: )  (Set (Var "x")))))) ; 
 
theorem :: GRFUNC_1:17 (Bool  "for" (Set (Var "f")) "," (Set (Var "g")) "," (Set (Var "h")) "being"   ($#m1_hidden :::"Function":::)  "st" (Bool (Bool (Set (Var "f")) "is"   ($#v2_funct_1 :::"one-to-one"::: )  ) & (Bool (Set (Var "g")) "is"   ($#v2_funct_1 :::"one-to-one"::: )  ) & (Bool (Set (Var "h"))  ($#r1_hidden :::"="::: )  (Set (Set (Var "f"))  ($#k2_xboole_0 :::"\/"::: )  (Set (Var "g")))) & (Bool (Set   ($#k10_xtuple_0 :::"rng"::: )  (Set (Var "f")))  ($#r1_xboole_0 :::"misses"::: )  (Set   ($#k10_xtuple_0 :::"rng"::: )  (Set (Var "g"))))) "holds"  (Bool (Set (Var "h")) "is"   ($#v2_funct_1 :::"one-to-one"::: )  )) ; 
 
theorem :: GRFUNC_1:18 canceled; 
 
theorem :: GRFUNC_1:19 canceled; 
 
theorem :: GRFUNC_1:20 (Bool  "for" (Set (Var "f")) "being"   ($#m1_hidden :::"Function":::)  "st" (Bool (Bool (Set (Var "f")) "is"   ($#v2_funct_1 :::"one-to-one"::: )  )) "holds"  (Bool  "for" (Set (Var "x")) "," (Set (Var "y")) "being"    ($#m1_hidden :::"set"::: )   "holds"   (Bool  "("  (Bool (Set  ($#k4_tarski :::"["::: ) (Set (Var "y")) "," (Set (Var "x")) ($#k4_tarski :::"]"::: ) )  ($#r2_hidden :::"in"::: )  (Set (Set (Var "f"))  ($#k2_funct_1 :::"""::: )  )) "iff" (Bool (Set  ($#k4_tarski :::"["::: ) (Set (Var "x")) "," (Set (Var "y")) ($#k4_tarski :::"]"::: ) )  ($#r2_hidden :::"in"::: )  (Set (Var "f")))  ")" ))) ; 
 
theorem :: GRFUNC_1:21 (Bool  "for" (Set (Var "f")) "being"   ($#m1_hidden :::"Function":::)  "st" (Bool (Bool (Set (Var "f"))  ($#r1_hidden :::"="::: )  (Set   ($#k1_xboole_0 :::"{}"::: )  ))) "holds"  (Bool (Set (Set (Var "f"))  ($#k2_funct_1 :::"""::: )  )  ($#r1_hidden :::"="::: )  (Set   ($#k1_xboole_0 :::"{}"::: )  ))) ; 
 
theorem :: GRFUNC_1:22 (Bool  "for" (Set (Var "x")) "," (Set (Var "X")) "being"    ($#m1_hidden :::"set"::: )    (Bool  "for" (Set (Var "f")) "being"   ($#m1_hidden :::"Function":::) "holds"   (Bool  "("  (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")))  ")" ) "iff" (Bool (Set  ($#k4_tarski :::"["::: ) (Set (Var "x")) "," (Set  "(" (Set (Var "f"))  ($#k1_funct_1 :::"."::: )  (Set (Var "x")) ")" ) ($#k4_tarski :::"]"::: ) )  ($#r2_hidden :::"in"::: )  (Set (Set (Var "f"))  ($#k5_relat_1 :::"|"::: )  (Set (Var "X"))))  ")" ))) ; 
 
theorem :: GRFUNC_1:23 (Bool  "for" (Set (Var "g")) "," (Set (Var "f")) "being"   ($#m1_hidden :::"Function":::)  "st" (Bool (Bool (Set (Var "g"))  ($#r1_tarski :::"c="::: )  (Set (Var "f")))) "holds"  (Bool (Set (Set (Var "f"))  ($#k5_relat_1 :::"|"::: )  (Set  "("  ($#k9_xtuple_0 :::"dom"::: )  (Set (Var "g")) ")" ))  ($#r1_hidden :::"="::: )  (Set (Var "g")))) ; 
 
theorem :: GRFUNC_1:24 (Bool  "for" (Set (Var "x")) "," (Set (Var "Y")) "being"    ($#m1_hidden :::"set"::: )    (Bool  "for" (Set (Var "f")) "being"   ($#m1_hidden :::"Function":::) "holds"   (Bool  "("  (Bool  "("  (Bool (Set (Var "x"))  ($#r2_hidden :::"in"::: )  (Set   ($#k9_xtuple_0 :::"dom"::: )  (Set (Var "f")))) & (Bool (Set (Set (Var "f"))  ($#k1_funct_1 :::"."::: )  (Set (Var "x")))  ($#r2_hidden :::"in"::: )  (Set (Var "Y")))  ")" ) "iff" (Bool (Set  ($#k4_tarski :::"["::: ) (Set (Var "x")) "," (Set  "(" (Set (Var "f"))  ($#k1_funct_1 :::"."::: )  (Set (Var "x")) ")" ) ($#k4_tarski :::"]"::: ) )  ($#r2_hidden :::"in"::: )  (Set (Set (Var "Y"))  ($#k6_relat_1 :::"|`"::: )  (Set (Var "f"))))  ")" ))) ; 
 
theorem :: GRFUNC_1:25 (Bool  "for" (Set (Var "g")) "," (Set (Var "f")) "being"   ($#m1_hidden :::"Function":::)  "st" (Bool (Bool (Set (Var "g"))  ($#r1_tarski :::"c="::: )  (Set (Var "f"))) & (Bool (Set (Var "f")) "is"   ($#v2_funct_1 :::"one-to-one"::: )  )) "holds"  (Bool (Set (Set  "("  ($#k10_xtuple_0 :::"rng"::: )  (Set (Var "g")) ")" )  ($#k6_relat_1 :::"|`"::: )  (Set (Var "f")))  ($#r1_hidden :::"="::: )  (Set (Var "g")))) ; 
 
theorem :: GRFUNC_1:26 (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 (Var "x"))  ($#r2_hidden :::"in"::: )  (Set (Set (Var "f"))  ($#k8_relat_1 :::"""::: )  (Set (Var "Y")))) "iff" (Bool  "("  (Bool (Set  ($#k4_tarski :::"["::: ) (Set (Var "x")) "," (Set  "(" (Set (Var "f"))  ($#k1_funct_1 :::"."::: )  (Set (Var "x")) ")" ) ($#k4_tarski :::"]"::: ) )  ($#r2_hidden :::"in"::: )  (Set (Var "f"))) & (Bool (Set (Set (Var "f"))  ($#k1_funct_1 :::"."::: )  (Set (Var "x")))  ($#r2_hidden :::"in"::: )  (Set (Var "Y")))  ")" )  ")" ))) ; 
 begin  
theorem :: GRFUNC_1:27 (Bool  "for" (Set (Var "X")) "being"    ($#m1_hidden :::"set"::: )    (Bool  "for" (Set (Var "f")) "," (Set (Var "g")) "being"   ($#m1_hidden :::"Function":::)  "st" (Bool (Bool (Set (Var "X"))  ($#r1_tarski :::"c="::: )  (Set   ($#k9_xtuple_0 :::"dom"::: )  (Set (Var "f")))) & (Bool (Set (Var "f"))  ($#r1_tarski :::"c="::: )  (Set (Var "g")))) "holds"  (Bool (Set (Set (Var "f"))  ($#k5_relat_1 :::"|"::: )  (Set (Var "X")))  ($#r1_hidden :::"="::: )  (Set (Set (Var "g"))  ($#k5_relat_1 :::"|"::: )  (Set (Var "X")))))) ; 
 
theorem :: GRFUNC_1:28 (Bool  "for" (Set (Var "f")) "being"   ($#m1_hidden :::"Function":::)  (Bool  "for" (Set (Var "x")) "being"    ($#m1_hidden :::"set"::: )    "st" (Bool (Bool (Set (Var "x"))  ($#r2_hidden :::"in"::: )  (Set   ($#k9_xtuple_0 :::"dom"::: )  (Set (Var "f"))))) "holds"  (Bool (Set (Set (Var "f"))  ($#k5_relat_1 :::"|"::: )  (Set  ($#k1_tarski :::"{"::: ) (Set (Var "x")) ($#k1_tarski :::"}"::: ) ))  ($#r1_hidden :::"="::: )  (Set  ($#k1_tarski :::"{"::: ) (Set  ($#k4_tarski :::"["::: ) (Set (Var "x")) "," (Set  "(" (Set (Var "f"))  ($#k1_funct_1 :::"."::: )  (Set (Var "x")) ")" ) ($#k4_tarski :::"]"::: ) ) ($#k1_tarski :::"}"::: ) )))) ; 
 
theorem :: GRFUNC_1:29 (Bool  "for" (Set (Var "f")) "," (Set (Var "g")) "being"   ($#m1_hidden :::"Function":::)  (Bool  "for" (Set (Var "x")) "being"    ($#m1_hidden :::"set"::: )    "st" (Bool (Bool (Set   ($#k9_xtuple_0 :::"dom"::: )  (Set (Var "f")))  ($#r1_hidden :::"="::: )  (Set   ($#k9_xtuple_0 :::"dom"::: )  (Set (Var "g")))) & (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 (Set (Set (Var "f"))  ($#k5_relat_1 :::"|"::: )  (Set  ($#k1_tarski :::"{"::: ) (Set (Var "x")) ($#k1_tarski :::"}"::: ) ))  ($#r1_hidden :::"="::: )  (Set (Set (Var "g"))  ($#k5_relat_1 :::"|"::: )  (Set  ($#k1_tarski :::"{"::: ) (Set (Var "x")) ($#k1_tarski :::"}"::: ) ))))) ; 
 
theorem :: GRFUNC_1:30 (Bool  "for" (Set (Var "f")) "," (Set (Var "g")) "being"   ($#m1_hidden :::"Function":::)  (Bool  "for" (Set (Var "x")) "," (Set (Var "y")) "being"    ($#m1_hidden :::"set"::: )    "st" (Bool (Bool (Set   ($#k9_xtuple_0 :::"dom"::: )  (Set (Var "f")))  ($#r1_hidden :::"="::: )  (Set   ($#k9_xtuple_0 :::"dom"::: )  (Set (Var "g")))) & (Bool (Set (Set (Var "f"))  ($#k1_funct_1 :::"."::: )  (Set (Var "x")))  ($#r1_hidden :::"="::: )  (Set (Set (Var "g"))  ($#k1_funct_1 :::"."::: )  (Set (Var "x")))) & (Bool (Set (Set (Var "f"))  ($#k1_funct_1 :::"."::: )  (Set (Var "y")))  ($#r1_hidden :::"="::: )  (Set (Set (Var "g"))  ($#k1_funct_1 :::"."::: )  (Set (Var "y"))))) "holds"  (Bool (Set (Set (Var "f"))  ($#k5_relat_1 :::"|"::: )  (Set  ($#k2_tarski :::"{"::: ) (Set (Var "x")) "," (Set (Var "y")) ($#k2_tarski :::"}"::: ) ))  ($#r1_hidden :::"="::: )  (Set (Set (Var "g"))  ($#k5_relat_1 :::"|"::: )  (Set  ($#k2_tarski :::"{"::: ) (Set (Var "x")) "," (Set (Var "y")) ($#k2_tarski :::"}"::: ) ))))) ; 
 
theorem :: GRFUNC_1:31 (Bool  "for" (Set (Var "f")) "," (Set (Var "g")) "being"   ($#m1_hidden :::"Function":::)  (Bool  "for" (Set (Var "x")) "," (Set (Var "y")) "," (Set (Var "z")) "being"    ($#m1_hidden :::"set"::: )    "st" (Bool (Bool (Set   ($#k9_xtuple_0 :::"dom"::: )  (Set (Var "f")))  ($#r1_hidden :::"="::: )  (Set   ($#k9_xtuple_0 :::"dom"::: )  (Set (Var "g")))) & (Bool (Set (Set (Var "f"))  ($#k1_funct_1 :::"."::: )  (Set (Var "x")))  ($#r1_hidden :::"="::: )  (Set (Set (Var "g"))  ($#k1_funct_1 :::"."::: )  (Set (Var "x")))) & (Bool (Set (Set (Var "f"))  ($#k1_funct_1 :::"."::: )  (Set (Var "y")))  ($#r1_hidden :::"="::: )  (Set (Set (Var "g"))  ($#k1_funct_1 :::"."::: )  (Set (Var "y")))) & (Bool (Set (Set (Var "f"))  ($#k1_funct_1 :::"."::: )  (Set (Var "z")))  ($#r1_hidden :::"="::: )  (Set (Set (Var "g"))  ($#k1_funct_1 :::"."::: )  (Set (Var "z"))))) "holds"  (Bool (Set (Set (Var "f"))  ($#k5_relat_1 :::"|"::: )  (Set  ($#k1_enumset1 :::"{"::: ) (Set (Var "x")) "," (Set (Var "y")) "," (Set (Var "z")) ($#k1_enumset1 :::"}"::: ) ))  ($#r1_hidden :::"="::: )  (Set (Set (Var "g"))  ($#k5_relat_1 :::"|"::: )  (Set  ($#k1_enumset1 :::"{"::: ) (Set (Var "x")) "," (Set (Var "y")) "," (Set (Var "z")) ($#k1_enumset1 :::"}"::: ) ))))) ; 
 registrationlet "f" be   ($#m1_hidden :::"Function":::); let "A" be    ($#m1_hidden :::"set"::: )  ; 
cluster (Set "f"  ($#k4_xboole_0 :::"\"::: )  "A") ->   ($#v1_funct_1 :::"Function-like"::: )   ; 
end; 
theorem :: GRFUNC_1:32 (Bool  "for" (Set (Var "x")) "being"    ($#m1_hidden :::"set"::: )    (Bool  "for" (Set (Var "f")) "," (Set (Var "g")) "being"   ($#m1_hidden :::"Function":::)  "st" (Bool (Bool (Set (Var "x"))  ($#r2_hidden :::"in"::: )  (Set (Set  "("  ($#k9_xtuple_0 :::"dom"::: )  (Set (Var "f")) ")" )  ($#k6_subset_1 :::"\"::: )  (Set  "("  ($#k9_xtuple_0 :::"dom"::: )  (Set (Var "g")) ")" )))) "holds"  (Bool (Set (Set  "(" (Set (Var "f"))  ($#k6_subset_1 :::"\"::: )  (Set (Var "g")) ")" )  ($#k1_funct_1 :::"."::: )  (Set (Var "x")))  ($#r1_hidden :::"="::: )  (Set (Set (Var "f"))  ($#k1_funct_1 :::"."::: )  (Set (Var "x")))))) ; 
 
theorem :: GRFUNC_1:33 (Bool  "for" (Set (Var "f")) "," (Set (Var "g")) "," (Set (Var "h")) "being"   ($#m1_hidden :::"Function":::)  "st" (Bool (Bool (Set (Var "f"))  ($#r1_tarski :::"c="::: )  (Set (Var "g"))) & (Bool (Set (Var "f"))  ($#r1_tarski :::"c="::: )  (Set (Var "h")))) "holds"  (Bool (Set (Set (Var "g"))  ($#k5_relat_1 :::"|"::: )  (Set  "("  ($#k9_xtuple_0 :::"dom"::: )  (Set (Var "f")) ")" ))  ($#r1_hidden :::"="::: )  (Set (Set (Var "h"))  ($#k5_relat_1 :::"|"::: )  (Set  "("  ($#k9_xtuple_0 :::"dom"::: )  (Set (Var "f")) ")" )))) ; 
 registrationlet "f" be   ($#m1_hidden :::"Function":::); let "g" be   ($#m1_subset_1 :::"Subset":::) "of" (Set (Const "f")); 
cluster   ($#v1_relat_1 :::"Relation-like"::: )     ($#v1_funct_1 :::"Function-like"::: )   "g"  ($#v5_funct_1 :::"-compatible"::: )    -> "f"  ($#v5_funct_1 :::"-compatible"::: )    for    ($#m1_hidden :::"set"::: )  ; 
end; 
theorem :: GRFUNC_1:34 (Bool  "for" (Set (Var "g")) "," (Set (Var "f")) "being"   ($#m1_hidden :::"Function":::)  "st" (Bool (Bool (Set (Var "g"))  ($#r1_tarski :::"c="::: )  (Set (Var "f")))) "holds"  (Bool (Set (Var "g"))  ($#r1_hidden :::"="::: )  (Set (Set (Var "f"))  ($#k5_relat_1 :::"|"::: )  (Set  "("  ($#k9_xtuple_0 :::"dom"::: )  (Set (Var "g")) ")" )))) ; 
 registrationlet "f" be   ($#m1_hidden :::"Function":::); let "g" be (Set (Const "f"))  ($#v5_funct_1 :::"-compatible"::: )    ($#m1_hidden :::"Function":::); 
cluster   -> "f"  ($#v5_funct_1 :::"-compatible"::: )    for    ($#m1_subset_1 :::"Element"::: )   "of" (Set bbbadK1_ZFMISC_1("g")); 
end; 
theorem :: GRFUNC_1:35 (Bool  "for" (Set (Var "x")) "," (Set (Var "X")) "being"    ($#m1_hidden :::"set"::: )    (Bool  "for" (Set (Var "g")) "," (Set (Var "f")) "being"   ($#m1_hidden :::"Function":::)  "st" (Bool (Bool (Set (Var "g"))  ($#r1_tarski :::"c="::: )  (Set (Var "f"))) & (Bool (Set (Var "x"))  ($#r2_hidden :::"in"::: )  (Set (Var "X"))) & (Bool (Set (Set (Var "X"))  ($#k3_xboole_0 :::"/\"::: )  (Set  "("  ($#k9_xtuple_0 :::"dom"::: )  (Set (Var "f")) ")" ))  ($#r1_tarski :::"c="::: )  (Set   ($#k9_xtuple_0 :::"dom"::: )  (Set (Var "g"))))) "holds"  (Bool (Set (Set (Var "f"))  ($#k1_funct_1 :::"."::: )  (Set (Var "x")))  ($#r1_hidden :::"="::: )  (Set (Set (Var "g"))  ($#k1_funct_1 :::"."::: )  (Set (Var "x")))))) ;