theorem Th7: :: CARD_3:7

for X, Y being set st X <> {} holds
Union (X --> Y) = Y