for x being object
for Y being set holds Union (x .--> Y) = Y by Th7;