let D be non empty set ; :: thesis: for F being PartFunc of D,REAL
for r being Real st 0 < r holds
F " {(- r)} = (max- F) " {r}
let F be PartFunc of D,REAL; :: thesis: for r being Real st 0 < r holds
F " {(- r)} = (max- F) " {r}
let r be Real; :: thesis: ( 0 < r implies F " {(- r)} = (max- F) " {r} )
A1: dom (max- F) = dom F by Def11;
assume A2: 0 < r ; :: thesis: F " {(- r)} = (max- F) " {r}
thus F " {(- r)} c= (max- F) " {r} :: according to XBOOLE_0:def 10 :: thesis: (max- F) " {r} c= F " {(- r)}

proof

let x be object ; :: according to TARSKI:def 3 :: thesis: ( not x in F " {(- r)} or x in (max- F) " {r} )
assume A3: x in F " {(- r)} ; :: thesis: x in (max- F) " {r}
then reconsider d = x as Element of D ;
F . d in {(- r)} by A3, FUNCT_1:def 7;
then A4: F . d = - r by TARSKI:def 1;
A5: d in dom F by A3, FUNCT_1:def 7;
then (max- F) . d = max- (F . d) by A1, Def11
.= r by A2, A4, XXREAL_0:def 10 ;
then (max- F) . d in {r} by TARSKI:def 1;
hence x in (max- F) " {r} by A1, A5, FUNCT_1:def 7; :: thesis: verum

end;

let x be object ; :: according to TARSKI:def 3 :: thesis: ( not x in (max- F) " {r} or x in F " {(- r)} )
assume A6: x in (max- F) " {r} ; :: thesis: x in F " {(- r)}
then reconsider d = x as Element of D ;
(max- F) . d in {r} by A6, FUNCT_1:def 7;
then A7: (max- F) . d = r by TARSKI:def 1;
A8: d in dom F by A1, A6, FUNCT_1:def 7;
then (max- F) . d = max- (F . d) by A1, Def11
.= max ((- (F . d)),0) ;
then - (F . d) = r by A2, A7, XXREAL_0:16;
then F . d in {(- r)} by TARSKI:def 1;
hence x in F " {(- r)} by A8, FUNCT_1:def 7; :: thesis: verum