let X be set ; :: thesis: for f, f1 being FinSequence
for P being Permutation of (dom f) st f1 = f * P holds
ex Q being Permutation of (dom (f - X)) st f1 - X = (f - X) * Q
let f, f1 be FinSequence; :: thesis: for P being Permutation of (dom f) st f1 = f * P holds
ex Q being Permutation of (dom (f - X)) st f1 - X = (f - X) * Q
let P be Permutation of (dom f); :: thesis: ( f1 = f * P implies ex Q being Permutation of (dom (f - X)) st f1 - X = (f - X) * Q )
assume A1: f1 = f * P ; :: thesis: ex Q being Permutation of (dom (f - X)) st f1 - X = (f - X) * Q
reconsider p = P as one-to-one Function ;
A2: rng P = dom f by FUNCT_2:def 3;
then A3: dom (p ") = dom f by FUNCT_1:33;
A4: P .: (f1 " X) = P .: (P " (f " X)) by A1, RELAT_1:146
.= f " X by A2, FUNCT_1:77, RELAT_1:132 ;
A5: dom P = dom f by FUNCT_2:52;
then A6: dom f1 = dom f by A1, A2, RELAT_1:27;
set DfX = (dom f1) \ (f1 " X);
set DX = (dom f) \ (f " X);
A7: card ((dom f) \ (f " X)) = (card (dom f)) - (card (f " X)) by CARD_2:44, RELAT_1:132;
A8: dom f = Seg (len f) by FINSEQ_1:def 3;
then A9: dom (Sgm ((dom f) \ (f " X))) = Seg (card ((dom f) \ (f " X))) by FINSEQ_3:40, XBOOLE_1:36;
A10: p " (f " X) = (p ") .: (f " X) by FUNCT_1:85;
f1 " X = P " (f " X) by A1, RELAT_1:146;
then A11: f " X,f1 " X are_equipotent by A3, A10, CARD_1:33, RELAT_1:132;
A12: (dom f1) \ (f1 " X) c= dom f1 by XBOOLE_1:36;
A13: rng (P * (Sgm ((dom f1) \ (f1 " X)))) = P .: (rng (Sgm ((dom f1) \ (f1 " X)))) by RELAT_1:127
.= P .: ((dom f1) \ (f1 " X)) by A6, A8, A12, FINSEQ_1:def 13
.= (P .: (dom P)) \ (P .: (f1 " X)) by A5, A6, FUNCT_1:64
.= (dom f) \ (f " X) by A4, A2, RELAT_1:113 ;
reconsider SDX = Sgm ((dom f) \ (f " X)) as one-to-one Function by A8, FINSEQ_3:92, XBOOLE_1:36;
A14: dom (SDX ") = rng SDX by FUNCT_1:33;
card (dom f) = len f by CARD_1:62;
then A15: dom (f - X) = dom SDX by A7, A9, FINSEQ_3:62;
card ((dom f1) \ (f1 " X)) = (card (dom f1)) - (card (f1 " X)) by CARD_2:44, RELAT_1:132;
then card ((dom f) \ (f " X)) = card ((dom f1) \ (f1 " X)) by A11, A6, A7, CARD_1:5;
then A16: dom SDX = dom (Sgm ((dom f1) \ (f1 " X))) by A6, A8, A9, FINSEQ_3:40, XBOOLE_1:36;
(dom f) \ (f " X) c= dom f by XBOOLE_1:36;
then A17: rng (Sgm ((dom f) \ (f " X))) = (dom f) \ (f " X) by A8, FINSEQ_1:def 13;
rng (SDX ") = dom SDX by FUNCT_1:33;
then A18: rng ((SDX ") * (P * (Sgm ((dom f1) \ (f1 " X))))) = dom SDX by A17, A14, A13, RELAT_1:28;
rng (Sgm ((dom f1) \ (f1 " X))) = (dom f1) \ (f1 " X) by A6, A8, A12, FINSEQ_1:def 13;
then dom (P * (Sgm ((dom f1) \ (f1 " X)))) = dom (Sgm ((dom f1) \ (f1 " X))) by A5, A6, RELAT_1:27, XBOOLE_1:36;
then dom ((SDX ") * (P * (Sgm ((dom f1) \ (f1 " X))))) = dom (Sgm ((dom f1) \ (f1 " X))) by A17, A14, A13, RELAT_1:27;
then reconsider Q = (SDX ") * (P * (Sgm ((dom f1) \ (f1 " X)))) as Function of (dom (f - X)),(dom (f - X)) by A18, A15, A16, FUNCT_2:1;
A19: Q is onto by A18, A15, FUNCT_2:def 3;
Sgm ((dom f1) \ (f1 " X)) is one-to-one by A6, A8, FINSEQ_3:92, XBOOLE_1:36;
then reconsider Q = Q as Permutation of (dom (f - X)) by A19;
SDX * (SDX ") = id ((dom f) \ (f " X)) by A17, FUNCT_1:39;
then A20: SDX * Q = (id ((dom f) \ (f " X))) * (P * (Sgm ((dom f1) \ (f1 " X)))) by RELAT_1:36
.= P * (Sgm ((dom f1) \ (f1 " X))) by A13, RELAT_1:53 ;
(f - X) * Q = (f * SDX) * Q by FINSEQ_3:def 1
.= f * (P * (Sgm ((dom f1) \ (f1 " X)))) by A20, RELAT_1:36
.= f1 * (Sgm ((dom f1) \ (f1 " X))) by A1, RELAT_1:36
.= f1 - X by FINSEQ_3:def 1 ;
hence ex Q being Permutation of (dom (f - X)) st f1 - X = (f - X) * Q ; :: thesis: verum