let s1, s2 be Ordinal; :: thesis: ( ex C being Cantor-normal-form Ordinal-Sequence st
( s1 = Sum^ C & rng (omega -exponent C) = (rng (omega -exponent (CantorNF a))) \/ (rng (omega -exponent (CantorNF b))) & ( for d being object st d in dom C holds
( ( omega -exponent (C . d) in (rng (omega -exponent (CantorNF a))) \ (rng (omega -exponent (CantorNF b))) implies omega -leading_coeff (C . d) = (omega -leading_coeff (CantorNF a)) . (((omega -exponent (CantorNF a)) ") . (omega -exponent (C . d))) ) & ( omega -exponent (C . d) in (rng (omega -exponent (CantorNF b))) \ (rng (omega -exponent (CantorNF a))) implies omega -leading_coeff (C . d) = (omega -leading_coeff (CantorNF b)) . (((omega -exponent (CantorNF b)) ") . (omega -exponent (C . d))) ) & ( omega -exponent (C . d) in (rng (omega -exponent (CantorNF a))) /\ (rng (omega -exponent (CantorNF b))) implies omega -leading_coeff (C . d) = ((omega -leading_coeff (CantorNF a)) . (((omega -exponent (CantorNF a)) ") . (omega -exponent (C . d)))) + ((omega -leading_coeff (CantorNF b)) . (((omega -exponent (CantorNF b)) ") . (omega -exponent (C . d)))) ) ) ) ) & ex C being Cantor-normal-form Ordinal-Sequence st
( s2 = Sum^ C & rng (omega -exponent C) = (rng (omega -exponent (CantorNF a))) \/ (rng (omega -exponent (CantorNF b))) & ( for d being object st d in dom C holds
( ( omega -exponent (C . d) in (rng (omega -exponent (CantorNF a))) \ (rng (omega -exponent (CantorNF b))) implies omega -leading_coeff (C . d) = (omega -leading_coeff (CantorNF a)) . (((omega -exponent (CantorNF a)) ") . (omega -exponent (C . d))) ) & ( omega -exponent (C . d) in (rng (omega -exponent (CantorNF b))) \ (rng (omega -exponent (CantorNF a))) implies omega -leading_coeff (C . d) = (omega -leading_coeff (CantorNF b)) . (((omega -exponent (CantorNF b)) ") . (omega -exponent (C . d))) ) & ( omega -exponent (C . d) in (rng (omega -exponent (CantorNF a))) /\ (rng (omega -exponent (CantorNF b))) implies omega -leading_coeff (C . d) = ((omega -leading_coeff (CantorNF a)) . (((omega -exponent (CantorNF a)) ") . (omega -exponent (C . d)))) + ((omega -leading_coeff (CantorNF b)) . (((omega -exponent (CantorNF b)) ") . (omega -exponent (C . d)))) ) ) ) ) implies s1 = s2 )
set E1 = omega -exponent (CantorNF a);
set E2 = omega -exponent (CantorNF b);
set L1 = omega -leading_coeff (CantorNF a);
set L2 = omega -leading_coeff (CantorNF b);
assume that
A32: ex C being Cantor-normal-form Ordinal-Sequence st
( s1 = Sum^ C & rng (omega -exponent C) = (rng (omega -exponent (CantorNF a))) \/ (rng (omega -exponent (CantorNF b))) & ( for d being object st d in dom C holds
( ( omega -exponent (C . d) in (rng (omega -exponent (CantorNF a))) \ (rng (omega -exponent (CantorNF b))) implies omega -leading_coeff (C . d) = (omega -leading_coeff (CantorNF a)) . (((omega -exponent (CantorNF a)) ") . (omega -exponent (C . d))) ) & ( omega -exponent (C . d) in (rng (omega -exponent (CantorNF b))) \ (rng (omega -exponent (CantorNF a))) implies omega -leading_coeff (C . d) = (omega -leading_coeff (CantorNF b)) . (((omega -exponent (CantorNF b)) ") . (omega -exponent (C . d))) ) & ( omega -exponent (C . d) in (rng (omega -exponent (CantorNF a))) /\ (rng (omega -exponent (CantorNF b))) implies omega -leading_coeff (C . d) = ((omega -leading_coeff (CantorNF a)) . (((omega -exponent (CantorNF a)) ") . (omega -exponent (C . d)))) + ((omega -leading_coeff (CantorNF b)) . (((omega -exponent (CantorNF b)) ") . (omega -exponent (C . d)))) ) ) ) ) and
A33: ex C being Cantor-normal-form Ordinal-Sequence st
( s2 = Sum^ C & rng (omega -exponent C) = (rng (omega -exponent (CantorNF a))) \/ (rng (omega -exponent (CantorNF b))) & ( for d being object st d in dom C holds
( ( omega -exponent (C . d) in (rng (omega -exponent (CantorNF a))) \ (rng (omega -exponent (CantorNF b))) implies omega -leading_coeff (C . d) = (omega -leading_coeff (CantorNF a)) . (((omega -exponent (CantorNF a)) ") . (omega -exponent (C . d))) ) & ( omega -exponent (C . d) in (rng (omega -exponent (CantorNF b))) \ (rng (omega -exponent (CantorNF a))) implies omega -leading_coeff (C . d) = (omega -leading_coeff (CantorNF b)) . (((omega -exponent (CantorNF b)) ") . (omega -exponent (C . d))) ) & ( omega -exponent (C . d) in (rng (omega -exponent (CantorNF a))) /\ (rng (omega -exponent (CantorNF b))) implies omega -leading_coeff (C . d) = ((omega -leading_coeff (CantorNF a)) . (((omega -exponent (CantorNF a)) ") . (omega -exponent (C . d)))) + ((omega -leading_coeff (CantorNF b)) . (((omega -exponent (CantorNF b)) ") . (omega -exponent (C . d)))) ) ) ) ) ; :: thesis: s1 = s2
consider C1 being Cantor-normal-form Ordinal-Sequence such that
A34: s1 = Sum^ C1 and
A35: rng (omega -exponent C1) = (rng (omega -exponent (CantorNF a))) \/ (rng (omega -exponent (CantorNF b))) and
A36: for d being object st d in dom C1 holds
( ( omega -exponent (C1 . d) in (rng (omega -exponent (CantorNF a))) \ (rng (omega -exponent (CantorNF b))) implies omega -leading_coeff (C1 . d) = (omega -leading_coeff (CantorNF a)) . (((omega -exponent (CantorNF a)) ") . (omega -exponent (C1 . d))) ) & ( omega -exponent (C1 . d) in (rng (omega -exponent (CantorNF b))) \ (rng (omega -exponent (CantorNF a))) implies omega -leading_coeff (C1 . d) = (omega -leading_coeff (CantorNF b)) . (((omega -exponent (CantorNF b)) ") . (omega -exponent (C1 . d))) ) & ( omega -exponent (C1 . d) in (rng (omega -exponent (CantorNF a))) /\ (rng (omega -exponent (CantorNF b))) implies omega -leading_coeff (C1 . d) = ((omega -leading_coeff (CantorNF a)) . (((omega -exponent (CantorNF a)) ") . (omega -exponent (C1 . d)))) + ((omega -leading_coeff (CantorNF b)) . (((omega -exponent (CantorNF b)) ") . (omega -exponent (C1 . d)))) ) ) by A32;
consider C2 being Cantor-normal-form Ordinal-Sequence such that
A37: s2 = Sum^ C2 and
A38: rng (omega -exponent C2) = (rng (omega -exponent (CantorNF a))) \/ (rng (omega -exponent (CantorNF b))) and
A39: for d being object st d in dom C2 holds
( ( omega -exponent (C2 . d) in (rng (omega -exponent (CantorNF a))) \ (rng (omega -exponent (CantorNF b))) implies omega -leading_coeff (C2 . d) = (omega -leading_coeff (CantorNF a)) . (((omega -exponent (CantorNF a)) ") . (omega -exponent (C2 . d))) ) & ( omega -exponent (C2 . d) in (rng (omega -exponent (CantorNF b))) \ (rng (omega -exponent (CantorNF a))) implies omega -leading_coeff (C2 . d) = (omega -leading_coeff (CantorNF b)) . (((omega -exponent (CantorNF b)) ") . (omega -exponent (C2 . d))) ) & ( omega -exponent (C2 . d) in (rng (omega -exponent (CantorNF a))) /\ (rng (omega -exponent (CantorNF b))) implies omega -leading_coeff (C2 . d) = ((omega -leading_coeff (CantorNF a)) . (((omega -exponent (CantorNF a)) ") . (omega -exponent (C2 . d)))) + ((omega -leading_coeff (CantorNF b)) . (((omega -exponent (CantorNF b)) ") . (omega -exponent (C2 . d)))) ) ) by A33;
A40: dom C1 = card (dom (omega -exponent C1)) by Def1
.= card (rng (omega -exponent C2)) by A35, A38, CARD_1:70
.= card (dom (omega -exponent C2)) by CARD_1:70
.= dom C2 by Def1 ;
for x being object st x in dom C1 holds
C1 . x = C2 . x

