:: deftheorem Def2 defines ProjMap TOPS_5:def 2 :
for f being Function
for b₂ being ManySortedFunction of dom f holds
( b₂ = ProjMap f iff for x being object st x in dom f holds
b₂ . x = proj (f,x) );