let g be Element of QUATERNION ; :: thesis: ex r, s, t, u being Element of REAL st g = [*r,s,t,u*]

per cases ( g in COMPLEX or not g in COMPLEX ) ;

suppose g in COMPLEX ; :: thesis: ex r, s, t, u being Element of REAL st g = [*r,s,t,u*]

then consider r, s being Element of REAL such that
A1: g = [*r,s*] by ARYTM_0:11;
take r ; :: thesis: ex s, t, u being Element of REAL st g = [*r,s,t,u*]
take s ; :: thesis: ex t, u being Element of REAL st g = [*r,s,t,u*]
take 0 ; :: thesis: ex u being Element of REAL st g = [*r,s,0 ,u*]
take 0 ; :: thesis: g = [*r,s,0 ,0 *]
thus g = [*r,s,0 ,0 *] by A1, Def6; :: thesis: verum

end;

suppose not g in COMPLEX ; :: thesis: ex r, s, t, u being Element of REAL st g = [*r,s,t,u*]

then A2: g in (Funcs 4,REAL ) \ { x where x is Element of Funcs 4,REAL : ( x . 2 = 0 & x . 3 = 0 ) } by XBOOLE_0:def 3;
then consider f being Function such that
A3: g = f and
A4: dom f = 4 and
A5: rng f c= REAL by FUNCT_2:def 2;
( 0 in 4 & 1 in 4 & 2 in 4 & 3 in 4 ) by CARD_1:90, ENUMSET1:def 2;
then ( f . 0 in rng f & f . 1 in rng f & f . 2 in rng f & f . 3 in rng f ) by A4, FUNCT_1:12;
then reconsider r = f . 0 , s = f . 1, t = f . 2, u = f . 3 as Element of REAL by A5;
A6: g = 0 ,1,2,3 --> r,s,t,u by A3, A4, Th6, CARD_1:90;
take r ; :: thesis: ex s, t, u being Element of REAL st g = [*r,s,t,u*]
take s ; :: thesis: ex t, u being Element of REAL st g = [*r,s,t,u*]
take t ; :: thesis: ex u being Element of REAL st g = [*r,s,t,u*]
take u ; :: thesis: g = [*r,s,t,u*]

now

assume ( t = 0 & u = 0 ) ; :: thesis: contradiction
then ( (0 ,1,2,3 --> r,s,t,u) . 2 = 0 & (0 ,1,2,3 --> r,s,t,u) . 3 = 0 ) by Lm1, Th3;
then g in { x where x is Element of Funcs 4,REAL : ( x . 2 = 0 & x . 3 = 0 ) } by A2, A6;
hence contradiction by A2, XBOOLE_0:def 5; :: thesis: verum

end;

hence g = [*r,s,t,u*] by A6, Def6; :: thesis: verum

end;

end;