for T being 1-sorted
for S being non empty 1-sorted
for f being Function of T,S
for H being Subset-Family of S holds (" f) .: H is Subset-Family of T