theorem Th1: :: LATTICE5:1

for f being Function
for F being Function-yielding Function st f = union (rng F) holds
dom f = union (rng (doms F))