let n be non empty Nat; :: thesis: for xv being Element of (n -VectSp_over F_Real)
for xt being Element of (TOP-REAL n) st xv = xt holds
- xv = - xt
let xv be Element of (n -VectSp_over F_Real); :: thesis: for xt being Element of (TOP-REAL n) st xv = xt holds
- xv = - xt
let xt be Element of (TOP-REAL n); :: thesis: ( xv = xt implies - xv = - xt )
assume A1: xv = xt ; :: thesis: - xv = - xt
thus - xv = (- (1. F_Real)) * xv by VECTSP_1:14
.= (- 1) * xt by A1, Th54
.= - xt by RLVECT_1:16 ; :: thesis: verum