theorem :: FUNCT_3:23

for B being set
for f being Function holds (" f) .: B c= bool (dom f)