for X, Y being set st ( Y <> {} or X = {} ) holds
ex f being Function st
( X = dom f & rng f c= Y )