let z1, z2 be quaternion number ; :: thesis: (z1 + z2) *' = (z1 *' ) + (z2 *' )
A1: ( z1 *' = [*(Rea z1),(- (Im1 z1)),(- (Im2 z1)),(- (Im3 z1))*] & z2 *' = [*(Rea z2),(- (Im1 z2)),(- (Im2 z2)),(- (Im3 z2))*] & (z1 + z2) *' = [*(Rea (z1 + z2)),(- (Im1 (z1 + z2))),(- (Im2 (z1 + z2))),(- (Im3 (z1 + z2)))*] ) by Th43;
then (z1 *' ) + (z2 *' ) = [*((Rea z1) + (Rea z2)),((- (Im1 z1)) + (- (Im1 z2))),((- (Im2 z1)) + (- (Im2 z2))),((- (Im3 z1)) + (- (Im3 z2)))*] by Def7
.= [*(Rea (z1 + z2)),(- ((Im1 z1) + (Im1 z2))),(- ((Im2 z1) + (Im2 z2))),(- ((Im3 z1) + (Im3 z2)))*] by Lm19
.= [*(Rea (z1 + z2)),(- (Im1 (z1 + z2))),(- ((Im2 z1) + (Im2 z2))),(- ((Im3 z1) + (Im3 z2)))*] by Lm19
.= [*(Rea (z1 + z2)),(- (Im1 (z1 + z2))),(- (Im2 (z1 + z2))),(- ((Im3 z1) + (Im3 z2)))*] by Lm19 ;
hence (z1 + z2) *' = (z1 *' ) + (z2 *' ) by A1, Lm19; :: thesis: verum