theorem :: FLEXARY1:47

for f being complex-valued FinSequence
for o being DoubleReorganization of dom f holds Sum f = Sum (Sum (f *. o))