let x be object ; :: thesis: 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))
let n be Nat; :: thesis: for f1, f2 being n -element real-valued FinSequence holds (abs (f1 - f2)) . x <= (abs (f1 - f2)) . (max_diff_index (f1,f2))
let f1, f2 be n -element real-valued FinSequence; :: thesis: (abs (f1 - f2)) . x <= (abs (f1 - f2)) . (max_diff_index (f1,f2))
set F = abs (f1 - f2);
A1: dom (abs (f1 - f2)) = dom (f1 - f2) by VALUED_1:def 11
.= (dom f1) /\ (dom f2) by VALUED_1:12 ;
set m = max_diff_index (f1,f2);
A2: ( dom f1 = Seg n & dom f2 = Seg n ) by FINSEQ_1:89;

per cases ( x in dom f1 or not x in dom f1 ) ;

suppose x in dom f1 ; :: thesis: (abs (f1 - f2)) . x <= (abs (f1 - f2)) . (max_diff_index (f1,f2))

then A3: (abs (f1 - f2)) . x in rng (abs (f1 - f2)) by A2, A1, FUNCT_1:def 3;
then sup (rng (abs (f1 - f2))) in rng (abs (f1 - f2)) by XXREAL_2:def 6;
then (abs (f1 - f2)) " {(sup (rng (abs (f1 - f2))))} <> {} by FUNCT_1:72;
then (abs (f1 - f2)) . (max_diff_index (f1,f2)) in {(sup (rng (abs (f1 - f2))))} by FUNCT_1:def 7;
then (abs (f1 - f2)) . (max_diff_index (f1,f2)) = sup (rng (abs (f1 - f2))) by TARSKI:def 1;
hence (abs (f1 - f2)) . x <= (abs (f1 - f2)) . (max_diff_index (f1,f2)) by A3, XXREAL_2:4; :: thesis: verum

end;

suppose not x in dom f1 ; :: thesis: (abs (f1 - f2)) . x <= (abs (f1 - f2)) . (max_diff_index (f1,f2))

then A4: not x in dom (abs (f1 - f2)) by A1, XBOOLE_0:def 4;
(abs (f1 - f2)) . (max_diff_index (f1,f2)) = |.((f1 - f2) . (max_diff_index (f1,f2))).| by VALUED_1:18;
hence (abs (f1 - f2)) . x <= (abs (f1 - f2)) . (max_diff_index (f1,f2)) by A4, FUNCT_1:def 2; :: thesis: verum

end;

end;