now :: thesis:

end;

then consider e0 being FinSequence of RelStr(# (sup ((rng (omega -exponent (CantorNF a))) \/ (rng (omega -exponent (CantorNF b))))),(RelIncl (sup ((rng (omega -exponent (CantorNF a))) \/ (rng (omega -exponent (CantorNF b)))))) #) such that
A2: e0 is R -desc_ordering by RELAT_2:def 6, ORDERS_5:78;
set e = FS2XFS e0;
A3: rng (FS2XFS e0) = rng e0 by Th15
.= R by A2, ORDERS_5:def 26 ;
reconsider e = FS2XFS e0 as Ordinal-Sequence ;

now :: thesis:

let a, b be Ordinal; :: thesis:
assume A4: ( a in b & b in dom e ) ; :: thesis:
then A5: a in dom e by ORDINAL1:10;
dom e in omega by CARD_1:61;
then ( a in omega & b in omega ) by A4, A5, ORDINAL1:10;
then reconsider n = a, m = b as Nat ;
card (Segm n) in card (Segm m) by A4;
then A6: n + 1 < m + 1 by NAT_1:41, XREAL_1:8;
A7: ( n + 1 in dom e0 & m + 1 in dom e0 ) by A4, A5, Th13;
then e0 /. (m + 1) < e0 /. (n + 1) by A2, A6, ORDERS_5:def 22;
then A8: ( [(e0 /. (m + 1)),(e0 /. (n + 1))] in the InternalRel of RelStr(# (sup ((rng (omega -exponent (CantorNF a))) \/ (rng (omega -exponent (CantorNF b))))),(RelIncl (sup ((rng (omega -exponent (CantorNF a))) \/ (rng (omega -exponent (CantorNF b)))))) #) & e0 /. (m + 1) <> e0 /. (n + 1) ) by ORDERS_2:def 5, ORDERS_2:def 6;
A9: ( e0 /. (m + 1) = e0 . (m + 1) & e0 /. (n + 1) = e0 . (n + 1) ) by A7, PARTFUN1:def 6;
( e0 . (m + 1) in rng e0 & e0 . (n + 1) in rng e0 ) by A7, FUNCT_1:3;
then ( e0 . (m + 1) in R & e0 . (n + 1) in R ) by A2, ORDERS_5:def 26;
then e0 . (m + 1) c= e0 . (n + 1) by A8, A9, WELLORD2:def 1;
then A10: e0 . (m + 1) c< e0 . (n + 1) by A8, A9, XBOOLE_0:def 8;
( n + 1 <= len e0 & m + 1 <= len e0 ) by A7, FINSEQ_3:25;
then ( (n + 1) - 1 < (len e0) - 0 & (m + 1) - 1 < (len e0) - 0 ) by XREAL_1:15;
then ( e . n = e0 . (n + 1) & e . m = e0 . (m + 1) ) by AFINSQ_1:def 8;
hence e . b in e . a by A10, ORDINAL1:11; :: thesis:

end;

A11: now :: thesis:

let x, y1, y2 be object ; :: thesis:
assume A12: ( x in dom e & S₁[x,y1] & S₁[x,y2] ) ; :: thesis:
then e . x in R by A3, FUNCT_1:3;

per cases by XBOOLE_0:def 3;

suppose ( e . x in rng (omega -exponent (CantorNF a)) & not e . x in rng (omega -exponent (CantorNF b)) ) ; :: thesis:

hence y1 = y2 by A12, XBOOLE_0:def 5; :: thesis:

end;

suppose ( e . x in rng (omega -exponent (CantorNF b)) & not e . x in rng (omega -exponent (CantorNF a)) ) ; :: thesis:

hence y1 = y2 by A12, XBOOLE_0:def 5; :: thesis:

end;

suppose ( e . x in rng (omega -exponent (CantorNF a)) & e . x in rng (omega -exponent (CantorNF b)) ) ; :: thesis:

hence y1 = y2 by A12, XBOOLE_0:def 4; :: thesis:

end;

A13: for x being object st x in dom e holds
ex y being object st S₁[x,y]

proof

let x be object ; :: thesis:
assume x in dom e ; :: thesis:
then e . x in R by A3, FUNCT_1:3;

per cases by XBOOLE_0:def 3;

suppose A14: ( e . x in rng (omega -exponent (CantorNF a)) & not e . x in rng (omega -exponent (CantorNF b)) ) ; :: thesis:

take (omega -leading_coeff (CantorNF a)) . (((omega -exponent (CantorNF a)) ") . (e . x)) ; :: thesis:
thus S₁[x,(omega -leading_coeff (CantorNF a)) . (((omega -exponent (CantorNF a)) ") . (e . x))] by A14, XBOOLE_0:def 4; :: thesis:

end;

suppose A15: ( e . x in rng (omega -exponent (CantorNF b)) & not e . x in rng (omega -exponent (CantorNF a)) ) ; :: thesis:

take (omega -leading_coeff (CantorNF b)) . (((omega -exponent (CantorNF b)) ") . (e . x)) ; :: thesis:
thus S₁[x,(omega -leading_coeff (CantorNF b)) . (((omega -exponent (CantorNF b)) ") . (e . x))] by A15, XBOOLE_0:def 4; :: thesis:

end;

suppose A16: ( e . x in rng (omega -exponent (CantorNF a)) & e . x in rng (omega -exponent (CantorNF b)) ) ; :: thesis:

take ((omega -leading_coeff (CantorNF a)) . (((omega -exponent (CantorNF a)) ") . (e . x))) + ((omega -leading_coeff (CantorNF b)) . (((omega -exponent (CantorNF b)) ") . (e . x))) ; :: thesis:
thus S₁[x,((omega -leading_coeff (CantorNF a)) . (((omega -exponent (CantorNF a)) ") . (e . x))) + ((omega -leading_coeff (CantorNF b)) . (((omega -exponent (CantorNF b)) ") . (e . x)))] by A16, XBOOLE_0:def 5; :: thesis:

end;

consider f being Function such that
A17: dom f = dom e and
A18: for x being object st x in dom e holds
S₁[x,f . x] from FUNCT_1:sch 2(A11, A13);
reconsider f = f as Sequence by A17, ORDINAL1:31;

now :: thesis:

let y be object ; :: thesis:
assume y in rng f ; :: thesis:
then consider x being object such that
A19: ( x in dom f & f . x = y ) by FUNCT_1:def 3;
e . x in rng e by A17, A19, FUNCT_1:3;

per cases by A3, XBOOLE_0:def 3;

suppose ( e . x in rng (omega -exponent (CantorNF a)) & not e . x in rng (omega -exponent (CantorNF b)) ) ; :: thesis:

then e . x in (rng (omega -exponent (CantorNF a))) \ (rng (omega -exponent (CantorNF b))) by XBOOLE_0:def 5;
then f . x = (omega -leading_coeff (CantorNF a)) . (((omega -exponent (CantorNF a)) ") . (e . x)) by A17, A18, A19;
hence y in NAT by A19, ORDINAL1:def 12; :: thesis:

end;

suppose ( e . x in rng (omega -exponent (CantorNF b)) & not e . x in rng (omega -exponent (CantorNF a)) ) ; :: thesis:

then e . x in (rng (omega -exponent (CantorNF b))) \ (rng (omega -exponent (CantorNF a))) by XBOOLE_0:def 5;
then f . x = (omega -leading_coeff (CantorNF b)) . (((omega -exponent (CantorNF b)) ") . (e . x)) by A17, A18, A19;
hence y in NAT by A19, ORDINAL1:def 12; :: thesis:

end;

suppose ( e . x in rng (omega -exponent (CantorNF a)) & e . x in rng (omega -exponent (CantorNF b)) ) ; :: thesis:

then e . x in (rng (omega -exponent (CantorNF a))) /\ (rng (omega -exponent (CantorNF b))) by XBOOLE_0:def 4;
then f . x = ((omega -leading_coeff (CantorNF a)) . (((omega -exponent (CantorNF a)) ") . (e . x))) + ((omega -leading_coeff (CantorNF b)) . (((omega -exponent (CantorNF b)) ") . (e . x))) by A17, A18, A19;
hence y in NAT by A19, ORDINAL1:def 12; :: thesis:

end;

then f is natural-valued by TARSKI:def 3, VALUED_0:def 6;
then reconsider f = f as natural-valued Ordinal-Sequence ;

now :: thesis:

let x be object ; :: thesis:
assume A20: x in dom f ; :: thesis:
A21: ( e . x in rng (omega -exponent (CantorNF a)) implies ((omega -exponent (CantorNF a)) ") . (e . x) in dom (omega -leading_coeff (CantorNF a)) )

proof

end;

A22: ( e . x in rng (omega -exponent (CantorNF b)) implies ((omega -exponent (CantorNF b)) ") . (e . x) in dom (omega -leading_coeff (CantorNF b)) )

proof

end;

e . x in rng e by A17, A20, FUNCT_1:3;

per cases by A3, XBOOLE_0:def 3;

suppose A23: ( e . x in rng (omega -exponent (CantorNF a)) & not e . x in rng (omega -exponent (CantorNF b)) ) ; :: thesis:

then e . x in (rng (omega -exponent (CantorNF a))) \ (rng (omega -exponent (CantorNF b))) by XBOOLE_0:def 5;
then f . x = (omega -leading_coeff (CantorNF a)) . (((omega -exponent (CantorNF a)) ") . (e . x)) by A17, A18, A20;
hence not f . x is empty by A21, A23, FUNCT_1:def 9; :: thesis:

end;

suppose A24: ( e . x in rng (omega -exponent (CantorNF b)) & not e . x in rng (omega -exponent (CantorNF a)) ) ; :: thesis:

then e . x in (rng (omega -exponent (CantorNF b))) \ (rng (omega -exponent (CantorNF a))) by XBOOLE_0:def 5;
then f . x = (omega -leading_coeff (CantorNF b)) . (((omega -exponent (CantorNF b)) ") . (e . x)) by A17, A18, A20;
hence not f . x is empty by A22, A24, FUNCT_1:def 9; :: thesis:

end;

suppose A25: ( e . x in rng (omega -exponent (CantorNF a)) & e . x in rng (omega -exponent (CantorNF b)) ) ; :: thesis:

then e . x in (rng (omega -exponent (CantorNF a))) /\ (rng (omega -exponent (CantorNF b))) by XBOOLE_0:def 4;
then A26: f . x = ((omega -leading_coeff (CantorNF a)) . (((omega -exponent (CantorNF a)) ") . (e . x))) + ((omega -leading_coeff (CantorNF b)) . (((omega -exponent (CantorNF b)) ") . (e . x))) by A17, A18, A20;
( (omega -leading_coeff (CantorNF a)) . (((omega -exponent (CantorNF a)) ") . (e . x)) <> {} & (omega -leading_coeff (CantorNF b)) . (((omega -exponent (CantorNF b)) ") . (e . x)) <> {} ) by A21, A22, A25, FUNCT_1:def 9;
hence not f . x is empty by A26; :: thesis:

end;

then reconsider f = f as non-empty natural-valued Ordinal-Sequence by FUNCT_1:def 9;
consider C being Cantor-normal-form Ordinal-Sequence such that
A27: ( omega -exponent C = e & omega -leading_coeff C = f ) by A17, Th66;
take Sum^ C ; :: thesis:
take C ; :: thesis:
thus Sum^ C = Sum^ C ; :: thesis:
thus rng (omega -exponent C) = (rng (omega -exponent (CantorNF a))) \/ (rng (omega -exponent (CantorNF b))) by A3, A27; :: thesis:
let d be object ; :: thesis:
assume A28: d in dom C ; :: thesis:

hereby :: thesis:

assume omega -exponent (C . d) in (rng (omega -exponent (CantorNF a))) \ (rng (omega -exponent (CantorNF b))) ; :: thesis:
then A29: e . d in (rng (omega -exponent (CantorNF a))) \ (rng (omega -exponent (CantorNF b))) by A27, A28, Def1;
d in dom (omega -exponent C) by A28, Def1;
then f . d = (omega -leading_coeff (CantorNF a)) . (((omega -exponent (CantorNF a)) ") . (e . d)) by A18, A27, A29
.= (omega -leading_coeff (CantorNF a)) . (((omega -exponent (CantorNF a)) ") . (omega -exponent (C . d))) by A27, A28, Def1 ;
hence omega -leading_coeff (C . d) = (omega -leading_coeff (CantorNF a)) . (((omega -exponent (CantorNF a)) ") . (omega -exponent (C . d))) by A27, A28, Def3; :: thesis:

end;

hereby :: thesis:

assume omega -exponent (C . d) in (rng (omega -exponent (CantorNF b))) \ (rng (omega -exponent (CantorNF a))) ; :: thesis:
then A30: e . d in (rng (omega -exponent (CantorNF b))) \ (rng (omega -exponent (CantorNF a))) by A27, A28, Def1;
d in dom (omega -exponent C) by A28, Def1;
then f . d = (omega -leading_coeff (CantorNF b)) . (((omega -exponent (CantorNF b)) ") . (e . d)) by A18, A27, A30
.= (omega -leading_coeff (CantorNF b)) . (((omega -exponent (CantorNF b)) ") . (omega -exponent (C . d))) by A27, A28, Def1 ;
hence omega -leading_coeff (C . d) = (omega -leading_coeff (CantorNF b)) . (((omega -exponent (CantorNF b)) ") . (omega -exponent (C . d))) by A27, A28, Def3; :: thesis:

end;