let a, b be Ordinal; :: thesis: b -exponent <%a%> = <%(b -exponent a)%>
A1: dom (b -exponent <%a%>) = dom <%a%> by Def1
.= 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 -exponent <%a%>) . 0 = b -exponent (<%a%> . 0) by Def1
.= b -exponent a ;
hence b -exponent <%a%> = <%(b -exponent a)%> by A1, AFINSQ_1:def 4; :: thesis: verum