theorem :: FLEXARY1:39

for F being non empty FinSequence
for G being FinSequence st rng G c= rng F holds
ex o being len b₁ -element DoubleReorganization of dom G st
for n being Nat holds
( o . n is increasing & F . n = G . (o _ (n,1)) & ... & F . n = G . (o _ (n,(len (o . n)))) )