:: deftheorem Def5 defines abscomplex SEQ_4:def 5 :
for b₁ being Function of COMPLEX,REAL holds
( b₁ = abscomplex iff for c being Element of COMPLEX holds b₁ . c = |.c.| );