let D be set ; 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; ( 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
; ( 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:62
.=
len p2
by A2, FINSEQ_4:62
;
then A4: dom p1 =
Seg (len p2)
by FINSEQ_1:def 3
.=
dom p2
by FINSEQ_1:def 3
;
then A6:
dom ((p1 ") * p2) = dom p2
by TARSKI:2;
A7:
rng (p1 ") = dom p1
by A1, FUNCT_1:33;
A8:
rng ((p1 ") * p2) c= dom p1
by A7, FUNCT_1:14;
A9:
dom p1 c= rng ((p1 ") * p2)
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:1;
then A16:
(p1 ") * p2 is Permutation of (dom p1)
by A1, A2, A15, FUNCT_2:57;
then A17:
dom p2 = dom (p1 * ((p1 ") * p2))
by A4, TARSKI:2;
for xd being object st xd in dom p2 holds
p2 . xd = (p1 * ((p1 ") * p2)) . xd
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:2; verum