:: deftheorem Def9 defines valued_reorganization FLEXARY1:def 9 :
for f being finite Function
for b₂ being DoubleReorganization of dom f holds
( b₂ is valued_reorganization of f iff ( ( for n being Nat ex x being object st x = f . (b₂ _ (n,1)) & ... & x = f . (b₂ _ (n,(len (b₂ . n)))) ) & ( for n1, n2, i1, i2 being Nat st i1 in dom (b₂ . n1) & i2 in dom (b₂ . n2) & f . (b₂ _ (n1,i1)) = f . (b₂ _ (n2,i2)) holds
n1 = n2 ) ) );