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