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) )

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

hence
support f = support (- f)
by TARSKI:2; :: thesis: verum
let x be object ; :: thesis: ( x in support f iff 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;hereby :: thesis: ( x in support (- f) implies x in support f )

assume A4:
x in support (- f)
; :: thesis: x in support fassume 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;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

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