for f being non empty Function
for P being a_partition of dom f holds { (f | a) where a is Element of P : verum } is a_partition of f