let c be Quaternion; for x1 being Real holds (- x1) * c = - (x1 * c)
let x1 be Real; (- x1) * c = - (x1 * c)
consider x, y, w, z being Element of REAL such that
A1:
c = [*x,y,w,z*]
by Lm1;
A2: (- x1) * c =
[*((- x1) * x),((- x1) * y),((- x1) * w),((- x1) * z)*]
by A1, QUATERNI:def 21
.=
[*(- (x1 * x)),(- (x1 * y)),(- (x1 * w)),(- (x1 * z))*]
;
A3:
- (x1 * c) = - [*(x1 * x),(x1 * y),(x1 * w),(x1 * z)*]
by A1, QUATERNI:def 21;
[*(x1 * x),(x1 * y),(x1 * w),(x1 * z)*] + [*(- (x1 * x)),(- (x1 * y)),(- (x1 * w)),(- (x1 * z))*] =
[*((x1 * x) + (- (x1 * x))),((x1 * y) + (- (x1 * y))),((x1 * w) + (- (x1 * w))),((x1 * z) + (- (x1 * z)))*]
by QUATERNI:def 7
.=
[*(In (0,REAL)),(In (0,REAL))*]
by QUATERNI:91
.=
0
by ARYTM_0:def 5
;
hence
(- x1) * c = - (x1 * c)
by A2, A3, QUATERNI:def 8; verum