:: deftheorem Def16 defines proj CARD_3:def 16 :
for f being Function
for x being object
for b₃ being Function holds
( b₃ = proj (f,x) iff ( dom b₃ = product f & ( for y being Function st y in dom b₃ holds
b₃ . y = y . x ) ) );