let Y be set ; :: thesis: for r being 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 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 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 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 ;
A7: r2 in dom (r (#) h) by ;
then r2 in dom h by VALUED_1:def 5;
then A8: r2 in Y /\ (dom h) by ;
A9: r1 in Y by ;
A10: r1 in dom (r (#) h) by ;
then r1 in dom h by VALUED_1:def 5;
then r1 in Y /\ (dom h) by ;
then h . r1 <= h . r2 by A1, A5, A8, Th22;
then r * (h . r1) <= (h . r2) * r by ;
then (r (#) h) . r1 <= r * (h . r2) by ;
hence (r (#) h) . r1 <= (r (#) h) . r2 by ; :: 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 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 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 ;
A17: r2 in dom (r (#) h) by ;
then r2 in dom h by VALUED_1:def 5;
then A18: r2 in Y /\ (dom h) by ;
A19: r1 in Y by ;
A20: r1 in dom (r (#) h) by ;
then r1 in dom h by VALUED_1:def 5;
then r1 in Y /\ (dom h) by ;
then h . r1 <= h . r2 by ;
then r * (h . r2) <= r * (h . r1) by ;
then (r (#) h) . r2 <= r * (h . r1) by ;
hence (r (#) h) . r2 <= (r (#) h) . r1 by ; :: thesis: verum
end;
hence (r (#) h) | Y is non-increasing by Th23; :: thesis: verum