let D be non empty set ; :: thesis: for F being PartFunc of D,REAL
for d being Element of D holds 0 <= (max- F) . d
let F be PartFunc of D,REAL; :: thesis: for d being Element of D holds 0 <= (max- F) . d
let d be Element of D; :: thesis: 0 <= (max- F) . d
A1: dom F = dom (max- F) by Def11;

per cases ( d in dom F or not d in dom F ) ;

suppose d in dom F ; :: thesis: 0 <= (max- F) . d

then (max- F) . d = max- (F . d) by A1, Def11
.= max ((- (F . d)),0) ;
hence 0 <= (max- F) . d by XXREAL_0:25; :: thesis: verum

end;

suppose not d in dom F ; :: thesis: 0 <= (max- F) . d

hence 0 <= (max- F) . d by A1, FUNCT_1:def 2; :: thesis: verum

end;

end;