let z be complex number ; :: thesis: ( z = 0 iff ((Re z) ^2 ) + ((Im z) ^2 ) = 0 )
set r = Re z;
set i = Im z;
thus ( z = 0 implies ((Re z) ^2 ) + ((Im z) ^2 ) = 0 ) by Th12; :: thesis: ( ((Re z) ^2 ) + ((Im z) ^2 ) = 0 implies z = 0 )
assume 0 = ((Re z) ^2 ) + ((Im z) ^2 ) ; :: thesis: z = 0
then ( Re z = 0 & Im z = 0 ) by Th2;
hence z = 0 by Th9, Th12; :: thesis: verum