:: deftheorem Def11 defines |. VALUED_1:def 11 :
for f being complex-valued Function
for b₂ being real-valued Function holds
( b₂ = |.f.| iff ( dom b₂ = dom f & ( for c being object st c in dom b₂ holds
b₂ . c = |.(f . c).| ) ) );