:: deftheorem defines |. COMPLEX1:def 12 :
for z being Complex holds |.z.| = sqrt (((Re z) ^2) + ((Im z) ^2));