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
.= - (f /. y) by CFUNCT_1:66
.= - (f . x) by ;
then (- f) . x <> 0 by ;
hence x in support (- f) by PRE_POLY:def 7; :: thesis: verum
end;
assume A4: x in support (- f) ; :: thesis:
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
.= - (f /. y) by CFUNCT_1:66
.= - (f . x) by ;
then f . x <> 0 by ;
hence x in support f by PRE_POLY:def 7; :: thesis: verum
end;
hence support f = support (- f) by TARSKI:2; :: thesis: verum