theorem :: FLEXARY1:51

for i being Nat
for f being FinSequence
for g being complex-valued FinSequence
for o1, o2 being DoubleReorganization of dom g st o1 is valued_reorganization of f & o2 is valued_reorganization of f & rng ((f *. o1) . i) = rng ((f *. o2) . i) holds
(Sum (g *. o1)) . i = (Sum (g *. o2)) . i