let x be set ; :: thesis: for n being Nat
for f1, f2 being real-valued b₁ -long FinSequence holds (abs (f1 - f2)) . x <= (abs (f1 - f2)) . (max_diff_index f1,f2)
let n be Nat; :: thesis: for f1, f2 being real-valued n -long FinSequence holds (abs (f1 - f2)) . x <= (abs (f1 - f2)) . (max_diff_index f1,f2)
let f1, f2 be real-valued n -long 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 EUCLID:3;

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 5;
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:142;
then (abs (f1 - f2)) . (max_diff_index f1,f2) in {(sup (rng (abs (f1 - f2))))} by FUNCT_1:def 13;
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) = abs ((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 4; :: thesis: verum

end;

end;