let z be Quaternion; :: thesis: ( ((((Rea z) ^2) + ((Im1 z) ^2)) + ((Im2 z) ^2)) + ((Im3 z) ^2) = 0 implies z = 0q )
assume A1: ((((Rea z) ^2) + ((Im1 z) ^2)) + ((Im2 z) ^2)) + ((Im3 z) ^2) = 0 ; :: thesis: z = 0q
then A2: Rea z = 0 by Lm9;
A3: Im1 z = 0 by A1, Lm9;
A4: Im2 z = 0 by A1, Lm9;
Im3 z = 0 by A1, Lm9;
hence z = 0q by A2, A3, A4, Th19; :: thesis: verum