let A be decreasing Ordinal-Sequence; :: thesis: for B being non-empty natural-valued Ordinal-Sequence st dom A = dom B holds
ex C being Cantor-normal-form Ordinal-Sequence st
( omega -exponent C = A & omega -leading_coeff C = B )
let B be non-empty natural-valued Ordinal-Sequence; :: thesis: ( dom A = dom B implies ex C being Cantor-normal-form Ordinal-Sequence st
( omega -exponent C = A & omega -leading_coeff C = B ) )
assume A1: dom A = dom B ; :: thesis: ex C being Cantor-normal-form Ordinal-Sequence st
( omega -exponent C = A & omega -leading_coeff C = B )
deffunc H₁( Ordinal) -> set = (B . $1) *^ (exp (omega,(A . $1)));
consider C being Ordinal-Sequence such that
A2: ( dom C = dom A & ( for a being Ordinal st a in dom A holds
C . a = H₁(a) ) ) from ORDINAL2:sch 3();

A3: now :: thesis: for a being Ordinal st a in dom C holds
C . a is Cantor-component

let a be Ordinal; :: thesis: ( a in dom C implies C . a is Cantor-component )
assume A4: a in dom C ; :: thesis: C . a is Cantor-component
then A5: C . a = (B . a) *^ (exp (omega,(A . a))) by A2;
B . a <> {} by A1, A2, A4, FUNCT_1:def 9;
hence C . a is Cantor-component by A5; :: thesis: verum

end;

now :: thesis: for a, b being Ordinal st a in b & b in dom C holds
omega -exponent (C . b) in omega -exponent (C . a)

let a, b be Ordinal; :: thesis: ( a in b & b in dom C implies omega -exponent (C . b) in omega -exponent (C . a) )
assume A6: ( a in b & b in dom C ) ; :: thesis: omega -exponent (C . b) in omega -exponent (C . a)
then A7: ( C . a = (B . a) *^ (exp (omega,(A . a))) & C . b = (B . b) *^ (exp (omega,(A . b))) ) by A2, ORDINAL1:10;
XA: rng B c= NAT by VALUED_0:def 6;
X0: b in dom B by A6, A1, A2;
then b c= dom B by ORDINAL1:def 2;
then xy: ( B . b in rng B & B . a in rng B ) by A6, X0, FUNCT_1:3;
( B . a <> {} & B . b <> {} ) by A1, A2, A6, ORDINAL1:10, FUNCT_1:def 9;
then ( 0 c< B . a & 0 c< B . b ) by XBOOLE_1:2, XBOOLE_0:def 8;
then ( 0 in B . a & 0 in B . b ) by ORDINAL1:11;
then ( omega -exponent (C . b) = A . b & omega -exponent (C . a) = A . a ) by A7, ORDINAL5:58, XA, xy;
hence omega -exponent (C . b) in omega -exponent (C . a) by A2, A6, ORDINAL5:def 1; :: thesis: verum

end;

then reconsider C = C as Cantor-normal-form Ordinal-Sequence by A3, ORDINAL5:def 11;
take C ; :: thesis: ( omega -exponent C = A & omega -leading_coeff C = B )
A9: dom (omega -exponent C) = dom A by A2, Def1;

now :: thesis: for a being object st a in dom (omega -exponent C) holds
(omega -exponent C) . a = A . a

let a be object ; :: thesis: ( a in dom (omega -exponent C) implies (omega -exponent C) . a = A . a )
assume a in dom (omega -exponent C) ; :: thesis: (omega -exponent C) . a = A . a
then A10: a in dom C by Def1;
then A11: C . a = (B . a) *^ (exp (omega,(A . a))) by A2;
B . a <> {} by A1, A2, A10, FUNCT_1:def 9;
then 0 c< B . a by XBOOLE_1:2, XBOOLE_0:def 8;
then A12: 0 in B . a by ORDINAL1:11;
Sa: B . a in rng B by FUNCT_1:3, A10, A1, A2;
rng B c= NAT by VALUED_0:def 6;
then omega -exponent (C . a) = A . a by A11, A12, ORDINAL5:58, Sa;
hence (omega -exponent C) . a = A . a by A10, Def1; :: thesis: verum

end;

hence omega -exponent C = A by A9, FUNCT_1:2; :: thesis: omega -leading_coeff C = B
A13: dom (omega -leading_coeff C) = dom B by A1, A2, Def3;

now :: thesis: for a being object st a in dom (omega -leading_coeff C) holds
(omega -leading_coeff C) . a = B . a

let a be object ; :: thesis: ( a in dom (omega -leading_coeff C) implies (omega -leading_coeff C) . a = B . a )
assume a in dom (omega -leading_coeff C) ; :: thesis: (omega -leading_coeff C) . a = B . a
then A14: a in dom C by Def3;
then C . a = (B . a) *^ (exp (omega,(A . a))) by A2;
then omega -leading_coeff (C . a) = B . a by Th57, ORDINAL1:def 12;
hence (omega -leading_coeff C) . a = B . a by A14, Def3; :: thesis: verum

end;

hence omega -leading_coeff C = B by A13, FUNCT_1:2; :: thesis: verum