for S being 1-sorted
for T being empty 1-sorted
for f being Function of S,T st dom f = [#] S holds
S is empty ;