for n being Nat
for F, F2 being FinSequence of REAL n
for h being Permutation of (dom F) st F2 = F (*) h holds
Sum F2 = Sum F