let X be set ; for f, f1 being FinSubsequence
for P being Permutation of (dom f) st f1 = f * P holds
ex Q being Permutation of (dom (Seq (f1 | (P " X)))) st Seq (f | X) = (Seq (f1 | (P " X))) * Q
let f, f1 be FinSubsequence; for P being Permutation of (dom f) st f1 = f * P holds
ex Q being Permutation of (dom (Seq (f1 | (P " X)))) st Seq (f | X) = (Seq (f1 | (P " X))) * Q
consider n being Nat such that
A1:
dom f c= Seg n
by FINSEQ_1:def 12;
let P be Permutation of (dom f); ( f1 = f * P implies ex Q being Permutation of (dom (Seq (f1 | (P " X)))) st Seq (f | X) = (Seq (f1 | (P " X))) * Q )
assume A2:
f1 = f * P
; ex Q being Permutation of (dom (Seq (f1 | (P " X)))) st Seq (f | X) = (Seq (f1 | (P " X))) * Q
set SPX = Sgm (P " X);
A3:
P " X c= dom P
by RELAT_1:132;
then A4:
dom (P | (P " X)) = P " X
by RELAT_1:62;
A5:
dom P = dom f
by FUNCT_2:52;
then A6:
Sgm (P " X) is one-to-one
by A1, A3, FINSEQ_3:92, XBOOLE_1:1;
set dfX = (dom f) /\ X;
set SdX = Sgm ((dom f) /\ X);
A7:
(dom f) /\ X c= dom f
by XBOOLE_1:17;
then
(dom f) /\ X c= Seg n
by A1;
then A8:
rng (Sgm ((dom f) /\ X)) = (dom f) /\ X
by FINSEQ_1:def 13;
A9:
rng P = dom f
by FUNCT_2:def 3;
then A10:
P " X = P " ((dom f) /\ X)
by RELAT_1:133;
then A11:
P " X = (P ") .: ((dom f) /\ X)
by FUNCT_1:85;
set PS = (P | (P " X)) * (Sgm (P " X));
A12:
P | (P " X) is one-to-one
by FUNCT_1:52;
P " X c= Seg n
by A1, A5, A3;
then A13:
rng (Sgm (P " X)) = P " X
by FINSEQ_1:def 13;
rng (P | (P " X)) =
P .: (P " ((dom f) /\ X))
by A10, RELAT_1:115
.=
(dom f) /\ X
by A9, FUNCT_1:77, XBOOLE_1:17
;
then A14:
rng ((P | (P " X)) * (Sgm (P " X))) = (dom f) /\ X
by A4, A13, RELAT_1:28;
A15:
dom (((P | (P " X)) * (Sgm (P " X))) ") = (dom f) /\ X
by A6, A12, A14, FUNCT_1:33;
dom (P ") = rng P
by FUNCT_1:33;
then
(dom f) /\ X,(P ") .: ((dom f) /\ X) are_equipotent
by A9, CARD_1:33, XBOOLE_1:17;
then
card ((dom f) /\ X) = card (P " X)
by A11, CARD_1:5;
then A16:
dom (Sgm (P " X)) = Seg (card ((dom f) /\ X))
by A1, A5, A3, FINSEQ_3:40, XBOOLE_1:1;
then
dom ((P | (P " X)) * (Sgm (P " X))) = Seg (card ((dom f) /\ X))
by A4, A13, RELAT_1:27;
then
rng (((P | (P " X)) * (Sgm (P " X))) ") = Seg (card ((dom f) /\ X))
by A6, A12, FUNCT_1:33;
then A17:
rng ((((P | (P " X)) * (Sgm (P " X))) ") * (Sgm ((dom f) /\ X))) = Seg (card ((dom f) /\ X))
by A15, A8, RELAT_1:28;
dom f1 = dom P
by A2, A9, RELAT_1:27;
then A18:
dom (f1 | (P " X)) = P " X
by RELAT_1:62, RELAT_1:132;
then A19:
dom (Seq (f1 | (P " X))) = Seg (card ((dom f) /\ X))
by A16, A13, RELAT_1:27;
dom (Sgm ((dom f) /\ X)) = Seg (card ((dom f) /\ X))
by A1, A7, FINSEQ_3:40, XBOOLE_1:1;
then
dom ((((P | (P " X)) * (Sgm (P " X))) ") * (Sgm ((dom f) /\ X))) = Seg (card ((dom f) /\ X))
by A15, A8, RELAT_1:27;
then reconsider PSS = (((P | (P " X)) * (Sgm (P " X))) ") * (Sgm ((dom f) /\ X)) as Function of (dom (Seq (f1 | (P " X)))),(dom (Seq (f1 | (P " X)))) by A19, A17, FUNCT_2:1;
A20:
PSS is onto
by A19, A17, FUNCT_2:def 3;
Sgm ((dom f) /\ X) is one-to-one
by A1, A7, FINSEQ_3:92, XBOOLE_1:1;
then reconsider PSS = PSS as Permutation of (dom (Seq (f1 | (P " X)))) by A6, A12, A20;
A21: ((P | (P " X)) * (Sgm (P " X))) * PSS =
(((P | (P " X)) * (Sgm (P " X))) * (((P | (P " X)) * (Sgm (P " X))) ")) * (Sgm ((dom f) /\ X))
by RELAT_1:36
.=
(id ((dom f) /\ X)) * (Sgm ((dom f) /\ X))
by A6, A12, A14, FUNCT_1:39
;
set fX = f | X;
A22:
f | X = f | ((dom f) /\ X)
by RELAT_1:157;
take
PSS
; Seq (f | X) = (Seq (f1 | (P " X))) * PSS
f1 | (P " X) = f * (P | (P " X))
by A2, RELAT_1:83;
hence (Seq (f1 | (P " X))) * PSS =
(f * ((P | (P " X)) * (Sgm (P " X)))) * PSS
by A18, RELAT_1:36
.=
f * ((id ((dom f) /\ X)) * (Sgm ((dom f) /\ X)))
by A21, RELAT_1:36
.=
(f * (id ((dom f) /\ X))) * (Sgm ((dom f) /\ X))
by RELAT_1:36
.=
(f | X) * (Sgm ((dom f) /\ X))
by A22, RELAT_1:65
.=
Seq (f | X)
by RELAT_1:61
;
verum