let Y be set ; :: thesis: for h being PartFunc of REAL ,REAL st Y misses dom h holds
( h | Y is increasing & h | Y is decreasing & h | Y is non-decreasing & h | Y is non-increasing & h | Y is monotone )
let h be PartFunc of REAL ,REAL ; :: thesis: ( Y misses dom h implies ( h | Y is increasing & h | Y is decreasing & h | Y is non-decreasing & h | Y is non-increasing & h | Y is monotone ) )
assume A1: Y /\ (dom h) = {} ; :: according to XBOOLE_0:def 7 :: thesis: ( h | Y is increasing & h | Y is decreasing & h | Y is non-decreasing & h | Y is non-increasing & h | Y is monotone )
then for r1, r2 being Element of REAL st r1 in Y /\ (dom h) & r2 in Y /\ (dom h) & r1 < r2 holds
h . r1 < h . r2 ;
hence h | Y is increasing by Def2; :: thesis: ( h | Y is decreasing & h | Y is non-decreasing & h | Y is non-increasing & h | Y is monotone )
for r1, r2 being Element of REAL st r1 in Y /\ (dom h) & r2 in Y /\ (dom h) & r1 < r2 holds
h . r2 < h . r1 by A1;
hence h | Y is decreasing by Def3; :: thesis: ( h | Y is non-decreasing & h | Y is non-increasing & h | Y is monotone )
for r1, r2 being Element of REAL st r1 in Y /\ (dom h) & r2 in Y /\ (dom h) & r1 < r2 holds
h . r1 <= h . r2 by A1;
hence h | Y is non-decreasing by Def4; :: thesis: ( h | Y is non-increasing & h | Y is monotone )
for r1, r2 being Element of REAL st r1 in Y /\ (dom h) & r2 in Y /\ (dom h) & r1 < r2 holds
h . r2 <= h . r1 by A1;
hence h | Y is non-increasing by Def5; :: thesis: h | Y is monotone
hence h | Y is monotone ; :: thesis: verum