let z be quaternion number ; :: 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)*]
reconsider x = z as Real by A1;
A2: x = Rea z by Lm2;
A3: 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 ;
thus z * <k> = [*0 ,0 ,0 ,(Rea z)*] by A3; :: thesis: verum