theorem :: FLEXARY1:30

for n being Nat
for f1, f2 being one-to-one natural-valued FinSequence st n > 1 & ((n |^ f1) . 1) + (((n |^ f1),2) +...) = ((n |^ f2) . 1) + (((n |^ f2),2) +...) holds
rng f1 = rng f2