let X be non empty set ; :: thesis: for f being nonpositive PartFunc of X,ExtREAL
for E being set holds f | E is nonpositive
let f be nonpositive PartFunc of X,ExtREAL; :: thesis: for E being set holds f | E is nonpositive
let E be set ; :: thesis: f | E is nonpositive

now :: thesis: for x being set st x in dom (f | E) holds
(f | E) . x <= 0

let x be set ; :: thesis: ( x in dom (f | E) implies (f | E) . x <= 0 )
assume x in dom (f | E) ; :: thesis: (f | E) . x <= 0
then (f | E) . x = f . x by FUNCT_1:47;
hence (f | E) . x <= 0 by MESFUNC5:8; :: thesis: verum

end;

hence f | E is nonpositive by MESFUNC5:9; :: thesis: verum