for X being non empty functional compatible set holds rng (union X) = union { (rng f) where f is Element of X : verum }