let X, Y be set ; :: thesis: for h being PartFunc of REAL,REAL st X c= Y & h | Y is decreasing holds

h | X is decreasing

let h be PartFunc of REAL,REAL; :: thesis: ( X c= Y & h | Y is decreasing implies h | X is decreasing )

assume that

A1: X c= Y and

A2: h | Y is decreasing ; :: thesis: h | X is decreasing

h | X is decreasing

let h be PartFunc of REAL,REAL; :: thesis: ( X c= Y & h | Y is decreasing implies h | X is decreasing )

assume that

A1: X c= Y and

A2: h | Y is decreasing ; :: thesis: h | X is decreasing

now :: thesis: for r1, r2 being Real st r1 in X /\ (dom h) & r2 in X /\ (dom h) & r1 < r2 holds

h . r1 > h . r2

hence
h | X is decreasing
by Th21; :: thesis: verumh . r1 > h . r2

A3:
X /\ (dom h) c= Y /\ (dom h)
by A1, XBOOLE_1:26;

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

assume ( r1 in X /\ (dom h) & r2 in X /\ (dom h) & r1 < r2 ) ; :: thesis: h . r1 > h . r2

hence h . r1 > h . r2 by A2, A3, Th21; :: thesis: verum

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

assume ( r1 in X /\ (dom h) & r2 in X /\ (dom h) & r1 < r2 ) ; :: thesis: h . r1 > h . r2

hence h . r1 > h . r2 by A2, A3, Th21; :: thesis: verum