theorem :: MBOOLEAN:22

for I, x being set holds union (I --> x) = I --> (union x)