let z be Quaternion; :: thesis: ( Rea (z *') = Rea z & Im1 (z *') = - (Im1 z) & Im2 (z *') = - (Im2 z) & Im3 (z *') = - (Im3 z) )
z *' = [*(Rea z),(- (Im1 z)),(- (Im2 z)),(- (Im3 z))*] by Lm19;
hence ( Rea (z *') = Rea z & Im1 (z *') = - (Im1 z) & Im2 (z *') = - (Im2 z) & Im3 (z *') = - (Im3 z) ) by Th16; :: thesis: verum