:: RFUNCT_2 semantic presentation begin theorem Th1: :: RFUNCT_2:1 for seq1, seq2, seq3 being Real_Sequence holds ( seq1 = seq2 - seq3 iff for n being Element of NAT holds seq1 . n = (seq2 . n) - (seq3 . n) ) proof let seq1, seq2, seq3 be Real_Sequence; ::_thesis: ( seq1 = seq2 - seq3 iff for n being Element of NAT holds seq1 . n = (seq2 . n) - (seq3 . n) ) thus ( seq1 = seq2 - seq3 implies for n being Element of NAT holds seq1 . n = (seq2 . n) - (seq3 . n) ) ::_thesis: ( ( for n being Element of NAT holds seq1 . n = (seq2 . n) - (seq3 . n) ) implies seq1 = seq2 - seq3 ) proof assume A1: seq1 = seq2 - seq3 ; ::_thesis: for n being Element of NAT holds seq1 . n = (seq2 . n) - (seq3 . n) now__::_thesis:_for_n_being_Element_of_NAT_holds_seq1_._n_=_(seq2_._n)_-_(seq3_._n) let n be Element of NAT ; ::_thesis: seq1 . n = (seq2 . n) - (seq3 . n) seq1 . n = (seq2 . n) + ((- seq3) . n) by A1, SEQ_1:7; then seq1 . n = (seq2 . n) + (- (seq3 . n)) by SEQ_1:10; hence seq1 . n = (seq2 . n) - (seq3 . n) ; ::_thesis: verum end; hence for n being Element of NAT holds seq1 . n = (seq2 . n) - (seq3 . n) ; ::_thesis: verum end; assume A2: for n being Element of NAT holds seq1 . n = (seq2 . n) - (seq3 . n) ; ::_thesis: seq1 = seq2 - seq3 now__::_thesis:_for_n_being_Element_of_NAT_holds_seq1_._n_=_(seq2_._n)_+_((-_seq3)_._n) let n be Element of NAT ; ::_thesis: seq1 . n = (seq2 . n) + ((- seq3) . n) thus seq1 . n = (seq2 . n) - (seq3 . n) by A2 .= (seq2 . n) + (- (seq3 . n)) .= (seq2 . n) + ((- seq3) . n) by SEQ_1:10 ; ::_thesis: verum end; hence seq1 = seq2 - seq3 by SEQ_1:7; ::_thesis: verum end; theorem Th2: :: RFUNCT_2:2 for seq1, seq2 being Real_Sequence for Ns being V37() sequence of NAT holds ( (seq1 + seq2) * Ns = (seq1 * Ns) + (seq2 * Ns) & (seq1 - seq2) * Ns = (seq1 * Ns) - (seq2 * Ns) & (seq1 (#) seq2) * Ns = (seq1 * Ns) (#) (seq2 * Ns) ) proof let seq1, seq2 be Real_Sequence; ::_thesis: for Ns being V37() sequence of NAT holds ( (seq1 + seq2) * Ns = (seq1 * Ns) + (seq2 * Ns) & (seq1 - seq2) * Ns = (seq1 * Ns) - (seq2 * Ns) & (seq1 (#) seq2) * Ns = (seq1 * Ns) (#) (seq2 * Ns) ) let Ns be V37() sequence of NAT; ::_thesis: ( (seq1 + seq2) * Ns = (seq1 * Ns) + (seq2 * Ns) & (seq1 - seq2) * Ns = (seq1 * Ns) - (seq2 * Ns) & (seq1 (#) seq2) * Ns = (seq1 * Ns) (#) (seq2 * Ns) ) now__::_thesis:_for_n_being_Element_of_NAT_holds_((seq1_+_seq2)_*_Ns)_._n_=_((seq1_*_Ns)_+_(seq2_*_Ns))_._n let n be Element of NAT ; ::_thesis: ((seq1 + seq2) * Ns) . n = ((seq1 * Ns) + (seq2 * Ns)) . n thus ((seq1 + seq2) * Ns) . n = (seq1 + seq2) . (Ns . n) by FUNCT_2:15 .= (seq1 . (Ns . n)) + (seq2 . (Ns . n)) by SEQ_1:7 .= ((seq1 * Ns) . n) + (seq2 . (Ns . n)) by FUNCT_2:15 .= ((seq1 * Ns) . n) + ((seq2 * Ns) . n) by FUNCT_2:15 .= ((seq1 * Ns) + (seq2 * Ns)) . n by SEQ_1:7 ; ::_thesis: verum end; hence (seq1 + seq2) * Ns = (seq1 * Ns) + (seq2 * Ns) by FUNCT_2:63; ::_thesis: ( (seq1 - seq2) * Ns = (seq1 * Ns) - (seq2 * Ns) & (seq1 (#) seq2) * Ns = (seq1 * Ns) (#) (seq2 * Ns) ) now__::_thesis:_for_n_being_Element_of_NAT_holds_((seq1_-_seq2)_*_Ns)_._n_=_((seq1_*_Ns)_-_(seq2_*_Ns))_._n let n be Element of NAT ; ::_thesis: ((seq1 - seq2) * Ns) . n = ((seq1 * Ns) - (seq2 * Ns)) . n thus ((seq1 - seq2) * Ns) . n = (seq1 - seq2) . (Ns . n) by FUNCT_2:15 .= (seq1 . (Ns . n)) - (seq2 . (Ns . n)) by Th1 .= ((seq1 * Ns) . n) - (seq2 . (Ns . n)) by FUNCT_2:15 .= ((seq1 * Ns) . n) - ((seq2 * Ns) . n) by FUNCT_2:15 .= ((seq1 * Ns) - (seq2 * Ns)) . n by Th1 ; ::_thesis: verum end; hence (seq1 - seq2) * Ns = (seq1 * Ns) - (seq2 * Ns) by FUNCT_2:63; ::_thesis: (seq1 (#) seq2) * Ns = (seq1 * Ns) (#) (seq2 * Ns) now__::_thesis:_for_n_being_Element_of_NAT_holds_((seq1_(#)_seq2)_*_Ns)_._n_=_((seq1_*_Ns)_(#)_(seq2_*_Ns))_._n let n be Element of NAT ; ::_thesis: ((seq1 (#) seq2) * Ns) . n = ((seq1 * Ns) (#) (seq2 * Ns)) . n thus ((seq1 (#) seq2) * Ns) . n = (seq1 (#) seq2) . (Ns . n) by FUNCT_2:15 .= (seq1 . (Ns . n)) * (seq2 . (Ns . n)) by SEQ_1:8 .= ((seq1 * Ns) . n) * (seq2 . (Ns . n)) by FUNCT_2:15 .= ((seq1 * Ns) . n) * ((seq2 * Ns) . n) by FUNCT_2:15 .= ((seq1 * Ns) (#) (seq2 * Ns)) . n by SEQ_1:8 ; ::_thesis: verum end; hence (seq1 (#) seq2) * Ns = (seq1 * Ns) (#) (seq2 * Ns) by FUNCT_2:63; ::_thesis: verum end; theorem Th3: :: RFUNCT_2:3 for p being Element of REAL for seq being Real_Sequence for Ns being V37() sequence of NAT holds (p (#) seq) * Ns = p (#) (seq * Ns) proof let p be Element of REAL ; ::_thesis: for seq being Real_Sequence for Ns being V37() sequence of NAT holds (p (#) seq) * Ns = p (#) (seq * Ns) let seq be Real_Sequence; ::_thesis: for Ns being V37() sequence of NAT holds (p (#) seq) * Ns = p (#) (seq * Ns) let Ns be V37() sequence of NAT; ::_thesis: (p (#) seq) * Ns = p (#) (seq * Ns) now__::_thesis:_for_n_being_Element_of_NAT_holds_((p_(#)_seq)_*_Ns)_._n_=_(p_(#)_(seq_*_Ns))_._n let n be Element of NAT ; ::_thesis: ((p (#) seq) * Ns) . n = (p (#) (seq * Ns)) . n thus ((p (#) seq) * Ns) . n = (p (#) seq) . (Ns . n) by FUNCT_2:15 .= p * (seq . (Ns . n)) by SEQ_1:9 .= p * ((seq * Ns) . n) by FUNCT_2:15 .= (p (#) (seq * Ns)) . n by SEQ_1:9 ; ::_thesis: verum end; hence (p (#) seq) * Ns = p (#) (seq * Ns) by FUNCT_2:63; ::_thesis: verum end; theorem :: RFUNCT_2:4 for seq being Real_Sequence for Ns being V37() sequence of NAT holds ( (- seq) * Ns = - (seq * Ns) & (abs seq) * Ns = abs (seq * Ns) ) proof let seq be Real_Sequence; ::_thesis: for Ns being V37() sequence of NAT holds ( (- seq) * Ns = - (seq * Ns) & (abs seq) * Ns = abs (seq * Ns) ) let Ns be V37() sequence of NAT; ::_thesis: ( (- seq) * Ns = - (seq * Ns) & (abs seq) * Ns = abs (seq * Ns) ) thus (- seq) * Ns = ((- 1) (#) seq) * Ns .= (- 1) (#) (seq * Ns) by Th3 .= - (seq * Ns) ; ::_thesis: (abs seq) * Ns = abs (seq * Ns) now__::_thesis:_for_n_being_Element_of_NAT_holds_((abs_seq)_*_Ns)_._n_=_(abs_(seq_*_Ns))_._n let n be Element of NAT ; ::_thesis: ((abs seq) * Ns) . n = (abs (seq * Ns)) . n thus ((abs seq) * Ns) . n = (abs seq) . (Ns . n) by FUNCT_2:15 .= abs (seq . (Ns . n)) by SEQ_1:12 .= abs ((seq * Ns) . n) by FUNCT_2:15 .= (abs (seq * Ns)) . n by SEQ_1:12 ; ::_thesis: verum end; hence (abs seq) * Ns = abs (seq * Ns) by FUNCT_2:63; ::_thesis: verum end; theorem Th5: :: RFUNCT_2:5 for seq being Real_Sequence for Ns being V37() sequence of NAT holds (seq * Ns) " = (seq ") * Ns proof let seq be Real_Sequence; ::_thesis: for Ns being V37() sequence of NAT holds (seq * Ns) " = (seq ") * Ns let Ns be V37() sequence of NAT; ::_thesis: (seq * Ns) " = (seq ") * Ns now__::_thesis:_for_n_being_Element_of_NAT_holds_((seq_*_Ns)_")_._n_=_((seq_")_*_Ns)_._n let n be Element of NAT ; ::_thesis: ((seq * Ns) ") . n = ((seq ") * Ns) . n thus ((seq * Ns) ") . n = ((seq * Ns) . n) " by VALUED_1:10 .= (seq . (Ns . n)) " by FUNCT_2:15 .= (seq ") . (Ns . n) by VALUED_1:10 .= ((seq ") * Ns) . n by FUNCT_2:15 ; ::_thesis: verum end; hence (seq * Ns) " = (seq ") * Ns by FUNCT_2:63; ::_thesis: verum end; theorem :: RFUNCT_2:6 for seq1, seq being Real_Sequence for Ns being V37() sequence of NAT holds (seq1 /" seq) * Ns = (seq1 * Ns) /" (seq * Ns) proof let seq1, seq be Real_Sequence; ::_thesis: for Ns being V37() sequence of NAT holds (seq1 /" seq) * Ns = (seq1 * Ns) /" (seq * Ns) let Ns be V37() sequence of NAT; ::_thesis: (seq1 /" seq) * Ns = (seq1 * Ns) /" (seq * Ns) thus (seq1 /" seq) * Ns = (seq1 (#) (seq ")) * Ns .= (seq1 * Ns) (#) ((seq ") * Ns) by Th2 .= (seq1 * Ns) (#) ((seq * Ns) ") by Th5 .= (seq1 * Ns) /" (seq * Ns) ; ::_thesis: verum end; theorem :: RFUNCT_2:7 for seq being Real_Sequence st seq is convergent & ( for n being Element of NAT holds seq . n <= 0 ) holds lim seq <= 0 proof let seq be Real_Sequence; ::_thesis: ( seq is convergent & ( for n being Element of NAT holds seq . n <= 0 ) implies lim seq <= 0 ) assume that A1: seq is convergent and A2: for n being Element of NAT holds seq . n <= 0 ; ::_thesis: lim seq <= 0 set seq1 = - seq; A3: now__::_thesis:_for_n_being_Element_of_NAT_holds_-_0_<=_(-_seq)_._n let n be Element of NAT ; ::_thesis: - 0 <= (- seq) . n ( (- seq) . n = - (seq . n) & seq . n <= 0 ) by A2, SEQ_1:10; hence - 0 <= (- seq) . n by XREAL_1:24; ::_thesis: verum end; - seq is convergent by A1, SEQ_2:9; then 0 <= lim (- seq) by A3, SEQ_2:17; then - 0 <= - (lim seq) by A1, SEQ_2:10; hence lim seq <= 0 by XREAL_1:24; ::_thesis: verum end; theorem Th8: :: RFUNCT_2:8 for W being non empty set for h1, h2 being PartFunc of W,REAL for seq being sequence of W st rng seq c= (dom h1) /\ (dom h2) holds ( (h1 + h2) /* seq = (h1 /* seq) + (h2 /* seq) & (h1 - h2) /* seq = (h1 /* seq) - (h2 /* seq) & (h1 (#) h2) /* seq = (h1 /* seq) (#) (h2 /* seq) ) proof let W be non empty set ; ::_thesis: for h1, h2 being PartFunc of W,REAL for seq being sequence of W st rng seq c= (dom h1) /\ (dom h2) holds ( (h1 + h2) /* seq = (h1 /* seq) + (h2 /* seq) & (h1 - h2) /* seq = (h1 /* seq) - (h2 /* seq) & (h1 (#) h2) /* seq = (h1 /* seq) (#) (h2 /* seq) ) let h1, h2 be PartFunc of W,REAL; ::_thesis: for seq being sequence of W st rng seq c= (dom h1) /\ (dom h2) holds ( (h1 + h2) /* seq = (h1 /* seq) + (h2 /* seq) & (h1 - h2) /* seq = (h1 /* seq) - (h2 /* seq) & (h1 (#) h2) /* seq = (h1 /* seq) (#) (h2 /* seq) ) let seq be sequence of W; ::_thesis: ( rng seq c= (dom h1) /\ (dom h2) implies ( (h1 + h2) /* seq = (h1 /* seq) + (h2 /* seq) & (h1 - h2) /* seq = (h1 /* seq) - (h2 /* seq) & (h1 (#) h2) /* seq = (h1 /* seq) (#) (h2 /* seq) ) ) A1: (dom h1) /\ (dom h2) c= dom h1 by XBOOLE_1:17; A2: (dom h1) /\ (dom h2) c= dom h2 by XBOOLE_1:17; assume A3: rng seq c= (dom h1) /\ (dom h2) ; ::_thesis: ( (h1 + h2) /* seq = (h1 /* seq) + (h2 /* seq) & (h1 - h2) /* seq = (h1 /* seq) - (h2 /* seq) & (h1 (#) h2) /* seq = (h1 /* seq) (#) (h2 /* seq) ) then A4: rng seq c= dom (h1 + h2) by VALUED_1:def_1; now__::_thesis:_for_n_being_Element_of_NAT_holds_((h1_+_h2)_/*_seq)_._n_=_((h1_/*_seq)_._n)_+_((h2_/*_seq)_._n) let n be Element of NAT ; ::_thesis: ((h1 + h2) /* seq) . n = ((h1 /* seq) . n) + ((h2 /* seq) . n) A5: seq . n in rng seq by VALUED_0:28; thus ((h1 + h2) /* seq) . n = (h1 + h2) . (seq . n) by A4, FUNCT_2:108 .= (h1 . (seq . n)) + (h2 . (seq . n)) by A4, A5, VALUED_1:def_1 .= ((h1 /* seq) . n) + (h2 . (seq . n)) by A3, A1, FUNCT_2:108, XBOOLE_1:1 .= ((h1 /* seq) . n) + ((h2 /* seq) . n) by A3, A2, FUNCT_2:108, XBOOLE_1:1 ; ::_thesis: verum end; hence (h1 + h2) /* seq = (h1 /* seq) + (h2 /* seq) by SEQ_1:7; ::_thesis: ( (h1 - h2) /* seq = (h1 /* seq) - (h2 /* seq) & (h1 (#) h2) /* seq = (h1 /* seq) (#) (h2 /* seq) ) A6: rng seq c= dom (h1 - h2) by A3, VALUED_1:12; now__::_thesis:_for_n_being_Element_of_NAT_holds_((h1_-_h2)_/*_seq)_._n_=_((h1_/*_seq)_._n)_-_((h2_/*_seq)_._n) let n be Element of NAT ; ::_thesis: ((h1 - h2) /* seq) . n = ((h1 /* seq) . n) - ((h2 /* seq) . n) A7: seq . n in rng seq by VALUED_0:28; thus ((h1 - h2) /* seq) . n = (h1 - h2) . (seq . n) by A6, FUNCT_2:108 .= (h1 . (seq . n)) - (h2 . (seq . n)) by A6, A7, VALUED_1:13 .= ((h1 /* seq) . n) - (h2 . (seq . n)) by A3, A1, FUNCT_2:108, XBOOLE_1:1 .= ((h1 /* seq) . n) - ((h2 /* seq) . n) by A3, A2, FUNCT_2:108, XBOOLE_1:1 ; ::_thesis: verum end; hence (h1 - h2) /* seq = (h1 /* seq) - (h2 /* seq) by Th1; ::_thesis: (h1 (#) h2) /* seq = (h1 /* seq) (#) (h2 /* seq) A8: rng seq c= dom (h1 (#) h2) by A3, VALUED_1:def_4; now__::_thesis:_for_n_being_Element_of_NAT_holds_((h1_(#)_h2)_/*_seq)_._n_=_((h1_/*_seq)_._n)_*_((h2_/*_seq)_._n) let n be Element of NAT ; ::_thesis: ((h1 (#) h2) /* seq) . n = ((h1 /* seq) . n) * ((h2 /* seq) . n) thus ((h1 (#) h2) /* seq) . n = (h1 (#) h2) . (seq . n) by A8, FUNCT_2:108 .= (h1 . (seq . n)) * (h2 . (seq . n)) by VALUED_1:5 .= ((h1 /* seq) . n) * (h2 . (seq . n)) by A3, A1, FUNCT_2:108, XBOOLE_1:1 .= ((h1 /* seq) . n) * ((h2 /* seq) . n) by A3, A2, FUNCT_2:108, XBOOLE_1:1 ; ::_thesis: verum end; hence (h1 (#) h2) /* seq = (h1 /* seq) (#) (h2 /* seq) by SEQ_1:8; ::_thesis: verum end; theorem Th9: :: RFUNCT_2:9 for W being non empty set for h being PartFunc of W,REAL for seq being sequence of W for r being real number st rng seq c= dom h holds (r (#) h) /* seq = r (#) (h /* seq) proof let W be non empty set ; ::_thesis: for h being PartFunc of W,REAL for seq being sequence of W for r being real number st rng seq c= dom h holds (r (#) h) /* seq = r (#) (h /* seq) let h be PartFunc of W,REAL; ::_thesis: for seq being sequence of W for r being real number st rng seq c= dom h holds (r (#) h) /* seq = r (#) (h /* seq) let seq be sequence of W; ::_thesis: for r being real number st rng seq c= dom h holds (r (#) h) /* seq = r (#) (h /* seq) let r be real number ; ::_thesis: ( rng seq c= dom h implies (r (#) h) /* seq = r (#) (h /* seq) ) assume A1: rng seq c= dom h ; ::_thesis: (r (#) h) /* seq = r (#) (h /* seq) then A2: rng seq c= dom (r (#) h) by VALUED_1:def_5; now__::_thesis:_for_n_being_Element_of_NAT_holds_((r_(#)_h)_/*_seq)_._n_=_r_*_((h_/*_seq)_._n) let n be Element of NAT ; ::_thesis: ((r (#) h) /* seq) . n = r * ((h /* seq) . n) A3: seq . n in rng seq by VALUED_0:28; thus ((r (#) h) /* seq) . n = (r (#) h) . (seq . n) by A2, FUNCT_2:108 .= r * (h . (seq . n)) by A2, A3, VALUED_1:def_5 .= r * ((h /* seq) . n) by A1, FUNCT_2:108 ; ::_thesis: verum end; hence (r (#) h) /* seq = r (#) (h /* seq) by SEQ_1:9; ::_thesis: verum end; theorem :: RFUNCT_2:10 for W being non empty set for h being PartFunc of W,REAL for seq being sequence of W st rng seq c= dom h holds ( abs (h /* seq) = (abs h) /* seq & - (h /* seq) = (- h) /* seq ) proof let W be non empty set ; ::_thesis: for h being PartFunc of W,REAL for seq being sequence of W st rng seq c= dom h holds ( abs (h /* seq) = (abs h) /* seq & - (h /* seq) = (- h) /* seq ) let h be PartFunc of W,REAL; ::_thesis: for seq being sequence of W st rng seq c= dom h holds ( abs (h /* seq) = (abs h) /* seq & - (h /* seq) = (- h) /* seq ) let seq be sequence of W; ::_thesis: ( rng seq c= dom h implies ( abs (h /* seq) = (abs h) /* seq & - (h /* seq) = (- h) /* seq ) ) assume A1: rng seq c= dom h ; ::_thesis: ( abs (h /* seq) = (abs h) /* seq & - (h /* seq) = (- h) /* seq ) then A2: rng seq c= dom (abs h) by VALUED_1:def_11; now__::_thesis:_for_n_being_Element_of_NAT_holds_(abs_(h_/*_seq))_._n_=_((abs_h)_/*_seq)_._n let n be Element of NAT ; ::_thesis: (abs (h /* seq)) . n = ((abs h) /* seq) . n thus (abs (h /* seq)) . n = abs ((h /* seq) . n) by SEQ_1:12 .= abs (h . (seq . n)) by A1, FUNCT_2:108 .= (abs h) . (seq . n) by VALUED_1:18 .= ((abs h) /* seq) . n by A2, FUNCT_2:108 ; ::_thesis: verum end; hence abs (h /* seq) = (abs h) /* seq by FUNCT_2:63; ::_thesis: - (h /* seq) = (- h) /* seq thus - (h /* seq) = (- 1) (#) (h /* seq) .= ((- 1) (#) h) /* seq by A1, Th9 .= (- h) /* seq ; ::_thesis: verum end; theorem :: RFUNCT_2:11 for W being non empty set for h being PartFunc of W,REAL for seq being sequence of W st rng seq c= dom (h ^) holds h /* seq is non-zero proof let W be non empty set ; ::_thesis: for h being PartFunc of W,REAL for seq being sequence of W st rng seq c= dom (h ^) holds h /* seq is non-zero let h be PartFunc of W,REAL; ::_thesis: for seq being sequence of W st rng seq c= dom (h ^) holds h /* seq is non-zero let seq be sequence of W; ::_thesis: ( rng seq c= dom (h ^) implies h /* seq is non-zero ) assume A1: rng seq c= dom (h ^) ; ::_thesis: h /* seq is non-zero then A2: ( (dom h) \ (h " {0}) c= dom h & rng seq c= (dom h) \ (h " {0}) ) by RFUNCT_1:def_2, XBOOLE_1:36; now__::_thesis:_for_n_being_Element_of_NAT_holds_not_(h_/*_seq)_._n_=_0 given n being Element of NAT such that A3: (h /* seq) . n = 0 ; ::_thesis: contradiction seq . n in rng seq by VALUED_0:28; then seq . n in dom (h ^) by A1; then seq . n in (dom h) \ (h " {0}) by RFUNCT_1:def_2; then ( seq . n in dom h & not seq . n in h " {0} ) by XBOOLE_0:def_5; then A4: not h . (seq . n) in {0} by FUNCT_1:def_7; h . (seq . n) = 0 by A2, A3, FUNCT_2:108, XBOOLE_1:1; hence contradiction by A4, TARSKI:def_1; ::_thesis: verum end; hence h /* seq is non-zero by SEQ_1:5; ::_thesis: verum end; theorem :: RFUNCT_2:12 for W being non empty set for h being PartFunc of W,REAL for seq being sequence of W st rng seq c= dom (h ^) holds (h ^) /* seq = (h /* seq) " proof let W be non empty set ; ::_thesis: for h being PartFunc of W,REAL for seq being sequence of W st rng seq c= dom (h ^) holds (h ^) /* seq = (h /* seq) " let h be PartFunc of W,REAL; ::_thesis: for seq being sequence of W st rng seq c= dom (h ^) holds (h ^) /* seq = (h /* seq) " let seq be sequence of W; ::_thesis: ( rng seq c= dom (h ^) implies (h ^) /* seq = (h /* seq) " ) assume A1: rng seq c= dom (h ^) ; ::_thesis: (h ^) /* seq = (h /* seq) " then A2: ( (dom h) \ (h " {0}) c= dom h & rng seq c= (dom h) \ (h " {0}) ) by RFUNCT_1:def_2, XBOOLE_1:36; now__::_thesis:_for_n_being_Element_of_NAT_holds_((h_^)_/*_seq)_._n_=_((h_/*_seq)_")_._n let n be Element of NAT ; ::_thesis: ((h ^) /* seq) . n = ((h /* seq) ") . n A3: seq . n in rng seq by VALUED_0:28; thus ((h ^) /* seq) . n = (h ^) . (seq . n) by A1, FUNCT_2:108 .= (h . (seq . n)) " by A1, A3, RFUNCT_1:def_2 .= ((h /* seq) . n) " by A2, FUNCT_2:108, XBOOLE_1:1 .= ((h /* seq) ") . n by VALUED_1:10 ; ::_thesis: verum end; hence (h ^) /* seq = (h /* seq) " by FUNCT_2:63; ::_thesis: verum end; theorem :: RFUNCT_2:13 for W being non empty set for h1, h2 being PartFunc of W,REAL for seq being sequence of W st h1 is total & h2 is total holds ( (h1 + h2) /* seq = (h1 /* seq) + (h2 /* seq) & (h1 - h2) /* seq = (h1 /* seq) - (h2 /* seq) & (h1 (#) h2) /* seq = (h1 /* seq) (#) (h2 /* seq) ) proof let W be non empty set ; ::_thesis: for h1, h2 being PartFunc of W,REAL for seq being sequence of W st h1 is total & h2 is total holds ( (h1 + h2) /* seq = (h1 /* seq) + (h2 /* seq) & (h1 - h2) /* seq = (h1 /* seq) - (h2 /* seq) & (h1 (#) h2) /* seq = (h1 /* seq) (#) (h2 /* seq) ) let h1, h2 be PartFunc of W,REAL; ::_thesis: for seq being sequence of W st h1 is total & h2 is total holds ( (h1 + h2) /* seq = (h1 /* seq) + (h2 /* seq) & (h1 - h2) /* seq = (h1 /* seq) - (h2 /* seq) & (h1 (#) h2) /* seq = (h1 /* seq) (#) (h2 /* seq) ) let seq be sequence of W; ::_thesis: ( h1 is total & h2 is total implies ( (h1 + h2) /* seq = (h1 /* seq) + (h2 /* seq) & (h1 - h2) /* seq = (h1 /* seq) - (h2 /* seq) & (h1 (#) h2) /* seq = (h1 /* seq) (#) (h2 /* seq) ) ) assume ( h1 is total & h2 is total ) ; ::_thesis: ( (h1 + h2) /* seq = (h1 /* seq) + (h2 /* seq) & (h1 - h2) /* seq = (h1 /* seq) - (h2 /* seq) & (h1 (#) h2) /* seq = (h1 /* seq) (#) (h2 /* seq) ) then dom (h1 + h2) = W by PARTFUN1:def_2; then (dom h1) /\ (dom h2) = W by VALUED_1:def_1; then A1: rng seq c= (dom h1) /\ (dom h2) ; hence (h1 + h2) /* seq = (h1 /* seq) + (h2 /* seq) by Th8; ::_thesis: ( (h1 - h2) /* seq = (h1 /* seq) - (h2 /* seq) & (h1 (#) h2) /* seq = (h1 /* seq) (#) (h2 /* seq) ) thus (h1 - h2) /* seq = (h1 /* seq) - (h2 /* seq) by A1, Th8; ::_thesis: (h1 (#) h2) /* seq = (h1 /* seq) (#) (h2 /* seq) thus (h1 (#) h2) /* seq = (h1 /* seq) (#) (h2 /* seq) by A1, Th8; ::_thesis: verum end; theorem :: RFUNCT_2:14 for r being Element of REAL for W being non empty set for h being PartFunc of W,REAL for seq being sequence of W st h is total holds (r (#) h) /* seq = r (#) (h /* seq) proof let r be Element of REAL ; ::_thesis: for W being non empty set for h being PartFunc of W,REAL for seq being sequence of W st h is total holds (r (#) h) /* seq = r (#) (h /* seq) let W be non empty set ; ::_thesis: for h being PartFunc of W,REAL for seq being sequence of W st h is total holds (r (#) h) /* seq = r (#) (h /* seq) let h be PartFunc of W,REAL; ::_thesis: for seq being sequence of W st h is total holds (r (#) h) /* seq = r (#) (h /* seq) let seq be sequence of W; ::_thesis: ( h is total implies (r (#) h) /* seq = r (#) (h /* seq) ) assume h is total ; ::_thesis: (r (#) h) /* seq = r (#) (h /* seq) then dom h = W by PARTFUN1:def_2; then rng seq c= dom h ; hence (r (#) h) /* seq = r (#) (h /* seq) by Th9; ::_thesis: verum end; theorem :: RFUNCT_2:15 for X being set for W being non empty set for h being PartFunc of W,REAL for seq being sequence of W st rng seq c= dom (h | X) holds abs ((h | X) /* seq) = ((abs h) | X) /* seq proof let X be set ; ::_thesis: for W being non empty set for h being PartFunc of W,REAL for seq being sequence of W st rng seq c= dom (h | X) holds abs ((h | X) /* seq) = ((abs h) | X) /* seq let W be non empty set ; ::_thesis: for h being PartFunc of W,REAL for seq being sequence of W st rng seq c= dom (h | X) holds abs ((h | X) /* seq) = ((abs h) | X) /* seq let h be PartFunc of W,REAL; ::_thesis: for seq being sequence of W st rng seq c= dom (h | X) holds abs ((h | X) /* seq) = ((abs h) | X) /* seq let seq be sequence of W; ::_thesis: ( rng seq c= dom (h | X) implies abs ((h | X) /* seq) = ((abs h) | X) /* seq ) assume A1: rng seq c= dom (h | X) ; ::_thesis: abs ((h | X) /* seq) = ((abs h) | X) /* seq A2: dom (h | X) = (dom h) /\ X by RELAT_1:61 .= (dom (abs h)) /\ X by VALUED_1:def_11 .= dom ((abs h) | X) by RELAT_1:61 ; now__::_thesis:_for_n_being_Element_of_NAT_holds_(abs_((h_|_X)_/*_seq))_._n_=_(((abs_h)_|_X)_/*_seq)_._n let n be Element of NAT ; ::_thesis: (abs ((h | X) /* seq)) . n = (((abs h) | X) /* seq) . n A3: seq . n in rng seq by VALUED_0:28; then seq . n in dom (h | X) by A1; then seq . n in (dom h) /\ X by RELAT_1:61; then A4: seq . n in X by XBOOLE_0:def_4; thus (abs ((h | X) /* seq)) . n = abs (((h | X) /* seq) . n) by SEQ_1:12 .= abs ((h | X) . (seq . n)) by A1, FUNCT_2:108 .= abs (h . (seq . n)) by A1, A3, FUNCT_1:47 .= (abs h) . (seq . n) by VALUED_1:18 .= ((abs h) | X) . (seq . n) by A4, FUNCT_1:49 .= (((abs h) | X) /* seq) . n by A1, A2, FUNCT_2:108 ; ::_thesis: verum end; hence abs ((h | X) /* seq) = ((abs h) | X) /* seq by FUNCT_2:63; ::_thesis: verum end; theorem :: RFUNCT_2:16 for X being set for W being non empty set for h being PartFunc of W,REAL for seq being sequence of W st rng seq c= dom (h | X) & h " {0} = {} holds ((h ^) | X) /* seq = ((h | X) /* seq) " proof let X be set ; ::_thesis: for W being non empty set for h being PartFunc of W,REAL for seq being sequence of W st rng seq c= dom (h | X) & h " {0} = {} holds ((h ^) | X) /* seq = ((h | X) /* seq) " let W be non empty set ; ::_thesis: for h being PartFunc of W,REAL for seq being sequence of W st rng seq c= dom (h | X) & h " {0} = {} holds ((h ^) | X) /* seq = ((h | X) /* seq) " let h be PartFunc of W,REAL; ::_thesis: for seq being sequence of W st rng seq c= dom (h | X) & h " {0} = {} holds ((h ^) | X) /* seq = ((h | X) /* seq) " let seq be sequence of W; ::_thesis: ( rng seq c= dom (h | X) & h " {0} = {} implies ((h ^) | X) /* seq = ((h | X) /* seq) " ) assume that A1: rng seq c= dom (h | X) and A2: h " {0} = {} ; ::_thesis: ((h ^) | X) /* seq = ((h | X) /* seq) " now__::_thesis:_for_x_being_set_st_x_in_rng_seq_holds_ x_in_dom_((h_^)_|_X) let x be set ; ::_thesis: ( x in rng seq implies x in dom ((h ^) | X) ) assume x in rng seq ; ::_thesis: x in dom ((h ^) | X) then x in dom (h | X) by A1; then A3: x in (dom h) /\ X by RELAT_1:61; then x in (dom h) \ (h " {0}) by A2, XBOOLE_0:def_4; then A4: x in dom (h ^) by RFUNCT_1:def_2; x in X by A3, XBOOLE_0:def_4; then x in (dom (h ^)) /\ X by A4, XBOOLE_0:def_4; hence x in dom ((h ^) | X) by RELAT_1:61; ::_thesis: verum end; then A5: rng seq c= dom ((h ^) | X) by TARSKI:def_3; now__::_thesis:_for_n_being_Element_of_NAT_holds_(((h_^)_|_X)_/*_seq)_._n_=_(((h_|_X)_/*_seq)_")_._n let n be Element of NAT ; ::_thesis: (((h ^) | X) /* seq) . n = (((h | X) /* seq) ") . n A6: seq . n in rng seq by VALUED_0:28; then seq . n in dom (h | X) by A1; then A7: seq . n in (dom h) /\ X by RELAT_1:61; then A8: seq . n in X by XBOOLE_0:def_4; seq . n in (dom h) \ (h " {0}) by A2, A7, XBOOLE_0:def_4; then A9: seq . n in dom (h ^) by RFUNCT_1:def_2; thus (((h ^) | X) /* seq) . n = ((h ^) | X) . (seq . n) by A5, FUNCT_2:108 .= (h ^) . (seq . n) by A8, FUNCT_1:49 .= (h . (seq . n)) " by A9, RFUNCT_1:def_2 .= ((h | X) . (seq . n)) " by A1, A6, FUNCT_1:47 .= (((h | X) /* seq) . n) " by A1, FUNCT_2:108 .= (((h | X) /* seq) ") . n by VALUED_1:10 ; ::_thesis: verum end; hence ((h ^) | X) /* seq = ((h | X) /* seq) " by FUNCT_2:63; ::_thesis: verum end; registration let Z be set ; let f be one-to-one Function; clusterf | Z -> one-to-one ; coherence f | Z is one-to-one by FUNCT_1:52; end; theorem :: RFUNCT_2:17 for X being set for h being one-to-one Function holds (h | X) " = (h ") | (h .: X) proof let X be set ; ::_thesis: for h being one-to-one Function holds (h | X) " = (h ") | (h .: X) let h be one-to-one Function; ::_thesis: (h | X) " = (h ") | (h .: X) reconsider hX = h | X as one-to-one Function ; now__::_thesis:_for_r_being_set_holds_ (_(_r_in_dom_((h_|_X)_")_implies_r_in_dom_((h_")_|_(h_.:_X))_)_&_(_r_in_dom_((h_")_|_(h_.:_X))_implies_r_in_dom_((h_|_X)_")_)_) let r be set ; ::_thesis: ( ( r in dom ((h | X) ") implies r in dom ((h ") | (h .: X)) ) & ( r in dom ((h ") | (h .: X)) implies r in dom ((h | X) ") ) ) thus ( r in dom ((h | X) ") implies r in dom ((h ") | (h .: X)) ) ::_thesis: ( r in dom ((h ") | (h .: X)) implies r in dom ((h | X) ") ) proof assume r in dom ((h | X) ") ; ::_thesis: r in dom ((h ") | (h .: X)) then r in rng hX by FUNCT_1:33; then consider g being set such that A1: g in dom (h | X) and A2: (h | X) . g = r by FUNCT_1:def_3; A3: h . g = r by A1, A2, FUNCT_1:47; A4: g in (dom h) /\ X by A1, RELAT_1:61; then g in dom h by XBOOLE_0:def_4; then r in rng h by A3, FUNCT_1:def_3; then A5: r in dom (h ") by FUNCT_1:33; ( g in dom h & g in X ) by A4, XBOOLE_0:def_4; then r in h .: X by A3, FUNCT_1:def_6; then r in (dom (h ")) /\ (h .: X) by A5, XBOOLE_0:def_4; hence r in dom ((h ") | (h .: X)) by RELAT_1:61; ::_thesis: verum end; assume r in dom ((h ") | (h .: X)) ; ::_thesis: r in dom ((h | X) ") then r in (dom (h ")) /\ (h .: X) by RELAT_1:61; then r in h .: X by XBOOLE_0:def_4; then consider t being set such that A6: t in dom h and A7: t in X and A8: h . t = r by FUNCT_1:def_6; t in (dom h) /\ X by A6, A7, XBOOLE_0:def_4; then A9: t in dom (h | X) by RELAT_1:61; (h | X) . t = r by A7, A8, FUNCT_1:49; then r in rng hX by A9, FUNCT_1:def_3; hence r in dom ((h | X) ") by FUNCT_1:33; ::_thesis: verum end; then A10: dom (hX ") = dom ((h ") | (h .: X)) by TARSKI:1; now__::_thesis:_for_r_being_set_holds_ (_not_r_in_dom_((h_|_X)_")_or_not_((h_|_X)_")_._r_<>_((h_")_|_(h_.:_X))_._r_) given r being set such that A11: r in dom ((h | X) ") and A12: ((h | X) ") . r <> ((h ") | (h .: X)) . r ; ::_thesis: contradiction r in (dom (h ")) /\ (h .: X) by A10, A11, RELAT_1:61; then r in h .: X by XBOOLE_0:def_4; then consider t being set such that t in dom h and t in X and A13: h . t = r by FUNCT_1:def_6; r in rng hX by A11, FUNCT_1:33; then consider g being set such that A14: g in dom (h | X) and A15: (h | X) . g = r by FUNCT_1:def_3; A16: h . g = r by A14, A15, FUNCT_1:47; g in (dom h) /\ X by A14, RELAT_1:61; then A17: g in dom h by XBOOLE_0:def_4; (hX ") . r <> (h ") . r by A10, A11, A12, FUNCT_1:47; then g <> (h ") . (h . t) by A14, A15, A13, FUNCT_1:34; hence contradiction by A13, A17, A16, FUNCT_1:34; ::_thesis: verum end; hence (h | X) " = (h ") | (h .: X) by A10, FUNCT_1:2; ::_thesis: verum end; theorem Th18: :: RFUNCT_2:18 for W being non empty set for h being PartFunc of W,REAL st rng h is real-bounded & upper_bound (rng h) = lower_bound (rng h) holds h is V8() proof let W be non empty set ; ::_thesis: for h being PartFunc of W,REAL st rng h is real-bounded & upper_bound (rng h) = lower_bound (rng h) holds h is V8() let h be PartFunc of W,REAL; ::_thesis: ( rng h is real-bounded & upper_bound (rng h) = lower_bound (rng h) implies h is V8() ) assume A1: ( rng h is real-bounded & upper_bound (rng h) = lower_bound (rng h) ) ; ::_thesis: h is V8() assume h is V8() ; ::_thesis: contradiction then consider x1, x2 being set such that A2: ( x1 in dom h & x2 in dom h ) and A3: h . x1 <> h . x2 by FUNCT_1:def_10; ( h . x1 in rng h & h . x2 in rng h ) by A2, FUNCT_1:def_3; hence contradiction by A1, A3, SEQ_4:12; ::_thesis: verum end; theorem :: RFUNCT_2:19 for Y being set for W being non empty set for h being PartFunc of W,REAL st h .: Y is real-bounded & upper_bound (h .: Y) = lower_bound (h .: Y) holds h | Y is V8() proof let Y be set ; ::_thesis: for W being non empty set for h being PartFunc of W,REAL st h .: Y is real-bounded & upper_bound (h .: Y) = lower_bound (h .: Y) holds h | Y is V8() let W be non empty set ; ::_thesis: for h being PartFunc of W,REAL st h .: Y is real-bounded & upper_bound (h .: Y) = lower_bound (h .: Y) holds h | Y is V8() let h be PartFunc of W,REAL; ::_thesis: ( h .: Y is real-bounded & upper_bound (h .: Y) = lower_bound (h .: Y) implies h | Y is V8() ) rng (h | Y) = h .: Y by RELAT_1:115; hence ( h .: Y is real-bounded & upper_bound (h .: Y) = lower_bound (h .: Y) implies h | Y is V8() ) by Th18; ::_thesis: verum end; definition let h be PartFunc of REAL,REAL; redefine attr h is increasing means :Def1: :: RFUNCT_2:def 1 for r1, r2 being Element of REAL st r1 in dom h & r2 in dom h & r1 < r2 holds h . r1 < h . r2; compatibility ( h is increasing iff for r1, r2 being Element of REAL st r1 in dom h & r2 in dom h & r1 < r2 holds h . r1 < h . r2 ) proof thus ( h is increasing implies for r1, r2 being Element of REAL st r1 in dom h & r2 in dom h & r1 < r2 holds h . r1 < h . r2 ) by VALUED_0:def_13; ::_thesis: ( ( for r1, r2 being Element of REAL st r1 in dom h & r2 in dom h & r1 < r2 holds h . r1 < h . r2 ) implies h is increasing ) assume A1: for r1, r2 being Element of REAL st r1 in dom h & r2 in dom h & r1 < r2 holds h . r1 < h . r2 ; ::_thesis: h is increasing let e1 be ext-real number ; :: according to VALUED_0:def_13 ::_thesis: for b1 being set holds ( not e1 in dom h or not b1 in dom h or b1 <= e1 or not h . b1 <= h . e1 ) let e2 be ext-real number ; ::_thesis: ( not e1 in dom h or not e2 in dom h or e2 <= e1 or not h . e2 <= h . e1 ) thus ( not e1 in dom h or not e2 in dom h or e2 <= e1 or not h . e2 <= h . e1 ) by A1; ::_thesis: verum end; redefine attr h is decreasing means :Def2: :: RFUNCT_2:def 2 for r1, r2 being Element of REAL st r1 in dom h & r2 in dom h & r1 < r2 holds h . r2 < h . r1; compatibility ( h is decreasing iff for r1, r2 being Element of REAL st r1 in dom h & r2 in dom h & r1 < r2 holds h . r2 < h . r1 ) proof thus ( h is decreasing implies for r1, r2 being Element of REAL st r1 in dom h & r2 in dom h & r1 < r2 holds h . r1 > h . r2 ) by VALUED_0:def_14; ::_thesis: ( ( for r1, r2 being Element of REAL st r1 in dom h & r2 in dom h & r1 < r2 holds h . r2 < h . r1 ) implies h is decreasing ) assume A2: for r1, r2 being Element of REAL st r1 in dom h & r2 in dom h & r1 < r2 holds h . r1 > h . r2 ; ::_thesis: h is decreasing let e1 be ext-real number ; :: according to VALUED_0:def_14 ::_thesis: for b1 being set holds ( not e1 in dom h or not b1 in dom h or b1 <= e1 or not h . e1 <= h . b1 ) let e2 be ext-real number ; ::_thesis: ( not e1 in dom h or not e2 in dom h or e2 <= e1 or not h . e1 <= h . e2 ) thus ( not e1 in dom h or not e2 in dom h or e2 <= e1 or not h . e1 <= h . e2 ) by A2; ::_thesis: verum end; redefine attr h is non-decreasing means :Def3: :: RFUNCT_2:def 3 for r1, r2 being Element of REAL st r1 in dom h & r2 in dom h & r1 < r2 holds h . r1 <= h . r2; compatibility ( h is non-decreasing iff for r1, r2 being Element of REAL st r1 in dom h & r2 in dom h & r1 < r2 holds h . r1 <= h . r2 ) proof thus ( h is non-decreasing implies for r1, r2 being Element of REAL st r1 in dom h & r2 in dom h & r1 < r2 holds h . r1 <= h . r2 ) by VALUED_0:def_15; ::_thesis: ( ( for r1, r2 being Element of REAL st r1 in dom h & r2 in dom h & r1 < r2 holds h . r1 <= h . r2 ) implies h is non-decreasing ) assume A3: for r1, r2 being Element of REAL st r1 in dom h & r2 in dom h & r1 < r2 holds h . r1 <= h . r2 ; ::_thesis: h is non-decreasing let e1 be ext-real number ; :: according to VALUED_0:def_15 ::_thesis: for b1 being set holds ( not e1 in dom h or not b1 in dom h or not e1 <= b1 or h . e1 <= h . b1 ) let e2 be ext-real number ; ::_thesis: ( not e1 in dom h or not e2 in dom h or not e1 <= e2 or h . e1 <= h . e2 ) assume A4: ( e1 in dom h & e2 in dom h ) ; ::_thesis: ( not e1 <= e2 or h . e1 <= h . e2 ) assume e1 <= e2 ; ::_thesis: h . e1 <= h . e2 then ( e1 < e2 or e1 = e2 ) by XXREAL_0:1; hence h . e1 <= h . e2 by A3, A4; ::_thesis: verum end; redefine attr h is non-increasing means :Def4: :: RFUNCT_2:def 4 for r1, r2 being Element of REAL st r1 in dom h & r2 in dom h & r1 < r2 holds h . r2 <= h . r1; compatibility ( h is non-increasing iff for r1, r2 being Element of REAL st r1 in dom h & r2 in dom h & r1 < r2 holds h . r2 <= h . r1 ) proof thus ( h is non-increasing implies for r1, r2 being Element of REAL st r1 in dom h & r2 in dom h & r1 < r2 holds h . r1 >= h . r2 ) by VALUED_0:def_16; ::_thesis: ( ( for r1, r2 being Element of REAL st r1 in dom h & r2 in dom h & r1 < r2 holds h . r2 <= h . r1 ) implies h is non-increasing ) assume A5: for r1, r2 being Element of REAL st r1 in dom h & r2 in dom h & r1 < r2 holds h . r1 >= h . r2 ; ::_thesis: h is non-increasing let e1 be ext-real number ; :: according to VALUED_0:def_16 ::_thesis: for b1 being set holds ( not e1 in dom h or not b1 in dom h or not e1 <= b1 or h . b1 <= h . e1 ) let e2 be ext-real number ; ::_thesis: ( not e1 in dom h or not e2 in dom h or not e1 <= e2 or h . e2 <= h . e1 ) assume A6: ( e1 in dom h & e2 in dom h ) ; ::_thesis: ( not e1 <= e2 or h . e2 <= h . e1 ) assume e1 <= e2 ; ::_thesis: h . e2 <= h . e1 then ( e1 < e2 or e1 = e2 ) by XXREAL_0:1; hence h . e2 <= h . e1 by A5, A6; ::_thesis: verum end; end; :: deftheorem Def1 defines increasing RFUNCT_2:def_1_:_ for h being PartFunc of REAL,REAL holds ( h is increasing iff for r1, r2 being Element of REAL st r1 in dom h & r2 in dom h & r1 < r2 holds h . r1 < h . r2 ); :: deftheorem Def2 defines decreasing RFUNCT_2:def_2_:_ for h being PartFunc of REAL,REAL holds ( h is decreasing iff for r1, r2 being Element of REAL st r1 in dom h & r2 in dom h & r1 < r2 holds h . r2 < h . r1 ); :: deftheorem Def3 defines non-decreasing RFUNCT_2:def_3_:_ for h being PartFunc of REAL,REAL holds ( h is non-decreasing iff for r1, r2 being Element of REAL st r1 in dom h & r2 in dom h & r1 < r2 holds h . r1 <= h . r2 ); :: deftheorem Def4 defines non-increasing RFUNCT_2:def_4_:_ for h being PartFunc of REAL,REAL holds ( h is non-increasing iff for r1, r2 being Element of REAL st r1 in dom h & r2 in dom h & r1 < r2 holds h . r2 <= h . r1 ); theorem Th20: :: RFUNCT_2:20 for Y being set for h being PartFunc of REAL,REAL holds ( h | Y is increasing iff for r1, r2 being Element of REAL st r1 in Y /\ (dom h) & r2 in Y /\ (dom h) & r1 < r2 holds h . r1 < h . r2 ) proof let Y be set ; ::_thesis: for h being PartFunc of REAL,REAL holds ( h | Y is increasing iff for r1, r2 being Element of REAL st r1 in Y /\ (dom h) & r2 in Y /\ (dom h) & r1 < r2 holds h . r1 < h . r2 ) let h be PartFunc of REAL,REAL; ::_thesis: ( h | Y is increasing iff for r1, r2 being Element of REAL st r1 in Y /\ (dom h) & r2 in Y /\ (dom h) & r1 < r2 holds h . r1 < h . r2 ) thus ( h | Y is increasing implies for r1, r2 being Element of REAL st r1 in Y /\ (dom h) & r2 in Y /\ (dom h) & r1 < r2 holds h . r2 > h . r1 ) ::_thesis: ( ( for r1, r2 being Element of REAL st r1 in Y /\ (dom h) & r2 in Y /\ (dom h) & r1 < r2 holds h . r1 < h . r2 ) implies h | Y is increasing ) proof assume A1: h | Y is increasing ; ::_thesis: for r1, r2 being Element of REAL st r1 in Y /\ (dom h) & r2 in Y /\ (dom h) & r1 < r2 holds h . r2 > h . r1 let r1, r2 be Element of REAL ; ::_thesis: ( r1 in Y /\ (dom h) & r2 in Y /\ (dom h) & r1 < r2 implies h . r2 > h . r1 ) assume that A2: r1 in Y /\ (dom h) and A3: r2 in Y /\ (dom h) and A4: r1 < r2 ; ::_thesis: h . r2 > h . r1 A5: r2 in dom (h | Y) by A3, RELAT_1:61; then A6: (h | Y) . r2 = h . r2 by FUNCT_1:47; A7: r1 in dom (h | Y) by A2, RELAT_1:61; then (h | Y) . r1 = h . r1 by FUNCT_1:47; hence h . r2 > h . r1 by A1, A4, A7, A5, A6, Def1; ::_thesis: verum end; assume A8: for r1, r2 being Element of REAL st r1 in Y /\ (dom h) & r2 in Y /\ (dom h) & r1 < r2 holds h . r2 > h . r1 ; ::_thesis: h | Y is increasing let r1 be Element of REAL ; :: according to RFUNCT_2:def_1 ::_thesis: for r2 being Element of REAL st r1 in dom (h | Y) & r2 in dom (h | Y) & r1 < r2 holds (h | Y) . r1 < (h | Y) . r2 let r2 be Element of REAL ; ::_thesis: ( r1 in dom (h | Y) & r2 in dom (h | Y) & r1 < r2 implies (h | Y) . r1 < (h | Y) . r2 ) assume that A9: ( r1 in dom (h | Y) & r2 in dom (h | Y) ) and A10: r1 < r2 ; ::_thesis: (h | Y) . r1 < (h | Y) . r2 A11: ( (h | Y) . r1 = h . r1 & (h | Y) . r2 = h . r2 ) by A9, FUNCT_1:47; ( r1 in Y /\ (dom h) & r2 in Y /\ (dom h) ) by A9, RELAT_1:61; hence (h | Y) . r1 < (h | Y) . r2 by A8, A10, A11; ::_thesis: verum end; theorem Th21: :: RFUNCT_2:21 for Y being set for h being PartFunc of REAL,REAL holds ( h | Y is decreasing iff for r1, r2 being Element of REAL st r1 in Y /\ (dom h) & r2 in Y /\ (dom h) & r1 < r2 holds h . r2 < h . r1 ) proof let Y be set ; ::_thesis: for h being PartFunc of REAL,REAL holds ( h | Y is decreasing iff for r1, r2 being Element of REAL st r1 in Y /\ (dom h) & r2 in Y /\ (dom h) & r1 < r2 holds h . r2 < h . r1 ) let h be PartFunc of REAL,REAL; ::_thesis: ( h | Y is decreasing iff for r1, r2 being Element of REAL st r1 in Y /\ (dom h) & r2 in Y /\ (dom h) & r1 < r2 holds h . r2 < h . r1 ) thus ( h | Y is decreasing implies for r1, r2 being Element of REAL st r1 in Y /\ (dom h) & r2 in Y /\ (dom h) & r1 < r2 holds h . r2 < h . r1 ) ::_thesis: ( ( for r1, r2 being Element of REAL st r1 in Y /\ (dom h) & r2 in Y /\ (dom h) & r1 < r2 holds h . r2 < h . r1 ) implies h | Y is decreasing ) proof assume A1: h | Y is decreasing ; ::_thesis: for r1, r2 being Element of REAL st r1 in Y /\ (dom h) & r2 in Y /\ (dom h) & r1 < r2 holds h . r2 < h . r1 let r1, r2 be Element of REAL ; ::_thesis: ( r1 in Y /\ (dom h) & r2 in Y /\ (dom h) & r1 < r2 implies h . r2 < h . r1 ) assume that A2: r1 in Y /\ (dom h) and A3: r2 in Y /\ (dom h) and A4: r1 < r2 ; ::_thesis: h . r2 < h . r1 A5: r2 in dom (h | Y) by A3, RELAT_1:61; then A6: (h | Y) . r2 = h . r2 by FUNCT_1:47; A7: r1 in dom (h | Y) by A2, RELAT_1:61; then (h | Y) . r1 = h . r1 by FUNCT_1:47; hence h . r2 < h . r1 by A1, A4, A7, A5, A6, Def2; ::_thesis: verum end; assume A8: for r1, r2 being Element of REAL st r1 in Y /\ (dom h) & r2 in Y /\ (dom h) & r1 < r2 holds h . r2 < h . r1 ; ::_thesis: h | Y is decreasing let r1 be Element of REAL ; :: according to RFUNCT_2:def_2 ::_thesis: for r2 being Element of REAL st r1 in dom (h | Y) & r2 in dom (h | Y) & r1 < r2 holds (h | Y) . r2 < (h | Y) . r1 let r2 be Element of REAL ; ::_thesis: ( r1 in dom (h | Y) & r2 in dom (h | Y) & r1 < r2 implies (h | Y) . r2 < (h | Y) . r1 ) assume that A9: ( r1 in dom (h | Y) & r2 in dom (h | Y) ) and A10: r1 < r2 ; ::_thesis: (h | Y) . r2 < (h | Y) . r1 A11: ( (h | Y) . r1 = h . r1 & (h | Y) . r2 = h . r2 ) by A9, FUNCT_1:47; ( r1 in Y /\ (dom h) & r2 in Y /\ (dom h) ) by A9, RELAT_1:61; hence (h | Y) . r2 < (h | Y) . r1 by A8, A10, A11; ::_thesis: verum end; theorem Th22: :: RFUNCT_2:22 for Y being set for h being PartFunc of REAL,REAL holds ( h | Y is non-decreasing iff for r1, r2 being Element of REAL st r1 in Y /\ (dom h) & r2 in Y /\ (dom h) & r1 < r2 holds h . r1 <= h . r2 ) proof let Y be set ; ::_thesis: for h being PartFunc of REAL,REAL holds ( h | Y is non-decreasing iff for r1, r2 being Element of REAL st r1 in Y /\ (dom h) & r2 in Y /\ (dom h) & r1 < r2 holds h . r1 <= h . r2 ) let h be PartFunc of REAL,REAL; ::_thesis: ( h | Y is non-decreasing iff for r1, r2 being Element of REAL st r1 in Y /\ (dom h) & r2 in Y /\ (dom h) & r1 < r2 holds h . r1 <= h . r2 ) thus ( h | Y is non-decreasing implies for r1, r2 being Element of REAL st r1 in Y /\ (dom h) & r2 in Y /\ (dom h) & r1 < r2 holds h . r1 <= h . r2 ) ::_thesis: ( ( for r1, r2 being Element of REAL st r1 in Y /\ (dom h) & r2 in Y /\ (dom h) & r1 < r2 holds h . r1 <= h . r2 ) implies h | Y is non-decreasing ) proof assume A1: h | Y is non-decreasing ; ::_thesis: for r1, r2 being Element of REAL st r1 in Y /\ (dom h) & r2 in Y /\ (dom h) & r1 < r2 holds h . r1 <= h . r2 let r1, r2 be Element of REAL ; ::_thesis: ( r1 in Y /\ (dom h) & r2 in Y /\ (dom h) & r1 < r2 implies h . r1 <= h . r2 ) assume that A2: r1 in Y /\ (dom h) and A3: r2 in Y /\ (dom h) and A4: r1 < r2 ; ::_thesis: h . r1 <= h . r2 A5: r2 in dom (h | Y) by A3, RELAT_1:61; then A6: (h | Y) . r2 = h . r2 by FUNCT_1:47; A7: r1 in dom (h | Y) by A2, RELAT_1:61; then (h | Y) . r1 = h . r1 by FUNCT_1:47; hence h . r1 <= h . r2 by A1, A4, A7, A5, A6, Def3; ::_thesis: verum end; assume A8: for r1, r2 being Element of REAL st r1 in Y /\ (dom h) & r2 in Y /\ (dom h) & r1 < r2 holds h . r1 <= h . r2 ; ::_thesis: h | Y is non-decreasing let r1 be Element of REAL ; :: according to RFUNCT_2:def_3 ::_thesis: for r2 being Element of REAL st r1 in dom (h | Y) & r2 in dom (h | Y) & r1 < r2 holds (h | Y) . r1 <= (h | Y) . r2 let r2 be Element of REAL ; ::_thesis: ( r1 in dom (h | Y) & r2 in dom (h | Y) & r1 < r2 implies (h | Y) . r1 <= (h | Y) . r2 ) assume that A9: ( r1 in dom (h | Y) & r2 in dom (h | Y) ) and A10: r1 < r2 ; ::_thesis: (h | Y) . r1 <= (h | Y) . r2 A11: ( (h | Y) . r1 = h . r1 & (h | Y) . r2 = h . r2 ) by A9, FUNCT_1:47; ( r1 in Y /\ (dom h) & r2 in Y /\ (dom h) ) by A9, RELAT_1:61; hence (h | Y) . r1 <= (h | Y) . r2 by A8, A10, A11; ::_thesis: verum end; theorem Th23: :: RFUNCT_2:23 for Y being set for h being PartFunc of REAL,REAL holds ( h | Y is non-increasing iff for r1, r2 being Element of REAL st r1 in Y /\ (dom h) & r2 in Y /\ (dom h) & r1 < r2 holds h . r2 <= h . r1 ) proof let Y be set ; ::_thesis: for h being PartFunc of REAL,REAL holds ( h | Y is non-increasing iff for r1, r2 being Element of REAL st r1 in Y /\ (dom h) & r2 in Y /\ (dom h) & r1 < r2 holds h . r2 <= h . r1 ) let h be PartFunc of REAL,REAL; ::_thesis: ( h | Y is non-increasing iff for r1, r2 being Element of REAL st r1 in Y /\ (dom h) & r2 in Y /\ (dom h) & r1 < r2 holds h . r2 <= h . r1 ) thus ( h | Y is non-increasing implies for r1, r2 being Element of REAL st r1 in Y /\ (dom h) & r2 in Y /\ (dom h) & r1 < r2 holds h . r2 <= h . r1 ) ::_thesis: ( ( for r1, r2 being Element of REAL st r1 in Y /\ (dom h) & r2 in Y /\ (dom h) & r1 < r2 holds h . r2 <= h . r1 ) implies h | Y is non-increasing ) proof assume A1: h | Y is non-increasing ; ::_thesis: for r1, r2 being Element of REAL st r1 in Y /\ (dom h) & r2 in Y /\ (dom h) & r1 < r2 holds h . r2 <= h . r1 let r1, r2 be Element of REAL ; ::_thesis: ( r1 in Y /\ (dom h) & r2 in Y /\ (dom h) & r1 < r2 implies h . r2 <= h . r1 ) assume that A2: r1 in Y /\ (dom h) and A3: r2 in Y /\ (dom h) and A4: r1 < r2 ; ::_thesis: h . r2 <= h . r1 A5: r2 in dom (h | Y) by A3, RELAT_1:61; then A6: (h | Y) . r2 = h . r2 by FUNCT_1:47; A7: r1 in dom (h | Y) by A2, RELAT_1:61; then (h | Y) . r1 = h . r1 by FUNCT_1:47; hence h . r2 <= h . r1 by A1, A4, A7, A5, A6, Def4; ::_thesis: verum end; assume A8: for r1, r2 being Element of REAL st r1 in Y /\ (dom h) & r2 in Y /\ (dom h) & r1 < r2 holds h . r2 <= h . r1 ; ::_thesis: h | Y is non-increasing let r1 be Element of REAL ; :: according to RFUNCT_2:def_4 ::_thesis: for r2 being Element of REAL st r1 in dom (h | Y) & r2 in dom (h | Y) & r1 < r2 holds (h | Y) . r2 <= (h | Y) . r1 let r2 be Element of REAL ; ::_thesis: ( r1 in dom (h | Y) & r2 in dom (h | Y) & r1 < r2 implies (h | Y) . r2 <= (h | Y) . r1 ) assume that A9: ( r1 in dom (h | Y) & r2 in dom (h | Y) ) and A10: r1 < r2 ; ::_thesis: (h | Y) . r2 <= (h | Y) . r1 A11: ( (h | Y) . r1 = h . r1 & (h | Y) . r2 = h . r2 ) by A9, FUNCT_1:47; ( r1 in Y /\ (dom h) & r2 in Y /\ (dom h) ) by A9, RELAT_1:61; hence (h | Y) . r2 <= (h | Y) . r1 by A8, A10, A11; ::_thesis: verum end; definition let h be PartFunc of REAL,REAL; attrh is monotone means :Def5: :: RFUNCT_2:def 5 ( h is non-decreasing or h is non-increasing ); end; :: deftheorem Def5 defines monotone RFUNCT_2:def_5_:_ for h being PartFunc of REAL,REAL holds ( h is monotone iff ( h is non-decreasing or h is non-increasing ) ); registration cluster Function-like non-decreasing -> monotone for Element of bool [:REAL,REAL:]; coherence for b1 being PartFunc of REAL,REAL st b1 is non-decreasing holds b1 is monotone by Def5; cluster Function-like non-increasing -> monotone for Element of bool [:REAL,REAL:]; coherence for b1 being PartFunc of REAL,REAL st b1 is non-increasing holds b1 is monotone by Def5; cluster Function-like non monotone -> non non-decreasing non non-increasing for Element of bool [:REAL,REAL:]; coherence for b1 being PartFunc of REAL,REAL st not b1 is monotone holds ( not b1 is non-decreasing & not b1 is non-increasing ) ; end; theorem Th24: :: RFUNCT_2:24 for Y being set for h being PartFunc of REAL,REAL holds ( h | Y is non-decreasing iff for r1, r2 being Element of REAL st r1 in Y /\ (dom h) & r2 in Y /\ (dom h) & r1 <= r2 holds h . r1 <= h . r2 ) proof let Y be set ; ::_thesis: for h being PartFunc of REAL,REAL holds ( h | Y is non-decreasing iff for r1, r2 being Element of REAL st r1 in Y /\ (dom h) & r2 in Y /\ (dom h) & r1 <= r2 holds h . r1 <= h . r2 ) let h be PartFunc of REAL,REAL; ::_thesis: ( h | Y is non-decreasing iff for r1, r2 being Element of REAL st r1 in Y /\ (dom h) & r2 in Y /\ (dom h) & r1 <= r2 holds h . r1 <= h . r2 ) thus ( h | Y is non-decreasing implies for r1, r2 being Element of REAL st r1 in Y /\ (dom h) & r2 in Y /\ (dom h) & r1 <= r2 holds h . r1 <= h . r2 ) ::_thesis: ( ( for r1, r2 being Element of REAL st r1 in Y /\ (dom h) & r2 in Y /\ (dom h) & r1 <= r2 holds h . r1 <= h . r2 ) implies h | Y is non-decreasing ) proof assume A1: h | Y is non-decreasing ; ::_thesis: for r1, r2 being Element of REAL st r1 in Y /\ (dom h) & r2 in Y /\ (dom h) & r1 <= r2 holds h . r1 <= h . r2 let r1, r2 be Element of REAL ; ::_thesis: ( r1 in Y /\ (dom h) & r2 in Y /\ (dom h) & r1 <= r2 implies h . r1 <= h . r2 ) assume that A2: ( r1 in Y /\ (dom h) & r2 in Y /\ (dom h) ) and A3: r1 <= r2 ; ::_thesis: h . r1 <= h . r2 now__::_thesis:_h_._r1_<=_h_._r2 percases ( r1 < r2 or r1 = r2 ) by A3, XXREAL_0:1; suppose r1 < r2 ; ::_thesis: h . r1 <= h . r2 hence h . r1 <= h . r2 by A1, A2, Th22; ::_thesis: verum end; suppose r1 = r2 ; ::_thesis: h . r1 <= h . r2 hence h . r1 <= h . r2 ; ::_thesis: verum end; end; end; hence h . r1 <= h . r2 ; ::_thesis: verum end; assume A4: for r1, r2 being Element of REAL st r1 in Y /\ (dom h) & r2 in Y /\ (dom h) & r1 <= r2 holds h . r1 <= h . r2 ; ::_thesis: h | Y is non-decreasing let r1 be Element of REAL ; :: according to RFUNCT_2:def_3 ::_thesis: for r2 being Element of REAL st r1 in dom (h | Y) & r2 in dom (h | Y) & r1 < r2 holds (h | Y) . r1 <= (h | Y) . r2 let r2 be Element of REAL ; ::_thesis: ( r1 in dom (h | Y) & r2 in dom (h | Y) & r1 < r2 implies (h | Y) . r1 <= (h | Y) . r2 ) assume that A5: ( r1 in dom (h | Y) & r2 in dom (h | Y) ) and A6: r1 < r2 ; ::_thesis: (h | Y) . r1 <= (h | Y) . r2 A7: ( (h | Y) . r1 = h . r1 & (h | Y) . r2 = h . r2 ) by A5, FUNCT_1:47; ( r1 in Y /\ (dom h) & r2 in Y /\ (dom h) ) by A5, RELAT_1:61; hence (h | Y) . r1 <= (h | Y) . r2 by A4, A6, A7; ::_thesis: verum end; theorem Th25: :: RFUNCT_2:25 for Y being set for h being PartFunc of REAL,REAL holds ( h | Y is non-increasing iff for r1, r2 being Element of REAL st r1 in Y /\ (dom h) & r2 in Y /\ (dom h) & r1 <= r2 holds h . r2 <= h . r1 ) proof let Y be set ; ::_thesis: for h being PartFunc of REAL,REAL holds ( h | Y is non-increasing iff for r1, r2 being Element of REAL st r1 in Y /\ (dom h) & r2 in Y /\ (dom h) & r1 <= r2 holds h . r2 <= h . r1 ) let h be PartFunc of REAL,REAL; ::_thesis: ( h | Y is non-increasing iff for r1, r2 being Element of REAL st r1 in Y /\ (dom h) & r2 in Y /\ (dom h) & r1 <= r2 holds h . r2 <= h . r1 ) thus ( h | Y is non-increasing implies for r1, r2 being Element of REAL st r1 in Y /\ (dom h) & r2 in Y /\ (dom h) & r1 <= r2 holds h . r2 <= h . r1 ) ::_thesis: ( ( for r1, r2 being Element of REAL st r1 in Y /\ (dom h) & r2 in Y /\ (dom h) & r1 <= r2 holds h . r2 <= h . r1 ) implies h | Y is non-increasing ) proof assume A1: h | Y is non-increasing ; ::_thesis: for r1, r2 being Element of REAL st r1 in Y /\ (dom h) & r2 in Y /\ (dom h) & r1 <= r2 holds h . r2 <= h . r1 let r1, r2 be Element of REAL ; ::_thesis: ( r1 in Y /\ (dom h) & r2 in Y /\ (dom h) & r1 <= r2 implies h . r2 <= h . r1 ) assume that A2: ( r1 in Y /\ (dom h) & r2 in Y /\ (dom h) ) and A3: r1 <= r2 ; ::_thesis: h . r2 <= h . r1 now__::_thesis:_h_._r2_<=_h_._r1 percases ( r1 < r2 or r1 = r2 ) by A3, XXREAL_0:1; suppose r1 < r2 ; ::_thesis: h . r2 <= h . r1 hence h . r2 <= h . r1 by A1, A2, Th23; ::_thesis: verum end; suppose r1 = r2 ; ::_thesis: h . r2 <= h . r1 hence h . r2 <= h . r1 ; ::_thesis: verum end; end; end; hence h . r2 <= h . r1 ; ::_thesis: verum end; assume A4: for r1, r2 being Element of REAL st r1 in Y /\ (dom h) & r2 in Y /\ (dom h) & r1 <= r2 holds h . r2 <= h . r1 ; ::_thesis: h | Y is non-increasing let r1 be Element of REAL ; :: according to RFUNCT_2:def_4 ::_thesis: for r2 being Element of REAL st r1 in dom (h | Y) & r2 in dom (h | Y) & r1 < r2 holds (h | Y) . r2 <= (h | Y) . r1 let r2 be Element of REAL ; ::_thesis: ( r1 in dom (h | Y) & r2 in dom (h | Y) & r1 < r2 implies (h | Y) . r2 <= (h | Y) . r1 ) assume that A5: ( r1 in dom (h | Y) & r2 in dom (h | Y) ) and A6: r1 < r2 ; ::_thesis: (h | Y) . r2 <= (h | Y) . r1 A7: ( (h | Y) . r1 = h . r1 & (h | Y) . r2 = h . r2 ) by A5, FUNCT_1:47; ( r1 in Y /\ (dom h) & r2 in Y /\ (dom h) ) by A5, RELAT_1:61; hence (h | Y) . r2 <= (h | Y) . r1 by A4, A6, A7; ::_thesis: verum end; registration cluster Function-like non-decreasing non-increasing -> V8() for Element of bool [:REAL,REAL:]; coherence for b1 being PartFunc of REAL,REAL st b1 is non-decreasing & b1 is non-increasing holds b1 is V8() proof let h be PartFunc of REAL,REAL; ::_thesis: ( h is non-decreasing & h is non-increasing implies h is V8() ) assume A1: ( h is non-decreasing & h is non-increasing ) ; ::_thesis: h is V8() let r1, r2 be set ; :: according to FUNCT_1:def_10 ::_thesis: ( not r1 in dom h or not r2 in dom h or h . r1 = h . r2 ) assume A2: ( r1 in dom h & r2 in dom h ) ; ::_thesis: h . r1 = h . r2 then reconsider r1 = r1, r2 = r2 as Real ; ( r1 < r2 or r1 = r2 or r2 < r1 ) by XXREAL_0:1; then ( h . r1 <= h . r2 & h . r2 <= h . r1 ) by A1, A2, Def3, Def4; hence h . r1 = h . r2 by XXREAL_0:1; ::_thesis: verum end; end; registration cluster Function-like V8() -> non-decreasing non-increasing for Element of bool [:REAL,REAL:]; coherence for b1 being PartFunc of REAL,REAL st b1 is V8() holds ( b1 is non-increasing & b1 is non-decreasing ) proof let h be PartFunc of REAL,REAL; ::_thesis: ( h is V8() implies ( h is non-increasing & h is non-decreasing ) ) assume A1: h is V8() ; ::_thesis: ( h is non-increasing & h is non-decreasing ) thus h is non-increasing ::_thesis: h is non-decreasing proof let r1 be Element of REAL ; :: according to RFUNCT_2:def_4 ::_thesis: for r2 being Element of REAL st r1 in dom h & r2 in dom h & r1 < r2 holds h . r2 <= h . r1 let r2 be Element of REAL ; ::_thesis: ( r1 in dom h & r2 in dom h & r1 < r2 implies h . r2 <= h . r1 ) assume ( r1 in dom h & r2 in dom h ) ; ::_thesis: ( not r1 < r2 or h . r2 <= h . r1 ) hence ( not r1 < r2 or h . r2 <= h . r1 ) by A1, FUNCT_1:def_10; ::_thesis: verum end; let r1 be Element of REAL ; :: according to RFUNCT_2:def_3 ::_thesis: for r2 being Element of REAL st r1 in dom h & r2 in dom h & r1 < r2 holds h . r1 <= h . r2 let r2 be Element of REAL ; ::_thesis: ( r1 in dom h & r2 in dom h & r1 < r2 implies h . r1 <= h . r2 ) assume ( r1 in dom h & r2 in dom h ) ; ::_thesis: ( not r1 < r2 or h . r1 <= h . r2 ) hence ( not r1 < r2 or h . r1 <= h . r2 ) by A1, FUNCT_1:def_10; ::_thesis: verum end; end; registration cluster Relation-like REAL -defined REAL -valued Function-like trivial complex-valued ext-real-valued real-valued for Element of bool [:REAL,REAL:]; existence ex b1 being PartFunc of REAL,REAL st b1 is trivial proof reconsider f = {} as PartFunc of REAL,REAL by RELSET_1:12; take f ; ::_thesis: f is trivial thus f is trivial ; ::_thesis: verum end; end; registration let h be increasing PartFunc of REAL,REAL; let X be set ; clusterh | X -> increasing for PartFunc of REAL,REAL; coherence for b1 being PartFunc of REAL,REAL st b1 = h | X holds b1 is increasing proof now__::_thesis:_for_r1,_r2_being_Element_of_REAL_st_r1_in_dom_(h_|_X)_&_r2_in_dom_(h_|_X)_&_r1_<_r2_holds_ (h_|_X)_._r1_<_(h_|_X)_._r2 let r1, r2 be Element of REAL ; ::_thesis: ( r1 in dom (h | X) & r2 in dom (h | X) & r1 < r2 implies (h | X) . r1 < (h | X) . r2 ) assume A1: ( r1 in dom (h | X) & r2 in dom (h | X) ) ; ::_thesis: ( r1 < r2 implies (h | X) . r1 < (h | X) . r2 ) then A2: ( h . r1 = (h | X) . r1 & h . r2 = (h | X) . r2 ) by FUNCT_1:47; assume A3: r1 < r2 ; ::_thesis: (h | X) . r1 < (h | X) . r2 ( r1 in dom h & r2 in dom h ) by A1, RELAT_1:57; hence (h | X) . r1 < (h | X) . r2 by A2, A3, Def1; ::_thesis: verum end; hence for b1 being PartFunc of REAL,REAL st b1 = h | X holds b1 is increasing by Def1; ::_thesis: verum end; end; registration let h be decreasing PartFunc of REAL,REAL; let X be set ; clusterh | X -> decreasing for PartFunc of REAL,REAL; coherence for b1 being PartFunc of REAL,REAL st b1 = h | X holds b1 is decreasing proof now__::_thesis:_for_r1,_r2_being_Element_of_REAL_st_r1_in_dom_(h_|_X)_&_r2_in_dom_(h_|_X)_&_r1_<_r2_holds_ (h_|_X)_._r1_>_(h_|_X)_._r2 let r1, r2 be Element of REAL ; ::_thesis: ( r1 in dom (h | X) & r2 in dom (h | X) & r1 < r2 implies (h | X) . r1 > (h | X) . r2 ) assume A1: ( r1 in dom (h | X) & r2 in dom (h | X) ) ; ::_thesis: ( r1 < r2 implies (h | X) . r1 > (h | X) . r2 ) then A2: ( h . r1 = (h | X) . r1 & h . r2 = (h | X) . r2 ) by FUNCT_1:47; assume A3: r1 < r2 ; ::_thesis: (h | X) . r1 > (h | X) . r2 ( r1 in dom h & r2 in dom h ) by A1, RELAT_1:57; hence (h | X) . r1 > (h | X) . r2 by A2, A3, Def2; ::_thesis: verum end; hence for b1 being PartFunc of REAL,REAL st b1 = h | X holds b1 is decreasing by Def2; ::_thesis: verum end; end; registration let h be non-decreasing PartFunc of REAL,REAL; let X be set ; clusterh | X -> non-decreasing for PartFunc of REAL,REAL; coherence for b1 being PartFunc of REAL,REAL st b1 = h | X holds b1 is non-decreasing proof now__::_thesis:_for_r1,_r2_being_Element_of_REAL_st_r1_in_dom_(h_|_X)_&_r2_in_dom_(h_|_X)_&_r1_<_r2_holds_ (h_|_X)_._r1_<=_(h_|_X)_._r2 let r1, r2 be Element of REAL ; ::_thesis: ( r1 in dom (h | X) & r2 in dom (h | X) & r1 < r2 implies (h | X) . r1 <= (h | X) . r2 ) assume A1: ( r1 in dom (h | X) & r2 in dom (h | X) ) ; ::_thesis: ( r1 < r2 implies (h | X) . r1 <= (h | X) . r2 ) then A2: ( h . r1 = (h | X) . r1 & h . r2 = (h | X) . r2 ) by FUNCT_1:47; assume A3: r1 < r2 ; ::_thesis: (h | X) . r1 <= (h | X) . r2 ( r1 in dom h & r2 in dom h ) by A1, RELAT_1:57; hence (h | X) . r1 <= (h | X) . r2 by A2, A3, Def3; ::_thesis: verum end; hence for b1 being PartFunc of REAL,REAL st b1 = h | X holds b1 is non-decreasing by Def3; ::_thesis: verum end; end; theorem :: RFUNCT_2:26 for Y being set for h being PartFunc of REAL,REAL st Y misses dom h holds ( h | Y is increasing & h | Y is decreasing & h | Y is non-decreasing & h | Y is non-increasing & h | Y is monotone ) proof let Y be set ; ::_thesis: for h being PartFunc of REAL,REAL st Y misses dom h holds ( h | Y is increasing & h | Y is decreasing & h | Y is non-decreasing & h | Y is non-increasing & h | Y is monotone ) let h be PartFunc of REAL,REAL; ::_thesis: ( Y misses dom h implies ( h | Y is increasing & h | Y is decreasing & h | Y is non-decreasing & h | Y is non-increasing & h | Y is monotone ) ) assume A1: Y /\ (dom h) = {} ; :: according to XBOOLE_0:def_7 ::_thesis: ( h | Y is increasing & h | Y is decreasing & h | Y is non-decreasing & h | Y is non-increasing & h | Y is monotone ) then for r1, r2 being Element of REAL st r1 in Y /\ (dom h) & r2 in Y /\ (dom h) & r1 < r2 holds h . r1 < h . r2 ; hence h | Y is increasing by Th20; ::_thesis: ( h | Y is decreasing & h | Y is non-decreasing & h | Y is non-increasing & h | Y is monotone ) for r1, r2 being Element of REAL st r1 in Y /\ (dom h) & r2 in Y /\ (dom h) & r1 < r2 holds h . r2 < h . r1 by A1; hence h | Y is decreasing by Th21; ::_thesis: ( h | Y is non-decreasing & h | Y is non-increasing & h | Y is monotone ) for r1, r2 being Element of REAL st r1 in Y /\ (dom h) & r2 in Y /\ (dom h) & r1 < r2 holds h . r1 <= h . r2 by A1; hence h | Y is non-decreasing by Th22; ::_thesis: ( h | Y is non-increasing & h | Y is monotone ) A2: for r1, r2 being Element of REAL st r1 in Y /\ (dom h) & r2 in Y /\ (dom h) & r1 < r2 holds h . r2 <= h . r1 by A1; hence h | Y is non-increasing by Th23; ::_thesis: h | Y is monotone thus h | Y is monotone by A2, Th23; ::_thesis: verum end; theorem :: RFUNCT_2:27 for Y, X being set for h being PartFunc of REAL,REAL st h | Y is non-decreasing & h | X is non-increasing holds h | (Y /\ X) is V8() proof let Y, X be set ; ::_thesis: for h being PartFunc of REAL,REAL st h | Y is non-decreasing & h | X is non-increasing holds h | (Y /\ X) is V8() let h be PartFunc of REAL,REAL; ::_thesis: ( h | Y is non-decreasing & h | X is non-increasing implies h | (Y /\ X) is V8() ) assume A1: ( h | Y is non-decreasing & h | X is non-increasing ) ; ::_thesis: h | (Y /\ X) is V8() now__::_thesis:_h_|_(Y_/\_X)_is_V8() percases ( (Y /\ X) /\ (dom h) = {} or (Y /\ X) /\ (dom h) <> {} ) ; suppose (Y /\ X) /\ (dom h) = {} ; ::_thesis: h | (Y /\ X) is V8() then Y /\ X misses dom h by XBOOLE_0:def_7; hence h | (Y /\ X) is V8() by PARTFUN2:39; ::_thesis: verum end; supposeA2: (Y /\ X) /\ (dom h) <> {} ; ::_thesis: h | (Y /\ X) is V8() set x = the Element of (Y /\ X) /\ (dom h); the Element of (Y /\ X) /\ (dom h) in dom h by A2, XBOOLE_0:def_4; then reconsider x = the Element of (Y /\ X) /\ (dom h) as Real ; now__::_thesis:_ex_r1_being_Element_of_REAL_st_ for_p_being_Element_of_REAL_st_p_in_(Y_/\_X)_/\_(dom_h)_holds_ h_._p_=_r1 take r1 = h . x; ::_thesis: for p being Element of REAL st p in (Y /\ X) /\ (dom h) holds h . p = r1 now__::_thesis:_for_p_being_Element_of_REAL_st_p_in_(Y_/\_X)_/\_(dom_h)_holds_ h_._p_=_r1 let p be Element of REAL ; ::_thesis: ( p in (Y /\ X) /\ (dom h) implies h . p = r1 ) assume A3: p in (Y /\ X) /\ (dom h) ; ::_thesis: h . p = r1 then A4: p in Y /\ X by XBOOLE_0:def_4; A5: p in dom h by A3, XBOOLE_0:def_4; p in X by A4, XBOOLE_0:def_4; then A6: p in X /\ (dom h) by A5, XBOOLE_0:def_4; A7: x in dom h by A2, XBOOLE_0:def_4; A8: x in Y /\ X by A2, XBOOLE_0:def_4; then x in Y by XBOOLE_0:def_4; then A9: x in Y /\ (dom h) by A7, XBOOLE_0:def_4; x in X by A8, XBOOLE_0:def_4; then A10: x in X /\ (dom h) by A7, XBOOLE_0:def_4; p in Y by A4, XBOOLE_0:def_4; then A11: p in Y /\ (dom h) by A5, XBOOLE_0:def_4; now__::_thesis:_h_._p_=_h_._x percases ( x <= p or p <= x ) ; suppose x <= p ; ::_thesis: h . p = h . x then ( h . x <= h . p & h . p <= h . x ) by A1, A11, A6, A9, A10, Th24, Th25; hence h . p = h . x by XXREAL_0:1; ::_thesis: verum end; suppose p <= x ; ::_thesis: h . p = h . x then ( h . p <= h . x & h . x <= h . p ) by A1, A11, A6, A9, A10, Th24, Th25; hence h . p = h . x by XXREAL_0:1; ::_thesis: verum end; end; end; hence h . p = r1 ; ::_thesis: verum end; hence for p being Element of REAL st p in (Y /\ X) /\ (dom h) holds h . p = r1 ; ::_thesis: verum end; hence h | (Y /\ X) is V8() by PARTFUN2:57; ::_thesis: verum end; end; end; hence h | (Y /\ X) is V8() ; ::_thesis: verum end; theorem :: RFUNCT_2:28 for X, Y being set for h being PartFunc of REAL,REAL st X c= Y & h | Y is increasing holds h | X is increasing proof let X, Y be set ; ::_thesis: for h being PartFunc of REAL,REAL st X c= Y & h | Y is increasing holds h | X is increasing let h be PartFunc of REAL,REAL; ::_thesis: ( X c= Y & h | Y is increasing implies h | X is increasing ) assume that A1: X c= Y and A2: h | Y is increasing ; ::_thesis: h | X is increasing now__::_thesis:_for_r1,_r2_being_Element_of_REAL_st_r1_in_X_/\_(dom_h)_&_r2_in_X_/\_(dom_h)_&_r1_<_r2_holds_ h_._r1_<_h_._r2 A3: X /\ (dom h) c= Y /\ (dom h) by A1, XBOOLE_1:26; let r1, r2 be Element of REAL ; ::_thesis: ( r1 in X /\ (dom h) & r2 in X /\ (dom h) & r1 < r2 implies h . r1 < h . r2 ) assume ( r1 in X /\ (dom h) & r2 in X /\ (dom h) & r1 < r2 ) ; ::_thesis: h . r1 < h . r2 hence h . r1 < h . r2 by A2, A3, Th20; ::_thesis: verum end; hence h | X is increasing by Th20; ::_thesis: verum end; theorem :: RFUNCT_2:29 for X, Y being set for h being PartFunc of REAL,REAL st X c= Y & h | Y is decreasing holds h | X is decreasing proof let X, Y be set ; ::_thesis: for h being PartFunc of REAL,REAL st X c= Y & h | Y is decreasing holds h | X is decreasing let h be PartFunc of REAL,REAL; ::_thesis: ( X c= Y & h | Y is decreasing implies h | X is decreasing ) assume that A1: X c= Y and A2: h | Y is decreasing ; ::_thesis: h | X is decreasing now__::_thesis:_for_r1,_r2_being_Element_of_REAL_st_r1_in_X_/\_(dom_h)_&_r2_in_X_/\_(dom_h)_&_r1_<_r2_holds_ h_._r1_>_h_._r2 A3: X /\ (dom h) c= Y /\ (dom h) by A1, XBOOLE_1:26; let r1, r2 be Element of REAL ; ::_thesis: ( r1 in X /\ (dom h) & r2 in X /\ (dom h) & r1 < r2 implies h . r1 > h . r2 ) assume ( r1 in X /\ (dom h) & r2 in X /\ (dom h) & r1 < r2 ) ; ::_thesis: h . r1 > h . r2 hence h . r1 > h . r2 by A2, A3, Th21; ::_thesis: verum end; hence h | X is decreasing by Th21; ::_thesis: verum end; theorem :: RFUNCT_2:30 for X, Y being set for h being PartFunc of REAL,REAL st X c= Y & h | Y is non-decreasing holds h | X is non-decreasing proof let X, Y be set ; ::_thesis: for h being PartFunc of REAL,REAL st X c= Y & h | Y is non-decreasing holds h | X is non-decreasing let h be PartFunc of REAL,REAL; ::_thesis: ( X c= Y & h | Y is non-decreasing implies h | X is non-decreasing ) assume that A1: X c= Y and A2: h | Y is non-decreasing ; ::_thesis: h | X is non-decreasing now__::_thesis:_for_r1,_r2_being_Element_of_REAL_st_r1_in_X_/\_(dom_h)_&_r2_in_X_/\_(dom_h)_&_r1_<_r2_holds_ h_._r1_<=_h_._r2 A3: X /\ (dom h) c= Y /\ (dom h) by A1, XBOOLE_1:26; let r1, r2 be Element of REAL ; ::_thesis: ( r1 in X /\ (dom h) & r2 in X /\ (dom h) & r1 < r2 implies h . r1 <= h . r2 ) assume ( r1 in X /\ (dom h) & r2 in X /\ (dom h) & r1 < r2 ) ; ::_thesis: h . r1 <= h . r2 hence h . r1 <= h . r2 by A2, A3, Th22; ::_thesis: verum end; hence h | X is non-decreasing by Th22; ::_thesis: verum end; theorem :: RFUNCT_2:31 for X, Y being set for h being PartFunc of REAL,REAL st X c= Y & h | Y is non-increasing holds h | X is non-increasing proof let X, Y be set ; ::_thesis: for h being PartFunc of REAL,REAL st X c= Y & h | Y is non-increasing holds h | X is non-increasing let h be PartFunc of REAL,REAL; ::_thesis: ( X c= Y & h | Y is non-increasing implies h | X is non-increasing ) assume that A1: X c= Y and A2: h | Y is non-increasing ; ::_thesis: h | X is non-increasing now__::_thesis:_for_r1,_r2_being_Element_of_REAL_st_r1_in_X_/\_(dom_h)_&_r2_in_X_/\_(dom_h)_&_r1_<_r2_holds_ h_._r1_>=_h_._r2 A3: X /\ (dom h) c= Y /\ (dom h) by A1, XBOOLE_1:26; let r1, r2 be Element of REAL ; ::_thesis: ( r1 in X /\ (dom h) & r2 in X /\ (dom h) & r1 < r2 implies h . r1 >= h . r2 ) assume ( r1 in X /\ (dom h) & r2 in X /\ (dom h) & r1 < r2 ) ; ::_thesis: h . r1 >= h . r2 hence h . r1 >= h . r2 by A2, A3, Th23; ::_thesis: verum end; hence h | X is non-increasing by Th23; ::_thesis: verum end; theorem Th32: :: RFUNCT_2:32 for Y being set for r being Element of REAL for h being PartFunc of REAL,REAL holds ( ( h | Y is increasing & 0 < r implies (r (#) h) | Y is increasing ) & ( r = 0 implies (r (#) h) | Y is V8() ) & ( h | Y is increasing & r < 0 implies (r (#) h) | Y is decreasing ) ) proof let Y be set ; ::_thesis: for r being Element of REAL for h being PartFunc of REAL,REAL holds ( ( h | Y is increasing & 0 < r implies (r (#) h) | Y is increasing ) & ( r = 0 implies (r (#) h) | Y is V8() ) & ( h | Y is increasing & r < 0 implies (r (#) h) | Y is decreasing ) ) let r be Element of REAL ; ::_thesis: for h being PartFunc of REAL,REAL holds ( ( h | Y is increasing & 0 < r implies (r (#) h) | Y is increasing ) & ( r = 0 implies (r (#) h) | Y is V8() ) & ( h | Y is increasing & r < 0 implies (r (#) h) | Y is decreasing ) ) let h be PartFunc of REAL,REAL; ::_thesis: ( ( h | Y is increasing & 0 < r implies (r (#) h) | Y is increasing ) & ( r = 0 implies (r (#) h) | Y is V8() ) & ( h | Y is increasing & r < 0 implies (r (#) h) | Y is decreasing ) ) thus ( h | Y is increasing & 0 < r implies (r (#) h) | Y is increasing ) ::_thesis: ( ( r = 0 implies (r (#) h) | Y is V8() ) & ( h | Y is increasing & r < 0 implies (r (#) h) | Y is decreasing ) ) proof assume that A1: h | Y is increasing and A2: 0 < r ; ::_thesis: (r (#) h) | Y is increasing now__::_thesis:_for_r1,_r2_being_Element_of_REAL_st_r1_in_Y_/\_(dom_(r_(#)_h))_&_r2_in_Y_/\_(dom_(r_(#)_h))_&_r1_<_r2_holds_ (r_(#)_h)_._r1_<_(r_(#)_h)_._r2 let r1, r2 be Element of REAL ; ::_thesis: ( r1 in Y /\ (dom (r (#) h)) & r2 in Y /\ (dom (r (#) h)) & r1 < r2 implies (r (#) h) . r1 < (r (#) h) . r2 ) assume that A3: r1 in Y /\ (dom (r (#) h)) and A4: r2 in Y /\ (dom (r (#) h)) and A5: r1 < r2 ; ::_thesis: (r (#) h) . r1 < (r (#) h) . r2 A6: r2 in Y by A4, XBOOLE_0:def_4; A7: r2 in dom (r (#) h) by A4, XBOOLE_0:def_4; then r2 in dom h by VALUED_1:def_5; then A8: r2 in Y /\ (dom h) by A6, XBOOLE_0:def_4; A9: r1 in Y by A3, XBOOLE_0:def_4; A10: r1 in dom (r (#) h) by A3, XBOOLE_0:def_4; then r1 in dom h by VALUED_1:def_5; then r1 in Y /\ (dom h) by A9, XBOOLE_0:def_4; then h . r1 < h . r2 by A1, A5, A8, Th20; then r * (h . r1) < r * (h . r2) by A2, XREAL_1:68; then (r (#) h) . r1 < r * (h . r2) by A10, VALUED_1:def_5; hence (r (#) h) . r1 < (r (#) h) . r2 by A7, VALUED_1:def_5; ::_thesis: verum end; hence (r (#) h) | Y is increasing by Th20; ::_thesis: verum end; thus ( r = 0 implies (r (#) h) | Y is V8() ) ::_thesis: ( h | Y is increasing & r < 0 implies (r (#) h) | Y is decreasing ) proof assume A11: r = 0 ; ::_thesis: (r (#) h) | Y is V8() now__::_thesis:_for_r1_being_Element_of_REAL_st_r1_in_Y_/\_(dom_(r_(#)_h))_holds_ (r_(#)_h)_._r1_=_0 let r1 be Element of REAL ; ::_thesis: ( r1 in Y /\ (dom (r (#) h)) implies (r (#) h) . r1 = 0 ) assume r1 in Y /\ (dom (r (#) h)) ; ::_thesis: (r (#) h) . r1 = 0 then A12: r1 in dom (r (#) h) by XBOOLE_0:def_4; r * (h . r1) = 0 by A11; hence (r (#) h) . r1 = 0 by A12, VALUED_1:def_5; ::_thesis: verum end; hence (r (#) h) | Y is V8() by PARTFUN2:57; ::_thesis: verum end; assume that A13: h | Y is increasing and A14: r < 0 ; ::_thesis: (r (#) h) | Y is decreasing now__::_thesis:_for_r1,_r2_being_Element_of_REAL_st_r1_in_Y_/\_(dom_(r_(#)_h))_&_r2_in_Y_/\_(dom_(r_(#)_h))_&_r1_<_r2_holds_ (r_(#)_h)_._r2_<_(r_(#)_h)_._r1 let r1, r2 be Element of REAL ; ::_thesis: ( r1 in Y /\ (dom (r (#) h)) & r2 in Y /\ (dom (r (#) h)) & r1 < r2 implies (r (#) h) . r2 < (r (#) h) . r1 ) assume that A15: r1 in Y /\ (dom (r (#) h)) and A16: r2 in Y /\ (dom (r (#) h)) and A17: r1 < r2 ; ::_thesis: (r (#) h) . r2 < (r (#) h) . r1 A18: r2 in Y by A16, XBOOLE_0:def_4; A19: r2 in dom (r (#) h) by A16, XBOOLE_0:def_4; then r2 in dom h by VALUED_1:def_5; then A20: r2 in Y /\ (dom h) by A18, XBOOLE_0:def_4; A21: r1 in Y by A15, XBOOLE_0:def_4; A22: r1 in dom (r (#) h) by A15, XBOOLE_0:def_4; then r1 in dom h by VALUED_1:def_5; then r1 in Y /\ (dom h) by A21, XBOOLE_0:def_4; then h . r1 < h . r2 by A13, A17, A20, Th20; then r * (h . r2) < r * (h . r1) by A14, XREAL_1:69; then (r (#) h) . r2 < r * (h . r1) by A19, VALUED_1:def_5; hence (r (#) h) . r2 < (r (#) h) . r1 by A22, VALUED_1:def_5; ::_thesis: verum end; hence (r (#) h) | Y is decreasing by Th21; ::_thesis: verum end; theorem :: RFUNCT_2:33 for Y being set for r being Element of REAL for h being PartFunc of REAL,REAL holds ( ( h | Y is decreasing & 0 < r implies (r (#) h) | Y is decreasing ) & ( h | Y is decreasing & r < 0 implies (r (#) h) | Y is increasing ) ) proof let Y be set ; ::_thesis: for r being Element of REAL for h being PartFunc of REAL,REAL holds ( ( h | Y is decreasing & 0 < r implies (r (#) h) | Y is decreasing ) & ( h | Y is decreasing & r < 0 implies (r (#) h) | Y is increasing ) ) let r be Element of REAL ; ::_thesis: for h being PartFunc of REAL,REAL holds ( ( h | Y is decreasing & 0 < r implies (r (#) h) | Y is decreasing ) & ( h | Y is decreasing & r < 0 implies (r (#) h) | Y is increasing ) ) let h be PartFunc of REAL,REAL; ::_thesis: ( ( h | Y is decreasing & 0 < r implies (r (#) h) | Y is decreasing ) & ( h | Y is decreasing & r < 0 implies (r (#) h) | Y is increasing ) ) thus ( h | Y is decreasing & 0 < r implies (r (#) h) | Y is decreasing ) ::_thesis: ( h | Y is decreasing & r < 0 implies (r (#) h) | Y is increasing ) proof assume that A1: h | Y is decreasing and A2: 0 < r ; ::_thesis: (r (#) h) | Y is decreasing now__::_thesis:_for_r1,_r2_being_Element_of_REAL_st_r1_in_Y_/\_(dom_(r_(#)_h))_&_r2_in_Y_/\_(dom_(r_(#)_h))_&_r1_<_r2_holds_ (r_(#)_h)_._r2_<_(r_(#)_h)_._r1 let r1, r2 be Element of REAL ; ::_thesis: ( r1 in Y /\ (dom (r (#) h)) & r2 in Y /\ (dom (r (#) h)) & r1 < r2 implies (r (#) h) . r2 < (r (#) h) . r1 ) assume that A3: r1 in Y /\ (dom (r (#) h)) and A4: r2 in Y /\ (dom (r (#) h)) and A5: r1 < r2 ; ::_thesis: (r (#) h) . r2 < (r (#) h) . r1 A6: r2 in Y by A4, XBOOLE_0:def_4; A7: r2 in dom (r (#) h) by A4, XBOOLE_0:def_4; then r2 in dom h by VALUED_1:def_5; then A8: r2 in Y /\ (dom h) by A6, XBOOLE_0:def_4; A9: r1 in Y by A3, XBOOLE_0:def_4; A10: r1 in dom (r (#) h) by A3, XBOOLE_0:def_4; then r1 in dom h by VALUED_1:def_5; then r1 in Y /\ (dom h) by A9, XBOOLE_0:def_4; then h . r2 < h . r1 by A1, A5, A8, Th21; then r * (h . r2) < r * (h . r1) by A2, XREAL_1:68; then (r (#) h) . r2 < r * (h . r1) by A7, VALUED_1:def_5; hence (r (#) h) . r2 < (r (#) h) . r1 by A10, VALUED_1:def_5; ::_thesis: verum end; hence (r (#) h) | Y is decreasing by Th21; ::_thesis: verum end; assume that A11: h | Y is decreasing and A12: r < 0 ; ::_thesis: (r (#) h) | Y is increasing now__::_thesis:_for_r1,_r2_being_Element_of_REAL_st_r1_in_Y_/\_(dom_(r_(#)_h))_&_r2_in_Y_/\_(dom_(r_(#)_h))_&_r1_<_r2_holds_ (r_(#)_h)_._r1_<_(r_(#)_h)_._r2 let r1, r2 be Element of REAL ; ::_thesis: ( r1 in Y /\ (dom (r (#) h)) & r2 in Y /\ (dom (r (#) h)) & r1 < r2 implies (r (#) h) . r1 < (r (#) h) . r2 ) assume that A13: r1 in Y /\ (dom (r (#) h)) and A14: r2 in Y /\ (dom (r (#) h)) and A15: r1 < r2 ; ::_thesis: (r (#) h) . r1 < (r (#) h) . r2 A16: r2 in Y by A14, XBOOLE_0:def_4; A17: r2 in dom (r (#) h) by A14, XBOOLE_0:def_4; then r2 in dom h by VALUED_1:def_5; then A18: r2 in Y /\ (dom h) by A16, XBOOLE_0:def_4; A19: r1 in Y by A13, XBOOLE_0:def_4; A20: r1 in dom (r (#) h) by A13, XBOOLE_0:def_4; then r1 in dom h by VALUED_1:def_5; then r1 in Y /\ (dom h) by A19, XBOOLE_0:def_4; then h . r2 < h . r1 by A11, A15, A18, Th21; then r * (h . r1) < r * (h . r2) by A12, XREAL_1:69; then (r (#) h) . r1 < r * (h . r2) by A20, VALUED_1:def_5; hence (r (#) h) . r1 < (r (#) h) . r2 by A17, VALUED_1:def_5; ::_thesis: verum end; hence (r (#) h) | Y is increasing by Th20; ::_thesis: verum end; theorem Th34: :: RFUNCT_2:34 for Y being set for r being Element of REAL for h being PartFunc of REAL,REAL holds ( ( h | Y is non-decreasing & 0 <= r implies (r (#) h) | Y is non-decreasing ) & ( h | Y is non-decreasing & r <= 0 implies (r (#) h) | Y is non-increasing ) ) proof let Y be set ; ::_thesis: for r being Element of REAL for h being PartFunc of REAL,REAL holds ( ( h | Y is non-decreasing & 0 <= r implies (r (#) h) | Y is non-decreasing ) & ( h | Y is non-decreasing & r <= 0 implies (r (#) h) | Y is non-increasing ) ) let r be Element of REAL ; ::_thesis: for h being PartFunc of REAL,REAL holds ( ( h | Y is non-decreasing & 0 <= r implies (r (#) h) | Y is non-decreasing ) & ( h | Y is non-decreasing & r <= 0 implies (r (#) h) | Y is non-increasing ) ) let h be PartFunc of REAL,REAL; ::_thesis: ( ( h | Y is non-decreasing & 0 <= r implies (r (#) h) | Y is non-decreasing ) & ( h | Y is non-decreasing & r <= 0 implies (r (#) h) | Y is non-increasing ) ) thus ( h | Y is non-decreasing & 0 <= r implies (r (#) h) | Y is non-decreasing ) ::_thesis: ( h | Y is non-decreasing & r <= 0 implies (r (#) h) | Y is non-increasing ) proof assume that A1: h | Y is non-decreasing and A2: 0 <= r ; ::_thesis: (r (#) h) | Y is non-decreasing now__::_thesis:_for_r1,_r2_being_Element_of_REAL_st_r1_in_Y_/\_(dom_(r_(#)_h))_&_r2_in_Y_/\_(dom_(r_(#)_h))_&_r1_<_r2_holds_ (r_(#)_h)_._r1_<=_(r_(#)_h)_._r2 let r1, r2 be Element of REAL ; ::_thesis: ( r1 in Y /\ (dom (r (#) h)) & r2 in Y /\ (dom (r (#) h)) & r1 < r2 implies (r (#) h) . r1 <= (r (#) h) . r2 ) assume that A3: r1 in Y /\ (dom (r (#) h)) and A4: r2 in Y /\ (dom (r (#) h)) and A5: r1 < r2 ; ::_thesis: (r (#) h) . r1 <= (r (#) h) . r2 A6: r2 in Y by A4, XBOOLE_0:def_4; A7: r2 in dom (r (#) h) by A4, XBOOLE_0:def_4; then r2 in dom h by VALUED_1:def_5; then A8: r2 in Y /\ (dom h) by A6, XBOOLE_0:def_4; A9: r1 in Y by A3, XBOOLE_0:def_4; A10: r1 in dom (r (#) h) by A3, XBOOLE_0:def_4; then r1 in dom h by VALUED_1:def_5; then r1 in Y /\ (dom h) by A9, XBOOLE_0:def_4; then h . r1 <= h . r2 by A1, A5, A8, Th22; then r * (h . r1) <= (h . r2) * r by A2, XREAL_1:64; then (r (#) h) . r1 <= r * (h . r2) by A10, VALUED_1:def_5; hence (r (#) h) . r1 <= (r (#) h) . r2 by A7, VALUED_1:def_5; ::_thesis: verum end; hence (r (#) h) | Y is non-decreasing by Th22; ::_thesis: verum end; assume that A11: h | Y is non-decreasing and A12: r <= 0 ; ::_thesis: (r (#) h) | Y is non-increasing now__::_thesis:_for_r1,_r2_being_Element_of_REAL_st_r1_in_Y_/\_(dom_(r_(#)_h))_&_r2_in_Y_/\_(dom_(r_(#)_h))_&_r1_<_r2_holds_ (r_(#)_h)_._r2_<=_(r_(#)_h)_._r1 let r1, r2 be Element of REAL ; ::_thesis: ( r1 in Y /\ (dom (r (#) h)) & r2 in Y /\ (dom (r (#) h)) & r1 < r2 implies (r (#) h) . r2 <= (r (#) h) . r1 ) assume that A13: r1 in Y /\ (dom (r (#) h)) and A14: r2 in Y /\ (dom (r (#) h)) and A15: r1 < r2 ; ::_thesis: (r (#) h) . r2 <= (r (#) h) . r1 A16: r2 in Y by A14, XBOOLE_0:def_4; A17: r2 in dom (r (#) h) by A14, XBOOLE_0:def_4; then r2 in dom h by VALUED_1:def_5; then A18: r2 in Y /\ (dom h) by A16, XBOOLE_0:def_4; A19: r1 in Y by A13, XBOOLE_0:def_4; A20: r1 in dom (r (#) h) by A13, XBOOLE_0:def_4; then r1 in dom h by VALUED_1:def_5; then r1 in Y /\ (dom h) by A19, XBOOLE_0:def_4; then h . r1 <= h . r2 by A11, A15, A18, Th22; then r * (h . r2) <= r * (h . r1) by A12, XREAL_1:65; then (r (#) h) . r2 <= r * (h . r1) by A17, VALUED_1:def_5; hence (r (#) h) . r2 <= (r (#) h) . r1 by A20, VALUED_1:def_5; ::_thesis: verum end; hence (r (#) h) | Y is non-increasing by Th23; ::_thesis: verum end; theorem :: RFUNCT_2:35 for Y being set for r being Element of REAL for h being PartFunc of REAL,REAL holds ( ( h | Y is non-increasing & 0 <= r implies (r (#) h) | Y is non-increasing ) & ( h | Y is non-increasing & r <= 0 implies (r (#) h) | Y is non-decreasing ) ) proof let Y be set ; ::_thesis: for r being Element of REAL for h being PartFunc of REAL,REAL holds ( ( h | Y is non-increasing & 0 <= r implies (r (#) h) | Y is non-increasing ) & ( h | Y is non-increasing & r <= 0 implies (r (#) h) | Y is non-decreasing ) ) let r be Element of REAL ; ::_thesis: for h being PartFunc of REAL,REAL holds ( ( h | Y is non-increasing & 0 <= r implies (r (#) h) | Y is non-increasing ) & ( h | Y is non-increasing & r <= 0 implies (r (#) h) | Y is non-decreasing ) ) let h be PartFunc of REAL,REAL; ::_thesis: ( ( h | Y is non-increasing & 0 <= r implies (r (#) h) | Y is non-increasing ) & ( h | Y is non-increasing & r <= 0 implies (r (#) h) | Y is non-decreasing ) ) thus ( h | Y is non-increasing & 0 <= r implies (r (#) h) | Y is non-increasing ) ::_thesis: ( h | Y is non-increasing & r <= 0 implies (r (#) h) | Y is non-decreasing ) proof assume that A1: h | Y is non-increasing and A2: 0 <= r ; ::_thesis: (r (#) h) | Y is non-increasing now__::_thesis:_for_r1,_r2_being_Element_of_REAL_st_r1_in_Y_/\_(dom_(r_(#)_h))_&_r2_in_Y_/\_(dom_(r_(#)_h))_&_r1_<_r2_holds_ (r_(#)_h)_._r2_<=_(r_(#)_h)_._r1 let r1, r2 be Element of REAL ; ::_thesis: ( r1 in Y /\ (dom (r (#) h)) & r2 in Y /\ (dom (r (#) h)) & r1 < r2 implies (r (#) h) . r2 <= (r (#) h) . r1 ) assume that A3: r1 in Y /\ (dom (r (#) h)) and A4: r2 in Y /\ (dom (r (#) h)) and A5: r1 < r2 ; ::_thesis: (r (#) h) . r2 <= (r (#) h) . r1 A6: r2 in Y by A4, XBOOLE_0:def_4; A7: r2 in dom (r (#) h) by A4, XBOOLE_0:def_4; then r2 in dom h by VALUED_1:def_5; then A8: r2 in Y /\ (dom h) by A6, XBOOLE_0:def_4; A9: r1 in Y by A3, XBOOLE_0:def_4; A10: r1 in dom (r (#) h) by A3, XBOOLE_0:def_4; then r1 in dom h by VALUED_1:def_5; then r1 in Y /\ (dom h) by A9, XBOOLE_0:def_4; then h . r2 <= h . r1 by A1, A5, A8, Th23; then r * (h . r2) <= (h . r1) * r by A2, XREAL_1:64; then (r (#) h) . r2 <= r * (h . r1) by A7, VALUED_1:def_5; hence (r (#) h) . r2 <= (r (#) h) . r1 by A10, VALUED_1:def_5; ::_thesis: verum end; hence (r (#) h) | Y is non-increasing by Th23; ::_thesis: verum end; assume that A11: h | Y is non-increasing and A12: r <= 0 ; ::_thesis: (r (#) h) | Y is non-decreasing now__::_thesis:_for_r1,_r2_being_Element_of_REAL_st_r1_in_Y_/\_(dom_(r_(#)_h))_&_r2_in_Y_/\_(dom_(r_(#)_h))_&_r1_<_r2_holds_ (r_(#)_h)_._r1_<=_(r_(#)_h)_._r2 let r1, r2 be Element of REAL ; ::_thesis: ( r1 in Y /\ (dom (r (#) h)) & r2 in Y /\ (dom (r (#) h)) & r1 < r2 implies (r (#) h) . r1 <= (r (#) h) . r2 ) assume that A13: r1 in Y /\ (dom (r (#) h)) and A14: r2 in Y /\ (dom (r (#) h)) and A15: r1 < r2 ; ::_thesis: (r (#) h) . r1 <= (r (#) h) . r2 A16: r2 in Y by A14, XBOOLE_0:def_4; A17: r2 in dom (r (#) h) by A14, XBOOLE_0:def_4; then r2 in dom h by VALUED_1:def_5; then A18: r2 in Y /\ (dom h) by A16, XBOOLE_0:def_4; A19: r1 in Y by A13, XBOOLE_0:def_4; A20: r1 in dom (r (#) h) by A13, XBOOLE_0:def_4; then r1 in dom h by VALUED_1:def_5; then r1 in Y /\ (dom h) by A19, XBOOLE_0:def_4; then h . r2 <= h . r1 by A11, A15, A18, Th23; then r * (h . r1) <= r * (h . r2) by A12, XREAL_1:65; then (r (#) h) . r1 <= r * (h . r2) by A20, VALUED_1:def_5; hence (r (#) h) . r1 <= (r (#) h) . r2 by A17, VALUED_1:def_5; ::_thesis: verum end; hence (r (#) h) | Y is non-decreasing by Th22; ::_thesis: verum end; theorem Th36: :: RFUNCT_2:36 for X, Y being set for r being Element of REAL for h1, h2 being PartFunc of REAL,REAL st r in (X /\ Y) /\ (dom (h1 + h2)) holds ( r in X /\ (dom h1) & r in Y /\ (dom h2) ) proof let X, Y be set ; ::_thesis: for r being Element of REAL for h1, h2 being PartFunc of REAL,REAL st r in (X /\ Y) /\ (dom (h1 + h2)) holds ( r in X /\ (dom h1) & r in Y /\ (dom h2) ) let r be Element of REAL ; ::_thesis: for h1, h2 being PartFunc of REAL,REAL st r in (X /\ Y) /\ (dom (h1 + h2)) holds ( r in X /\ (dom h1) & r in Y /\ (dom h2) ) let h1, h2 be PartFunc of REAL,REAL; ::_thesis: ( r in (X /\ Y) /\ (dom (h1 + h2)) implies ( r in X /\ (dom h1) & r in Y /\ (dom h2) ) ) assume A1: r in (X /\ Y) /\ (dom (h1 + h2)) ; ::_thesis: ( r in X /\ (dom h1) & r in Y /\ (dom h2) ) then r in dom (h1 + h2) by XBOOLE_0:def_4; then r in (dom h1) /\ (dom h2) by VALUED_1:def_1; then A2: ( r in dom h1 & r in dom h2 ) by XBOOLE_0:def_4; r in X /\ Y by A1, XBOOLE_0:def_4; then ( r in X & r in Y ) by XBOOLE_0:def_4; hence ( r in X /\ (dom h1) & r in Y /\ (dom h2) ) by A2, XBOOLE_0:def_4; ::_thesis: verum end; theorem :: RFUNCT_2:37 for X, Y being set for h1, h2 being PartFunc of REAL,REAL holds ( ( h1 | X is increasing & h2 | Y is increasing implies (h1 + h2) | (X /\ Y) is increasing ) & ( h1 | X is decreasing & h2 | Y is decreasing implies (h1 + h2) | (X /\ Y) is decreasing ) & ( h1 | X is non-decreasing & h2 | Y is non-decreasing implies (h1 + h2) | (X /\ Y) is non-decreasing ) & ( h1 | X is non-increasing & h2 | Y is non-increasing implies (h1 + h2) | (X /\ Y) is non-increasing ) ) proof let X, Y be set ; ::_thesis: for h1, h2 being PartFunc of REAL,REAL holds ( ( h1 | X is increasing & h2 | Y is increasing implies (h1 + h2) | (X /\ Y) is increasing ) & ( h1 | X is decreasing & h2 | Y is decreasing implies (h1 + h2) | (X /\ Y) is decreasing ) & ( h1 | X is non-decreasing & h2 | Y is non-decreasing implies (h1 + h2) | (X /\ Y) is non-decreasing ) & ( h1 | X is non-increasing & h2 | Y is non-increasing implies (h1 + h2) | (X /\ Y) is non-increasing ) ) let h1, h2 be PartFunc of REAL,REAL; ::_thesis: ( ( h1 | X is increasing & h2 | Y is increasing implies (h1 + h2) | (X /\ Y) is increasing ) & ( h1 | X is decreasing & h2 | Y is decreasing implies (h1 + h2) | (X /\ Y) is decreasing ) & ( h1 | X is non-decreasing & h2 | Y is non-decreasing implies (h1 + h2) | (X /\ Y) is non-decreasing ) & ( h1 | X is non-increasing & h2 | Y is non-increasing implies (h1 + h2) | (X /\ Y) is non-increasing ) ) thus ( h1 | X is increasing & h2 | Y is increasing implies (h1 + h2) | (X /\ Y) is increasing ) ::_thesis: ( ( h1 | X is decreasing & h2 | Y is decreasing implies (h1 + h2) | (X /\ Y) is decreasing ) & ( h1 | X is non-decreasing & h2 | Y is non-decreasing implies (h1 + h2) | (X /\ Y) is non-decreasing ) & ( h1 | X is non-increasing & h2 | Y is non-increasing implies (h1 + h2) | (X /\ Y) is non-increasing ) ) proof assume that A1: h1 | X is increasing and A2: h2 | Y is increasing ; ::_thesis: (h1 + h2) | (X /\ Y) is increasing now__::_thesis:_for_r1,_r2_being_Element_of_REAL_st_r1_in_(X_/\_Y)_/\_(dom_(h1_+_h2))_&_r2_in_(X_/\_Y)_/\_(dom_(h1_+_h2))_&_r1_<_r2_holds_ (h1_+_h2)_._r1_<_(h1_+_h2)_._r2 let r1, r2 be Element of REAL ; ::_thesis: ( r1 in (X /\ Y) /\ (dom (h1 + h2)) & r2 in (X /\ Y) /\ (dom (h1 + h2)) & r1 < r2 implies (h1 + h2) . r1 < (h1 + h2) . r2 ) assume that A3: r1 in (X /\ Y) /\ (dom (h1 + h2)) and A4: r2 in (X /\ Y) /\ (dom (h1 + h2)) and A5: r1 < r2 ; ::_thesis: (h1 + h2) . r1 < (h1 + h2) . r2 ( r1 in Y /\ (dom h2) & r2 in Y /\ (dom h2) ) by A3, A4, Th36; then A6: h2 . r1 < h2 . r2 by A2, A5, Th20; A7: r1 in dom (h1 + h2) by A3, XBOOLE_0:def_4; ( r1 in X /\ (dom h1) & r2 in X /\ (dom h1) ) by A3, A4, Th36; then h1 . r1 < h1 . r2 by A1, A5, Th20; then (h1 . r1) + (h2 . r1) < (h1 . r2) + (h2 . r2) by A6, XREAL_1:8; then A8: (h1 + h2) . r1 < (h1 . r2) + (h2 . r2) by A7, VALUED_1:def_1; r2 in dom (h1 + h2) by A4, XBOOLE_0:def_4; hence (h1 + h2) . r1 < (h1 + h2) . r2 by A8, VALUED_1:def_1; ::_thesis: verum end; hence (h1 + h2) | (X /\ Y) is increasing by Th20; ::_thesis: verum end; thus ( h1 | X is decreasing & h2 | Y is decreasing implies (h1 + h2) | (X /\ Y) is decreasing ) ::_thesis: ( ( h1 | X is non-decreasing & h2 | Y is non-decreasing implies (h1 + h2) | (X /\ Y) is non-decreasing ) & ( h1 | X is non-increasing & h2 | Y is non-increasing implies (h1 + h2) | (X /\ Y) is non-increasing ) ) proof assume that A9: h1 | X is decreasing and A10: h2 | Y is decreasing ; ::_thesis: (h1 + h2) | (X /\ Y) is decreasing now__::_thesis:_for_r1,_r2_being_Element_of_REAL_st_r1_in_(X_/\_Y)_/\_(dom_(h1_+_h2))_&_r2_in_(X_/\_Y)_/\_(dom_(h1_+_h2))_&_r1_<_r2_holds_ (h1_+_h2)_._r2_<_(h1_+_h2)_._r1 let r1, r2 be Element of REAL ; ::_thesis: ( r1 in (X /\ Y) /\ (dom (h1 + h2)) & r2 in (X /\ Y) /\ (dom (h1 + h2)) & r1 < r2 implies (h1 + h2) . r2 < (h1 + h2) . r1 ) assume that A11: r1 in (X /\ Y) /\ (dom (h1 + h2)) and A12: r2 in (X /\ Y) /\ (dom (h1 + h2)) and A13: r1 < r2 ; ::_thesis: (h1 + h2) . r2 < (h1 + h2) . r1 ( r1 in Y /\ (dom h2) & r2 in Y /\ (dom h2) ) by A11, A12, Th36; then A14: h2 . r2 < h2 . r1 by A10, A13, Th21; A15: r2 in dom (h1 + h2) by A12, XBOOLE_0:def_4; ( r1 in X /\ (dom h1) & r2 in X /\ (dom h1) ) by A11, A12, Th36; then h1 . r2 < h1 . r1 by A9, A13, Th21; then (h1 . r2) + (h2 . r2) < (h1 . r1) + (h2 . r1) by A14, XREAL_1:8; then A16: (h1 + h2) . r2 < (h1 . r1) + (h2 . r1) by A15, VALUED_1:def_1; r1 in dom (h1 + h2) by A11, XBOOLE_0:def_4; hence (h1 + h2) . r2 < (h1 + h2) . r1 by A16, VALUED_1:def_1; ::_thesis: verum end; hence (h1 + h2) | (X /\ Y) is decreasing by Th21; ::_thesis: verum end; thus ( h1 | X is non-decreasing & h2 | Y is non-decreasing implies (h1 + h2) | (X /\ Y) is non-decreasing ) ::_thesis: ( h1 | X is non-increasing & h2 | Y is non-increasing implies (h1 + h2) | (X /\ Y) is non-increasing ) proof assume that A17: h1 | X is non-decreasing and A18: h2 | Y is non-decreasing ; ::_thesis: (h1 + h2) | (X /\ Y) is non-decreasing now__::_thesis:_for_r1,_r2_being_Element_of_REAL_st_r1_in_(X_/\_Y)_/\_(dom_(h1_+_h2))_&_r2_in_(X_/\_Y)_/\_(dom_(h1_+_h2))_&_r1_<_r2_holds_ (h1_+_h2)_._r1_<=_(h1_+_h2)_._r2 let r1, r2 be Element of REAL ; ::_thesis: ( r1 in (X /\ Y) /\ (dom (h1 + h2)) & r2 in (X /\ Y) /\ (dom (h1 + h2)) & r1 < r2 implies (h1 + h2) . r1 <= (h1 + h2) . r2 ) assume that A19: r1 in (X /\ Y) /\ (dom (h1 + h2)) and A20: r2 in (X /\ Y) /\ (dom (h1 + h2)) and A21: r1 < r2 ; ::_thesis: (h1 + h2) . r1 <= (h1 + h2) . r2 ( r1 in Y /\ (dom h2) & r2 in Y /\ (dom h2) ) by A19, A20, Th36; then A22: h2 . r1 <= h2 . r2 by A18, A21, Th22; A23: r1 in dom (h1 + h2) by A19, XBOOLE_0:def_4; ( r1 in X /\ (dom h1) & r2 in X /\ (dom h1) ) by A19, A20, Th36; then h1 . r1 <= h1 . r2 by A17, A21, Th22; then (h1 . r1) + (h2 . r1) <= (h1 . r2) + (h2 . r2) by A22, XREAL_1:7; then A24: (h1 + h2) . r1 <= (h1 . r2) + (h2 . r2) by A23, VALUED_1:def_1; r2 in dom (h1 + h2) by A20, XBOOLE_0:def_4; hence (h1 + h2) . r1 <= (h1 + h2) . r2 by A24, VALUED_1:def_1; ::_thesis: verum end; hence (h1 + h2) | (X /\ Y) is non-decreasing by Th22; ::_thesis: verum end; assume that A25: h1 | X is non-increasing and A26: h2 | Y is non-increasing ; ::_thesis: (h1 + h2) | (X /\ Y) is non-increasing now__::_thesis:_for_r1,_r2_being_Element_of_REAL_st_r1_in_(X_/\_Y)_/\_(dom_(h1_+_h2))_&_r2_in_(X_/\_Y)_/\_(dom_(h1_+_h2))_&_r1_<_r2_holds_ (h1_+_h2)_._r2_<=_(h1_+_h2)_._r1 let r1, r2 be Element of REAL ; ::_thesis: ( r1 in (X /\ Y) /\ (dom (h1 + h2)) & r2 in (X /\ Y) /\ (dom (h1 + h2)) & r1 < r2 implies (h1 + h2) . r2 <= (h1 + h2) . r1 ) assume that A27: r1 in (X /\ Y) /\ (dom (h1 + h2)) and A28: r2 in (X /\ Y) /\ (dom (h1 + h2)) and A29: r1 < r2 ; ::_thesis: (h1 + h2) . r2 <= (h1 + h2) . r1 ( r1 in Y /\ (dom h2) & r2 in Y /\ (dom h2) ) by A27, A28, Th36; then A30: h2 . r2 <= h2 . r1 by A26, A29, Th23; A31: r2 in dom (h1 + h2) by A28, XBOOLE_0:def_4; ( r1 in X /\ (dom h1) & r2 in X /\ (dom h1) ) by A27, A28, Th36; then h1 . r2 <= h1 . r1 by A25, A29, Th23; then (h1 . r2) + (h2 . r2) <= (h1 . r1) + (h2 . r1) by A30, XREAL_1:7; then A32: (h1 + h2) . r2 <= (h1 . r1) + (h2 . r1) by A31, VALUED_1:def_1; r1 in dom (h1 + h2) by A27, XBOOLE_0:def_4; hence (h1 + h2) . r2 <= (h1 + h2) . r1 by A32, VALUED_1:def_1; ::_thesis: verum end; hence (h1 + h2) | (X /\ Y) is non-increasing by Th23; ::_thesis: verum end; theorem :: RFUNCT_2:38 for X, Y being set for h1, h2 being PartFunc of REAL,REAL holds ( ( h1 | X is increasing & h2 | Y is V8() implies (h1 + h2) | (X /\ Y) is increasing ) & ( h1 | X is decreasing & h2 | Y is V8() implies (h1 + h2) | (X /\ Y) is decreasing ) ) proof let X, Y be set ; ::_thesis: for h1, h2 being PartFunc of REAL,REAL holds ( ( h1 | X is increasing & h2 | Y is V8() implies (h1 + h2) | (X /\ Y) is increasing ) & ( h1 | X is decreasing & h2 | Y is V8() implies (h1 + h2) | (X /\ Y) is decreasing ) ) let h1, h2 be PartFunc of REAL,REAL; ::_thesis: ( ( h1 | X is increasing & h2 | Y is V8() implies (h1 + h2) | (X /\ Y) is increasing ) & ( h1 | X is decreasing & h2 | Y is V8() implies (h1 + h2) | (X /\ Y) is decreasing ) ) thus ( h1 | X is increasing & h2 | Y is V8() implies (h1 + h2) | (X /\ Y) is increasing ) ::_thesis: ( h1 | X is decreasing & h2 | Y is V8() implies (h1 + h2) | (X /\ Y) is decreasing ) proof assume that A1: h1 | X is increasing and A2: h2 | Y is V8() ; ::_thesis: (h1 + h2) | (X /\ Y) is increasing consider r being Element of REAL such that A3: for p being Element of REAL st p in Y /\ (dom h2) holds h2 . p = r by A2, PARTFUN2:57; now__::_thesis:_for_r1,_r2_being_Element_of_REAL_st_r1_in_(X_/\_Y)_/\_(dom_(h1_+_h2))_&_r2_in_(X_/\_Y)_/\_(dom_(h1_+_h2))_&_r1_<_r2_holds_ (h1_+_h2)_._r1_<_(h1_+_h2)_._r2 let r1, r2 be Element of REAL ; ::_thesis: ( r1 in (X /\ Y) /\ (dom (h1 + h2)) & r2 in (X /\ Y) /\ (dom (h1 + h2)) & r1 < r2 implies (h1 + h2) . r1 < (h1 + h2) . r2 ) assume that A4: r1 in (X /\ Y) /\ (dom (h1 + h2)) and A5: r2 in (X /\ Y) /\ (dom (h1 + h2)) and A6: r1 < r2 ; ::_thesis: (h1 + h2) . r1 < (h1 + h2) . r2 ( r1 in X /\ (dom h1) & r2 in X /\ (dom h1) ) by A4, A5, Th36; then h1 . r1 < h1 . r2 by A1, A6, Th20; then A7: (h1 . r1) + r < (h1 . r2) + r by XREAL_1:6; r1 in Y /\ (dom h2) by A4, Th36; then A8: (h1 . r1) + (h2 . r1) < (h1 . r2) + r by A3, A7; A9: r1 in dom (h1 + h2) by A4, XBOOLE_0:def_4; r2 in Y /\ (dom h2) by A5, Th36; then (h1 . r1) + (h2 . r1) < (h1 . r2) + (h2 . r2) by A3, A8; then A10: (h1 + h2) . r1 < (h1 . r2) + (h2 . r2) by A9, VALUED_1:def_1; r2 in dom (h1 + h2) by A5, XBOOLE_0:def_4; hence (h1 + h2) . r1 < (h1 + h2) . r2 by A10, VALUED_1:def_1; ::_thesis: verum end; hence (h1 + h2) | (X /\ Y) is increasing by Th20; ::_thesis: verum end; assume that A11: h1 | X is decreasing and A12: h2 | Y is V8() ; ::_thesis: (h1 + h2) | (X /\ Y) is decreasing consider r being Element of REAL such that A13: for p being Element of REAL st p in Y /\ (dom h2) holds h2 . p = r by A12, PARTFUN2:57; now__::_thesis:_for_r1,_r2_being_Element_of_REAL_st_r1_in_(X_/\_Y)_/\_(dom_(h1_+_h2))_&_r2_in_(X_/\_Y)_/\_(dom_(h1_+_h2))_&_r1_<_r2_holds_ (h1_+_h2)_._r2_<_(h1_+_h2)_._r1 let r1, r2 be Element of REAL ; ::_thesis: ( r1 in (X /\ Y) /\ (dom (h1 + h2)) & r2 in (X /\ Y) /\ (dom (h1 + h2)) & r1 < r2 implies (h1 + h2) . r2 < (h1 + h2) . r1 ) assume that A14: r1 in (X /\ Y) /\ (dom (h1 + h2)) and A15: r2 in (X /\ Y) /\ (dom (h1 + h2)) and A16: r1 < r2 ; ::_thesis: (h1 + h2) . r2 < (h1 + h2) . r1 ( r1 in X /\ (dom h1) & r2 in X /\ (dom h1) ) by A14, A15, Th36; then h1 . r2 < h1 . r1 by A11, A16, Th21; then A17: (h1 . r2) + r < (h1 . r1) + r by XREAL_1:6; r2 in Y /\ (dom h2) by A15, Th36; then A18: (h1 . r2) + (h2 . r2) < (h1 . r1) + r by A13, A17; A19: r2 in dom (h1 + h2) by A15, XBOOLE_0:def_4; r1 in Y /\ (dom h2) by A14, Th36; then (h1 . r2) + (h2 . r2) < (h1 . r1) + (h2 . r1) by A13, A18; then A20: (h1 + h2) . r2 < (h1 . r1) + (h2 . r1) by A19, VALUED_1:def_1; r1 in dom (h1 + h2) by A14, XBOOLE_0:def_4; hence (h1 + h2) . r2 < (h1 + h2) . r1 by A20, VALUED_1:def_1; ::_thesis: verum end; hence (h1 + h2) | (X /\ Y) is decreasing by Th21; ::_thesis: verum end; theorem :: RFUNCT_2:39 for X, Y being set for h1, h2 being PartFunc of REAL,REAL st h1 | X is increasing & h2 | Y is non-decreasing holds (h1 + h2) | (X /\ Y) is increasing proof let X, Y be set ; ::_thesis: for h1, h2 being PartFunc of REAL,REAL st h1 | X is increasing & h2 | Y is non-decreasing holds (h1 + h2) | (X /\ Y) is increasing let h1, h2 be PartFunc of REAL,REAL; ::_thesis: ( h1 | X is increasing & h2 | Y is non-decreasing implies (h1 + h2) | (X /\ Y) is increasing ) assume that A1: h1 | X is increasing and A2: h2 | Y is non-decreasing ; ::_thesis: (h1 + h2) | (X /\ Y) is increasing now__::_thesis:_for_r1,_r2_being_Element_of_REAL_st_r1_in_(X_/\_Y)_/\_(dom_(h1_+_h2))_&_r2_in_(X_/\_Y)_/\_(dom_(h1_+_h2))_&_r1_<_r2_holds_ (h1_+_h2)_._r1_<_(h1_+_h2)_._r2 let r1, r2 be Element of REAL ; ::_thesis: ( r1 in (X /\ Y) /\ (dom (h1 + h2)) & r2 in (X /\ Y) /\ (dom (h1 + h2)) & r1 < r2 implies (h1 + h2) . r1 < (h1 + h2) . r2 ) assume that A3: r1 in (X /\ Y) /\ (dom (h1 + h2)) and A4: r2 in (X /\ Y) /\ (dom (h1 + h2)) and A5: r1 < r2 ; ::_thesis: (h1 + h2) . r1 < (h1 + h2) . r2 A6: r2 in X /\ Y by A4, XBOOLE_0:def_4; then A7: r2 in Y by XBOOLE_0:def_4; A8: r2 in dom (h1 + h2) by A4, XBOOLE_0:def_4; then A9: r2 in (dom h1) /\ (dom h2) by VALUED_1:def_1; then r2 in dom h2 by XBOOLE_0:def_4; then A10: r2 in Y /\ (dom h2) by A7, XBOOLE_0:def_4; A11: r1 in X /\ Y by A3, XBOOLE_0:def_4; then A12: r1 in Y by XBOOLE_0:def_4; A13: r1 in dom (h1 + h2) by A3, XBOOLE_0:def_4; then A14: r1 in (dom h1) /\ (dom h2) by VALUED_1:def_1; then r1 in dom h2 by XBOOLE_0:def_4; then r1 in Y /\ (dom h2) by A12, XBOOLE_0:def_4; then A15: h2 . r1 <= h2 . r2 by A2, A5, A10, Th22; A16: r2 in X by A6, XBOOLE_0:def_4; A17: r1 in X by A11, XBOOLE_0:def_4; r2 in dom h1 by A9, XBOOLE_0:def_4; then A18: r2 in X /\ (dom h1) by A16, XBOOLE_0:def_4; r1 in dom h1 by A14, XBOOLE_0:def_4; then r1 in X /\ (dom h1) by A17, XBOOLE_0:def_4; then h1 . r1 < h1 . r2 by A1, A5, A18, Th20; then (h1 . r1) + (h2 . r1) < (h1 . r2) + (h2 . r2) by A15, XREAL_1:8; then (h1 + h2) . r1 < (h1 . r2) + (h2 . r2) by A13, VALUED_1:def_1; hence (h1 + h2) . r1 < (h1 + h2) . r2 by A8, VALUED_1:def_1; ::_thesis: verum end; hence (h1 + h2) | (X /\ Y) is increasing by Th20; ::_thesis: verum end; theorem :: RFUNCT_2:40 for X, Y being set for h1, h2 being PartFunc of REAL,REAL st h1 | X is non-increasing & h2 | Y is V8() holds (h1 + h2) | (X /\ Y) is non-increasing proof let X, Y be set ; ::_thesis: for h1, h2 being PartFunc of REAL,REAL st h1 | X is non-increasing & h2 | Y is V8() holds (h1 + h2) | (X /\ Y) is non-increasing let h1, h2 be PartFunc of REAL,REAL; ::_thesis: ( h1 | X is non-increasing & h2 | Y is V8() implies (h1 + h2) | (X /\ Y) is non-increasing ) assume that A1: h1 | X is non-increasing and A2: h2 | Y is V8() ; ::_thesis: (h1 + h2) | (X /\ Y) is non-increasing now__::_thesis:_for_r1,_r2_being_Element_of_REAL_st_r1_in_(X_/\_Y)_/\_(dom_(h1_+_h2))_&_r2_in_(X_/\_Y)_/\_(dom_(h1_+_h2))_&_r1_<_r2_holds_ (h1_+_h2)_._r2_<=_(h1_+_h2)_._r1 let r1, r2 be Element of REAL ; ::_thesis: ( r1 in (X /\ Y) /\ (dom (h1 + h2)) & r2 in (X /\ Y) /\ (dom (h1 + h2)) & r1 < r2 implies (h1 + h2) . r2 <= (h1 + h2) . r1 ) assume that A3: r1 in (X /\ Y) /\ (dom (h1 + h2)) and A4: r2 in (X /\ Y) /\ (dom (h1 + h2)) and A5: r1 < r2 ; ::_thesis: (h1 + h2) . r2 <= (h1 + h2) . r1 A6: r2 in X /\ Y by A4, XBOOLE_0:def_4; then A7: r2 in X by XBOOLE_0:def_4; A8: r2 in Y by A6, XBOOLE_0:def_4; A9: r2 in dom (h1 + h2) by A4, XBOOLE_0:def_4; then A10: r2 in (dom h1) /\ (dom h2) by VALUED_1:def_1; then r2 in dom h2 by XBOOLE_0:def_4; then A11: r2 in Y /\ (dom h2) by A8, XBOOLE_0:def_4; r2 in dom h1 by A10, XBOOLE_0:def_4; then A12: r2 in X /\ (dom h1) by A7, XBOOLE_0:def_4; A13: r1 in X /\ Y by A3, XBOOLE_0:def_4; then A14: r1 in X by XBOOLE_0:def_4; A15: r1 in Y by A13, XBOOLE_0:def_4; A16: r1 in dom (h1 + h2) by A3, XBOOLE_0:def_4; then A17: r1 in (dom h1) /\ (dom h2) by VALUED_1:def_1; then r1 in dom h2 by XBOOLE_0:def_4; then r1 in Y /\ (dom h2) by A15, XBOOLE_0:def_4; then A18: h2 . r2 = h2 . r1 by A2, A11, PARTFUN2:58; r1 in dom h1 by A17, XBOOLE_0:def_4; then r1 in X /\ (dom h1) by A14, XBOOLE_0:def_4; then h1 . r2 <= h1 . r1 by A1, A5, A12, Th23; then (h1 . r2) + (h2 . r2) <= (h1 . r1) + (h2 . r1) by A18, XREAL_1:6; then (h1 + h2) . r2 <= (h1 . r1) + (h2 . r1) by A9, VALUED_1:def_1; hence (h1 + h2) . r2 <= (h1 + h2) . r1 by A16, VALUED_1:def_1; ::_thesis: verum end; hence (h1 + h2) | (X /\ Y) is non-increasing by Th23; ::_thesis: verum end; theorem :: RFUNCT_2:41 for X, Y being set for h1, h2 being PartFunc of REAL,REAL st h1 | X is decreasing & h2 | Y is non-increasing holds (h1 + h2) | (X /\ Y) is decreasing proof let X, Y be set ; ::_thesis: for h1, h2 being PartFunc of REAL,REAL st h1 | X is decreasing & h2 | Y is non-increasing holds (h1 + h2) | (X /\ Y) is decreasing let h1, h2 be PartFunc of REAL,REAL; ::_thesis: ( h1 | X is decreasing & h2 | Y is non-increasing implies (h1 + h2) | (X /\ Y) is decreasing ) assume that A1: h1 | X is decreasing and A2: h2 | Y is non-increasing ; ::_thesis: (h1 + h2) | (X /\ Y) is decreasing now__::_thesis:_for_r1,_r2_being_Element_of_REAL_st_r1_in_(X_/\_Y)_/\_(dom_(h1_+_h2))_&_r2_in_(X_/\_Y)_/\_(dom_(h1_+_h2))_&_r1_<_r2_holds_ (h1_+_h2)_._r2_<_(h1_+_h2)_._r1 let r1, r2 be Element of REAL ; ::_thesis: ( r1 in (X /\ Y) /\ (dom (h1 + h2)) & r2 in (X /\ Y) /\ (dom (h1 + h2)) & r1 < r2 implies (h1 + h2) . r2 < (h1 + h2) . r1 ) assume that A3: r1 in (X /\ Y) /\ (dom (h1 + h2)) and A4: r2 in (X /\ Y) /\ (dom (h1 + h2)) and A5: r1 < r2 ; ::_thesis: (h1 + h2) . r2 < (h1 + h2) . r1 A6: r2 in X /\ Y by A4, XBOOLE_0:def_4; then A7: r2 in Y by XBOOLE_0:def_4; A8: r2 in dom (h1 + h2) by A4, XBOOLE_0:def_4; then A9: r2 in (dom h1) /\ (dom h2) by VALUED_1:def_1; then r2 in dom h2 by XBOOLE_0:def_4; then A10: r2 in Y /\ (dom h2) by A7, XBOOLE_0:def_4; A11: r1 in X /\ Y by A3, XBOOLE_0:def_4; then A12: r1 in Y by XBOOLE_0:def_4; A13: r1 in dom (h1 + h2) by A3, XBOOLE_0:def_4; then A14: r1 in (dom h1) /\ (dom h2) by VALUED_1:def_1; then r1 in dom h2 by XBOOLE_0:def_4; then r1 in Y /\ (dom h2) by A12, XBOOLE_0:def_4; then A15: h2 . r2 <= h2 . r1 by A2, A5, A10, Th23; A16: r2 in X by A6, XBOOLE_0:def_4; A17: r1 in X by A11, XBOOLE_0:def_4; r2 in dom h1 by A9, XBOOLE_0:def_4; then A18: r2 in X /\ (dom h1) by A16, XBOOLE_0:def_4; r1 in dom h1 by A14, XBOOLE_0:def_4; then r1 in X /\ (dom h1) by A17, XBOOLE_0:def_4; then h1 . r2 < h1 . r1 by A1, A5, A18, Th21; then (h1 . r2) + (h2 . r2) < (h1 . r1) + (h2 . r1) by A15, XREAL_1:8; then (h1 + h2) . r2 < (h1 . r1) + (h2 . r1) by A8, VALUED_1:def_1; hence (h1 + h2) . r2 < (h1 + h2) . r1 by A13, VALUED_1:def_1; ::_thesis: verum end; hence (h1 + h2) | (X /\ Y) is decreasing by Th21; ::_thesis: verum end; theorem :: RFUNCT_2:42 for X, Y being set for h1, h2 being PartFunc of REAL,REAL st h1 | X is non-decreasing & h2 | Y is V8() holds (h1 + h2) | (X /\ Y) is non-decreasing proof let X, Y be set ; ::_thesis: for h1, h2 being PartFunc of REAL,REAL st h1 | X is non-decreasing & h2 | Y is V8() holds (h1 + h2) | (X /\ Y) is non-decreasing let h1, h2 be PartFunc of REAL,REAL; ::_thesis: ( h1 | X is non-decreasing & h2 | Y is V8() implies (h1 + h2) | (X /\ Y) is non-decreasing ) assume that A1: h1 | X is non-decreasing and A2: h2 | Y is V8() ; ::_thesis: (h1 + h2) | (X /\ Y) is non-decreasing now__::_thesis:_for_r1,_r2_being_Element_of_REAL_st_r1_in_(X_/\_Y)_/\_(dom_(h1_+_h2))_&_r2_in_(X_/\_Y)_/\_(dom_(h1_+_h2))_&_r1_<_r2_holds_ (h1_+_h2)_._r1_<=_(h1_+_h2)_._r2 let r1, r2 be Element of REAL ; ::_thesis: ( r1 in (X /\ Y) /\ (dom (h1 + h2)) & r2 in (X /\ Y) /\ (dom (h1 + h2)) & r1 < r2 implies (h1 + h2) . r1 <= (h1 + h2) . r2 ) assume that A3: r1 in (X /\ Y) /\ (dom (h1 + h2)) and A4: r2 in (X /\ Y) /\ (dom (h1 + h2)) and A5: r1 < r2 ; ::_thesis: (h1 + h2) . r1 <= (h1 + h2) . r2 A6: r2 in X /\ Y by A4, XBOOLE_0:def_4; then A7: r2 in X by XBOOLE_0:def_4; A8: r2 in Y by A6, XBOOLE_0:def_4; A9: r2 in dom (h1 + h2) by A4, XBOOLE_0:def_4; then A10: r2 in (dom h1) /\ (dom h2) by VALUED_1:def_1; then r2 in dom h2 by XBOOLE_0:def_4; then A11: r2 in Y /\ (dom h2) by A8, XBOOLE_0:def_4; r2 in dom h1 by A10, XBOOLE_0:def_4; then A12: r2 in X /\ (dom h1) by A7, XBOOLE_0:def_4; A13: r1 in X /\ Y by A3, XBOOLE_0:def_4; then A14: r1 in X by XBOOLE_0:def_4; A15: r1 in Y by A13, XBOOLE_0:def_4; A16: r1 in dom (h1 + h2) by A3, XBOOLE_0:def_4; then A17: r1 in (dom h1) /\ (dom h2) by VALUED_1:def_1; then r1 in dom h2 by XBOOLE_0:def_4; then r1 in Y /\ (dom h2) by A15, XBOOLE_0:def_4; then A18: h2 . r2 = h2 . r1 by A2, A11, PARTFUN2:58; r1 in dom h1 by A17, XBOOLE_0:def_4; then r1 in X /\ (dom h1) by A14, XBOOLE_0:def_4; then h1 . r1 <= h1 . r2 by A1, A5, A12, Th22; then (h1 . r1) + (h2 . r1) <= (h1 . r2) + (h2 . r2) by A18, XREAL_1:6; then (h1 + h2) . r1 <= (h1 . r2) + (h2 . r2) by A16, VALUED_1:def_1; hence (h1 + h2) . r1 <= (h1 + h2) . r2 by A9, VALUED_1:def_1; ::_thesis: verum end; hence (h1 + h2) | (X /\ Y) is non-decreasing by Th22; ::_thesis: verum end; theorem :: RFUNCT_2:43 for x being set for h being PartFunc of REAL,REAL holds h | {x} is non-increasing proof let x be set ; ::_thesis: for h being PartFunc of REAL,REAL holds h | {x} is non-increasing let h be PartFunc of REAL,REAL; ::_thesis: h | {x} is non-increasing now__::_thesis:_for_r1,_r2_being_Element_of_REAL_st_r1_in_{x}_/\_(dom_h)_&_r2_in_{x}_/\_(dom_h)_&_r1_<_r2_holds_ h_._r1_>=_h_._r2 let r1, r2 be Element of REAL ; ::_thesis: ( r1 in {x} /\ (dom h) & r2 in {x} /\ (dom h) & r1 < r2 implies h . r1 >= h . r2 ) assume that A1: r1 in {x} /\ (dom h) and A2: r2 in {x} /\ (dom h) and r1 < r2 ; ::_thesis: h . r1 >= h . r2 r1 in {x} by A1, XBOOLE_0:def_4; then A3: r1 = x by TARSKI:def_1; r2 in {x} by A2, XBOOLE_0:def_4; hence h . r1 >= h . r2 by A3, TARSKI:def_1; ::_thesis: verum end; hence h | {x} is non-increasing by Th23; ::_thesis: verum end; theorem :: RFUNCT_2:44 for x being set for h being PartFunc of REAL,REAL holds h | {x} is decreasing proof let x be set ; ::_thesis: for h being PartFunc of REAL,REAL holds h | {x} is decreasing let h be PartFunc of REAL,REAL; ::_thesis: h | {x} is decreasing now__::_thesis:_for_r1,_r2_being_Element_of_REAL_st_r1_in_{x}_/\_(dom_h)_&_r2_in_{x}_/\_(dom_h)_&_r1_<_r2_holds_ h_._r1_>_h_._r2 let r1, r2 be Element of REAL ; ::_thesis: ( r1 in {x} /\ (dom h) & r2 in {x} /\ (dom h) & r1 < r2 implies h . r1 > h . r2 ) assume that A1: r1 in {x} /\ (dom h) and A2: r2 in {x} /\ (dom h) and A3: r1 < r2 ; ::_thesis: h . r1 > h . r2 r1 in {x} by A1, XBOOLE_0:def_4; then A4: r1 = x by TARSKI:def_1; r2 in {x} by A2, XBOOLE_0:def_4; hence h . r1 > h . r2 by A3, A4, TARSKI:def_1; ::_thesis: verum end; hence h | {x} is decreasing by Th21; ::_thesis: verum end; theorem :: RFUNCT_2:45 for x being set for h being PartFunc of REAL,REAL holds h | {x} is non-decreasing proof let x be set ; ::_thesis: for h being PartFunc of REAL,REAL holds h | {x} is non-decreasing let h be PartFunc of REAL,REAL; ::_thesis: h | {x} is non-decreasing now__::_thesis:_for_r1,_r2_being_Element_of_REAL_st_r1_in_{x}_/\_(dom_h)_&_r2_in_{x}_/\_(dom_h)_&_r1_<_r2_holds_ h_._r1_<=_h_._r2 let r1, r2 be Element of REAL ; ::_thesis: ( r1 in {x} /\ (dom h) & r2 in {x} /\ (dom h) & r1 < r2 implies h . r1 <= h . r2 ) assume that A1: r1 in {x} /\ (dom h) and A2: r2 in {x} /\ (dom h) and r1 < r2 ; ::_thesis: h . r1 <= h . r2 r1 in {x} by A1, XBOOLE_0:def_4; then A3: r1 = x by TARSKI:def_1; r2 in {x} by A2, XBOOLE_0:def_4; hence h . r1 <= h . r2 by A3, TARSKI:def_1; ::_thesis: verum end; hence h | {x} is non-decreasing by Th22; ::_thesis: verum end; theorem :: RFUNCT_2:46 for x being set for h being PartFunc of REAL,REAL holds h | {x} is non-increasing proof let x be set ; ::_thesis: for h being PartFunc of REAL,REAL holds h | {x} is non-increasing let h be PartFunc of REAL,REAL; ::_thesis: h | {x} is non-increasing now__::_thesis:_for_r1,_r2_being_Element_of_REAL_st_r1_in_{x}_/\_(dom_h)_&_r2_in_{x}_/\_(dom_h)_&_r1_<_r2_holds_ h_._r2_<=_h_._r1 let r1, r2 be Element of REAL ; ::_thesis: ( r1 in {x} /\ (dom h) & r2 in {x} /\ (dom h) & r1 < r2 implies h . r2 <= h . r1 ) assume that A1: r1 in {x} /\ (dom h) and A2: r2 in {x} /\ (dom h) and r1 < r2 ; ::_thesis: h . r2 <= h . r1 r1 in {x} by A1, XBOOLE_0:def_4; then A3: r1 = x by TARSKI:def_1; r2 in {x} by A2, XBOOLE_0:def_4; hence h . r2 <= h . r1 by A3, TARSKI:def_1; ::_thesis: verum end; hence h | {x} is non-increasing by Th23; ::_thesis: verum end; theorem :: RFUNCT_2:47 for R being Subset of REAL holds (id R) | R is increasing proof let R be Subset of REAL; ::_thesis: (id R) | R is increasing now__::_thesis:_for_r1,_r2_being_Element_of_REAL_st_r1_in_R_/\_(dom_(id_R))_&_r2_in_R_/\_(dom_(id_R))_&_r1_<_r2_holds_ (id_R)_._r1_<_(id_R)_._r2 let r1, r2 be Element of REAL ; ::_thesis: ( r1 in R /\ (dom (id R)) & r2 in R /\ (dom (id R)) & r1 < r2 implies (id R) . r1 < (id R) . r2 ) assume that A1: r1 in R /\ (dom (id R)) and A2: r2 in R /\ (dom (id R)) and A3: r1 < r2 ; ::_thesis: (id R) . r1 < (id R) . r2 r1 in R by A1, XBOOLE_0:def_4; then A4: (id R) . r1 = r1 by FUNCT_1:18; r2 in R by A2, XBOOLE_0:def_4; hence (id R) . r1 < (id R) . r2 by A3, A4, FUNCT_1:18; ::_thesis: verum end; hence (id R) | R is increasing by Th20; ::_thesis: verum end; theorem :: RFUNCT_2:48 for X being set for h being PartFunc of REAL,REAL st h | X is increasing holds (- h) | X is decreasing proof let X be set ; ::_thesis: for h being PartFunc of REAL,REAL st h | X is increasing holds (- h) | X is decreasing let h be PartFunc of REAL,REAL; ::_thesis: ( h | X is increasing implies (- h) | X is decreasing ) assume h | X is increasing ; ::_thesis: (- h) | X is decreasing then ((- 1) (#) h) | X is decreasing by Th32; hence (- h) | X is decreasing ; ::_thesis: verum end; theorem :: RFUNCT_2:49 for X being set for h being PartFunc of REAL,REAL st h | X is non-decreasing holds (- h) | X is non-increasing proof let X be set ; ::_thesis: for h being PartFunc of REAL,REAL st h | X is non-decreasing holds (- h) | X is non-increasing let h be PartFunc of REAL,REAL; ::_thesis: ( h | X is non-decreasing implies (- h) | X is non-increasing ) assume h | X is non-decreasing ; ::_thesis: (- h) | X is non-increasing then ((- 1) (#) h) | X is non-increasing by Th34; hence (- h) | X is non-increasing ; ::_thesis: verum end; theorem :: RFUNCT_2:50 for p, g being Element of REAL for h being PartFunc of REAL,REAL st ( h | [.p,g.] is increasing or h | [.p,g.] is decreasing ) holds h | [.p,g.] is one-to-one proof let p, g be Element of REAL ; ::_thesis: for h being PartFunc of REAL,REAL st ( h | [.p,g.] is increasing or h | [.p,g.] is decreasing ) holds h | [.p,g.] is one-to-one let h be PartFunc of REAL,REAL; ::_thesis: ( ( h | [.p,g.] is increasing or h | [.p,g.] is decreasing ) implies h | [.p,g.] is one-to-one ) assume A1: ( h | [.p,g.] is increasing or h | [.p,g.] is decreasing ) ; ::_thesis: h | [.p,g.] is one-to-one now__::_thesis:_h_|_[.p,g.]_is_one-to-one percases ( h | [.p,g.] is increasing or h | [.p,g.] is decreasing ) by A1; supposeA2: h | [.p,g.] is increasing ; ::_thesis: h | [.p,g.] is one-to-one now__::_thesis:_for_p1,_p2_being_Element_of_REAL_st_p1_in_dom_(h_|_[.p,g.])_&_p2_in_dom_(h_|_[.p,g.])_&_(h_|_[.p,g.])_._p1_=_(h_|_[.p,g.])_._p2_holds_ p1_=_p2 let p1, p2 be Element of REAL ; ::_thesis: ( p1 in dom (h | [.p,g.]) & p2 in dom (h | [.p,g.]) & (h | [.p,g.]) . p1 = (h | [.p,g.]) . p2 implies p1 = p2 ) assume that A3: p1 in dom (h | [.p,g.]) and A4: p2 in dom (h | [.p,g.]) and A5: (h | [.p,g.]) . p1 = (h | [.p,g.]) . p2 ; ::_thesis: p1 = p2 A6: ( p1 in [.p,g.] /\ (dom h) & p2 in [.p,g.] /\ (dom h) ) by A3, A4, RELAT_1:61; A7: h . p1 = (h | [.p,g.]) . p2 by A3, A5, FUNCT_1:47 .= h . p2 by A4, FUNCT_1:47 ; thus p1 = p2 ::_thesis: verum proof assume A8: p1 <> p2 ; ::_thesis: contradiction now__::_thesis:_contradiction percases ( p1 < p2 or p2 < p1 ) by A8, XXREAL_0:1; suppose p1 < p2 ; ::_thesis: contradiction hence contradiction by A2, A7, A6, Th20; ::_thesis: verum end; suppose p2 < p1 ; ::_thesis: contradiction hence contradiction by A2, A7, A6, Th20; ::_thesis: verum end; end; end; hence contradiction ; ::_thesis: verum end; end; hence h | [.p,g.] is one-to-one by PARTFUN1:8; ::_thesis: verum end; supposeA9: h | [.p,g.] is decreasing ; ::_thesis: h | [.p,g.] is one-to-one now__::_thesis:_for_p1,_p2_being_Element_of_REAL_st_p1_in_dom_(h_|_[.p,g.])_&_p2_in_dom_(h_|_[.p,g.])_&_(h_|_[.p,g.])_._p1_=_(h_|_[.p,g.])_._p2_holds_ p1_=_p2 let p1, p2 be Element of REAL ; ::_thesis: ( p1 in dom (h | [.p,g.]) & p2 in dom (h | [.p,g.]) & (h | [.p,g.]) . p1 = (h | [.p,g.]) . p2 implies p1 = p2 ) assume that A10: p1 in dom (h | [.p,g.]) and A11: p2 in dom (h | [.p,g.]) and A12: (h | [.p,g.]) . p1 = (h | [.p,g.]) . p2 ; ::_thesis: p1 = p2 A13: ( p1 in [.p,g.] /\ (dom h) & p2 in [.p,g.] /\ (dom h) ) by A10, A11, RELAT_1:61; A14: h . p1 = (h | [.p,g.]) . p2 by A10, A12, FUNCT_1:47 .= h . p2 by A11, FUNCT_1:47 ; thus p1 = p2 ::_thesis: verum proof assume A15: p1 <> p2 ; ::_thesis: contradiction now__::_thesis:_contradiction percases ( p1 < p2 or p2 < p1 ) by A15, XXREAL_0:1; suppose p1 < p2 ; ::_thesis: contradiction hence contradiction by A9, A14, A13, Th21; ::_thesis: verum end; suppose p2 < p1 ; ::_thesis: contradiction hence contradiction by A9, A14, A13, Th21; ::_thesis: verum end; end; end; hence contradiction ; ::_thesis: verum end; end; hence h | [.p,g.] is one-to-one by PARTFUN1:8; ::_thesis: verum end; end; end; hence h | [.p,g.] is one-to-one ; ::_thesis: verum end; theorem :: RFUNCT_2:51 for p, g being Element of REAL for h being one-to-one PartFunc of REAL,REAL st h | [.p,g.] is increasing holds ((h | [.p,g.]) ") | (h .: [.p,g.]) is increasing proof let p, g be Element of REAL ; ::_thesis: for h being one-to-one PartFunc of REAL,REAL st h | [.p,g.] is increasing holds ((h | [.p,g.]) ") | (h .: [.p,g.]) is increasing let h be one-to-one PartFunc of REAL,REAL; ::_thesis: ( h | [.p,g.] is increasing implies ((h | [.p,g.]) ") | (h .: [.p,g.]) is increasing ) assume that A1: h | [.p,g.] is increasing and A2: not ((h | [.p,g.]) ") | (h .: [.p,g.]) is increasing ; ::_thesis: contradiction consider y1, y2 being Real such that A3: y1 in (h .: [.p,g.]) /\ (dom ((h | [.p,g.]) ")) and A4: y2 in (h .: [.p,g.]) /\ (dom ((h | [.p,g.]) ")) and A5: y1 < y2 and A6: ((h | [.p,g.]) ") . y1 >= ((h | [.p,g.]) ") . y2 by A2, Th20; y1 in h .: [.p,g.] by A3, XBOOLE_0:def_4; then A7: y1 in rng (h | [.p,g.]) by RELAT_1:115; y2 in h .: [.p,g.] by A4, XBOOLE_0:def_4; then A8: y2 in rng (h | [.p,g.]) by RELAT_1:115; A9: (h | [.p,g.]) | [.p,g.] is increasing by A1; now__::_thesis:_contradiction percases ( ((h | [.p,g.]) ") . y1 = ((h | [.p,g.]) ") . y2 or ((h | [.p,g.]) ") . y1 <> ((h | [.p,g.]) ") . y2 ) ; suppose ((h | [.p,g.]) ") . y1 = ((h | [.p,g.]) ") . y2 ; ::_thesis: contradiction then y1 = (h | [.p,g.]) . (((h | [.p,g.]) ") . y2) by A7, FUNCT_1:35 .= y2 by A8, FUNCT_1:35 ; hence contradiction by A5; ::_thesis: verum end; supposeA10: ((h | [.p,g.]) ") . y1 <> ((h | [.p,g.]) ") . y2 ; ::_thesis: contradiction A11: dom (h | [.p,g.]) = dom ((h | [.p,g.]) | [.p,g.]) by RELAT_1:72 .= [.p,g.] /\ (dom (h | [.p,g.])) by RELAT_1:61 ; A12: ( ((h | [.p,g.]) ") . y2 in dom (h | [.p,g.]) & ((h | [.p,g.]) ") . y1 in dom (h | [.p,g.]) ) by A7, A8, PARTFUN2:60; ((h | [.p,g.]) ") . y2 < ((h | [.p,g.]) ") . y1 by A6, A10, XXREAL_0:1; then (h | [.p,g.]) . (((h | [.p,g.]) ") . y2) < (h | [.p,g.]) . (((h | [.p,g.]) ") . y1) by A9, A12, A11, Th20; then y2 < (h | [.p,g.]) . (((h | [.p,g.]) ") . y1) by A8, FUNCT_1:35; hence contradiction by A5, A7, FUNCT_1:35; ::_thesis: verum end; end; end; hence contradiction ; ::_thesis: verum end; theorem :: RFUNCT_2:52 for p, g being Element of REAL for h being one-to-one PartFunc of REAL,REAL st h | [.p,g.] is decreasing holds ((h | [.p,g.]) ") | (h .: [.p,g.]) is decreasing proof let p, g be Element of REAL ; ::_thesis: for h being one-to-one PartFunc of REAL,REAL st h | [.p,g.] is decreasing holds ((h | [.p,g.]) ") | (h .: [.p,g.]) is decreasing let h be one-to-one PartFunc of REAL,REAL; ::_thesis: ( h | [.p,g.] is decreasing implies ((h | [.p,g.]) ") | (h .: [.p,g.]) is decreasing ) assume that A1: h | [.p,g.] is decreasing and A2: not ((h | [.p,g.]) ") | (h .: [.p,g.]) is decreasing ; ::_thesis: contradiction consider y1, y2 being Real such that A3: y1 in (h .: [.p,g.]) /\ (dom ((h | [.p,g.]) ")) and A4: y2 in (h .: [.p,g.]) /\ (dom ((h | [.p,g.]) ")) and A5: y1 < y2 and A6: ((h | [.p,g.]) ") . y2 >= ((h | [.p,g.]) ") . y1 by A2, Th21; y1 in h .: [.p,g.] by A3, XBOOLE_0:def_4; then A7: y1 in rng (h | [.p,g.]) by RELAT_1:115; y2 in h .: [.p,g.] by A4, XBOOLE_0:def_4; then A8: y2 in rng (h | [.p,g.]) by RELAT_1:115; A9: (h | [.p,g.]) | [.p,g.] is decreasing by A1; now__::_thesis:_contradiction percases ( ((h | [.p,g.]) ") . y1 = ((h | [.p,g.]) ") . y2 or ((h | [.p,g.]) ") . y1 <> ((h | [.p,g.]) ") . y2 ) ; suppose ((h | [.p,g.]) ") . y1 = ((h | [.p,g.]) ") . y2 ; ::_thesis: contradiction then y1 = (h | [.p,g.]) . (((h | [.p,g.]) ") . y2) by A7, FUNCT_1:35 .= y2 by A8, FUNCT_1:35 ; hence contradiction by A5; ::_thesis: verum end; supposeA10: ((h | [.p,g.]) ") . y1 <> ((h | [.p,g.]) ") . y2 ; ::_thesis: contradiction A11: dom (h | [.p,g.]) = dom ((h | [.p,g.]) | [.p,g.]) by RELAT_1:72 .= [.p,g.] /\ (dom (h | [.p,g.])) by RELAT_1:61 ; A12: ( ((h | [.p,g.]) ") . y2 in dom (h | [.p,g.]) & ((h | [.p,g.]) ") . y1 in dom (h | [.p,g.]) ) by A7, A8, PARTFUN2:60; ((h | [.p,g.]) ") . y2 > ((h | [.p,g.]) ") . y1 by A6, A10, XXREAL_0:1; then (h | [.p,g.]) . (((h | [.p,g.]) ") . y2) < (h | [.p,g.]) . (((h | [.p,g.]) ") . y1) by A9, A12, A11, Th21; then y2 < (h | [.p,g.]) . (((h | [.p,g.]) ") . y1) by A8, FUNCT_1:35; hence contradiction by A5, A7, FUNCT_1:35; ::_thesis: verum end; end; end; hence contradiction ; ::_thesis: verum end;