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 object ; :: 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 ;
(abs F) . rr in {r} by A3, FUNCT_1:def 7;
then |.(F . rr).| in {r} by VALUED_1:18;
then A4: |.(F . rr).| = r by TARSKI:def 1;
A5: rr in dom (abs F) by A3, FUNCT_1:def 7;
now :: thesis: ( ( 0 <= F . rr & x in F " {(- r),r} ) or ( F . rr < 0 & x in F " {(- r),r} ) )
per cases ( 0 <= F . rr or F . rr < 0 ) ;
case 0 <= F . rr ; :: thesis: x in F " {(- r),r}
then F . rr = r by A4, ABSVALUE:def 1;
then F . rr in {(- r),r} by TARSKI:def 2;
hence x in F " {(- r),r} by A2, A5, FUNCT_1:def 7; :: thesis: verum
end;
case F . rr < 0 ; :: thesis: x in F " {(- r),r}
then - (F . rr) = r by A4, ABSVALUE:def 1;
then F . rr in {(- r),r} by TARSKI:def 2;
hence x in F " {(- r),r} by A2, A5, FUNCT_1:def 7; :: thesis: verum
end;
end;
end;
hence x in F " {(- r),r} ; :: thesis: verum
end;
let x be object ; :: 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 by A6, FUNCT_1:def 7;
A8: F . rr in {(- r),r} by A6, FUNCT_1:def 7;
now :: thesis: ( ( F . rr = - r & x in (abs F) " {r} ) or ( F . rr = r & x in (abs F) " {r} ) )
per cases ( F . rr = - r or F . rr = r ) by A8, TARSKI:def 2;
case F . rr = - r ; :: thesis: x in (abs F) " {r}
then r = |.(- (F . rr)).| by A1, ABSVALUE:def 1
.= |.(F . rr).| by COMPLEX1:52
.= (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 7; :: thesis: verum
end;
case F . rr = r ; :: thesis: x in (abs F) " {r}
then r = |.(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 7; :: thesis: verum
end;
end;
end;
hence x in (abs F) " {r} ; :: thesis: verum