let X, Y be set ; :: thesis: for h being PartFunc of REAL ,REAL st X c= Y & h | Y is non-increasing holds
h | X is non-increasing
let h be PartFunc of REAL ,REAL ; :: thesis: ( X c= Y & h | Y is non-increasing implies h | X is non-increasing )
assume A1: ( X c= Y & h | Y is non-increasing ) ; :: thesis: h | X is non-increasing

now

let r1, r2 be Element of REAL ; :: thesis: ( r1 in X /\ (dom h) & r2 in X /\ (dom h) & r1 < r2 implies h . r1 >= h . r2 )
assume A2: ( r1 in X /\ (dom h) & r2 in X /\ (dom h) & r1 < r2 ) ; :: thesis: h . r1 >= h . r2
X /\ (dom h) c= Y /\ (dom h) by A1, XBOOLE_1:26;
hence h . r1 >= h . r2 by A1, A2, Def5; :: thesis: verum

end;

hence h | X is non-increasing by Def5; :: thesis: verum