let z be quaternion number ; :: thesis: ( Rea z = 0 & Im1 z = 0 & Im2 z = 0 & Im3 z = 0 implies z = 0q )
assume that
A1: Rea z = 0 and
A2: Im1 z = 0 and
A3: Im2 z = 0 and
A4: Im3 z = 0 ; :: thesis: z = 0q
A5: Rea z = Rea [*0 ,0 ,0 ,0 *] by A1, Th23;
A6: Im1 z = Im1 [*0 ,0 ,0 ,0 *] by A2, Th23;
A7: Im2 z = Im2 [*0 ,0 ,0 ,0 *] by A3, Th23;
Im3 z = Im3 [*0 ,0 ,0 ,0 *] by A4, Th23;
hence z = 0q by A5, A6, A7, Lm7, Th25; :: thesis: verum