let z1 be Quaternion; :: thesis: for x being Real st z1 = x holds
( Rea (z1 * <i>) = 0 & Im1 (z1 * <i>) = x & Im2 (z1 * <i>) = 0 & Im3 (z1 * <i>) = 0 )
let x be Real; :: thesis: ( z1 = x implies ( Rea (z1 * <i>) = 0 & Im1 (z1 * <i>) = x & Im2 (z1 * <i>) = 0 & Im3 (z1 * <i>) = 0 ) )
assume A1: z1 = x ; :: thesis: ( Rea (z1 * <i>) = 0 & Im1 (z1 * <i>) = x & Im2 (z1 * <i>) = 0 & Im3 (z1 * <i>) = 0 )
A2: Rea (z1 * <i>) = ((((Rea z1) * (Rea <i>)) - ((Im1 z1) * (Im1 <i>))) - ((Im2 z1) * (Im2 <i>))) - ((Im3 z1) * (Im3 <i>)) by Lm17;
A3: Im1 (z1 * <i>) = ((((Rea z1) * (Im1 <i>)) + ((Im1 z1) * (Rea <i>))) + ((Im2 z1) * (Im3 <i>))) - ((Im3 z1) * (Im2 <i>)) by Lm17;
A4: Im2 (z1 * <i>) = ((((Rea z1) * (Im2 <i>)) + ((Im2 z1) * (Rea <i>))) + ((Im3 z1) * (Im1 <i>))) - ((Im1 z1) * (Im3 <i>)) by Lm17;
Im3 (z1 * <i>) = ((((Rea z1) * (Im3 <i>)) + ((Im3 z1) * (Rea <i>))) + ((Im1 z1) * (Im2 <i>))) - ((Im2 z1) * (Im1 <i>)) by Lm17;
hence ( Rea (z1 * <i>) = 0 & Im1 (z1 * <i>) = x & Im2 (z1 * <i>) = 0 & Im3 (z1 * <i>) = 0 ) by A1, A2, A3, A4, Lm18, Th23; :: thesis: verum