let n be Nat; for d being one-to-one a_partition of n ex e being odd-valued a_partition of n st
for j being Nat
for O1 being odd-valued FinSequence
for a1 being natural-valued FinSequence st len O1 = len d & len d = len a1 & d = O1 (#) (2 |^ a1) holds
for sort being DoubleReorganization of dom d st 1 = O1 . (sort _ (1,1)) & ... & 1 = O1 . (sort _ (1,(len (sort . 1)))) & 3 = O1 . (sort _ (2,1)) & ... & 3 = O1 . (sort _ (2,(len (sort . 2)))) & 5 = O1 . (sort _ (3,1)) & ... & 5 = O1 . (sort _ (3,(len (sort . 3)))) & ( for i being Nat holds (2 * i) - 1 = O1 . (sort _ (i,1)) & ... & (2 * i) - 1 = O1 . (sort _ (i,(len (sort . i)))) ) holds
( card (Coim (e,1)) = ((2 |^ a1) . (sort _ (1,1))) + (((((2 |^ a1) *. sort) . 1),2) +...) & card (Coim (e,3)) = ((2 |^ a1) . (sort _ (2,1))) + (((((2 |^ a1) *. sort) . 2),2) +...) & card (Coim (e,5)) = ((2 |^ a1) . (sort _ (3,1))) + (((((2 |^ a1) *. sort) . 3),2) +...) & card (Coim (e,((j * 2) - 1))) = ((2 |^ a1) . (sort _ (j,1))) + (((((2 |^ a1) *. sort) . j),2) +...) )
let d be one-to-one a_partition of n; ex e being odd-valued a_partition of n st
for j being Nat
for O1 being odd-valued FinSequence
for a1 being natural-valued FinSequence st len O1 = len d & len d = len a1 & d = O1 (#) (2 |^ a1) holds
for sort being DoubleReorganization of dom d st 1 = O1 . (sort _ (1,1)) & ... & 1 = O1 . (sort _ (1,(len (sort . 1)))) & 3 = O1 . (sort _ (2,1)) & ... & 3 = O1 . (sort _ (2,(len (sort . 2)))) & 5 = O1 . (sort _ (3,1)) & ... & 5 = O1 . (sort _ (3,(len (sort . 3)))) & ( for i being Nat holds (2 * i) - 1 = O1 . (sort _ (i,1)) & ... & (2 * i) - 1 = O1 . (sort _ (i,(len (sort . i)))) ) holds
( card (Coim (e,1)) = ((2 |^ a1) . (sort _ (1,1))) + (((((2 |^ a1) *. sort) . 1),2) +...) & card (Coim (e,3)) = ((2 |^ a1) . (sort _ (2,1))) + (((((2 |^ a1) *. sort) . 2),2) +...) & card (Coim (e,5)) = ((2 |^ a1) . (sort _ (3,1))) + (((((2 |^ a1) *. sort) . 3),2) +...) & card (Coim (e,((j * 2) - 1))) = ((2 |^ a1) . (sort _ (j,1))) + (((((2 |^ a1) *. sort) . j),2) +...) )
consider O being odd-valued FinSequence, a being natural-valued FinSequence such that
A1:
( len O = len d & len d = len a & d = O (#) (2 |^ a) )
and
d . 1 = (O . 1) * (2 |^ (a . 1)) & ... & d . (len d) = (O . (len d)) * (2 |^ (a . (len d)))
by Th6;
len (2 |^ a) = len O
by A1, CARD_1:def 7;
then reconsider sort = the odd_organization of O as DoubleReorganization of dom (2 |^ a) by FINSEQ_3:29;
consider mu being 2 * (len sort) -element FinSequence of NAT such that
A2:
for j being Nat holds
( mu . (2 * j) = 0 & mu . ((2 * j) - 1) = ((2 |^ a) . (sort _ (j,1))) + (((((2 |^ a) *. sort) . j),2) +...) )
by Th10;
set alpha = a * (sort . 1);
set beta = a * (sort . 2);
set gamma = a * (sort . 3);
A3:
n = ((((((2 |^ (a * (sort . 1))) . 1) + (((2 |^ (a * (sort . 1))),2) +...)) * 1) + ((((2 |^ (a * (sort . 2))) . 1) + (((2 |^ (a * (sort . 2))),2) +...)) * 3)) + ((((2 |^ (a * (sort . 3))) . 1) + (((2 |^ (a * (sort . 3))),2) +...)) * 5)) + ((((id (dom mu)) (#) mu),7) +...)
proof
reconsider o1 =
sort as
DoubleReorganization of
dom d by A1, FINSEQ_3:29;
A4:
(
dom (d *. o1) = dom o1 &
dom ((2 |^ a) *. sort) = dom sort )
by FOMODEL2:def 6;
A5:
for
j being
Nat holds
Sum ((d *. o1) . j) = ((2 * j) - 1) * (mu . ((2 * j) - 1))
proof
let j be
Nat;
Sum ((d *. o1) . j) = ((2 * j) - 1) * (mu . ((2 * j) - 1))
A6:
mu . ((2 * j) - 1) = ((2 |^ a) . (sort _ (j,1))) + (((((2 |^ a) *. sort) . j),2) +...)
by A2;
per cases
( j in dom o1 or not j in dom sort )
;
suppose
j in dom o1
;
Sum ((d *. o1) . j) = ((2 * j) - 1) * (mu . ((2 * j) - 1))set jj =
(2 * j) - 1;
A7:
(d *. o1) . j = d * (o1 . j)
by FLEXARY1:41;
A8:
((2 |^ a) *. sort) . j = (2 |^ a) * (sort . j)
by FLEXARY1:41;
A9:
len ((d *. o1) . j) = len (o1 . j)
by CARD_1:def 7;
A10:
len (((2 |^ a) *. sort) . j) = len (sort . j)
by CARD_1:def 7;
for
n being
Nat st 1
<= n &
n <= len (sort . j) holds
((d *. o1) . j) . n = (((2 * j) - 1) * (((2 |^ a) *. sort) . j)) . n
proof
let n be
Nat;
( 1 <= n & n <= len (sort . j) implies ((d *. o1) . j) . n = (((2 * j) - 1) * (((2 |^ a) *. sort) . j)) . n )
assume A11:
( 1
<= n &
n <= len (sort . j) )
;
((d *. o1) . j) . n = (((2 * j) - 1) * (((2 |^ a) *. sort) . j)) . n
A12:
(2 * j) - 1
= O . (o1 _ (j,1)) & ... &
(2 * j) - 1
= O . (o1 _ (j,(len (o1 . j))))
by Def4;
thus ((d *. o1) . j) . n =
d . (o1 _ (j,n))
by A11, A9, FINSEQ_3:25, A7, FUNCT_1:12
.=
(O . (o1 _ (j,n))) * ((2 |^ a) . (o1 _ (j,n)))
by A1, VALUED_1:5
.=
((2 * j) - 1) * ((2 |^ a) . (o1 _ (j,n)))
by A12, A11
.=
((2 * j) - 1) * ((((2 |^ a) *. sort) . j) . n)
by A11, A10, FINSEQ_3:25, A8, FUNCT_1:12
.=
(((2 * j) - 1) * (((2 |^ a) *. sort) . j)) . n
by VALUED_1:6
;
verum
end; then A13:
(d *. o1) . j = ((2 * j) - 1) * (((2 |^ a) *. sort) . j)
by A9, CARD_1:def 7;
(((2 |^ a) *. sort) . j) . 1
= ((2 |^ a) *. sort) _ (
j,1)
;
then
(2 |^ a) . (sort _ (j,1)) = (((2 |^ a) *. sort) . j) . 1
by FLEXARY1:42;
then Sum (((2 |^ a) *. sort) . j) =
((2 |^ a) . (sort _ (j,1))) + (((((2 |^ a) *. sort) . j),2) +...)
by FLEXARY1:22
.=
mu . ((2 * j) - 1)
by A2
;
hence
Sum ((d *. o1) . j) = ((2 * j) - 1) * (mu . ((2 * j) - 1))
by A13, RVSUM_1:87;
verum end; end;
end;
set I =
idseq (len mu);
A16:
idseq (len mu) = id (dom mu)
by FINSEQ_1:def 3;
A17:
( 1
-' 1
= 0 & 2
-' 1
= 2
- 1 )
by XREAL_1:233, XREAL_1:232;
A18:
for
j being
Nat holds (
(Sum (d *. o1)),
(4 + (j * 1)))
+...+ (
(Sum (d *. o1)),
((4 + (j * 1)) + (1 -' 1)))
= (
((idseq (len mu)) (#) mu),
(7 + (j * 2)))
+...+ (
((idseq (len mu)) (#) mu),
((7 + (j * 2)) + (2 -' 1)))
proof
let j be
Nat;
((Sum (d *. o1)),(4 + (j * 1))) +...+ ((Sum (d *. o1)),((4 + (j * 1)) + (1 -' 1))) = (((idseq (len mu)) (#) mu),(7 + (j * 2))) +...+ (((idseq (len mu)) (#) mu),((7 + (j * 2)) + (2 -' 1)))
set S =
Sum (d *. o1);
A19: (
(Sum (d *. o1)),
(4 + (j * 1)))
+...+ (
(Sum (d *. o1)),
((4 + (j * 1)) + (1 -' 1))) =
(Sum (d *. o1)) . (4 + j)
by A17, FLEXARY1:11
.=
Sum ((d *. o1) . (4 + j))
by FLEXARY1:def 8
.=
((2 * (4 + j)) - 1) * (mu . ((2 * (4 + j)) - 1))
by A5
.=
((2 * j) + 7) * (mu . ((2 * j) + 7))
;
A20: (
((idseq (len mu)) (#) mu),
(7 + (j * 2)))
+...+ (
((idseq (len mu)) (#) mu),
((7 + (j * 2)) + (2 -' 1))) =
(((idseq (len mu)) (#) mu) . (7 + (j * 2))) + ((((idseq (len mu)) (#) mu),((7 + (j * 2)) + 1)) +...+ (((idseq (len mu)) (#) mu),((7 + (j * 2)) + 1)))
by NAT_1:11, FLEXARY1:13, A17
.=
(((idseq (len mu)) (#) mu) . (7 + (j * 2))) + (((idseq (len mu)) (#) mu) . ((7 + (j * 2)) + 1))
by FLEXARY1:11
;
(7 + (j * 2)) + 1
= 2
* (j + 4)
;
then
mu . ((7 + (j * 2)) + 1) = 0
by A2;
then
((idseq (len mu)) (#) mu) . ((7 + (j * 2)) + 1) = ((7 + (j * 2)) + 1) * 0
by A16, Lm2;
hence
(
(Sum (d *. o1)),
(4 + (j * 1)))
+...+ (
(Sum (d *. o1)),
((4 + (j * 1)) + (1 -' 1)))
= (
((idseq (len mu)) (#) mu),
(7 + (j * 2)))
+...+ (
((idseq (len mu)) (#) mu),
((7 + (j * 2)) + (2 -' 1)))
by A19, A20, A16, Lm2;
verum
end;
A21:
(
(Sum (d *. o1)),4)
+... = (
((idseq (len mu)) (#) mu),7)
+...
from FLEXARY1:sch 1(A18);
A22:
(2 * 1) - 1
= 1
;
then A23: 1
* (mu . 1) =
Sum ((d *. o1) . 1)
by A5
.=
(Sum (d *. o1)) . 1
by FLEXARY1:def 8
;
A24:
(2 * 2) - 1
= 3
;
then A25: 3
* (mu . 3) =
Sum ((d *. o1) . 2)
by A5
.=
(Sum (d *. o1)) . 2
by FLEXARY1:def 8
;
A26:
(2 * 3) - 1
= 5
;
then A27: 5
* (mu . 5) =
Sum ((d *. o1) . 3)
by A5
.=
(Sum (d *. o1)) . 3
by FLEXARY1:def 8
;
for
j being
Nat holds
(
(2 |^ a) . (sort _ (j,1)) = (2 |^ (a * (sort . j))) . 1 &
((2 |^ a) *. sort) . j = 2
|^ (a * (sort . j)) )
then A29:
(
(2 |^ a) . (sort _ (1,1)) = (2 |^ (a * (sort . 1))) . 1 &
(2 |^ a) . (sort _ (2,1)) = (2 |^ (a * (sort . 2))) . 1 &
(2 |^ a) . (sort _ (3,1)) = (2 |^ (a * (sort . 3))) . 1 &
((2 |^ a) *. sort) . 1
= 2
|^ (a * (sort . 1)) &
((2 |^ a) *. sort) . 2
= 2
|^ (a * (sort . 2)) &
((2 |^ a) *. sort) . 3
= 2
|^ (a * (sort . 3)) )
;
thus n =
Sum d
by Def3
.=
Sum (Sum (d *. o1))
by FLEXARY1:47
.=
(1 * (mu . 1)) + (((Sum (d *. o1)),2) +...)
by FLEXARY1:22, A23
.=
(1 * (mu . 1)) + ((3 * (mu . 3)) + (((Sum (d *. o1)),(2 + 1)) +...))
by A25, FLEXARY1:20
.=
((1 * (mu . 1)) + (3 * (mu . 3))) + (((Sum (d *. o1)),3) +...)
.=
((1 * (mu . 1)) + (3 * (mu . 3))) + ((5 * (mu . 5)) + (((Sum (d *. o1)),(3 + 1)) +...))
by FLEXARY1:20, A27
.=
(((1 * (mu . 1)) + (3 * (mu . 3))) + (5 * (mu . 5))) + ((((id (dom mu)) (#) mu),7) +...)
by A16, A21
.=
(((1 * (((2 |^ a) . (sort _ (1,1))) + (((((2 |^ a) *. sort) . 1),2) +...))) + (3 * (mu . 3))) + (5 * (mu . 5))) + ((((id (dom mu)) (#) mu),7) +...)
by A2, A22
.=
(((1 * (((2 |^ a) . (sort _ (1,1))) + (((((2 |^ a) *. sort) . 1),2) +...))) + (3 * (((2 |^ a) . (sort _ (2,1))) + (((((2 |^ a) *. sort) . 2),2) +...)))) + (5 * (mu . 5))) + ((((id (dom mu)) (#) mu),7) +...)
by A2, A24
.=
((((((2 |^ (a * (sort . 1))) . 1) + (((2 |^ (a * (sort . 1))),2) +...)) * 1) + ((((2 |^ (a * (sort . 2))) . 1) + (((2 |^ (a * (sort . 2))),2) +...)) * 3)) + ((((2 |^ (a * (sort . 3))) . 1) + (((2 |^ (a * (sort . 3))),2) +...)) * 5)) + ((((id (dom mu)) (#) mu),7) +...)
by A2, A26, A29
;
verum
end;
A30:
n = ((((mu . 1) * 1) + ((mu . 3) * 3)) + ((mu . 5) * 5)) + ((((id (dom mu)) (#) mu),7) +...)
proof
for
j being
Nat holds
(
(2 |^ a) . (sort _ (j,1)) = (2 |^ (a * (sort . j))) . 1 &
((2 |^ a) *. sort) . j = 2
|^ (a * (sort . j)) )
then A32:
(
(2 |^ a) . (sort _ (1,1)) = (2 |^ (a * (sort . 1))) . 1 &
(2 |^ a) . (sort _ (2,1)) = (2 |^ (a * (sort . 2))) . 1 &
(2 |^ a) . (sort _ (3,1)) = (2 |^ (a * (sort . 3))) . 1 &
((2 |^ a) *. sort) . 1
= 2
|^ (a * (sort . 1)) &
((2 |^ a) *. sort) . 2
= 2
|^ (a * (sort . 2)) &
((2 |^ a) *. sort) . 3
= 2
|^ (a * (sort . 3)) )
;
A33:
((2 |^ a) . (sort _ (1,1))) + (((((2 |^ a) *. sort) . 1),2) +...) = mu . ((2 * 1) - 1)
by A2;
A34:
((2 |^ a) . (sort _ (2,1))) + (((((2 |^ a) *. sort) . 2),2) +...) = mu . ((2 * 2) - 1)
by A2;
((2 |^ a) . (sort _ (3,1))) + (((((2 |^ a) *. sort) . 3),2) +...) = mu . ((2 * 3) - 1)
by A2;
hence
n = ((((mu . 1) * 1) + ((mu . 3) * 3)) + ((mu . 5) * 5)) + ((((id (dom mu)) (#) mu),7) +...)
by A33, A34, A3, A32;
verum
end;
consider h being odd-valued FinSequence such that
A35:
( h is non-decreasing & ( for i being Nat holds card (Coim (h,i)) = mu . i ) )
by Lm3, A2;
A36:
n = ((((card (Coim (h,1))) * 1) + ((card (Coim (h,3))) * 3)) + ((card (Coim (h,5))) * 5)) + ((((id (dom mu)) (#) mu),7) +...)
n = Sum h
proof
set I =
idseq (len mu);
A38:
idseq (len mu) = id (dom mu)
by FINSEQ_1:def 3;
then
((idseq (len mu)) (#) mu) . 3
= 3
* (mu . 3)
by Lm2;
then A39: (
((idseq (len mu)) (#) mu),3)
+... =
(3 * (mu . 3)) + ((((idseq (len mu)) (#) mu),(3 + 1)) +...)
by FLEXARY1:20
.=
(3 * (card (Coim (h,3)))) + ((((idseq (len mu)) (#) mu),(3 + 1)) +...)
by A35
;
A40:
(
((idseq (len mu)) (#) mu) . 4
= 4
* (mu . 4) & 4
= 2
* 2 )
by A38, Lm2;
then
mu . 4
= 0
by A2;
then A41:
(
((idseq (len mu)) (#) mu),4)
+... = 0 + ((((idseq (len mu)) (#) mu),(4 + 1)) +...)
by A40, FLEXARY1:20;
((idseq (len mu)) (#) mu) . 5
= 5
* (mu . 5)
by A38, Lm2;
then A42: (
((idseq (len mu)) (#) mu),5)
+... =
(5 * (mu . 5)) + ((((idseq (len mu)) (#) mu),(5 + 1)) +...)
by FLEXARY1:20
.=
(5 * (card (Coim (h,5)))) + ((((idseq (len mu)) (#) mu),(5 + 1)) +...)
by A35
;
A43:
(
((idseq (len mu)) (#) mu) . 6
= 6
* (mu . 6) & 6
= 3
* 2 )
by A38, Lm2;
then
mu . 6
= 0
by A2;
then A44:
(
((idseq (len mu)) (#) mu),6)
+... = 0 + ((((idseq (len mu)) (#) mu),(6 + 1)) +...)
by A43, FLEXARY1:20;
2
* 1
= 2
;
then
mu . 2
= 0
by A2;
then
2
* (mu . 2) = 0
;
hence Sum h =
((1 * (mu . 1)) + 0) + ((((id (dom mu)) (#) mu),3) +...)
by Th9, A35
.=
(1 * (card (Coim (h,1)))) + ((((id (dom mu)) (#) mu),3) +...)
by A35
.=
n
by A36, A39, A41, A38, A42, A44
;
verum
end;
then reconsider h = h as odd-valued a_partition of n by A35, Def3;
take
h
; for j being Nat
for O1 being odd-valued FinSequence
for a1 being natural-valued FinSequence st len O1 = len d & len d = len a1 & d = O1 (#) (2 |^ a1) holds
for sort being DoubleReorganization of dom d st 1 = O1 . (sort _ (1,1)) & ... & 1 = O1 . (sort _ (1,(len (sort . 1)))) & 3 = O1 . (sort _ (2,1)) & ... & 3 = O1 . (sort _ (2,(len (sort . 2)))) & 5 = O1 . (sort _ (3,1)) & ... & 5 = O1 . (sort _ (3,(len (sort . 3)))) & ( for i being Nat holds (2 * i) - 1 = O1 . (sort _ (i,1)) & ... & (2 * i) - 1 = O1 . (sort _ (i,(len (sort . i)))) ) holds
( card (Coim (h,1)) = ((2 |^ a1) . (sort _ (1,1))) + (((((2 |^ a1) *. sort) . 1),2) +...) & card (Coim (h,3)) = ((2 |^ a1) . (sort _ (2,1))) + (((((2 |^ a1) *. sort) . 2),2) +...) & card (Coim (h,5)) = ((2 |^ a1) . (sort _ (3,1))) + (((((2 |^ a1) *. sort) . 3),2) +...) & card (Coim (h,((j * 2) - 1))) = ((2 |^ a1) . (sort _ (j,1))) + (((((2 |^ a1) *. sort) . j),2) +...) )
let j be Nat; for O1 being odd-valued FinSequence
for a1 being natural-valued FinSequence st len O1 = len d & len d = len a1 & d = O1 (#) (2 |^ a1) holds
for sort being DoubleReorganization of dom d st 1 = O1 . (sort _ (1,1)) & ... & 1 = O1 . (sort _ (1,(len (sort . 1)))) & 3 = O1 . (sort _ (2,1)) & ... & 3 = O1 . (sort _ (2,(len (sort . 2)))) & 5 = O1 . (sort _ (3,1)) & ... & 5 = O1 . (sort _ (3,(len (sort . 3)))) & ( for i being Nat holds (2 * i) - 1 = O1 . (sort _ (i,1)) & ... & (2 * i) - 1 = O1 . (sort _ (i,(len (sort . i)))) ) holds
( card (Coim (h,1)) = ((2 |^ a1) . (sort _ (1,1))) + (((((2 |^ a1) *. sort) . 1),2) +...) & card (Coim (h,3)) = ((2 |^ a1) . (sort _ (2,1))) + (((((2 |^ a1) *. sort) . 2),2) +...) & card (Coim (h,5)) = ((2 |^ a1) . (sort _ (3,1))) + (((((2 |^ a1) *. sort) . 3),2) +...) & card (Coim (h,((j * 2) - 1))) = ((2 |^ a1) . (sort _ (j,1))) + (((((2 |^ a1) *. sort) . j),2) +...) )
let O1 be odd-valued FinSequence; for a1 being natural-valued FinSequence st len O1 = len d & len d = len a1 & d = O1 (#) (2 |^ a1) holds
for sort being DoubleReorganization of dom d st 1 = O1 . (sort _ (1,1)) & ... & 1 = O1 . (sort _ (1,(len (sort . 1)))) & 3 = O1 . (sort _ (2,1)) & ... & 3 = O1 . (sort _ (2,(len (sort . 2)))) & 5 = O1 . (sort _ (3,1)) & ... & 5 = O1 . (sort _ (3,(len (sort . 3)))) & ( for i being Nat holds (2 * i) - 1 = O1 . (sort _ (i,1)) & ... & (2 * i) - 1 = O1 . (sort _ (i,(len (sort . i)))) ) holds
( card (Coim (h,1)) = ((2 |^ a1) . (sort _ (1,1))) + (((((2 |^ a1) *. sort) . 1),2) +...) & card (Coim (h,3)) = ((2 |^ a1) . (sort _ (2,1))) + (((((2 |^ a1) *. sort) . 2),2) +...) & card (Coim (h,5)) = ((2 |^ a1) . (sort _ (3,1))) + (((((2 |^ a1) *. sort) . 3),2) +...) & card (Coim (h,((j * 2) - 1))) = ((2 |^ a1) . (sort _ (j,1))) + (((((2 |^ a1) *. sort) . j),2) +...) )
let a1 be natural-valued FinSequence; ( len O1 = len d & len d = len a1 & d = O1 (#) (2 |^ a1) implies for sort being DoubleReorganization of dom d st 1 = O1 . (sort _ (1,1)) & ... & 1 = O1 . (sort _ (1,(len (sort . 1)))) & 3 = O1 . (sort _ (2,1)) & ... & 3 = O1 . (sort _ (2,(len (sort . 2)))) & 5 = O1 . (sort _ (3,1)) & ... & 5 = O1 . (sort _ (3,(len (sort . 3)))) & ( for i being Nat holds (2 * i) - 1 = O1 . (sort _ (i,1)) & ... & (2 * i) - 1 = O1 . (sort _ (i,(len (sort . i)))) ) holds
( card (Coim (h,1)) = ((2 |^ a1) . (sort _ (1,1))) + (((((2 |^ a1) *. sort) . 1),2) +...) & card (Coim (h,3)) = ((2 |^ a1) . (sort _ (2,1))) + (((((2 |^ a1) *. sort) . 2),2) +...) & card (Coim (h,5)) = ((2 |^ a1) . (sort _ (3,1))) + (((((2 |^ a1) *. sort) . 3),2) +...) & card (Coim (h,((j * 2) - 1))) = ((2 |^ a1) . (sort _ (j,1))) + (((((2 |^ a1) *. sort) . j),2) +...) ) )
assume A45:
( len O1 = len d & len d = len a1 & d = O1 (#) (2 |^ a1) )
; for sort being DoubleReorganization of dom d st 1 = O1 . (sort _ (1,1)) & ... & 1 = O1 . (sort _ (1,(len (sort . 1)))) & 3 = O1 . (sort _ (2,1)) & ... & 3 = O1 . (sort _ (2,(len (sort . 2)))) & 5 = O1 . (sort _ (3,1)) & ... & 5 = O1 . (sort _ (3,(len (sort . 3)))) & ( for i being Nat holds (2 * i) - 1 = O1 . (sort _ (i,1)) & ... & (2 * i) - 1 = O1 . (sort _ (i,(len (sort . i)))) ) holds
( card (Coim (h,1)) = ((2 |^ a1) . (sort _ (1,1))) + (((((2 |^ a1) *. sort) . 1),2) +...) & card (Coim (h,3)) = ((2 |^ a1) . (sort _ (2,1))) + (((((2 |^ a1) *. sort) . 2),2) +...) & card (Coim (h,5)) = ((2 |^ a1) . (sort _ (3,1))) + (((((2 |^ a1) *. sort) . 3),2) +...) & card (Coim (h,((j * 2) - 1))) = ((2 |^ a1) . (sort _ (j,1))) + (((((2 |^ a1) *. sort) . j),2) +...) )
let sort1 be DoubleReorganization of dom d; ( 1 = O1 . (sort1 _ (1,1)) & ... & 1 = O1 . (sort1 _ (1,(len (sort1 . 1)))) & 3 = O1 . (sort1 _ (2,1)) & ... & 3 = O1 . (sort1 _ (2,(len (sort1 . 2)))) & 5 = O1 . (sort1 _ (3,1)) & ... & 5 = O1 . (sort1 _ (3,(len (sort1 . 3)))) & ( for i being Nat holds (2 * i) - 1 = O1 . (sort1 _ (i,1)) & ... & (2 * i) - 1 = O1 . (sort1 _ (i,(len (sort1 . i)))) ) implies ( card (Coim (h,1)) = ((2 |^ a1) . (sort1 _ (1,1))) + (((((2 |^ a1) *. sort1) . 1),2) +...) & card (Coim (h,3)) = ((2 |^ a1) . (sort1 _ (2,1))) + (((((2 |^ a1) *. sort1) . 2),2) +...) & card (Coim (h,5)) = ((2 |^ a1) . (sort1 _ (3,1))) + (((((2 |^ a1) *. sort1) . 3),2) +...) & card (Coim (h,((j * 2) - 1))) = ((2 |^ a1) . (sort1 _ (j,1))) + (((((2 |^ a1) *. sort1) . j),2) +...) ) )
assume A46:
( 1 = O1 . (sort1 _ (1,1)) & ... & 1 = O1 . (sort1 _ (1,(len (sort1 . 1)))) & 3 = O1 . (sort1 _ (2,1)) & ... & 3 = O1 . (sort1 _ (2,(len (sort1 . 2)))) & 5 = O1 . (sort1 _ (3,1)) & ... & 5 = O1 . (sort1 _ (3,(len (sort1 . 3)))) & ( for i being Nat holds (2 * i) - 1 = O1 . (sort1 _ (i,1)) & ... & (2 * i) - 1 = O1 . (sort1 _ (i,(len (sort1 . i)))) ) )
; ( card (Coim (h,1)) = ((2 |^ a1) . (sort1 _ (1,1))) + (((((2 |^ a1) *. sort1) . 1),2) +...) & card (Coim (h,3)) = ((2 |^ a1) . (sort1 _ (2,1))) + (((((2 |^ a1) *. sort1) . 2),2) +...) & card (Coim (h,5)) = ((2 |^ a1) . (sort1 _ (3,1))) + (((((2 |^ a1) *. sort1) . 3),2) +...) & card (Coim (h,((j * 2) - 1))) = ((2 |^ a1) . (sort1 _ (j,1))) + (((((2 |^ a1) *. sort1) . j),2) +...) )
for j being Nat st 1 <= j & j <= len d holds
( O . j = O1 . j & a . j = a1 . j )
proof
let j be
Nat;
( 1 <= j & j <= len d implies ( O . j = O1 . j & a . j = a1 . j ) )
assume A48:
( 1
<= j &
j <= len d )
;
( O . j = O1 . j & a . j = a1 . j )
A49:
(O1 . j) * ((2 |^ a1) . j) =
(O1 (#) (2 |^ a1)) . j
by VALUED_1:5
.=
(O . j) * ((2 |^ a) . j)
by VALUED_1:5, A1, A45
;
j in dom a
by A48, FINSEQ_3:25, A1;
then A50:
(2 |^ a) . j =
2
to_power (a . j)
by FLEXARY1:def 4
.=
2
|^ (a . j)
;
j in dom a1
by A48, FINSEQ_3:25, A45;
then A51:
(2 |^ a1) . j =
2
to_power (a1 . j)
by FLEXARY1:def 4
.=
2
|^ (a1 . j)
;
j in dom O
by A48, FINSEQ_3:25, A1;
then
O . j is
odd Nat
by Def2;
then consider i1 being
Nat such that A52:
O . j = (2 * i1) + 1
by ABIAN:9;
j in dom O1
by A48, FINSEQ_3:25, A45;
then
O1 . j is
odd Nat
by Def2;
then
ex
i2 being
Nat st
O1 . j = (2 * i2) + 1
by ABIAN:9;
hence
(
O . j = O1 . j &
a . j = a1 . j )
by A50, A51, A52, A49, CARD_4:4;
verum
end;
then A53:
( O = O1 & a = a1 )
by A45, A1;
A54:
for j being Nat holds card (Coim (h,((j * 2) - 1))) = ((2 |^ a1) . (sort1 _ (j,1))) + (((((2 |^ a1) *. sort1) . j),2) +...)
proof
let j be
Nat;
card (Coim (h,((j * 2) - 1))) = ((2 |^ a1) . (sort1 _ (j,1))) + (((((2 |^ a1) *. sort1) . j),2) +...)
A55:
(2 |^ a) . (sort _ (j,1)) = ((2 |^ a) *. sort) _ (
j,1)
by FLEXARY1:42;
A56:
len (2 |^ a) = len a
by CARD_1:def 7;
then A57:
(
dom O = dom d &
dom d = dom a &
dom (2 |^ a) = dom a )
by A1, FINSEQ_3:29;
card (Coim (h,((j * 2) - 1))) = mu . ((2 * j) - 1)
then A60:
card (Coim (h,((j * 2) - 1))) =
((((2 |^ a) *. sort) . j) . 1) + (((((2 |^ a) *. sort) . j),2) +...)
by A2, A55
.=
Sum (((2 |^ a) *. sort) . j)
by FLEXARY1:22
;
reconsider S =
sort1 as
DoubleReorganization of
dom (2 |^ a) by A56, A1, FINSEQ_3:29;
(2 |^ a1) . (sort1 _ (j,1)) = ((2 |^ a1) *. sort1) _ (
j,1)
by FLEXARY1:42;
then A61:
((2 |^ a1) . (sort1 _ (j,1))) + (((((2 |^ a1) *. sort1) . j),2) +...) = Sum (((2 |^ a) *. S) . j)
by A53, FLEXARY1:22;
A62:
sort1 is
odd_organization of
O
by A57, Th4, A46, A53;
thus card (Coim (h,((j * 2) - 1))) =
(Sum ((2 |^ a) *. sort)) . j
by FLEXARY1:def 8, A60
.=
(Sum ((2 |^ a) *. S)) . j
by A62, Th5
.=
((2 |^ a1) . (sort1 _ (j,1))) + (((((2 |^ a1) *. sort1) . j),2) +...)
by FLEXARY1:def 8, A61
;
verum
end;
( (2 * 1) - 1 = 1 & (2 * 2) - 1 = 3 & (2 * 3) - 1 = 5 )
;
hence
( card (Coim (h,1)) = ((2 |^ a1) . (sort1 _ (1,1))) + (((((2 |^ a1) *. sort1) . 1),2) +...) & card (Coim (h,3)) = ((2 |^ a1) . (sort1 _ (2,1))) + (((((2 |^ a1) *. sort1) . 2),2) +...) & card (Coim (h,5)) = ((2 |^ a1) . (sort1 _ (3,1))) + (((((2 |^ a1) *. sort1) . 3),2) +...) & card (Coim (h,((j * 2) - 1))) = ((2 |^ a1) . (sort1 _ (j,1))) + (((((2 |^ a1) *. sort1) . j),2) +...) )
by A54; verum