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