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 Def10;
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, Def10
.= 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, Def10
.= 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