theorem Th36: :: QUATERNI:43

for z being Quaternion holds z *' = [*(Rea z),(- (Im1 z)),(- (Im2 z)),(- (Im3 z))*]