theorem Th60: :: ORDINAL7:47

for a, b being Ordinal holds b -leading_coeff <%a%> = <%(b -leading_coeff a)%>