let z1 be quaternion number ; :: thesis: for x being Real st z1 = x holds
( Rea (z1 * <k> ) = 0 & Im1 (z1 * <k> ) = 0 & Im2 (z1 * <k> ) = 0 & Im3 (z1 * <k> ) = x )
let x be Real; :: thesis: ( z1 = x implies ( Rea (z1 * <k> ) = 0 & Im1 (z1 * <k> ) = 0 & Im2 (z1 * <k> ) = 0 & Im3 (z1 * <k> ) = x ) )
assume A1: z1 = x ; :: thesis: ( Rea (z1 * <k> ) = 0 & Im1 (z1 * <k> ) = 0 & Im2 (z1 * <k> ) = 0 & Im3 (z1 * <k> ) = x )
( Rea (z1 * <k> ) = ((((Rea z1) * (Rea <k> )) - ((Im1 z1) * (Im1 <k> ))) - ((Im2 z1) * (Im2 <k> ))) - ((Im3 z1) * (Im3 <k> )) & Im1 (z1 * <k> ) = ((((Rea z1) * (Im1 <k> )) + ((Im1 z1) * (Rea <k> ))) + ((Im2 z1) * (Im3 <k> ))) - ((Im3 z1) * (Im2 <k> )) & Im2 (z1 * <k> ) = ((((Rea z1) * (Im2 <k> )) + ((Im2 z1) * (Rea <k> ))) + ((Im3 z1) * (Im1 <k> ))) - ((Im1 z1) * (Im3 <k> )) & Im3 (z1 * <k> ) = ((((Rea z1) * (Im3 <k> )) + ((Im3 z1) * (Rea <k> ))) + ((Im1 z1) * (Im2 <k> ))) - ((Im2 z1) * (Im1 <k> )) ) by Lm16;
hence ( Rea (z1 * <k> ) = 0 & Im1 (z1 * <k> ) = 0 & Im2 (z1 * <k> ) = 0 & Im3 (z1 * <k> ) = x ) by A1, Lm17, Th31; :: thesis: verum