let a be non empty Ordinal; :: thesis: for b being Ordinal
for n being non zero Nat st b in omega -exponent (last (CantorNF a)) holds
CantorNF (a +^ (n *^ (exp (omega,b)))) = (CantorNF a) ^ <%(n *^ (exp (omega,b)))%>
let b be Ordinal; :: thesis: for n being non zero Nat st b in omega -exponent (last (CantorNF a)) holds
CantorNF (a +^ (n *^ (exp (omega,b)))) = (CantorNF a) ^ <%(n *^ (exp (omega,b)))%>
let n be non zero Nat; :: thesis: ( b in omega -exponent (last (CantorNF a)) implies CantorNF (a +^ (n *^ (exp (omega,b)))) = (CantorNF a) ^ <%(n *^ (exp (omega,b)))%> )
assume A1: b in omega -exponent (last (CantorNF a)) ; :: thesis: CantorNF (a +^ (n *^ (exp (omega,b)))) = (CantorNF a) ^ <%(n *^ (exp (omega,b)))%>
set A = CantorNF a;
set B = <%(n *^ (exp (omega,b)))%>;
A2: (CantorNF a) ^ <%(n *^ (exp (omega,b)))%> is Cantor-normal-form by A1, Th37;
Sum^ ((CantorNF a) ^ <%(n *^ (exp (omega,b)))%>) = (Sum^ (CantorNF a)) +^ (n *^ (exp (omega,b))) by ORDINAL5:54
.= a +^ (n *^ (exp (omega,b))) ;
hence CantorNF (a +^ (n *^ (exp (omega,b)))) = (CantorNF a) ^ <%(n *^ (exp (omega,b)))%> by A2; :: thesis: verum