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 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 Th20; :: thesis: ( h | Y is decreasing & h | Y is non-decreasing & h | Y is non-increasing & h | Y is monotone )
for r1, r2 being 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 Th21; :: thesis: ( h | Y is non-decreasing & h | Y is non-increasing & h | Y is monotone )
for r1, r2 being 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 Th22; :: thesis: ( h | Y is non-increasing & h | Y is monotone )
A2: for r1, r2 being 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 Th23; :: thesis: h | Y is monotone
thus h | Y is monotone by A2, Th23; :: thesis: verum