let r be Real; :: thesis: for b₁ being Complex st r = sqrt (((Re b₁) ^2) + ((Im b₁) ^2)) holds
r = sqrt (((Re r) ^2) + ((Im r) ^2))
reconsider rr = r as Element of REAL by XREAL_0:def 1;
let z be Complex; :: 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))
( (Re z) ^2 >= 0 & (Im z) ^2 >= 0 ) by XREAL_1:63;
then r >= 0 by A1, SQUARE_1:def 2;
then A2: Re rr >= 0 by Def1;
thus r = Re rr by Def1
.= sqrt (((Re r) ^2) + ((Im r) ^2)) by A2, SQUARE_1:22 ; :: thesis: verum