:: VALUED_2 semantic presentation begin definitionlet "Y" be ($#v4_funct_1 :::"functional"::: ) ($#m1_hidden :::"set"::: ) ; func :::"DOMS"::: "Y" -> ($#m1_hidden :::"set"::: ) equals :: VALUED_2:def 1 (Set ($#k3_tarski :::"union"::: ) "{" (Set "(" ($#k9_xtuple_0 :::"dom"::: ) (Set (Var "f")) ")" ) where f "is" ($#m1_subset_1 :::"Element"::: ) "of" "Y" : (Bool verum) "}" ); end; :: deftheorem defines :::"DOMS"::: VALUED_2:def 1 : (Bool "for" (Set (Var "Y")) "being" ($#v4_funct_1 :::"functional"::: ) ($#m1_hidden :::"set"::: ) "holds" (Bool (Set ($#k1_valued_2 :::"DOMS"::: ) (Set (Var "Y"))) ($#r1_hidden :::"="::: ) (Set ($#k3_tarski :::"union"::: ) "{" (Set "(" ($#k9_xtuple_0 :::"dom"::: ) (Set (Var "f")) ")" ) where f "is" ($#m1_subset_1 :::"Element"::: ) "of" (Set (Var "Y")) : (Bool verum) "}" ))); definitionlet "X" be ($#m1_hidden :::"set"::: ) ; attr "X" is :::"complex-functions-membered"::: means :: VALUED_2:def 2 (Bool "for" (Set (Var "x")) "being" ($#m1_hidden :::"set"::: ) "st" (Bool (Bool (Set (Var "x")) ($#r2_hidden :::"in"::: ) "X")) "holds" (Bool (Set (Var "x")) "is" ($#v1_valued_0 :::"complex-valued"::: ) ($#m1_hidden :::"Function":::))); end; :: deftheorem defines :::"complex-functions-membered"::: VALUED_2:def 2 : (Bool "for" (Set (Var "X")) "being" ($#m1_hidden :::"set"::: ) "holds" (Bool "(" (Bool (Set (Var "X")) "is" ($#v1_valued_2 :::"complex-functions-membered"::: ) ) "iff" (Bool "for" (Set (Var "x")) "being" ($#m1_hidden :::"set"::: ) "st" (Bool (Bool (Set (Var "x")) ($#r2_hidden :::"in"::: ) (Set (Var "X")))) "holds" (Bool (Set (Var "x")) "is" ($#v1_valued_0 :::"complex-valued"::: ) ($#m1_hidden :::"Function":::))) ")" )); definitionlet "X" be ($#m1_hidden :::"set"::: ) ; attr "X" is :::"ext-real-functions-membered"::: means :: VALUED_2:def 3 (Bool "for" (Set (Var "x")) "being" ($#m1_hidden :::"set"::: ) "st" (Bool (Bool (Set (Var "x")) ($#r2_hidden :::"in"::: ) "X")) "holds" (Bool (Set (Var "x")) "is" ($#v2_valued_0 :::"ext-real-valued"::: ) ($#m1_hidden :::"Function":::))); end; :: deftheorem defines :::"ext-real-functions-membered"::: VALUED_2:def 3 : (Bool "for" (Set (Var "X")) "being" ($#m1_hidden :::"set"::: ) "holds" (Bool "(" (Bool (Set (Var "X")) "is" ($#v2_valued_2 :::"ext-real-functions-membered"::: ) ) "iff" (Bool "for" (Set (Var "x")) "being" ($#m1_hidden :::"set"::: ) "st" (Bool (Bool (Set (Var "x")) ($#r2_hidden :::"in"::: ) (Set (Var "X")))) "holds" (Bool (Set (Var "x")) "is" ($#v2_valued_0 :::"ext-real-valued"::: ) ($#m1_hidden :::"Function":::))) ")" )); definitionlet "X" be ($#m1_hidden :::"set"::: ) ; attr "X" is :::"real-functions-membered"::: means :: VALUED_2:def 4 (Bool "for" (Set (Var "x")) "being" ($#m1_hidden :::"set"::: ) "st" (Bool (Bool (Set (Var "x")) ($#r2_hidden :::"in"::: ) "X")) "holds" (Bool (Set (Var "x")) "is" ($#v3_valued_0 :::"real-valued"::: ) ($#m1_hidden :::"Function":::))); end; :: deftheorem defines :::"real-functions-membered"::: VALUED_2:def 4 : (Bool "for" (Set (Var "X")) "being" ($#m1_hidden :::"set"::: ) "holds" (Bool "(" (Bool (Set (Var "X")) "is" ($#v3_valued_2 :::"real-functions-membered"::: ) ) "iff" (Bool "for" (Set (Var "x")) "being" ($#m1_hidden :::"set"::: ) "st" (Bool (Bool (Set (Var "x")) ($#r2_hidden :::"in"::: ) (Set (Var "X")))) "holds" (Bool (Set (Var "x")) "is" ($#v3_valued_0 :::"real-valued"::: ) ($#m1_hidden :::"Function":::))) ")" )); definitionlet "X" be ($#m1_hidden :::"set"::: ) ; attr "X" is :::"rational-functions-membered"::: means :: VALUED_2:def 5 (Bool "for" (Set (Var "x")) "being" ($#m1_hidden :::"set"::: ) "st" (Bool (Bool (Set (Var "x")) ($#r2_hidden :::"in"::: ) "X")) "holds" (Bool (Set (Var "x")) "is" (Set ($#k3_numbers :::"RAT"::: ) ) ($#v5_relat_1 :::"-valued"::: ) ($#m1_hidden :::"Function":::))); end; :: deftheorem defines :::"rational-functions-membered"::: VALUED_2:def 5 : (Bool "for" (Set (Var "X")) "being" ($#m1_hidden :::"set"::: ) "holds" (Bool "(" (Bool (Set (Var "X")) "is" ($#v4_valued_2 :::"rational-functions-membered"::: ) ) "iff" (Bool "for" (Set (Var "x")) "being" ($#m1_hidden :::"set"::: ) "st" (Bool (Bool (Set (Var "x")) ($#r2_hidden :::"in"::: ) (Set (Var "X")))) "holds" (Bool (Set (Var "x")) "is" (Set ($#k3_numbers :::"RAT"::: ) ) ($#v5_relat_1 :::"-valued"::: ) ($#m1_hidden :::"Function":::))) ")" )); definitionlet "X" be ($#m1_hidden :::"set"::: ) ; attr "X" is :::"integer-functions-membered"::: means :: VALUED_2:def 6 (Bool "for" (Set (Var "x")) "being" ($#m1_hidden :::"set"::: ) "st" (Bool (Bool (Set (Var "x")) ($#r2_hidden :::"in"::: ) "X")) "holds" (Bool (Set (Var "x")) "is" (Set ($#k4_numbers :::"INT"::: ) ) ($#v5_relat_1 :::"-valued"::: ) ($#m1_hidden :::"Function":::))); end; :: deftheorem defines :::"integer-functions-membered"::: VALUED_2:def 6 : (Bool "for" (Set (Var "X")) "being" ($#m1_hidden :::"set"::: ) "holds" (Bool "(" (Bool (Set (Var "X")) "is" ($#v5_valued_2 :::"integer-functions-membered"::: ) ) "iff" (Bool "for" (Set (Var "x")) "being" ($#m1_hidden :::"set"::: ) "st" (Bool (Bool (Set (Var "x")) ($#r2_hidden :::"in"::: ) (Set (Var "X")))) "holds" (Bool (Set (Var "x")) "is" (Set ($#k4_numbers :::"INT"::: ) ) ($#v5_relat_1 :::"-valued"::: ) ($#m1_hidden :::"Function":::))) ")" )); definitionlet "X" be ($#m1_hidden :::"set"::: ) ; attr "X" is :::"natural-functions-membered"::: means :: VALUED_2:def 7 (Bool "for" (Set (Var "x")) "being" ($#m1_hidden :::"set"::: ) "st" (Bool (Bool (Set (Var "x")) ($#r2_hidden :::"in"::: ) "X")) "holds" (Bool (Set (Var "x")) "is" ($#v4_valued_0 :::"natural-valued"::: ) ($#m1_hidden :::"Function":::))); end; :: deftheorem defines :::"natural-functions-membered"::: VALUED_2:def 7 : (Bool "for" (Set (Var "X")) "being" ($#m1_hidden :::"set"::: ) "holds" (Bool "(" (Bool (Set (Var "X")) "is" ($#v6_valued_2 :::"natural-functions-membered"::: ) ) "iff" (Bool "for" (Set (Var "x")) "being" ($#m1_hidden :::"set"::: ) "st" (Bool (Bool (Set (Var "x")) ($#r2_hidden :::"in"::: ) (Set (Var "X")))) "holds" (Bool (Set (Var "x")) "is" ($#v4_valued_0 :::"natural-valued"::: ) ($#m1_hidden :::"Function":::))) ")" )); registration cluster ($#v6_valued_2 :::"natural-functions-membered"::: ) -> ($#v5_valued_2 :::"integer-functions-membered"::: ) for ($#m1_hidden :::"set"::: ) ; cluster ($#v5_valued_2 :::"integer-functions-membered"::: ) -> ($#v4_valued_2 :::"rational-functions-membered"::: ) for ($#m1_hidden :::"set"::: ) ; cluster ($#v4_valued_2 :::"rational-functions-membered"::: ) -> ($#v3_valued_2 :::"real-functions-membered"::: ) for ($#m1_hidden :::"set"::: ) ; cluster ($#v3_valued_2 :::"real-functions-membered"::: ) -> ($#v1_valued_2 :::"complex-functions-membered"::: ) for ($#m1_hidden :::"set"::: ) ; cluster ($#v3_valued_2 :::"real-functions-membered"::: ) -> ($#v2_valued_2 :::"ext-real-functions-membered"::: ) for ($#m1_hidden :::"set"::: ) ; end; registration cluster ($#v1_xboole_0 :::"empty"::: ) -> ($#v6_valued_2 :::"natural-functions-membered"::: ) for ($#m1_hidden :::"set"::: ) ; end; registrationlet "f" be ($#v1_valued_0 :::"complex-valued"::: ) ($#m1_hidden :::"Function":::); cluster (Set ($#k1_tarski :::"{"::: ) "f" ($#k1_tarski :::"}"::: ) ) -> ($#v1_valued_2 :::"complex-functions-membered"::: ) ; end; registration cluster ($#v1_valued_2 :::"complex-functions-membered"::: ) -> ($#v4_funct_1 :::"functional"::: ) for ($#m1_hidden :::"set"::: ) ; cluster ($#v2_valued_2 :::"ext-real-functions-membered"::: ) -> ($#v4_funct_1 :::"functional"::: ) for ($#m1_hidden :::"set"::: ) ; end; registration cluster ($#~v1_xboole_0 "non" ($#v1_xboole_0 :::"empty"::: ) ) ($#v6_valued_2 :::"natural-functions-membered"::: ) for ($#m1_hidden :::"set"::: ) ; end; registrationlet "X" be ($#v1_valued_2 :::"complex-functions-membered"::: ) ($#m1_hidden :::"set"::: ) ; cluster -> ($#v1_valued_2 :::"complex-functions-membered"::: ) for ($#m1_subset_1 :::"Element"::: ) "of" (Set bbbadK1_ZFMISC_1("X")); end; registrationlet "X" be ($#v2_valued_2 :::"ext-real-functions-membered"::: ) ($#m1_hidden :::"set"::: ) ; cluster -> ($#v2_valued_2 :::"ext-real-functions-membered"::: ) for ($#m1_subset_1 :::"Element"::: ) "of" (Set bbbadK1_ZFMISC_1("X")); end; registrationlet "X" be ($#v3_valued_2 :::"real-functions-membered"::: ) ($#m1_hidden :::"set"::: ) ; cluster -> ($#v3_valued_2 :::"real-functions-membered"::: ) for ($#m1_subset_1 :::"Element"::: ) "of" (Set bbbadK1_ZFMISC_1("X")); end; registrationlet "X" be ($#v4_valued_2 :::"rational-functions-membered"::: ) ($#m1_hidden :::"set"::: ) ; cluster -> ($#v4_valued_2 :::"rational-functions-membered"::: ) for ($#m1_subset_1 :::"Element"::: ) "of" (Set bbbadK1_ZFMISC_1("X")); end; registrationlet "X" be ($#v5_valued_2 :::"integer-functions-membered"::: ) ($#m1_hidden :::"set"::: ) ; cluster -> ($#v5_valued_2 :::"integer-functions-membered"::: ) for ($#m1_subset_1 :::"Element"::: ) "of" (Set bbbadK1_ZFMISC_1("X")); end; registrationlet "X" be ($#v6_valued_2 :::"natural-functions-membered"::: ) ($#m1_hidden :::"set"::: ) ; cluster -> ($#v6_valued_2 :::"natural-functions-membered"::: ) for ($#m1_subset_1 :::"Element"::: ) "of" (Set bbbadK1_ZFMISC_1("X")); end; definitionlet "D" be ($#m1_hidden :::"set"::: ) ; func :::"C_PFuncs"::: "D" -> ($#m1_hidden :::"set"::: ) means :: VALUED_2:def 8 (Bool "for" (Set (Var "f")) "being" ($#m1_hidden :::"set"::: ) "holds" (Bool "(" (Bool (Set (Var "f")) ($#r2_hidden :::"in"::: ) it) "iff" (Bool (Set (Var "f")) "is" ($#m1_subset_1 :::"PartFunc":::) "of" "D" "," (Set ($#k2_numbers :::"COMPLEX"::: ) )) ")" )); end; :: deftheorem defines :::"C_PFuncs"::: VALUED_2:def 8 : (Bool "for" (Set (Var "D")) "," (Set (Var "b2")) "being" ($#m1_hidden :::"set"::: ) "holds" (Bool "(" (Bool (Set (Var "b2")) ($#r1_hidden :::"="::: ) (Set ($#k2_valued_2 :::"C_PFuncs"::: ) (Set (Var "D")))) "iff" (Bool "for" (Set (Var "f")) "being" ($#m1_hidden :::"set"::: ) "holds" (Bool "(" (Bool (Set (Var "f")) ($#r2_hidden :::"in"::: ) (Set (Var "b2"))) "iff" (Bool (Set (Var "f")) "is" ($#m1_subset_1 :::"PartFunc":::) "of" (Set (Var "D")) "," (Set ($#k2_numbers :::"COMPLEX"::: ) )) ")" )) ")" )); definitionlet "D" be ($#m1_hidden :::"set"::: ) ; func :::"C_Funcs"::: "D" -> ($#m1_hidden :::"set"::: ) means :: VALUED_2:def 9 (Bool "for" (Set (Var "f")) "being" ($#m1_hidden :::"set"::: ) "holds" (Bool "(" (Bool (Set (Var "f")) ($#r2_hidden :::"in"::: ) it) "iff" (Bool (Set (Var "f")) "is" ($#m1_subset_1 :::"Function":::) "of" "D" "," (Set ($#k2_numbers :::"COMPLEX"::: ) )) ")" )); end; :: deftheorem defines :::"C_Funcs"::: VALUED_2:def 9 : (Bool "for" (Set (Var "D")) "," (Set (Var "b2")) "being" ($#m1_hidden :::"set"::: ) "holds" (Bool "(" (Bool (Set (Var "b2")) ($#r1_hidden :::"="::: ) (Set ($#k3_valued_2 :::"C_Funcs"::: ) (Set (Var "D")))) "iff" (Bool "for" (Set (Var "f")) "being" ($#m1_hidden :::"set"::: ) "holds" (Bool "(" (Bool (Set (Var "f")) ($#r2_hidden :::"in"::: ) (Set (Var "b2"))) "iff" (Bool (Set (Var "f")) "is" ($#m1_subset_1 :::"Function":::) "of" (Set (Var "D")) "," (Set ($#k2_numbers :::"COMPLEX"::: ) )) ")" )) ")" )); definitionlet "D" be ($#m1_hidden :::"set"::: ) ; func :::"E_PFuncs"::: "D" -> ($#m1_hidden :::"set"::: ) means :: VALUED_2:def 10 (Bool "for" (Set (Var "f")) "being" ($#m1_hidden :::"set"::: ) "holds" (Bool "(" (Bool (Set (Var "f")) ($#r2_hidden :::"in"::: ) it) "iff" (Bool (Set (Var "f")) "is" ($#m1_subset_1 :::"PartFunc":::) "of" "D" "," (Set ($#k7_numbers :::"ExtREAL"::: ) )) ")" )); end; :: deftheorem defines :::"E_PFuncs"::: VALUED_2:def 10 : (Bool "for" (Set (Var "D")) "," (Set (Var "b2")) "being" ($#m1_hidden :::"set"::: ) "holds" (Bool "(" (Bool (Set (Var "b2")) ($#r1_hidden :::"="::: ) (Set ($#k4_valued_2 :::"E_PFuncs"::: ) (Set (Var "D")))) "iff" (Bool "for" (Set (Var "f")) "being" ($#m1_hidden :::"set"::: ) "holds" (Bool "(" (Bool (Set (Var "f")) ($#r2_hidden :::"in"::: ) (Set (Var "b2"))) "iff" (Bool (Set (Var "f")) "is" ($#m1_subset_1 :::"PartFunc":::) "of" (Set (Var "D")) "," (Set ($#k7_numbers :::"ExtREAL"::: ) )) ")" )) ")" )); definitionlet "D" be ($#m1_hidden :::"set"::: ) ; func :::"E_Funcs"::: "D" -> ($#m1_hidden :::"set"::: ) means :: VALUED_2:def 11 (Bool "for" (Set (Var "f")) "being" ($#m1_hidden :::"set"::: ) "holds" (Bool "(" (Bool (Set (Var "f")) ($#r2_hidden :::"in"::: ) it) "iff" (Bool (Set (Var "f")) "is" ($#m1_subset_1 :::"Function":::) "of" "D" "," (Set ($#k7_numbers :::"ExtREAL"::: ) )) ")" )); end; :: deftheorem defines :::"E_Funcs"::: VALUED_2:def 11 : (Bool "for" (Set (Var "D")) "," (Set (Var "b2")) "being" ($#m1_hidden :::"set"::: ) "holds" (Bool "(" (Bool (Set (Var "b2")) ($#r1_hidden :::"="::: ) (Set ($#k5_valued_2 :::"E_Funcs"::: ) (Set (Var "D")))) "iff" (Bool "for" (Set (Var "f")) "being" ($#m1_hidden :::"set"::: ) "holds" (Bool "(" (Bool (Set (Var "f")) ($#r2_hidden :::"in"::: ) (Set (Var "b2"))) "iff" (Bool (Set (Var "f")) "is" ($#m1_subset_1 :::"Function":::) "of" (Set (Var "D")) "," (Set ($#k7_numbers :::"ExtREAL"::: ) )) ")" )) ")" )); definitionlet "D" be ($#m1_hidden :::"set"::: ) ; func :::"R_PFuncs"::: "D" -> ($#m1_hidden :::"set"::: ) means :: VALUED_2:def 12 (Bool "for" (Set (Var "f")) "being" ($#m1_hidden :::"set"::: ) "holds" (Bool "(" (Bool (Set (Var "f")) ($#r2_hidden :::"in"::: ) it) "iff" (Bool (Set (Var "f")) "is" ($#m1_subset_1 :::"PartFunc":::) "of" "D" "," (Set ($#k1_numbers :::"REAL"::: ) )) ")" )); end; :: deftheorem defines :::"R_PFuncs"::: VALUED_2:def 12 : (Bool "for" (Set (Var "D")) "," (Set (Var "b2")) "being" ($#m1_hidden :::"set"::: ) "holds" (Bool "(" (Bool (Set (Var "b2")) ($#r1_hidden :::"="::: ) (Set ($#k6_valued_2 :::"R_PFuncs"::: ) (Set (Var "D")))) "iff" (Bool "for" (Set (Var "f")) "being" ($#m1_hidden :::"set"::: ) "holds" (Bool "(" (Bool (Set (Var "f")) ($#r2_hidden :::"in"::: ) (Set (Var "b2"))) "iff" (Bool (Set (Var "f")) "is" ($#m1_subset_1 :::"PartFunc":::) "of" (Set (Var "D")) "," (Set ($#k1_numbers :::"REAL"::: ) )) ")" )) ")" )); definitionlet "D" be ($#m1_hidden :::"set"::: ) ; func :::"R_Funcs"::: "D" -> ($#m1_hidden :::"set"::: ) means :: VALUED_2:def 13 (Bool "for" (Set (Var "f")) "being" ($#m1_hidden :::"set"::: ) "holds" (Bool "(" (Bool (Set (Var "f")) ($#r2_hidden :::"in"::: ) it) "iff" (Bool (Set (Var "f")) "is" ($#m1_subset_1 :::"Function":::) "of" "D" "," (Set ($#k1_numbers :::"REAL"::: ) )) ")" )); end; :: deftheorem defines :::"R_Funcs"::: VALUED_2:def 13 : (Bool "for" (Set (Var "D")) "," (Set (Var "b2")) "being" ($#m1_hidden :::"set"::: ) "holds" (Bool "(" (Bool (Set (Var "b2")) ($#r1_hidden :::"="::: ) (Set ($#k7_valued_2 :::"R_Funcs"::: ) (Set (Var "D")))) "iff" (Bool "for" (Set (Var "f")) "being" ($#m1_hidden :::"set"::: ) "holds" (Bool "(" (Bool (Set (Var "f")) ($#r2_hidden :::"in"::: ) (Set (Var "b2"))) "iff" (Bool (Set (Var "f")) "is" ($#m1_subset_1 :::"Function":::) "of" (Set (Var "D")) "," (Set ($#k1_numbers :::"REAL"::: ) )) ")" )) ")" )); definitionlet "D" be ($#m1_hidden :::"set"::: ) ; func :::"Q_PFuncs"::: "D" -> ($#m1_hidden :::"set"::: ) means :: VALUED_2:def 14 (Bool "for" (Set (Var "f")) "being" ($#m1_hidden :::"set"::: ) "holds" (Bool "(" (Bool (Set (Var "f")) ($#r2_hidden :::"in"::: ) it) "iff" (Bool (Set (Var "f")) "is" ($#m1_subset_1 :::"PartFunc":::) "of" "D" "," (Set ($#k3_numbers :::"RAT"::: ) )) ")" )); end; :: deftheorem defines :::"Q_PFuncs"::: VALUED_2:def 14 : (Bool "for" (Set (Var "D")) "," (Set (Var "b2")) "being" ($#m1_hidden :::"set"::: ) "holds" (Bool "(" (Bool (Set (Var "b2")) ($#r1_hidden :::"="::: ) (Set ($#k8_valued_2 :::"Q_PFuncs"::: ) (Set (Var "D")))) "iff" (Bool "for" (Set (Var "f")) "being" ($#m1_hidden :::"set"::: ) "holds" (Bool "(" (Bool (Set (Var "f")) ($#r2_hidden :::"in"::: ) (Set (Var "b2"))) "iff" (Bool (Set (Var "f")) "is" ($#m1_subset_1 :::"PartFunc":::) "of" (Set (Var "D")) "," (Set ($#k3_numbers :::"RAT"::: ) )) ")" )) ")" )); definitionlet "D" be ($#m1_hidden :::"set"::: ) ; func :::"Q_Funcs"::: "D" -> ($#m1_hidden :::"set"::: ) means :: VALUED_2:def 15 (Bool "for" (Set (Var "f")) "being" ($#m1_hidden :::"set"::: ) "holds" (Bool "(" (Bool (Set (Var "f")) ($#r2_hidden :::"in"::: ) it) "iff" (Bool (Set (Var "f")) "is" ($#m1_subset_1 :::"Function":::) "of" "D" "," (Set ($#k3_numbers :::"RAT"::: ) )) ")" )); end; :: deftheorem defines :::"Q_Funcs"::: VALUED_2:def 15 : (Bool "for" (Set (Var "D")) "," (Set (Var "b2")) "being" ($#m1_hidden :::"set"::: ) "holds" (Bool "(" (Bool (Set (Var "b2")) ($#r1_hidden :::"="::: ) (Set ($#k9_valued_2 :::"Q_Funcs"::: ) (Set (Var "D")))) "iff" (Bool "for" (Set (Var "f")) "being" ($#m1_hidden :::"set"::: ) "holds" (Bool "(" (Bool (Set (Var "f")) ($#r2_hidden :::"in"::: ) (Set (Var "b2"))) "iff" (Bool (Set (Var "f")) "is" ($#m1_subset_1 :::"Function":::) "of" (Set (Var "D")) "," (Set ($#k3_numbers :::"RAT"::: ) )) ")" )) ")" )); definitionlet "D" be ($#m1_hidden :::"set"::: ) ; func :::"I_PFuncs"::: "D" -> ($#m1_hidden :::"set"::: ) means :: VALUED_2:def 16 (Bool "for" (Set (Var "f")) "being" ($#m1_hidden :::"set"::: ) "holds" (Bool "(" (Bool (Set (Var "f")) ($#r2_hidden :::"in"::: ) it) "iff" (Bool (Set (Var "f")) "is" ($#m1_subset_1 :::"PartFunc":::) "of" "D" "," (Set ($#k4_numbers :::"INT"::: ) )) ")" )); end; :: deftheorem defines :::"I_PFuncs"::: VALUED_2:def 16 : (Bool "for" (Set (Var "D")) "," (Set (Var "b2")) "being" ($#m1_hidden :::"set"::: ) "holds" (Bool "(" (Bool (Set (Var "b2")) ($#r1_hidden :::"="::: ) (Set ($#k10_valued_2 :::"I_PFuncs"::: ) (Set (Var "D")))) "iff" (Bool "for" (Set (Var "f")) "being" ($#m1_hidden :::"set"::: ) "holds" (Bool "(" (Bool (Set (Var "f")) ($#r2_hidden :::"in"::: ) (Set (Var "b2"))) "iff" (Bool (Set (Var "f")) "is" ($#m1_subset_1 :::"PartFunc":::) "of" (Set (Var "D")) "," (Set ($#k4_numbers :::"INT"::: ) )) ")" )) ")" )); definitionlet "D" be ($#m1_hidden :::"set"::: ) ; func :::"I_Funcs"::: "D" -> ($#m1_hidden :::"set"::: ) means :: VALUED_2:def 17 (Bool "for" (Set (Var "f")) "being" ($#m1_hidden :::"set"::: ) "holds" (Bool "(" (Bool (Set (Var "f")) ($#r2_hidden :::"in"::: ) it) "iff" (Bool (Set (Var "f")) "is" ($#m1_subset_1 :::"Function":::) "of" "D" "," (Set ($#k4_numbers :::"INT"::: ) )) ")" )); end; :: deftheorem defines :::"I_Funcs"::: VALUED_2:def 17 : (Bool "for" (Set (Var "D")) "," (Set (Var "b2")) "being" ($#m1_hidden :::"set"::: ) "holds" (Bool "(" (Bool (Set (Var "b2")) ($#r1_hidden :::"="::: ) (Set ($#k11_valued_2 :::"I_Funcs"::: ) (Set (Var "D")))) "iff" (Bool "for" (Set (Var "f")) "being" ($#m1_hidden :::"set"::: ) "holds" (Bool "(" (Bool (Set (Var "f")) ($#r2_hidden :::"in"::: ) (Set (Var "b2"))) "iff" (Bool (Set (Var "f")) "is" ($#m1_subset_1 :::"Function":::) "of" (Set (Var "D")) "," (Set ($#k4_numbers :::"INT"::: ) )) ")" )) ")" )); definitionlet "D" be ($#m1_hidden :::"set"::: ) ; func :::"N_PFuncs"::: "D" -> ($#m1_hidden :::"set"::: ) means :: VALUED_2:def 18 (Bool "for" (Set (Var "f")) "being" ($#m1_hidden :::"set"::: ) "holds" (Bool "(" (Bool (Set (Var "f")) ($#r2_hidden :::"in"::: ) it) "iff" (Bool (Set (Var "f")) "is" ($#m1_subset_1 :::"PartFunc":::) "of" "D" "," (Set ($#k5_numbers :::"NAT"::: ) )) ")" )); end; :: deftheorem defines :::"N_PFuncs"::: VALUED_2:def 18 : (Bool "for" (Set (Var "D")) "," (Set (Var "b2")) "being" ($#m1_hidden :::"set"::: ) "holds" (Bool "(" (Bool (Set (Var "b2")) ($#r1_hidden :::"="::: ) (Set ($#k12_valued_2 :::"N_PFuncs"::: ) (Set (Var "D")))) "iff" (Bool "for" (Set (Var "f")) "being" ($#m1_hidden :::"set"::: ) "holds" (Bool "(" (Bool (Set (Var "f")) ($#r2_hidden :::"in"::: ) (Set (Var "b2"))) "iff" (Bool (Set (Var "f")) "is" ($#m1_subset_1 :::"PartFunc":::) "of" (Set (Var "D")) "," (Set ($#k5_numbers :::"NAT"::: ) )) ")" )) ")" )); definitionlet "D" be ($#m1_hidden :::"set"::: ) ; func :::"N_Funcs"::: "D" -> ($#m1_hidden :::"set"::: ) means :: VALUED_2:def 19 (Bool "for" (Set (Var "f")) "being" ($#m1_hidden :::"set"::: ) "holds" (Bool "(" (Bool (Set (Var "f")) ($#r2_hidden :::"in"::: ) it) "iff" (Bool (Set (Var "f")) "is" ($#m1_subset_1 :::"Function":::) "of" "D" "," (Set ($#k5_numbers :::"NAT"::: ) )) ")" )); end; :: deftheorem defines :::"N_Funcs"::: VALUED_2:def 19 : (Bool "for" (Set (Var "D")) "," (Set (Var "b2")) "being" ($#m1_hidden :::"set"::: ) "holds" (Bool "(" (Bool (Set (Var "b2")) ($#r1_hidden :::"="::: ) (Set ($#k13_valued_2 :::"N_Funcs"::: ) (Set (Var "D")))) "iff" (Bool "for" (Set (Var "f")) "being" ($#m1_hidden :::"set"::: ) "holds" (Bool "(" (Bool (Set (Var "f")) ($#r2_hidden :::"in"::: ) (Set (Var "b2"))) "iff" (Bool (Set (Var "f")) "is" ($#m1_subset_1 :::"Function":::) "of" (Set (Var "D")) "," (Set ($#k5_numbers :::"NAT"::: ) )) ")" )) ")" )); theorem :: VALUED_2:1 (Bool "for" (Set (Var "X")) "being" ($#m1_hidden :::"set"::: ) "holds" (Bool (Set ($#k3_valued_2 :::"C_Funcs"::: ) (Set (Var "X"))) "is" ($#m1_subset_1 :::"Subset":::) "of" (Set "(" ($#k2_valued_2 :::"C_PFuncs"::: ) (Set (Var "X")) ")" ))) ; theorem :: VALUED_2:2 (Bool "for" (Set (Var "X")) "being" ($#m1_hidden :::"set"::: ) "holds" (Bool (Set ($#k5_valued_2 :::"E_Funcs"::: ) (Set (Var "X"))) "is" ($#m1_subset_1 :::"Subset":::) "of" (Set "(" ($#k4_valued_2 :::"E_PFuncs"::: ) (Set (Var "X")) ")" ))) ; theorem :: VALUED_2:3 (Bool "for" (Set (Var "X")) "being" ($#m1_hidden :::"set"::: ) "holds" (Bool (Set ($#k7_valued_2 :::"R_Funcs"::: ) (Set (Var "X"))) "is" ($#m1_subset_1 :::"Subset":::) "of" (Set "(" ($#k6_valued_2 :::"R_PFuncs"::: ) (Set (Var "X")) ")" ))) ; theorem :: VALUED_2:4 (Bool "for" (Set (Var "X")) "being" ($#m1_hidden :::"set"::: ) "holds" (Bool (Set ($#k9_valued_2 :::"Q_Funcs"::: ) (Set (Var "X"))) "is" ($#m1_subset_1 :::"Subset":::) "of" (Set "(" ($#k8_valued_2 :::"Q_PFuncs"::: ) (Set (Var "X")) ")" ))) ; theorem :: VALUED_2:5 (Bool "for" (Set (Var "X")) "being" ($#m1_hidden :::"set"::: ) "holds" (Bool (Set ($#k11_valued_2 :::"I_Funcs"::: ) (Set (Var "X"))) "is" ($#m1_subset_1 :::"Subset":::) "of" (Set "(" ($#k10_valued_2 :::"I_PFuncs"::: ) (Set (Var "X")) ")" ))) ; theorem :: VALUED_2:6 (Bool "for" (Set (Var "X")) "being" ($#m1_hidden :::"set"::: ) "holds" (Bool (Set ($#k13_valued_2 :::"N_Funcs"::: ) (Set (Var "X"))) "is" ($#m1_subset_1 :::"Subset":::) "of" (Set "(" ($#k12_valued_2 :::"N_PFuncs"::: ) (Set (Var "X")) ")" ))) ; registrationlet "X" be ($#m1_hidden :::"set"::: ) ; cluster (Set ($#k2_valued_2 :::"C_PFuncs"::: ) "X") -> ($#v1_valued_2 :::"complex-functions-membered"::: ) ; cluster (Set ($#k3_valued_2 :::"C_Funcs"::: ) "X") -> ($#v1_valued_2 :::"complex-functions-membered"::: ) ; cluster (Set ($#k4_valued_2 :::"E_PFuncs"::: ) "X") -> ($#v2_valued_2 :::"ext-real-functions-membered"::: ) ; cluster (Set ($#k5_valued_2 :::"E_Funcs"::: ) "X") -> ($#v2_valued_2 :::"ext-real-functions-membered"::: ) ; cluster (Set ($#k6_valued_2 :::"R_PFuncs"::: ) "X") -> ($#v3_valued_2 :::"real-functions-membered"::: ) ; cluster (Set ($#k7_valued_2 :::"R_Funcs"::: ) "X") -> ($#v3_valued_2 :::"real-functions-membered"::: ) ; cluster (Set ($#k8_valued_2 :::"Q_PFuncs"::: ) "X") -> ($#v4_valued_2 :::"rational-functions-membered"::: ) ; cluster (Set ($#k9_valued_2 :::"Q_Funcs"::: ) "X") -> ($#v4_valued_2 :::"rational-functions-membered"::: ) ; cluster (Set ($#k10_valued_2 :::"I_PFuncs"::: ) "X") -> ($#v5_valued_2 :::"integer-functions-membered"::: ) ; cluster (Set ($#k11_valued_2 :::"I_Funcs"::: ) "X") -> ($#v5_valued_2 :::"integer-functions-membered"::: ) ; cluster (Set ($#k12_valued_2 :::"N_PFuncs"::: ) "X") -> ($#v6_valued_2 :::"natural-functions-membered"::: ) ; cluster (Set ($#k13_valued_2 :::"N_Funcs"::: ) "X") -> ($#v6_valued_2 :::"natural-functions-membered"::: ) ; end; registrationlet "X" be ($#v1_valued_2 :::"complex-functions-membered"::: ) ($#m1_hidden :::"set"::: ) ; cluster -> ($#v1_valued_0 :::"complex-valued"::: ) for ($#m1_subset_1 :::"Element"::: ) "of" "X"; end; registrationlet "X" be ($#v2_valued_2 :::"ext-real-functions-membered"::: ) ($#m1_hidden :::"set"::: ) ; cluster -> ($#v2_valued_0 :::"ext-real-valued"::: ) for ($#m1_subset_1 :::"Element"::: ) "of" "X"; end; registrationlet "X" be ($#v3_valued_2 :::"real-functions-membered"::: ) ($#m1_hidden :::"set"::: ) ; cluster -> ($#v3_valued_0 :::"real-valued"::: ) for ($#m1_subset_1 :::"Element"::: ) "of" "X"; end; registrationlet "X" be ($#v4_valued_2 :::"rational-functions-membered"::: ) ($#m1_hidden :::"set"::: ) ; cluster -> (Set ($#k3_numbers :::"RAT"::: ) ) ($#v5_relat_1 :::"-valued"::: ) for ($#m1_subset_1 :::"Element"::: ) "of" "X"; end; registrationlet "X" be ($#v5_valued_2 :::"integer-functions-membered"::: ) ($#m1_hidden :::"set"::: ) ; cluster -> (Set ($#k4_numbers :::"INT"::: ) ) ($#v5_relat_1 :::"-valued"::: ) for ($#m1_subset_1 :::"Element"::: ) "of" "X"; end; registrationlet "X" be ($#v6_valued_2 :::"natural-functions-membered"::: ) ($#m1_hidden :::"set"::: ) ; cluster -> ($#v4_valued_0 :::"natural-valued"::: ) for ($#m1_subset_1 :::"Element"::: ) "of" "X"; end; registrationlet "X", "x" be ($#m1_hidden :::"set"::: ) ; let "Y" be ($#v1_valued_2 :::"complex-functions-membered"::: ) ($#m1_hidden :::"set"::: ) ; let "f" be ($#m1_subset_1 :::"PartFunc":::) "of" (Set (Const "X")) "," (Set (Const "Y")); cluster (Set "f" ($#k1_funct_1 :::"."::: ) "x") -> ($#v1_relat_1 :::"Relation-like"::: ) ($#v1_funct_1 :::"Function-like"::: ) ; end; registrationlet "X", "x" be ($#m1_hidden :::"set"::: ) ; let "Y" be ($#v2_valued_2 :::"ext-real-functions-membered"::: ) ($#m1_hidden :::"set"::: ) ; let "f" be ($#m1_subset_1 :::"PartFunc":::) "of" (Set (Const "X")) "," (Set (Const "Y")); cluster (Set "f" ($#k1_funct_1 :::"."::: ) "x") -> ($#v1_relat_1 :::"Relation-like"::: ) ($#v1_funct_1 :::"Function-like"::: ) ; end; registrationlet "X", "x" be ($#m1_hidden :::"set"::: ) ; let "Y" be ($#v1_valued_2 :::"complex-functions-membered"::: ) ($#m1_hidden :::"set"::: ) ; let "f" be ($#m1_subset_1 :::"PartFunc":::) "of" (Set (Const "X")) "," (Set (Const "Y")); cluster (Set "f" ($#k1_funct_1 :::"."::: ) "x") -> ($#v1_valued_0 :::"complex-valued"::: ) ; end; registrationlet "X", "x" be ($#m1_hidden :::"set"::: ) ; let "Y" be ($#v2_valued_2 :::"ext-real-functions-membered"::: ) ($#m1_hidden :::"set"::: ) ; let "f" be ($#m1_subset_1 :::"PartFunc":::) "of" (Set (Const "X")) "," (Set (Const "Y")); cluster (Set "f" ($#k1_funct_1 :::"."::: ) "x") -> ($#v2_valued_0 :::"ext-real-valued"::: ) ; end; registrationlet "X", "x" be ($#m1_hidden :::"set"::: ) ; let "Y" be ($#v3_valued_2 :::"real-functions-membered"::: ) ($#m1_hidden :::"set"::: ) ; let "f" be ($#m1_subset_1 :::"PartFunc":::) "of" (Set (Const "X")) "," (Set (Const "Y")); cluster (Set "f" ($#k1_funct_1 :::"."::: ) "x") -> ($#v3_valued_0 :::"real-valued"::: ) ; end; registrationlet "X", "x" be ($#m1_hidden :::"set"::: ) ; let "Y" be ($#v4_valued_2 :::"rational-functions-membered"::: ) ($#m1_hidden :::"set"::: ) ; let "f" be ($#m1_subset_1 :::"PartFunc":::) "of" (Set (Const "X")) "," (Set (Const "Y")); cluster (Set "f" ($#k1_funct_1 :::"."::: ) "x") -> (Set ($#k3_numbers :::"RAT"::: ) ) ($#v5_relat_1 :::"-valued"::: ) ; end; registrationlet "X", "x" be ($#m1_hidden :::"set"::: ) ; let "Y" be ($#v5_valued_2 :::"integer-functions-membered"::: ) ($#m1_hidden :::"set"::: ) ; let "f" be ($#m1_subset_1 :::"PartFunc":::) "of" (Set (Const "X")) "," (Set (Const "Y")); cluster (Set "f" ($#k1_funct_1 :::"."::: ) "x") -> (Set ($#k4_numbers :::"INT"::: ) ) ($#v5_relat_1 :::"-valued"::: ) ; end; registrationlet "X", "x" be ($#m1_hidden :::"set"::: ) ; let "Y" be ($#v6_valued_2 :::"natural-functions-membered"::: ) ($#m1_hidden :::"set"::: ) ; let "f" be ($#m1_subset_1 :::"PartFunc":::) "of" (Set (Const "X")) "," (Set (Const "Y")); cluster (Set "f" ($#k1_funct_1 :::"."::: ) "x") -> ($#v4_valued_0 :::"natural-valued"::: ) ; end; registrationlet "X" be ($#m1_hidden :::"set"::: ) ; let "Y" be ($#v1_membered :::"complex-membered"::: ) ($#m1_hidden :::"set"::: ) ; cluster (Set ($#k4_partfun1 :::"PFuncs"::: ) "(" "X" "," "Y" ")" ) -> ($#v1_valued_2 :::"complex-functions-membered"::: ) ; end; registrationlet "X" be ($#m1_hidden :::"set"::: ) ; let "Y" be ($#v2_membered :::"ext-real-membered"::: ) ($#m1_hidden :::"set"::: ) ; cluster (Set ($#k4_partfun1 :::"PFuncs"::: ) "(" "X" "," "Y" ")" ) -> ($#v2_valued_2 :::"ext-real-functions-membered"::: ) ; end; registrationlet "X" be ($#m1_hidden :::"set"::: ) ; let "Y" be ($#v3_membered :::"real-membered"::: ) ($#m1_hidden :::"set"::: ) ; cluster (Set ($#k4_partfun1 :::"PFuncs"::: ) "(" "X" "," "Y" ")" ) -> ($#v3_valued_2 :::"real-functions-membered"::: ) ; end; registrationlet "X" be ($#m1_hidden :::"set"::: ) ; let "Y" be ($#v4_membered :::"rational-membered"::: ) ($#m1_hidden :::"set"::: ) ; cluster (Set ($#k4_partfun1 :::"PFuncs"::: ) "(" "X" "," "Y" ")" ) -> ($#v4_valued_2 :::"rational-functions-membered"::: ) ; end; registrationlet "X" be ($#m1_hidden :::"set"::: ) ; let "Y" be ($#v5_membered :::"integer-membered"::: ) ($#m1_hidden :::"set"::: ) ; cluster (Set ($#k4_partfun1 :::"PFuncs"::: ) "(" "X" "," "Y" ")" ) -> ($#v5_valued_2 :::"integer-functions-membered"::: ) ; end; registrationlet "X" be ($#m1_hidden :::"set"::: ) ; let "Y" be ($#v6_membered :::"natural-membered"::: ) ($#m1_hidden :::"set"::: ) ; cluster (Set ($#k4_partfun1 :::"PFuncs"::: ) "(" "X" "," "Y" ")" ) -> ($#v6_valued_2 :::"natural-functions-membered"::: ) ; end; registrationlet "X" be ($#m1_hidden :::"set"::: ) ; let "Y" be ($#v1_membered :::"complex-membered"::: ) ($#m1_hidden :::"set"::: ) ; cluster (Set ($#k1_funct_2 :::"Funcs"::: ) "(" "X" "," "Y" ")" ) -> ($#v1_valued_2 :::"complex-functions-membered"::: ) ; end; registrationlet "X" be ($#m1_hidden :::"set"::: ) ; let "Y" be ($#v2_membered :::"ext-real-membered"::: ) ($#m1_hidden :::"set"::: ) ; cluster (Set ($#k1_funct_2 :::"Funcs"::: ) "(" "X" "," "Y" ")" ) -> ($#v2_valued_2 :::"ext-real-functions-membered"::: ) ; end; registrationlet "X" be ($#m1_hidden :::"set"::: ) ; let "Y" be ($#v3_membered :::"real-membered"::: ) ($#m1_hidden :::"set"::: ) ; cluster (Set ($#k1_funct_2 :::"Funcs"::: ) "(" "X" "," "Y" ")" ) -> ($#v3_valued_2 :::"real-functions-membered"::: ) ; end; registrationlet "X" be ($#m1_hidden :::"set"::: ) ; let "Y" be ($#v4_membered :::"rational-membered"::: ) ($#m1_hidden :::"set"::: ) ; cluster (Set ($#k1_funct_2 :::"Funcs"::: ) "(" "X" "," "Y" ")" ) -> ($#v4_valued_2 :::"rational-functions-membered"::: ) ; end; registrationlet "X" be ($#m1_hidden :::"set"::: ) ; let "Y" be ($#v5_membered :::"integer-membered"::: ) ($#m1_hidden :::"set"::: ) ; cluster (Set ($#k1_funct_2 :::"Funcs"::: ) "(" "X" "," "Y" ")" ) -> ($#v5_valued_2 :::"integer-functions-membered"::: ) ; end; registrationlet "X" be ($#m1_hidden :::"set"::: ) ; let "Y" be ($#v6_membered :::"natural-membered"::: ) ($#m1_hidden :::"set"::: ) ; cluster (Set ($#k1_funct_2 :::"Funcs"::: ) "(" "X" "," "Y" ")" ) -> ($#v6_valued_2 :::"natural-functions-membered"::: ) ; end; definitionlet "R" be ($#m1_hidden :::"Relation":::); attr "R" is :::"complex-functions-valued"::: means :: VALUED_2:def 20 (Bool (Set ($#k10_xtuple_0 :::"rng"::: ) "R") "is" ($#v1_valued_2 :::"complex-functions-membered"::: ) ); attr "R" is :::"ext-real-functions-valued"::: means :: VALUED_2:def 21 (Bool (Set ($#k10_xtuple_0 :::"rng"::: ) "R") "is" ($#v2_valued_2 :::"ext-real-functions-membered"::: ) ); attr "R" is :::"real-functions-valued"::: means :: VALUED_2:def 22 (Bool (Set ($#k10_xtuple_0 :::"rng"::: ) "R") "is" ($#v3_valued_2 :::"real-functions-membered"::: ) ); attr "R" is :::"rational-functions-valued"::: means :: VALUED_2:def 23 (Bool (Set ($#k10_xtuple_0 :::"rng"::: ) "R") "is" ($#v4_valued_2 :::"rational-functions-membered"::: ) ); attr "R" is :::"integer-functions-valued"::: means :: VALUED_2:def 24 (Bool (Set ($#k10_xtuple_0 :::"rng"::: ) "R") "is" ($#v5_valued_2 :::"integer-functions-membered"::: ) ); attr "R" is :::"natural-functions-valued"::: means :: VALUED_2:def 25 (Bool (Set ($#k10_xtuple_0 :::"rng"::: ) "R") "is" ($#v6_valued_2 :::"natural-functions-membered"::: ) ); end; :: deftheorem defines :::"complex-functions-valued"::: VALUED_2:def 20 : (Bool "for" (Set (Var "R")) "being" ($#m1_hidden :::"Relation":::) "holds" (Bool "(" (Bool (Set (Var "R")) "is" ($#v7_valued_2 :::"complex-functions-valued"::: ) ) "iff" (Bool (Set ($#k10_xtuple_0 :::"rng"::: ) (Set (Var "R"))) "is" ($#v1_valued_2 :::"complex-functions-membered"::: ) ) ")" )); :: deftheorem defines :::"ext-real-functions-valued"::: VALUED_2:def 21 : (Bool "for" (Set (Var "R")) "being" ($#m1_hidden :::"Relation":::) "holds" (Bool "(" (Bool (Set (Var "R")) "is" ($#v8_valued_2 :::"ext-real-functions-valued"::: ) ) "iff" (Bool (Set ($#k10_xtuple_0 :::"rng"::: ) (Set (Var "R"))) "is" ($#v2_valued_2 :::"ext-real-functions-membered"::: ) ) ")" )); :: deftheorem defines :::"real-functions-valued"::: VALUED_2:def 22 : (Bool "for" (Set (Var "R")) "being" ($#m1_hidden :::"Relation":::) "holds" (Bool "(" (Bool (Set (Var "R")) "is" ($#v9_valued_2 :::"real-functions-valued"::: ) ) "iff" (Bool (Set ($#k10_xtuple_0 :::"rng"::: ) (Set (Var "R"))) "is" ($#v3_valued_2 :::"real-functions-membered"::: ) ) ")" )); :: deftheorem defines :::"rational-functions-valued"::: VALUED_2:def 23 : (Bool "for" (Set (Var "R")) "being" ($#m1_hidden :::"Relation":::) "holds" (Bool "(" (Bool (Set (Var "R")) "is" ($#v10_valued_2 :::"rational-functions-valued"::: ) ) "iff" (Bool (Set ($#k10_xtuple_0 :::"rng"::: ) (Set (Var "R"))) "is" ($#v4_valued_2 :::"rational-functions-membered"::: ) ) ")" )); :: deftheorem defines :::"integer-functions-valued"::: VALUED_2:def 24 : (Bool "for" (Set (Var "R")) "being" ($#m1_hidden :::"Relation":::) "holds" (Bool "(" (Bool (Set (Var "R")) "is" ($#v11_valued_2 :::"integer-functions-valued"::: ) ) "iff" (Bool (Set ($#k10_xtuple_0 :::"rng"::: ) (Set (Var "R"))) "is" ($#v5_valued_2 :::"integer-functions-membered"::: ) ) ")" )); :: deftheorem defines :::"natural-functions-valued"::: VALUED_2:def 25 : (Bool "for" (Set (Var "R")) "being" ($#m1_hidden :::"Relation":::) "holds" (Bool "(" (Bool (Set (Var "R")) "is" ($#v12_valued_2 :::"natural-functions-valued"::: ) ) "iff" (Bool (Set ($#k10_xtuple_0 :::"rng"::: ) (Set (Var "R"))) "is" ($#v6_valued_2 :::"natural-functions-membered"::: ) ) ")" )); registrationlet "Y" be ($#v1_valued_2 :::"complex-functions-membered"::: ) ($#m1_hidden :::"set"::: ) ; cluster ($#v1_relat_1 :::"Relation-like"::: ) "Y" ($#v5_relat_1 :::"-valued"::: ) ($#v1_funct_1 :::"Function-like"::: ) -> "Y" ($#v5_relat_1 :::"-valued"::: ) ($#v7_valued_2 :::"complex-functions-valued"::: ) for ($#m1_hidden :::"set"::: ) ; end; definitionlet "f" be ($#m1_hidden :::"Function":::); redefine attr "f" is :::"complex-functions-valued"::: means :: VALUED_2:def 26 (Bool "for" (Set (Var "x")) "being" ($#m1_hidden :::"set"::: ) "st" (Bool (Bool (Set (Var "x")) ($#r2_hidden :::"in"::: ) (Set ($#k9_xtuple_0 :::"dom"::: ) "f"))) "holds" (Bool (Set "f" ($#k1_funct_1 :::"."::: ) (Set (Var "x"))) "is" ($#v1_valued_0 :::"complex-valued"::: ) ($#m1_hidden :::"Function":::))); redefine attr "f" is :::"ext-real-functions-valued"::: means :: VALUED_2:def 27 (Bool "for" (Set (Var "x")) "being" ($#m1_hidden :::"set"::: ) "st" (Bool (Bool (Set (Var "x")) ($#r2_hidden :::"in"::: ) (Set ($#k9_xtuple_0 :::"dom"::: ) "f"))) "holds" (Bool (Set "f" ($#k1_funct_1 :::"."::: ) (Set (Var "x"))) "is" ($#v2_valued_0 :::"ext-real-valued"::: ) ($#m1_hidden :::"Function":::))); redefine attr "f" is :::"real-functions-valued"::: means :: VALUED_2:def 28 (Bool "for" (Set (Var "x")) "being" ($#m1_hidden :::"set"::: ) "st" (Bool (Bool (Set (Var "x")) ($#r2_hidden :::"in"::: ) (Set ($#k9_xtuple_0 :::"dom"::: ) "f"))) "holds" (Bool (Set "f" ($#k1_funct_1 :::"."::: ) (Set (Var "x"))) "is" ($#v3_valued_0 :::"real-valued"::: ) ($#m1_hidden :::"Function":::))); redefine attr "f" is :::"rational-functions-valued"::: means :: VALUED_2:def 29 (Bool "for" (Set (Var "x")) "being" ($#m1_hidden :::"set"::: ) "st" (Bool (Bool (Set (Var "x")) ($#r2_hidden :::"in"::: ) (Set ($#k9_xtuple_0 :::"dom"::: ) "f"))) "holds" (Bool (Set "f" ($#k1_funct_1 :::"."::: ) (Set (Var "x"))) "is" (Set ($#k3_numbers :::"RAT"::: ) ) ($#v5_relat_1 :::"-valued"::: ) ($#m1_hidden :::"Function":::))); redefine attr "f" is :::"integer-functions-valued"::: means :: VALUED_2:def 30 (Bool "for" (Set (Var "x")) "being" ($#m1_hidden :::"set"::: ) "st" (Bool (Bool (Set (Var "x")) ($#r2_hidden :::"in"::: ) (Set ($#k9_xtuple_0 :::"dom"::: ) "f"))) "holds" (Bool (Set "f" ($#k1_funct_1 :::"."::: ) (Set (Var "x"))) "is" (Set ($#k4_numbers :::"INT"::: ) ) ($#v5_relat_1 :::"-valued"::: ) ($#m1_hidden :::"Function":::))); redefine attr "f" is :::"natural-functions-valued"::: means :: VALUED_2:def 31 (Bool "for" (Set (Var "x")) "being" ($#m1_hidden :::"set"::: ) "st" (Bool (Bool (Set (Var "x")) ($#r2_hidden :::"in"::: ) (Set ($#k9_xtuple_0 :::"dom"::: ) "f"))) "holds" (Bool (Set "f" ($#k1_funct_1 :::"."::: ) (Set (Var "x"))) "is" ($#v4_valued_0 :::"natural-valued"::: ) ($#m1_hidden :::"Function":::))); end; :: deftheorem defines :::"complex-functions-valued"::: VALUED_2:def 26 : (Bool "for" (Set (Var "f")) "being" ($#m1_hidden :::"Function":::) "holds" (Bool "(" (Bool (Set (Var "f")) "is" ($#v7_valued_2 :::"complex-functions-valued"::: ) ) "iff" (Bool "for" (Set (Var "x")) "being" ($#m1_hidden :::"set"::: ) "st" (Bool (Bool (Set (Var "x")) ($#r2_hidden :::"in"::: ) (Set ($#k9_xtuple_0 :::"dom"::: ) (Set (Var "f"))))) "holds" (Bool (Set (Set (Var "f")) ($#k1_funct_1 :::"."::: ) (Set (Var "x"))) "is" ($#v1_valued_0 :::"complex-valued"::: ) ($#m1_hidden :::"Function":::))) ")" )); :: deftheorem defines :::"ext-real-functions-valued"::: VALUED_2:def 27 : (Bool "for" (Set (Var "f")) "being" ($#m1_hidden :::"Function":::) "holds" (Bool "(" (Bool (Set (Var "f")) "is" ($#v8_valued_2 :::"ext-real-functions-valued"::: ) ) "iff" (Bool "for" (Set (Var "x")) "being" ($#m1_hidden :::"set"::: ) "st" (Bool (Bool (Set (Var "x")) ($#r2_hidden :::"in"::: ) (Set ($#k9_xtuple_0 :::"dom"::: ) (Set (Var "f"))))) "holds" (Bool (Set (Set (Var "f")) ($#k1_funct_1 :::"."::: ) (Set (Var "x"))) "is" ($#v2_valued_0 :::"ext-real-valued"::: ) ($#m1_hidden :::"Function":::))) ")" )); :: deftheorem defines :::"real-functions-valued"::: VALUED_2:def 28 : (Bool "for" (Set (Var "f")) "being" ($#m1_hidden :::"Function":::) "holds" (Bool "(" (Bool (Set (Var "f")) "is" ($#v9_valued_2 :::"real-functions-valued"::: ) ) "iff" (Bool "for" (Set (Var "x")) "being" ($#m1_hidden :::"set"::: ) "st" (Bool (Bool (Set (Var "x")) ($#r2_hidden :::"in"::: ) (Set ($#k9_xtuple_0 :::"dom"::: ) (Set (Var "f"))))) "holds" (Bool (Set (Set (Var "f")) ($#k1_funct_1 :::"."::: ) (Set (Var "x"))) "is" ($#v3_valued_0 :::"real-valued"::: ) ($#m1_hidden :::"Function":::))) ")" )); :: deftheorem defines :::"rational-functions-valued"::: VALUED_2:def 29 : (Bool "for" (Set (Var "f")) "being" ($#m1_hidden :::"Function":::) "holds" (Bool "(" (Bool (Set (Var "f")) "is" ($#v10_valued_2 :::"rational-functions-valued"::: ) ) "iff" (Bool "for" (Set (Var "x")) "being" ($#m1_hidden :::"set"::: ) "st" (Bool (Bool (Set (Var "x")) ($#r2_hidden :::"in"::: ) (Set ($#k9_xtuple_0 :::"dom"::: ) (Set (Var "f"))))) "holds" (Bool (Set (Set (Var "f")) ($#k1_funct_1 :::"."::: ) (Set (Var "x"))) "is" (Set ($#k3_numbers :::"RAT"::: ) ) ($#v5_relat_1 :::"-valued"::: ) ($#m1_hidden :::"Function":::))) ")" )); :: deftheorem defines :::"integer-functions-valued"::: VALUED_2:def 30 : (Bool "for" (Set (Var "f")) "being" ($#m1_hidden :::"Function":::) "holds" (Bool "(" (Bool (Set (Var "f")) "is" ($#v11_valued_2 :::"integer-functions-valued"::: ) ) "iff" (Bool "for" (Set (Var "x")) "being" ($#m1_hidden :::"set"::: ) "st" (Bool (Bool (Set (Var "x")) ($#r2_hidden :::"in"::: ) (Set ($#k9_xtuple_0 :::"dom"::: ) (Set (Var "f"))))) "holds" (Bool (Set (Set (Var "f")) ($#k1_funct_1 :::"."::: ) (Set (Var "x"))) "is" (Set ($#k4_numbers :::"INT"::: ) ) ($#v5_relat_1 :::"-valued"::: ) ($#m1_hidden :::"Function":::))) ")" )); :: deftheorem defines :::"natural-functions-valued"::: VALUED_2:def 31 : (Bool "for" (Set (Var "f")) "being" ($#m1_hidden :::"Function":::) "holds" (Bool "(" (Bool (Set (Var "f")) "is" ($#v12_valued_2 :::"natural-functions-valued"::: ) ) "iff" (Bool "for" (Set (Var "x")) "being" ($#m1_hidden :::"set"::: ) "st" (Bool (Bool (Set (Var "x")) ($#r2_hidden :::"in"::: ) (Set ($#k9_xtuple_0 :::"dom"::: ) (Set (Var "f"))))) "holds" (Bool (Set (Set (Var "f")) ($#k1_funct_1 :::"."::: ) (Set (Var "x"))) "is" ($#v4_valued_0 :::"natural-valued"::: ) ($#m1_hidden :::"Function":::))) ")" )); registration cluster ($#v1_relat_1 :::"Relation-like"::: ) ($#v12_valued_2 :::"natural-functions-valued"::: ) -> ($#v11_valued_2 :::"integer-functions-valued"::: ) for ($#m1_hidden :::"set"::: ) ; cluster ($#v1_relat_1 :::"Relation-like"::: ) ($#v11_valued_2 :::"integer-functions-valued"::: ) -> ($#v10_valued_2 :::"rational-functions-valued"::: ) for ($#m1_hidden :::"set"::: ) ; cluster ($#v1_relat_1 :::"Relation-like"::: ) ($#v10_valued_2 :::"rational-functions-valued"::: ) -> ($#v9_valued_2 :::"real-functions-valued"::: ) for ($#m1_hidden :::"set"::: ) ; cluster ($#v1_relat_1 :::"Relation-like"::: ) ($#v9_valued_2 :::"real-functions-valued"::: ) -> ($#v8_valued_2 :::"ext-real-functions-valued"::: ) for ($#m1_hidden :::"set"::: ) ; cluster ($#v1_relat_1 :::"Relation-like"::: ) ($#v9_valued_2 :::"real-functions-valued"::: ) -> ($#v7_valued_2 :::"complex-functions-valued"::: ) for ($#m1_hidden :::"set"::: ) ; end; registration cluster ($#v1_relat_1 :::"Relation-like"::: ) ($#v1_xboole_0 :::"empty"::: ) -> ($#v12_valued_2 :::"natural-functions-valued"::: ) for ($#m1_hidden :::"set"::: ) ; end; registration cluster ($#v1_relat_1 :::"Relation-like"::: ) ($#v1_funct_1 :::"Function-like"::: ) ($#v12_valued_2 :::"natural-functions-valued"::: ) for ($#m1_hidden :::"set"::: ) ; end; registrationlet "R" be ($#v7_valued_2 :::"complex-functions-valued"::: ) ($#m1_hidden :::"Relation":::); cluster (Set ($#k10_xtuple_0 :::"rng"::: ) "R") -> ($#v1_valued_2 :::"complex-functions-membered"::: ) ; end; registrationlet "R" be ($#v8_valued_2 :::"ext-real-functions-valued"::: ) ($#m1_hidden :::"Relation":::); cluster (Set ($#k10_xtuple_0 :::"rng"::: ) "R") -> ($#v2_valued_2 :::"ext-real-functions-membered"::: ) ; end; registrationlet "R" be ($#v9_valued_2 :::"real-functions-valued"::: ) ($#m1_hidden :::"Relation":::); cluster (Set ($#k10_xtuple_0 :::"rng"::: ) "R") -> ($#v3_valued_2 :::"real-functions-membered"::: ) ; end; registrationlet "R" be ($#v10_valued_2 :::"rational-functions-valued"::: ) ($#m1_hidden :::"Relation":::); cluster (Set ($#k10_xtuple_0 :::"rng"::: ) "R") -> ($#v4_valued_2 :::"rational-functions-membered"::: ) ; end; registrationlet "R" be ($#v11_valued_2 :::"integer-functions-valued"::: ) ($#m1_hidden :::"Relation":::); cluster (Set ($#k10_xtuple_0 :::"rng"::: ) "R") -> ($#v5_valued_2 :::"integer-functions-membered"::: ) ; end; registrationlet "R" be ($#v12_valued_2 :::"natural-functions-valued"::: ) ($#m1_hidden :::"Relation":::); cluster (Set ($#k10_xtuple_0 :::"rng"::: ) "R") -> ($#v6_valued_2 :::"natural-functions-membered"::: ) ; end; registrationlet "X" be ($#m1_hidden :::"set"::: ) ; let "Y" be ($#v1_valued_2 :::"complex-functions-membered"::: ) ($#m1_hidden :::"set"::: ) ; cluster ($#v1_funct_1 :::"Function-like"::: ) -> ($#v7_valued_2 :::"complex-functions-valued"::: ) for ($#m1_subset_1 :::"Element"::: ) "of" (Set bbbadK1_ZFMISC_1((Set bbbadK2_ZFMISC_1("X" "," "Y")))); end; registrationlet "X" be ($#m1_hidden :::"set"::: ) ; let "Y" be ($#v2_valued_2 :::"ext-real-functions-membered"::: ) ($#m1_hidden :::"set"::: ) ; cluster ($#v1_funct_1 :::"Function-like"::: ) -> ($#v8_valued_2 :::"ext-real-functions-valued"::: ) for ($#m1_subset_1 :::"Element"::: ) "of" (Set bbbadK1_ZFMISC_1((Set bbbadK2_ZFMISC_1("X" "," "Y")))); end; registrationlet "X" be ($#m1_hidden :::"set"::: ) ; let "Y" be ($#v3_valued_2 :::"real-functions-membered"::: ) ($#m1_hidden :::"set"::: ) ; cluster ($#v1_funct_1 :::"Function-like"::: ) -> ($#v9_valued_2 :::"real-functions-valued"::: ) for ($#m1_subset_1 :::"Element"::: ) "of" (Set bbbadK1_ZFMISC_1((Set bbbadK2_ZFMISC_1("X" "," "Y")))); end; registrationlet "X" be ($#m1_hidden :::"set"::: ) ; let "Y" be ($#v4_valued_2 :::"rational-functions-membered"::: ) ($#m1_hidden :::"set"::: ) ; cluster ($#v1_funct_1 :::"Function-like"::: ) -> ($#v10_valued_2 :::"rational-functions-valued"::: ) for ($#m1_subset_1 :::"Element"::: ) "of" (Set bbbadK1_ZFMISC_1((Set bbbadK2_ZFMISC_1("X" "," "Y")))); end; registrationlet "X" be ($#m1_hidden :::"set"::: ) ; let "Y" be ($#v5_valued_2 :::"integer-functions-membered"::: ) ($#m1_hidden :::"set"::: ) ; cluster ($#v1_funct_1 :::"Function-like"::: ) -> ($#v11_valued_2 :::"integer-functions-valued"::: ) for ($#m1_subset_1 :::"Element"::: ) "of" (Set bbbadK1_ZFMISC_1((Set bbbadK2_ZFMISC_1("X" "," "Y")))); end; registrationlet "X" be ($#m1_hidden :::"set"::: ) ; let "Y" be ($#v6_valued_2 :::"natural-functions-membered"::: ) ($#m1_hidden :::"set"::: ) ; cluster ($#v1_funct_1 :::"Function-like"::: ) -> ($#v12_valued_2 :::"natural-functions-valued"::: ) for ($#m1_subset_1 :::"Element"::: ) "of" (Set bbbadK1_ZFMISC_1((Set bbbadK2_ZFMISC_1("X" "," "Y")))); end; registrationlet "f" be ($#v7_valued_2 :::"complex-functions-valued"::: ) ($#m1_hidden :::"Function":::); let "x" be ($#m1_hidden :::"set"::: ) ; cluster (Set "f" ($#k1_funct_1 :::"."::: ) "x") -> ($#v1_relat_1 :::"Relation-like"::: ) ($#v1_funct_1 :::"Function-like"::: ) ; end; registrationlet "f" be ($#v8_valued_2 :::"ext-real-functions-valued"::: ) ($#m1_hidden :::"Function":::); let "x" be ($#m1_hidden :::"set"::: ) ; cluster (Set "f" ($#k1_funct_1 :::"."::: ) "x") -> ($#v1_relat_1 :::"Relation-like"::: ) ($#v1_funct_1 :::"Function-like"::: ) ; end; registrationlet "f" be ($#v7_valued_2 :::"complex-functions-valued"::: ) ($#m1_hidden :::"Function":::); let "x" be ($#m1_hidden :::"set"::: ) ; cluster (Set "f" ($#k1_funct_1 :::"."::: ) "x") -> ($#v1_valued_0 :::"complex-valued"::: ) ; end; registrationlet "f" be ($#v8_valued_2 :::"ext-real-functions-valued"::: ) ($#m1_hidden :::"Function":::); let "x" be ($#m1_hidden :::"set"::: ) ; cluster (Set "f" ($#k1_funct_1 :::"."::: ) "x") -> ($#v2_valued_0 :::"ext-real-valued"::: ) ; end; registrationlet "f" be ($#v9_valued_2 :::"real-functions-valued"::: ) ($#m1_hidden :::"Function":::); let "x" be ($#m1_hidden :::"set"::: ) ; cluster (Set "f" ($#k1_funct_1 :::"."::: ) "x") -> ($#v3_valued_0 :::"real-valued"::: ) ; end; registrationlet "f" be ($#v10_valued_2 :::"rational-functions-valued"::: ) ($#m1_hidden :::"Function":::); let "x" be ($#m1_hidden :::"set"::: ) ; cluster (Set "f" ($#k1_funct_1 :::"."::: ) "x") -> (Set ($#k3_numbers :::"RAT"::: ) ) ($#v5_relat_1 :::"-valued"::: ) ; end; registrationlet "f" be ($#v11_valued_2 :::"integer-functions-valued"::: ) ($#m1_hidden :::"Function":::); let "x" be ($#m1_hidden :::"set"::: ) ; cluster (Set "f" ($#k1_funct_1 :::"."::: ) "x") -> (Set ($#k4_numbers :::"INT"::: ) ) ($#v5_relat_1 :::"-valued"::: ) ; end; registrationlet "f" be ($#v12_valued_2 :::"natural-functions-valued"::: ) ($#m1_hidden :::"Function":::); let "x" be ($#m1_hidden :::"set"::: ) ; cluster (Set "f" ($#k1_funct_1 :::"."::: ) "x") -> ($#v4_valued_0 :::"natural-valued"::: ) ; end; begin theorem :: VALUED_2:7 (Bool "for" (Set (Var "c1")) "," (Set (Var "c2")) "being" ($#v1_xcmplx_0 :::"complex"::: ) ($#m1_hidden :::"number"::: ) (Bool "for" (Set (Var "g")) "being" ($#v1_valued_0 :::"complex-valued"::: ) ($#m1_hidden :::"Function":::) "st" (Bool (Bool (Set (Var "g")) ($#r1_hidden :::"<>"::: ) (Set ($#k1_xboole_0 :::"{}"::: ) )) & (Bool (Set (Set (Var "g")) ($#k7_valued_1 :::"+"::: ) (Set (Var "c1"))) ($#r1_hidden :::"="::: ) (Set (Set (Var "g")) ($#k7_valued_1 :::"+"::: ) (Set (Var "c2"))))) "holds" (Bool (Set (Var "c1")) ($#r1_hidden :::"="::: ) (Set (Var "c2"))))) ; theorem :: VALUED_2:8 (Bool "for" (Set (Var "c1")) "," (Set (Var "c2")) "being" ($#v1_xcmplx_0 :::"complex"::: ) ($#m1_hidden :::"number"::: ) (Bool "for" (Set (Var "g")) "being" ($#v1_valued_0 :::"complex-valued"::: ) ($#m1_hidden :::"Function":::) "st" (Bool (Bool (Set (Var "g")) ($#r1_hidden :::"<>"::: ) (Set ($#k1_xboole_0 :::"{}"::: ) )) & (Bool (Set (Set (Var "g")) ($#k13_valued_1 :::"-"::: ) (Set (Var "c1"))) ($#r1_hidden :::"="::: ) (Set (Set (Var "g")) ($#k13_valued_1 :::"-"::: ) (Set (Var "c2"))))) "holds" (Bool (Set (Var "c1")) ($#r1_hidden :::"="::: ) (Set (Var "c2"))))) ; theorem :: VALUED_2:9 (Bool "for" (Set (Var "c1")) "," (Set (Var "c2")) "being" ($#v1_xcmplx_0 :::"complex"::: ) ($#m1_hidden :::"number"::: ) (Bool "for" (Set (Var "g")) "being" ($#v1_valued_0 :::"complex-valued"::: ) ($#m1_hidden :::"Function":::) "st" (Bool (Bool (Set (Var "g")) ($#r1_hidden :::"<>"::: ) (Set ($#k1_xboole_0 :::"{}"::: ) )) & (Bool (Set (Var "g")) "is" ($#v2_relat_1 :::"non-empty"::: ) ) & (Bool (Set (Set (Var "g")) ($#k24_valued_1 :::"(#)"::: ) (Set (Var "c1"))) ($#r1_hidden :::"="::: ) (Set (Set (Var "g")) ($#k24_valued_1 :::"(#)"::: ) (Set (Var "c2"))))) "holds" (Bool (Set (Var "c1")) ($#r1_hidden :::"="::: ) (Set (Var "c2"))))) ; theorem :: VALUED_2:10 (Bool "for" (Set (Var "c")) "being" ($#v1_xcmplx_0 :::"complex"::: ) ($#m1_hidden :::"number"::: ) (Bool "for" (Set (Var "g")) "being" ($#v1_valued_0 :::"complex-valued"::: ) ($#m1_hidden :::"Function":::) "holds" (Bool (Set ($#k30_valued_1 :::"-"::: ) (Set "(" (Set (Var "g")) ($#k7_valued_1 :::"+"::: ) (Set (Var "c")) ")" )) ($#r1_hidden :::"="::: ) (Set (Set "(" ($#k30_valued_1 :::"-"::: ) (Set (Var "g")) ")" ) ($#k13_valued_1 :::"-"::: ) (Set (Var "c")))))) ; theorem :: VALUED_2:11 (Bool "for" (Set (Var "c")) "being" ($#v1_xcmplx_0 :::"complex"::: ) ($#m1_hidden :::"number"::: ) (Bool "for" (Set (Var "g")) "being" ($#v1_valued_0 :::"complex-valued"::: ) ($#m1_hidden :::"Function":::) "holds" (Bool (Set ($#k30_valued_1 :::"-"::: ) (Set "(" (Set (Var "g")) ($#k13_valued_1 :::"-"::: ) (Set (Var "c")) ")" )) ($#r1_hidden :::"="::: ) (Set (Set "(" ($#k30_valued_1 :::"-"::: ) (Set (Var "g")) ")" ) ($#k7_valued_1 :::"+"::: ) (Set (Var "c")))))) ; theorem :: VALUED_2:12 (Bool "for" (Set (Var "c1")) "," (Set (Var "c2")) "being" ($#v1_xcmplx_0 :::"complex"::: ) ($#m1_hidden :::"number"::: ) (Bool "for" (Set (Var "g")) "being" ($#v1_valued_0 :::"complex-valued"::: ) ($#m1_hidden :::"Function":::) "holds" (Bool (Set (Set "(" (Set (Var "g")) ($#k7_valued_1 :::"+"::: ) (Set (Var "c1")) ")" ) ($#k7_valued_1 :::"+"::: ) (Set (Var "c2"))) ($#r1_hidden :::"="::: ) (Set (Set (Var "g")) ($#k7_valued_1 :::"+"::: ) (Set "(" (Set (Var "c1")) ($#k2_xcmplx_0 :::"+"::: ) (Set (Var "c2")) ")" ))))) ; theorem :: VALUED_2:13 (Bool "for" (Set (Var "c1")) "," (Set (Var "c2")) "being" ($#v1_xcmplx_0 :::"complex"::: ) ($#m1_hidden :::"number"::: ) (Bool "for" (Set (Var "g")) "being" ($#v1_valued_0 :::"complex-valued"::: ) ($#m1_hidden :::"Function":::) "holds" (Bool (Set (Set "(" (Set (Var "g")) ($#k7_valued_1 :::"+"::: ) (Set (Var "c1")) ")" ) ($#k13_valued_1 :::"-"::: ) (Set (Var "c2"))) ($#r1_hidden :::"="::: ) (Set (Set (Var "g")) ($#k7_valued_1 :::"+"::: ) (Set "(" (Set (Var "c1")) ($#k6_xcmplx_0 :::"-"::: ) (Set (Var "c2")) ")" ))))) ; theorem :: VALUED_2:14 (Bool "for" (Set (Var "c1")) "," (Set (Var "c2")) "being" ($#v1_xcmplx_0 :::"complex"::: ) ($#m1_hidden :::"number"::: ) (Bool "for" (Set (Var "g")) "being" ($#v1_valued_0 :::"complex-valued"::: ) ($#m1_hidden :::"Function":::) "holds" (Bool (Set (Set "(" (Set (Var "g")) ($#k13_valued_1 :::"-"::: ) (Set (Var "c1")) ")" ) ($#k7_valued_1 :::"+"::: ) (Set (Var "c2"))) ($#r1_hidden :::"="::: ) (Set (Set (Var "g")) ($#k13_valued_1 :::"-"::: ) (Set "(" (Set (Var "c1")) ($#k6_xcmplx_0 :::"-"::: ) (Set (Var "c2")) ")" ))))) ; theorem :: VALUED_2:15 (Bool "for" (Set (Var "c1")) "," (Set (Var "c2")) "being" ($#v1_xcmplx_0 :::"complex"::: ) ($#m1_hidden :::"number"::: ) (Bool "for" (Set (Var "g")) "being" ($#v1_valued_0 :::"complex-valued"::: ) ($#m1_hidden :::"Function":::) "holds" (Bool (Set (Set "(" (Set (Var "g")) ($#k13_valued_1 :::"-"::: ) (Set (Var "c1")) ")" ) ($#k13_valued_1 :::"-"::: ) (Set (Var "c2"))) ($#r1_hidden :::"="::: ) (Set (Set (Var "g")) ($#k13_valued_1 :::"-"::: ) (Set "(" (Set (Var "c1")) ($#k2_xcmplx_0 :::"+"::: ) (Set (Var "c2")) ")" ))))) ; theorem :: VALUED_2:16 (Bool "for" (Set (Var "c1")) "," (Set (Var "c2")) "being" ($#v1_xcmplx_0 :::"complex"::: ) ($#m1_hidden :::"number"::: ) (Bool "for" (Set (Var "g")) "being" ($#v1_valued_0 :::"complex-valued"::: ) ($#m1_hidden :::"Function":::) "holds" (Bool (Set (Set "(" (Set (Var "g")) ($#k24_valued_1 :::"(#)"::: ) (Set (Var "c1")) ")" ) ($#k24_valued_1 :::"(#)"::: ) (Set (Var "c2"))) ($#r1_hidden :::"="::: ) (Set (Set (Var "g")) ($#k24_valued_1 :::"(#)"::: ) (Set "(" (Set (Var "c1")) ($#k3_xcmplx_0 :::"*"::: ) (Set (Var "c2")) ")" ))))) ; theorem :: VALUED_2:17 (Bool "for" (Set (Var "g")) "," (Set (Var "h")) "being" ($#v1_valued_0 :::"complex-valued"::: ) ($#m1_hidden :::"Function":::) "holds" (Bool (Set ($#k30_valued_1 :::"-"::: ) (Set "(" (Set (Var "g")) ($#k1_valued_1 :::"+"::: ) (Set (Var "h")) ")" )) ($#r1_hidden :::"="::: ) (Set (Set "(" ($#k30_valued_1 :::"-"::: ) (Set (Var "g")) ")" ) ($#k45_valued_1 :::"-"::: ) (Set (Var "h"))))) ; theorem :: VALUED_2:18 (Bool "for" (Set (Var "g")) "," (Set (Var "h")) "being" ($#v1_valued_0 :::"complex-valued"::: ) ($#m1_hidden :::"Function":::) "holds" (Bool (Set (Set (Var "g")) ($#k45_valued_1 :::"-"::: ) (Set (Var "h"))) ($#r1_hidden :::"="::: ) (Set ($#k30_valued_1 :::"-"::: ) (Set "(" (Set (Var "h")) ($#k45_valued_1 :::"-"::: ) (Set (Var "g")) ")" )))) ; theorem :: VALUED_2:19 (Bool "for" (Set (Var "g")) "," (Set (Var "h")) "," (Set (Var "k")) "being" ($#v1_valued_0 :::"complex-valued"::: ) ($#m1_hidden :::"Function":::) "holds" (Bool (Set (Set "(" (Set (Var "g")) ($#k18_valued_1 :::"(#)"::: ) (Set (Var "h")) ")" ) ($#k50_valued_1 :::"/""::: ) (Set (Var "k"))) ($#r1_hidden :::"="::: ) (Set (Set (Var "g")) ($#k18_valued_1 :::"(#)"::: ) (Set "(" (Set (Var "h")) ($#k50_valued_1 :::"/""::: ) (Set (Var "k")) ")" )))) ; theorem :: VALUED_2:20 (Bool "for" (Set (Var "g")) "," (Set (Var "h")) "," (Set (Var "k")) "being" ($#v1_valued_0 :::"complex-valued"::: ) ($#m1_hidden :::"Function":::) "holds" (Bool (Set (Set "(" (Set (Var "g")) ($#k50_valued_1 :::"/""::: ) (Set (Var "h")) ")" ) ($#k18_valued_1 :::"(#)"::: ) (Set (Var "k"))) ($#r1_hidden :::"="::: ) (Set (Set "(" (Set (Var "g")) ($#k18_valued_1 :::"(#)"::: ) (Set (Var "k")) ")" ) ($#k50_valued_1 :::"/""::: ) (Set (Var "h"))))) ; theorem :: VALUED_2:21 (Bool "for" (Set (Var "g")) "," (Set (Var "h")) "," (Set (Var "k")) "being" ($#v1_valued_0 :::"complex-valued"::: ) ($#m1_hidden :::"Function":::) "holds" (Bool (Set (Set "(" (Set (Var "g")) ($#k50_valued_1 :::"/""::: ) (Set (Var "h")) ")" ) ($#k50_valued_1 :::"/""::: ) (Set (Var "k"))) ($#r1_hidden :::"="::: ) (Set (Set (Var "g")) ($#k50_valued_1 :::"/""::: ) (Set "(" (Set (Var "h")) ($#k18_valued_1 :::"(#)"::: ) (Set (Var "k")) ")" )))) ; theorem :: VALUED_2:22 (Bool "for" (Set (Var "c")) "being" ($#v1_xcmplx_0 :::"complex"::: ) ($#m1_hidden :::"number"::: ) (Bool "for" (Set (Var "g")) "being" ($#v1_valued_0 :::"complex-valued"::: ) ($#m1_hidden :::"Function":::) "holds" (Bool (Set (Set (Var "c")) ($#k24_valued_1 :::"(#)"::: ) (Set "(" ($#k30_valued_1 :::"-"::: ) (Set (Var "g")) ")" )) ($#r1_hidden :::"="::: ) (Set (Set "(" ($#k4_xcmplx_0 :::"-"::: ) (Set (Var "c")) ")" ) ($#k24_valued_1 :::"(#)"::: ) (Set (Var "g")))))) ; theorem :: VALUED_2:23 (Bool "for" (Set (Var "c")) "being" ($#v1_xcmplx_0 :::"complex"::: ) ($#m1_hidden :::"number"::: ) (Bool "for" (Set (Var "g")) "being" ($#v1_valued_0 :::"complex-valued"::: ) ($#m1_hidden :::"Function":::) "holds" (Bool (Set (Set (Var "c")) ($#k24_valued_1 :::"(#)"::: ) (Set "(" ($#k30_valued_1 :::"-"::: ) (Set (Var "g")) ")" )) ($#r1_hidden :::"="::: ) (Set ($#k30_valued_1 :::"-"::: ) (Set "(" (Set (Var "c")) ($#k24_valued_1 :::"(#)"::: ) (Set (Var "g")) ")" ))))) ; theorem :: VALUED_2:24 (Bool "for" (Set (Var "c")) "being" ($#v1_xcmplx_0 :::"complex"::: ) ($#m1_hidden :::"number"::: ) (Bool "for" (Set (Var "g")) "being" ($#v1_valued_0 :::"complex-valued"::: ) ($#m1_hidden :::"Function":::) "holds" (Bool (Set (Set "(" ($#k4_xcmplx_0 :::"-"::: ) (Set (Var "c")) ")" ) ($#k24_valued_1 :::"(#)"::: ) (Set (Var "g"))) ($#r1_hidden :::"="::: ) (Set ($#k30_valued_1 :::"-"::: ) (Set "(" (Set (Var "c")) ($#k24_valued_1 :::"(#)"::: ) (Set (Var "g")) ")" ))))) ; theorem :: VALUED_2:25 (Bool "for" (Set (Var "g")) "," (Set (Var "h")) "being" ($#v1_valued_0 :::"complex-valued"::: ) ($#m1_hidden :::"Function":::) "holds" (Bool (Set ($#k30_valued_1 :::"-"::: ) (Set "(" (Set (Var "g")) ($#k18_valued_1 :::"(#)"::: ) (Set (Var "h")) ")" )) ($#r1_hidden :::"="::: ) (Set (Set "(" ($#k30_valued_1 :::"-"::: ) (Set (Var "g")) ")" ) ($#k18_valued_1 :::"(#)"::: ) (Set (Var "h"))))) ; theorem :: VALUED_2:26 (Bool "for" (Set (Var "g")) "," (Set (Var "h")) "being" ($#v1_valued_0 :::"complex-valued"::: ) ($#m1_hidden :::"Function":::) "holds" (Bool (Set ($#k30_valued_1 :::"-"::: ) (Set "(" (Set (Var "g")) ($#k50_valued_1 :::"/""::: ) (Set (Var "h")) ")" )) ($#r1_hidden :::"="::: ) (Set (Set "(" ($#k30_valued_1 :::"-"::: ) (Set (Var "g")) ")" ) ($#k50_valued_1 :::"/""::: ) (Set (Var "h"))))) ; theorem :: VALUED_2:27 (Bool "for" (Set (Var "g")) "," (Set (Var "h")) "being" ($#v1_valued_0 :::"complex-valued"::: ) ($#m1_hidden :::"Function":::) "holds" (Bool (Set ($#k30_valued_1 :::"-"::: ) (Set "(" (Set (Var "g")) ($#k50_valued_1 :::"/""::: ) (Set (Var "h")) ")" )) ($#r1_hidden :::"="::: ) (Set (Set (Var "g")) ($#k50_valued_1 :::"/""::: ) (Set "(" ($#k30_valued_1 :::"-"::: ) (Set (Var "h")) ")" )))) ; definitionlet "f" be ($#v1_valued_0 :::"complex-valued"::: ) ($#m1_hidden :::"Function":::); let "c" be ($#v1_xcmplx_0 :::"complex"::: ) ($#m1_hidden :::"number"::: ) ; func "f" :::"(/)"::: "c" -> ($#m1_hidden :::"Function":::) equals :: VALUED_2:def 32 (Set (Set "(" (Num 1) ($#k7_xcmplx_0 :::"/"::: ) "c" ")" ) ($#k24_valued_1 :::"(#)"::: ) "f"); end; :: deftheorem defines :::"(/)"::: VALUED_2:def 32 : (Bool "for" (Set (Var "f")) "being" ($#v1_valued_0 :::"complex-valued"::: ) ($#m1_hidden :::"Function":::) (Bool "for" (Set (Var "c")) "being" ($#v1_xcmplx_0 :::"complex"::: ) ($#m1_hidden :::"number"::: ) "holds" (Bool (Set (Set (Var "f")) ($#k14_valued_2 :::"(/)"::: ) (Set (Var "c"))) ($#r1_hidden :::"="::: ) (Set (Set "(" (Num 1) ($#k7_xcmplx_0 :::"/"::: ) (Set (Var "c")) ")" ) ($#k24_valued_1 :::"(#)"::: ) (Set (Var "f")))))); registrationlet "f" be ($#v1_valued_0 :::"complex-valued"::: ) ($#m1_hidden :::"Function":::); let "c" be ($#v1_xcmplx_0 :::"complex"::: ) ($#m1_hidden :::"number"::: ) ; cluster (Set "f" ($#k14_valued_2 :::"(/)"::: ) "c") -> ($#v1_valued_0 :::"complex-valued"::: ) ; end; registrationlet "f" be ($#v3_valued_0 :::"real-valued"::: ) ($#m1_hidden :::"Function":::); let "r" be ($#v1_xreal_0 :::"real"::: ) ($#m1_hidden :::"number"::: ) ; cluster (Set "f" ($#k14_valued_2 :::"(/)"::: ) "r") -> ($#v3_valued_0 :::"real-valued"::: ) ; end; registrationlet "f" be (Set ($#k3_numbers :::"RAT"::: ) ) ($#v5_relat_1 :::"-valued"::: ) ($#m1_hidden :::"Function":::); let "r" be ($#v1_rat_1 :::"rational"::: ) ($#m1_hidden :::"number"::: ) ; cluster (Set "f" ($#k14_valued_2 :::"(/)"::: ) "r") -> (Set ($#k3_numbers :::"RAT"::: ) ) ($#v5_relat_1 :::"-valued"::: ) ; end; registrationlet "f" be ($#v1_valued_0 :::"complex-valued"::: ) ($#m1_hidden :::"FinSequence":::); let "c" be ($#v1_xcmplx_0 :::"complex"::: ) ($#m1_hidden :::"number"::: ) ; cluster (Set "f" ($#k14_valued_2 :::"(/)"::: ) "c") -> ($#v1_finseq_1 :::"FinSequence-like"::: ) ; end; theorem :: VALUED_2:28 (Bool "for" (Set (Var "c")) "being" ($#v1_xcmplx_0 :::"complex"::: ) ($#m1_hidden :::"number"::: ) (Bool "for" (Set (Var "g")) "being" ($#v1_valued_0 :::"complex-valued"::: ) ($#m1_hidden :::"Function":::) "holds" (Bool (Set ($#k9_xtuple_0 :::"dom"::: ) (Set "(" (Set (Var "g")) ($#k14_valued_2 :::"(/)"::: ) (Set (Var "c")) ")" )) ($#r1_hidden :::"="::: ) (Set ($#k9_xtuple_0 :::"dom"::: ) (Set (Var "g")))))) ; theorem :: VALUED_2:29 (Bool "for" (Set (Var "x")) "being" ($#m1_hidden :::"set"::: ) (Bool "for" (Set (Var "c")) "being" ($#v1_xcmplx_0 :::"complex"::: ) ($#m1_hidden :::"number"::: ) (Bool "for" (Set (Var "g")) "being" ($#v1_valued_0 :::"complex-valued"::: ) ($#m1_hidden :::"Function":::) "holds" (Bool (Set (Set "(" (Set (Var "g")) ($#k14_valued_2 :::"(/)"::: ) (Set (Var "c")) ")" ) ($#k1_funct_1 :::"."::: ) (Set (Var "x"))) ($#r1_hidden :::"="::: ) (Set (Set "(" (Set (Var "g")) ($#k1_funct_1 :::"."::: ) (Set (Var "x")) ")" ) ($#k7_xcmplx_0 :::"/"::: ) (Set (Var "c"))))))) ; theorem :: VALUED_2:30 (Bool "for" (Set (Var "c")) "being" ($#v1_xcmplx_0 :::"complex"::: ) ($#m1_hidden :::"number"::: ) (Bool "for" (Set (Var "g")) "being" ($#v1_valued_0 :::"complex-valued"::: ) ($#m1_hidden :::"Function":::) "holds" (Bool (Set (Set "(" ($#k30_valued_1 :::"-"::: ) (Set (Var "g")) ")" ) ($#k14_valued_2 :::"(/)"::: ) (Set (Var "c"))) ($#r1_hidden :::"="::: ) (Set ($#k30_valued_1 :::"-"::: ) (Set "(" (Set (Var "g")) ($#k14_valued_2 :::"(/)"::: ) (Set (Var "c")) ")" ))))) ; theorem :: VALUED_2:31 (Bool "for" (Set (Var "c")) "being" ($#v1_xcmplx_0 :::"complex"::: ) ($#m1_hidden :::"number"::: ) (Bool "for" (Set (Var "g")) "being" ($#v1_valued_0 :::"complex-valued"::: ) ($#m1_hidden :::"Function":::) "holds" (Bool (Set (Set (Var "g")) ($#k14_valued_2 :::"(/)"::: ) (Set "(" ($#k4_xcmplx_0 :::"-"::: ) (Set (Var "c")) ")" )) ($#r1_hidden :::"="::: ) (Set ($#k30_valued_1 :::"-"::: ) (Set "(" (Set (Var "g")) ($#k14_valued_2 :::"(/)"::: ) (Set (Var "c")) ")" ))))) ; theorem :: VALUED_2:32 (Bool "for" (Set (Var "c")) "being" ($#v1_xcmplx_0 :::"complex"::: ) ($#m1_hidden :::"number"::: ) (Bool "for" (Set (Var "g")) "being" ($#v1_valued_0 :::"complex-valued"::: ) ($#m1_hidden :::"Function":::) "holds" (Bool (Set (Set (Var "g")) ($#k14_valued_2 :::"(/)"::: ) (Set "(" ($#k4_xcmplx_0 :::"-"::: ) (Set (Var "c")) ")" )) ($#r1_hidden :::"="::: ) (Set (Set "(" ($#k30_valued_1 :::"-"::: ) (Set (Var "g")) ")" ) ($#k14_valued_2 :::"(/)"::: ) (Set (Var "c")))))) ; theorem :: VALUED_2:33 (Bool "for" (Set (Var "c1")) "," (Set (Var "c2")) "being" ($#v1_xcmplx_0 :::"complex"::: ) ($#m1_hidden :::"number"::: ) (Bool "for" (Set (Var "g")) "being" ($#v1_valued_0 :::"complex-valued"::: ) ($#m1_hidden :::"Function":::) "st" (Bool (Bool (Set (Var "g")) ($#r1_hidden :::"<>"::: ) (Set ($#k1_xboole_0 :::"{}"::: ) )) & (Bool (Set (Var "g")) "is" ($#v2_relat_1 :::"non-empty"::: ) ) & (Bool (Set (Set (Var "g")) ($#k14_valued_2 :::"(/)"::: ) (Set (Var "c1"))) ($#r1_hidden :::"="::: ) (Set (Set (Var "g")) ($#k14_valued_2 :::"(/)"::: ) (Set (Var "c2"))))) "holds" (Bool (Set (Var "c1")) ($#r1_hidden :::"="::: ) (Set (Var "c2"))))) ; theorem :: VALUED_2:34 (Bool "for" (Set (Var "c1")) "," (Set (Var "c2")) "being" ($#v1_xcmplx_0 :::"complex"::: ) ($#m1_hidden :::"number"::: ) (Bool "for" (Set (Var "g")) "being" ($#v1_valued_0 :::"complex-valued"::: ) ($#m1_hidden :::"Function":::) "holds" (Bool (Set (Set "(" (Set (Var "g")) ($#k24_valued_1 :::"(#)"::: ) (Set (Var "c1")) ")" ) ($#k14_valued_2 :::"(/)"::: ) (Set (Var "c2"))) ($#r1_hidden :::"="::: ) (Set (Set (Var "g")) ($#k24_valued_1 :::"(#)"::: ) (Set "(" (Set (Var "c1")) ($#k7_xcmplx_0 :::"/"::: ) (Set (Var "c2")) ")" ))))) ; theorem :: VALUED_2:35 (Bool "for" (Set (Var "c1")) "," (Set (Var "c2")) "being" ($#v1_xcmplx_0 :::"complex"::: ) ($#m1_hidden :::"number"::: ) (Bool "for" (Set (Var "g")) "being" ($#v1_valued_0 :::"complex-valued"::: ) ($#m1_hidden :::"Function":::) "holds" (Bool (Set (Set "(" (Set (Var "g")) ($#k14_valued_2 :::"(/)"::: ) (Set (Var "c1")) ")" ) ($#k24_valued_1 :::"(#)"::: ) (Set (Var "c2"))) ($#r1_hidden :::"="::: ) (Set (Set "(" (Set (Var "g")) ($#k24_valued_1 :::"(#)"::: ) (Set (Var "c2")) ")" ) ($#k14_valued_2 :::"(/)"::: ) (Set (Var "c1")))))) ; theorem :: VALUED_2:36 (Bool "for" (Set (Var "c1")) "," (Set (Var "c2")) "being" ($#v1_xcmplx_0 :::"complex"::: ) ($#m1_hidden :::"number"::: ) (Bool "for" (Set (Var "g")) "being" ($#v1_valued_0 :::"complex-valued"::: ) ($#m1_hidden :::"Function":::) "holds" (Bool (Set (Set "(" (Set (Var "g")) ($#k14_valued_2 :::"(/)"::: ) (Set (Var "c1")) ")" ) ($#k14_valued_2 :::"(/)"::: ) (Set (Var "c2"))) ($#r1_hidden :::"="::: ) (Set (Set (Var "g")) ($#k14_valued_2 :::"(/)"::: ) (Set "(" (Set (Var "c1")) ($#k3_xcmplx_0 :::"*"::: ) (Set (Var "c2")) ")" ))))) ; theorem :: VALUED_2:37 (Bool "for" (Set (Var "c")) "being" ($#v1_xcmplx_0 :::"complex"::: ) ($#m1_hidden :::"number"::: ) (Bool "for" (Set (Var "g")) "," (Set (Var "h")) "being" ($#v1_valued_0 :::"complex-valued"::: ) ($#m1_hidden :::"Function":::) "holds" (Bool (Set (Set "(" (Set (Var "g")) ($#k1_valued_1 :::"+"::: ) (Set (Var "h")) ")" ) ($#k14_valued_2 :::"(/)"::: ) (Set (Var "c"))) ($#r1_hidden :::"="::: ) (Set (Set "(" (Set (Var "g")) ($#k14_valued_2 :::"(/)"::: ) (Set (Var "c")) ")" ) ($#k1_valued_1 :::"+"::: ) (Set "(" (Set (Var "h")) ($#k14_valued_2 :::"(/)"::: ) (Set (Var "c")) ")" ))))) ; theorem :: VALUED_2:38 (Bool "for" (Set (Var "c")) "being" ($#v1_xcmplx_0 :::"complex"::: ) ($#m1_hidden :::"number"::: ) (Bool "for" (Set (Var "g")) "," (Set (Var "h")) "being" ($#v1_valued_0 :::"complex-valued"::: ) ($#m1_hidden :::"Function":::) "holds" (Bool (Set (Set "(" (Set (Var "g")) ($#k45_valued_1 :::"-"::: ) (Set (Var "h")) ")" ) ($#k14_valued_2 :::"(/)"::: ) (Set (Var "c"))) ($#r1_hidden :::"="::: ) (Set (Set "(" (Set (Var "g")) ($#k14_valued_2 :::"(/)"::: ) (Set (Var "c")) ")" ) ($#k45_valued_1 :::"-"::: ) (Set "(" (Set (Var "h")) ($#k14_valued_2 :::"(/)"::: ) (Set (Var "c")) ")" ))))) ; theorem :: VALUED_2:39 (Bool "for" (Set (Var "c")) "being" ($#v1_xcmplx_0 :::"complex"::: ) ($#m1_hidden :::"number"::: ) (Bool "for" (Set (Var "g")) "," (Set (Var "h")) "being" ($#v1_valued_0 :::"complex-valued"::: ) ($#m1_hidden :::"Function":::) "holds" (Bool (Set (Set "(" (Set (Var "g")) ($#k18_valued_1 :::"(#)"::: ) (Set (Var "h")) ")" ) ($#k14_valued_2 :::"(/)"::: ) (Set (Var "c"))) ($#r1_hidden :::"="::: ) (Set (Set (Var "g")) ($#k18_valued_1 :::"(#)"::: ) (Set "(" (Set (Var "h")) ($#k14_valued_2 :::"(/)"::: ) (Set (Var "c")) ")" ))))) ; theorem :: VALUED_2:40 (Bool "for" (Set (Var "c")) "being" ($#v1_xcmplx_0 :::"complex"::: ) ($#m1_hidden :::"number"::: ) (Bool "for" (Set (Var "g")) "," (Set (Var "h")) "being" ($#v1_valued_0 :::"complex-valued"::: ) ($#m1_hidden :::"Function":::) "holds" (Bool (Set (Set "(" (Set (Var "g")) ($#k50_valued_1 :::"/""::: ) (Set (Var "h")) ")" ) ($#k14_valued_2 :::"(/)"::: ) (Set (Var "c"))) ($#r1_hidden :::"="::: ) (Set (Set (Var "g")) ($#k50_valued_1 :::"/""::: ) (Set "(" (Set (Var "h")) ($#k24_valued_1 :::"(#)"::: ) (Set (Var "c")) ")" ))))) ; definitionlet "f" be ($#v7_valued_2 :::"complex-functions-valued"::: ) ($#m1_hidden :::"Function":::); func :::"<->"::: "f" -> ($#m1_hidden :::"Function":::) means :: VALUED_2:def 33 (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 ($#k30_valued_1 :::"-"::: ) (Set "(" "f" ($#k1_funct_1 :::"."::: ) (Set (Var "x")) ")" ))) ")" ) ")" ); end; :: deftheorem defines :::"<->"::: VALUED_2:def 33 : (Bool "for" (Set (Var "f")) "being" ($#v7_valued_2 :::"complex-functions-valued"::: ) ($#m1_hidden :::"Function":::) (Bool "for" (Set (Var "b2")) "being" ($#m1_hidden :::"Function":::) "holds" (Bool "(" (Bool (Set (Var "b2")) ($#r1_hidden :::"="::: ) (Set ($#k15_valued_2 :::"<->"::: ) (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 ($#k30_valued_1 :::"-"::: ) (Set "(" (Set (Var "f")) ($#k1_funct_1 :::"."::: ) (Set (Var "x")) ")" ))) ")" ) ")" ) ")" ))); definitionlet "X" be ($#m1_hidden :::"set"::: ) ; let "Y" be ($#v1_valued_2 :::"complex-functions-membered"::: ) ($#m1_hidden :::"set"::: ) ; let "f" be ($#m1_subset_1 :::"PartFunc":::) "of" (Set (Const "X")) "," (Set (Const "Y")); :: original: :::"<->"::: redefine func :::"<->"::: "f" -> ($#m1_subset_1 :::"PartFunc":::) "of" "X" "," (Set "(" ($#k2_valued_2 :::"C_PFuncs"::: ) (Set "(" ($#k1_valued_2 :::"DOMS"::: ) "Y" ")" ) ")" ); end; definitionlet "X" be ($#m1_hidden :::"set"::: ) ; let "Y" be ($#v3_valued_2 :::"real-functions-membered"::: ) ($#m1_hidden :::"set"::: ) ; let "f" be ($#m1_subset_1 :::"PartFunc":::) "of" (Set (Const "X")) "," (Set (Const "Y")); :: original: :::"<->"::: redefine func :::"<->"::: "f" -> ($#m1_subset_1 :::"PartFunc":::) "of" "X" "," (Set "(" ($#k6_valued_2 :::"R_PFuncs"::: ) (Set "(" ($#k1_valued_2 :::"DOMS"::: ) "Y" ")" ) ")" ); end; definitionlet "X" be ($#m1_hidden :::"set"::: ) ; let "Y" be ($#v4_valued_2 :::"rational-functions-membered"::: ) ($#m1_hidden :::"set"::: ) ; let "f" be ($#m1_subset_1 :::"PartFunc":::) "of" (Set (Const "X")) "," (Set (Const "Y")); :: original: :::"<->"::: redefine func :::"<->"::: "f" -> ($#m1_subset_1 :::"PartFunc":::) "of" "X" "," (Set "(" ($#k8_valued_2 :::"Q_PFuncs"::: ) (Set "(" ($#k1_valued_2 :::"DOMS"::: ) "Y" ")" ) ")" ); end; definitionlet "X" be ($#m1_hidden :::"set"::: ) ; let "Y" be ($#v5_valued_2 :::"integer-functions-membered"::: ) ($#m1_hidden :::"set"::: ) ; let "f" be ($#m1_subset_1 :::"PartFunc":::) "of" (Set (Const "X")) "," (Set (Const "Y")); :: original: :::"<->"::: redefine func :::"<->"::: "f" -> ($#m1_subset_1 :::"PartFunc":::) "of" "X" "," (Set "(" ($#k10_valued_2 :::"I_PFuncs"::: ) (Set "(" ($#k1_valued_2 :::"DOMS"::: ) "Y" ")" ) ")" ); end; registrationlet "Y" be ($#v1_valued_2 :::"complex-functions-membered"::: ) ($#m1_hidden :::"set"::: ) ; let "f" be ($#m2_finseq_1 :::"FinSequence"::: ) "of" (Set (Const "Y")); cluster (Set ($#k15_valued_2 :::"<->"::: ) "f") -> ($#v1_finseq_1 :::"FinSequence-like"::: ) ; end; theorem :: VALUED_2:41 (Bool "for" (Set (Var "X")) "being" ($#m1_hidden :::"set"::: ) (Bool "for" (Set (Var "Y")) "being" ($#v1_valued_2 :::"complex-functions-membered"::: ) ($#m1_hidden :::"set"::: ) (Bool "for" (Set (Var "f")) "being" ($#m1_subset_1 :::"PartFunc":::) "of" (Set (Var "X")) "," (Set (Var "Y")) "holds" (Bool (Set ($#k16_valued_2 :::"<->"::: ) (Set "(" ($#k16_valued_2 :::"<->"::: ) (Set (Var "f")) ")" )) ($#r1_hidden :::"="::: ) (Set (Var "f")))))) ; theorem :: VALUED_2:42 (Bool "for" (Set (Var "X1")) "," (Set (Var "X2")) "being" ($#m1_hidden :::"set"::: ) (Bool "for" (Set (Var "Y1")) "," (Set (Var "Y2")) "being" ($#v1_valued_2 :::"complex-functions-membered"::: ) ($#m1_hidden :::"set"::: ) (Bool "for" (Set (Var "f1")) "being" ($#m1_subset_1 :::"PartFunc":::) "of" (Set (Var "X1")) "," (Set (Var "Y1")) (Bool "for" (Set (Var "f2")) "being" ($#m1_subset_1 :::"PartFunc":::) "of" (Set (Var "X2")) "," (Set (Var "Y2")) "st" (Bool (Bool (Set ($#k16_valued_2 :::"<->"::: ) (Set (Var "f1"))) ($#r1_hidden :::"="::: ) (Set ($#k16_valued_2 :::"<->"::: ) (Set (Var "f2"))))) "holds" (Bool (Set (Var "f1")) ($#r1_hidden :::"="::: ) (Set (Var "f2"))))))) ; definitionlet "X" be ($#v1_valued_2 :::"complex-functions-membered"::: ) ($#m1_hidden :::"set"::: ) ; let "Y" be ($#m1_hidden :::"set"::: ) ; let "f" be ($#m1_subset_1 :::"PartFunc":::) "of" (Set (Const "X")) "," (Set (Const "Y")); func "f" :::"(-)"::: -> ($#m1_hidden :::"Function":::) means :: VALUED_2:def 34 (Bool "(" (Bool (Set ($#k9_xtuple_0 :::"dom"::: ) it) ($#r1_hidden :::"="::: ) (Set ($#k1_relset_1 :::"dom"::: ) "f")) & (Bool "(" "for" (Set (Var "x")) "being" ($#v1_valued_0 :::"complex-valued"::: ) ($#m1_hidden :::"Function":::) "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 "f" ($#k1_funct_1 :::"."::: ) (Set "(" ($#k30_valued_1 :::"-"::: ) (Set (Var "x")) ")" ))) ")" ) ")" ); end; :: deftheorem defines :::"(-)"::: VALUED_2:def 34 : (Bool "for" (Set (Var "X")) "being" ($#v1_valued_2 :::"complex-functions-membered"::: ) ($#m1_hidden :::"set"::: ) (Bool "for" (Set (Var "Y")) "being" ($#m1_hidden :::"set"::: ) (Bool "for" (Set (Var "f")) "being" ($#m1_subset_1 :::"PartFunc":::) "of" (Set (Var "X")) "," (Set (Var "Y")) (Bool "for" (Set (Var "b4")) "being" ($#m1_hidden :::"Function":::) "holds" (Bool "(" (Bool (Set (Var "b4")) ($#r1_hidden :::"="::: ) (Set (Set (Var "f")) ($#k20_valued_2 :::"(-)"::: ) )) "iff" (Bool "(" (Bool (Set ($#k9_xtuple_0 :::"dom"::: ) (Set (Var "b4"))) ($#r1_hidden :::"="::: ) (Set ($#k1_relset_1 :::"dom"::: ) (Set (Var "f")))) & (Bool "(" "for" (Set (Var "x")) "being" ($#v1_valued_0 :::"complex-valued"::: ) ($#m1_hidden :::"Function":::) "st" (Bool (Bool (Set (Var "x")) ($#r2_hidden :::"in"::: ) (Set ($#k9_xtuple_0 :::"dom"::: ) (Set (Var "b4"))))) "holds" (Bool (Set (Set (Var "b4")) ($#k1_funct_1 :::"."::: ) (Set (Var "x"))) ($#r1_hidden :::"="::: ) (Set (Set (Var "f")) ($#k1_funct_1 :::"."::: ) (Set "(" ($#k30_valued_1 :::"-"::: ) (Set (Var "x")) ")" ))) ")" ) ")" ) ")" ))))); definitionlet "f" be ($#v7_valued_2 :::"complex-functions-valued"::: ) ($#m1_hidden :::"Function":::); func :::""::: "f" -> ($#m1_hidden :::"Function":::) means :: VALUED_2:def 35 (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 (Set "(" "f" ($#k1_funct_1 :::"."::: ) (Set (Var "x")) ")" ) ($#k35_valued_1 :::"""::: ) )) ")" ) ")" ); end; :: deftheorem defines :::""::: VALUED_2:def 35 : (Bool "for" (Set (Var "f")) "being" ($#v7_valued_2 :::"complex-functions-valued"::: ) ($#m1_hidden :::"Function":::) (Bool "for" (Set (Var "b2")) "being" ($#m1_hidden :::"Function":::) "holds" (Bool "(" (Bool (Set (Var "b2")) ($#r1_hidden :::"="::: ) (Set ($#k21_valued_2 :::""::: ) (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 (Set "(" (Set (Var "f")) ($#k1_funct_1 :::"."::: ) (Set (Var "x")) ")" ) ($#k35_valued_1 :::"""::: ) )) ")" ) ")" ) ")" ))); definitionlet "X" be ($#m1_hidden :::"set"::: ) ; let "Y" be ($#v1_valued_2 :::"complex-functions-membered"::: ) ($#m1_hidden :::"set"::: ) ; let "f" be ($#m1_subset_1 :::"PartFunc":::) "of" (Set (Const "X")) "," (Set (Const "Y")); :: original: :::""::: redefine func :::""::: "f" -> ($#m1_subset_1 :::"PartFunc":::) "of" "X" "," (Set "(" ($#k2_valued_2 :::"C_PFuncs"::: ) (Set "(" ($#k1_valued_2 :::"DOMS"::: ) "Y" ")" ) ")" ); end; definitionlet "X" be ($#m1_hidden :::"set"::: ) ; let "Y" be ($#v3_valued_2 :::"real-functions-membered"::: ) ($#m1_hidden :::"set"::: ) ; let "f" be ($#m1_subset_1 :::"PartFunc":::) "of" (Set (Const "X")) "," (Set (Const "Y")); :: original: :::""::: redefine func :::""::: "f" -> ($#m1_subset_1 :::"PartFunc":::) "of" "X" "," (Set "(" ($#k6_valued_2 :::"R_PFuncs"::: ) (Set "(" ($#k1_valued_2 :::"DOMS"::: ) "Y" ")" ) ")" ); end; definitionlet "X" be ($#m1_hidden :::"set"::: ) ; let "Y" be ($#v4_valued_2 :::"rational-functions-membered"::: ) ($#m1_hidden :::"set"::: ) ; let "f" be ($#m1_subset_1 :::"PartFunc":::) "of" (Set (Const "X")) "," (Set (Const "Y")); :: original: :::""::: redefine func :::""::: "f" -> ($#m1_subset_1 :::"PartFunc":::) "of" "X" "," (Set "(" ($#k8_valued_2 :::"Q_PFuncs"::: ) (Set "(" ($#k1_valued_2 :::"DOMS"::: ) "Y" ")" ) ")" ); end; registrationlet "Y" be ($#v1_valued_2 :::"complex-functions-membered"::: ) ($#m1_hidden :::"set"::: ) ; let "f" be ($#m2_finseq_1 :::"FinSequence"::: ) "of" (Set (Const "Y")); cluster (Set ($#k21_valued_2 :::""::: ) "f") -> ($#v1_finseq_1 :::"FinSequence-like"::: ) ; end; theorem :: VALUED_2:43 (Bool "for" (Set (Var "X")) "being" ($#m1_hidden :::"set"::: ) (Bool "for" (Set (Var "Y")) "being" ($#v1_valued_2 :::"complex-functions-membered"::: ) ($#m1_hidden :::"set"::: ) (Bool "for" (Set (Var "f")) "being" ($#m1_subset_1 :::"PartFunc":::) "of" (Set (Var "X")) "," (Set (Var "Y")) "holds" (Bool (Set ($#k22_valued_2 :::""::: ) (Set "(" ($#k22_valued_2 :::""::: ) (Set (Var "f")) ")" )) ($#r1_hidden :::"="::: ) (Set (Var "f")))))) ; definitionlet "f" be ($#v7_valued_2 :::"complex-functions-valued"::: ) ($#m1_hidden :::"Function":::); func :::"abs"::: "f" -> ($#m1_hidden :::"Function":::) means :: VALUED_2:def 36 (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 ($#k54_valued_1 :::"abs"::: ) (Set "(" "f" ($#k1_funct_1 :::"."::: ) (Set (Var "x")) ")" ))) ")" ) ")" ); end; :: deftheorem defines :::"abs"::: VALUED_2:def 36 : (Bool "for" (Set (Var "f")) "being" ($#v7_valued_2 :::"complex-functions-valued"::: ) ($#m1_hidden :::"Function":::) (Bool "for" (Set (Var "b2")) "being" ($#m1_hidden :::"Function":::) "holds" (Bool "(" (Bool (Set (Var "b2")) ($#r1_hidden :::"="::: ) (Set ($#k25_valued_2 :::"abs"::: ) (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 ($#k54_valued_1 :::"abs"::: ) (Set "(" (Set (Var "f")) ($#k1_funct_1 :::"."::: ) (Set (Var "x")) ")" ))) ")" ) ")" ) ")" ))); definitionlet "X" be ($#m1_hidden :::"set"::: ) ; let "Y" be ($#v1_valued_2 :::"complex-functions-membered"::: ) ($#m1_hidden :::"set"::: ) ; let "f" be ($#m1_subset_1 :::"PartFunc":::) "of" (Set (Const "X")) "," (Set (Const "Y")); :: original: :::"abs"::: redefine func :::"abs"::: "f" -> ($#m1_subset_1 :::"PartFunc":::) "of" "X" "," (Set "(" ($#k2_valued_2 :::"C_PFuncs"::: ) (Set "(" ($#k1_valued_2 :::"DOMS"::: ) "Y" ")" ) ")" ); end; definitionlet "X" be ($#m1_hidden :::"set"::: ) ; let "Y" be ($#v3_valued_2 :::"real-functions-membered"::: ) ($#m1_hidden :::"set"::: ) ; let "f" be ($#m1_subset_1 :::"PartFunc":::) "of" (Set (Const "X")) "," (Set (Const "Y")); :: original: :::"abs"::: redefine func :::"abs"::: "f" -> ($#m1_subset_1 :::"PartFunc":::) "of" "X" "," (Set "(" ($#k6_valued_2 :::"R_PFuncs"::: ) (Set "(" ($#k1_valued_2 :::"DOMS"::: ) "Y" ")" ) ")" ); end; definitionlet "X" be ($#m1_hidden :::"set"::: ) ; let "Y" be ($#v4_valued_2 :::"rational-functions-membered"::: ) ($#m1_hidden :::"set"::: ) ; let "f" be ($#m1_subset_1 :::"PartFunc":::) "of" (Set (Const "X")) "," (Set (Const "Y")); :: original: :::"abs"::: redefine func :::"abs"::: "f" -> ($#m1_subset_1 :::"PartFunc":::) "of" "X" "," (Set "(" ($#k8_valued_2 :::"Q_PFuncs"::: ) (Set "(" ($#k1_valued_2 :::"DOMS"::: ) "Y" ")" ) ")" ); end; definitionlet "X" be ($#m1_hidden :::"set"::: ) ; let "Y" be ($#v5_valued_2 :::"integer-functions-membered"::: ) ($#m1_hidden :::"set"::: ) ; let "f" be ($#m1_subset_1 :::"PartFunc":::) "of" (Set (Const "X")) "," (Set (Const "Y")); :: original: :::"abs"::: redefine func :::"abs"::: "f" -> ($#m1_subset_1 :::"PartFunc":::) "of" "X" "," (Set "(" ($#k12_valued_2 :::"N_PFuncs"::: ) (Set "(" ($#k1_valued_2 :::"DOMS"::: ) "Y" ")" ) ")" ); end; registrationlet "Y" be ($#v1_valued_2 :::"complex-functions-membered"::: ) ($#m1_hidden :::"set"::: ) ; let "f" be ($#m2_finseq_1 :::"FinSequence"::: ) "of" (Set (Const "Y")); cluster (Set ($#k25_valued_2 :::"abs"::: ) "f") -> ($#v1_finseq_1 :::"FinSequence-like"::: ) ; end; theorem :: VALUED_2:44 (Bool "for" (Set (Var "X")) "being" ($#m1_hidden :::"set"::: ) (Bool "for" (Set (Var "Y")) "being" ($#v1_valued_2 :::"complex-functions-membered"::: ) ($#m1_hidden :::"set"::: ) (Bool "for" (Set (Var "f")) "being" ($#m1_subset_1 :::"PartFunc":::) "of" (Set (Var "X")) "," (Set (Var "Y")) "holds" (Bool (Set ($#k26_valued_2 :::"abs"::: ) (Set "(" ($#k26_valued_2 :::"abs"::: ) (Set (Var "f")) ")" )) ($#r1_hidden :::"="::: ) (Set ($#k26_valued_2 :::"abs"::: ) (Set (Var "f"))))))) ; definitionlet "Y" be ($#v1_valued_2 :::"complex-functions-membered"::: ) ($#m1_hidden :::"set"::: ) ; let "f" be (Set (Const "Y")) ($#v5_relat_1 :::"-valued"::: ) ($#m1_hidden :::"Function":::); let "c" be ($#v1_xcmplx_0 :::"complex"::: ) ($#m1_hidden :::"number"::: ) ; func "f" :::"[+]"::: "c" -> ($#m1_hidden :::"Function":::) means :: VALUED_2:def 37 (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 "c" ($#k7_valued_1 :::"+"::: ) (Set "(" "f" ($#k1_funct_1 :::"."::: ) (Set (Var "x")) ")" ))) ")" ) ")" ); end; :: deftheorem defines :::"[+]"::: VALUED_2:def 37 : (Bool "for" (Set (Var "Y")) "being" ($#v1_valued_2 :::"complex-functions-membered"::: ) ($#m1_hidden :::"set"::: ) (Bool "for" (Set (Var "f")) "being" (Set (Var "b1")) ($#v5_relat_1 :::"-valued"::: ) ($#m1_hidden :::"Function":::) (Bool "for" (Set (Var "c")) "being" ($#v1_xcmplx_0 :::"complex"::: ) ($#m1_hidden :::"number"::: ) (Bool "for" (Set (Var "b4")) "being" ($#m1_hidden :::"Function":::) "holds" (Bool "(" (Bool (Set (Var "b4")) ($#r1_hidden :::"="::: ) (Set (Set (Var "f")) ($#k30_valued_2 :::"[+]"::: ) (Set (Var "c")))) "iff" (Bool "(" (Bool (Set ($#k9_xtuple_0 :::"dom"::: ) (Set (Var "b4"))) ($#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 "b4"))))) "holds" (Bool (Set (Set (Var "b4")) ($#k1_funct_1 :::"."::: ) (Set (Var "x"))) ($#r1_hidden :::"="::: ) (Set (Set (Var "c")) ($#k7_valued_1 :::"+"::: ) (Set "(" (Set (Var "f")) ($#k1_funct_1 :::"."::: ) (Set (Var "x")) ")" ))) ")" ) ")" ) ")" ))))); definitionlet "X" be ($#m1_hidden :::"set"::: ) ; let "Y" be ($#v1_valued_2 :::"complex-functions-membered"::: ) ($#m1_hidden :::"set"::: ) ; let "f" be ($#m1_subset_1 :::"PartFunc":::) "of" (Set (Const "X")) "," (Set (Const "Y")); let "c" be ($#v1_xcmplx_0 :::"complex"::: ) ($#m1_hidden :::"number"::: ) ; :: original: :::"[+]"::: redefine func "f" :::"[+]"::: "c" -> ($#m1_subset_1 :::"PartFunc":::) "of" "X" "," (Set "(" ($#k2_valued_2 :::"C_PFuncs"::: ) (Set "(" ($#k1_valued_2 :::"DOMS"::: ) "Y" ")" ) ")" ); end; definitionlet "X" be ($#m1_hidden :::"set"::: ) ; let "Y" be ($#v3_valued_2 :::"real-functions-membered"::: ) ($#m1_hidden :::"set"::: ) ; let "f" be ($#m1_subset_1 :::"PartFunc":::) "of" (Set (Const "X")) "," (Set (Const "Y")); let "c" be ($#v1_xreal_0 :::"real"::: ) ($#m1_hidden :::"number"::: ) ; :: original: :::"[+]"::: redefine func "f" :::"[+]"::: "c" -> ($#m1_subset_1 :::"PartFunc":::) "of" "X" "," (Set "(" ($#k6_valued_2 :::"R_PFuncs"::: ) (Set "(" ($#k1_valued_2 :::"DOMS"::: ) "Y" ")" ) ")" ); end; definitionlet "X" be ($#m1_hidden :::"set"::: ) ; let "Y" be ($#v4_valued_2 :::"rational-functions-membered"::: ) ($#m1_hidden :::"set"::: ) ; let "f" be ($#m1_subset_1 :::"PartFunc":::) "of" (Set (Const "X")) "," (Set (Const "Y")); let "c" be ($#v1_rat_1 :::"rational"::: ) ($#m1_hidden :::"number"::: ) ; :: original: :::"[+]"::: redefine func "f" :::"[+]"::: "c" -> ($#m1_subset_1 :::"PartFunc":::) "of" "X" "," (Set "(" ($#k8_valued_2 :::"Q_PFuncs"::: ) (Set "(" ($#k1_valued_2 :::"DOMS"::: ) "Y" ")" ) ")" ); end; definitionlet "X" be ($#m1_hidden :::"set"::: ) ; let "Y" be ($#v5_valued_2 :::"integer-functions-membered"::: ) ($#m1_hidden :::"set"::: ) ; let "f" be ($#m1_subset_1 :::"PartFunc":::) "of" (Set (Const "X")) "," (Set (Const "Y")); let "c" be ($#v1_int_1 :::"integer"::: ) ($#m1_hidden :::"number"::: ) ; :: original: :::"[+]"::: redefine func "f" :::"[+]"::: "c" -> ($#m1_subset_1 :::"PartFunc":::) "of" "X" "," (Set "(" ($#k10_valued_2 :::"I_PFuncs"::: ) (Set "(" ($#k1_valued_2 :::"DOMS"::: ) "Y" ")" ) ")" ); end; definitionlet "X" be ($#m1_hidden :::"set"::: ) ; let "Y" be ($#v6_valued_2 :::"natural-functions-membered"::: ) ($#m1_hidden :::"set"::: ) ; let "f" be ($#m1_subset_1 :::"PartFunc":::) "of" (Set (Const "X")) "," (Set (Const "Y")); let "c" be ($#m1_hidden :::"Nat":::); :: original: :::"[+]"::: redefine func "f" :::"[+]"::: "c" -> ($#m1_subset_1 :::"PartFunc":::) "of" "X" "," (Set "(" ($#k12_valued_2 :::"N_PFuncs"::: ) (Set "(" ($#k1_valued_2 :::"DOMS"::: ) "Y" ")" ) ")" ); end; theorem :: VALUED_2:45 (Bool "for" (Set (Var "X")) "being" ($#m1_hidden :::"set"::: ) (Bool "for" (Set (Var "Y")) "being" ($#v1_valued_2 :::"complex-functions-membered"::: ) ($#m1_hidden :::"set"::: ) (Bool "for" (Set (Var "c1")) "," (Set (Var "c2")) "being" ($#v1_xcmplx_0 :::"complex"::: ) ($#m1_hidden :::"number"::: ) (Bool "for" (Set (Var "f")) "being" ($#m1_subset_1 :::"PartFunc":::) "of" (Set (Var "X")) "," (Set (Var "Y")) "holds" (Bool (Set (Set "(" (Set (Var "f")) ($#k31_valued_2 :::"[+]"::: ) (Set (Var "c1")) ")" ) ($#k31_valued_2 :::"[+]"::: ) (Set (Var "c2"))) ($#r1_hidden :::"="::: ) (Set (Set (Var "f")) ($#k31_valued_2 :::"[+]"::: ) (Set "(" (Set (Var "c1")) ($#k2_xcmplx_0 :::"+"::: ) (Set (Var "c2")) ")" ))))))) ; theorem :: VALUED_2:46 (Bool "for" (Set (Var "X")) "being" ($#m1_hidden :::"set"::: ) (Bool "for" (Set (Var "Y")) "being" ($#v1_valued_2 :::"complex-functions-membered"::: ) ($#m1_hidden :::"set"::: ) (Bool "for" (Set (Var "c1")) "," (Set (Var "c2")) "being" ($#v1_xcmplx_0 :::"complex"::: ) ($#m1_hidden :::"number"::: ) (Bool "for" (Set (Var "f")) "being" ($#m1_subset_1 :::"PartFunc":::) "of" (Set (Var "X")) "," (Set (Var "Y")) "st" (Bool (Bool (Set (Var "f")) ($#r1_hidden :::"<>"::: ) (Set ($#k1_xboole_0 :::"{}"::: ) )) & (Bool (Set (Var "f")) "is" ($#v2_relat_1 :::"non-empty"::: ) ) & (Bool (Set (Set (Var "f")) ($#k31_valued_2 :::"[+]"::: ) (Set (Var "c1"))) ($#r2_relset_1 :::"="::: ) (Set (Set (Var "f")) ($#k31_valued_2 :::"[+]"::: ) (Set (Var "c2"))))) "holds" (Bool (Set (Var "c1")) ($#r1_hidden :::"="::: ) (Set (Var "c2"))))))) ; definitionlet "Y" be ($#v1_valued_2 :::"complex-functions-membered"::: ) ($#m1_hidden :::"set"::: ) ; let "f" be (Set (Const "Y")) ($#v5_relat_1 :::"-valued"::: ) ($#m1_hidden :::"Function":::); let "c" be ($#v1_xcmplx_0 :::"complex"::: ) ($#m1_hidden :::"number"::: ) ; func "f" :::"[-]"::: "c" -> ($#m1_hidden :::"Function":::) equals :: VALUED_2:def 38 (Set "f" ($#k30_valued_2 :::"[+]"::: ) (Set "(" ($#k4_xcmplx_0 :::"-"::: ) "c" ")" )); end; :: deftheorem defines :::"[-]"::: VALUED_2:def 38 : (Bool "for" (Set (Var "Y")) "being" ($#v1_valued_2 :::"complex-functions-membered"::: ) ($#m1_hidden :::"set"::: ) (Bool "for" (Set (Var "f")) "being" (Set (Var "b1")) ($#v5_relat_1 :::"-valued"::: ) ($#m1_hidden :::"Function":::) (Bool "for" (Set (Var "c")) "being" ($#v1_xcmplx_0 :::"complex"::: ) ($#m1_hidden :::"number"::: ) "holds" (Bool (Set (Set (Var "f")) ($#k36_valued_2 :::"[-]"::: ) (Set (Var "c"))) ($#r1_hidden :::"="::: ) (Set (Set (Var "f")) ($#k30_valued_2 :::"[+]"::: ) (Set "(" ($#k4_xcmplx_0 :::"-"::: ) (Set (Var "c")) ")" )))))); theorem :: VALUED_2:47 (Bool "for" (Set (Var "X")) "being" ($#m1_hidden :::"set"::: ) (Bool "for" (Set (Var "Y")) "being" ($#v1_valued_2 :::"complex-functions-membered"::: ) ($#m1_hidden :::"set"::: ) (Bool "for" (Set (Var "c")) "being" ($#v1_xcmplx_0 :::"complex"::: ) ($#m1_hidden :::"number"::: ) (Bool "for" (Set (Var "f")) "being" ($#m1_subset_1 :::"PartFunc":::) "of" (Set (Var "X")) "," (Set (Var "Y")) "holds" (Bool (Set ($#k9_xtuple_0 :::"dom"::: ) (Set "(" (Set (Var "f")) ($#k36_valued_2 :::"[-]"::: ) (Set (Var "c")) ")" )) ($#r1_hidden :::"="::: ) (Set ($#k1_relset_1 :::"dom"::: ) (Set (Var "f")))))))) ; theorem :: VALUED_2:48 (Bool "for" (Set (Var "X")) "," (Set (Var "x")) "being" ($#m1_hidden :::"set"::: ) (Bool "for" (Set (Var "Y")) "being" ($#v1_valued_2 :::"complex-functions-membered"::: ) ($#m1_hidden :::"set"::: ) (Bool "for" (Set (Var "c")) "being" ($#v1_xcmplx_0 :::"complex"::: ) ($#m1_hidden :::"number"::: ) (Bool "for" (Set (Var "f")) "being" ($#m1_subset_1 :::"PartFunc":::) "of" (Set (Var "X")) "," (Set (Var "Y")) "st" (Bool (Bool (Set (Var "x")) ($#r2_hidden :::"in"::: ) (Set ($#k9_xtuple_0 :::"dom"::: ) (Set "(" (Set (Var "f")) ($#k36_valued_2 :::"[-]"::: ) (Set (Var "c")) ")" )))) "holds" (Bool (Set (Set "(" (Set (Var "f")) ($#k36_valued_2 :::"[-]"::: ) (Set (Var "c")) ")" ) ($#k1_funct_1 :::"."::: ) (Set (Var "x"))) ($#r1_hidden :::"="::: ) (Set (Set "(" (Set (Var "f")) ($#k1_funct_1 :::"."::: ) (Set (Var "x")) ")" ) ($#k13_valued_1 :::"-"::: ) (Set (Var "c")))))))) ; definitionlet "X" be ($#m1_hidden :::"set"::: ) ; let "Y" be ($#v1_valued_2 :::"complex-functions-membered"::: ) ($#m1_hidden :::"set"::: ) ; let "f" be ($#m1_subset_1 :::"PartFunc":::) "of" (Set (Const "X")) "," (Set (Const "Y")); let "c" be ($#v1_xcmplx_0 :::"complex"::: ) ($#m1_hidden :::"number"::: ) ; :: original: :::"[-]"::: redefine func "f" :::"[-]"::: "c" -> ($#m1_subset_1 :::"PartFunc":::) "of" "X" "," (Set "(" ($#k2_valued_2 :::"C_PFuncs"::: ) (Set "(" ($#k1_valued_2 :::"DOMS"::: ) "Y" ")" ) ")" ); end; definitionlet "X" be ($#m1_hidden :::"set"::: ) ; let "Y" be ($#v3_valued_2 :::"real-functions-membered"::: ) ($#m1_hidden :::"set"::: ) ; let "f" be ($#m1_subset_1 :::"PartFunc":::) "of" (Set (Const "X")) "," (Set (Const "Y")); let "c" be ($#v1_xreal_0 :::"real"::: ) ($#m1_hidden :::"number"::: ) ; :: original: :::"[-]"::: redefine func "f" :::"[-]"::: "c" -> ($#m1_subset_1 :::"PartFunc":::) "of" "X" "," (Set "(" ($#k6_valued_2 :::"R_PFuncs"::: ) (Set "(" ($#k1_valued_2 :::"DOMS"::: ) "Y" ")" ) ")" ); end; definitionlet "X" be ($#m1_hidden :::"set"::: ) ; let "Y" be ($#v4_valued_2 :::"rational-functions-membered"::: ) ($#m1_hidden :::"set"::: ) ; let "f" be ($#m1_subset_1 :::"PartFunc":::) "of" (Set (Const "X")) "," (Set (Const "Y")); let "c" be ($#v1_rat_1 :::"rational"::: ) ($#m1_hidden :::"number"::: ) ; :: original: :::"[-]"::: redefine func "f" :::"[-]"::: "c" -> ($#m1_subset_1 :::"PartFunc":::) "of" "X" "," (Set "(" ($#k8_valued_2 :::"Q_PFuncs"::: ) (Set "(" ($#k1_valued_2 :::"DOMS"::: ) "Y" ")" ) ")" ); end; definitionlet "X" be ($#m1_hidden :::"set"::: ) ; let "Y" be ($#v5_valued_2 :::"integer-functions-membered"::: ) ($#m1_hidden :::"set"::: ) ; let "f" be ($#m1_subset_1 :::"PartFunc":::) "of" (Set (Const "X")) "," (Set (Const "Y")); let "c" be ($#v1_int_1 :::"integer"::: ) ($#m1_hidden :::"number"::: ) ; :: original: :::"[-]"::: redefine func "f" :::"[-]"::: "c" -> ($#m1_subset_1 :::"PartFunc":::) "of" "X" "," (Set "(" ($#k10_valued_2 :::"I_PFuncs"::: ) (Set "(" ($#k1_valued_2 :::"DOMS"::: ) "Y" ")" ) ")" ); end; theorem :: VALUED_2:49 (Bool "for" (Set (Var "X")) "being" ($#m1_hidden :::"set"::: ) (Bool "for" (Set (Var "Y")) "being" ($#v1_valued_2 :::"complex-functions-membered"::: ) ($#m1_hidden :::"set"::: ) (Bool "for" (Set (Var "c1")) "," (Set (Var "c2")) "being" ($#v1_xcmplx_0 :::"complex"::: ) ($#m1_hidden :::"number"::: ) (Bool "for" (Set (Var "f")) "being" ($#m1_subset_1 :::"PartFunc":::) "of" (Set (Var "X")) "," (Set (Var "Y")) "st" (Bool (Bool (Set (Var "f")) ($#r1_hidden :::"<>"::: ) (Set ($#k1_xboole_0 :::"{}"::: ) )) & (Bool (Set (Var "f")) "is" ($#v2_relat_1 :::"non-empty"::: ) ) & (Bool (Set (Set (Var "f")) ($#k37_valued_2 :::"[-]"::: ) (Set (Var "c1"))) ($#r2_relset_1 :::"="::: ) (Set (Set (Var "f")) ($#k37_valued_2 :::"[-]"::: ) (Set (Var "c2"))))) "holds" (Bool (Set (Var "c1")) ($#r1_hidden :::"="::: ) (Set (Var "c2"))))))) ; theorem :: VALUED_2:50 (Bool "for" (Set (Var "X")) "being" ($#m1_hidden :::"set"::: ) (Bool "for" (Set (Var "Y")) "being" ($#v1_valued_2 :::"complex-functions-membered"::: ) ($#m1_hidden :::"set"::: ) (Bool "for" (Set (Var "c1")) "," (Set (Var "c2")) "being" ($#v1_xcmplx_0 :::"complex"::: ) ($#m1_hidden :::"number"::: ) (Bool "for" (Set (Var "f")) "being" ($#m1_subset_1 :::"PartFunc":::) "of" (Set (Var "X")) "," (Set (Var "Y")) "holds" (Bool (Set (Set "(" (Set (Var "f")) ($#k31_valued_2 :::"[+]"::: ) (Set (Var "c1")) ")" ) ($#k37_valued_2 :::"[-]"::: ) (Set (Var "c2"))) ($#r1_hidden :::"="::: ) (Set (Set (Var "f")) ($#k31_valued_2 :::"[+]"::: ) (Set "(" (Set (Var "c1")) ($#k6_xcmplx_0 :::"-"::: ) (Set (Var "c2")) ")" ))))))) ; theorem :: VALUED_2:51 (Bool "for" (Set (Var "X")) "being" ($#m1_hidden :::"set"::: ) (Bool "for" (Set (Var "Y")) "being" ($#v1_valued_2 :::"complex-functions-membered"::: ) ($#m1_hidden :::"set"::: ) (Bool "for" (Set (Var "c1")) "," (Set (Var "c2")) "being" ($#v1_xcmplx_0 :::"complex"::: ) ($#m1_hidden :::"number"::: ) (Bool "for" (Set (Var "f")) "being" ($#m1_subset_1 :::"PartFunc":::) "of" (Set (Var "X")) "," (Set (Var "Y")) "holds" (Bool (Set (Set "(" (Set (Var "f")) ($#k37_valued_2 :::"[-]"::: ) (Set (Var "c1")) ")" ) ($#k31_valued_2 :::"[+]"::: ) (Set (Var "c2"))) ($#r1_hidden :::"="::: ) (Set (Set (Var "f")) ($#k37_valued_2 :::"[-]"::: ) (Set "(" (Set (Var "c1")) ($#k6_xcmplx_0 :::"-"::: ) (Set (Var "c2")) ")" ))))))) ; theorem :: VALUED_2:52 (Bool "for" (Set (Var "X")) "being" ($#m1_hidden :::"set"::: ) (Bool "for" (Set (Var "Y")) "being" ($#v1_valued_2 :::"complex-functions-membered"::: ) ($#m1_hidden :::"set"::: ) (Bool "for" (Set (Var "c1")) "," (Set (Var "c2")) "being" ($#v1_xcmplx_0 :::"complex"::: ) ($#m1_hidden :::"number"::: ) (Bool "for" (Set (Var "f")) "being" ($#m1_subset_1 :::"PartFunc":::) "of" (Set (Var "X")) "," (Set (Var "Y")) "holds" (Bool (Set (Set "(" (Set (Var "f")) ($#k37_valued_2 :::"[-]"::: ) (Set (Var "c1")) ")" ) ($#k37_valued_2 :::"[-]"::: ) (Set (Var "c2"))) ($#r1_hidden :::"="::: ) (Set (Set (Var "f")) ($#k37_valued_2 :::"[-]"::: ) (Set "(" (Set (Var "c1")) ($#k2_xcmplx_0 :::"+"::: ) (Set (Var "c2")) ")" ))))))) ; definitionlet "Y" be ($#v1_valued_2 :::"complex-functions-membered"::: ) ($#m1_hidden :::"set"::: ) ; let "f" be (Set (Const "Y")) ($#v5_relat_1 :::"-valued"::: ) ($#m1_hidden :::"Function":::); let "c" be ($#v1_xcmplx_0 :::"complex"::: ) ($#m1_hidden :::"number"::: ) ; func "f" :::"[#]"::: "c" -> ($#m1_hidden :::"Function":::) means :: VALUED_2:def 39 (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 "c" ($#k24_valued_1 :::"(#)"::: ) (Set "(" "f" ($#k1_funct_1 :::"."::: ) (Set (Var "x")) ")" ))) ")" ) ")" ); end; :: deftheorem defines :::"[#]"::: VALUED_2:def 39 : (Bool "for" (Set (Var "Y")) "being" ($#v1_valued_2 :::"complex-functions-membered"::: ) ($#m1_hidden :::"set"::: ) (Bool "for" (Set (Var "f")) "being" (Set (Var "b1")) ($#v5_relat_1 :::"-valued"::: ) ($#m1_hidden :::"Function":::) (Bool "for" (Set (Var "c")) "being" ($#v1_xcmplx_0 :::"complex"::: ) ($#m1_hidden :::"number"::: ) (Bool "for" (Set (Var "b4")) "being" ($#m1_hidden :::"Function":::) "holds" (Bool "(" (Bool (Set (Var "b4")) ($#r1_hidden :::"="::: ) (Set (Set (Var "f")) ($#k41_valued_2 :::"[#]"::: ) (Set (Var "c")))) "iff" (Bool "(" (Bool (Set ($#k9_xtuple_0 :::"dom"::: ) (Set (Var "b4"))) ($#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 "b4"))))) "holds" (Bool (Set (Set (Var "b4")) ($#k1_funct_1 :::"."::: ) (Set (Var "x"))) ($#r1_hidden :::"="::: ) (Set (Set (Var "c")) ($#k24_valued_1 :::"(#)"::: ) (Set "(" (Set (Var "f")) ($#k1_funct_1 :::"."::: ) (Set (Var "x")) ")" ))) ")" ) ")" ) ")" ))))); definitionlet "X" be ($#m1_hidden :::"set"::: ) ; let "Y" be ($#v1_valued_2 :::"complex-functions-membered"::: ) ($#m1_hidden :::"set"::: ) ; let "f" be ($#m1_subset_1 :::"PartFunc":::) "of" (Set (Const "X")) "," (Set (Const "Y")); let "c" be ($#v1_xcmplx_0 :::"complex"::: ) ($#m1_hidden :::"number"::: ) ; :: original: :::"[#]"::: redefine func "f" :::"[#]"::: "c" -> ($#m1_subset_1 :::"PartFunc":::) "of" "X" "," (Set "(" ($#k2_valued_2 :::"C_PFuncs"::: ) (Set "(" ($#k1_valued_2 :::"DOMS"::: ) "Y" ")" ) ")" ); end; definitionlet "X" be ($#m1_hidden :::"set"::: ) ; let "Y" be ($#v3_valued_2 :::"real-functions-membered"::: ) ($#m1_hidden :::"set"::: ) ; let "f" be ($#m1_subset_1 :::"PartFunc":::) "of" (Set (Const "X")) "," (Set (Const "Y")); let "c" be ($#v1_xreal_0 :::"real"::: ) ($#m1_hidden :::"number"::: ) ; :: original: :::"[#]"::: redefine func "f" :::"[#]"::: "c" -> ($#m1_subset_1 :::"PartFunc":::) "of" "X" "," (Set "(" ($#k6_valued_2 :::"R_PFuncs"::: ) (Set "(" ($#k1_valued_2 :::"DOMS"::: ) "Y" ")" ) ")" ); end; definitionlet "X" be ($#m1_hidden :::"set"::: ) ; let "Y" be ($#v4_valued_2 :::"rational-functions-membered"::: ) ($#m1_hidden :::"set"::: ) ; let "f" be ($#m1_subset_1 :::"PartFunc":::) "of" (Set (Const "X")) "," (Set (Const "Y")); let "c" be ($#v1_rat_1 :::"rational"::: ) ($#m1_hidden :::"number"::: ) ; :: original: :::"[#]"::: redefine func "f" :::"[#]"::: "c" -> ($#m1_subset_1 :::"PartFunc":::) "of" "X" "," (Set "(" ($#k8_valued_2 :::"Q_PFuncs"::: ) (Set "(" ($#k1_valued_2 :::"DOMS"::: ) "Y" ")" ) ")" ); end; definitionlet "X" be ($#m1_hidden :::"set"::: ) ; let "Y" be ($#v5_valued_2 :::"integer-functions-membered"::: ) ($#m1_hidden :::"set"::: ) ; let "f" be ($#m1_subset_1 :::"PartFunc":::) "of" (Set (Const "X")) "," (Set (Const "Y")); let "c" be ($#v1_int_1 :::"integer"::: ) ($#m1_hidden :::"number"::: ) ; :: original: :::"[#]"::: redefine func "f" :::"[#]"::: "c" -> ($#m1_subset_1 :::"PartFunc":::) "of" "X" "," (Set "(" ($#k10_valued_2 :::"I_PFuncs"::: ) (Set "(" ($#k1_valued_2 :::"DOMS"::: ) "Y" ")" ) ")" ); end; definitionlet "X" be ($#m1_hidden :::"set"::: ) ; let "Y" be ($#v6_valued_2 :::"natural-functions-membered"::: ) ($#m1_hidden :::"set"::: ) ; let "f" be ($#m1_subset_1 :::"PartFunc":::) "of" (Set (Const "X")) "," (Set (Const "Y")); let "c" be ($#m1_hidden :::"Nat":::); :: original: :::"[#]"::: redefine func "f" :::"[#]"::: "c" -> ($#m1_subset_1 :::"PartFunc":::) "of" "X" "," (Set "(" ($#k12_valued_2 :::"N_PFuncs"::: ) (Set "(" ($#k1_valued_2 :::"DOMS"::: ) "Y" ")" ) ")" ); end; theorem :: VALUED_2:53 (Bool "for" (Set (Var "X")) "being" ($#m1_hidden :::"set"::: ) (Bool "for" (Set (Var "Y")) "being" ($#v1_valued_2 :::"complex-functions-membered"::: ) ($#m1_hidden :::"set"::: ) (Bool "for" (Set (Var "c1")) "," (Set (Var "c2")) "being" ($#v1_xcmplx_0 :::"complex"::: ) ($#m1_hidden :::"number"::: ) (Bool "for" (Set (Var "f")) "being" ($#m1_subset_1 :::"PartFunc":::) "of" (Set (Var "X")) "," (Set (Var "Y")) "holds" (Bool (Set (Set "(" (Set (Var "f")) ($#k42_valued_2 :::"[#]"::: ) (Set (Var "c1")) ")" ) ($#k42_valued_2 :::"[#]"::: ) (Set (Var "c2"))) ($#r1_hidden :::"="::: ) (Set (Set (Var "f")) ($#k42_valued_2 :::"[#]"::: ) (Set "(" (Set (Var "c1")) ($#k3_xcmplx_0 :::"*"::: ) (Set (Var "c2")) ")" ))))))) ; theorem :: VALUED_2:54 (Bool "for" (Set (Var "X")) "being" ($#m1_hidden :::"set"::: ) (Bool "for" (Set (Var "Y")) "being" ($#v1_valued_2 :::"complex-functions-membered"::: ) ($#m1_hidden :::"set"::: ) (Bool "for" (Set (Var "c1")) "," (Set (Var "c2")) "being" ($#v1_xcmplx_0 :::"complex"::: ) ($#m1_hidden :::"number"::: ) (Bool "for" (Set (Var "f")) "being" ($#m1_subset_1 :::"PartFunc":::) "of" (Set (Var "X")) "," (Set (Var "Y")) "st" (Bool (Bool (Set (Var "f")) ($#r1_hidden :::"<>"::: ) (Set ($#k1_xboole_0 :::"{}"::: ) )) & (Bool (Set (Var "f")) "is" ($#v2_relat_1 :::"non-empty"::: ) ) & (Bool "(" "for" (Set (Var "x")) "being" ($#m1_hidden :::"set"::: ) "st" (Bool (Bool (Set (Var "x")) ($#r2_hidden :::"in"::: ) (Set ($#k1_relset_1 :::"dom"::: ) (Set (Var "f"))))) "holds" (Bool (Set (Set (Var "f")) ($#k1_funct_1 :::"."::: ) (Set (Var "x"))) "is" ($#v2_relat_1 :::"non-empty"::: ) ) ")" ) & (Bool (Set (Set (Var "f")) ($#k42_valued_2 :::"[#]"::: ) (Set (Var "c1"))) ($#r2_relset_1 :::"="::: ) (Set (Set (Var "f")) ($#k42_valued_2 :::"[#]"::: ) (Set (Var "c2"))))) "holds" (Bool (Set (Var "c1")) ($#r1_hidden :::"="::: ) (Set (Var "c2"))))))) ; definitionlet "Y" be ($#v1_valued_2 :::"complex-functions-membered"::: ) ($#m1_hidden :::"set"::: ) ; let "f" be (Set (Const "Y")) ($#v5_relat_1 :::"-valued"::: ) ($#m1_hidden :::"Function":::); let "c" be ($#v1_xcmplx_0 :::"complex"::: ) ($#m1_hidden :::"number"::: ) ; func "f" :::"[/]"::: "c" -> ($#m1_hidden :::"Function":::) equals :: VALUED_2:def 40 (Set "f" ($#k41_valued_2 :::"[#]"::: ) (Set "(" "c" ($#k5_xcmplx_0 :::"""::: ) ")" )); end; :: deftheorem defines :::"[/]"::: VALUED_2:def 40 : (Bool "for" (Set (Var "Y")) "being" ($#v1_valued_2 :::"complex-functions-membered"::: ) ($#m1_hidden :::"set"::: ) (Bool "for" (Set (Var "f")) "being" (Set (Var "b1")) ($#v5_relat_1 :::"-valued"::: ) ($#m1_hidden :::"Function":::) (Bool "for" (Set (Var "c")) "being" ($#v1_xcmplx_0 :::"complex"::: ) ($#m1_hidden :::"number"::: ) "holds" (Bool (Set (Set (Var "f")) ($#k47_valued_2 :::"[/]"::: ) (Set (Var "c"))) ($#r1_hidden :::"="::: ) (Set (Set (Var "f")) ($#k41_valued_2 :::"[#]"::: ) (Set "(" (Set (Var "c")) ($#k5_xcmplx_0 :::"""::: ) ")" )))))); theorem :: VALUED_2:55 (Bool "for" (Set (Var "X")) "being" ($#m1_hidden :::"set"::: ) (Bool "for" (Set (Var "Y")) "being" ($#v1_valued_2 :::"complex-functions-membered"::: ) ($#m1_hidden :::"set"::: ) (Bool "for" (Set (Var "c")) "being" ($#v1_xcmplx_0 :::"complex"::: ) ($#m1_hidden :::"number"::: ) (Bool "for" (Set (Var "f")) "being" ($#m1_subset_1 :::"PartFunc":::) "of" (Set (Var "X")) "," (Set (Var "Y")) "holds" (Bool (Set ($#k9_xtuple_0 :::"dom"::: ) (Set "(" (Set (Var "f")) ($#k47_valued_2 :::"[/]"::: ) (Set (Var "c")) ")" )) ($#r1_hidden :::"="::: ) (Set ($#k1_relset_1 :::"dom"::: ) (Set (Var "f")))))))) ; theorem :: VALUED_2:56 (Bool "for" (Set (Var "X")) "," (Set (Var "x")) "being" ($#m1_hidden :::"set"::: ) (Bool "for" (Set (Var "Y")) "being" ($#v1_valued_2 :::"complex-functions-membered"::: ) ($#m1_hidden :::"set"::: ) (Bool "for" (Set (Var "c")) "being" ($#v1_xcmplx_0 :::"complex"::: ) ($#m1_hidden :::"number"::: ) (Bool "for" (Set (Var "f")) "being" ($#m1_subset_1 :::"PartFunc":::) "of" (Set (Var "X")) "," (Set (Var "Y")) "st" (Bool (Bool (Set (Var "x")) ($#r2_hidden :::"in"::: ) (Set ($#k9_xtuple_0 :::"dom"::: ) (Set "(" (Set (Var "f")) ($#k47_valued_2 :::"[/]"::: ) (Set (Var "c")) ")" )))) "holds" (Bool (Set (Set "(" (Set (Var "f")) ($#k47_valued_2 :::"[/]"::: ) (Set (Var "c")) ")" ) ($#k1_funct_1 :::"."::: ) (Set (Var "x"))) ($#r1_hidden :::"="::: ) (Set (Set "(" (Set (Var "c")) ($#k5_xcmplx_0 :::"""::: ) ")" ) ($#k24_valued_1 :::"(#)"::: ) (Set "(" (Set (Var "f")) ($#k1_funct_1 :::"."::: ) (Set (Var "x")) ")" ))))))) ; definitionlet "X" be ($#m1_hidden :::"set"::: ) ; let "Y" be ($#v1_valued_2 :::"complex-functions-membered"::: ) ($#m1_hidden :::"set"::: ) ; let "f" be ($#m1_subset_1 :::"PartFunc":::) "of" (Set (Const "X")) "," (Set (Const "Y")); let "c" be ($#v1_xcmplx_0 :::"complex"::: ) ($#m1_hidden :::"number"::: ) ; :: original: :::"[/]"::: redefine func "f" :::"[/]"::: "c" -> ($#m1_subset_1 :::"PartFunc":::) "of" "X" "," (Set "(" ($#k2_valued_2 :::"C_PFuncs"::: ) (Set "(" ($#k1_valued_2 :::"DOMS"::: ) "Y" ")" ) ")" ); end; definitionlet "X" be ($#m1_hidden :::"set"::: ) ; let "Y" be ($#v3_valued_2 :::"real-functions-membered"::: ) ($#m1_hidden :::"set"::: ) ; let "f" be ($#m1_subset_1 :::"PartFunc":::) "of" (Set (Const "X")) "," (Set (Const "Y")); let "c" be ($#v1_xreal_0 :::"real"::: ) ($#m1_hidden :::"number"::: ) ; :: original: :::"[/]"::: redefine func "f" :::"[/]"::: "c" -> ($#m1_subset_1 :::"PartFunc":::) "of" "X" "," (Set "(" ($#k6_valued_2 :::"R_PFuncs"::: ) (Set "(" ($#k1_valued_2 :::"DOMS"::: ) "Y" ")" ) ")" ); end; definitionlet "X" be ($#m1_hidden :::"set"::: ) ; let "Y" be ($#v4_valued_2 :::"rational-functions-membered"::: ) ($#m1_hidden :::"set"::: ) ; let "f" be ($#m1_subset_1 :::"PartFunc":::) "of" (Set (Const "X")) "," (Set (Const "Y")); let "c" be ($#v1_rat_1 :::"rational"::: ) ($#m1_hidden :::"number"::: ) ; :: original: :::"[/]"::: redefine func "f" :::"[/]"::: "c" -> ($#m1_subset_1 :::"PartFunc":::) "of" "X" "," (Set "(" ($#k8_valued_2 :::"Q_PFuncs"::: ) (Set "(" ($#k1_valued_2 :::"DOMS"::: ) "Y" ")" ) ")" ); end; theorem :: VALUED_2:57 (Bool "for" (Set (Var "X")) "being" ($#m1_hidden :::"set"::: ) (Bool "for" (Set (Var "Y")) "being" ($#v1_valued_2 :::"complex-functions-membered"::: ) ($#m1_hidden :::"set"::: ) (Bool "for" (Set (Var "c1")) "," (Set (Var "c2")) "being" ($#v1_xcmplx_0 :::"complex"::: ) ($#m1_hidden :::"number"::: ) (Bool "for" (Set (Var "f")) "being" ($#m1_subset_1 :::"PartFunc":::) "of" (Set (Var "X")) "," (Set (Var "Y")) "holds" (Bool (Set (Set "(" (Set (Var "f")) ($#k48_valued_2 :::"[/]"::: ) (Set (Var "c1")) ")" ) ($#k48_valued_2 :::"[/]"::: ) (Set (Var "c2"))) ($#r1_hidden :::"="::: ) (Set (Set (Var "f")) ($#k48_valued_2 :::"[/]"::: ) (Set "(" (Set (Var "c1")) ($#k3_xcmplx_0 :::"*"::: ) (Set (Var "c2")) ")" ))))))) ; theorem :: VALUED_2:58 (Bool "for" (Set (Var "X")) "being" ($#m1_hidden :::"set"::: ) (Bool "for" (Set (Var "Y")) "being" ($#v1_valued_2 :::"complex-functions-membered"::: ) ($#m1_hidden :::"set"::: ) (Bool "for" (Set (Var "c1")) "," (Set (Var "c2")) "being" ($#v1_xcmplx_0 :::"complex"::: ) ($#m1_hidden :::"number"::: ) (Bool "for" (Set (Var "f")) "being" ($#m1_subset_1 :::"PartFunc":::) "of" (Set (Var "X")) "," (Set (Var "Y")) "st" (Bool (Bool (Set (Var "f")) ($#r1_hidden :::"<>"::: ) (Set ($#k1_xboole_0 :::"{}"::: ) )) & (Bool (Set (Var "f")) "is" ($#v2_relat_1 :::"non-empty"::: ) ) & (Bool "(" "for" (Set (Var "x")) "being" ($#m1_hidden :::"set"::: ) "st" (Bool (Bool (Set (Var "x")) ($#r2_hidden :::"in"::: ) (Set ($#k1_relset_1 :::"dom"::: ) (Set (Var "f"))))) "holds" (Bool (Set (Set (Var "f")) ($#k1_funct_1 :::"."::: ) (Set (Var "x"))) "is" ($#v2_relat_1 :::"non-empty"::: ) ) ")" ) & (Bool (Set (Set (Var "f")) ($#k48_valued_2 :::"[/]"::: ) (Set (Var "c1"))) ($#r2_relset_1 :::"="::: ) (Set (Set (Var "f")) ($#k48_valued_2 :::"[/]"::: ) (Set (Var "c2"))))) "holds" (Bool (Set (Var "c1")) ($#r1_hidden :::"="::: ) (Set (Var "c2"))))))) ; definitionlet "Y" be ($#v1_valued_2 :::"complex-functions-membered"::: ) ($#m1_hidden :::"set"::: ) ; let "f" be (Set (Const "Y")) ($#v5_relat_1 :::"-valued"::: ) ($#m1_hidden :::"Function":::); let "g" be ($#v1_valued_0 :::"complex-valued"::: ) ($#m1_hidden :::"Function":::); func "f" :::"<+>"::: "g" -> ($#m1_hidden :::"Function":::) means :: VALUED_2:def 41 (Bool "(" (Bool (Set ($#k9_xtuple_0 :::"dom"::: ) it) ($#r1_hidden :::"="::: ) (Set (Set "(" ($#k9_xtuple_0 :::"dom"::: ) "f" ")" ) ($#k3_xboole_0 :::"/\"::: ) (Set "(" ($#k9_xtuple_0 :::"dom"::: ) "g" ")" ))) & (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 (Set "(" "f" ($#k1_funct_1 :::"."::: ) (Set (Var "x")) ")" ) ($#k7_valued_1 :::"+"::: ) (Set "(" "g" ($#k1_funct_1 :::"."::: ) (Set (Var "x")) ")" ))) ")" ) ")" ); end; :: deftheorem defines :::"<+>"::: VALUED_2:def 41 : (Bool "for" (Set (Var "Y")) "being" ($#v1_valued_2 :::"complex-functions-membered"::: ) ($#m1_hidden :::"set"::: ) (Bool "for" (Set (Var "f")) "being" (Set (Var "b1")) ($#v5_relat_1 :::"-valued"::: ) ($#m1_hidden :::"Function":::) (Bool "for" (Set (Var "g")) "being" ($#v1_valued_0 :::"complex-valued"::: ) ($#m1_hidden :::"Function":::) (Bool "for" (Set (Var "b4")) "being" ($#m1_hidden :::"Function":::) "holds" (Bool "(" (Bool (Set (Var "b4")) ($#r1_hidden :::"="::: ) (Set (Set (Var "f")) ($#k51_valued_2 :::"<+>"::: ) (Set (Var "g")))) "iff" (Bool "(" (Bool (Set ($#k9_xtuple_0 :::"dom"::: ) (Set (Var "b4"))) ($#r1_hidden :::"="::: ) (Set (Set "(" ($#k9_xtuple_0 :::"dom"::: ) (Set (Var "f")) ")" ) ($#k3_xboole_0 :::"/\"::: ) (Set "(" ($#k9_xtuple_0 :::"dom"::: ) (Set (Var "g")) ")" ))) & (Bool "(" "for" (Set (Var "x")) "being" ($#m1_hidden :::"set"::: ) "st" (Bool (Bool (Set (Var "x")) ($#r2_hidden :::"in"::: ) (Set ($#k9_xtuple_0 :::"dom"::: ) (Set (Var "b4"))))) "holds" (Bool (Set (Set (Var "b4")) ($#k1_funct_1 :::"."::: ) (Set (Var "x"))) ($#r1_hidden :::"="::: ) (Set (Set "(" (Set (Var "f")) ($#k1_funct_1 :::"."::: ) (Set (Var "x")) ")" ) ($#k7_valued_1 :::"+"::: ) (Set "(" (Set (Var "g")) ($#k1_funct_1 :::"."::: ) (Set (Var "x")) ")" ))) ")" ) ")" ) ")" ))))); definitionlet "X" be ($#m1_hidden :::"set"::: ) ; let "Y" be ($#v1_valued_2 :::"complex-functions-membered"::: ) ($#m1_hidden :::"set"::: ) ; let "f" be ($#m1_subset_1 :::"PartFunc":::) "of" (Set (Const "X")) "," (Set (Const "Y")); let "g" be ($#v1_valued_0 :::"complex-valued"::: ) ($#m1_hidden :::"Function":::); :: original: :::"<+>"::: redefine func "f" :::"<+>"::: "g" -> ($#m1_subset_1 :::"PartFunc":::) "of" (Set "(" "X" ($#k3_xboole_0 :::"/\"::: ) (Set "(" ($#k9_xtuple_0 :::"dom"::: ) "g" ")" ) ")" ) "," (Set "(" ($#k2_valued_2 :::"C_PFuncs"::: ) (Set "(" ($#k1_valued_2 :::"DOMS"::: ) "Y" ")" ) ")" ); end; definitionlet "X" be ($#m1_hidden :::"set"::: ) ; let "Y" be ($#v3_valued_2 :::"real-functions-membered"::: ) ($#m1_hidden :::"set"::: ) ; let "f" be ($#m1_subset_1 :::"PartFunc":::) "of" (Set (Const "X")) "," (Set (Const "Y")); let "g" be ($#v3_valued_0 :::"real-valued"::: ) ($#m1_hidden :::"Function":::); :: original: :::"<+>"::: redefine func "f" :::"<+>"::: "g" -> ($#m1_subset_1 :::"PartFunc":::) "of" (Set "(" "X" ($#k3_xboole_0 :::"/\"::: ) (Set "(" ($#k9_xtuple_0 :::"dom"::: ) "g" ")" ) ")" ) "," (Set "(" ($#k6_valued_2 :::"R_PFuncs"::: ) (Set "(" ($#k1_valued_2 :::"DOMS"::: ) "Y" ")" ) ")" ); end; definitionlet "X" be ($#m1_hidden :::"set"::: ) ; let "Y" be ($#v4_valued_2 :::"rational-functions-membered"::: ) ($#m1_hidden :::"set"::: ) ; let "f" be ($#m1_subset_1 :::"PartFunc":::) "of" (Set (Const "X")) "," (Set (Const "Y")); let "g" be (Set ($#k3_numbers :::"RAT"::: ) ) ($#v5_relat_1 :::"-valued"::: ) ($#m1_hidden :::"Function":::); :: original: :::"<+>"::: redefine func "f" :::"<+>"::: "g" -> ($#m1_subset_1 :::"PartFunc":::) "of" (Set "(" "X" ($#k3_xboole_0 :::"/\"::: ) (Set "(" ($#k9_xtuple_0 :::"dom"::: ) "g" ")" ) ")" ) "," (Set "(" ($#k8_valued_2 :::"Q_PFuncs"::: ) (Set "(" ($#k1_valued_2 :::"DOMS"::: ) "Y" ")" ) ")" ); end; definitionlet "X" be ($#m1_hidden :::"set"::: ) ; let "Y" be ($#v5_valued_2 :::"integer-functions-membered"::: ) ($#m1_hidden :::"set"::: ) ; let "f" be ($#m1_subset_1 :::"PartFunc":::) "of" (Set (Const "X")) "," (Set (Const "Y")); let "g" be (Set ($#k4_numbers :::"INT"::: ) ) ($#v5_relat_1 :::"-valued"::: ) ($#m1_hidden :::"Function":::); :: original: :::"<+>"::: redefine func "f" :::"<+>"::: "g" -> ($#m1_subset_1 :::"PartFunc":::) "of" (Set "(" "X" ($#k3_xboole_0 :::"/\"::: ) (Set "(" ($#k9_xtuple_0 :::"dom"::: ) "g" ")" ) ")" ) "," (Set "(" ($#k10_valued_2 :::"I_PFuncs"::: ) (Set "(" ($#k1_valued_2 :::"DOMS"::: ) "Y" ")" ) ")" ); end; definitionlet "X" be ($#m1_hidden :::"set"::: ) ; let "Y" be ($#v6_valued_2 :::"natural-functions-membered"::: ) ($#m1_hidden :::"set"::: ) ; let "f" be ($#m1_subset_1 :::"PartFunc":::) "of" (Set (Const "X")) "," (Set (Const "Y")); let "g" be ($#v4_valued_0 :::"natural-valued"::: ) ($#m1_hidden :::"Function":::); :: original: :::"<+>"::: redefine func "f" :::"<+>"::: "g" -> ($#m1_subset_1 :::"PartFunc":::) "of" (Set "(" "X" ($#k3_xboole_0 :::"/\"::: ) (Set "(" ($#k9_xtuple_0 :::"dom"::: ) "g" ")" ) ")" ) "," (Set "(" ($#k12_valued_2 :::"N_PFuncs"::: ) (Set "(" ($#k1_valued_2 :::"DOMS"::: ) "Y" ")" ) ")" ); end; theorem :: VALUED_2:59 (Bool "for" (Set (Var "X")) "being" ($#m1_hidden :::"set"::: ) (Bool "for" (Set (Var "Y")) "being" ($#v1_valued_2 :::"complex-functions-membered"::: ) ($#m1_hidden :::"set"::: ) (Bool "for" (Set (Var "f")) "being" ($#m1_subset_1 :::"PartFunc":::) "of" (Set (Var "X")) "," (Set (Var "Y")) (Bool "for" (Set (Var "g")) "," (Set (Var "h")) "being" ($#v1_valued_0 :::"complex-valued"::: ) ($#m1_hidden :::"Function":::) "holds" (Bool (Set (Set "(" (Set (Var "f")) ($#k52_valued_2 :::"<+>"::: ) (Set (Var "g")) ")" ) ($#k52_valued_2 :::"<+>"::: ) (Set (Var "h"))) ($#r1_hidden :::"="::: ) (Set (Set (Var "f")) ($#k52_valued_2 :::"<+>"::: ) (Set "(" (Set (Var "g")) ($#k1_valued_1 :::"+"::: ) (Set (Var "h")) ")" ))))))) ; theorem :: VALUED_2:60 (Bool "for" (Set (Var "X")) "being" ($#m1_hidden :::"set"::: ) (Bool "for" (Set (Var "Y")) "being" ($#v1_valued_2 :::"complex-functions-membered"::: ) ($#m1_hidden :::"set"::: ) (Bool "for" (Set (Var "f")) "being" ($#m1_subset_1 :::"PartFunc":::) "of" (Set (Var "X")) "," (Set (Var "Y")) (Bool "for" (Set (Var "g")) "being" ($#v1_valued_0 :::"complex-valued"::: ) ($#m1_hidden :::"Function":::) "holds" (Bool (Set ($#k16_valued_2 :::"<->"::: ) (Set "(" (Set (Var "f")) ($#k52_valued_2 :::"<+>"::: ) (Set (Var "g")) ")" )) ($#r1_hidden :::"="::: ) (Set (Set "(" ($#k16_valued_2 :::"<->"::: ) (Set (Var "f")) ")" ) ($#k52_valued_2 :::"<+>"::: ) (Set "(" ($#k30_valued_1 :::"-"::: ) (Set (Var "g")) ")" ))))))) ; definitionlet "Y" be ($#v1_valued_2 :::"complex-functions-membered"::: ) ($#m1_hidden :::"set"::: ) ; let "f" be (Set (Const "Y")) ($#v5_relat_1 :::"-valued"::: ) ($#m1_hidden :::"Function":::); let "g" be ($#v1_valued_0 :::"complex-valued"::: ) ($#m1_hidden :::"Function":::); func "f" :::"<->"::: "g" -> ($#m1_hidden :::"Function":::) equals :: VALUED_2:def 42 (Set "f" ($#k51_valued_2 :::"<+>"::: ) (Set "(" ($#k30_valued_1 :::"-"::: ) "g" ")" )); end; :: deftheorem defines :::"<->"::: VALUED_2:def 42 : (Bool "for" (Set (Var "Y")) "being" ($#v1_valued_2 :::"complex-functions-membered"::: ) ($#m1_hidden :::"set"::: ) (Bool "for" (Set (Var "f")) "being" (Set (Var "b1")) ($#v5_relat_1 :::"-valued"::: ) ($#m1_hidden :::"Function":::) (Bool "for" (Set (Var "g")) "being" ($#v1_valued_0 :::"complex-valued"::: ) ($#m1_hidden :::"Function":::) "holds" (Bool (Set (Set (Var "f")) ($#k57_valued_2 :::"<->"::: ) (Set (Var "g"))) ($#r1_hidden :::"="::: ) (Set (Set (Var "f")) ($#k51_valued_2 :::"<+>"::: ) (Set "(" ($#k30_valued_1 :::"-"::: ) (Set (Var "g")) ")" )))))); theorem :: VALUED_2:61 (Bool "for" (Set (Var "X")) "being" ($#m1_hidden :::"set"::: ) (Bool "for" (Set (Var "Y")) "being" ($#v1_valued_2 :::"complex-functions-membered"::: ) ($#m1_hidden :::"set"::: ) (Bool "for" (Set (Var "f")) "being" ($#m1_subset_1 :::"PartFunc":::) "of" (Set (Var "X")) "," (Set (Var "Y")) (Bool "for" (Set (Var "g")) "being" ($#v1_valued_0 :::"complex-valued"::: ) ($#m1_hidden :::"Function":::) "holds" (Bool (Set ($#k9_xtuple_0 :::"dom"::: ) (Set "(" (Set (Var "f")) ($#k57_valued_2 :::"<->"::: ) (Set (Var "g")) ")" )) ($#r1_hidden :::"="::: ) (Set (Set "(" ($#k1_relset_1 :::"dom"::: ) (Set (Var "f")) ")" ) ($#k8_subset_1 :::"/\"::: ) (Set "(" ($#k9_xtuple_0 :::"dom"::: ) (Set (Var "g")) ")" ))))))) ; theorem :: VALUED_2:62 (Bool "for" (Set (Var "X")) "," (Set (Var "x")) "being" ($#m1_hidden :::"set"::: ) (Bool "for" (Set (Var "Y")) "being" ($#v1_valued_2 :::"complex-functions-membered"::: ) ($#m1_hidden :::"set"::: ) (Bool "for" (Set (Var "f")) "being" ($#m1_subset_1 :::"PartFunc":::) "of" (Set (Var "X")) "," (Set (Var "Y")) (Bool "for" (Set (Var "g")) "being" ($#v1_valued_0 :::"complex-valued"::: ) ($#m1_hidden :::"Function":::) "st" (Bool (Bool (Set (Var "x")) ($#r2_hidden :::"in"::: ) (Set ($#k9_xtuple_0 :::"dom"::: ) (Set "(" (Set (Var "f")) ($#k57_valued_2 :::"<->"::: ) (Set (Var "g")) ")" )))) "holds" (Bool (Set (Set "(" (Set (Var "f")) ($#k57_valued_2 :::"<->"::: ) (Set (Var "g")) ")" ) ($#k1_funct_1 :::"."::: ) (Set (Var "x"))) ($#r1_hidden :::"="::: ) (Set (Set "(" (Set (Var "f")) ($#k1_funct_1 :::"."::: ) (Set (Var "x")) ")" ) ($#k13_valued_1 :::"-"::: ) (Set "(" (Set (Var "g")) ($#k1_funct_1 :::"."::: ) (Set (Var "x")) ")" ))))))) ; definitionlet "X" be ($#m1_hidden :::"set"::: ) ; let "Y" be ($#v1_valued_2 :::"complex-functions-membered"::: ) ($#m1_hidden :::"set"::: ) ; let "f" be ($#m1_subset_1 :::"PartFunc":::) "of" (Set (Const "X")) "," (Set (Const "Y")); let "g" be ($#v1_valued_0 :::"complex-valued"::: ) ($#m1_hidden :::"Function":::); :: original: :::"<->"::: redefine func "f" :::"<->"::: "g" -> ($#m1_subset_1 :::"PartFunc":::) "of" (Set "(" "X" ($#k3_xboole_0 :::"/\"::: ) (Set "(" ($#k9_xtuple_0 :::"dom"::: ) "g" ")" ) ")" ) "," (Set "(" ($#k2_valued_2 :::"C_PFuncs"::: ) (Set "(" ($#k1_valued_2 :::"DOMS"::: ) "Y" ")" ) ")" ); end; definitionlet "X" be ($#m1_hidden :::"set"::: ) ; let "Y" be ($#v3_valued_2 :::"real-functions-membered"::: ) ($#m1_hidden :::"set"::: ) ; let "f" be ($#m1_subset_1 :::"PartFunc":::) "of" (Set (Const "X")) "," (Set (Const "Y")); let "g" be ($#v3_valued_0 :::"real-valued"::: ) ($#m1_hidden :::"Function":::); :: original: :::"<->"::: redefine func "f" :::"<->"::: "g" -> ($#m1_subset_1 :::"PartFunc":::) "of" (Set "(" "X" ($#k3_xboole_0 :::"/\"::: ) (Set "(" ($#k9_xtuple_0 :::"dom"::: ) "g" ")" ) ")" ) "," (Set "(" ($#k6_valued_2 :::"R_PFuncs"::: ) (Set "(" ($#k1_valued_2 :::"DOMS"::: ) "Y" ")" ) ")" ); end; definitionlet "X" be ($#m1_hidden :::"set"::: ) ; let "Y" be ($#v4_valued_2 :::"rational-functions-membered"::: ) ($#m1_hidden :::"set"::: ) ; let "f" be ($#m1_subset_1 :::"PartFunc":::) "of" (Set (Const "X")) "," (Set (Const "Y")); let "g" be (Set ($#k3_numbers :::"RAT"::: ) ) ($#v5_relat_1 :::"-valued"::: ) ($#m1_hidden :::"Function":::); :: original: :::"<->"::: redefine func "f" :::"<->"::: "g" -> ($#m1_subset_1 :::"PartFunc":::) "of" (Set "(" "X" ($#k3_xboole_0 :::"/\"::: ) (Set "(" ($#k9_xtuple_0 :::"dom"::: ) "g" ")" ) ")" ) "," (Set "(" ($#k8_valued_2 :::"Q_PFuncs"::: ) (Set "(" ($#k1_valued_2 :::"DOMS"::: ) "Y" ")" ) ")" ); end; definitionlet "X" be ($#m1_hidden :::"set"::: ) ; let "Y" be ($#v5_valued_2 :::"integer-functions-membered"::: ) ($#m1_hidden :::"set"::: ) ; let "f" be ($#m1_subset_1 :::"PartFunc":::) "of" (Set (Const "X")) "," (Set (Const "Y")); let "g" be (Set ($#k4_numbers :::"INT"::: ) ) ($#v5_relat_1 :::"-valued"::: ) ($#m1_hidden :::"Function":::); :: original: :::"<->"::: redefine func "f" :::"<->"::: "g" -> ($#m1_subset_1 :::"PartFunc":::) "of" (Set "(" "X" ($#k3_xboole_0 :::"/\"::: ) (Set "(" ($#k9_xtuple_0 :::"dom"::: ) "g" ")" ) ")" ) "," (Set "(" ($#k10_valued_2 :::"I_PFuncs"::: ) (Set "(" ($#k1_valued_2 :::"DOMS"::: ) "Y" ")" ) ")" ); end; theorem :: VALUED_2:63 (Bool "for" (Set (Var "X")) "being" ($#m1_hidden :::"set"::: ) (Bool "for" (Set (Var "Y")) "being" ($#v1_valued_2 :::"complex-functions-membered"::: ) ($#m1_hidden :::"set"::: ) (Bool "for" (Set (Var "f")) "being" ($#m1_subset_1 :::"PartFunc":::) "of" (Set (Var "X")) "," (Set (Var "Y")) (Bool "for" (Set (Var "g")) "being" ($#v1_valued_0 :::"complex-valued"::: ) ($#m1_hidden :::"Function":::) "holds" (Bool (Set (Set (Var "f")) ($#k58_valued_2 :::"<->"::: ) (Set "(" ($#k30_valued_1 :::"-"::: ) (Set (Var "g")) ")" )) ($#r1_hidden :::"="::: ) (Set (Set (Var "f")) ($#k52_valued_2 :::"<+>"::: ) (Set (Var "g")))))))) ; theorem :: VALUED_2:64 (Bool "for" (Set (Var "X")) "being" ($#m1_hidden :::"set"::: ) (Bool "for" (Set (Var "Y")) "being" ($#v1_valued_2 :::"complex-functions-membered"::: ) ($#m1_hidden :::"set"::: ) (Bool "for" (Set (Var "f")) "being" ($#m1_subset_1 :::"PartFunc":::) "of" (Set (Var "X")) "," (Set (Var "Y")) (Bool "for" (Set (Var "g")) "being" ($#v1_valued_0 :::"complex-valued"::: ) ($#m1_hidden :::"Function":::) "holds" (Bool (Set ($#k16_valued_2 :::"<->"::: ) (Set "(" (Set (Var "f")) ($#k58_valued_2 :::"<->"::: ) (Set (Var "g")) ")" )) ($#r2_relset_1 :::"="::: ) (Set (Set "(" ($#k16_valued_2 :::"<->"::: ) (Set (Var "f")) ")" ) ($#k52_valued_2 :::"<+>"::: ) (Set (Var "g")))))))) ; theorem :: VALUED_2:65 (Bool "for" (Set (Var "X")) "being" ($#m1_hidden :::"set"::: ) (Bool "for" (Set (Var "Y")) "being" ($#v1_valued_2 :::"complex-functions-membered"::: ) ($#m1_hidden :::"set"::: ) (Bool "for" (Set (Var "f")) "being" ($#m1_subset_1 :::"PartFunc":::) "of" (Set (Var "X")) "," (Set (Var "Y")) (Bool "for" (Set (Var "g")) "," (Set (Var "h")) "being" ($#v1_valued_0 :::"complex-valued"::: ) ($#m1_hidden :::"Function":::) "holds" (Bool (Set (Set "(" (Set (Var "f")) ($#k52_valued_2 :::"<+>"::: ) (Set (Var "g")) ")" ) ($#k58_valued_2 :::"<->"::: ) (Set (Var "h"))) ($#r1_hidden :::"="::: ) (Set (Set (Var "f")) ($#k52_valued_2 :::"<+>"::: ) (Set "(" (Set (Var "g")) ($#k45_valued_1 :::"-"::: ) (Set (Var "h")) ")" ))))))) ; theorem :: VALUED_2:66 (Bool "for" (Set (Var "X")) "being" ($#m1_hidden :::"set"::: ) (Bool "for" (Set (Var "Y")) "being" ($#v1_valued_2 :::"complex-functions-membered"::: ) ($#m1_hidden :::"set"::: ) (Bool "for" (Set (Var "f")) "being" ($#m1_subset_1 :::"PartFunc":::) "of" (Set (Var "X")) "," (Set (Var "Y")) (Bool "for" (Set (Var "g")) "," (Set (Var "h")) "being" ($#v1_valued_0 :::"complex-valued"::: ) ($#m1_hidden :::"Function":::) "holds" (Bool (Set (Set "(" (Set (Var "f")) ($#k58_valued_2 :::"<->"::: ) (Set (Var "g")) ")" ) ($#k52_valued_2 :::"<+>"::: ) (Set (Var "h"))) ($#r1_hidden :::"="::: ) (Set (Set (Var "f")) ($#k58_valued_2 :::"<->"::: ) (Set "(" (Set (Var "g")) ($#k45_valued_1 :::"-"::: ) (Set (Var "h")) ")" ))))))) ; theorem :: VALUED_2:67 (Bool "for" (Set (Var "X")) "being" ($#m1_hidden :::"set"::: ) (Bool "for" (Set (Var "Y")) "being" ($#v1_valued_2 :::"complex-functions-membered"::: ) ($#m1_hidden :::"set"::: ) (Bool "for" (Set (Var "f")) "being" ($#m1_subset_1 :::"PartFunc":::) "of" (Set (Var "X")) "," (Set (Var "Y")) (Bool "for" (Set (Var "g")) "," (Set (Var "h")) "being" ($#v1_valued_0 :::"complex-valued"::: ) ($#m1_hidden :::"Function":::) "holds" (Bool (Set (Set "(" (Set (Var "f")) ($#k58_valued_2 :::"<->"::: ) (Set (Var "g")) ")" ) ($#k58_valued_2 :::"<->"::: ) (Set (Var "h"))) ($#r1_hidden :::"="::: ) (Set (Set (Var "f")) ($#k58_valued_2 :::"<->"::: ) (Set "(" (Set (Var "g")) ($#k1_valued_1 :::"+"::: ) (Set (Var "h")) ")" ))))))) ; definitionlet "Y" be ($#v1_valued_2 :::"complex-functions-membered"::: ) ($#m1_hidden :::"set"::: ) ; let "f" be (Set (Const "Y")) ($#v5_relat_1 :::"-valued"::: ) ($#m1_hidden :::"Function":::); let "g" be ($#v1_valued_0 :::"complex-valued"::: ) ($#m1_hidden :::"Function":::); func "f" :::"<#>"::: "g" -> ($#m1_hidden :::"Function":::) means :: VALUED_2:def 43 (Bool "(" (Bool (Set ($#k9_xtuple_0 :::"dom"::: ) it) ($#r1_hidden :::"="::: ) (Set (Set "(" ($#k9_xtuple_0 :::"dom"::: ) "f" ")" ) ($#k3_xboole_0 :::"/\"::: ) (Set "(" ($#k9_xtuple_0 :::"dom"::: ) "g" ")" ))) & (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 (Set "(" "f" ($#k1_funct_1 :::"."::: ) (Set (Var "x")) ")" ) ($#k24_valued_1 :::"(#)"::: ) (Set "(" "g" ($#k1_funct_1 :::"."::: ) (Set (Var "x")) ")" ))) ")" ) ")" ); end; :: deftheorem defines :::"<#>"::: VALUED_2:def 43 : (Bool "for" (Set (Var "Y")) "being" ($#v1_valued_2 :::"complex-functions-membered"::: ) ($#m1_hidden :::"set"::: ) (Bool "for" (Set (Var "f")) "being" (Set (Var "b1")) ($#v5_relat_1 :::"-valued"::: ) ($#m1_hidden :::"Function":::) (Bool "for" (Set (Var "g")) "being" ($#v1_valued_0 :::"complex-valued"::: ) ($#m1_hidden :::"Function":::) (Bool "for" (Set (Var "b4")) "being" ($#m1_hidden :::"Function":::) "holds" (Bool "(" (Bool (Set (Var "b4")) ($#r1_hidden :::"="::: ) (Set (Set (Var "f")) ($#k62_valued_2 :::"<#>"::: ) (Set (Var "g")))) "iff" (Bool "(" (Bool (Set ($#k9_xtuple_0 :::"dom"::: ) (Set (Var "b4"))) ($#r1_hidden :::"="::: ) (Set (Set "(" ($#k9_xtuple_0 :::"dom"::: ) (Set (Var "f")) ")" ) ($#k3_xboole_0 :::"/\"::: ) (Set "(" ($#k9_xtuple_0 :::"dom"::: ) (Set (Var "g")) ")" ))) & (Bool "(" "for" (Set (Var "x")) "being" ($#m1_hidden :::"set"::: ) "st" (Bool (Bool (Set (Var "x")) ($#r2_hidden :::"in"::: ) (Set ($#k9_xtuple_0 :::"dom"::: ) (Set (Var "b4"))))) "holds" (Bool (Set (Set (Var "b4")) ($#k1_funct_1 :::"."::: ) (Set (Var "x"))) ($#r1_hidden :::"="::: ) (Set (Set "(" (Set (Var "f")) ($#k1_funct_1 :::"."::: ) (Set (Var "x")) ")" ) ($#k24_valued_1 :::"(#)"::: ) (Set "(" (Set (Var "g")) ($#k1_funct_1 :::"."::: ) (Set (Var "x")) ")" ))) ")" ) ")" ) ")" ))))); definitionlet "X" be ($#m1_hidden :::"set"::: ) ; let "Y" be ($#v1_valued_2 :::"complex-functions-membered"::: ) ($#m1_hidden :::"set"::: ) ; let "f" be ($#m1_subset_1 :::"PartFunc":::) "of" (Set (Const "X")) "," (Set (Const "Y")); let "g" be ($#v1_valued_0 :::"complex-valued"::: ) ($#m1_hidden :::"Function":::); :: original: :::"<#>"::: redefine func "f" :::"<#>"::: "g" -> ($#m1_subset_1 :::"PartFunc":::) "of" (Set "(" "X" ($#k3_xboole_0 :::"/\"::: ) (Set "(" ($#k9_xtuple_0 :::"dom"::: ) "g" ")" ) ")" ) "," (Set "(" ($#k2_valued_2 :::"C_PFuncs"::: ) (Set "(" ($#k1_valued_2 :::"DOMS"::: ) "Y" ")" ) ")" ); end; definitionlet "X" be ($#m1_hidden :::"set"::: ) ; let "Y" be ($#v3_valued_2 :::"real-functions-membered"::: ) ($#m1_hidden :::"set"::: ) ; let "f" be ($#m1_subset_1 :::"PartFunc":::) "of" (Set (Const "X")) "," (Set (Const "Y")); let "g" be ($#v3_valued_0 :::"real-valued"::: ) ($#m1_hidden :::"Function":::); :: original: :::"<#>"::: redefine func "f" :::"<#>"::: "g" -> ($#m1_subset_1 :::"PartFunc":::) "of" (Set "(" "X" ($#k3_xboole_0 :::"/\"::: ) (Set "(" ($#k9_xtuple_0 :::"dom"::: ) "g" ")" ) ")" ) "," (Set "(" ($#k6_valued_2 :::"R_PFuncs"::: ) (Set "(" ($#k1_valued_2 :::"DOMS"::: ) "Y" ")" ) ")" ); end; definitionlet "X" be ($#m1_hidden :::"set"::: ) ; let "Y" be ($#v4_valued_2 :::"rational-functions-membered"::: ) ($#m1_hidden :::"set"::: ) ; let "f" be ($#m1_subset_1 :::"PartFunc":::) "of" (Set (Const "X")) "," (Set (Const "Y")); let "g" be (Set ($#k3_numbers :::"RAT"::: ) ) ($#v5_relat_1 :::"-valued"::: ) ($#m1_hidden :::"Function":::); :: original: :::"<#>"::: redefine func "f" :::"<#>"::: "g" -> ($#m1_subset_1 :::"PartFunc":::) "of" (Set "(" "X" ($#k3_xboole_0 :::"/\"::: ) (Set "(" ($#k9_xtuple_0 :::"dom"::: ) "g" ")" ) ")" ) "," (Set "(" ($#k8_valued_2 :::"Q_PFuncs"::: ) (Set "(" ($#k1_valued_2 :::"DOMS"::: ) "Y" ")" ) ")" ); end; definitionlet "X" be ($#m1_hidden :::"set"::: ) ; let "Y" be ($#v5_valued_2 :::"integer-functions-membered"::: ) ($#m1_hidden :::"set"::: ) ; let "f" be ($#m1_subset_1 :::"PartFunc":::) "of" (Set (Const "X")) "," (Set (Const "Y")); let "g" be (Set ($#k4_numbers :::"INT"::: ) ) ($#v5_relat_1 :::"-valued"::: ) ($#m1_hidden :::"Function":::); :: original: :::"<#>"::: redefine func "f" :::"<#>"::: "g" -> ($#m1_subset_1 :::"PartFunc":::) "of" (Set "(" "X" ($#k3_xboole_0 :::"/\"::: ) (Set "(" ($#k9_xtuple_0 :::"dom"::: ) "g" ")" ) ")" ) "," (Set "(" ($#k10_valued_2 :::"I_PFuncs"::: ) (Set "(" ($#k1_valued_2 :::"DOMS"::: ) "Y" ")" ) ")" ); end; definitionlet "X" be ($#m1_hidden :::"set"::: ) ; let "Y" be ($#v6_valued_2 :::"natural-functions-membered"::: ) ($#m1_hidden :::"set"::: ) ; let "f" be ($#m1_subset_1 :::"PartFunc":::) "of" (Set (Const "X")) "," (Set (Const "Y")); let "g" be ($#v4_valued_0 :::"natural-valued"::: ) ($#m1_hidden :::"Function":::); :: original: :::"<#>"::: redefine func "f" :::"<#>"::: "g" -> ($#m1_subset_1 :::"PartFunc":::) "of" (Set "(" "X" ($#k3_xboole_0 :::"/\"::: ) (Set "(" ($#k9_xtuple_0 :::"dom"::: ) "g" ")" ) ")" ) "," (Set "(" ($#k12_valued_2 :::"N_PFuncs"::: ) (Set "(" ($#k1_valued_2 :::"DOMS"::: ) "Y" ")" ) ")" ); end; theorem :: VALUED_2:68 (Bool "for" (Set (Var "X")) "being" ($#m1_hidden :::"set"::: ) (Bool "for" (Set (Var "Y")) "being" ($#v1_valued_2 :::"complex-functions-membered"::: ) ($#m1_hidden :::"set"::: ) (Bool "for" (Set (Var "f")) "being" ($#m1_subset_1 :::"PartFunc":::) "of" (Set (Var "X")) "," (Set (Var "Y")) (Bool "for" (Set (Var "g")) "being" ($#v1_valued_0 :::"complex-valued"::: ) ($#m1_hidden :::"Function":::) "holds" (Bool (Set (Set (Var "f")) ($#k63_valued_2 :::"<#>"::: ) (Set "(" ($#k30_valued_1 :::"-"::: ) (Set (Var "g")) ")" )) ($#r1_hidden :::"="::: ) (Set (Set "(" ($#k16_valued_2 :::"<->"::: ) (Set (Var "f")) ")" ) ($#k63_valued_2 :::"<#>"::: ) (Set (Var "g")))))))) ; theorem :: VALUED_2:69 (Bool "for" (Set (Var "X")) "being" ($#m1_hidden :::"set"::: ) (Bool "for" (Set (Var "Y")) "being" ($#v1_valued_2 :::"complex-functions-membered"::: ) ($#m1_hidden :::"set"::: ) (Bool "for" (Set (Var "f")) "being" ($#m1_subset_1 :::"PartFunc":::) "of" (Set (Var "X")) "," (Set (Var "Y")) (Bool "for" (Set (Var "g")) "being" ($#v1_valued_0 :::"complex-valued"::: ) ($#m1_hidden :::"Function":::) "holds" (Bool (Set (Set (Var "f")) ($#k63_valued_2 :::"<#>"::: ) (Set "(" ($#k30_valued_1 :::"-"::: ) (Set (Var "g")) ")" )) ($#r1_hidden :::"="::: ) (Set ($#k16_valued_2 :::"<->"::: ) (Set "(" (Set (Var "f")) ($#k63_valued_2 :::"<#>"::: ) (Set (Var "g")) ")" ))))))) ; theorem :: VALUED_2:70 (Bool "for" (Set (Var "X")) "being" ($#m1_hidden :::"set"::: ) (Bool "for" (Set (Var "Y")) "being" ($#v1_valued_2 :::"complex-functions-membered"::: ) ($#m1_hidden :::"set"::: ) (Bool "for" (Set (Var "f")) "being" ($#m1_subset_1 :::"PartFunc":::) "of" (Set (Var "X")) "," (Set (Var "Y")) (Bool "for" (Set (Var "g")) "," (Set (Var "h")) "being" ($#v1_valued_0 :::"complex-valued"::: ) ($#m1_hidden :::"Function":::) "holds" (Bool (Set (Set "(" (Set (Var "f")) ($#k63_valued_2 :::"<#>"::: ) (Set (Var "g")) ")" ) ($#k63_valued_2 :::"<#>"::: ) (Set (Var "h"))) ($#r1_hidden :::"="::: ) (Set (Set (Var "f")) ($#k63_valued_2 :::"<#>"::: ) (Set "(" (Set (Var "g")) ($#k18_valued_1 :::"(#)"::: ) (Set (Var "h")) ")" ))))))) ; definitionlet "Y" be ($#v1_valued_2 :::"complex-functions-membered"::: ) ($#m1_hidden :::"set"::: ) ; let "f" be (Set (Const "Y")) ($#v5_relat_1 :::"-valued"::: ) ($#m1_hidden :::"Function":::); let "g" be ($#v1_valued_0 :::"complex-valued"::: ) ($#m1_hidden :::"Function":::); func "f" :::""::: "g" -> ($#m1_hidden :::"Function":::) equals :: VALUED_2:def 44 (Set "f" ($#k62_valued_2 :::"<#>"::: ) (Set "(" "g" ($#k35_valued_1 :::"""::: ) ")" )); end; :: deftheorem defines :::""::: VALUED_2:def 44 : (Bool "for" (Set (Var "Y")) "being" ($#v1_valued_2 :::"complex-functions-membered"::: ) ($#m1_hidden :::"set"::: ) (Bool "for" (Set (Var "f")) "being" (Set (Var "b1")) ($#v5_relat_1 :::"-valued"::: ) ($#m1_hidden :::"Function":::) (Bool "for" (Set (Var "g")) "being" ($#v1_valued_0 :::"complex-valued"::: ) ($#m1_hidden :::"Function":::) "holds" (Bool (Set (Set (Var "f")) ($#k68_valued_2 :::""::: ) (Set (Var "g"))) ($#r1_hidden :::"="::: ) (Set (Set (Var "f")) ($#k62_valued_2 :::"<#>"::: ) (Set "(" (Set (Var "g")) ($#k35_valued_1 :::"""::: ) ")" )))))); theorem :: VALUED_2:71 (Bool "for" (Set (Var "X")) "being" ($#m1_hidden :::"set"::: ) (Bool "for" (Set (Var "Y")) "being" ($#v1_valued_2 :::"complex-functions-membered"::: ) ($#m1_hidden :::"set"::: ) (Bool "for" (Set (Var "f")) "being" ($#m1_subset_1 :::"PartFunc":::) "of" (Set (Var "X")) "," (Set (Var "Y")) (Bool "for" (Set (Var "g")) "being" ($#v1_valued_0 :::"complex-valued"::: ) ($#m1_hidden :::"Function":::) "holds" (Bool (Set ($#k9_xtuple_0 :::"dom"::: ) (Set "(" (Set (Var "f")) ($#k68_valued_2 :::""::: ) (Set (Var "g")) ")" )) ($#r1_hidden :::"="::: ) (Set (Set "(" ($#k1_relset_1 :::"dom"::: ) (Set (Var "f")) ")" ) ($#k8_subset_1 :::"/\"::: ) (Set "(" ($#k9_xtuple_0 :::"dom"::: ) (Set (Var "g")) ")" ))))))) ; theorem :: VALUED_2:72 (Bool "for" (Set (Var "X")) "," (Set (Var "x")) "being" ($#m1_hidden :::"set"::: ) (Bool "for" (Set (Var "Y")) "being" ($#v1_valued_2 :::"complex-functions-membered"::: ) ($#m1_hidden :::"set"::: ) (Bool "for" (Set (Var "f")) "being" ($#m1_subset_1 :::"PartFunc":::) "of" (Set (Var "X")) "," (Set (Var "Y")) (Bool "for" (Set (Var "g")) "being" ($#v1_valued_0 :::"complex-valued"::: ) ($#m1_hidden :::"Function":::) "st" (Bool (Bool (Set (Var "x")) ($#r2_hidden :::"in"::: ) (Set ($#k9_xtuple_0 :::"dom"::: ) (Set "(" (Set (Var "f")) ($#k68_valued_2 :::""::: ) (Set (Var "g")) ")" )))) "holds" (Bool (Set (Set "(" (Set (Var "f")) ($#k68_valued_2 :::""::: ) (Set (Var "g")) ")" ) ($#k1_funct_1 :::"."::: ) (Set (Var "x"))) ($#r1_hidden :::"="::: ) (Set (Set "(" (Set (Var "f")) ($#k1_funct_1 :::"."::: ) (Set (Var "x")) ")" ) ($#k14_valued_2 :::"(/)"::: ) (Set "(" (Set (Var "g")) ($#k1_funct_1 :::"."::: ) (Set (Var "x")) ")" ))))))) ; definitionlet "X" be ($#m1_hidden :::"set"::: ) ; let "Y" be ($#v1_valued_2 :::"complex-functions-membered"::: ) ($#m1_hidden :::"set"::: ) ; let "f" be ($#m1_subset_1 :::"PartFunc":::) "of" (Set (Const "X")) "," (Set (Const "Y")); let "g" be ($#v1_valued_0 :::"complex-valued"::: ) ($#m1_hidden :::"Function":::); :: original: :::""::: redefine func "f" :::""::: "g" -> ($#m1_subset_1 :::"PartFunc":::) "of" (Set "(" "X" ($#k3_xboole_0 :::"/\"::: ) (Set "(" ($#k9_xtuple_0 :::"dom"::: ) "g" ")" ) ")" ) "," (Set "(" ($#k2_valued_2 :::"C_PFuncs"::: ) (Set "(" ($#k1_valued_2 :::"DOMS"::: ) "Y" ")" ) ")" ); end; definitionlet "X" be ($#m1_hidden :::"set"::: ) ; let "Y" be ($#v3_valued_2 :::"real-functions-membered"::: ) ($#m1_hidden :::"set"::: ) ; let "f" be ($#m1_subset_1 :::"PartFunc":::) "of" (Set (Const "X")) "," (Set (Const "Y")); let "g" be ($#v3_valued_0 :::"real-valued"::: ) ($#m1_hidden :::"Function":::); :: original: :::""::: redefine func "f" :::""::: "g" -> ($#m1_subset_1 :::"PartFunc":::) "of" (Set "(" "X" ($#k3_xboole_0 :::"/\"::: ) (Set "(" ($#k9_xtuple_0 :::"dom"::: ) "g" ")" ) ")" ) "," (Set "(" ($#k6_valued_2 :::"R_PFuncs"::: ) (Set "(" ($#k1_valued_2 :::"DOMS"::: ) "Y" ")" ) ")" ); end; definitionlet "X" be ($#m1_hidden :::"set"::: ) ; let "Y" be ($#v4_valued_2 :::"rational-functions-membered"::: ) ($#m1_hidden :::"set"::: ) ; let "f" be ($#m1_subset_1 :::"PartFunc":::) "of" (Set (Const "X")) "," (Set (Const "Y")); let "g" be (Set ($#k3_numbers :::"RAT"::: ) ) ($#v5_relat_1 :::"-valued"::: ) ($#m1_hidden :::"Function":::); :: original: :::""::: redefine func "f" :::""::: "g" -> ($#m1_subset_1 :::"PartFunc":::) "of" (Set "(" "X" ($#k3_xboole_0 :::"/\"::: ) (Set "(" ($#k9_xtuple_0 :::"dom"::: ) "g" ")" ) ")" ) "," (Set "(" ($#k8_valued_2 :::"Q_PFuncs"::: ) (Set "(" ($#k1_valued_2 :::"DOMS"::: ) "Y" ")" ) ")" ); end; theorem :: VALUED_2:73 (Bool "for" (Set (Var "X")) "being" ($#m1_hidden :::"set"::: ) (Bool "for" (Set (Var "Y")) "being" ($#v1_valued_2 :::"complex-functions-membered"::: ) ($#m1_hidden :::"set"::: ) (Bool "for" (Set (Var "f")) "being" ($#m1_subset_1 :::"PartFunc":::) "of" (Set (Var "X")) "," (Set (Var "Y")) (Bool "for" (Set (Var "g")) "," (Set (Var "h")) "being" ($#v1_valued_0 :::"complex-valued"::: ) ($#m1_hidden :::"Function":::) "holds" (Bool (Set (Set "(" (Set (Var "f")) ($#k63_valued_2 :::"<#>"::: ) (Set (Var "g")) ")" ) ($#k69_valued_2 :::""::: ) (Set (Var "h"))) ($#r1_hidden :::"="::: ) (Set (Set (Var "f")) ($#k63_valued_2 :::"<#>"::: ) (Set "(" (Set (Var "g")) ($#k50_valued_1 :::"/""::: ) (Set (Var "h")) ")" ))))))) ; definitionlet "Y1", "Y2" be ($#v1_valued_2 :::"complex-functions-membered"::: ) ($#m1_hidden :::"set"::: ) ; let "f" be (Set (Const "Y1")) ($#v5_relat_1 :::"-valued"::: ) ($#m1_hidden :::"Function":::); let "g" be (Set (Const "Y2")) ($#v5_relat_1 :::"-valued"::: ) ($#m1_hidden :::"Function":::); func "f" :::"<++>"::: "g" -> ($#m1_hidden :::"Function":::) means :: VALUED_2:def 45 (Bool "(" (Bool (Set ($#k9_xtuple_0 :::"dom"::: ) it) ($#r1_hidden :::"="::: ) (Set (Set "(" ($#k9_xtuple_0 :::"dom"::: ) "f" ")" ) ($#k3_xboole_0 :::"/\"::: ) (Set "(" ($#k9_xtuple_0 :::"dom"::: ) "g" ")" ))) & (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 (Set "(" "f" ($#k1_funct_1 :::"."::: ) (Set (Var "x")) ")" ) ($#k1_valued_1 :::"+"::: ) (Set "(" "g" ($#k1_funct_1 :::"."::: ) (Set (Var "x")) ")" ))) ")" ) ")" ); end; :: deftheorem defines :::"<++>"::: VALUED_2:def 45 : (Bool "for" (Set (Var "Y1")) "," (Set (Var "Y2")) "being" ($#v1_valued_2 :::"complex-functions-membered"::: ) ($#m1_hidden :::"set"::: ) (Bool "for" (Set (Var "f")) "being" (Set (Var "b1")) ($#v5_relat_1 :::"-valued"::: ) ($#m1_hidden :::"Function":::) (Bool "for" (Set (Var "g")) "being" (Set (Var "b2")) ($#v5_relat_1 :::"-valued"::: ) ($#m1_hidden :::"Function":::) (Bool "for" (Set (Var "b5")) "being" ($#m1_hidden :::"Function":::) "holds" (Bool "(" (Bool (Set (Var "b5")) ($#r1_hidden :::"="::: ) (Set (Set (Var "f")) ($#k72_valued_2 :::"<++>"::: ) (Set (Var "g")))) "iff" (Bool "(" (Bool (Set ($#k9_xtuple_0 :::"dom"::: ) (Set (Var "b5"))) ($#r1_hidden :::"="::: ) (Set (Set "(" ($#k9_xtuple_0 :::"dom"::: ) (Set (Var "f")) ")" ) ($#k3_xboole_0 :::"/\"::: ) (Set "(" ($#k9_xtuple_0 :::"dom"::: ) (Set (Var "g")) ")" ))) & (Bool "(" "for" (Set (Var "x")) "being" ($#m1_hidden :::"set"::: ) "st" (Bool (Bool (Set (Var "x")) ($#r2_hidden :::"in"::: ) (Set ($#k9_xtuple_0 :::"dom"::: ) (Set (Var "b5"))))) "holds" (Bool (Set (Set (Var "b5")) ($#k1_funct_1 :::"."::: ) (Set (Var "x"))) ($#r1_hidden :::"="::: ) (Set (Set "(" (Set (Var "f")) ($#k1_funct_1 :::"."::: ) (Set (Var "x")) ")" ) ($#k1_valued_1 :::"+"::: ) (Set "(" (Set (Var "g")) ($#k1_funct_1 :::"."::: ) (Set (Var "x")) ")" ))) ")" ) ")" ) ")" ))))); definitionlet "X1", "X2" be ($#m1_hidden :::"set"::: ) ; let "Y1", "Y2" be ($#v1_valued_2 :::"complex-functions-membered"::: ) ($#m1_hidden :::"set"::: ) ; let "f" be ($#m1_subset_1 :::"PartFunc":::) "of" (Set (Const "X1")) "," (Set (Const "Y1")); let "g" be ($#m1_subset_1 :::"PartFunc":::) "of" (Set (Const "X2")) "," (Set (Const "Y2")); :: original: :::"<++>"::: redefine func "f" :::"<++>"::: "g" -> ($#m1_subset_1 :::"PartFunc":::) "of" (Set "(" "X1" ($#k3_xboole_0 :::"/\"::: ) "X2" ")" ) "," (Set "(" ($#k2_valued_2 :::"C_PFuncs"::: ) (Set "(" (Set "(" ($#k1_valued_2 :::"DOMS"::: ) "Y1" ")" ) ($#k3_xboole_0 :::"/\"::: ) (Set "(" ($#k1_valued_2 :::"DOMS"::: ) "Y2" ")" ) ")" ) ")" ); end; definitionlet "X1", "X2" be ($#m1_hidden :::"set"::: ) ; let "Y1", "Y2" be ($#v3_valued_2 :::"real-functions-membered"::: ) ($#m1_hidden :::"set"::: ) ; let "f" be ($#m1_subset_1 :::"PartFunc":::) "of" (Set (Const "X1")) "," (Set (Const "Y1")); let "g" be ($#m1_subset_1 :::"PartFunc":::) "of" (Set (Const "X2")) "," (Set (Const "Y2")); :: original: :::"<++>"::: redefine func "f" :::"<++>"::: "g" -> ($#m1_subset_1 :::"PartFunc":::) "of" (Set "(" "X1" ($#k3_xboole_0 :::"/\"::: ) "X2" ")" ) "," (Set "(" ($#k6_valued_2 :::"R_PFuncs"::: ) (Set "(" (Set "(" ($#k1_valued_2 :::"DOMS"::: ) "Y1" ")" ) ($#k3_xboole_0 :::"/\"::: ) (Set "(" ($#k1_valued_2 :::"DOMS"::: ) "Y2" ")" ) ")" ) ")" ); end; definitionlet "X1", "X2" be ($#m1_hidden :::"set"::: ) ; let "Y1", "Y2" be ($#v4_valued_2 :::"rational-functions-membered"::: ) ($#m1_hidden :::"set"::: ) ; let "f" be ($#m1_subset_1 :::"PartFunc":::) "of" (Set (Const "X1")) "," (Set (Const "Y1")); let "g" be ($#m1_subset_1 :::"PartFunc":::) "of" (Set (Const "X2")) "," (Set (Const "Y2")); :: original: :::"<++>"::: redefine func "f" :::"<++>"::: "g" -> ($#m1_subset_1 :::"PartFunc":::) "of" (Set "(" "X1" ($#k3_xboole_0 :::"/\"::: ) "X2" ")" ) "," (Set "(" ($#k8_valued_2 :::"Q_PFuncs"::: ) (Set "(" (Set "(" ($#k1_valued_2 :::"DOMS"::: ) "Y1" ")" ) ($#k3_xboole_0 :::"/\"::: ) (Set "(" ($#k1_valued_2 :::"DOMS"::: ) "Y2" ")" ) ")" ) ")" ); end; definitionlet "X1", "X2" be ($#m1_hidden :::"set"::: ) ; let "Y1", "Y2" be ($#v5_valued_2 :::"integer-functions-membered"::: ) ($#m1_hidden :::"set"::: ) ; let "f" be ($#m1_subset_1 :::"PartFunc":::) "of" (Set (Const "X1")) "," (Set (Const "Y1")); let "g" be ($#m1_subset_1 :::"PartFunc":::) "of" (Set (Const "X2")) "," (Set (Const "Y2")); :: original: :::"<++>"::: redefine func "f" :::"<++>"::: "g" -> ($#m1_subset_1 :::"PartFunc":::) "of" (Set "(" "X1" ($#k3_xboole_0 :::"/\"::: ) "X2" ")" ) "," (Set "(" ($#k10_valued_2 :::"I_PFuncs"::: ) (Set "(" (Set "(" ($#k1_valued_2 :::"DOMS"::: ) "Y1" ")" ) ($#k3_xboole_0 :::"/\"::: ) (Set "(" ($#k1_valued_2 :::"DOMS"::: ) "Y2" ")" ) ")" ) ")" ); end; definitionlet "X1", "X2" be ($#m1_hidden :::"set"::: ) ; let "Y1", "Y2" be ($#v6_valued_2 :::"natural-functions-membered"::: ) ($#m1_hidden :::"set"::: ) ; let "f" be ($#m1_subset_1 :::"PartFunc":::) "of" (Set (Const "X1")) "," (Set (Const "Y1")); let "g" be ($#m1_subset_1 :::"PartFunc":::) "of" (Set (Const "X2")) "," (Set (Const "Y2")); :: original: :::"<++>"::: redefine func "f" :::"<++>"::: "g" -> ($#m1_subset_1 :::"PartFunc":::) "of" (Set "(" "X1" ($#k3_xboole_0 :::"/\"::: ) "X2" ")" ) "," (Set "(" ($#k12_valued_2 :::"N_PFuncs"::: ) (Set "(" (Set "(" ($#k1_valued_2 :::"DOMS"::: ) "Y1" ")" ) ($#k3_xboole_0 :::"/\"::: ) (Set "(" ($#k1_valued_2 :::"DOMS"::: ) "Y2" ")" ) ")" ) ")" ); end; theorem :: VALUED_2:74 (Bool "for" (Set (Var "X1")) "," (Set (Var "X2")) "being" ($#m1_hidden :::"set"::: ) (Bool "for" (Set (Var "Y1")) "," (Set (Var "Y2")) "being" ($#v1_valued_2 :::"complex-functions-membered"::: ) ($#m1_hidden :::"set"::: ) (Bool "for" (Set (Var "f1")) "being" ($#m1_subset_1 :::"PartFunc":::) "of" (Set (Var "X1")) "," (Set (Var "Y1")) (Bool "for" (Set (Var "f2")) "being" ($#m1_subset_1 :::"PartFunc":::) "of" (Set (Var "X2")) "," (Set (Var "Y2")) "holds" (Bool (Set (Set (Var "f1")) ($#k73_valued_2 :::"<++>"::: ) (Set (Var "f2"))) ($#r1_hidden :::"="::: ) (Set (Set (Var "f2")) ($#k73_valued_2 :::"<++>"::: ) (Set (Var "f1")))))))) ; theorem :: VALUED_2:75 (Bool "for" (Set (Var "X")) "," (Set (Var "X1")) "," (Set (Var "X2")) "being" ($#m1_hidden :::"set"::: ) (Bool "for" (Set (Var "Y")) "," (Set (Var "Y1")) "," (Set (Var "Y2")) "being" ($#v1_valued_2 :::"complex-functions-membered"::: ) ($#m1_hidden :::"set"::: ) (Bool "for" (Set (Var "f")) "being" ($#m1_subset_1 :::"PartFunc":::) "of" (Set (Var "X")) "," (Set (Var "Y")) (Bool "for" (Set (Var "f1")) "being" ($#m1_subset_1 :::"PartFunc":::) "of" (Set (Var "X1")) "," (Set (Var "Y1")) (Bool "for" (Set (Var "f2")) "being" ($#m1_subset_1 :::"PartFunc":::) "of" (Set (Var "X2")) "," (Set (Var "Y2")) "holds" (Bool (Set (Set "(" (Set (Var "f")) ($#k73_valued_2 :::"<++>"::: ) (Set (Var "f1")) ")" ) ($#k73_valued_2 :::"<++>"::: ) (Set (Var "f2"))) ($#r1_hidden :::"="::: ) (Set (Set (Var "f")) ($#k73_valued_2 :::"<++>"::: ) (Set "(" (Set (Var "f1")) ($#k73_valued_2 :::"<++>"::: ) (Set (Var "f2")) ")" )))))))) ; theorem :: VALUED_2:76 (Bool "for" (Set (Var "X1")) "," (Set (Var "X2")) "being" ($#m1_hidden :::"set"::: ) (Bool "for" (Set (Var "Y1")) "," (Set (Var "Y2")) "being" ($#v1_valued_2 :::"complex-functions-membered"::: ) ($#m1_hidden :::"set"::: ) (Bool "for" (Set (Var "f1")) "being" ($#m1_subset_1 :::"PartFunc":::) "of" (Set (Var "X1")) "," (Set (Var "Y1")) (Bool "for" (Set (Var "f2")) "being" ($#m1_subset_1 :::"PartFunc":::) "of" (Set (Var "X2")) "," (Set (Var "Y2")) "holds" (Bool (Set ($#k16_valued_2 :::"<->"::: ) (Set "(" (Set (Var "f1")) ($#k73_valued_2 :::"<++>"::: ) (Set (Var "f2")) ")" )) ($#r1_hidden :::"="::: ) (Set (Set "(" ($#k16_valued_2 :::"<->"::: ) (Set (Var "f1")) ")" ) ($#k73_valued_2 :::"<++>"::: ) (Set "(" ($#k16_valued_2 :::"<->"::: ) (Set (Var "f2")) ")" ))))))) ; definitionlet "Y1", "Y2" be ($#v1_valued_2 :::"complex-functions-membered"::: ) ($#m1_hidden :::"set"::: ) ; let "f" be (Set (Const "Y1")) ($#v5_relat_1 :::"-valued"::: ) ($#m1_hidden :::"Function":::); let "g" be (Set (Const "Y2")) ($#v5_relat_1 :::"-valued"::: ) ($#m1_hidden :::"Function":::); func "f" :::"<-->"::: "g" -> ($#m1_hidden :::"Function":::) means :: VALUED_2:def 46 (Bool "(" (Bool (Set ($#k9_xtuple_0 :::"dom"::: ) it) ($#r1_hidden :::"="::: ) (Set (Set "(" ($#k9_xtuple_0 :::"dom"::: ) "f" ")" ) ($#k3_xboole_0 :::"/\"::: ) (Set "(" ($#k9_xtuple_0 :::"dom"::: ) "g" ")" ))) & (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 (Set "(" "f" ($#k1_funct_1 :::"."::: ) (Set (Var "x")) ")" ) ($#k45_valued_1 :::"-"::: ) (Set "(" "g" ($#k1_funct_1 :::"."::: ) (Set (Var "x")) ")" ))) ")" ) ")" ); end; :: deftheorem defines :::"<-->"::: VALUED_2:def 46 : (Bool "for" (Set (Var "Y1")) "," (Set (Var "Y2")) "being" ($#v1_valued_2 :::"complex-functions-membered"::: ) ($#m1_hidden :::"set"::: ) (Bool "for" (Set (Var "f")) "being" (Set (Var "b1")) ($#v5_relat_1 :::"-valued"::: ) ($#m1_hidden :::"Function":::) (Bool "for" (Set (Var "g")) "being" (Set (Var "b2")) ($#v5_relat_1 :::"-valued"::: ) ($#m1_hidden :::"Function":::) (Bool "for" (Set (Var "b5")) "being" ($#m1_hidden :::"Function":::) "holds" (Bool "(" (Bool (Set (Var "b5")) ($#r1_hidden :::"="::: ) (Set (Set (Var "f")) ($#k78_valued_2 :::"<-->"::: ) (Set (Var "g")))) "iff" (Bool "(" (Bool (Set ($#k9_xtuple_0 :::"dom"::: ) (Set (Var "b5"))) ($#r1_hidden :::"="::: ) (Set (Set "(" ($#k9_xtuple_0 :::"dom"::: ) (Set (Var "f")) ")" ) ($#k3_xboole_0 :::"/\"::: ) (Set "(" ($#k9_xtuple_0 :::"dom"::: ) (Set (Var "g")) ")" ))) & (Bool "(" "for" (Set (Var "x")) "being" ($#m1_hidden :::"set"::: ) "st" (Bool (Bool (Set (Var "x")) ($#r2_hidden :::"in"::: ) (Set ($#k9_xtuple_0 :::"dom"::: ) (Set (Var "b5"))))) "holds" (Bool (Set (Set (Var "b5")) ($#k1_funct_1 :::"."::: ) (Set (Var "x"))) ($#r1_hidden :::"="::: ) (Set (Set "(" (Set (Var "f")) ($#k1_funct_1 :::"."::: ) (Set (Var "x")) ")" ) ($#k45_valued_1 :::"-"::: ) (Set "(" (Set (Var "g")) ($#k1_funct_1 :::"."::: ) (Set (Var "x")) ")" ))) ")" ) ")" ) ")" ))))); definitionlet "X1", "X2" be ($#m1_hidden :::"set"::: ) ; let "Y1", "Y2" be ($#v1_valued_2 :::"complex-functions-membered"::: ) ($#m1_hidden :::"set"::: ) ; let "f" be ($#m1_subset_1 :::"PartFunc":::) "of" (Set (Const "X1")) "," (Set (Const "Y1")); let "g" be ($#m1_subset_1 :::"PartFunc":::) "of" (Set (Const "X2")) "," (Set (Const "Y2")); :: original: :::"<-->"::: redefine func "f" :::"<-->"::: "g" -> ($#m1_subset_1 :::"PartFunc":::) "of" (Set "(" "X1" ($#k3_xboole_0 :::"/\"::: ) "X2" ")" ) "," (Set "(" ($#k2_valued_2 :::"C_PFuncs"::: ) (Set "(" (Set "(" ($#k1_valued_2 :::"DOMS"::: ) "Y1" ")" ) ($#k3_xboole_0 :::"/\"::: ) (Set "(" ($#k1_valued_2 :::"DOMS"::: ) "Y2" ")" ) ")" ) ")" ); end; definitionlet "X1", "X2" be ($#m1_hidden :::"set"::: ) ; let "Y1", "Y2" be ($#v3_valued_2 :::"real-functions-membered"::: ) ($#m1_hidden :::"set"::: ) ; let "f" be ($#m1_subset_1 :::"PartFunc":::) "of" (Set (Const "X1")) "," (Set (Const "Y1")); let "g" be ($#m1_subset_1 :::"PartFunc":::) "of" (Set (Const "X2")) "," (Set (Const "Y2")); :: original: :::"<-->"::: redefine func "f" :::"<-->"::: "g" -> ($#m1_subset_1 :::"PartFunc":::) "of" (Set "(" "X1" ($#k3_xboole_0 :::"/\"::: ) "X2" ")" ) "," (Set "(" ($#k6_valued_2 :::"R_PFuncs"::: ) (Set "(" (Set "(" ($#k1_valued_2 :::"DOMS"::: ) "Y1" ")" ) ($#k3_xboole_0 :::"/\"::: ) (Set "(" ($#k1_valued_2 :::"DOMS"::: ) "Y2" ")" ) ")" ) ")" ); end; definitionlet "X1", "X2" be ($#m1_hidden :::"set"::: ) ; let "Y1", "Y2" be ($#v4_valued_2 :::"rational-functions-membered"::: ) ($#m1_hidden :::"set"::: ) ; let "f" be ($#m1_subset_1 :::"PartFunc":::) "of" (Set (Const "X1")) "," (Set (Const "Y1")); let "g" be ($#m1_subset_1 :::"PartFunc":::) "of" (Set (Const "X2")) "," (Set (Const "Y2")); :: original: :::"<-->"::: redefine func "f" :::"<-->"::: "g" -> ($#m1_subset_1 :::"PartFunc":::) "of" (Set "(" "X1" ($#k3_xboole_0 :::"/\"::: ) "X2" ")" ) "," (Set "(" ($#k8_valued_2 :::"Q_PFuncs"::: ) (Set "(" (Set "(" ($#k1_valued_2 :::"DOMS"::: ) "Y1" ")" ) ($#k3_xboole_0 :::"/\"::: ) (Set "(" ($#k1_valued_2 :::"DOMS"::: ) "Y2" ")" ) ")" ) ")" ); end; definitionlet "X1", "X2" be ($#m1_hidden :::"set"::: ) ; let "Y1", "Y2" be ($#v5_valued_2 :::"integer-functions-membered"::: ) ($#m1_hidden :::"set"::: ) ; let "f" be ($#m1_subset_1 :::"PartFunc":::) "of" (Set (Const "X1")) "," (Set (Const "Y1")); let "g" be ($#m1_subset_1 :::"PartFunc":::) "of" (Set (Const "X2")) "," (Set (Const "Y2")); :: original: :::"<-->"::: redefine func "f" :::"<-->"::: "g" -> ($#m1_subset_1 :::"PartFunc":::) "of" (Set "(" "X1" ($#k3_xboole_0 :::"/\"::: ) "X2" ")" ) "," (Set "(" ($#k10_valued_2 :::"I_PFuncs"::: ) (Set "(" (Set "(" ($#k1_valued_2 :::"DOMS"::: ) "Y1" ")" ) ($#k3_xboole_0 :::"/\"::: ) (Set "(" ($#k1_valued_2 :::"DOMS"::: ) "Y2" ")" ) ")" ) ")" ); end; theorem :: VALUED_2:77 (Bool "for" (Set (Var "X1")) "," (Set (Var "X2")) "being" ($#m1_hidden :::"set"::: ) (Bool "for" (Set (Var "Y1")) "," (Set (Var "Y2")) "being" ($#v1_valued_2 :::"complex-functions-membered"::: ) ($#m1_hidden :::"set"::: ) (Bool "for" (Set (Var "f1")) "being" ($#m1_subset_1 :::"PartFunc":::) "of" (Set (Var "X1")) "," (Set (Var "Y1")) (Bool "for" (Set (Var "f2")) "being" ($#m1_subset_1 :::"PartFunc":::) "of" (Set (Var "X2")) "," (Set (Var "Y2")) "holds" (Bool (Set (Set (Var "f1")) ($#k79_valued_2 :::"<-->"::: ) (Set (Var "f2"))) ($#r1_hidden :::"="::: ) (Set ($#k16_valued_2 :::"<->"::: ) (Set "(" (Set (Var "f2")) ($#k79_valued_2 :::"<-->"::: ) (Set (Var "f1")) ")" ))))))) ; theorem :: VALUED_2:78 (Bool "for" (Set (Var "X1")) "," (Set (Var "X2")) "being" ($#m1_hidden :::"set"::: ) (Bool "for" (Set (Var "Y1")) "," (Set (Var "Y2")) "being" ($#v1_valued_2 :::"complex-functions-membered"::: ) ($#m1_hidden :::"set"::: ) (Bool "for" (Set (Var "f1")) "being" ($#m1_subset_1 :::"PartFunc":::) "of" (Set (Var "X1")) "," (Set (Var "Y1")) (Bool "for" (Set (Var "f2")) "being" ($#m1_subset_1 :::"PartFunc":::) "of" (Set (Var "X2")) "," (Set (Var "Y2")) "holds" (Bool (Set ($#k16_valued_2 :::"<->"::: ) (Set "(" (Set (Var "f1")) ($#k79_valued_2 :::"<-->"::: ) (Set (Var "f2")) ")" )) ($#r1_hidden :::"="::: ) (Set (Set "(" ($#k16_valued_2 :::"<->"::: ) (Set (Var "f1")) ")" ) ($#k73_valued_2 :::"<++>"::: ) (Set (Var "f2")))))))) ; theorem :: VALUED_2:79 (Bool "for" (Set (Var "X")) "," (Set (Var "X1")) "," (Set (Var "X2")) "being" ($#m1_hidden :::"set"::: ) (Bool "for" (Set (Var "Y")) "," (Set (Var "Y1")) "," (Set (Var "Y2")) "being" ($#v1_valued_2 :::"complex-functions-membered"::: ) ($#m1_hidden :::"set"::: ) (Bool "for" (Set (Var "f")) "being" ($#m1_subset_1 :::"PartFunc":::) "of" (Set (Var "X")) "," (Set (Var "Y")) (Bool "for" (Set (Var "f1")) "being" ($#m1_subset_1 :::"PartFunc":::) "of" (Set (Var "X1")) "," (Set (Var "Y1")) (Bool "for" (Set (Var "f2")) "being" ($#m1_subset_1 :::"PartFunc":::) "of" (Set (Var "X2")) "," (Set (Var "Y2")) "holds" (Bool (Set (Set "(" (Set (Var "f")) ($#k73_valued_2 :::"<++>"::: ) (Set (Var "f1")) ")" ) ($#k79_valued_2 :::"<-->"::: ) (Set (Var "f2"))) ($#r1_hidden :::"="::: ) (Set (Set (Var "f")) ($#k73_valued_2 :::"<++>"::: ) (Set "(" (Set (Var "f1")) ($#k79_valued_2 :::"<-->"::: ) (Set (Var "f2")) ")" )))))))) ; theorem :: VALUED_2:80 (Bool "for" (Set (Var "X")) "," (Set (Var "X1")) "," (Set (Var "X2")) "being" ($#m1_hidden :::"set"::: ) (Bool "for" (Set (Var "Y")) "," (Set (Var "Y1")) "," (Set (Var "Y2")) "being" ($#v1_valued_2 :::"complex-functions-membered"::: ) ($#m1_hidden :::"set"::: ) (Bool "for" (Set (Var "f")) "being" ($#m1_subset_1 :::"PartFunc":::) "of" (Set (Var "X")) "," (Set (Var "Y")) (Bool "for" (Set (Var "f1")) "being" ($#m1_subset_1 :::"PartFunc":::) "of" (Set (Var "X1")) "," (Set (Var "Y1")) (Bool "for" (Set (Var "f2")) "being" ($#m1_subset_1 :::"PartFunc":::) "of" (Set (Var "X2")) "," (Set (Var "Y2")) "holds" (Bool (Set (Set "(" (Set (Var "f")) ($#k79_valued_2 :::"<-->"::: ) (Set (Var "f1")) ")" ) ($#k73_valued_2 :::"<++>"::: ) (Set (Var "f2"))) ($#r1_hidden :::"="::: ) (Set (Set (Var "f")) ($#k79_valued_2 :::"<-->"::: ) (Set "(" (Set (Var "f1")) ($#k79_valued_2 :::"<-->"::: ) (Set (Var "f2")) ")" )))))))) ; theorem :: VALUED_2:81 (Bool "for" (Set (Var "X")) "," (Set (Var "X1")) "," (Set (Var "X2")) "being" ($#m1_hidden :::"set"::: ) (Bool "for" (Set (Var "Y")) "," (Set (Var "Y1")) "," (Set (Var "Y2")) "being" ($#v1_valued_2 :::"complex-functions-membered"::: ) ($#m1_hidden :::"set"::: ) (Bool "for" (Set (Var "f")) "being" ($#m1_subset_1 :::"PartFunc":::) "of" (Set (Var "X")) "," (Set (Var "Y")) (Bool "for" (Set (Var "f1")) "being" ($#m1_subset_1 :::"PartFunc":::) "of" (Set (Var "X1")) "," (Set (Var "Y1")) (Bool "for" (Set (Var "f2")) "being" ($#m1_subset_1 :::"PartFunc":::) "of" (Set (Var "X2")) "," (Set (Var "Y2")) "holds" (Bool (Set (Set "(" (Set (Var "f")) ($#k79_valued_2 :::"<-->"::: ) (Set (Var "f1")) ")" ) ($#k79_valued_2 :::"<-->"::: ) (Set (Var "f2"))) ($#r1_hidden :::"="::: ) (Set (Set (Var "f")) ($#k79_valued_2 :::"<-->"::: ) (Set "(" (Set (Var "f1")) ($#k73_valued_2 :::"<++>"::: ) (Set (Var "f2")) ")" )))))))) ; theorem :: VALUED_2:82 (Bool "for" (Set (Var "X")) "," (Set (Var "X1")) "," (Set (Var "X2")) "being" ($#m1_hidden :::"set"::: ) (Bool "for" (Set (Var "Y")) "," (Set (Var "Y1")) "," (Set (Var "Y2")) "being" ($#v1_valued_2 :::"complex-functions-membered"::: ) ($#m1_hidden :::"set"::: ) (Bool "for" (Set (Var "f")) "being" ($#m1_subset_1 :::"PartFunc":::) "of" (Set (Var "X")) "," (Set (Var "Y")) (Bool "for" (Set (Var "f1")) "being" ($#m1_subset_1 :::"PartFunc":::) "of" (Set (Var "X1")) "," (Set (Var "Y1")) (Bool "for" (Set (Var "f2")) "being" ($#m1_subset_1 :::"PartFunc":::) "of" (Set (Var "X2")) "," (Set (Var "Y2")) "holds" (Bool (Set (Set "(" (Set (Var "f")) ($#k79_valued_2 :::"<-->"::: ) (Set (Var "f1")) ")" ) ($#k79_valued_2 :::"<-->"::: ) (Set (Var "f2"))) ($#r1_hidden :::"="::: ) (Set (Set "(" (Set (Var "f")) ($#k79_valued_2 :::"<-->"::: ) (Set (Var "f2")) ")" ) ($#k79_valued_2 :::"<-->"::: ) (Set (Var "f1"))))))))) ; definitionlet "Y1", "Y2" be ($#v1_valued_2 :::"complex-functions-membered"::: ) ($#m1_hidden :::"set"::: ) ; let "f" be (Set (Const "Y1")) ($#v5_relat_1 :::"-valued"::: ) ($#m1_hidden :::"Function":::); let "g" be (Set (Const "Y2")) ($#v5_relat_1 :::"-valued"::: ) ($#m1_hidden :::"Function":::); func "f" :::"<##>"::: "g" -> ($#m1_hidden :::"Function":::) means :: VALUED_2:def 47 (Bool "(" (Bool (Set ($#k9_xtuple_0 :::"dom"::: ) it) ($#r1_hidden :::"="::: ) (Set (Set "(" ($#k9_xtuple_0 :::"dom"::: ) "f" ")" ) ($#k3_xboole_0 :::"/\"::: ) (Set "(" ($#k9_xtuple_0 :::"dom"::: ) "g" ")" ))) & (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 (Set "(" "f" ($#k1_funct_1 :::"."::: ) (Set (Var "x")) ")" ) ($#k18_valued_1 :::"(#)"::: ) (Set "(" "g" ($#k1_funct_1 :::"."::: ) (Set (Var "x")) ")" ))) ")" ) ")" ); end; :: deftheorem defines :::"<##>"::: VALUED_2:def 47 : (Bool "for" (Set (Var "Y1")) "," (Set (Var "Y2")) "being" ($#v1_valued_2 :::"complex-functions-membered"::: ) ($#m1_hidden :::"set"::: ) (Bool "for" (Set (Var "f")) "being" (Set (Var "b1")) ($#v5_relat_1 :::"-valued"::: ) ($#m1_hidden :::"Function":::) (Bool "for" (Set (Var "g")) "being" (Set (Var "b2")) ($#v5_relat_1 :::"-valued"::: ) ($#m1_hidden :::"Function":::) (Bool "for" (Set (Var "b5")) "being" ($#m1_hidden :::"Function":::) "holds" (Bool "(" (Bool (Set (Var "b5")) ($#r1_hidden :::"="::: ) (Set (Set (Var "f")) ($#k83_valued_2 :::"<##>"::: ) (Set (Var "g")))) "iff" (Bool "(" (Bool (Set ($#k9_xtuple_0 :::"dom"::: ) (Set (Var "b5"))) ($#r1_hidden :::"="::: ) (Set (Set "(" ($#k9_xtuple_0 :::"dom"::: ) (Set (Var "f")) ")" ) ($#k3_xboole_0 :::"/\"::: ) (Set "(" ($#k9_xtuple_0 :::"dom"::: ) (Set (Var "g")) ")" ))) & (Bool "(" "for" (Set (Var "x")) "being" ($#m1_hidden :::"set"::: ) "st" (Bool (Bool (Set (Var "x")) ($#r2_hidden :::"in"::: ) (Set ($#k9_xtuple_0 :::"dom"::: ) (Set (Var "b5"))))) "holds" (Bool (Set (Set (Var "b5")) ($#k1_funct_1 :::"."::: ) (Set (Var "x"))) ($#r1_hidden :::"="::: ) (Set (Set "(" (Set (Var "f")) ($#k1_funct_1 :::"."::: ) (Set (Var "x")) ")" ) ($#k18_valued_1 :::"(#)"::: ) (Set "(" (Set (Var "g")) ($#k1_funct_1 :::"."::: ) (Set (Var "x")) ")" ))) ")" ) ")" ) ")" ))))); definitionlet "X1", "X2" be ($#m1_hidden :::"set"::: ) ; let "Y1", "Y2" be ($#v1_valued_2 :::"complex-functions-membered"::: ) ($#m1_hidden :::"set"::: ) ; let "f" be ($#m1_subset_1 :::"PartFunc":::) "of" (Set (Const "X1")) "," (Set (Const "Y1")); let "g" be ($#m1_subset_1 :::"PartFunc":::) "of" (Set (Const "X2")) "," (Set (Const "Y2")); :: original: :::"<##>"::: redefine func "f" :::"<##>"::: "g" -> ($#m1_subset_1 :::"PartFunc":::) "of" (Set "(" "X1" ($#k3_xboole_0 :::"/\"::: ) "X2" ")" ) "," (Set "(" ($#k2_valued_2 :::"C_PFuncs"::: ) (Set "(" (Set "(" ($#k1_valued_2 :::"DOMS"::: ) "Y1" ")" ) ($#k3_xboole_0 :::"/\"::: ) (Set "(" ($#k1_valued_2 :::"DOMS"::: ) "Y2" ")" ) ")" ) ")" ); end; definitionlet "X1", "X2" be ($#m1_hidden :::"set"::: ) ; let "Y1", "Y2" be ($#v3_valued_2 :::"real-functions-membered"::: ) ($#m1_hidden :::"set"::: ) ; let "f" be ($#m1_subset_1 :::"PartFunc":::) "of" (Set (Const "X1")) "," (Set (Const "Y1")); let "g" be ($#m1_subset_1 :::"PartFunc":::) "of" (Set (Const "X2")) "," (Set (Const "Y2")); :: original: :::"<##>"::: redefine func "f" :::"<##>"::: "g" -> ($#m1_subset_1 :::"PartFunc":::) "of" (Set "(" "X1" ($#k3_xboole_0 :::"/\"::: ) "X2" ")" ) "," (Set "(" ($#k6_valued_2 :::"R_PFuncs"::: ) (Set "(" (Set "(" ($#k1_valued_2 :::"DOMS"::: ) "Y1" ")" ) ($#k3_xboole_0 :::"/\"::: ) (Set "(" ($#k1_valued_2 :::"DOMS"::: ) "Y2" ")" ) ")" ) ")" ); end; definitionlet "X1", "X2" be ($#m1_hidden :::"set"::: ) ; let "Y1", "Y2" be ($#v4_valued_2 :::"rational-functions-membered"::: ) ($#m1_hidden :::"set"::: ) ; let "f" be ($#m1_subset_1 :::"PartFunc":::) "of" (Set (Const "X1")) "," (Set (Const "Y1")); let "g" be ($#m1_subset_1 :::"PartFunc":::) "of" (Set (Const "X2")) "," (Set (Const "Y2")); :: original: :::"<##>"::: redefine func "f" :::"<##>"::: "g" -> ($#m1_subset_1 :::"PartFunc":::) "of" (Set "(" "X1" ($#k3_xboole_0 :::"/\"::: ) "X2" ")" ) "," (Set "(" ($#k8_valued_2 :::"Q_PFuncs"::: ) (Set "(" (Set "(" ($#k1_valued_2 :::"DOMS"::: ) "Y1" ")" ) ($#k3_xboole_0 :::"/\"::: ) (Set "(" ($#k1_valued_2 :::"DOMS"::: ) "Y2" ")" ) ")" ) ")" ); end; definitionlet "X1", "X2" be ($#m1_hidden :::"set"::: ) ; let "Y1", "Y2" be ($#v5_valued_2 :::"integer-functions-membered"::: ) ($#m1_hidden :::"set"::: ) ; let "f" be ($#m1_subset_1 :::"PartFunc":::) "of" (Set (Const "X1")) "," (Set (Const "Y1")); let "g" be ($#m1_subset_1 :::"PartFunc":::) "of" (Set (Const "X2")) "," (Set (Const "Y2")); :: original: :::"<##>"::: redefine func "f" :::"<##>"::: "g" -> ($#m1_subset_1 :::"PartFunc":::) "of" (Set "(" "X1" ($#k3_xboole_0 :::"/\"::: ) "X2" ")" ) "," (Set "(" ($#k10_valued_2 :::"I_PFuncs"::: ) (Set "(" (Set "(" ($#k1_valued_2 :::"DOMS"::: ) "Y1" ")" ) ($#k3_xboole_0 :::"/\"::: ) (Set "(" ($#k1_valued_2 :::"DOMS"::: ) "Y2" ")" ) ")" ) ")" ); end; definitionlet "X1", "X2" be ($#m1_hidden :::"set"::: ) ; let "Y1", "Y2" be ($#v6_valued_2 :::"natural-functions-membered"::: ) ($#m1_hidden :::"set"::: ) ; let "f" be ($#m1_subset_1 :::"PartFunc":::) "of" (Set (Const "X1")) "," (Set (Const "Y1")); let "g" be ($#m1_subset_1 :::"PartFunc":::) "of" (Set (Const "X2")) "," (Set (Const "Y2")); :: original: :::"<##>"::: redefine func "f" :::"<##>"::: "g" -> ($#m1_subset_1 :::"PartFunc":::) "of" (Set "(" "X1" ($#k3_xboole_0 :::"/\"::: ) "X2" ")" ) "," (Set "(" ($#k12_valued_2 :::"N_PFuncs"::: ) (Set "(" (Set "(" ($#k1_valued_2 :::"DOMS"::: ) "Y1" ")" ) ($#k3_xboole_0 :::"/\"::: ) (Set "(" ($#k1_valued_2 :::"DOMS"::: ) "Y2" ")" ) ")" ) ")" ); end; theorem :: VALUED_2:83 (Bool "for" (Set (Var "X1")) "," (Set (Var "X2")) "being" ($#m1_hidden :::"set"::: ) (Bool "for" (Set (Var "Y1")) "," (Set (Var "Y2")) "being" ($#v1_valued_2 :::"complex-functions-membered"::: ) ($#m1_hidden :::"set"::: ) (Bool "for" (Set (Var "f1")) "being" ($#m1_subset_1 :::"PartFunc":::) "of" (Set (Var "X1")) "," (Set (Var "Y1")) (Bool "for" (Set (Var "f2")) "being" ($#m1_subset_1 :::"PartFunc":::) "of" (Set (Var "X2")) "," (Set (Var "Y2")) "holds" (Bool (Set (Set (Var "f1")) ($#k84_valued_2 :::"<##>"::: ) (Set (Var "f2"))) ($#r1_hidden :::"="::: ) (Set (Set (Var "f2")) ($#k84_valued_2 :::"<##>"::: ) (Set (Var "f1")))))))) ; theorem :: VALUED_2:84 (Bool "for" (Set (Var "X")) "," (Set (Var "X1")) "," (Set (Var "X2")) "being" ($#m1_hidden :::"set"::: ) (Bool "for" (Set (Var "Y")) "," (Set (Var "Y1")) "," (Set (Var "Y2")) "being" ($#v1_valued_2 :::"complex-functions-membered"::: ) ($#m1_hidden :::"set"::: ) (Bool "for" (Set (Var "f")) "being" ($#m1_subset_1 :::"PartFunc":::) "of" (Set (Var "X")) "," (Set (Var "Y")) (Bool "for" (Set (Var "f1")) "being" ($#m1_subset_1 :::"PartFunc":::) "of" (Set (Var "X1")) "," (Set (Var "Y1")) (Bool "for" (Set (Var "f2")) "being" ($#m1_subset_1 :::"PartFunc":::) "of" (Set (Var "X2")) "," (Set (Var "Y2")) "holds" (Bool (Set (Set "(" (Set (Var "f")) ($#k84_valued_2 :::"<##>"::: ) (Set (Var "f1")) ")" ) ($#k84_valued_2 :::"<##>"::: ) (Set (Var "f2"))) ($#r1_hidden :::"="::: ) (Set (Set (Var "f")) ($#k84_valued_2 :::"<##>"::: ) (Set "(" (Set (Var "f1")) ($#k84_valued_2 :::"<##>"::: ) (Set (Var "f2")) ")" )))))))) ; theorem :: VALUED_2:85 (Bool "for" (Set (Var "X1")) "," (Set (Var "X2")) "being" ($#m1_hidden :::"set"::: ) (Bool "for" (Set (Var "Y1")) "," (Set (Var "Y2")) "being" ($#v1_valued_2 :::"complex-functions-membered"::: ) ($#m1_hidden :::"set"::: ) (Bool "for" (Set (Var "f1")) "being" ($#m1_subset_1 :::"PartFunc":::) "of" (Set (Var "X1")) "," (Set (Var "Y1")) (Bool "for" (Set (Var "f2")) "being" ($#m1_subset_1 :::"PartFunc":::) "of" (Set (Var "X2")) "," (Set (Var "Y2")) "holds" (Bool (Set (Set "(" ($#k16_valued_2 :::"<->"::: ) (Set (Var "f1")) ")" ) ($#k84_valued_2 :::"<##>"::: ) (Set (Var "f2"))) ($#r1_hidden :::"="::: ) (Set ($#k16_valued_2 :::"<->"::: ) (Set "(" (Set (Var "f1")) ($#k84_valued_2 :::"<##>"::: ) (Set (Var "f2")) ")" ))))))) ; theorem :: VALUED_2:86 (Bool "for" (Set (Var "X1")) "," (Set (Var "X2")) "being" ($#m1_hidden :::"set"::: ) (Bool "for" (Set (Var "Y1")) "," (Set (Var "Y2")) "being" ($#v1_valued_2 :::"complex-functions-membered"::: ) ($#m1_hidden :::"set"::: ) (Bool "for" (Set (Var "f1")) "being" ($#m1_subset_1 :::"PartFunc":::) "of" (Set (Var "X1")) "," (Set (Var "Y1")) (Bool "for" (Set (Var "f2")) "being" ($#m1_subset_1 :::"PartFunc":::) "of" (Set (Var "X2")) "," (Set (Var "Y2")) "holds" (Bool (Set (Set (Var "f1")) ($#k84_valued_2 :::"<##>"::: ) (Set "(" ($#k16_valued_2 :::"<->"::: ) (Set (Var "f2")) ")" )) ($#r1_hidden :::"="::: ) (Set ($#k16_valued_2 :::"<->"::: ) (Set "(" (Set (Var "f1")) ($#k84_valued_2 :::"<##>"::: ) (Set (Var "f2")) ")" ))))))) ; theorem :: VALUED_2:87 (Bool "for" (Set (Var "X")) "," (Set (Var "X1")) "," (Set (Var "X2")) "being" ($#m1_hidden :::"set"::: ) (Bool "for" (Set (Var "Y")) "," (Set (Var "Y1")) "," (Set (Var "Y2")) "being" ($#v1_valued_2 :::"complex-functions-membered"::: ) ($#m1_hidden :::"set"::: ) (Bool "for" (Set (Var "f")) "being" ($#m1_subset_1 :::"PartFunc":::) "of" (Set (Var "X")) "," (Set (Var "Y")) (Bool "for" (Set (Var "f1")) "being" ($#m1_subset_1 :::"PartFunc":::) "of" (Set (Var "X1")) "," (Set (Var "Y1")) (Bool "for" (Set (Var "f2")) "being" ($#m1_subset_1 :::"PartFunc":::) "of" (Set (Var "X2")) "," (Set (Var "Y2")) "holds" (Bool (Set (Set (Var "f")) ($#k84_valued_2 :::"<##>"::: ) (Set "(" (Set (Var "f1")) ($#k73_valued_2 :::"<++>"::: ) (Set (Var "f2")) ")" )) ($#r1_hidden :::"="::: ) (Set (Set "(" (Set (Var "f")) ($#k84_valued_2 :::"<##>"::: ) (Set (Var "f1")) ")" ) ($#k73_valued_2 :::"<++>"::: ) (Set "(" (Set (Var "f")) ($#k84_valued_2 :::"<##>"::: ) (Set (Var "f2")) ")" )))))))) ; theorem :: VALUED_2:88 (Bool "for" (Set (Var "X")) "," (Set (Var "X1")) "," (Set (Var "X2")) "being" ($#m1_hidden :::"set"::: ) (Bool "for" (Set (Var "Y")) "," (Set (Var "Y1")) "," (Set (Var "Y2")) "being" ($#v1_valued_2 :::"complex-functions-membered"::: ) ($#m1_hidden :::"set"::: ) (Bool "for" (Set (Var "f")) "being" ($#m1_subset_1 :::"PartFunc":::) "of" (Set (Var "X")) "," (Set (Var "Y")) (Bool "for" (Set (Var "f1")) "being" ($#m1_subset_1 :::"PartFunc":::) "of" (Set (Var "X1")) "," (Set (Var "Y1")) (Bool "for" (Set (Var "f2")) "being" ($#m1_subset_1 :::"PartFunc":::) "of" (Set (Var "X2")) "," (Set (Var "Y2")) "holds" (Bool (Set (Set "(" (Set (Var "f1")) ($#k73_valued_2 :::"<++>"::: ) (Set (Var "f2")) ")" ) ($#k84_valued_2 :::"<##>"::: ) (Set (Var "f"))) ($#r1_hidden :::"="::: ) (Set (Set "(" (Set (Var "f1")) ($#k84_valued_2 :::"<##>"::: ) (Set (Var "f")) ")" ) ($#k73_valued_2 :::"<++>"::: ) (Set "(" (Set (Var "f2")) ($#k84_valued_2 :::"<##>"::: ) (Set (Var "f")) ")" )))))))) ; theorem :: VALUED_2:89 (Bool "for" (Set (Var "X")) "," (Set (Var "X1")) "," (Set (Var "X2")) "being" ($#m1_hidden :::"set"::: ) (Bool "for" (Set (Var "Y")) "," (Set (Var "Y1")) "," (Set (Var "Y2")) "being" ($#v1_valued_2 :::"complex-functions-membered"::: ) ($#m1_hidden :::"set"::: ) (Bool "for" (Set (Var "f")) "being" ($#m1_subset_1 :::"PartFunc":::) "of" (Set (Var "X")) "," (Set (Var "Y")) (Bool "for" (Set (Var "f1")) "being" ($#m1_subset_1 :::"PartFunc":::) "of" (Set (Var "X1")) "," (Set (Var "Y1")) (Bool "for" (Set (Var "f2")) "being" ($#m1_subset_1 :::"PartFunc":::) "of" (Set (Var "X2")) "," (Set (Var "Y2")) "holds" (Bool (Set (Set (Var "f")) ($#k84_valued_2 :::"<##>"::: ) (Set "(" (Set (Var "f1")) ($#k79_valued_2 :::"<-->"::: ) (Set (Var "f2")) ")" )) ($#r1_hidden :::"="::: ) (Set (Set "(" (Set (Var "f")) ($#k84_valued_2 :::"<##>"::: ) (Set (Var "f1")) ")" ) ($#k79_valued_2 :::"<-->"::: ) (Set "(" (Set (Var "f")) ($#k84_valued_2 :::"<##>"::: ) (Set (Var "f2")) ")" )))))))) ; theorem :: VALUED_2:90 (Bool "for" (Set (Var "X")) "," (Set (Var "X1")) "," (Set (Var "X2")) "being" ($#m1_hidden :::"set"::: ) (Bool "for" (Set (Var "Y")) "," (Set (Var "Y1")) "," (Set (Var "Y2")) "being" ($#v1_valued_2 :::"complex-functions-membered"::: ) ($#m1_hidden :::"set"::: ) (Bool "for" (Set (Var "f")) "being" ($#m1_subset_1 :::"PartFunc":::) "of" (Set (Var "X")) "," (Set (Var "Y")) (Bool "for" (Set (Var "f1")) "being" ($#m1_subset_1 :::"PartFunc":::) "of" (Set (Var "X1")) "," (Set (Var "Y1")) (Bool "for" (Set (Var "f2")) "being" ($#m1_subset_1 :::"PartFunc":::) "of" (Set (Var "X2")) "," (Set (Var "Y2")) "holds" (Bool (Set (Set "(" (Set (Var "f1")) ($#k79_valued_2 :::"<-->"::: ) (Set (Var "f2")) ")" ) ($#k84_valued_2 :::"<##>"::: ) (Set (Var "f"))) ($#r1_hidden :::"="::: ) (Set (Set "(" (Set (Var "f1")) ($#k84_valued_2 :::"<##>"::: ) (Set (Var "f")) ")" ) ($#k79_valued_2 :::"<-->"::: ) (Set "(" (Set (Var "f2")) ($#k84_valued_2 :::"<##>"::: ) (Set (Var "f")) ")" )))))))) ; definitionlet "Y1", "Y2" be ($#v1_valued_2 :::"complex-functions-membered"::: ) ($#m1_hidden :::"set"::: ) ; let "f" be (Set (Const "Y1")) ($#v5_relat_1 :::"-valued"::: ) ($#m1_hidden :::"Function":::); let "g" be (Set (Const "Y2")) ($#v5_relat_1 :::"-valued"::: ) ($#m1_hidden :::"Function":::); func "f" :::""::: "g" -> ($#m1_hidden :::"Function":::) means :: VALUED_2:def 48 (Bool "(" (Bool (Set ($#k9_xtuple_0 :::"dom"::: ) it) ($#r1_hidden :::"="::: ) (Set (Set "(" ($#k9_xtuple_0 :::"dom"::: ) "f" ")" ) ($#k3_xboole_0 :::"/\"::: ) (Set "(" ($#k9_xtuple_0 :::"dom"::: ) "g" ")" ))) & (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 (Set "(" "f" ($#k1_funct_1 :::"."::: ) (Set (Var "x")) ")" ) ($#k50_valued_1 :::"/""::: ) (Set "(" "g" ($#k1_funct_1 :::"."::: ) (Set (Var "x")) ")" ))) ")" ) ")" ); end; :: deftheorem defines :::""::: VALUED_2:def 48 : (Bool "for" (Set (Var "Y1")) "," (Set (Var "Y2")) "being" ($#v1_valued_2 :::"complex-functions-membered"::: ) ($#m1_hidden :::"set"::: ) (Bool "for" (Set (Var "f")) "being" (Set (Var "b1")) ($#v5_relat_1 :::"-valued"::: ) ($#m1_hidden :::"Function":::) (Bool "for" (Set (Var "g")) "being" (Set (Var "b2")) ($#v5_relat_1 :::"-valued"::: ) ($#m1_hidden :::"Function":::) (Bool "for" (Set (Var "b5")) "being" ($#m1_hidden :::"Function":::) "holds" (Bool "(" (Bool (Set (Var "b5")) ($#r1_hidden :::"="::: ) (Set (Set (Var "f")) ($#k89_valued_2 :::""::: ) (Set (Var "g")))) "iff" (Bool "(" (Bool (Set ($#k9_xtuple_0 :::"dom"::: ) (Set (Var "b5"))) ($#r1_hidden :::"="::: ) (Set (Set "(" ($#k9_xtuple_0 :::"dom"::: ) (Set (Var "f")) ")" ) ($#k3_xboole_0 :::"/\"::: ) (Set "(" ($#k9_xtuple_0 :::"dom"::: ) (Set (Var "g")) ")" ))) & (Bool "(" "for" (Set (Var "x")) "being" ($#m1_hidden :::"set"::: ) "st" (Bool (Bool (Set (Var "x")) ($#r2_hidden :::"in"::: ) (Set ($#k9_xtuple_0 :::"dom"::: ) (Set (Var "b5"))))) "holds" (Bool (Set (Set (Var "b5")) ($#k1_funct_1 :::"."::: ) (Set (Var "x"))) ($#r1_hidden :::"="::: ) (Set (Set "(" (Set (Var "f")) ($#k1_funct_1 :::"."::: ) (Set (Var "x")) ")" ) ($#k50_valued_1 :::"/""::: ) (Set "(" (Set (Var "g")) ($#k1_funct_1 :::"."::: ) (Set (Var "x")) ")" ))) ")" ) ")" ) ")" ))))); definitionlet "X1", "X2" be ($#m1_hidden :::"set"::: ) ; let "Y1", "Y2" be ($#v1_valued_2 :::"complex-functions-membered"::: ) ($#m1_hidden :::"set"::: ) ; let "f" be ($#m1_subset_1 :::"PartFunc":::) "of" (Set (Const "X1")) "," (Set (Const "Y1")); let "g" be ($#m1_subset_1 :::"PartFunc":::) "of" (Set (Const "X2")) "," (Set (Const "Y2")); :: original: :::""::: redefine func "f" :::""::: "g" -> ($#m1_subset_1 :::"PartFunc":::) "of" (Set "(" "X1" ($#k3_xboole_0 :::"/\"::: ) "X2" ")" ) "," (Set "(" ($#k2_valued_2 :::"C_PFuncs"::: ) (Set "(" (Set "(" ($#k1_valued_2 :::"DOMS"::: ) "Y1" ")" ) ($#k3_xboole_0 :::"/\"::: ) (Set "(" ($#k1_valued_2 :::"DOMS"::: ) "Y2" ")" ) ")" ) ")" ); end; definitionlet "X1", "X2" be ($#m1_hidden :::"set"::: ) ; let "Y1", "Y2" be ($#v3_valued_2 :::"real-functions-membered"::: ) ($#m1_hidden :::"set"::: ) ; let "f" be ($#m1_subset_1 :::"PartFunc":::) "of" (Set (Const "X1")) "," (Set (Const "Y1")); let "g" be ($#m1_subset_1 :::"PartFunc":::) "of" (Set (Const "X2")) "," (Set (Const "Y2")); :: original: :::""::: redefine func "f" :::""::: "g" -> ($#m1_subset_1 :::"PartFunc":::) "of" (Set "(" "X1" ($#k3_xboole_0 :::"/\"::: ) "X2" ")" ) "," (Set "(" ($#k6_valued_2 :::"R_PFuncs"::: ) (Set "(" (Set "(" ($#k1_valued_2 :::"DOMS"::: ) "Y1" ")" ) ($#k3_xboole_0 :::"/\"::: ) (Set "(" ($#k1_valued_2 :::"DOMS"::: ) "Y2" ")" ) ")" ) ")" ); end; definitionlet "X1", "X2" be ($#m1_hidden :::"set"::: ) ; let "Y1", "Y2" be ($#v4_valued_2 :::"rational-functions-membered"::: ) ($#m1_hidden :::"set"::: ) ; let "f" be ($#m1_subset_1 :::"PartFunc":::) "of" (Set (Const "X1")) "," (Set (Const "Y1")); let "g" be ($#m1_subset_1 :::"PartFunc":::) "of" (Set (Const "X2")) "," (Set (Const "Y2")); :: original: :::""::: redefine func "f" :::""::: "g" -> ($#m1_subset_1 :::"PartFunc":::) "of" (Set "(" "X1" ($#k3_xboole_0 :::"/\"::: ) "X2" ")" ) "," (Set "(" ($#k8_valued_2 :::"Q_PFuncs"::: ) (Set "(" (Set "(" ($#k1_valued_2 :::"DOMS"::: ) "Y1" ")" ) ($#k3_xboole_0 :::"/\"::: ) (Set "(" ($#k1_valued_2 :::"DOMS"::: ) "Y2" ")" ) ")" ) ")" ); end; theorem :: VALUED_2:91 (Bool "for" (Set (Var "X1")) "," (Set (Var "X2")) "being" ($#m1_hidden :::"set"::: ) (Bool "for" (Set (Var "Y1")) "," (Set (Var "Y2")) "being" ($#v1_valued_2 :::"complex-functions-membered"::: ) ($#m1_hidden :::"set"::: ) (Bool "for" (Set (Var "f1")) "being" ($#m1_subset_1 :::"PartFunc":::) "of" (Set (Var "X1")) "," (Set (Var "Y1")) (Bool "for" (Set (Var "f2")) "being" ($#m1_subset_1 :::"PartFunc":::) "of" (Set (Var "X2")) "," (Set (Var "Y2")) "holds" (Bool (Set (Set "(" ($#k16_valued_2 :::"<->"::: ) (Set (Var "f1")) ")" ) ($#k90_valued_2 :::""::: ) (Set (Var "f2"))) ($#r1_hidden :::"="::: ) (Set ($#k16_valued_2 :::"<->"::: ) (Set "(" (Set (Var "f1")) ($#k90_valued_2 :::""::: ) (Set (Var "f2")) ")" ))))))) ; theorem :: VALUED_2:92 (Bool "for" (Set (Var "X1")) "," (Set (Var "X2")) "being" ($#m1_hidden :::"set"::: ) (Bool "for" (Set (Var "Y1")) "," (Set (Var "Y2")) "being" ($#v1_valued_2 :::"complex-functions-membered"::: ) ($#m1_hidden :::"set"::: ) (Bool "for" (Set (Var "f1")) "being" ($#m1_subset_1 :::"PartFunc":::) "of" (Set (Var "X1")) "," (Set (Var "Y1")) (Bool "for" (Set (Var "f2")) "being" ($#m1_subset_1 :::"PartFunc":::) "of" (Set (Var "X2")) "," (Set (Var "Y2")) "holds" (Bool (Set (Set (Var "f1")) ($#k90_valued_2 :::""::: ) (Set "(" ($#k16_valued_2 :::"<->"::: ) (Set (Var "f2")) ")" )) ($#r1_hidden :::"="::: ) (Set ($#k16_valued_2 :::"<->"::: ) (Set "(" (Set (Var "f1")) ($#k90_valued_2 :::""::: ) (Set (Var "f2")) ")" ))))))) ; theorem :: VALUED_2:93 (Bool "for" (Set (Var "X")) "," (Set (Var "X1")) "," (Set (Var "X2")) "being" ($#m1_hidden :::"set"::: ) (Bool "for" (Set (Var "Y")) "," (Set (Var "Y1")) "," (Set (Var "Y2")) "being" ($#v1_valued_2 :::"complex-functions-membered"::: ) ($#m1_hidden :::"set"::: ) (Bool "for" (Set (Var "f")) "being" ($#m1_subset_1 :::"PartFunc":::) "of" (Set (Var "X")) "," (Set (Var "Y")) (Bool "for" (Set (Var "f1")) "being" ($#m1_subset_1 :::"PartFunc":::) "of" (Set (Var "X1")) "," (Set (Var "Y1")) (Bool "for" (Set (Var "f2")) "being" ($#m1_subset_1 :::"PartFunc":::) "of" (Set (Var "X2")) "," (Set (Var "Y2")) "holds" (Bool (Set (Set "(" (Set (Var "f")) ($#k84_valued_2 :::"<##>"::: ) (Set (Var "f1")) ")" ) ($#k90_valued_2 :::""::: ) (Set (Var "f2"))) ($#r1_hidden :::"="::: ) (Set (Set (Var "f")) ($#k84_valued_2 :::"<##>"::: ) (Set "(" (Set (Var "f1")) ($#k90_valued_2 :::""::: ) (Set (Var "f2")) ")" )))))))) ; theorem :: VALUED_2:94 (Bool "for" (Set (Var "X")) "," (Set (Var "X1")) "," (Set (Var "X2")) "being" ($#m1_hidden :::"set"::: ) (Bool "for" (Set (Var "Y")) "," (Set (Var "Y1")) "," (Set (Var "Y2")) "being" ($#v1_valued_2 :::"complex-functions-membered"::: ) ($#m1_hidden :::"set"::: ) (Bool "for" (Set (Var "f")) "being" ($#m1_subset_1 :::"PartFunc":::) "of" (Set (Var "X")) "," (Set (Var "Y")) (Bool "for" (Set (Var "f1")) "being" ($#m1_subset_1 :::"PartFunc":::) "of" (Set (Var "X1")) "," (Set (Var "Y1")) (Bool "for" (Set (Var "f2")) "being" ($#m1_subset_1 :::"PartFunc":::) "of" (Set (Var "X2")) "," (Set (Var "Y2")) "holds" (Bool (Set (Set "(" (Set (Var "f")) ($#k90_valued_2 :::""::: ) (Set (Var "f1")) ")" ) ($#k84_valued_2 :::"<##>"::: ) (Set (Var "f2"))) ($#r1_hidden :::"="::: ) (Set (Set "(" (Set (Var "f")) ($#k84_valued_2 :::"<##>"::: ) (Set (Var "f2")) ")" ) ($#k90_valued_2 :::""::: ) (Set (Var "f1"))))))))) ; theorem :: VALUED_2:95 (Bool "for" (Set (Var "X")) "," (Set (Var "X1")) "," (Set (Var "X2")) "being" ($#m1_hidden :::"set"::: ) (Bool "for" (Set (Var "Y")) "," (Set (Var "Y1")) "," (Set (Var "Y2")) "being" ($#v1_valued_2 :::"complex-functions-membered"::: ) ($#m1_hidden :::"set"::: ) (Bool "for" (Set (Var "f")) "being" ($#m1_subset_1 :::"PartFunc":::) "of" (Set (Var "X")) "," (Set (Var "Y")) (Bool "for" (Set (Var "f1")) "being" ($#m1_subset_1 :::"PartFunc":::) "of" (Set (Var "X1")) "," (Set (Var "Y1")) (Bool "for" (Set (Var "f2")) "being" ($#m1_subset_1 :::"PartFunc":::) "of" (Set (Var "X2")) "," (Set (Var "Y2")) "holds" (Bool (Set (Set "(" (Set (Var "f")) ($#k90_valued_2 :::""::: ) (Set (Var "f1")) ")" ) ($#k90_valued_2 :::""::: ) (Set (Var "f2"))) ($#r1_hidden :::"="::: ) (Set (Set (Var "f")) ($#k90_valued_2 :::""::: ) (Set "(" (Set (Var "f1")) ($#k84_valued_2 :::"<##>"::: ) (Set (Var "f2")) ")" )))))))) ; theorem :: VALUED_2:96 (Bool "for" (Set (Var "X")) "," (Set (Var "X1")) "," (Set (Var "X2")) "being" ($#m1_hidden :::"set"::: ) (Bool "for" (Set (Var "Y")) "," (Set (Var "Y1")) "," (Set (Var "Y2")) "being" ($#v1_valued_2 :::"complex-functions-membered"::: ) ($#m1_hidden :::"set"::: ) (Bool "for" (Set (Var "f")) "being" ($#m1_subset_1 :::"PartFunc":::) "of" (Set (Var "X")) "," (Set (Var "Y")) (Bool "for" (Set (Var "f1")) "being" ($#m1_subset_1 :::"PartFunc":::) "of" (Set (Var "X1")) "," (Set (Var "Y1")) (Bool "for" (Set (Var "f2")) "being" ($#m1_subset_1 :::"PartFunc":::) "of" (Set (Var "X2")) "," (Set (Var "Y2")) "holds" (Bool (Set (Set "(" (Set (Var "f1")) ($#k73_valued_2 :::"<++>"::: ) (Set (Var "f2")) ")" ) ($#k90_valued_2 :::""::: ) (Set (Var "f"))) ($#r1_hidden :::"="::: ) (Set (Set "(" (Set (Var "f1")) ($#k90_valued_2 :::""::: ) (Set (Var "f")) ")" ) ($#k73_valued_2 :::"<++>"::: ) (Set "(" (Set (Var "f2")) ($#k90_valued_2 :::""::: ) (Set (Var "f")) ")" )))))))) ; theorem :: VALUED_2:97 (Bool "for" (Set (Var "X")) "," (Set (Var "X1")) "," (Set (Var "X2")) "being" ($#m1_hidden :::"set"::: ) (Bool "for" (Set (Var "Y")) "," (Set (Var "Y1")) "," (Set (Var "Y2")) "being" ($#v1_valued_2 :::"complex-functions-membered"::: ) ($#m1_hidden :::"set"::: ) (Bool "for" (Set (Var "f")) "being" ($#m1_subset_1 :::"PartFunc":::) "of" (Set (Var "X")) "," (Set (Var "Y")) (Bool "for" (Set (Var "f1")) "being" ($#m1_subset_1 :::"PartFunc":::) "of" (Set (Var "X1")) "," (Set (Var "Y1")) (Bool "for" (Set (Var "f2")) "being" ($#m1_subset_1 :::"PartFunc":::) "of" (Set (Var "X2")) "," (Set (Var "Y2")) "holds" (Bool (Set (Set "(" (Set (Var "f1")) ($#k79_valued_2 :::"<-->"::: ) (Set (Var "f2")) ")" ) ($#k90_valued_2 :::""::: ) (Set (Var "f"))) ($#r1_hidden :::"="::: ) (Set (Set "(" (Set (Var "f1")) ($#k90_valued_2 :::""::: ) (Set (Var "f")) ")" ) ($#k79_valued_2 :::"<-->"::: ) (Set "(" (Set (Var "f2")) ($#k90_valued_2 :::""::: ) (Set (Var "f")) ")" )))))))) ;