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 Def11;
assume A2: for d being Element of D st d in dom F holds
F . d <= 0 ; :: thesis: max- F = - F

A3: 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 A4: d in dom F ; :: thesis: (max- F) . d = (- F) . d
then A5: F . d <= 0 by A2;
thus (max- F) . d = max- (F . d) by A1, A4, Def11
.= - (F . d) by A5, XXREAL_0:def 10
.= (- F) . d by VALUED_1:8 ; :: thesis: verum

end;

dom F = dom (- F) by VALUED_1:8;
hence max- F = - F by A1, A3, PARTFUN1:5; :: thesis: verum