:: deftheorem defines *' QUATERNI:def 21 :
for z being Quaternion holds z *' = (((Rea z) + ((- (Im1 z)) * <i>)) + ((- (Im2 z)) * <j>)) + ((- (Im3 z)) * <k>);