let z be Quaternion; ( z is Real implies z * <k> = [*0,0,0,(Rea z)*] )
assume A1:
z is Real
; 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)*]
; verum