defpred S₁[ non empty Ordinal] means for a being non empty Ordinal
for b being Ordinal st b in $1 holds
a (+) b in a (+) $1;
let a be non empty Ordinal; :: thesis:
let b, d be Ordinal; :: thesis:
assume A1: ( b in d & (CantorNF b) . 0 <> (CantorNF d) . 0 ) ; :: thesis:
then A2: omega -exponent b c= omega -exponent d by Th22, ORDINAL1:def 2;
set c = omega -exponent d;
defpred S₂[ Nat] means ( $1 in dom (CantorNF a) & omega -exponent ((CantorNF a) . $1) c= omega -exponent d & ( for j being Nat st j < $1 holds
omega -exponent d in omega -exponent ((CantorNF a) . j) ) );

per cases ;

suppose A3: for i being Nat holds not S₂[i] ; :: thesis:

defpred S₃[ Nat] means ( $1 in dom (CantorNF a) implies omega -exponent d in omega -exponent ((CantorNF a) . $1) );
A4: for k being Nat st ( for j being Nat st j < k holds
S₃[j] ) holds
S₃[k]

proof

let k be Nat; :: thesis:
assume that
A5: for j being Nat st j < k holds
S₃[j] and
A6: k in dom (CantorNF a) and
A7: not omega -exponent d in omega -exponent ((CantorNF a) . k) ; :: thesis:
A8: omega -exponent ((CantorNF a) . k) c= omega -exponent d by A7, ORDINAL1:16;
for j being Nat st j < k holds
omega -exponent d in omega -exponent ((CantorNF a) . j)

proof

let j be Nat; :: thesis:
assume A9: j < k ; :: thesis:
then j in Segm k by NAT_1:44;
then j in dom (CantorNF a) by A6, ORDINAL1:10;
hence omega -exponent d in omega -exponent ((CantorNF a) . j) by A5, A9; :: thesis:

end;

hence contradiction by A3, A6, A8; :: thesis:

end;

A10: for k being Nat holds S₃[k] from NAT_1:sch 4(A4);
consider A0 being Cantor-normal-form Ordinal-Sequence, a0 being Cantor-component Ordinal such that
A11: CantorNF a = A0 ^ <%a0%> by Th29;
len (CantorNF a) = (len A0) + (len <%a0%>) by A11, AFINSQ_1:17
.= (len A0) + 1 by AFINSQ_1:34 ;
then len A0 < len (CantorNF a) by NAT_1:13;
then len A0 in Segm (len (CantorNF a)) by NAT_1:44;
then omega -exponent d in omega -exponent ((CantorNF a) . (len A0)) by A10;
then omega -exponent d in omega -exponent a0 by A11, AFINSQ_1:36;
then A12: omega -exponent d in omega -exponent (last (CantorNF a)) by A11, AFINSQ_1:92;
then A13: a (+) d = a +^ d by Th85;
a (+) b = a +^ b by A2, A12, Th85, ORDINAL1:12;
hence a (+) b in a (+) d by A1, A13, ORDINAL2:32; :: thesis:

end;

suppose ex i being Nat st S₂[i] ; :: thesis:

proof

A30: ( i in dom (CantorNF (a (+) b)) & i in dom (CantorNF (a (+) d)) ) by A14, Th77, TARSKI:def 3;

now :: thesis:

let x be object ; :: thesis:

hereby :: thesis:

assume x in dom ((CantorNF (a (+) b)) | i) ; :: thesis:
then A31: x in i by RELAT_1:57;
then x in dom (CantorNF (a (+) d)) by A30, ORDINAL1:10;
hence x in dom ((CantorNF (a (+) d)) | i) by A31, RELAT_1:57; :: thesis:

end;

assume x in dom ((CantorNF (a (+) d)) | i) ; :: thesis:
then A32: x in i by RELAT_1:57;
then x in dom (CantorNF (a (+) b)) by A30, ORDINAL1:10;
hence x in dom ((CantorNF (a (+) b)) | i) by A32, RELAT_1:57; :: thesis:

end;

hence dom ((CantorNF (a (+) b)) | i) = dom ((CantorNF (a (+) d)) | i) by TARSKI:2; :: thesis:

end;

A33: for n being Nat st n in dom ((CantorNF (a (+) b)) | i) holds
((CantorNF (a (+) b)) | i) . n = (CantorNF a) . n

proof

defpred S₃[ Nat] means ( $1 in dom ((CantorNF (a (+) b)) | i) & ((CantorNF (a (+) b)) | i) . $1 <> (CantorNF a) . $1 );
assume A34: ex n being Nat st S₃[n] ; :: thesis:
consider n being Nat such that
A35: ( S₃[n] & ( for m being Nat st S₃[m] holds
n <= m ) ) from NAT_1:sch 5(A34);
A36: n in i by A35, RELAT_1:57;
then A37: n in dom (CantorNF a) by A14, ORDINAL1:10;
then A38: n in dom (CantorNF (a (+) b)) by Th77, TARSKI:def 3;
A39: not omega -exponent ((CantorNF (a (+) b)) . n) in rng (omega -exponent (CantorNF b))

proof

end;

A45: omega -exponent ((CantorNF (a (+) b)) . n) = (omega -exponent (CantorNF a)) . n

proof

proof

assume not m in n ; :: thesis:

per cases by ORDINAL1:14;

suppose m = n ; :: thesis:

hence contradiction by A46, A48; :: thesis:

end;

suppose A50: n in m ; :: thesis:

A51: m in dom (CantorNF a) by A48, Def1;
then omega -exponent ((CantorNF a) . m) in omega -exponent ((CantorNF a) . n) by A50, ORDINAL5:def 11;
then (omega -exponent (CantorNF a)) . m in omega -exponent ((CantorNF a) . n) by A51, Def1;
hence contradiction by A37, A46, A48, Def1; :: thesis:

