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 constant ) & ( 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 constant ) & ( 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 constant ) & ( 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 constant ) & ( 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

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, Th43;
then r * (h . r1) < r * (h . r2) by A2, XREAL_1:70;
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 Th43; :: thesis: verum

end;

thus ( r = 0 implies (r (#) h) | Y is constant ) :: thesis: ( h | Y is increasing & r < 0 implies (r (#) h) | Y is decreasing )

proof

assume A11: r = 0 ; :: thesis: (r (#) h) | Y is constant

now

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 constant by PARTFUN2:76; :: thesis: verum

end;

assume that
A13: h | Y is increasing and
A14: r < 0 ; :: thesis: (r (#) h) | Y is 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) . 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, Th43;
then r * (h . r2) < r * (h . r1) by A14, XREAL_1:71;
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 Th44; :: thesis: verum