theorem :: COMPLEX1:72

for a being Real holds sqrt (a ^2) = |.a.| by Lm28;