:: RFUNCT_1  semantic presentation begin  






















definitionlet "f1", "f2" be   ($#v1_valued_0 :::"complex-valued"::: )    ($#m1_hidden :::"Function":::); func "f1" :::"/"::: "f2" ->   ($#m1_hidden :::"Function":::) means :: RFUNCT_1:def 1 (Bool  "("  (Bool (Set   ($#k9_xtuple_0 :::"dom"::: )  it)  ($#r1_hidden :::"="::: )  (Set (Set  "("  ($#k9_xtuple_0 :::"dom"::: )  "f1" ")" )  ($#k9_subset_1 :::"/\"::: )  (Set  "(" (Set  "("  ($#k9_xtuple_0 :::"dom"::: )  "f2" ")" )  ($#k6_subset_1 :::"\"::: )  (Set  "(" "f2"  ($#k8_relat_1 :::"""::: )  (Set  ($#k1_tarski :::"{"::: ) (Set  ($#k6_numbers :::"0"::: ) ) ($#k1_tarski :::"}"::: ) ) ")" ) ")" ))) & (Bool  "("   "for" (Set (Var "c")) "being"    ($#m1_hidden :::"set"::: )    "st" (Bool (Bool (Set (Var "c"))  ($#r2_hidden :::"in"::: )  (Set   ($#k9_xtuple_0 :::"dom"::: )  it))) "holds"  (Bool (Set it  ($#k1_funct_1 :::"."::: )  (Set (Var "c")))  ($#r1_hidden :::"="::: )  (Set (Set  "(" "f1"  ($#k1_funct_1 :::"."::: )  (Set (Var "c")) ")" )  ($#k3_xcmplx_0 :::"*"::: )  (Set  "(" (Set  "(" "f2"  ($#k1_funct_1 :::"."::: )  (Set (Var "c")) ")" )  ($#k5_xcmplx_0 :::"""::: )  ")" )))  ")" )  ")" ); end; 






:: deftheorem    defines :::"/"::: RFUNCT_1:def 1 :  (Bool  "for" (Set (Var "f1")) "," (Set (Var "f2")) "being"   ($#v1_valued_0 :::"complex-valued"::: )    ($#m1_hidden :::"Function":::)  (Bool  "for" (Set (Var "b3")) "being"   ($#m1_hidden :::"Function":::) "holds"   (Bool  "("  (Bool (Set (Var "b3"))  ($#r1_hidden :::"="::: )  (Set (Set (Var "f1"))  ($#k1_rfunct_1 :::"/"::: )  (Set (Var "f2")))) "iff" (Bool  "("  (Bool (Set   ($#k9_xtuple_0 :::"dom"::: )  (Set (Var "b3")))  ($#r1_hidden :::"="::: )  (Set (Set  "("  ($#k9_xtuple_0 :::"dom"::: )  (Set (Var "f1")) ")" )  ($#k9_subset_1 :::"/\"::: )  (Set  "(" (Set  "("  ($#k9_xtuple_0 :::"dom"::: )  (Set (Var "f2")) ")" )  ($#k6_subset_1 :::"\"::: )  (Set  "(" (Set (Var "f2"))  ($#k8_relat_1 :::"""::: )  (Set  ($#k1_tarski :::"{"::: ) (Set  ($#k6_numbers :::"0"::: ) ) ($#k1_tarski :::"}"::: ) ) ")" ) ")" ))) & (Bool  "("   "for" (Set (Var "c")) "being"    ($#m1_hidden :::"set"::: )    "st" (Bool (Bool (Set (Var "c"))  ($#r2_hidden :::"in"::: )  (Set   ($#k9_xtuple_0 :::"dom"::: )  (Set (Var "b3"))))) "holds"  (Bool (Set (Set (Var "b3"))  ($#k1_funct_1 :::"."::: )  (Set (Var "c")))  ($#r1_hidden :::"="::: )  (Set (Set  "(" (Set (Var "f1"))  ($#k1_funct_1 :::"."::: )  (Set (Var "c")) ")" )  ($#k3_xcmplx_0 :::"*"::: )  (Set  "(" (Set  "(" (Set (Var "f2"))  ($#k1_funct_1 :::"."::: )  (Set (Var "c")) ")" )  ($#k5_xcmplx_0 :::"""::: )  ")" )))  ")" )  ")" )  ")" ))); 
 registrationlet "f1", "f2" be   ($#v1_valued_0 :::"complex-valued"::: )    ($#m1_hidden :::"Function":::); 
cluster (Set "f1"  ($#k1_rfunct_1 :::"/"::: )  "f2") ->   ($#v1_valued_0 :::"complex-valued"::: )   ; 
end; registrationlet "f1", "f2" be   ($#v3_valued_0 :::"real-valued"::: )    ($#m1_hidden :::"Function":::); 
cluster (Set "f1"  ($#k1_rfunct_1 :::"/"::: )  "f2") ->   ($#v3_valued_0 :::"real-valued"::: )   ; 
end; definitionlet "C" be    ($#m1_hidden :::"set"::: )  ; let "D" be   ($#v1_membered :::"complex-membered"::: )     ($#m1_hidden :::"set"::: )  ; let "f1", "f2" be   ($#m1_subset_1 :::"PartFunc":::) "of" (Set (Const "C")) "," (Set (Const "D")); :: original: :::"/"::: redefine func "f1" :::"/"::: "f2" ->   ($#m1_subset_1 :::"PartFunc":::) "of" "C" "," (Set  ($#k2_numbers :::"COMPLEX"::: ) ); end; definitionlet "C" be    ($#m1_hidden :::"set"::: )  ; let "D" be   ($#v3_membered :::"real-membered"::: )     ($#m1_hidden :::"set"::: )  ; let "f1", "f2" be   ($#m1_subset_1 :::"PartFunc":::) "of" (Set (Const "C")) "," (Set (Const "D")); :: original: :::"/"::: redefine func "f1" :::"/"::: "f2" ->   ($#m1_subset_1 :::"PartFunc":::) "of" "C" "," (Set  ($#k1_numbers :::"REAL"::: ) ); end; definitionlet "f" be   ($#v1_valued_0 :::"complex-valued"::: )    ($#m1_hidden :::"Function":::); func "f" :::"^":::  ->   ($#m1_hidden :::"Function":::) means :: RFUNCT_1:def 2 (Bool  "("  (Bool (Set   ($#k9_xtuple_0 :::"dom"::: )  it)  ($#r1_hidden :::"="::: )  (Set (Set  "("  ($#k9_xtuple_0 :::"dom"::: )  "f" ")" )  ($#k6_subset_1 :::"\"::: )  (Set  "(" "f"  ($#k8_relat_1 :::"""::: )  (Set  ($#k1_tarski :::"{"::: ) (Set  ($#k6_numbers :::"0"::: ) ) ($#k1_tarski :::"}"::: ) ) ")" ))) & (Bool  "("   "for" (Set (Var "c")) "being"    ($#m1_hidden :::"set"::: )    "st" (Bool (Bool (Set (Var "c"))  ($#r2_hidden :::"in"::: )  (Set   ($#k9_xtuple_0 :::"dom"::: )  it))) "holds"  (Bool (Set it  ($#k1_funct_1 :::"."::: )  (Set (Var "c")))  ($#r1_hidden :::"="::: )  (Set (Set  "(" "f"  ($#k1_funct_1 :::"."::: )  (Set (Var "c")) ")" )  ($#k5_xcmplx_0 :::"""::: )  ))  ")" )  ")" ); end; 





:: deftheorem    defines :::"^"::: RFUNCT_1:def 2 :  (Bool  "for" (Set (Var "f")) "being"   ($#v1_valued_0 :::"complex-valued"::: )    ($#m1_hidden :::"Function":::)  (Bool  "for" (Set (Var "b2")) "being"   ($#m1_hidden :::"Function":::) "holds"   (Bool  "("  (Bool (Set (Var "b2"))  ($#r1_hidden :::"="::: )  (Set (Set (Var "f"))  ($#k4_rfunct_1 :::"^"::: )  )) "iff" (Bool  "("  (Bool (Set   ($#k9_xtuple_0 :::"dom"::: )  (Set (Var "b2")))  ($#r1_hidden :::"="::: )  (Set (Set  "("  ($#k9_xtuple_0 :::"dom"::: )  (Set (Var "f")) ")" )  ($#k6_subset_1 :::"\"::: )  (Set  "(" (Set (Var "f"))  ($#k8_relat_1 :::"""::: )  (Set  ($#k1_tarski :::"{"::: ) (Set  ($#k6_numbers :::"0"::: ) ) ($#k1_tarski :::"}"::: ) ) ")" ))) & (Bool  "("   "for" (Set (Var "c")) "being"    ($#m1_hidden :::"set"::: )    "st" (Bool (Bool (Set (Var "c"))  ($#r2_hidden :::"in"::: )  (Set   ($#k9_xtuple_0 :::"dom"::: )  (Set (Var "b2"))))) "holds"  (Bool (Set (Set (Var "b2"))  ($#k1_funct_1 :::"."::: )  (Set (Var "c")))  ($#r1_hidden :::"="::: )  (Set (Set  "(" (Set (Var "f"))  ($#k1_funct_1 :::"."::: )  (Set (Var "c")) ")" )  ($#k5_xcmplx_0 :::"""::: )  ))  ")" )  ")" )  ")" ))); 
 registrationlet "f" be   ($#v1_valued_0 :::"complex-valued"::: )    ($#m1_hidden :::"Function":::); 
cluster (Set "f"  ($#k4_rfunct_1 :::"^"::: )  ) ->   ($#v1_valued_0 :::"complex-valued"::: )   ; 
end; registrationlet "f" be   ($#v3_valued_0 :::"real-valued"::: )    ($#m1_hidden :::"Function":::); 
cluster (Set "f"  ($#k4_rfunct_1 :::"^"::: )  ) ->   ($#v3_valued_0 :::"real-valued"::: )   ; 
end; definitionlet "C" be    ($#m1_hidden :::"set"::: )  ; let "D" be   ($#v1_membered :::"complex-membered"::: )     ($#m1_hidden :::"set"::: )  ; let "f" be   ($#m1_subset_1 :::"PartFunc":::) "of" (Set (Const "C")) "," (Set (Const "D")); :: original: :::"^"::: redefine func "f" :::"^":::  ->   ($#m1_subset_1 :::"PartFunc":::) "of" "C" "," (Set  ($#k2_numbers :::"COMPLEX"::: ) ); end; definitionlet "C" be    ($#m1_hidden :::"set"::: )  ; let "D" be   ($#v3_membered :::"real-membered"::: )     ($#m1_hidden :::"set"::: )  ; let "f" be   ($#m1_subset_1 :::"PartFunc":::) "of" (Set (Const "C")) "," (Set (Const "D")); :: original: :::"^"::: redefine func "f" :::"^":::  ->   ($#m1_subset_1 :::"PartFunc":::) "of" "C" "," (Set  ($#k1_numbers :::"REAL"::: ) ); end; 
theorem :: RFUNCT_1:1 (Bool  "for" (Set (Var "g")) "being"   ($#v1_valued_0 :::"complex-valued"::: )    ($#m1_hidden :::"Function":::) "holds"   (Bool  "("  (Bool (Set   ($#k9_xtuple_0 :::"dom"::: )  (Set  "(" (Set (Var "g"))  ($#k4_rfunct_1 :::"^"::: )  ")" ))  ($#r1_tarski :::"c="::: )  (Set   ($#k9_xtuple_0 :::"dom"::: )  (Set (Var "g")))) & (Bool (Set (Set  "("  ($#k9_xtuple_0 :::"dom"::: )  (Set (Var "g")) ")" )  ($#k9_subset_1 :::"/\"::: )  (Set  "(" (Set  "("  ($#k9_xtuple_0 :::"dom"::: )  (Set (Var "g")) ")" )  ($#k6_subset_1 :::"\"::: )  (Set  "(" (Set (Var "g"))  ($#k8_relat_1 :::"""::: )  (Set  ($#k1_tarski :::"{"::: ) (Set  ($#k6_numbers :::"0"::: ) ) ($#k1_tarski :::"}"::: ) ) ")" ) ")" ))  ($#r1_hidden :::"="::: )  (Set (Set  "("  ($#k9_xtuple_0 :::"dom"::: )  (Set (Var "g")) ")" )  ($#k6_subset_1 :::"\"::: )  (Set  "(" (Set (Var "g"))  ($#k8_relat_1 :::"""::: )  (Set  ($#k1_tarski :::"{"::: ) (Set  ($#k6_numbers :::"0"::: ) ) ($#k1_tarski :::"}"::: ) ) ")" )))  ")" )) ; 
 
theorem :: RFUNCT_1:2 (Bool  "for" (Set (Var "f1")) "," (Set (Var "f2")) "being"   ($#v1_valued_0 :::"complex-valued"::: )    ($#m1_hidden :::"Function":::) "holds"  (Bool (Set (Set  "("  ($#k9_xtuple_0 :::"dom"::: )  (Set  "(" (Set (Var "f1"))  ($#k18_valued_1 :::"(#)"::: )  (Set (Var "f2")) ")" ) ")" )  ($#k6_subset_1 :::"\"::: )  (Set  "(" (Set  "(" (Set (Var "f1"))  ($#k18_valued_1 :::"(#)"::: )  (Set (Var "f2")) ")" )  ($#k8_relat_1 :::"""::: )  (Set  ($#k1_tarski :::"{"::: ) (Set  ($#k6_numbers :::"0"::: ) ) ($#k1_tarski :::"}"::: ) ) ")" ))  ($#r1_hidden :::"="::: )  (Set (Set  "(" (Set  "("  ($#k9_xtuple_0 :::"dom"::: )  (Set (Var "f1")) ")" )  ($#k6_subset_1 :::"\"::: )  (Set  "(" (Set (Var "f1"))  ($#k8_relat_1 :::"""::: )  (Set  ($#k1_tarski :::"{"::: ) (Set  ($#k6_numbers :::"0"::: ) ) ($#k1_tarski :::"}"::: ) ) ")" ) ")" )  ($#k9_subset_1 :::"/\"::: )  (Set  "(" (Set  "("  ($#k9_xtuple_0 :::"dom"::: )  (Set (Var "f2")) ")" )  ($#k6_subset_1 :::"\"::: )  (Set  "(" (Set (Var "f2"))  ($#k8_relat_1 :::"""::: )  (Set  ($#k1_tarski :::"{"::: ) (Set  ($#k6_numbers :::"0"::: ) ) ($#k1_tarski :::"}"::: ) ) ")" ) ")" )))) ; 
 
theorem :: RFUNCT_1:3 (Bool  "for" (Set (Var "C")) "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"   ($#v1_valued_0 :::"complex-valued"::: )    ($#m1_hidden :::"Function":::)  "st" (Bool (Bool (Set (Var "c"))  ($#r2_hidden :::"in"::: )  (Set   ($#k9_xtuple_0 :::"dom"::: )  (Set  "(" (Set (Var "f"))  ($#k4_rfunct_1 :::"^"::: )  ")" )))) "holds"  (Bool (Set (Set (Var "f"))  ($#k1_funct_1 :::"."::: )  (Set (Var "c")))  ($#r1_hidden :::"<>"::: )  (Set   ($#k6_numbers :::"0"::: )  ))))) ; 
 
theorem :: RFUNCT_1:4 (Bool  "for" (Set (Var "f")) "being"   ($#v1_valued_0 :::"complex-valued"::: )    ($#m1_hidden :::"Function":::) "holds"  (Bool (Set (Set  "(" (Set (Var "f"))  ($#k4_rfunct_1 :::"^"::: )  ")" )  ($#k8_relat_1 :::"""::: )  (Set  ($#k1_tarski :::"{"::: ) (Set  ($#k6_numbers :::"0"::: ) ) ($#k1_tarski :::"}"::: ) ))  ($#r1_hidden :::"="::: )  (Set   ($#k1_xboole_0 :::"{}"::: )  ))) ; 
 
theorem :: RFUNCT_1:5 (Bool  "for" (Set (Var "f")) "being"   ($#v1_valued_0 :::"complex-valued"::: )    ($#m1_hidden :::"Function":::) "holds"   (Bool  "("  (Bool (Set (Set  "("  ($#k54_valued_1 :::"abs"::: )  (Set (Var "f")) ")" )  ($#k8_relat_1 :::"""::: )  (Set  ($#k1_tarski :::"{"::: ) (Set  ($#k6_numbers :::"0"::: ) ) ($#k1_tarski :::"}"::: ) ))  ($#r1_hidden :::"="::: )  (Set (Set (Var "f"))  ($#k8_relat_1 :::"""::: )  (Set  ($#k1_tarski :::"{"::: ) (Set  ($#k6_numbers :::"0"::: ) ) ($#k1_tarski :::"}"::: ) ))) & (Bool (Set (Set  "("  ($#k30_valued_1 :::"-"::: )  (Set (Var "f")) ")" )  ($#k8_relat_1 :::"""::: )  (Set  ($#k1_tarski :::"{"::: ) (Set  ($#k6_numbers :::"0"::: ) ) ($#k1_tarski :::"}"::: ) ))  ($#r1_hidden :::"="::: )  (Set (Set (Var "f"))  ($#k8_relat_1 :::"""::: )  (Set  ($#k1_tarski :::"{"::: ) (Set  ($#k6_numbers :::"0"::: ) ) ($#k1_tarski :::"}"::: ) )))  ")" )) ; 
 
theorem :: RFUNCT_1:6 (Bool  "for" (Set (Var "f")) "being"   ($#v1_valued_0 :::"complex-valued"::: )    ($#m1_hidden :::"Function":::) "holds"  (Bool (Set   ($#k9_xtuple_0 :::"dom"::: )  (Set  "(" (Set  "(" (Set (Var "f"))  ($#k4_rfunct_1 :::"^"::: )  ")" )  ($#k4_rfunct_1 :::"^"::: )  ")" ))  ($#r1_hidden :::"="::: )  (Set   ($#k9_xtuple_0 :::"dom"::: )  (Set  "(" (Set (Var "f"))  ($#k5_relat_1 :::"|"::: )  (Set  "("  ($#k9_xtuple_0 :::"dom"::: )  (Set  "(" (Set (Var "f"))  ($#k4_rfunct_1 :::"^"::: )  ")" ) ")" ) ")" )))) ; 
 
theorem :: RFUNCT_1:7 (Bool  "for" (Set (Var "f")) "being"   ($#v1_valued_0 :::"complex-valued"::: )    ($#m1_hidden :::"Function":::)  (Bool  "for" (Set (Var "r")) "being"   ($#v1_xcmplx_0 :::"complex"::: )     ($#m1_hidden :::"number"::: )    "st" (Bool (Bool (Set (Var "r"))  ($#r1_hidden :::"<>"::: )  (Set   ($#k6_numbers :::"0"::: )  ))) "holds"  (Bool (Set (Set  "(" (Set (Var "r"))  ($#k24_valued_1 :::"(#)"::: )  (Set (Var "f")) ")" )  ($#k8_relat_1 :::"""::: )  (Set  ($#k1_tarski :::"{"::: ) (Set  ($#k6_numbers :::"0"::: ) ) ($#k1_tarski :::"}"::: ) ))  ($#r1_hidden :::"="::: )  (Set (Set (Var "f"))  ($#k8_relat_1 :::"""::: )  (Set  ($#k1_tarski :::"{"::: ) (Set  ($#k6_numbers :::"0"::: ) ) ($#k1_tarski :::"}"::: ) ))))) ; 
 
theorem :: RFUNCT_1:8 (Bool  "for" (Set (Var "f1")) "," (Set (Var "f2")) "," (Set (Var "f3")) "being"   ($#v1_valued_0 :::"complex-valued"::: )    ($#m1_hidden :::"Function":::) "holds"  (Bool (Set (Set  "(" (Set (Var "f1"))  ($#k1_valued_1 :::"+"::: )  (Set (Var "f2")) ")" )  ($#k1_valued_1 :::"+"::: )  (Set (Var "f3")))  ($#r1_hidden :::"="::: )  (Set (Set (Var "f1"))  ($#k1_valued_1 :::"+"::: )  (Set  "(" (Set (Var "f2"))  ($#k1_valued_1 :::"+"::: )  (Set (Var "f3")) ")" )))) ; 
 
theorem :: RFUNCT_1:9 (Bool  "for" (Set (Var "f1")) "," (Set (Var "f2")) "," (Set (Var "f3")) "being"   ($#v1_valued_0 :::"complex-valued"::: )    ($#m1_hidden :::"Function":::) "holds"  (Bool (Set (Set  "(" (Set (Var "f1"))  ($#k18_valued_1 :::"(#)"::: )  (Set (Var "f2")) ")" )  ($#k18_valued_1 :::"(#)"::: )  (Set (Var "f3")))  ($#r1_hidden :::"="::: )  (Set (Set (Var "f1"))  ($#k18_valued_1 :::"(#)"::: )  (Set  "(" (Set (Var "f2"))  ($#k18_valued_1 :::"(#)"::: )  (Set (Var "f3")) ")" )))) ; 
 
theorem :: RFUNCT_1:10 (Bool  "for" (Set (Var "f1")) "," (Set (Var "f2")) "," (Set (Var "f3")) "being"   ($#v1_valued_0 :::"complex-valued"::: )    ($#m1_hidden :::"Function":::) "holds"  (Bool (Set (Set  "(" (Set (Var "f1"))  ($#k1_valued_1 :::"+"::: )  (Set (Var "f2")) ")" )  ($#k18_valued_1 :::"(#)"::: )  (Set (Var "f3")))  ($#r1_hidden :::"="::: )  (Set (Set  "(" (Set (Var "f1"))  ($#k18_valued_1 :::"(#)"::: )  (Set (Var "f3")) ")" )  ($#k1_valued_1 :::"+"::: )  (Set  "(" (Set (Var "f2"))  ($#k18_valued_1 :::"(#)"::: )  (Set (Var "f3")) ")" )))) ; 
 
theorem :: RFUNCT_1:11 (Bool  "for" (Set (Var "f3")) "," (Set (Var "f1")) "," (Set (Var "f2")) "being"   ($#v1_valued_0 :::"complex-valued"::: )    ($#m1_hidden :::"Function":::) "holds"  (Bool (Set (Set (Var "f3"))  ($#k18_valued_1 :::"(#)"::: )  (Set  "(" (Set (Var "f1"))  ($#k1_valued_1 :::"+"::: )  (Set (Var "f2")) ")" ))  ($#r1_hidden :::"="::: )  (Set (Set  "(" (Set (Var "f3"))  ($#k18_valued_1 :::"(#)"::: )  (Set (Var "f1")) ")" )  ($#k1_valued_1 :::"+"::: )  (Set  "(" (Set (Var "f3"))  ($#k18_valued_1 :::"(#)"::: )  (Set (Var "f2")) ")" )))) ; 
 
theorem :: RFUNCT_1:12 (Bool  "for" (Set (Var "f1")) "," (Set (Var "f2")) "being"   ($#v1_valued_0 :::"complex-valued"::: )    ($#m1_hidden :::"Function":::)  (Bool  "for" (Set (Var "r")) "being"   ($#v1_xcmplx_0 :::"complex"::: )     ($#m1_hidden :::"number"::: )   "holds"  (Bool (Set (Set (Var "r"))  ($#k24_valued_1 :::"(#)"::: )  (Set  "(" (Set (Var "f1"))  ($#k18_valued_1 :::"(#)"::: )  (Set (Var "f2")) ")" ))  ($#r1_hidden :::"="::: )  (Set (Set  "(" (Set (Var "r"))  ($#k24_valued_1 :::"(#)"::: )  (Set (Var "f1")) ")" )  ($#k18_valued_1 :::"(#)"::: )  (Set (Var "f2")))))) ; 
 
theorem :: RFUNCT_1:13 (Bool  "for" (Set (Var "f1")) "," (Set (Var "f2")) "being"   ($#v1_valued_0 :::"complex-valued"::: )    ($#m1_hidden :::"Function":::)  (Bool  "for" (Set (Var "r")) "being"   ($#v1_xcmplx_0 :::"complex"::: )     ($#m1_hidden :::"number"::: )   "holds"  (Bool (Set (Set (Var "r"))  ($#k24_valued_1 :::"(#)"::: )  (Set  "(" (Set (Var "f1"))  ($#k18_valued_1 :::"(#)"::: )  (Set (Var "f2")) ")" ))  ($#r1_hidden :::"="::: )  (Set (Set (Var "f1"))  ($#k18_valued_1 :::"(#)"::: )  (Set  "(" (Set (Var "r"))  ($#k24_valued_1 :::"(#)"::: )  (Set (Var "f2")) ")" ))))) ; 
 
theorem :: RFUNCT_1:14 (Bool  "for" (Set (Var "f1")) "," (Set (Var "f2")) "," (Set (Var "f3")) "being"   ($#v1_valued_0 :::"complex-valued"::: )    ($#m1_hidden :::"Function":::) "holds"  (Bool (Set (Set  "(" (Set (Var "f1"))  ($#k45_valued_1 :::"-"::: )  (Set (Var "f2")) ")" )  ($#k18_valued_1 :::"(#)"::: )  (Set (Var "f3")))  ($#r1_hidden :::"="::: )  (Set (Set  "(" (Set (Var "f1"))  ($#k18_valued_1 :::"(#)"::: )  (Set (Var "f3")) ")" )  ($#k45_valued_1 :::"-"::: )  (Set  "(" (Set (Var "f2"))  ($#k18_valued_1 :::"(#)"::: )  (Set (Var "f3")) ")" )))) ; 
 
theorem :: RFUNCT_1:15 (Bool  "for" (Set (Var "f3")) "," (Set (Var "f1")) "," (Set (Var "f2")) "being"   ($#v1_valued_0 :::"complex-valued"::: )    ($#m1_hidden :::"Function":::) "holds"  (Bool (Set (Set  "(" (Set (Var "f3"))  ($#k18_valued_1 :::"(#)"::: )  (Set (Var "f1")) ")" )  ($#k45_valued_1 :::"-"::: )  (Set  "(" (Set (Var "f3"))  ($#k18_valued_1 :::"(#)"::: )  (Set (Var "f2")) ")" ))  ($#r1_hidden :::"="::: )  (Set (Set (Var "f3"))  ($#k18_valued_1 :::"(#)"::: )  (Set  "(" (Set (Var "f1"))  ($#k45_valued_1 :::"-"::: )  (Set (Var "f2")) ")" )))) ; 
 
theorem :: RFUNCT_1:16 (Bool  "for" (Set (Var "f1")) "," (Set (Var "f2")) "being"   ($#v1_valued_0 :::"complex-valued"::: )    ($#m1_hidden :::"Function":::)  (Bool  "for" (Set (Var "r")) "being"   ($#v1_xcmplx_0 :::"complex"::: )     ($#m1_hidden :::"number"::: )   "holds"  (Bool (Set (Set (Var "r"))  ($#k24_valued_1 :::"(#)"::: )  (Set  "(" (Set (Var "f1"))  ($#k1_valued_1 :::"+"::: )  (Set (Var "f2")) ")" ))  ($#r1_hidden :::"="::: )  (Set (Set  "(" (Set (Var "r"))  ($#k24_valued_1 :::"(#)"::: )  (Set (Var "f1")) ")" )  ($#k1_valued_1 :::"+"::: )  (Set  "(" (Set (Var "r"))  ($#k24_valued_1 :::"(#)"::: )  (Set (Var "f2")) ")" ))))) ; 
 
theorem :: RFUNCT_1:17 (Bool  "for" (Set (Var "f")) "being"   ($#v1_valued_0 :::"complex-valued"::: )    ($#m1_hidden :::"Function":::)  (Bool  "for" (Set (Var "r")) "," (Set (Var "p")) "being"   ($#v1_xcmplx_0 :::"complex"::: )     ($#m1_hidden :::"number"::: )   "holds"  (Bool (Set (Set  "(" (Set (Var "r"))  ($#k3_xcmplx_0 :::"*"::: )  (Set (Var "p")) ")" )  ($#k24_valued_1 :::"(#)"::: )  (Set (Var "f")))  ($#r1_hidden :::"="::: )  (Set (Set (Var "r"))  ($#k24_valued_1 :::"(#)"::: )  (Set  "(" (Set (Var "p"))  ($#k24_valued_1 :::"(#)"::: )  (Set (Var "f")) ")" ))))) ; 
 
theorem :: RFUNCT_1:18 (Bool  "for" (Set (Var "f1")) "," (Set (Var "f2")) "being"   ($#v1_valued_0 :::"complex-valued"::: )    ($#m1_hidden :::"Function":::)  (Bool  "for" (Set (Var "r")) "being"   ($#v1_xcmplx_0 :::"complex"::: )     ($#m1_hidden :::"number"::: )   "holds"  (Bool (Set (Set (Var "r"))  ($#k24_valued_1 :::"(#)"::: )  (Set  "(" (Set (Var "f1"))  ($#k45_valued_1 :::"-"::: )  (Set (Var "f2")) ")" ))  ($#r1_hidden :::"="::: )  (Set (Set  "(" (Set (Var "r"))  ($#k24_valued_1 :::"(#)"::: )  (Set (Var "f1")) ")" )  ($#k45_valued_1 :::"-"::: )  (Set  "(" (Set (Var "r"))  ($#k24_valued_1 :::"(#)"::: )  (Set (Var "f2")) ")" ))))) ; 
 
theorem :: RFUNCT_1:19 (Bool  "for" (Set (Var "f1")) "," (Set (Var "f2")) "being"   ($#v1_valued_0 :::"complex-valued"::: )    ($#m1_hidden :::"Function":::) "holds"  (Bool (Set (Set (Var "f1"))  ($#k45_valued_1 :::"-"::: )  (Set (Var "f2")))  ($#r1_hidden :::"="::: )  (Set (Set  "("  ($#k1_real_1 :::"-"::: )  (Num 1) ")" )  ($#k24_valued_1 :::"(#)"::: )  (Set  "(" (Set (Var "f2"))  ($#k45_valued_1 :::"-"::: )  (Set (Var "f1")) ")" )))) ; 
 
theorem :: RFUNCT_1:20 (Bool  "for" (Set (Var "f1")) "," (Set (Var "f2")) "," (Set (Var "f3")) "being"   ($#v1_valued_0 :::"complex-valued"::: )    ($#m1_hidden :::"Function":::) "holds"  (Bool (Set (Set (Var "f1"))  ($#k45_valued_1 :::"-"::: )  (Set  "(" (Set (Var "f2"))  ($#k1_valued_1 :::"+"::: )  (Set (Var "f3")) ")" ))  ($#r1_hidden :::"="::: )  (Set (Set  "(" (Set (Var "f1"))  ($#k45_valued_1 :::"-"::: )  (Set (Var "f2")) ")" )  ($#k45_valued_1 :::"-"::: )  (Set (Var "f3"))))) ; 
 
theorem :: RFUNCT_1:21 (Bool  "for" (Set (Var "f")) "being"   ($#v1_valued_0 :::"complex-valued"::: )    ($#m1_hidden :::"Function":::) "holds"  (Bool (Set (Num 1)  ($#k24_valued_1 :::"(#)"::: )  (Set (Var "f")))  ($#r1_hidden :::"="::: )  (Set (Var "f")))) ; 
 
theorem :: RFUNCT_1:22 (Bool  "for" (Set (Var "f1")) "," (Set (Var "f2")) "," (Set (Var "f3")) "being"   ($#v1_valued_0 :::"complex-valued"::: )    ($#m1_hidden :::"Function":::) "holds"  (Bool (Set (Set (Var "f1"))  ($#k45_valued_1 :::"-"::: )  (Set  "(" (Set (Var "f2"))  ($#k45_valued_1 :::"-"::: )  (Set (Var "f3")) ")" ))  ($#r1_hidden :::"="::: )  (Set (Set  "(" (Set (Var "f1"))  ($#k45_valued_1 :::"-"::: )  (Set (Var "f2")) ")" )  ($#k1_valued_1 :::"+"::: )  (Set (Var "f3"))))) ; 
 
theorem :: RFUNCT_1:23 (Bool  "for" (Set (Var "f1")) "," (Set (Var "f2")) "," (Set (Var "f3")) "being"   ($#v1_valued_0 :::"complex-valued"::: )    ($#m1_hidden :::"Function":::) "holds"  (Bool (Set (Set (Var "f1"))  ($#k1_valued_1 :::"+"::: )  (Set  "(" (Set (Var "f2"))  ($#k45_valued_1 :::"-"::: )  (Set (Var "f3")) ")" ))  ($#r1_hidden :::"="::: )  (Set (Set  "(" (Set (Var "f1"))  ($#k1_valued_1 :::"+"::: )  (Set (Var "f2")) ")" )  ($#k45_valued_1 :::"-"::: )  (Set (Var "f3"))))) ; 
 
theorem :: RFUNCT_1:24 (Bool  "for" (Set (Var "f1")) "," (Set (Var "f2")) "being"   ($#v1_valued_0 :::"complex-valued"::: )    ($#m1_hidden :::"Function":::) "holds"  (Bool (Set   ($#k54_valued_1 :::"abs"::: )  (Set  "(" (Set (Var "f1"))  ($#k18_valued_1 :::"(#)"::: )  (Set (Var "f2")) ")" ))  ($#r1_hidden :::"="::: )  (Set (Set  "("  ($#k54_valued_1 :::"abs"::: )  (Set (Var "f1")) ")" )  ($#k18_valued_1 :::"(#)"::: )  (Set  "("  ($#k54_valued_1 :::"abs"::: )  (Set (Var "f2")) ")" )))) ; 
 
theorem :: RFUNCT_1:25 (Bool  "for" (Set (Var "f")) "being"   ($#v1_valued_0 :::"complex-valued"::: )    ($#m1_hidden :::"Function":::)  (Bool  "for" (Set (Var "r")) "being"   ($#v1_xcmplx_0 :::"complex"::: )     ($#m1_hidden :::"number"::: )   "holds"  (Bool (Set   ($#k54_valued_1 :::"abs"::: )  (Set  "(" (Set (Var "r"))  ($#k24_valued_1 :::"(#)"::: )  (Set (Var "f")) ")" ))  ($#r1_hidden :::"="::: )  (Set (Set  "("  ($#k18_complex1 :::"abs"::: )  (Set (Var "r")) ")" )  ($#k24_valued_1 :::"(#)"::: )  (Set  "("  ($#k54_valued_1 :::"abs"::: )  (Set (Var "f")) ")" ))))) ; 
 
theorem :: RFUNCT_1:26 (Bool  "for" (Set (Var "f")) "being"   ($#v1_valued_0 :::"complex-valued"::: )    ($#m1_hidden :::"Function":::) "holds"  (Bool (Set (Set  "(" (Set (Var "f"))  ($#k4_rfunct_1 :::"^"::: )  ")" )  ($#k4_rfunct_1 :::"^"::: )  )  ($#r1_hidden :::"="::: )  (Set (Set (Var "f"))  ($#k5_relat_1 :::"|"::: )  (Set  "("  ($#k9_xtuple_0 :::"dom"::: )  (Set  "(" (Set (Var "f"))  ($#k4_rfunct_1 :::"^"::: )  ")" ) ")" )))) ; 
 
theorem :: RFUNCT_1:27 (Bool  "for" (Set (Var "f1")) "," (Set (Var "f2")) "being"   ($#v1_valued_0 :::"complex-valued"::: )    ($#m1_hidden :::"Function":::) "holds"  (Bool (Set (Set  "(" (Set (Var "f1"))  ($#k18_valued_1 :::"(#)"::: )  (Set (Var "f2")) ")" )  ($#k4_rfunct_1 :::"^"::: )  )  ($#r1_hidden :::"="::: )  (Set (Set  "(" (Set (Var "f1"))  ($#k4_rfunct_1 :::"^"::: )  ")" )  ($#k18_valued_1 :::"(#)"::: )  (Set  "(" (Set (Var "f2"))  ($#k4_rfunct_1 :::"^"::: )  ")" )))) ; 
 
theorem :: RFUNCT_1:28 (Bool  "for" (Set (Var "f")) "being"   ($#v1_valued_0 :::"complex-valued"::: )    ($#m1_hidden :::"Function":::)  (Bool  "for" (Set (Var "r")) "being"   ($#v1_xcmplx_0 :::"complex"::: )     ($#m1_hidden :::"number"::: )    "st" (Bool (Bool (Set (Var "r"))  ($#r1_hidden :::"<>"::: )  (Set   ($#k6_numbers :::"0"::: )  ))) "holds"  (Bool (Set (Set  "(" (Set (Var "r"))  ($#k24_valued_1 :::"(#)"::: )  (Set (Var "f")) ")" )  ($#k4_rfunct_1 :::"^"::: )  )  ($#r1_hidden :::"="::: )  (Set (Set  "(" (Set (Var "r"))  ($#k5_xcmplx_0 :::"""::: )  ")" )  ($#k24_valued_1 :::"(#)"::: )  (Set  "(" (Set (Var "f"))  ($#k4_rfunct_1 :::"^"::: )  ")" ))))) ; 
 
theorem :: RFUNCT_1:29 (Bool  "for" (Set (Var "f")) "being"   ($#v1_valued_0 :::"complex-valued"::: )    ($#m1_hidden :::"Function":::) "holds"  (Bool (Set (Set  "("  ($#k30_valued_1 :::"-"::: )  (Set (Var "f")) ")" )  ($#k4_rfunct_1 :::"^"::: )  )  ($#r1_hidden :::"="::: )  (Set (Set  "("  ($#k1_real_1 :::"-"::: )  (Num 1) ")" )  ($#k24_valued_1 :::"(#)"::: )  (Set  "(" (Set (Var "f"))  ($#k4_rfunct_1 :::"^"::: )  ")" )))) ; 
 
theorem :: RFUNCT_1:30 (Bool  "for" (Set (Var "f")) "being"   ($#v1_valued_0 :::"complex-valued"::: )    ($#m1_hidden :::"Function":::) "holds"  (Bool (Set (Set  "("  ($#k54_valued_1 :::"abs"::: )  (Set (Var "f")) ")" )  ($#k4_rfunct_1 :::"^"::: )  )  ($#r1_hidden :::"="::: )  (Set   ($#k54_valued_1 :::"abs"::: )  (Set  "(" (Set (Var "f"))  ($#k4_rfunct_1 :::"^"::: )  ")" )))) ; 
 
theorem :: RFUNCT_1:31 (Bool  "for" (Set (Var "f")) "," (Set (Var "g")) "being"   ($#v1_valued_0 :::"complex-valued"::: )    ($#m1_hidden :::"Function":::) "holds"  (Bool (Set (Set (Var "f"))  ($#k1_rfunct_1 :::"/"::: )  (Set (Var "g")))  ($#r1_hidden :::"="::: )  (Set (Set (Var "f"))  ($#k18_valued_1 :::"(#)"::: )  (Set  "(" (Set (Var "g"))  ($#k4_rfunct_1 :::"^"::: )  ")" )))) ; 
 
theorem :: RFUNCT_1:32 (Bool  "for" (Set (Var "g")) "," (Set (Var "f")) "being"   ($#v1_valued_0 :::"complex-valued"::: )    ($#m1_hidden :::"Function":::)  (Bool  "for" (Set (Var "r")) "being"   ($#v1_xcmplx_0 :::"complex"::: )     ($#m1_hidden :::"number"::: )   "holds"  (Bool (Set (Set (Var "r"))  ($#k24_valued_1 :::"(#)"::: )  (Set  "(" (Set (Var "g"))  ($#k1_rfunct_1 :::"/"::: )  (Set (Var "f")) ")" ))  ($#r1_hidden :::"="::: )  (Set (Set  "(" (Set (Var "r"))  ($#k24_valued_1 :::"(#)"::: )  (Set (Var "g")) ")" )  ($#k1_rfunct_1 :::"/"::: )  (Set (Var "f")))))) ; 
 
theorem :: RFUNCT_1:33 (Bool  "for" (Set (Var "f")) "," (Set (Var "g")) "being"   ($#v1_valued_0 :::"complex-valued"::: )    ($#m1_hidden :::"Function":::) "holds"  (Bool (Set (Set  "(" (Set (Var "f"))  ($#k1_rfunct_1 :::"/"::: )  (Set (Var "g")) ")" )  ($#k18_valued_1 :::"(#)"::: )  (Set (Var "g")))  ($#r1_hidden :::"="::: )  (Set (Set (Var "f"))  ($#k5_relat_1 :::"|"::: )  (Set  "("  ($#k9_xtuple_0 :::"dom"::: )  (Set  "(" (Set (Var "g"))  ($#k4_rfunct_1 :::"^"::: )  ")" ) ")" )))) ; 
 
theorem :: RFUNCT_1:34 (Bool  "for" (Set (Var "f")) "," (Set (Var "g")) "," (Set (Var "f1")) "," (Set (Var "g1")) "being"   ($#v1_valued_0 :::"complex-valued"::: )    ($#m1_hidden :::"Function":::) "holds"  (Bool (Set (Set  "(" (Set (Var "f"))  ($#k1_rfunct_1 :::"/"::: )  (Set (Var "g")) ")" )  ($#k18_valued_1 :::"(#)"::: )  (Set  "(" (Set (Var "f1"))  ($#k1_rfunct_1 :::"/"::: )  (Set (Var "g1")) ")" ))  ($#r1_hidden :::"="::: )  (Set (Set  "(" (Set (Var "f"))  ($#k18_valued_1 :::"(#)"::: )  (Set (Var "f1")) ")" )  ($#k1_rfunct_1 :::"/"::: )  (Set  "(" (Set (Var "g"))  ($#k18_valued_1 :::"(#)"::: )  (Set (Var "g1")) ")" )))) ; 
 
theorem :: RFUNCT_1:35 (Bool  "for" (Set (Var "f1")) "," (Set (Var "f2")) "being"   ($#v1_valued_0 :::"complex-valued"::: )    ($#m1_hidden :::"Function":::) "holds"  (Bool (Set (Set  "(" (Set (Var "f1"))  ($#k1_rfunct_1 :::"/"::: )  (Set (Var "f2")) ")" )  ($#k4_rfunct_1 :::"^"::: )  )  ($#r1_hidden :::"="::: )  (Set (Set  "(" (Set (Var "f2"))  ($#k5_relat_1 :::"|"::: )  (Set  "("  ($#k9_xtuple_0 :::"dom"::: )  (Set  "(" (Set (Var "f2"))  ($#k4_rfunct_1 :::"^"::: )  ")" ) ")" ) ")" )  ($#k1_rfunct_1 :::"/"::: )  (Set (Var "f1"))))) ; 
 
theorem :: RFUNCT_1:36 (Bool  "for" (Set (Var "g")) "," (Set (Var "f1")) "," (Set (Var "f2")) "being"   ($#v1_valued_0 :::"complex-valued"::: )    ($#m1_hidden :::"Function":::) "holds"  (Bool (Set (Set (Var "g"))  ($#k18_valued_1 :::"(#)"::: )  (Set  "(" (Set (Var "f1"))  ($#k1_rfunct_1 :::"/"::: )  (Set (Var "f2")) ")" ))  ($#r1_hidden :::"="::: )  (Set (Set  "(" (Set (Var "g"))  ($#k18_valued_1 :::"(#)"::: )  (Set (Var "f1")) ")" )  ($#k1_rfunct_1 :::"/"::: )  (Set (Var "f2"))))) ; 
 
theorem :: RFUNCT_1:37 (Bool  "for" (Set (Var "g")) "," (Set (Var "f1")) "," (Set (Var "f2")) "being"   ($#v1_valued_0 :::"complex-valued"::: )    ($#m1_hidden :::"Function":::) "holds"  (Bool (Set (Set (Var "g"))  ($#k1_rfunct_1 :::"/"::: )  (Set  "(" (Set (Var "f1"))  ($#k1_rfunct_1 :::"/"::: )  (Set (Var "f2")) ")" ))  ($#r1_hidden :::"="::: )  (Set (Set  "(" (Set (Var "g"))  ($#k18_valued_1 :::"(#)"::: )  (Set  "(" (Set (Var "f2"))  ($#k5_relat_1 :::"|"::: )  (Set  "("  ($#k9_xtuple_0 :::"dom"::: )  (Set  "(" (Set (Var "f2"))  ($#k4_rfunct_1 :::"^"::: )  ")" ) ")" ) ")" ) ")" )  ($#k1_rfunct_1 :::"/"::: )  (Set (Var "f1"))))) ; 
 
theorem :: RFUNCT_1:38 (Bool  "for" (Set (Var "f")) "," (Set (Var "g")) "being"   ($#v1_valued_0 :::"complex-valued"::: )    ($#m1_hidden :::"Function":::) "holds"   (Bool  "("  (Bool (Set   ($#k30_valued_1 :::"-"::: )  (Set  "(" (Set (Var "f"))  ($#k1_rfunct_1 :::"/"::: )  (Set (Var "g")) ")" ))  ($#r1_hidden :::"="::: )  (Set (Set  "("  ($#k30_valued_1 :::"-"::: )  (Set (Var "f")) ")" )  ($#k1_rfunct_1 :::"/"::: )  (Set (Var "g")))) & (Bool (Set (Set (Var "f"))  ($#k1_rfunct_1 :::"/"::: )  (Set  "("  ($#k30_valued_1 :::"-"::: )  (Set (Var "g")) ")" ))  ($#r1_hidden :::"="::: )  (Set   ($#k30_valued_1 :::"-"::: )  (Set  "(" (Set (Var "f"))  ($#k1_rfunct_1 :::"/"::: )  (Set (Var "g")) ")" )))  ")" )) ; 
 
theorem :: RFUNCT_1:39 (Bool  "for" (Set (Var "f1")) "," (Set (Var "f")) "," (Set (Var "f2")) "being"   ($#v1_valued_0 :::"complex-valued"::: )    ($#m1_hidden :::"Function":::) "holds"   (Bool  "("  (Bool (Set (Set  "(" (Set (Var "f1"))  ($#k1_rfunct_1 :::"/"::: )  (Set (Var "f")) ")" )  ($#k1_valued_1 :::"+"::: )  (Set  "(" (Set (Var "f2"))  ($#k1_rfunct_1 :::"/"::: )  (Set (Var "f")) ")" ))  ($#r1_hidden :::"="::: )  (Set (Set  "(" (Set (Var "f1"))  ($#k1_valued_1 :::"+"::: )  (Set (Var "f2")) ")" )  ($#k1_rfunct_1 :::"/"::: )  (Set (Var "f")))) & (Bool (Set (Set  "(" (Set (Var "f1"))  ($#k1_rfunct_1 :::"/"::: )  (Set (Var "f")) ")" )  ($#k45_valued_1 :::"-"::: )  (Set  "(" (Set (Var "f2"))  ($#k1_rfunct_1 :::"/"::: )  (Set (Var "f")) ")" ))  ($#r1_hidden :::"="::: )  (Set (Set  "(" (Set (Var "f1"))  ($#k45_valued_1 :::"-"::: )  (Set (Var "f2")) ")" )  ($#k1_rfunct_1 :::"/"::: )  (Set (Var "f"))))  ")" )) ; 
 
theorem :: RFUNCT_1:40 (Bool  "for" (Set (Var "f1")) "," (Set (Var "f")) "," (Set (Var "g1")) "," (Set (Var "g")) "being"   ($#v1_valued_0 :::"complex-valued"::: )    ($#m1_hidden :::"Function":::) "holds"  (Bool (Set (Set  "(" (Set (Var "f1"))  ($#k1_rfunct_1 :::"/"::: )  (Set (Var "f")) ")" )  ($#k1_valued_1 :::"+"::: )  (Set  "(" (Set (Var "g1"))  ($#k1_rfunct_1 :::"/"::: )  (Set (Var "g")) ")" ))  ($#r1_hidden :::"="::: )  (Set (Set  "(" (Set  "(" (Set (Var "f1"))  ($#k18_valued_1 :::"(#)"::: )  (Set (Var "g")) ")" )  ($#k1_valued_1 :::"+"::: )  (Set  "(" (Set (Var "g1"))  ($#k18_valued_1 :::"(#)"::: )  (Set (Var "f")) ")" ) ")" )  ($#k1_rfunct_1 :::"/"::: )  (Set  "(" (Set (Var "f"))  ($#k18_valued_1 :::"(#)"::: )  (Set (Var "g")) ")" )))) ; 
 
theorem :: RFUNCT_1:41 (Bool  "for" (Set (Var "f")) "," (Set (Var "g")) "," (Set (Var "f1")) "," (Set (Var "g1")) "being"   ($#v1_valued_0 :::"complex-valued"::: )    ($#m1_hidden :::"Function":::) "holds"  (Bool (Set (Set  "(" (Set (Var "f"))  ($#k1_rfunct_1 :::"/"::: )  (Set (Var "g")) ")" )  ($#k1_rfunct_1 :::"/"::: )  (Set  "(" (Set (Var "f1"))  ($#k1_rfunct_1 :::"/"::: )  (Set (Var "g1")) ")" ))  ($#r1_hidden :::"="::: )  (Set (Set  "(" (Set (Var "f"))  ($#k18_valued_1 :::"(#)"::: )  (Set  "(" (Set (Var "g1"))  ($#k5_relat_1 :::"|"::: )  (Set  "("  ($#k9_xtuple_0 :::"dom"::: )  (Set  "(" (Set (Var "g1"))  ($#k4_rfunct_1 :::"^"::: )  ")" ) ")" ) ")" ) ")" )  ($#k1_rfunct_1 :::"/"::: )  (Set  "(" (Set (Var "g"))  ($#k18_valued_1 :::"(#)"::: )  (Set (Var "f1")) ")" )))) ; 
 
theorem :: RFUNCT_1:42 (Bool  "for" (Set (Var "f1")) "," (Set (Var "f")) "," (Set (Var "g1")) "," (Set (Var "g")) "being"   ($#v1_valued_0 :::"complex-valued"::: )    ($#m1_hidden :::"Function":::) "holds"  (Bool (Set (Set  "(" (Set (Var "f1"))  ($#k1_rfunct_1 :::"/"::: )  (Set (Var "f")) ")" )  ($#k45_valued_1 :::"-"::: )  (Set  "(" (Set (Var "g1"))  ($#k1_rfunct_1 :::"/"::: )  (Set (Var "g")) ")" ))  ($#r1_hidden :::"="::: )  (Set (Set  "(" (Set  "(" (Set (Var "f1"))  ($#k18_valued_1 :::"(#)"::: )  (Set (Var "g")) ")" )  ($#k45_valued_1 :::"-"::: )  (Set  "(" (Set (Var "g1"))  ($#k18_valued_1 :::"(#)"::: )  (Set (Var "f")) ")" ) ")" )  ($#k1_rfunct_1 :::"/"::: )  (Set  "(" (Set (Var "f"))  ($#k18_valued_1 :::"(#)"::: )  (Set (Var "g")) ")" )))) ; 
 
theorem :: RFUNCT_1:43 (Bool  "for" (Set (Var "f1")) "," (Set (Var "f2")) "being"   ($#v1_valued_0 :::"complex-valued"::: )    ($#m1_hidden :::"Function":::) "holds"  (Bool (Set   ($#k54_valued_1 :::"abs"::: )  (Set  "(" (Set (Var "f1"))  ($#k1_rfunct_1 :::"/"::: )  (Set (Var "f2")) ")" ))  ($#r1_hidden :::"="::: )  (Set (Set  "("  ($#k54_valued_1 :::"abs"::: )  (Set (Var "f1")) ")" )  ($#k1_rfunct_1 :::"/"::: )  (Set  "("  ($#k54_valued_1 :::"abs"::: )  (Set (Var "f2")) ")" )))) ; 
 
theorem :: RFUNCT_1:44 (Bool  "for" (Set (Var "X")) "being"    ($#m1_hidden :::"set"::: )    (Bool  "for" (Set (Var "f1")) "," (Set (Var "f2")) "being"   ($#v1_valued_0 :::"complex-valued"::: )    ($#m1_hidden :::"Function":::) "holds"   (Bool  "("  (Bool (Set (Set  "(" (Set (Var "f1"))  ($#k1_valued_1 :::"+"::: )  (Set (Var "f2")) ")" )  ($#k5_relat_1 :::"|"::: )  (Set (Var "X")))  ($#r1_hidden :::"="::: )  (Set (Set  "(" (Set (Var "f1"))  ($#k5_relat_1 :::"|"::: )  (Set (Var "X")) ")" )  ($#k1_valued_1 :::"+"::: )  (Set  "(" (Set (Var "f2"))  ($#k5_relat_1 :::"|"::: )  (Set (Var "X")) ")" ))) & (Bool (Set (Set  "(" (Set (Var "f1"))  ($#k1_valued_1 :::"+"::: )  (Set (Var "f2")) ")" )  ($#k5_relat_1 :::"|"::: )  (Set (Var "X")))  ($#r1_hidden :::"="::: )  (Set (Set  "(" (Set (Var "f1"))  ($#k5_relat_1 :::"|"::: )  (Set (Var "X")) ")" )  ($#k1_valued_1 :::"+"::: )  (Set (Var "f2")))) & (Bool (Set (Set  "(" (Set (Var "f1"))  ($#k1_valued_1 :::"+"::: )  (Set (Var "f2")) ")" )  ($#k5_relat_1 :::"|"::: )  (Set (Var "X")))  ($#r1_hidden :::"="::: )  (Set (Set (Var "f1"))  ($#k1_valued_1 :::"+"::: )  (Set  "(" (Set (Var "f2"))  ($#k5_relat_1 :::"|"::: )  (Set (Var "X")) ")" )))  ")" ))) ; 
 
theorem :: RFUNCT_1:45 (Bool  "for" (Set (Var "X")) "being"    ($#m1_hidden :::"set"::: )    (Bool  "for" (Set (Var "f1")) "," (Set (Var "f2")) "being"   ($#v1_valued_0 :::"complex-valued"::: )    ($#m1_hidden :::"Function":::) "holds"   (Bool  "("  (Bool (Set (Set  "(" (Set (Var "f1"))  ($#k18_valued_1 :::"(#)"::: )  (Set (Var "f2")) ")" )  ($#k5_relat_1 :::"|"::: )  (Set (Var "X")))  ($#r1_hidden :::"="::: )  (Set (Set  "(" (Set (Var "f1"))  ($#k5_relat_1 :::"|"::: )  (Set (Var "X")) ")" )  ($#k18_valued_1 :::"(#)"::: )  (Set  "(" (Set (Var "f2"))  ($#k5_relat_1 :::"|"::: )  (Set (Var "X")) ")" ))) & (Bool (Set (Set  "(" (Set (Var "f1"))  ($#k18_valued_1 :::"(#)"::: )  (Set (Var "f2")) ")" )  ($#k5_relat_1 :::"|"::: )  (Set (Var "X")))  ($#r1_hidden :::"="::: )  (Set (Set  "(" (Set (Var "f1"))  ($#k5_relat_1 :::"|"::: )  (Set (Var "X")) ")" )  ($#k18_valued_1 :::"(#)"::: )  (Set (Var "f2")))) & (Bool (Set (Set  "(" (Set (Var "f1"))  ($#k18_valued_1 :::"(#)"::: )  (Set (Var "f2")) ")" )  ($#k5_relat_1 :::"|"::: )  (Set (Var "X")))  ($#r1_hidden :::"="::: )  (Set (Set (Var "f1"))  ($#k18_valued_1 :::"(#)"::: )  (Set  "(" (Set (Var "f2"))  ($#k5_relat_1 :::"|"::: )  (Set (Var "X")) ")" )))  ")" ))) ; 
 
theorem :: RFUNCT_1:46 (Bool  "for" (Set (Var "X")) "being"    ($#m1_hidden :::"set"::: )    (Bool  "for" (Set (Var "f")) "being"   ($#v1_valued_0 :::"complex-valued"::: )    ($#m1_hidden :::"Function":::) "holds"   (Bool  "("  (Bool (Set (Set  "("  ($#k30_valued_1 :::"-"::: )  (Set (Var "f")) ")" )  ($#k5_relat_1 :::"|"::: )  (Set (Var "X")))  ($#r1_hidden :::"="::: )  (Set   ($#k30_valued_1 :::"-"::: )  (Set  "(" (Set (Var "f"))  ($#k5_relat_1 :::"|"::: )  (Set (Var "X")) ")" ))) & (Bool (Set (Set  "(" (Set (Var "f"))  ($#k4_rfunct_1 :::"^"::: )  ")" )  ($#k5_relat_1 :::"|"::: )  (Set (Var "X")))  ($#r1_hidden :::"="::: )  (Set (Set  "(" (Set (Var "f"))  ($#k5_relat_1 :::"|"::: )  (Set (Var "X")) ")" )  ($#k4_rfunct_1 :::"^"::: )  )) & (Bool (Set (Set  "("  ($#k54_valued_1 :::"abs"::: )  (Set (Var "f")) ")" )  ($#k5_relat_1 :::"|"::: )  (Set (Var "X")))  ($#r1_hidden :::"="::: )  (Set   ($#k54_valued_1 :::"abs"::: )  (Set  "(" (Set (Var "f"))  ($#k5_relat_1 :::"|"::: )  (Set (Var "X")) ")" )))  ")" ))) ; 
 
theorem :: RFUNCT_1:47 (Bool  "for" (Set (Var "X")) "being"    ($#m1_hidden :::"set"::: )    (Bool  "for" (Set (Var "f1")) "," (Set (Var "f2")) "being"   ($#v1_valued_0 :::"complex-valued"::: )    ($#m1_hidden :::"Function":::) "holds"   (Bool  "("  (Bool (Set (Set  "(" (Set (Var "f1"))  ($#k45_valued_1 :::"-"::: )  (Set (Var "f2")) ")" )  ($#k5_relat_1 :::"|"::: )  (Set (Var "X")))  ($#r1_hidden :::"="::: )  (Set (Set  "(" (Set (Var "f1"))  ($#k5_relat_1 :::"|"::: )  (Set (Var "X")) ")" )  ($#k45_valued_1 :::"-"::: )  (Set  "(" (Set (Var "f2"))  ($#k5_relat_1 :::"|"::: )  (Set (Var "X")) ")" ))) & (Bool (Set (Set  "(" (Set (Var "f1"))  ($#k45_valued_1 :::"-"::: )  (Set (Var "f2")) ")" )  ($#k5_relat_1 :::"|"::: )  (Set (Var "X")))  ($#r1_hidden :::"="::: )  (Set (Set  "(" (Set (Var "f1"))  ($#k5_relat_1 :::"|"::: )  (Set (Var "X")) ")" )  ($#k45_valued_1 :::"-"::: )  (Set (Var "f2")))) & (Bool (Set (Set  "(" (Set (Var "f1"))  ($#k45_valued_1 :::"-"::: )  (Set (Var "f2")) ")" )  ($#k5_relat_1 :::"|"::: )  (Set (Var "X")))  ($#r1_hidden :::"="::: )  (Set (Set (Var "f1"))  ($#k45_valued_1 :::"-"::: )  (Set  "(" (Set (Var "f2"))  ($#k5_relat_1 :::"|"::: )  (Set (Var "X")) ")" )))  ")" ))) ; 
 
theorem :: RFUNCT_1:48 (Bool  "for" (Set (Var "X")) "being"    ($#m1_hidden :::"set"::: )    (Bool  "for" (Set (Var "f1")) "," (Set (Var "f2")) "being"   ($#v1_valued_0 :::"complex-valued"::: )    ($#m1_hidden :::"Function":::) "holds"   (Bool  "("  (Bool (Set (Set  "(" (Set (Var "f1"))  ($#k1_rfunct_1 :::"/"::: )  (Set (Var "f2")) ")" )  ($#k5_relat_1 :::"|"::: )  (Set (Var "X")))  ($#r1_hidden :::"="::: )  (Set (Set  "(" (Set (Var "f1"))  ($#k5_relat_1 :::"|"::: )  (Set (Var "X")) ")" )  ($#k1_rfunct_1 :::"/"::: )  (Set  "(" (Set (Var "f2"))  ($#k5_relat_1 :::"|"::: )  (Set (Var "X")) ")" ))) & (Bool (Set (Set  "(" (Set (Var "f1"))  ($#k1_rfunct_1 :::"/"::: )  (Set (Var "f2")) ")" )  ($#k5_relat_1 :::"|"::: )  (Set (Var "X")))  ($#r1_hidden :::"="::: )  (Set (Set  "(" (Set (Var "f1"))  ($#k5_relat_1 :::"|"::: )  (Set (Var "X")) ")" )  ($#k1_rfunct_1 :::"/"::: )  (Set (Var "f2")))) & (Bool (Set (Set  "(" (Set (Var "f1"))  ($#k1_rfunct_1 :::"/"::: )  (Set (Var "f2")) ")" )  ($#k5_relat_1 :::"|"::: )  (Set (Var "X")))  ($#r1_hidden :::"="::: )  (Set (Set (Var "f1"))  ($#k1_rfunct_1 :::"/"::: )  (Set  "(" (Set (Var "f2"))  ($#k5_relat_1 :::"|"::: )  (Set (Var "X")) ")" )))  ")" ))) ; 
 
theorem :: RFUNCT_1:49 (Bool  "for" (Set (Var "X")) "being"    ($#m1_hidden :::"set"::: )    (Bool  "for" (Set (Var "f")) "being"   ($#v1_valued_0 :::"complex-valued"::: )    ($#m1_hidden :::"Function":::)  (Bool  "for" (Set (Var "r")) "being"   ($#v1_xcmplx_0 :::"complex"::: )     ($#m1_hidden :::"number"::: )   "holds"  (Bool (Set (Set  "(" (Set (Var "r"))  ($#k24_valued_1 :::"(#)"::: )  (Set (Var "f")) ")" )  ($#k5_relat_1 :::"|"::: )  (Set (Var "X")))  ($#r1_hidden :::"="::: )  (Set (Set (Var "r"))  ($#k24_valued_1 :::"(#)"::: )  (Set  "(" (Set (Var "f"))  ($#k5_relat_1 :::"|"::: )  (Set (Var "X")) ")" )))))) ; 
 











theorem :: RFUNCT_1:50 (Bool  "for" (Set (Var "C")) "being"  ($#~v1_xboole_0  "non"   ($#v1_xboole_0 :::"empty"::: )   )    ($#m1_hidden :::"set"::: )    (Bool  "for" (Set (Var "f1")) "," (Set (Var "f2")) "being"   ($#m1_subset_1 :::"PartFunc":::) "of" (Set (Var "C")) "," (Set  ($#k1_numbers :::"REAL"::: ) ) "holds"   (Bool  "("   "("  (Bool (Bool (Set (Var "f1")) "is"   ($#v1_partfun1 :::"total"::: )  ) & (Bool (Set (Var "f2")) "is"   ($#v1_partfun1 :::"total"::: )  )) "implies" (Bool (Set (Set (Var "f1"))  ($#k3_valued_1 :::"+"::: )  (Set (Var "f2"))) "is"   ($#v1_partfun1 :::"total"::: )  )  ")"  &  "("  (Bool (Bool (Set (Set (Var "f1"))  ($#k3_valued_1 :::"+"::: )  (Set (Var "f2"))) "is"   ($#v1_partfun1 :::"total"::: )  )) "implies" (Bool  "("  (Bool (Set (Var "f1")) "is"   ($#v1_partfun1 :::"total"::: )  ) & (Bool (Set (Var "f2")) "is"   ($#v1_partfun1 :::"total"::: )  )  ")" )  ")"  &  "("  (Bool (Bool (Set (Var "f1")) "is"   ($#v1_partfun1 :::"total"::: )  ) & (Bool (Set (Var "f2")) "is"   ($#v1_partfun1 :::"total"::: )  )) "implies" (Bool (Set (Set (Var "f1"))  ($#k47_valued_1 :::"-"::: )  (Set (Var "f2"))) "is"   ($#v1_partfun1 :::"total"::: )  )  ")"  &  "("  (Bool (Bool (Set (Set (Var "f1"))  ($#k47_valued_1 :::"-"::: )  (Set (Var "f2"))) "is"   ($#v1_partfun1 :::"total"::: )  )) "implies" (Bool  "("  (Bool (Set (Var "f1")) "is"   ($#v1_partfun1 :::"total"::: )  ) & (Bool (Set (Var "f2")) "is"   ($#v1_partfun1 :::"total"::: )  )  ")" )  ")"  &  "("  (Bool (Bool (Set (Var "f1")) "is"   ($#v1_partfun1 :::"total"::: )  ) & (Bool (Set (Var "f2")) "is"   ($#v1_partfun1 :::"total"::: )  )) "implies" (Bool (Set (Set (Var "f1"))  ($#k20_valued_1 :::"(#)"::: )  (Set (Var "f2"))) "is"   ($#v1_partfun1 :::"total"::: )  )  ")"  &  "("  (Bool (Bool (Set (Set (Var "f1"))  ($#k20_valued_1 :::"(#)"::: )  (Set (Var "f2"))) "is"   ($#v1_partfun1 :::"total"::: )  )) "implies" (Bool  "("  (Bool (Set (Var "f1")) "is"   ($#v1_partfun1 :::"total"::: )  ) & (Bool (Set (Var "f2")) "is"   ($#v1_partfun1 :::"total"::: )  )  ")" )  ")"   ")" ))) ; 
 
theorem :: RFUNCT_1:51 (Bool  "for" (Set (Var "C")) "being"  ($#~v1_xboole_0  "non"   ($#v1_xboole_0 :::"empty"::: )   )    ($#m1_hidden :::"set"::: )    (Bool  "for" (Set (Var "r")) "being"   ($#v1_xreal_0 :::"real"::: )     ($#m1_hidden :::"number"::: )    (Bool  "for" (Set (Var "f")) "being"   ($#m1_subset_1 :::"PartFunc":::) "of" (Set (Var "C")) "," (Set  ($#k1_numbers :::"REAL"::: ) ) "holds"   (Bool  "("  (Bool (Set (Var "f")) "is"   ($#v1_partfun1 :::"total"::: )  ) "iff" (Bool (Set (Set (Var "r"))  ($#k26_valued_1 :::"(#)"::: )  (Set (Var "f"))) "is"   ($#v1_partfun1 :::"total"::: )  )  ")" )))) ; 
 
theorem :: RFUNCT_1:52 (Bool  "for" (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  ($#k1_numbers :::"REAL"::: ) ) "holds"   (Bool  "("  (Bool (Set (Var "f")) "is"   ($#v1_partfun1 :::"total"::: )  ) "iff" (Bool (Set   ($#k32_valued_1 :::"-"::: )  (Set (Var "f"))) "is"   ($#v1_partfun1 :::"total"::: )  )  ")" ))) ; 
 
theorem :: RFUNCT_1:53 (Bool  "for" (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  ($#k1_numbers :::"REAL"::: ) ) "holds"   (Bool  "("  (Bool (Set (Var "f")) "is"   ($#v1_partfun1 :::"total"::: )  ) "iff" (Bool (Set   ($#k56_valued_1 :::"abs"::: )  (Set (Var "f"))) "is"   ($#v1_partfun1 :::"total"::: )  )  ")" ))) ; 
 
theorem :: RFUNCT_1:54 (Bool  "for" (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  ($#k1_numbers :::"REAL"::: ) ) "holds"   (Bool  "("  (Bool (Set (Set (Var "f"))  ($#k6_rfunct_1 :::"^"::: )  ) "is"   ($#v1_partfun1 :::"total"::: )  ) "iff" (Bool  "("  (Bool (Set (Set (Var "f"))  ($#k8_relset_1 :::"""::: )  (Set  ($#k1_tarski :::"{"::: ) (Set  ($#k6_numbers :::"0"::: ) ) ($#k1_tarski :::"}"::: ) ))  ($#r1_hidden :::"="::: )  (Set   ($#k1_xboole_0 :::"{}"::: )  )) & (Bool (Set (Var "f")) "is"   ($#v1_partfun1 :::"total"::: )  )  ")" )  ")" ))) ; 
 
theorem :: RFUNCT_1:55 (Bool  "for" (Set (Var "C")) "being"  ($#~v1_xboole_0  "non"   ($#v1_xboole_0 :::"empty"::: )   )    ($#m1_hidden :::"set"::: )    (Bool  "for" (Set (Var "f1")) "," (Set (Var "f2")) "being"   ($#m1_subset_1 :::"PartFunc":::) "of" (Set (Var "C")) "," (Set  ($#k1_numbers :::"REAL"::: ) ) "holds"   (Bool  "("  (Bool  "("  (Bool (Set (Var "f1")) "is"   ($#v1_partfun1 :::"total"::: )  ) & (Bool (Set (Set (Var "f2"))  ($#k8_relset_1 :::"""::: )  (Set  ($#k1_tarski :::"{"::: ) (Set  ($#k6_numbers :::"0"::: ) ) ($#k1_tarski :::"}"::: ) ))  ($#r1_hidden :::"="::: )  (Set   ($#k1_xboole_0 :::"{}"::: )  )) & (Bool (Set (Var "f2")) "is"   ($#v1_partfun1 :::"total"::: )  )  ")" ) "iff" (Bool (Set (Set (Var "f1"))  ($#k3_rfunct_1 :::"/"::: )  (Set (Var "f2"))) "is"   ($#v1_partfun1 :::"total"::: )  )  ")" ))) ; 
 
theorem :: RFUNCT_1:56 (Bool  "for" (Set (Var "C")) "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 "f2")) "being"   ($#m1_subset_1 :::"PartFunc":::) "of" (Set (Var "C")) "," (Set  ($#k1_numbers :::"REAL"::: ) )  "st" (Bool (Bool (Set (Var "f1")) "is"   ($#v1_partfun1 :::"total"::: )  ) & (Bool (Set (Var "f2")) "is"   ($#v1_partfun1 :::"total"::: )  )) "holds"  (Bool  "("  (Bool (Set (Set  "(" (Set (Var "f1"))  ($#k3_valued_1 :::"+"::: )  (Set (Var "f2")) ")" )  ($#k1_funct_1 :::"."::: )  (Set (Var "c")))  ($#r1_hidden :::"="::: )  (Set (Set  "(" (Set (Var "f1"))  ($#k1_funct_1 :::"."::: )  (Set (Var "c")) ")" )  ($#k2_xcmplx_0 :::"+"::: )  (Set  "(" (Set (Var "f2"))  ($#k1_funct_1 :::"."::: )  (Set (Var "c")) ")" ))) & (Bool (Set (Set  "(" (Set (Var "f1"))  ($#k47_valued_1 :::"-"::: )  (Set (Var "f2")) ")" )  ($#k1_funct_1 :::"."::: )  (Set (Var "c")))  ($#r1_hidden :::"="::: )  (Set (Set  "(" (Set (Var "f1"))  ($#k1_funct_1 :::"."::: )  (Set (Var "c")) ")" )  ($#k6_xcmplx_0 :::"-"::: )  (Set  "(" (Set (Var "f2"))  ($#k1_funct_1 :::"."::: )  (Set (Var "c")) ")" ))) & (Bool (Set (Set  "(" (Set (Var "f1"))  ($#k20_valued_1 :::"(#)"::: )  (Set (Var "f2")) ")" )  ($#k1_funct_1 :::"."::: )  (Set (Var "c")))  ($#r1_hidden :::"="::: )  (Set (Set  "(" (Set (Var "f1"))  ($#k1_funct_1 :::"."::: )  (Set (Var "c")) ")" )  ($#k3_xcmplx_0 :::"*"::: )  (Set  "(" (Set (Var "f2"))  ($#k1_funct_1 :::"."::: )  (Set (Var "c")) ")" )))  ")" )))) ; 
 
theorem :: RFUNCT_1:57 (Bool  "for" (Set (Var "C")) "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 "r")) "being"   ($#v1_xreal_0 :::"real"::: )     ($#m1_hidden :::"number"::: )    (Bool  "for" (Set (Var "f")) "being"   ($#m1_subset_1 :::"PartFunc":::) "of" (Set (Var "C")) "," (Set  ($#k1_numbers :::"REAL"::: ) )  "st" (Bool (Bool (Set (Var "f")) "is"   ($#v1_partfun1 :::"total"::: )  )) "holds"  (Bool (Set (Set  "(" (Set (Var "r"))  ($#k26_valued_1 :::"(#)"::: )  (Set (Var "f")) ")" )  ($#k1_funct_1 :::"."::: )  (Set (Var "c")))  ($#r1_hidden :::"="::: )  (Set (Set (Var "r"))  ($#k3_xcmplx_0 :::"*"::: )  (Set  "(" (Set (Var "f"))  ($#k1_funct_1 :::"."::: )  (Set (Var "c")) ")" ))))))) ; 
 
theorem :: RFUNCT_1:58 (Bool  "for" (Set (Var "C")) "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  ($#k1_numbers :::"REAL"::: ) )  "st" (Bool (Bool (Set (Var "f")) "is"   ($#v1_partfun1 :::"total"::: )  )) "holds"  (Bool  "("  (Bool (Set (Set  "("  ($#k32_valued_1 :::"-"::: )  (Set (Var "f")) ")" )  ($#k1_funct_1 :::"."::: )  (Set (Var "c")))  ($#r1_hidden :::"="::: )  (Set   ($#k4_xcmplx_0 :::"-"::: )  (Set  "(" (Set (Var "f"))  ($#k1_funct_1 :::"."::: )  (Set (Var "c")) ")" ))) & (Bool (Set (Set  "("  ($#k56_valued_1 :::"abs"::: )  (Set (Var "f")) ")" )  ($#k1_funct_1 :::"."::: )  (Set (Var "c")))  ($#r1_hidden :::"="::: )  (Set   ($#k18_complex1 :::"abs"::: )  (Set  "(" (Set (Var "f"))  ($#k1_funct_1 :::"."::: )  (Set (Var "c")) ")" )))  ")" )))) ; 
 
theorem :: RFUNCT_1:59 (Bool  "for" (Set (Var "C")) "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  ($#k1_numbers :::"REAL"::: ) )  "st" (Bool (Bool (Set (Set (Var "f"))  ($#k6_rfunct_1 :::"^"::: )  ) "is"   ($#v1_partfun1 :::"total"::: )  )) "holds"  (Bool (Set (Set  "(" (Set (Var "f"))  ($#k6_rfunct_1 :::"^"::: )  ")" )  ($#k1_funct_1 :::"."::: )  (Set (Var "c")))  ($#r1_hidden :::"="::: )  (Set (Set  "(" (Set (Var "f"))  ($#k1_funct_1 :::"."::: )  (Set (Var "c")) ")" )  ($#k5_xcmplx_0 :::"""::: )  ))))) ; 
 
theorem :: RFUNCT_1:60 (Bool  "for" (Set (Var "C")) "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 "f2")) "being"   ($#m1_subset_1 :::"PartFunc":::) "of" (Set (Var "C")) "," (Set  ($#k1_numbers :::"REAL"::: ) )  "st" (Bool (Bool (Set (Var "f1")) "is"   ($#v1_partfun1 :::"total"::: )  ) & (Bool (Set (Set (Var "f2"))  ($#k6_rfunct_1 :::"^"::: )  ) "is"   ($#v1_partfun1 :::"total"::: )  )) "holds"  (Bool (Set (Set  "(" (Set (Var "f1"))  ($#k3_rfunct_1 :::"/"::: )  (Set (Var "f2")) ")" )  ($#k1_funct_1 :::"."::: )  (Set (Var "c")))  ($#r1_hidden :::"="::: )  (Set (Set  "(" (Set (Var "f1"))  ($#k1_funct_1 :::"."::: )  (Set (Var "c")) ")" )  ($#k3_xcmplx_0 :::"*"::: )  (Set  "(" (Set  "(" (Set (Var "f2"))  ($#k1_funct_1 :::"."::: )  (Set (Var "c")) ")" )  ($#k5_xcmplx_0 :::"""::: )  ")" )))))) ; 
 definitionlet "X", "C" be    ($#m1_hidden :::"set"::: )  ; :: original: :::"chi"::: redefine func  :::"chi":::  "(" "X" "," "C" ")"  ->   ($#m1_subset_1 :::"PartFunc":::) "of" "C" "," (Set  ($#k1_numbers :::"REAL"::: ) ); end; registrationlet "X", "C" be    ($#m1_hidden :::"set"::: )  ; 
cluster (Set   ($#k4_funct_3 :::"chi"::: )   "(" "X" "," "C" ")" ) ->   ($#v1_partfun1 :::"total"::: )    for  ($#m1_subset_1 :::"PartFunc":::) "of" "C" "," (Set  ($#k1_numbers :::"REAL"::: ) ); 
end; 
theorem :: RFUNCT_1:61 (Bool  "for" (Set (Var "X")) "being"    ($#m1_hidden :::"set"::: )    (Bool  "for" (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  ($#k1_numbers :::"REAL"::: ) ) "holds"   (Bool  "("  (Bool (Set (Var "f"))  ($#r2_relset_1 :::"="::: )  (Set   ($#k7_rfunct_1 :::"chi"::: )   "(" (Set (Var "X")) "," (Set (Var "C")) ")" )) "iff" (Bool  "("  (Bool (Set   ($#k1_relset_1 :::"dom"::: )  (Set (Var "f")))  ($#r1_hidden :::"="::: )  (Set (Var "C"))) & (Bool  "("   "for" (Set (Var "c")) "being"    ($#m1_subset_1 :::"Element"::: )   "of" (Set (Var "C")) "holds"   (Bool  "("   "("  (Bool (Bool (Set (Var "c"))  ($#r2_hidden :::"in"::: )  (Set (Var "X")))) "implies" (Bool (Set (Set (Var "f"))  ($#k1_funct_1 :::"."::: )  (Set (Var "c")))  ($#r1_hidden :::"="::: )  (Num 1))  ")"  &  "("  (Bool (Bool (Bool  "not" (Set (Var "c"))  ($#r2_hidden :::"in"::: )  (Set (Var "X"))))) "implies" (Bool (Set (Set (Var "f"))  ($#k1_funct_1 :::"."::: )  (Set (Var "c")))  ($#r1_hidden :::"="::: )  (Set   ($#k6_numbers :::"0"::: )  ))  ")"   ")" )  ")" )  ")" )  ")" )))) ; 
 
theorem :: RFUNCT_1:62 (Bool  "for" (Set (Var "X")) "being"    ($#m1_hidden :::"set"::: )    (Bool  "for" (Set (Var "C")) "being"  ($#~v1_xboole_0  "non"   ($#v1_xboole_0 :::"empty"::: )   )    ($#m1_hidden :::"set"::: )   "holds"  (Bool (Set   ($#k7_rfunct_1 :::"chi"::: )   "(" (Set (Var "X")) "," (Set (Var "C")) ")" ) "is"   ($#v1_partfun1 :::"total"::: )  ))) ; 
 
theorem :: RFUNCT_1:63 (Bool  "for" (Set (Var "X")) "being"    ($#m1_hidden :::"set"::: )    (Bool  "for" (Set (Var "C")) "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")) "holds"   (Bool  "("  (Bool (Set (Var "c"))  ($#r2_hidden :::"in"::: )  (Set (Var "X"))) "iff" (Bool (Set (Set  "("  ($#k7_rfunct_1 :::"chi"::: )   "(" (Set (Var "X")) "," (Set (Var "C")) ")"  ")" )  ($#k1_funct_1 :::"."::: )  (Set (Var "c")))  ($#r1_hidden :::"="::: )  (Num 1))  ")" )))) ; 
 
theorem :: RFUNCT_1:64 (Bool  "for" (Set (Var "X")) "being"    ($#m1_hidden :::"set"::: )    (Bool  "for" (Set (Var "C")) "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")) "holds"   (Bool  "("  (Bool (Bool  "not" (Set (Var "c"))  ($#r2_hidden :::"in"::: )  (Set (Var "X")))) "iff" (Bool (Set (Set  "("  ($#k7_rfunct_1 :::"chi"::: )   "(" (Set (Var "X")) "," (Set (Var "C")) ")"  ")" )  ($#k1_funct_1 :::"."::: )  (Set (Var "c")))  ($#r1_hidden :::"="::: )  (Set   ($#k6_numbers :::"0"::: )  ))  ")" )))) ; 
 
theorem :: RFUNCT_1:65 (Bool  "for" (Set (Var "X")) "being"    ($#m1_hidden :::"set"::: )    (Bool  "for" (Set (Var "C")) "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")) "holds"   (Bool  "("  (Bool (Set (Var "c"))  ($#r2_hidden :::"in"::: )  (Set (Set (Var "C"))  ($#k6_subset_1 :::"\"::: )  (Set (Var "X")))) "iff" (Bool (Set (Set  "("  ($#k7_rfunct_1 :::"chi"::: )   "(" (Set (Var "X")) "," (Set (Var "C")) ")"  ")" )  ($#k1_funct_1 :::"."::: )  (Set (Var "c")))  ($#r1_hidden :::"="::: )  (Set   ($#k6_numbers :::"0"::: )  ))  ")" )))) ; 
 
theorem :: RFUNCT_1:66 (Bool  "for" (Set (Var "C")) "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")) "holds"  (Bool (Set (Set  "("  ($#k7_rfunct_1 :::"chi"::: )   "(" (Set (Var "C")) "," (Set (Var "C")) ")"  ")" )  ($#k1_funct_1 :::"."::: )  (Set (Var "c")))  ($#r1_hidden :::"="::: )  (Num 1)))) ; 
 
theorem :: RFUNCT_1:67 (Bool  "for" (Set (Var "X")) "being"    ($#m1_hidden :::"set"::: )    (Bool  "for" (Set (Var "C")) "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")) "holds"   (Bool  "("  (Bool (Set (Set  "("  ($#k7_rfunct_1 :::"chi"::: )   "(" (Set (Var "X")) "," (Set (Var "C")) ")"  ")" )  ($#k1_funct_1 :::"."::: )  (Set (Var "c")))  ($#r1_hidden :::"<>"::: )  (Num 1)) "iff" (Bool (Set (Set  "("  ($#k7_rfunct_1 :::"chi"::: )   "(" (Set (Var "X")) "," (Set (Var "C")) ")"  ")" )  ($#k1_funct_1 :::"."::: )  (Set (Var "c")))  ($#r1_hidden :::"="::: )  (Set   ($#k6_numbers :::"0"::: )  ))  ")" )))) ; 
 
theorem :: RFUNCT_1:68 (Bool  "for" (Set (Var "X")) "," (Set (Var "Y")) "being"    ($#m1_hidden :::"set"::: )    (Bool  "for" (Set (Var "C")) "being"  ($#~v1_xboole_0  "non"   ($#v1_xboole_0 :::"empty"::: )   )    ($#m1_hidden :::"set"::: )    "st" (Bool (Bool (Set (Var "X"))  ($#r1_xboole_0 :::"misses"::: )  (Set (Var "Y")))) "holds"  (Bool (Set (Set  "("  ($#k7_rfunct_1 :::"chi"::: )   "(" (Set (Var "X")) "," (Set (Var "C")) ")"  ")" )  ($#k3_valued_1 :::"+"::: )  (Set  "("  ($#k7_rfunct_1 :::"chi"::: )   "(" (Set (Var "Y")) "," (Set (Var "C")) ")"  ")" ))  ($#r2_relset_1 :::"="::: )  (Set   ($#k7_rfunct_1 :::"chi"::: )   "(" (Set  "(" (Set (Var "X"))  ($#k2_xboole_0 :::"\/"::: )  (Set (Var "Y")) ")" ) "," (Set (Var "C")) ")" )))) ; 
 
theorem :: RFUNCT_1:69 (Bool  "for" (Set (Var "X")) "," (Set (Var "Y")) "being"    ($#m1_hidden :::"set"::: )    (Bool  "for" (Set (Var "C")) "being"  ($#~v1_xboole_0  "non"   ($#v1_xboole_0 :::"empty"::: )   )    ($#m1_hidden :::"set"::: )   "holds"  (Bool (Set (Set  "("  ($#k7_rfunct_1 :::"chi"::: )   "(" (Set (Var "X")) "," (Set (Var "C")) ")"  ")" )  ($#k20_valued_1 :::"(#)"::: )  (Set  "("  ($#k7_rfunct_1 :::"chi"::: )   "(" (Set (Var "Y")) "," (Set (Var "C")) ")"  ")" ))  ($#r2_relset_1 :::"="::: )  (Set   ($#k7_rfunct_1 :::"chi"::: )   "(" (Set  "(" (Set (Var "X"))  ($#k3_xboole_0 :::"/\"::: )  (Set (Var "Y")) ")" ) "," (Set (Var "C")) ")" )))) ; 
 



theorem :: RFUNCT_1:70 (Bool  "for" (Set (Var "Y")) "being"    ($#m1_hidden :::"set"::: )    (Bool  "for" (Set (Var "f")) "being"   ($#v3_valued_0 :::"real-valued"::: )    ($#m1_hidden :::"Function":::) "holds"   (Bool  "("  (Bool (Set (Set (Var "f"))  ($#k5_relat_1 :::"|"::: )  (Set (Var "Y"))) "is"   ($#v1_seq_2 :::"bounded_above"::: )  ) "iff" (Bool  "ex" (Set (Var "r")) "being"   ($#v1_xreal_0 :::"real"::: )     ($#m1_hidden :::"number"::: )   "st"  (Bool  "for" (Set (Var "c")) "being"    ($#m1_hidden :::"set"::: )    "st" (Bool (Bool (Set (Var "c"))  ($#r2_hidden :::"in"::: )  (Set (Set (Var "Y"))  ($#k3_xboole_0 :::"/\"::: )  (Set  "("  ($#k9_xtuple_0 :::"dom"::: )  (Set (Var "f")) ")" )))) "holds"  (Bool (Set (Set (Var "f"))  ($#k1_funct_1 :::"."::: )  (Set (Var "c")))  ($#r1_xxreal_0 :::"<="::: )  (Set (Var "r")))))  ")" ))) ; 
 
theorem :: RFUNCT_1:71 (Bool  "for" (Set (Var "Y")) "being"    ($#m1_hidden :::"set"::: )    (Bool  "for" (Set (Var "f")) "being"   ($#v3_valued_0 :::"real-valued"::: )    ($#m1_hidden :::"Function":::) "holds"   (Bool  "("  (Bool (Set (Set (Var "f"))  ($#k5_relat_1 :::"|"::: )  (Set (Var "Y"))) "is"   ($#v2_seq_2 :::"bounded_below"::: )  ) "iff" (Bool  "ex" (Set (Var "r")) "being"   ($#v1_xreal_0 :::"real"::: )     ($#m1_hidden :::"number"::: )   "st"  (Bool  "for" (Set (Var "c")) "being"    ($#m1_hidden :::"set"::: )    "st" (Bool (Bool (Set (Var "c"))  ($#r2_hidden :::"in"::: )  (Set (Set (Var "Y"))  ($#k3_xboole_0 :::"/\"::: )  (Set  "("  ($#k9_xtuple_0 :::"dom"::: )  (Set (Var "f")) ")" )))) "holds"  (Bool (Set (Var "r"))  ($#r1_xxreal_0 :::"<="::: )  (Set (Set (Var "f"))  ($#k1_funct_1 :::"."::: )  (Set (Var "c"))))))  ")" ))) ; 
 
theorem :: RFUNCT_1:72 (Bool  "for" (Set (Var "f")) "being"   ($#v3_valued_0 :::"real-valued"::: )    ($#m1_hidden :::"Function":::) "holds"   (Bool  "("  (Bool (Set (Var "f")) "is"   ($#v1_comseq_2 :::"bounded"::: )  ) "iff" (Bool  "ex" (Set (Var "r")) "being"   ($#v1_xreal_0 :::"real"::: )     ($#m1_hidden :::"number"::: )   "st"  (Bool  "for" (Set (Var "c")) "being"    ($#m1_hidden :::"set"::: )    "st" (Bool (Bool (Set (Var "c"))  ($#r2_hidden :::"in"::: )  (Set   ($#k9_xtuple_0 :::"dom"::: )  (Set (Var "f"))))) "holds"  (Bool (Set   ($#k18_complex1 :::"abs"::: )  (Set  "(" (Set (Var "f"))  ($#k1_funct_1 :::"."::: )  (Set (Var "c")) ")" ))  ($#r1_xxreal_0 :::"<="::: )  (Set (Var "r")))))  ")" )) ; 
 
theorem :: RFUNCT_1:73 (Bool  "for" (Set (Var "Y")) "being"    ($#m1_hidden :::"set"::: )    (Bool  "for" (Set (Var "f")) "being"   ($#v3_valued_0 :::"real-valued"::: )    ($#m1_hidden :::"Function":::) "holds"   (Bool  "("  (Bool (Set (Set (Var "f"))  ($#k5_relat_1 :::"|"::: )  (Set (Var "Y"))) "is"   ($#v1_comseq_2 :::"bounded"::: )  ) "iff" (Bool  "ex" (Set (Var "r")) "being"   ($#v1_xreal_0 :::"real"::: )     ($#m1_hidden :::"number"::: )   "st"  (Bool  "for" (Set (Var "c")) "being"    ($#m1_hidden :::"set"::: )    "st" (Bool (Bool (Set (Var "c"))  ($#r2_hidden :::"in"::: )  (Set (Set (Var "Y"))  ($#k3_xboole_0 :::"/\"::: )  (Set  "("  ($#k9_xtuple_0 :::"dom"::: )  (Set (Var "f")) ")" )))) "holds"  (Bool (Set   ($#k18_complex1 :::"abs"::: )  (Set  "(" (Set (Var "f"))  ($#k1_funct_1 :::"."::: )  (Set (Var "c")) ")" ))  ($#r1_xxreal_0 :::"<="::: )  (Set (Var "r")))))  ")" ))) ; 
 
theorem :: RFUNCT_1:74 (Bool  "for" (Set (Var "Y")) "," (Set (Var "X")) "being"    ($#m1_hidden :::"set"::: )    (Bool  "for" (Set (Var "f")) "being"   ($#v3_valued_0 :::"real-valued"::: )    ($#m1_hidden :::"Function":::) "holds"   (Bool  "("   "("  (Bool (Bool (Set (Var "Y"))  ($#r1_tarski :::"c="::: )  (Set (Var "X"))) & (Bool (Set (Set (Var "f"))  ($#k5_relat_1 :::"|"::: )  (Set (Var "X"))) "is"   ($#v1_seq_2 :::"bounded_above"::: )  )) "implies" (Bool (Set (Set (Var "f"))  ($#k5_relat_1 :::"|"::: )  (Set (Var "Y"))) "is"   ($#v1_seq_2 :::"bounded_above"::: )  )  ")"  &  "("  (Bool (Bool (Set (Var "Y"))  ($#r1_tarski :::"c="::: )  (Set (Var "X"))) & (Bool (Set (Set (Var "f"))  ($#k5_relat_1 :::"|"::: )  (Set (Var "X"))) "is"   ($#v2_seq_2 :::"bounded_below"::: )  )) "implies" (Bool (Set (Set (Var "f"))  ($#k5_relat_1 :::"|"::: )  (Set (Var "Y"))) "is"   ($#v2_seq_2 :::"bounded_below"::: )  )  ")"  &  "("  (Bool (Bool (Set (Var "Y"))  ($#r1_tarski :::"c="::: )  (Set (Var "X"))) & (Bool (Set (Set (Var "f"))  ($#k5_relat_1 :::"|"::: )  (Set (Var "X"))) "is"   ($#v1_comseq_2 :::"bounded"::: )  )) "implies" (Bool (Set (Set (Var "f"))  ($#k5_relat_1 :::"|"::: )  (Set (Var "Y"))) "is"   ($#v1_comseq_2 :::"bounded"::: )  )  ")"   ")" ))) ; 
 
theorem :: RFUNCT_1:75 (Bool  "for" (Set (Var "X")) "," (Set (Var "Y")) "being"    ($#m1_hidden :::"set"::: )    (Bool  "for" (Set (Var "f")) "being"   ($#v3_valued_0 :::"real-valued"::: )    ($#m1_hidden :::"Function":::)  "st" (Bool (Bool (Set (Set (Var "f"))  ($#k5_relat_1 :::"|"::: )  (Set (Var "X"))) "is"   ($#v1_seq_2 :::"bounded_above"::: )  ) & (Bool (Set (Set (Var "f"))  ($#k5_relat_1 :::"|"::: )  (Set (Var "Y"))) "is"   ($#v2_seq_2 :::"bounded_below"::: )  )) "holds"  (Bool (Set (Set (Var "f"))  ($#k5_relat_1 :::"|"::: )  (Set  "(" (Set (Var "X"))  ($#k3_xboole_0 :::"/\"::: )  (Set (Var "Y")) ")" )) "is"   ($#v1_comseq_2 :::"bounded"::: )  ))) ; 
 registration
cluster   ($#v1_relat_1 :::"Relation-like"::: )     ($#v1_funct_1 :::"Function-like"::: )     ($#v3_funct_1 :::"constant"::: )     ($#v3_valued_0 :::"real-valued"::: )    ->   ($#v3_valued_0 :::"real-valued"::: )     ($#v1_comseq_2 :::"bounded"::: )    for    ($#m1_hidden :::"set"::: )  ; 
end; 
theorem :: RFUNCT_1:76 (Bool  "for" (Set (Var "X")) "being"    ($#m1_hidden :::"set"::: )    (Bool  "for" (Set (Var "f")) "being"   ($#v3_valued_0 :::"real-valued"::: )    ($#m1_hidden :::"Function":::)  "st" (Bool (Bool (Set (Var "X"))  ($#r1_xboole_0 :::"misses"::: )  (Set   ($#k9_xtuple_0 :::"dom"::: )  (Set (Var "f"))))) "holds"  (Bool (Set (Set (Var "f"))  ($#k5_relat_1 :::"|"::: )  (Set (Var "X"))) "is"   ($#v1_comseq_2 :::"bounded"::: )  ))) ; 
 
theorem :: RFUNCT_1:77 (Bool  "for" (Set (Var "Y")) "being"    ($#m1_hidden :::"set"::: )    (Bool  "for" (Set (Var "f")) "being"   ($#v3_valued_0 :::"real-valued"::: )    ($#m1_hidden :::"Function":::) "holds"  (Bool (Set (Set  "(" (Set  ($#k6_numbers :::"0"::: ) )  ($#k24_valued_1 :::"(#)"::: )  (Set (Var "f")) ")" )  ($#k5_relat_1 :::"|"::: )  (Set (Var "Y"))) "is"   ($#v1_comseq_2 :::"bounded"::: )  ))) ; 
 registrationlet "f" be   ($#v3_valued_0 :::"real-valued"::: )     ($#v1_seq_2 :::"bounded_above"::: )    ($#m1_hidden :::"Function":::); let "X" be    ($#m1_hidden :::"set"::: )  ; 
cluster (Set "f"  ($#k5_relat_1 :::"|"::: )  "X") ->   ($#v3_valued_0 :::"real-valued"::: )     ($#v1_seq_2 :::"bounded_above"::: )    for  ($#v3_valued_0 :::"real-valued"::: )    ($#m1_hidden :::"Function":::); 
end; registrationlet "f" be   ($#v3_valued_0 :::"real-valued"::: )     ($#v2_seq_2 :::"bounded_below"::: )    ($#m1_hidden :::"Function":::); let "X" be    ($#m1_hidden :::"set"::: )  ; 
cluster (Set "f"  ($#k5_relat_1 :::"|"::: )  "X") ->   ($#v3_valued_0 :::"real-valued"::: )     ($#v2_seq_2 :::"bounded_below"::: )    for  ($#v3_valued_0 :::"real-valued"::: )    ($#m1_hidden :::"Function":::); 
end; registrationlet "f" be   ($#v3_valued_0 :::"real-valued"::: )     ($#v1_seq_2 :::"bounded_above"::: )    ($#m1_hidden :::"Function":::); let "r" be  ($#~v3_xxreal_0  "non"   ($#v3_xxreal_0 :::"negative"::: )   )    ($#v1_xreal_0 :::"real"::: )     ($#m1_hidden :::"number"::: )  ; 
cluster (Set "r"  ($#k24_valued_1 :::"(#)"::: )  "f") ->   ($#v3_valued_0 :::"real-valued"::: )     ($#v1_seq_2 :::"bounded_above"::: )    for  ($#v3_valued_0 :::"real-valued"::: )    ($#m1_hidden :::"Function":::); 
end; registrationlet "f" be   ($#v3_valued_0 :::"real-valued"::: )     ($#v2_seq_2 :::"bounded_below"::: )    ($#m1_hidden :::"Function":::); let "r" be  ($#~v3_xxreal_0  "non"   ($#v3_xxreal_0 :::"negative"::: )   )    ($#v1_xreal_0 :::"real"::: )     ($#m1_hidden :::"number"::: )  ; 
cluster (Set "r"  ($#k24_valued_1 :::"(#)"::: )  "f") ->   ($#v3_valued_0 :::"real-valued"::: )     ($#v2_seq_2 :::"bounded_below"::: )    for  ($#v3_valued_0 :::"real-valued"::: )    ($#m1_hidden :::"Function":::); 
end; registrationlet "f" be   ($#v3_valued_0 :::"real-valued"::: )     ($#v1_seq_2 :::"bounded_above"::: )    ($#m1_hidden :::"Function":::); let "r" be  ($#~v2_xxreal_0  "non"   ($#v2_xxreal_0 :::"positive"::: )   )    ($#v1_xreal_0 :::"real"::: )     ($#m1_hidden :::"number"::: )  ; 
cluster (Set "r"  ($#k24_valued_1 :::"(#)"::: )  "f") ->   ($#v3_valued_0 :::"real-valued"::: )     ($#v2_seq_2 :::"bounded_below"::: )    for  ($#v3_valued_0 :::"real-valued"::: )    ($#m1_hidden :::"Function":::); 
end; registrationlet "f" be   ($#v3_valued_0 :::"real-valued"::: )     ($#v2_seq_2 :::"bounded_below"::: )    ($#m1_hidden :::"Function":::); let "r" be  ($#~v2_xxreal_0  "non"   ($#v2_xxreal_0 :::"positive"::: )   )    ($#v1_xreal_0 :::"real"::: )     ($#m1_hidden :::"number"::: )  ; 
cluster (Set "r"  ($#k24_valued_1 :::"(#)"::: )  "f") ->   ($#v3_valued_0 :::"real-valued"::: )     ($#v1_seq_2 :::"bounded_above"::: )    for  ($#v3_valued_0 :::"real-valued"::: )    ($#m1_hidden :::"Function":::); 
end; 
theorem :: RFUNCT_1:78 (Bool  "for" (Set (Var "Y")) "being"    ($#m1_hidden :::"set"::: )    (Bool  "for" (Set (Var "r")) "being"   ($#v1_xreal_0 :::"real"::: )     ($#m1_hidden :::"number"::: )    (Bool  "for" (Set (Var "f")) "being"   ($#v3_valued_0 :::"real-valued"::: )    ($#m1_hidden :::"Function":::) "holds"   (Bool  "("   "("  (Bool (Bool (Set (Set (Var "f"))  ($#k5_relat_1 :::"|"::: )  (Set (Var "Y"))) "is"   ($#v1_seq_2 :::"bounded_above"::: )  ) & (Bool (Set   ($#k6_numbers :::"0"::: )  )  ($#r1_xxreal_0 :::"<="::: )  (Set (Var "r")))) "implies" (Bool (Set (Set  "(" (Set (Var "r"))  ($#k24_valued_1 :::"(#)"::: )  (Set (Var "f")) ")" )  ($#k5_relat_1 :::"|"::: )  (Set (Var "Y"))) "is"   ($#v1_seq_2 :::"bounded_above"::: )  )  ")"  &  "("  (Bool (Bool (Set (Set (Var "f"))  ($#k5_relat_1 :::"|"::: )  (Set (Var "Y"))) "is"   ($#v1_seq_2 :::"bounded_above"::: )  ) & (Bool (Set (Var "r"))  ($#r1_xxreal_0 :::"<="::: )  (Set   ($#k6_numbers :::"0"::: )  ))) "implies" (Bool (Set (Set  "(" (Set (Var "r"))  ($#k24_valued_1 :::"(#)"::: )  (Set (Var "f")) ")" )  ($#k5_relat_1 :::"|"::: )  (Set (Var "Y"))) "is"   ($#v2_seq_2 :::"bounded_below"::: )  )  ")"   ")" )))) ; 
 
theorem :: RFUNCT_1:79 (Bool  "for" (Set (Var "Y")) "being"    ($#m1_hidden :::"set"::: )    (Bool  "for" (Set (Var "r")) "being"   ($#v1_xreal_0 :::"real"::: )     ($#m1_hidden :::"number"::: )    (Bool  "for" (Set (Var "f")) "being"   ($#v3_valued_0 :::"real-valued"::: )    ($#m1_hidden :::"Function":::) "holds"   (Bool  "("   "("  (Bool (Bool (Set (Set (Var "f"))  ($#k5_relat_1 :::"|"::: )  (Set (Var "Y"))) "is"   ($#v2_seq_2 :::"bounded_below"::: )  ) & (Bool (Set   ($#k6_numbers :::"0"::: )  )  ($#r1_xxreal_0 :::"<="::: )  (Set (Var "r")))) "implies" (Bool (Set (Set  "(" (Set (Var "r"))  ($#k24_valued_1 :::"(#)"::: )  (Set (Var "f")) ")" )  ($#k5_relat_1 :::"|"::: )  (Set (Var "Y"))) "is"   ($#v2_seq_2 :::"bounded_below"::: )  )  ")"  &  "("  (Bool (Bool (Set (Set (Var "f"))  ($#k5_relat_1 :::"|"::: )  (Set (Var "Y"))) "is"   ($#v2_seq_2 :::"bounded_below"::: )  ) & (Bool (Set (Var "r"))  ($#r1_xxreal_0 :::"<="::: )  (Set   ($#k6_numbers :::"0"::: )  ))) "implies" (Bool (Set (Set  "(" (Set (Var "r"))  ($#k24_valued_1 :::"(#)"::: )  (Set (Var "f")) ")" )  ($#k5_relat_1 :::"|"::: )  (Set (Var "Y"))) "is"   ($#v1_seq_2 :::"bounded_above"::: )  )  ")"   ")" )))) ; 
 
theorem :: RFUNCT_1:80 (Bool  "for" (Set (Var "Y")) "being"    ($#m1_hidden :::"set"::: )    (Bool  "for" (Set (Var "r")) "being"   ($#v1_xreal_0 :::"real"::: )     ($#m1_hidden :::"number"::: )    (Bool  "for" (Set (Var "f")) "being"   ($#v3_valued_0 :::"real-valued"::: )    ($#m1_hidden :::"Function":::)  "st" (Bool (Bool (Set (Set (Var "f"))  ($#k5_relat_1 :::"|"::: )  (Set (Var "Y"))) "is"   ($#v1_comseq_2 :::"bounded"::: )  )) "holds"  (Bool (Set (Set  "(" (Set (Var "r"))  ($#k24_valued_1 :::"(#)"::: )  (Set (Var "f")) ")" )  ($#k5_relat_1 :::"|"::: )  (Set (Var "Y"))) "is"   ($#v1_comseq_2 :::"bounded"::: )  )))) ; 
 registrationlet "f" be   ($#v3_valued_0 :::"real-valued"::: )    ($#m1_hidden :::"Function":::); 
cluster (Set  ($#k54_valued_1 :::"|."::: ) "f" ($#k54_valued_1 :::".|"::: ) ) ->   ($#v2_seq_2 :::"bounded_below"::: )   ; 
end; 
theorem :: RFUNCT_1:81 (Bool  "for" (Set (Var "X")) "being"    ($#m1_hidden :::"set"::: )    (Bool  "for" (Set (Var "f")) "being"   ($#v3_valued_0 :::"real-valued"::: )    ($#m1_hidden :::"Function":::) "holds"  (Bool (Set (Set  "("  ($#k54_valued_1 :::"abs"::: )  (Set (Var "f")) ")" )  ($#k5_relat_1 :::"|"::: )  (Set (Var "X"))) "is"   ($#v2_seq_2 :::"bounded_below"::: )  ))) ; 
 registrationlet "f" be   ($#v3_valued_0 :::"real-valued"::: )     ($#v1_comseq_2 :::"bounded"::: )    ($#m1_hidden :::"Function":::); 
cluster (Set  ($#k54_valued_1 :::"|."::: ) "f" ($#k54_valued_1 :::".|"::: ) ) ->   ($#v3_valued_0 :::"real-valued"::: )     ($#v1_comseq_2 :::"bounded"::: )    for  ($#v3_valued_0 :::"real-valued"::: )    ($#m1_hidden :::"Function":::); 
end; registrationlet "f" be   ($#v3_valued_0 :::"real-valued"::: )     ($#v1_seq_2 :::"bounded_above"::: )    ($#m1_hidden :::"Function":::); 
cluster (Set   ($#k30_valued_1 :::"-"::: )  "f") ->   ($#v3_valued_0 :::"real-valued"::: )     ($#v2_seq_2 :::"bounded_below"::: )    for  ($#v3_valued_0 :::"real-valued"::: )    ($#m1_hidden :::"Function":::); 
end; 
theorem :: RFUNCT_1:82 (Bool  "for" (Set (Var "Y")) "being"    ($#m1_hidden :::"set"::: )    (Bool  "for" (Set (Var "f")) "being"   ($#v3_valued_0 :::"real-valued"::: )    ($#m1_hidden :::"Function":::)  "st" (Bool (Bool (Set (Set (Var "f"))  ($#k5_relat_1 :::"|"::: )  (Set (Var "Y"))) "is"   ($#v1_comseq_2 :::"bounded"::: )  )) "holds"  (Bool  "("  (Bool (Set (Set  "("  ($#k54_valued_1 :::"abs"::: )  (Set (Var "f")) ")" )  ($#k5_relat_1 :::"|"::: )  (Set (Var "Y"))) "is"   ($#v1_comseq_2 :::"bounded"::: )  ) & (Bool (Set (Set  "("  ($#k30_valued_1 :::"-"::: )  (Set (Var "f")) ")" )  ($#k5_relat_1 :::"|"::: )  (Set (Var "Y"))) "is"   ($#v1_comseq_2 :::"bounded"::: )  )  ")" ))) ; 
 



registrationlet "f1", "f2" be   ($#v3_valued_0 :::"real-valued"::: )     ($#v1_seq_2 :::"bounded_above"::: )    ($#m1_hidden :::"Function":::); 
cluster (Set "f1"  ($#k1_valued_1 :::"+"::: )  "f2") ->   ($#v3_valued_0 :::"real-valued"::: )     ($#v1_seq_2 :::"bounded_above"::: )    for  ($#v3_valued_0 :::"real-valued"::: )    ($#m1_hidden :::"Function":::); 
end; registrationlet "f1", "f2" be   ($#v3_valued_0 :::"real-valued"::: )     ($#v2_seq_2 :::"bounded_below"::: )    ($#m1_hidden :::"Function":::); 
cluster (Set "f1"  ($#k1_valued_1 :::"+"::: )  "f2") ->   ($#v3_valued_0 :::"real-valued"::: )     ($#v2_seq_2 :::"bounded_below"::: )    for  ($#v3_valued_0 :::"real-valued"::: )    ($#m1_hidden :::"Function":::); 
end; 
theorem :: RFUNCT_1:83 (Bool  "for" (Set (Var "X")) "," (Set (Var "Y")) "being"    ($#m1_hidden :::"set"::: )    (Bool  "for" (Set (Var "f1")) "," (Set (Var "f2")) "being"   ($#v3_valued_0 :::"real-valued"::: )    ($#m1_hidden :::"Function":::) "holds"   (Bool  "("   "("  (Bool (Bool (Set (Set (Var "f1"))  ($#k5_relat_1 :::"|"::: )  (Set (Var "X"))) "is"   ($#v1_seq_2 :::"bounded_above"::: )  ) & (Bool (Set (Set (Var "f2"))  ($#k5_relat_1 :::"|"::: )  (Set (Var "Y"))) "is"   ($#v1_seq_2 :::"bounded_above"::: )  )) "implies" (Bool (Set (Set  "(" (Set (Var "f1"))  ($#k1_valued_1 :::"+"::: )  (Set (Var "f2")) ")" )  ($#k5_relat_1 :::"|"::: )  (Set  "(" (Set (Var "X"))  ($#k3_xboole_0 :::"/\"::: )  (Set (Var "Y")) ")" )) "is"   ($#v1_seq_2 :::"bounded_above"::: )  )  ")"  &  "("  (Bool (Bool (Set (Set (Var "f1"))  ($#k5_relat_1 :::"|"::: )  (Set (Var "X"))) "is"   ($#v2_seq_2 :::"bounded_below"::: )  ) & (Bool (Set (Set (Var "f2"))  ($#k5_relat_1 :::"|"::: )  (Set (Var "Y"))) "is"   ($#v2_seq_2 :::"bounded_below"::: )  )) "implies" (Bool (Set (Set  "(" (Set (Var "f1"))  ($#k1_valued_1 :::"+"::: )  (Set (Var "f2")) ")" )  ($#k5_relat_1 :::"|"::: )  (Set  "(" (Set (Var "X"))  ($#k3_xboole_0 :::"/\"::: )  (Set (Var "Y")) ")" )) "is"   ($#v2_seq_2 :::"bounded_below"::: )  )  ")"  &  "("  (Bool (Bool (Set (Set (Var "f1"))  ($#k5_relat_1 :::"|"::: )  (Set (Var "X"))) "is"   ($#v1_comseq_2 :::"bounded"::: )  ) & (Bool (Set (Set (Var "f2"))  ($#k5_relat_1 :::"|"::: )  (Set (Var "Y"))) "is"   ($#v1_comseq_2 :::"bounded"::: )  )) "implies" (Bool (Set (Set  "(" (Set (Var "f1"))  ($#k1_valued_1 :::"+"::: )  (Set (Var "f2")) ")" )  ($#k5_relat_1 :::"|"::: )  (Set  "(" (Set (Var "X"))  ($#k3_xboole_0 :::"/\"::: )  (Set (Var "Y")) ")" )) "is"   ($#v1_comseq_2 :::"bounded"::: )  )  ")"   ")" ))) ; 
 registrationlet "f1", "f2" be   ($#v3_valued_0 :::"real-valued"::: )     ($#v1_comseq_2 :::"bounded"::: )    ($#m1_hidden :::"Function":::); 
cluster (Set "f1"  ($#k18_valued_1 :::"(#)"::: )  "f2") ->   ($#v3_valued_0 :::"real-valued"::: )     ($#v1_comseq_2 :::"bounded"::: )    for  ($#v3_valued_0 :::"real-valued"::: )    ($#m1_hidden :::"Function":::); 
end; 
theorem :: RFUNCT_1:84 (Bool  "for" (Set (Var "X")) "," (Set (Var "Y")) "being"    ($#m1_hidden :::"set"::: )    (Bool  "for" (Set (Var "f1")) "," (Set (Var "f2")) "being"   ($#v3_valued_0 :::"real-valued"::: )    ($#m1_hidden :::"Function":::)  "st" (Bool (Bool (Set (Set (Var "f1"))  ($#k5_relat_1 :::"|"::: )  (Set (Var "X"))) "is"   ($#v1_comseq_2 :::"bounded"::: )  ) & (Bool (Set (Set (Var "f2"))  ($#k5_relat_1 :::"|"::: )  (Set (Var "Y"))) "is"   ($#v1_comseq_2 :::"bounded"::: )  )) "holds"  (Bool  "("  (Bool (Set (Set  "(" (Set (Var "f1"))  ($#k18_valued_1 :::"(#)"::: )  (Set (Var "f2")) ")" )  ($#k5_relat_1 :::"|"::: )  (Set  "(" (Set (Var "X"))  ($#k3_xboole_0 :::"/\"::: )  (Set (Var "Y")) ")" )) "is"   ($#v1_comseq_2 :::"bounded"::: )  ) & (Bool (Set (Set  "(" (Set (Var "f1"))  ($#k45_valued_1 :::"-"::: )  (Set (Var "f2")) ")" )  ($#k5_relat_1 :::"|"::: )  (Set  "(" (Set (Var "X"))  ($#k3_xboole_0 :::"/\"::: )  (Set (Var "Y")) ")" )) "is"   ($#v1_comseq_2 :::"bounded"::: )  )  ")" ))) ; 
 
theorem :: RFUNCT_1:85 (Bool  "for" (Set (Var "X")) "," (Set (Var "Y")) "being"    ($#m1_hidden :::"set"::: )    (Bool  "for" (Set (Var "f")) "being"   ($#v3_valued_0 :::"real-valued"::: )    ($#m1_hidden :::"Function":::)  "st" (Bool (Bool (Set (Set (Var "f"))  ($#k5_relat_1 :::"|"::: )  (Set (Var "X"))) "is"   ($#v1_seq_2 :::"bounded_above"::: )  ) & (Bool (Set (Set (Var "f"))  ($#k5_relat_1 :::"|"::: )  (Set (Var "Y"))) "is"   ($#v1_seq_2 :::"bounded_above"::: )  )) "holds"  (Bool (Set (Set (Var "f"))  ($#k5_relat_1 :::"|"::: )  (Set  "(" (Set (Var "X"))  ($#k2_xboole_0 :::"\/"::: )  (Set (Var "Y")) ")" )) "is"   ($#v1_seq_2 :::"bounded_above"::: )  ))) ; 
 
theorem :: RFUNCT_1:86 (Bool  "for" (Set (Var "X")) "," (Set (Var "Y")) "being"    ($#m1_hidden :::"set"::: )    (Bool  "for" (Set (Var "f")) "being"   ($#v3_valued_0 :::"real-valued"::: )    ($#m1_hidden :::"Function":::)  "st" (Bool (Bool (Set (Set (Var "f"))  ($#k5_relat_1 :::"|"::: )  (Set (Var "X"))) "is"   ($#v2_seq_2 :::"bounded_below"::: )  ) & (Bool (Set (Set (Var "f"))  ($#k5_relat_1 :::"|"::: )  (Set (Var "Y"))) "is"   ($#v2_seq_2 :::"bounded_below"::: )  )) "holds"  (Bool (Set (Set (Var "f"))  ($#k5_relat_1 :::"|"::: )  (Set  "(" (Set (Var "X"))  ($#k2_xboole_0 :::"\/"::: )  (Set (Var "Y")) ")" )) "is"   ($#v2_seq_2 :::"bounded_below"::: )  ))) ; 
 
theorem :: RFUNCT_1:87 (Bool  "for" (Set (Var "X")) "," (Set (Var "Y")) "being"    ($#m1_hidden :::"set"::: )    (Bool  "for" (Set (Var "f")) "being"   ($#v3_valued_0 :::"real-valued"::: )    ($#m1_hidden :::"Function":::)  "st" (Bool (Bool (Set (Set (Var "f"))  ($#k5_relat_1 :::"|"::: )  (Set (Var "X"))) "is"   ($#v1_comseq_2 :::"bounded"::: )  ) & (Bool (Set (Set (Var "f"))  ($#k5_relat_1 :::"|"::: )  (Set (Var "Y"))) "is"   ($#v1_comseq_2 :::"bounded"::: )  )) "holds"  (Bool (Set (Set (Var "f"))  ($#k5_relat_1 :::"|"::: )  (Set  "(" (Set (Var "X"))  ($#k2_xboole_0 :::"\/"::: )  (Set (Var "Y")) ")" )) "is"   ($#v1_comseq_2 :::"bounded"::: )  ))) ; 
 




registrationlet "C" be  ($#~v1_xboole_0  "non"   ($#v1_xboole_0 :::"empty"::: )   )    ($#m1_hidden :::"set"::: )  ; let "f1", "f2" be   ($#v3_funct_1 :::"constant"::: )    ($#m1_subset_1 :::"PartFunc":::) "of" (Set (Const "C")) "," (Set  ($#k1_numbers :::"REAL"::: ) ); 
cluster (Set "f1"  ($#k1_valued_1 :::"+"::: )  "f2") ->   ($#v3_funct_1 :::"constant"::: )   ; 

cluster (Set "f1"  ($#k45_valued_1 :::"-"::: )  "f2") ->   ($#v3_funct_1 :::"constant"::: )   ; 

cluster (Set "f1"  ($#k18_valued_1 :::"(#)"::: )  "f2") ->   ($#v3_funct_1 :::"constant"::: )   ; 
end; 
theorem :: RFUNCT_1:88 (Bool  "for" (Set (Var "X")) "," (Set (Var "Y")) "being"    ($#m1_hidden :::"set"::: )    (Bool  "for" (Set (Var "C")) "being"  ($#~v1_xboole_0  "non"   ($#v1_xboole_0 :::"empty"::: )   )    ($#m1_hidden :::"set"::: )    (Bool  "for" (Set (Var "f1")) "," (Set (Var "f2")) "being"   ($#m1_subset_1 :::"PartFunc":::) "of" (Set (Var "C")) "," (Set  ($#k1_numbers :::"REAL"::: ) )  "st" (Bool (Bool (Set (Set (Var "f1"))  ($#k2_partfun1 :::"|"::: )  (Set (Var "X"))) "is"   ($#v3_funct_1 :::"constant"::: )  ) & (Bool (Set (Set (Var "f2"))  ($#k2_partfun1 :::"|"::: )  (Set (Var "Y"))) "is"   ($#v3_funct_1 :::"constant"::: )  )) "holds"  (Bool  "("  (Bool (Set (Set  "(" (Set (Var "f1"))  ($#k3_valued_1 :::"+"::: )  (Set (Var "f2")) ")" )  ($#k2_partfun1 :::"|"::: )  (Set  "(" (Set (Var "X"))  ($#k3_xboole_0 :::"/\"::: )  (Set (Var "Y")) ")" )) "is"   ($#v3_funct_1 :::"constant"::: )  ) & (Bool (Set (Set  "(" (Set (Var "f1"))  ($#k47_valued_1 :::"-"::: )  (Set (Var "f2")) ")" )  ($#k2_partfun1 :::"|"::: )  (Set  "(" (Set (Var "X"))  ($#k3_xboole_0 :::"/\"::: )  (Set (Var "Y")) ")" )) "is"   ($#v3_funct_1 :::"constant"::: )  ) & (Bool (Set (Set  "(" (Set (Var "f1"))  ($#k20_valued_1 :::"(#)"::: )  (Set (Var "f2")) ")" )  ($#k2_partfun1 :::"|"::: )  (Set  "(" (Set (Var "X"))  ($#k3_xboole_0 :::"/\"::: )  (Set (Var "Y")) ")" )) "is"   ($#v3_funct_1 :::"constant"::: )  )  ")" )))) ; 
 registrationlet "C" be  ($#~v1_xboole_0  "non"   ($#v1_xboole_0 :::"empty"::: )   )    ($#m1_hidden :::"set"::: )  ; let "f" be   ($#v3_funct_1 :::"constant"::: )    ($#m1_subset_1 :::"PartFunc":::) "of" (Set (Const "C")) "," (Set  ($#k1_numbers :::"REAL"::: ) ); 
cluster (Set   ($#k30_valued_1 :::"-"::: )  "f") ->   ($#v3_funct_1 :::"constant"::: )   ; 

cluster (Set  ($#k54_valued_1 :::"|."::: ) "f" ($#k54_valued_1 :::".|"::: ) ) ->   ($#v3_funct_1 :::"constant"::: )   ; 
let "p" be   ($#v1_xreal_0 :::"real"::: )     ($#m1_hidden :::"number"::: )  ; 
cluster (Set "p"  ($#k24_valued_1 :::"(#)"::: )  "f") ->   ($#v3_funct_1 :::"constant"::: )   ; 
end; 
theorem :: RFUNCT_1:89 (Bool  "for" (Set (Var "Y")) "being"    ($#m1_hidden :::"set"::: )    (Bool  "for" (Set (Var "C")) "being"  ($#~v1_xboole_0  "non"   ($#v1_xboole_0 :::"empty"::: )   )    ($#m1_hidden :::"set"::: )    (Bool  "for" (Set (Var "p")) "being"   ($#v1_xreal_0 :::"real"::: )     ($#m1_hidden :::"number"::: )    (Bool  "for" (Set (Var "f")) "being"   ($#m1_subset_1 :::"PartFunc":::) "of" (Set (Var "C")) "," (Set  ($#k1_numbers :::"REAL"::: ) )  "st" (Bool (Bool (Set (Set (Var "f"))  ($#k2_partfun1 :::"|"::: )  (Set (Var "Y"))) "is"   ($#v3_funct_1 :::"constant"::: )  )) "holds"  (Bool (Set (Set  "(" (Set (Var "p"))  ($#k26_valued_1 :::"(#)"::: )  (Set (Var "f")) ")" )  ($#k2_partfun1 :::"|"::: )  (Set (Var "Y"))) "is"   ($#v3_funct_1 :::"constant"::: )  ))))) ; 
 
theorem :: RFUNCT_1:90 (Bool  "for" (Set (Var "Y")) "being"    ($#m1_hidden :::"set"::: )    (Bool  "for" (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  ($#k1_numbers :::"REAL"::: ) )  "st" (Bool (Bool (Set (Set (Var "f"))  ($#k2_partfun1 :::"|"::: )  (Set (Var "Y"))) "is"   ($#v3_funct_1 :::"constant"::: )  )) "holds"  (Bool (Set (Set  "("  ($#k32_valued_1 :::"-"::: )  (Set (Var "f")) ")" )  ($#k2_partfun1 :::"|"::: )  (Set (Var "Y"))) "is"   ($#v3_funct_1 :::"constant"::: )  )))) ; 
 
theorem :: RFUNCT_1:91 (Bool  "for" (Set (Var "Y")) "being"    ($#m1_hidden :::"set"::: )    (Bool  "for" (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  ($#k1_numbers :::"REAL"::: ) )  "st" (Bool (Bool (Set (Set (Var "f"))  ($#k2_partfun1 :::"|"::: )  (Set (Var "Y"))) "is"   ($#v3_funct_1 :::"constant"::: )  )) "holds"  (Bool (Set (Set  "("  ($#k56_valued_1 :::"abs"::: )  (Set (Var "f")) ")" )  ($#k2_partfun1 :::"|"::: )  (Set (Var "Y"))) "is"   ($#v3_funct_1 :::"constant"::: )  )))) ; 
 
theorem :: RFUNCT_1:92 (Bool  "for" (Set (Var "Y")) "being"    ($#m1_hidden :::"set"::: )    (Bool  "for" (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  ($#k1_numbers :::"REAL"::: ) )  "st" (Bool (Bool (Set (Set (Var "f"))  ($#k2_partfun1 :::"|"::: )  (Set (Var "Y"))) "is"   ($#v3_funct_1 :::"constant"::: )  )) "holds"  (Bool  "("  (Bool  "("   "for" (Set (Var "r")) "being"   ($#v1_xreal_0 :::"real"::: )     ($#m1_hidden :::"number"::: )   "holds"  (Bool (Set (Set  "(" (Set (Var "r"))  ($#k26_valued_1 :::"(#)"::: )  (Set (Var "f")) ")" )  ($#k2_partfun1 :::"|"::: )  (Set (Var "Y"))) "is"   ($#v1_comseq_2 :::"bounded"::: )  )  ")" ) & (Bool (Set (Set  "("  ($#k32_valued_1 :::"-"::: )  (Set (Var "f")) ")" )  ($#k2_partfun1 :::"|"::: )  (Set (Var "Y"))) "is"   ($#v1_comseq_2 :::"bounded"::: )  ) & (Bool (Set (Set  "("  ($#k56_valued_1 :::"abs"::: )  (Set (Var "f")) ")" )  ($#k2_partfun1 :::"|"::: )  (Set (Var "Y"))) "is"   ($#v1_comseq_2 :::"bounded"::: )  )  ")" )))) ; 
 
theorem :: RFUNCT_1:93 (Bool  "for" (Set (Var "X")) "," (Set (Var "Y")) "being"    ($#m1_hidden :::"set"::: )    (Bool  "for" (Set (Var "C")) "being"  ($#~v1_xboole_0  "non"   ($#v1_xboole_0 :::"empty"::: )   )    ($#m1_hidden :::"set"::: )    (Bool  "for" (Set (Var "f1")) "," (Set (Var "f2")) "being"   ($#m1_subset_1 :::"PartFunc":::) "of" (Set (Var "C")) "," (Set  ($#k1_numbers :::"REAL"::: ) ) "holds"   (Bool  "("   "("  (Bool (Bool (Set (Set (Var "f1"))  ($#k2_partfun1 :::"|"::: )  (Set (Var "X"))) "is"   ($#v1_seq_2 :::"bounded_above"::: )  ) & (Bool (Set (Set (Var "f2"))  ($#k2_partfun1 :::"|"::: )  (Set (Var "Y"))) "is"   ($#v3_funct_1 :::"constant"::: )  )) "implies" (Bool (Set (Set  "(" (Set (Var "f1"))  ($#k3_valued_1 :::"+"::: )  (Set (Var "f2")) ")" )  ($#k2_partfun1 :::"|"::: )  (Set  "(" (Set (Var "X"))  ($#k3_xboole_0 :::"/\"::: )  (Set (Var "Y")) ")" )) "is"   ($#v1_seq_2 :::"bounded_above"::: )  )  ")"  &  "("  (Bool (Bool (Set (Set (Var "f1"))  ($#k2_partfun1 :::"|"::: )  (Set (Var "X"))) "is"   ($#v2_seq_2 :::"bounded_below"::: )  ) & (Bool (Set (Set (Var "f2"))  ($#k2_partfun1 :::"|"::: )  (Set (Var "Y"))) "is"   ($#v3_funct_1 :::"constant"::: )  )) "implies" (Bool (Set (Set  "(" (Set (Var "f1"))  ($#k3_valued_1 :::"+"::: )  (Set (Var "f2")) ")" )  ($#k2_partfun1 :::"|"::: )  (Set  "(" (Set (Var "X"))  ($#k3_xboole_0 :::"/\"::: )  (Set (Var "Y")) ")" )) "is"   ($#v2_seq_2 :::"bounded_below"::: )  )  ")"  &  "("  (Bool (Bool (Set (Set (Var "f1"))  ($#k2_partfun1 :::"|"::: )  (Set (Var "X"))) "is"   ($#v1_comseq_2 :::"bounded"::: )  ) & (Bool (Set (Set (Var "f2"))  ($#k2_partfun1 :::"|"::: )  (Set (Var "Y"))) "is"   ($#v3_funct_1 :::"constant"::: )  )) "implies" (Bool (Set (Set  "(" (Set (Var "f1"))  ($#k3_valued_1 :::"+"::: )  (Set (Var "f2")) ")" )  ($#k2_partfun1 :::"|"::: )  (Set  "(" (Set (Var "X"))  ($#k3_xboole_0 :::"/\"::: )  (Set (Var "Y")) ")" )) "is"   ($#v1_comseq_2 :::"bounded"::: )  )  ")"   ")" )))) ; 
 
theorem :: RFUNCT_1:94 (Bool  "for" (Set (Var "X")) "," (Set (Var "Y")) "being"    ($#m1_hidden :::"set"::: )    (Bool  "for" (Set (Var "C")) "being"  ($#~v1_xboole_0  "non"   ($#v1_xboole_0 :::"empty"::: )   )    ($#m1_hidden :::"set"::: )    (Bool  "for" (Set (Var "f1")) "," (Set (Var "f2")) "being"   ($#m1_subset_1 :::"PartFunc":::) "of" (Set (Var "C")) "," (Set  ($#k1_numbers :::"REAL"::: ) ) "holds"   (Bool  "("   "("  (Bool (Bool (Set (Set (Var "f1"))  ($#k2_partfun1 :::"|"::: )  (Set (Var "X"))) "is"   ($#v1_seq_2 :::"bounded_above"::: )  ) & (Bool (Set (Set (Var "f2"))  ($#k2_partfun1 :::"|"::: )  (Set (Var "Y"))) "is"   ($#v3_funct_1 :::"constant"::: )  )) "implies" (Bool (Set (Set  "(" (Set (Var "f1"))  ($#k47_valued_1 :::"-"::: )  (Set (Var "f2")) ")" )  ($#k2_partfun1 :::"|"::: )  (Set  "(" (Set (Var "X"))  ($#k3_xboole_0 :::"/\"::: )  (Set (Var "Y")) ")" )) "is"   ($#v1_seq_2 :::"bounded_above"::: )  )  ")"  &  "("  (Bool (Bool (Set (Set (Var "f1"))  ($#k2_partfun1 :::"|"::: )  (Set (Var "X"))) "is"   ($#v2_seq_2 :::"bounded_below"::: )  ) & (Bool (Set (Set (Var "f2"))  ($#k2_partfun1 :::"|"::: )  (Set (Var "Y"))) "is"   ($#v3_funct_1 :::"constant"::: )  )) "implies" (Bool (Set (Set  "(" (Set (Var "f1"))  ($#k47_valued_1 :::"-"::: )  (Set (Var "f2")) ")" )  ($#k2_partfun1 :::"|"::: )  (Set  "(" (Set (Var "X"))  ($#k3_xboole_0 :::"/\"::: )  (Set (Var "Y")) ")" )) "is"   ($#v2_seq_2 :::"bounded_below"::: )  )  ")"  &  "("  (Bool (Bool (Set (Set (Var "f1"))  ($#k2_partfun1 :::"|"::: )  (Set (Var "X"))) "is"   ($#v1_comseq_2 :::"bounded"::: )  ) & (Bool (Set (Set (Var "f2"))  ($#k2_partfun1 :::"|"::: )  (Set (Var "Y"))) "is"   ($#v3_funct_1 :::"constant"::: )  )) "implies" (Bool  "("  (Bool (Set (Set  "(" (Set (Var "f1"))  ($#k47_valued_1 :::"-"::: )  (Set (Var "f2")) ")" )  ($#k2_partfun1 :::"|"::: )  (Set  "(" (Set (Var "X"))  ($#k3_xboole_0 :::"/\"::: )  (Set (Var "Y")) ")" )) "is"   ($#v1_comseq_2 :::"bounded"::: )  ) & (Bool (Set (Set  "(" (Set (Var "f2"))  ($#k47_valued_1 :::"-"::: )  (Set (Var "f1")) ")" )  ($#k2_partfun1 :::"|"::: )  (Set  "(" (Set (Var "X"))  ($#k3_xboole_0 :::"/\"::: )  (Set (Var "Y")) ")" )) "is"   ($#v1_comseq_2 :::"bounded"::: )  ) & (Bool (Set (Set  "(" (Set (Var "f1"))  ($#k20_valued_1 :::"(#)"::: )  (Set (Var "f2")) ")" )  ($#k2_partfun1 :::"|"::: )  (Set  "(" (Set (Var "X"))  ($#k3_xboole_0 :::"/\"::: )  (Set (Var "Y")) ")" )) "is"   ($#v1_comseq_2 :::"bounded"::: )  )  ")" )  ")"   ")" )))) ;