:: RFUNCT_3 semantic presentation begin definitionlet "r" be ($#v1_xreal_0 :::"real"::: ) ($#m1_hidden :::"number"::: ) ; func :::"max+"::: "r" -> ($#m1_subset_1 :::"Real":::) equals :: RFUNCT_3:def 1 (Set ($#k4_xxreal_0 :::"max"::: ) "(" "r" "," (Set ($#k6_numbers :::"0"::: ) ) ")" ); func :::"max-"::: "r" -> ($#m1_subset_1 :::"Real":::) equals :: RFUNCT_3:def 2 (Set ($#k4_xxreal_0 :::"max"::: ) "(" (Set "(" ($#k4_xcmplx_0 :::"-"::: ) "r" ")" ) "," (Set ($#k6_numbers :::"0"::: ) ) ")" ); end; :: deftheorem defines :::"max+"::: RFUNCT_3:def 1 : (Bool "for" (Set (Var "r")) "being" ($#v1_xreal_0 :::"real"::: ) ($#m1_hidden :::"number"::: ) "holds" (Bool (Set ($#k1_rfunct_3 :::"max+"::: ) (Set (Var "r"))) ($#r1_hidden :::"="::: ) (Set ($#k4_xxreal_0 :::"max"::: ) "(" (Set (Var "r")) "," (Set ($#k6_numbers :::"0"::: ) ) ")" ))); :: deftheorem defines :::"max-"::: RFUNCT_3:def 2 : (Bool "for" (Set (Var "r")) "being" ($#v1_xreal_0 :::"real"::: ) ($#m1_hidden :::"number"::: ) "holds" (Bool (Set ($#k2_rfunct_3 :::"max-"::: ) (Set (Var "r"))) ($#r1_hidden :::"="::: ) (Set ($#k4_xxreal_0 :::"max"::: ) "(" (Set "(" ($#k4_xcmplx_0 :::"-"::: ) (Set (Var "r")) ")" ) "," (Set ($#k6_numbers :::"0"::: ) ) ")" ))); theorem :: RFUNCT_3:1 (Bool "for" (Set (Var "r")) "being" ($#v1_xreal_0 :::"real"::: ) ($#m1_hidden :::"number"::: ) "holds" (Bool (Set (Var "r")) ($#r1_hidden :::"="::: ) (Set (Set "(" ($#k1_rfunct_3 :::"max+"::: ) (Set (Var "r")) ")" ) ($#k9_real_1 :::"-"::: ) (Set "(" ($#k2_rfunct_3 :::"max-"::: ) (Set (Var "r")) ")" )))) ; theorem :: RFUNCT_3:2 (Bool "for" (Set (Var "r")) "being" ($#v1_xreal_0 :::"real"::: ) ($#m1_hidden :::"number"::: ) "holds" (Bool (Set ($#k18_complex1 :::"abs"::: ) (Set (Var "r"))) ($#r1_hidden :::"="::: ) (Set (Set "(" ($#k1_rfunct_3 :::"max+"::: ) (Set (Var "r")) ")" ) ($#k7_real_1 :::"+"::: ) (Set "(" ($#k2_rfunct_3 :::"max-"::: ) (Set (Var "r")) ")" )))) ; theorem :: RFUNCT_3:3 (Bool "for" (Set (Var "r")) "being" ($#v1_xreal_0 :::"real"::: ) ($#m1_hidden :::"number"::: ) "holds" (Bool (Set (Num 2) ($#k8_real_1 :::"*"::: ) (Set "(" ($#k1_rfunct_3 :::"max+"::: ) (Set (Var "r")) ")" )) ($#r1_hidden :::"="::: ) (Set (Set (Var "r")) ($#k3_real_1 :::"+"::: ) (Set "(" ($#k18_complex1 :::"abs"::: ) (Set (Var "r")) ")" )))) ; theorem :: RFUNCT_3:4 (Bool "for" (Set (Var "r")) "," (Set (Var "s")) "being" ($#v1_xreal_0 :::"real"::: ) ($#m1_hidden :::"number"::: ) "st" (Bool (Bool (Set ($#k6_numbers :::"0"::: ) ) ($#r1_xxreal_0 :::"<="::: ) (Set (Var "r")))) "holds" (Bool (Set ($#k1_rfunct_3 :::"max+"::: ) (Set "(" (Set (Var "r")) ($#k3_xcmplx_0 :::"*"::: ) (Set (Var "s")) ")" )) ($#r1_hidden :::"="::: ) (Set (Set (Var "r")) ($#k4_real_1 :::"*"::: ) (Set "(" ($#k1_rfunct_3 :::"max+"::: ) (Set (Var "s")) ")" )))) ; theorem :: RFUNCT_3:5 (Bool "for" (Set (Var "r")) "," (Set (Var "s")) "being" ($#v1_xreal_0 :::"real"::: ) ($#m1_hidden :::"number"::: ) "holds" (Bool (Set ($#k1_rfunct_3 :::"max+"::: ) (Set "(" (Set (Var "r")) ($#k2_xcmplx_0 :::"+"::: ) (Set (Var "s")) ")" )) ($#r1_xxreal_0 :::"<="::: ) (Set (Set "(" ($#k1_rfunct_3 :::"max+"::: ) (Set (Var "r")) ")" ) ($#k7_real_1 :::"+"::: ) (Set "(" ($#k1_rfunct_3 :::"max+"::: ) (Set (Var "s")) ")" )))) ; begin theorem :: RFUNCT_3:6 (Bool "for" (Set (Var "D")) "being" ($#~v1_xboole_0 "non" ($#v1_xboole_0 :::"empty"::: ) ) ($#m1_hidden :::"set"::: ) (Bool "for" (Set (Var "F")) "being" ($#m1_subset_1 :::"PartFunc":::) "of" (Set (Var "D")) "," (Set ($#k1_numbers :::"REAL"::: ) ) (Bool "for" (Set (Var "r")) "," (Set (Var "s")) "being" ($#v1_xreal_0 :::"real"::: ) ($#m1_hidden :::"number"::: ) "st" (Bool (Bool (Set (Var "r")) ($#r1_hidden :::"<>"::: ) (Set ($#k6_numbers :::"0"::: ) ))) "holds" (Bool (Set (Set (Var "F")) ($#k8_relset_1 :::"""::: ) (Set ($#k1_tarski :::"{"::: ) (Set "(" (Set (Var "s")) ($#k13_complex1 :::"/"::: ) (Set (Var "r")) ")" ) ($#k1_tarski :::"}"::: ) )) ($#r1_hidden :::"="::: ) (Set (Set "(" (Set (Var "r")) ($#k26_valued_1 :::"(#)"::: ) (Set (Var "F")) ")" ) ($#k8_relset_1 :::"""::: ) (Set ($#k1_tarski :::"{"::: ) (Set (Var "s")) ($#k1_tarski :::"}"::: ) )))))) ; theorem :: RFUNCT_3:7 (Bool "for" (Set (Var "D")) "being" ($#~v1_xboole_0 "non" ($#v1_xboole_0 :::"empty"::: ) ) ($#m1_hidden :::"set"::: ) (Bool "for" (Set (Var "F")) "being" ($#m1_subset_1 :::"PartFunc":::) "of" (Set (Var "D")) "," (Set ($#k1_numbers :::"REAL"::: ) ) "holds" (Bool (Set (Set "(" (Set ($#k6_numbers :::"0"::: ) ) ($#k26_valued_1 :::"(#)"::: ) (Set (Var "F")) ")" ) ($#k8_relset_1 :::"""::: ) (Set ($#k1_tarski :::"{"::: ) (Set ($#k6_numbers :::"0"::: ) ) ($#k1_tarski :::"}"::: ) )) ($#r1_hidden :::"="::: ) (Set ($#k1_relset_1 :::"dom"::: ) (Set (Var "F")))))) ; theorem :: RFUNCT_3:8 (Bool "for" (Set (Var "D")) "being" ($#~v1_xboole_0 "non" ($#v1_xboole_0 :::"empty"::: ) ) ($#m1_hidden :::"set"::: ) (Bool "for" (Set (Var "F")) "being" ($#m1_subset_1 :::"PartFunc":::) "of" (Set (Var "D")) "," (Set ($#k1_numbers :::"REAL"::: ) ) (Bool "for" (Set (Var "r")) "being" ($#m1_subset_1 :::"Real":::) "st" (Bool (Bool (Set ($#k6_numbers :::"0"::: ) ) ($#r1_xxreal_0 :::"<"::: ) (Set (Var "r")))) "holds" (Bool (Set (Set "(" ($#k56_valued_1 :::"abs"::: ) (Set (Var "F")) ")" ) ($#k8_relset_1 :::"""::: ) (Set ($#k1_tarski :::"{"::: ) (Set (Var "r")) ($#k1_tarski :::"}"::: ) )) ($#r1_hidden :::"="::: ) (Set (Set (Var "F")) ($#k8_relset_1 :::"""::: ) (Set ($#k2_tarski :::"{"::: ) (Set "(" ($#k1_real_1 :::"-"::: ) (Set (Var "r")) ")" ) "," (Set (Var "r")) ($#k2_tarski :::"}"::: ) )))))) ; theorem :: RFUNCT_3:9 (Bool "for" (Set (Var "D")) "being" ($#~v1_xboole_0 "non" ($#v1_xboole_0 :::"empty"::: ) ) ($#m1_hidden :::"set"::: ) (Bool "for" (Set (Var "F")) "being" ($#m1_subset_1 :::"PartFunc":::) "of" (Set (Var "D")) "," (Set ($#k1_numbers :::"REAL"::: ) ) "holds" (Bool (Set (Set "(" ($#k56_valued_1 :::"abs"::: ) (Set (Var "F")) ")" ) ($#k8_relset_1 :::"""::: ) (Set ($#k1_tarski :::"{"::: ) (Set ($#k6_numbers :::"0"::: ) ) ($#k1_tarski :::"}"::: ) )) ($#r1_hidden :::"="::: ) (Set (Set (Var "F")) ($#k8_relset_1 :::"""::: ) (Set ($#k1_tarski :::"{"::: ) (Set ($#k6_numbers :::"0"::: ) ) ($#k1_tarski :::"}"::: ) ))))) ; theorem :: RFUNCT_3:10 (Bool "for" (Set (Var "D")) "being" ($#~v1_xboole_0 "non" ($#v1_xboole_0 :::"empty"::: ) ) ($#m1_hidden :::"set"::: ) (Bool "for" (Set (Var "F")) "being" ($#m1_subset_1 :::"PartFunc":::) "of" (Set (Var "D")) "," (Set ($#k1_numbers :::"REAL"::: ) ) (Bool "for" (Set (Var "r")) "being" ($#m1_subset_1 :::"Real":::) "st" (Bool (Bool (Set (Var "r")) ($#r1_xxreal_0 :::"<"::: ) (Set ($#k6_numbers :::"0"::: ) ))) "holds" (Bool (Set (Set "(" ($#k56_valued_1 :::"abs"::: ) (Set (Var "F")) ")" ) ($#k8_relset_1 :::"""::: ) (Set ($#k1_tarski :::"{"::: ) (Set (Var "r")) ($#k1_tarski :::"}"::: ) )) ($#r1_hidden :::"="::: ) (Set ($#k1_xboole_0 :::"{}"::: ) ))))) ; theorem :: RFUNCT_3:11 (Bool "for" (Set (Var "D")) "," (Set (Var "C")) "being" ($#~v1_xboole_0 "non" ($#v1_xboole_0 :::"empty"::: ) ) ($#m1_hidden :::"set"::: ) (Bool "for" (Set (Var "F")) "being" ($#m1_subset_1 :::"PartFunc":::) "of" (Set (Var "D")) "," (Set ($#k1_numbers :::"REAL"::: ) ) (Bool "for" (Set (Var "G")) "being" ($#m1_subset_1 :::"PartFunc":::) "of" (Set (Var "C")) "," (Set ($#k1_numbers :::"REAL"::: ) ) (Bool "for" (Set (Var "r")) "being" ($#m1_subset_1 :::"Real":::) "st" (Bool (Bool (Set (Var "r")) ($#r1_hidden :::"<>"::: ) (Set ($#k6_numbers :::"0"::: ) ))) "holds" (Bool "(" (Bool (Set (Var "F")) "," (Set (Var "G")) ($#r2_classes1 :::"are_fiberwise_equipotent"::: ) ) "iff" (Bool (Set (Set (Var "r")) ($#k26_valued_1 :::"(#)"::: ) (Set (Var "F"))) "," (Set (Set (Var "r")) ($#k26_valued_1 :::"(#)"::: ) (Set (Var "G"))) ($#r2_classes1 :::"are_fiberwise_equipotent"::: ) ) ")" ))))) ; theorem :: RFUNCT_3:12 (Bool "for" (Set (Var "D")) "," (Set (Var "C")) "being" ($#~v1_xboole_0 "non" ($#v1_xboole_0 :::"empty"::: ) ) ($#m1_hidden :::"set"::: ) (Bool "for" (Set (Var "F")) "being" ($#m1_subset_1 :::"PartFunc":::) "of" (Set (Var "D")) "," (Set ($#k1_numbers :::"REAL"::: ) ) (Bool "for" (Set (Var "G")) "being" ($#m1_subset_1 :::"PartFunc":::) "of" (Set (Var "C")) "," (Set ($#k1_numbers :::"REAL"::: ) ) "holds" (Bool "(" (Bool (Set (Var "F")) "," (Set (Var "G")) ($#r2_classes1 :::"are_fiberwise_equipotent"::: ) ) "iff" (Bool (Set ($#k32_valued_1 :::"-"::: ) (Set (Var "F"))) "," (Set ($#k32_valued_1 :::"-"::: ) (Set (Var "G"))) ($#r2_classes1 :::"are_fiberwise_equipotent"::: ) ) ")" )))) ; theorem :: RFUNCT_3:13 (Bool "for" (Set (Var "D")) "," (Set (Var "C")) "being" ($#~v1_xboole_0 "non" ($#v1_xboole_0 :::"empty"::: ) ) ($#m1_hidden :::"set"::: ) (Bool "for" (Set (Var "F")) "being" ($#m1_subset_1 :::"PartFunc":::) "of" (Set (Var "D")) "," (Set ($#k1_numbers :::"REAL"::: ) ) (Bool "for" (Set (Var "G")) "being" ($#m1_subset_1 :::"PartFunc":::) "of" (Set (Var "C")) "," (Set ($#k1_numbers :::"REAL"::: ) ) "st" (Bool (Bool (Set (Var "F")) "," (Set (Var "G")) ($#r2_classes1 :::"are_fiberwise_equipotent"::: ) )) "holds" (Bool (Set ($#k56_valued_1 :::"abs"::: ) (Set (Var "F"))) "," (Set ($#k56_valued_1 :::"abs"::: ) (Set (Var "G"))) ($#r2_classes1 :::"are_fiberwise_equipotent"::: ) )))) ; definitionlet "X", "Y" be ($#m1_hidden :::"set"::: ) ; mode :::"PartFunc-set"::: "of" "X" "," "Y" -> ($#m1_hidden :::"set"::: ) means :: RFUNCT_3:def 3 (Bool "for" (Set (Var "x")) "being" ($#m1_subset_1 :::"Element"::: ) "of" it "holds" (Bool (Set (Var "x")) "is" ($#m1_subset_1 :::"PartFunc":::) "of" "X" "," "Y")); end; :: deftheorem defines :::"PartFunc-set"::: RFUNCT_3:def 3 : (Bool "for" (Set (Var "X")) "," (Set (Var "Y")) "being" ($#m1_hidden :::"set"::: ) (Bool "for" (Set (Var "b3")) "being" ($#m1_hidden :::"set"::: ) "holds" (Bool "(" (Bool (Set (Var "b3")) "is" ($#m1_rfunct_3 :::"PartFunc-set"::: ) "of" (Set (Var "X")) "," (Set (Var "Y"))) "iff" (Bool "for" (Set (Var "x")) "being" ($#m1_subset_1 :::"Element"::: ) "of" (Set (Var "b3")) "holds" (Bool (Set (Var "x")) "is" ($#m1_subset_1 :::"PartFunc":::) "of" (Set (Var "X")) "," (Set (Var "Y")))) ")" ))); registrationlet "X", "Y" be ($#m1_hidden :::"set"::: ) ; cluster ($#~v1_xboole_0 "non" ($#v1_xboole_0 :::"empty"::: ) ) for ($#m1_rfunct_3 :::"PartFunc-set"::: ) "of" "X" "," "Y"; end; definitionlet "X", "Y" be ($#m1_hidden :::"set"::: ) ; mode PFUNC_DOMAIN of "X" "," "Y" is ($#~v1_xboole_0 "non" ($#v1_xboole_0 :::"empty"::: ) ) ($#m1_rfunct_3 :::"PartFunc-set"::: ) "of" "X" "," "Y"; end; definitionlet "X", "Y" be ($#m1_hidden :::"set"::: ) ; :: original: :::"PFuncs"::: redefine func :::"PFuncs"::: "(" "X" "," "Y" ")" -> ($#m1_rfunct_3 :::"PartFunc-set"::: ) "of" "X" "," "Y"; let "P" be ($#~v1_xboole_0 "non" ($#v1_xboole_0 :::"empty"::: ) ) ($#m1_rfunct_3 :::"PartFunc-set"::: ) "of" (Set (Const "X")) "," (Set (Const "Y")); :: original: :::"Element"::: redefine mode :::"Element"::: "of" "P" -> ($#m1_subset_1 :::"PartFunc":::) "of" "X" "," "Y"; end; definitionlet "D", "C" be ($#~v1_xboole_0 "non" ($#v1_xboole_0 :::"empty"::: ) ) ($#m1_hidden :::"set"::: ) ; let "X" be ($#m1_subset_1 :::"Subset":::) "of" (Set (Const "D")); let "c" be ($#m1_subset_1 :::"Element"::: ) "of" (Set (Const "C")); :: original: :::"-->"::: redefine func "X" :::"-->"::: "c" -> ($#m2_rfunct_3 :::"Element"::: ) "of" (Set ($#k3_rfunct_3 :::"PFuncs"::: ) "(" "D" "," "C" ")" ); end; registrationlet "D" be ($#~v1_xboole_0 "non" ($#v1_xboole_0 :::"empty"::: ) ) ($#m1_hidden :::"set"::: ) ; let "E" be ($#v3_membered :::"real-membered"::: ) ($#m1_hidden :::"set"::: ) ; cluster -> ($#v3_valued_0 :::"real-valued"::: ) for ($#m1_subset_1 :::"Element"::: ) "of" (Set ($#k3_rfunct_3 :::"PFuncs"::: ) "(" "D" "," "E" ")" ); end; definitionlet "D" be ($#~v1_xboole_0 "non" ($#v1_xboole_0 :::"empty"::: ) ) ($#m1_hidden :::"set"::: ) ; let "E" be ($#v3_membered :::"real-membered"::: ) ($#m1_hidden :::"set"::: ) ; let "F1", "F2" be ($#m2_rfunct_3 :::"Element"::: ) "of" (Set ($#k3_rfunct_3 :::"PFuncs"::: ) "(" (Set (Const "D")) "," (Set (Const "E")) ")" ); :: original: :::"+"::: redefine func "F1" :::"+"::: "F2" -> ($#m2_rfunct_3 :::"Element"::: ) "of" (Set ($#k3_rfunct_3 :::"PFuncs"::: ) "(" "D" "," (Set ($#k1_numbers :::"REAL"::: ) ) ")" ); :: original: :::"-"::: redefine func "F1" :::"-"::: "F2" -> ($#m2_rfunct_3 :::"Element"::: ) "of" (Set ($#k3_rfunct_3 :::"PFuncs"::: ) "(" "D" "," (Set ($#k1_numbers :::"REAL"::: ) ) ")" ); :: original: :::"(#)"::: redefine func "F1" :::"(#)"::: "F2" -> ($#m2_rfunct_3 :::"Element"::: ) "of" (Set ($#k3_rfunct_3 :::"PFuncs"::: ) "(" "D" "," (Set ($#k1_numbers :::"REAL"::: ) ) ")" ); :: original: :::"/"::: redefine func "F1" :::"/"::: "F2" -> ($#m2_rfunct_3 :::"Element"::: ) "of" (Set ($#k3_rfunct_3 :::"PFuncs"::: ) "(" "D" "," (Set ($#k1_numbers :::"REAL"::: ) ) ")" ); end; definitionlet "D" be ($#~v1_xboole_0 "non" ($#v1_xboole_0 :::"empty"::: ) ) ($#m1_hidden :::"set"::: ) ; let "E" be ($#v3_membered :::"real-membered"::: ) ($#m1_hidden :::"set"::: ) ; let "F" be ($#m2_rfunct_3 :::"Element"::: ) "of" (Set ($#k3_rfunct_3 :::"PFuncs"::: ) "(" (Set (Const "D")) "," (Set (Const "E")) ")" ); :: original: :::"|."::: redefine func :::"abs"::: "F" -> ($#m2_rfunct_3 :::"Element"::: ) "of" (Set ($#k3_rfunct_3 :::"PFuncs"::: ) "(" "D" "," (Set ($#k1_numbers :::"REAL"::: ) ) ")" ); :: original: :::"-"::: redefine func :::"-"::: "F" -> ($#m2_rfunct_3 :::"Element"::: ) "of" (Set ($#k3_rfunct_3 :::"PFuncs"::: ) "(" "D" "," (Set ($#k1_numbers :::"REAL"::: ) ) ")" ); :: original: :::"^"::: redefine func "F" :::"^"::: -> ($#m2_rfunct_3 :::"Element"::: ) "of" (Set ($#k3_rfunct_3 :::"PFuncs"::: ) "(" "D" "," (Set ($#k1_numbers :::"REAL"::: ) ) ")" ); end; definitionlet "D" be ($#~v1_xboole_0 "non" ($#v1_xboole_0 :::"empty"::: ) ) ($#m1_hidden :::"set"::: ) ; let "E" be ($#v3_membered :::"real-membered"::: ) ($#m1_hidden :::"set"::: ) ; let "F" be ($#m2_rfunct_3 :::"Element"::: ) "of" (Set ($#k3_rfunct_3 :::"PFuncs"::: ) "(" (Set (Const "D")) "," (Set (Const "E")) ")" ); let "r" be ($#v1_xreal_0 :::"real"::: ) ($#m1_hidden :::"number"::: ) ; :: original: :::"(#)"::: redefine func "r" :::"(#)"::: "F" -> ($#m2_rfunct_3 :::"Element"::: ) "of" (Set ($#k3_rfunct_3 :::"PFuncs"::: ) "(" "D" "," (Set ($#k1_numbers :::"REAL"::: ) ) ")" ); end; definitionlet "D" be ($#~v1_xboole_0 "non" ($#v1_xboole_0 :::"empty"::: ) ) ($#m1_hidden :::"set"::: ) ; func :::"addpfunc"::: "D" -> ($#m1_subset_1 :::"BinOp":::) "of" (Set "(" ($#k3_rfunct_3 :::"PFuncs"::: ) "(" "D" "," (Set ($#k1_numbers :::"REAL"::: ) ) ")" ")" ) means :: RFUNCT_3:def 4 (Bool "for" (Set (Var "F1")) "," (Set (Var "F2")) "being" ($#m2_rfunct_3 :::"Element"::: ) "of" (Set ($#k3_rfunct_3 :::"PFuncs"::: ) "(" "D" "," (Set ($#k1_numbers :::"REAL"::: ) ) ")" ) "holds" (Bool (Set it ($#k5_binop_1 :::"."::: ) "(" (Set (Var "F1")) "," (Set (Var "F2")) ")" ) ($#r1_hidden :::"="::: ) (Set (Set (Var "F1")) ($#k5_rfunct_3 :::"+"::: ) (Set (Var "F2"))))); end; :: deftheorem defines :::"addpfunc"::: RFUNCT_3:def 4 : (Bool "for" (Set (Var "D")) "being" ($#~v1_xboole_0 "non" ($#v1_xboole_0 :::"empty"::: ) ) ($#m1_hidden :::"set"::: ) (Bool "for" (Set (Var "b2")) "being" ($#m1_subset_1 :::"BinOp":::) "of" (Set "(" ($#k3_rfunct_3 :::"PFuncs"::: ) "(" (Set (Var "D")) "," (Set ($#k1_numbers :::"REAL"::: ) ) ")" ")" ) "holds" (Bool "(" (Bool (Set (Var "b2")) ($#r1_hidden :::"="::: ) (Set ($#k13_rfunct_3 :::"addpfunc"::: ) (Set (Var "D")))) "iff" (Bool "for" (Set (Var "F1")) "," (Set (Var "F2")) "being" ($#m2_rfunct_3 :::"Element"::: ) "of" (Set ($#k3_rfunct_3 :::"PFuncs"::: ) "(" (Set (Var "D")) "," (Set ($#k1_numbers :::"REAL"::: ) ) ")" ) "holds" (Bool (Set (Set (Var "b2")) ($#k5_binop_1 :::"."::: ) "(" (Set (Var "F1")) "," (Set (Var "F2")) ")" ) ($#r1_hidden :::"="::: ) (Set (Set (Var "F1")) ($#k5_rfunct_3 :::"+"::: ) (Set (Var "F2"))))) ")" ))); theorem :: RFUNCT_3:14 (Bool "for" (Set (Var "D")) "being" ($#~v1_xboole_0 "non" ($#v1_xboole_0 :::"empty"::: ) ) ($#m1_hidden :::"set"::: ) "holds" (Bool (Set ($#k13_rfunct_3 :::"addpfunc"::: ) (Set (Var "D"))) "is" ($#v1_binop_1 :::"commutative"::: ) )) ; theorem :: RFUNCT_3:15 (Bool "for" (Set (Var "D")) "being" ($#~v1_xboole_0 "non" ($#v1_xboole_0 :::"empty"::: ) ) ($#m1_hidden :::"set"::: ) "holds" (Bool (Set ($#k13_rfunct_3 :::"addpfunc"::: ) (Set (Var "D"))) "is" ($#v2_binop_1 :::"associative"::: ) )) ; theorem :: RFUNCT_3:16 (Bool "for" (Set (Var "D")) "being" ($#~v1_xboole_0 "non" ($#v1_xboole_0 :::"empty"::: ) ) ($#m1_hidden :::"set"::: ) "holds" (Bool (Set (Set "(" ($#k2_subset_1 :::"[#]"::: ) (Set (Var "D")) ")" ) ($#k4_rfunct_3 :::"-->"::: ) (Set ($#k6_numbers :::"0"::: ) )) ($#r3_binop_1 :::"is_a_unity_wrt"::: ) (Set ($#k13_rfunct_3 :::"addpfunc"::: ) (Set (Var "D"))))) ; theorem :: RFUNCT_3:17 (Bool "for" (Set (Var "D")) "being" ($#~v1_xboole_0 "non" ($#v1_xboole_0 :::"empty"::: ) ) ($#m1_hidden :::"set"::: ) "holds" (Bool (Set ($#k4_binop_1 :::"the_unity_wrt"::: ) (Set "(" ($#k13_rfunct_3 :::"addpfunc"::: ) (Set (Var "D")) ")" )) ($#r1_hidden :::"="::: ) (Set (Set "(" ($#k2_subset_1 :::"[#]"::: ) (Set (Var "D")) ")" ) ($#k4_rfunct_3 :::"-->"::: ) (Set ($#k6_numbers :::"0"::: ) )))) ; theorem :: RFUNCT_3:18 (Bool "for" (Set (Var "D")) "being" ($#~v1_xboole_0 "non" ($#v1_xboole_0 :::"empty"::: ) ) ($#m1_hidden :::"set"::: ) "holds" (Bool (Set ($#k13_rfunct_3 :::"addpfunc"::: ) (Set (Var "D"))) "is" ($#v1_setwiseo :::"having_a_unity"::: ) )) ; definitionlet "D" be ($#~v1_xboole_0 "non" ($#v1_xboole_0 :::"empty"::: ) ) ($#m1_hidden :::"set"::: ) ; let "f" be ($#m2_finseq_1 :::"FinSequence"::: ) "of" (Set ($#k3_rfunct_3 :::"PFuncs"::: ) "(" (Set (Const "D")) "," (Set ($#k1_numbers :::"REAL"::: ) ) ")" ); func :::"Sum"::: "f" -> ($#m2_rfunct_3 :::"Element"::: ) "of" (Set ($#k3_rfunct_3 :::"PFuncs"::: ) "(" "D" "," (Set ($#k1_numbers :::"REAL"::: ) ) ")" ) equals :: RFUNCT_3:def 5 (Set (Set "(" ($#k13_rfunct_3 :::"addpfunc"::: ) "D" ")" ) ($#k1_finsop_1 :::"$$"::: ) "f"); end; :: deftheorem defines :::"Sum"::: RFUNCT_3:def 5 : (Bool "for" (Set (Var "D")) "being" ($#~v1_xboole_0 "non" ($#v1_xboole_0 :::"empty"::: ) ) ($#m1_hidden :::"set"::: ) (Bool "for" (Set (Var "f")) "being" ($#m2_finseq_1 :::"FinSequence"::: ) "of" (Set ($#k3_rfunct_3 :::"PFuncs"::: ) "(" (Set (Var "D")) "," (Set ($#k1_numbers :::"REAL"::: ) ) ")" ) "holds" (Bool (Set ($#k14_rfunct_3 :::"Sum"::: ) (Set (Var "f"))) ($#r1_hidden :::"="::: ) (Set (Set "(" ($#k13_rfunct_3 :::"addpfunc"::: ) (Set (Var "D")) ")" ) ($#k1_finsop_1 :::"$$"::: ) (Set (Var "f")))))); theorem :: RFUNCT_3:19 (Bool "for" (Set (Var "D")) "being" ($#~v1_xboole_0 "non" ($#v1_xboole_0 :::"empty"::: ) ) ($#m1_hidden :::"set"::: ) "holds" (Bool (Set ($#k14_rfunct_3 :::"Sum"::: ) (Set "(" ($#k6_finseq_1 :::"<*>"::: ) (Set "(" ($#k3_rfunct_3 :::"PFuncs"::: ) "(" (Set (Var "D")) "," (Set ($#k1_numbers :::"REAL"::: ) ) ")" ")" ) ")" )) ($#r2_relset_1 :::"="::: ) (Set (Set "(" ($#k2_subset_1 :::"[#]"::: ) (Set (Var "D")) ")" ) ($#k4_rfunct_3 :::"-->"::: ) (Set ($#k6_numbers :::"0"::: ) )))) ; theorem :: RFUNCT_3:20 (Bool "for" (Set (Var "D")) "being" ($#~v1_xboole_0 "non" ($#v1_xboole_0 :::"empty"::: ) ) ($#m1_hidden :::"set"::: ) (Bool "for" (Set (Var "f")) "being" ($#m2_finseq_1 :::"FinSequence"::: ) "of" (Set ($#k3_rfunct_3 :::"PFuncs"::: ) "(" (Set (Var "D")) "," (Set ($#k1_numbers :::"REAL"::: ) ) ")" ) (Bool "for" (Set (Var "G")) "being" ($#m2_rfunct_3 :::"Element"::: ) "of" (Set ($#k3_rfunct_3 :::"PFuncs"::: ) "(" (Set (Var "D")) "," (Set ($#k1_numbers :::"REAL"::: ) ) ")" ) "holds" (Bool (Set ($#k14_rfunct_3 :::"Sum"::: ) (Set "(" (Set (Var "f")) ($#k8_finseq_1 :::"^"::: ) (Set ($#k12_finseq_1 :::"<*"::: ) (Set (Var "G")) ($#k12_finseq_1 :::"*>"::: ) ) ")" )) ($#r2_relset_1 :::"="::: ) (Set (Set "(" ($#k14_rfunct_3 :::"Sum"::: ) (Set (Var "f")) ")" ) ($#k5_rfunct_3 :::"+"::: ) (Set (Var "G"))))))) ; theorem :: RFUNCT_3:21 (Bool "for" (Set (Var "D")) "being" ($#~v1_xboole_0 "non" ($#v1_xboole_0 :::"empty"::: ) ) ($#m1_hidden :::"set"::: ) (Bool "for" (Set (Var "f1")) "," (Set (Var "f2")) "being" ($#m2_finseq_1 :::"FinSequence"::: ) "of" (Set ($#k3_rfunct_3 :::"PFuncs"::: ) "(" (Set (Var "D")) "," (Set ($#k1_numbers :::"REAL"::: ) ) ")" ) "holds" (Bool (Set ($#k14_rfunct_3 :::"Sum"::: ) (Set "(" (Set (Var "f1")) ($#k8_finseq_1 :::"^"::: ) (Set (Var "f2")) ")" )) ($#r2_relset_1 :::"="::: ) (Set (Set "(" ($#k14_rfunct_3 :::"Sum"::: ) (Set (Var "f1")) ")" ) ($#k5_rfunct_3 :::"+"::: ) (Set "(" ($#k14_rfunct_3 :::"Sum"::: ) (Set (Var "f2")) ")" ))))) ; theorem :: RFUNCT_3:22 (Bool "for" (Set (Var "D")) "being" ($#~v1_xboole_0 "non" ($#v1_xboole_0 :::"empty"::: ) ) ($#m1_hidden :::"set"::: ) (Bool "for" (Set (Var "f")) "being" ($#m2_finseq_1 :::"FinSequence"::: ) "of" (Set ($#k3_rfunct_3 :::"PFuncs"::: ) "(" (Set (Var "D")) "," (Set ($#k1_numbers :::"REAL"::: ) ) ")" ) (Bool "for" (Set (Var "G")) "being" ($#m2_rfunct_3 :::"Element"::: ) "of" (Set ($#k3_rfunct_3 :::"PFuncs"::: ) "(" (Set (Var "D")) "," (Set ($#k1_numbers :::"REAL"::: ) ) ")" ) "holds" (Bool (Set ($#k14_rfunct_3 :::"Sum"::: ) (Set "(" (Set ($#k12_finseq_1 :::"<*"::: ) (Set (Var "G")) ($#k12_finseq_1 :::"*>"::: ) ) ($#k8_finseq_1 :::"^"::: ) (Set (Var "f")) ")" )) ($#r2_relset_1 :::"="::: ) (Set (Set (Var "G")) ($#k5_rfunct_3 :::"+"::: ) (Set "(" ($#k14_rfunct_3 :::"Sum"::: ) (Set (Var "f")) ")" )))))) ; theorem :: RFUNCT_3:23 (Bool "for" (Set (Var "D")) "being" ($#~v1_xboole_0 "non" ($#v1_xboole_0 :::"empty"::: ) ) ($#m1_hidden :::"set"::: ) (Bool "for" (Set (Var "G1")) "," (Set (Var "G2")) "being" ($#m2_rfunct_3 :::"Element"::: ) "of" (Set ($#k3_rfunct_3 :::"PFuncs"::: ) "(" (Set (Var "D")) "," (Set ($#k1_numbers :::"REAL"::: ) ) ")" ) "holds" (Bool (Set ($#k14_rfunct_3 :::"Sum"::: ) (Set ($#k2_finseq_4 :::"<*"::: ) (Set (Var "G1")) "," (Set (Var "G2")) ($#k2_finseq_4 :::"*>"::: ) )) ($#r2_relset_1 :::"="::: ) (Set (Set (Var "G1")) ($#k5_rfunct_3 :::"+"::: ) (Set (Var "G2")))))) ; theorem :: RFUNCT_3:24 (Bool "for" (Set (Var "D")) "being" ($#~v1_xboole_0 "non" ($#v1_xboole_0 :::"empty"::: ) ) ($#m1_hidden :::"set"::: ) (Bool "for" (Set (Var "G1")) "," (Set (Var "G2")) "," (Set (Var "G3")) "being" ($#m2_rfunct_3 :::"Element"::: ) "of" (Set ($#k3_rfunct_3 :::"PFuncs"::: ) "(" (Set (Var "D")) "," (Set ($#k1_numbers :::"REAL"::: ) ) ")" ) "holds" (Bool (Set ($#k14_rfunct_3 :::"Sum"::: ) (Set ($#k3_finseq_4 :::"<*"::: ) (Set (Var "G1")) "," (Set (Var "G2")) "," (Set (Var "G3")) ($#k3_finseq_4 :::"*>"::: ) )) ($#r2_relset_1 :::"="::: ) (Set (Set "(" (Set (Var "G1")) ($#k5_rfunct_3 :::"+"::: ) (Set (Var "G2")) ")" ) ($#k5_rfunct_3 :::"+"::: ) (Set (Var "G3")))))) ; theorem :: RFUNCT_3:25 (Bool "for" (Set (Var "D")) "being" ($#~v1_xboole_0 "non" ($#v1_xboole_0 :::"empty"::: ) ) ($#m1_hidden :::"set"::: ) (Bool "for" (Set (Var "f")) "," (Set (Var "g")) "being" ($#m2_finseq_1 :::"FinSequence"::: ) "of" (Set ($#k3_rfunct_3 :::"PFuncs"::: ) "(" (Set (Var "D")) "," (Set ($#k1_numbers :::"REAL"::: ) ) ")" ) "st" (Bool (Bool (Set (Var "f")) "," (Set (Var "g")) ($#r2_classes1 :::"are_fiberwise_equipotent"::: ) )) "holds" (Bool (Set ($#k14_rfunct_3 :::"Sum"::: ) (Set (Var "f"))) ($#r2_relset_1 :::"="::: ) (Set ($#k14_rfunct_3 :::"Sum"::: ) (Set (Var "g")))))) ; definitionlet "D" be ($#~v1_xboole_0 "non" ($#v1_xboole_0 :::"empty"::: ) ) ($#m1_hidden :::"set"::: ) ; let "f" be ($#m1_hidden :::"FinSequence":::); func :::"CHI"::: "(" "f" "," "D" ")" -> ($#m2_finseq_1 :::"FinSequence"::: ) "of" (Set ($#k3_rfunct_3 :::"PFuncs"::: ) "(" "D" "," (Set ($#k1_numbers :::"REAL"::: ) ) ")" ) means :: RFUNCT_3:def 6 (Bool "(" (Bool (Set ($#k3_finseq_1 :::"len"::: ) it) ($#r1_hidden :::"="::: ) (Set ($#k3_finseq_1 :::"len"::: ) "f")) & (Bool "(" "for" (Set (Var "n")) "being" ($#m1_subset_1 :::"Element"::: ) "of" (Set ($#k5_numbers :::"NAT"::: ) ) "st" (Bool (Bool (Set (Var "n")) ($#r2_hidden :::"in"::: ) (Set ($#k4_finseq_1 :::"dom"::: ) it))) "holds" (Bool (Set it ($#k1_funct_1 :::"."::: ) (Set (Var "n"))) ($#r1_hidden :::"="::: ) (Set ($#k7_rfunct_1 :::"chi"::: ) "(" (Set "(" "f" ($#k1_funct_1 :::"."::: ) (Set (Var "n")) ")" ) "," "D" ")" )) ")" ) ")" ); end; :: deftheorem defines :::"CHI"::: RFUNCT_3:def 6 : (Bool "for" (Set (Var "D")) "being" ($#~v1_xboole_0 "non" ($#v1_xboole_0 :::"empty"::: ) ) ($#m1_hidden :::"set"::: ) (Bool "for" (Set (Var "f")) "being" ($#m1_hidden :::"FinSequence":::) (Bool "for" (Set (Var "b3")) "being" ($#m2_finseq_1 :::"FinSequence"::: ) "of" (Set ($#k3_rfunct_3 :::"PFuncs"::: ) "(" (Set (Var "D")) "," (Set ($#k1_numbers :::"REAL"::: ) ) ")" ) "holds" (Bool "(" (Bool (Set (Var "b3")) ($#r1_hidden :::"="::: ) (Set ($#k15_rfunct_3 :::"CHI"::: ) "(" (Set (Var "f")) "," (Set (Var "D")) ")" )) "iff" (Bool "(" (Bool (Set ($#k3_finseq_1 :::"len"::: ) (Set (Var "b3"))) ($#r1_hidden :::"="::: ) (Set ($#k3_finseq_1 :::"len"::: ) (Set (Var "f")))) & (Bool "(" "for" (Set (Var "n")) "being" ($#m1_subset_1 :::"Element"::: ) "of" (Set ($#k5_numbers :::"NAT"::: ) ) "st" (Bool (Bool (Set (Var "n")) ($#r2_hidden :::"in"::: ) (Set ($#k4_finseq_1 :::"dom"::: ) (Set (Var "b3"))))) "holds" (Bool (Set (Set (Var "b3")) ($#k1_funct_1 :::"."::: ) (Set (Var "n"))) ($#r1_hidden :::"="::: ) (Set ($#k7_rfunct_1 :::"chi"::: ) "(" (Set "(" (Set (Var "f")) ($#k1_funct_1 :::"."::: ) (Set (Var "n")) ")" ) "," (Set (Var "D")) ")" )) ")" ) ")" ) ")" )))); definitionlet "D" be ($#~v1_xboole_0 "non" ($#v1_xboole_0 :::"empty"::: ) ) ($#m1_hidden :::"set"::: ) ; let "f" be ($#m2_finseq_1 :::"FinSequence"::: ) "of" (Set ($#k3_rfunct_3 :::"PFuncs"::: ) "(" (Set (Const "D")) "," (Set ($#k1_numbers :::"REAL"::: ) ) ")" ); let "R" be ($#m2_finseq_1 :::"FinSequence"::: ) "of" (Set ($#k1_numbers :::"REAL"::: ) ); func "R" :::"(#)"::: "f" -> ($#m2_finseq_1 :::"FinSequence"::: ) "of" (Set ($#k3_rfunct_3 :::"PFuncs"::: ) "(" "D" "," (Set ($#k1_numbers :::"REAL"::: ) ) ")" ) means :: RFUNCT_3:def 7 (Bool "(" (Bool (Set ($#k3_finseq_1 :::"len"::: ) it) ($#r1_hidden :::"="::: ) (Set ($#k6_nat_1 :::"min"::: ) "(" (Set "(" ($#k3_finseq_1 :::"len"::: ) "R" ")" ) "," (Set "(" ($#k3_finseq_1 :::"len"::: ) "f" ")" ) ")" )) & (Bool "(" "for" (Set (Var "n")) "being" ($#m1_subset_1 :::"Element"::: ) "of" (Set ($#k5_numbers :::"NAT"::: ) ) "st" (Bool (Bool (Set (Var "n")) ($#r2_hidden :::"in"::: ) (Set ($#k4_finseq_1 :::"dom"::: ) it))) "holds" (Bool "for" (Set (Var "F")) "being" ($#m1_subset_1 :::"PartFunc":::) "of" "D" "," (Set ($#k1_numbers :::"REAL"::: ) ) (Bool "for" (Set (Var "r")) "being" ($#m1_subset_1 :::"Real":::) "st" (Bool (Bool (Set (Var "r")) ($#r1_hidden :::"="::: ) (Set "R" ($#k1_seq_1 :::"."::: ) (Set (Var "n")))) & (Bool (Set (Var "F")) ($#r1_hidden :::"="::: ) (Set "f" ($#k1_funct_1 :::"."::: ) (Set (Var "n"))))) "holds" (Bool (Set it ($#k1_funct_1 :::"."::: ) (Set (Var "n"))) ($#r1_hidden :::"="::: ) (Set (Set (Var "r")) ($#k26_valued_1 :::"(#)"::: ) (Set (Var "F")))))) ")" ) ")" ); end; :: deftheorem defines :::"(#)"::: RFUNCT_3:def 7 : (Bool "for" (Set (Var "D")) "being" ($#~v1_xboole_0 "non" ($#v1_xboole_0 :::"empty"::: ) ) ($#m1_hidden :::"set"::: ) (Bool "for" (Set (Var "f")) "being" ($#m2_finseq_1 :::"FinSequence"::: ) "of" (Set ($#k3_rfunct_3 :::"PFuncs"::: ) "(" (Set (Var "D")) "," (Set ($#k1_numbers :::"REAL"::: ) ) ")" ) (Bool "for" (Set (Var "R")) "being" ($#m2_finseq_1 :::"FinSequence"::: ) "of" (Set ($#k1_numbers :::"REAL"::: ) ) (Bool "for" (Set (Var "b4")) "being" ($#m2_finseq_1 :::"FinSequence"::: ) "of" (Set ($#k3_rfunct_3 :::"PFuncs"::: ) "(" (Set (Var "D")) "," (Set ($#k1_numbers :::"REAL"::: ) ) ")" ) "holds" (Bool "(" (Bool (Set (Var "b4")) ($#r1_hidden :::"="::: ) (Set (Set (Var "R")) ($#k16_rfunct_3 :::"(#)"::: ) (Set (Var "f")))) "iff" (Bool "(" (Bool (Set ($#k3_finseq_1 :::"len"::: ) (Set (Var "b4"))) ($#r1_hidden :::"="::: ) (Set ($#k6_nat_1 :::"min"::: ) "(" (Set "(" ($#k3_finseq_1 :::"len"::: ) (Set (Var "R")) ")" ) "," (Set "(" ($#k3_finseq_1 :::"len"::: ) (Set (Var "f")) ")" ) ")" )) & (Bool "(" "for" (Set (Var "n")) "being" ($#m1_subset_1 :::"Element"::: ) "of" (Set ($#k5_numbers :::"NAT"::: ) ) "st" (Bool (Bool (Set (Var "n")) ($#r2_hidden :::"in"::: ) (Set ($#k4_finseq_1 :::"dom"::: ) (Set (Var "b4"))))) "holds" (Bool "for" (Set (Var "F")) "being" ($#m1_subset_1 :::"PartFunc":::) "of" (Set (Var "D")) "," (Set ($#k1_numbers :::"REAL"::: ) ) (Bool "for" (Set (Var "r")) "being" ($#m1_subset_1 :::"Real":::) "st" (Bool (Bool (Set (Var "r")) ($#r1_hidden :::"="::: ) (Set (Set (Var "R")) ($#k1_seq_1 :::"."::: ) (Set (Var "n")))) & (Bool (Set (Var "F")) ($#r1_hidden :::"="::: ) (Set (Set (Var "f")) ($#k1_funct_1 :::"."::: ) (Set (Var "n"))))) "holds" (Bool (Set (Set (Var "b4")) ($#k1_funct_1 :::"."::: ) (Set (Var "n"))) ($#r1_hidden :::"="::: ) (Set (Set (Var "r")) ($#k26_valued_1 :::"(#)"::: ) (Set (Var "F")))))) ")" ) ")" ) ")" ))))); definitionlet "D" be ($#~v1_xboole_0 "non" ($#v1_xboole_0 :::"empty"::: ) ) ($#m1_hidden :::"set"::: ) ; let "f" be ($#m2_finseq_1 :::"FinSequence"::: ) "of" (Set ($#k3_rfunct_3 :::"PFuncs"::: ) "(" (Set (Const "D")) "," (Set ($#k1_numbers :::"REAL"::: ) ) ")" ); let "d" be ($#m1_subset_1 :::"Element"::: ) "of" (Set (Const "D")); func "f" :::"#"::: "d" -> ($#m2_finseq_1 :::"FinSequence"::: ) "of" (Set ($#k1_numbers :::"REAL"::: ) ) means :: RFUNCT_3:def 8 (Bool "(" (Bool (Set ($#k3_finseq_1 :::"len"::: ) it) ($#r1_hidden :::"="::: ) (Set ($#k3_finseq_1 :::"len"::: ) "f")) & (Bool "(" "for" (Set (Var "n")) "being" ($#m1_subset_1 :::"Element"::: ) "of" (Set ($#k5_numbers :::"NAT"::: ) ) "st" (Bool (Bool (Set (Var "n")) ($#r2_hidden :::"in"::: ) (Set ($#k4_finseq_1 :::"dom"::: ) it))) "holds" (Bool (Set it ($#k1_seq_1 :::"."::: ) (Set (Var "n"))) ($#r1_hidden :::"="::: ) (Set (Set "(" "f" ($#k1_funct_1 :::"."::: ) (Set (Var "n")) ")" ) ($#k1_funct_1 :::"."::: ) "d")) ")" ) ")" ); end; :: deftheorem defines :::"#"::: RFUNCT_3:def 8 : (Bool "for" (Set (Var "D")) "being" ($#~v1_xboole_0 "non" ($#v1_xboole_0 :::"empty"::: ) ) ($#m1_hidden :::"set"::: ) (Bool "for" (Set (Var "f")) "being" ($#m2_finseq_1 :::"FinSequence"::: ) "of" (Set ($#k3_rfunct_3 :::"PFuncs"::: ) "(" (Set (Var "D")) "," (Set ($#k1_numbers :::"REAL"::: ) ) ")" ) (Bool "for" (Set (Var "d")) "being" ($#m1_subset_1 :::"Element"::: ) "of" (Set (Var "D")) (Bool "for" (Set (Var "b4")) "being" ($#m2_finseq_1 :::"FinSequence"::: ) "of" (Set ($#k1_numbers :::"REAL"::: ) ) "holds" (Bool "(" (Bool (Set (Var "b4")) ($#r1_hidden :::"="::: ) (Set (Set (Var "f")) ($#k17_rfunct_3 :::"#"::: ) (Set (Var "d")))) "iff" (Bool "(" (Bool (Set ($#k3_finseq_1 :::"len"::: ) (Set (Var "b4"))) ($#r1_hidden :::"="::: ) (Set ($#k3_finseq_1 :::"len"::: ) (Set (Var "f")))) & (Bool "(" "for" (Set (Var "n")) "being" ($#m1_subset_1 :::"Element"::: ) "of" (Set ($#k5_numbers :::"NAT"::: ) ) "st" (Bool (Bool (Set (Var "n")) ($#r2_hidden :::"in"::: ) (Set ($#k4_finseq_1 :::"dom"::: ) (Set (Var "b4"))))) "holds" (Bool (Set (Set (Var "b4")) ($#k1_seq_1 :::"."::: ) (Set (Var "n"))) ($#r1_hidden :::"="::: ) (Set (Set "(" (Set (Var "f")) ($#k1_funct_1 :::"."::: ) (Set (Var "n")) ")" ) ($#k1_funct_1 :::"."::: ) (Set (Var "d")))) ")" ) ")" ) ")" ))))); definitionlet "D", "C" be ($#~v1_xboole_0 "non" ($#v1_xboole_0 :::"empty"::: ) ) ($#m1_hidden :::"set"::: ) ; let "f" be ($#m2_finseq_1 :::"FinSequence"::: ) "of" (Set ($#k3_rfunct_3 :::"PFuncs"::: ) "(" (Set (Const "D")) "," (Set (Const "C")) ")" ); let "d" be ($#m1_subset_1 :::"Element"::: ) "of" (Set (Const "D")); pred "d" :::"is_common_for_dom"::: "f" means :: RFUNCT_3:def 9 (Bool "for" (Set (Var "n")) "being" ($#m1_subset_1 :::"Element"::: ) "of" (Set ($#k5_numbers :::"NAT"::: ) ) "st" (Bool (Bool (Set (Var "n")) ($#r2_hidden :::"in"::: ) (Set ($#k4_finseq_1 :::"dom"::: ) "f"))) "holds" (Bool "d" ($#r2_hidden :::"in"::: ) (Set ($#k9_xtuple_0 :::"dom"::: ) (Set "(" "f" ($#k1_funct_1 :::"."::: ) (Set (Var "n")) ")" )))); end; :: deftheorem defines :::"is_common_for_dom"::: RFUNCT_3:def 9 : (Bool "for" (Set (Var "D")) "," (Set (Var "C")) "being" ($#~v1_xboole_0 "non" ($#v1_xboole_0 :::"empty"::: ) ) ($#m1_hidden :::"set"::: ) (Bool "for" (Set (Var "f")) "being" ($#m2_finseq_1 :::"FinSequence"::: ) "of" (Set ($#k3_rfunct_3 :::"PFuncs"::: ) "(" (Set (Var "D")) "," (Set (Var "C")) ")" ) (Bool "for" (Set (Var "d")) "being" ($#m1_subset_1 :::"Element"::: ) "of" (Set (Var "D")) "holds" (Bool "(" (Bool (Set (Var "d")) ($#r1_rfunct_3 :::"is_common_for_dom"::: ) (Set (Var "f"))) "iff" (Bool "for" (Set (Var "n")) "being" ($#m1_subset_1 :::"Element"::: ) "of" (Set ($#k5_numbers :::"NAT"::: ) ) "st" (Bool (Bool (Set (Var "n")) ($#r2_hidden :::"in"::: ) (Set ($#k4_finseq_1 :::"dom"::: ) (Set (Var "f"))))) "holds" (Bool (Set (Var "d")) ($#r2_hidden :::"in"::: ) (Set ($#k9_xtuple_0 :::"dom"::: ) (Set "(" (Set (Var "f")) ($#k1_funct_1 :::"."::: ) (Set (Var "n")) ")" )))) ")" )))); theorem :: RFUNCT_3:26 (Bool "for" (Set (Var "D")) "," (Set (Var "C")) "being" ($#~v1_xboole_0 "non" ($#v1_xboole_0 :::"empty"::: ) ) ($#m1_hidden :::"set"::: ) (Bool "for" (Set (Var "f")) "being" ($#m2_finseq_1 :::"FinSequence"::: ) "of" (Set ($#k3_rfunct_3 :::"PFuncs"::: ) "(" (Set (Var "D")) "," (Set (Var "C")) ")" ) (Bool "for" (Set (Var "d")) "being" ($#m1_subset_1 :::"Element"::: ) "of" (Set (Var "D")) (Bool "for" (Set (Var "n")) "being" ($#m1_subset_1 :::"Element"::: ) "of" (Set ($#k5_numbers :::"NAT"::: ) ) "st" (Bool (Bool (Set (Var "d")) ($#r1_rfunct_3 :::"is_common_for_dom"::: ) (Set (Var "f"))) & (Bool (Set (Var "n")) ($#r1_hidden :::"<>"::: ) (Set ($#k6_numbers :::"0"::: ) ))) "holds" (Bool (Set (Var "d")) ($#r1_rfunct_3 :::"is_common_for_dom"::: ) (Set (Set (Var "f")) ($#k17_finseq_1 :::"|"::: ) (Set (Var "n")))))))) ; theorem :: RFUNCT_3:27 (Bool "for" (Set (Var "D")) "," (Set (Var "C")) "being" ($#~v1_xboole_0 "non" ($#v1_xboole_0 :::"empty"::: ) ) ($#m1_hidden :::"set"::: ) (Bool "for" (Set (Var "f")) "being" ($#m2_finseq_1 :::"FinSequence"::: ) "of" (Set ($#k3_rfunct_3 :::"PFuncs"::: ) "(" (Set (Var "D")) "," (Set (Var "C")) ")" ) (Bool "for" (Set (Var "d")) "being" ($#m1_subset_1 :::"Element"::: ) "of" (Set (Var "D")) (Bool "for" (Set (Var "n")) "being" ($#m1_subset_1 :::"Element"::: ) "of" (Set ($#k5_numbers :::"NAT"::: ) ) "st" (Bool (Bool (Set (Var "d")) ($#r1_rfunct_3 :::"is_common_for_dom"::: ) (Set (Var "f")))) "holds" (Bool (Set (Var "d")) ($#r1_rfunct_3 :::"is_common_for_dom"::: ) (Set (Set (Var "f")) ($#k2_rfinseq :::"/^"::: ) (Set (Var "n")))))))) ; theorem :: RFUNCT_3:28 (Bool "for" (Set (Var "D")) "being" ($#~v1_xboole_0 "non" ($#v1_xboole_0 :::"empty"::: ) ) ($#m1_hidden :::"set"::: ) (Bool "for" (Set (Var "d")) "being" ($#m1_subset_1 :::"Element"::: ) "of" (Set (Var "D")) (Bool "for" (Set (Var "f")) "being" ($#m2_finseq_1 :::"FinSequence"::: ) "of" (Set ($#k3_rfunct_3 :::"PFuncs"::: ) "(" (Set (Var "D")) "," (Set ($#k1_numbers :::"REAL"::: ) ) ")" ) "st" (Bool (Bool (Set ($#k3_finseq_1 :::"len"::: ) (Set (Var "f"))) ($#r1_hidden :::"<>"::: ) (Set ($#k6_numbers :::"0"::: ) ))) "holds" (Bool "(" (Bool (Set (Var "d")) ($#r1_rfunct_3 :::"is_common_for_dom"::: ) (Set (Var "f"))) "iff" (Bool (Set (Var "d")) ($#r2_hidden :::"in"::: ) (Set ($#k1_relset_1 :::"dom"::: ) (Set "(" ($#k14_rfunct_3 :::"Sum"::: ) (Set (Var "f")) ")" ))) ")" )))) ; theorem :: RFUNCT_3:29 (Bool "for" (Set (Var "D")) "being" ($#~v1_xboole_0 "non" ($#v1_xboole_0 :::"empty"::: ) ) ($#m1_hidden :::"set"::: ) (Bool "for" (Set (Var "f")) "being" ($#m2_finseq_1 :::"FinSequence"::: ) "of" (Set ($#k3_rfunct_3 :::"PFuncs"::: ) "(" (Set (Var "D")) "," (Set ($#k1_numbers :::"REAL"::: ) ) ")" ) (Bool "for" (Set (Var "d")) "being" ($#m1_subset_1 :::"Element"::: ) "of" (Set (Var "D")) (Bool "for" (Set (Var "n")) "being" ($#m1_subset_1 :::"Element"::: ) "of" (Set ($#k5_numbers :::"NAT"::: ) ) "holds" (Bool (Set (Set "(" (Set (Var "f")) ($#k17_finseq_1 :::"|"::: ) (Set (Var "n")) ")" ) ($#k17_rfunct_3 :::"#"::: ) (Set (Var "d"))) ($#r1_hidden :::"="::: ) (Set (Set "(" (Set (Var "f")) ($#k17_rfunct_3 :::"#"::: ) (Set (Var "d")) ")" ) ($#k17_finseq_1 :::"|"::: ) (Set (Var "n")))))))) ; theorem :: RFUNCT_3:30 (Bool "for" (Set (Var "D")) "being" ($#~v1_xboole_0 "non" ($#v1_xboole_0 :::"empty"::: ) ) ($#m1_hidden :::"set"::: ) (Bool "for" (Set (Var "f")) "being" ($#m1_hidden :::"FinSequence":::) (Bool "for" (Set (Var "d")) "being" ($#m1_subset_1 :::"Element"::: ) "of" (Set (Var "D")) "holds" (Bool (Set (Var "d")) ($#r1_rfunct_3 :::"is_common_for_dom"::: ) (Set ($#k15_rfunct_3 :::"CHI"::: ) "(" (Set (Var "f")) "," (Set (Var "D")) ")" ))))) ; theorem :: RFUNCT_3:31 (Bool "for" (Set (Var "D")) "being" ($#~v1_xboole_0 "non" ($#v1_xboole_0 :::"empty"::: ) ) ($#m1_hidden :::"set"::: ) (Bool "for" (Set (Var "d")) "being" ($#m1_subset_1 :::"Element"::: ) "of" (Set (Var "D")) (Bool "for" (Set (Var "f")) "being" ($#m2_finseq_1 :::"FinSequence"::: ) "of" (Set ($#k3_rfunct_3 :::"PFuncs"::: ) "(" (Set (Var "D")) "," (Set ($#k1_numbers :::"REAL"::: ) ) ")" ) (Bool "for" (Set (Var "R")) "being" ($#m2_finseq_1 :::"FinSequence"::: ) "of" (Set ($#k1_numbers :::"REAL"::: ) ) "st" (Bool (Bool (Set (Var "d")) ($#r1_rfunct_3 :::"is_common_for_dom"::: ) (Set (Var "f")))) "holds" (Bool (Set (Var "d")) ($#r1_rfunct_3 :::"is_common_for_dom"::: ) (Set (Set (Var "R")) ($#k16_rfunct_3 :::"(#)"::: ) (Set (Var "f")))))))) ; theorem :: RFUNCT_3:32 (Bool "for" (Set (Var "D")) "being" ($#~v1_xboole_0 "non" ($#v1_xboole_0 :::"empty"::: ) ) ($#m1_hidden :::"set"::: ) (Bool "for" (Set (Var "f")) "being" ($#m1_hidden :::"FinSequence":::) (Bool "for" (Set (Var "R")) "being" ($#m2_finseq_1 :::"FinSequence"::: ) "of" (Set ($#k1_numbers :::"REAL"::: ) ) (Bool "for" (Set (Var "d")) "being" ($#m1_subset_1 :::"Element"::: ) "of" (Set (Var "D")) "holds" (Bool (Set (Var "d")) ($#r1_rfunct_3 :::"is_common_for_dom"::: ) (Set (Set (Var "R")) ($#k16_rfunct_3 :::"(#)"::: ) (Set "(" ($#k15_rfunct_3 :::"CHI"::: ) "(" (Set (Var "f")) "," (Set (Var "D")) ")" ")" ))))))) ; theorem :: RFUNCT_3:33 (Bool "for" (Set (Var "D")) "being" ($#~v1_xboole_0 "non" ($#v1_xboole_0 :::"empty"::: ) ) ($#m1_hidden :::"set"::: ) (Bool "for" (Set (Var "d")) "being" ($#m1_subset_1 :::"Element"::: ) "of" (Set (Var "D")) (Bool "for" (Set (Var "f")) "being" ($#m2_finseq_1 :::"FinSequence"::: ) "of" (Set ($#k3_rfunct_3 :::"PFuncs"::: ) "(" (Set (Var "D")) "," (Set ($#k1_numbers :::"REAL"::: ) ) ")" ) "st" (Bool (Bool (Set (Var "d")) ($#r1_rfunct_3 :::"is_common_for_dom"::: ) (Set (Var "f")))) "holds" (Bool (Set (Set "(" ($#k14_rfunct_3 :::"Sum"::: ) (Set (Var "f")) ")" ) ($#k1_seq_1 :::"."::: ) (Set (Var "d"))) ($#r1_hidden :::"="::: ) (Set ($#k18_rvsum_1 :::"Sum"::: ) (Set "(" (Set (Var "f")) ($#k17_rfunct_3 :::"#"::: ) (Set (Var "d")) ")" )))))) ; definitionlet "D" be ($#~v1_xboole_0 "non" ($#v1_xboole_0 :::"empty"::: ) ) ($#m1_hidden :::"set"::: ) ; let "F" be ($#m1_subset_1 :::"PartFunc":::) "of" (Set (Const "D")) "," (Set ($#k1_numbers :::"REAL"::: ) ); func :::"max+"::: "F" -> ($#m1_subset_1 :::"PartFunc":::) "of" "D" "," (Set ($#k1_numbers :::"REAL"::: ) ) means :: RFUNCT_3:def 10 (Bool "(" (Bool (Set ($#k1_relset_1 :::"dom"::: ) it) ($#r1_hidden :::"="::: ) (Set ($#k1_relset_1 :::"dom"::: ) "F")) & (Bool "(" "for" (Set (Var "d")) "being" ($#m1_subset_1 :::"Element"::: ) "of" "D" "st" (Bool (Bool (Set (Var "d")) ($#r2_hidden :::"in"::: ) (Set ($#k1_relset_1 :::"dom"::: ) it))) "holds" (Bool (Set it ($#k1_seq_1 :::"."::: ) (Set (Var "d"))) ($#r1_hidden :::"="::: ) (Set ($#k1_rfunct_3 :::"max+"::: ) (Set "(" "F" ($#k1_seq_1 :::"."::: ) (Set (Var "d")) ")" ))) ")" ) ")" ); func :::"max-"::: "F" -> ($#m1_subset_1 :::"PartFunc":::) "of" "D" "," (Set ($#k1_numbers :::"REAL"::: ) ) means :: RFUNCT_3:def 11 (Bool "(" (Bool (Set ($#k1_relset_1 :::"dom"::: ) it) ($#r1_hidden :::"="::: ) (Set ($#k1_relset_1 :::"dom"::: ) "F")) & (Bool "(" "for" (Set (Var "d")) "being" ($#m1_subset_1 :::"Element"::: ) "of" "D" "st" (Bool (Bool (Set (Var "d")) ($#r2_hidden :::"in"::: ) (Set ($#k1_relset_1 :::"dom"::: ) it))) "holds" (Bool (Set it ($#k1_seq_1 :::"."::: ) (Set (Var "d"))) ($#r1_hidden :::"="::: ) (Set ($#k2_rfunct_3 :::"max-"::: ) (Set "(" "F" ($#k1_seq_1 :::"."::: ) (Set (Var "d")) ")" ))) ")" ) ")" ); end; :: deftheorem defines :::"max+"::: RFUNCT_3:def 10 : (Bool "for" (Set (Var "D")) "being" ($#~v1_xboole_0 "non" ($#v1_xboole_0 :::"empty"::: ) ) ($#m1_hidden :::"set"::: ) (Bool "for" (Set (Var "F")) "," (Set (Var "b3")) "being" ($#m1_subset_1 :::"PartFunc":::) "of" (Set (Var "D")) "," (Set ($#k1_numbers :::"REAL"::: ) ) "holds" (Bool "(" (Bool (Set (Var "b3")) ($#r1_hidden :::"="::: ) (Set ($#k18_rfunct_3 :::"max+"::: ) (Set (Var "F")))) "iff" (Bool "(" (Bool (Set ($#k1_relset_1 :::"dom"::: ) (Set (Var "b3"))) ($#r1_hidden :::"="::: ) (Set ($#k1_relset_1 :::"dom"::: ) (Set (Var "F")))) & (Bool "(" "for" (Set (Var "d")) "being" ($#m1_subset_1 :::"Element"::: ) "of" (Set (Var "D")) "st" (Bool (Bool (Set (Var "d")) ($#r2_hidden :::"in"::: ) (Set ($#k1_relset_1 :::"dom"::: ) (Set (Var "b3"))))) "holds" (Bool (Set (Set (Var "b3")) ($#k1_seq_1 :::"."::: ) (Set (Var "d"))) ($#r1_hidden :::"="::: ) (Set ($#k1_rfunct_3 :::"max+"::: ) (Set "(" (Set (Var "F")) ($#k1_seq_1 :::"."::: ) (Set (Var "d")) ")" ))) ")" ) ")" ) ")" ))); :: deftheorem defines :::"max-"::: RFUNCT_3:def 11 : (Bool "for" (Set (Var "D")) "being" ($#~v1_xboole_0 "non" ($#v1_xboole_0 :::"empty"::: ) ) ($#m1_hidden :::"set"::: ) (Bool "for" (Set (Var "F")) "," (Set (Var "b3")) "being" ($#m1_subset_1 :::"PartFunc":::) "of" (Set (Var "D")) "," (Set ($#k1_numbers :::"REAL"::: ) ) "holds" (Bool "(" (Bool (Set (Var "b3")) ($#r1_hidden :::"="::: ) (Set ($#k19_rfunct_3 :::"max-"::: ) (Set (Var "F")))) "iff" (Bool "(" (Bool (Set ($#k1_relset_1 :::"dom"::: ) (Set (Var "b3"))) ($#r1_hidden :::"="::: ) (Set ($#k1_relset_1 :::"dom"::: ) (Set (Var "F")))) & (Bool "(" "for" (Set (Var "d")) "being" ($#m1_subset_1 :::"Element"::: ) "of" (Set (Var "D")) "st" (Bool (Bool (Set (Var "d")) ($#r2_hidden :::"in"::: ) (Set ($#k1_relset_1 :::"dom"::: ) (Set (Var "b3"))))) "holds" (Bool (Set (Set (Var "b3")) ($#k1_seq_1 :::"."::: ) (Set (Var "d"))) ($#r1_hidden :::"="::: ) (Set ($#k2_rfunct_3 :::"max-"::: ) (Set "(" (Set (Var "F")) ($#k1_seq_1 :::"."::: ) (Set (Var "d")) ")" ))) ")" ) ")" ) ")" ))); theorem :: RFUNCT_3:34 (Bool "for" (Set (Var "D")) "being" ($#~v1_xboole_0 "non" ($#v1_xboole_0 :::"empty"::: ) ) ($#m1_hidden :::"set"::: ) (Bool "for" (Set (Var "F")) "being" ($#m1_subset_1 :::"PartFunc":::) "of" (Set (Var "D")) "," (Set ($#k1_numbers :::"REAL"::: ) ) "holds" (Bool "(" (Bool (Set (Var "F")) ($#r2_relset_1 :::"="::: ) (Set (Set "(" ($#k18_rfunct_3 :::"max+"::: ) (Set (Var "F")) ")" ) ($#k47_valued_1 :::"-"::: ) (Set "(" ($#k19_rfunct_3 :::"max-"::: ) (Set (Var "F")) ")" ))) & (Bool (Set ($#k56_valued_1 :::"abs"::: ) (Set (Var "F"))) ($#r2_relset_1 :::"="::: ) (Set (Set "(" ($#k18_rfunct_3 :::"max+"::: ) (Set (Var "F")) ")" ) ($#k3_valued_1 :::"+"::: ) (Set "(" ($#k19_rfunct_3 :::"max-"::: ) (Set (Var "F")) ")" ))) & (Bool (Set (Num 2) ($#k26_valued_1 :::"(#)"::: ) (Set "(" ($#k18_rfunct_3 :::"max+"::: ) (Set (Var "F")) ")" )) ($#r2_relset_1 :::"="::: ) (Set (Set (Var "F")) ($#k3_valued_1 :::"+"::: ) (Set "(" ($#k56_valued_1 :::"abs"::: ) (Set (Var "F")) ")" ))) ")" ))) ; theorem :: RFUNCT_3:35 (Bool "for" (Set (Var "D")) "being" ($#~v1_xboole_0 "non" ($#v1_xboole_0 :::"empty"::: ) ) ($#m1_hidden :::"set"::: ) (Bool "for" (Set (Var "F")) "being" ($#m1_subset_1 :::"PartFunc":::) "of" (Set (Var "D")) "," (Set ($#k1_numbers :::"REAL"::: ) ) (Bool "for" (Set (Var "r")) "being" ($#m1_subset_1 :::"Real":::) "st" (Bool (Bool (Set ($#k6_numbers :::"0"::: ) ) ($#r1_xxreal_0 :::"<"::: ) (Set (Var "r")))) "holds" (Bool (Set (Set (Var "F")) ($#k8_relset_1 :::"""::: ) (Set ($#k1_tarski :::"{"::: ) (Set (Var "r")) ($#k1_tarski :::"}"::: ) )) ($#r1_hidden :::"="::: ) (Set (Set "(" ($#k18_rfunct_3 :::"max+"::: ) (Set (Var "F")) ")" ) ($#k8_relset_1 :::"""::: ) (Set ($#k1_tarski :::"{"::: ) (Set (Var "r")) ($#k1_tarski :::"}"::: ) )))))) ; theorem :: RFUNCT_3:36 (Bool "for" (Set (Var "D")) "being" ($#~v1_xboole_0 "non" ($#v1_xboole_0 :::"empty"::: ) ) ($#m1_hidden :::"set"::: ) (Bool "for" (Set (Var "F")) "being" ($#m1_subset_1 :::"PartFunc":::) "of" (Set (Var "D")) "," (Set ($#k1_numbers :::"REAL"::: ) ) "holds" (Bool (Set (Set (Var "F")) ($#k8_relset_1 :::"""::: ) (Set "(" ($#k1_limfunc1 :::"left_closed_halfline"::: ) (Set ($#k6_numbers :::"0"::: ) ) ")" )) ($#r1_hidden :::"="::: ) (Set (Set "(" ($#k18_rfunct_3 :::"max+"::: ) (Set (Var "F")) ")" ) ($#k8_relset_1 :::"""::: ) (Set ($#k1_tarski :::"{"::: ) (Set ($#k6_numbers :::"0"::: ) ) ($#k1_tarski :::"}"::: ) ))))) ; theorem :: RFUNCT_3:37 (Bool "for" (Set (Var "D")) "being" ($#~v1_xboole_0 "non" ($#v1_xboole_0 :::"empty"::: ) ) ($#m1_hidden :::"set"::: ) (Bool "for" (Set (Var "F")) "being" ($#m1_subset_1 :::"PartFunc":::) "of" (Set (Var "D")) "," (Set ($#k1_numbers :::"REAL"::: ) ) (Bool "for" (Set (Var "d")) "being" ($#m1_subset_1 :::"Element"::: ) "of" (Set (Var "D")) "holds" (Bool (Set ($#k6_numbers :::"0"::: ) ) ($#r1_xxreal_0 :::"<="::: ) (Set (Set "(" ($#k18_rfunct_3 :::"max+"::: ) (Set (Var "F")) ")" ) ($#k1_seq_1 :::"."::: ) (Set (Var "d"))))))) ; theorem :: RFUNCT_3:38 (Bool "for" (Set (Var "D")) "being" ($#~v1_xboole_0 "non" ($#v1_xboole_0 :::"empty"::: ) ) ($#m1_hidden :::"set"::: ) (Bool "for" (Set (Var "F")) "being" ($#m1_subset_1 :::"PartFunc":::) "of" (Set (Var "D")) "," (Set ($#k1_numbers :::"REAL"::: ) ) (Bool "for" (Set (Var "r")) "being" ($#m1_subset_1 :::"Real":::) "st" (Bool (Bool (Set ($#k6_numbers :::"0"::: ) ) ($#r1_xxreal_0 :::"<"::: ) (Set (Var "r")))) "holds" (Bool (Set (Set (Var "F")) ($#k8_relset_1 :::"""::: ) (Set ($#k1_tarski :::"{"::: ) (Set "(" ($#k1_real_1 :::"-"::: ) (Set (Var "r")) ")" ) ($#k1_tarski :::"}"::: ) )) ($#r1_hidden :::"="::: ) (Set (Set "(" ($#k19_rfunct_3 :::"max-"::: ) (Set (Var "F")) ")" ) ($#k8_relset_1 :::"""::: ) (Set ($#k1_tarski :::"{"::: ) (Set (Var "r")) ($#k1_tarski :::"}"::: ) )))))) ; theorem :: RFUNCT_3:39 (Bool "for" (Set (Var "D")) "being" ($#~v1_xboole_0 "non" ($#v1_xboole_0 :::"empty"::: ) ) ($#m1_hidden :::"set"::: ) (Bool "for" (Set (Var "F")) "being" ($#m1_subset_1 :::"PartFunc":::) "of" (Set (Var "D")) "," (Set ($#k1_numbers :::"REAL"::: ) ) "holds" (Bool (Set (Set (Var "F")) ($#k8_relset_1 :::"""::: ) (Set "(" ($#k2_limfunc1 :::"right_closed_halfline"::: ) (Set ($#k6_numbers :::"0"::: ) ) ")" )) ($#r1_hidden :::"="::: ) (Set (Set "(" ($#k19_rfunct_3 :::"max-"::: ) (Set (Var "F")) ")" ) ($#k8_relset_1 :::"""::: ) (Set ($#k1_tarski :::"{"::: ) (Set ($#k6_numbers :::"0"::: ) ) ($#k1_tarski :::"}"::: ) ))))) ; theorem :: RFUNCT_3:40 (Bool "for" (Set (Var "D")) "being" ($#~v1_xboole_0 "non" ($#v1_xboole_0 :::"empty"::: ) ) ($#m1_hidden :::"set"::: ) (Bool "for" (Set (Var "F")) "being" ($#m1_subset_1 :::"PartFunc":::) "of" (Set (Var "D")) "," (Set ($#k1_numbers :::"REAL"::: ) ) (Bool "for" (Set (Var "d")) "being" ($#m1_subset_1 :::"Element"::: ) "of" (Set (Var "D")) "holds" (Bool (Set ($#k6_numbers :::"0"::: ) ) ($#r1_xxreal_0 :::"<="::: ) (Set (Set "(" ($#k19_rfunct_3 :::"max-"::: ) (Set (Var "F")) ")" ) ($#k1_seq_1 :::"."::: ) (Set (Var "d"))))))) ; theorem :: RFUNCT_3:41 (Bool "for" (Set (Var "D")) "," (Set (Var "C")) "being" ($#~v1_xboole_0 "non" ($#v1_xboole_0 :::"empty"::: ) ) ($#m1_hidden :::"set"::: ) (Bool "for" (Set (Var "F")) "being" ($#m1_subset_1 :::"PartFunc":::) "of" (Set (Var "D")) "," (Set ($#k1_numbers :::"REAL"::: ) ) (Bool "for" (Set (Var "G")) "being" ($#m1_subset_1 :::"PartFunc":::) "of" (Set (Var "C")) "," (Set ($#k1_numbers :::"REAL"::: ) ) "st" (Bool (Bool (Set (Var "F")) "," (Set (Var "G")) ($#r2_classes1 :::"are_fiberwise_equipotent"::: ) )) "holds" (Bool (Set ($#k18_rfunct_3 :::"max+"::: ) (Set (Var "F"))) "," (Set ($#k18_rfunct_3 :::"max+"::: ) (Set (Var "G"))) ($#r2_classes1 :::"are_fiberwise_equipotent"::: ) )))) ; theorem :: RFUNCT_3:42 (Bool "for" (Set (Var "D")) "," (Set (Var "C")) "being" ($#~v1_xboole_0 "non" ($#v1_xboole_0 :::"empty"::: ) ) ($#m1_hidden :::"set"::: ) (Bool "for" (Set (Var "F")) "being" ($#m1_subset_1 :::"PartFunc":::) "of" (Set (Var "D")) "," (Set ($#k1_numbers :::"REAL"::: ) ) (Bool "for" (Set (Var "G")) "being" ($#m1_subset_1 :::"PartFunc":::) "of" (Set (Var "C")) "," (Set ($#k1_numbers :::"REAL"::: ) ) "st" (Bool (Bool (Set (Var "F")) "," (Set (Var "G")) ($#r2_classes1 :::"are_fiberwise_equipotent"::: ) )) "holds" (Bool (Set ($#k19_rfunct_3 :::"max-"::: ) (Set (Var "F"))) "," (Set ($#k19_rfunct_3 :::"max-"::: ) (Set (Var "G"))) ($#r2_classes1 :::"are_fiberwise_equipotent"::: ) )))) ; registrationlet "D" be ($#~v1_xboole_0 "non" ($#v1_xboole_0 :::"empty"::: ) ) ($#m1_hidden :::"set"::: ) ; let "F" be ($#v1_finset_1 :::"finite"::: ) ($#m1_subset_1 :::"PartFunc":::) "of" (Set (Const "D")) "," (Set ($#k1_numbers :::"REAL"::: ) ); cluster (Set ($#k18_rfunct_3 :::"max+"::: ) "F") -> ($#v1_finset_1 :::"finite"::: ) ; cluster (Set ($#k19_rfunct_3 :::"max-"::: ) "F") -> ($#v1_finset_1 :::"finite"::: ) ; end; theorem :: RFUNCT_3:43 (Bool "for" (Set (Var "D")) "," (Set (Var "C")) "being" ($#~v1_xboole_0 "non" ($#v1_xboole_0 :::"empty"::: ) ) ($#m1_hidden :::"set"::: ) (Bool "for" (Set (Var "F")) "being" ($#v1_finset_1 :::"finite"::: ) ($#m1_subset_1 :::"PartFunc":::) "of" (Set (Var "D")) "," (Set ($#k1_numbers :::"REAL"::: ) ) (Bool "for" (Set (Var "G")) "being" ($#v1_finset_1 :::"finite"::: ) ($#m1_subset_1 :::"PartFunc":::) "of" (Set (Var "C")) "," (Set ($#k1_numbers :::"REAL"::: ) ) "st" (Bool (Bool (Set ($#k18_rfunct_3 :::"max+"::: ) (Set (Var "F"))) "," (Set ($#k18_rfunct_3 :::"max+"::: ) (Set (Var "G"))) ($#r2_classes1 :::"are_fiberwise_equipotent"::: ) ) & (Bool (Set ($#k19_rfunct_3 :::"max-"::: ) (Set (Var "F"))) "," (Set ($#k19_rfunct_3 :::"max-"::: ) (Set (Var "G"))) ($#r2_classes1 :::"are_fiberwise_equipotent"::: ) )) "holds" (Bool (Set (Var "F")) "," (Set (Var "G")) ($#r2_classes1 :::"are_fiberwise_equipotent"::: ) )))) ; theorem :: RFUNCT_3:44 (Bool "for" (Set (Var "D")) "being" ($#~v1_xboole_0 "non" ($#v1_xboole_0 :::"empty"::: ) ) ($#m1_hidden :::"set"::: ) (Bool "for" (Set (Var "F")) "being" ($#m1_subset_1 :::"PartFunc":::) "of" (Set (Var "D")) "," (Set ($#k1_numbers :::"REAL"::: ) ) (Bool "for" (Set (Var "X")) "being" ($#m1_hidden :::"set"::: ) "holds" (Bool (Set (Set "(" ($#k18_rfunct_3 :::"max+"::: ) (Set (Var "F")) ")" ) ($#k2_partfun1 :::"|"::: ) (Set (Var "X"))) ($#r2_relset_1 :::"="::: ) (Set ($#k18_rfunct_3 :::"max+"::: ) (Set "(" (Set (Var "F")) ($#k2_partfun1 :::"|"::: ) (Set (Var "X")) ")" )))))) ; theorem :: RFUNCT_3:45 (Bool "for" (Set (Var "D")) "being" ($#~v1_xboole_0 "non" ($#v1_xboole_0 :::"empty"::: ) ) ($#m1_hidden :::"set"::: ) (Bool "for" (Set (Var "F")) "being" ($#m1_subset_1 :::"PartFunc":::) "of" (Set (Var "D")) "," (Set ($#k1_numbers :::"REAL"::: ) ) (Bool "for" (Set (Var "X")) "being" ($#m1_hidden :::"set"::: ) "holds" (Bool (Set (Set "(" ($#k19_rfunct_3 :::"max-"::: ) (Set (Var "F")) ")" ) ($#k2_partfun1 :::"|"::: ) (Set (Var "X"))) ($#r2_relset_1 :::"="::: ) (Set ($#k19_rfunct_3 :::"max-"::: ) (Set "(" (Set (Var "F")) ($#k2_partfun1 :::"|"::: ) (Set (Var "X")) ")" )))))) ; theorem :: RFUNCT_3:46 (Bool "for" (Set (Var "D")) "being" ($#~v1_xboole_0 "non" ($#v1_xboole_0 :::"empty"::: ) ) ($#m1_hidden :::"set"::: ) (Bool "for" (Set (Var "F")) "being" ($#m1_subset_1 :::"PartFunc":::) "of" (Set (Var "D")) "," (Set ($#k1_numbers :::"REAL"::: ) ) "st" (Bool (Bool "(" "for" (Set (Var "d")) "being" ($#m1_subset_1 :::"Element"::: ) "of" (Set (Var "D")) "st" (Bool (Bool (Set (Var "d")) ($#r2_hidden :::"in"::: ) (Set ($#k1_relset_1 :::"dom"::: ) (Set (Var "F"))))) "holds" (Bool (Set (Set (Var "F")) ($#k1_seq_1 :::"."::: ) (Set (Var "d"))) ($#r1_xxreal_0 :::">="::: ) (Set ($#k6_numbers :::"0"::: ) )) ")" )) "holds" (Bool (Set ($#k18_rfunct_3 :::"max+"::: ) (Set (Var "F"))) ($#r2_relset_1 :::"="::: ) (Set (Var "F"))))) ; theorem :: RFUNCT_3:47 (Bool "for" (Set (Var "D")) "being" ($#~v1_xboole_0 "non" ($#v1_xboole_0 :::"empty"::: ) ) ($#m1_hidden :::"set"::: ) (Bool "for" (Set (Var "F")) "being" ($#m1_subset_1 :::"PartFunc":::) "of" (Set (Var "D")) "," (Set ($#k1_numbers :::"REAL"::: ) ) "st" (Bool (Bool "(" "for" (Set (Var "d")) "being" ($#m1_subset_1 :::"Element"::: ) "of" (Set (Var "D")) "st" (Bool (Bool (Set (Var "d")) ($#r2_hidden :::"in"::: ) (Set ($#k1_relset_1 :::"dom"::: ) (Set (Var "F"))))) "holds" (Bool (Set (Set (Var "F")) ($#k1_seq_1 :::"."::: ) (Set (Var "d"))) ($#r1_xxreal_0 :::"<="::: ) (Set ($#k6_numbers :::"0"::: ) )) ")" )) "holds" (Bool (Set ($#k19_rfunct_3 :::"max-"::: ) (Set (Var "F"))) ($#r2_relset_1 :::"="::: ) (Set ($#k32_valued_1 :::"-"::: ) (Set (Var "F")))))) ; theorem :: RFUNCT_3:48 (Bool "for" (Set (Var "D")) "being" ($#~v1_xboole_0 "non" ($#v1_xboole_0 :::"empty"::: ) ) ($#m1_hidden :::"set"::: ) (Bool "for" (Set (Var "F")) "being" ($#m1_subset_1 :::"PartFunc":::) "of" (Set (Var "D")) "," (Set ($#k1_numbers :::"REAL"::: ) ) "holds" (Bool (Set (Set (Var "F")) ($#k15_valued_1 :::"-"::: ) (Set ($#k6_numbers :::"0"::: ) )) ($#r2_relset_1 :::"="::: ) (Set (Var "F"))))) ; theorem :: RFUNCT_3:49 (Bool "for" (Set (Var "D")) "being" ($#~v1_xboole_0 "non" ($#v1_xboole_0 :::"empty"::: ) ) ($#m1_hidden :::"set"::: ) (Bool "for" (Set (Var "F")) "being" ($#m1_subset_1 :::"PartFunc":::) "of" (Set (Var "D")) "," (Set ($#k1_numbers :::"REAL"::: ) ) (Bool "for" (Set (Var "r")) "being" ($#m1_subset_1 :::"Real":::) (Bool "for" (Set (Var "X")) "being" ($#m1_hidden :::"set"::: ) "holds" (Bool (Set (Set "(" (Set (Var "F")) ($#k2_partfun1 :::"|"::: ) (Set (Var "X")) ")" ) ($#k15_valued_1 :::"-"::: ) (Set (Var "r"))) ($#r2_relset_1 :::"="::: ) (Set (Set "(" (Set (Var "F")) ($#k15_valued_1 :::"-"::: ) (Set (Var "r")) ")" ) ($#k2_partfun1 :::"|"::: ) (Set (Var "X")))))))) ; theorem :: RFUNCT_3:50 (Bool "for" (Set (Var "D")) "being" ($#~v1_xboole_0 "non" ($#v1_xboole_0 :::"empty"::: ) ) ($#m1_hidden :::"set"::: ) (Bool "for" (Set (Var "F")) "being" ($#m1_subset_1 :::"PartFunc":::) "of" (Set (Var "D")) "," (Set ($#k1_numbers :::"REAL"::: ) ) (Bool "for" (Set (Var "r")) "," (Set (Var "s")) "being" ($#m1_subset_1 :::"Real":::) "holds" (Bool (Set (Set (Var "F")) ($#k8_relset_1 :::"""::: ) (Set ($#k1_tarski :::"{"::: ) (Set "(" (Set (Var "s")) ($#k7_real_1 :::"+"::: ) (Set (Var "r")) ")" ) ($#k1_tarski :::"}"::: ) )) ($#r1_hidden :::"="::: ) (Set (Set "(" (Set (Var "F")) ($#k15_valued_1 :::"-"::: ) (Set (Var "r")) ")" ) ($#k8_relset_1 :::"""::: ) (Set ($#k1_tarski :::"{"::: ) (Set (Var "s")) ($#k1_tarski :::"}"::: ) )))))) ; theorem :: RFUNCT_3:51 (Bool "for" (Set (Var "D")) "," (Set (Var "C")) "being" ($#~v1_xboole_0 "non" ($#v1_xboole_0 :::"empty"::: ) ) ($#m1_hidden :::"set"::: ) (Bool "for" (Set (Var "F")) "being" ($#m1_subset_1 :::"PartFunc":::) "of" (Set (Var "D")) "," (Set ($#k1_numbers :::"REAL"::: ) ) (Bool "for" (Set (Var "G")) "being" ($#m1_subset_1 :::"PartFunc":::) "of" (Set (Var "C")) "," (Set ($#k1_numbers :::"REAL"::: ) ) (Bool "for" (Set (Var "r")) "being" ($#m1_subset_1 :::"Real":::) "holds" (Bool "(" (Bool (Set (Var "F")) "," (Set (Var "G")) ($#r2_classes1 :::"are_fiberwise_equipotent"::: ) ) "iff" (Bool (Set (Set (Var "F")) ($#k15_valued_1 :::"-"::: ) (Set (Var "r"))) "," (Set (Set (Var "G")) ($#k15_valued_1 :::"-"::: ) (Set (Var "r"))) ($#r2_classes1 :::"are_fiberwise_equipotent"::: ) ) ")" ))))) ; definitionlet "F" be ($#m1_subset_1 :::"PartFunc":::) "of" (Set ($#k1_numbers :::"REAL"::: ) ) "," (Set ($#k1_numbers :::"REAL"::: ) ); let "X" be ($#m1_hidden :::"set"::: ) ; pred "F" :::"is_convex_on"::: "X" means :: RFUNCT_3:def 12 (Bool "(" (Bool "X" ($#r1_tarski :::"c="::: ) (Set ($#k1_relset_1 :::"dom"::: ) "F")) & (Bool "(" "for" (Set (Var "p")) "being" ($#m1_subset_1 :::"Real":::) "st" (Bool (Bool (Set ($#k6_numbers :::"0"::: ) ) ($#r1_xxreal_0 :::"<="::: ) (Set (Var "p"))) & (Bool (Set (Var "p")) ($#r1_xxreal_0 :::"<="::: ) (Num 1))) "holds" (Bool "for" (Set (Var "r")) "," (Set (Var "s")) "being" ($#m1_subset_1 :::"Real":::) "st" (Bool (Bool (Set (Var "r")) ($#r2_hidden :::"in"::: ) "X") & (Bool (Set (Var "s")) ($#r2_hidden :::"in"::: ) "X") & (Bool (Set (Set "(" (Set (Var "p")) ($#k8_real_1 :::"*"::: ) (Set (Var "r")) ")" ) ($#k7_real_1 :::"+"::: ) (Set "(" (Set "(" (Num 1) ($#k9_real_1 :::"-"::: ) (Set (Var "p")) ")" ) ($#k8_real_1 :::"*"::: ) (Set (Var "s")) ")" )) ($#r2_hidden :::"in"::: ) "X")) "holds" (Bool (Set "F" ($#k1_seq_1 :::"."::: ) (Set "(" (Set "(" (Set (Var "p")) ($#k8_real_1 :::"*"::: ) (Set (Var "r")) ")" ) ($#k7_real_1 :::"+"::: ) (Set "(" (Set "(" (Num 1) ($#k9_real_1 :::"-"::: ) (Set (Var "p")) ")" ) ($#k8_real_1 :::"*"::: ) (Set (Var "s")) ")" ) ")" )) ($#r1_xxreal_0 :::"<="::: ) (Set (Set "(" (Set (Var "p")) ($#k8_real_1 :::"*"::: ) (Set "(" "F" ($#k1_seq_1 :::"."::: ) (Set (Var "r")) ")" ) ")" ) ($#k7_real_1 :::"+"::: ) (Set "(" (Set "(" (Num 1) ($#k9_real_1 :::"-"::: ) (Set (Var "p")) ")" ) ($#k8_real_1 :::"*"::: ) (Set "(" "F" ($#k1_seq_1 :::"."::: ) (Set (Var "s")) ")" ) ")" )))) ")" ) ")" ); end; :: deftheorem defines :::"is_convex_on"::: RFUNCT_3:def 12 : (Bool "for" (Set (Var "F")) "being" ($#m1_subset_1 :::"PartFunc":::) "of" (Set ($#k1_numbers :::"REAL"::: ) ) "," (Set ($#k1_numbers :::"REAL"::: ) ) (Bool "for" (Set (Var "X")) "being" ($#m1_hidden :::"set"::: ) "holds" (Bool "(" (Bool (Set (Var "F")) ($#r2_rfunct_3 :::"is_convex_on"::: ) (Set (Var "X"))) "iff" (Bool "(" (Bool (Set (Var "X")) ($#r1_tarski :::"c="::: ) (Set ($#k1_relset_1 :::"dom"::: ) (Set (Var "F")))) & (Bool "(" "for" (Set (Var "p")) "being" ($#m1_subset_1 :::"Real":::) "st" (Bool (Bool (Set ($#k6_numbers :::"0"::: ) ) ($#r1_xxreal_0 :::"<="::: ) (Set (Var "p"))) & (Bool (Set (Var "p")) ($#r1_xxreal_0 :::"<="::: ) (Num 1))) "holds" (Bool "for" (Set (Var "r")) "," (Set (Var "s")) "being" ($#m1_subset_1 :::"Real":::) "st" (Bool (Bool (Set (Var "r")) ($#r2_hidden :::"in"::: ) (Set (Var "X"))) & (Bool (Set (Var "s")) ($#r2_hidden :::"in"::: ) (Set (Var "X"))) & (Bool (Set (Set "(" (Set (Var "p")) ($#k8_real_1 :::"*"::: ) (Set (Var "r")) ")" ) ($#k7_real_1 :::"+"::: ) (Set "(" (Set "(" (Num 1) ($#k9_real_1 :::"-"::: ) (Set (Var "p")) ")" ) ($#k8_real_1 :::"*"::: ) (Set (Var "s")) ")" )) ($#r2_hidden :::"in"::: ) (Set (Var "X")))) "holds" (Bool (Set (Set (Var "F")) ($#k1_seq_1 :::"."::: ) (Set "(" (Set "(" (Set (Var "p")) ($#k8_real_1 :::"*"::: ) (Set (Var "r")) ")" ) ($#k7_real_1 :::"+"::: ) (Set "(" (Set "(" (Num 1) ($#k9_real_1 :::"-"::: ) (Set (Var "p")) ")" ) ($#k8_real_1 :::"*"::: ) (Set (Var "s")) ")" ) ")" )) ($#r1_xxreal_0 :::"<="::: ) (Set (Set "(" (Set (Var "p")) ($#k8_real_1 :::"*"::: ) (Set "(" (Set (Var "F")) ($#k1_seq_1 :::"."::: ) (Set (Var "r")) ")" ) ")" ) ($#k7_real_1 :::"+"::: ) (Set "(" (Set "(" (Num 1) ($#k9_real_1 :::"-"::: ) (Set (Var "p")) ")" ) ($#k8_real_1 :::"*"::: ) (Set "(" (Set (Var "F")) ($#k1_seq_1 :::"."::: ) (Set (Var "s")) ")" ) ")" )))) ")" ) ")" ) ")" ))); theorem :: RFUNCT_3:52 (Bool "for" (Set (Var "a")) "," (Set (Var "b")) "being" ($#m1_subset_1 :::"Real":::) (Bool "for" (Set (Var "F")) "being" ($#m1_subset_1 :::"PartFunc":::) "of" (Set ($#k1_numbers :::"REAL"::: ) ) "," (Set ($#k1_numbers :::"REAL"::: ) ) "holds" (Bool "(" (Bool (Set (Var "F")) ($#r2_rfunct_3 :::"is_convex_on"::: ) (Set ($#k1_rcomp_1 :::"[."::: ) (Set (Var "a")) "," (Set (Var "b")) ($#k1_rcomp_1 :::".]"::: ) )) "iff" (Bool "(" (Bool (Set ($#k1_rcomp_1 :::"[."::: ) (Set (Var "a")) "," (Set (Var "b")) ($#k1_rcomp_1 :::".]"::: ) ) ($#r1_tarski :::"c="::: ) (Set ($#k1_relset_1 :::"dom"::: ) (Set (Var "F")))) & (Bool "(" "for" (Set (Var "p")) "being" ($#m1_subset_1 :::"Real":::) "st" (Bool (Bool (Set ($#k6_numbers :::"0"::: ) ) ($#r1_xxreal_0 :::"<="::: ) (Set (Var "p"))) & (Bool (Set (Var "p")) ($#r1_xxreal_0 :::"<="::: ) (Num 1))) "holds" (Bool "for" (Set (Var "r")) "," (Set (Var "s")) "being" ($#m1_subset_1 :::"Real":::) "st" (Bool (Bool (Set (Var "r")) ($#r2_hidden :::"in"::: ) (Set ($#k1_rcomp_1 :::"[."::: ) (Set (Var "a")) "," (Set (Var "b")) ($#k1_rcomp_1 :::".]"::: ) )) & (Bool (Set (Var "s")) ($#r2_hidden :::"in"::: ) (Set ($#k1_rcomp_1 :::"[."::: ) (Set (Var "a")) "," (Set (Var "b")) ($#k1_rcomp_1 :::".]"::: ) ))) "holds" (Bool (Set (Set (Var "F")) ($#k1_seq_1 :::"."::: ) (Set "(" (Set "(" (Set (Var "p")) ($#k8_real_1 :::"*"::: ) (Set (Var "r")) ")" ) ($#k7_real_1 :::"+"::: ) (Set "(" (Set "(" (Num 1) ($#k9_real_1 :::"-"::: ) (Set (Var "p")) ")" ) ($#k8_real_1 :::"*"::: ) (Set (Var "s")) ")" ) ")" )) ($#r1_xxreal_0 :::"<="::: ) (Set (Set "(" (Set (Var "p")) ($#k8_real_1 :::"*"::: ) (Set "(" (Set (Var "F")) ($#k1_seq_1 :::"."::: ) (Set (Var "r")) ")" ) ")" ) ($#k7_real_1 :::"+"::: ) (Set "(" (Set "(" (Num 1) ($#k9_real_1 :::"-"::: ) (Set (Var "p")) ")" ) ($#k8_real_1 :::"*"::: ) (Set "(" (Set (Var "F")) ($#k1_seq_1 :::"."::: ) (Set (Var "s")) ")" ) ")" )))) ")" ) ")" ) ")" ))) ; theorem :: RFUNCT_3:53 (Bool "for" (Set (Var "a")) "," (Set (Var "b")) "being" ($#m1_subset_1 :::"Real":::) (Bool "for" (Set (Var "F")) "being" ($#m1_subset_1 :::"PartFunc":::) "of" (Set ($#k1_numbers :::"REAL"::: ) ) "," (Set ($#k1_numbers :::"REAL"::: ) ) "holds" (Bool "(" (Bool (Set (Var "F")) ($#r2_rfunct_3 :::"is_convex_on"::: ) (Set ($#k1_rcomp_1 :::"[."::: ) (Set (Var "a")) "," (Set (Var "b")) ($#k1_rcomp_1 :::".]"::: ) )) "iff" (Bool "(" (Bool (Set ($#k1_rcomp_1 :::"[."::: ) (Set (Var "a")) "," (Set (Var "b")) ($#k1_rcomp_1 :::".]"::: ) ) ($#r1_tarski :::"c="::: ) (Set ($#k1_relset_1 :::"dom"::: ) (Set (Var "F")))) & (Bool "(" "for" (Set (Var "x1")) "," (Set (Var "x2")) "," (Set (Var "x3")) "being" ($#m1_subset_1 :::"Real":::) "st" (Bool (Bool (Set (Var "x1")) ($#r2_hidden :::"in"::: ) (Set ($#k1_rcomp_1 :::"[."::: ) (Set (Var "a")) "," (Set (Var "b")) ($#k1_rcomp_1 :::".]"::: ) )) & (Bool (Set (Var "x2")) ($#r2_hidden :::"in"::: ) (Set ($#k1_rcomp_1 :::"[."::: ) (Set (Var "a")) "," (Set (Var "b")) ($#k1_rcomp_1 :::".]"::: ) )) & (Bool (Set (Var "x3")) ($#r2_hidden :::"in"::: ) (Set ($#k1_rcomp_1 :::"[."::: ) (Set (Var "a")) "," (Set (Var "b")) ($#k1_rcomp_1 :::".]"::: ) )) & (Bool (Set (Var "x1")) ($#r1_xxreal_0 :::"<"::: ) (Set (Var "x2"))) & (Bool (Set (Var "x2")) ($#r1_xxreal_0 :::"<"::: ) (Set (Var "x3")))) "holds" (Bool (Set (Set "(" (Set "(" (Set (Var "F")) ($#k1_seq_1 :::"."::: ) (Set (Var "x1")) ")" ) ($#k9_real_1 :::"-"::: ) (Set "(" (Set (Var "F")) ($#k1_seq_1 :::"."::: ) (Set (Var "x2")) ")" ) ")" ) ($#k10_real_1 :::"/"::: ) (Set "(" (Set (Var "x1")) ($#k9_real_1 :::"-"::: ) (Set (Var "x2")) ")" )) ($#r1_xxreal_0 :::"<="::: ) (Set (Set "(" (Set "(" (Set (Var "F")) ($#k1_seq_1 :::"."::: ) (Set (Var "x2")) ")" ) ($#k9_real_1 :::"-"::: ) (Set "(" (Set (Var "F")) ($#k1_seq_1 :::"."::: ) (Set (Var "x3")) ")" ) ")" ) ($#k10_real_1 :::"/"::: ) (Set "(" (Set (Var "x2")) ($#k9_real_1 :::"-"::: ) (Set (Var "x3")) ")" ))) ")" ) ")" ) ")" ))) ; theorem :: RFUNCT_3:54 (Bool "for" (Set (Var "F")) "being" ($#m1_subset_1 :::"PartFunc":::) "of" (Set ($#k1_numbers :::"REAL"::: ) ) "," (Set ($#k1_numbers :::"REAL"::: ) ) (Bool "for" (Set (Var "X")) "," (Set (Var "Y")) "being" ($#m1_hidden :::"set"::: ) "st" (Bool (Bool (Set (Var "F")) ($#r2_rfunct_3 :::"is_convex_on"::: ) (Set (Var "X"))) & (Bool (Set (Var "Y")) ($#r1_tarski :::"c="::: ) (Set (Var "X")))) "holds" (Bool (Set (Var "F")) ($#r2_rfunct_3 :::"is_convex_on"::: ) (Set (Var "Y"))))) ; theorem :: RFUNCT_3:55 (Bool "for" (Set (Var "F")) "being" ($#m1_subset_1 :::"PartFunc":::) "of" (Set ($#k1_numbers :::"REAL"::: ) ) "," (Set ($#k1_numbers :::"REAL"::: ) ) (Bool "for" (Set (Var "X")) "being" ($#m1_hidden :::"set"::: ) (Bool "for" (Set (Var "r")) "being" ($#m1_subset_1 :::"Real":::) "holds" (Bool "(" (Bool (Set (Var "F")) ($#r2_rfunct_3 :::"is_convex_on"::: ) (Set (Var "X"))) "iff" (Bool (Set (Set (Var "F")) ($#k15_valued_1 :::"-"::: ) (Set (Var "r"))) ($#r2_rfunct_3 :::"is_convex_on"::: ) (Set (Var "X"))) ")" )))) ; theorem :: RFUNCT_3:56 (Bool "for" (Set (Var "F")) "being" ($#m1_subset_1 :::"PartFunc":::) "of" (Set ($#k1_numbers :::"REAL"::: ) ) "," (Set ($#k1_numbers :::"REAL"::: ) ) (Bool "for" (Set (Var "X")) "being" ($#m1_hidden :::"set"::: ) (Bool "for" (Set (Var "r")) "being" ($#m1_subset_1 :::"Real":::) "st" (Bool (Bool (Set ($#k6_numbers :::"0"::: ) ) ($#r1_xxreal_0 :::"<"::: ) (Set (Var "r")))) "holds" (Bool "(" (Bool (Set (Var "F")) ($#r2_rfunct_3 :::"is_convex_on"::: ) (Set (Var "X"))) "iff" (Bool (Set (Set (Var "r")) ($#k26_valued_1 :::"(#)"::: ) (Set (Var "F"))) ($#r2_rfunct_3 :::"is_convex_on"::: ) (Set (Var "X"))) ")" )))) ; theorem :: RFUNCT_3:57 (Bool "for" (Set (Var "F")) "being" ($#m1_subset_1 :::"PartFunc":::) "of" (Set ($#k1_numbers :::"REAL"::: ) ) "," (Set ($#k1_numbers :::"REAL"::: ) ) (Bool "for" (Set (Var "X")) "being" ($#m1_hidden :::"set"::: ) "st" (Bool (Bool (Set (Var "X")) ($#r1_tarski :::"c="::: ) (Set ($#k1_relset_1 :::"dom"::: ) (Set (Var "F"))))) "holds" (Bool (Set (Set ($#k6_numbers :::"0"::: ) ) ($#k26_valued_1 :::"(#)"::: ) (Set (Var "F"))) ($#r2_rfunct_3 :::"is_convex_on"::: ) (Set (Var "X"))))) ; theorem :: RFUNCT_3:58 (Bool "for" (Set (Var "F")) "," (Set (Var "G")) "being" ($#m1_subset_1 :::"PartFunc":::) "of" (Set ($#k1_numbers :::"REAL"::: ) ) "," (Set ($#k1_numbers :::"REAL"::: ) ) (Bool "for" (Set (Var "X")) "being" ($#m1_hidden :::"set"::: ) "st" (Bool (Bool (Set (Var "F")) ($#r2_rfunct_3 :::"is_convex_on"::: ) (Set (Var "X"))) & (Bool (Set (Var "G")) ($#r2_rfunct_3 :::"is_convex_on"::: ) (Set (Var "X")))) "holds" (Bool (Set (Set (Var "F")) ($#k3_valued_1 :::"+"::: ) (Set (Var "G"))) ($#r2_rfunct_3 :::"is_convex_on"::: ) (Set (Var "X"))))) ; theorem :: RFUNCT_3:59 (Bool "for" (Set (Var "F")) "being" ($#m1_subset_1 :::"PartFunc":::) "of" (Set ($#k1_numbers :::"REAL"::: ) ) "," (Set ($#k1_numbers :::"REAL"::: ) ) (Bool "for" (Set (Var "X")) "being" ($#m1_hidden :::"set"::: ) (Bool "for" (Set (Var "r")) "being" ($#m1_subset_1 :::"Real":::) "st" (Bool (Bool (Set (Var "F")) ($#r2_rfunct_3 :::"is_convex_on"::: ) (Set (Var "X")))) "holds" (Bool (Set ($#k18_rfunct_3 :::"max+"::: ) (Set "(" (Set (Var "F")) ($#k15_valued_1 :::"-"::: ) (Set (Var "r")) ")" )) ($#r2_rfunct_3 :::"is_convex_on"::: ) (Set (Var "X")))))) ; theorem :: RFUNCT_3:60 (Bool "for" (Set (Var "F")) "being" ($#m1_subset_1 :::"PartFunc":::) "of" (Set ($#k1_numbers :::"REAL"::: ) ) "," (Set ($#k1_numbers :::"REAL"::: ) ) (Bool "for" (Set (Var "X")) "being" ($#m1_hidden :::"set"::: ) "st" (Bool (Bool (Set (Var "F")) ($#r2_rfunct_3 :::"is_convex_on"::: ) (Set (Var "X")))) "holds" (Bool (Set ($#k18_rfunct_3 :::"max+"::: ) (Set (Var "F"))) ($#r2_rfunct_3 :::"is_convex_on"::: ) (Set (Var "X"))))) ; theorem :: RFUNCT_3:61 (Bool (Set ($#k1_partfun2 :::"id"::: ) (Set "(" ($#k2_subset_1 :::"[#]"::: ) (Set ($#k1_numbers :::"REAL"::: ) ) ")" )) ($#r2_rfunct_3 :::"is_convex_on"::: ) (Set ($#k1_numbers :::"REAL"::: ) )) ; theorem :: RFUNCT_3:62 (Bool "for" (Set (Var "r")) "being" ($#m1_subset_1 :::"Real":::) "holds" (Bool (Set ($#k18_rfunct_3 :::"max+"::: ) (Set "(" (Set "(" ($#k1_partfun2 :::"id"::: ) (Set "(" ($#k2_subset_1 :::"[#]"::: ) (Set ($#k1_numbers :::"REAL"::: ) ) ")" ) ")" ) ($#k15_valued_1 :::"-"::: ) (Set (Var "r")) ")" )) ($#r2_rfunct_3 :::"is_convex_on"::: ) (Set ($#k1_numbers :::"REAL"::: ) ))) ; definitionlet "D" be ($#~v1_xboole_0 "non" ($#v1_xboole_0 :::"empty"::: ) ) ($#m1_hidden :::"set"::: ) ; let "F" be ($#m1_subset_1 :::"PartFunc":::) "of" (Set (Const "D")) "," (Set ($#k1_numbers :::"REAL"::: ) ); let "X" be ($#m1_hidden :::"set"::: ) ; assume (Bool (Set ($#k1_relset_1 :::"dom"::: ) (Set "(" (Set (Const "F")) ($#k2_partfun1 :::"|"::: ) (Set (Const "X")) ")" )) "is" ($#v1_finset_1 :::"finite"::: ) ) ; func :::"FinS"::: "(" "F" "," "X" ")" -> ($#v8_valued_0 :::"non-increasing"::: ) ($#m2_finseq_1 :::"FinSequence"::: ) "of" (Set ($#k1_numbers :::"REAL"::: ) ) means :: RFUNCT_3:def 13 (Bool (Set "F" ($#k2_partfun1 :::"|"::: ) "X") "," it ($#r2_classes1 :::"are_fiberwise_equipotent"::: ) ); end; :: deftheorem defines :::"FinS"::: RFUNCT_3:def 13 : (Bool "for" (Set (Var "D")) "being" ($#~v1_xboole_0 "non" ($#v1_xboole_0 :::"empty"::: ) ) ($#m1_hidden :::"set"::: ) (Bool "for" (Set (Var "F")) "being" ($#m1_subset_1 :::"PartFunc":::) "of" (Set (Var "D")) "," (Set ($#k1_numbers :::"REAL"::: ) ) (Bool "for" (Set (Var "X")) "being" ($#m1_hidden :::"set"::: ) "st" (Bool (Bool (Set ($#k1_relset_1 :::"dom"::: ) (Set "(" (Set (Var "F")) ($#k2_partfun1 :::"|"::: ) (Set (Var "X")) ")" )) "is" ($#v1_finset_1 :::"finite"::: ) )) "holds" (Bool "for" (Set (Var "b4")) "being" ($#v8_valued_0 :::"non-increasing"::: ) ($#m2_finseq_1 :::"FinSequence"::: ) "of" (Set ($#k1_numbers :::"REAL"::: ) ) "holds" (Bool "(" (Bool (Set (Var "b4")) ($#r1_hidden :::"="::: ) (Set ($#k20_rfunct_3 :::"FinS"::: ) "(" (Set (Var "F")) "," (Set (Var "X")) ")" )) "iff" (Bool (Set (Set (Var "F")) ($#k2_partfun1 :::"|"::: ) (Set (Var "X"))) "," (Set (Var "b4")) ($#r2_classes1 :::"are_fiberwise_equipotent"::: ) ) ")" ))))); theorem :: RFUNCT_3:63 (Bool "for" (Set (Var "D")) "being" ($#~v1_xboole_0 "non" ($#v1_xboole_0 :::"empty"::: ) ) ($#m1_hidden :::"set"::: ) (Bool "for" (Set (Var "F")) "being" ($#m1_subset_1 :::"PartFunc":::) "of" (Set (Var "D")) "," (Set ($#k1_numbers :::"REAL"::: ) ) (Bool "for" (Set (Var "X")) "being" ($#m1_hidden :::"set"::: ) "st" (Bool (Bool (Set ($#k1_relset_1 :::"dom"::: ) (Set "(" (Set (Var "F")) ($#k2_partfun1 :::"|"::: ) (Set (Var "X")) ")" )) "is" ($#v1_finset_1 :::"finite"::: ) )) "holds" (Bool (Set ($#k20_rfunct_3 :::"FinS"::: ) "(" (Set (Var "F")) "," (Set "(" ($#k1_relset_1 :::"dom"::: ) (Set "(" (Set (Var "F")) ($#k2_partfun1 :::"|"::: ) (Set (Var "X")) ")" ) ")" ) ")" ) ($#r1_hidden :::"="::: ) (Set ($#k20_rfunct_3 :::"FinS"::: ) "(" (Set (Var "F")) "," (Set (Var "X")) ")" ))))) ; theorem :: RFUNCT_3:64 (Bool "for" (Set (Var "D")) "being" ($#~v1_xboole_0 "non" ($#v1_xboole_0 :::"empty"::: ) ) ($#m1_hidden :::"set"::: ) (Bool "for" (Set (Var "F")) "being" ($#m1_subset_1 :::"PartFunc":::) "of" (Set (Var "D")) "," (Set ($#k1_numbers :::"REAL"::: ) ) (Bool "for" (Set (Var "X")) "being" ($#m1_hidden :::"set"::: ) "st" (Bool (Bool (Set ($#k1_relset_1 :::"dom"::: ) (Set "(" (Set (Var "F")) ($#k2_partfun1 :::"|"::: ) (Set (Var "X")) ")" )) "is" ($#v1_finset_1 :::"finite"::: ) )) "holds" (Bool (Set ($#k20_rfunct_3 :::"FinS"::: ) "(" (Set "(" (Set (Var "F")) ($#k2_partfun1 :::"|"::: ) (Set (Var "X")) ")" ) "," (Set (Var "X")) ")" ) ($#r1_hidden :::"="::: ) (Set ($#k20_rfunct_3 :::"FinS"::: ) "(" (Set (Var "F")) "," (Set (Var "X")) ")" ))))) ; theorem :: RFUNCT_3:65 (Bool "for" (Set (Var "D")) "being" ($#~v1_xboole_0 "non" ($#v1_xboole_0 :::"empty"::: ) ) ($#m1_hidden :::"set"::: ) (Bool "for" (Set (Var "d")) "being" ($#m1_subset_1 :::"Element"::: ) "of" (Set (Var "D")) (Bool "for" (Set (Var "X")) "being" ($#m1_hidden :::"set"::: ) (Bool "for" (Set (Var "F")) "being" ($#m1_subset_1 :::"PartFunc":::) "of" (Set (Var "D")) "," (Set ($#k1_numbers :::"REAL"::: ) ) "st" (Bool (Bool (Set (Var "X")) "is" ($#v1_finset_1 :::"finite"::: ) ) & (Bool (Set (Var "d")) ($#r2_hidden :::"in"::: ) (Set ($#k1_relset_1 :::"dom"::: ) (Set "(" (Set (Var "F")) ($#k2_partfun1 :::"|"::: ) (Set (Var "X")) ")" )))) "holds" (Bool (Set (Set "(" ($#k20_rfunct_3 :::"FinS"::: ) "(" (Set (Var "F")) "," (Set "(" (Set (Var "X")) ($#k6_subset_1 :::"\"::: ) (Set ($#k1_tarski :::"{"::: ) (Set (Var "d")) ($#k1_tarski :::"}"::: ) ) ")" ) ")" ")" ) ($#k8_finseq_1 :::"^"::: ) (Set ($#k12_finseq_1 :::"<*"::: ) (Set "(" (Set (Var "F")) ($#k1_seq_1 :::"."::: ) (Set (Var "d")) ")" ) ($#k12_finseq_1 :::"*>"::: ) )) "," (Set (Set (Var "F")) ($#k2_partfun1 :::"|"::: ) (Set (Var "X"))) ($#r2_classes1 :::"are_fiberwise_equipotent"::: ) ))))) ; theorem :: RFUNCT_3:66 (Bool "for" (Set (Var "D")) "being" ($#~v1_xboole_0 "non" ($#v1_xboole_0 :::"empty"::: ) ) ($#m1_hidden :::"set"::: ) (Bool "for" (Set (Var "d")) "being" ($#m1_subset_1 :::"Element"::: ) "of" (Set (Var "D")) (Bool "for" (Set (Var "X")) "being" ($#m1_hidden :::"set"::: ) (Bool "for" (Set (Var "F")) "being" ($#m1_subset_1 :::"PartFunc":::) "of" (Set (Var "D")) "," (Set ($#k1_numbers :::"REAL"::: ) ) "st" (Bool (Bool (Set ($#k1_relset_1 :::"dom"::: ) (Set "(" (Set (Var "F")) ($#k2_partfun1 :::"|"::: ) (Set (Var "X")) ")" )) "is" ($#v1_finset_1 :::"finite"::: ) ) & (Bool (Set (Var "d")) ($#r2_hidden :::"in"::: ) (Set ($#k1_relset_1 :::"dom"::: ) (Set "(" (Set (Var "F")) ($#k2_partfun1 :::"|"::: ) (Set (Var "X")) ")" )))) "holds" (Bool (Set (Set "(" ($#k20_rfunct_3 :::"FinS"::: ) "(" (Set (Var "F")) "," (Set "(" (Set (Var "X")) ($#k6_subset_1 :::"\"::: ) (Set ($#k1_tarski :::"{"::: ) (Set (Var "d")) ($#k1_tarski :::"}"::: ) ) ")" ) ")" ")" ) ($#k8_finseq_1 :::"^"::: ) (Set ($#k12_finseq_1 :::"<*"::: ) (Set "(" (Set (Var "F")) ($#k1_seq_1 :::"."::: ) (Set (Var "d")) ")" ) ($#k12_finseq_1 :::"*>"::: ) )) "," (Set (Set (Var "F")) ($#k2_partfun1 :::"|"::: ) (Set (Var "X"))) ($#r2_classes1 :::"are_fiberwise_equipotent"::: ) ))))) ; theorem :: RFUNCT_3:67 (Bool "for" (Set (Var "D")) "being" ($#~v1_xboole_0 "non" ($#v1_xboole_0 :::"empty"::: ) ) ($#m1_hidden :::"set"::: ) (Bool "for" (Set (Var "F")) "being" ($#m1_subset_1 :::"PartFunc":::) "of" (Set (Var "D")) "," (Set ($#k1_numbers :::"REAL"::: ) ) (Bool "for" (Set (Var "X")) "being" ($#m1_hidden :::"set"::: ) (Bool "for" (Set (Var "Y")) "being" ($#v1_finset_1 :::"finite"::: ) ($#m1_hidden :::"set"::: ) "st" (Bool (Bool (Set (Var "Y")) ($#r1_hidden :::"="::: ) (Set ($#k1_relset_1 :::"dom"::: ) (Set "(" (Set (Var "F")) ($#k2_partfun1 :::"|"::: ) (Set (Var "X")) ")" )))) "holds" (Bool (Set ($#k3_finseq_1 :::"len"::: ) (Set "(" ($#k20_rfunct_3 :::"FinS"::: ) "(" (Set (Var "F")) "," (Set (Var "X")) ")" ")" )) ($#r1_hidden :::"="::: ) (Set ($#k5_card_1 :::"card"::: ) (Set (Var "Y")))))))) ; theorem :: RFUNCT_3:68 (Bool "for" (Set (Var "D")) "being" ($#~v1_xboole_0 "non" ($#v1_xboole_0 :::"empty"::: ) ) ($#m1_hidden :::"set"::: ) (Bool "for" (Set (Var "F")) "being" ($#m1_subset_1 :::"PartFunc":::) "of" (Set (Var "D")) "," (Set ($#k1_numbers :::"REAL"::: ) ) "holds" (Bool (Set ($#k20_rfunct_3 :::"FinS"::: ) "(" (Set (Var "F")) "," (Set ($#k1_xboole_0 :::"{}"::: ) ) ")" ) ($#r1_hidden :::"="::: ) (Set ($#k6_finseq_1 :::"<*>"::: ) (Set ($#k1_numbers :::"REAL"::: ) ))))) ; theorem :: RFUNCT_3:69 (Bool "for" (Set (Var "D")) "being" ($#~v1_xboole_0 "non" ($#v1_xboole_0 :::"empty"::: ) ) ($#m1_hidden :::"set"::: ) (Bool "for" (Set (Var "F")) "being" ($#m1_subset_1 :::"PartFunc":::) "of" (Set (Var "D")) "," (Set ($#k1_numbers :::"REAL"::: ) ) (Bool "for" (Set (Var "d")) "being" ($#m1_subset_1 :::"Element"::: ) "of" (Set (Var "D")) "st" (Bool (Bool (Set (Var "d")) ($#r2_hidden :::"in"::: ) (Set ($#k1_relset_1 :::"dom"::: ) (Set (Var "F"))))) "holds" (Bool (Set ($#k20_rfunct_3 :::"FinS"::: ) "(" (Set (Var "F")) "," (Set ($#k1_tarski :::"{"::: ) (Set (Var "d")) ($#k1_tarski :::"}"::: ) ) ")" ) ($#r1_hidden :::"="::: ) (Set ($#k12_finseq_1 :::"<*"::: ) (Set "(" (Set (Var "F")) ($#k1_seq_1 :::"."::: ) (Set (Var "d")) ")" ) ($#k12_finseq_1 :::"*>"::: ) ))))) ; theorem :: RFUNCT_3:70 (Bool "for" (Set (Var "D")) "being" ($#~v1_xboole_0 "non" ($#v1_xboole_0 :::"empty"::: ) ) ($#m1_hidden :::"set"::: ) (Bool "for" (Set (Var "F")) "being" ($#m1_subset_1 :::"PartFunc":::) "of" (Set (Var "D")) "," (Set ($#k1_numbers :::"REAL"::: ) ) (Bool "for" (Set (Var "X")) "being" ($#m1_hidden :::"set"::: ) (Bool "for" (Set (Var "d")) "being" ($#m1_subset_1 :::"Element"::: ) "of" (Set (Var "D")) "st" (Bool (Bool (Set ($#k1_relset_1 :::"dom"::: ) (Set "(" (Set (Var "F")) ($#k2_partfun1 :::"|"::: ) (Set (Var "X")) ")" )) "is" ($#v1_finset_1 :::"finite"::: ) ) & (Bool (Set (Var "d")) ($#r2_hidden :::"in"::: ) (Set ($#k1_relset_1 :::"dom"::: ) (Set "(" (Set (Var "F")) ($#k2_partfun1 :::"|"::: ) (Set (Var "X")) ")" ))) & (Bool (Set (Set "(" ($#k20_rfunct_3 :::"FinS"::: ) "(" (Set (Var "F")) "," (Set (Var "X")) ")" ")" ) ($#k1_seq_1 :::"."::: ) (Set "(" ($#k3_finseq_1 :::"len"::: ) (Set "(" ($#k20_rfunct_3 :::"FinS"::: ) "(" (Set (Var "F")) "," (Set (Var "X")) ")" ")" ) ")" )) ($#r1_hidden :::"="::: ) (Set (Set (Var "F")) ($#k1_seq_1 :::"."::: ) (Set (Var "d"))))) "holds" (Bool (Set ($#k20_rfunct_3 :::"FinS"::: ) "(" (Set (Var "F")) "," (Set (Var "X")) ")" ) ($#r1_hidden :::"="::: ) (Set (Set "(" ($#k20_rfunct_3 :::"FinS"::: ) "(" (Set (Var "F")) "," (Set "(" (Set (Var "X")) ($#k6_subset_1 :::"\"::: ) (Set ($#k1_tarski :::"{"::: ) (Set (Var "d")) ($#k1_tarski :::"}"::: ) ) ")" ) ")" ")" ) ($#k8_finseq_1 :::"^"::: ) (Set ($#k12_finseq_1 :::"<*"::: ) (Set "(" (Set (Var "F")) ($#k1_seq_1 :::"."::: ) (Set (Var "d")) ")" ) ($#k12_finseq_1 :::"*>"::: ) ))))))) ; theorem :: RFUNCT_3:71 (Bool "for" (Set (Var "D")) "being" ($#~v1_xboole_0 "non" ($#v1_xboole_0 :::"empty"::: ) ) ($#m1_hidden :::"set"::: ) (Bool "for" (Set (Var "F")) "being" ($#m1_subset_1 :::"PartFunc":::) "of" (Set (Var "D")) "," (Set ($#k1_numbers :::"REAL"::: ) ) (Bool "for" (Set (Var "X")) "," (Set (Var "Y")) "being" ($#m1_hidden :::"set"::: ) "st" (Bool (Bool (Set ($#k1_relset_1 :::"dom"::: ) (Set "(" (Set (Var "F")) ($#k2_partfun1 :::"|"::: ) (Set (Var "X")) ")" )) "is" ($#v1_finset_1 :::"finite"::: ) ) & (Bool (Set (Var "Y")) ($#r1_tarski :::"c="::: ) (Set (Var "X"))) & (Bool "(" "for" (Set (Var "d1")) "," (Set (Var "d2")) "being" ($#m1_subset_1 :::"Element"::: ) "of" (Set (Var "D")) "st" (Bool (Bool (Set (Var "d1")) ($#r2_hidden :::"in"::: ) (Set ($#k1_relset_1 :::"dom"::: ) (Set "(" (Set (Var "F")) ($#k2_partfun1 :::"|"::: ) (Set (Var "Y")) ")" ))) & (Bool (Set (Var "d2")) ($#r2_hidden :::"in"::: ) (Set ($#k1_relset_1 :::"dom"::: ) (Set "(" (Set (Var "F")) ($#k2_partfun1 :::"|"::: ) (Set "(" (Set (Var "X")) ($#k6_subset_1 :::"\"::: ) (Set (Var "Y")) ")" ) ")" )))) "holds" (Bool (Set (Set (Var "F")) ($#k1_seq_1 :::"."::: ) (Set (Var "d1"))) ($#r1_xxreal_0 :::">="::: ) (Set (Set (Var "F")) ($#k1_seq_1 :::"."::: ) (Set (Var "d2")))) ")" )) "holds" (Bool (Set ($#k20_rfunct_3 :::"FinS"::: ) "(" (Set (Var "F")) "," (Set (Var "X")) ")" ) ($#r1_hidden :::"="::: ) (Set (Set "(" ($#k20_rfunct_3 :::"FinS"::: ) "(" (Set (Var "F")) "," (Set (Var "Y")) ")" ")" ) ($#k8_finseq_1 :::"^"::: ) (Set "(" ($#k20_rfunct_3 :::"FinS"::: ) "(" (Set (Var "F")) "," (Set "(" (Set (Var "X")) ($#k6_subset_1 :::"\"::: ) (Set (Var "Y")) ")" ) ")" ")" )))))) ; theorem :: RFUNCT_3:72 (Bool "for" (Set (Var "D")) "being" ($#~v1_xboole_0 "non" ($#v1_xboole_0 :::"empty"::: ) ) ($#m1_hidden :::"set"::: ) (Bool "for" (Set (Var "F")) "being" ($#m1_subset_1 :::"PartFunc":::) "of" (Set (Var "D")) "," (Set ($#k1_numbers :::"REAL"::: ) ) (Bool "for" (Set (Var "r")) "being" ($#m1_subset_1 :::"Real":::) (Bool "for" (Set (Var "X")) "being" ($#m1_hidden :::"set"::: ) (Bool "for" (Set (Var "d")) "being" ($#m1_subset_1 :::"Element"::: ) "of" (Set (Var "D")) "st" (Bool (Bool (Set ($#k1_relset_1 :::"dom"::: ) (Set "(" (Set (Var "F")) ($#k2_partfun1 :::"|"::: ) (Set (Var "X")) ")" )) "is" ($#v1_finset_1 :::"finite"::: ) ) & (Bool (Set (Var "d")) ($#r2_hidden :::"in"::: ) (Set ($#k1_relset_1 :::"dom"::: ) (Set "(" (Set (Var "F")) ($#k2_partfun1 :::"|"::: ) (Set (Var "X")) ")" )))) "holds" (Bool "(" (Bool (Set (Set "(" ($#k20_rfunct_3 :::"FinS"::: ) "(" (Set "(" (Set (Var "F")) ($#k15_valued_1 :::"-"::: ) (Set (Var "r")) ")" ) "," (Set (Var "X")) ")" ")" ) ($#k1_seq_1 :::"."::: ) (Set "(" ($#k3_finseq_1 :::"len"::: ) (Set "(" ($#k20_rfunct_3 :::"FinS"::: ) "(" (Set "(" (Set (Var "F")) ($#k15_valued_1 :::"-"::: ) (Set (Var "r")) ")" ) "," (Set (Var "X")) ")" ")" ) ")" )) ($#r1_hidden :::"="::: ) (Set (Set "(" (Set (Var "F")) ($#k15_valued_1 :::"-"::: ) (Set (Var "r")) ")" ) ($#k1_seq_1 :::"."::: ) (Set (Var "d")))) "iff" (Bool (Set (Set "(" ($#k20_rfunct_3 :::"FinS"::: ) "(" (Set (Var "F")) "," (Set (Var "X")) ")" ")" ) ($#k1_seq_1 :::"."::: ) (Set "(" ($#k3_finseq_1 :::"len"::: ) (Set "(" ($#k20_rfunct_3 :::"FinS"::: ) "(" (Set (Var "F")) "," (Set (Var "X")) ")" ")" ) ")" )) ($#r1_hidden :::"="::: ) (Set (Set (Var "F")) ($#k1_seq_1 :::"."::: ) (Set (Var "d")))) ")" )))))) ; theorem :: RFUNCT_3:73 (Bool "for" (Set (Var "D")) "being" ($#~v1_xboole_0 "non" ($#v1_xboole_0 :::"empty"::: ) ) ($#m1_hidden :::"set"::: ) (Bool "for" (Set (Var "F")) "being" ($#m1_subset_1 :::"PartFunc":::) "of" (Set (Var "D")) "," (Set ($#k1_numbers :::"REAL"::: ) ) (Bool "for" (Set (Var "r")) "being" ($#m1_subset_1 :::"Real":::) (Bool "for" (Set (Var "X")) "being" ($#m1_hidden :::"set"::: ) (Bool "for" (Set (Var "Z")) "being" ($#v1_finset_1 :::"finite"::: ) ($#m1_hidden :::"set"::: ) "st" (Bool (Bool (Set (Var "Z")) ($#r1_hidden :::"="::: ) (Set ($#k1_relset_1 :::"dom"::: ) (Set "(" (Set (Var "F")) ($#k2_partfun1 :::"|"::: ) (Set (Var "X")) ")" )))) "holds" (Bool (Set ($#k20_rfunct_3 :::"FinS"::: ) "(" (Set "(" (Set (Var "F")) ($#k15_valued_1 :::"-"::: ) (Set (Var "r")) ")" ) "," (Set (Var "X")) ")" ) ($#r1_hidden :::"="::: ) (Set (Set "(" ($#k20_rfunct_3 :::"FinS"::: ) "(" (Set (Var "F")) "," (Set (Var "X")) ")" ")" ) ($#k8_rvsum_1 :::"-"::: ) (Set "(" (Set "(" ($#k5_card_1 :::"card"::: ) (Set (Var "Z")) ")" ) ($#k5_finseq_2 :::"|->"::: ) (Set (Var "r")) ")" )))))))) ; theorem :: RFUNCT_3:74 (Bool "for" (Set (Var "D")) "being" ($#~v1_xboole_0 "non" ($#v1_xboole_0 :::"empty"::: ) ) ($#m1_hidden :::"set"::: ) (Bool "for" (Set (Var "F")) "being" ($#m1_subset_1 :::"PartFunc":::) "of" (Set (Var "D")) "," (Set ($#k1_numbers :::"REAL"::: ) ) (Bool "for" (Set (Var "X")) "being" ($#m1_hidden :::"set"::: ) "st" (Bool (Bool (Set ($#k1_relset_1 :::"dom"::: ) (Set "(" (Set (Var "F")) ($#k2_partfun1 :::"|"::: ) (Set (Var "X")) ")" )) "is" ($#v1_finset_1 :::"finite"::: ) ) & (Bool "(" "for" (Set (Var "d")) "being" ($#m1_subset_1 :::"Element"::: ) "of" (Set (Var "D")) "st" (Bool (Bool (Set (Var "d")) ($#r2_hidden :::"in"::: ) (Set ($#k1_relset_1 :::"dom"::: ) (Set "(" (Set (Var "F")) ($#k2_partfun1 :::"|"::: ) (Set (Var "X")) ")" )))) "holds" (Bool (Set (Set (Var "F")) ($#k1_seq_1 :::"."::: ) (Set (Var "d"))) ($#r1_xxreal_0 :::">="::: ) (Set ($#k6_numbers :::"0"::: ) )) ")" )) "holds" (Bool (Set ($#k20_rfunct_3 :::"FinS"::: ) "(" (Set "(" ($#k18_rfunct_3 :::"max+"::: ) (Set (Var "F")) ")" ) "," (Set (Var "X")) ")" ) ($#r1_hidden :::"="::: ) (Set ($#k20_rfunct_3 :::"FinS"::: ) "(" (Set (Var "F")) "," (Set (Var "X")) ")" ))))) ; theorem :: RFUNCT_3:75 (Bool "for" (Set (Var "D")) "being" ($#~v1_xboole_0 "non" ($#v1_xboole_0 :::"empty"::: ) ) ($#m1_hidden :::"set"::: ) (Bool "for" (Set (Var "F")) "being" ($#m1_subset_1 :::"PartFunc":::) "of" (Set (Var "D")) "," (Set ($#k1_numbers :::"REAL"::: ) ) (Bool "for" (Set (Var "X")) "being" ($#m1_hidden :::"set"::: ) (Bool "for" (Set (Var "r")) "being" ($#m1_subset_1 :::"Real":::) (Bool "for" (Set (Var "Z")) "being" ($#v1_finset_1 :::"finite"::: ) ($#m1_hidden :::"set"::: ) "st" (Bool (Bool (Set (Var "Z")) ($#r1_hidden :::"="::: ) (Set ($#k1_relset_1 :::"dom"::: ) (Set "(" (Set (Var "F")) ($#k2_partfun1 :::"|"::: ) (Set (Var "X")) ")" ))) & (Bool (Set ($#k1_rvsum_1 :::"rng"::: ) (Set "(" (Set (Var "F")) ($#k2_partfun1 :::"|"::: ) (Set (Var "X")) ")" )) ($#r1_hidden :::"="::: ) (Set ($#k1_tarski :::"{"::: ) (Set (Var "r")) ($#k1_tarski :::"}"::: ) ))) "holds" (Bool (Set ($#k20_rfunct_3 :::"FinS"::: ) "(" (Set (Var "F")) "," (Set (Var "X")) ")" ) ($#r1_hidden :::"="::: ) (Set (Set "(" ($#k5_card_1 :::"card"::: ) (Set (Var "Z")) ")" ) ($#k5_finseq_2 :::"|->"::: ) (Set (Var "r"))))))))) ; theorem :: RFUNCT_3:76 (Bool "for" (Set (Var "D")) "being" ($#~v1_xboole_0 "non" ($#v1_xboole_0 :::"empty"::: ) ) ($#m1_hidden :::"set"::: ) (Bool "for" (Set (Var "F")) "being" ($#m1_subset_1 :::"PartFunc":::) "of" (Set (Var "D")) "," (Set ($#k1_numbers :::"REAL"::: ) ) (Bool "for" (Set (Var "X")) "," (Set (Var "Y")) "being" ($#m1_hidden :::"set"::: ) "st" (Bool (Bool (Set ($#k1_relset_1 :::"dom"::: ) (Set "(" (Set (Var "F")) ($#k2_partfun1 :::"|"::: ) (Set "(" (Set (Var "X")) ($#k2_xboole_0 :::"\/"::: ) (Set (Var "Y")) ")" ) ")" )) "is" ($#v1_finset_1 :::"finite"::: ) ) & (Bool (Set (Var "X")) ($#r1_xboole_0 :::"misses"::: ) (Set (Var "Y")))) "holds" (Bool (Set ($#k20_rfunct_3 :::"FinS"::: ) "(" (Set (Var "F")) "," (Set "(" (Set (Var "X")) ($#k2_xboole_0 :::"\/"::: ) (Set (Var "Y")) ")" ) ")" ) "," (Set (Set "(" ($#k20_rfunct_3 :::"FinS"::: ) "(" (Set (Var "F")) "," (Set (Var "X")) ")" ")" ) ($#k8_finseq_1 :::"^"::: ) (Set "(" ($#k20_rfunct_3 :::"FinS"::: ) "(" (Set (Var "F")) "," (Set (Var "Y")) ")" ")" )) ($#r2_classes1 :::"are_fiberwise_equipotent"::: ) )))) ; definitionlet "D" be ($#~v1_xboole_0 "non" ($#v1_xboole_0 :::"empty"::: ) ) ($#m1_hidden :::"set"::: ) ; let "F" be ($#m1_subset_1 :::"PartFunc":::) "of" (Set (Const "D")) "," (Set ($#k1_numbers :::"REAL"::: ) ); let "X" be ($#m1_hidden :::"set"::: ) ; func :::"Sum"::: "(" "F" "," "X" ")" -> ($#m1_subset_1 :::"Real":::) equals :: RFUNCT_3:def 14 (Set ($#k18_rvsum_1 :::"Sum"::: ) (Set "(" ($#k20_rfunct_3 :::"FinS"::: ) "(" "F" "," "X" ")" ")" )); end; :: deftheorem defines :::"Sum"::: RFUNCT_3:def 14 : (Bool "for" (Set (Var "D")) "being" ($#~v1_xboole_0 "non" ($#v1_xboole_0 :::"empty"::: ) ) ($#m1_hidden :::"set"::: ) (Bool "for" (Set (Var "F")) "being" ($#m1_subset_1 :::"PartFunc":::) "of" (Set (Var "D")) "," (Set ($#k1_numbers :::"REAL"::: ) ) (Bool "for" (Set (Var "X")) "being" ($#m1_hidden :::"set"::: ) "holds" (Bool (Set ($#k21_rfunct_3 :::"Sum"::: ) "(" (Set (Var "F")) "," (Set (Var "X")) ")" ) ($#r1_hidden :::"="::: ) (Set ($#k18_rvsum_1 :::"Sum"::: ) (Set "(" ($#k20_rfunct_3 :::"FinS"::: ) "(" (Set (Var "F")) "," (Set (Var "X")) ")" ")" )))))); theorem :: RFUNCT_3:77 (Bool "for" (Set (Var "D")) "being" ($#~v1_xboole_0 "non" ($#v1_xboole_0 :::"empty"::: ) ) ($#m1_hidden :::"set"::: ) (Bool "for" (Set (Var "F")) "being" ($#m1_subset_1 :::"PartFunc":::) "of" (Set (Var "D")) "," (Set ($#k1_numbers :::"REAL"::: ) ) (Bool "for" (Set (Var "X")) "being" ($#m1_hidden :::"set"::: ) (Bool "for" (Set (Var "r")) "being" ($#m1_subset_1 :::"Real":::) "st" (Bool (Bool (Set ($#k1_relset_1 :::"dom"::: ) (Set "(" (Set (Var "F")) ($#k2_partfun1 :::"|"::: ) (Set (Var "X")) ")" )) "is" ($#v1_finset_1 :::"finite"::: ) )) "holds" (Bool (Set ($#k21_rfunct_3 :::"Sum"::: ) "(" (Set "(" (Set (Var "r")) ($#k26_valued_1 :::"(#)"::: ) (Set (Var "F")) ")" ) "," (Set (Var "X")) ")" ) ($#r1_hidden :::"="::: ) (Set (Set (Var "r")) ($#k8_real_1 :::"*"::: ) (Set "(" ($#k21_rfunct_3 :::"Sum"::: ) "(" (Set (Var "F")) "," (Set (Var "X")) ")" ")" ))))))) ; theorem :: RFUNCT_3:78 (Bool "for" (Set (Var "D")) "being" ($#~v1_xboole_0 "non" ($#v1_xboole_0 :::"empty"::: ) ) ($#m1_hidden :::"set"::: ) (Bool "for" (Set (Var "F")) "," (Set (Var "G")) "being" ($#m1_subset_1 :::"PartFunc":::) "of" (Set (Var "D")) "," (Set ($#k1_numbers :::"REAL"::: ) ) (Bool "for" (Set (Var "X")) "being" ($#m1_hidden :::"set"::: ) (Bool "for" (Set (Var "Y")) "being" ($#v1_finset_1 :::"finite"::: ) ($#m1_hidden :::"set"::: ) "st" (Bool (Bool (Set (Var "Y")) ($#r1_hidden :::"="::: ) (Set ($#k1_relset_1 :::"dom"::: ) (Set "(" (Set (Var "F")) ($#k2_partfun1 :::"|"::: ) (Set (Var "X")) ")" ))) & (Bool (Set ($#k1_relset_1 :::"dom"::: ) (Set "(" (Set (Var "F")) ($#k2_partfun1 :::"|"::: ) (Set (Var "X")) ")" )) ($#r1_hidden :::"="::: ) (Set ($#k1_relset_1 :::"dom"::: ) (Set "(" (Set (Var "G")) ($#k2_partfun1 :::"|"::: ) (Set (Var "X")) ")" )))) "holds" (Bool (Set ($#k21_rfunct_3 :::"Sum"::: ) "(" (Set "(" (Set (Var "F")) ($#k3_valued_1 :::"+"::: ) (Set (Var "G")) ")" ) "," (Set (Var "X")) ")" ) ($#r1_hidden :::"="::: ) (Set (Set "(" ($#k21_rfunct_3 :::"Sum"::: ) "(" (Set (Var "F")) "," (Set (Var "X")) ")" ")" ) ($#k7_real_1 :::"+"::: ) (Set "(" ($#k21_rfunct_3 :::"Sum"::: ) "(" (Set (Var "G")) "," (Set (Var "X")) ")" ")" ))))))) ; theorem :: RFUNCT_3:79 (Bool "for" (Set (Var "D")) "being" ($#~v1_xboole_0 "non" ($#v1_xboole_0 :::"empty"::: ) ) ($#m1_hidden :::"set"::: ) (Bool "for" (Set (Var "F")) "," (Set (Var "G")) "being" ($#m1_subset_1 :::"PartFunc":::) "of" (Set (Var "D")) "," (Set ($#k1_numbers :::"REAL"::: ) ) (Bool "for" (Set (Var "X")) "being" ($#m1_hidden :::"set"::: ) "st" (Bool (Bool (Set ($#k1_relset_1 :::"dom"::: ) (Set "(" (Set (Var "F")) ($#k2_partfun1 :::"|"::: ) (Set (Var "X")) ")" )) "is" ($#v1_finset_1 :::"finite"::: ) ) & (Bool (Set ($#k1_relset_1 :::"dom"::: ) (Set "(" (Set (Var "F")) ($#k2_partfun1 :::"|"::: ) (Set (Var "X")) ")" )) ($#r1_hidden :::"="::: ) (Set ($#k1_relset_1 :::"dom"::: ) (Set "(" (Set (Var "G")) ($#k2_partfun1 :::"|"::: ) (Set (Var "X")) ")" )))) "holds" (Bool (Set ($#k21_rfunct_3 :::"Sum"::: ) "(" (Set "(" (Set (Var "F")) ($#k47_valued_1 :::"-"::: ) (Set (Var "G")) ")" ) "," (Set (Var "X")) ")" ) ($#r1_hidden :::"="::: ) (Set (Set "(" ($#k21_rfunct_3 :::"Sum"::: ) "(" (Set (Var "F")) "," (Set (Var "X")) ")" ")" ) ($#k9_real_1 :::"-"::: ) (Set "(" ($#k21_rfunct_3 :::"Sum"::: ) "(" (Set (Var "G")) "," (Set (Var "X")) ")" ")" )))))) ; theorem :: RFUNCT_3:80 (Bool "for" (Set (Var "D")) "being" ($#~v1_xboole_0 "non" ($#v1_xboole_0 :::"empty"::: ) ) ($#m1_hidden :::"set"::: ) (Bool "for" (Set (Var "F")) "being" ($#m1_subset_1 :::"PartFunc":::) "of" (Set (Var "D")) "," (Set ($#k1_numbers :::"REAL"::: ) ) (Bool "for" (Set (Var "X")) "being" ($#m1_hidden :::"set"::: ) (Bool "for" (Set (Var "r")) "being" ($#m1_subset_1 :::"Real":::) (Bool "for" (Set (Var "Y")) "being" ($#v1_finset_1 :::"finite"::: ) ($#m1_hidden :::"set"::: ) "st" (Bool (Bool (Set (Var "Y")) ($#r1_hidden :::"="::: ) (Set ($#k1_relset_1 :::"dom"::: ) (Set "(" (Set (Var "F")) ($#k2_partfun1 :::"|"::: ) (Set (Var "X")) ")" )))) "holds" (Bool (Set ($#k21_rfunct_3 :::"Sum"::: ) "(" (Set "(" (Set (Var "F")) ($#k15_valued_1 :::"-"::: ) (Set (Var "r")) ")" ) "," (Set (Var "X")) ")" ) ($#r1_hidden :::"="::: ) (Set (Set "(" ($#k21_rfunct_3 :::"Sum"::: ) "(" (Set (Var "F")) "," (Set (Var "X")) ")" ")" ) ($#k9_real_1 :::"-"::: ) (Set "(" (Set (Var "r")) ($#k8_real_1 :::"*"::: ) (Set "(" ($#k5_card_1 :::"card"::: ) (Set (Var "Y")) ")" ) ")" )))))))) ; theorem :: RFUNCT_3:81 (Bool "for" (Set (Var "D")) "being" ($#~v1_xboole_0 "non" ($#v1_xboole_0 :::"empty"::: ) ) ($#m1_hidden :::"set"::: ) (Bool "for" (Set (Var "F")) "being" ($#m1_subset_1 :::"PartFunc":::) "of" (Set (Var "D")) "," (Set ($#k1_numbers :::"REAL"::: ) ) "holds" (Bool (Set ($#k21_rfunct_3 :::"Sum"::: ) "(" (Set (Var "F")) "," (Set ($#k1_xboole_0 :::"{}"::: ) ) ")" ) ($#r1_hidden :::"="::: ) (Set ($#k6_numbers :::"0"::: ) )))) ; theorem :: RFUNCT_3:82 (Bool "for" (Set (Var "D")) "being" ($#~v1_xboole_0 "non" ($#v1_xboole_0 :::"empty"::: ) ) ($#m1_hidden :::"set"::: ) (Bool "for" (Set (Var "F")) "being" ($#m1_subset_1 :::"PartFunc":::) "of" (Set (Var "D")) "," (Set ($#k1_numbers :::"REAL"::: ) ) (Bool "for" (Set (Var "d")) "being" ($#m1_subset_1 :::"Element"::: ) "of" (Set (Var "D")) "st" (Bool (Bool (Set (Var "d")) ($#r2_hidden :::"in"::: ) (Set ($#k1_relset_1 :::"dom"::: ) (Set (Var "F"))))) "holds" (Bool (Set ($#k21_rfunct_3 :::"Sum"::: ) "(" (Set (Var "F")) "," (Set ($#k1_tarski :::"{"::: ) (Set (Var "d")) ($#k1_tarski :::"}"::: ) ) ")" ) ($#r1_hidden :::"="::: ) (Set (Set (Var "F")) ($#k1_seq_1 :::"."::: ) (Set (Var "d"))))))) ; theorem :: RFUNCT_3:83 (Bool "for" (Set (Var "D")) "being" ($#~v1_xboole_0 "non" ($#v1_xboole_0 :::"empty"::: ) ) ($#m1_hidden :::"set"::: ) (Bool "for" (Set (Var "F")) "being" ($#m1_subset_1 :::"PartFunc":::) "of" (Set (Var "D")) "," (Set ($#k1_numbers :::"REAL"::: ) ) (Bool "for" (Set (Var "X")) "," (Set (Var "Y")) "being" ($#m1_hidden :::"set"::: ) "st" (Bool (Bool (Set ($#k1_relset_1 :::"dom"::: ) (Set "(" (Set (Var "F")) ($#k2_partfun1 :::"|"::: ) (Set "(" (Set (Var "X")) ($#k2_xboole_0 :::"\/"::: ) (Set (Var "Y")) ")" ) ")" )) "is" ($#v1_finset_1 :::"finite"::: ) ) & (Bool (Set (Var "X")) ($#r1_xboole_0 :::"misses"::: ) (Set (Var "Y")))) "holds" (Bool (Set ($#k21_rfunct_3 :::"Sum"::: ) "(" (Set (Var "F")) "," (Set "(" (Set (Var "X")) ($#k2_xboole_0 :::"\/"::: ) (Set (Var "Y")) ")" ) ")" ) ($#r1_hidden :::"="::: ) (Set (Set "(" ($#k21_rfunct_3 :::"Sum"::: ) "(" (Set (Var "F")) "," (Set (Var "X")) ")" ")" ) ($#k7_real_1 :::"+"::: ) (Set "(" ($#k21_rfunct_3 :::"Sum"::: ) "(" (Set (Var "F")) "," (Set (Var "Y")) ")" ")" )))))) ; theorem :: RFUNCT_3:84 (Bool "for" (Set (Var "D")) "being" ($#~v1_xboole_0 "non" ($#v1_xboole_0 :::"empty"::: ) ) ($#m1_hidden :::"set"::: ) (Bool "for" (Set (Var "F")) "being" ($#m1_subset_1 :::"PartFunc":::) "of" (Set (Var "D")) "," (Set ($#k1_numbers :::"REAL"::: ) ) (Bool "for" (Set (Var "X")) "," (Set (Var "Y")) "being" ($#m1_hidden :::"set"::: ) "st" (Bool (Bool (Set ($#k1_relset_1 :::"dom"::: ) (Set "(" (Set (Var "F")) ($#k2_partfun1 :::"|"::: ) (Set "(" (Set (Var "X")) ($#k2_xboole_0 :::"\/"::: ) (Set (Var "Y")) ")" ) ")" )) "is" ($#v1_finset_1 :::"finite"::: ) ) & (Bool (Set ($#k1_relset_1 :::"dom"::: ) (Set "(" (Set (Var "F")) ($#k2_partfun1 :::"|"::: ) (Set (Var "X")) ")" )) ($#r1_xboole_0 :::"misses"::: ) (Set ($#k1_relset_1 :::"dom"::: ) (Set "(" (Set (Var "F")) ($#k2_partfun1 :::"|"::: ) (Set (Var "Y")) ")" )))) "holds" (Bool (Set ($#k21_rfunct_3 :::"Sum"::: ) "(" (Set (Var "F")) "," (Set "(" (Set (Var "X")) ($#k2_xboole_0 :::"\/"::: ) (Set (Var "Y")) ")" ) ")" ) ($#r1_hidden :::"="::: ) (Set (Set "(" ($#k21_rfunct_3 :::"Sum"::: ) "(" (Set (Var "F")) "," (Set (Var "X")) ")" ")" ) ($#k7_real_1 :::"+"::: ) (Set "(" ($#k21_rfunct_3 :::"Sum"::: ) "(" (Set (Var "F")) "," (Set (Var "Y")) ")" ")" )))))) ;