let a, b, c be Ordinal; ( a (+) b = a (+) c implies b = c )
assume A1:
a (+) b = a (+) c
; b = c
set C1 = CantorNF (a (+) b);
set C2 = CantorNF (a (+) c);
set E1 = omega -exponent (CantorNF a);
set E2 = omega -exponent (CantorNF b);
set E3 = omega -exponent (CantorNF c);
set L1 = omega -leading_coeff (CantorNF a);
set L2 = omega -leading_coeff (CantorNF b);
set L3 = omega -leading_coeff (CantorNF c);
A2:
rng (omega -exponent (CantorNF b)) = rng (omega -exponent (CantorNF c))
proof
assume
rng (omega -exponent (CantorNF b)) <> rng (omega -exponent (CantorNF c))
;
contradiction
per cases then
( not rng (omega -exponent (CantorNF b)) c= rng (omega -exponent (CantorNF c)) or not rng (omega -exponent (CantorNF c)) c= rng (omega -exponent (CantorNF b)) )
by XBOOLE_0:def 10;
suppose
not
rng (omega -exponent (CantorNF b)) c= rng (omega -exponent (CantorNF c))
;
contradictionthen consider y being
object such that A3:
(
y in rng (omega -exponent (CantorNF b)) & not
y in rng (omega -exponent (CantorNF c)) )
by TARSKI:def 3;
y in (rng (omega -exponent (CantorNF a))) \/ (rng (omega -exponent (CantorNF b)))
by A3, XBOOLE_0:def 3;
then A4:
y in rng (omega -exponent (CantorNF (a (+) b)))
by Th76;
then consider x being
object such that A5:
(
x in dom (omega -exponent (CantorNF (a (+) b))) &
(omega -exponent (CantorNF (a (+) b))) . x = y )
by FUNCT_1:def 3;
A6:
x in dom (CantorNF (a (+) b))
by A5, Def1;
then A7:
y = omega -exponent ((CantorNF (a (+) b)) . x)
by A5, Def1;
A8:
omega -exponent ((CantorNF (a (+) b)) . x) in rng (omega -exponent (CantorNF a))
then
omega -exponent ((CantorNF (a (+) b)) . x) in (rng (omega -exponent (CantorNF a))) /\ (rng (omega -exponent (CantorNF b)))
by A3, A7, XBOOLE_0:def 4;
then A9:
omega -leading_coeff ((CantorNF (a (+) b)) . x) = ((omega -leading_coeff (CantorNF a)) . (((omega -exponent (CantorNF a)) ") . (omega -exponent ((CantorNF (a (+) b)) . x)))) + ((omega -leading_coeff (CantorNF b)) . (((omega -exponent (CantorNF b)) ") . (omega -exponent ((CantorNF (a (+) b)) . x))))
by A6, Th80;
omega -exponent ((CantorNF (a (+) b)) . x) in (rng (omega -exponent (CantorNF a))) \ (rng (omega -exponent (CantorNF c)))
by A3, A7, A8, XBOOLE_0:def 5;
then
omega -leading_coeff ((CantorNF (a (+) b)) . x) = ((omega -leading_coeff (CantorNF a)) . (((omega -exponent (CantorNF a)) ") . (omega -exponent ((CantorNF (a (+) b)) . x)))) + 0
by A1, A6, Th78;
then A10:
0 = (omega -leading_coeff (CantorNF b)) . (((omega -exponent (CantorNF b)) ") . y)
by A7, A9;
y in dom ((omega -exponent (CantorNF b)) ")
by A3, FUNCT_1:33;
then
((omega -exponent (CantorNF b)) ") . y in rng ((omega -exponent (CantorNF b)) ")
by FUNCT_1:3;
then
((omega -exponent (CantorNF b)) ") . y in dom (omega -exponent (CantorNF b))
by FUNCT_1:33;
then
((omega -exponent (CantorNF b)) ") . y in dom (CantorNF b)
by Def1;
then
((omega -exponent (CantorNF b)) ") . y in dom (omega -leading_coeff (CantorNF b))
by Def3;
hence
contradiction
by A10, FUNCT_1:def 9;
verum end; suppose
not
rng (omega -exponent (CantorNF c)) c= rng (omega -exponent (CantorNF b))
;
contradictionthen consider y being
object such that A11:
(
y in rng (omega -exponent (CantorNF c)) & not
y in rng (omega -exponent (CantorNF b)) )
by TARSKI:def 3;
y in (rng (omega -exponent (CantorNF a))) \/ (rng (omega -exponent (CantorNF c)))
by A11, XBOOLE_0:def 3;
then A12:
y in rng (omega -exponent (CantorNF (a (+) c)))
by Th76;
then consider x being
object such that A13:
(
x in dom (omega -exponent (CantorNF (a (+) c))) &
(omega -exponent (CantorNF (a (+) c))) . x = y )
by FUNCT_1:def 3;
A14:
x in dom (CantorNF (a (+) c))
by A13, Def1;
then A15:
y = omega -exponent ((CantorNF (a (+) c)) . x)
by A13, Def1;
A16:
omega -exponent ((CantorNF (a (+) c)) . x) in rng (omega -exponent (CantorNF a))
then
omega -exponent ((CantorNF (a (+) c)) . x) in (rng (omega -exponent (CantorNF a))) /\ (rng (omega -exponent (CantorNF c)))
by A11, A15, XBOOLE_0:def 4;
then A17:
omega -leading_coeff ((CantorNF (a (+) c)) . x) = ((omega -leading_coeff (CantorNF a)) . (((omega -exponent (CantorNF a)) ") . (omega -exponent ((CantorNF (a (+) c)) . x)))) + ((omega -leading_coeff (CantorNF c)) . (((omega -exponent (CantorNF c)) ") . (omega -exponent ((CantorNF (a (+) c)) . x))))
by A14, Th80;
omega -exponent ((CantorNF (a (+) c)) . x) in (rng (omega -exponent (CantorNF a))) \ (rng (omega -exponent (CantorNF b)))
by A11, A15, A16, XBOOLE_0:def 5;
then
omega -leading_coeff ((CantorNF (a (+) c)) . x) = ((omega -leading_coeff (CantorNF a)) . (((omega -exponent (CantorNF a)) ") . (omega -exponent ((CantorNF (a (+) c)) . x)))) + 0
by A1, A14, Th78;
then A18:
0 = (omega -leading_coeff (CantorNF c)) . (((omega -exponent (CantorNF c)) ") . y)
by A15, A17;
y in dom ((omega -exponent (CantorNF c)) ")
by A11, FUNCT_1:33;
then
((omega -exponent (CantorNF c)) ") . y in rng ((omega -exponent (CantorNF c)) ")
by FUNCT_1:3;
then
((omega -exponent (CantorNF c)) ") . y in dom (omega -exponent (CantorNF c))
by FUNCT_1:33;
then
((omega -exponent (CantorNF c)) ") . y in dom (CantorNF c)
by Def1;
then
((omega -exponent (CantorNF c)) ") . y in dom (omega -leading_coeff (CantorNF c))
by Def3;
hence
contradiction
by A18, FUNCT_1:def 9;
verum end; end;
end;
then A19:
omega -exponent (CantorNF b) = omega -exponent (CantorNF c)
by Th34;
A20: dom (omega -leading_coeff (CantorNF b)) =
dom (CantorNF b)
by Def3
.=
card (dom (omega -exponent (CantorNF b)))
by Def1
.=
card (rng (omega -exponent (CantorNF b)))
by CARD_1:70
.=
card (dom (omega -exponent (CantorNF c)))
by A2, CARD_1:70
.=
dom (CantorNF c)
by Def1
.=
dom (omega -leading_coeff (CantorNF c))
by Def3
;
for x being object st x in dom (omega -leading_coeff (CantorNF b)) holds
(omega -leading_coeff (CantorNF b)) . x = (omega -leading_coeff (CantorNF c)) . x
proof
let x be
object ;
( x in dom (omega -leading_coeff (CantorNF b)) implies (omega -leading_coeff (CantorNF b)) . x = (omega -leading_coeff (CantorNF c)) . x )
assume
x in dom (omega -leading_coeff (CantorNF b))
;
(omega -leading_coeff (CantorNF b)) . x = (omega -leading_coeff (CantorNF c)) . x
then
x in dom (CantorNF b)
by Def3;
then A21:
x in dom (omega -exponent (CantorNF b))
by Def1;
then A22:
(omega -exponent (CantorNF b)) . x in rng (omega -exponent (CantorNF b))
by FUNCT_1:3;
then
(omega -exponent (CantorNF b)) . x in (rng (omega -exponent (CantorNF a))) \/ (rng (omega -exponent (CantorNF b)))
by XBOOLE_0:def 3;
then
(omega -exponent (CantorNF b)) . x in rng (omega -exponent (CantorNF (a (+) b)))
by Th76;
then consider y being
object such that A23:
(
y in dom (omega -exponent (CantorNF (a (+) b))) &
(omega -exponent (CantorNF (a (+) b))) . y = (omega -exponent (CantorNF b)) . x )
by FUNCT_1:def 3;
A24:
y in dom (CantorNF (a (+) b))
by A23, Def1;
then A25:
omega -exponent ((CantorNF (a (+) b)) . y) = (omega -exponent (CantorNF b)) . x
by A23, Def1;
per cases
( omega -exponent ((CantorNF (a (+) b)) . y) in rng (omega -exponent (CantorNF a)) or not omega -exponent ((CantorNF (a (+) b)) . y) in rng (omega -exponent (CantorNF a)) )
;
suppose
omega -exponent ((CantorNF (a (+) b)) . y) in rng (omega -exponent (CantorNF a))
;
(omega -leading_coeff (CantorNF b)) . x = (omega -leading_coeff (CantorNF c)) . xthen A26:
omega -exponent ((CantorNF (a (+) b)) . y) in (rng (omega -exponent (CantorNF a))) /\ (rng (omega -exponent (CantorNF b)))
by A22, A25, XBOOLE_0:def 4;
then A27:
omega -exponent ((CantorNF (a (+) c)) . y) in (rng (omega -exponent (CantorNF a))) /\ (rng (omega -exponent (CantorNF c)))
by A1, A2;
((omega -leading_coeff (CantorNF a)) . (((omega -exponent (CantorNF a)) ") . ((omega -exponent (CantorNF b)) . x))) + ((omega -leading_coeff (CantorNF b)) . (((omega -exponent (CantorNF b)) ") . ((omega -exponent (CantorNF b)) . x))) =
omega -leading_coeff ((CantorNF (a (+) b)) . y)
by A24, A25, A26, Th80
.=
((omega -leading_coeff (CantorNF a)) . (((omega -exponent (CantorNF a)) ") . ((omega -exponent (CantorNF b)) . x))) + ((omega -leading_coeff (CantorNF c)) . (((omega -exponent (CantorNF c)) ") . ((omega -exponent (CantorNF b)) . x)))
by A1, A24, A25, A27, Th80
;
hence (omega -leading_coeff (CantorNF b)) . x =
(omega -leading_coeff (CantorNF c)) . (((omega -exponent (CantorNF c)) ") . ((omega -exponent (CantorNF b)) . x))
by A21, FUNCT_1:34
.=
(omega -leading_coeff (CantorNF c)) . x
by A19, A21, FUNCT_1:34
;
verum end; suppose
not
omega -exponent ((CantorNF (a (+) b)) . y) in rng (omega -exponent (CantorNF a))
;
(omega -leading_coeff (CantorNF b)) . x = (omega -leading_coeff (CantorNF c)) . xthen A29:
omega -exponent ((CantorNF (a (+) b)) . y) in (rng (omega -exponent (CantorNF b))) \ (rng (omega -exponent (CantorNF a)))
by A22, A25, XBOOLE_0:def 5;
then A30:
omega -exponent ((CantorNF (a (+) c)) . y) in (rng (omega -exponent (CantorNF c))) \ (rng (omega -exponent (CantorNF a)))
by A1, A2;
thus (omega -leading_coeff (CantorNF b)) . x =
(omega -leading_coeff (CantorNF b)) . (((omega -exponent (CantorNF b)) ") . ((omega -exponent (CantorNF b)) . x))
by A21, FUNCT_1:34
.=
omega -leading_coeff ((CantorNF (a (+) b)) . y)
by A24, A25, A29, Th79
.=
(omega -leading_coeff (CantorNF c)) . (((omega -exponent (CantorNF c)) ") . ((omega -exponent (CantorNF b)) . x))
by A1, A24, A25, A30, Th79
.=
(omega -leading_coeff (CantorNF c)) . x
by A19, A21, FUNCT_1:34
;
verum end; end;
end;
then
omega -leading_coeff (CantorNF b) = omega -leading_coeff (CantorNF c)
by A20, FUNCT_1:2;
then
Sum^ (CantorNF b) = Sum^ (CantorNF c)
by A19, Th67;
hence
b = c
; verum