let c be Quaternion; :: thesis: for x1 being Real holds (- x1) * c = - (x1 * c)
let x1 be Real; :: thesis: (- 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; :: thesis: verum