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