let m, n, x, y, z be Quaternion; ( z = ((m + n) + x) + y implies ( Rea z = (((Rea m) + (Rea n)) + (Rea x)) + (Rea y) & Im1 z = (((Im1 m) + (Im1 n)) + (Im1 x)) + (Im1 y) & Im2 z = (((Im2 m) + (Im2 n)) + (Im2 x)) + (Im2 y) & Im3 z = (((Im3 m) + (Im3 n)) + (Im3 x)) + (Im3 y) ) )
assume A1:
z = ((m + n) + x) + y
; ( Rea z = (((Rea m) + (Rea n)) + (Rea x)) + (Rea y) & Im1 z = (((Im1 m) + (Im1 n)) + (Im1 x)) + (Im1 y) & Im2 z = (((Im2 m) + (Im2 n)) + (Im2 x)) + (Im2 y) & Im3 z = (((Im3 m) + (Im3 n)) + (Im3 x)) + (Im3 y) )
consider m1, m2, m3, m4, n1, n2, n3, n4 being Real such that
A2:
m = [*m1,m2,m3,m4*]
and
A3:
n = [*n1,n2,n3,n4*]
and
A4:
m + n = [*(m1 + n1),(m2 + n2),(m3 + n3),(m4 + n4)*]
by Def6;
consider x1, x2, x3, x4, y1, y2, y3, y4 being Real such that
A5:
x = [*x1,x2,x3,x4*]
and
A6:
y = [*y1,y2,y3,y4*]
and
x + y = [*(x1 + y1),(x2 + y2),(x3 + y3),(x4 + y4)*]
by Def6;
A7:
Rea m = m1
by A2, Th16;
A8:
Rea n = n1
by A3, Th16;
A9:
Rea x = x1
by A5, Th16;
A10:
Rea y = y1
by A6, Th16;
A11:
Im1 m = m2
by A2, Th16;
A12:
Im1 n = n2
by A3, Th16;
A13:
Im1 x = x2
by A5, Th16;
A14:
Im1 y = y2
by A6, Th16;
A15:
Im2 m = m3
by A2, Th16;
A16:
Im2 n = n3
by A3, Th16;
A17:
Im2 x = x3
by A5, Th16;
A18:
Im2 y = y3
by A6, Th16;
A19:
Im3 m = m4
by A2, Th16;
A20:
Im3 n = n4
by A3, Th16;
A21:
Im3 x = x4
by A5, Th16;
A22:
Im3 y = y4
by A6, Th16;
(m + n) + x = [*((m1 + n1) + x1),((m2 + n2) + x2),((m3 + n3) + x3),((m4 + n4) + x4)*]
by A4, A5, Def6;
then
z = [*(((m1 + n1) + x1) + y1),(((m2 + n2) + x2) + y2),(((m3 + n3) + x3) + y3),(((m4 + n4) + x4) + y4)*]
by A1, A6, Def6;
hence
( Rea z = (((Rea m) + (Rea n)) + (Rea x)) + (Rea y) & Im1 z = (((Im1 m) + (Im1 n)) + (Im1 x)) + (Im1 y) & Im2 z = (((Im2 m) + (Im2 n)) + (Im2 x)) + (Im2 y) & Im3 z = (((Im3 m) + (Im3 n)) + (Im3 x)) + (Im3 y) )
by A7, A8, A9, A10, A11, A12, A13, A14, A15, A16, A17, A18, A19, A20, A21, A22, Th16; verum