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 A1: a in dom A ; :: thesis: A . a = ((omega -leading_coeff A) . a) *^ (exp (omega,((omega -exponent A) . a)))
hence A . a = (omega -leading_coeff (A . a)) *^ (exp (omega,(omega -exponent (A . a)))) by Th64
.= ((omega -leading_coeff A) . a) *^ (exp (omega,(omega -exponent (A . a)))) by A1, Def3
.= ((omega -leading_coeff A) . a) *^ (exp (omega,((omega -exponent A) . a))) by A1, Def1 ;
:: thesis: verum