theorem Th45: :: ORDINAL3:45

for A, B being Ordinal st B <> {} holds
union (A +^ B) = A +^ (union B)