let i be Nat; :: thesis: for O being odd-valued FinSequence
for a being natural-valued FinSequence
for s being odd_organization of O st len O = len a & O (#) (2 |^ a) is one-to-one holds
(a *. s) . i is one-to-one
let O be odd-valued FinSequence; :: thesis: for a being natural-valued FinSequence
for s being odd_organization of O st len O = len a & O (#) (2 |^ a) is one-to-one holds
(a *. s) . i is one-to-one
let a be natural-valued FinSequence; :: thesis: for s being odd_organization of O st len O = len a & O (#) (2 |^ a) is one-to-one holds
(a *. s) . i is one-to-one
let s be odd_organization of O; :: thesis: ( len O = len a & O (#) (2 |^ a) is one-to-one implies (a *. s) . i is one-to-one )
set p = O (#) (2 |^ a);
assume A1: ( len O = len a & O (#) (2 |^ a) is one-to-one ) ; :: thesis: (a *. s) . i is one-to-one
then reconsider S = s as DoubleReorganization of dom a by FINSEQ_3:29;
A2: (a *. S) . i = a * (S . i) by FLEXARY1:41;
thus (a *. s) . i is one-to-one :: thesis: verum

proof

assume not (a *. s) . i is one-to-one ; :: thesis: contradiction
then consider x1, x2 being object such that
A3: ( x1 in dom ((a *. S) . i) & x2 in dom ((a *. S) . i) & ((a *. S) . i) . x1 = ((a *. S) . i) . x2 & x1 <> x2 ) ;
reconsider x1 = x1, x2 = x2 as Nat by A3;
set s1 = s _ (i,x1);
set s2 = s _ (i,x2);
A4: ( x1 in dom (s . i) & s _ (i,x1) in dom a & a . (s _ (i,x1)) = ((a *. S) . i) . x1 ) by A2, A3, FUNCT_1:11, FUNCT_1:12;
A5: ( x2 in dom (S . i) & s _ (i,x2) in dom a & a . (s _ (i,x2)) = ((a *. S) . i) . x2 ) by A2, A3, FUNCT_1:11, FUNCT_1:12;
A6: (2 * i) - 1 = O . (s _ (i,1)) & ... & (2 * i) - 1 = O . (s _ (i,(len (s . i)))) by Def4;
( 1 <= x1 & x1 <= len (s . i) ) by A4, FINSEQ_3:25;
then A7: (2 * i) - 1 = O . (s _ (i,x1)) by A6;
( 1 <= x2 & x2 <= len (s . i) ) by A5, FINSEQ_3:25;
then A8: (2 * i) - 1 = O . (s _ (i,x2)) by A6;
O is len O -element by CARD_1:def 7;
then A9: len (O (#) (2 |^ a)) = len a by A1, CARD_1:def 7;
A10: ( 1 <= (s . i) . x1 & (s . i) . x1 <= len a ) by A4, FINSEQ_3:25;
( 1 <= (s . i) . x2 & (s . i) . x2 <= len a ) by A5, FINSEQ_3:25;
then A11: ( s _ (i,x2) in dom (O (#) (2 |^ a)) & s _ (i,x1) in dom (O (#) (2 |^ a)) ) by A9, A10, FINSEQ_3:25;
A12: (O (#) (2 |^ a)) . (s _ (i,x1)) = (O . (s _ (i,x1))) * ((2 |^ a) . (s _ (i,x1))) by VALUED_1:5;
A13: (2 |^ a) . (s _ (i,x1)) = 2 to_power (a . (s _ (i,x1))) by A4, FLEXARY1:def 4;
(O (#) (2 |^ a)) . (s _ (i,x2)) = (O . (s _ (i,x2))) * ((2 |^ a) . (s _ (i,x2))) by VALUED_1:5;
then (O (#) (2 |^ a)) . (s _ (i,x2)) = (O (#) (2 |^ a)) . (s _ (i,x1)) by A5, FLEXARY1:def 4, A13, A12, A7, A8, A4, A3;
then s _ (i,x2) = s _ (i,x1) by A11, A1;
hence contradiction by A4, A5, FUNCT_1:def 4, A3; :: thesis: verum

end;