let n be Nat; :: thesis:
let e be odd-valued a_partition of n; :: thesis:
A1: Sum e = n by Def3;
deffunc H₁( object ) -> Element of omega = card (Coim (e,$1));
consider H being FinSequence such that
A2: ( len H = n & ( for k being Nat st k in dom H holds
H . k = H₁(k) ) ) from FINSEQ_1:sch 2();
rng H c= NAT

proof

let y be object ; :: according to TARSKI:def 3 :: thesis:
assume y in rng H ; :: thesis:
then consider x being object such that
A3: ( x in dom H & H . x = y ) by FUNCT_1:def 3;
reconsider x = x as Nat by A3;
H . x = card (Coim (e,x)) by A3, A2;
hence y in NAT by A3; :: thesis:

end;

then reconsider H = H as natural-valued FinSequence by VALUED_0:def 6;
A4: dom H = Seg (len H) by FINSEQ_1:def 3;
A5: Sum e = Sum ((idseq n) (#) H)

proof

A6: for i being Nat st i in dom e holds
0 <= e . i ;
for i being Nat holds card (Coim (e,i)) = H . i

proof

let i be Nat; :: thesis:

per cases by FINSEQ_3:25;

suppose i in dom H ; :: thesis:

hence card (Coim (e,i)) = H . i by A2; :: thesis:

end;

suppose i < 1 ; :: thesis:

then A8: ( not i in rng e & not i in dom H ) by NAT_1:14, FINSEQ_3:25;
then ( H . i = 0 & e " {i} = {} ) by FUNCT_1:def 2, FUNCT_1:72;
then Coim (e,i) = {} by RELAT_1:def 17;
hence card (Coim (e,i)) = H . i by A8, FUNCT_1:def 2; :: thesis:

end;

suppose A9: i > len H ; :: thesis:

then A10: not i in dom H by FINSEQ_3:25;
Coim (e,i) = {}

proof

assume Coim (e,i) <> {} ; :: thesis:
then e " {i} <> {} by RELAT_1:def 17;
then i in rng e by FUNCT_1:72;
then consider x being object such that
A11: ( x in dom e & e . x = i ) by FUNCT_1:def 3;
reconsider x = x as Nat by A11;
i <= Sum e by A11, A6, MATRPROB:5;
hence contradiction by Def3, A9, A2; :: thesis:

end;

hence card (Coim (e,i)) = H . i by A10, FUNCT_1:def 2; :: thesis:

end;

hence Sum e = ((1 * (H . 1)) + (2 * (H . 2))) + ((((id (dom H)) (#) H),3) +...) by Th9
.= ((1 * (H . 1)) + (((id (dom H)) (#) H) . 2)) + ((((id (dom H)) (#) H),3) +...) by Lm2
.= ((((id (dom H)) (#) H) . 1) + (((id (dom H)) (#) H) . 2)) + ((((id (dom H)) (#) H),3) +...) by Lm2
.= (((id (dom H)) (#) H) . 1) + ((((id (dom H)) (#) H) . 2) + ((((id (dom H)) (#) H),(2 + 1)) +...))
.= (((id (dom H)) (#) H) . 1) + ((((id (dom H)) (#) H),2) +...) by FLEXARY1:20
.= Sum ((idseq n) (#) H) by A4, A2, FLEXARY1:22 ;
:: thesis:

end;

defpred S₁[ Nat, object ] means ex f being natural-valued increasing FinSequence st
( H . $1 = ((2 |^ f) . 1) + (((2 |^ f),2) +...) & $2 = $1 * (2 |^ f) );
ex p being FinSequence of NAT * st
( dom p = Seg (len H) & ( for k being Nat st k in Seg (len H) holds
S₁[k,p . k] ) )

proof

A12: for k being Nat st k in Seg (len H) holds
ex x being object st S₁[k,x]

proof

let k be Nat; :: thesis:
assume k in Seg (len H) ; :: thesis:
consider f being natural-valued increasing FinSequence such that
A13: H . k = ((2 |^ f) . 1) + (((2 |^ f),2) +...) by FLEXARY1:31;
take G = k * (2 |^ f); :: thesis:
thus S₁[k,G] by A13; :: thesis:

end;

consider p being FinSequence such that
A14: ( dom p = Seg (len H) & ( for k being Nat st k in Seg (len H) holds
S₁[k,p . k] ) ) from FINSEQ_1:sch 1(A12);
rng p c= NAT *

proof

let y be object ; :: according to TARSKI:def 3 :: thesis:
assume y in rng p ; :: thesis:
then consider x being object such that
A15: ( x in dom p & p . x = y ) by FUNCT_1:def 3;
reconsider x = x as Nat by A15;
consider f being natural-valued increasing FinSequence such that
A16: ( H . x = ((2 |^ f) . 1) + (((2 |^ f),2) +...) & p . x = x * (2 |^ f) ) by A15, A14;
rng (x * (2 |^ f)) c= NAT by VALUED_0:def 6;
then x * (2 |^ f) is FinSequence of NAT by FINSEQ_1:def 4;
hence y in NAT * by FINSEQ_1:def 11, A15, A16; :: thesis:

end;

then p is FinSequence of NAT * by FINSEQ_1:def 4;
hence ex p being FinSequence of NAT * st
( dom p = Seg (len H) & ( for k being Nat st k in Seg (len H) holds
S₁[k,p . k] ) ) by A14; :: thesis:

end;

then consider p being FinSequence of NAT * such that
A17: ( dom p = Seg (len H) & ( for k being Nat st k in Seg (len H) holds
S₁[k,p . k] ) ) ;
A18: for k being Nat st p . k <> {} holds
k is odd

proof

let k be Nat; :: thesis:
assume A19: p . k <> {} ; :: thesis:
then A20: k in dom p by FUNCT_1:def 2;
then consider f being natural-valued increasing FinSequence such that
A21: ( H . k = ((2 |^ f) . 1) + (((2 |^ f),2) +...) & p . k = k * (2 |^ f) ) by A17;
consider j being object such that
A22: j in dom (p . k) by A19, XBOOLE_0:def 1;
reconsider j = j as Nat by A22;
A23: dom (p . k) = dom (2 |^ f) by A21, VALUED_1:def 5;
then j in dom f by A22, FLEXARY1:def 4;
then (2 |^ f) . j = 2 to_power (f . j) by FLEXARY1:def 4
.= 2 |^ (f . j) ;
then A24: (2 |^ f) . j > 0 by NEWTON:83;
for i being Nat st i in dom (2 |^ f) holds
0 <= (2 |^ f) . i ;
then A25: Sum (2 |^ f) > 0 by A22, A24, A23, RVSUM_1:85;
A26: rng e c= OddNAT by Def1;
H . k = card (Coim (e,k)) by A20, A4, A17, A2;
then Coim (e,k) <> {} by FLEXARY1:22, A25, A21;
then e " {k} <> {} by RELAT_1:def 17;
then k in OddNAT by FUNCT_1:72, A26;
hence k is odd by Th2; :: thesis:

end;

A27: ( H is n -element & H is complex-valued ) by A2, CARD_1:def 7;
len p = n by A17, A2, FINSEQ_1:def 3;
then A28: len (Sum p) = n by CARD_1:def 7;

now :: thesis:

let i be Nat; :: thesis:
assume ( 1 <= i & i <= n ) ; :: thesis:
then i in Seg (len H) by A2;
then consider f being natural-valued increasing FinSequence such that
A29: ( H . i = ((2 |^ f) . 1) + (((2 |^ f),2) +...) & p . i = i * (2 |^ f) ) by A17;
thus (Sum p) . i = Sum (i * (2 |^ f)) by A29, FLEXARY1:def 8
.= i * (Sum (2 |^ f)) by RVSUM_1:87
.= i * (H . i) by A29, FLEXARY1:22
.= ((idseq n) (#) H) . i by A4, A2, Lm2 ; :: thesis:

end;

then A30: Sum p = (idseq n) (#) H by CARD_1:def 7, A27, A28;
set NC = NAT -concatenation ;
set np = (NAT -concatenation) "**" p;
NAT * c= COMPLEX * by NUMBERS:20, FINSEQ_1:62;
then reconsider p1 = p as FinSequence of COMPLEX * by FINSEQ_2:24;
rng ((NAT -concatenation) "**" p) c= REAL ;
then reconsider np = (NAT -concatenation) "**" p as FinSequence of REAL by FINSEQ_1:def 4;
set sp = sort_a np;
Sum ((COMPLEX -concatenation) "**" p1) = Sum np by FLEXARY1:5;
then A31: Sum np = n by FLEXARY1:48, A30, A5, A1;
A32: Sum (sort_a np) = n by RFINSEQ2:def 6, RFINSEQ:9, A31;
A33: rng (sort_a np) = rng np by RFINSEQ2:def 6, CLASSES1:75;
A34: rng np = Values p by FLEXARY1:4;
sort_a np is one-to-one a_partition of n

proof

not 0 in rng (sort_a np)

proof

assume 0 in rng (sort_a np) ; :: thesis:
then consider x, y being object such that
A35: ( x in dom p & y in dom (p . x) & 0 = (p . x) . y ) by A33, A34, FLEXARY1:1;
reconsider x = x, y = y as Nat by A35;
consider f being natural-valued increasing FinSequence such that
A36: ( H . x = ((2 |^ f) . 1) + (((2 |^ f),2) +...) & p . x = x * (2 |^ f) ) by A35, A17;
A37: 1 <= x by A35, FINSEQ_3:25;
A38: (x * (2 |^ f)) . y = x * ((2 |^ f) . y) by RVSUM_1:45;
y in dom (2 |^ f) by A35, A36, VALUED_1:def 5;
then y in dom f by FLEXARY1:def 4;
then (2 |^ f) . y = 2 to_power (f . y) by FLEXARY1:def 4
.= 2 |^ (f . y) ;
then (2 |^ f) . y > 0 by NEWTON:83;
hence contradiction by A35, A36, A37, A38; :: thesis:

end;

then A39: sort_a np is non-zero by ORDINAL1:def 15;
A40: Sum (sort_a np) = n by RFINSEQ2:def 6, RFINSEQ:9, A31;
A41: sort_a np is natural-valued by A34, A33, VALUED_0:def 6;
sort_a np is one-to-one

proof

now :: thesis:

let x1, x2 be set ; :: thesis:
assume A42: ( x1 in dom (sort_a np) & x2 in dom (sort_a np) & (sort_a np) . x1 = (sort_a np) . x2 ) ; :: thesis:
(sort_a np) . x1 in {((sort_a np) . x1)} by TARSKI:def 1;
then A43: ( x1 in (sort_a np) " {((sort_a np) . x1)} & x2 in (sort_a np) " {((sort_a np) . x1)} ) by FUNCT_1:def 7, A42;
assume x1 <> x2 ; :: thesis:
then not (sort_a np) " {((sort_a np) . x1)} is trivial by A43, SUBSET_1:def 7;
then A44: card ((sort_a np) " {((sort_a np) . x1)}) >= 2 by NAT_D:60;
card (Coim ((sort_a np),((sort_a np) . x1))) = card (Coim (np,((sort_a np) . x1))) by CLASSES1:def 10, RFINSEQ2:def 6;
then card (Coim (np,((sort_a np) . x1))) >= 2 by A44, RELAT_1:def 17;
then A45: card (np " {((sort_a np) . x1)}) >= 2 by RELAT_1:def 17;
then not np " {((sort_a np) . x1)} is trivial by NAT_D:60;
then consider d1, d2 being Element of np " {((sort_a np) . x1)} such that
A46: d1 <> d2 by SUBSET_1:def 7;
not np " {((sort_a np) . x1)} is empty by A45;
then A47: ( d1 in dom np & np . d1 in {((sort_a np) . x1)} & d2 in dom np & np . d2 in {((sort_a np) . x1)} ) by FUNCT_1:def 7;
then A48: ( np . d1 = (sort_a np) . x1 & np . d2 = (sort_a np) . x1 ) by TARSKI:def 1;
consider n1, k1 being Nat such that
A49: ( n1 + 1 in dom p & k1 in dom (p . (n1 + 1)) & d1 = k1 + (len ((NAT -concatenation) "**" (p | n1))) ) by FLEXARY1:6, A47;
set n2 = n1 + 1;
A50: np . d1 = (p . (n1 + 1)) . k1 by FLEXARY1:8, A49;
consider f being natural-valued increasing FinSequence such that
A51: ( H . (n1 + 1) = ((2 |^ f) . 1) + (((2 |^ f),2) +...) & p . (n1 + 1) = (n1 + 1) * (2 |^ f) ) by A49, A17;
A52: (p . (n1 + 1)) . k1 = (n1 + 1) * ((2 |^ f) . k1) by A51, RVSUM_1:45;
k1 in dom (2 |^ f) by A49, A51, VALUED_1:def 5;
then A53: k1 in dom f by FLEXARY1:def 4;
then A54: (2 |^ f) . k1 = 2 to_power (f . k1) by FLEXARY1:def 4
.= 2 |^ (f . k1) ;
consider n3, k3 being Nat such that
A55: ( n3 + 1 in dom p & k3 in dom (p . (n3 + 1)) & d2 = k3 + (len ((NAT -concatenation) "**" (p | n3))) ) by FLEXARY1:6, A47;
set n4 = n3 + 1;
consider g being natural-valued increasing FinSequence such that
A56: ( H . (n3 + 1) = ((2 |^ g) . 1) + (((2 |^ g),2) +...) & p . (n3 + 1) = (n3 + 1) * (2 |^ g) ) by A55, A17;
k3 in dom (2 |^ g) by A55, A56, VALUED_1:def 5;
then A57: k3 in dom g by FLEXARY1:def 4;
then A58: (2 |^ g) . k3 = 2 to_power (g . k3) by FLEXARY1:def 4
.= 2 |^ (g . k3) ;
A59: ( p . (n3 + 1) <> {} & p . (n1 + 1) <> {} ) by A55, A49;
then consider c2 being Nat such that
A60: n1 + 1 = (2 * c2) + 1 by A18, ABIAN:9;
consider c4 being Nat such that
A61: n3 + 1 = (2 * c4) + 1 by A59, A18, ABIAN:9;
(p . (n1 + 1)) . k1 = (p . (n3 + 1)) . k3 by A48, A50, FLEXARY1:8, A55;
then A62: (n1 + 1) * (2 |^ (f . k1)) = (n3 + 1) * (2 |^ (g . k3)) by A56, RVSUM_1:45, A58, A52, A54;
then A63: ( c2 = c4 & f . k1 = g . k3 ) by A60, A61, CARD_4:4;
n3 + 1 = n1 + 1 by A62, A60, A61, CARD_4:4;
then A64: f = g by A51, A56, FLEXARY1:27;
f is one-to-one ;
hence sort_a np is one-to-one by A57, A53, A64, A63, A49, A55, A60, A61, A46; :: thesis:

end;

hence sort_a np is one-to-one ; :: thesis:

end;

hence sort_a np is one-to-one a_partition of n by Def3, A39, A41, A40; :: thesis:

end;

then reconsider sp = sort_a np as one-to-one a_partition of n ;
take sp ; :: thesis:
for O being odd-valued FinSequence
for a being natural-valued FinSequence
for sort being odd_organization of O st len O = len sp & len sp = len a & sp = O (#) (2 |^ a) holds
for j being Nat holds card (Coim (e,((j * 2) - 1))) = ((((2 |^ a) *. sort) . j),1) +...

proof

let O be odd-valued FinSequence; :: thesis:
let a be natural-valued FinSequence; :: thesis:
let sort be odd_organization of O; :: thesis:
assume A65: ( len O = len sp & len sp = len a & sp = O (#) (2 |^ a) ) ; :: thesis:
let j be Nat; :: thesis:
A66: ( dom a = dom sp & dom sp = dom O & dom a = dom (2 |^ a) ) by FLEXARY1:def 4, FINSEQ_3:29, A65;
then reconsider S = sort as DoubleReorganization of dom (2 |^ a) ;
A67: (2 * j) - 1 = O . (sort _ (j,1)) & ... & (2 * j) - 1 = O . (sort _ (j,(len (sort . j)))) by Def4;

per cases ;

suppose A68: j < 1 ; :: thesis:

then j = 0 by NAT_1:14;
then not (2 * j) - 1 in rng e ;
then e " {((2 * j) - 1)} = {} by FUNCT_1:72;
then A69: Coim (e,((2 * j) - 1)) = {} by RELAT_1:def 17;
not j in dom ((2 |^ a) *. S) by FINSEQ_3:25, A68;
then Sum (((2 |^ a) *. S) . j) = 0 by FUNCT_1:def 2, RVSUM_1:72;
hence card (Coim (e,((j * 2) - 1))) = ((((2 |^ a) *. sort) . j),1) +... by FLEXARY1:21, A69; :: thesis:

end;

suppose A70: (j * 2) - 1 > n ; :: thesis:

A71: Coim (e,((j * 2) - 1)) = {}

proof

assume Coim (e,((j * 2) - 1)) <> {} ; :: thesis:
then e " {((j * 2) - 1)} <> 0 by RELAT_1:def 17;
then (2 * j) - 1 in rng e by FUNCT_1:72;
then consider w being object such that
A72: ( w in dom e & e . w = (2 * j) - 1 ) by FUNCT_1:def 3;
for i being Nat st i in dom e holds
0 <= e . i ;
hence contradiction by A72, MATRPROB:5, A1, A70; :: thesis:

end;

((2 |^ a) *. S) . j = {}

proof

set L = len (S . j);
set SjL = (S . j) . (len (S . j));
assume A74: ((2 |^ a) *. S) . j <> {} ; :: thesis:
len (((2 |^ a) *. S) . j) = len (S . j) by CARD_1:def 7;
then A75: len (S . j) >= 1 by A74, NAT_1:14;
then A76: (2 * j) - 1 = O . (sort _ (j,(len (S . j)))) by A67;
S . j <> {} by A74;
then A77: j in dom S by FUNCT_1:def 2;
len (S . j) in dom (S . j) by A75, FINSEQ_3:25;
then A78: (S . j) . (len (S . j)) in Values S by FLEXARY1:1, A77;
then A79: (S . j) . (len (S . j)) in dom O by FLEXARY1:def 7;
then A80: sp . ((S . j) . (len (S . j))) = (O . ((S . j) . (len (S . j)))) * ((2 |^ a) . ((S . j) . (len (S . j)))) by VALUED_1:def 4, A66, A65;
A81: (2 |^ a) . ((S . j) . (len (S . j))) = 2 to_power (a . ((S . j) . (len (S . j)))) by FLEXARY1:def 4, A66, A79;
A82: for i being Nat st i in dom sp holds
0 <= sp . i ;
2 |^ (a . ((S . j) . (len (S . j)))) > 0 by NEWTON:83;
then 2 |^ (a . ((S . j) . (len (S . j)))) >= 1 by NAT_1:14;
then A83: sp . ((S . j) . (len (S . j))) >= 1 * ((2 * j) - 1) by A76, A80, A81, XREAL_1:66;
(S . j) . (len (S . j)) in dom sp by A78, FLEXARY1:def 7, A66;
then sp . ((S . j) . (len (S . j))) <= n by A82, MATRPROB:5, A32;
hence contradiction by A83, A70, XXREAL_0:2; :: thesis:

end;

hence card (Coim (e,((j * 2) - 1))) = ((((2 |^ a) *. sort) . j),1) +... by RVSUM_1:72, FLEXARY1:21, A71; :: thesis:

end;

suppose A84: ( j >= 1 & (j * 2) - 1 <= n ) ; :: thesis:

set J = (j * 2) - 1;
2 * j >= 2 * 1 by A84, XREAL_1:64;
then A85: (j * 2) - 1 >= 2 - 1 by XREAL_1:9;
then consider f being natural-valued increasing FinSequence such that
A86: ( H . ((j * 2) - 1) = ((2 |^ f) . 1) + (((2 |^ f),2) +...) & p . ((j * 2) - 1) = ((j * 2) - 1) * (2 |^ f) ) by A84, FINSEQ_3:25, A2, A17, A4;
reconsider j1 = j - 1 as Nat by A84;
A87: (j * 2) - 1 = (2 * j1) + 1 ;
A88: ((2 |^ a) *. S) . j is FinSequence of REAL by RVSUM_1:145;
A89: 2 |^ f is FinSequence of REAL by RVSUM_1:145;
for x being object holds card (Coim ((((2 |^ a) *. sort) . j),x)) = card (Coim ((2 |^ f),x))

proof

proof

assume y in rng (((2 |^ a) *. sort) . j) ; :: thesis:
then consider x being object such that
A93: ( x in dom (((2 |^ a) *. S) . j) & (((2 |^ a) *. S) . j) . x = y ) by FUNCT_1:def 3;
reconsider x = x as Nat by A93;
set Sjx = (S . j) . x;
A94: ( x in dom (S . j) & (S . j) . x in dom (2 |^ a) ) by A90, A93, FUNCT_1:11;
then A95: ( 1 <= x & x <= len (S . j) ) by FINSEQ_3:25;
(j * 2) - 1 = O . (sort _ (j,1)) & ... & (j * 2) - 1 = O . (sort _ (j,(len (sort . j)))) by Def4;
then A96: (j * 2) - 1 = O . (sort _ (j,x)) by A95;
(S . j) . x in dom a by A94, FLEXARY1:def 4;
then A97: (2 |^ a) . ((S . j) . x) = 2 to_power (a . ((S . j) . x)) by FLEXARY1:def 4;
sp . ((S . j) . x) in Values p by A66, A94, FUNCT_1:def 3, A33, A34;
then consider u, w being object such that
A98: ( u in dom p & w in dom (p . u) & sp . ((S . j) . x) = (p . u) . w ) by FLEXARY1:1;
reconsider u = u, w = w as Nat by A98;
p . u <> {} by A98;
then consider s being Nat such that
A99: u = (2 * s) + 1 by A18, ABIAN:9;
consider fu being natural-valued increasing FinSequence such that
A100: ( H . u = ((2 |^ fu) . 1) + (((2 |^ fu),2) +...) & p . u = u * (2 |^ fu) ) by A17, A98;
A101: (p . u) . w = u * ((2 |^ fu) . w) by A100, RVSUM_1:45;
w in dom (2 |^ fu) by A100, A98, VALUED_1:def 5;
then w in dom fu by FLEXARY1:def 4;
then A102: (2 |^ fu) . w = 2 to_power (fu . w) by FLEXARY1:def 4;
then A103: ((j * 2) - 1) * (2 |^ (a . ((S . j) . x))) = ((2 * s) + 1) * (2 |^ (fu . w)) by A98, A101, A99, A65, VALUED_1:5, A97, A96;
then A104: ( j1 = s & a . ((S . j) . x) = fu . w ) by CARD_4:4, A87;
A105: u * (2 |^ fu) = ((j * 2) - 1) * (2 |^ f) by A103, CARD_4:4, A87, A100, A86, A99;
then A106: w in dom (2 |^ f) by A98, A100, VALUED_1:def 5;
u * ((2 |^ fu) . w) = ((j * 2) - 1) * ((2 |^ f) . w) by A105, A100, A101, RVSUM_1:45;
then A107: (2 |^ fu) . w = (2 |^ f) . w by A104, A99, XCMPLX_1:5;
y = (2 |^ fu) . w by A102, A104, A90, A93, FUNCT_1:12, A97;
hence y in rng (2 |^ f) by A106, A107, FUNCT_1:def 3; :: thesis:

end;

A108: ( y in rng (2 |^ f) implies y in rng (((2 |^ a) *. sort) . j) )

proof

assume y in rng (2 |^ f) ; :: thesis:
then consider x being object such that
A109: ( x in dom (2 |^ f) & (2 |^ f) . x = y ) by FUNCT_1:def 3;
reconsider x = x as Nat by A109;
x in dom f by A109, FLEXARY1:def 4;
then A110: (2 |^ f) . x = 2 to_power (f . x) by FLEXARY1:def 4;
A111: x in dom (p . ((j * 2) - 1)) by A86, A109, VALUED_1:def 5;
set pJx = (p . ((j * 2) - 1)) . x;
(j * 2) - 1 in dom p by A85, A84, A2, A17;
then (p . ((j * 2) - 1)) . x in rng sp by FLEXARY1:1, A111, A33, A34;
then consider w being object such that
A112: ( w in dom sp & sp . w = (p . ((j * 2) - 1)) . x ) by FUNCT_1:def 3;
reconsider w = w as Nat by A112;
A113: sp . w = (O . w) * ((2 |^ a) . w) by A65, VALUED_1:5;
Values sort = dom O by FLEXARY1:def 7;
then consider r, t being object such that
A114: ( r in dom S & t in dom (S . r) & (S . r) . t = w ) by FLEXARY1:1, A112, A66;
reconsider r = r, t = t as Nat by A114;
1 <= r by A114, FINSEQ_3:25;
then reconsider r1 = r - 1 as Nat ;
set R = (2 * r) - 1;
A115: (2 * r) - 1 = O . (sort _ (r,1)) & ... & (2 * r) - 1 = O . (sort _ (r,(len (sort . r)))) by Def4;
( 1 <= t & t <= len (S . r) ) by A114, FINSEQ_3:25;
then A116: (2 * r) - 1 = O . (sort _ (r,t)) by A115;
A117: (2 |^ a) . w = 2 to_power (a . w) by A112, A66, FLEXARY1:def 4;
then ((j * 2) - 1) * (2 |^ (f . x)) = ((2 * r1) + 1) * (2 |^ (a . w)) by A110, A113, A86, RVSUM_1:45, A112, A116, A114;
then A118: ( j1 = r1 & f . x = a . w ) by CARD_4:4, A87;
then A119: t in dom ((2 |^ a) * (S . j)) by A112, A66, A114, FUNCT_1:11;
then ((2 |^ a) * (S . j)) . t = (2 |^ f) . x by A114, A118, FUNCT_1:12, A110, A117;
hence y in rng (((2 |^ a) *. sort) . j) by A109, A119, A90, FUNCT_1:def 3; :: thesis:

end;

per cases ;

suppose A120: Coim ((((2 |^ a) *. sort) . j),y) = {} ; :: thesis:

Coim ((2 |^ f),y) = {}

proof

assume Coim ((2 |^ f),y) <> {} ; :: thesis:
then (2 |^ f) " {y} <> {} by RELAT_1:def 17;
then (((2 |^ a) *. sort) . j) " {y} <> {} by FUNCT_1:72, A108;
hence contradiction by RELAT_1:def 17, A120; :: thesis:

end;

hence card (Coim ((((2 |^ a) *. sort) . j),y)) = card (Coim ((2 |^ f),y)) by A120; :: thesis:

end;

suppose Coim ((((2 |^ a) *. sort) . j),y) <> {} ; :: thesis:

then A121: (((2 |^ a) *. sort) . j) " {y} <> {} by RELAT_1:def 17;
then A122: y in rng (((2 |^ a) *. sort) . j) by FUNCT_1:72;
A123: 2 + 0 = 2 ;
((2 |^ a) *. S) . j = 2 |^ (a * (S . j)) by FLEXARY1:25, A90
.= 2 |^ ((a *. S) . j) by FLEXARY1:41 ;
then ex x being object st (((2 |^ a) *. sort) . j) " {y} = {x} by A91, A123, A122, FUNCT_1:74;
then A124: card (Coim ((((2 |^ a) *. sort) . j),y)) = 1 by CARD_2:42, RELAT_1:def 17;
ex x being object st (2 |^ f) " {y} = {x} by A121, FUNCT_1:72, A92, A123, FUNCT_1:74;
hence card (Coim ((((2 |^ a) *. sort) . j),y)) = card (Coim ((2 |^ f),y)) by CARD_2:42, A124, RELAT_1:def 17; :: thesis:

end;

then Sum (((2 |^ a) *. S) . j) = Sum (2 |^ f) by CLASSES1:def 10, A89, A88, RFINSEQ:9
.= ((2 |^ f) . 1) + (((2 |^ f),2) +...) by FLEXARY1:22
.= card (Coim (e,((j * 2) - 1))) by A85, A84, FINSEQ_3:25, A2, A86 ;
hence card (Coim (e,((j * 2) - 1))) = ((((2 |^ a) *. sort) . j),1) +... by FLEXARY1:21; :: thesis:

end;

hence e = Euler_transformation sp by Th12; :: thesis: