let D be set ; :: thesis: for p1, p2 being FinSequence of D st p1 is one-to-one & p2 is one-to-one & rng p1 = rng p2 holds
( dom p1 = dom p2 & ex P being Permutation of (dom p1) st
( p2 = p1 * P & dom P = dom p1 & rng P = dom p1 ) )
let p1, p2 be FinSequence of D; :: thesis: ( p1 is one-to-one & p2 is one-to-one & rng p1 = rng p2 implies ( dom p1 = dom p2 & ex P being Permutation of (dom p1) st
( p2 = p1 * P & dom P = dom p1 & rng P = dom p1 ) ) )
assume that
A1: p1 is one-to-one and
A2: p2 is one-to-one and
A3: rng p1 = rng p2 ; :: thesis: ( dom p1 = dom p2 & ex P being Permutation of (dom p1) st
( p2 = p1 * P & dom P = dom p1 & rng P = dom p1 ) )
set P = (p1 " ) * p2;
len p1 = card (rng p2) by A1, A3, FINSEQ_4:77
.= len p2 by A2, FINSEQ_4:77 ;
then A4: dom p1 = Seg (len p2) by FINSEQ_1:def 3
.= dom p2 by FINSEQ_1:def 3 ;

A5: now

let xd be set ; :: thesis: ( xd in dom ((p1 " ) * p2) iff xd in dom p2 )
dom (p1 " ) = rng p1 by A1, FUNCT_1:55;
then ( xd in dom p2 implies p2 . xd in dom (p1 " ) ) by A3, FUNCT_1:12;
hence ( xd in dom ((p1 " ) * p2) iff xd in dom p2 ) by FUNCT_1:21; :: thesis: verum

end;

then A6: dom ((p1 " ) * p2) = dom p2 by TARSKI:2;
A7: rng (p1 " ) = dom p1 by A1, FUNCT_1:55;
A8: rng ((p1 " ) * p2) c= dom p1

proof

let xd be set ; :: according to TARSKI:def 3 :: thesis: ( not xd in rng ((p1 " ) * p2) or xd in dom p1 )
assume xd in rng ((p1 " ) * p2) ; :: thesis: xd in dom p1
hence xd in dom p1 by A7, FUNCT_1:25; :: thesis: verum

end;

A9: dom p1 c= rng ((p1 " ) * p2)

proof

let xd be set ; :: according to TARSKI:def 3 :: thesis: ( not xd in dom p1 or xd in rng ((p1 " ) * p2) )
assume xd in dom p1 ; :: thesis: xd in rng ((p1 " ) * p2)
then xd in rng (p1 " ) by A1, FUNCT_1:55;
then consider yd being set such that
A10: yd in dom (p1 " ) and
A11: xd = (p1 " ) . yd by FUNCT_1:def 5;
yd in rng p2 by A1, A3, A10, FUNCT_1:55;
then consider z being set such that
A12: z in dom p2 and
A13: yd = p2 . z by FUNCT_1:def 5;
xd = ((p1 " ) * p2) . z by A11, A12, A13, FUNCT_1:23;
hence xd in rng ((p1 " ) * p2) by A6, A12, FUNCT_1:def 5; :: thesis: verum

end;

A14: dom ((p1 " ) * p2) = dom p1 by A4, A5, TARSKI:2;
A15: rng ((p1 " ) * p2) = dom p1 by A8, A9, XBOOLE_0:def 10;
then (p1 " ) * p2 is Function of (dom p1),(dom p1) by A14, FUNCT_2:3;
then A16: (p1 " ) * p2 is Permutation of (dom p1) by A1, A2, A15, FUNCT_2:83;

now

let xd be set ; :: thesis: ( xd in dom (p1 * ((p1 " ) * p2)) iff xd in dom p1 )
( xd in dom ((p1 " ) * p2) implies ((p1 " ) * p2) . xd in dom p1 ) by A15, FUNCT_1:12;
hence ( xd in dom (p1 * ((p1 " ) * p2)) iff xd in dom p1 ) by A14, FUNCT_1:21; :: thesis: verum

end;

then A17: dom p2 = dom (p1 * ((p1 " ) * p2)) by A4, TARSKI:2;
for xd being set st xd in dom p2 holds
p2 . xd = (p1 * ((p1 " ) * p2)) . xd

proof

let xd be set ; :: thesis: ( xd in dom p2 implies p2 . xd = (p1 * ((p1 " ) * p2)) . xd )
assume A18: xd in dom p2 ; :: thesis: p2 . xd = (p1 * ((p1 " ) * p2)) . xd
then A19: p2 . xd in rng p1 by A3, FUNCT_1:12;
(p1 * ((p1 " ) * p2)) . xd = p1 . (((p1 " ) * p2) . xd) by A4, A14, A18, FUNCT_1:23
.= p1 . ((p1 " ) . (p2 . xd)) by A18, FUNCT_1:23
.= p2 . xd by A1, A19, FUNCT_1:57 ;
hence p2 . xd = (p1 * ((p1 " ) * p2)) . xd ; :: thesis: verum

end;

hence ( dom p1 = dom p2 & ex P being Permutation of (dom p1) st
( p2 = p1 * P & dom P = dom p1 & rng P = dom p1 ) ) by A4, A14, A15, A16, A17, FUNCT_1:9; :: thesis: verum