let n be Nat; :: thesis: for f1, f2 being n -element real-valued FinSequence st n <> 0 holds
max_diff_index (f1,f2) in dom f1
let f1, f2 be n -element real-valued FinSequence; :: thesis: ( n <> 0 implies max_diff_index (f1,f2) in dom f1 )
set F = abs (f1 - f2);
assume n <> 0 ; :: thesis: max_diff_index (f1,f2) in dom f1
then not abs (f1 - f2) is empty ;
then sup (rng (abs (f1 - f2))) in rng (abs (f1 - f2)) by XXREAL_2:def 6;
then A1: (abs (f1 - f2)) " {(sup (rng (abs (f1 - f2))))} <> {} by FUNCT_1:72;
A2: dom f1 = Seg n by FINSEQ_1:89;
A3: dom (abs (f1 - f2)) = Seg n by FINSEQ_1:89;
A4: (abs (f1 - f2)) " {(sup (rng (abs (f1 - f2))))} c= dom (abs (f1 - f2)) by RELAT_1:132;
max_diff_index (f1,f2) in (abs (f1 - f2)) " {(sup (rng (abs (f1 - f2))))} by A1;
hence max_diff_index (f1,f2) in dom f1 by A4, A2, A3; :: thesis: verum