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