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

A2: now :: thesis: for c being object st c in dom a holds
(- x) . c = - (a . c)

let c be object ; :: thesis: ( c in dom a implies (- x) . c = - (a . c) )
assume c in dom a ; :: thesis: (- x) . c = - (a . c)
reconsider jj = 1 as Element of REAL by XREAL_0:def 1;
thus (- x) . c = ((- jj) * x) . c by RLVECT_1:16
.= (- jj) * (a . c) by A1, VALUED_1:6
.= - (a . c) ; :: thesis: verum

end;

dom (- x) = A by FUNCT_2:92;
hence - x = - a by A1, A2, FUNCT_2:92, VALUED_1:9; :: thesis: verum