let z1, z2 be Quaternion; :: thesis: (z1 + z2) *' = (z1 *') + (z2 *')
A1: z1 *' = [*(Rea z1),(- (Im1 z1)),(- (Im2 z1)),(- (Im3 z1))*] by Th36;
A2: z2 *' = [*(Rea z2),(- (Im1 z2)),(- (Im2 z2)),(- (Im3 z2))*] by Th36;
A3: (z1 + z2) *' = [*(Rea (z1 + z2)),(- (Im1 (z1 + z2))),(- (Im2 (z1 + z2))),(- (Im3 (z1 + z2)))*] by Th36;
(z1 *') + (z2 *') = [*((Rea z1) + (Rea z2)),((- (Im1 z1)) + (- (Im1 z2))),((- (Im2 z1)) + (- (Im2 z2))),((- (Im3 z1)) + (- (Im3 z2)))*] by A1, A2, Def6
.= [*(Rea (z1 + z2)),(- ((Im1 z1) + (Im1 z2))),(- ((Im2 z1) + (Im2 z2))),(- ((Im3 z1) + (Im3 z2)))*] by Th29
.= [*(Rea (z1 + z2)),(- (Im1 (z1 + z2))),(- ((Im2 z1) + (Im2 z2))),(- ((Im3 z1) + (Im3 z2)))*] by Th29
.= [*(Rea (z1 + z2)),(- (Im1 (z1 + z2))),(- (Im2 (z1 + z2))),(- ((Im3 z1) + (Im3 z2)))*] by Th29 ;
hence (z1 + z2) *' = (z1 *') + (z2 *') by A3, Th29; :: thesis: verum