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