let g be quaternion number ; :: thesis: ex r, s, t, u being Element of REAL st g = [*r,s,t,u*]
g in QUATERNION by QUATERNI:def 2;
hence ex r, s, t, u being Element of REAL st g = [*r,s,t,u*] by QUATERNI:7; :: thesis: verum