defpred S1[ Nat] means for A, B being Cantor-normal-form Ordinal-Sequence st (dom A) \/ (dom B) = $1 & Sum^ A = Sum^ B holds
A = B;
A1:
S1[ 0 ]
A2:
for n being Nat st S1[n] holds
S1[n + 1]
proof
let n be
Nat;
( S1[n] implies S1[n + 1] )
assume A3:
S1[
n]
;
S1[n + 1]
let A,
B be
Cantor-normal-form Ordinal-Sequence;
( (dom A) \/ (dom B) = n + 1 & Sum^ A = Sum^ B implies A = B )
assume A4:
(
(dom A) \/ (dom B) = n + 1 &
Sum^ A = Sum^ B )
;
A = B
dom A <> {}
then A6:
A <> {}
;
dom B <> {}
then
B <> {}
;
then consider b being
Cantor-component Ordinal,
B0 being
Cantor-normal-form Ordinal-Sequence such that A7:
B = <%b%> ^ B0
by ORDINAL5:67;
consider a being
Cantor-component Ordinal,
A0 being
Cantor-normal-form Ordinal-Sequence such that A8:
A = <%a%> ^ A0
by A6, ORDINAL5:67;
A9:
a +^ (Sum^ A0) =
Sum^ B
by A4, A8, ORDINAL5:55
.=
b +^ (Sum^ B0)
by A7, ORDINAL5:55
;
A10:
a = b
proof
A11:
(
A . 0 = a &
B . 0 = b )
by A7, A8, AFINSQ_1:35;
then A12:
omega -exponent a =
omega -exponent (Sum^ B)
by A4, Th44
.=
omega -exponent b
by A11, Th44
;
consider d1 being
Ordinal,
n1 being
Nat such that A13:
(
0 in Segm n1 &
a = n1 *^ (exp (omega,d1)) )
by ORDINAL5:def 9;
consider d2 being
Ordinal,
n2 being
Nat such that A14:
(
0 in Segm n2 &
b = n2 *^ (exp (omega,d2)) )
by ORDINAL5:def 9;
(
0 in n1 &
n1 in omega )
by A13, ORDINAL1:def 12;
then A15:
omega -exponent a = d1
by A13, ORDINAL5:58;
(
0 in n2 &
n2 in omega )
by A14, ORDINAL1:def 12;
then A16:
omega -exponent b = d2
by A14, ORDINAL5:58;
then A17:
d1 = d2
by A12, A15;
assume
a <> b
;
contradiction
per cases then
( a in b or b in a )
by ORDINAL1:14;
suppose A18:
a in b
;
contradictionthen a +^ (Sum^ A0) =
(a +^ (b -^ a)) +^ (Sum^ B0)
by A9, ORDINAL3:51
.=
a +^ ((b -^ a) +^ (Sum^ B0))
by ORDINAL3:30
;
then A19:
Sum^ A0 = (b -^ a) +^ (Sum^ B0)
by ORDINAL3:21;
A20:
n1 in n2
by A13, A14, A17, A18, ORDINAL3:34;
A21:
b -^ a = (n2 -^ n1) *^ (exp (omega,d1))
by A13, A14, A17, ORDINAL3:63;
(
0 in n2 -^ n1 &
n2 -^ n1 in omega )
by A20, ORDINAL3:55, ORDINAL1:def 12;
then A22:
omega -exponent (b -^ a) = d1
by A21, ORDINAL5:58;
A23:
b -^ a c= (b -^ a) +^ (Sum^ B0)
by ORDINAL3:24;
then A24:
d1 c= omega -exponent (Sum^ A0)
by A19, A22, Th22;
0 in b -^ a
by A18, ORDINAL3:55;
then A25:
0 in Sum^ A0
by A19, A23;
Sum^ A0 in exp (
omega,
(omega -exponent a))
by A8, Th43;
hence
contradiction
by A15, A24, A25, Th23, ORDINAL1:5;
verum end; suppose A26:
b in a
;
contradictionthen b +^ (Sum^ B0) =
(b +^ (a -^ b)) +^ (Sum^ A0)
by A9, ORDINAL3:51
.=
b +^ ((a -^ b) +^ (Sum^ A0))
by ORDINAL3:30
;
then A27:
Sum^ B0 = (a -^ b) +^ (Sum^ A0)
by ORDINAL3:21;
A28:
n2 in n1
by A13, A14, A17, A26, ORDINAL3:34;
A29:
a -^ b = (n1 -^ n2) *^ (exp (omega,d1))
by A13, A14, A17, ORDINAL3:63;
(
0 in n1 -^ n2 &
n1 -^ n2 in omega )
by A28, ORDINAL3:55, ORDINAL1:def 12;
then A30:
omega -exponent (a -^ b) = d1
by A29, ORDINAL5:58;
A31:
a -^ b c= (a -^ b) +^ (Sum^ A0)
by ORDINAL3:24;
then A32:
d1 c= omega -exponent (Sum^ B0)
by A27, A30, Th22;
0 in a -^ b
by A26, ORDINAL3:55;
then A33:
0 in Sum^ B0
by A27, A31;
Sum^ B0 in exp (
omega,
(omega -exponent b))
by A7, Th43;
hence
contradiction
by A16, A17, A32, A33, Th23, ORDINAL1:5;
verum end;
end;
then A34:
Sum^ A0 = Sum^ B0
by A9, ORDINAL3:21;
(dom A0) \/ (dom B0) =
((max ((len A0),(len B0))) + 1) - 1
.=
(max (((len A0) + 1),((len B0) + 1))) - 1
by FUZZY_2:42
.=
(max (((len A0) + (len <%a%>)),((len B0) + 1))) - 1
by AFINSQ_1:34
.=
(max (((len A0) + (len <%a%>)),((len B0) + (len <%b%>)))) - 1
by AFINSQ_1:34
.=
(max ((len A),((len B0) + (len <%b%>)))) - 1
by A8, AFINSQ_1:17
.=
(max ((len A),(len B))) - 1
by A7, AFINSQ_1:17
.=
n
by A4
;
hence
A = B
by A3, A7, A8, A10, A34;
verum
end;
A35:
for n being Nat holds S1[n]
from NAT_1:sch 2(A1, A2);
let A, B be Cantor-normal-form Ordinal-Sequence; ( Sum^ A = Sum^ B implies A = B )
assume A36:
Sum^ A = Sum^ B
; A = B
(dom A) \/ (dom B) is natural
;
hence
A = B
by A35, A36; verum