let z be Quaternion; :: thesis: ( Rea z = 0 implies z *' = - z )
assume A1: Rea z = 0 ; :: thesis: z *' = - z
- z = (((- (Rea z)) + ((- (Im1 z)) * <i>)) + ((- (Im2 z)) * <j>)) + ((- (Im3 z)) * <k>) by Lm24;
hence z *' = - z by A1; :: thesis: verum