theorem Th54: :: ORDINAL6:54

for g being Ordinal-Sequence-valued Sequence st dom g <> {} & ( for a being Ordinal st a in dom g holds
g . a is normal ) holds
for a being Ordinal
for f being Ordinal-Sequence st a in dom (criticals g) & f in rng g holds
f . a c= (criticals g) . a