let E1, E2 be odd-valued a_partition of n; ( ( for j being Nat
for O being odd-valued FinSequence
for a being natural-valued FinSequence st len O = len p & len p = len a & p = O (#) (2 |^ a) holds
for sort being DoubleReorganization of dom p st 1 = O . (sort _ (1,1)) & ... & 1 = O . (sort _ (1,(len (sort . 1)))) & 3 = O . (sort _ (2,1)) & ... & 3 = O . (sort _ (2,(len (sort . 2)))) & 5 = O . (sort _ (3,1)) & ... & 5 = O . (sort _ (3,(len (sort . 3)))) & ( for i being Nat holds (2 * i) - 1 = O . (sort _ (i,1)) & ... & (2 * i) - 1 = O . (sort _ (i,(len (sort . i)))) ) holds
( card (Coim (E1,1)) = ((2 |^ a) . (sort _ (1,1))) + (((((2 |^ a) *. sort) . 1),2) +...) & card (Coim (E1,3)) = ((2 |^ a) . (sort _ (2,1))) + (((((2 |^ a) *. sort) . 2),2) +...) & card (Coim (E1,5)) = ((2 |^ a) . (sort _ (3,1))) + (((((2 |^ a) *. sort) . 3),2) +...) & card (Coim (E1,((j * 2) - 1))) = ((2 |^ a) . (sort _ (j,1))) + (((((2 |^ a) *. sort) . j),2) +...) ) ) & ( for j being Nat
for O being odd-valued FinSequence
for a being natural-valued FinSequence st len O = len p & len p = len a & p = O (#) (2 |^ a) holds
for sort being DoubleReorganization of dom p st 1 = O . (sort _ (1,1)) & ... & 1 = O . (sort _ (1,(len (sort . 1)))) & 3 = O . (sort _ (2,1)) & ... & 3 = O . (sort _ (2,(len (sort . 2)))) & 5 = O . (sort _ (3,1)) & ... & 5 = O . (sort _ (3,(len (sort . 3)))) & ( for i being Nat holds (2 * i) - 1 = O . (sort _ (i,1)) & ... & (2 * i) - 1 = O . (sort _ (i,(len (sort . i)))) ) holds
( card (Coim (E2,1)) = ((2 |^ a) . (sort _ (1,1))) + (((((2 |^ a) *. sort) . 1),2) +...) & card (Coim (E2,3)) = ((2 |^ a) . (sort _ (2,1))) + (((((2 |^ a) *. sort) . 2),2) +...) & card (Coim (E2,5)) = ((2 |^ a) . (sort _ (3,1))) + (((((2 |^ a) *. sort) . 3),2) +...) & card (Coim (E2,((j * 2) - 1))) = ((2 |^ a) . (sort _ (j,1))) + (((((2 |^ a) *. sort) . j),2) +...) ) ) implies E1 = E2 )
assume that
A1:
for j being Nat
for O being odd-valued FinSequence
for a being natural-valued FinSequence st len O = len p & len p = len a & p = O (#) (2 |^ a) holds
for sort being DoubleReorganization of dom p st 1 = O . (sort _ (1,1)) & ... & 1 = O . (sort _ (1,(len (sort . 1)))) & 3 = O . (sort _ (2,1)) & ... & 3 = O . (sort _ (2,(len (sort . 2)))) & 5 = O . (sort _ (3,1)) & ... & 5 = O . (sort _ (3,(len (sort . 3)))) & ( for i being Nat holds (2 * i) - 1 = O . (sort _ (i,1)) & ... & (2 * i) - 1 = O . (sort _ (i,(len (sort . i)))) ) holds
( card (Coim (E1,1)) = ((2 |^ a) . (sort _ (1,1))) + (((((2 |^ a) *. sort) . 1),2) +...) & card (Coim (E1,3)) = ((2 |^ a) . (sort _ (2,1))) + (((((2 |^ a) *. sort) . 2),2) +...) & card (Coim (E1,5)) = ((2 |^ a) . (sort _ (3,1))) + (((((2 |^ a) *. sort) . 3),2) +...) & card (Coim (E1,((j * 2) - 1))) = ((2 |^ a) . (sort _ (j,1))) + (((((2 |^ a) *. sort) . j),2) +...) )
and
A2:
for j being Nat
for O being odd-valued FinSequence
for a being natural-valued FinSequence st len O = len p & len p = len a & p = O (#) (2 |^ a) holds
for sort being DoubleReorganization of dom p st 1 = O . (sort _ (1,1)) & ... & 1 = O . (sort _ (1,(len (sort . 1)))) & 3 = O . (sort _ (2,1)) & ... & 3 = O . (sort _ (2,(len (sort . 2)))) & 5 = O . (sort _ (3,1)) & ... & 5 = O . (sort _ (3,(len (sort . 3)))) & ( for i being Nat holds (2 * i) - 1 = O . (sort _ (i,1)) & ... & (2 * i) - 1 = O . (sort _ (i,(len (sort . i)))) ) holds
( card (Coim (E2,1)) = ((2 |^ a) . (sort _ (1,1))) + (((((2 |^ a) *. sort) . 1),2) +...) & card (Coim (E2,3)) = ((2 |^ a) . (sort _ (2,1))) + (((((2 |^ a) *. sort) . 2),2) +...) & card (Coim (E2,5)) = ((2 |^ a) . (sort _ (3,1))) + (((((2 |^ a) *. sort) . 3),2) +...) & card (Coim (E2,((j * 2) - 1))) = ((2 |^ a) . (sort _ (j,1))) + (((((2 |^ a) *. sort) . j),2) +...) )
; E1 = E2
consider O being odd-valued FinSequence, a being natural-valued FinSequence such that
A3:
( len O = len p & len p = len a & p = O (#) (2 |^ a) )
and
p . 1 = (O . 1) * (2 |^ (a . 1)) & ... & p . (len p) = (O . (len p)) * (2 |^ (a . (len p)))
by Th6;
reconsider sort = the odd_organization of O as DoubleReorganization of dom p by A3, FINSEQ_3:29;
A4:
(2 * 1) - 1 = 1
;
A5:
(2 * 2) - 1 = 3
;
(2 * 3) - 1 = 5
;
then A6:
( 1 = O . (sort _ (1,1)) & ... & 1 = O . (sort _ (1,(len (sort . 1)))) & 3 = O . (sort _ (2,1)) & ... & 3 = O . (sort _ (2,(len (sort . 2)))) & 5 = O . (sort _ (3,1)) & ... & 5 = O . (sort _ (3,(len (sort . 3)))) & ( for i being Nat holds (2 * i) - 1 = O . (sort _ (i,1)) & ... & (2 * i) - 1 = O . (sort _ (i,(len (sort . i)))) ) )
by A4, Def4, A5;
A7:
for x being object holds card (Coim (E1,x)) = card (Coim (E2,x))
proof
let x be
object ;
card (Coim (E1,x)) = card (Coim (E2,x))
per cases
( not x in OddNAT or x in OddNAT )
;
suppose
x in OddNAT
;
card (Coim (E1,x)) = card (Coim (E2,x))then consider i being
Element of
NAT such that A9:
x = (2 * i) + 1
by FIB_NUM2:def 4;
set i1 =
i + 1;
card (Coim (E1,(((i + 1) * 2) - 1))) =
((2 |^ a) . (sort _ ((i + 1),1))) + (((((2 |^ a) *. sort) . (i + 1)),2) +...)
by A1, A3, A6
.=
card (Coim (E2,(((i + 1) * 2) - 1)))
by A6, A3, A2
;
hence
card (Coim (E1,x)) = card (Coim (E2,x))
by A9;
verum end; end;
end;
thus
E1 = E2
verum