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