theorem Th27: :: FLEXARY1:27

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