:: deftheorem Def7 defines " FUNCT_1:def 7 :
for f being Function
for Y being set
for b₃ being set holds
( b₃ = f " Y iff for x being object holds
( x in b₃ iff ( x in dom f & f . x in Y ) ) );