let D be non empty set ; :: thesis: 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 ; :: thesis: for r being Real st 0 < r holds
(abs F) " {r} = F " {(- r),r}
let r be Real; :: thesis: ( 0 < r implies (abs F) " {r} = F " {(- r),r} )
assume A1: 0 < r ; :: thesis: (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} :: according to XBOOLE_0:def 10 :: thesis: F " {(- r),r} c= (abs F) " {r}

proof

let x be set ; :: according to TARSKI:def 3 :: thesis: ( not x in (abs F) " {r} or x in F " {(- r),r} )
assume A3: x in (abs F) " {r} ; :: thesis: x in F " {(- r),r}
then reconsider rr = x as Element of D ;
A4: ( rr in dom (abs F) & (abs F) . rr in {r} ) by A3, FUNCT_1:def 13;
then abs (F . rr) in {r} by VALUED_1:18;
then A5: abs (F . rr) = r by TARSKI:def 1;

now

per cases ( 0 <= F . rr or F . rr < 0 ) ;

case 0 <= F . rr ; :: thesis: x in F " {(- r),r}

then F . rr = r by A5, ABSVALUE:def 1;
then F . rr in {(- r),r} by TARSKI:def 2;
hence x in F " {(- r),r} by A2, A4, FUNCT_1:def 13; :: thesis: verum

end;

case F . rr < 0 ; :: thesis: x in F " {(- r),r}

then - (F . rr) = r by A5, ABSVALUE:def 1;
then F . rr in {(- r),r} by TARSKI:def 2;
hence x in F " {(- r),r} by A2, A4, FUNCT_1:def 13; :: thesis: verum

end;

end;

end;

hence x in F " {(- r),r} ; :: thesis: verum

end;

let x be set ; :: according to TARSKI:def 3 :: thesis: ( not x in F " {(- r),r} or x in (abs F) " {r} )
assume A6: x in F " {(- r),r} ; :: thesis: x in (abs F) " {r}
then reconsider rr = x as Element of D ;
A7: ( rr in dom F & F . rr in {(- r),r} ) by A6, FUNCT_1:def 13;

now

per cases ( F . rr = - r or F . rr = r ) by A7, TARSKI:def 2;

case F . rr = - r ; :: thesis: x in (abs F) " {r}

then r = abs (- (F . rr)) by A1, ABSVALUE:def 1
.= abs (F . rr) by COMPLEX1:138
.= (abs F) . rr by VALUED_1:18 ;
then (abs F) . rr in {r} by TARSKI:def 1;
hence x in (abs F) " {r} by A2, A7, FUNCT_1:def 13; :: thesis: verum

end;

case F . rr = r ; :: thesis: x in (abs F) " {r}

then r = abs (F . rr) by A1, ABSVALUE:def 1
.= (abs F) . rr by VALUED_1:18 ;
then (abs F) . rr in {r} by TARSKI:def 1;
hence x in (abs F) " {r} by A2, A7, FUNCT_1:def 13; :: thesis: verum

end;

end;

end;

hence x in (abs F) " {r} ; :: thesis: verum