let F be FinSequence; :: thesis: for A being Subset of (rng F) ex p being Permutation of (dom F) st (F - (A `)) ^ (F - A) = F * p
let A be Subset of (rng F); :: thesis: ex p being Permutation of (dom F) st (F - (A `)) ^ (F - A) = F * p
set F1 = F - (A `);
set F2 = F - A;
A ` = (rng F) \ A by SUBSET_1:def 5;
then F " (A `) misses F " A by FUNCT_1:141, XBOOLE_1:79;
then (card (F " (A `))) + (card (F " A)) = card ((F " (A `)) \/ (F " A)) by CARD_2:53
.= card (F " ((A `) \/ A)) by RELAT_1:175
.= card (F " ([#] (rng F))) by SUBSET_1:25
.= card (F " (rng F)) by SUBSET_1:def 4
.= card (dom F) by RELAT_1:169
.= len F by CARD_1:104 ;
then A5: len F = ((len F) - (card (F " (A `)))) + ((len F) - (card (F " A)))
.= (len (F - (A `))) + ((len F) - (card (F " A))) by Th66
.= (len (F - (A `))) + (len (F - A)) by Th66 ;
(rng F) \ (rng (F - (A `))) = (rng F) \ ((rng F) \ (A `)) by Th72
.= (rng F) \ ((rng F) \ ((rng F) \ A)) by SUBSET_1:def 5
.= (rng F) \ ((rng F) /\ A) by XBOOLE_1:48
.= (rng F) \ A by XBOOLE_1:47
.= rng (F - A) by Th72 ;
then reconsider p = (Sgm (F " (rng (F - (A `))))) ^ (Sgm (F " (rng (F - A)))) as Permutation of (dom F) by Th123;
reconsider F3 = F * p as FinSequence by FINSEQ_2:44;
take p ; :: thesis: (F - (A `)) ^ (F - A) = F * p

A8: now

A9: F " (A `) = F " ((rng F) \ A) by SUBSET_1:def 5
.= (F " (rng F)) \ (F " A) by FUNCT_1:138
.= (dom F) \ (F " A) by RELAT_1:169 ;
A10: F " (rng F) = dom F by RELAT_1:169;
then A11: card ((F " (rng F)) \ (F " (A `))) = (card (F " (rng F))) - (card (F " (A `))) by A9, CARD_2:63, XBOOLE_1:36
.= (card (Seg (len F))) - (card (F " (A `))) by A10, FINSEQ_1:def 3
.= (len F) - (card (F " (A `))) by FINSEQ_1:78
.= len (F - (A `)) by Th66 ;
F " (rng (F - (A `))) c= dom F by RELAT_1:167;
then A12: F " (rng (F - (A `))) c= Seg (len F) by FINSEQ_1:def 3;
let k be Element of NAT ; :: thesis: ( k in dom (F - (A `)) implies (F * p) . k = (F - (A `)) . k )
assume A13: k in dom (F - (A `)) ; :: thesis: (F * p) . k = (F - (A `)) . k
A14: dom (Sgm (F " (rng (F - (A `))))) = Seg (len (Sgm (F " (rng (F - (A `)))))) by FINSEQ_1:def 3
.= Seg (card (F " (rng (F - (A `))))) by A12, Th44
.= Seg (card (F " ((rng F) \ (A `)))) by Th72
.= Seg (len (F - (A `))) by A11, FUNCT_1:138
.= dom (F - (A `)) by FINSEQ_1:def 3 ;
dom (Sgm (F " (rng (F - (A `))))) c= dom p by FINSEQ_1:39;
hence (F * p) . k = F . (p . k) by A13, A14, FUNCT_1:23
.= F . ((Sgm (F " (rng (F - (A `))))) . k) by A13, A14, FINSEQ_1:def 7
.= (F * (Sgm (F " (rng (F - (A `)))))) . k by A13, A14, FUNCT_1:23
.= (F * (Sgm (F " ((rng F) \ (A `))))) . k by Th72
.= (F * (Sgm (F " ((rng F) \ ((rng F) \ A))))) . k by SUBSET_1:def 5
.= (F * (Sgm (F " ((rng F) /\ A)))) . k by XBOOLE_1:48
.= (F * (Sgm ((F " (rng F)) /\ (F " A)))) . k by FUNCT_1:137
.= (F * (Sgm ((dom F) /\ (F " A)))) . k by RELAT_1:169
.= (F - (A `)) . k by A9, XBOOLE_1:48 ;
:: thesis: verum

end;

A15: now

A16: F " (rng F) = dom F by RELAT_1:169;
F " A c= dom F by RELAT_1:167;
then F " A c= F " (rng F) by RELAT_1:169;
then A17: card ((F " (rng F)) \ (F " A)) = (card (F " (rng F))) - (card (F " A)) by CARD_2:63
.= (card (Seg (len F))) - (card (F " A)) by A16, FINSEQ_1:def 3
.= (len F) - (card (F " A)) by FINSEQ_1:78
.= len (F - A) by Th66 ;
dom F = Seg (len F) by FINSEQ_1:def 3;
then len (Sgm (F " (rng (F - A)))) = card (F " (rng (F - A))) by Th44, RELAT_1:167
.= card (F " ((rng F) \ A)) by Th72
.= len (F - A) by A17, FUNCT_1:138 ;
then A18: dom (Sgm (F " (rng (F - A)))) = dom (F - A) by Th31;
A19: F " (rng F) = dom F by RELAT_1:169;
F " (A `) = F " ((rng F) \ A) by SUBSET_1:def 5
.= (F " (rng F)) \ (F " A) by FUNCT_1:138
.= (dom F) \ (F " A) by RELAT_1:169 ;
then A20: card ((F " (rng F)) \ (F " (A `))) = (card (F " (rng F))) - (card (F " (A `))) by A19, CARD_2:63, XBOOLE_1:36
.= (card (Seg (len F))) - (card (F " (A `))) by A19, FINSEQ_1:def 3
.= (len F) - (card (F " (A `))) by FINSEQ_1:78
.= len (F - (A `)) by Th66 ;
let k be Element of NAT ; :: thesis: ( k in dom (F - A) implies (F * p) . ((len (F - (A `))) + k) = (F - A) . k )
assume A21: k in dom (F - A) ; :: thesis: (F * p) . ((len (F - (A `))) + k) = (F - A) . k
F " (rng (F - (A `))) c= dom F by RELAT_1:167;
then F " (rng (F - (A `))) c= Seg (len F) by FINSEQ_1:def 3;
then A22: len (Sgm (F " (rng (F - (A `))))) = card (F " (rng (F - (A `)))) by Th44
.= card (F " ((rng F) \ (A `))) by Th72
.= len (F - (A `)) by A20, FUNCT_1:138 ;
then (len (F - (A `))) + k in dom p by A21, A18, FINSEQ_1:41;
hence (F * p) . ((len (F - (A `))) + k) = F . (p . ((len (F - (A `))) + k)) by FUNCT_1:23
.= F . ((Sgm (F " (rng (F - A)))) . k) by A21, A18, A22, FINSEQ_1:def 7
.= (F * (Sgm (F " (rng (F - A))))) . k by A21, A18, FUNCT_1:23
.= (F * (Sgm (F " ((rng F) \ A)))) . k by Th72
.= (F * (Sgm ((F " (rng F)) \ (F " A)))) . k by FUNCT_1:138
.= (F - A) . k by RELAT_1:169 ;
:: thesis: verum

end;

len F3 = (len (F - (A `))) + (len (F - A)) by A5, FINSEQ_2:48;
hence (F - (A `)) ^ (F - A) = F * p by A8, A15, Th43; :: thesis: verum