theorem Th45: :: ORDINAL6:45

for f being Ordinal-Sequence st f is normal holds
for a being Ordinal st a in dom (criticals f) holds
f . a c= (criticals f) . a