let z be quaternion number ; :: thesis: ( Rea z = 0 & Im1 z = 0 & Im2 z = 0 & Im3 z = 0 implies z = 0q )
assume ( Rea z = 0 & Im1 z = 0 & Im2 z = 0 & Im3 z = 0 ) ; :: thesis: z = 0q
then ( Rea z = Rea [*0 ,0 ,0 ,0 *] & Im1 z = Im1 [*0 ,0 ,0 ,0 *] & Im2 z = Im2 [*0 ,0 ,0 ,0 *] & Im3 z = Im3 [*0 ,0 ,0 ,0 *] ) by Th23;
hence z = 0q by Lm5, Th25; :: thesis: verum