let X be set ; :: thesis: 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; :: thesis: 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); :: thesis: ( 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 ; :: thesis: 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 ; :: thesis: 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 ;
:: thesis: verum