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

now

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

proof

assume A1: c in (abs f) " {0} ; :: thesis: c in f " {0}
then (abs f) . c in {0} by FUNCT_1:def 13;
then (abs f) . c = 0 by TARSKI:def 1;
then abs (f . c) = 0 by VALUED_1:18;
then f . c = 0 by COMPLEX1:131;
then A2: f . c in {0} by TARSKI:def 1;
c in dom (abs f) by A1, FUNCT_1:def 13;
then c in dom f by VALUED_1:def 11;
hence c in f " {0} by A2, FUNCT_1:def 13; :: thesis: verum

end;

assume A3: c in f " {0} ; :: thesis: c in (abs f) " {0}
then f . c in {0} by FUNCT_1:def 13;
then f . c = 0 by TARSKI:def 1;
then abs (f . c) = 0 by ABSVALUE:7;
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 13;
then c in dom (abs f) by VALUED_1:def 11;
hence c in (abs f) " {0} by A4, FUNCT_1:def 13; :: thesis: verum

end;

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

now

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

proof

assume A5: c in (- f) " {0} ; :: thesis: c in f " {0}
then (- f) . c in {0} by FUNCT_1:def 13;
then (- f) . c = 0 by TARSKI:def 1;
then - (- (f . c)) = - 0 by VALUED_1:8;
then A6: f . c in {0} by TARSKI:def 1;
c in dom (- f) by A5, FUNCT_1:def 13;
then c in dom f by VALUED_1:8;
hence c in f " {0} by A6, FUNCT_1:def 13; :: thesis: verum

end;

assume A7: c in f " {0} ; :: thesis: c in (- f) " {0}
then f . c in {0} by FUNCT_1:def 13;
then f . c = 0 by TARSKI:def 1;
then (- f) . c = - 0 by VALUED_1:8;
then A8: (- f) . c in {0} by TARSKI:def 1;
c in dom f by A7, FUNCT_1:def 13;
then c in dom (- f) by VALUED_1:8;
hence c in (- f) " {0} by A8, FUNCT_1:def 13; :: thesis: verum

end;

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