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