let z be quaternion number ; :: thesis: ( z is Real implies z * <j> = [*0 ,0 ,(Rea z),0 *] )
assume A1: z is Real ; :: thesis: z * <j> = [*0 ,0 ,(Rea z),0 *]
then reconsider x = z as Real ;
A2: x = Rea z by Lm2;
z * <j> = [*(Rea (z * <j> )),(Im1 (z * <j> )),(Im2 (z * <j> )),(Im3 (z * <j> ))*] by QUATERNI:24
.= [*0 ,(Im1 (z * <j> )),(Im2 (z * <j> )),(Im3 (z * <j> ))*] by A1, QUATERNI:34
.= [*0 ,0 ,(Im2 (z * <j> )),(Im3 (z * <j> ))*] by A1, QUATERNI:34
.= [*0 ,0 ,x,(Im3 (z * <j> ))*] by QUATERNI:34
.= [*0 ,0 ,(Rea z),0 *] by A2, QUATERNI:34 ;
hence z * <j> = [*0 ,0 ,(Rea z),0 *] ; :: thesis: verum