let A be set ; :: thesis: for f being Function of A,COMPLEX holds support f = support (- f)
let f be Function of A,COMPLEX; :: thesis: support f = support (- f)
for x being object holds
( x in support f iff x in support (- f) )

proof

let x be object ; :: thesis: ( x in support f iff x in support (- f) )

hereby :: thesis: ( x in support (- f) implies x in support f )

assume A1: x in support f ; :: thesis: x in support (- f)
then A2: x in dom f ;
then A3: x in dom (- f) by CFUNCT_1:5;
reconsider A = A as non empty set by A1;
reconsider y = x as Element of A by A2;
(- f) . x = (- f) /. y by A3, PARTFUN1:def 6
.= - (f /. y) by CFUNCT_1:66
.= - (f . x) by A1, PARTFUN1:def 6 ;
then (- f) . x <> 0 by A1, PRE_POLY:def 7;
hence x in support (- f) by PRE_POLY:def 7; :: thesis: verum

end;

assume A4: x in support (- f) ; :: thesis: x in support f
then A5: x in dom (- f) ;
then A6: x in dom f by CFUNCT_1:5;
reconsider A = A as non empty set by A4;
reconsider y = x as Element of A by A5;
(- f) . x = (- f) /. y by A4, PARTFUN1:def 6
.= - (f /. y) by CFUNCT_1:66
.= - (f . x) by A6, PARTFUN1:def 6 ;
then f . x <> 0 by A4, PRE_POLY:def 7;
hence x in support f by PRE_POLY:def 7; :: thesis: verum

end;

hence support f = support (- f) by TARSKI:2; :: thesis: verum