assume A1: x = a ; :: thesis: - x = - a
then reconsider a2 = a as Element of REAL n ;
reconsider a1 = a2 as Element of n -tuples_on REAL ;
- x = (- 1) * x by RLVECT_1:29
.= - a1 by A1 ;
hence - x = - a ; :: thesis: verum