let i be Nat; :: thesis: for f1, f2 being n -element real-valued FinSequence st i = the Element of (abs (f1 - f2)) " {(sup (rng (abs (f1 - f2))))} holds
i = the Element of (abs (f2 - f1)) " {(sup (rng (abs (f2 - f1))))}
let f1, f2 be n -element real-valued FinSequence; :: thesis: ( i = the Element of (abs (f1 - f2)) " {(sup (rng (abs (f1 - f2))))} implies i = the Element of (abs (f2 - f1)) " {(sup (rng (abs (f2 - f1))))} )
abs (f1 - f2) = abs (f2 - f1) by Th3;
hence ( i = the Element of (abs (f1 - f2)) " {(sup (rng (abs (f1 - f2))))} implies i = the Element of (abs (f2 - f1)) " {(sup (rng (abs (f2 - f1))))} ) ; :: thesis: verum