let a, b be Ordinal; :: thesis: b -leading_coeff <%a%> = <%(b -leading_coeff a)%>
A1: dom (b -leading_coeff <%a%>) = dom <%a%> by Def3
.= 1 by AFINSQ_1:def 4 ;
0 in 1 by TARSKI:def 1, CARD_1:49;
then 0 in dom <%a%> by AFINSQ_1:def 4;
then (b -leading_coeff <%a%>) . 0 = b -leading_coeff (<%a%> . 0) by Def3
.= b -leading_coeff a ;
hence b -leading_coeff <%a%> = <%(b -leading_coeff a)%> by A1, AFINSQ_1:def 4; :: thesis: verum