for X being set
for Y being non empty set
for f being Function of X,Y holds { (f " {y}) where y is Element of Y : y in rng f } is a_partition of X