let r, z be complex 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 reconsider r9 = r as real number ;
A2: Im r = 0 by A1, Def3;
( (Re z) ^2 >= 0 & (Im z) ^2 >= 0 ) by XREAL_1:65;
then r9 >= 0 by A1, SQUARE_1:def 4;
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:89 ; :: thesis: verum