let D be non empty set ; :: thesis: for F being PartFunc of D,REAL st ( for d being Element of D st d in dom F holds
F . d >= 0 ) holds
max+ F = F
let F be PartFunc of D,REAL ; :: thesis: ( ( for d being Element of D st d in dom F holds
F . d >= 0 ) implies max+ F = F )
assume A1: for d being Element of D st d in dom F holds
F . d >= 0 ; :: thesis: max+ F = F
A2: dom (max+ F) = dom F by Def10;

now

let d be Element of D; :: thesis: ( d in dom F implies (max+ F) . d = F . d )
assume A3: d in dom F ; :: thesis: (max+ F) . d = F . d
then A4: F . d >= 0 by A1;
thus (max+ F) . d = max+ (F . d) by A2, A3, Def10
.= F . d by A4, XXREAL_0:def 10 ; :: thesis: verum

end;

hence max+ F = F by A2, PARTFUN1:34; :: thesis: verum