let r, s be Real; :: thesis: for f being increasing FinSequence of REAL st rng f = {r,s} & len f = 2 & r <= s holds
( f . 1 = r & f . 2 = s )
let f be increasing FinSequence of REAL ; :: thesis: ( rng f = {r,s} & len f = 2 & r <= s implies ( f . 1 = r & f . 2 = s ) )
assume that
A1: rng f = {r,s} and
A2: len f = 2 and
A3: r <= s ; :: thesis: ( f . 1 = r & f . 2 = s )

now :: thesis: ( f . 1 = s & f . 2 = r implies ( f . 1 = r & f . 2 = s ) )

A4: 2 in dom f by A2, FINSEQ_3:25;
A5: 1 in dom f by A2, FINSEQ_3:25;
assume ( f . 1 = s & f . 2 = r ) ; :: thesis: ( f . 1 = r & f . 2 = s )
hence ( f . 1 = r & f . 2 = s ) by A3, A5, A4, SEQM_3:def 1; :: thesis: verum

end;

hence ( f . 1 = r & f . 2 = s ) by A1, A2, FINSEQ_3:151; :: thesis: verum