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 )
A1: dom (max+ F) = dom F by Def10;
assume A2: for d being Element of D st d in dom F holds
F . d >= 0 ; :: thesis: max+ F = F
now :: thesis: for d being Element of D st d in dom F holds
(max+ F) . d = F . d
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 A2;
thus (max+ F) . d = max+ (F . d) by A1, A3, Def10
.= F . d by A4, XXREAL_0:def 10 ; :: thesis: verum
end;
hence max+ F = F by A1, PARTFUN1:5; :: thesis: verum