let z be quaternion number ; :: thesis: ( Im1 z = 0 & Im2 z = 0 & Im3 z = 0 implies z = Rea z )
set x = Rea z;
assume ( Im1 z = 0 & Im2 z = 0 & Im3 z = 0 ) ; :: thesis: z = Rea z
then A2: z = [*(Rea z),0 ,0 ,0 *] by QUATERNI:24;
[*(Rea z),0 ,0 ,0 *] = [*(Rea z),0 *] by QUATERNI:91;
hence z = Rea z by A2, ARYTM_0:def 7; :: thesis: verum