theorem Th37: :: FLEXARY1:37

for i being Nat
for D being finite set
for o being DoubleReorganization of D
for F being one-to-one FinSequence st i in dom o & (rng F) /\ D c= rng (o . i) holds
o +* (i,F) is DoubleReorganization of (rng F) \/ (D \ (rng (o . i)))