theorem Th38: :: FLEXARY1:38

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