let D be non empty set ; 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; for r being Real st 0 < r holds
F " {r} = (max+ F) " {r}
let r be Real; ( 0 < r implies F " {r} = (max+ F) " {r} )
A1:
dom (max+ F) = dom F
by Def10;
assume A2:
0 < r
; F " {r} = (max+ F) " {r}
thus
F " {r} c= (max+ F) " {r}
XBOOLE_0:def 10 (max+ F) " {r} c= F " {r}
let x be object ; TARSKI:def 3 ( not x in (max+ F) " {r} or x in F " {r} )
assume A6:
x in (max+ F) " {r}
; 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; verum