theorem Th13: :: COMPUT_1:14

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