let f be complex-valued Function; :: thesis: ( (abs f) " = f " & (- f) " = f " )
now :: thesis: for c being object holds
( ( c in (abs f) " implies c in f " ) & ( c in f " implies c in (abs f) " ) )
let c be object ; :: thesis: ( ( c in (abs f) " implies c in f " ) & ( c in f " implies c in (abs f) " ) )
reconsider cc = c as object ;
thus ( c in (abs f) " implies c in f " ) :: thesis: ( c in f " implies c in (abs f) " )
proof end;
assume A3: c in f " ; :: thesis: c in (abs f) "
then f . c in by FUNCT_1:def 7;
then f . c = 0 by TARSKI:def 1;
then |.(f . cc).| = 0 by ABSVALUE:2;
then (abs f) . c = 0 by VALUED_1:18;
then A4: (abs f) . c in by TARSKI:def 1;
c in dom f by ;
then c in dom (abs f) by VALUED_1:def 11;
hence c in (abs f) " by ; :: thesis: verum
end;
hence (abs f) " = f " by TARSKI:2; :: thesis: (- f) " = f "
now :: thesis: for c being object holds
( ( c in (- f) " implies c in f " ) & ( c in f " implies c in (- f) " ) )
let c be object ; :: thesis: ( ( c in (- f) " implies c in f " ) & ( c in f " implies c in (- f) " ) )
reconsider cc = c as object ;
thus ( c in (- f) " implies c in f " ) :: thesis: ( c in f " implies c in (- f) " )
proof
assume A5: c in (- f) " ; :: thesis: c in f "
then (- f) . c in by FUNCT_1:def 7;
then (- f) . c = 0 by TARSKI:def 1;
then - (- (f . cc)) = - (In (0,REAL)) by VALUED_1:8;
then A6: f . c in by TARSKI:def 1;
c in dom (- f) by ;
then c in dom f by VALUED_1:8;
hence c in f " by ; :: thesis: verum
end;
assume A7: c in f " ; :: thesis: c in (- f) "
then f . c in by FUNCT_1:def 7;
then f . c = 0 by TARSKI:def 1;
then (- f) . c = - (In (0,REAL)) by VALUED_1:8;
then A8: (- f) . c in by TARSKI:def 1;
c in dom f by ;
then c in dom (- f) by VALUED_1:8;
hence c in (- f) " by ; :: thesis: verum
end;
hence (- f) " = f " by TARSKI:2; :: thesis: verum