let z1, z2 be quaternion number ; :: thesis: ( z1 - z2 = 0 implies z1 = z2 )
assume A1: z1 - z2 = 0 ; :: thesis: z1 = z2
A2: ( Rea (z1 - z2) = (Rea z1) - (Rea z2) & Im1 (z1 - z2) = (Im1 z1) - (Im1 z2) & Im2 (z1 - z2) = (Im2 z1) - (Im2 z2) & Im3 (z1 - z2) = (Im3 z1) - (Im3 z2) ) by Lm34;
( Rea (z1 - z2) = 0 & Im1 (z1 - z2) = 0 & Im2 (z1 - z2) = 0 & Im3 (z1 - z2) = 0 ) by A1, Lm5, Th23;
hence z1 = z2 by A2, Th25; :: thesis: verum