let f be odd-valued FinSequence; :: thesis: for o being DoubleReorganization of dom f st ( for n being Nat holds (2 * n) - 1 = f . (o _ (n,1)) & ... & (2 * n) - 1 = f . (o _ (n,(len (o . n)))) ) holds
o is odd_organization of f
let o be DoubleReorganization of dom f; :: thesis: ( ( for n being Nat holds (2 * n) - 1 = f . (o _ (n,1)) & ... & (2 * n) - 1 = f . (o _ (n,(len (o . n)))) ) implies o is odd_organization of f )
assume A1: for n being Nat holds (2 * n) - 1 = f . (o _ (n,1)) & ... & (2 * n) - 1 = f . (o _ (n,(len (o . n)))) ; :: thesis: o is odd_organization of f
A2: for n being Nat ex x being object st x = f . (o _ (n,1)) & ... & x = f . (o _ (n,(len (o . n))))
proof
let n be Nat; :: thesis: ex x being object st x = f . (o _ (n,1)) & ... & x = f . (o _ (n,(len (o . n))))
take x = (2 * n) - 1; :: thesis: x = f . (o _ (n,1)) & ... & x = f . (o _ (n,(len (o . n))))
thus x = f . (o _ (n,1)) & ... & x = f . (o _ (n,(len (o . n)))) by A1; :: thesis: verum
end;
for n1, n2, i1, i2 being Nat st i1 in dom (o . n1) & i2 in dom (o . n2) & f . (o _ (n1,i1)) = f . (o _ (n2,i2)) holds
n1 = n2
proof
let n1, n2, i1, i2 be Nat; :: thesis: ( i1 in dom (o . n1) & i2 in dom (o . n2) & f . (o _ (n1,i1)) = f . (o _ (n2,i2)) implies n1 = n2 )
assume A3: ( i1 in dom (o . n1) & i2 in dom (o . n2) & f . (o _ (n1,i1)) = f . (o _ (n2,i2)) ) ; :: thesis: n1 = n2
A4: (2 * n1) - 1 = f . (o _ (n1,1)) & ... & (2 * n1) - 1 = f . (o _ (n1,(len (o . n1)))) by A1;
( 1 <= i1 & i1 <= len (o . n1) ) by A3, FINSEQ_3:25;
then A5: f . (o _ (n1,i1)) = (2 * n1) - 1 by A4;
A6: (2 * n2) - 1 = f . (o _ (n2,1)) & ... & (2 * n2) - 1 = f . (o _ (n2,(len (o . n2)))) by A1;
( 1 <= i2 & i2 <= len (o . n2) ) by A3, FINSEQ_3:25;
then (2 * n2) - 1 = (2 * n1) - 1 by A6, A5, A3;
hence n1 = n2 ; :: thesis: verum
end;
then o is valued_reorganization of f by A2, FLEXARY1:def 9;
hence o is odd_organization of f by A1, Def4; :: thesis: verum