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