theorem Th3: :: ORDINAL4:3
for fi, psi being Ordinal-Sequence
for A being Ordinal st A is_limes_of psi holds
A is_limes_of fi ^ psi