theorem :: EUCLID_9:4

for n being Nat
for f1, f2 being b₁ -element real-valued FinSequence st n <> 0 holds
max_diff_index (f1,f2) in dom f1