let a be Ordinal; :: thesis: for n being Nat holds a (+) n = a +^ n
let n be Nat; :: thesis: a (+) n = a +^ n
A1: 0 c= omega -exponent (last (CantorNF a)) ;
thus a (+) n = a (+) (n *^ 1) by ORDINAL2:39
.= a (+) (n *^ (exp (omega,0))) by ORDINAL2:43
.= a +^ (n *^ (exp (omega,0))) by A1, Th86
.= a +^ (n *^ 1) by ORDINAL2:43
.= a +^ n by ORDINAL2:39 ; :: thesis: verum