theorem :: FLEXARY1:49

for n being Nat
for f being finite Function
for o being valued_reorganization of f holds
( rng ((f *. o) . n) = {} or ( rng ((f *. o) . n) = {(f . (o _ (n,1)))} & 1 in dom (o . n) ) )