for V, W being non empty 1-sorted
for T being Function of V,W holds
( dom T = [#] V & rng T c= [#] W )