:: deftheorem defines max_diff_index EUCLID_9:def 1 :
for n being Nat
for f1, f2 being b₁ -element real-valued FinSequence holds max_diff_index (f1,f2) = the Element of (abs (f1 - f2)) " {(sup (rng (abs (f1 - f2))))};