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} )
assume A1: 0 < r ; :: thesis: F " {(- r)} = (max- F) " {r}
A2: dom (max- F) = dom F by Def11;
thus F " {(- r)} c= (max- F) " {r} :: according to XBOOLE_0:def 10 :: thesis: (max- F) " {r} c= F " {(- r)}

proof

let x be set ; :: 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 ;
A4: ( d in dom F & F . d in {(- r)} ) by A3, FUNCT_1:def 13;
then A5: F . d = - r by TARSKI:def 1;
(max- F) . d = max- (F . d) by A2, A4, Def11
.= r by A1, A5, XXREAL_0:def 10 ;
then (max- F) . d in {r} by TARSKI:def 1;
hence x in (max- F) " {r} by A2, A4, FUNCT_1:def 13; :: thesis: verum

end;

let x be set ; :: 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 ;
A7: ( d in dom F & (max- F) . d in {r} ) by A2, A6, FUNCT_1:def 13;
then A8: (max- F) . d = r by TARSKI:def 1;
(max- F) . d = max- (F . d) by A2, A7, Def11
.= max (- (F . d)),0 ;
then - (F . d) = r by A1, A8, XXREAL_0:16;
then F . d in {(- r)} by TARSKI:def 1;
hence x in F " {(- r)} by A7, FUNCT_1:def 13; :: thesis: verum