for x being object
for n being Nat
for f1, f2 being b₂ -element real-valued FinSequence holds (abs (f1 - f2)) . x <= (abs (f1 - f2)) . (max_diff_index (f1,f2))