proof

let x be object ; :: thesis: ( x in dom C1 implies C1 . x = C2 . x )
set e1 = omega -exponent (C1 . x);
set e2 = omega -exponent (C2 . x);
assume A41: x in dom C1 ; :: thesis: C1 . x = C2 . x
then A42: omega -exponent (C1 . x) = (omega -exponent C1) . x by Def1
.= (omega -exponent C2) . x by A35, A38, Th34
.= omega -exponent (C2 . x) by A40, A41, Def1 ;
x in dom (omega -exponent C1) by A41, Def1;
then (omega -exponent C1) . x in rng (omega -exponent C1) by FUNCT_1:3;
then A43: omega -exponent (C1 . x) in (rng (omega -exponent (CantorNF a))) \/ (rng (omega -exponent (CantorNF b))) by A35, A41, Def1;
A44: omega -leading_coeff (C1 . x) = omega -leading_coeff (C2 . x)

proof

per cases ( ( omega -exponent (C1 . x) in rng (omega -exponent (CantorNF a)) & not omega -exponent (C1 . x) in rng (omega -exponent (CantorNF b)) ) or ( omega -exponent (C1 . x) in rng (omega -exponent (CantorNF b)) & not omega -exponent (C1 . x) in rng (omega -exponent (CantorNF a)) ) or ( omega -exponent (C1 . x) in rng (omega -exponent (CantorNF a)) & omega -exponent (C1 . x) in rng (omega -exponent (CantorNF b)) ) ) by A43, XBOOLE_0:def 3;

