theorem :: ORDINAL7:48

for A, B being Ordinal-Sequence
for b being Ordinal holds b -leading_coeff (A ^ B) = (b -leading_coeff A) ^ (b -leading_coeff B)