for i being Nat
for f being FinSequence
for o1, o2 being valued_reorganization of f st rng ((f *. o1) . i) = rng ((f *. o2) . i) holds
rng (o1 . i) = rng (o2 . i) by Lm7;