let g be Quaternion; ex r, s, t, u being Element of REAL st g = [*r,s,t,u*]
consider r, s, t, u being Real such that
A1:
g = [*r,s,t,u*]
by QUATERNI:7;
reconsider r = r, s = s, t = t, u = u as Element of REAL by XREAL_0:def 1;
g = [*r,s,t,u*]
by A1;
hence
ex r, s, t, u being Element of REAL st g = [*r,s,t,u*]
; verum