let Y be set ; :: thesis: for r being 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 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 ) )

A14: h | Y is increasing and

A15: r < 0 ; :: thesis: (r (#) h) | Y is decreasing

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 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

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

A1: h | Y is increasing and

A2: 0 < r ; :: thesis: (r (#) h) | Y is increasing

end;A1: h | Y is increasing and

A2: 0 < r ; :: thesis: (r (#) h) | Y is 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) . r1 < (r (#) h) . r2

hence
(r (#) h) | Y is increasing
by Th20; :: thesis: verum(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 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;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

proof

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

A12: 0 in REAL by XREAL_0:def 1;

end;A12: 0 in REAL by XREAL_0:def 1;

now :: thesis: for r1 being Element of REAL st r1 in Y /\ (dom (r (#) h)) holds

(r (#) h) . r1 = 0

hence
(r (#) h) | Y is V8()
by PARTFUN2:57, A12; :: thesis: verum(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 A13: r1 in dom (r (#) h) by XBOOLE_0:def 4;

r * (h . r1) = 0 by A11;

hence (r (#) h) . r1 = 0 by A13, VALUED_1:def 5; :: thesis: verum

end;assume r1 in Y /\ (dom (r (#) h)) ; :: thesis: (r (#) h) . r1 = 0

then A13: r1 in dom (r (#) h) by XBOOLE_0:def 4;

r * (h . r1) = 0 by A11;

hence (r (#) h) . r1 = 0 by A13, VALUED_1:def 5; :: thesis: verum

A14: h | Y is increasing and

A15: r < 0 ; :: thesis: (r (#) h) | Y is 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) . r2 < (r (#) h) . r1

hence
(r (#) h) | Y is decreasing
by Th21; :: thesis: verum(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

A16: r1 in Y /\ (dom (r (#) h)) and

A17: r2 in Y /\ (dom (r (#) h)) and

A18: r1 < r2 ; :: thesis: (r (#) h) . r2 < (r (#) h) . r1

A19: r2 in Y by A17, XBOOLE_0:def 4;

A20: r2 in dom (r (#) h) by A17, XBOOLE_0:def 4;

then r2 in dom h by VALUED_1:def 5;

then A21: r2 in Y /\ (dom h) by A19, XBOOLE_0:def 4;

A22: r1 in Y by A16, XBOOLE_0:def 4;

A23: r1 in dom (r (#) h) by A16, XBOOLE_0:def 4;

then r1 in dom h by VALUED_1:def 5;

then r1 in Y /\ (dom h) by A22, XBOOLE_0:def 4;

then h . r1 < h . r2 by A14, A18, A21, Th20;

then r * (h . r2) < r * (h . r1) by A15, XREAL_1:69;

then (r (#) h) . r2 < r * (h . r1) by A20, VALUED_1:def 5;

hence (r (#) h) . r2 < (r (#) h) . r1 by A23, VALUED_1:def 5; :: thesis: verum

end;assume that

A16: r1 in Y /\ (dom (r (#) h)) and

A17: r2 in Y /\ (dom (r (#) h)) and

A18: r1 < r2 ; :: thesis: (r (#) h) . r2 < (r (#) h) . r1

A19: r2 in Y by A17, XBOOLE_0:def 4;

A20: r2 in dom (r (#) h) by A17, XBOOLE_0:def 4;

then r2 in dom h by VALUED_1:def 5;

then A21: r2 in Y /\ (dom h) by A19, XBOOLE_0:def 4;

A22: r1 in Y by A16, XBOOLE_0:def 4;

A23: r1 in dom (r (#) h) by A16, XBOOLE_0:def 4;

then r1 in dom h by VALUED_1:def 5;

then r1 in Y /\ (dom h) by A22, XBOOLE_0:def 4;

then h . r1 < h . r2 by A14, A18, A21, Th20;

then r * (h . r2) < r * (h . r1) by A15, XREAL_1:69;

then (r (#) h) . r2 < r * (h . r1) by A20, VALUED_1:def 5;

hence (r (#) h) . r2 < (r (#) h) . r1 by A23, VALUED_1:def 5; :: thesis: verum