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 ARYTM_0:def 7, A2; :: thesis: verum