let p, q be FinSequence of REAL ; :: thesis: ( rng p = rng q & p is increasing & q is increasing implies p = q )
assume A1: rng p = rng q ; :: thesis: ( not p is increasing or not q is increasing or p = q )
assume that
A2: p is increasing and
A3: q is increasing ; :: thesis: p = q
A4: q is one-to-one by A3;
p is one-to-one by A2;
then len p = len q by A1, A4, FINSEQ_1:48;
hence p = q by A1, A2, A3, SEQ_4:141; :: thesis: verum