assume A1: x = a ; :: thesis: - x = - a
a2: ( dom (- x) = A & dom x = A ) by FUNCT_2:169;

now

let c be set ; :: thesis: ( c in dom a implies (- x) . c = - (a . c) )
assume c in dom a ; :: thesis: (- x) . c = - (a . c)
thus (- x) . c = ((- 1) * x) . c by RLVECT_1:29
.= (- 1) * (a . c) by A1, VALUED_1:6
.= - (a . c) ; :: thesis: verum

end;

hence - x = - a by a2, A1, VALUED_1:9; :: thesis: verum