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

2 in Seg (len f) by A2, FINSEQ_1:1;
then A4: 2 in dom f by FINSEQ_1:def 3;
1 in Seg (len f) by A2, FINSEQ_1:1;
then A5: 1 in dom f by FINSEQ_1:def 3;
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, Th7; :: thesis: verum