let z be Quaternion; :: 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 Def14;
A4: Im3 z = 0 by A2, Def15;
A5: ex z9 being Complex st
( z = z9 & Rea z = Re z9 ) by A2, Def12;
consider z9 being Complex such that
A6: z = z9 and
A7: Im1 z = Im z9 by A2, Def13;
reconsider Rz = Rea z, Imz = Im1 z as Element of REAL by XREAL_0:def 1;
[*Rz,Imz*] = z9 by A5, A6, A7, Lm8;
hence z = [*(Rea z),(Im1 z),(Im2 z),(Im3 z)*] by A3, A4, A6, Lm3; :: 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 Def13;
A10: ex f being Function of 4,REAL st
( z = f & Rea z = f . 0 ) by A8, Def12;
A11: ex f being Function of 4,REAL st
( z = f & Im2 z = f . 2 ) by A8, Def14;
A12: ex f being Function of 4,REAL st
( z = f & Im3 z = f . 3 ) by A8, Def15;
consider a, b, c, d being Real such that
A13: z = (0,1,2,3) --> (a,b,c,d) by A9, Th15;
reconsider a = a, b = b, c = c, d = d as Element of REAL by XREAL_0:def 1;
A14: z = (0,1,2,3) --> (a,b,c,d) by A13;
A15: Rea z = a by A10, A14, FUNCT_4:142;
A16: Im1 z = b by A9, A14, FUNCT_4:141;
A17: Im2 z = c by A11, A14, FUNCT_4:140;
A18: Im3 z = d by A12, A14, FUNCT_4:139;
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 A19: 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 A14, CARD_1:52, FUNCT_2:8;
( f . 2 <> 0 or f . 3 <> 0 ) by A19;
then ( c <> 0 or d <> 0 ) by A14, FUNCT_4:139, FUNCT_4:140;
hence z = [*(Rea z),(Im1 z),(Im2 z),(Im3 z)*] by A14, A15, A16, A17, A18, Def5; :: thesis: verum
end;
end;