suppose ( omega -exponent (C1 . x) in rng (omega -exponent (CantorNF a)) & not omega -exponent (C1 . x) in rng (omega -exponent (CantorNF b)) ) ; :: thesis: omega -leading_coeff (C1 . x) = omega -leading_coeff (C2 . x)

then A45: omega -exponent (C1 . x) in (rng (omega -exponent (CantorNF a))) \ (rng (omega -exponent (CantorNF b))) by XBOOLE_0:def 5;
hence omega -leading_coeff (C1 . x) = (omega -leading_coeff (CantorNF a)) . (((omega -exponent (CantorNF a)) ") . (omega -exponent (C2 . x))) by A36, A41, A42
.= omega -leading_coeff (C2 . x) by A39, A40, A41, A42, A45 ;
:: thesis: verum

end;

suppose ( omega -exponent (C1 . x) in rng (omega -exponent (CantorNF b)) & not omega -exponent (C1 . x) in rng (omega -exponent (CantorNF a)) ) ; :: thesis: omega -leading_coeff (C1 . x) = omega -leading_coeff (C2 . x)

then A46: omega -exponent (C1 . x) in (rng (omega -exponent (CantorNF b))) \ (rng (omega -exponent (CantorNF a))) by XBOOLE_0:def 5;
hence omega -leading_coeff (C1 . x) = (omega -leading_coeff (CantorNF b)) . (((omega -exponent (CantorNF b)) ") . (omega -exponent (C2 . x))) by A36, A41, A42
.= omega -leading_coeff (C2 . x) by A39, A40, A41, A42, A46 ;
:: thesis: verum

end;

suppose ( omega -exponent (C1 . x) in rng (omega -exponent (CantorNF a)) & omega -exponent (C1 . x) in rng (omega -exponent (CantorNF b)) ) ; :: thesis: omega -leading_coeff (C1 . x) = omega -leading_coeff (C2 . x)

then A47: omega -exponent (C1 . x) in (rng (omega -exponent (CantorNF a))) /\ (rng (omega -exponent (CantorNF b))) by XBOOLE_0:def 4;
hence omega -leading_coeff (C1 . x) = ((omega -leading_coeff (CantorNF a)) . (((omega -exponent (CantorNF a)) ") . (omega -exponent (C2 . x)))) + ((omega -leading_coeff (CantorNF b)) . (((omega -exponent (CantorNF b)) ") . (omega -exponent (C2 . x)))) by A36, A41, A42
.= omega -leading_coeff (C2 . x) by A39, A40, A41, A42, A47 ;
:: thesis: verum

end;

end;

end;

thus C1 . x = (omega -leading_coeff (C1 . x)) *^ (exp (omega,(omega -exponent (C1 . x)))) by A41, Th64
.= C2 . x by A40, A41, A42, A44, Th64 ; :: thesis: verum

end;

hence s1 = s2 by A34, A37, A40, FUNCT_1:2; :: thesis: verum