:: deftheorem Def1 defines *' COMSEQ_2:def 1 :
for f, b₂ being complex-valued Function holds
( b₂ = f *' iff ( dom b₂ = dom f & ( for c being set st c in dom b₂ holds
b₂ . c = (f . c) *' ) ) );