x is Element of REAL n by REAL_NS1:def 6;
then reconsider xn = x as Element of (REAL-NS n) by REAL_NS1:def 4;
assume A1: x = a ; :: thesis: - x = - a
then reconsider a1 = a as Element of REAL n by REAL_NS1:def 6;
thus - x = - xn by REAL_NS1:13
.= - a1 by A1, REAL_NS1:4
.= - a ; :: thesis: verum