theorem :: ORDINAL7:50

for A being finite Ordinal-Sequence
for b being Ordinal
for n being Nat holds b -leading_coeff (A /^ n) = (b -leading_coeff A) /^ n