for f being set
for p being Relation
for x being set st x in rng p holds
the_rank_of x in the_rank_of [p,f]