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

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

hence
f | E is nonpositive
by MESFUNC5:9; :: thesis: verum(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;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