let z be quaternion number ; :: 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 Lm10;
A3: Im1 z = 0 by A1, Lm10;
A4: Im2 z = 0 by A1, Lm10;
Im3 z = 0 by A1, Lm10;
hence z = 0q by A2, A3, A4, Th26; :: thesis: verum