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

( 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