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 Def11;
A3: dom F = dom (- F) by VALUED_1:8;

now

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

end;

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