let Y be set ; :: thesis: for h being PartFunc of REAL,REAL holds

( h | Y is non-increasing iff for r1, r2 being Real st r1 in Y /\ (dom h) & r2 in Y /\ (dom h) & r1 < r2 holds

h . r2 <= h . r1 )

let h be PartFunc of REAL,REAL; :: thesis: ( h | Y is non-increasing iff for r1, r2 being Real st r1 in Y /\ (dom h) & r2 in Y /\ (dom h) & r1 < r2 holds

h . r2 <= h . r1 )

thus ( h | Y is non-increasing implies for r1, r2 being Real st r1 in Y /\ (dom h) & r2 in Y /\ (dom h) & r1 < r2 holds

h . r2 <= h . r1 ) :: thesis: ( ( for r1, r2 being Real st r1 in Y /\ (dom h) & r2 in Y /\ (dom h) & r1 < r2 holds

h . r2 <= h . r1 ) implies h | Y is non-increasing )

h . r2 <= h . r1 ; :: thesis: h | Y is non-increasing

let r1 be Real; :: according to RFUNCT_2:def 4 :: thesis: for r2 being Real st r1 in dom (h | Y) & r2 in dom (h | Y) & r1 < r2 holds

(h | Y) . r2 <= (h | Y) . r1

let r2 be Real; :: thesis: ( r1 in dom (h | Y) & r2 in dom (h | Y) & r1 < r2 implies (h | Y) . r2 <= (h | Y) . r1 )

assume that

A9: ( r1 in dom (h | Y) & r2 in dom (h | Y) ) and

A10: r1 < r2 ; :: thesis: (h | Y) . r2 <= (h | Y) . r1

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) . r2 <= (h | Y) . r1 by A8, A10, A11; :: thesis: verum

( h | Y is non-increasing iff for r1, r2 being Real st r1 in Y /\ (dom h) & r2 in Y /\ (dom h) & r1 < r2 holds

h . r2 <= h . r1 )

let h be PartFunc of REAL,REAL; :: thesis: ( h | Y is non-increasing iff for r1, r2 being Real st r1 in Y /\ (dom h) & r2 in Y /\ (dom h) & r1 < r2 holds

h . r2 <= h . r1 )

thus ( h | Y is non-increasing implies for r1, r2 being Real st r1 in Y /\ (dom h) & r2 in Y /\ (dom h) & r1 < r2 holds

h . r2 <= h . r1 ) :: thesis: ( ( for r1, r2 being Real st r1 in Y /\ (dom h) & r2 in Y /\ (dom h) & r1 < r2 holds

h . r2 <= h . r1 ) implies h | Y is non-increasing )

proof

assume A8:
for r1, r2 being Real st r1 in Y /\ (dom h) & r2 in Y /\ (dom h) & r1 < r2 holds
assume A1:
h | Y is non-increasing
; :: thesis: for r1, r2 being Real st r1 in Y /\ (dom h) & r2 in Y /\ (dom h) & r1 < r2 holds

h . r2 <= h . r1

let r1, r2 be Real; :: thesis: ( r1 in Y /\ (dom h) & r2 in Y /\ (dom h) & r1 < r2 implies h . r2 <= h . r1 )

assume that

A2: r1 in Y /\ (dom h) and

A3: r2 in Y /\ (dom h) and

A4: r1 < r2 ; :: thesis: h . r2 <= h . r1

A5: r2 in dom (h | Y) by A3, RELAT_1:61;

then A6: (h | Y) . r2 = h . r2 by FUNCT_1:47;

A7: r1 in dom (h | Y) by A2, RELAT_1:61;

then (h | Y) . r1 = h . r1 by FUNCT_1:47;

hence h . r2 <= h . r1 by A1, A4, A7, A5, A6; :: thesis: verum

end;h . r2 <= h . r1

let r1, r2 be Real; :: thesis: ( r1 in Y /\ (dom h) & r2 in Y /\ (dom h) & r1 < r2 implies h . r2 <= h . r1 )

assume that

A2: r1 in Y /\ (dom h) and

A3: r2 in Y /\ (dom h) and

A4: r1 < r2 ; :: thesis: h . r2 <= h . r1

A5: r2 in dom (h | Y) by A3, RELAT_1:61;

then A6: (h | Y) . r2 = h . r2 by FUNCT_1:47;

A7: r1 in dom (h | Y) by A2, RELAT_1:61;

then (h | Y) . r1 = h . r1 by FUNCT_1:47;

hence h . r2 <= h . r1 by A1, A4, A7, A5, A6; :: thesis: verum

h . r2 <= h . r1 ; :: thesis: h | Y is non-increasing

let r1 be Real; :: according to RFUNCT_2:def 4 :: thesis: for r2 being Real st r1 in dom (h | Y) & r2 in dom (h | Y) & r1 < r2 holds

(h | Y) . r2 <= (h | Y) . r1

let r2 be Real; :: thesis: ( r1 in dom (h | Y) & r2 in dom (h | Y) & r1 < r2 implies (h | Y) . r2 <= (h | Y) . r1 )

assume that

A9: ( r1 in dom (h | Y) & r2 in dom (h | Y) ) and

A10: r1 < r2 ; :: thesis: (h | Y) . r2 <= (h | Y) . r1

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) . r2 <= (h | Y) . r1 by A8, A10, A11; :: thesis: verum