theorem Th47: :: ORDINAL3:47

for A, B being Ordinal st A <> {} holds
ex C, D being Ordinal st
( B = (C *^ A) +^ D & D in A )