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 )
proof
let f be complex-valued Function; :: thesis: ( - f in - X iff f in X )
hereby :: thesis: ( f in X implies - f in - X )
assume - 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;
assume A3: f in X ; :: thesis: - 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;
hence - X = (-) X by Def3; :: thesis: verum