let v be FinSequence of REAL ; :: thesis: ( v is increasing implies for n, m being Nat st n in dom v & m in dom v & n <> m holds
v . n <> v . m )
assume A1: v is increasing ; :: thesis: for n, m being Nat st n in dom v & m in dom v & n <> m holds
v . n <> v . m
let n, m be Nat; :: thesis: ( n in dom v & m in dom v & n <> m implies v . n <> v . m )
assume that
A2: ( n in dom v & m in dom v ) and
A3: n <> m ; :: thesis: v . n <> v . m

now :: thesis: v . n <> v . m

per cases ( n < m or n > m ) by A3, XXREAL_0:1;

suppose n < m ; :: thesis: v . n <> v . m

hence v . n <> v . m by A1, A2, SEQM_3:def 1; :: thesis: verum

end;

suppose n > m ; :: thesis: v . n <> v . m

hence v . n <> v . m by A1, A2, SEQM_3:def 1; :: thesis: verum

end;

end;

end;

hence v . n <> v . m ; :: thesis: verum