:: RFUNCT_2 semantic presentation begin theorem :: RFUNCT_2:1 (Bool "for" (Set (Var "seq1")) "," (Set (Var "seq2")) "," (Set (Var "seq3")) "being" ($#m1_subset_1 :::"Real_Sequence":::) "holds" (Bool "(" (Bool (Set (Var "seq1")) ($#r2_relset_1 :::"="::: ) (Set (Set (Var "seq2")) ($#k47_valued_1 :::"-"::: ) (Set (Var "seq3")))) "iff" (Bool "for" (Set (Var "n")) "being" ($#m2_subset_1 :::"Element"::: ) "of" (Set ($#k5_numbers :::"NAT"::: ) ) "holds" (Bool (Set (Set (Var "seq1")) ($#k1_seq_1 :::"."::: ) (Set (Var "n"))) ($#r1_hidden :::"="::: ) (Set (Set "(" (Set (Var "seq2")) ($#k1_seq_1 :::"."::: ) (Set (Var "n")) ")" ) ($#k9_real_1 :::"-"::: ) (Set "(" (Set (Var "seq3")) ($#k1_seq_1 :::"."::: ) (Set (Var "n")) ")" )))) ")" )) ; theorem :: RFUNCT_2:2 (Bool "for" (Set (Var "seq1")) "," (Set (Var "seq2")) "being" ($#m1_subset_1 :::"Real_Sequence":::) (Bool "for" (Set (Var "Ns")) "being" bbbadV5_VALUED_0() ($#m1_subset_1 :::"sequence":::) "of" (Set ($#k5_numbers :::"NAT"::: ) ) "holds" (Bool "(" (Bool (Set (Set "(" (Set (Var "seq1")) ($#k3_valued_1 :::"+"::: ) (Set (Var "seq2")) ")" ) ($#k2_valued_0 :::"*"::: ) (Set (Var "Ns"))) ($#r2_relset_1 :::"="::: ) (Set (Set "(" (Set (Var "seq1")) ($#k2_valued_0 :::"*"::: ) (Set (Var "Ns")) ")" ) ($#k3_valued_1 :::"+"::: ) (Set "(" (Set (Var "seq2")) ($#k2_valued_0 :::"*"::: ) (Set (Var "Ns")) ")" ))) & (Bool (Set (Set "(" (Set (Var "seq1")) ($#k47_valued_1 :::"-"::: ) (Set (Var "seq2")) ")" ) ($#k2_valued_0 :::"*"::: ) (Set (Var "Ns"))) ($#r2_relset_1 :::"="::: ) (Set (Set "(" (Set (Var "seq1")) ($#k2_valued_0 :::"*"::: ) (Set (Var "Ns")) ")" ) ($#k47_valued_1 :::"-"::: ) (Set "(" (Set (Var "seq2")) ($#k2_valued_0 :::"*"::: ) (Set (Var "Ns")) ")" ))) & (Bool (Set (Set "(" (Set (Var "seq1")) ($#k20_valued_1 :::"(#)"::: ) (Set (Var "seq2")) ")" ) ($#k2_valued_0 :::"*"::: ) (Set (Var "Ns"))) ($#r2_relset_1 :::"="::: ) (Set (Set "(" (Set (Var "seq1")) ($#k2_valued_0 :::"*"::: ) (Set (Var "Ns")) ")" ) ($#k20_valued_1 :::"(#)"::: ) (Set "(" (Set (Var "seq2")) ($#k2_valued_0 :::"*"::: ) (Set (Var "Ns")) ")" ))) ")" ))) ; theorem :: RFUNCT_2:3 (Bool "for" (Set (Var "p")) "being" ($#m1_subset_1 :::"Element"::: ) "of" (Set ($#k1_numbers :::"REAL"::: ) ) (Bool "for" (Set (Var "seq")) "being" ($#m1_subset_1 :::"Real_Sequence":::) (Bool "for" (Set (Var "Ns")) "being" bbbadV5_VALUED_0() ($#m1_subset_1 :::"sequence":::) "of" (Set ($#k5_numbers :::"NAT"::: ) ) "holds" (Bool (Set (Set "(" (Set (Var "p")) ($#k26_valued_1 :::"(#)"::: ) (Set (Var "seq")) ")" ) ($#k2_valued_0 :::"*"::: ) (Set (Var "Ns"))) ($#r2_relset_1 :::"="::: ) (Set (Set (Var "p")) ($#k26_valued_1 :::"(#)"::: ) (Set "(" (Set (Var "seq")) ($#k2_valued_0 :::"*"::: ) (Set (Var "Ns")) ")" )))))) ; theorem :: RFUNCT_2:4 (Bool "for" (Set (Var "seq")) "being" ($#m1_subset_1 :::"Real_Sequence":::) (Bool "for" (Set (Var "Ns")) "being" bbbadV5_VALUED_0() ($#m1_subset_1 :::"sequence":::) "of" (Set ($#k5_numbers :::"NAT"::: ) ) "holds" (Bool "(" (Bool (Set (Set "(" ($#k32_valued_1 :::"-"::: ) (Set (Var "seq")) ")" ) ($#k2_valued_0 :::"*"::: ) (Set (Var "Ns"))) ($#r2_relset_1 :::"="::: ) (Set ($#k32_valued_1 :::"-"::: ) (Set "(" (Set (Var "seq")) ($#k2_valued_0 :::"*"::: ) (Set (Var "Ns")) ")" ))) & (Bool (Set (Set "(" ($#k56_valued_1 :::"abs"::: ) (Set (Var "seq")) ")" ) ($#k2_valued_0 :::"*"::: ) (Set (Var "Ns"))) ($#r2_relset_1 :::"="::: ) (Set ($#k56_valued_1 :::"abs"::: ) (Set "(" (Set (Var "seq")) ($#k2_valued_0 :::"*"::: ) (Set (Var "Ns")) ")" ))) ")" ))) ; theorem :: RFUNCT_2:5 (Bool "for" (Set (Var "seq")) "being" ($#m1_subset_1 :::"Real_Sequence":::) (Bool "for" (Set (Var "Ns")) "being" bbbadV5_VALUED_0() ($#m1_subset_1 :::"sequence":::) "of" (Set ($#k5_numbers :::"NAT"::: ) ) "holds" (Bool (Set (Set "(" (Set (Var "seq")) ($#k2_valued_0 :::"*"::: ) (Set (Var "Ns")) ")" ) ($#k37_valued_1 :::"""::: ) ) ($#r2_relset_1 :::"="::: ) (Set (Set "(" (Set (Var "seq")) ($#k37_valued_1 :::"""::: ) ")" ) ($#k2_valued_0 :::"*"::: ) (Set (Var "Ns")))))) ; theorem :: RFUNCT_2:6 (Bool "for" (Set (Var "seq1")) "," (Set (Var "seq")) "being" ($#m1_subset_1 :::"Real_Sequence":::) (Bool "for" (Set (Var "Ns")) "being" bbbadV5_VALUED_0() ($#m1_subset_1 :::"sequence":::) "of" (Set ($#k5_numbers :::"NAT"::: ) ) "holds" (Bool (Set (Set "(" (Set (Var "seq1")) ($#k52_valued_1 :::"/""::: ) (Set (Var "seq")) ")" ) ($#k2_valued_0 :::"*"::: ) (Set (Var "Ns"))) ($#r2_relset_1 :::"="::: ) (Set (Set "(" (Set (Var "seq1")) ($#k2_valued_0 :::"*"::: ) (Set (Var "Ns")) ")" ) ($#k52_valued_1 :::"/""::: ) (Set "(" (Set (Var "seq")) ($#k2_valued_0 :::"*"::: ) (Set (Var "Ns")) ")" ))))) ; theorem :: RFUNCT_2:7 (Bool "for" (Set (Var "seq")) "being" ($#m1_subset_1 :::"Real_Sequence":::) "st" (Bool (Bool (Set (Var "seq")) "is" ($#v2_comseq_2 :::"convergent"::: ) ) & (Bool "(" "for" (Set (Var "n")) "being" ($#m2_subset_1 :::"Element"::: ) "of" (Set ($#k5_numbers :::"NAT"::: ) ) "holds" (Bool (Set (Set (Var "seq")) ($#k1_seq_1 :::"."::: ) (Set (Var "n"))) ($#r1_xxreal_0 :::"<="::: ) (Set ($#k6_numbers :::"0"::: ) )) ")" )) "holds" (Bool (Set ($#k2_seq_2 :::"lim"::: ) (Set (Var "seq"))) ($#r1_xxreal_0 :::"<="::: ) (Set ($#k6_numbers :::"0"::: ) ))) ; theorem :: RFUNCT_2:8 (Bool "for" (Set (Var "W")) "being" ($#~v1_xboole_0 "non" ($#v1_xboole_0 :::"empty"::: ) ) ($#m1_hidden :::"set"::: ) (Bool "for" (Set (Var "h1")) "," (Set (Var "h2")) "being" ($#m1_subset_1 :::"PartFunc":::) "of" (Set (Var "W")) "," (Set ($#k1_numbers :::"REAL"::: ) ) (Bool "for" (Set (Var "seq")) "being" ($#m1_subset_1 :::"sequence":::) "of" (Set (Var "W")) "st" (Bool (Bool (Set ($#k2_relset_1 :::"rng"::: ) (Set (Var "seq"))) ($#r1_tarski :::"c="::: ) (Set (Set "(" ($#k1_relset_1 :::"dom"::: ) (Set (Var "h1")) ")" ) ($#k9_subset_1 :::"/\"::: ) (Set "(" ($#k1_relset_1 :::"dom"::: ) (Set (Var "h2")) ")" )))) "holds" (Bool "(" (Bool (Set (Set "(" (Set (Var "h1")) ($#k3_valued_1 :::"+"::: ) (Set (Var "h2")) ")" ) ($#k8_funct_2 :::"/*"::: ) (Set (Var "seq"))) ($#r2_relset_1 :::"="::: ) (Set (Set "(" (Set (Var "h1")) ($#k8_funct_2 :::"/*"::: ) (Set (Var "seq")) ")" ) ($#k3_valued_1 :::"+"::: ) (Set "(" (Set (Var "h2")) ($#k8_funct_2 :::"/*"::: ) (Set (Var "seq")) ")" ))) & (Bool (Set (Set "(" (Set (Var "h1")) ($#k47_valued_1 :::"-"::: ) (Set (Var "h2")) ")" ) ($#k8_funct_2 :::"/*"::: ) (Set (Var "seq"))) ($#r2_relset_1 :::"="::: ) (Set (Set "(" (Set (Var "h1")) ($#k8_funct_2 :::"/*"::: ) (Set (Var "seq")) ")" ) ($#k47_valued_1 :::"-"::: ) (Set "(" (Set (Var "h2")) ($#k8_funct_2 :::"/*"::: ) (Set (Var "seq")) ")" ))) & (Bool (Set (Set "(" (Set (Var "h1")) ($#k20_valued_1 :::"(#)"::: ) (Set (Var "h2")) ")" ) ($#k8_funct_2 :::"/*"::: ) (Set (Var "seq"))) ($#r2_relset_1 :::"="::: ) (Set (Set "(" (Set (Var "h1")) ($#k8_funct_2 :::"/*"::: ) (Set (Var "seq")) ")" ) ($#k20_valued_1 :::"(#)"::: ) (Set "(" (Set (Var "h2")) ($#k8_funct_2 :::"/*"::: ) (Set (Var "seq")) ")" ))) ")" )))) ; theorem :: RFUNCT_2:9 (Bool "for" (Set (Var "W")) "being" ($#~v1_xboole_0 "non" ($#v1_xboole_0 :::"empty"::: ) ) ($#m1_hidden :::"set"::: ) (Bool "for" (Set (Var "h")) "being" ($#m1_subset_1 :::"PartFunc":::) "of" (Set (Var "W")) "," (Set ($#k1_numbers :::"REAL"::: ) ) (Bool "for" (Set (Var "seq")) "being" ($#m1_subset_1 :::"sequence":::) "of" (Set (Var "W")) (Bool "for" (Set (Var "r")) "being" ($#v1_xreal_0 :::"real"::: ) ($#m1_hidden :::"number"::: ) "st" (Bool (Bool (Set ($#k2_relset_1 :::"rng"::: ) (Set (Var "seq"))) ($#r1_tarski :::"c="::: ) (Set ($#k1_relset_1 :::"dom"::: ) (Set (Var "h"))))) "holds" (Bool (Set (Set "(" (Set (Var "r")) ($#k26_valued_1 :::"(#)"::: ) (Set (Var "h")) ")" ) ($#k8_funct_2 :::"/*"::: ) (Set (Var "seq"))) ($#r2_relset_1 :::"="::: ) (Set (Set (Var "r")) ($#k26_valued_1 :::"(#)"::: ) (Set "(" (Set (Var "h")) ($#k8_funct_2 :::"/*"::: ) (Set (Var "seq")) ")" ))))))) ; theorem :: RFUNCT_2:10 (Bool "for" (Set (Var "W")) "being" ($#~v1_xboole_0 "non" ($#v1_xboole_0 :::"empty"::: ) ) ($#m1_hidden :::"set"::: ) (Bool "for" (Set (Var "h")) "being" ($#m1_subset_1 :::"PartFunc":::) "of" (Set (Var "W")) "," (Set ($#k1_numbers :::"REAL"::: ) ) (Bool "for" (Set (Var "seq")) "being" ($#m1_subset_1 :::"sequence":::) "of" (Set (Var "W")) "st" (Bool (Bool (Set ($#k2_relset_1 :::"rng"::: ) (Set (Var "seq"))) ($#r1_tarski :::"c="::: ) (Set ($#k1_relset_1 :::"dom"::: ) (Set (Var "h"))))) "holds" (Bool "(" (Bool (Set ($#k56_valued_1 :::"abs"::: ) (Set "(" (Set (Var "h")) ($#k8_funct_2 :::"/*"::: ) (Set (Var "seq")) ")" )) ($#r2_relset_1 :::"="::: ) (Set (Set "(" ($#k56_valued_1 :::"abs"::: ) (Set (Var "h")) ")" ) ($#k8_funct_2 :::"/*"::: ) (Set (Var "seq")))) & (Bool (Set ($#k32_valued_1 :::"-"::: ) (Set "(" (Set (Var "h")) ($#k8_funct_2 :::"/*"::: ) (Set (Var "seq")) ")" )) ($#r2_relset_1 :::"="::: ) (Set (Set "(" ($#k32_valued_1 :::"-"::: ) (Set (Var "h")) ")" ) ($#k8_funct_2 :::"/*"::: ) (Set (Var "seq")))) ")" )))) ; theorem :: RFUNCT_2:11 (Bool "for" (Set (Var "W")) "being" ($#~v1_xboole_0 "non" ($#v1_xboole_0 :::"empty"::: ) ) ($#m1_hidden :::"set"::: ) (Bool "for" (Set (Var "h")) "being" ($#m1_subset_1 :::"PartFunc":::) "of" (Set (Var "W")) "," (Set ($#k1_numbers :::"REAL"::: ) ) (Bool "for" (Set (Var "seq")) "being" ($#m1_subset_1 :::"sequence":::) "of" (Set (Var "W")) "st" (Bool (Bool (Set ($#k2_relset_1 :::"rng"::: ) (Set (Var "seq"))) ($#r1_tarski :::"c="::: ) (Set ($#k1_relset_1 :::"dom"::: ) (Set "(" (Set (Var "h")) ($#k6_rfunct_1 :::"^"::: ) ")" )))) "holds" (Bool (Set (Set (Var "h")) ($#k8_funct_2 :::"/*"::: ) (Set (Var "seq"))) "is" ($#v2_relat_1 :::"non-zero"::: ) )))) ; theorem :: RFUNCT_2:12 (Bool "for" (Set (Var "W")) "being" ($#~v1_xboole_0 "non" ($#v1_xboole_0 :::"empty"::: ) ) ($#m1_hidden :::"set"::: ) (Bool "for" (Set (Var "h")) "being" ($#m1_subset_1 :::"PartFunc":::) "of" (Set (Var "W")) "," (Set ($#k1_numbers :::"REAL"::: ) ) (Bool "for" (Set (Var "seq")) "being" ($#m1_subset_1 :::"sequence":::) "of" (Set (Var "W")) "st" (Bool (Bool (Set ($#k2_relset_1 :::"rng"::: ) (Set (Var "seq"))) ($#r1_tarski :::"c="::: ) (Set ($#k1_relset_1 :::"dom"::: ) (Set "(" (Set (Var "h")) ($#k6_rfunct_1 :::"^"::: ) ")" )))) "holds" (Bool (Set (Set "(" (Set (Var "h")) ($#k6_rfunct_1 :::"^"::: ) ")" ) ($#k8_funct_2 :::"/*"::: ) (Set (Var "seq"))) ($#r2_relset_1 :::"="::: ) (Set (Set "(" (Set (Var "h")) ($#k8_funct_2 :::"/*"::: ) (Set (Var "seq")) ")" ) ($#k37_valued_1 :::"""::: ) ))))) ; theorem :: RFUNCT_2:13 (Bool "for" (Set (Var "W")) "being" ($#~v1_xboole_0 "non" ($#v1_xboole_0 :::"empty"::: ) ) ($#m1_hidden :::"set"::: ) (Bool "for" (Set (Var "h1")) "," (Set (Var "h2")) "being" ($#m1_subset_1 :::"PartFunc":::) "of" (Set (Var "W")) "," (Set ($#k1_numbers :::"REAL"::: ) ) (Bool "for" (Set (Var "seq")) "being" ($#m1_subset_1 :::"sequence":::) "of" (Set (Var "W")) "st" (Bool (Bool (Set (Var "h1")) "is" ($#v1_partfun1 :::"total"::: ) ) & (Bool (Set (Var "h2")) "is" ($#v1_partfun1 :::"total"::: ) )) "holds" (Bool "(" (Bool (Set (Set "(" (Set (Var "h1")) ($#k3_valued_1 :::"+"::: ) (Set (Var "h2")) ")" ) ($#k8_funct_2 :::"/*"::: ) (Set (Var "seq"))) ($#r2_relset_1 :::"="::: ) (Set (Set "(" (Set (Var "h1")) ($#k8_funct_2 :::"/*"::: ) (Set (Var "seq")) ")" ) ($#k3_valued_1 :::"+"::: ) (Set "(" (Set (Var "h2")) ($#k8_funct_2 :::"/*"::: ) (Set (Var "seq")) ")" ))) & (Bool (Set (Set "(" (Set (Var "h1")) ($#k47_valued_1 :::"-"::: ) (Set (Var "h2")) ")" ) ($#k8_funct_2 :::"/*"::: ) (Set (Var "seq"))) ($#r2_relset_1 :::"="::: ) (Set (Set "(" (Set (Var "h1")) ($#k8_funct_2 :::"/*"::: ) (Set (Var "seq")) ")" ) ($#k47_valued_1 :::"-"::: ) (Set "(" (Set (Var "h2")) ($#k8_funct_2 :::"/*"::: ) (Set (Var "seq")) ")" ))) & (Bool (Set (Set "(" (Set (Var "h1")) ($#k20_valued_1 :::"(#)"::: ) (Set (Var "h2")) ")" ) ($#k8_funct_2 :::"/*"::: ) (Set (Var "seq"))) ($#r2_relset_1 :::"="::: ) (Set (Set "(" (Set (Var "h1")) ($#k8_funct_2 :::"/*"::: ) (Set (Var "seq")) ")" ) ($#k20_valued_1 :::"(#)"::: ) (Set "(" (Set (Var "h2")) ($#k8_funct_2 :::"/*"::: ) (Set (Var "seq")) ")" ))) ")" )))) ; theorem :: RFUNCT_2:14 (Bool "for" (Set (Var "r")) "being" ($#m1_subset_1 :::"Element"::: ) "of" (Set ($#k1_numbers :::"REAL"::: ) ) (Bool "for" (Set (Var "W")) "being" ($#~v1_xboole_0 "non" ($#v1_xboole_0 :::"empty"::: ) ) ($#m1_hidden :::"set"::: ) (Bool "for" (Set (Var "h")) "being" ($#m1_subset_1 :::"PartFunc":::) "of" (Set (Var "W")) "," (Set ($#k1_numbers :::"REAL"::: ) ) (Bool "for" (Set (Var "seq")) "being" ($#m1_subset_1 :::"sequence":::) "of" (Set (Var "W")) "st" (Bool (Bool (Set (Var "h")) "is" ($#v1_partfun1 :::"total"::: ) )) "holds" (Bool (Set (Set "(" (Set (Var "r")) ($#k26_valued_1 :::"(#)"::: ) (Set (Var "h")) ")" ) ($#k8_funct_2 :::"/*"::: ) (Set (Var "seq"))) ($#r2_relset_1 :::"="::: ) (Set (Set (Var "r")) ($#k26_valued_1 :::"(#)"::: ) (Set "(" (Set (Var "h")) ($#k8_funct_2 :::"/*"::: ) (Set (Var "seq")) ")" ))))))) ; theorem :: RFUNCT_2:15 (Bool "for" (Set (Var "X")) "being" ($#m1_hidden :::"set"::: ) (Bool "for" (Set (Var "W")) "being" ($#~v1_xboole_0 "non" ($#v1_xboole_0 :::"empty"::: ) ) ($#m1_hidden :::"set"::: ) (Bool "for" (Set (Var "h")) "being" ($#m1_subset_1 :::"PartFunc":::) "of" (Set (Var "W")) "," (Set ($#k1_numbers :::"REAL"::: ) ) (Bool "for" (Set (Var "seq")) "being" ($#m1_subset_1 :::"sequence":::) "of" (Set (Var "W")) "st" (Bool (Bool (Set ($#k2_relset_1 :::"rng"::: ) (Set (Var "seq"))) ($#r1_tarski :::"c="::: ) (Set ($#k1_relset_1 :::"dom"::: ) (Set "(" (Set (Var "h")) ($#k2_partfun1 :::"|"::: ) (Set (Var "X")) ")" )))) "holds" (Bool (Set ($#k56_valued_1 :::"abs"::: ) (Set "(" (Set "(" (Set (Var "h")) ($#k2_partfun1 :::"|"::: ) (Set (Var "X")) ")" ) ($#k8_funct_2 :::"/*"::: ) (Set (Var "seq")) ")" )) ($#r2_relset_1 :::"="::: ) (Set (Set "(" (Set "(" ($#k56_valued_1 :::"abs"::: ) (Set (Var "h")) ")" ) ($#k2_partfun1 :::"|"::: ) (Set (Var "X")) ")" ) ($#k8_funct_2 :::"/*"::: ) (Set (Var "seq")))))))) ; theorem :: RFUNCT_2:16 (Bool "for" (Set (Var "X")) "being" ($#m1_hidden :::"set"::: ) (Bool "for" (Set (Var "W")) "being" ($#~v1_xboole_0 "non" ($#v1_xboole_0 :::"empty"::: ) ) ($#m1_hidden :::"set"::: ) (Bool "for" (Set (Var "h")) "being" ($#m1_subset_1 :::"PartFunc":::) "of" (Set (Var "W")) "," (Set ($#k1_numbers :::"REAL"::: ) ) (Bool "for" (Set (Var "seq")) "being" ($#m1_subset_1 :::"sequence":::) "of" (Set (Var "W")) "st" (Bool (Bool (Set ($#k2_relset_1 :::"rng"::: ) (Set (Var "seq"))) ($#r1_tarski :::"c="::: ) (Set ($#k1_relset_1 :::"dom"::: ) (Set "(" (Set (Var "h")) ($#k2_partfun1 :::"|"::: ) (Set (Var "X")) ")" ))) & (Bool (Set (Set (Var "h")) ($#k8_relset_1 :::"""::: ) (Set ($#k1_seq_4 :::"{"::: ) (Set ($#k6_numbers :::"0"::: ) ) ($#k1_seq_4 :::"}"::: ) )) ($#r1_hidden :::"="::: ) (Set ($#k1_xboole_0 :::"{}"::: ) ))) "holds" (Bool (Set (Set "(" (Set "(" (Set (Var "h")) ($#k6_rfunct_1 :::"^"::: ) ")" ) ($#k2_partfun1 :::"|"::: ) (Set (Var "X")) ")" ) ($#k8_funct_2 :::"/*"::: ) (Set (Var "seq"))) ($#r2_relset_1 :::"="::: ) (Set (Set "(" (Set "(" (Set (Var "h")) ($#k2_partfun1 :::"|"::: ) (Set (Var "X")) ")" ) ($#k8_funct_2 :::"/*"::: ) (Set (Var "seq")) ")" ) ($#k37_valued_1 :::"""::: ) )))))) ; registrationlet "Z" be ($#m1_hidden :::"set"::: ) ; let "f" be ($#v2_funct_1 :::"one-to-one"::: ) ($#m1_hidden :::"Function":::); cluster (Set "f" ($#k5_relat_1 :::"|"::: ) "Z") -> ($#v2_funct_1 :::"one-to-one"::: ) ; end; theorem :: RFUNCT_2:17 (Bool "for" (Set (Var "X")) "being" ($#m1_hidden :::"set"::: ) (Bool "for" (Set (Var "h")) "being" ($#v2_funct_1 :::"one-to-one"::: ) ($#m1_hidden :::"Function":::) "holds" (Bool (Set (Set "(" (Set (Var "h")) ($#k5_relat_1 :::"|"::: ) (Set (Var "X")) ")" ) ($#k2_funct_1 :::"""::: ) ) ($#r1_hidden :::"="::: ) (Set (Set "(" (Set (Var "h")) ($#k2_funct_1 :::"""::: ) ")" ) ($#k5_relat_1 :::"|"::: ) (Set "(" (Set (Var "h")) ($#k7_relat_1 :::".:"::: ) (Set (Var "X")) ")" ))))) ; theorem :: RFUNCT_2:18 (Bool "for" (Set (Var "W")) "being" ($#~v1_xboole_0 "non" ($#v1_xboole_0 :::"empty"::: ) ) ($#m1_hidden :::"set"::: ) (Bool "for" (Set (Var "h")) "being" ($#m1_subset_1 :::"PartFunc":::) "of" (Set (Var "W")) "," (Set ($#k1_numbers :::"REAL"::: ) ) "st" (Bool (Bool (Set ($#k2_relset_1 :::"rng"::: ) (Set (Var "h"))) "is" ($#v5_xxreal_2 :::"real-bounded"::: ) ) & (Bool (Set ($#k4_seq_4 :::"upper_bound"::: ) (Set "(" ($#k2_relset_1 :::"rng"::: ) (Set (Var "h")) ")" )) ($#r1_hidden :::"="::: ) (Set ($#k5_seq_4 :::"lower_bound"::: ) (Set "(" ($#k2_relset_1 :::"rng"::: ) (Set (Var "h")) ")" )))) "holds" (Bool (Set (Var "h")) "is" bbbadV3_FUNCT_1()))) ; theorem :: RFUNCT_2:19 (Bool "for" (Set (Var "Y")) "being" ($#m1_hidden :::"set"::: ) (Bool "for" (Set (Var "W")) "being" ($#~v1_xboole_0 "non" ($#v1_xboole_0 :::"empty"::: ) ) ($#m1_hidden :::"set"::: ) (Bool "for" (Set (Var "h")) "being" ($#m1_subset_1 :::"PartFunc":::) "of" (Set (Var "W")) "," (Set ($#k1_numbers :::"REAL"::: ) ) "st" (Bool (Bool (Set (Set (Var "h")) ($#k7_relset_1 :::".:"::: ) (Set (Var "Y"))) "is" ($#v5_xxreal_2 :::"real-bounded"::: ) ) & (Bool (Set ($#k4_seq_4 :::"upper_bound"::: ) (Set "(" (Set (Var "h")) ($#k7_relset_1 :::".:"::: ) (Set (Var "Y")) ")" )) ($#r1_hidden :::"="::: ) (Set ($#k5_seq_4 :::"lower_bound"::: ) (Set "(" (Set (Var "h")) ($#k7_relset_1 :::".:"::: ) (Set (Var "Y")) ")" )))) "holds" (Bool (Set (Set (Var "h")) ($#k2_partfun1 :::"|"::: ) (Set (Var "Y"))) "is" bbbadV3_FUNCT_1())))) ; definitionlet "h" be ($#m1_subset_1 :::"PartFunc":::) "of" (Set ($#k1_numbers :::"REAL"::: ) ) "," (Set ($#k1_numbers :::"REAL"::: ) ); redefine attr "h" is :::"increasing"::: means :: RFUNCT_2:def 1 (Bool "for" (Set (Var "r1")) "," (Set (Var "r2")) "being" ($#m1_subset_1 :::"Element"::: ) "of" (Set ($#k1_numbers :::"REAL"::: ) ) "st" (Bool (Bool (Set (Var "r1")) ($#r2_hidden :::"in"::: ) (Set ($#k1_relset_1 :::"dom"::: ) "h")) & (Bool (Set (Var "r2")) ($#r2_hidden :::"in"::: ) (Set ($#k1_relset_1 :::"dom"::: ) "h")) & (Bool (Set (Var "r1")) ($#r1_xxreal_0 :::"<"::: ) (Set (Var "r2")))) "holds" (Bool (Set "h" ($#k1_seq_1 :::"."::: ) (Set (Var "r1"))) ($#r1_xxreal_0 :::"<"::: ) (Set "h" ($#k1_seq_1 :::"."::: ) (Set (Var "r2"))))); redefine attr "h" is :::"decreasing"::: means :: RFUNCT_2:def 2 (Bool "for" (Set (Var "r1")) "," (Set (Var "r2")) "being" ($#m1_subset_1 :::"Element"::: ) "of" (Set ($#k1_numbers :::"REAL"::: ) ) "st" (Bool (Bool (Set (Var "r1")) ($#r2_hidden :::"in"::: ) (Set ($#k1_relset_1 :::"dom"::: ) "h")) & (Bool (Set (Var "r2")) ($#r2_hidden :::"in"::: ) (Set ($#k1_relset_1 :::"dom"::: ) "h")) & (Bool (Set (Var "r1")) ($#r1_xxreal_0 :::"<"::: ) (Set (Var "r2")))) "holds" (Bool (Set "h" ($#k1_seq_1 :::"."::: ) (Set (Var "r2"))) ($#r1_xxreal_0 :::"<"::: ) (Set "h" ($#k1_seq_1 :::"."::: ) (Set (Var "r1"))))); redefine attr "h" is :::"non-decreasing"::: means :: RFUNCT_2:def 3 (Bool "for" (Set (Var "r1")) "," (Set (Var "r2")) "being" ($#m1_subset_1 :::"Element"::: ) "of" (Set ($#k1_numbers :::"REAL"::: ) ) "st" (Bool (Bool (Set (Var "r1")) ($#r2_hidden :::"in"::: ) (Set ($#k1_relset_1 :::"dom"::: ) "h")) & (Bool (Set (Var "r2")) ($#r2_hidden :::"in"::: ) (Set ($#k1_relset_1 :::"dom"::: ) "h")) & (Bool (Set (Var "r1")) ($#r1_xxreal_0 :::"<"::: ) (Set (Var "r2")))) "holds" (Bool (Set "h" ($#k1_seq_1 :::"."::: ) (Set (Var "r1"))) ($#r1_xxreal_0 :::"<="::: ) (Set "h" ($#k1_seq_1 :::"."::: ) (Set (Var "r2"))))); redefine attr "h" is :::"non-increasing"::: means :: RFUNCT_2:def 4 (Bool "for" (Set (Var "r1")) "," (Set (Var "r2")) "being" ($#m1_subset_1 :::"Element"::: ) "of" (Set ($#k1_numbers :::"REAL"::: ) ) "st" (Bool (Bool (Set (Var "r1")) ($#r2_hidden :::"in"::: ) (Set ($#k1_relset_1 :::"dom"::: ) "h")) & (Bool (Set (Var "r2")) ($#r2_hidden :::"in"::: ) (Set ($#k1_relset_1 :::"dom"::: ) "h")) & (Bool (Set (Var "r1")) ($#r1_xxreal_0 :::"<"::: ) (Set (Var "r2")))) "holds" (Bool (Set "h" ($#k1_seq_1 :::"."::: ) (Set (Var "r2"))) ($#r1_xxreal_0 :::"<="::: ) (Set "h" ($#k1_seq_1 :::"."::: ) (Set (Var "r1"))))); end; :: deftheorem defines :::"increasing"::: RFUNCT_2:def 1 : (Bool "for" (Set (Var "h")) "being" ($#m1_subset_1 :::"PartFunc":::) "of" (Set ($#k1_numbers :::"REAL"::: ) ) "," (Set ($#k1_numbers :::"REAL"::: ) ) "holds" (Bool "(" (Bool (Set (Var "h")) "is" ($#v5_valued_0 :::"increasing"::: ) ) "iff" (Bool "for" (Set (Var "r1")) "," (Set (Var "r2")) "being" ($#m1_subset_1 :::"Element"::: ) "of" (Set ($#k1_numbers :::"REAL"::: ) ) "st" (Bool (Bool (Set (Var "r1")) ($#r2_hidden :::"in"::: ) (Set ($#k1_relset_1 :::"dom"::: ) (Set (Var "h")))) & (Bool (Set (Var "r2")) ($#r2_hidden :::"in"::: ) (Set ($#k1_relset_1 :::"dom"::: ) (Set (Var "h")))) & (Bool (Set (Var "r1")) ($#r1_xxreal_0 :::"<"::: ) (Set (Var "r2")))) "holds" (Bool (Set (Set (Var "h")) ($#k1_seq_1 :::"."::: ) (Set (Var "r1"))) ($#r1_xxreal_0 :::"<"::: ) (Set (Set (Var "h")) ($#k1_seq_1 :::"."::: ) (Set (Var "r2"))))) ")" )); :: deftheorem defines :::"decreasing"::: RFUNCT_2:def 2 : (Bool "for" (Set (Var "h")) "being" ($#m1_subset_1 :::"PartFunc":::) "of" (Set ($#k1_numbers :::"REAL"::: ) ) "," (Set ($#k1_numbers :::"REAL"::: ) ) "holds" (Bool "(" (Bool (Set (Var "h")) "is" ($#v6_valued_0 :::"decreasing"::: ) ) "iff" (Bool "for" (Set (Var "r1")) "," (Set (Var "r2")) "being" ($#m1_subset_1 :::"Element"::: ) "of" (Set ($#k1_numbers :::"REAL"::: ) ) "st" (Bool (Bool (Set (Var "r1")) ($#r2_hidden :::"in"::: ) (Set ($#k1_relset_1 :::"dom"::: ) (Set (Var "h")))) & (Bool (Set (Var "r2")) ($#r2_hidden :::"in"::: ) (Set ($#k1_relset_1 :::"dom"::: ) (Set (Var "h")))) & (Bool (Set (Var "r1")) ($#r1_xxreal_0 :::"<"::: ) (Set (Var "r2")))) "holds" (Bool (Set (Set (Var "h")) ($#k1_seq_1 :::"."::: ) (Set (Var "r2"))) ($#r1_xxreal_0 :::"<"::: ) (Set (Set (Var "h")) ($#k1_seq_1 :::"."::: ) (Set (Var "r1"))))) ")" )); :: deftheorem defines :::"non-decreasing"::: RFUNCT_2:def 3 : (Bool "for" (Set (Var "h")) "being" ($#m1_subset_1 :::"PartFunc":::) "of" (Set ($#k1_numbers :::"REAL"::: ) ) "," (Set ($#k1_numbers :::"REAL"::: ) ) "holds" (Bool "(" (Bool (Set (Var "h")) "is" ($#v7_valued_0 :::"non-decreasing"::: ) ) "iff" (Bool "for" (Set (Var "r1")) "," (Set (Var "r2")) "being" ($#m1_subset_1 :::"Element"::: ) "of" (Set ($#k1_numbers :::"REAL"::: ) ) "st" (Bool (Bool (Set (Var "r1")) ($#r2_hidden :::"in"::: ) (Set ($#k1_relset_1 :::"dom"::: ) (Set (Var "h")))) & (Bool (Set (Var "r2")) ($#r2_hidden :::"in"::: ) (Set ($#k1_relset_1 :::"dom"::: ) (Set (Var "h")))) & (Bool (Set (Var "r1")) ($#r1_xxreal_0 :::"<"::: ) (Set (Var "r2")))) "holds" (Bool (Set (Set (Var "h")) ($#k1_seq_1 :::"."::: ) (Set (Var "r1"))) ($#r1_xxreal_0 :::"<="::: ) (Set (Set (Var "h")) ($#k1_seq_1 :::"."::: ) (Set (Var "r2"))))) ")" )); :: deftheorem defines :::"non-increasing"::: RFUNCT_2:def 4 : (Bool "for" (Set (Var "h")) "being" ($#m1_subset_1 :::"PartFunc":::) "of" (Set ($#k1_numbers :::"REAL"::: ) ) "," (Set ($#k1_numbers :::"REAL"::: ) ) "holds" (Bool "(" (Bool (Set (Var "h")) "is" ($#v8_valued_0 :::"non-increasing"::: ) ) "iff" (Bool "for" (Set (Var "r1")) "," (Set (Var "r2")) "being" ($#m1_subset_1 :::"Element"::: ) "of" (Set ($#k1_numbers :::"REAL"::: ) ) "st" (Bool (Bool (Set (Var "r1")) ($#r2_hidden :::"in"::: ) (Set ($#k1_relset_1 :::"dom"::: ) (Set (Var "h")))) & (Bool (Set (Var "r2")) ($#r2_hidden :::"in"::: ) (Set ($#k1_relset_1 :::"dom"::: ) (Set (Var "h")))) & (Bool (Set (Var "r1")) ($#r1_xxreal_0 :::"<"::: ) (Set (Var "r2")))) "holds" (Bool (Set (Set (Var "h")) ($#k1_seq_1 :::"."::: ) (Set (Var "r2"))) ($#r1_xxreal_0 :::"<="::: ) (Set (Set (Var "h")) ($#k1_seq_1 :::"."::: ) (Set (Var "r1"))))) ")" )); theorem :: RFUNCT_2:20 (Bool "for" (Set (Var "Y")) "being" ($#m1_hidden :::"set"::: ) (Bool "for" (Set (Var "h")) "being" ($#m1_subset_1 :::"PartFunc":::) "of" (Set ($#k1_numbers :::"REAL"::: ) ) "," (Set ($#k1_numbers :::"REAL"::: ) ) "holds" (Bool "(" (Bool (Set (Set (Var "h")) ($#k2_partfun1 :::"|"::: ) (Set (Var "Y"))) "is" ($#v5_valued_0 :::"increasing"::: ) ) "iff" (Bool "for" (Set (Var "r1")) "," (Set (Var "r2")) "being" ($#m1_subset_1 :::"Element"::: ) "of" (Set ($#k1_numbers :::"REAL"::: ) ) "st" (Bool (Bool (Set (Var "r1")) ($#r2_hidden :::"in"::: ) (Set (Set (Var "Y")) ($#k9_subset_1 :::"/\"::: ) (Set "(" ($#k1_relset_1 :::"dom"::: ) (Set (Var "h")) ")" ))) & (Bool (Set (Var "r2")) ($#r2_hidden :::"in"::: ) (Set (Set (Var "Y")) ($#k9_subset_1 :::"/\"::: ) (Set "(" ($#k1_relset_1 :::"dom"::: ) (Set (Var "h")) ")" ))) & (Bool (Set (Var "r1")) ($#r1_xxreal_0 :::"<"::: ) (Set (Var "r2")))) "holds" (Bool (Set (Set (Var "h")) ($#k1_seq_1 :::"."::: ) (Set (Var "r1"))) ($#r1_xxreal_0 :::"<"::: ) (Set (Set (Var "h")) ($#k1_seq_1 :::"."::: ) (Set (Var "r2"))))) ")" ))) ; theorem :: RFUNCT_2:21 (Bool "for" (Set (Var "Y")) "being" ($#m1_hidden :::"set"::: ) (Bool "for" (Set (Var "h")) "being" ($#m1_subset_1 :::"PartFunc":::) "of" (Set ($#k1_numbers :::"REAL"::: ) ) "," (Set ($#k1_numbers :::"REAL"::: ) ) "holds" (Bool "(" (Bool (Set (Set (Var "h")) ($#k2_partfun1 :::"|"::: ) (Set (Var "Y"))) "is" ($#v6_valued_0 :::"decreasing"::: ) ) "iff" (Bool "for" (Set (Var "r1")) "," (Set (Var "r2")) "being" ($#m1_subset_1 :::"Element"::: ) "of" (Set ($#k1_numbers :::"REAL"::: ) ) "st" (Bool (Bool (Set (Var "r1")) ($#r2_hidden :::"in"::: ) (Set (Set (Var "Y")) ($#k9_subset_1 :::"/\"::: ) (Set "(" ($#k1_relset_1 :::"dom"::: ) (Set (Var "h")) ")" ))) & (Bool (Set (Var "r2")) ($#r2_hidden :::"in"::: ) (Set (Set (Var "Y")) ($#k9_subset_1 :::"/\"::: ) (Set "(" ($#k1_relset_1 :::"dom"::: ) (Set (Var "h")) ")" ))) & (Bool (Set (Var "r1")) ($#r1_xxreal_0 :::"<"::: ) (Set (Var "r2")))) "holds" (Bool (Set (Set (Var "h")) ($#k1_seq_1 :::"."::: ) (Set (Var "r2"))) ($#r1_xxreal_0 :::"<"::: ) (Set (Set (Var "h")) ($#k1_seq_1 :::"."::: ) (Set (Var "r1"))))) ")" ))) ; theorem :: RFUNCT_2:22 (Bool "for" (Set (Var "Y")) "being" ($#m1_hidden :::"set"::: ) (Bool "for" (Set (Var "h")) "being" ($#m1_subset_1 :::"PartFunc":::) "of" (Set ($#k1_numbers :::"REAL"::: ) ) "," (Set ($#k1_numbers :::"REAL"::: ) ) "holds" (Bool "(" (Bool (Set (Set (Var "h")) ($#k2_partfun1 :::"|"::: ) (Set (Var "Y"))) "is" ($#v7_valued_0 :::"non-decreasing"::: ) ) "iff" (Bool "for" (Set (Var "r1")) "," (Set (Var "r2")) "being" ($#m1_subset_1 :::"Element"::: ) "of" (Set ($#k1_numbers :::"REAL"::: ) ) "st" (Bool (Bool (Set (Var "r1")) ($#r2_hidden :::"in"::: ) (Set (Set (Var "Y")) ($#k9_subset_1 :::"/\"::: ) (Set "(" ($#k1_relset_1 :::"dom"::: ) (Set (Var "h")) ")" ))) & (Bool (Set (Var "r2")) ($#r2_hidden :::"in"::: ) (Set (Set (Var "Y")) ($#k9_subset_1 :::"/\"::: ) (Set "(" ($#k1_relset_1 :::"dom"::: ) (Set (Var "h")) ")" ))) & (Bool (Set (Var "r1")) ($#r1_xxreal_0 :::"<"::: ) (Set (Var "r2")))) "holds" (Bool (Set (Set (Var "h")) ($#k1_seq_1 :::"."::: ) (Set (Var "r1"))) ($#r1_xxreal_0 :::"<="::: ) (Set (Set (Var "h")) ($#k1_seq_1 :::"."::: ) (Set (Var "r2"))))) ")" ))) ; theorem :: RFUNCT_2:23 (Bool "for" (Set (Var "Y")) "being" ($#m1_hidden :::"set"::: ) (Bool "for" (Set (Var "h")) "being" ($#m1_subset_1 :::"PartFunc":::) "of" (Set ($#k1_numbers :::"REAL"::: ) ) "," (Set ($#k1_numbers :::"REAL"::: ) ) "holds" (Bool "(" (Bool (Set (Set (Var "h")) ($#k2_partfun1 :::"|"::: ) (Set (Var "Y"))) "is" ($#v8_valued_0 :::"non-increasing"::: ) ) "iff" (Bool "for" (Set (Var "r1")) "," (Set (Var "r2")) "being" ($#m1_subset_1 :::"Element"::: ) "of" (Set ($#k1_numbers :::"REAL"::: ) ) "st" (Bool (Bool (Set (Var "r1")) ($#r2_hidden :::"in"::: ) (Set (Set (Var "Y")) ($#k9_subset_1 :::"/\"::: ) (Set "(" ($#k1_relset_1 :::"dom"::: ) (Set (Var "h")) ")" ))) & (Bool (Set (Var "r2")) ($#r2_hidden :::"in"::: ) (Set (Set (Var "Y")) ($#k9_subset_1 :::"/\"::: ) (Set "(" ($#k1_relset_1 :::"dom"::: ) (Set (Var "h")) ")" ))) & (Bool (Set (Var "r1")) ($#r1_xxreal_0 :::"<"::: ) (Set (Var "r2")))) "holds" (Bool (Set (Set (Var "h")) ($#k1_seq_1 :::"."::: ) (Set (Var "r2"))) ($#r1_xxreal_0 :::"<="::: ) (Set (Set (Var "h")) ($#k1_seq_1 :::"."::: ) (Set (Var "r1"))))) ")" ))) ; definitionlet "h" be ($#m1_subset_1 :::"PartFunc":::) "of" (Set ($#k1_numbers :::"REAL"::: ) ) "," (Set ($#k1_numbers :::"REAL"::: ) ); attr "h" is :::"monotone"::: means :: RFUNCT_2:def 5 (Bool "(" (Bool "h" "is" ($#v7_valued_0 :::"non-decreasing"::: ) ) "or" (Bool "h" "is" ($#v8_valued_0 :::"non-increasing"::: ) ) ")" ); end; :: deftheorem defines :::"monotone"::: RFUNCT_2:def 5 : (Bool "for" (Set (Var "h")) "being" ($#m1_subset_1 :::"PartFunc":::) "of" (Set ($#k1_numbers :::"REAL"::: ) ) "," (Set ($#k1_numbers :::"REAL"::: ) ) "holds" (Bool "(" (Bool (Set (Var "h")) "is" ($#v1_rfunct_2 :::"monotone"::: ) ) "iff" (Bool "(" (Bool (Set (Var "h")) "is" ($#v7_valued_0 :::"non-decreasing"::: ) ) "or" (Bool (Set (Var "h")) "is" ($#v8_valued_0 :::"non-increasing"::: ) ) ")" ) ")" )); registration cluster ($#v1_funct_1 :::"Function-like"::: ) ($#v7_valued_0 :::"non-decreasing"::: ) -> ($#v1_rfunct_2 :::"monotone"::: ) for ($#m1_subset_1 :::"Element"::: ) "of" (Set ($#k1_zfmisc_1 :::"bool"::: ) (Set ($#k2_zfmisc_1 :::"[:"::: ) (Set ($#k1_numbers :::"REAL"::: ) ) "," (Set ($#k1_numbers :::"REAL"::: ) ) ($#k2_zfmisc_1 :::":]"::: ) )); cluster ($#v1_funct_1 :::"Function-like"::: ) ($#v8_valued_0 :::"non-increasing"::: ) -> ($#v1_rfunct_2 :::"monotone"::: ) for ($#m1_subset_1 :::"Element"::: ) "of" (Set ($#k1_zfmisc_1 :::"bool"::: ) (Set ($#k2_zfmisc_1 :::"[:"::: ) (Set ($#k1_numbers :::"REAL"::: ) ) "," (Set ($#k1_numbers :::"REAL"::: ) ) ($#k2_zfmisc_1 :::":]"::: ) )); cluster ($#v1_funct_1 :::"Function-like"::: ) ($#~v1_rfunct_2 "non" ($#v1_rfunct_2 :::"monotone"::: ) ) -> ($#~v7_valued_0 "non" ($#v7_valued_0 :::"non-decreasing"::: ) ) ($#~v8_valued_0 "non" ($#v8_valued_0 :::"non-increasing"::: ) ) for ($#m1_subset_1 :::"Element"::: ) "of" (Set ($#k1_zfmisc_1 :::"bool"::: ) (Set ($#k2_zfmisc_1 :::"[:"::: ) (Set ($#k1_numbers :::"REAL"::: ) ) "," (Set ($#k1_numbers :::"REAL"::: ) ) ($#k2_zfmisc_1 :::":]"::: ) )); end; theorem :: RFUNCT_2:24 (Bool "for" (Set (Var "Y")) "being" ($#m1_hidden :::"set"::: ) (Bool "for" (Set (Var "h")) "being" ($#m1_subset_1 :::"PartFunc":::) "of" (Set ($#k1_numbers :::"REAL"::: ) ) "," (Set ($#k1_numbers :::"REAL"::: ) ) "holds" (Bool "(" (Bool (Set (Set (Var "h")) ($#k2_partfun1 :::"|"::: ) (Set (Var "Y"))) "is" ($#v7_valued_0 :::"non-decreasing"::: ) ) "iff" (Bool "for" (Set (Var "r1")) "," (Set (Var "r2")) "being" ($#m1_subset_1 :::"Element"::: ) "of" (Set ($#k1_numbers :::"REAL"::: ) ) "st" (Bool (Bool (Set (Var "r1")) ($#r2_hidden :::"in"::: ) (Set (Set (Var "Y")) ($#k9_subset_1 :::"/\"::: ) (Set "(" ($#k1_relset_1 :::"dom"::: ) (Set (Var "h")) ")" ))) & (Bool (Set (Var "r2")) ($#r2_hidden :::"in"::: ) (Set (Set (Var "Y")) ($#k9_subset_1 :::"/\"::: ) (Set "(" ($#k1_relset_1 :::"dom"::: ) (Set (Var "h")) ")" ))) & (Bool (Set (Var "r1")) ($#r1_xxreal_0 :::"<="::: ) (Set (Var "r2")))) "holds" (Bool (Set (Set (Var "h")) ($#k1_seq_1 :::"."::: ) (Set (Var "r1"))) ($#r1_xxreal_0 :::"<="::: ) (Set (Set (Var "h")) ($#k1_seq_1 :::"."::: ) (Set (Var "r2"))))) ")" ))) ; theorem :: RFUNCT_2:25 (Bool "for" (Set (Var "Y")) "being" ($#m1_hidden :::"set"::: ) (Bool "for" (Set (Var "h")) "being" ($#m1_subset_1 :::"PartFunc":::) "of" (Set ($#k1_numbers :::"REAL"::: ) ) "," (Set ($#k1_numbers :::"REAL"::: ) ) "holds" (Bool "(" (Bool (Set (Set (Var "h")) ($#k2_partfun1 :::"|"::: ) (Set (Var "Y"))) "is" ($#v8_valued_0 :::"non-increasing"::: ) ) "iff" (Bool "for" (Set (Var "r1")) "," (Set (Var "r2")) "being" ($#m1_subset_1 :::"Element"::: ) "of" (Set ($#k1_numbers :::"REAL"::: ) ) "st" (Bool (Bool (Set (Var "r1")) ($#r2_hidden :::"in"::: ) (Set (Set (Var "Y")) ($#k9_subset_1 :::"/\"::: ) (Set "(" ($#k1_relset_1 :::"dom"::: ) (Set (Var "h")) ")" ))) & (Bool (Set (Var "r2")) ($#r2_hidden :::"in"::: ) (Set (Set (Var "Y")) ($#k9_subset_1 :::"/\"::: ) (Set "(" ($#k1_relset_1 :::"dom"::: ) (Set (Var "h")) ")" ))) & (Bool (Set (Var "r1")) ($#r1_xxreal_0 :::"<="::: ) (Set (Var "r2")))) "holds" (Bool (Set (Set (Var "h")) ($#k1_seq_1 :::"."::: ) (Set (Var "r2"))) ($#r1_xxreal_0 :::"<="::: ) (Set (Set (Var "h")) ($#k1_seq_1 :::"."::: ) (Set (Var "r1"))))) ")" ))) ; registration cluster ($#v1_funct_1 :::"Function-like"::: ) ($#v7_valued_0 :::"non-decreasing"::: ) ($#v8_valued_0 :::"non-increasing"::: ) -> bbbadV3_FUNCT_1() for ($#m1_subset_1 :::"Element"::: ) "of" (Set ($#k1_zfmisc_1 :::"bool"::: ) (Set ($#k2_zfmisc_1 :::"[:"::: ) (Set ($#k1_numbers :::"REAL"::: ) ) "," (Set ($#k1_numbers :::"REAL"::: ) ) ($#k2_zfmisc_1 :::":]"::: ) )); end; registration cluster ($#v1_funct_1 :::"Function-like"::: ) bbbadV3_FUNCT_1() -> ($#v7_valued_0 :::"non-decreasing"::: ) ($#v8_valued_0 :::"non-increasing"::: ) for ($#m1_subset_1 :::"Element"::: ) "of" (Set ($#k1_zfmisc_1 :::"bool"::: ) (Set ($#k2_zfmisc_1 :::"[:"::: ) (Set ($#k1_numbers :::"REAL"::: ) ) "," (Set ($#k1_numbers :::"REAL"::: ) ) ($#k2_zfmisc_1 :::":]"::: ) )); end; registration cluster ($#v1_relat_1 :::"Relation-like"::: ) (Set ($#k1_numbers :::"REAL"::: ) ) ($#v4_relat_1 :::"-defined"::: ) (Set ($#k1_numbers :::"REAL"::: ) ) ($#v5_relat_1 :::"-valued"::: ) ($#v1_funct_1 :::"Function-like"::: ) ($#v1_zfmisc_1 :::"trivial"::: ) ($#v1_valued_0 :::"complex-valued"::: ) ($#v2_valued_0 :::"ext-real-valued"::: ) ($#v3_valued_0 :::"real-valued"::: ) for ($#m1_subset_1 :::"Element"::: ) "of" (Set ($#k1_zfmisc_1 :::"bool"::: ) (Set ($#k2_zfmisc_1 :::"[:"::: ) (Set ($#k1_numbers :::"REAL"::: ) ) "," (Set ($#k1_numbers :::"REAL"::: ) ) ($#k2_zfmisc_1 :::":]"::: ) )); end; registrationlet "h" be ($#v5_valued_0 :::"increasing"::: ) ($#m1_subset_1 :::"PartFunc":::) "of" (Set ($#k1_numbers :::"REAL"::: ) ) "," (Set ($#k1_numbers :::"REAL"::: ) ); let "X" be ($#m1_hidden :::"set"::: ) ; cluster (Set "h" ($#k5_relat_1 :::"|"::: ) "X") -> ($#v5_valued_0 :::"increasing"::: ) for ($#m1_subset_1 :::"PartFunc":::) "of" (Set ($#k1_numbers :::"REAL"::: ) ) "," (Set ($#k1_numbers :::"REAL"::: ) ); end; registrationlet "h" be ($#v6_valued_0 :::"decreasing"::: ) ($#m1_subset_1 :::"PartFunc":::) "of" (Set ($#k1_numbers :::"REAL"::: ) ) "," (Set ($#k1_numbers :::"REAL"::: ) ); let "X" be ($#m1_hidden :::"set"::: ) ; cluster (Set "h" ($#k5_relat_1 :::"|"::: ) "X") -> ($#v6_valued_0 :::"decreasing"::: ) for ($#m1_subset_1 :::"PartFunc":::) "of" (Set ($#k1_numbers :::"REAL"::: ) ) "," (Set ($#k1_numbers :::"REAL"::: ) ); end; registrationlet "h" be ($#v7_valued_0 :::"non-decreasing"::: ) ($#m1_subset_1 :::"PartFunc":::) "of" (Set ($#k1_numbers :::"REAL"::: ) ) "," (Set ($#k1_numbers :::"REAL"::: ) ); let "X" be ($#m1_hidden :::"set"::: ) ; cluster (Set "h" ($#k5_relat_1 :::"|"::: ) "X") -> ($#v7_valued_0 :::"non-decreasing"::: ) for ($#m1_subset_1 :::"PartFunc":::) "of" (Set ($#k1_numbers :::"REAL"::: ) ) "," (Set ($#k1_numbers :::"REAL"::: ) ); end; theorem :: RFUNCT_2:26 (Bool "for" (Set (Var "Y")) "being" ($#m1_hidden :::"set"::: ) (Bool "for" (Set (Var "h")) "being" ($#m1_subset_1 :::"PartFunc":::) "of" (Set ($#k1_numbers :::"REAL"::: ) ) "," (Set ($#k1_numbers :::"REAL"::: ) ) "st" (Bool (Bool (Set (Var "Y")) ($#r1_xboole_0 :::"misses"::: ) (Set ($#k1_relset_1 :::"dom"::: ) (Set (Var "h"))))) "holds" (Bool "(" (Bool (Set (Set (Var "h")) ($#k2_partfun1 :::"|"::: ) (Set (Var "Y"))) "is" ($#v5_valued_0 :::"increasing"::: ) ) & (Bool (Set (Set (Var "h")) ($#k2_partfun1 :::"|"::: ) (Set (Var "Y"))) "is" ($#v6_valued_0 :::"decreasing"::: ) ) & (Bool (Set (Set (Var "h")) ($#k2_partfun1 :::"|"::: ) (Set (Var "Y"))) "is" ($#v7_valued_0 :::"non-decreasing"::: ) ) & (Bool (Set (Set (Var "h")) ($#k2_partfun1 :::"|"::: ) (Set (Var "Y"))) "is" ($#v8_valued_0 :::"non-increasing"::: ) ) & (Bool (Set (Set (Var "h")) ($#k2_partfun1 :::"|"::: ) (Set (Var "Y"))) "is" ($#v1_rfunct_2 :::"monotone"::: ) ) ")" ))) ; theorem :: RFUNCT_2:27 (Bool "for" (Set (Var "Y")) "," (Set (Var "X")) "being" ($#m1_hidden :::"set"::: ) (Bool "for" (Set (Var "h")) "being" ($#m1_subset_1 :::"PartFunc":::) "of" (Set ($#k1_numbers :::"REAL"::: ) ) "," (Set ($#k1_numbers :::"REAL"::: ) ) "st" (Bool (Bool (Set (Set (Var "h")) ($#k2_partfun1 :::"|"::: ) (Set (Var "Y"))) "is" ($#v7_valued_0 :::"non-decreasing"::: ) ) & (Bool (Set (Set (Var "h")) ($#k2_partfun1 :::"|"::: ) (Set (Var "X"))) "is" ($#v8_valued_0 :::"non-increasing"::: ) )) "holds" (Bool (Set (Set (Var "h")) ($#k2_partfun1 :::"|"::: ) (Set "(" (Set (Var "Y")) ($#k3_xboole_0 :::"/\"::: ) (Set (Var "X")) ")" )) "is" bbbadV3_FUNCT_1()))) ; theorem :: RFUNCT_2:28 (Bool "for" (Set (Var "X")) "," (Set (Var "Y")) "being" ($#m1_hidden :::"set"::: ) (Bool "for" (Set (Var "h")) "being" ($#m1_subset_1 :::"PartFunc":::) "of" (Set ($#k1_numbers :::"REAL"::: ) ) "," (Set ($#k1_numbers :::"REAL"::: ) ) "st" (Bool (Bool (Set (Var "X")) ($#r1_tarski :::"c="::: ) (Set (Var "Y"))) & (Bool (Set (Set (Var "h")) ($#k2_partfun1 :::"|"::: ) (Set (Var "Y"))) "is" ($#v5_valued_0 :::"increasing"::: ) )) "holds" (Bool (Set (Set (Var "h")) ($#k2_partfun1 :::"|"::: ) (Set (Var "X"))) "is" ($#v5_valued_0 :::"increasing"::: ) ))) ; theorem :: RFUNCT_2:29 (Bool "for" (Set (Var "X")) "," (Set (Var "Y")) "being" ($#m1_hidden :::"set"::: ) (Bool "for" (Set (Var "h")) "being" ($#m1_subset_1 :::"PartFunc":::) "of" (Set ($#k1_numbers :::"REAL"::: ) ) "," (Set ($#k1_numbers :::"REAL"::: ) ) "st" (Bool (Bool (Set (Var "X")) ($#r1_tarski :::"c="::: ) (Set (Var "Y"))) & (Bool (Set (Set (Var "h")) ($#k2_partfun1 :::"|"::: ) (Set (Var "Y"))) "is" ($#v6_valued_0 :::"decreasing"::: ) )) "holds" (Bool (Set (Set (Var "h")) ($#k2_partfun1 :::"|"::: ) (Set (Var "X"))) "is" ($#v6_valued_0 :::"decreasing"::: ) ))) ; theorem :: RFUNCT_2:30 (Bool "for" (Set (Var "X")) "," (Set (Var "Y")) "being" ($#m1_hidden :::"set"::: ) (Bool "for" (Set (Var "h")) "being" ($#m1_subset_1 :::"PartFunc":::) "of" (Set ($#k1_numbers :::"REAL"::: ) ) "," (Set ($#k1_numbers :::"REAL"::: ) ) "st" (Bool (Bool (Set (Var "X")) ($#r1_tarski :::"c="::: ) (Set (Var "Y"))) & (Bool (Set (Set (Var "h")) ($#k2_partfun1 :::"|"::: ) (Set (Var "Y"))) "is" ($#v7_valued_0 :::"non-decreasing"::: ) )) "holds" (Bool (Set (Set (Var "h")) ($#k2_partfun1 :::"|"::: ) (Set (Var "X"))) "is" ($#v7_valued_0 :::"non-decreasing"::: ) ))) ; theorem :: RFUNCT_2:31 (Bool "for" (Set (Var "X")) "," (Set (Var "Y")) "being" ($#m1_hidden :::"set"::: ) (Bool "for" (Set (Var "h")) "being" ($#m1_subset_1 :::"PartFunc":::) "of" (Set ($#k1_numbers :::"REAL"::: ) ) "," (Set ($#k1_numbers :::"REAL"::: ) ) "st" (Bool (Bool (Set (Var "X")) ($#r1_tarski :::"c="::: ) (Set (Var "Y"))) & (Bool (Set (Set (Var "h")) ($#k2_partfun1 :::"|"::: ) (Set (Var "Y"))) "is" ($#v8_valued_0 :::"non-increasing"::: ) )) "holds" (Bool (Set (Set (Var "h")) ($#k2_partfun1 :::"|"::: ) (Set (Var "X"))) "is" ($#v8_valued_0 :::"non-increasing"::: ) ))) ; theorem :: RFUNCT_2:32 (Bool "for" (Set (Var "Y")) "being" ($#m1_hidden :::"set"::: ) (Bool "for" (Set (Var "r")) "being" ($#m1_subset_1 :::"Element"::: ) "of" (Set ($#k1_numbers :::"REAL"::: ) ) (Bool "for" (Set (Var "h")) "being" ($#m1_subset_1 :::"PartFunc":::) "of" (Set ($#k1_numbers :::"REAL"::: ) ) "," (Set ($#k1_numbers :::"REAL"::: ) ) "holds" (Bool "(" "(" (Bool (Bool (Set (Set (Var "h")) ($#k2_partfun1 :::"|"::: ) (Set (Var "Y"))) "is" ($#v5_valued_0 :::"increasing"::: ) ) & (Bool (Set ($#k6_numbers :::"0"::: ) ) ($#r1_xxreal_0 :::"<"::: ) (Set (Var "r")))) "implies" (Bool (Set (Set "(" (Set (Var "r")) ($#k26_valued_1 :::"(#)"::: ) (Set (Var "h")) ")" ) ($#k2_partfun1 :::"|"::: ) (Set (Var "Y"))) "is" ($#v5_valued_0 :::"increasing"::: ) ) ")" & "(" (Bool (Bool (Set (Var "r")) ($#r1_hidden :::"="::: ) (Set ($#k6_numbers :::"0"::: ) ))) "implies" (Bool (Set (Set "(" (Set (Var "r")) ($#k26_valued_1 :::"(#)"::: ) (Set (Var "h")) ")" ) ($#k2_partfun1 :::"|"::: ) (Set (Var "Y"))) "is" bbbadV3_FUNCT_1()) ")" & "(" (Bool (Bool (Set (Set (Var "h")) ($#k2_partfun1 :::"|"::: ) (Set (Var "Y"))) "is" ($#v5_valued_0 :::"increasing"::: ) ) & (Bool (Set (Var "r")) ($#r1_xxreal_0 :::"<"::: ) (Set ($#k6_numbers :::"0"::: ) ))) "implies" (Bool (Set (Set "(" (Set (Var "r")) ($#k26_valued_1 :::"(#)"::: ) (Set (Var "h")) ")" ) ($#k2_partfun1 :::"|"::: ) (Set (Var "Y"))) "is" ($#v6_valued_0 :::"decreasing"::: ) ) ")" ")" )))) ; theorem :: RFUNCT_2:33 (Bool "for" (Set (Var "Y")) "being" ($#m1_hidden :::"set"::: ) (Bool "for" (Set (Var "r")) "being" ($#m1_subset_1 :::"Element"::: ) "of" (Set ($#k1_numbers :::"REAL"::: ) ) (Bool "for" (Set (Var "h")) "being" ($#m1_subset_1 :::"PartFunc":::) "of" (Set ($#k1_numbers :::"REAL"::: ) ) "," (Set ($#k1_numbers :::"REAL"::: ) ) "holds" (Bool "(" "(" (Bool (Bool (Set (Set (Var "h")) ($#k2_partfun1 :::"|"::: ) (Set (Var "Y"))) "is" ($#v6_valued_0 :::"decreasing"::: ) ) & (Bool (Set ($#k6_numbers :::"0"::: ) ) ($#r1_xxreal_0 :::"<"::: ) (Set (Var "r")))) "implies" (Bool (Set (Set "(" (Set (Var "r")) ($#k26_valued_1 :::"(#)"::: ) (Set (Var "h")) ")" ) ($#k2_partfun1 :::"|"::: ) (Set (Var "Y"))) "is" ($#v6_valued_0 :::"decreasing"::: ) ) ")" & "(" (Bool (Bool (Set (Set (Var "h")) ($#k2_partfun1 :::"|"::: ) (Set (Var "Y"))) "is" ($#v6_valued_0 :::"decreasing"::: ) ) & (Bool (Set (Var "r")) ($#r1_xxreal_0 :::"<"::: ) (Set ($#k6_numbers :::"0"::: ) ))) "implies" (Bool (Set (Set "(" (Set (Var "r")) ($#k26_valued_1 :::"(#)"::: ) (Set (Var "h")) ")" ) ($#k2_partfun1 :::"|"::: ) (Set (Var "Y"))) "is" ($#v5_valued_0 :::"increasing"::: ) ) ")" ")" )))) ; theorem :: RFUNCT_2:34 (Bool "for" (Set (Var "Y")) "being" ($#m1_hidden :::"set"::: ) (Bool "for" (Set (Var "r")) "being" ($#m1_subset_1 :::"Element"::: ) "of" (Set ($#k1_numbers :::"REAL"::: ) ) (Bool "for" (Set (Var "h")) "being" ($#m1_subset_1 :::"PartFunc":::) "of" (Set ($#k1_numbers :::"REAL"::: ) ) "," (Set ($#k1_numbers :::"REAL"::: ) ) "holds" (Bool "(" "(" (Bool (Bool (Set (Set (Var "h")) ($#k2_partfun1 :::"|"::: ) (Set (Var "Y"))) "is" ($#v7_valued_0 :::"non-decreasing"::: ) ) & (Bool (Set ($#k6_numbers :::"0"::: ) ) ($#r1_xxreal_0 :::"<="::: ) (Set (Var "r")))) "implies" (Bool (Set (Set "(" (Set (Var "r")) ($#k26_valued_1 :::"(#)"::: ) (Set (Var "h")) ")" ) ($#k2_partfun1 :::"|"::: ) (Set (Var "Y"))) "is" ($#v7_valued_0 :::"non-decreasing"::: ) ) ")" & "(" (Bool (Bool (Set (Set (Var "h")) ($#k2_partfun1 :::"|"::: ) (Set (Var "Y"))) "is" ($#v7_valued_0 :::"non-decreasing"::: ) ) & (Bool (Set (Var "r")) ($#r1_xxreal_0 :::"<="::: ) (Set ($#k6_numbers :::"0"::: ) ))) "implies" (Bool (Set (Set "(" (Set (Var "r")) ($#k26_valued_1 :::"(#)"::: ) (Set (Var "h")) ")" ) ($#k2_partfun1 :::"|"::: ) (Set (Var "Y"))) "is" ($#v8_valued_0 :::"non-increasing"::: ) ) ")" ")" )))) ; theorem :: RFUNCT_2:35 (Bool "for" (Set (Var "Y")) "being" ($#m1_hidden :::"set"::: ) (Bool "for" (Set (Var "r")) "being" ($#m1_subset_1 :::"Element"::: ) "of" (Set ($#k1_numbers :::"REAL"::: ) ) (Bool "for" (Set (Var "h")) "being" ($#m1_subset_1 :::"PartFunc":::) "of" (Set ($#k1_numbers :::"REAL"::: ) ) "," (Set ($#k1_numbers :::"REAL"::: ) ) "holds" (Bool "(" "(" (Bool (Bool (Set (Set (Var "h")) ($#k2_partfun1 :::"|"::: ) (Set (Var "Y"))) "is" ($#v8_valued_0 :::"non-increasing"::: ) ) & (Bool (Set ($#k6_numbers :::"0"::: ) ) ($#r1_xxreal_0 :::"<="::: ) (Set (Var "r")))) "implies" (Bool (Set (Set "(" (Set (Var "r")) ($#k26_valued_1 :::"(#)"::: ) (Set (Var "h")) ")" ) ($#k2_partfun1 :::"|"::: ) (Set (Var "Y"))) "is" ($#v8_valued_0 :::"non-increasing"::: ) ) ")" & "(" (Bool (Bool (Set (Set (Var "h")) ($#k2_partfun1 :::"|"::: ) (Set (Var "Y"))) "is" ($#v8_valued_0 :::"non-increasing"::: ) ) & (Bool (Set (Var "r")) ($#r1_xxreal_0 :::"<="::: ) (Set ($#k6_numbers :::"0"::: ) ))) "implies" (Bool (Set (Set "(" (Set (Var "r")) ($#k26_valued_1 :::"(#)"::: ) (Set (Var "h")) ")" ) ($#k2_partfun1 :::"|"::: ) (Set (Var "Y"))) "is" ($#v7_valued_0 :::"non-decreasing"::: ) ) ")" ")" )))) ; theorem :: RFUNCT_2:36 (Bool "for" (Set (Var "X")) "," (Set (Var "Y")) "being" ($#m1_hidden :::"set"::: ) (Bool "for" (Set (Var "r")) "being" ($#m1_subset_1 :::"Element"::: ) "of" (Set ($#k1_numbers :::"REAL"::: ) ) (Bool "for" (Set (Var "h1")) "," (Set (Var "h2")) "being" ($#m1_subset_1 :::"PartFunc":::) "of" (Set ($#k1_numbers :::"REAL"::: ) ) "," (Set ($#k1_numbers :::"REAL"::: ) ) "st" (Bool (Bool (Set (Var "r")) ($#r2_hidden :::"in"::: ) (Set (Set "(" (Set (Var "X")) ($#k3_xboole_0 :::"/\"::: ) (Set (Var "Y")) ")" ) ($#k9_subset_1 :::"/\"::: ) (Set "(" ($#k1_relset_1 :::"dom"::: ) (Set "(" (Set (Var "h1")) ($#k3_valued_1 :::"+"::: ) (Set (Var "h2")) ")" ) ")" )))) "holds" (Bool "(" (Bool (Set (Var "r")) ($#r2_hidden :::"in"::: ) (Set (Set (Var "X")) ($#k9_subset_1 :::"/\"::: ) (Set "(" ($#k1_relset_1 :::"dom"::: ) (Set (Var "h1")) ")" ))) & (Bool (Set (Var "r")) ($#r2_hidden :::"in"::: ) (Set (Set (Var "Y")) ($#k9_subset_1 :::"/\"::: ) (Set "(" ($#k1_relset_1 :::"dom"::: ) (Set (Var "h2")) ")" ))) ")" )))) ; theorem :: RFUNCT_2:37 (Bool "for" (Set (Var "X")) "," (Set (Var "Y")) "being" ($#m1_hidden :::"set"::: ) (Bool "for" (Set (Var "h1")) "," (Set (Var "h2")) "being" ($#m1_subset_1 :::"PartFunc":::) "of" (Set ($#k1_numbers :::"REAL"::: ) ) "," (Set ($#k1_numbers :::"REAL"::: ) ) "holds" (Bool "(" "(" (Bool (Bool (Set (Set (Var "h1")) ($#k2_partfun1 :::"|"::: ) (Set (Var "X"))) "is" ($#v5_valued_0 :::"increasing"::: ) ) & (Bool (Set (Set (Var "h2")) ($#k2_partfun1 :::"|"::: ) (Set (Var "Y"))) "is" ($#v5_valued_0 :::"increasing"::: ) )) "implies" (Bool (Set (Set "(" (Set (Var "h1")) ($#k3_valued_1 :::"+"::: ) (Set (Var "h2")) ")" ) ($#k2_partfun1 :::"|"::: ) (Set "(" (Set (Var "X")) ($#k3_xboole_0 :::"/\"::: ) (Set (Var "Y")) ")" )) "is" ($#v5_valued_0 :::"increasing"::: ) ) ")" & "(" (Bool (Bool (Set (Set (Var "h1")) ($#k2_partfun1 :::"|"::: ) (Set (Var "X"))) "is" ($#v6_valued_0 :::"decreasing"::: ) ) & (Bool (Set (Set (Var "h2")) ($#k2_partfun1 :::"|"::: ) (Set (Var "Y"))) "is" ($#v6_valued_0 :::"decreasing"::: ) )) "implies" (Bool (Set (Set "(" (Set (Var "h1")) ($#k3_valued_1 :::"+"::: ) (Set (Var "h2")) ")" ) ($#k2_partfun1 :::"|"::: ) (Set "(" (Set (Var "X")) ($#k3_xboole_0 :::"/\"::: ) (Set (Var "Y")) ")" )) "is" ($#v6_valued_0 :::"decreasing"::: ) ) ")" & "(" (Bool (Bool (Set (Set (Var "h1")) ($#k2_partfun1 :::"|"::: ) (Set (Var "X"))) "is" ($#v7_valued_0 :::"non-decreasing"::: ) ) & (Bool (Set (Set (Var "h2")) ($#k2_partfun1 :::"|"::: ) (Set (Var "Y"))) "is" ($#v7_valued_0 :::"non-decreasing"::: ) )) "implies" (Bool (Set (Set "(" (Set (Var "h1")) ($#k3_valued_1 :::"+"::: ) (Set (Var "h2")) ")" ) ($#k2_partfun1 :::"|"::: ) (Set "(" (Set (Var "X")) ($#k3_xboole_0 :::"/\"::: ) (Set (Var "Y")) ")" )) "is" ($#v7_valued_0 :::"non-decreasing"::: ) ) ")" & "(" (Bool (Bool (Set (Set (Var "h1")) ($#k2_partfun1 :::"|"::: ) (Set (Var "X"))) "is" ($#v8_valued_0 :::"non-increasing"::: ) ) & (Bool (Set (Set (Var "h2")) ($#k2_partfun1 :::"|"::: ) (Set (Var "Y"))) "is" ($#v8_valued_0 :::"non-increasing"::: ) )) "implies" (Bool (Set (Set "(" (Set (Var "h1")) ($#k3_valued_1 :::"+"::: ) (Set (Var "h2")) ")" ) ($#k2_partfun1 :::"|"::: ) (Set "(" (Set (Var "X")) ($#k3_xboole_0 :::"/\"::: ) (Set (Var "Y")) ")" )) "is" ($#v8_valued_0 :::"non-increasing"::: ) ) ")" ")" ))) ; theorem :: RFUNCT_2:38 (Bool "for" (Set (Var "X")) "," (Set (Var "Y")) "being" ($#m1_hidden :::"set"::: ) (Bool "for" (Set (Var "h1")) "," (Set (Var "h2")) "being" ($#m1_subset_1 :::"PartFunc":::) "of" (Set ($#k1_numbers :::"REAL"::: ) ) "," (Set ($#k1_numbers :::"REAL"::: ) ) "holds" (Bool "(" "(" (Bool (Bool (Set (Set (Var "h1")) ($#k2_partfun1 :::"|"::: ) (Set (Var "X"))) "is" ($#v5_valued_0 :::"increasing"::: ) ) & (Bool (Set (Set (Var "h2")) ($#k2_partfun1 :::"|"::: ) (Set (Var "Y"))) "is" bbbadV3_FUNCT_1())) "implies" (Bool (Set (Set "(" (Set (Var "h1")) ($#k3_valued_1 :::"+"::: ) (Set (Var "h2")) ")" ) ($#k2_partfun1 :::"|"::: ) (Set "(" (Set (Var "X")) ($#k3_xboole_0 :::"/\"::: ) (Set (Var "Y")) ")" )) "is" ($#v5_valued_0 :::"increasing"::: ) ) ")" & "(" (Bool (Bool (Set (Set (Var "h1")) ($#k2_partfun1 :::"|"::: ) (Set (Var "X"))) "is" ($#v6_valued_0 :::"decreasing"::: ) ) & (Bool (Set (Set (Var "h2")) ($#k2_partfun1 :::"|"::: ) (Set (Var "Y"))) "is" bbbadV3_FUNCT_1())) "implies" (Bool (Set (Set "(" (Set (Var "h1")) ($#k3_valued_1 :::"+"::: ) (Set (Var "h2")) ")" ) ($#k2_partfun1 :::"|"::: ) (Set "(" (Set (Var "X")) ($#k3_xboole_0 :::"/\"::: ) (Set (Var "Y")) ")" )) "is" ($#v6_valued_0 :::"decreasing"::: ) ) ")" ")" ))) ; theorem :: RFUNCT_2:39 (Bool "for" (Set (Var "X")) "," (Set (Var "Y")) "being" ($#m1_hidden :::"set"::: ) (Bool "for" (Set (Var "h1")) "," (Set (Var "h2")) "being" ($#m1_subset_1 :::"PartFunc":::) "of" (Set ($#k1_numbers :::"REAL"::: ) ) "," (Set ($#k1_numbers :::"REAL"::: ) ) "st" (Bool (Bool (Set (Set (Var "h1")) ($#k2_partfun1 :::"|"::: ) (Set (Var "X"))) "is" ($#v5_valued_0 :::"increasing"::: ) ) & (Bool (Set (Set (Var "h2")) ($#k2_partfun1 :::"|"::: ) (Set (Var "Y"))) "is" ($#v7_valued_0 :::"non-decreasing"::: ) )) "holds" (Bool (Set (Set "(" (Set (Var "h1")) ($#k3_valued_1 :::"+"::: ) (Set (Var "h2")) ")" ) ($#k2_partfun1 :::"|"::: ) (Set "(" (Set (Var "X")) ($#k3_xboole_0 :::"/\"::: ) (Set (Var "Y")) ")" )) "is" ($#v5_valued_0 :::"increasing"::: ) ))) ; theorem :: RFUNCT_2:40 (Bool "for" (Set (Var "X")) "," (Set (Var "Y")) "being" ($#m1_hidden :::"set"::: ) (Bool "for" (Set (Var "h1")) "," (Set (Var "h2")) "being" ($#m1_subset_1 :::"PartFunc":::) "of" (Set ($#k1_numbers :::"REAL"::: ) ) "," (Set ($#k1_numbers :::"REAL"::: ) ) "st" (Bool (Bool (Set (Set (Var "h1")) ($#k2_partfun1 :::"|"::: ) (Set (Var "X"))) "is" ($#v8_valued_0 :::"non-increasing"::: ) ) & (Bool (Set (Set (Var "h2")) ($#k2_partfun1 :::"|"::: ) (Set (Var "Y"))) "is" bbbadV3_FUNCT_1())) "holds" (Bool (Set (Set "(" (Set (Var "h1")) ($#k3_valued_1 :::"+"::: ) (Set (Var "h2")) ")" ) ($#k2_partfun1 :::"|"::: ) (Set "(" (Set (Var "X")) ($#k3_xboole_0 :::"/\"::: ) (Set (Var "Y")) ")" )) "is" ($#v8_valued_0 :::"non-increasing"::: ) ))) ; theorem :: RFUNCT_2:41 (Bool "for" (Set (Var "X")) "," (Set (Var "Y")) "being" ($#m1_hidden :::"set"::: ) (Bool "for" (Set (Var "h1")) "," (Set (Var "h2")) "being" ($#m1_subset_1 :::"PartFunc":::) "of" (Set ($#k1_numbers :::"REAL"::: ) ) "," (Set ($#k1_numbers :::"REAL"::: ) ) "st" (Bool (Bool (Set (Set (Var "h1")) ($#k2_partfun1 :::"|"::: ) (Set (Var "X"))) "is" ($#v6_valued_0 :::"decreasing"::: ) ) & (Bool (Set (Set (Var "h2")) ($#k2_partfun1 :::"|"::: ) (Set (Var "Y"))) "is" ($#v8_valued_0 :::"non-increasing"::: ) )) "holds" (Bool (Set (Set "(" (Set (Var "h1")) ($#k3_valued_1 :::"+"::: ) (Set (Var "h2")) ")" ) ($#k2_partfun1 :::"|"::: ) (Set "(" (Set (Var "X")) ($#k3_xboole_0 :::"/\"::: ) (Set (Var "Y")) ")" )) "is" ($#v6_valued_0 :::"decreasing"::: ) ))) ; theorem :: RFUNCT_2:42 (Bool "for" (Set (Var "X")) "," (Set (Var "Y")) "being" ($#m1_hidden :::"set"::: ) (Bool "for" (Set (Var "h1")) "," (Set (Var "h2")) "being" ($#m1_subset_1 :::"PartFunc":::) "of" (Set ($#k1_numbers :::"REAL"::: ) ) "," (Set ($#k1_numbers :::"REAL"::: ) ) "st" (Bool (Bool (Set (Set (Var "h1")) ($#k2_partfun1 :::"|"::: ) (Set (Var "X"))) "is" ($#v7_valued_0 :::"non-decreasing"::: ) ) & (Bool (Set (Set (Var "h2")) ($#k2_partfun1 :::"|"::: ) (Set (Var "Y"))) "is" bbbadV3_FUNCT_1())) "holds" (Bool (Set (Set "(" (Set (Var "h1")) ($#k3_valued_1 :::"+"::: ) (Set (Var "h2")) ")" ) ($#k2_partfun1 :::"|"::: ) (Set "(" (Set (Var "X")) ($#k3_xboole_0 :::"/\"::: ) (Set (Var "Y")) ")" )) "is" ($#v7_valued_0 :::"non-decreasing"::: ) ))) ; theorem :: RFUNCT_2:43 (Bool "for" (Set (Var "x")) "being" ($#m1_hidden :::"set"::: ) (Bool "for" (Set (Var "h")) "being" ($#m1_subset_1 :::"PartFunc":::) "of" (Set ($#k1_numbers :::"REAL"::: ) ) "," (Set ($#k1_numbers :::"REAL"::: ) ) "holds" (Bool (Set (Set (Var "h")) ($#k2_partfun1 :::"|"::: ) (Set ($#k1_tarski :::"{"::: ) (Set (Var "x")) ($#k1_tarski :::"}"::: ) )) "is" ($#v8_valued_0 :::"non-increasing"::: ) ))) ; theorem :: RFUNCT_2:44 (Bool "for" (Set (Var "x")) "being" ($#m1_hidden :::"set"::: ) (Bool "for" (Set (Var "h")) "being" ($#m1_subset_1 :::"PartFunc":::) "of" (Set ($#k1_numbers :::"REAL"::: ) ) "," (Set ($#k1_numbers :::"REAL"::: ) ) "holds" (Bool (Set (Set (Var "h")) ($#k2_partfun1 :::"|"::: ) (Set ($#k1_tarski :::"{"::: ) (Set (Var "x")) ($#k1_tarski :::"}"::: ) )) "is" ($#v6_valued_0 :::"decreasing"::: ) ))) ; theorem :: RFUNCT_2:45 (Bool "for" (Set (Var "x")) "being" ($#m1_hidden :::"set"::: ) (Bool "for" (Set (Var "h")) "being" ($#m1_subset_1 :::"PartFunc":::) "of" (Set ($#k1_numbers :::"REAL"::: ) ) "," (Set ($#k1_numbers :::"REAL"::: ) ) "holds" (Bool (Set (Set (Var "h")) ($#k2_partfun1 :::"|"::: ) (Set ($#k1_tarski :::"{"::: ) (Set (Var "x")) ($#k1_tarski :::"}"::: ) )) "is" ($#v7_valued_0 :::"non-decreasing"::: ) ))) ; theorem :: RFUNCT_2:46 (Bool "for" (Set (Var "x")) "being" ($#m1_hidden :::"set"::: ) (Bool "for" (Set (Var "h")) "being" ($#m1_subset_1 :::"PartFunc":::) "of" (Set ($#k1_numbers :::"REAL"::: ) ) "," (Set ($#k1_numbers :::"REAL"::: ) ) "holds" (Bool (Set (Set (Var "h")) ($#k2_partfun1 :::"|"::: ) (Set ($#k1_tarski :::"{"::: ) (Set (Var "x")) ($#k1_tarski :::"}"::: ) )) "is" ($#v8_valued_0 :::"non-increasing"::: ) ))) ; theorem :: RFUNCT_2:47 (Bool "for" (Set (Var "R")) "being" ($#m1_subset_1 :::"Subset":::) "of" (Set ($#k1_numbers :::"REAL"::: ) ) "holds" (Bool (Set (Set "(" ($#k1_partfun2 :::"id"::: ) (Set (Var "R")) ")" ) ($#k2_partfun1 :::"|"::: ) (Set (Var "R"))) "is" ($#v5_valued_0 :::"increasing"::: ) )) ; theorem :: RFUNCT_2:48 (Bool "for" (Set (Var "X")) "being" ($#m1_hidden :::"set"::: ) (Bool "for" (Set (Var "h")) "being" ($#m1_subset_1 :::"PartFunc":::) "of" (Set ($#k1_numbers :::"REAL"::: ) ) "," (Set ($#k1_numbers :::"REAL"::: ) ) "st" (Bool (Bool (Set (Set (Var "h")) ($#k2_partfun1 :::"|"::: ) (Set (Var "X"))) "is" ($#v5_valued_0 :::"increasing"::: ) )) "holds" (Bool (Set (Set "(" ($#k32_valued_1 :::"-"::: ) (Set (Var "h")) ")" ) ($#k2_partfun1 :::"|"::: ) (Set (Var "X"))) "is" ($#v6_valued_0 :::"decreasing"::: ) ))) ; theorem :: RFUNCT_2:49 (Bool "for" (Set (Var "X")) "being" ($#m1_hidden :::"set"::: ) (Bool "for" (Set (Var "h")) "being" ($#m1_subset_1 :::"PartFunc":::) "of" (Set ($#k1_numbers :::"REAL"::: ) ) "," (Set ($#k1_numbers :::"REAL"::: ) ) "st" (Bool (Bool (Set (Set (Var "h")) ($#k2_partfun1 :::"|"::: ) (Set (Var "X"))) "is" ($#v7_valued_0 :::"non-decreasing"::: ) )) "holds" (Bool (Set (Set "(" ($#k32_valued_1 :::"-"::: ) (Set (Var "h")) ")" ) ($#k2_partfun1 :::"|"::: ) (Set (Var "X"))) "is" ($#v8_valued_0 :::"non-increasing"::: ) ))) ; theorem :: RFUNCT_2:50 (Bool "for" (Set (Var "p")) "," (Set (Var "g")) "being" ($#m1_subset_1 :::"Element"::: ) "of" (Set ($#k1_numbers :::"REAL"::: ) ) (Bool "for" (Set (Var "h")) "being" ($#m1_subset_1 :::"PartFunc":::) "of" (Set ($#k1_numbers :::"REAL"::: ) ) "," (Set ($#k1_numbers :::"REAL"::: ) ) "st" (Bool (Bool "(" (Bool (Set (Set (Var "h")) ($#k2_partfun1 :::"|"::: ) (Set ($#k1_rcomp_1 :::"[."::: ) (Set (Var "p")) "," (Set (Var "g")) ($#k1_rcomp_1 :::".]"::: ) )) "is" ($#v5_valued_0 :::"increasing"::: ) ) "or" (Bool (Set (Set (Var "h")) ($#k2_partfun1 :::"|"::: ) (Set ($#k1_rcomp_1 :::"[."::: ) (Set (Var "p")) "," (Set (Var "g")) ($#k1_rcomp_1 :::".]"::: ) )) "is" ($#v6_valued_0 :::"decreasing"::: ) ) ")" )) "holds" (Bool (Set (Set (Var "h")) ($#k2_partfun1 :::"|"::: ) (Set ($#k1_rcomp_1 :::"[."::: ) (Set (Var "p")) "," (Set (Var "g")) ($#k1_rcomp_1 :::".]"::: ) )) "is" ($#v2_funct_1 :::"one-to-one"::: ) ))) ; theorem :: RFUNCT_2:51 (Bool "for" (Set (Var "p")) "," (Set (Var "g")) "being" ($#m1_subset_1 :::"Element"::: ) "of" (Set ($#k1_numbers :::"REAL"::: ) ) (Bool "for" (Set (Var "h")) "being" ($#v2_funct_1 :::"one-to-one"::: ) ($#m1_subset_1 :::"PartFunc":::) "of" (Set ($#k1_numbers :::"REAL"::: ) ) "," (Set ($#k1_numbers :::"REAL"::: ) ) "st" (Bool (Bool (Set (Set (Var "h")) ($#k2_partfun1 :::"|"::: ) (Set ($#k1_rcomp_1 :::"[."::: ) (Set (Var "p")) "," (Set (Var "g")) ($#k1_rcomp_1 :::".]"::: ) )) "is" ($#v5_valued_0 :::"increasing"::: ) )) "holds" (Bool (Set (Set "(" (Set "(" (Set (Var "h")) ($#k2_partfun1 :::"|"::: ) (Set ($#k1_rcomp_1 :::"[."::: ) (Set (Var "p")) "," (Set (Var "g")) ($#k1_rcomp_1 :::".]"::: ) ) ")" ) ($#k2_partfun2 :::"""::: ) ")" ) ($#k2_partfun1 :::"|"::: ) (Set "(" (Set (Var "h")) ($#k7_relset_1 :::".:"::: ) (Set ($#k1_rcomp_1 :::"[."::: ) (Set (Var "p")) "," (Set (Var "g")) ($#k1_rcomp_1 :::".]"::: ) ) ")" )) "is" ($#v5_valued_0 :::"increasing"::: ) ))) ; theorem :: RFUNCT_2:52 (Bool "for" (Set (Var "p")) "," (Set (Var "g")) "being" ($#m1_subset_1 :::"Element"::: ) "of" (Set ($#k1_numbers :::"REAL"::: ) ) (Bool "for" (Set (Var "h")) "being" ($#v2_funct_1 :::"one-to-one"::: ) ($#m1_subset_1 :::"PartFunc":::) "of" (Set ($#k1_numbers :::"REAL"::: ) ) "," (Set ($#k1_numbers :::"REAL"::: ) ) "st" (Bool (Bool (Set (Set (Var "h")) ($#k2_partfun1 :::"|"::: ) (Set ($#k1_rcomp_1 :::"[."::: ) (Set (Var "p")) "," (Set (Var "g")) ($#k1_rcomp_1 :::".]"::: ) )) "is" ($#v6_valued_0 :::"decreasing"::: ) )) "holds" (Bool (Set (Set "(" (Set "(" (Set (Var "h")) ($#k2_partfun1 :::"|"::: ) (Set ($#k1_rcomp_1 :::"[."::: ) (Set (Var "p")) "," (Set (Var "g")) ($#k1_rcomp_1 :::".]"::: ) ) ")" ) ($#k2_partfun2 :::"""::: ) ")" ) ($#k2_partfun1 :::"|"::: ) (Set "(" (Set (Var "h")) ($#k7_relset_1 :::".:"::: ) (Set ($#k1_rcomp_1 :::"[."::: ) (Set (Var "p")) "," (Set (Var "g")) ($#k1_rcomp_1 :::".]"::: ) ) ")" )) "is" ($#v6_valued_0 :::"decreasing"::: ) ))) ;