for X being set
for f being Function st X <> {} & X c= dom f holds
f .: X <> {}