let z be quaternion number ; :: thesis: ( ((((Rea z) ^2 ) + ((Im1 z) ^2 )) + ((Im2 z) ^2 )) + ((Im3 z) ^2 ) = 0 implies z = 0q )
assume ((((Rea z) ^2 ) + ((Im1 z) ^2 )) + ((Im2 z) ^2 )) + ((Im3 z) ^2 ) = 0 ; :: thesis: z = 0q
then ( Rea z = 0 & Im1 z = 0 & Im2 z = 0 & Im3 z = 0 ) by Lm8;
hence z = 0q by Th26; :: thesis: verum