theorem :: FUNCT_1:110

for B being non empty functional set
for f being Function st f = union B holds
( dom f = union { (dom g) where g is Element of B : verum } & rng f = union { (rng g) where g is Element of B : verum } )