for X being set
for f being Function holds card (f .: X) c= card X by Th64;