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 r' = r as real number ;
( (Re z) ^2 >= 0 & (Im z) ^2 >= 0 ) by XREAL_1:65;
then r' >= 0 by A1, SQUARE_1:def 4;
then A2: Re r >= 0 by A1, Def2;
A3: Im r = 0 by A1, Def3;
thus r = Re r by A1, Def2
.= sqrt (((Re r) ^2 ) + ((Im r) ^2 )) by A2, A3, SQUARE_1:89 ; :: thesis: verum