let x, y, z be Quaternion; ( 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
; ( 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; verum