:: deftheorem Def2 defines *' COMSEQ_2:def 2 :
for C being non empty set
for f, b₃ being Function of C,COMPLEX holds
( b₃ = f *' iff for n being Element of C holds b₃ . n = (f . n) *' );