[*1,0,0,0*] = [*jj,zz*] by Lm3;
hence 1 is quaternion number by ARYTM_0:def 5; :: thesis: verum