let Y be set ; for h being PartFunc of REAL,REAL holds
( h | Y is non-decreasing iff for r1, r2 being Real st r1 in Y /\ (dom h) & r2 in Y /\ (dom h) & r1 < r2 holds
h . r1 <= h . r2 )
let h be PartFunc of REAL,REAL; ( h | Y is non-decreasing iff for r1, r2 being Real st r1 in Y /\ (dom h) & r2 in Y /\ (dom h) & r1 < r2 holds
h . r1 <= h . r2 )
thus
( h | Y is non-decreasing implies for r1, r2 being Real st r1 in Y /\ (dom h) & r2 in Y /\ (dom h) & r1 < r2 holds
h . r1 <= h . r2 )
( ( for r1, r2 being Real st r1 in Y /\ (dom h) & r2 in Y /\ (dom h) & r1 < r2 holds
h . r1 <= h . r2 ) implies h | Y is non-decreasing )
assume A8:
for r1, r2 being Real st r1 in Y /\ (dom h) & r2 in Y /\ (dom h) & r1 < r2 holds
h . r1 <= h . r2
; h | Y is non-decreasing
let r1 be Real; RFUNCT_2:def 3 for r2 being Real st r1 in dom (h | Y) & r2 in dom (h | Y) & r1 < r2 holds
(h | Y) . r1 <= (h | Y) . r2
let r2 be Real; ( r1 in dom (h | Y) & r2 in dom (h | Y) & r1 < r2 implies (h | Y) . r1 <= (h | Y) . r2 )
assume that
A9:
( r1 in dom (h | Y) & r2 in dom (h | Y) )
and
A10:
r1 < r2
; (h | Y) . r1 <= (h | Y) . r2
A11:
( (h | Y) . r1 = h . r1 & (h | Y) . r2 = h . r2 )
by A9, FUNCT_1:47;
( r1 in Y /\ (dom h) & r2 in Y /\ (dom h) )
by A9, RELAT_1:61;
hence
(h | Y) . r1 <= (h | Y) . r2
by A8, A10, A11; verum