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:33;
then A5: dom ((q ") * p) = dom p by RELAT_1:27
.= 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:28
.= dom q by A3, FUNCT_1:33
.= Seg (len q) by FINSEQ_1:def 3 ;
then r is one-to-one by A2, A5, Th60;
hence p is one-to-one by A4, FUNCT_1:26; :: thesis: verum