:: deftheorem Def7 defines DoubleReorganization FLEXARY1:def 7 :
for D being finite set
for b₂ being double-one-to-one FinSequence of D * holds
( b₂ is DoubleReorganization of D iff Values b₂ = D );