let f be complex-valued Function; :: thesis: ( (abs f) " {0} = f " {0} & (- f) " {0} = f " {0} )

now :: thesis: for c being object holds

( ( c in (abs f) " {0} implies c in f " {0} ) & ( c in f " {0} implies c in (abs f) " {0} ) )

hence
(abs f) " {0} = f " {0}
by TARSKI:2; :: thesis: (- f) " {0} = f " {0}( ( c in (abs f) " {0} implies c in f " {0} ) & ( c in f " {0} implies c in (abs f) " {0} ) )

let c be object ; :: thesis: ( ( c in (abs f) " {0} implies c in f " {0} ) & ( c in f " {0} implies c in (abs f) " {0} ) )

reconsider cc = c as object ;

thus ( c in (abs f) " {0} implies c in f " {0} ) :: thesis: ( c in f " {0} implies c in (abs f) " {0} )

then f . c in {0} 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 {0} by TARSKI:def 1;

c in dom f by A3, FUNCT_1:def 7;

then c in dom (abs f) by VALUED_1:def 11;

hence c in (abs f) " {0} by A4, FUNCT_1:def 7; :: thesis: verum

end;reconsider cc = c as object ;

thus ( c in (abs f) " {0} implies c in f " {0} ) :: thesis: ( c in f " {0} implies c in (abs f) " {0} )

proof

assume A3:
c in f " {0}
; :: thesis: c in (abs f) " {0}
assume A1:
c in (abs f) " {0}
; :: thesis: c in f " {0}

then (abs f) . c in {0} by FUNCT_1:def 7;

then (abs f) . c = 0 by TARSKI:def 1;

then |.(f . cc).| = 0 by VALUED_1:18;

then f . c = 0 by COMPLEX1:45;

then A2: f . c in {0} by TARSKI:def 1;

c in dom (abs f) by A1, FUNCT_1:def 7;

then c in dom f by VALUED_1:def 11;

hence c in f " {0} by A2, FUNCT_1:def 7; :: thesis: verum

end;then (abs f) . c in {0} by FUNCT_1:def 7;

then (abs f) . c = 0 by TARSKI:def 1;

then |.(f . cc).| = 0 by VALUED_1:18;

then f . c = 0 by COMPLEX1:45;

then A2: f . c in {0} by TARSKI:def 1;

c in dom (abs f) by A1, FUNCT_1:def 7;

then c in dom f by VALUED_1:def 11;

hence c in f " {0} by A2, FUNCT_1:def 7; :: thesis: verum

then f . c in {0} 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 {0} by TARSKI:def 1;

c in dom f by A3, FUNCT_1:def 7;

then c in dom (abs f) by VALUED_1:def 11;

hence c in (abs f) " {0} by A4, FUNCT_1:def 7; :: thesis: verum

now :: thesis: for c being object holds

( ( c in (- f) " {0} implies c in f " {0} ) & ( c in f " {0} implies c in (- f) " {0} ) )

hence
(- f) " {0} = f " {0}
by TARSKI:2; :: thesis: verum( ( c in (- f) " {0} implies c in f " {0} ) & ( c in f " {0} implies c in (- f) " {0} ) )

let c be object ; :: thesis: ( ( c in (- f) " {0} implies c in f " {0} ) & ( c in f " {0} implies c in (- f) " {0} ) )

reconsider cc = c as object ;

thus ( c in (- f) " {0} implies c in f " {0} ) :: thesis: ( c in f " {0} implies c in (- f) " {0} )

then f . c in {0} 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 {0} by TARSKI:def 1;

c in dom f by A7, FUNCT_1:def 7;

then c in dom (- f) by VALUED_1:8;

hence c in (- f) " {0} by A8, FUNCT_1:def 7; :: thesis: verum

end;reconsider cc = c as object ;

thus ( c in (- f) " {0} implies c in f " {0} ) :: thesis: ( c in f " {0} implies c in (- f) " {0} )

proof

assume A7:
c in f " {0}
; :: thesis: c in (- f) " {0}
assume A5:
c in (- f) " {0}
; :: thesis: c in f " {0}

then (- f) . c in {0} 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 {0} by TARSKI:def 1;

c in dom (- f) by A5, FUNCT_1:def 7;

then c in dom f by VALUED_1:8;

hence c in f " {0} by A6, FUNCT_1:def 7; :: thesis: verum

end;then (- f) . c in {0} 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 {0} by TARSKI:def 1;

c in dom (- f) by A5, FUNCT_1:def 7;

then c in dom f by VALUED_1:8;

hence c in f " {0} by A6, FUNCT_1:def 7; :: thesis: verum

then f . c in {0} 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 {0} by TARSKI:def 1;

c in dom f by A7, FUNCT_1:def 7;

then c in dom (- f) by VALUED_1:8;

hence c in (- f) " {0} by A8, FUNCT_1:def 7; :: thesis: verum