let c be Quaternion; :: thesis: - c = (- 1q) * c
consider x, y, w, z being Element of REAL such that
A1: c = [*x,y,w,z*] by Lm1;
A2: c + [*(- x),(- y),(- w),(- z)*] = [*(x + (- x)),(y + (- y)),(w + (- w)),(z + (- z))*] by A1, QUATERNI:def 7
.= [*(In (0,REAL)),(In (0,REAL))*] by QUATERNI:91
.= 0 by ARYTM_0:def 5 ;
1q = [*jj,(In (0,REAL))*] by ARYTM_0:def 5
.= [*1,0,0,0*] by QUATERNI:91 ;
then 1q + [*(- 1),0,0,0*] = [*(jj + (- jj)),(0 + 0),(0 + 0),(0 + 0)*] by QUATERNI:def 7
.= [*(In (0,REAL)),(In (0,REAL))*] by QUATERNI:91
.= 0 by ARYTM_0:def 5 ;
then (- 1q) * c = [*(- 1),0,0,0*] * [*x,y,w,z*] by A1, QUATERNI:def 8
.= [*(((((- 1) * x) - (0 * y)) - (0 * w)) - (0 * z)),(((((- 1) * y) + (0 * x)) + (0 * z)) - (0 * w)),(((((- 1) * w) + (x * 0)) + (y * 0)) - (z * 0)),(((((- jj) * z) + (0 * x)) + (0 * w)) - (0 * y))*] by QUATERNI:def 10 ;
hence - c = (- 1q) * c by A2, QUATERNI:def 8; :: thesis: verum