let x, y, z be quaternion number ; :: 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 Element of 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 Def7;
( Rea x = x1 & Rea y = y1 & Im1 x = x2 & Im1 y = y2 & Im2 x = x3 & Im2 y = y3 & Im3 x = x4 & Im3 y = y4 ) by A2, A3, Th23;
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, Th23; :: thesis: verum