let A, B be Cantor-normal-form Ordinal-Sequence; :: thesis: ( omega -exponent A = omega -exponent B & omega -leading_coeff A = omega -leading_coeff B implies A = B )
assume that
A1: omega -exponent A = omega -exponent B and
A2: omega -leading_coeff A = omega -leading_coeff B ; :: thesis: A = B
A3: dom A = dom (omega -exponent A) by Def1
.= dom B by A1, Def1 ;

now :: thesis: for a being object st a in dom A holds
A . a = B . a

let a be object ; :: thesis: ( a in dom A implies A . a = B . a )
assume A4: a in dom A ; :: thesis: A . a = B . a
hence A . a = ((omega -leading_coeff A) . a) *^ (exp (omega,((omega -exponent A) . a))) by Th65
.= B . a by A1, A2, A3, A4, Th65 ;
:: thesis: verum

end;

hence A = B by A3, FUNCT_1:2; :: thesis: verum