let r, z be real number ; :: thesis: ( r = sqrt (((Re z) ^2) + ((Im z) ^2)) implies r = sqrt (((Re r) ^2) + ((Im r) ^2)) )
assume A1: r = sqrt (((Re z) ^2) + ((Im z) ^2)) ; :: thesis: r = sqrt (((Re r) ^2) + ((Im r) ^2))
then A2: Im r = 0 by Def3;
( (Re z) ^2 >= 0 & (Im z) ^2 >= 0 ) by XREAL_1:63;
then r >= 0 by A1, SQUARE_1:def 2;
then A3: Re r >= 0 by A1, Def2;
thus r = Re r by A1, Def2
.= sqrt (((Re r) ^2) + ((Im r) ^2)) by A3, A2, SQUARE_1:22 ; :: thesis: verum