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