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 Def11;
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, 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; verum