let n be Nat; :: thesis: for x being VECTOR of (REAL-NS n)

for a being Element of REAL n st x = a holds

- x = - a

let x be VECTOR of (REAL-NS n); :: thesis: for a being Element of REAL n st x = a holds

- x = - a

let a be Element of REAL n; :: thesis: ( x = a implies - x = - a )

assume A1: x = a ; :: thesis: - x = - a

reconsider a1 = a as Element of n -tuples_on REAL by EUCLID:def 1;

- x = (- 1) * x by RLVECT_1:16

.= - a1 by A1, Th3 ;

hence - x = - a ; :: thesis: verum

for a being Element of REAL n st x = a holds

- x = - a

let x be VECTOR of (REAL-NS n); :: thesis: for a being Element of REAL n st x = a holds

- x = - a

let a be Element of REAL n; :: thesis: ( x = a implies - x = - a )

assume A1: x = a ; :: thesis: - x = - a

reconsider a1 = a as Element of n -tuples_on REAL by EUCLID:def 1;

- x = (- 1) * x by RLVECT_1:16

.= - a1 by A1, Th3 ;

hence - x = - a ; :: thesis: verum