end;

end;

A57: n in dom (omega -exponent (CantorNF a)) by A37, Def1;
n in dom (omega -exponent (CantorNF a)) by A37, Def1;
then omega -exponent ((CantorNF (a (+) b)) . n) in rng (omega -exponent (CantorNF a)) by A45, FUNCT_1:3;
then omega -exponent ((CantorNF (a (+) b)) . n) in (rng (omega -exponent (CantorNF a))) \ (rng (omega -exponent (CantorNF b))) by A39, XBOOLE_0:def 5;
then A58: omega -leading_coeff ((CantorNF (a (+) b)) . n) = (omega -leading_coeff (CantorNF a)) . (((omega -exponent (CantorNF a)) ") . ((omega -exponent (CantorNF a)) . n)) by A38, A45, Th78
.= (omega -leading_coeff (CantorNF a)) . n by A57, FUNCT_1:34 ;
((CantorNF (a (+) b)) | i) . n = (CantorNF (a (+) b)) . n by A36, FUNCT_1:49
.= ((omega -leading_coeff (CantorNF a)) . n) *^ (exp (omega,(omega -exponent ((CantorNF (a (+) b)) . n)))) by A38, A58, Th64
.= (CantorNF a) . n by A37, A45, Th65 ;
hence contradiction by A35; :: thesis:

end;

A59: for n being Nat st n in dom ((CantorNF (a (+) d)) | i) holds
((CantorNF (a (+) d)) | i) . n = (CantorNF a) . n

proof

defpred S₃[ Nat] means ( $1 in dom ((CantorNF (a (+) d)) | i) & ((CantorNF (a (+) d)) | i) . $1 <> (CantorNF a) . $1 );
assume A60: ex n being Nat st S₃[n] ; :: thesis:
consider n being Nat such that
A61: ( S₃[n] & ( for m being Nat st S₃[m] holds
n <= m ) ) from NAT_1:sch 5(A60);
A62: n in i by A61, RELAT_1:57;
then A63: n in dom (CantorNF a) by A14, ORDINAL1:10;
then A64: n in dom (CantorNF (a (+) d)) by Th77, TARSKI:def 3;
A65: not omega -exponent ((CantorNF (a (+) d)) . n) in rng (omega -exponent (CantorNF d))

proof

end;

A70: omega -exponent ((CantorNF (a (+) d)) . n) = (omega -exponent (CantorNF a)) . n

proof

proof

assume not m in n ; :: thesis:

per cases by ORDINAL1:14;

suppose m = n ; :: thesis:

hence contradiction by A71, A73; :: thesis:

end;

suppose A75: n in m ; :: thesis:

A76: m in dom (CantorNF a) by A73, Def1;
then omega -exponent ((CantorNF a) . m) in omega -exponent ((CantorNF a) . n) by A75, ORDINAL5:def 11;
then (omega -exponent (CantorNF a)) . m in omega -exponent ((CantorNF a) . n) by A76, Def1;
hence contradiction by A63, A71, A73, Def1; :: thesis:

end;

then m in Segm n ;
then A77: m < n by NAT_1:44;
A78: m in dom ((CantorNF (a (+) d)) | i) by A61, A74, ORDINAL1:10;
A79: m in dom (CantorNF a) by A63, A74, ORDINAL1:10;
A80: m in dom (CantorNF (a (+) d)) by A64, A74, ORDINAL1:10;
A81: (omega -exponent (CantorNF (a (+) d))) . m = omega -exponent ((CantorNF (a (+) d)) . m) by A64, A74, Def1, ORDINAL1:10
.= omega -exponent (((CantorNF (a (+) d)) | i) . m) by A78, FUNCT_1:47
.= omega -exponent ((CantorNF a) . m) by A61, A77, A78
.= (omega -exponent (CantorNF a)) . m by A79, Def1 ;
omega -exponent ((CantorNF (a (+) d)) . n) in omega -exponent ((CantorNF (a (+) d)) . m) by A64, A74, ORDINAL5:def 11;
then (omega -exponent (CantorNF (a (+) d))) . n in omega -exponent ((CantorNF (a (+) d)) . m) by A64, Def1;
then (omega -exponent (CantorNF (a (+) d))) . n in (omega -exponent (CantorNF (a (+) d))) . m by A80, Def1;
hence contradiction by A73, A81; :: thesis:

end;

A82: n in dom (omega -exponent (CantorNF a)) by A63, Def1;
n in dom (omega -exponent (CantorNF a)) by A63, Def1;
then omega -exponent ((CantorNF (a (+) d)) . n) in rng (omega -exponent (CantorNF a)) by A70, FUNCT_1:3;
then omega -exponent ((CantorNF (a (+) d)) . n) in (rng (omega -exponent (CantorNF a))) \ (rng (omega -exponent (CantorNF d))) by A65, XBOOLE_0:def 5;
then A83: omega -leading_coeff ((CantorNF (a (+) d)) . n) = (omega -leading_coeff (CantorNF a)) . (((omega -exponent (CantorNF a)) ") . (omega -exponent ((CantorNF (a (+) d)) . n))) by A64, Th78
.= (omega -leading_coeff (CantorNF a)) . n by A70, A82, FUNCT_1:34 ;
((CantorNF (a (+) d)) | i) . n = (CantorNF (a (+) d)) . n by A62, FUNCT_1:49
.= ((omega -leading_coeff (CantorNF a)) . n) *^ (exp (omega,(omega -exponent ((CantorNF (a (+) d)) . n)))) by A64, A83, Th64
.= (CantorNF a) . n by A63, A70, Th65 ;
hence contradiction by A61; :: thesis:

end;

for x being object st x in dom ((CantorNF (a (+) b)) | i) holds
((CantorNF (a (+) b)) | i) . x = ((CantorNF (a (+) d)) | i) . x

proof

let x be object ; :: thesis:
assume x in dom ((CantorNF (a (+) b)) | i) ; :: thesis:
then ( ((CantorNF (a (+) b)) | i) . x = (CantorNF a) . x & ((CantorNF (a (+) d)) | i) . x = (CantorNF a) . x ) by A29, A33, A59;
hence ((CantorNF (a (+) b)) | i) . x = ((CantorNF (a (+) d)) | i) . x ; :: thesis:

end;

then A85: Sum^ ((CantorNF (a (+) b)) | i) = Sum^ ((CantorNF (a (+) d)) | i) by A29, FUNCT_1:2;
A86: omega -exponent ((CantorNF (a (+) d)) . i) = omega -exponent d

proof

assume A87: omega -exponent ((CantorNF (a (+) d)) . i) <> omega -exponent d ; :: thesis:
A88: not omega -exponent ((CantorNF (a (+) d)) . i) in rng (omega -exponent (CantorNF d))

proof

not omega -exponent ((CantorNF (a (+) d)) . i) in omega -exponent d

proof

assume A89: omega -exponent ((CantorNF (a (+) d)) . i) in omega -exponent d ; :: thesis:
consider j being object such that
A90: ( j in dom (omega -exponent (CantorNF (a (+) d))) & (omega -exponent (CantorNF (a (+) d))) . j = omega -exponent d ) by A19, FUNCT_1:def 3;
reconsider j = j as Nat by A90;
A91: j in dom (CantorNF (a (+) d)) by A90, Def1;
then A92: omega -exponent ((CantorNF (a (+) d)) . j) = omega -exponent d by A90, Def1;

per cases by ORDINAL1:14;

suppose A93: j in i ; :: thesis:

then A94: j in Segm i ;
(CantorNF a) . j = ((CantorNF (a (+) d)) | i) . j by A59, A91, A93, RELAT_1:57
.= (CantorNF (a (+) d)) . j by A93, FUNCT_1:49 ;
then A95: omega -exponent d = omega -exponent ((CantorNF a) . j) by A92;
omega -exponent d in omega -exponent ((CantorNF a) . j) by A14, A94, NAT_1:44;
hence contradiction by A95; :: thesis:

end;

suppose j = i ; :: thesis:

hence contradiction by A89, A92; :: thesis:

end;

suppose i in j ; :: thesis:

hence contradiction by A89, A91, A92, ORDINAL5:def 11; :: thesis:

end;

then A96: omega -exponent d in omega -exponent ((CantorNF (a (+) d)) . i) by A87, ORDINAL1:14;
assume omega -exponent ((CantorNF (a (+) d)) . i) in rng (omega -exponent (CantorNF d)) ; :: thesis:
then consider k being object such that
A97: ( k in dom (omega -exponent (CantorNF d)) & (omega -exponent (CantorNF d)) . k = omega -exponent ((CantorNF (a (+) d)) . i) ) by FUNCT_1:def 3;
reconsider k = k as Nat by A97;
omega -exponent (Sum^ (CantorNF d)) in (omega -exponent (CantorNF d)) . k by A96, A97;
then omega -exponent ((CantorNF d) . 0) in (omega -exponent (CantorNF d)) . k by Th44;
then A98: (omega -exponent (CantorNF d)) . 0 in (omega -exponent (CantorNF d)) . k by A15, Def1;

per cases ;

suppose k = 0 ; :: thesis:

hence contradiction by A98; :: thesis:

end;

suppose 0 < k ; :: thesis:

then 0 in Segm k by NAT_1:44;
hence contradiction by A97, A98, ORDINAL5:def 1; :: thesis:

end;

omega -exponent ((CantorNF (a (+) d)) . i) = (omega -exponent (CantorNF a)) . i

proof

per cases by XXREAL_0:1;

suppose j < i ; :: thesis:

then A102: j in Segm i by NAT_1:44;
then A103: j in dom (CantorNF a) by A14, ORDINAL1:10;
( i in dom (CantorNF (a (+) b)) & i in dom (CantorNF (a (+) d)) ) by A14, Th77, TARSKI:def 3;
then ( j in dom (CantorNF (a (+) b)) & j in dom (CantorNF (a (+) d)) ) by A102, ORDINAL1:10;
then A104: ( j in dom ((CantorNF (a (+) b)) | i) & j in dom ((CantorNF (a (+) d)) | i) ) by A102, RELAT_1:57;
then A105: omega -exponent ((CantorNF (a (+) d)) . j) = omega -exponent (((CantorNF (a (+) d)) | i) . j) by FUNCT_1:47
.= omega -exponent ((CantorNF a) . j) by A59, A104
.= omega -exponent ((CantorNF (a (+) d)) . i) by A101, A103, Def1 ;
i in dom (CantorNF (a (+) d)) by A14, Th77, TARSKI:def 3;
then omega -exponent ((CantorNF (a (+) d)) . i) in omega -exponent ((CantorNF (a (+) d)) . j) by A102, ORDINAL5:def 11;
hence contradiction by A105; :: thesis:

end;

suppose j = i ; :: thesis:

hence contradiction by A100, A101; :: thesis:

end;

suppose j > i ; :: thesis:

proof

end;

then (omega -exponent (CantorNF a)) . i in rng (omega -exponent ((CantorNF (a (+) d)) /^ i)) by A25, A109, XBOOLE_0:def 5;
then consider k being object such that
A114: ( k in dom (omega -exponent ((CantorNF (a (+) d)) /^ i)) & (omega -exponent ((CantorNF (a (+) d)) /^ i)) . k = (omega -exponent (CantorNF a)) . i ) by FUNCT_1:def 3;
reconsider k = k as Nat by A114;
A115: k in dom ((CantorNF (a (+) d)) /^ i) by A114, Def1;
then A116: (omega -exponent (CantorNF a)) . i = omega -exponent (((CantorNF (a (+) d)) /^ i) . k) by A114, Def1
.= omega -exponent ((CantorNF (a (+) d)) . (k + i)) by A115, AFINSQ_2:def 2 ;

per cases ;

suppose k = 0 ; :: thesis:

hence contradiction by A108, A116; :: thesis:

end;

suppose 0 < k ; :: thesis:

end;

then omega -exponent ((CantorNF (a (+) d)) . i) c= omega -exponent d by A14, Def1;
then A119: omega -exponent ((CantorNF (a (+) d)) . i) in omega -exponent d by A87, XBOOLE_0:def 8, ORDINAL1:11;
not omega -exponent d in rng (omega -exponent ((CantorNF (a (+) d)) | i))

proof

assume omega -exponent d in rng (omega -exponent ((CantorNF (a (+) d)) | i)) ; :: thesis:
then consider m being object such that
A121: ( m in dom (omega -exponent ((CantorNF (a (+) d)) | i)) & (omega -exponent ((CantorNF (a (+) d)) | i)) . m = omega -exponent d ) by FUNCT_1:def 3;
reconsider m = m as Nat by A121;
A122: m in dom ((CantorNF (a (+) d)) | i) by A121, Def1;
then A123: ( m in dom (CantorNF (a (+) d)) & m in i ) by RELAT_1:57;
omega -exponent d = omega -exponent (((CantorNF (a (+) d)) | i) . m) by A121, A122, Def1
.= omega -exponent ((CantorNF (a (+) d)) . m) by A122, FUNCT_1:47
.= (omega -exponent (CantorNF (a (+) d))) . m by A123, Def1 ;
then (omega -exponent (CantorNF a)) . m c= omega -exponent d by Th97;
then A125: omega -exponent ((CantorNF a) . m) c= omega -exponent d by A14, A123, Def1, ORDINAL1:10;
m in Segm i by A123;
then omega -exponent d in omega -exponent ((CantorNF a) . m) by A14, NAT_1:44;
then omega -exponent d in omega -exponent d by A125;
hence contradiction ; :: thesis:

end;

then omega -exponent d in rng (omega -exponent ((CantorNF (a (+) d)) /^ i)) by A18, A25, XBOOLE_0:def 5;
then consider m being object such that
A126: ( m in dom (omega -exponent ((CantorNF (a (+) d)) /^ i)) & (omega -exponent ((CantorNF (a (+) d)) /^ i)) . m = omega -exponent d ) by FUNCT_1:def 3;
reconsider m = m as Nat by A126;
A127: m in dom ((CantorNF (a (+) d)) /^ i) by A126, Def1;
then A128: omega -exponent d = omega -exponent (((CantorNF (a (+) d)) /^ i) . m) by A126, Def1
.= omega -exponent ((CantorNF (a (+) d)) . (m + i)) by A127, AFINSQ_2:def 2 ;

per cases ;

suppose m = 0 ; :: thesis:

hence contradiction by A119, A128; :: thesis:

end;

suppose m > 0 ; :: thesis:

end;

A131: ( omega -exponent b = omega -exponent d implies omega -exponent ((CantorNF (a (+) b)) . i) = omega -exponent d )

proof

assume A132: omega -exponent b = omega -exponent d ; :: thesis:

per cases ;

suppose b <> {} ; :: thesis:

proof

not omega -exponent ((CantorNF (a (+) b)) . i) in omega -exponent d

proof

assume A138: omega -exponent ((CantorNF (a (+) b)) . i) in omega -exponent d ; :: thesis:
consider j being object such that
A139: ( j in dom (omega -exponent (CantorNF (a (+) b))) & (omega -exponent (CantorNF (a (+) b))) . j = omega -exponent d ) by A135, FUNCT_1:def 3;
reconsider j = j as Nat by A139;
A140: j in dom (CantorNF (a (+) b)) by A139, Def1;
then A141: omega -exponent ((CantorNF (a (+) b)) . j) = omega -exponent d by A139, Def1;

per cases by ORDINAL1:14;

suppose A142: j in i ; :: thesis:

then A143: j in Segm i ;
(CantorNF a) . j = ((CantorNF (a (+) b)) | i) . j by A33, A140, A142, RELAT_1:57
.= (CantorNF (a (+) b)) . j by A142, FUNCT_1:49 ;
then A144: omega -exponent d = omega -exponent ((CantorNF a) . j) by A141;
omega -exponent d in omega -exponent ((CantorNF a) . j) by A14, A143, NAT_1:44;
hence contradiction by A144; :: thesis:

end;

suppose j = i ; :: thesis:

hence contradiction by A138, A141; :: thesis:

end;

suppose i in j ; :: thesis:

hence contradiction by A138, A140, A141, ORDINAL5:def 11; :: thesis:

end;

per cases ;

suppose k = 0 ; :: thesis:

hence contradiction by A148; :: thesis:

end;

suppose 0 < k ; :: thesis:

then 0 in Segm k by NAT_1:44;
hence contradiction by A146, A148, ORDINAL5:def 1; :: thesis:

end;

omega -exponent ((CantorNF (a (+) b)) . i) = (omega -exponent (CantorNF a)) . i

proof

per cases by XXREAL_0:1;

suppose j < i ; :: thesis:

end;

suppose j = i ; :: thesis:

hence contradiction by A150, A151; :: thesis:

end;

suppose j > i ; :: thesis:

proof

end;

then (omega -exponent (CantorNF a)) . i in rng (omega -exponent ((CantorNF (a (+) b)) /^ i)) by A28, A159, XBOOLE_0:def 5;
then consider k being object such that
A164: ( k in dom (omega -exponent ((CantorNF (a (+) b)) /^ i)) & (omega -exponent ((CantorNF (a (+) b)) /^ i)) . k = (omega -exponent (CantorNF a)) . i ) by FUNCT_1:def 3;
reconsider k = k as Nat by A164;
A165: k in dom ((CantorNF (a (+) b)) /^ i) by A164, Def1;
then A166: (omega -exponent (CantorNF a)) . i = omega -exponent (((CantorNF (a (+) b)) /^ i) . k) by A164, Def1
.= omega -exponent ((CantorNF (a (+) b)) . (k + i)) by A165, AFINSQ_2:def 2 ;

per cases ;

suppose k = 0 ; :: thesis:

hence contradiction by A158, A166; :: thesis:

end;

suppose 0 < k ; :: thesis:

end;

then omega -exponent ((CantorNF (a (+) b)) . i) c= omega -exponent d by A14, Def1;
then A169: omega -exponent ((CantorNF (a (+) b)) . i) in omega -exponent d by ORDINAL1:11, A136, XBOOLE_0:def 8;
not omega -exponent d in rng (omega -exponent ((CantorNF (a (+) b)) | i))

proof

assume omega -exponent d in rng (omega -exponent ((CantorNF (a (+) b)) | i)) ; :: thesis:
then consider m being object such that
A171: ( m in dom (omega -exponent ((CantorNF (a (+) b)) | i)) & (omega -exponent ((CantorNF (a (+) b)) | i)) . m = omega -exponent d ) by FUNCT_1:def 3;
reconsider m = m as Nat by A171;
A172: m in dom ((CantorNF (a (+) b)) | i) by A171, Def1;
then A173: ( m in dom (CantorNF (a (+) b)) & m in i ) by RELAT_1:57;
omega -exponent d = omega -exponent (((CantorNF (a (+) b)) | i) . m) by A171, A172, Def1
.= omega -exponent ((CantorNF (a (+) b)) . m) by A172, FUNCT_1:47
.= (omega -exponent (CantorNF (a (+) b))) . m by A173, Def1 ;
then (omega -exponent (CantorNF a)) . m c= omega -exponent d by Th97;
then A175: omega -exponent ((CantorNF a) . m) c= omega -exponent d by Def1, A14, A173, ORDINAL1:10;
m in Segm i by A173;
then omega -exponent d in omega -exponent ((CantorNF a) . m) by A14, NAT_1:44;
then omega -exponent d in omega -exponent d by A175;
hence contradiction ; :: thesis:

end;

then omega -exponent d in rng (omega -exponent ((CantorNF (a (+) b)) /^ i)) by A134, A28, XBOOLE_0:def 5;
then consider m being object such that
A176: ( m in dom (omega -exponent ((CantorNF (a (+) b)) /^ i)) & (omega -exponent ((CantorNF (a (+) b)) /^ i)) . m = omega -exponent d ) by FUNCT_1:def 3;
reconsider m = m as Nat by A176;
A177: m in dom ((CantorNF (a (+) b)) /^ i) by A176, Def1;
then A178: omega -exponent d = omega -exponent (((CantorNF (a (+) b)) /^ i) . m) by A176, Def1
.= omega -exponent ((CantorNF (a (+) b)) . (m + i)) by A177, AFINSQ_2:def 2 ;

per cases ;

suppose m = 0 ; :: thesis:

hence contradiction by A169, A178; :: thesis:

end;

suppose m > 0 ; :: thesis:

end;

suppose A181: b = {} ; :: thesis:

then A182: omega -exponent d = 0 by A132, ORDINAL5:def 10;
assume omega -exponent ((CantorNF (a (+) b)) . i) <> omega -exponent d ; :: thesis:
hence contradiction by A14, A182, A181, Th82; :: thesis:

end;

A183: Sum^ ((CantorNF (a (+) b)) /^ i) in (CantorNF (a (+) d)) . i

proof

per cases ) /^ i <> {} & omega -exponent d c= omega -exponent ((CantorNF a) . i) ) or ( (CantorNF (a (+) b)) /^ i <> {} & omega -exponent ((CantorNF a) . i) in omega -exponent d ) or (CantorNF (a (+) b)) /^ i = {} ) by ORDINAL1:16;

suppose A184: ( (CantorNF (a (+) b)) /^ i <> {} & omega -exponent d c= omega -exponent ((CantorNF a) . i) ) ; :: thesis:

per cases by ORDINAL1:16;

suppose A190: omega -exponent b in omega -exponent d ; :: thesis:

omega -exponent d c= (omega -exponent (CantorNF (a (+) b))) . i by A86, A186, Th97;
then A191: omega -exponent d c= omega -exponent ((CantorNF (a (+) b)) . i) by A22, Def1;
A192: not omega -exponent ((CantorNF (a (+) b)) . i) in rng (omega -exponent (CantorNF b))

proof

assume omega -exponent ((CantorNF (a (+) b)) . i) in rng (omega -exponent (CantorNF b)) ; :: thesis:
then consider j being object such that
A193: ( j in dom (omega -exponent (CantorNF b)) & (omega -exponent (CantorNF b)) . j = omega -exponent ((CantorNF (a (+) b)) . i) ) by FUNCT_1:def 3;
reconsider j = j as Nat by A193;
A194: j in dom (CantorNF b) by A193, Def1;

per cases ;

suppose j = 0 ; :: thesis:

then omega -exponent ((CantorNF (a (+) b)) . i) = omega -exponent ((CantorNF b) . 0) by A193, A194, Def1
.= omega -exponent (Sum^ (CantorNF b)) by Th44
.= omega -exponent b ;
hence contradiction by A190, A191, ORDINAL1:12; :: thesis:

end;

suppose 0 < j ; :: thesis:

then 0 in Segm j by NAT_1:44;
then omega -exponent ((CantorNF b) . j) in omega -exponent ((CantorNF b) . 0) by A194, ORDINAL5:def 11;
then omega -exponent ((CantorNF (a (+) b)) . i) in omega -exponent ((CantorNF b) . 0) by A193, A194, Def1;
then omega -exponent ((CantorNF (a (+) b)) . i) in omega -exponent (Sum^ (CantorNF b)) by Th44;
hence contradiction by A190, A191; :: thesis:

end;

proof

assume i <> j ; :: thesis:

per cases by XXREAL_0:1;

suppose i < j ; :: thesis:

then i in Segm j by NAT_1:44;
then omega -exponent ((CantorNF a) . j) in omega -exponent ((CantorNF a) . i) by A197, ORDINAL5:def 11;
then (omega -exponent (CantorNF a)) . j in omega -exponent ((CantorNF a) . i) by A197, Def1;
then omega -exponent ((CantorNF (a (+) b)) . i) in (omega -exponent (CantorNF a)) . i by A14, A196, Def1;
then (omega -exponent (CantorNF (a (+) b))) . i in (omega -exponent (CantorNF a)) . i by A22, Def1;
then (omega -exponent (CantorNF (a (+) b))) . i in (omega -exponent (CantorNF (a (+) b))) . i by Th97, TARSKI:def 3;
hence contradiction ; :: thesis:

end;

suppose j < i ; :: thesis:

then j in Segm i by NAT_1:44;
then A199: j in i ;
j in dom (CantorNF (a (+) b)) by A197, Th77, TARSKI:def 3;
then (CantorNF a) . j = ((CantorNF (a (+) b)) | i) . j by A33, A199, RELAT_1:57
.= (CantorNF (a (+) b)) . j by A199, FUNCT_1:49 ;
then A200: omega -exponent ((CantorNF (a (+) b)) . j) = omega -exponent ((CantorNF (a (+) b)) . i) by A196, A197, Def1;
omega -exponent ((CantorNF (a (+) b)) . i) in omega -exponent ((CantorNF (a (+) b)) . j) by A22, A199, ORDINAL5:def 11;
hence contradiction by A200; :: thesis:

end;

end;

suppose omega -exponent d c= omega -exponent b ; :: thesis:

then A206: omega -exponent d = omega -exponent b by A2, XBOOLE_0:def 10;
then A207: omega -exponent ((CantorNF (a (+) b)) . i) = omega -exponent d by A131;
A208: 0 in dom ((CantorNF (a (+) b)) /^ i) by A184, XBOOLE_1:61, ORDINAL1:11;
exp (omega,(omega -exponent b0)) = exp (omega,(omega -exponent (((CantorNF (a (+) b)) /^ i) . 0))) by A185, AFINSQ_1:35
.= exp (omega,(omega -exponent ((CantorNF (a (+) b)) . (0 + i)))) by A208, AFINSQ_2:def 2
.= 1 *^ (exp (omega,(omega -exponent d))) by A131, A206, ORDINAL2:39 ;
then A209: Sum^ B0 in 1 *^ (exp (omega,(omega -exponent d))) by A185, Th43;
A210: omega -exponent ((CantorNF (a (+) b)) . i) = omega -exponent ((CantorNF a) . i) by A14, A131, A184, A206, XBOOLE_0:def 10
.= (omega -exponent (CantorNF a)) . i by A14, Def1 ;
then A211: omega -exponent ((CantorNF (a (+) b)) . i) in rng (omega -exponent (CantorNF a)) by A21, FUNCT_1:3;

per cases ;

suppose b <> {} ; :: thesis:

proof

assume not (omega -leading_coeff (CantorNF b)) . 0 in (omega -leading_coeff (CantorNF d)) . 0 ; :: thesis:
then A217: (omega -leading_coeff (CantorNF d)) . 0 c= (omega -leading_coeff (CantorNF b)) . 0 by ORDINAL1:16;
then 0 in dom (omega -leading_coeff (CantorNF b)) by FUNCT_1:def 2, A189;
then A218: 0 in dom (CantorNF b) by Def3;
(omega -leading_coeff (CantorNF d)) . 0 in (omega -leading_coeff (CantorNF b)) . 0

proof

assume not (omega -leading_coeff (CantorNF d)) . 0 in (omega -leading_coeff (CantorNF b)) . 0 ; :: thesis:
then (omega -leading_coeff (CantorNF b)) . 0 c= (omega -leading_coeff (CantorNF d)) . 0 by ORDINAL1:16;
then (omega -leading_coeff (CantorNF b)) . 0 = (omega -leading_coeff (CantorNF d)) . 0 by A217, XBOOLE_0:def 10;
then (CantorNF d) . 0 = ((omega -leading_coeff (CantorNF b)) . 0) *^ (exp (omega,(omega -exponent d))) by A15, A20, Th65
.= (CantorNF b) . 0 by A215, A218, Th65 ;
hence contradiction by A1; :: thesis:

end;

end;

end;

suppose b = {} ; :: thesis:

end;

suppose A225: ( (CantorNF (a (+) b)) /^ i <> {} & omega -exponent ((CantorNF a) . i) in omega -exponent d ) ; :: thesis:

A226: (CantorNF (a (+) d)) . i is Cantor-component by A22, ORDINAL5:def 11;

per cases by ORDINAL1:16;

suppose A227: omega -exponent b in omega -exponent d ; :: thesis:

A228: omega -exponent ((CantorNF (a (+) b)) . i) in omega -exponent d

proof

assume not omega -exponent ((CantorNF (a (+) b)) . i) in omega -exponent d ; :: thesis:
then A229: omega -exponent d c= omega -exponent ((CantorNF (a (+) b)) . i) by ORDINAL1:16;
i in dom (omega -exponent (CantorNF (a (+) b))) by A22, Def1;
then (omega -exponent (CantorNF (a (+) b))) . i in rng (omega -exponent (CantorNF (a (+) b))) by FUNCT_1:3;
then omega -exponent ((CantorNF (a (+) b)) . i) in rng (omega -exponent (CantorNF (a (+) b))) by A22, Def1;
then omega -exponent ((CantorNF (a (+) b)) . i) in (rng (omega -exponent (CantorNF a))) \/ (rng (omega -exponent (CantorNF b))) by Th76;

per cases by XBOOLE_0:def 3;

suppose omega -exponent ((CantorNF (a (+) b)) . i) in rng (omega -exponent (CantorNF a)) ; :: thesis:

then consider j being object such that
A230: ( j in dom (omega -exponent (CantorNF a)) & (omega -exponent (CantorNF a)) . j = omega -exponent ((CantorNF (a (+) b)) . i) ) by FUNCT_1:def 3;
reconsider j = j as Nat by A230;
A231: j in dom (CantorNF a) by A230, Def1;
then A232: j in dom (CantorNF (a (+) b)) by Th77, TARSKI:def 3;
A233: omega -exponent ((CantorNF (a (+) b)) . i) = omega -exponent ((CantorNF a) . j) by A230, A231, Def1;

per cases by ORDINAL1:14;

suppose A234: j in i ; :: thesis:

then (CantorNF a) . j = ((CantorNF (a (+) b)) | i) . j by A33, A232, RELAT_1:57
.= (CantorNF (a (+) b)) . j by A234, FUNCT_1:49 ;
then A235: omega -exponent ((CantorNF (a (+) b)) . i) = omega -exponent ((CantorNF (a (+) b)) . j) by A233;
omega -exponent ((CantorNF (a (+) b)) . i) in omega -exponent ((CantorNF (a (+) b)) . j) by A22, A234, ORDINAL5:def 11;
hence contradiction by A235; :: thesis:

end;

suppose j = i ; :: thesis:

hence contradiction by A225, A229, A233, ORDINAL1:12; :: thesis:

end;

suppose i in j ; :: thesis:

then omega -exponent ((CantorNF a) . j) in omega -exponent ((CantorNF a) . i) by A231, ORDINAL5:def 11;
hence contradiction by A229, A233, A225; :: thesis:

end;

suppose omega -exponent ((CantorNF (a (+) b)) . i) in rng (omega -exponent (CantorNF b)) ; :: thesis:

then consider j being object such that
A236: ( j in dom (omega -exponent (CantorNF b)) & (omega -exponent (CantorNF b)) . j = omega -exponent ((CantorNF (a (+) b)) . i) ) by FUNCT_1:def 3;
reconsider j = j as Nat by A236;
A237: j in dom (CantorNF b) by A236, Def1;
then A238: omega -exponent ((CantorNF (a (+) b)) . i) = omega -exponent ((CantorNF b) . j) by A236, Def1;

per cases ;

suppose j = 0 ; :: thesis:

then omega -exponent ((CantorNF (a (+) b)) . i) = omega -exponent (Sum^ (CantorNF b)) by A238, Th44
.= omega -exponent b ;
hence contradiction by A227, A229, ORDINAL1:12; :: thesis:

end;

suppose 0 < j ; :: thesis:

then 0 in Segm j by NAT_1:44;
then omega -exponent ((CantorNF (a (+) b)) . i) in omega -exponent ((CantorNF b) . 0) by A237, A238, ORDINAL5:def 11;
then omega -exponent ((CantorNF (a (+) b)) . i) in omega -exponent (Sum^ (CantorNF b)) by Th44;
hence contradiction by A227, A229; :: thesis:

end;

now :: thesis:

let j be Ordinal; :: thesis:
assume A239: j in dom ((CantorNF (a (+) b)) /^ i) ; :: thesis:
then reconsider m = j as Nat ;
A240: ((CantorNF (a (+) b)) /^ i) . j is Cantor-component by A239, ORDINAL5:def 11;

per cases ;

suppose m = 0 ; :: thesis:

then omega -exponent (((CantorNF (a (+) b)) /^ i) . m) = omega -exponent ((CantorNF (a (+) b)) . (0 + i)) by A239, AFINSQ_2:def 2;
then exp (omega,(omega -exponent (((CantorNF (a (+) b)) /^ i) . j))) in exp (omega,(omega -exponent d)) by A228, ORDINAL4:24;
then (omega -leading_coeff (((CantorNF (a (+) b)) /^ i) . j)) *^ (exp (omega,(omega -exponent (((CantorNF (a (+) b)) /^ i) . j)))) in exp (omega,(omega -exponent d)) by A240, Th42;
hence ((CantorNF (a (+) b)) /^ i) . j in exp (omega,(omega -exponent d)) by A240, Th59; :: thesis:

end;

suppose 0 < m ; :: thesis:

then 0 in Segm j by NAT_1:44;
then A242: 0 in j ;
0 in dom ((CantorNF (a (+) b)) /^ i) by A239, XBOOLE_1:61, ORDINAL1:11;
then ((CantorNF (a (+) b)) /^ i) . 0 = (CantorNF (a (+) b)) . (0 + i) by AFINSQ_2:def 2;
then omega -exponent (((CantorNF (a (+) b)) /^ i) . j) in omega -exponent ((CantorNF (a (+) b)) . i) by A239, A242, ORDINAL5:def 11;
then omega -exponent (((CantorNF (a (+) b)) /^ i) . j) in omega -exponent d by A228, ORDINAL1:10;
then exp (omega,(omega -exponent (((CantorNF (a (+) b)) /^ i) . j))) in exp (omega,(omega -exponent d)) by ORDINAL4:24;
then (omega -leading_coeff (((CantorNF (a (+) b)) /^ i) . j)) *^ (exp (omega,(omega -exponent (((CantorNF (a (+) b)) /^ i) . j)))) in exp (omega,(omega -exponent d)) by A240, Th42;
hence ((CantorNF (a (+) b)) /^ i) . j in exp (omega,(omega -exponent d)) by A240, Th59; :: thesis:

end;

then Sum^ ((CantorNF (a (+) b)) /^ i) in exp (omega,(omega -exponent ((CantorNF (a (+) d)) . i))) by A86, Th41;
then Sum^ ((CantorNF (a (+) b)) /^ i) in (omega -leading_coeff ((CantorNF (a (+) d)) . i)) *^ (exp (omega,(omega -exponent ((CantorNF (a (+) d)) . i)))) by A226, ORDINAL3:32;
hence Sum^ ((CantorNF (a (+) b)) /^ i) in (CantorNF (a (+) d)) . i by A226, Th59; :: thesis:

end;

suppose omega -exponent d c= omega -exponent b ; :: thesis:

then A243: omega -exponent b = omega -exponent d by A2, XBOOLE_0:def 10;
then A244: omega -exponent ((CantorNF (a (+) b)) . i) = omega -exponent d by A131;
A245: not omega -exponent d in rng (omega -exponent (CantorNF a))

proof

assume omega -exponent d in rng (omega -exponent (CantorNF a)) ; :: thesis:
then consider j being object such that
A246: ( j in dom (omega -exponent (CantorNF a)) & (omega -exponent (CantorNF a)) . j = omega -exponent d ) by FUNCT_1:def 3;
reconsider j = j as Nat by A246;
A247: j in dom (CantorNF a) by A246, Def1;
then A248: omega -exponent ((CantorNF a) . j) = omega -exponent d by A246, Def1;

per cases by ORDINAL1:14;

suppose i in j ; :: thesis:

hence contradiction by A225, A247, A248, ORDINAL5:def 11; :: thesis:

end;

suppose i = j ; :: thesis:

hence contradiction by A225, A248; :: thesis:

end;

suppose j in i ; :: thesis:

then j in Segm i ;
then omega -exponent d in omega -exponent ((CantorNF a) . j) by A14, NAT_1:44;
hence contradiction by A248; :: thesis:

end;

proof

assume not (omega -leading_coeff (CantorNF b)) . 0 in (omega -leading_coeff (CantorNF d)) . 0 ; :: thesis:
then A255: (omega -leading_coeff (CantorNF d)) . 0 c= (omega -leading_coeff (CantorNF b)) . 0 by ORDINAL1:16;
(omega -leading_coeff (CantorNF d)) . 0 in (omega -leading_coeff (CantorNF b)) . 0

proof

assume not (omega -leading_coeff (CantorNF d)) . 0 in (omega -leading_coeff (CantorNF b)) . 0 ; :: thesis:
then (omega -leading_coeff (CantorNF b)) . 0 c= (omega -leading_coeff (CantorNF d)) . 0 by ORDINAL1:16;
then A256: (omega -leading_coeff (CantorNF b)) . 0 = (omega -leading_coeff (CantorNF d)) . 0 by A255, XBOOLE_0:def 10;
(CantorNF b) . 0 = ((omega -leading_coeff (CantorNF b)) . 0) *^ (exp (omega,((omega -exponent (CantorNF b)) . 0))) by A250, Th65
.= (CantorNF d) . 0 by A15, A20, A252, A256, Th65 ;
hence contradiction by A1; :: thesis:

end;

end;

end;

suppose (CantorNF (a (+) b)) /^ i = {} ; :: thesis:

hence Sum^ ((CantorNF (a (+) b)) /^ i) in (CantorNF (a (+) d)) . i by A22, XBOOLE_1:61, ORDINAL1:11, ORDINAL5:52; :: thesis:

end;

i in Segm (dom (CantorNF (a (+) d))) by A14, Th77, TARSKI:def 3;
then 0 + i < len (CantorNF (a (+) d)) by NAT_1:44;
then Sum^ ((CantorNF (a (+) b)) /^ i) in ((CantorNF (a (+) d)) /^ i) . 0 by A183, AFINSQ_2:8;
then Sum^ ((CantorNF (a (+) b)) /^ i) in Sum^ ((CantorNF (a (+) d)) /^ i) by ORDINAL5:56, TARSKI:def 3;
then A265: (Sum^ ((CantorNF (a (+) b)) | i)) +^ (Sum^ ((CantorNF (a (+) b)) /^ i)) in (Sum^ ((CantorNF (a (+) d)) | i)) +^ (Sum^ ((CantorNF (a (+) d)) /^ i)) by A85, ORDINAL2:32;
A266: a (+) b = Sum^ (((CantorNF (a (+) b)) | i) ^ ((CantorNF (a (+) b)) /^ i))
.= (Sum^ ((CantorNF (a (+) b)) | i)) +^ (Sum^ ((CantorNF (a (+) b)) /^ i)) by Th24 ;
a (+) d = Sum^ (((CantorNF (a (+) d)) | i) ^ ((CantorNF (a (+) d)) /^ i))
.= (Sum^ ((CantorNF (a (+) d)) | i)) +^ (Sum^ ((CantorNF (a (+) d)) /^ i)) by Th24 ;
hence a (+) b in a (+) d by A265, A266; :: thesis:

end;