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

end;

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

end;

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

end;

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