let z be Element of R_Quaternion; :: thesis: ( z *' = 0. R_Quaternion implies z = 0. R_Quaternion )
assume z *' = 0. R_Quaternion ; :: thesis: z = 0. R_Quaternion
then z *' = 0q by Def10;
then z = 0q by QUATERNI:46;
hence z = 0. R_Quaternion by Def10; :: thesis: verum