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

end;

hence (r (#) h) | Y is increasing by Def2; :: 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 A4: 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 A5: r1 in dom (r (#) h) by XBOOLE_0:def 4;
r * (h . r1) = 0 by A4;
hence (r (#) h) . r1 = 0 by A5, VALUED_1:def 5; :: thesis: verum

end;

hence (r (#) h) | Y is constant by PARTFUN2:76; :: thesis: verum

end;

assume A6: ( h | Y is increasing & 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 A7: ( r1 in Y /\ (dom (r (#) h)) & r2 in Y /\ (dom (r (#) h)) & r1 < r2 ) ; :: thesis: (r (#) h) . r2 < (r (#) h) . r1
then A8: ( 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 . r1 < h . r2 by A6, A7, Def2;
then r * (h . r2) < r * (h . r1) by A6, XREAL_1:71;
then (r (#) h) . r2 < r * (h . r1) by A8, VALUED_1:def 5;
hence (r (#) h) . r2 < (r (#) h) . r1 by A8, VALUED_1:def 5; :: thesis: verum

end;

hence (r (#) h) | Y is decreasing by Def3; :: thesis: verum