theorem Th2: :: CARD_5:2

for y being object
for f being Function holds
( y in Union f iff ex x being object st
( x in dom f & y in f . x ) )