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 A1: ( h | Y is non-increasing & 0 <= r ) ; :: thesis: (r (#) h) | Y is non-increasing

now

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 A2: ( r1 in Y /\ (dom (r (#) h)) & r2 in Y /\ (dom (r (#) h)) & r1 < r2 ) ; :: thesis: (r (#) h) . r2 <= (r (#) h) . r1
then A3: ( r1 in Y & r1 in dom (r (#) h) & r2 in Y & r2 in dom (r (#) h) ) by XBOOLE_0:def 4;
then ( r1 in Y & r1 in dom h & r2 in Y & r2 in dom h ) by VALUED_1:def 5;
then ( r1 in Y /\ (dom h) & r2 in Y /\ (dom h) ) by XBOOLE_0:def 4;
then h . r2 <= h . r1 by A1, A2, Def5;
then r * (h . r2) <= (h . r1) * r by A1, XREAL_1:66;
then (r (#) h) . r2 <= r * (h . r1) by A3, VALUED_1:def 5;
hence (r (#) h) . r2 <= (r (#) h) . r1 by A3, VALUED_1:def 5; :: thesis: verum

end;

hence (r (#) h) | Y is non-increasing by Def5; :: thesis: verum

end;

assume A4: ( h | Y is non-increasing & r <= 0 ) ; :: thesis: (r (#) h) | Y is non-decreasing

now

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 A5: ( r1 in Y /\ (dom (r (#) h)) & r2 in Y /\ (dom (r (#) h)) & r1 < r2 ) ; :: thesis: (r (#) h) . r1 <= (r (#) h) . r2
then A6: ( r1 in Y & r1 in dom (r (#) h) & r2 in Y & r2 in dom (r (#) h) ) by XBOOLE_0:def 4;
then ( r1 in Y & r1 in dom h & r2 in Y & r2 in dom h ) by VALUED_1:def 5;
then ( r1 in Y /\ (dom h) & r2 in Y /\ (dom h) ) by XBOOLE_0:def 4;
then h . r2 <= h . r1 by A4, A5, Def5;
then r * (h . r1) <= r * (h . r2) by A4, XREAL_1:67;
then (r (#) h) . r1 <= r * (h . r2) by A6, VALUED_1:def 5;
hence (r (#) h) . r1 <= (r (#) h) . r2 by A6, VALUED_1:def 5; :: thesis: verum

end;

hence (r (#) h) | Y is non-decreasing by Def4; :: thesis: verum