theorem :: MATRTOP1:10

for X being set
for cf, cf1 being complex-valued FinSubsequence
for P being Permutation of (dom cf) st cf1 = cf * P holds
Sum (Seq (cf | X)) = Sum (Seq (cf1 | (P " X)))