let A be Cantor-normal-form Ordinal-Sequence; :: thesis: for a being object st a in dom A holds
A . a = (omega -leading_coeff (A . a)) *^ (exp (omega,(omega -exponent (A . a))))
let a be object ; :: thesis: ( a in dom A implies A . a = (omega -leading_coeff (A . a)) *^ (exp (omega,(omega -exponent (A . a)))) )
assume a in dom A ; :: thesis: A . a = (omega -leading_coeff (A . a)) *^ (exp (omega,(omega -exponent (A . a))))
then A . a is Cantor-component by ORDINAL5:def 11;
hence A . a = (omega -leading_coeff (A . a)) *^ (exp (omega,(omega -exponent (A . a)))) by Th59; :: thesis: verum