:: PARTFUN3 semantic presentation begin registrationlet "r" be ($#v1_xreal_0 :::"real"::: ) ($#m1_hidden :::"number"::: ) ; cluster (Set "r" ($#k7_xcmplx_0 :::"/"::: ) "r") -> ($#~v3_xxreal_0 "non" ($#v3_xxreal_0 :::"negative"::: ) ) ; end; registrationlet "r" be ($#v1_xreal_0 :::"real"::: ) ($#m1_hidden :::"number"::: ) ; cluster (Set "r" ($#k3_xcmplx_0 :::"*"::: ) "r") -> ($#~v3_xxreal_0 "non" ($#v3_xxreal_0 :::"negative"::: ) ) ; cluster (Set "r" ($#k3_xcmplx_0 :::"*"::: ) (Set "(" "r" ($#k5_xcmplx_0 :::"""::: ) ")" )) -> ($#~v3_xxreal_0 "non" ($#v3_xxreal_0 :::"negative"::: ) ) ; end; registrationlet "r" be ($#v1_xreal_0 :::"real"::: ) ($#~v3_xxreal_0 "non" ($#v3_xxreal_0 :::"negative"::: ) ) ($#m1_hidden :::"number"::: ) ; cluster (Set ($#k6_square_1 :::"sqrt"::: ) "r") -> ($#~v3_xxreal_0 "non" ($#v3_xxreal_0 :::"negative"::: ) ) ; end; registrationlet "r" be ($#v1_xreal_0 :::"real"::: ) ($#v2_xxreal_0 :::"positive"::: ) ($#m1_hidden :::"number"::: ) ; cluster (Set ($#k6_square_1 :::"sqrt"::: ) "r") -> ($#v2_xxreal_0 :::"positive"::: ) ; end; theorem :: PARTFUN3:1 (Bool "for" (Set (Var "f")) "being" ($#m1_hidden :::"Function":::) (Bool "for" (Set (Var "A")) "being" ($#m1_hidden :::"set"::: ) "st" (Bool (Bool (Set (Var "f")) "is" ($#v2_funct_1 :::"one-to-one"::: ) ) & (Bool (Set (Var "A")) ($#r1_tarski :::"c="::: ) (Set ($#k9_xtuple_0 :::"dom"::: ) (Set "(" (Set (Var "f")) ($#k2_funct_1 :::"""::: ) ")" )))) "holds" (Bool (Set (Set (Var "f")) ($#k7_relat_1 :::".:"::: ) (Set "(" (Set "(" (Set (Var "f")) ($#k2_funct_1 :::"""::: ) ")" ) ($#k7_relat_1 :::".:"::: ) (Set (Var "A")) ")" )) ($#r1_hidden :::"="::: ) (Set (Var "A"))))) ; registrationlet "f" be ($#v2_relat_1 :::"non-empty"::: ) ($#m1_hidden :::"Function":::); cluster (Set "f" ($#k8_relat_1 :::"""::: ) (Set ($#k1_tarski :::"{"::: ) (Set ($#k6_numbers :::"0"::: ) ) ($#k1_tarski :::"}"::: ) )) -> ($#v1_xboole_0 :::"empty"::: ) ; end; definitionlet "R" be ($#m1_hidden :::"Relation":::); attr "R" is :::"positive-yielding"::: means :: PARTFUN3:def 1 (Bool "for" (Set (Var "r")) "being" ($#v1_xreal_0 :::"real"::: ) ($#m1_hidden :::"number"::: ) "st" (Bool (Bool (Set (Var "r")) ($#r2_hidden :::"in"::: ) (Set ($#k10_xtuple_0 :::"rng"::: ) "R"))) "holds" (Bool (Set ($#k6_numbers :::"0"::: ) ) ($#r1_xxreal_0 :::"<"::: ) (Set (Var "r")))); attr "R" is :::"negative-yielding"::: means :: PARTFUN3:def 2 (Bool "for" (Set (Var "r")) "being" ($#v1_xreal_0 :::"real"::: ) ($#m1_hidden :::"number"::: ) "st" (Bool (Bool (Set (Var "r")) ($#r2_hidden :::"in"::: ) (Set ($#k10_xtuple_0 :::"rng"::: ) "R"))) "holds" (Bool (Set ($#k6_numbers :::"0"::: ) ) ($#r1_xxreal_0 :::">"::: ) (Set (Var "r")))); attr "R" is :::"nonpositive-yielding"::: means :: PARTFUN3:def 3 (Bool "for" (Set (Var "r")) "being" ($#v1_xreal_0 :::"real"::: ) ($#m1_hidden :::"number"::: ) "st" (Bool (Bool (Set (Var "r")) ($#r2_hidden :::"in"::: ) (Set ($#k10_xtuple_0 :::"rng"::: ) "R"))) "holds" (Bool (Set ($#k6_numbers :::"0"::: ) ) ($#r1_xxreal_0 :::">="::: ) (Set (Var "r")))); attr "R" is :::"nonnegative-yielding"::: means :: PARTFUN3:def 4 (Bool "for" (Set (Var "r")) "being" ($#v1_xreal_0 :::"real"::: ) ($#m1_hidden :::"number"::: ) "st" (Bool (Bool (Set (Var "r")) ($#r2_hidden :::"in"::: ) (Set ($#k10_xtuple_0 :::"rng"::: ) "R"))) "holds" (Bool (Set ($#k6_numbers :::"0"::: ) ) ($#r1_xxreal_0 :::"<="::: ) (Set (Var "r")))); end; :: deftheorem defines :::"positive-yielding"::: PARTFUN3:def 1 : (Bool "for" (Set (Var "R")) "being" ($#m1_hidden :::"Relation":::) "holds" (Bool "(" (Bool (Set (Var "R")) "is" ($#v1_partfun3 :::"positive-yielding"::: ) ) "iff" (Bool "for" (Set (Var "r")) "being" ($#v1_xreal_0 :::"real"::: ) ($#m1_hidden :::"number"::: ) "st" (Bool (Bool (Set (Var "r")) ($#r2_hidden :::"in"::: ) (Set ($#k10_xtuple_0 :::"rng"::: ) (Set (Var "R"))))) "holds" (Bool (Set ($#k6_numbers :::"0"::: ) ) ($#r1_xxreal_0 :::"<"::: ) (Set (Var "r")))) ")" )); :: deftheorem defines :::"negative-yielding"::: PARTFUN3:def 2 : (Bool "for" (Set (Var "R")) "being" ($#m1_hidden :::"Relation":::) "holds" (Bool "(" (Bool (Set (Var "R")) "is" ($#v2_partfun3 :::"negative-yielding"::: ) ) "iff" (Bool "for" (Set (Var "r")) "being" ($#v1_xreal_0 :::"real"::: ) ($#m1_hidden :::"number"::: ) "st" (Bool (Bool (Set (Var "r")) ($#r2_hidden :::"in"::: ) (Set ($#k10_xtuple_0 :::"rng"::: ) (Set (Var "R"))))) "holds" (Bool (Set ($#k6_numbers :::"0"::: ) ) ($#r1_xxreal_0 :::">"::: ) (Set (Var "r")))) ")" )); :: deftheorem defines :::"nonpositive-yielding"::: PARTFUN3:def 3 : (Bool "for" (Set (Var "R")) "being" ($#m1_hidden :::"Relation":::) "holds" (Bool "(" (Bool (Set (Var "R")) "is" ($#v3_partfun3 :::"nonpositive-yielding"::: ) ) "iff" (Bool "for" (Set (Var "r")) "being" ($#v1_xreal_0 :::"real"::: ) ($#m1_hidden :::"number"::: ) "st" (Bool (Bool (Set (Var "r")) ($#r2_hidden :::"in"::: ) (Set ($#k10_xtuple_0 :::"rng"::: ) (Set (Var "R"))))) "holds" (Bool (Set ($#k6_numbers :::"0"::: ) ) ($#r1_xxreal_0 :::">="::: ) (Set (Var "r")))) ")" )); :: deftheorem defines :::"nonnegative-yielding"::: PARTFUN3:def 4 : (Bool "for" (Set (Var "R")) "being" ($#m1_hidden :::"Relation":::) "holds" (Bool "(" (Bool (Set (Var "R")) "is" ($#v4_partfun3 :::"nonnegative-yielding"::: ) ) "iff" (Bool "for" (Set (Var "r")) "being" ($#v1_xreal_0 :::"real"::: ) ($#m1_hidden :::"number"::: ) "st" (Bool (Bool (Set (Var "r")) ($#r2_hidden :::"in"::: ) (Set ($#k10_xtuple_0 :::"rng"::: ) (Set (Var "R"))))) "holds" (Bool (Set ($#k6_numbers :::"0"::: ) ) ($#r1_xxreal_0 :::"<="::: ) (Set (Var "r")))) ")" )); registrationlet "X" be ($#m1_hidden :::"set"::: ) ; let "r" be ($#v1_xreal_0 :::"real"::: ) ($#v2_xxreal_0 :::"positive"::: ) ($#m1_hidden :::"number"::: ) ; cluster (Set "X" ($#k2_funcop_1 :::"-->"::: ) "r") -> ($#v1_partfun3 :::"positive-yielding"::: ) ; end; registrationlet "X" be ($#m1_hidden :::"set"::: ) ; let "r" be ($#v1_xreal_0 :::"real"::: ) ($#v3_xxreal_0 :::"negative"::: ) ($#m1_hidden :::"number"::: ) ; cluster (Set "X" ($#k2_funcop_1 :::"-->"::: ) "r") -> ($#v2_partfun3 :::"negative-yielding"::: ) ; end; registrationlet "X" be ($#m1_hidden :::"set"::: ) ; let "r" be ($#v1_xreal_0 :::"real"::: ) ($#~v2_xxreal_0 "non" ($#v2_xxreal_0 :::"positive"::: ) ) ($#m1_hidden :::"number"::: ) ; cluster (Set "X" ($#k2_funcop_1 :::"-->"::: ) "r") -> ($#v3_partfun3 :::"nonpositive-yielding"::: ) ; end; registrationlet "X" be ($#m1_hidden :::"set"::: ) ; let "r" be ($#v1_xreal_0 :::"real"::: ) ($#~v3_xxreal_0 "non" ($#v3_xxreal_0 :::"negative"::: ) ) ($#m1_hidden :::"number"::: ) ; cluster (Set "X" ($#k2_funcop_1 :::"-->"::: ) "r") -> ($#v4_partfun3 :::"nonnegative-yielding"::: ) ; end; registrationlet "X" be ($#~v1_xboole_0 "non" ($#v1_xboole_0 :::"empty"::: ) ) ($#m1_hidden :::"set"::: ) ; cluster (Set "X" ($#k2_funcop_1 :::"-->"::: ) (Set ($#k6_numbers :::"0"::: ) )) -> ($#~v2_relat_1 "non" ($#v2_relat_1 :::"non-empty"::: ) ) ; end; registration cluster ($#v1_relat_1 :::"Relation-like"::: ) ($#v1_partfun3 :::"positive-yielding"::: ) -> ($#v2_relat_1 :::"non-empty"::: ) ($#v4_partfun3 :::"nonnegative-yielding"::: ) for ($#m1_hidden :::"set"::: ) ; cluster ($#v1_relat_1 :::"Relation-like"::: ) ($#v2_partfun3 :::"negative-yielding"::: ) -> ($#v2_relat_1 :::"non-empty"::: ) ($#v3_partfun3 :::"nonpositive-yielding"::: ) for ($#m1_hidden :::"set"::: ) ; end; registrationlet "X" be ($#m1_hidden :::"set"::: ) ; cluster ($#v1_relat_1 :::"Relation-like"::: ) "X" ($#v4_relat_1 :::"-defined"::: ) (Set ($#k1_numbers :::"REAL"::: ) ) ($#v5_relat_1 :::"-valued"::: ) ($#v1_funct_1 :::"Function-like"::: ) ($#v1_partfun1 :::"total"::: ) bbbadV1_FUNCT_2("X" "," (Set ($#k1_numbers :::"REAL"::: ) )) ($#v1_valued_0 :::"complex-valued"::: ) ($#v2_valued_0 :::"ext-real-valued"::: ) ($#v3_valued_0 :::"real-valued"::: ) ($#v2_partfun3 :::"negative-yielding"::: ) for ($#m1_subset_1 :::"Element"::: ) "of" (Set bbbadK1_ZFMISC_1((Set bbbadK2_ZFMISC_1("X" "," (Set ($#k1_numbers :::"REAL"::: ) ))))); cluster ($#v1_relat_1 :::"Relation-like"::: ) "X" ($#v4_relat_1 :::"-defined"::: ) (Set ($#k1_numbers :::"REAL"::: ) ) ($#v5_relat_1 :::"-valued"::: ) ($#v1_funct_1 :::"Function-like"::: ) ($#v1_partfun1 :::"total"::: ) bbbadV1_FUNCT_2("X" "," (Set ($#k1_numbers :::"REAL"::: ) )) ($#v1_valued_0 :::"complex-valued"::: ) ($#v2_valued_0 :::"ext-real-valued"::: ) ($#v3_valued_0 :::"real-valued"::: ) ($#v1_partfun3 :::"positive-yielding"::: ) for ($#m1_subset_1 :::"Element"::: ) "of" (Set bbbadK1_ZFMISC_1((Set bbbadK2_ZFMISC_1("X" "," (Set ($#k1_numbers :::"REAL"::: ) ))))); end; registration cluster ($#v1_relat_1 :::"Relation-like"::: ) ($#v2_relat_1 :::"non-empty"::: ) ($#v1_funct_1 :::"Function-like"::: ) ($#v3_valued_0 :::"real-valued"::: ) for ($#m1_hidden :::"set"::: ) ; end; theorem :: PARTFUN3:2 (Bool "for" (Set (Var "f")) "being" ($#v2_relat_1 :::"non-empty"::: ) ($#v3_valued_0 :::"real-valued"::: ) ($#m1_hidden :::"Function":::) "holds" (Bool (Set ($#k9_xtuple_0 :::"dom"::: ) (Set "(" (Set (Var "f")) ($#k4_rfunct_1 :::"^"::: ) ")" )) ($#r1_hidden :::"="::: ) (Set ($#k9_xtuple_0 :::"dom"::: ) (Set (Var "f"))))) ; theorem :: PARTFUN3:3 (Bool "for" (Set (Var "X")) "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 "X")) "," (Set ($#k1_numbers :::"REAL"::: ) ) (Bool "for" (Set (Var "g")) "being" ($#v2_relat_1 :::"non-empty"::: ) ($#m1_subset_1 :::"PartFunc":::) "of" (Set (Var "X")) "," (Set ($#k1_numbers :::"REAL"::: ) ) "holds" (Bool (Set ($#k1_relset_1 :::"dom"::: ) (Set "(" (Set (Var "f")) ($#k3_rfunct_1 :::"/"::: ) (Set (Var "g")) ")" )) ($#r1_hidden :::"="::: ) (Set (Set "(" ($#k1_relset_1 :::"dom"::: ) (Set (Var "f")) ")" ) ($#k9_subset_1 :::"/\"::: ) (Set "(" ($#k1_relset_1 :::"dom"::: ) (Set (Var "g")) ")" )))))) ; registrationlet "X" be ($#m1_hidden :::"set"::: ) ; let "f", "g" be ($#v3_partfun3 :::"nonpositive-yielding"::: ) ($#m1_subset_1 :::"PartFunc":::) "of" (Set (Const "X")) "," (Set ($#k1_numbers :::"REAL"::: ) ); cluster (Set "f" ($#k1_valued_1 :::"+"::: ) "g") -> ($#v3_partfun3 :::"nonpositive-yielding"::: ) ; end; registrationlet "X" be ($#m1_hidden :::"set"::: ) ; let "f", "g" be ($#v4_partfun3 :::"nonnegative-yielding"::: ) ($#m1_subset_1 :::"PartFunc":::) "of" (Set (Const "X")) "," (Set ($#k1_numbers :::"REAL"::: ) ); cluster (Set "f" ($#k1_valued_1 :::"+"::: ) "g") -> ($#v4_partfun3 :::"nonnegative-yielding"::: ) ; end; registrationlet "X" be ($#m1_hidden :::"set"::: ) ; let "f" be ($#v1_partfun3 :::"positive-yielding"::: ) ($#m1_subset_1 :::"PartFunc":::) "of" (Set (Const "X")) "," (Set ($#k1_numbers :::"REAL"::: ) ); let "g" be ($#v4_partfun3 :::"nonnegative-yielding"::: ) ($#m1_subset_1 :::"PartFunc":::) "of" (Set (Const "X")) "," (Set ($#k1_numbers :::"REAL"::: ) ); cluster (Set "f" ($#k1_valued_1 :::"+"::: ) "g") -> ($#v1_partfun3 :::"positive-yielding"::: ) ; end; registrationlet "X" be ($#m1_hidden :::"set"::: ) ; let "f" be ($#v4_partfun3 :::"nonnegative-yielding"::: ) ($#m1_subset_1 :::"PartFunc":::) "of" (Set (Const "X")) "," (Set ($#k1_numbers :::"REAL"::: ) ); let "g" be ($#v1_partfun3 :::"positive-yielding"::: ) ($#m1_subset_1 :::"PartFunc":::) "of" (Set (Const "X")) "," (Set ($#k1_numbers :::"REAL"::: ) ); cluster (Set "f" ($#k1_valued_1 :::"+"::: ) "g") -> ($#v1_partfun3 :::"positive-yielding"::: ) ; end; registrationlet "X" be ($#m1_hidden :::"set"::: ) ; let "f" be ($#v3_partfun3 :::"nonpositive-yielding"::: ) ($#m1_subset_1 :::"PartFunc":::) "of" (Set (Const "X")) "," (Set ($#k1_numbers :::"REAL"::: ) ); let "g" be ($#v2_partfun3 :::"negative-yielding"::: ) ($#m1_subset_1 :::"PartFunc":::) "of" (Set (Const "X")) "," (Set ($#k1_numbers :::"REAL"::: ) ); cluster (Set "f" ($#k1_valued_1 :::"+"::: ) "g") -> ($#v2_partfun3 :::"negative-yielding"::: ) ; end; registrationlet "X" be ($#m1_hidden :::"set"::: ) ; let "f" be ($#v2_partfun3 :::"negative-yielding"::: ) ($#m1_subset_1 :::"PartFunc":::) "of" (Set (Const "X")) "," (Set ($#k1_numbers :::"REAL"::: ) ); let "g" be ($#v3_partfun3 :::"nonpositive-yielding"::: ) ($#m1_subset_1 :::"PartFunc":::) "of" (Set (Const "X")) "," (Set ($#k1_numbers :::"REAL"::: ) ); cluster (Set "f" ($#k1_valued_1 :::"+"::: ) "g") -> ($#v2_partfun3 :::"negative-yielding"::: ) ; end; registrationlet "X" be ($#m1_hidden :::"set"::: ) ; let "f" be ($#v4_partfun3 :::"nonnegative-yielding"::: ) ($#m1_subset_1 :::"PartFunc":::) "of" (Set (Const "X")) "," (Set ($#k1_numbers :::"REAL"::: ) ); let "g" be ($#v3_partfun3 :::"nonpositive-yielding"::: ) ($#m1_subset_1 :::"PartFunc":::) "of" (Set (Const "X")) "," (Set ($#k1_numbers :::"REAL"::: ) ); cluster (Set "f" ($#k45_valued_1 :::"-"::: ) "g") -> ($#v4_partfun3 :::"nonnegative-yielding"::: ) ; end; registrationlet "X" be ($#m1_hidden :::"set"::: ) ; let "f" be ($#v3_partfun3 :::"nonpositive-yielding"::: ) ($#m1_subset_1 :::"PartFunc":::) "of" (Set (Const "X")) "," (Set ($#k1_numbers :::"REAL"::: ) ); let "g" be ($#v4_partfun3 :::"nonnegative-yielding"::: ) ($#m1_subset_1 :::"PartFunc":::) "of" (Set (Const "X")) "," (Set ($#k1_numbers :::"REAL"::: ) ); cluster (Set "f" ($#k45_valued_1 :::"-"::: ) "g") -> ($#v3_partfun3 :::"nonpositive-yielding"::: ) ; end; registrationlet "X" be ($#m1_hidden :::"set"::: ) ; let "f" be ($#v1_partfun3 :::"positive-yielding"::: ) ($#m1_subset_1 :::"PartFunc":::) "of" (Set (Const "X")) "," (Set ($#k1_numbers :::"REAL"::: ) ); let "g" be ($#v3_partfun3 :::"nonpositive-yielding"::: ) ($#m1_subset_1 :::"PartFunc":::) "of" (Set (Const "X")) "," (Set ($#k1_numbers :::"REAL"::: ) ); cluster (Set "f" ($#k45_valued_1 :::"-"::: ) "g") -> ($#v1_partfun3 :::"positive-yielding"::: ) ; end; registrationlet "X" be ($#m1_hidden :::"set"::: ) ; let "f" be ($#v3_partfun3 :::"nonpositive-yielding"::: ) ($#m1_subset_1 :::"PartFunc":::) "of" (Set (Const "X")) "," (Set ($#k1_numbers :::"REAL"::: ) ); let "g" be ($#v1_partfun3 :::"positive-yielding"::: ) ($#m1_subset_1 :::"PartFunc":::) "of" (Set (Const "X")) "," (Set ($#k1_numbers :::"REAL"::: ) ); cluster (Set "f" ($#k45_valued_1 :::"-"::: ) "g") -> ($#v2_partfun3 :::"negative-yielding"::: ) ; end; registrationlet "X" be ($#m1_hidden :::"set"::: ) ; let "f" be ($#v2_partfun3 :::"negative-yielding"::: ) ($#m1_subset_1 :::"PartFunc":::) "of" (Set (Const "X")) "," (Set ($#k1_numbers :::"REAL"::: ) ); let "g" be ($#v4_partfun3 :::"nonnegative-yielding"::: ) ($#m1_subset_1 :::"PartFunc":::) "of" (Set (Const "X")) "," (Set ($#k1_numbers :::"REAL"::: ) ); cluster (Set "f" ($#k45_valued_1 :::"-"::: ) "g") -> ($#v2_partfun3 :::"negative-yielding"::: ) ; end; registrationlet "X" be ($#m1_hidden :::"set"::: ) ; let "f" be ($#v4_partfun3 :::"nonnegative-yielding"::: ) ($#m1_subset_1 :::"PartFunc":::) "of" (Set (Const "X")) "," (Set ($#k1_numbers :::"REAL"::: ) ); let "g" be ($#v2_partfun3 :::"negative-yielding"::: ) ($#m1_subset_1 :::"PartFunc":::) "of" (Set (Const "X")) "," (Set ($#k1_numbers :::"REAL"::: ) ); cluster (Set "f" ($#k45_valued_1 :::"-"::: ) "g") -> ($#v1_partfun3 :::"positive-yielding"::: ) ; end; registrationlet "X" be ($#m1_hidden :::"set"::: ) ; let "f", "g" be ($#v3_partfun3 :::"nonpositive-yielding"::: ) ($#m1_subset_1 :::"PartFunc":::) "of" (Set (Const "X")) "," (Set ($#k1_numbers :::"REAL"::: ) ); cluster (Set "f" ($#k18_valued_1 :::"(#)"::: ) "g") -> ($#v4_partfun3 :::"nonnegative-yielding"::: ) ; end; registrationlet "X" be ($#m1_hidden :::"set"::: ) ; let "f", "g" be ($#v4_partfun3 :::"nonnegative-yielding"::: ) ($#m1_subset_1 :::"PartFunc":::) "of" (Set (Const "X")) "," (Set ($#k1_numbers :::"REAL"::: ) ); cluster (Set "f" ($#k18_valued_1 :::"(#)"::: ) "g") -> ($#v4_partfun3 :::"nonnegative-yielding"::: ) ; end; registrationlet "X" be ($#m1_hidden :::"set"::: ) ; let "f" be ($#v3_partfun3 :::"nonpositive-yielding"::: ) ($#m1_subset_1 :::"PartFunc":::) "of" (Set (Const "X")) "," (Set ($#k1_numbers :::"REAL"::: ) ); let "g" be ($#v4_partfun3 :::"nonnegative-yielding"::: ) ($#m1_subset_1 :::"PartFunc":::) "of" (Set (Const "X")) "," (Set ($#k1_numbers :::"REAL"::: ) ); cluster (Set "f" ($#k18_valued_1 :::"(#)"::: ) "g") -> ($#v3_partfun3 :::"nonpositive-yielding"::: ) ; end; registrationlet "X" be ($#m1_hidden :::"set"::: ) ; let "f" be ($#v4_partfun3 :::"nonnegative-yielding"::: ) ($#m1_subset_1 :::"PartFunc":::) "of" (Set (Const "X")) "," (Set ($#k1_numbers :::"REAL"::: ) ); let "g" be ($#v3_partfun3 :::"nonpositive-yielding"::: ) ($#m1_subset_1 :::"PartFunc":::) "of" (Set (Const "X")) "," (Set ($#k1_numbers :::"REAL"::: ) ); cluster (Set "f" ($#k18_valued_1 :::"(#)"::: ) "g") -> ($#v3_partfun3 :::"nonpositive-yielding"::: ) ; end; registrationlet "X" be ($#m1_hidden :::"set"::: ) ; let "f" be ($#v1_partfun3 :::"positive-yielding"::: ) ($#m1_subset_1 :::"PartFunc":::) "of" (Set (Const "X")) "," (Set ($#k1_numbers :::"REAL"::: ) ); let "g" be ($#v2_partfun3 :::"negative-yielding"::: ) ($#m1_subset_1 :::"PartFunc":::) "of" (Set (Const "X")) "," (Set ($#k1_numbers :::"REAL"::: ) ); cluster (Set "f" ($#k18_valued_1 :::"(#)"::: ) "g") -> ($#v2_partfun3 :::"negative-yielding"::: ) ; end; registrationlet "X" be ($#m1_hidden :::"set"::: ) ; let "f" be ($#v2_partfun3 :::"negative-yielding"::: ) ($#m1_subset_1 :::"PartFunc":::) "of" (Set (Const "X")) "," (Set ($#k1_numbers :::"REAL"::: ) ); let "g" be ($#v1_partfun3 :::"positive-yielding"::: ) ($#m1_subset_1 :::"PartFunc":::) "of" (Set (Const "X")) "," (Set ($#k1_numbers :::"REAL"::: ) ); cluster (Set "f" ($#k18_valued_1 :::"(#)"::: ) "g") -> ($#v2_partfun3 :::"negative-yielding"::: ) ; end; registrationlet "X" be ($#m1_hidden :::"set"::: ) ; let "f", "g" be ($#v1_partfun3 :::"positive-yielding"::: ) ($#m1_subset_1 :::"PartFunc":::) "of" (Set (Const "X")) "," (Set ($#k1_numbers :::"REAL"::: ) ); cluster (Set "f" ($#k18_valued_1 :::"(#)"::: ) "g") -> ($#v1_partfun3 :::"positive-yielding"::: ) ; end; registrationlet "X" be ($#m1_hidden :::"set"::: ) ; let "f", "g" be ($#v2_partfun3 :::"negative-yielding"::: ) ($#m1_subset_1 :::"PartFunc":::) "of" (Set (Const "X")) "," (Set ($#k1_numbers :::"REAL"::: ) ); cluster (Set "f" ($#k18_valued_1 :::"(#)"::: ) "g") -> ($#v1_partfun3 :::"positive-yielding"::: ) ; end; registrationlet "X" be ($#m1_hidden :::"set"::: ) ; let "f", "g" be ($#v2_relat_1 :::"non-empty"::: ) ($#m1_subset_1 :::"PartFunc":::) "of" (Set (Const "X")) "," (Set ($#k1_numbers :::"REAL"::: ) ); cluster (Set "f" ($#k18_valued_1 :::"(#)"::: ) "g") -> ($#v2_relat_1 :::"non-empty"::: ) ; end; registrationlet "X" be ($#m1_hidden :::"set"::: ) ; let "f" be ($#m1_subset_1 :::"PartFunc":::) "of" (Set (Const "X")) "," (Set ($#k1_numbers :::"REAL"::: ) ); cluster (Set "f" ($#k18_valued_1 :::"(#)"::: ) "f") -> ($#v4_partfun3 :::"nonnegative-yielding"::: ) ; end; registrationlet "X" be ($#m1_hidden :::"set"::: ) ; let "r" be ($#v1_xreal_0 :::"real"::: ) ($#~v2_xxreal_0 "non" ($#v2_xxreal_0 :::"positive"::: ) ) ($#m1_hidden :::"number"::: ) ; let "f" be ($#v3_partfun3 :::"nonpositive-yielding"::: ) ($#m1_subset_1 :::"PartFunc":::) "of" (Set (Const "X")) "," (Set ($#k1_numbers :::"REAL"::: ) ); cluster (Set "r" ($#k24_valued_1 :::"(#)"::: ) "f") -> ($#v4_partfun3 :::"nonnegative-yielding"::: ) ; end; registrationlet "X" be ($#m1_hidden :::"set"::: ) ; let "r" be ($#v1_xreal_0 :::"real"::: ) ($#~v3_xxreal_0 "non" ($#v3_xxreal_0 :::"negative"::: ) ) ($#m1_hidden :::"number"::: ) ; let "f" be ($#v4_partfun3 :::"nonnegative-yielding"::: ) ($#m1_subset_1 :::"PartFunc":::) "of" (Set (Const "X")) "," (Set ($#k1_numbers :::"REAL"::: ) ); cluster (Set "r" ($#k24_valued_1 :::"(#)"::: ) "f") -> ($#v4_partfun3 :::"nonnegative-yielding"::: ) ; end; registrationlet "X" be ($#m1_hidden :::"set"::: ) ; let "r" be ($#v1_xreal_0 :::"real"::: ) ($#~v2_xxreal_0 "non" ($#v2_xxreal_0 :::"positive"::: ) ) ($#m1_hidden :::"number"::: ) ; let "f" be ($#v4_partfun3 :::"nonnegative-yielding"::: ) ($#m1_subset_1 :::"PartFunc":::) "of" (Set (Const "X")) "," (Set ($#k1_numbers :::"REAL"::: ) ); cluster (Set "r" ($#k24_valued_1 :::"(#)"::: ) "f") -> ($#v3_partfun3 :::"nonpositive-yielding"::: ) ; end; registrationlet "X" be ($#m1_hidden :::"set"::: ) ; let "r" be ($#v1_xreal_0 :::"real"::: ) ($#~v3_xxreal_0 "non" ($#v3_xxreal_0 :::"negative"::: ) ) ($#m1_hidden :::"number"::: ) ; let "f" be ($#v3_partfun3 :::"nonpositive-yielding"::: ) ($#m1_subset_1 :::"PartFunc":::) "of" (Set (Const "X")) "," (Set ($#k1_numbers :::"REAL"::: ) ); cluster (Set "r" ($#k24_valued_1 :::"(#)"::: ) "f") -> ($#v3_partfun3 :::"nonpositive-yielding"::: ) ; end; registrationlet "X" be ($#m1_hidden :::"set"::: ) ; let "r" be ($#v1_xreal_0 :::"real"::: ) ($#v2_xxreal_0 :::"positive"::: ) ($#m1_hidden :::"number"::: ) ; let "f" be ($#v2_partfun3 :::"negative-yielding"::: ) ($#m1_subset_1 :::"PartFunc":::) "of" (Set (Const "X")) "," (Set ($#k1_numbers :::"REAL"::: ) ); cluster (Set "r" ($#k24_valued_1 :::"(#)"::: ) "f") -> ($#v2_partfun3 :::"negative-yielding"::: ) ; end; registrationlet "X" be ($#m1_hidden :::"set"::: ) ; let "r" be ($#v1_xreal_0 :::"real"::: ) ($#v3_xxreal_0 :::"negative"::: ) ($#m1_hidden :::"number"::: ) ; let "f" be ($#v1_partfun3 :::"positive-yielding"::: ) ($#m1_subset_1 :::"PartFunc":::) "of" (Set (Const "X")) "," (Set ($#k1_numbers :::"REAL"::: ) ); cluster (Set "r" ($#k24_valued_1 :::"(#)"::: ) "f") -> ($#v2_partfun3 :::"negative-yielding"::: ) ; end; registrationlet "X" be ($#m1_hidden :::"set"::: ) ; let "r" be ($#v1_xreal_0 :::"real"::: ) ($#v2_xxreal_0 :::"positive"::: ) ($#m1_hidden :::"number"::: ) ; let "f" be ($#v1_partfun3 :::"positive-yielding"::: ) ($#m1_subset_1 :::"PartFunc":::) "of" (Set (Const "X")) "," (Set ($#k1_numbers :::"REAL"::: ) ); cluster (Set "r" ($#k24_valued_1 :::"(#)"::: ) "f") -> ($#v1_partfun3 :::"positive-yielding"::: ) ; end; registrationlet "X" be ($#m1_hidden :::"set"::: ) ; let "r" be ($#v1_xreal_0 :::"real"::: ) ($#v3_xxreal_0 :::"negative"::: ) ($#m1_hidden :::"number"::: ) ; let "f" be ($#v2_partfun3 :::"negative-yielding"::: ) ($#m1_subset_1 :::"PartFunc":::) "of" (Set (Const "X")) "," (Set ($#k1_numbers :::"REAL"::: ) ); cluster (Set "r" ($#k24_valued_1 :::"(#)"::: ) "f") -> ($#v1_partfun3 :::"positive-yielding"::: ) ; end; registrationlet "X" be ($#m1_hidden :::"set"::: ) ; let "r" be ($#~v1_xboole_0 "non" ($#v1_xboole_0 :::"zero"::: ) ) ($#v1_xreal_0 :::"real"::: ) ($#m1_hidden :::"number"::: ) ; let "f" be ($#v2_relat_1 :::"non-empty"::: ) ($#m1_subset_1 :::"PartFunc":::) "of" (Set (Const "X")) "," (Set ($#k1_numbers :::"REAL"::: ) ); cluster (Set "r" ($#k24_valued_1 :::"(#)"::: ) "f") -> ($#v2_relat_1 :::"non-empty"::: ) ; end; registrationlet "X" be ($#~v1_xboole_0 "non" ($#v1_xboole_0 :::"empty"::: ) ) ($#m1_hidden :::"set"::: ) ; let "f", "g" be ($#v3_partfun3 :::"nonpositive-yielding"::: ) ($#m1_subset_1 :::"PartFunc":::) "of" (Set (Const "X")) "," (Set ($#k1_numbers :::"REAL"::: ) ); cluster (Set "f" ($#k1_rfunct_1 :::"/"::: ) "g") -> ($#v4_partfun3 :::"nonnegative-yielding"::: ) ; end; registrationlet "X" be ($#~v1_xboole_0 "non" ($#v1_xboole_0 :::"empty"::: ) ) ($#m1_hidden :::"set"::: ) ; let "f", "g" be ($#v4_partfun3 :::"nonnegative-yielding"::: ) ($#m1_subset_1 :::"PartFunc":::) "of" (Set (Const "X")) "," (Set ($#k1_numbers :::"REAL"::: ) ); cluster (Set "f" ($#k1_rfunct_1 :::"/"::: ) "g") -> ($#v4_partfun3 :::"nonnegative-yielding"::: ) ; end; registrationlet "X" be ($#~v1_xboole_0 "non" ($#v1_xboole_0 :::"empty"::: ) ) ($#m1_hidden :::"set"::: ) ; let "f" be ($#v3_partfun3 :::"nonpositive-yielding"::: ) ($#m1_subset_1 :::"PartFunc":::) "of" (Set (Const "X")) "," (Set ($#k1_numbers :::"REAL"::: ) ); let "g" be ($#v4_partfun3 :::"nonnegative-yielding"::: ) ($#m1_subset_1 :::"PartFunc":::) "of" (Set (Const "X")) "," (Set ($#k1_numbers :::"REAL"::: ) ); cluster (Set "f" ($#k1_rfunct_1 :::"/"::: ) "g") -> ($#v3_partfun3 :::"nonpositive-yielding"::: ) ; end; registrationlet "X" be ($#~v1_xboole_0 "non" ($#v1_xboole_0 :::"empty"::: ) ) ($#m1_hidden :::"set"::: ) ; let "f" be ($#v4_partfun3 :::"nonnegative-yielding"::: ) ($#m1_subset_1 :::"PartFunc":::) "of" (Set (Const "X")) "," (Set ($#k1_numbers :::"REAL"::: ) ); let "g" be ($#v3_partfun3 :::"nonpositive-yielding"::: ) ($#m1_subset_1 :::"PartFunc":::) "of" (Set (Const "X")) "," (Set ($#k1_numbers :::"REAL"::: ) ); cluster (Set "f" ($#k1_rfunct_1 :::"/"::: ) "g") -> ($#v3_partfun3 :::"nonpositive-yielding"::: ) ; end; registrationlet "X" be ($#~v1_xboole_0 "non" ($#v1_xboole_0 :::"empty"::: ) ) ($#m1_hidden :::"set"::: ) ; let "f" be ($#v1_partfun3 :::"positive-yielding"::: ) ($#m1_subset_1 :::"PartFunc":::) "of" (Set (Const "X")) "," (Set ($#k1_numbers :::"REAL"::: ) ); let "g" be ($#v2_partfun3 :::"negative-yielding"::: ) ($#m1_subset_1 :::"PartFunc":::) "of" (Set (Const "X")) "," (Set ($#k1_numbers :::"REAL"::: ) ); cluster (Set "f" ($#k1_rfunct_1 :::"/"::: ) "g") -> ($#v2_partfun3 :::"negative-yielding"::: ) ; end; registrationlet "X" be ($#~v1_xboole_0 "non" ($#v1_xboole_0 :::"empty"::: ) ) ($#m1_hidden :::"set"::: ) ; let "f" be ($#v2_partfun3 :::"negative-yielding"::: ) ($#m1_subset_1 :::"PartFunc":::) "of" (Set (Const "X")) "," (Set ($#k1_numbers :::"REAL"::: ) ); let "g" be ($#v1_partfun3 :::"positive-yielding"::: ) ($#m1_subset_1 :::"PartFunc":::) "of" (Set (Const "X")) "," (Set ($#k1_numbers :::"REAL"::: ) ); cluster (Set "f" ($#k1_rfunct_1 :::"/"::: ) "g") -> ($#v2_partfun3 :::"negative-yielding"::: ) ; end; registrationlet "X" be ($#~v1_xboole_0 "non" ($#v1_xboole_0 :::"empty"::: ) ) ($#m1_hidden :::"set"::: ) ; let "f", "g" be ($#v1_partfun3 :::"positive-yielding"::: ) ($#m1_subset_1 :::"PartFunc":::) "of" (Set (Const "X")) "," (Set ($#k1_numbers :::"REAL"::: ) ); cluster (Set "f" ($#k1_rfunct_1 :::"/"::: ) "g") -> ($#v1_partfun3 :::"positive-yielding"::: ) ; end; registrationlet "X" be ($#~v1_xboole_0 "non" ($#v1_xboole_0 :::"empty"::: ) ) ($#m1_hidden :::"set"::: ) ; let "f", "g" be ($#v2_partfun3 :::"negative-yielding"::: ) ($#m1_subset_1 :::"PartFunc":::) "of" (Set (Const "X")) "," (Set ($#k1_numbers :::"REAL"::: ) ); cluster (Set "f" ($#k1_rfunct_1 :::"/"::: ) "g") -> ($#v1_partfun3 :::"positive-yielding"::: ) ; end; registrationlet "X" be ($#~v1_xboole_0 "non" ($#v1_xboole_0 :::"empty"::: ) ) ($#m1_hidden :::"set"::: ) ; let "f" be ($#m1_subset_1 :::"PartFunc":::) "of" (Set (Const "X")) "," (Set ($#k1_numbers :::"REAL"::: ) ); cluster (Set "f" ($#k1_rfunct_1 :::"/"::: ) "f") -> ($#v4_partfun3 :::"nonnegative-yielding"::: ) ; end; registrationlet "X" be ($#~v1_xboole_0 "non" ($#v1_xboole_0 :::"empty"::: ) ) ($#m1_hidden :::"set"::: ) ; let "f", "g" be ($#v2_relat_1 :::"non-empty"::: ) ($#m1_subset_1 :::"PartFunc":::) "of" (Set (Const "X")) "," (Set ($#k1_numbers :::"REAL"::: ) ); cluster (Set "f" ($#k1_rfunct_1 :::"/"::: ) "g") -> ($#v2_relat_1 :::"non-empty"::: ) ; end; registrationlet "X" be ($#m1_hidden :::"set"::: ) ; let "f" be ($#v3_partfun3 :::"nonpositive-yielding"::: ) ($#m1_subset_1 :::"Function":::) "of" (Set (Const "X")) "," (Set ($#k1_numbers :::"REAL"::: ) ); cluster (Set ($#k35_valued_1 :::"Inv"::: ) "f") -> ($#v3_partfun3 :::"nonpositive-yielding"::: ) ; end; registrationlet "X" be ($#m1_hidden :::"set"::: ) ; let "f" be ($#v4_partfun3 :::"nonnegative-yielding"::: ) ($#m1_subset_1 :::"Function":::) "of" (Set (Const "X")) "," (Set ($#k1_numbers :::"REAL"::: ) ); cluster (Set ($#k35_valued_1 :::"Inv"::: ) "f") -> ($#v4_partfun3 :::"nonnegative-yielding"::: ) ; end; registrationlet "X" be ($#m1_hidden :::"set"::: ) ; let "f" be ($#v1_partfun3 :::"positive-yielding"::: ) ($#m1_subset_1 :::"Function":::) "of" (Set (Const "X")) "," (Set ($#k1_numbers :::"REAL"::: ) ); cluster (Set ($#k35_valued_1 :::"Inv"::: ) "f") -> ($#v1_partfun3 :::"positive-yielding"::: ) ; end; registrationlet "X" be ($#m1_hidden :::"set"::: ) ; let "f" be ($#v2_partfun3 :::"negative-yielding"::: ) ($#m1_subset_1 :::"Function":::) "of" (Set (Const "X")) "," (Set ($#k1_numbers :::"REAL"::: ) ); cluster (Set ($#k35_valued_1 :::"Inv"::: ) "f") -> ($#v2_partfun3 :::"negative-yielding"::: ) ; end; registrationlet "X" be ($#m1_hidden :::"set"::: ) ; let "f" be ($#v2_relat_1 :::"non-empty"::: ) ($#m1_subset_1 :::"Function":::) "of" (Set (Const "X")) "," (Set ($#k1_numbers :::"REAL"::: ) ); cluster (Set ($#k35_valued_1 :::"Inv"::: ) "f") -> ($#v2_relat_1 :::"non-empty"::: ) ; end; registrationlet "X" be ($#m1_hidden :::"set"::: ) ; let "f" be ($#v2_relat_1 :::"non-empty"::: ) ($#m1_subset_1 :::"Function":::) "of" (Set (Const "X")) "," (Set ($#k1_numbers :::"REAL"::: ) ); cluster (Set ($#k30_valued_1 :::"-"::: ) "f") -> ($#v2_relat_1 :::"non-empty"::: ) ; end; registrationlet "X" be ($#m1_hidden :::"set"::: ) ; let "f" be ($#v3_partfun3 :::"nonpositive-yielding"::: ) ($#m1_subset_1 :::"Function":::) "of" (Set (Const "X")) "," (Set ($#k1_numbers :::"REAL"::: ) ); cluster (Set ($#k30_valued_1 :::"-"::: ) "f") -> ($#v4_partfun3 :::"nonnegative-yielding"::: ) ; end; registrationlet "X" be ($#m1_hidden :::"set"::: ) ; let "f" be ($#v4_partfun3 :::"nonnegative-yielding"::: ) ($#m1_subset_1 :::"Function":::) "of" (Set (Const "X")) "," (Set ($#k1_numbers :::"REAL"::: ) ); cluster (Set ($#k30_valued_1 :::"-"::: ) "f") -> ($#v3_partfun3 :::"nonpositive-yielding"::: ) ; end; registrationlet "X" be ($#m1_hidden :::"set"::: ) ; let "f" be ($#v1_partfun3 :::"positive-yielding"::: ) ($#m1_subset_1 :::"Function":::) "of" (Set (Const "X")) "," (Set ($#k1_numbers :::"REAL"::: ) ); cluster (Set ($#k30_valued_1 :::"-"::: ) "f") -> ($#v2_partfun3 :::"negative-yielding"::: ) ; end; registrationlet "X" be ($#m1_hidden :::"set"::: ) ; let "f" be ($#v2_partfun3 :::"negative-yielding"::: ) ($#m1_subset_1 :::"Function":::) "of" (Set (Const "X")) "," (Set ($#k1_numbers :::"REAL"::: ) ); cluster (Set ($#k30_valued_1 :::"-"::: ) "f") -> ($#v1_partfun3 :::"positive-yielding"::: ) ; end; registrationlet "X" be ($#m1_hidden :::"set"::: ) ; let "f" be ($#m1_subset_1 :::"Function":::) "of" (Set (Const "X")) "," (Set ($#k1_numbers :::"REAL"::: ) ); cluster (Set ($#k54_valued_1 :::"|."::: ) "f" ($#k54_valued_1 :::".|"::: ) ) -> ($#v4_partfun3 :::"nonnegative-yielding"::: ) ; end; registrationlet "X" be ($#m1_hidden :::"set"::: ) ; let "f" be ($#v2_relat_1 :::"non-empty"::: ) ($#m1_subset_1 :::"Function":::) "of" (Set (Const "X")) "," (Set ($#k1_numbers :::"REAL"::: ) ); cluster (Set ($#k54_valued_1 :::"|."::: ) "f" ($#k54_valued_1 :::".|"::: ) ) -> ($#v1_partfun3 :::"positive-yielding"::: ) ; end; registrationlet "X" be ($#~v1_xboole_0 "non" ($#v1_xboole_0 :::"empty"::: ) ) ($#m1_hidden :::"set"::: ) ; let "f" be ($#v3_partfun3 :::"nonpositive-yielding"::: ) ($#m1_subset_1 :::"Function":::) "of" (Set (Const "X")) "," (Set ($#k1_numbers :::"REAL"::: ) ); cluster (Set "f" ($#k4_rfunct_1 :::"^"::: ) ) -> ($#v3_partfun3 :::"nonpositive-yielding"::: ) ; end; registrationlet "X" be ($#~v1_xboole_0 "non" ($#v1_xboole_0 :::"empty"::: ) ) ($#m1_hidden :::"set"::: ) ; let "f" be ($#v4_partfun3 :::"nonnegative-yielding"::: ) ($#m1_subset_1 :::"Function":::) "of" (Set (Const "X")) "," (Set ($#k1_numbers :::"REAL"::: ) ); cluster (Set "f" ($#k4_rfunct_1 :::"^"::: ) ) -> ($#v4_partfun3 :::"nonnegative-yielding"::: ) ; end; registrationlet "X" be ($#~v1_xboole_0 "non" ($#v1_xboole_0 :::"empty"::: ) ) ($#m1_hidden :::"set"::: ) ; let "f" be ($#v1_partfun3 :::"positive-yielding"::: ) ($#m1_subset_1 :::"Function":::) "of" (Set (Const "X")) "," (Set ($#k1_numbers :::"REAL"::: ) ); cluster (Set "f" ($#k4_rfunct_1 :::"^"::: ) ) -> ($#v1_partfun3 :::"positive-yielding"::: ) ; end; registrationlet "X" be ($#~v1_xboole_0 "non" ($#v1_xboole_0 :::"empty"::: ) ) ($#m1_hidden :::"set"::: ) ; let "f" be ($#v2_partfun3 :::"negative-yielding"::: ) ($#m1_subset_1 :::"Function":::) "of" (Set (Const "X")) "," (Set ($#k1_numbers :::"REAL"::: ) ); cluster (Set "f" ($#k4_rfunct_1 :::"^"::: ) ) -> ($#v2_partfun3 :::"negative-yielding"::: ) ; end; registrationlet "X" be ($#~v1_xboole_0 "non" ($#v1_xboole_0 :::"empty"::: ) ) ($#m1_hidden :::"set"::: ) ; let "f" be ($#v2_relat_1 :::"non-empty"::: ) ($#m1_subset_1 :::"Function":::) "of" (Set (Const "X")) "," (Set ($#k1_numbers :::"REAL"::: ) ); cluster (Set "f" ($#k4_rfunct_1 :::"^"::: ) ) -> ($#v2_relat_1 :::"non-empty"::: ) ; end; definitionlet "f" be ($#v3_valued_0 :::"real-valued"::: ) ($#m1_hidden :::"Function":::); func :::"sqrt"::: "f" -> ($#m1_hidden :::"Function":::) means :: PARTFUN3:def 5 (Bool "(" (Bool (Set ($#k9_xtuple_0 :::"dom"::: ) it) ($#r1_hidden :::"="::: ) (Set ($#k9_xtuple_0 :::"dom"::: ) "f")) & (Bool "(" "for" (Set (Var "x")) "being" ($#m1_hidden :::"set"::: ) "st" (Bool (Bool (Set (Var "x")) ($#r2_hidden :::"in"::: ) (Set ($#k9_xtuple_0 :::"dom"::: ) it))) "holds" (Bool (Set it ($#k1_funct_1 :::"."::: ) (Set (Var "x"))) ($#r1_hidden :::"="::: ) (Set ($#k7_square_1 :::"sqrt"::: ) (Set "(" "f" ($#k1_seq_1 :::"."::: ) (Set (Var "x")) ")" ))) ")" ) ")" ); end; :: deftheorem defines :::"sqrt"::: PARTFUN3:def 5 : (Bool "for" (Set (Var "f")) "being" ($#v3_valued_0 :::"real-valued"::: ) ($#m1_hidden :::"Function":::) (Bool "for" (Set (Var "b2")) "being" ($#m1_hidden :::"Function":::) "holds" (Bool "(" (Bool (Set (Var "b2")) ($#r1_hidden :::"="::: ) (Set ($#k1_partfun3 :::"sqrt"::: ) (Set (Var "f")))) "iff" (Bool "(" (Bool (Set ($#k9_xtuple_0 :::"dom"::: ) (Set (Var "b2"))) ($#r1_hidden :::"="::: ) (Set ($#k9_xtuple_0 :::"dom"::: ) (Set (Var "f")))) & (Bool "(" "for" (Set (Var "x")) "being" ($#m1_hidden :::"set"::: ) "st" (Bool (Bool (Set (Var "x")) ($#r2_hidden :::"in"::: ) (Set ($#k9_xtuple_0 :::"dom"::: ) (Set (Var "b2"))))) "holds" (Bool (Set (Set (Var "b2")) ($#k1_funct_1 :::"."::: ) (Set (Var "x"))) ($#r1_hidden :::"="::: ) (Set ($#k7_square_1 :::"sqrt"::: ) (Set "(" (Set (Var "f")) ($#k1_seq_1 :::"."::: ) (Set (Var "x")) ")" ))) ")" ) ")" ) ")" ))); registrationlet "f" be ($#v3_valued_0 :::"real-valued"::: ) ($#m1_hidden :::"Function":::); cluster (Set ($#k1_partfun3 :::"sqrt"::: ) "f") -> ($#v3_valued_0 :::"real-valued"::: ) ; 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: :::"sqrt"::: redefine func :::"sqrt"::: "f" -> ($#m1_subset_1 :::"PartFunc":::) "of" "C" "," (Set ($#k1_numbers :::"REAL"::: ) ); end; registrationlet "X" be ($#m1_hidden :::"set"::: ) ; let "f" be ($#v4_partfun3 :::"nonnegative-yielding"::: ) ($#m1_subset_1 :::"Function":::) "of" (Set (Const "X")) "," (Set ($#k1_numbers :::"REAL"::: ) ); cluster (Set ($#k1_partfun3 :::"sqrt"::: ) "f") -> ($#v4_partfun3 :::"nonnegative-yielding"::: ) ; end; registrationlet "X" be ($#m1_hidden :::"set"::: ) ; let "f" be ($#v1_partfun3 :::"positive-yielding"::: ) ($#m1_subset_1 :::"Function":::) "of" (Set (Const "X")) "," (Set ($#k1_numbers :::"REAL"::: ) ); cluster (Set ($#k1_partfun3 :::"sqrt"::: ) "f") -> ($#v1_partfun3 :::"positive-yielding"::: ) ; end; definitionlet "X" be ($#m1_hidden :::"set"::: ) ; let "f" be ($#m1_subset_1 :::"Function":::) "of" (Set (Const "X")) "," (Set ($#k1_numbers :::"REAL"::: ) ); :: original: :::"sqrt"::: redefine func :::"sqrt"::: "f" -> ($#m1_subset_1 :::"Function":::) "of" "X" "," (Set ($#k1_numbers :::"REAL"::: ) ); end; definitionlet "X" be ($#m1_hidden :::"set"::: ) ; let "f" be ($#v2_relat_1 :::"non-empty"::: ) ($#m1_subset_1 :::"Function":::) "of" (Set (Const "X")) "," (Set ($#k1_numbers :::"REAL"::: ) ); :: original: :::"^"::: redefine func "f" :::"^"::: -> ($#m1_subset_1 :::"Function":::) "of" "X" "," (Set ($#k1_numbers :::"REAL"::: ) ); end; definitionlet "X" be ($#~v1_xboole_0 "non" ($#v1_xboole_0 :::"empty"::: ) ) ($#m1_hidden :::"set"::: ) ; let "f" be ($#m1_subset_1 :::"Function":::) "of" (Set (Const "X")) "," (Set ($#k1_numbers :::"REAL"::: ) ); let "g" be ($#v2_relat_1 :::"non-empty"::: ) ($#m1_subset_1 :::"Function":::) "of" (Set (Const "X")) "," (Set ($#k1_numbers :::"REAL"::: ) ); :: original: :::"/"::: redefine func "f" :::"/"::: "g" -> ($#m1_subset_1 :::"Function":::) "of" "X" "," (Set ($#k1_numbers :::"REAL"::: ) ); end;