:: deftheorem Def6 defines .: FUNCT_1:def 6 :
for f being Function
for X being set
for b₃ being set holds
( b₃ = f .: X iff for y being object holds
( y in b₃ iff ex x being object st
( x in dom f & x in X & y = f . x ) ) );