let x, y, z be Quaternion; :: thesis: ( z = x + y implies ( Rea z = (Rea x) + (Rea y) & Im1 z = (Im1 x) + (Im1 y) & Im2 z = (Im2 x) + (Im2 y) & Im3 z = (Im3 x) + (Im3 y) ) )
assume A1: z = x + y ; :: thesis: ( Rea z = (Rea x) + (Rea y) & Im1 z = (Im1 x) + (Im1 y) & Im2 z = (Im2 x) + (Im2 y) & Im3 z = (Im3 x) + (Im3 y) )
consider x1, x2, x3, x4, y1, y2, y3, y4 being Real such that
A2: x = [*x1,x2,x3,x4*] and
A3: y = [*y1,y2,y3,y4*] and
A4: x + y = [*(x1 + y1),(x2 + y2),(x3 + y3),(x4 + y4)*] by Def6;
A5: Rea x = x1 by A2, Th16;
A6: Rea y = y1 by A3, Th16;
A7: Im1 x = x2 by A2, Th16;
A8: Im1 y = y2 by A3, Th16;
A9: Im2 x = x3 by A2, Th16;
A10: Im2 y = y3 by A3, Th16;
A11: Im3 x = x4 by A2, Th16;
Im3 y = y4 by A3, Th16;
hence ( Rea z = (Rea x) + (Rea y) & Im1 z = (Im1 x) + (Im1 y) & Im2 z = (Im2 x) + (Im2 y) & Im3 z = (Im3 x) + (Im3 y) ) by A1, A4, A5, A6, A7, A8, A9, A10, A11, Th16; :: thesis: verum