let D be non empty set ; for F being PartFunc of D,REAL
for r being Real st 0 < r holds
(abs F) " {r} = F " {(- r),r}
let F be PartFunc of D,REAL; for r being Real st 0 < r holds
(abs F) " {r} = F " {(- r),r}
let r be Real; ( 0 < r implies (abs F) " {r} = F " {(- r),r} )
assume A1:
0 < r
; (abs F) " {r} = F " {(- r),r}
A2:
dom (abs F) = dom F
by VALUED_1:def 11;
thus
(abs F) " {r} c= F " {(- r),r}
XBOOLE_0:def 10 F " {(- r),r} c= (abs F) " {r}
let x be object ; TARSKI:def 3 ( not x in F " {(- r),r} or x in (abs F) " {r} )
assume A6:
x in F " {(- r),r}
; x in (abs F) " {r}
then reconsider rr = x as Element of D ;
A7:
rr in dom F
by A6, FUNCT_1:def 7;
A8:
F . rr in {(- r),r}
by A6, FUNCT_1:def 7;
hence
x in (abs F) " {r}
; verum