:: VALUED_1 semantic presentation begin registration cluster ($#v1_relat_1 :::"Relation-like"::: ) ($#v1_funct_1 :::"Function-like"::: ) ($#v1_valued_0 :::"complex-valued"::: ) ($#v1_finseq_1 :::"FinSequence-like"::: ) for ($#m1_hidden :::"set"::: ) ; end; registrationlet "r" be ($#v1_rat_1 :::"rational"::: ) ($#m1_hidden :::"number"::: ) ; cluster (Set ($#k16_complex1 :::"|."::: ) "r" ($#k16_complex1 :::".|"::: ) ) -> ($#v1_rat_1 :::"rational"::: ) ; end; definitionlet "f1", "f2" be ($#v1_valued_0 :::"complex-valued"::: ) ($#m1_hidden :::"Function":::); func "f1" :::"+"::: "f2" -> ($#m1_hidden :::"Function":::) means :: VALUED_1:def 1 (Bool "(" (Bool (Set ($#k9_xtuple_0 :::"dom"::: ) it) ($#r1_hidden :::"="::: ) (Set (Set "(" ($#k9_xtuple_0 :::"dom"::: ) "f1" ")" ) ($#k3_xboole_0 :::"/\"::: ) (Set "(" ($#k9_xtuple_0 :::"dom"::: ) "f2" ")" ))) & (Bool "(" "for" (Set (Var "c")) "being" ($#m1_hidden :::"set"::: ) "st" (Bool (Bool (Set (Var "c")) ($#r2_hidden :::"in"::: ) (Set ($#k9_xtuple_0 :::"dom"::: ) it))) "holds" (Bool (Set it ($#k1_funct_1 :::"."::: ) (Set (Var "c"))) ($#r1_hidden :::"="::: ) (Set (Set "(" "f1" ($#k1_funct_1 :::"."::: ) (Set (Var "c")) ")" ) ($#k2_xcmplx_0 :::"+"::: ) (Set "(" "f2" ($#k1_funct_1 :::"."::: ) (Set (Var "c")) ")" ))) ")" ) ")" ); commutativity (Bool "for" (Set (Var "b1")) "being" ($#m1_hidden :::"Function":::) (Bool "for" (Set (Var "f1")) "," (Set (Var "f2")) "being" ($#v1_valued_0 :::"complex-valued"::: ) ($#m1_hidden :::"Function":::) "st" (Bool (Bool (Set ($#k9_xtuple_0 :::"dom"::: ) (Set (Var "b1"))) ($#r1_hidden :::"="::: ) (Set (Set "(" ($#k9_xtuple_0 :::"dom"::: ) (Set (Var "f1")) ")" ) ($#k3_xboole_0 :::"/\"::: ) (Set "(" ($#k9_xtuple_0 :::"dom"::: ) (Set (Var "f2")) ")" ))) & (Bool "(" "for" (Set (Var "c")) "being" ($#m1_hidden :::"set"::: ) "st" (Bool (Bool (Set (Var "c")) ($#r2_hidden :::"in"::: ) (Set ($#k9_xtuple_0 :::"dom"::: ) (Set (Var "b1"))))) "holds" (Bool (Set (Set (Var "b1")) ($#k1_funct_1 :::"."::: ) (Set (Var "c"))) ($#r1_hidden :::"="::: ) (Set (Set "(" (Set (Var "f1")) ($#k1_funct_1 :::"."::: ) (Set (Var "c")) ")" ) ($#k2_xcmplx_0 :::"+"::: ) (Set "(" (Set (Var "f2")) ($#k1_funct_1 :::"."::: ) (Set (Var "c")) ")" ))) ")" )) "holds" (Bool "(" (Bool (Set ($#k9_xtuple_0 :::"dom"::: ) (Set (Var "b1"))) ($#r1_hidden :::"="::: ) (Set (Set "(" ($#k9_xtuple_0 :::"dom"::: ) (Set (Var "f2")) ")" ) ($#k3_xboole_0 :::"/\"::: ) (Set "(" ($#k9_xtuple_0 :::"dom"::: ) (Set (Var "f1")) ")" ))) & (Bool "(" "for" (Set (Var "c")) "being" ($#m1_hidden :::"set"::: ) "st" (Bool (Bool (Set (Var "c")) ($#r2_hidden :::"in"::: ) (Set ($#k9_xtuple_0 :::"dom"::: ) (Set (Var "b1"))))) "holds" (Bool (Set (Set (Var "b1")) ($#k1_funct_1 :::"."::: ) (Set (Var "c"))) ($#r1_hidden :::"="::: ) (Set (Set "(" (Set (Var "f2")) ($#k1_funct_1 :::"."::: ) (Set (Var "c")) ")" ) ($#k2_xcmplx_0 :::"+"::: ) (Set "(" (Set (Var "f1")) ($#k1_funct_1 :::"."::: ) (Set (Var "c")) ")" ))) ")" ) ")" ))) ; end; :: deftheorem defines :::"+"::: VALUED_1:def 1 : (Bool "for" (Set (Var "f1")) "," (Set (Var "f2")) "being" ($#v1_valued_0 :::"complex-valued"::: ) ($#m1_hidden :::"Function":::) (Bool "for" (Set (Var "b3")) "being" ($#m1_hidden :::"Function":::) "holds" (Bool "(" (Bool (Set (Var "b3")) ($#r1_hidden :::"="::: ) (Set (Set (Var "f1")) ($#k1_valued_1 :::"+"::: ) (Set (Var "f2")))) "iff" (Bool "(" (Bool (Set ($#k9_xtuple_0 :::"dom"::: ) (Set (Var "b3"))) ($#r1_hidden :::"="::: ) (Set (Set "(" ($#k9_xtuple_0 :::"dom"::: ) (Set (Var "f1")) ")" ) ($#k3_xboole_0 :::"/\"::: ) (Set "(" ($#k9_xtuple_0 :::"dom"::: ) (Set (Var "f2")) ")" ))) & (Bool "(" "for" (Set (Var "c")) "being" ($#m1_hidden :::"set"::: ) "st" (Bool (Bool (Set (Var "c")) ($#r2_hidden :::"in"::: ) (Set ($#k9_xtuple_0 :::"dom"::: ) (Set (Var "b3"))))) "holds" (Bool (Set (Set (Var "b3")) ($#k1_funct_1 :::"."::: ) (Set (Var "c"))) ($#r1_hidden :::"="::: ) (Set (Set "(" (Set (Var "f1")) ($#k1_funct_1 :::"."::: ) (Set (Var "c")) ")" ) ($#k2_xcmplx_0 :::"+"::: ) (Set "(" (Set (Var "f2")) ($#k1_funct_1 :::"."::: ) (Set (Var "c")) ")" ))) ")" ) ")" ) ")" ))); registrationlet "f1", "f2" be ($#v1_valued_0 :::"complex-valued"::: ) ($#m1_hidden :::"Function":::); cluster (Set "f1" ($#k1_valued_1 :::"+"::: ) "f2") -> ($#v1_valued_0 :::"complex-valued"::: ) ; end; registrationlet "f1", "f2" be ($#v3_valued_0 :::"real-valued"::: ) ($#m1_hidden :::"Function":::); cluster (Set "f1" ($#k1_valued_1 :::"+"::: ) "f2") -> ($#v3_valued_0 :::"real-valued"::: ) ; end; registrationlet "f1", "f2" be (Set ($#k3_numbers :::"RAT"::: ) ) ($#v5_relat_1 :::"-valued"::: ) ($#m1_hidden :::"Function":::); cluster (Set "f1" ($#k1_valued_1 :::"+"::: ) "f2") -> (Set ($#k3_numbers :::"RAT"::: ) ) ($#v5_relat_1 :::"-valued"::: ) ; end; registrationlet "f1", "f2" be (Set ($#k4_numbers :::"INT"::: ) ) ($#v5_relat_1 :::"-valued"::: ) ($#m1_hidden :::"Function":::); cluster (Set "f1" ($#k1_valued_1 :::"+"::: ) "f2") -> (Set ($#k4_numbers :::"INT"::: ) ) ($#v5_relat_1 :::"-valued"::: ) ; end; registrationlet "f1", "f2" be ($#v4_valued_0 :::"natural-valued"::: ) ($#m1_hidden :::"Function":::); cluster (Set "f1" ($#k1_valued_1 :::"+"::: ) "f2") -> ($#v4_valued_0 :::"natural-valued"::: ) ; end; definitionlet "C" be ($#m1_hidden :::"set"::: ) ; let "D1", "D2" be ($#v1_membered :::"complex-membered"::: ) ($#m1_hidden :::"set"::: ) ; let "f1" be ($#m1_subset_1 :::"PartFunc":::) "of" (Set (Const "C")) "," (Set (Const "D1")); let "f2" be ($#m1_subset_1 :::"PartFunc":::) "of" (Set (Const "C")) "," (Set (Const "D2")); :: original: :::"+"::: redefine func "f1" :::"+"::: "f2" -> ($#m1_subset_1 :::"PartFunc":::) "of" "C" "," (Set ($#k2_numbers :::"COMPLEX"::: ) ); end; definitionlet "C" be ($#m1_hidden :::"set"::: ) ; let "D1", "D2" be ($#v3_membered :::"real-membered"::: ) ($#m1_hidden :::"set"::: ) ; let "f1" be ($#m1_subset_1 :::"PartFunc":::) "of" (Set (Const "C")) "," (Set (Const "D1")); let "f2" be ($#m1_subset_1 :::"PartFunc":::) "of" (Set (Const "C")) "," (Set (Const "D2")); :: original: :::"+"::: redefine func "f1" :::"+"::: "f2" -> ($#m1_subset_1 :::"PartFunc":::) "of" "C" "," (Set ($#k1_numbers :::"REAL"::: ) ); end; definitionlet "C" be ($#m1_hidden :::"set"::: ) ; let "D1", "D2" be ($#v4_membered :::"rational-membered"::: ) ($#m1_hidden :::"set"::: ) ; let "f1" be ($#m1_subset_1 :::"PartFunc":::) "of" (Set (Const "C")) "," (Set (Const "D1")); let "f2" be ($#m1_subset_1 :::"PartFunc":::) "of" (Set (Const "C")) "," (Set (Const "D2")); :: original: :::"+"::: redefine func "f1" :::"+"::: "f2" -> ($#m1_subset_1 :::"PartFunc":::) "of" "C" "," (Set ($#k3_numbers :::"RAT"::: ) ); end; definitionlet "C" be ($#m1_hidden :::"set"::: ) ; let "D1", "D2" be ($#v5_membered :::"integer-membered"::: ) ($#m1_hidden :::"set"::: ) ; let "f1" be ($#m1_subset_1 :::"PartFunc":::) "of" (Set (Const "C")) "," (Set (Const "D1")); let "f2" be ($#m1_subset_1 :::"PartFunc":::) "of" (Set (Const "C")) "," (Set (Const "D2")); :: original: :::"+"::: redefine func "f1" :::"+"::: "f2" -> ($#m1_subset_1 :::"PartFunc":::) "of" "C" "," (Set ($#k4_numbers :::"INT"::: ) ); end; definitionlet "C" be ($#m1_hidden :::"set"::: ) ; let "D1", "D2" be ($#v6_membered :::"natural-membered"::: ) ($#m1_hidden :::"set"::: ) ; let "f1" be ($#m1_subset_1 :::"PartFunc":::) "of" (Set (Const "C")) "," (Set (Const "D1")); let "f2" be ($#m1_subset_1 :::"PartFunc":::) "of" (Set (Const "C")) "," (Set (Const "D2")); :: original: :::"+"::: redefine func "f1" :::"+"::: "f2" -> ($#m1_subset_1 :::"PartFunc":::) "of" "C" "," (Set ($#k5_numbers :::"NAT"::: ) ); end; registrationlet "C" be ($#m1_hidden :::"set"::: ) ; let "D1", "D2" be ($#~v1_xboole_0 "non" ($#v1_xboole_0 :::"empty"::: ) ) ($#v1_membered :::"complex-membered"::: ) ($#m1_hidden :::"set"::: ) ; let "f1" be ($#m1_subset_1 :::"Function":::) "of" (Set (Const "C")) "," (Set (Const "D1")); let "f2" be ($#m1_subset_1 :::"Function":::) "of" (Set (Const "C")) "," (Set (Const "D2")); cluster (Set "f1" ($#k1_valued_1 :::"+"::: ) "f2") -> ($#v1_partfun1 :::"total"::: ) for ($#m1_subset_1 :::"PartFunc":::) "of" "C" "," (Set ($#k2_numbers :::"COMPLEX"::: ) ); end; registrationlet "C" be ($#m1_hidden :::"set"::: ) ; let "D1", "D2" be ($#~v1_xboole_0 "non" ($#v1_xboole_0 :::"empty"::: ) ) ($#v3_membered :::"real-membered"::: ) ($#m1_hidden :::"set"::: ) ; let "f1" be ($#m1_subset_1 :::"Function":::) "of" (Set (Const "C")) "," (Set (Const "D1")); let "f2" be ($#m1_subset_1 :::"Function":::) "of" (Set (Const "C")) "," (Set (Const "D2")); cluster (Set "f1" ($#k1_valued_1 :::"+"::: ) "f2") -> ($#v1_partfun1 :::"total"::: ) for ($#m1_subset_1 :::"PartFunc":::) "of" "C" "," (Set ($#k1_numbers :::"REAL"::: ) ); end; registrationlet "C" be ($#m1_hidden :::"set"::: ) ; let "D1", "D2" be ($#~v1_xboole_0 "non" ($#v1_xboole_0 :::"empty"::: ) ) ($#v4_membered :::"rational-membered"::: ) ($#m1_hidden :::"set"::: ) ; let "f1" be ($#m1_subset_1 :::"Function":::) "of" (Set (Const "C")) "," (Set (Const "D1")); let "f2" be ($#m1_subset_1 :::"Function":::) "of" (Set (Const "C")) "," (Set (Const "D2")); cluster (Set "f1" ($#k1_valued_1 :::"+"::: ) "f2") -> ($#v1_partfun1 :::"total"::: ) for ($#m1_subset_1 :::"PartFunc":::) "of" "C" "," (Set ($#k3_numbers :::"RAT"::: ) ); end; registrationlet "C" be ($#m1_hidden :::"set"::: ) ; let "D1", "D2" be ($#~v1_xboole_0 "non" ($#v1_xboole_0 :::"empty"::: ) ) ($#v5_membered :::"integer-membered"::: ) ($#m1_hidden :::"set"::: ) ; let "f1" be ($#m1_subset_1 :::"Function":::) "of" (Set (Const "C")) "," (Set (Const "D1")); let "f2" be ($#m1_subset_1 :::"Function":::) "of" (Set (Const "C")) "," (Set (Const "D2")); cluster (Set "f1" ($#k1_valued_1 :::"+"::: ) "f2") -> ($#v1_partfun1 :::"total"::: ) for ($#m1_subset_1 :::"PartFunc":::) "of" "C" "," (Set ($#k4_numbers :::"INT"::: ) ); end; registrationlet "C" be ($#m1_hidden :::"set"::: ) ; let "D1", "D2" be ($#~v1_xboole_0 "non" ($#v1_xboole_0 :::"empty"::: ) ) ($#v6_membered :::"natural-membered"::: ) ($#m1_hidden :::"set"::: ) ; let "f1" be ($#m1_subset_1 :::"Function":::) "of" (Set (Const "C")) "," (Set (Const "D1")); let "f2" be ($#m1_subset_1 :::"Function":::) "of" (Set (Const "C")) "," (Set (Const "D2")); cluster (Set "f1" ($#k1_valued_1 :::"+"::: ) "f2") -> ($#v1_partfun1 :::"total"::: ) for ($#m1_subset_1 :::"PartFunc":::) "of" "C" "," (Set ($#k5_numbers :::"NAT"::: ) ); end; theorem :: VALUED_1:1 (Bool "for" (Set (Var "C")) "being" ($#m1_hidden :::"set"::: ) (Bool "for" (Set (Var "D1")) "," (Set (Var "D2")) "being" ($#~v1_xboole_0 "non" ($#v1_xboole_0 :::"empty"::: ) ) ($#v1_membered :::"complex-membered"::: ) ($#m1_hidden :::"set"::: ) (Bool "for" (Set (Var "f1")) "being" ($#m1_subset_1 :::"Function":::) "of" (Set (Var "C")) "," (Set (Var "D1")) (Bool "for" (Set (Var "f2")) "being" ($#m1_subset_1 :::"Function":::) "of" (Set (Var "C")) "," (Set (Var "D2")) (Bool "for" (Set (Var "c")) "being" ($#m1_subset_1 :::"Element"::: ) "of" (Set (Var "C")) "holds" (Bool (Set (Set "(" (Set (Var "f1")) ($#k2_valued_1 :::"+"::: ) (Set (Var "f2")) ")" ) ($#k1_funct_1 :::"."::: ) (Set (Var "c"))) ($#r1_hidden :::"="::: ) (Set (Set "(" (Set (Var "f1")) ($#k1_funct_1 :::"."::: ) (Set (Var "c")) ")" ) ($#k2_xcmplx_0 :::"+"::: ) (Set "(" (Set (Var "f2")) ($#k1_funct_1 :::"."::: ) (Set (Var "c")) ")" )))))))) ; registrationlet "f1", "f2" be ($#v1_valued_0 :::"complex-valued"::: ) ($#m1_hidden :::"FinSequence":::); cluster (Set "f1" ($#k1_valued_1 :::"+"::: ) "f2") -> ($#v1_finseq_1 :::"FinSequence-like"::: ) ; end; begin definitionlet "f" be ($#v1_valued_0 :::"complex-valued"::: ) ($#m1_hidden :::"Function":::); let "r" be ($#v1_xcmplx_0 :::"complex"::: ) ($#m1_hidden :::"number"::: ) ; func "r" :::"+"::: "f" -> ($#m1_hidden :::"Function":::) means :: VALUED_1:def 2 (Bool "(" (Bool (Set ($#k9_xtuple_0 :::"dom"::: ) it) ($#r1_hidden :::"="::: ) (Set ($#k9_xtuple_0 :::"dom"::: ) "f")) & (Bool "(" "for" (Set (Var "c")) "being" ($#m1_hidden :::"set"::: ) "st" (Bool (Bool (Set (Var "c")) ($#r2_hidden :::"in"::: ) (Set ($#k9_xtuple_0 :::"dom"::: ) it))) "holds" (Bool (Set it ($#k1_funct_1 :::"."::: ) (Set (Var "c"))) ($#r1_hidden :::"="::: ) (Set "r" ($#k2_xcmplx_0 :::"+"::: ) (Set "(" "f" ($#k1_funct_1 :::"."::: ) (Set (Var "c")) ")" ))) ")" ) ")" ); end; :: deftheorem defines :::"+"::: VALUED_1:def 2 : (Bool "for" (Set (Var "f")) "being" ($#v1_valued_0 :::"complex-valued"::: ) ($#m1_hidden :::"Function":::) (Bool "for" (Set (Var "r")) "being" ($#v1_xcmplx_0 :::"complex"::: ) ($#m1_hidden :::"number"::: ) (Bool "for" (Set (Var "b3")) "being" ($#m1_hidden :::"Function":::) "holds" (Bool "(" (Bool (Set (Var "b3")) ($#r1_hidden :::"="::: ) (Set (Set (Var "r")) ($#k7_valued_1 :::"+"::: ) (Set (Var "f")))) "iff" (Bool "(" (Bool (Set ($#k9_xtuple_0 :::"dom"::: ) (Set (Var "b3"))) ($#r1_hidden :::"="::: ) (Set ($#k9_xtuple_0 :::"dom"::: ) (Set (Var "f")))) & (Bool "(" "for" (Set (Var "c")) "being" ($#m1_hidden :::"set"::: ) "st" (Bool (Bool (Set (Var "c")) ($#r2_hidden :::"in"::: ) (Set ($#k9_xtuple_0 :::"dom"::: ) (Set (Var "b3"))))) "holds" (Bool (Set (Set (Var "b3")) ($#k1_funct_1 :::"."::: ) (Set (Var "c"))) ($#r1_hidden :::"="::: ) (Set (Set (Var "r")) ($#k2_xcmplx_0 :::"+"::: ) (Set "(" (Set (Var "f")) ($#k1_funct_1 :::"."::: ) (Set (Var "c")) ")" ))) ")" ) ")" ) ")" )))); notationlet "f" be ($#v1_valued_0 :::"complex-valued"::: ) ($#m1_hidden :::"Function":::); let "r" be ($#v1_xcmplx_0 :::"complex"::: ) ($#m1_hidden :::"number"::: ) ; synonym "f" :::"+"::: "r" for "r" :::"+"::: "f"; end; registrationlet "f" be ($#v1_valued_0 :::"complex-valued"::: ) ($#m1_hidden :::"Function":::); let "r" be ($#v1_xcmplx_0 :::"complex"::: ) ($#m1_hidden :::"number"::: ) ; cluster (Set "r" ($#k7_valued_1 :::"+"::: ) "f") -> ($#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 "r" ($#k7_valued_1 :::"+"::: ) "f") -> ($#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 "r" ($#k7_valued_1 :::"+"::: ) "f") -> (Set ($#k3_numbers :::"RAT"::: ) ) ($#v5_relat_1 :::"-valued"::: ) ; end; registrationlet "f" be (Set ($#k4_numbers :::"INT"::: ) ) ($#v5_relat_1 :::"-valued"::: ) ($#m1_hidden :::"Function":::); let "r" be ($#v1_int_1 :::"integer"::: ) ($#m1_hidden :::"number"::: ) ; cluster (Set "r" ($#k7_valued_1 :::"+"::: ) "f") -> (Set ($#k4_numbers :::"INT"::: ) ) ($#v5_relat_1 :::"-valued"::: ) ; end; registrationlet "f" be ($#v4_valued_0 :::"natural-valued"::: ) ($#m1_hidden :::"Function":::); let "r" be ($#m1_hidden :::"Nat":::); cluster (Set "r" ($#k7_valued_1 :::"+"::: ) "f") -> ($#v4_valued_0 :::"natural-valued"::: ) ; end; definitionlet "C" be ($#m1_hidden :::"set"::: ) ; let "D" be ($#v1_membered :::"complex-membered"::: ) ($#m1_hidden :::"set"::: ) ; let "f" be ($#m1_subset_1 :::"PartFunc":::) "of" (Set (Const "C")) "," (Set (Const "D")); let "r" be ($#v1_xcmplx_0 :::"complex"::: ) ($#m1_hidden :::"number"::: ) ; :: original: :::"+"::: redefine func "r" :::"+"::: "f" -> ($#m1_subset_1 :::"PartFunc":::) "of" "C" "," (Set ($#k2_numbers :::"COMPLEX"::: ) ); end; definitionlet "C" be ($#m1_hidden :::"set"::: ) ; let "D" be ($#v3_membered :::"real-membered"::: ) ($#m1_hidden :::"set"::: ) ; let "f" be ($#m1_subset_1 :::"PartFunc":::) "of" (Set (Const "C")) "," (Set (Const "D")); let "r" be ($#v1_xreal_0 :::"real"::: ) ($#m1_hidden :::"number"::: ) ; :: original: :::"+"::: redefine func "r" :::"+"::: "f" -> ($#m1_subset_1 :::"PartFunc":::) "of" "C" "," (Set ($#k1_numbers :::"REAL"::: ) ); end; definitionlet "C" be ($#m1_hidden :::"set"::: ) ; let "D" be ($#v4_membered :::"rational-membered"::: ) ($#m1_hidden :::"set"::: ) ; let "f" be ($#m1_subset_1 :::"PartFunc":::) "of" (Set (Const "C")) "," (Set (Const "D")); let "r" be ($#v1_rat_1 :::"rational"::: ) ($#m1_hidden :::"number"::: ) ; :: original: :::"+"::: redefine func "r" :::"+"::: "f" -> ($#m1_subset_1 :::"PartFunc":::) "of" "C" "," (Set ($#k3_numbers :::"RAT"::: ) ); end; definitionlet "C" be ($#m1_hidden :::"set"::: ) ; let "D" be ($#v5_membered :::"integer-membered"::: ) ($#m1_hidden :::"set"::: ) ; let "f" be ($#m1_subset_1 :::"PartFunc":::) "of" (Set (Const "C")) "," (Set (Const "D")); let "r" be ($#v1_int_1 :::"integer"::: ) ($#m1_hidden :::"number"::: ) ; :: original: :::"+"::: redefine func "r" :::"+"::: "f" -> ($#m1_subset_1 :::"PartFunc":::) "of" "C" "," (Set ($#k4_numbers :::"INT"::: ) ); end; definitionlet "C" be ($#m1_hidden :::"set"::: ) ; let "D" be ($#v6_membered :::"natural-membered"::: ) ($#m1_hidden :::"set"::: ) ; let "f" be ($#m1_subset_1 :::"PartFunc":::) "of" (Set (Const "C")) "," (Set (Const "D")); let "r" be ($#m1_hidden :::"Nat":::); :: original: :::"+"::: redefine func "r" :::"+"::: "f" -> ($#m1_subset_1 :::"PartFunc":::) "of" "C" "," (Set ($#k5_numbers :::"NAT"::: ) ); end; registrationlet "C" be ($#m1_hidden :::"set"::: ) ; let "D" be ($#~v1_xboole_0 "non" ($#v1_xboole_0 :::"empty"::: ) ) ($#v1_membered :::"complex-membered"::: ) ($#m1_hidden :::"set"::: ) ; let "f" be ($#m1_subset_1 :::"Function":::) "of" (Set (Const "C")) "," (Set (Const "D")); let "r" be ($#v1_xcmplx_0 :::"complex"::: ) ($#m1_hidden :::"number"::: ) ; cluster (Set "r" ($#k7_valued_1 :::"+"::: ) "f") -> ($#v1_partfun1 :::"total"::: ) for ($#m1_subset_1 :::"PartFunc":::) "of" "C" "," (Set ($#k2_numbers :::"COMPLEX"::: ) ); end; registrationlet "C" be ($#m1_hidden :::"set"::: ) ; let "D" be ($#~v1_xboole_0 "non" ($#v1_xboole_0 :::"empty"::: ) ) ($#v3_membered :::"real-membered"::: ) ($#m1_hidden :::"set"::: ) ; let "f" be ($#m1_subset_1 :::"Function":::) "of" (Set (Const "C")) "," (Set (Const "D")); let "r" be ($#v1_xreal_0 :::"real"::: ) ($#m1_hidden :::"number"::: ) ; cluster (Set "r" ($#k7_valued_1 :::"+"::: ) "f") -> ($#v1_partfun1 :::"total"::: ) for ($#m1_subset_1 :::"PartFunc":::) "of" "C" "," (Set ($#k1_numbers :::"REAL"::: ) ); end; registrationlet "C" be ($#m1_hidden :::"set"::: ) ; let "D" be ($#~v1_xboole_0 "non" ($#v1_xboole_0 :::"empty"::: ) ) ($#v4_membered :::"rational-membered"::: ) ($#m1_hidden :::"set"::: ) ; let "f" be ($#m1_subset_1 :::"Function":::) "of" (Set (Const "C")) "," (Set (Const "D")); let "r" be ($#v1_rat_1 :::"rational"::: ) ($#m1_hidden :::"number"::: ) ; cluster (Set "r" ($#k7_valued_1 :::"+"::: ) "f") -> ($#v1_partfun1 :::"total"::: ) for ($#m1_subset_1 :::"PartFunc":::) "of" "C" "," (Set ($#k3_numbers :::"RAT"::: ) ); end; registrationlet "C" be ($#m1_hidden :::"set"::: ) ; let "D" be ($#~v1_xboole_0 "non" ($#v1_xboole_0 :::"empty"::: ) ) ($#v5_membered :::"integer-membered"::: ) ($#m1_hidden :::"set"::: ) ; let "f" be ($#m1_subset_1 :::"Function":::) "of" (Set (Const "C")) "," (Set (Const "D")); let "r" be ($#v1_int_1 :::"integer"::: ) ($#m1_hidden :::"number"::: ) ; cluster (Set "r" ($#k7_valued_1 :::"+"::: ) "f") -> ($#v1_partfun1 :::"total"::: ) for ($#m1_subset_1 :::"PartFunc":::) "of" "C" "," (Set ($#k4_numbers :::"INT"::: ) ); end; registrationlet "C" be ($#m1_hidden :::"set"::: ) ; let "D" be ($#~v1_xboole_0 "non" ($#v1_xboole_0 :::"empty"::: ) ) ($#v6_membered :::"natural-membered"::: ) ($#m1_hidden :::"set"::: ) ; let "f" be ($#m1_subset_1 :::"Function":::) "of" (Set (Const "C")) "," (Set (Const "D")); let "r" be ($#m1_hidden :::"Nat":::); cluster (Set "r" ($#k7_valued_1 :::"+"::: ) "f") -> ($#v1_partfun1 :::"total"::: ) for ($#m1_subset_1 :::"PartFunc":::) "of" "C" "," (Set ($#k5_numbers :::"NAT"::: ) ); end; theorem :: VALUED_1:2 (Bool "for" (Set (Var "C")) "being" ($#~v1_xboole_0 "non" ($#v1_xboole_0 :::"empty"::: ) ) ($#m1_hidden :::"set"::: ) (Bool "for" (Set (Var "D")) "being" ($#~v1_xboole_0 "non" ($#v1_xboole_0 :::"empty"::: ) ) ($#v1_membered :::"complex-membered"::: ) ($#m1_hidden :::"set"::: ) (Bool "for" (Set (Var "f")) "being" ($#m1_subset_1 :::"Function":::) "of" (Set (Var "C")) "," (Set (Var "D")) (Bool "for" (Set (Var "r")) "being" ($#v1_xcmplx_0 :::"complex"::: ) ($#m1_hidden :::"number"::: ) (Bool "for" (Set (Var "c")) "being" ($#m1_subset_1 :::"Element"::: ) "of" (Set (Var "C")) "holds" (Bool (Set (Set "(" (Set (Var "r")) ($#k8_valued_1 :::"+"::: ) (Set (Var "f")) ")" ) ($#k3_funct_2 :::"."::: ) (Set (Var "c"))) ($#r1_hidden :::"="::: ) (Set (Set (Var "r")) ($#k2_xcmplx_0 :::"+"::: ) (Set "(" (Set (Var "f")) ($#k3_funct_2 :::"."::: ) (Set (Var "c")) ")" )))))))) ; registrationlet "f" be ($#v1_valued_0 :::"complex-valued"::: ) ($#m1_hidden :::"FinSequence":::); let "r" be ($#v1_xcmplx_0 :::"complex"::: ) ($#m1_hidden :::"number"::: ) ; cluster (Set "r" ($#k7_valued_1 :::"+"::: ) "f") -> ($#v1_finseq_1 :::"FinSequence-like"::: ) ; end; begin definitionlet "f" be ($#v1_valued_0 :::"complex-valued"::: ) ($#m1_hidden :::"Function":::); let "r" be ($#v1_xcmplx_0 :::"complex"::: ) ($#m1_hidden :::"number"::: ) ; func "f" :::"-"::: "r" -> ($#m1_hidden :::"Function":::) equals :: VALUED_1:def 3 (Set (Set "(" ($#k4_xcmplx_0 :::"-"::: ) "r" ")" ) ($#k7_valued_1 :::"+"::: ) "f"); end; :: deftheorem defines :::"-"::: VALUED_1:def 3 : (Bool "for" (Set (Var "f")) "being" ($#v1_valued_0 :::"complex-valued"::: ) ($#m1_hidden :::"Function":::) (Bool "for" (Set (Var "r")) "being" ($#v1_xcmplx_0 :::"complex"::: ) ($#m1_hidden :::"number"::: ) "holds" (Bool (Set (Set (Var "f")) ($#k13_valued_1 :::"-"::: ) (Set (Var "r"))) ($#r1_hidden :::"="::: ) (Set (Set "(" ($#k4_xcmplx_0 :::"-"::: ) (Set (Var "r")) ")" ) ($#k7_valued_1 :::"+"::: ) (Set (Var "f")))))); theorem :: VALUED_1:3 (Bool "for" (Set (Var "f")) "being" ($#v1_valued_0 :::"complex-valued"::: ) ($#m1_hidden :::"Function":::) (Bool "for" (Set (Var "r")) "being" ($#v1_xcmplx_0 :::"complex"::: ) ($#m1_hidden :::"number"::: ) "holds" (Bool "(" (Bool (Set ($#k9_xtuple_0 :::"dom"::: ) (Set "(" (Set (Var "f")) ($#k13_valued_1 :::"-"::: ) (Set (Var "r")) ")" )) ($#r1_hidden :::"="::: ) (Set ($#k9_xtuple_0 :::"dom"::: ) (Set (Var "f")))) & (Bool "(" "for" (Set (Var "c")) "being" ($#m1_hidden :::"set"::: ) "st" (Bool (Bool (Set (Var "c")) ($#r2_hidden :::"in"::: ) (Set ($#k9_xtuple_0 :::"dom"::: ) (Set (Var "f"))))) "holds" (Bool (Set (Set "(" (Set (Var "f")) ($#k13_valued_1 :::"-"::: ) (Set (Var "r")) ")" ) ($#k1_funct_1 :::"."::: ) (Set (Var "c"))) ($#r1_hidden :::"="::: ) (Set (Set "(" (Set (Var "f")) ($#k1_funct_1 :::"."::: ) (Set (Var "c")) ")" ) ($#k6_xcmplx_0 :::"-"::: ) (Set (Var "r")))) ")" ) ")" ))) ; registrationlet "f" be ($#v1_valued_0 :::"complex-valued"::: ) ($#m1_hidden :::"Function":::); let "r" be ($#v1_xcmplx_0 :::"complex"::: ) ($#m1_hidden :::"number"::: ) ; cluster (Set "f" ($#k13_valued_1 :::"-"::: ) "r") -> ($#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" ($#k13_valued_1 :::"-"::: ) "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" ($#k13_valued_1 :::"-"::: ) "r") -> (Set ($#k3_numbers :::"RAT"::: ) ) ($#v5_relat_1 :::"-valued"::: ) ; end; registrationlet "f" be (Set ($#k4_numbers :::"INT"::: ) ) ($#v5_relat_1 :::"-valued"::: ) ($#m1_hidden :::"Function":::); let "r" be ($#v1_int_1 :::"integer"::: ) ($#m1_hidden :::"number"::: ) ; cluster (Set "f" ($#k13_valued_1 :::"-"::: ) "r") -> (Set ($#k4_numbers :::"INT"::: ) ) ($#v5_relat_1 :::"-valued"::: ) ; end; definitionlet "C" be ($#m1_hidden :::"set"::: ) ; let "D" be ($#v1_membered :::"complex-membered"::: ) ($#m1_hidden :::"set"::: ) ; let "f" be ($#m1_subset_1 :::"PartFunc":::) "of" (Set (Const "C")) "," (Set (Const "D")); let "r" be ($#v1_xcmplx_0 :::"complex"::: ) ($#m1_hidden :::"number"::: ) ; :: original: :::"-"::: redefine func "f" :::"-"::: "r" -> ($#m1_subset_1 :::"PartFunc":::) "of" "C" "," (Set ($#k2_numbers :::"COMPLEX"::: ) ); end; definitionlet "C" be ($#m1_hidden :::"set"::: ) ; let "D" be ($#v3_membered :::"real-membered"::: ) ($#m1_hidden :::"set"::: ) ; let "f" be ($#m1_subset_1 :::"PartFunc":::) "of" (Set (Const "C")) "," (Set (Const "D")); let "r" be ($#v1_xreal_0 :::"real"::: ) ($#m1_hidden :::"number"::: ) ; :: original: :::"-"::: redefine func "f" :::"-"::: "r" -> ($#m1_subset_1 :::"PartFunc":::) "of" "C" "," (Set ($#k1_numbers :::"REAL"::: ) ); end; definitionlet "C" be ($#m1_hidden :::"set"::: ) ; let "D" be ($#v4_membered :::"rational-membered"::: ) ($#m1_hidden :::"set"::: ) ; let "f" be ($#m1_subset_1 :::"PartFunc":::) "of" (Set (Const "C")) "," (Set (Const "D")); let "r" be ($#v1_rat_1 :::"rational"::: ) ($#m1_hidden :::"number"::: ) ; :: original: :::"-"::: redefine func "f" :::"-"::: "r" -> ($#m1_subset_1 :::"PartFunc":::) "of" "C" "," (Set ($#k3_numbers :::"RAT"::: ) ); end; definitionlet "C" be ($#m1_hidden :::"set"::: ) ; let "D" be ($#v5_membered :::"integer-membered"::: ) ($#m1_hidden :::"set"::: ) ; let "f" be ($#m1_subset_1 :::"PartFunc":::) "of" (Set (Const "C")) "," (Set (Const "D")); let "r" be ($#v1_int_1 :::"integer"::: ) ($#m1_hidden :::"number"::: ) ; :: original: :::"-"::: redefine func "f" :::"-"::: "r" -> ($#m1_subset_1 :::"PartFunc":::) "of" "C" "," (Set ($#k4_numbers :::"INT"::: ) ); end; registrationlet "C" be ($#m1_hidden :::"set"::: ) ; let "D" be ($#~v1_xboole_0 "non" ($#v1_xboole_0 :::"empty"::: ) ) ($#v1_membered :::"complex-membered"::: ) ($#m1_hidden :::"set"::: ) ; let "f" be ($#m1_subset_1 :::"Function":::) "of" (Set (Const "C")) "," (Set (Const "D")); let "r" be ($#v1_xcmplx_0 :::"complex"::: ) ($#m1_hidden :::"number"::: ) ; cluster (Set "f" ($#k13_valued_1 :::"-"::: ) "r") -> ($#v1_partfun1 :::"total"::: ) for ($#m1_subset_1 :::"PartFunc":::) "of" "C" "," (Set ($#k2_numbers :::"COMPLEX"::: ) ); end; registrationlet "C" be ($#m1_hidden :::"set"::: ) ; let "D" be ($#~v1_xboole_0 "non" ($#v1_xboole_0 :::"empty"::: ) ) ($#v3_membered :::"real-membered"::: ) ($#m1_hidden :::"set"::: ) ; let "f" be ($#m1_subset_1 :::"Function":::) "of" (Set (Const "C")) "," (Set (Const "D")); let "r" be ($#v1_xreal_0 :::"real"::: ) ($#m1_hidden :::"number"::: ) ; cluster (Set "f" ($#k13_valued_1 :::"-"::: ) "r") -> ($#v1_partfun1 :::"total"::: ) for ($#m1_subset_1 :::"PartFunc":::) "of" "C" "," (Set ($#k1_numbers :::"REAL"::: ) ); end; registrationlet "C" be ($#m1_hidden :::"set"::: ) ; let "D" be ($#~v1_xboole_0 "non" ($#v1_xboole_0 :::"empty"::: ) ) ($#v4_membered :::"rational-membered"::: ) ($#m1_hidden :::"set"::: ) ; let "f" be ($#m1_subset_1 :::"Function":::) "of" (Set (Const "C")) "," (Set (Const "D")); let "r" be ($#v1_rat_1 :::"rational"::: ) ($#m1_hidden :::"number"::: ) ; cluster (Set "f" ($#k13_valued_1 :::"-"::: ) "r") -> ($#v1_partfun1 :::"total"::: ) for ($#m1_subset_1 :::"PartFunc":::) "of" "C" "," (Set ($#k3_numbers :::"RAT"::: ) ); end; registrationlet "C" be ($#m1_hidden :::"set"::: ) ; let "D" be ($#~v1_xboole_0 "non" ($#v1_xboole_0 :::"empty"::: ) ) ($#v5_membered :::"integer-membered"::: ) ($#m1_hidden :::"set"::: ) ; let "f" be ($#m1_subset_1 :::"Function":::) "of" (Set (Const "C")) "," (Set (Const "D")); let "r" be ($#v1_int_1 :::"integer"::: ) ($#m1_hidden :::"number"::: ) ; cluster (Set "f" ($#k13_valued_1 :::"-"::: ) "r") -> ($#v1_partfun1 :::"total"::: ) for ($#m1_subset_1 :::"PartFunc":::) "of" "C" "," (Set ($#k4_numbers :::"INT"::: ) ); end; theorem :: VALUED_1:4 (Bool "for" (Set (Var "C")) "being" ($#~v1_xboole_0 "non" ($#v1_xboole_0 :::"empty"::: ) ) ($#m1_hidden :::"set"::: ) (Bool "for" (Set (Var "D")) "being" ($#~v1_xboole_0 "non" ($#v1_xboole_0 :::"empty"::: ) ) ($#v1_membered :::"complex-membered"::: ) ($#m1_hidden :::"set"::: ) (Bool "for" (Set (Var "f")) "being" ($#m1_subset_1 :::"Function":::) "of" (Set (Var "C")) "," (Set (Var "D")) (Bool "for" (Set (Var "r")) "being" ($#v1_xcmplx_0 :::"complex"::: ) ($#m1_hidden :::"number"::: ) (Bool "for" (Set (Var "c")) "being" ($#m1_subset_1 :::"Element"::: ) "of" (Set (Var "C")) "holds" (Bool (Set (Set "(" (Set (Var "f")) ($#k14_valued_1 :::"-"::: ) (Set (Var "r")) ")" ) ($#k3_funct_2 :::"."::: ) (Set (Var "c"))) ($#r1_hidden :::"="::: ) (Set (Set "(" (Set (Var "f")) ($#k3_funct_2 :::"."::: ) (Set (Var "c")) ")" ) ($#k6_xcmplx_0 :::"-"::: ) (Set (Var "r"))))))))) ; registrationlet "f" be ($#v1_valued_0 :::"complex-valued"::: ) ($#m1_hidden :::"FinSequence":::); let "r" be ($#v1_xcmplx_0 :::"complex"::: ) ($#m1_hidden :::"number"::: ) ; cluster (Set "f" ($#k13_valued_1 :::"-"::: ) "r") -> ($#v1_finseq_1 :::"FinSequence-like"::: ) ; end; begin definitionlet "f1", "f2" be ($#v1_valued_0 :::"complex-valued"::: ) ($#m1_hidden :::"Function":::); func "f1" :::"(#)"::: "f2" -> ($#m1_hidden :::"Function":::) means :: VALUED_1:def 4 (Bool "(" (Bool (Set ($#k9_xtuple_0 :::"dom"::: ) it) ($#r1_hidden :::"="::: ) (Set (Set "(" ($#k9_xtuple_0 :::"dom"::: ) "f1" ")" ) ($#k3_xboole_0 :::"/\"::: ) (Set "(" ($#k9_xtuple_0 :::"dom"::: ) "f2" ")" ))) & (Bool "(" "for" (Set (Var "c")) "being" ($#m1_hidden :::"set"::: ) "st" (Bool (Bool (Set (Var "c")) ($#r2_hidden :::"in"::: ) (Set ($#k9_xtuple_0 :::"dom"::: ) it))) "holds" (Bool (Set it ($#k1_funct_1 :::"."::: ) (Set (Var "c"))) ($#r1_hidden :::"="::: ) (Set (Set "(" "f1" ($#k1_funct_1 :::"."::: ) (Set (Var "c")) ")" ) ($#k3_xcmplx_0 :::"*"::: ) (Set "(" "f2" ($#k1_funct_1 :::"."::: ) (Set (Var "c")) ")" ))) ")" ) ")" ); commutativity (Bool "for" (Set (Var "b1")) "being" ($#m1_hidden :::"Function":::) (Bool "for" (Set (Var "f1")) "," (Set (Var "f2")) "being" ($#v1_valued_0 :::"complex-valued"::: ) ($#m1_hidden :::"Function":::) "st" (Bool (Bool (Set ($#k9_xtuple_0 :::"dom"::: ) (Set (Var "b1"))) ($#r1_hidden :::"="::: ) (Set (Set "(" ($#k9_xtuple_0 :::"dom"::: ) (Set (Var "f1")) ")" ) ($#k3_xboole_0 :::"/\"::: ) (Set "(" ($#k9_xtuple_0 :::"dom"::: ) (Set (Var "f2")) ")" ))) & (Bool "(" "for" (Set (Var "c")) "being" ($#m1_hidden :::"set"::: ) "st" (Bool (Bool (Set (Var "c")) ($#r2_hidden :::"in"::: ) (Set ($#k9_xtuple_0 :::"dom"::: ) (Set (Var "b1"))))) "holds" (Bool (Set (Set (Var "b1")) ($#k1_funct_1 :::"."::: ) (Set (Var "c"))) ($#r1_hidden :::"="::: ) (Set (Set "(" (Set (Var "f1")) ($#k1_funct_1 :::"."::: ) (Set (Var "c")) ")" ) ($#k3_xcmplx_0 :::"*"::: ) (Set "(" (Set (Var "f2")) ($#k1_funct_1 :::"."::: ) (Set (Var "c")) ")" ))) ")" )) "holds" (Bool "(" (Bool (Set ($#k9_xtuple_0 :::"dom"::: ) (Set (Var "b1"))) ($#r1_hidden :::"="::: ) (Set (Set "(" ($#k9_xtuple_0 :::"dom"::: ) (Set (Var "f2")) ")" ) ($#k3_xboole_0 :::"/\"::: ) (Set "(" ($#k9_xtuple_0 :::"dom"::: ) (Set (Var "f1")) ")" ))) & (Bool "(" "for" (Set (Var "c")) "being" ($#m1_hidden :::"set"::: ) "st" (Bool (Bool (Set (Var "c")) ($#r2_hidden :::"in"::: ) (Set ($#k9_xtuple_0 :::"dom"::: ) (Set (Var "b1"))))) "holds" (Bool (Set (Set (Var "b1")) ($#k1_funct_1 :::"."::: ) (Set (Var "c"))) ($#r1_hidden :::"="::: ) (Set (Set "(" (Set (Var "f2")) ($#k1_funct_1 :::"."::: ) (Set (Var "c")) ")" ) ($#k3_xcmplx_0 :::"*"::: ) (Set "(" (Set (Var "f1")) ($#k1_funct_1 :::"."::: ) (Set (Var "c")) ")" ))) ")" ) ")" ))) ; end; :: deftheorem defines :::"(#)"::: VALUED_1:def 4 : (Bool "for" (Set (Var "f1")) "," (Set (Var "f2")) "being" ($#v1_valued_0 :::"complex-valued"::: ) ($#m1_hidden :::"Function":::) (Bool "for" (Set (Var "b3")) "being" ($#m1_hidden :::"Function":::) "holds" (Bool "(" (Bool (Set (Var "b3")) ($#r1_hidden :::"="::: ) (Set (Set (Var "f1")) ($#k18_valued_1 :::"(#)"::: ) (Set (Var "f2")))) "iff" (Bool "(" (Bool (Set ($#k9_xtuple_0 :::"dom"::: ) (Set (Var "b3"))) ($#r1_hidden :::"="::: ) (Set (Set "(" ($#k9_xtuple_0 :::"dom"::: ) (Set (Var "f1")) ")" ) ($#k3_xboole_0 :::"/\"::: ) (Set "(" ($#k9_xtuple_0 :::"dom"::: ) (Set (Var "f2")) ")" ))) & (Bool "(" "for" (Set (Var "c")) "being" ($#m1_hidden :::"set"::: ) "st" (Bool (Bool (Set (Var "c")) ($#r2_hidden :::"in"::: ) (Set ($#k9_xtuple_0 :::"dom"::: ) (Set (Var "b3"))))) "holds" (Bool (Set (Set (Var "b3")) ($#k1_funct_1 :::"."::: ) (Set (Var "c"))) ($#r1_hidden :::"="::: ) (Set (Set "(" (Set (Var "f1")) ($#k1_funct_1 :::"."::: ) (Set (Var "c")) ")" ) ($#k3_xcmplx_0 :::"*"::: ) (Set "(" (Set (Var "f2")) ($#k1_funct_1 :::"."::: ) (Set (Var "c")) ")" ))) ")" ) ")" ) ")" ))); theorem :: VALUED_1:5 (Bool "for" (Set (Var "f1")) "," (Set (Var "f2")) "being" ($#v1_valued_0 :::"complex-valued"::: ) ($#m1_hidden :::"Function":::) (Bool "for" (Set (Var "c")) "being" ($#m1_hidden :::"set"::: ) "holds" (Bool (Set (Set "(" (Set (Var "f1")) ($#k18_valued_1 :::"(#)"::: ) (Set (Var "f2")) ")" ) ($#k1_funct_1 :::"."::: ) (Set (Var "c"))) ($#r1_hidden :::"="::: ) (Set (Set "(" (Set (Var "f1")) ($#k1_funct_1 :::"."::: ) (Set (Var "c")) ")" ) ($#k3_xcmplx_0 :::"*"::: ) (Set "(" (Set (Var "f2")) ($#k1_funct_1 :::"."::: ) (Set (Var "c")) ")" ))))) ; registrationlet "f1", "f2" be ($#v1_valued_0 :::"complex-valued"::: ) ($#m1_hidden :::"Function":::); cluster (Set "f1" ($#k18_valued_1 :::"(#)"::: ) "f2") -> ($#v1_valued_0 :::"complex-valued"::: ) ; end; registrationlet "f1", "f2" be ($#v3_valued_0 :::"real-valued"::: ) ($#m1_hidden :::"Function":::); cluster (Set "f1" ($#k18_valued_1 :::"(#)"::: ) "f2") -> ($#v3_valued_0 :::"real-valued"::: ) ; end; registrationlet "f1", "f2" be (Set ($#k3_numbers :::"RAT"::: ) ) ($#v5_relat_1 :::"-valued"::: ) ($#m1_hidden :::"Function":::); cluster (Set "f1" ($#k18_valued_1 :::"(#)"::: ) "f2") -> (Set ($#k3_numbers :::"RAT"::: ) ) ($#v5_relat_1 :::"-valued"::: ) ; end; registrationlet "f1", "f2" be (Set ($#k4_numbers :::"INT"::: ) ) ($#v5_relat_1 :::"-valued"::: ) ($#m1_hidden :::"Function":::); cluster (Set "f1" ($#k18_valued_1 :::"(#)"::: ) "f2") -> (Set ($#k4_numbers :::"INT"::: ) ) ($#v5_relat_1 :::"-valued"::: ) ; end; registrationlet "f1", "f2" be ($#v4_valued_0 :::"natural-valued"::: ) ($#m1_hidden :::"Function":::); cluster (Set "f1" ($#k18_valued_1 :::"(#)"::: ) "f2") -> ($#v4_valued_0 :::"natural-valued"::: ) ; end; definitionlet "C" be ($#m1_hidden :::"set"::: ) ; let "D1", "D2" be ($#v1_membered :::"complex-membered"::: ) ($#m1_hidden :::"set"::: ) ; let "f1" be ($#m1_subset_1 :::"PartFunc":::) "of" (Set (Const "C")) "," (Set (Const "D1")); let "f2" be ($#m1_subset_1 :::"PartFunc":::) "of" (Set (Const "C")) "," (Set (Const "D2")); :: original: :::"(#)"::: redefine func "f1" :::"(#)"::: "f2" -> ($#m1_subset_1 :::"PartFunc":::) "of" "C" "," (Set ($#k2_numbers :::"COMPLEX"::: ) ); end; definitionlet "C" be ($#m1_hidden :::"set"::: ) ; let "D1", "D2" be ($#v3_membered :::"real-membered"::: ) ($#m1_hidden :::"set"::: ) ; let "f1" be ($#m1_subset_1 :::"PartFunc":::) "of" (Set (Const "C")) "," (Set (Const "D1")); let "f2" be ($#m1_subset_1 :::"PartFunc":::) "of" (Set (Const "C")) "," (Set (Const "D2")); :: original: :::"(#)"::: redefine func "f1" :::"(#)"::: "f2" -> ($#m1_subset_1 :::"PartFunc":::) "of" "C" "," (Set ($#k1_numbers :::"REAL"::: ) ); end; definitionlet "C" be ($#m1_hidden :::"set"::: ) ; let "D1", "D2" be ($#v4_membered :::"rational-membered"::: ) ($#m1_hidden :::"set"::: ) ; let "f1" be ($#m1_subset_1 :::"PartFunc":::) "of" (Set (Const "C")) "," (Set (Const "D1")); let "f2" be ($#m1_subset_1 :::"PartFunc":::) "of" (Set (Const "C")) "," (Set (Const "D2")); :: original: :::"(#)"::: redefine func "f1" :::"(#)"::: "f2" -> ($#m1_subset_1 :::"PartFunc":::) "of" "C" "," (Set ($#k3_numbers :::"RAT"::: ) ); end; definitionlet "C" be ($#m1_hidden :::"set"::: ) ; let "D1", "D2" be ($#v5_membered :::"integer-membered"::: ) ($#m1_hidden :::"set"::: ) ; let "f1" be ($#m1_subset_1 :::"PartFunc":::) "of" (Set (Const "C")) "," (Set (Const "D1")); let "f2" be ($#m1_subset_1 :::"PartFunc":::) "of" (Set (Const "C")) "," (Set (Const "D2")); :: original: :::"(#)"::: redefine func "f1" :::"(#)"::: "f2" -> ($#m1_subset_1 :::"PartFunc":::) "of" "C" "," (Set ($#k4_numbers :::"INT"::: ) ); end; definitionlet "C" be ($#m1_hidden :::"set"::: ) ; let "D1", "D2" be ($#v6_membered :::"natural-membered"::: ) ($#m1_hidden :::"set"::: ) ; let "f1" be ($#m1_subset_1 :::"PartFunc":::) "of" (Set (Const "C")) "," (Set (Const "D1")); let "f2" be ($#m1_subset_1 :::"PartFunc":::) "of" (Set (Const "C")) "," (Set (Const "D2")); :: original: :::"(#)"::: redefine func "f1" :::"(#)"::: "f2" -> ($#m1_subset_1 :::"PartFunc":::) "of" "C" "," (Set ($#k5_numbers :::"NAT"::: ) ); end; registrationlet "C" be ($#m1_hidden :::"set"::: ) ; let "D1", "D2" be ($#~v1_xboole_0 "non" ($#v1_xboole_0 :::"empty"::: ) ) ($#v1_membered :::"complex-membered"::: ) ($#m1_hidden :::"set"::: ) ; let "f1" be ($#m1_subset_1 :::"Function":::) "of" (Set (Const "C")) "," (Set (Const "D1")); let "f2" be ($#m1_subset_1 :::"Function":::) "of" (Set (Const "C")) "," (Set (Const "D2")); cluster (Set "f1" ($#k18_valued_1 :::"(#)"::: ) "f2") -> ($#v1_partfun1 :::"total"::: ) for ($#m1_subset_1 :::"PartFunc":::) "of" "C" "," (Set ($#k2_numbers :::"COMPLEX"::: ) ); end; registrationlet "C" be ($#m1_hidden :::"set"::: ) ; let "D1", "D2" be ($#~v1_xboole_0 "non" ($#v1_xboole_0 :::"empty"::: ) ) ($#v3_membered :::"real-membered"::: ) ($#m1_hidden :::"set"::: ) ; let "f1" be ($#m1_subset_1 :::"Function":::) "of" (Set (Const "C")) "," (Set (Const "D1")); let "f2" be ($#m1_subset_1 :::"Function":::) "of" (Set (Const "C")) "," (Set (Const "D2")); cluster (Set "f1" ($#k18_valued_1 :::"(#)"::: ) "f2") -> ($#v1_partfun1 :::"total"::: ) for ($#m1_subset_1 :::"PartFunc":::) "of" "C" "," (Set ($#k1_numbers :::"REAL"::: ) ); end; registrationlet "C" be ($#m1_hidden :::"set"::: ) ; let "D1", "D2" be ($#~v1_xboole_0 "non" ($#v1_xboole_0 :::"empty"::: ) ) ($#v4_membered :::"rational-membered"::: ) ($#m1_hidden :::"set"::: ) ; let "f1" be ($#m1_subset_1 :::"Function":::) "of" (Set (Const "C")) "," (Set (Const "D1")); let "f2" be ($#m1_subset_1 :::"Function":::) "of" (Set (Const "C")) "," (Set (Const "D2")); cluster (Set "f1" ($#k18_valued_1 :::"(#)"::: ) "f2") -> ($#v1_partfun1 :::"total"::: ) for ($#m1_subset_1 :::"PartFunc":::) "of" "C" "," (Set ($#k3_numbers :::"RAT"::: ) ); end; registrationlet "C" be ($#m1_hidden :::"set"::: ) ; let "D1", "D2" be ($#~v1_xboole_0 "non" ($#v1_xboole_0 :::"empty"::: ) ) ($#v5_membered :::"integer-membered"::: ) ($#m1_hidden :::"set"::: ) ; let "f1" be ($#m1_subset_1 :::"Function":::) "of" (Set (Const "C")) "," (Set (Const "D1")); let "f2" be ($#m1_subset_1 :::"Function":::) "of" (Set (Const "C")) "," (Set (Const "D2")); cluster (Set "f1" ($#k18_valued_1 :::"(#)"::: ) "f2") -> ($#v1_partfun1 :::"total"::: ) for ($#m1_subset_1 :::"PartFunc":::) "of" "C" "," (Set ($#k4_numbers :::"INT"::: ) ); end; registrationlet "C" be ($#m1_hidden :::"set"::: ) ; let "D1", "D2" be ($#~v1_xboole_0 "non" ($#v1_xboole_0 :::"empty"::: ) ) ($#v6_membered :::"natural-membered"::: ) ($#m1_hidden :::"set"::: ) ; let "f1" be ($#m1_subset_1 :::"Function":::) "of" (Set (Const "C")) "," (Set (Const "D1")); let "f2" be ($#m1_subset_1 :::"Function":::) "of" (Set (Const "C")) "," (Set (Const "D2")); cluster (Set "f1" ($#k18_valued_1 :::"(#)"::: ) "f2") -> ($#v1_partfun1 :::"total"::: ) for ($#m1_subset_1 :::"PartFunc":::) "of" "C" "," (Set ($#k5_numbers :::"NAT"::: ) ); end; registrationlet "f1", "f2" be ($#v1_valued_0 :::"complex-valued"::: ) ($#m1_hidden :::"FinSequence":::); cluster (Set "f1" ($#k18_valued_1 :::"(#)"::: ) "f2") -> ($#v1_finseq_1 :::"FinSequence-like"::: ) ; end; begin definitionlet "f" be ($#v1_valued_0 :::"complex-valued"::: ) ($#m1_hidden :::"Function":::); let "r" be ($#v1_xcmplx_0 :::"complex"::: ) ($#m1_hidden :::"number"::: ) ; func "r" :::"(#)"::: "f" -> ($#m1_hidden :::"Function":::) means :: VALUED_1:def 5 (Bool "(" (Bool (Set ($#k9_xtuple_0 :::"dom"::: ) it) ($#r1_hidden :::"="::: ) (Set ($#k9_xtuple_0 :::"dom"::: ) "f")) & (Bool "(" "for" (Set (Var "c")) "being" ($#m1_hidden :::"set"::: ) "st" (Bool (Bool (Set (Var "c")) ($#r2_hidden :::"in"::: ) (Set ($#k9_xtuple_0 :::"dom"::: ) it))) "holds" (Bool (Set it ($#k1_funct_1 :::"."::: ) (Set (Var "c"))) ($#r1_hidden :::"="::: ) (Set "r" ($#k3_xcmplx_0 :::"*"::: ) (Set "(" "f" ($#k1_funct_1 :::"."::: ) (Set (Var "c")) ")" ))) ")" ) ")" ); end; :: deftheorem defines :::"(#)"::: VALUED_1:def 5 : (Bool "for" (Set (Var "f")) "being" ($#v1_valued_0 :::"complex-valued"::: ) ($#m1_hidden :::"Function":::) (Bool "for" (Set (Var "r")) "being" ($#v1_xcmplx_0 :::"complex"::: ) ($#m1_hidden :::"number"::: ) (Bool "for" (Set (Var "b3")) "being" ($#m1_hidden :::"Function":::) "holds" (Bool "(" (Bool (Set (Var "b3")) ($#r1_hidden :::"="::: ) (Set (Set (Var "r")) ($#k24_valued_1 :::"(#)"::: ) (Set (Var "f")))) "iff" (Bool "(" (Bool (Set ($#k9_xtuple_0 :::"dom"::: ) (Set (Var "b3"))) ($#r1_hidden :::"="::: ) (Set ($#k9_xtuple_0 :::"dom"::: ) (Set (Var "f")))) & (Bool "(" "for" (Set (Var "c")) "being" ($#m1_hidden :::"set"::: ) "st" (Bool (Bool (Set (Var "c")) ($#r2_hidden :::"in"::: ) (Set ($#k9_xtuple_0 :::"dom"::: ) (Set (Var "b3"))))) "holds" (Bool (Set (Set (Var "b3")) ($#k1_funct_1 :::"."::: ) (Set (Var "c"))) ($#r1_hidden :::"="::: ) (Set (Set (Var "r")) ($#k3_xcmplx_0 :::"*"::: ) (Set "(" (Set (Var "f")) ($#k1_funct_1 :::"."::: ) (Set (Var "c")) ")" ))) ")" ) ")" ) ")" )))); notationlet "f" be ($#v1_valued_0 :::"complex-valued"::: ) ($#m1_hidden :::"Function":::); let "r" be ($#v1_xcmplx_0 :::"complex"::: ) ($#m1_hidden :::"number"::: ) ; synonym "f" :::"(#)"::: "r" for "r" :::"(#)"::: "f"; end; theorem :: VALUED_1:6 (Bool "for" (Set (Var "f")) "being" ($#v1_valued_0 :::"complex-valued"::: ) ($#m1_hidden :::"Function":::) (Bool "for" (Set (Var "r")) "being" ($#v1_xcmplx_0 :::"complex"::: ) ($#m1_hidden :::"number"::: ) (Bool "for" (Set (Var "c")) "being" ($#m1_hidden :::"set"::: ) "holds" (Bool (Set (Set "(" (Set (Var "r")) ($#k24_valued_1 :::"(#)"::: ) (Set (Var "f")) ")" ) ($#k1_funct_1 :::"."::: ) (Set (Var "c"))) ($#r1_hidden :::"="::: ) (Set (Set (Var "r")) ($#k3_xcmplx_0 :::"*"::: ) (Set "(" (Set (Var "f")) ($#k1_funct_1 :::"."::: ) (Set (Var "c")) ")" )))))) ; registrationlet "f" be ($#v1_valued_0 :::"complex-valued"::: ) ($#m1_hidden :::"Function":::); let "r" be ($#v1_xcmplx_0 :::"complex"::: ) ($#m1_hidden :::"number"::: ) ; cluster (Set "r" ($#k24_valued_1 :::"(#)"::: ) "f") -> ($#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 "r" ($#k24_valued_1 :::"(#)"::: ) "f") -> ($#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 "r" ($#k24_valued_1 :::"(#)"::: ) "f") -> (Set ($#k3_numbers :::"RAT"::: ) ) ($#v5_relat_1 :::"-valued"::: ) ; end; registrationlet "f" be (Set ($#k4_numbers :::"INT"::: ) ) ($#v5_relat_1 :::"-valued"::: ) ($#m1_hidden :::"Function":::); let "r" be ($#v1_int_1 :::"integer"::: ) ($#m1_hidden :::"number"::: ) ; cluster (Set "r" ($#k24_valued_1 :::"(#)"::: ) "f") -> (Set ($#k4_numbers :::"INT"::: ) ) ($#v5_relat_1 :::"-valued"::: ) ; end; registrationlet "f" be ($#v4_valued_0 :::"natural-valued"::: ) ($#m1_hidden :::"Function":::); let "r" be ($#m1_hidden :::"Nat":::); cluster (Set "r" ($#k24_valued_1 :::"(#)"::: ) "f") -> ($#v4_valued_0 :::"natural-valued"::: ) ; end; definitionlet "C" be ($#m1_hidden :::"set"::: ) ; let "D" be ($#v1_membered :::"complex-membered"::: ) ($#m1_hidden :::"set"::: ) ; let "f" be ($#m1_subset_1 :::"PartFunc":::) "of" (Set (Const "C")) "," (Set (Const "D")); let "r" be ($#v1_xcmplx_0 :::"complex"::: ) ($#m1_hidden :::"number"::: ) ; :: original: :::"(#)"::: redefine func "r" :::"(#)"::: "f" -> ($#m1_subset_1 :::"PartFunc":::) "of" "C" "," (Set ($#k2_numbers :::"COMPLEX"::: ) ); end; definitionlet "C" be ($#m1_hidden :::"set"::: ) ; let "D" be ($#v3_membered :::"real-membered"::: ) ($#m1_hidden :::"set"::: ) ; let "f" be ($#m1_subset_1 :::"PartFunc":::) "of" (Set (Const "C")) "," (Set (Const "D")); let "r" be ($#v1_xreal_0 :::"real"::: ) ($#m1_hidden :::"number"::: ) ; :: original: :::"(#)"::: redefine func "r" :::"(#)"::: "f" -> ($#m1_subset_1 :::"PartFunc":::) "of" "C" "," (Set ($#k1_numbers :::"REAL"::: ) ); end; definitionlet "C" be ($#m1_hidden :::"set"::: ) ; let "D" be ($#v4_membered :::"rational-membered"::: ) ($#m1_hidden :::"set"::: ) ; let "f" be ($#m1_subset_1 :::"PartFunc":::) "of" (Set (Const "C")) "," (Set (Const "D")); let "r" be ($#v1_rat_1 :::"rational"::: ) ($#m1_hidden :::"number"::: ) ; :: original: :::"(#)"::: redefine func "r" :::"(#)"::: "f" -> ($#m1_subset_1 :::"PartFunc":::) "of" "C" "," (Set ($#k3_numbers :::"RAT"::: ) ); end; definitionlet "C" be ($#m1_hidden :::"set"::: ) ; let "D" be ($#v5_membered :::"integer-membered"::: ) ($#m1_hidden :::"set"::: ) ; let "f" be ($#m1_subset_1 :::"PartFunc":::) "of" (Set (Const "C")) "," (Set (Const "D")); let "r" be ($#v1_int_1 :::"integer"::: ) ($#m1_hidden :::"number"::: ) ; :: original: :::"(#)"::: redefine func "r" :::"(#)"::: "f" -> ($#m1_subset_1 :::"PartFunc":::) "of" "C" "," (Set ($#k4_numbers :::"INT"::: ) ); end; definitionlet "C" be ($#m1_hidden :::"set"::: ) ; let "D" be ($#v6_membered :::"natural-membered"::: ) ($#m1_hidden :::"set"::: ) ; let "f" be ($#m1_subset_1 :::"PartFunc":::) "of" (Set (Const "C")) "," (Set (Const "D")); let "r" be ($#m1_hidden :::"Nat":::); :: original: :::"(#)"::: redefine func "r" :::"(#)"::: "f" -> ($#m1_subset_1 :::"PartFunc":::) "of" "C" "," (Set ($#k5_numbers :::"NAT"::: ) ); end; registrationlet "C" be ($#m1_hidden :::"set"::: ) ; let "D" be ($#~v1_xboole_0 "non" ($#v1_xboole_0 :::"empty"::: ) ) ($#v1_membered :::"complex-membered"::: ) ($#m1_hidden :::"set"::: ) ; let "f" be ($#m1_subset_1 :::"Function":::) "of" (Set (Const "C")) "," (Set (Const "D")); let "r" be ($#v1_xcmplx_0 :::"complex"::: ) ($#m1_hidden :::"number"::: ) ; cluster (Set "r" ($#k24_valued_1 :::"(#)"::: ) "f") -> ($#v1_partfun1 :::"total"::: ) for ($#m1_subset_1 :::"PartFunc":::) "of" "C" "," (Set ($#k2_numbers :::"COMPLEX"::: ) ); end; registrationlet "C" be ($#m1_hidden :::"set"::: ) ; let "D" be ($#~v1_xboole_0 "non" ($#v1_xboole_0 :::"empty"::: ) ) ($#v3_membered :::"real-membered"::: ) ($#m1_hidden :::"set"::: ) ; let "f" be ($#m1_subset_1 :::"Function":::) "of" (Set (Const "C")) "," (Set (Const "D")); let "r" be ($#v1_xreal_0 :::"real"::: ) ($#m1_hidden :::"number"::: ) ; cluster (Set "r" ($#k24_valued_1 :::"(#)"::: ) "f") -> ($#v1_partfun1 :::"total"::: ) for ($#m1_subset_1 :::"PartFunc":::) "of" "C" "," (Set ($#k1_numbers :::"REAL"::: ) ); end; registrationlet "C" be ($#m1_hidden :::"set"::: ) ; let "D" be ($#~v1_xboole_0 "non" ($#v1_xboole_0 :::"empty"::: ) ) ($#v4_membered :::"rational-membered"::: ) ($#m1_hidden :::"set"::: ) ; let "f" be ($#m1_subset_1 :::"Function":::) "of" (Set (Const "C")) "," (Set (Const "D")); let "r" be ($#v1_rat_1 :::"rational"::: ) ($#m1_hidden :::"number"::: ) ; cluster (Set "r" ($#k24_valued_1 :::"(#)"::: ) "f") -> ($#v1_partfun1 :::"total"::: ) for ($#m1_subset_1 :::"PartFunc":::) "of" "C" "," (Set ($#k3_numbers :::"RAT"::: ) ); end; registrationlet "C" be ($#m1_hidden :::"set"::: ) ; let "D" be ($#~v1_xboole_0 "non" ($#v1_xboole_0 :::"empty"::: ) ) ($#v5_membered :::"integer-membered"::: ) ($#m1_hidden :::"set"::: ) ; let "f" be ($#m1_subset_1 :::"Function":::) "of" (Set (Const "C")) "," (Set (Const "D")); let "r" be ($#v1_int_1 :::"integer"::: ) ($#m1_hidden :::"number"::: ) ; cluster (Set "r" ($#k24_valued_1 :::"(#)"::: ) "f") -> ($#v1_partfun1 :::"total"::: ) for ($#m1_subset_1 :::"PartFunc":::) "of" "C" "," (Set ($#k4_numbers :::"INT"::: ) ); end; registrationlet "C" be ($#m1_hidden :::"set"::: ) ; let "D" be ($#~v1_xboole_0 "non" ($#v1_xboole_0 :::"empty"::: ) ) ($#v6_membered :::"natural-membered"::: ) ($#m1_hidden :::"set"::: ) ; let "f" be ($#m1_subset_1 :::"Function":::) "of" (Set (Const "C")) "," (Set (Const "D")); let "r" be ($#m1_hidden :::"Nat":::); cluster (Set "r" ($#k24_valued_1 :::"(#)"::: ) "f") -> ($#v1_partfun1 :::"total"::: ) for ($#m1_subset_1 :::"PartFunc":::) "of" "C" "," (Set ($#k5_numbers :::"NAT"::: ) ); end; theorem :: VALUED_1:7 (Bool "for" (Set (Var "C")) "being" ($#~v1_xboole_0 "non" ($#v1_xboole_0 :::"empty"::: ) ) ($#m1_hidden :::"set"::: ) (Bool "for" (Set (Var "D")) "being" ($#~v1_xboole_0 "non" ($#v1_xboole_0 :::"empty"::: ) ) ($#v1_membered :::"complex-membered"::: ) ($#m1_hidden :::"set"::: ) (Bool "for" (Set (Var "f")) "being" ($#m1_subset_1 :::"Function":::) "of" (Set (Var "C")) "," (Set (Var "D")) (Bool "for" (Set (Var "r")) "being" ($#v1_xcmplx_0 :::"complex"::: ) ($#m1_hidden :::"number"::: ) (Bool "for" (Set (Var "g")) "being" ($#m1_subset_1 :::"Function":::) "of" (Set (Var "C")) "," (Set ($#k2_numbers :::"COMPLEX"::: ) ) "st" (Bool (Bool "(" "for" (Set (Var "c")) "being" ($#m1_subset_1 :::"Element"::: ) "of" (Set (Var "C")) "holds" (Bool (Set (Set (Var "g")) ($#k3_funct_2 :::"."::: ) (Set (Var "c"))) ($#r1_hidden :::"="::: ) (Set (Set (Var "r")) ($#k3_xcmplx_0 :::"*"::: ) (Set "(" (Set (Var "f")) ($#k3_funct_2 :::"."::: ) (Set (Var "c")) ")" ))) ")" )) "holds" (Bool (Set (Var "g")) ($#r2_funct_2 :::"="::: ) (Set (Set (Var "r")) ($#k25_valued_1 :::"(#)"::: ) (Set (Var "f"))))))))) ; registrationlet "f" be ($#v1_valued_0 :::"complex-valued"::: ) ($#m1_hidden :::"FinSequence":::); let "r" be ($#v1_xcmplx_0 :::"complex"::: ) ($#m1_hidden :::"number"::: ) ; cluster (Set "r" ($#k24_valued_1 :::"(#)"::: ) "f") -> ($#v1_finseq_1 :::"FinSequence-like"::: ) ; end; begin definitionlet "f" be ($#v1_valued_0 :::"complex-valued"::: ) ($#m1_hidden :::"Function":::); func :::"-"::: "f" -> ($#v1_valued_0 :::"complex-valued"::: ) ($#m1_hidden :::"Function":::) equals :: VALUED_1:def 6 (Set (Set "(" ($#k4_xcmplx_0 :::"-"::: ) (Num 1) ")" ) ($#k24_valued_1 :::"(#)"::: ) "f"); involutiveness (Bool "for" (Set (Var "b1")) "," (Set (Var "b2")) "being" ($#v1_valued_0 :::"complex-valued"::: ) ($#m1_hidden :::"Function":::) "st" (Bool (Bool (Set (Var "b1")) ($#r1_hidden :::"="::: ) (Set (Set "(" ($#k4_xcmplx_0 :::"-"::: ) (Num 1) ")" ) ($#k24_valued_1 :::"(#)"::: ) (Set (Var "b2"))))) "holds" (Bool (Set (Var "b2")) ($#r1_hidden :::"="::: ) (Set (Set "(" ($#k4_xcmplx_0 :::"-"::: ) (Num 1) ")" ) ($#k24_valued_1 :::"(#)"::: ) (Set (Var "b1"))))) ; end; :: deftheorem defines :::"-"::: VALUED_1:def 6 : (Bool "for" (Set (Var "f")) "being" ($#v1_valued_0 :::"complex-valued"::: ) ($#m1_hidden :::"Function":::) "holds" (Bool (Set ($#k30_valued_1 :::"-"::: ) (Set (Var "f"))) ($#r1_hidden :::"="::: ) (Set (Set "(" ($#k4_xcmplx_0 :::"-"::: ) (Num 1) ")" ) ($#k24_valued_1 :::"(#)"::: ) (Set (Var "f"))))); theorem :: VALUED_1:8 (Bool "for" (Set (Var "f")) "being" ($#v1_valued_0 :::"complex-valued"::: ) ($#m1_hidden :::"Function":::) "holds" (Bool "(" (Bool (Set ($#k9_xtuple_0 :::"dom"::: ) (Set "(" ($#k30_valued_1 :::"-"::: ) (Set (Var "f")) ")" )) ($#r1_hidden :::"="::: ) (Set ($#k9_xtuple_0 :::"dom"::: ) (Set (Var "f")))) & (Bool "(" "for" (Set (Var "c")) "being" ($#m1_hidden :::"set"::: ) "holds" (Bool (Set (Set "(" ($#k30_valued_1 :::"-"::: ) (Set (Var "f")) ")" ) ($#k1_funct_1 :::"."::: ) (Set (Var "c"))) ($#r1_hidden :::"="::: ) (Set ($#k4_xcmplx_0 :::"-"::: ) (Set "(" (Set (Var "f")) ($#k1_funct_1 :::"."::: ) (Set (Var "c")) ")" ))) ")" ) ")" )) ; theorem :: VALUED_1:9 (Bool "for" (Set (Var "f")) "being" ($#v1_valued_0 :::"complex-valued"::: ) ($#m1_hidden :::"Function":::) (Bool "for" (Set (Var "g")) "being" ($#m1_hidden :::"Function":::) "st" (Bool (Bool (Set ($#k9_xtuple_0 :::"dom"::: ) (Set (Var "f"))) ($#r1_hidden :::"="::: ) (Set ($#k9_xtuple_0 :::"dom"::: ) (Set (Var "g")))) & (Bool "(" "for" (Set (Var "c")) "being" ($#m1_hidden :::"set"::: ) "st" (Bool (Bool (Set (Var "c")) ($#r2_hidden :::"in"::: ) (Set ($#k9_xtuple_0 :::"dom"::: ) (Set (Var "f"))))) "holds" (Bool (Set (Set (Var "g")) ($#k1_funct_1 :::"."::: ) (Set (Var "c"))) ($#r1_hidden :::"="::: ) (Set ($#k4_xcmplx_0 :::"-"::: ) (Set "(" (Set (Var "f")) ($#k1_funct_1 :::"."::: ) (Set (Var "c")) ")" ))) ")" )) "holds" (Bool (Set (Var "g")) ($#r1_hidden :::"="::: ) (Set ($#k30_valued_1 :::"-"::: ) (Set (Var "f")))))) ; registrationlet "f" be ($#v1_valued_0 :::"complex-valued"::: ) ($#m1_hidden :::"Function":::); cluster (Set ($#k30_valued_1 :::"-"::: ) "f") -> ($#v1_valued_0 :::"complex-valued"::: ) ; end; registrationlet "f" be ($#v3_valued_0 :::"real-valued"::: ) ($#m1_hidden :::"Function":::); cluster (Set ($#k30_valued_1 :::"-"::: ) "f") -> ($#v1_valued_0 :::"complex-valued"::: ) ($#v3_valued_0 :::"real-valued"::: ) ; end; registrationlet "f" be (Set ($#k3_numbers :::"RAT"::: ) ) ($#v5_relat_1 :::"-valued"::: ) ($#m1_hidden :::"Function":::); cluster (Set ($#k30_valued_1 :::"-"::: ) "f") -> (Set ($#k3_numbers :::"RAT"::: ) ) ($#v5_relat_1 :::"-valued"::: ) ($#v1_valued_0 :::"complex-valued"::: ) ; end; registrationlet "f" be (Set ($#k4_numbers :::"INT"::: ) ) ($#v5_relat_1 :::"-valued"::: ) ($#m1_hidden :::"Function":::); cluster (Set ($#k30_valued_1 :::"-"::: ) "f") -> (Set ($#k4_numbers :::"INT"::: ) ) ($#v5_relat_1 :::"-valued"::: ) ($#v1_valued_0 :::"complex-valued"::: ) ; end; definitionlet "C" be ($#m1_hidden :::"set"::: ) ; let "D" be ($#v1_membered :::"complex-membered"::: ) ($#m1_hidden :::"set"::: ) ; let "f" be ($#m1_subset_1 :::"PartFunc":::) "of" (Set (Const "C")) "," (Set (Const "D")); :: original: :::"-"::: redefine func :::"-"::: "f" -> ($#m1_subset_1 :::"PartFunc":::) "of" "C" "," (Set ($#k2_numbers :::"COMPLEX"::: ) ); end; definitionlet "C" be ($#m1_hidden :::"set"::: ) ; let "D" be ($#v3_membered :::"real-membered"::: ) ($#m1_hidden :::"set"::: ) ; let "f" be ($#m1_subset_1 :::"PartFunc":::) "of" (Set (Const "C")) "," (Set (Const "D")); :: original: :::"-"::: redefine func :::"-"::: "f" -> ($#m1_subset_1 :::"PartFunc":::) "of" "C" "," (Set ($#k1_numbers :::"REAL"::: ) ); end; definitionlet "C" be ($#m1_hidden :::"set"::: ) ; let "D" be ($#v4_membered :::"rational-membered"::: ) ($#m1_hidden :::"set"::: ) ; let "f" be ($#m1_subset_1 :::"PartFunc":::) "of" (Set (Const "C")) "," (Set (Const "D")); :: original: :::"-"::: redefine func :::"-"::: "f" -> ($#m1_subset_1 :::"PartFunc":::) "of" "C" "," (Set ($#k3_numbers :::"RAT"::: ) ); end; definitionlet "C" be ($#m1_hidden :::"set"::: ) ; let "D" be ($#v5_membered :::"integer-membered"::: ) ($#m1_hidden :::"set"::: ) ; let "f" be ($#m1_subset_1 :::"PartFunc":::) "of" (Set (Const "C")) "," (Set (Const "D")); :: original: :::"-"::: redefine func :::"-"::: "f" -> ($#m1_subset_1 :::"PartFunc":::) "of" "C" "," (Set ($#k4_numbers :::"INT"::: ) ); end; registrationlet "C" be ($#m1_hidden :::"set"::: ) ; let "D" be ($#~v1_xboole_0 "non" ($#v1_xboole_0 :::"empty"::: ) ) ($#v1_membered :::"complex-membered"::: ) ($#m1_hidden :::"set"::: ) ; let "f" be ($#m1_subset_1 :::"Function":::) "of" (Set (Const "C")) "," (Set (Const "D")); cluster (Set ($#k30_valued_1 :::"-"::: ) "f") -> ($#v1_partfun1 :::"total"::: ) for ($#m1_subset_1 :::"PartFunc":::) "of" "C" "," (Set ($#k2_numbers :::"COMPLEX"::: ) ); end; registrationlet "C" be ($#m1_hidden :::"set"::: ) ; let "D" be ($#~v1_xboole_0 "non" ($#v1_xboole_0 :::"empty"::: ) ) ($#v3_membered :::"real-membered"::: ) ($#m1_hidden :::"set"::: ) ; let "f" be ($#m1_subset_1 :::"Function":::) "of" (Set (Const "C")) "," (Set (Const "D")); cluster (Set ($#k30_valued_1 :::"-"::: ) "f") -> ($#v1_partfun1 :::"total"::: ) for ($#m1_subset_1 :::"PartFunc":::) "of" "C" "," (Set ($#k1_numbers :::"REAL"::: ) ); end; registrationlet "C" be ($#m1_hidden :::"set"::: ) ; let "D" be ($#~v1_xboole_0 "non" ($#v1_xboole_0 :::"empty"::: ) ) ($#v4_membered :::"rational-membered"::: ) ($#m1_hidden :::"set"::: ) ; let "f" be ($#m1_subset_1 :::"Function":::) "of" (Set (Const "C")) "," (Set (Const "D")); cluster (Set ($#k30_valued_1 :::"-"::: ) "f") -> ($#v1_partfun1 :::"total"::: ) for ($#m1_subset_1 :::"PartFunc":::) "of" "C" "," (Set ($#k3_numbers :::"RAT"::: ) ); end; registrationlet "C" be ($#m1_hidden :::"set"::: ) ; let "D" be ($#~v1_xboole_0 "non" ($#v1_xboole_0 :::"empty"::: ) ) ($#v5_membered :::"integer-membered"::: ) ($#m1_hidden :::"set"::: ) ; let "f" be ($#m1_subset_1 :::"Function":::) "of" (Set (Const "C")) "," (Set (Const "D")); cluster (Set ($#k30_valued_1 :::"-"::: ) "f") -> ($#v1_partfun1 :::"total"::: ) for ($#m1_subset_1 :::"PartFunc":::) "of" "C" "," (Set ($#k4_numbers :::"INT"::: ) ); end; registrationlet "f" be ($#v1_valued_0 :::"complex-valued"::: ) ($#m1_hidden :::"FinSequence":::); cluster (Set ($#k30_valued_1 :::"-"::: ) "f") -> ($#v1_valued_0 :::"complex-valued"::: ) ($#v1_finseq_1 :::"FinSequence-like"::: ) ; end; begin definitionlet "f" be ($#v1_valued_0 :::"complex-valued"::: ) ($#m1_hidden :::"Function":::); func "f" :::"""::: -> ($#v1_valued_0 :::"complex-valued"::: ) ($#m1_hidden :::"Function":::) means :: VALUED_1:def 7 (Bool "(" (Bool (Set ($#k9_xtuple_0 :::"dom"::: ) it) ($#r1_hidden :::"="::: ) (Set ($#k9_xtuple_0 :::"dom"::: ) "f")) & (Bool "(" "for" (Set (Var "c")) "being" ($#m1_hidden :::"set"::: ) "st" (Bool (Bool (Set (Var "c")) ($#r2_hidden :::"in"::: ) (Set ($#k9_xtuple_0 :::"dom"::: ) it))) "holds" (Bool (Set it ($#k1_funct_1 :::"."::: ) (Set (Var "c"))) ($#r1_hidden :::"="::: ) (Set (Set "(" "f" ($#k1_funct_1 :::"."::: ) (Set (Var "c")) ")" ) ($#k5_xcmplx_0 :::"""::: ) )) ")" ) ")" ); involutiveness (Bool "for" (Set (Var "b1")) "," (Set (Var "b2")) "being" ($#v1_valued_0 :::"complex-valued"::: ) ($#m1_hidden :::"Function":::) "st" (Bool (Bool (Set ($#k9_xtuple_0 :::"dom"::: ) (Set (Var "b1"))) ($#r1_hidden :::"="::: ) (Set ($#k9_xtuple_0 :::"dom"::: ) (Set (Var "b2")))) & (Bool "(" "for" (Set (Var "c")) "being" ($#m1_hidden :::"set"::: ) "st" (Bool (Bool (Set (Var "c")) ($#r2_hidden :::"in"::: ) (Set ($#k9_xtuple_0 :::"dom"::: ) (Set (Var "b1"))))) "holds" (Bool (Set (Set (Var "b1")) ($#k1_funct_1 :::"."::: ) (Set (Var "c"))) ($#r1_hidden :::"="::: ) (Set (Set "(" (Set (Var "b2")) ($#k1_funct_1 :::"."::: ) (Set (Var "c")) ")" ) ($#k5_xcmplx_0 :::"""::: ) )) ")" )) "holds" (Bool "(" (Bool (Set ($#k9_xtuple_0 :::"dom"::: ) (Set (Var "b2"))) ($#r1_hidden :::"="::: ) (Set ($#k9_xtuple_0 :::"dom"::: ) (Set (Var "b1")))) & (Bool "(" "for" (Set (Var "c")) "being" ($#m1_hidden :::"set"::: ) "st" (Bool (Bool (Set (Var "c")) ($#r2_hidden :::"in"::: ) (Set ($#k9_xtuple_0 :::"dom"::: ) (Set (Var "b2"))))) "holds" (Bool (Set (Set (Var "b2")) ($#k1_funct_1 :::"."::: ) (Set (Var "c"))) ($#r1_hidden :::"="::: ) (Set (Set "(" (Set (Var "b1")) ($#k1_funct_1 :::"."::: ) (Set (Var "c")) ")" ) ($#k5_xcmplx_0 :::"""::: ) )) ")" ) ")" )) ; end; :: deftheorem defines :::"""::: VALUED_1:def 7 : (Bool "for" (Set (Var "f")) "," (Set (Var "b2")) "being" ($#v1_valued_0 :::"complex-valued"::: ) ($#m1_hidden :::"Function":::) "holds" (Bool "(" (Bool (Set (Var "b2")) ($#r1_hidden :::"="::: ) (Set (Set (Var "f")) ($#k35_valued_1 :::"""::: ) )) "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 "c")) "being" ($#m1_hidden :::"set"::: ) "st" (Bool (Bool (Set (Var "c")) ($#r2_hidden :::"in"::: ) (Set ($#k9_xtuple_0 :::"dom"::: ) (Set (Var "b2"))))) "holds" (Bool (Set (Set (Var "b2")) ($#k1_funct_1 :::"."::: ) (Set (Var "c"))) ($#r1_hidden :::"="::: ) (Set (Set "(" (Set (Var "f")) ($#k1_funct_1 :::"."::: ) (Set (Var "c")) ")" ) ($#k5_xcmplx_0 :::"""::: ) )) ")" ) ")" ) ")" )); theorem :: VALUED_1:10 (Bool "for" (Set (Var "f")) "being" ($#v1_valued_0 :::"complex-valued"::: ) ($#m1_hidden :::"Function":::) (Bool "for" (Set (Var "c")) "being" ($#m1_hidden :::"set"::: ) "holds" (Bool (Set (Set "(" (Set (Var "f")) ($#k35_valued_1 :::"""::: ) ")" ) ($#k1_funct_1 :::"."::: ) (Set (Var "c"))) ($#r1_hidden :::"="::: ) (Set (Set "(" (Set (Var "f")) ($#k1_funct_1 :::"."::: ) (Set (Var "c")) ")" ) ($#k5_xcmplx_0 :::"""::: ) )))) ; registrationlet "f" be ($#v3_valued_0 :::"real-valued"::: ) ($#m1_hidden :::"Function":::); cluster (Set "f" ($#k35_valued_1 :::"""::: ) ) -> ($#v1_valued_0 :::"complex-valued"::: ) ($#v3_valued_0 :::"real-valued"::: ) ; end; registrationlet "f" be (Set ($#k3_numbers :::"RAT"::: ) ) ($#v5_relat_1 :::"-valued"::: ) ($#m1_hidden :::"Function":::); cluster (Set "f" ($#k35_valued_1 :::"""::: ) ) -> (Set ($#k3_numbers :::"RAT"::: ) ) ($#v5_relat_1 :::"-valued"::: ) ($#v1_valued_0 :::"complex-valued"::: ) ; end; definitionlet "C" be ($#m1_hidden :::"set"::: ) ; let "D" be ($#v1_membered :::"complex-membered"::: ) ($#m1_hidden :::"set"::: ) ; let "f" be ($#m1_subset_1 :::"PartFunc":::) "of" (Set (Const "C")) "," (Set (Const "D")); :: original: :::"""::: redefine func "f" :::"""::: -> ($#m1_subset_1 :::"PartFunc":::) "of" "C" "," (Set ($#k2_numbers :::"COMPLEX"::: ) ); end; definitionlet "C" be ($#m1_hidden :::"set"::: ) ; let "D" be ($#v3_membered :::"real-membered"::: ) ($#m1_hidden :::"set"::: ) ; let "f" be ($#m1_subset_1 :::"PartFunc":::) "of" (Set (Const "C")) "," (Set (Const "D")); :: original: :::"""::: redefine func "f" :::"""::: -> ($#m1_subset_1 :::"PartFunc":::) "of" "C" "," (Set ($#k1_numbers :::"REAL"::: ) ); end; definitionlet "C" be ($#m1_hidden :::"set"::: ) ; let "D" be ($#v4_membered :::"rational-membered"::: ) ($#m1_hidden :::"set"::: ) ; let "f" be ($#m1_subset_1 :::"PartFunc":::) "of" (Set (Const "C")) "," (Set (Const "D")); :: original: :::"""::: redefine func "f" :::"""::: -> ($#m1_subset_1 :::"PartFunc":::) "of" "C" "," (Set ($#k3_numbers :::"RAT"::: ) ); end; registrationlet "C" be ($#m1_hidden :::"set"::: ) ; let "D" be ($#~v1_xboole_0 "non" ($#v1_xboole_0 :::"empty"::: ) ) ($#v1_membered :::"complex-membered"::: ) ($#m1_hidden :::"set"::: ) ; let "f" be ($#m1_subset_1 :::"Function":::) "of" (Set (Const "C")) "," (Set (Const "D")); cluster (Set "f" ($#k35_valued_1 :::"""::: ) ) -> ($#v1_partfun1 :::"total"::: ) for ($#m1_subset_1 :::"PartFunc":::) "of" "C" "," (Set ($#k2_numbers :::"COMPLEX"::: ) ); end; registrationlet "C" be ($#m1_hidden :::"set"::: ) ; let "D" be ($#~v1_xboole_0 "non" ($#v1_xboole_0 :::"empty"::: ) ) ($#v3_membered :::"real-membered"::: ) ($#m1_hidden :::"set"::: ) ; let "f" be ($#m1_subset_1 :::"Function":::) "of" (Set (Const "C")) "," (Set (Const "D")); cluster (Set "f" ($#k35_valued_1 :::"""::: ) ) -> ($#v1_partfun1 :::"total"::: ) for ($#m1_subset_1 :::"PartFunc":::) "of" "C" "," (Set ($#k1_numbers :::"REAL"::: ) ); end; registrationlet "C" be ($#m1_hidden :::"set"::: ) ; let "D" be ($#~v1_xboole_0 "non" ($#v1_xboole_0 :::"empty"::: ) ) ($#v4_membered :::"rational-membered"::: ) ($#m1_hidden :::"set"::: ) ; let "f" be ($#m1_subset_1 :::"Function":::) "of" (Set (Const "C")) "," (Set (Const "D")); cluster (Set "f" ($#k35_valued_1 :::"""::: ) ) -> ($#v1_partfun1 :::"total"::: ) for ($#m1_subset_1 :::"PartFunc":::) "of" "C" "," (Set ($#k3_numbers :::"RAT"::: ) ); end; registrationlet "f" be ($#v1_valued_0 :::"complex-valued"::: ) ($#m1_hidden :::"FinSequence":::); cluster (Set "f" ($#k35_valued_1 :::"""::: ) ) -> ($#v1_valued_0 :::"complex-valued"::: ) ($#v1_finseq_1 :::"FinSequence-like"::: ) ; end; begin definitionlet "f" be ($#v1_valued_0 :::"complex-valued"::: ) ($#m1_hidden :::"Function":::); func "f" :::"^2"::: -> ($#m1_hidden :::"Function":::) equals :: VALUED_1:def 8 (Set "f" ($#k18_valued_1 :::"(#)"::: ) "f"); end; :: deftheorem defines :::"^2"::: VALUED_1:def 8 : (Bool "for" (Set (Var "f")) "being" ($#v1_valued_0 :::"complex-valued"::: ) ($#m1_hidden :::"Function":::) "holds" (Bool (Set (Set (Var "f")) ($#k39_valued_1 :::"^2"::: ) ) ($#r1_hidden :::"="::: ) (Set (Set (Var "f")) ($#k18_valued_1 :::"(#)"::: ) (Set (Var "f"))))); theorem :: VALUED_1:11 (Bool "for" (Set (Var "f")) "being" ($#v1_valued_0 :::"complex-valued"::: ) ($#m1_hidden :::"Function":::) "holds" (Bool "(" (Bool (Set ($#k9_xtuple_0 :::"dom"::: ) (Set "(" (Set (Var "f")) ($#k39_valued_1 :::"^2"::: ) ")" )) ($#r1_hidden :::"="::: ) (Set ($#k9_xtuple_0 :::"dom"::: ) (Set (Var "f")))) & (Bool "(" "for" (Set (Var "c")) "being" ($#m1_hidden :::"set"::: ) "holds" (Bool (Set (Set "(" (Set (Var "f")) ($#k39_valued_1 :::"^2"::: ) ")" ) ($#k1_funct_1 :::"."::: ) (Set (Var "c"))) ($#r1_hidden :::"="::: ) (Set (Set "(" (Set (Var "f")) ($#k1_funct_1 :::"."::: ) (Set (Var "c")) ")" ) ($#k3_square_1 :::"^2"::: ) )) ")" ) ")" )) ; registrationlet "f" be ($#v1_valued_0 :::"complex-valued"::: ) ($#m1_hidden :::"Function":::); cluster (Set "f" ($#k39_valued_1 :::"^2"::: ) ) -> ($#v1_valued_0 :::"complex-valued"::: ) ; end; registrationlet "f" be ($#v3_valued_0 :::"real-valued"::: ) ($#m1_hidden :::"Function":::); cluster (Set "f" ($#k39_valued_1 :::"^2"::: ) ) -> ($#v3_valued_0 :::"real-valued"::: ) ; end; registrationlet "f" be (Set ($#k3_numbers :::"RAT"::: ) ) ($#v5_relat_1 :::"-valued"::: ) ($#m1_hidden :::"Function":::); cluster (Set "f" ($#k39_valued_1 :::"^2"::: ) ) -> (Set ($#k3_numbers :::"RAT"::: ) ) ($#v5_relat_1 :::"-valued"::: ) ; end; registrationlet "f" be (Set ($#k4_numbers :::"INT"::: ) ) ($#v5_relat_1 :::"-valued"::: ) ($#m1_hidden :::"Function":::); cluster (Set "f" ($#k39_valued_1 :::"^2"::: ) ) -> (Set ($#k4_numbers :::"INT"::: ) ) ($#v5_relat_1 :::"-valued"::: ) ; end; registrationlet "f" be ($#v4_valued_0 :::"natural-valued"::: ) ($#m1_hidden :::"Function":::); cluster (Set "f" ($#k39_valued_1 :::"^2"::: ) ) -> ($#v4_valued_0 :::"natural-valued"::: ) ; end; definitionlet "C" be ($#m1_hidden :::"set"::: ) ; let "D" be ($#v1_membered :::"complex-membered"::: ) ($#m1_hidden :::"set"::: ) ; let "f" be ($#m1_subset_1 :::"PartFunc":::) "of" (Set (Const "C")) "," (Set (Const "D")); :: original: :::"^2"::: redefine func "f" :::"^2"::: -> ($#m1_subset_1 :::"PartFunc":::) "of" "C" "," (Set ($#k2_numbers :::"COMPLEX"::: ) ); end; definitionlet "C" be ($#m1_hidden :::"set"::: ) ; let "D" be ($#v3_membered :::"real-membered"::: ) ($#m1_hidden :::"set"::: ) ; let "f" be ($#m1_subset_1 :::"PartFunc":::) "of" (Set (Const "C")) "," (Set (Const "D")); :: original: :::"^2"::: redefine func "f" :::"^2"::: -> ($#m1_subset_1 :::"PartFunc":::) "of" "C" "," (Set ($#k1_numbers :::"REAL"::: ) ); end; definitionlet "C" be ($#m1_hidden :::"set"::: ) ; let "D" be ($#v4_membered :::"rational-membered"::: ) ($#m1_hidden :::"set"::: ) ; let "f" be ($#m1_subset_1 :::"PartFunc":::) "of" (Set (Const "C")) "," (Set (Const "D")); :: original: :::"^2"::: redefine func "f" :::"^2"::: -> ($#m1_subset_1 :::"PartFunc":::) "of" "C" "," (Set ($#k3_numbers :::"RAT"::: ) ); end; definitionlet "C" be ($#m1_hidden :::"set"::: ) ; let "D" be ($#v5_membered :::"integer-membered"::: ) ($#m1_hidden :::"set"::: ) ; let "f" be ($#m1_subset_1 :::"PartFunc":::) "of" (Set (Const "C")) "," (Set (Const "D")); :: original: :::"^2"::: redefine func "f" :::"^2"::: -> ($#m1_subset_1 :::"PartFunc":::) "of" "C" "," (Set ($#k4_numbers :::"INT"::: ) ); end; definitionlet "C" be ($#m1_hidden :::"set"::: ) ; let "D" be ($#v6_membered :::"natural-membered"::: ) ($#m1_hidden :::"set"::: ) ; let "f" be ($#m1_subset_1 :::"PartFunc":::) "of" (Set (Const "C")) "," (Set (Const "D")); :: original: :::"^2"::: redefine func "f" :::"^2"::: -> ($#m1_subset_1 :::"PartFunc":::) "of" "C" "," (Set ($#k5_numbers :::"NAT"::: ) ); end; registrationlet "C" be ($#m1_hidden :::"set"::: ) ; let "D" be ($#~v1_xboole_0 "non" ($#v1_xboole_0 :::"empty"::: ) ) ($#v1_membered :::"complex-membered"::: ) ($#m1_hidden :::"set"::: ) ; let "f" be ($#m1_subset_1 :::"Function":::) "of" (Set (Const "C")) "," (Set (Const "D")); cluster (Set "f" ($#k39_valued_1 :::"^2"::: ) ) -> ($#v1_partfun1 :::"total"::: ) for ($#m1_subset_1 :::"PartFunc":::) "of" "C" "," (Set ($#k2_numbers :::"COMPLEX"::: ) ); end; registrationlet "C" be ($#m1_hidden :::"set"::: ) ; let "D" be ($#~v1_xboole_0 "non" ($#v1_xboole_0 :::"empty"::: ) ) ($#v3_membered :::"real-membered"::: ) ($#m1_hidden :::"set"::: ) ; let "f" be ($#m1_subset_1 :::"Function":::) "of" (Set (Const "C")) "," (Set (Const "D")); cluster (Set "f" ($#k39_valued_1 :::"^2"::: ) ) -> ($#v1_partfun1 :::"total"::: ) for ($#m1_subset_1 :::"PartFunc":::) "of" "C" "," (Set ($#k1_numbers :::"REAL"::: ) ); end; registrationlet "C" be ($#m1_hidden :::"set"::: ) ; let "D" be ($#~v1_xboole_0 "non" ($#v1_xboole_0 :::"empty"::: ) ) ($#v4_membered :::"rational-membered"::: ) ($#m1_hidden :::"set"::: ) ; let "f" be ($#m1_subset_1 :::"Function":::) "of" (Set (Const "C")) "," (Set (Const "D")); cluster (Set "f" ($#k39_valued_1 :::"^2"::: ) ) -> ($#v1_partfun1 :::"total"::: ) for ($#m1_subset_1 :::"PartFunc":::) "of" "C" "," (Set ($#k3_numbers :::"RAT"::: ) ); end; registrationlet "C" be ($#m1_hidden :::"set"::: ) ; let "D" be ($#~v1_xboole_0 "non" ($#v1_xboole_0 :::"empty"::: ) ) ($#v5_membered :::"integer-membered"::: ) ($#m1_hidden :::"set"::: ) ; let "f" be ($#m1_subset_1 :::"Function":::) "of" (Set (Const "C")) "," (Set (Const "D")); cluster (Set "f" ($#k39_valued_1 :::"^2"::: ) ) -> ($#v1_partfun1 :::"total"::: ) for ($#m1_subset_1 :::"PartFunc":::) "of" "C" "," (Set ($#k4_numbers :::"INT"::: ) ); end; registrationlet "C" be ($#m1_hidden :::"set"::: ) ; let "D" be ($#~v1_xboole_0 "non" ($#v1_xboole_0 :::"empty"::: ) ) ($#v6_membered :::"natural-membered"::: ) ($#m1_hidden :::"set"::: ) ; let "f" be ($#m1_subset_1 :::"Function":::) "of" (Set (Const "C")) "," (Set (Const "D")); cluster (Set "f" ($#k39_valued_1 :::"^2"::: ) ) -> ($#v1_partfun1 :::"total"::: ) for ($#m1_subset_1 :::"PartFunc":::) "of" "C" "," (Set ($#k5_numbers :::"NAT"::: ) ); end; registrationlet "f" be ($#v1_valued_0 :::"complex-valued"::: ) ($#m1_hidden :::"FinSequence":::); cluster (Set "f" ($#k39_valued_1 :::"^2"::: ) ) -> ($#v1_finseq_1 :::"FinSequence-like"::: ) ; end; begin definitionlet "f1", "f2" be ($#v1_valued_0 :::"complex-valued"::: ) ($#m1_hidden :::"Function":::); func "f1" :::"-"::: "f2" -> ($#m1_hidden :::"Function":::) equals :: VALUED_1:def 9 (Set "f1" ($#k1_valued_1 :::"+"::: ) (Set "(" ($#k30_valued_1 :::"-"::: ) "f2" ")" )); end; :: deftheorem defines :::"-"::: VALUED_1:def 9 : (Bool "for" (Set (Var "f1")) "," (Set (Var "f2")) "being" ($#v1_valued_0 :::"complex-valued"::: ) ($#m1_hidden :::"Function":::) "holds" (Bool (Set (Set (Var "f1")) ($#k45_valued_1 :::"-"::: ) (Set (Var "f2"))) ($#r1_hidden :::"="::: ) (Set (Set (Var "f1")) ($#k1_valued_1 :::"+"::: ) (Set "(" ($#k30_valued_1 :::"-"::: ) (Set (Var "f2")) ")" )))); registrationlet "f1", "f2" be ($#v1_valued_0 :::"complex-valued"::: ) ($#m1_hidden :::"Function":::); cluster (Set "f1" ($#k45_valued_1 :::"-"::: ) "f2") -> ($#v1_valued_0 :::"complex-valued"::: ) ; end; registrationlet "f1", "f2" be ($#v3_valued_0 :::"real-valued"::: ) ($#m1_hidden :::"Function":::); cluster (Set "f1" ($#k45_valued_1 :::"-"::: ) "f2") -> ($#v3_valued_0 :::"real-valued"::: ) ; end; registrationlet "f1", "f2" be (Set ($#k3_numbers :::"RAT"::: ) ) ($#v5_relat_1 :::"-valued"::: ) ($#m1_hidden :::"Function":::); cluster (Set "f1" ($#k45_valued_1 :::"-"::: ) "f2") -> (Set ($#k3_numbers :::"RAT"::: ) ) ($#v5_relat_1 :::"-valued"::: ) ; end; registrationlet "f1", "f2" be (Set ($#k4_numbers :::"INT"::: ) ) ($#v5_relat_1 :::"-valued"::: ) ($#m1_hidden :::"Function":::); cluster (Set "f1" ($#k45_valued_1 :::"-"::: ) "f2") -> (Set ($#k4_numbers :::"INT"::: ) ) ($#v5_relat_1 :::"-valued"::: ) ; end; theorem :: VALUED_1:12 (Bool "for" (Set (Var "f1")) "," (Set (Var "f2")) "being" ($#v1_valued_0 :::"complex-valued"::: ) ($#m1_hidden :::"Function":::) "holds" (Bool (Set ($#k9_xtuple_0 :::"dom"::: ) (Set "(" (Set (Var "f1")) ($#k45_valued_1 :::"-"::: ) (Set (Var "f2")) ")" )) ($#r1_hidden :::"="::: ) (Set (Set "(" ($#k9_xtuple_0 :::"dom"::: ) (Set (Var "f1")) ")" ) ($#k3_xboole_0 :::"/\"::: ) (Set "(" ($#k9_xtuple_0 :::"dom"::: ) (Set (Var "f2")) ")" )))) ; theorem :: VALUED_1:13 (Bool "for" (Set (Var "f1")) "," (Set (Var "f2")) "being" ($#v1_valued_0 :::"complex-valued"::: ) ($#m1_hidden :::"Function":::) (Bool "for" (Set (Var "c")) "being" ($#m1_hidden :::"set"::: ) "st" (Bool (Bool (Set (Var "c")) ($#r2_hidden :::"in"::: ) (Set ($#k9_xtuple_0 :::"dom"::: ) (Set "(" (Set (Var "f1")) ($#k45_valued_1 :::"-"::: ) (Set (Var "f2")) ")" )))) "holds" (Bool (Set (Set "(" (Set (Var "f1")) ($#k45_valued_1 :::"-"::: ) (Set (Var "f2")) ")" ) ($#k1_funct_1 :::"."::: ) (Set (Var "c"))) ($#r1_hidden :::"="::: ) (Set (Set "(" (Set (Var "f1")) ($#k1_funct_1 :::"."::: ) (Set (Var "c")) ")" ) ($#k6_xcmplx_0 :::"-"::: ) (Set "(" (Set (Var "f2")) ($#k1_funct_1 :::"."::: ) (Set (Var "c")) ")" ))))) ; theorem :: VALUED_1:14 (Bool "for" (Set (Var "f1")) "," (Set (Var "f2")) "being" ($#v1_valued_0 :::"complex-valued"::: ) ($#m1_hidden :::"Function":::) (Bool "for" (Set (Var "f")) "being" ($#m1_hidden :::"Function":::) "st" (Bool (Bool (Set ($#k9_xtuple_0 :::"dom"::: ) (Set (Var "f"))) ($#r1_hidden :::"="::: ) (Set ($#k9_xtuple_0 :::"dom"::: ) (Set "(" (Set (Var "f1")) ($#k45_valued_1 :::"-"::: ) (Set (Var "f2")) ")" ))) & (Bool "(" "for" (Set (Var "c")) "being" ($#m1_hidden :::"set"::: ) "st" (Bool (Bool (Set (Var "c")) ($#r2_hidden :::"in"::: ) (Set ($#k9_xtuple_0 :::"dom"::: ) (Set (Var "f"))))) "holds" (Bool (Set (Set (Var "f")) ($#k1_funct_1 :::"."::: ) (Set (Var "c"))) ($#r1_hidden :::"="::: ) (Set (Set "(" (Set (Var "f1")) ($#k1_funct_1 :::"."::: ) (Set (Var "c")) ")" ) ($#k6_xcmplx_0 :::"-"::: ) (Set "(" (Set (Var "f2")) ($#k1_funct_1 :::"."::: ) (Set (Var "c")) ")" ))) ")" )) "holds" (Bool (Set (Var "f")) ($#r1_hidden :::"="::: ) (Set (Set (Var "f1")) ($#k45_valued_1 :::"-"::: ) (Set (Var "f2")))))) ; definitionlet "C" be ($#m1_hidden :::"set"::: ) ; let "D1", "D2" be ($#v1_membered :::"complex-membered"::: ) ($#m1_hidden :::"set"::: ) ; let "f1" be ($#m1_subset_1 :::"PartFunc":::) "of" (Set (Const "C")) "," (Set (Const "D1")); let "f2" be ($#m1_subset_1 :::"PartFunc":::) "of" (Set (Const "C")) "," (Set (Const "D2")); :: original: :::"-"::: redefine func "f1" :::"-"::: "f2" -> ($#m1_subset_1 :::"PartFunc":::) "of" "C" "," (Set ($#k2_numbers :::"COMPLEX"::: ) ); end; definitionlet "C" be ($#m1_hidden :::"set"::: ) ; let "D1", "D2" be ($#v3_membered :::"real-membered"::: ) ($#m1_hidden :::"set"::: ) ; let "f1" be ($#m1_subset_1 :::"PartFunc":::) "of" (Set (Const "C")) "," (Set (Const "D1")); let "f2" be ($#m1_subset_1 :::"PartFunc":::) "of" (Set (Const "C")) "," (Set (Const "D2")); :: original: :::"-"::: redefine func "f1" :::"-"::: "f2" -> ($#m1_subset_1 :::"PartFunc":::) "of" "C" "," (Set ($#k1_numbers :::"REAL"::: ) ); end; definitionlet "C" be ($#m1_hidden :::"set"::: ) ; let "D1", "D2" be ($#v4_membered :::"rational-membered"::: ) ($#m1_hidden :::"set"::: ) ; let "f1" be ($#m1_subset_1 :::"PartFunc":::) "of" (Set (Const "C")) "," (Set (Const "D1")); let "f2" be ($#m1_subset_1 :::"PartFunc":::) "of" (Set (Const "C")) "," (Set (Const "D2")); :: original: :::"-"::: redefine func "f1" :::"-"::: "f2" -> ($#m1_subset_1 :::"PartFunc":::) "of" "C" "," (Set ($#k3_numbers :::"RAT"::: ) ); end; definitionlet "C" be ($#m1_hidden :::"set"::: ) ; let "D1", "D2" be ($#v5_membered :::"integer-membered"::: ) ($#m1_hidden :::"set"::: ) ; let "f1" be ($#m1_subset_1 :::"PartFunc":::) "of" (Set (Const "C")) "," (Set (Const "D1")); let "f2" be ($#m1_subset_1 :::"PartFunc":::) "of" (Set (Const "C")) "," (Set (Const "D2")); :: original: :::"-"::: redefine func "f1" :::"-"::: "f2" -> ($#m1_subset_1 :::"PartFunc":::) "of" "C" "," (Set ($#k4_numbers :::"INT"::: ) ); end; registrationlet "C" be ($#m1_hidden :::"set"::: ) ; let "D1", "D2" be ($#~v1_xboole_0 "non" ($#v1_xboole_0 :::"empty"::: ) ) ($#v1_membered :::"complex-membered"::: ) ($#m1_hidden :::"set"::: ) ; let "f1" be ($#m1_subset_1 :::"Function":::) "of" (Set (Const "C")) "," (Set (Const "D1")); let "f2" be ($#m1_subset_1 :::"Function":::) "of" (Set (Const "C")) "," (Set (Const "D2")); cluster (Set "f1" ($#k45_valued_1 :::"-"::: ) "f2") -> ($#v1_partfun1 :::"total"::: ) for ($#m1_subset_1 :::"PartFunc":::) "of" "C" "," (Set ($#k2_numbers :::"COMPLEX"::: ) ); end; registrationlet "C" be ($#m1_hidden :::"set"::: ) ; let "D1", "D2" be ($#~v1_xboole_0 "non" ($#v1_xboole_0 :::"empty"::: ) ) ($#v3_membered :::"real-membered"::: ) ($#m1_hidden :::"set"::: ) ; let "f1" be ($#m1_subset_1 :::"Function":::) "of" (Set (Const "C")) "," (Set (Const "D1")); let "f2" be ($#m1_subset_1 :::"Function":::) "of" (Set (Const "C")) "," (Set (Const "D2")); cluster (Set "f1" ($#k45_valued_1 :::"-"::: ) "f2") -> ($#v1_partfun1 :::"total"::: ) for ($#m1_subset_1 :::"PartFunc":::) "of" "C" "," (Set ($#k1_numbers :::"REAL"::: ) ); end; registrationlet "C" be ($#m1_hidden :::"set"::: ) ; let "D1", "D2" be ($#~v1_xboole_0 "non" ($#v1_xboole_0 :::"empty"::: ) ) ($#v4_membered :::"rational-membered"::: ) ($#m1_hidden :::"set"::: ) ; let "f1" be ($#m1_subset_1 :::"Function":::) "of" (Set (Const "C")) "," (Set (Const "D1")); let "f2" be ($#m1_subset_1 :::"Function":::) "of" (Set (Const "C")) "," (Set (Const "D2")); cluster (Set "f1" ($#k45_valued_1 :::"-"::: ) "f2") -> ($#v1_partfun1 :::"total"::: ) for ($#m1_subset_1 :::"PartFunc":::) "of" "C" "," (Set ($#k3_numbers :::"RAT"::: ) ); end; registrationlet "C" be ($#m1_hidden :::"set"::: ) ; let "D1", "D2" be ($#~v1_xboole_0 "non" ($#v1_xboole_0 :::"empty"::: ) ) ($#v5_membered :::"integer-membered"::: ) ($#m1_hidden :::"set"::: ) ; let "f1" be ($#m1_subset_1 :::"Function":::) "of" (Set (Const "C")) "," (Set (Const "D1")); let "f2" be ($#m1_subset_1 :::"Function":::) "of" (Set (Const "C")) "," (Set (Const "D2")); cluster (Set "f1" ($#k45_valued_1 :::"-"::: ) "f2") -> ($#v1_partfun1 :::"total"::: ) for ($#m1_subset_1 :::"PartFunc":::) "of" "C" "," (Set ($#k4_numbers :::"INT"::: ) ); end; theorem :: VALUED_1:15 (Bool "for" (Set (Var "C")) "being" ($#m1_hidden :::"set"::: ) (Bool "for" (Set (Var "D1")) "," (Set (Var "D2")) "being" ($#~v1_xboole_0 "non" ($#v1_xboole_0 :::"empty"::: ) ) ($#v1_membered :::"complex-membered"::: ) ($#m1_hidden :::"set"::: ) (Bool "for" (Set (Var "f1")) "being" ($#m1_subset_1 :::"Function":::) "of" (Set (Var "C")) "," (Set (Var "D1")) (Bool "for" (Set (Var "f2")) "being" ($#m1_subset_1 :::"Function":::) "of" (Set (Var "C")) "," (Set (Var "D2")) (Bool "for" (Set (Var "c")) "being" ($#m1_subset_1 :::"Element"::: ) "of" (Set (Var "C")) "holds" (Bool (Set (Set "(" (Set (Var "f1")) ($#k46_valued_1 :::"-"::: ) (Set (Var "f2")) ")" ) ($#k1_funct_1 :::"."::: ) (Set (Var "c"))) ($#r1_hidden :::"="::: ) (Set (Set "(" (Set (Var "f1")) ($#k1_funct_1 :::"."::: ) (Set (Var "c")) ")" ) ($#k6_xcmplx_0 :::"-"::: ) (Set "(" (Set (Var "f2")) ($#k1_funct_1 :::"."::: ) (Set (Var "c")) ")" )))))))) ; registrationlet "f1", "f2" be ($#v1_valued_0 :::"complex-valued"::: ) ($#m1_hidden :::"FinSequence":::); cluster (Set "f1" ($#k45_valued_1 :::"-"::: ) "f2") -> ($#v1_finseq_1 :::"FinSequence-like"::: ) ; end; begin definitionlet "f1", "f2" be ($#v1_valued_0 :::"complex-valued"::: ) ($#m1_hidden :::"Function":::); func "f1" :::"/""::: "f2" -> ($#m1_hidden :::"Function":::) equals :: VALUED_1:def 10 (Set "f1" ($#k18_valued_1 :::"(#)"::: ) (Set "(" "f2" ($#k35_valued_1 :::"""::: ) ")" )); end; :: deftheorem defines :::"/""::: VALUED_1:def 10 : (Bool "for" (Set (Var "f1")) "," (Set (Var "f2")) "being" ($#v1_valued_0 :::"complex-valued"::: ) ($#m1_hidden :::"Function":::) "holds" (Bool (Set (Set (Var "f1")) ($#k50_valued_1 :::"/""::: ) (Set (Var "f2"))) ($#r1_hidden :::"="::: ) (Set (Set (Var "f1")) ($#k18_valued_1 :::"(#)"::: ) (Set "(" (Set (Var "f2")) ($#k35_valued_1 :::"""::: ) ")" )))); theorem :: VALUED_1:16 (Bool "for" (Set (Var "f1")) "," (Set (Var "f2")) "being" ($#v1_valued_0 :::"complex-valued"::: ) ($#m1_hidden :::"Function":::) "holds" (Bool (Set ($#k9_xtuple_0 :::"dom"::: ) (Set "(" (Set (Var "f1")) ($#k50_valued_1 :::"/""::: ) (Set (Var "f2")) ")" )) ($#r1_hidden :::"="::: ) (Set (Set "(" ($#k9_xtuple_0 :::"dom"::: ) (Set (Var "f1")) ")" ) ($#k3_xboole_0 :::"/\"::: ) (Set "(" ($#k9_xtuple_0 :::"dom"::: ) (Set (Var "f2")) ")" )))) ; theorem :: VALUED_1:17 (Bool "for" (Set (Var "f1")) "," (Set (Var "f2")) "being" ($#v1_valued_0 :::"complex-valued"::: ) ($#m1_hidden :::"Function":::) (Bool "for" (Set (Var "c")) "being" ($#m1_hidden :::"set"::: ) "holds" (Bool (Set (Set "(" (Set (Var "f1")) ($#k50_valued_1 :::"/""::: ) (Set (Var "f2")) ")" ) ($#k1_funct_1 :::"."::: ) (Set (Var "c"))) ($#r1_hidden :::"="::: ) (Set (Set "(" (Set (Var "f1")) ($#k1_funct_1 :::"."::: ) (Set (Var "c")) ")" ) ($#k13_complex1 :::"/"::: ) (Set "(" (Set (Var "f2")) ($#k1_funct_1 :::"."::: ) (Set (Var "c")) ")" ))))) ; registrationlet "f1", "f2" be ($#v1_valued_0 :::"complex-valued"::: ) ($#m1_hidden :::"Function":::); cluster (Set "f1" ($#k50_valued_1 :::"/""::: ) "f2") -> ($#v1_valued_0 :::"complex-valued"::: ) ; end; registrationlet "f1", "f2" be ($#v3_valued_0 :::"real-valued"::: ) ($#m1_hidden :::"Function":::); cluster (Set "f1" ($#k50_valued_1 :::"/""::: ) "f2") -> ($#v3_valued_0 :::"real-valued"::: ) ; end; registrationlet "f1", "f2" be (Set ($#k3_numbers :::"RAT"::: ) ) ($#v5_relat_1 :::"-valued"::: ) ($#m1_hidden :::"Function":::); cluster (Set "f1" ($#k50_valued_1 :::"/""::: ) "f2") -> (Set ($#k3_numbers :::"RAT"::: ) ) ($#v5_relat_1 :::"-valued"::: ) ; end; definitionlet "C" be ($#m1_hidden :::"set"::: ) ; let "D1", "D2" be ($#v1_membered :::"complex-membered"::: ) ($#m1_hidden :::"set"::: ) ; let "f1" be ($#m1_subset_1 :::"PartFunc":::) "of" (Set (Const "C")) "," (Set (Const "D1")); let "f2" be ($#m1_subset_1 :::"PartFunc":::) "of" (Set (Const "C")) "," (Set (Const "D2")); :: original: :::"/""::: redefine func "f1" :::"/""::: "f2" -> ($#m1_subset_1 :::"PartFunc":::) "of" "C" "," (Set ($#k2_numbers :::"COMPLEX"::: ) ); end; definitionlet "C" be ($#m1_hidden :::"set"::: ) ; let "D1", "D2" be ($#v3_membered :::"real-membered"::: ) ($#m1_hidden :::"set"::: ) ; let "f1" be ($#m1_subset_1 :::"PartFunc":::) "of" (Set (Const "C")) "," (Set (Const "D1")); let "f2" be ($#m1_subset_1 :::"PartFunc":::) "of" (Set (Const "C")) "," (Set (Const "D2")); :: original: :::"/""::: redefine func "f1" :::"/""::: "f2" -> ($#m1_subset_1 :::"PartFunc":::) "of" "C" "," (Set ($#k1_numbers :::"REAL"::: ) ); end; definitionlet "C" be ($#m1_hidden :::"set"::: ) ; let "D1", "D2" be ($#v4_membered :::"rational-membered"::: ) ($#m1_hidden :::"set"::: ) ; let "f1" be ($#m1_subset_1 :::"PartFunc":::) "of" (Set (Const "C")) "," (Set (Const "D1")); let "f2" be ($#m1_subset_1 :::"PartFunc":::) "of" (Set (Const "C")) "," (Set (Const "D2")); :: original: :::"/""::: redefine func "f1" :::"/""::: "f2" -> ($#m1_subset_1 :::"PartFunc":::) "of" "C" "," (Set ($#k3_numbers :::"RAT"::: ) ); end; registrationlet "C" be ($#m1_hidden :::"set"::: ) ; let "D1", "D2" be ($#~v1_xboole_0 "non" ($#v1_xboole_0 :::"empty"::: ) ) ($#v1_membered :::"complex-membered"::: ) ($#m1_hidden :::"set"::: ) ; let "f1" be ($#m1_subset_1 :::"Function":::) "of" (Set (Const "C")) "," (Set (Const "D1")); let "f2" be ($#m1_subset_1 :::"Function":::) "of" (Set (Const "C")) "," (Set (Const "D2")); cluster (Set "f1" ($#k50_valued_1 :::"/""::: ) "f2") -> ($#v1_partfun1 :::"total"::: ) for ($#m1_subset_1 :::"PartFunc":::) "of" "C" "," (Set ($#k2_numbers :::"COMPLEX"::: ) ); end; registrationlet "C" be ($#m1_hidden :::"set"::: ) ; let "D1", "D2" be ($#~v1_xboole_0 "non" ($#v1_xboole_0 :::"empty"::: ) ) ($#v3_membered :::"real-membered"::: ) ($#m1_hidden :::"set"::: ) ; let "f1" be ($#m1_subset_1 :::"Function":::) "of" (Set (Const "C")) "," (Set (Const "D1")); let "f2" be ($#m1_subset_1 :::"Function":::) "of" (Set (Const "C")) "," (Set (Const "D2")); cluster (Set "f1" ($#k50_valued_1 :::"/""::: ) "f2") -> ($#v1_partfun1 :::"total"::: ) for ($#m1_subset_1 :::"PartFunc":::) "of" "C" "," (Set ($#k1_numbers :::"REAL"::: ) ); end; registrationlet "C" be ($#m1_hidden :::"set"::: ) ; let "D1", "D2" be ($#~v1_xboole_0 "non" ($#v1_xboole_0 :::"empty"::: ) ) ($#v4_membered :::"rational-membered"::: ) ($#m1_hidden :::"set"::: ) ; let "f1" be ($#m1_subset_1 :::"Function":::) "of" (Set (Const "C")) "," (Set (Const "D1")); let "f2" be ($#m1_subset_1 :::"Function":::) "of" (Set (Const "C")) "," (Set (Const "D2")); cluster (Set "f1" ($#k50_valued_1 :::"/""::: ) "f2") -> ($#v1_partfun1 :::"total"::: ) for ($#m1_subset_1 :::"PartFunc":::) "of" "C" "," (Set ($#k3_numbers :::"RAT"::: ) ); end; registrationlet "f1", "f2" be ($#v1_valued_0 :::"complex-valued"::: ) ($#m1_hidden :::"FinSequence":::); cluster (Set "f1" ($#k50_valued_1 :::"/""::: ) "f2") -> ($#v1_finseq_1 :::"FinSequence-like"::: ) ; end; begin definitionlet "f" be ($#v1_valued_0 :::"complex-valued"::: ) ($#m1_hidden :::"Function":::); func :::"|.":::"f":::".|"::: -> ($#v3_valued_0 :::"real-valued"::: ) ($#m1_hidden :::"Function":::) means :: VALUED_1:def 11 (Bool "(" (Bool (Set ($#k9_xtuple_0 :::"dom"::: ) it) ($#r1_hidden :::"="::: ) (Set ($#k9_xtuple_0 :::"dom"::: ) "f")) & (Bool "(" "for" (Set (Var "c")) "being" ($#m1_hidden :::"set"::: ) "st" (Bool (Bool (Set (Var "c")) ($#r2_hidden :::"in"::: ) (Set ($#k9_xtuple_0 :::"dom"::: ) it))) "holds" (Bool (Set it ($#k1_funct_1 :::"."::: ) (Set (Var "c"))) ($#r1_hidden :::"="::: ) (Set ($#k17_complex1 :::"|."::: ) (Set "(" "f" ($#k1_funct_1 :::"."::: ) (Set (Var "c")) ")" ) ($#k17_complex1 :::".|"::: ) )) ")" ) ")" ); projectivity (Bool "for" (Set (Var "b1")) "being" ($#v3_valued_0 :::"real-valued"::: ) ($#m1_hidden :::"Function":::) (Bool "for" (Set (Var "b2")) "being" ($#v1_valued_0 :::"complex-valued"::: ) ($#m1_hidden :::"Function":::) "st" (Bool (Bool (Set ($#k9_xtuple_0 :::"dom"::: ) (Set (Var "b1"))) ($#r1_hidden :::"="::: ) (Set ($#k9_xtuple_0 :::"dom"::: ) (Set (Var "b2")))) & (Bool "(" "for" (Set (Var "c")) "being" ($#m1_hidden :::"set"::: ) "st" (Bool (Bool (Set (Var "c")) ($#r2_hidden :::"in"::: ) (Set ($#k9_xtuple_0 :::"dom"::: ) (Set (Var "b1"))))) "holds" (Bool (Set (Set (Var "b1")) ($#k1_funct_1 :::"."::: ) (Set (Var "c"))) ($#r1_hidden :::"="::: ) (Set ($#k17_complex1 :::"|."::: ) (Set "(" (Set (Var "b2")) ($#k1_funct_1 :::"."::: ) (Set (Var "c")) ")" ) ($#k17_complex1 :::".|"::: ) )) ")" )) "holds" (Bool "(" (Bool (Set ($#k9_xtuple_0 :::"dom"::: ) (Set (Var "b1"))) ($#r1_hidden :::"="::: ) (Set ($#k9_xtuple_0 :::"dom"::: ) (Set (Var "b1")))) & (Bool "(" "for" (Set (Var "c")) "being" ($#m1_hidden :::"set"::: ) "st" (Bool (Bool (Set (Var "c")) ($#r2_hidden :::"in"::: ) (Set ($#k9_xtuple_0 :::"dom"::: ) (Set (Var "b1"))))) "holds" (Bool (Set (Set (Var "b1")) ($#k1_funct_1 :::"."::: ) (Set (Var "c"))) ($#r1_hidden :::"="::: ) (Set ($#k17_complex1 :::"|."::: ) (Set "(" (Set (Var "b1")) ($#k1_funct_1 :::"."::: ) (Set (Var "c")) ")" ) ($#k17_complex1 :::".|"::: ) )) ")" ) ")" ))) ; end; :: deftheorem defines :::"|."::: VALUED_1:def 11 : (Bool "for" (Set (Var "f")) "being" ($#v1_valued_0 :::"complex-valued"::: ) ($#m1_hidden :::"Function":::) (Bool "for" (Set (Var "b2")) "being" ($#v3_valued_0 :::"real-valued"::: ) ($#m1_hidden :::"Function":::) "holds" (Bool "(" (Bool (Set (Var "b2")) ($#r1_hidden :::"="::: ) (Set ($#k54_valued_1 :::"|."::: ) (Set (Var "f")) ($#k54_valued_1 :::".|"::: ) )) "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 "c")) "being" ($#m1_hidden :::"set"::: ) "st" (Bool (Bool (Set (Var "c")) ($#r2_hidden :::"in"::: ) (Set ($#k9_xtuple_0 :::"dom"::: ) (Set (Var "b2"))))) "holds" (Bool (Set (Set (Var "b2")) ($#k1_funct_1 :::"."::: ) (Set (Var "c"))) ($#r1_hidden :::"="::: ) (Set ($#k17_complex1 :::"|."::: ) (Set "(" (Set (Var "f")) ($#k1_funct_1 :::"."::: ) (Set (Var "c")) ")" ) ($#k17_complex1 :::".|"::: ) )) ")" ) ")" ) ")" ))); notationlet "f" be ($#v1_valued_0 :::"complex-valued"::: ) ($#m1_hidden :::"Function":::); synonym :::"abs"::: "f" for :::"|.":::"f":::".|":::; end; theorem :: VALUED_1:18 (Bool "for" (Set (Var "f")) "being" ($#v1_valued_0 :::"complex-valued"::: ) ($#m1_hidden :::"Function":::) (Bool "for" (Set (Var "c")) "being" ($#m1_hidden :::"set"::: ) "holds" (Bool (Set (Set ($#k54_valued_1 :::"|."::: ) (Set (Var "f")) ($#k54_valued_1 :::".|"::: ) ) ($#k1_funct_1 :::"."::: ) (Set (Var "c"))) ($#r1_hidden :::"="::: ) (Set ($#k17_complex1 :::"|."::: ) (Set "(" (Set (Var "f")) ($#k1_funct_1 :::"."::: ) (Set (Var "c")) ")" ) ($#k17_complex1 :::".|"::: ) )))) ; registrationlet "f" be (Set ($#k3_numbers :::"RAT"::: ) ) ($#v5_relat_1 :::"-valued"::: ) ($#m1_hidden :::"Function":::); cluster (Set ($#k54_valued_1 :::"|."::: ) "f" ($#k54_valued_1 :::".|"::: ) ) -> (Set ($#k3_numbers :::"RAT"::: ) ) ($#v5_relat_1 :::"-valued"::: ) ($#v3_valued_0 :::"real-valued"::: ) ; end; registrationlet "f" be (Set ($#k4_numbers :::"INT"::: ) ) ($#v5_relat_1 :::"-valued"::: ) ($#m1_hidden :::"Function":::); cluster (Set ($#k54_valued_1 :::"|."::: ) "f" ($#k54_valued_1 :::".|"::: ) ) -> ($#v3_valued_0 :::"real-valued"::: ) ($#v4_valued_0 :::"natural-valued"::: ) ; end; definitionlet "C" be ($#m1_hidden :::"set"::: ) ; let "D" be ($#v1_membered :::"complex-membered"::: ) ($#m1_hidden :::"set"::: ) ; let "f" be ($#m1_subset_1 :::"PartFunc":::) "of" (Set (Const "C")) "," (Set (Const "D")); :: original: :::"|."::: redefine func :::"|.":::"f":::".|"::: -> ($#m1_subset_1 :::"PartFunc":::) "of" "C" "," (Set ($#k1_numbers :::"REAL"::: ) ); end; definitionlet "C" be ($#m1_hidden :::"set"::: ) ; let "D" be ($#v1_membered :::"complex-membered"::: ) ($#m1_hidden :::"set"::: ) ; let "f" be ($#m1_subset_1 :::"PartFunc":::) "of" (Set (Const "C")) "," (Set (Const "D")); :: original: :::"|."::: redefine func :::"abs"::: "f" -> ($#m1_subset_1 :::"PartFunc":::) "of" "C" "," (Set ($#k1_numbers :::"REAL"::: ) ); end; definitionlet "C" be ($#m1_hidden :::"set"::: ) ; let "D" be ($#v4_membered :::"rational-membered"::: ) ($#m1_hidden :::"set"::: ) ; let "f" be ($#m1_subset_1 :::"PartFunc":::) "of" (Set (Const "C")) "," (Set (Const "D")); :: original: :::"|."::: redefine func :::"|.":::"f":::".|"::: -> ($#m1_subset_1 :::"PartFunc":::) "of" "C" "," (Set ($#k3_numbers :::"RAT"::: ) ); end; definitionlet "C" be ($#m1_hidden :::"set"::: ) ; let "D" be ($#v4_membered :::"rational-membered"::: ) ($#m1_hidden :::"set"::: ) ; let "f" be ($#m1_subset_1 :::"PartFunc":::) "of" (Set (Const "C")) "," (Set (Const "D")); :: original: :::"|."::: redefine func :::"abs"::: "f" -> ($#m1_subset_1 :::"PartFunc":::) "of" "C" "," (Set ($#k3_numbers :::"RAT"::: ) ); end; definitionlet "C" be ($#m1_hidden :::"set"::: ) ; let "D" be ($#v5_membered :::"integer-membered"::: ) ($#m1_hidden :::"set"::: ) ; let "f" be ($#m1_subset_1 :::"PartFunc":::) "of" (Set (Const "C")) "," (Set (Const "D")); :: original: :::"|."::: redefine func :::"|.":::"f":::".|"::: -> ($#m1_subset_1 :::"PartFunc":::) "of" "C" "," (Set ($#k5_numbers :::"NAT"::: ) ); end; definitionlet "C" be ($#m1_hidden :::"set"::: ) ; let "D" be ($#v5_membered :::"integer-membered"::: ) ($#m1_hidden :::"set"::: ) ; let "f" be ($#m1_subset_1 :::"PartFunc":::) "of" (Set (Const "C")) "," (Set (Const "D")); :: original: :::"|."::: redefine func :::"abs"::: "f" -> ($#m1_subset_1 :::"PartFunc":::) "of" "C" "," (Set ($#k5_numbers :::"NAT"::: ) ); end; registrationlet "C" be ($#m1_hidden :::"set"::: ) ; let "D" be ($#~v1_xboole_0 "non" ($#v1_xboole_0 :::"empty"::: ) ) ($#v1_membered :::"complex-membered"::: ) ($#m1_hidden :::"set"::: ) ; let "f" be ($#m1_subset_1 :::"Function":::) "of" (Set (Const "C")) "," (Set (Const "D")); cluster (Set ($#k54_valued_1 :::"|."::: ) "f" ($#k54_valued_1 :::".|"::: ) ) -> ($#v1_partfun1 :::"total"::: ) for ($#m1_subset_1 :::"PartFunc":::) "of" "C" "," (Set ($#k1_numbers :::"REAL"::: ) ); end; registrationlet "C" be ($#m1_hidden :::"set"::: ) ; let "D" be ($#~v1_xboole_0 "non" ($#v1_xboole_0 :::"empty"::: ) ) ($#v4_membered :::"rational-membered"::: ) ($#m1_hidden :::"set"::: ) ; let "f" be ($#m1_subset_1 :::"Function":::) "of" (Set (Const "C")) "," (Set (Const "D")); cluster (Set ($#k54_valued_1 :::"|."::: ) "f" ($#k54_valued_1 :::".|"::: ) ) -> ($#v1_partfun1 :::"total"::: ) for ($#m1_subset_1 :::"PartFunc":::) "of" "C" "," (Set ($#k3_numbers :::"RAT"::: ) ); end; registrationlet "C" be ($#m1_hidden :::"set"::: ) ; let "D" be ($#~v1_xboole_0 "non" ($#v1_xboole_0 :::"empty"::: ) ) ($#v5_membered :::"integer-membered"::: ) ($#m1_hidden :::"set"::: ) ; let "f" be ($#m1_subset_1 :::"Function":::) "of" (Set (Const "C")) "," (Set (Const "D")); cluster (Set ($#k54_valued_1 :::"|."::: ) "f" ($#k54_valued_1 :::".|"::: ) ) -> ($#v1_partfun1 :::"total"::: ) for ($#m1_subset_1 :::"PartFunc":::) "of" "C" "," (Set ($#k5_numbers :::"NAT"::: ) ); end; registrationlet "f" be ($#v1_valued_0 :::"complex-valued"::: ) ($#m1_hidden :::"FinSequence":::); cluster (Set ($#k54_valued_1 :::"|."::: ) "f" ($#k54_valued_1 :::".|"::: ) ) -> ($#v3_valued_0 :::"real-valued"::: ) ($#v1_finseq_1 :::"FinSequence-like"::: ) ; end; theorem :: VALUED_1:19 (Bool "for" (Set (Var "f")) "," (Set (Var "g")) "being" ($#m1_hidden :::"FinSequence":::) (Bool "for" (Set (Var "h")) "being" ($#m1_hidden :::"Function":::) "st" (Bool (Bool (Set ($#k9_xtuple_0 :::"dom"::: ) (Set (Var "h"))) ($#r1_hidden :::"="::: ) (Set (Set "(" ($#k4_finseq_1 :::"dom"::: ) (Set (Var "f")) ")" ) ($#k9_subset_1 :::"/\"::: ) (Set "(" ($#k4_finseq_1 :::"dom"::: ) (Set (Var "g")) ")" )))) "holds" (Bool (Set (Var "h")) "is" ($#m1_hidden :::"FinSequence":::)))) ; begin definitionlet "p" be ($#m1_hidden :::"Function":::); let "k" be ($#m1_hidden :::"Nat":::); func :::"Shift"::: "(" "p" "," "k" ")" -> ($#m1_hidden :::"Function":::) means :: VALUED_1:def 12 (Bool "(" (Bool (Set ($#k9_xtuple_0 :::"dom"::: ) it) ($#r1_hidden :::"="::: ) "{" (Set "(" (Set (Var "m")) ($#k2_nat_1 :::"+"::: ) "k" ")" ) where m "is" ($#m2_subset_1 :::"Element"::: ) "of" (Set ($#k5_numbers :::"NAT"::: ) ) : (Bool (Set (Var "m")) ($#r2_hidden :::"in"::: ) (Set ($#k9_xtuple_0 :::"dom"::: ) "p")) "}" ) & (Bool "(" "for" (Set (Var "m")) "being" ($#m2_subset_1 :::"Element"::: ) "of" (Set ($#k5_numbers :::"NAT"::: ) ) "st" (Bool (Bool (Set (Var "m")) ($#r2_hidden :::"in"::: ) (Set ($#k9_xtuple_0 :::"dom"::: ) "p"))) "holds" (Bool (Set it ($#k1_funct_1 :::"."::: ) (Set "(" (Set (Var "m")) ($#k2_nat_1 :::"+"::: ) "k" ")" )) ($#r1_hidden :::"="::: ) (Set "p" ($#k1_funct_1 :::"."::: ) (Set (Var "m")))) ")" ) ")" ); end; :: deftheorem defines :::"Shift"::: VALUED_1:def 12 : (Bool "for" (Set (Var "p")) "being" ($#m1_hidden :::"Function":::) (Bool "for" (Set (Var "k")) "being" ($#m1_hidden :::"Nat":::) (Bool "for" (Set (Var "b3")) "being" ($#m1_hidden :::"Function":::) "holds" (Bool "(" (Bool (Set (Var "b3")) ($#r1_hidden :::"="::: ) (Set ($#k61_valued_1 :::"Shift"::: ) "(" (Set (Var "p")) "," (Set (Var "k")) ")" )) "iff" (Bool "(" (Bool (Set ($#k9_xtuple_0 :::"dom"::: ) (Set (Var "b3"))) ($#r1_hidden :::"="::: ) "{" (Set "(" (Set (Var "m")) ($#k2_nat_1 :::"+"::: ) (Set (Var "k")) ")" ) where m "is" ($#m2_subset_1 :::"Element"::: ) "of" (Set ($#k5_numbers :::"NAT"::: ) ) : (Bool (Set (Var "m")) ($#r2_hidden :::"in"::: ) (Set ($#k9_xtuple_0 :::"dom"::: ) (Set (Var "p")))) "}" ) & (Bool "(" "for" (Set (Var "m")) "being" ($#m2_subset_1 :::"Element"::: ) "of" (Set ($#k5_numbers :::"NAT"::: ) ) "st" (Bool (Bool (Set (Var "m")) ($#r2_hidden :::"in"::: ) (Set ($#k9_xtuple_0 :::"dom"::: ) (Set (Var "p"))))) "holds" (Bool (Set (Set (Var "b3")) ($#k1_funct_1 :::"."::: ) (Set "(" (Set (Var "m")) ($#k2_nat_1 :::"+"::: ) (Set (Var "k")) ")" )) ($#r1_hidden :::"="::: ) (Set (Set (Var "p")) ($#k1_funct_1 :::"."::: ) (Set (Var "m")))) ")" ) ")" ) ")" )))); registrationlet "p" be ($#m1_hidden :::"Function":::); let "k" be ($#m1_hidden :::"Nat":::); cluster (Set ($#k61_valued_1 :::"Shift"::: ) "(" "p" "," "k" ")" ) -> (Set ($#k5_numbers :::"NAT"::: ) ) ($#v4_relat_1 :::"-defined"::: ) ; end; theorem :: VALUED_1:20 (Bool "for" (Set (Var "P")) "," (Set (Var "Q")) "being" ($#m1_hidden :::"Function":::) (Bool "for" (Set (Var "k")) "being" ($#m1_hidden :::"Nat":::) "st" (Bool (Bool (Set (Var "P")) ($#r1_tarski :::"c="::: ) (Set (Var "Q")))) "holds" (Bool (Set ($#k61_valued_1 :::"Shift"::: ) "(" (Set (Var "P")) "," (Set (Var "k")) ")" ) ($#r1_tarski :::"c="::: ) (Set ($#k61_valued_1 :::"Shift"::: ) "(" (Set (Var "Q")) "," (Set (Var "k")) ")" )))) ; theorem :: VALUED_1:21 (Bool "for" (Set (Var "n")) "," (Set (Var "m")) "being" ($#m1_hidden :::"Nat":::) (Bool "for" (Set (Var "I")) "being" ($#m1_hidden :::"Function":::) "holds" (Bool (Set ($#k61_valued_1 :::"Shift"::: ) "(" (Set "(" ($#k61_valued_1 :::"Shift"::: ) "(" (Set (Var "I")) "," (Set (Var "m")) ")" ")" ) "," (Set (Var "n")) ")" ) ($#r1_hidden :::"="::: ) (Set ($#k61_valued_1 :::"Shift"::: ) "(" (Set (Var "I")) "," (Set "(" (Set (Var "m")) ($#k2_xcmplx_0 :::"+"::: ) (Set (Var "n")) ")" ) ")" )))) ; theorem :: VALUED_1:22 (Bool "for" (Set (Var "s")) "," (Set (Var "f")) "being" ($#m1_hidden :::"Function":::) (Bool "for" (Set (Var "n")) "being" ($#m1_hidden :::"Nat":::) "holds" (Bool (Set ($#k61_valued_1 :::"Shift"::: ) "(" (Set "(" (Set (Var "f")) ($#k3_relat_1 :::"*"::: ) (Set (Var "s")) ")" ) "," (Set (Var "n")) ")" ) ($#r1_hidden :::"="::: ) (Set (Set (Var "f")) ($#k3_relat_1 :::"*"::: ) (Set "(" ($#k61_valued_1 :::"Shift"::: ) "(" (Set (Var "s")) "," (Set (Var "n")) ")" ")" ))))) ; theorem :: VALUED_1:23 (Bool "for" (Set (Var "I")) "," (Set (Var "J")) "being" ($#m1_hidden :::"Function":::) (Bool "for" (Set (Var "n")) "being" ($#m1_hidden :::"Nat":::) "holds" (Bool (Set ($#k61_valued_1 :::"Shift"::: ) "(" (Set "(" (Set (Var "I")) ($#k1_funct_4 :::"+*"::: ) (Set (Var "J")) ")" ) "," (Set (Var "n")) ")" ) ($#r1_hidden :::"="::: ) (Set (Set "(" ($#k61_valued_1 :::"Shift"::: ) "(" (Set (Var "I")) "," (Set (Var "n")) ")" ")" ) ($#k1_funct_4 :::"+*"::: ) (Set "(" ($#k61_valued_1 :::"Shift"::: ) "(" (Set (Var "J")) "," (Set (Var "n")) ")" ")" ))))) ; theorem :: VALUED_1:24 (Bool "for" (Set (Var "p")) "being" ($#m1_hidden :::"Function":::) (Bool "for" (Set (Var "k")) "," (Set (Var "il")) "being" ($#m1_hidden :::"Nat":::) "st" (Bool (Bool (Set (Var "il")) ($#r2_hidden :::"in"::: ) (Set ($#k9_xtuple_0 :::"dom"::: ) (Set (Var "p"))))) "holds" (Bool (Set (Set (Var "il")) ($#k2_xcmplx_0 :::"+"::: ) (Set (Var "k"))) ($#r2_hidden :::"in"::: ) (Set ($#k1_relset_1 :::"dom"::: ) (Set "(" ($#k61_valued_1 :::"Shift"::: ) "(" (Set (Var "p")) "," (Set (Var "k")) ")" ")" ))))) ; theorem :: VALUED_1:25 (Bool "for" (Set (Var "p")) "being" ($#m1_hidden :::"Function":::) (Bool "for" (Set (Var "k")) "being" ($#m1_hidden :::"Nat":::) "holds" (Bool (Set ($#k10_xtuple_0 :::"rng"::: ) (Set "(" ($#k61_valued_1 :::"Shift"::: ) "(" (Set (Var "p")) "," (Set (Var "k")) ")" ")" )) ($#r1_tarski :::"c="::: ) (Set ($#k10_xtuple_0 :::"rng"::: ) (Set (Var "p")))))) ; theorem :: VALUED_1:26 (Bool "for" (Set (Var "p")) "being" ($#m1_hidden :::"Function":::) "st" (Bool (Bool (Set ($#k9_xtuple_0 :::"dom"::: ) (Set (Var "p"))) ($#r1_tarski :::"c="::: ) (Set ($#k5_numbers :::"NAT"::: ) ))) "holds" (Bool "for" (Set (Var "k")) "being" ($#m1_hidden :::"Nat":::) "holds" (Bool (Set ($#k10_xtuple_0 :::"rng"::: ) (Set "(" ($#k61_valued_1 :::"Shift"::: ) "(" (Set (Var "p")) "," (Set (Var "k")) ")" ")" )) ($#r1_hidden :::"="::: ) (Set ($#k10_xtuple_0 :::"rng"::: ) (Set (Var "p")))))) ; registrationlet "p" be ($#v1_finset_1 :::"finite"::: ) ($#m1_hidden :::"Function":::); let "k" be ($#m1_hidden :::"Nat":::); cluster (Set ($#k61_valued_1 :::"Shift"::: ) "(" "p" "," "k" ")" ) -> ($#v1_finset_1 :::"finite"::: ) ; end; definitionlet "X" be ($#~v1_xboole_0 "non" ($#v1_xboole_0 :::"empty"::: ) ) ($#v2_membered :::"ext-real-membered"::: ) ($#m1_hidden :::"set"::: ) ; let "s" be ($#m1_subset_1 :::"sequence":::) "of" (Set (Const "X")); :: original: :::"increasing"::: redefine attr "s" is :::"increasing"::: means :: VALUED_1:def 13 (Bool "for" (Set (Var "n")) "being" ($#m1_hidden :::"Nat":::) "holds" (Bool (Set "s" ($#k8_nat_1 :::"."::: ) (Set (Var "n"))) ($#r1_xxreal_0 :::"<"::: ) (Set "s" ($#k8_nat_1 :::"."::: ) (Set "(" (Set (Var "n")) ($#k1_nat_1 :::"+"::: ) (Num 1) ")" )))); :: original: :::"decreasing"::: redefine attr "s" is :::"decreasing"::: means :: VALUED_1:def 14 (Bool "for" (Set (Var "n")) "being" ($#m1_hidden :::"Nat":::) "holds" (Bool (Set "s" ($#k8_nat_1 :::"."::: ) (Set (Var "n"))) ($#r1_xxreal_0 :::">"::: ) (Set "s" ($#k8_nat_1 :::"."::: ) (Set "(" (Set (Var "n")) ($#k1_nat_1 :::"+"::: ) (Num 1) ")" )))); :: original: :::"non-decreasing"::: redefine attr "s" is :::"non-decreasing"::: means :: VALUED_1:def 15 (Bool "for" (Set (Var "n")) "being" ($#m1_hidden :::"Nat":::) "holds" (Bool (Set "s" ($#k8_nat_1 :::"."::: ) (Set (Var "n"))) ($#r1_xxreal_0 :::"<="::: ) (Set "s" ($#k8_nat_1 :::"."::: ) (Set "(" (Set (Var "n")) ($#k1_nat_1 :::"+"::: ) (Num 1) ")" )))); :: original: :::"non-increasing"::: redefine attr "s" is :::"non-increasing"::: means :: VALUED_1:def 16 (Bool "for" (Set (Var "n")) "being" ($#m1_hidden :::"Nat":::) "holds" (Bool (Set "s" ($#k8_nat_1 :::"."::: ) (Set (Var "n"))) ($#r1_xxreal_0 :::">="::: ) (Set "s" ($#k8_nat_1 :::"."::: ) (Set "(" (Set (Var "n")) ($#k1_nat_1 :::"+"::: ) (Num 1) ")" )))); end; :: deftheorem defines :::"increasing"::: VALUED_1:def 13 : (Bool "for" (Set (Var "X")) "being" ($#~v1_xboole_0 "non" ($#v1_xboole_0 :::"empty"::: ) ) ($#v2_membered :::"ext-real-membered"::: ) ($#m1_hidden :::"set"::: ) (Bool "for" (Set (Var "s")) "being" ($#m1_subset_1 :::"sequence":::) "of" (Set (Var "X")) "holds" (Bool "(" (Bool (Set (Var "s")) "is" ($#v5_valued_0 :::"increasing"::: ) ) "iff" (Bool "for" (Set (Var "n")) "being" ($#m1_hidden :::"Nat":::) "holds" (Bool (Set (Set (Var "s")) ($#k8_nat_1 :::"."::: ) (Set (Var "n"))) ($#r1_xxreal_0 :::"<"::: ) (Set (Set (Var "s")) ($#k8_nat_1 :::"."::: ) (Set "(" (Set (Var "n")) ($#k1_nat_1 :::"+"::: ) (Num 1) ")" )))) ")" ))); :: deftheorem defines :::"decreasing"::: VALUED_1:def 14 : (Bool "for" (Set (Var "X")) "being" ($#~v1_xboole_0 "non" ($#v1_xboole_0 :::"empty"::: ) ) ($#v2_membered :::"ext-real-membered"::: ) ($#m1_hidden :::"set"::: ) (Bool "for" (Set (Var "s")) "being" ($#m1_subset_1 :::"sequence":::) "of" (Set (Var "X")) "holds" (Bool "(" (Bool (Set (Var "s")) "is" ($#v6_valued_0 :::"decreasing"::: ) ) "iff" (Bool "for" (Set (Var "n")) "being" ($#m1_hidden :::"Nat":::) "holds" (Bool (Set (Set (Var "s")) ($#k8_nat_1 :::"."::: ) (Set (Var "n"))) ($#r1_xxreal_0 :::">"::: ) (Set (Set (Var "s")) ($#k8_nat_1 :::"."::: ) (Set "(" (Set (Var "n")) ($#k1_nat_1 :::"+"::: ) (Num 1) ")" )))) ")" ))); :: deftheorem defines :::"non-decreasing"::: VALUED_1:def 15 : (Bool "for" (Set (Var "X")) "being" ($#~v1_xboole_0 "non" ($#v1_xboole_0 :::"empty"::: ) ) ($#v2_membered :::"ext-real-membered"::: ) ($#m1_hidden :::"set"::: ) (Bool "for" (Set (Var "s")) "being" ($#m1_subset_1 :::"sequence":::) "of" (Set (Var "X")) "holds" (Bool "(" (Bool (Set (Var "s")) "is" ($#v7_valued_0 :::"non-decreasing"::: ) ) "iff" (Bool "for" (Set (Var "n")) "being" ($#m1_hidden :::"Nat":::) "holds" (Bool (Set (Set (Var "s")) ($#k8_nat_1 :::"."::: ) (Set (Var "n"))) ($#r1_xxreal_0 :::"<="::: ) (Set (Set (Var "s")) ($#k8_nat_1 :::"."::: ) (Set "(" (Set (Var "n")) ($#k1_nat_1 :::"+"::: ) (Num 1) ")" )))) ")" ))); :: deftheorem defines :::"non-increasing"::: VALUED_1:def 16 : (Bool "for" (Set (Var "X")) "being" ($#~v1_xboole_0 "non" ($#v1_xboole_0 :::"empty"::: ) ) ($#v2_membered :::"ext-real-membered"::: ) ($#m1_hidden :::"set"::: ) (Bool "for" (Set (Var "s")) "being" ($#m1_subset_1 :::"sequence":::) "of" (Set (Var "X")) "holds" (Bool "(" (Bool (Set (Var "s")) "is" ($#v8_valued_0 :::"non-increasing"::: ) ) "iff" (Bool "for" (Set (Var "n")) "being" ($#m1_hidden :::"Nat":::) "holds" (Bool (Set (Set (Var "s")) ($#k8_nat_1 :::"."::: ) (Set (Var "n"))) ($#r1_xxreal_0 :::">="::: ) (Set (Set (Var "s")) ($#k8_nat_1 :::"."::: ) (Set "(" (Set (Var "n")) ($#k1_nat_1 :::"+"::: ) (Num 1) ")" )))) ")" ))); scheme :: VALUED_1:sch 1 SubSeqChoice{ F1() -> ($#~v1_xboole_0 "non" ($#v1_xboole_0 :::"empty"::: ) ) ($#m1_hidden :::"set"::: ) , F2() -> ($#m1_subset_1 :::"sequence":::) "of" (Set F1 "(" ")" ), P1[ ($#m1_hidden :::"set"::: ) ] } : (Bool "ex" (Set (Var "S1")) "being" ($#m2_valued_0 :::"subsequence"::: ) "of" (Set F2 "(" ")" ) "st" (Bool "for" (Set (Var "n")) "being" ($#m2_subset_1 :::"Element"::: ) "of" (Set ($#k5_numbers :::"NAT"::: ) ) "holds" (Bool P1[(Set (Set (Var "S1")) ($#k8_nat_1 :::"."::: ) (Set (Var "n")))]))) provided (Bool "for" (Set (Var "n")) "being" ($#m2_subset_1 :::"Element"::: ) "of" (Set ($#k5_numbers :::"NAT"::: ) ) (Bool "ex" (Set (Var "m")) "being" ($#m2_subset_1 :::"Element"::: ) "of" (Set ($#k5_numbers :::"NAT"::: ) ) "st" (Bool "(" (Bool (Set (Var "n")) ($#r1_xxreal_0 :::"<="::: ) (Set (Var "m"))) & (Bool P1[(Set (Set F2 "(" ")" ) ($#k8_nat_1 :::"."::: ) (Set (Var "m")))]) ")" ))) proof end; theorem :: VALUED_1:27 (Bool "for" (Set (Var "k")) "being" ($#m1_hidden :::"Nat":::) (Bool "for" (Set (Var "F")) "being" (Set ($#k5_numbers :::"NAT"::: ) ) ($#v4_relat_1 :::"-defined"::: ) ($#m1_hidden :::"Function":::) "holds" (Bool (Set ($#k1_relset_1 :::"dom"::: ) (Set (Var "F"))) "," (Set ($#k1_relset_1 :::"dom"::: ) (Set "(" ($#k61_valued_1 :::"Shift"::: ) "(" (Set (Var "F")) "," (Set (Var "k")) ")" ")" )) ($#r2_tarski :::"are_equipotent"::: ) ))) ; registrationlet "F" be (Set ($#k5_numbers :::"NAT"::: ) ) ($#v4_relat_1 :::"-defined"::: ) ($#m1_hidden :::"Function":::); reduce ; end; theorem :: VALUED_1:28 (Bool "for" (Set (Var "F")) "being" (Set ($#k5_numbers :::"NAT"::: ) ) ($#v4_relat_1 :::"-defined"::: ) ($#m1_hidden :::"Function":::) "holds" (Bool (Set ($#k61_valued_1 :::"Shift"::: ) "(" (Set (Var "F")) "," (Set ($#k6_numbers :::"0"::: ) ) ")" ) ($#r1_hidden :::"="::: ) (Set (Var "F")))) ; registrationlet "X" be ($#~v1_xboole_0 "non" ($#v1_xboole_0 :::"empty"::: ) ) ($#m1_hidden :::"set"::: ) ; let "F" be (Set (Const "X")) ($#v5_relat_1 :::"-valued"::: ) ($#m1_hidden :::"Function":::); let "k" be ($#m1_hidden :::"Nat":::); cluster (Set ($#k61_valued_1 :::"Shift"::: ) "(" "F" "," "k" ")" ) -> "X" ($#v5_relat_1 :::"-valued"::: ) ; end; registration cluster ($#v1_relat_1 :::"Relation-like"::: ) (Set ($#k5_numbers :::"NAT"::: ) ) ($#v4_relat_1 :::"-defined"::: ) ($#v1_funct_1 :::"Function-like"::: ) ($#~v1_xboole_0 "non" ($#v1_xboole_0 :::"empty"::: ) ) for ($#m1_hidden :::"set"::: ) ; end; registrationlet "F" be ($#v1_xboole_0 :::"empty"::: ) ($#m1_hidden :::"Function":::); let "k" be ($#m1_hidden :::"Nat":::); cluster (Set ($#k61_valued_1 :::"Shift"::: ) "(" "F" "," "k" ")" ) -> ($#v1_xboole_0 :::"empty"::: ) ; end; registrationlet "F" be (Set ($#k5_numbers :::"NAT"::: ) ) ($#v4_relat_1 :::"-defined"::: ) ($#~v1_xboole_0 "non" ($#v1_xboole_0 :::"empty"::: ) ) ($#m1_hidden :::"Function":::); let "k" be ($#m1_hidden :::"Nat":::); cluster (Set ($#k61_valued_1 :::"Shift"::: ) "(" "F" "," "k" ")" ) -> ($#~v1_xboole_0 "non" ($#v1_xboole_0 :::"empty"::: ) ) ; end; theorem :: VALUED_1:29 (Bool "for" (Set (Var "F")) "being" ($#m1_hidden :::"Function":::) (Bool "for" (Set (Var "k")) "being" ($#m1_hidden :::"Nat":::) "st" (Bool (Bool (Set (Var "k")) ($#r1_xxreal_0 :::">"::: ) (Set ($#k6_numbers :::"0"::: ) ))) "holds" (Bool "not" (Bool (Set ($#k6_numbers :::"0"::: ) ) ($#r2_hidden :::"in"::: ) (Set ($#k1_relset_1 :::"dom"::: ) (Set "(" ($#k61_valued_1 :::"Shift"::: ) "(" (Set (Var "F")) "," (Set (Var "k")) ")" ")" )))))) ; registration cluster ($#v1_relat_1 :::"Relation-like"::: ) (Set ($#k5_numbers :::"NAT"::: ) ) ($#v4_relat_1 :::"-defined"::: ) ($#v1_funct_1 :::"Function-like"::: ) ($#~v1_xboole_0 "non" ($#v1_xboole_0 :::"empty"::: ) ) ($#v1_finset_1 :::"finite"::: ) for ($#m1_hidden :::"set"::: ) ; end; registrationlet "F" be (Set ($#k5_numbers :::"NAT"::: ) ) ($#v4_relat_1 :::"-defined"::: ) ($#m1_hidden :::"Relation":::); cluster (Set ($#k9_xtuple_0 :::"dom"::: ) "F") -> ($#v6_membered :::"natural-membered"::: ) ; end; definitionlet "F" be (Set ($#k5_numbers :::"NAT"::: ) ) ($#v4_relat_1 :::"-defined"::: ) ($#~v1_xboole_0 "non" ($#v1_xboole_0 :::"empty"::: ) ) ($#v1_finset_1 :::"finite"::: ) ($#m1_hidden :::"Function":::); func :::"LastLoc"::: "F" -> ($#m2_subset_1 :::"Element"::: ) "of" (Set ($#k5_numbers :::"NAT"::: ) ) equals :: VALUED_1:def 17 (Set ($#k1_xxreal_2 :::"max"::: ) (Set "(" ($#k1_relset_1 :::"dom"::: ) "F" ")" )); end; :: deftheorem defines :::"LastLoc"::: VALUED_1:def 17 : (Bool "for" (Set (Var "F")) "being" (Set ($#k5_numbers :::"NAT"::: ) ) ($#v4_relat_1 :::"-defined"::: ) ($#~v1_xboole_0 "non" ($#v1_xboole_0 :::"empty"::: ) ) ($#v1_finset_1 :::"finite"::: ) ($#m1_hidden :::"Function":::) "holds" (Bool (Set ($#k62_valued_1 :::"LastLoc"::: ) (Set (Var "F"))) ($#r1_hidden :::"="::: ) (Set ($#k1_xxreal_2 :::"max"::: ) (Set "(" ($#k1_relset_1 :::"dom"::: ) (Set (Var "F")) ")" )))); definitionlet "F" be (Set ($#k5_numbers :::"NAT"::: ) ) ($#v4_relat_1 :::"-defined"::: ) ($#~v1_xboole_0 "non" ($#v1_xboole_0 :::"empty"::: ) ) ($#v1_finset_1 :::"finite"::: ) ($#m1_hidden :::"Function":::); func :::"CutLastLoc"::: "F" -> ($#m1_hidden :::"Function":::) equals :: VALUED_1:def 18 (Set "F" ($#k6_subset_1 :::"\"::: ) (Set "(" (Set "(" ($#k62_valued_1 :::"LastLoc"::: ) "F" ")" ) ($#k16_funcop_1 :::".-->"::: ) (Set "(" "F" ($#k1_funct_1 :::"."::: ) (Set "(" ($#k62_valued_1 :::"LastLoc"::: ) "F" ")" ) ")" ) ")" )); end; :: deftheorem defines :::"CutLastLoc"::: VALUED_1:def 18 : (Bool "for" (Set (Var "F")) "being" (Set ($#k5_numbers :::"NAT"::: ) ) ($#v4_relat_1 :::"-defined"::: ) ($#~v1_xboole_0 "non" ($#v1_xboole_0 :::"empty"::: ) ) ($#v1_finset_1 :::"finite"::: ) ($#m1_hidden :::"Function":::) "holds" (Bool (Set ($#k63_valued_1 :::"CutLastLoc"::: ) (Set (Var "F"))) ($#r1_hidden :::"="::: ) (Set (Set (Var "F")) ($#k6_subset_1 :::"\"::: ) (Set "(" (Set "(" ($#k62_valued_1 :::"LastLoc"::: ) (Set (Var "F")) ")" ) ($#k16_funcop_1 :::".-->"::: ) (Set "(" (Set (Var "F")) ($#k1_funct_1 :::"."::: ) (Set "(" ($#k62_valued_1 :::"LastLoc"::: ) (Set (Var "F")) ")" ) ")" ) ")" )))); registrationlet "F" be (Set ($#k5_numbers :::"NAT"::: ) ) ($#v4_relat_1 :::"-defined"::: ) ($#~v1_xboole_0 "non" ($#v1_xboole_0 :::"empty"::: ) ) ($#v1_finset_1 :::"finite"::: ) ($#m1_hidden :::"Function":::); cluster (Set ($#k63_valued_1 :::"CutLastLoc"::: ) "F") -> (Set ($#k5_numbers :::"NAT"::: ) ) ($#v4_relat_1 :::"-defined"::: ) ($#v1_finset_1 :::"finite"::: ) ; end; theorem :: VALUED_1:30 (Bool "for" (Set (Var "F")) "being" (Set ($#k5_numbers :::"NAT"::: ) ) ($#v4_relat_1 :::"-defined"::: ) ($#~v1_xboole_0 "non" ($#v1_xboole_0 :::"empty"::: ) ) ($#v1_finset_1 :::"finite"::: ) ($#m1_hidden :::"Function":::) "holds" (Bool (Set ($#k62_valued_1 :::"LastLoc"::: ) (Set (Var "F"))) ($#r2_hidden :::"in"::: ) (Set ($#k1_relset_1 :::"dom"::: ) (Set (Var "F"))))) ; theorem :: VALUED_1:31 (Bool "for" (Set (Var "F")) "," (Set (Var "G")) "being" (Set ($#k5_numbers :::"NAT"::: ) ) ($#v4_relat_1 :::"-defined"::: ) ($#~v1_xboole_0 "non" ($#v1_xboole_0 :::"empty"::: ) ) ($#v1_finset_1 :::"finite"::: ) ($#m1_hidden :::"Function":::) "st" (Bool (Bool (Set (Var "F")) ($#r1_tarski :::"c="::: ) (Set (Var "G")))) "holds" (Bool (Set ($#k62_valued_1 :::"LastLoc"::: ) (Set (Var "F"))) ($#r1_xxreal_0 :::"<="::: ) (Set ($#k62_valued_1 :::"LastLoc"::: ) (Set (Var "G"))))) ; theorem :: VALUED_1:32 (Bool "for" (Set (Var "F")) "being" (Set ($#k5_numbers :::"NAT"::: ) ) ($#v4_relat_1 :::"-defined"::: ) ($#~v1_xboole_0 "non" ($#v1_xboole_0 :::"empty"::: ) ) ($#v1_finset_1 :::"finite"::: ) ($#m1_hidden :::"Function":::) (Bool "for" (Set (Var "l")) "being" ($#m2_subset_1 :::"Element"::: ) "of" (Set ($#k5_numbers :::"NAT"::: ) ) "st" (Bool (Bool (Set (Var "l")) ($#r2_hidden :::"in"::: ) (Set ($#k1_relset_1 :::"dom"::: ) (Set (Var "F"))))) "holds" (Bool (Set (Var "l")) ($#r1_xxreal_0 :::"<="::: ) (Set ($#k62_valued_1 :::"LastLoc"::: ) (Set (Var "F")))))) ; definitionlet "F" be (Set ($#k5_numbers :::"NAT"::: ) ) ($#v4_relat_1 :::"-defined"::: ) ($#~v1_xboole_0 "non" ($#v1_xboole_0 :::"empty"::: ) ) ($#m1_hidden :::"Function":::); func :::"FirstLoc"::: "F" -> ($#m2_subset_1 :::"Element"::: ) "of" (Set ($#k5_numbers :::"NAT"::: ) ) equals :: VALUED_1:def 19 (Set ($#k2_xxreal_2 :::"min"::: ) (Set "(" ($#k1_relset_1 :::"dom"::: ) "F" ")" )); end; :: deftheorem defines :::"FirstLoc"::: VALUED_1:def 19 : (Bool "for" (Set (Var "F")) "being" (Set ($#k5_numbers :::"NAT"::: ) ) ($#v4_relat_1 :::"-defined"::: ) ($#~v1_xboole_0 "non" ($#v1_xboole_0 :::"empty"::: ) ) ($#m1_hidden :::"Function":::) "holds" (Bool (Set ($#k64_valued_1 :::"FirstLoc"::: ) (Set (Var "F"))) ($#r1_hidden :::"="::: ) (Set ($#k2_xxreal_2 :::"min"::: ) (Set "(" ($#k1_relset_1 :::"dom"::: ) (Set (Var "F")) ")" )))); theorem :: VALUED_1:33 (Bool "for" (Set (Var "F")) "being" (Set ($#k5_numbers :::"NAT"::: ) ) ($#v4_relat_1 :::"-defined"::: ) ($#~v1_xboole_0 "non" ($#v1_xboole_0 :::"empty"::: ) ) ($#v1_finset_1 :::"finite"::: ) ($#m1_hidden :::"Function":::) "holds" (Bool (Set ($#k64_valued_1 :::"FirstLoc"::: ) (Set (Var "F"))) ($#r2_hidden :::"in"::: ) (Set ($#k1_relset_1 :::"dom"::: ) (Set (Var "F"))))) ; theorem :: VALUED_1:34 (Bool "for" (Set (Var "F")) "," (Set (Var "G")) "being" (Set ($#k5_numbers :::"NAT"::: ) ) ($#v4_relat_1 :::"-defined"::: ) ($#~v1_xboole_0 "non" ($#v1_xboole_0 :::"empty"::: ) ) ($#v1_finset_1 :::"finite"::: ) ($#m1_hidden :::"Function":::) "st" (Bool (Bool (Set (Var "F")) ($#r1_tarski :::"c="::: ) (Set (Var "G")))) "holds" (Bool (Set ($#k64_valued_1 :::"FirstLoc"::: ) (Set (Var "G"))) ($#r1_xxreal_0 :::"<="::: ) (Set ($#k64_valued_1 :::"FirstLoc"::: ) (Set (Var "F"))))) ; theorem :: VALUED_1:35 (Bool "for" (Set (Var "l1")) "being" ($#m2_subset_1 :::"Element"::: ) "of" (Set ($#k5_numbers :::"NAT"::: ) ) (Bool "for" (Set (Var "F")) "being" (Set ($#k5_numbers :::"NAT"::: ) ) ($#v4_relat_1 :::"-defined"::: ) ($#~v1_xboole_0 "non" ($#v1_xboole_0 :::"empty"::: ) ) ($#v1_finset_1 :::"finite"::: ) ($#m1_hidden :::"Function":::) "st" (Bool (Bool (Set (Var "l1")) ($#r2_hidden :::"in"::: ) (Set ($#k1_relset_1 :::"dom"::: ) (Set (Var "F"))))) "holds" (Bool (Set ($#k64_valued_1 :::"FirstLoc"::: ) (Set (Var "F"))) ($#r1_xxreal_0 :::"<="::: ) (Set (Var "l1"))))) ; theorem :: VALUED_1:36 (Bool "for" (Set (Var "F")) "being" (Set ($#k5_numbers :::"NAT"::: ) ) ($#v4_relat_1 :::"-defined"::: ) ($#~v1_xboole_0 "non" ($#v1_xboole_0 :::"empty"::: ) ) ($#v1_finset_1 :::"finite"::: ) ($#m1_hidden :::"Function":::) "holds" (Bool (Set ($#k1_relset_1 :::"dom"::: ) (Set "(" ($#k63_valued_1 :::"CutLastLoc"::: ) (Set (Var "F")) ")" )) ($#r1_hidden :::"="::: ) (Set (Set "(" ($#k1_relset_1 :::"dom"::: ) (Set (Var "F")) ")" ) ($#k7_subset_1 :::"\"::: ) (Set ($#k1_tarski :::"{"::: ) (Set "(" ($#k62_valued_1 :::"LastLoc"::: ) (Set (Var "F")) ")" ) ($#k1_tarski :::"}"::: ) )))) ; theorem :: VALUED_1:37 (Bool "for" (Set (Var "F")) "being" (Set ($#k5_numbers :::"NAT"::: ) ) ($#v4_relat_1 :::"-defined"::: ) ($#~v1_xboole_0 "non" ($#v1_xboole_0 :::"empty"::: ) ) ($#v1_finset_1 :::"finite"::: ) ($#m1_hidden :::"Function":::) "holds" (Bool (Set ($#k1_relset_1 :::"dom"::: ) (Set (Var "F"))) ($#r1_hidden :::"="::: ) (Set (Set "(" ($#k1_relset_1 :::"dom"::: ) (Set "(" ($#k63_valued_1 :::"CutLastLoc"::: ) (Set (Var "F")) ")" ) ")" ) ($#k2_xboole_0 :::"\/"::: ) (Set ($#k1_tarski :::"{"::: ) (Set "(" ($#k62_valued_1 :::"LastLoc"::: ) (Set (Var "F")) ")" ) ($#k1_tarski :::"}"::: ) )))) ; registration cluster ($#v1_relat_1 :::"Relation-like"::: ) (Set ($#k5_numbers :::"NAT"::: ) ) ($#v4_relat_1 :::"-defined"::: ) ($#v1_funct_1 :::"Function-like"::: ) ($#v1_finset_1 :::"finite"::: ) (Num 1) ($#v3_card_1 :::"-element"::: ) for ($#m1_hidden :::"set"::: ) ; end; registrationlet "F" be (Set ($#k5_numbers :::"NAT"::: ) ) ($#v4_relat_1 :::"-defined"::: ) ($#v1_finset_1 :::"finite"::: ) (Num 1) ($#v3_card_1 :::"-element"::: ) ($#m1_hidden :::"Function":::); cluster (Set ($#k63_valued_1 :::"CutLastLoc"::: ) "F") -> ($#v1_xboole_0 :::"empty"::: ) ; end; theorem :: VALUED_1:38 (Bool "for" (Set (Var "F")) "being" (Set ($#k5_numbers :::"NAT"::: ) ) ($#v4_relat_1 :::"-defined"::: ) ($#~v1_xboole_0 "non" ($#v1_xboole_0 :::"empty"::: ) ) ($#v1_finset_1 :::"finite"::: ) ($#m1_hidden :::"Function":::) "holds" (Bool (Set ($#k5_card_1 :::"card"::: ) (Set "(" ($#k63_valued_1 :::"CutLastLoc"::: ) (Set (Var "F")) ")" )) ($#r1_hidden :::"="::: ) (Set (Set "(" ($#k5_card_1 :::"card"::: ) (Set (Var "F")) ")" ) ($#k6_xcmplx_0 :::"-"::: ) (Num 1)))) ; begin registrationlet "X" be ($#m1_hidden :::"set"::: ) ; let "f" be (Set (Const "X")) ($#v4_relat_1 :::"-defined"::: ) ($#v1_valued_0 :::"complex-valued"::: ) ($#m1_hidden :::"Function":::); cluster (Set ($#k30_valued_1 :::"-"::: ) "f") -> "X" ($#v4_relat_1 :::"-defined"::: ) ($#v1_valued_0 :::"complex-valued"::: ) ; cluster (Set "f" ($#k35_valued_1 :::"""::: ) ) -> "X" ($#v4_relat_1 :::"-defined"::: ) ($#v1_valued_0 :::"complex-valued"::: ) ; cluster (Set "f" ($#k39_valued_1 :::"^2"::: ) ) -> "X" ($#v4_relat_1 :::"-defined"::: ) ; cluster (Set ($#k54_valued_1 :::"|."::: ) "f" ($#k54_valued_1 :::".|"::: ) ) -> "X" ($#v4_relat_1 :::"-defined"::: ) ($#v3_valued_0 :::"real-valued"::: ) ; end; registrationlet "X" be ($#m1_hidden :::"set"::: ) ; cluster ($#v1_relat_1 :::"Relation-like"::: ) "X" ($#v4_relat_1 :::"-defined"::: ) (Set ($#k3_numbers :::"RAT"::: ) ) ($#v5_relat_1 :::"-valued"::: ) ($#v1_funct_1 :::"Function-like"::: ) ($#v1_partfun1 :::"total"::: ) ($#v1_valued_0 :::"complex-valued"::: ) ($#v2_valued_0 :::"ext-real-valued"::: ) ($#v3_valued_0 :::"real-valued"::: ) ($#v4_valued_0 :::"natural-valued"::: ) for ($#m1_hidden :::"set"::: ) ; end; registrationlet "X" be ($#m1_hidden :::"set"::: ) ; let "f" be (Set (Const "X")) ($#v4_relat_1 :::"-defined"::: ) ($#v1_partfun1 :::"total"::: ) ($#v1_valued_0 :::"complex-valued"::: ) ($#m1_hidden :::"Function":::); cluster (Set ($#k30_valued_1 :::"-"::: ) "f") -> ($#v1_partfun1 :::"total"::: ) ($#v1_valued_0 :::"complex-valued"::: ) ; cluster (Set "f" ($#k35_valued_1 :::"""::: ) ) -> ($#v1_partfun1 :::"total"::: ) ($#v1_valued_0 :::"complex-valued"::: ) ; cluster (Set "f" ($#k39_valued_1 :::"^2"::: ) ) -> ($#v1_partfun1 :::"total"::: ) ; cluster (Set ($#k54_valued_1 :::"|."::: ) "f" ($#k54_valued_1 :::".|"::: ) ) -> ($#v1_partfun1 :::"total"::: ) ($#v3_valued_0 :::"real-valued"::: ) ; end; registrationlet "X" be ($#m1_hidden :::"set"::: ) ; let "f" be (Set (Const "X")) ($#v4_relat_1 :::"-defined"::: ) ($#v1_valued_0 :::"complex-valued"::: ) ($#m1_hidden :::"Function":::); let "r" be ($#v1_xcmplx_0 :::"complex"::: ) ($#m1_hidden :::"number"::: ) ; cluster (Set "r" ($#k7_valued_1 :::"+"::: ) "f") -> "X" ($#v4_relat_1 :::"-defined"::: ) ; cluster (Set "f" ($#k13_valued_1 :::"-"::: ) "r") -> "X" ($#v4_relat_1 :::"-defined"::: ) ; cluster (Set "r" ($#k24_valued_1 :::"(#)"::: ) "f") -> "X" ($#v4_relat_1 :::"-defined"::: ) ; end; registrationlet "X" be ($#m1_hidden :::"set"::: ) ; let "f" be (Set (Const "X")) ($#v4_relat_1 :::"-defined"::: ) ($#v1_partfun1 :::"total"::: ) ($#v1_valued_0 :::"complex-valued"::: ) ($#m1_hidden :::"Function":::); let "r" be ($#v1_xcmplx_0 :::"complex"::: ) ($#m1_hidden :::"number"::: ) ; cluster (Set "r" ($#k7_valued_1 :::"+"::: ) "f") -> ($#v1_partfun1 :::"total"::: ) ; cluster (Set "f" ($#k13_valued_1 :::"-"::: ) "r") -> ($#v1_partfun1 :::"total"::: ) ; cluster (Set "r" ($#k24_valued_1 :::"(#)"::: ) "f") -> ($#v1_partfun1 :::"total"::: ) ; end; registrationlet "X" be ($#m1_hidden :::"set"::: ) ; let "f1" be ($#v1_valued_0 :::"complex-valued"::: ) ($#m1_hidden :::"Function":::); let "f2" be (Set (Const "X")) ($#v4_relat_1 :::"-defined"::: ) ($#v1_valued_0 :::"complex-valued"::: ) ($#m1_hidden :::"Function":::); cluster (Set "f1" ($#k1_valued_1 :::"+"::: ) "f2") -> "X" ($#v4_relat_1 :::"-defined"::: ) ; cluster (Set "f1" ($#k45_valued_1 :::"-"::: ) "f2") -> "X" ($#v4_relat_1 :::"-defined"::: ) ; cluster (Set "f1" ($#k18_valued_1 :::"(#)"::: ) "f2") -> "X" ($#v4_relat_1 :::"-defined"::: ) ; cluster (Set "f1" ($#k50_valued_1 :::"/""::: ) "f2") -> "X" ($#v4_relat_1 :::"-defined"::: ) ; end; registrationlet "X" be ($#m1_hidden :::"set"::: ) ; let "f1", "f2" be (Set (Const "X")) ($#v4_relat_1 :::"-defined"::: ) ($#v1_partfun1 :::"total"::: ) ($#v1_valued_0 :::"complex-valued"::: ) ($#m1_hidden :::"Function":::); cluster (Set "f1" ($#k1_valued_1 :::"+"::: ) "f2") -> ($#v1_partfun1 :::"total"::: ) ; cluster (Set "f1" ($#k45_valued_1 :::"-"::: ) "f2") -> ($#v1_partfun1 :::"total"::: ) ; cluster (Set "f1" ($#k18_valued_1 :::"(#)"::: ) "f2") -> ($#v1_partfun1 :::"total"::: ) ; cluster (Set "f1" ($#k50_valued_1 :::"/""::: ) "f2") -> ($#v1_partfun1 :::"total"::: ) ; end; registrationlet "X" be ($#~v1_xboole_0 "non" ($#v1_xboole_0 :::"empty"::: ) ) ($#m1_hidden :::"set"::: ) ; let "F" be (Set ($#k5_numbers :::"NAT"::: ) ) ($#v4_relat_1 :::"-defined"::: ) (Set (Const "X")) ($#v5_relat_1 :::"-valued"::: ) ($#~v1_xboole_0 "non" ($#v1_xboole_0 :::"empty"::: ) ) ($#v1_finset_1 :::"finite"::: ) ($#m1_hidden :::"Function":::); cluster (Set ($#k63_valued_1 :::"CutLastLoc"::: ) "F") -> "X" ($#v5_relat_1 :::"-valued"::: ) ; end; theorem :: VALUED_1:39 (Bool "for" (Set (Var "f")) "being" ($#m1_hidden :::"Function":::) (Bool "for" (Set (Var "i")) "," (Set (Var "n")) "being" ($#m1_hidden :::"Nat":::) "st" (Bool (Bool (Set (Var "i")) ($#r2_hidden :::"in"::: ) (Set ($#k1_relset_1 :::"dom"::: ) (Set "(" ($#k61_valued_1 :::"Shift"::: ) "(" (Set (Var "f")) "," (Set (Var "n")) ")" ")" )))) "holds" (Bool "ex" (Set (Var "j")) "being" ($#m1_hidden :::"Nat":::) "st" (Bool "(" (Bool (Set (Var "j")) ($#r2_hidden :::"in"::: ) (Set ($#k9_xtuple_0 :::"dom"::: ) (Set (Var "f")))) & (Bool (Set (Var "i")) ($#r1_hidden :::"="::: ) (Set (Set (Var "j")) ($#k2_xcmplx_0 :::"+"::: ) (Set (Var "n")))) ")" )))) ;