for D being non empty set
for M being FinSequence of D * holds Values M = union { (rng f) where f is Element of D * : f in rng M }