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