theorem Th5: :: EULRPART:5

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