let g be Quaternion; :: thesis: 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*] ; :: thesis: verum