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

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