let p, q be FinSequence; :: thesis: ( rng p = rng q & len p = len q & q is one-to-one implies p is one-to-one )
assume that
A1: rng p = rng q and
A2: len p = len q and
A3: q is one-to-one ; :: thesis: p is one-to-one
A4: rng p = dom (q " ) by A1, A3, FUNCT_1:55;
then A5: dom ((q " ) * p) = dom p by RELAT_1:46
.= Seg (len p) by FINSEQ_1:def 3 ;
then reconsider r = (q " ) * p as FinSequence by FINSEQ_1:def 2;
rng r = rng (q " ) by A4, RELAT_1:47
.= dom q by A3, FUNCT_1:55
.= Seg (len q) by FINSEQ_1:def 3 ;
then r is one-to-one by A2, A5, Th75;
hence p is one-to-one by A4, FUNCT_1:48; :: thesis: verum