let n be Nat; :: thesis: for X being Subset of (TOP-REAL n) holds - X = (-) X

set T = TOP-REAL n;

let X be Subset of (TOP-REAL n); :: thesis: - X = (-) X

for f being complex-valued Function holds

( - f in - X iff f in X )

set T = TOP-REAL n;

let X be Subset of (TOP-REAL n); :: thesis: - X = (-) X

for f being complex-valued Function holds

( - f in - X iff f in X )

proof

hence
- X = (-) X
by Def3; :: thesis: verum
let f be complex-valued Function; :: thesis: ( - f in - X iff f in X )

then reconsider g = f as Element of (TOP-REAL n) ;

- g = (- 1) * g ;

hence - f in - X by A3; :: thesis: verum

end;hereby :: thesis: ( f in X implies - f in - X )

assume A3:
f in X
; :: thesis: - f in - Xassume
- f in - X
; :: thesis: f in X

then consider v being Element of (TOP-REAL n) such that

A1: - f = (- 1) * v and

A2: v in X ;

reconsider g = - f as Element of (TOP-REAL n) by A1;

- g = - (- v) by A1

.= v ;

hence f in X by A2; :: thesis: verum

end;then consider v being Element of (TOP-REAL n) such that

A1: - f = (- 1) * v and

A2: v in X ;

reconsider g = - f as Element of (TOP-REAL n) by A1;

- g = - (- v) by A1

.= v ;

hence f in X by A2; :: thesis: verum

then reconsider g = f as Element of (TOP-REAL n) ;

- g = (- 1) * g ;

hence - f in - X by A3; :: thesis: verum