theorem Th57: :: REAL_NS2:57

for n being non empty Nat
for xv being Element of (n -VectSp_over F_Real)
for xt being Element of (TOP-REAL n) st xv = xt holds
- xv = - xt