let m, n, x, y, z be quaternion number ; :: thesis: ( 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 ; :: thesis: ( 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 Element of 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 Def7;
consider x1, x2, x3, x4, y1, y2, y3, y4 being Element of 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 Def7;
A7: ( Rea m = m1 & Rea n = n1 & Rea x = x1 & Rea y = y1 & Im1 m = m2 & Im1 n = n2 & Im1 x = x2 & Im1 y = y2 & Im2 m = m3 & Im2 n = n3 & Im2 x = x3 & Im2 y = y3 & Im3 m = m4 & Im3 n = n4 & Im3 x = x4 & Im3 y = y4 ) by A2, A3, A5, A6, Th23;
(m + n) + x = [*((m1 + n1) + x1),((m2 + n2) + x2),((m3 + n3) + x3),((m4 + n4) + x4)*] by A4, A5, Def7;
then z = [*(((m1 + n1) + x1) + y1),(((m2 + n2) + x2) + y2),(((m3 + n3) + x3) + y3),(((m4 + n4) + x4) + y4)*] by A1, A6, Def7;
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, Th23; :: thesis: verum