let z be quaternion number ; :: thesis: z = [*(Rea z),(Im1 z),(Im2 z),(Im3 z)*]
A1: z in QUATERNION by Def2;

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

suppose A2: z in COMPLEX ; :: thesis: z = [*(Rea z),(Im1 z),(Im2 z),(Im3 z)*]

then A3: Im2 z = 0 by Def15;
A4: Im3 z = 0 by A2, Def16;
A5: ex z9 being complex number st
( z = z9 & Rea z = Re z9 ) by A2, Def13;
consider z9 being complex number such that
A6: z = z9 and
A7: Im1 z = Im z9 by A2, Def14;
[*(Rea z),(Im1 z)*] = z9 by A5, A6, A7, Lm9;
hence z = [*(Rea z),(Im1 z),(Im2 z),(Im3 z)*] by A3, A4, A6, Lm4; :: thesis: verum

end;

suppose A8: not z in COMPLEX ; :: thesis: z = [*(Rea z),(Im1 z),(Im2 z),(Im3 z)*]

then A9: ex f being Function of 4,REAL st
( z = f & Im1 z = f . 1 ) by Def14;
A10: ex f being Function of 4,REAL st
( z = f & Rea z = f . 0 ) by A8, Def13;
A11: ex f being Function of 4,REAL st
( z = f & Im2 z = f . 2 ) by A8, Def15;
A12: ex f being Function of 4,REAL st
( z = f & Im3 z = f . 3 ) by A8, Def16;
consider a, b, c, d being Element of REAL such that
A13: z = (0,1,2,3) --> (a,b,c,d) by A9, Th22;
A14: Rea z = a by A10, A13, Lm1, Th3;
A15: Im1 z = b by A9, A13, Lm1, Th3;
A16: Im2 z = c by A11, A13, Lm1, Th3;
A17: Im3 z = d by A12, A13, Lm1, Th3;
z in (Funcs (4,REAL)) \ { x where x is Element of Funcs (4,REAL) : ( x . 2 = 0 & x . 3 = 0 ) } by A1, A8, XBOOLE_0:def 3;
then A18: not z in { x where x is Element of Funcs (4,REAL) : ( x . 2 = 0 & x . 3 = 0 ) } by XBOOLE_0:def 5;
reconsider f = z as Element of Funcs (4,REAL) by A13, CARD_1:52, FUNCT_2:8;
( f . 2 <> 0 or f . 3 <> 0 ) by A18;
then ( c <> 0 or d <> 0 ) by A13, Lm1, Th3;
hence z = [*(Rea z),(Im1 z),(Im2 z),(Im3 z)*] by A13, A14, A15, A16, A17, Def6; :: thesis: verum

end;

end;