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 4;
then F " (A `) misses F " A by FUNCT_1:71, XBOOLE_1:79;
then (card (F " (A `))) + (card (F " A)) = card ((F " (A `)) \/ (F " A)) by CARD_2:40
.= card (F " ((A `) \/ A)) by RELAT_1:140
.= card (F " ([#] (rng F))) by SUBSET_1:10
.= card (F " (rng F)) by SUBSET_1:def 3
.= card (dom F) by RELAT_1:134
.= len F by CARD_1:62 ;
then A1: len F = ((len F) - (card (F " (A `)))) + ((len F) - (card (F " A)))
.= (len (F - (A `))) + ((len F) - (card (F " A))) by Th57
.= (len (F - (A `))) + (len (F - A)) by Th57 ;
(rng F) \ (rng (F - (A `))) = (rng F) \ ((rng F) \ (A `)) by Th63
.= (rng F) \ ((rng F) \ ((rng F) \ A)) by SUBSET_1:def 4
.= (rng F) \ ((rng F) /\ A) by XBOOLE_1:48
.= (rng F) \ A by XBOOLE_1:47
.= rng (F - A) by Th63 ;
then reconsider p = (Sgm (F " (rng (F - (A `))))) ^ (Sgm (F " (rng (F - A)))) as Permutation of (dom F) by Th112;
reconsider F3 = F * p as FinSequence by FINSEQ_2:40;
take p ; :: thesis: (F - (A `)) ^ (F - A) = F * p
A2: now :: thesis: for k being Nat st k in dom (F - (A `)) holds
(F * p) . k = (F - (A `)) . k
A3: F " (A `) = F " ((rng F) \ A) by SUBSET_1:def 4
.= (F " (rng F)) \ (F " A) by FUNCT_1:69
.= (dom F) \ (F " A) by RELAT_1:134 ;
A4: F " (rng F) = dom F by RELAT_1:134;
then A5: card ((F " (rng F)) \ (F " (A `))) = (card (F " (rng F))) - (card (F " (A `))) by A3, CARD_2:44, XBOOLE_1:36
.= (card (Seg (len F))) - (card (F " (A `))) by A4, FINSEQ_1:def 3
.= (len F) - (card (F " (A `))) by FINSEQ_1:57
.= len (F - (A `)) by Th57 ;
F " (rng (F - (A `))) c= dom F by RELAT_1:132;
then A6: F " (rng (F - (A `))) c= Seg (len F) by FINSEQ_1:def 3;
let k be Nat; :: thesis: ( k in dom (F - (A `)) implies (F * p) . k = (F - (A `)) . k )
assume A7: k in dom (F - (A `)) ; :: thesis: (F * p) . k = (F - (A `)) . k
A8: 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 A6, Th37
.= Seg (card (F " ((rng F) \ (A `)))) by Th63
.= Seg (len (F - (A `))) by A5, FUNCT_1:69
.= dom (F - (A `)) by FINSEQ_1:def 3 ;
dom (Sgm (F " (rng (F - (A `))))) c= dom p by FINSEQ_1:26;
hence (F * p) . k = F . (p . k) by A7, A8, FUNCT_1:13
.= F . ((Sgm (F " (rng (F - (A `))))) . k) by A7, A8, FINSEQ_1:def 7
.= (F * (Sgm (F " (rng (F - (A `)))))) . k by A7, A8, FUNCT_1:13
.= (F * (Sgm (F " ((rng F) \ (A `))))) . k by Th63
.= (F * (Sgm (F " ((rng F) \ ((rng F) \ A))))) . k by SUBSET_1:def 4
.= (F * (Sgm (F " ((rng F) /\ A)))) . k by XBOOLE_1:48
.= (F * (Sgm ((F " (rng F)) /\ (F " A)))) . k by FUNCT_1:68
.= (F * (Sgm ((dom F) /\ (F " A)))) . k by RELAT_1:134
.= (F - (A `)) . k by A3, XBOOLE_1:48 ;
:: thesis: verum
end;
A9: now :: thesis: for k being Nat st k in dom (F - A) holds
(F * p) . ((len (F - (A `))) + k) = (F - A) . k
A10: F " (rng F) = dom F by RELAT_1:134;
F " A c= dom F by RELAT_1:132;
then F " A c= F " (rng F) by RELAT_1:134;
then A11: card ((F " (rng F)) \ (F " A)) = (card (F " (rng F))) - (card (F " A)) by CARD_2:44
.= (card (Seg (len F))) - (card (F " A)) by A10, FINSEQ_1:def 3
.= (len F) - (card (F " A)) by FINSEQ_1:57
.= len (F - A) by Th57 ;
dom F = Seg (len F) by FINSEQ_1:def 3;
then len (Sgm (F " (rng (F - A)))) = card (F " (rng (F - A))) by Th37, RELAT_1:132
.= card (F " ((rng F) \ A)) by Th63
.= len (F - A) by A11, FUNCT_1:69 ;
then A12: dom (Sgm (F " (rng (F - A)))) = dom (F - A) by Th27;
A13: F " (rng F) = dom F by RELAT_1:134;
F " (A `) = F " ((rng F) \ A) by SUBSET_1:def 4
.= (F " (rng F)) \ (F " A) by FUNCT_1:69
.= (dom F) \ (F " A) by RELAT_1:134 ;
then A14: card ((F " (rng F)) \ (F " (A `))) = (card (F " (rng F))) - (card (F " (A `))) by A13, CARD_2:44, XBOOLE_1:36
.= (card (Seg (len F))) - (card (F " (A `))) by A13, FINSEQ_1:def 3
.= (len F) - (card (F " (A `))) by FINSEQ_1:57
.= len (F - (A `)) by Th57 ;
let k be Nat; :: thesis: ( k in dom (F - A) implies (F * p) . ((len (F - (A `))) + k) = (F - A) . k )
assume A15: 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:132;
then F " (rng (F - (A `))) c= Seg (len F) by FINSEQ_1:def 3;
then A16: len (Sgm (F " (rng (F - (A `))))) = card (F " (rng (F - (A `)))) by Th37
.= card (F " ((rng F) \ (A `))) by Th63
.= len (F - (A `)) by A14, FUNCT_1:69 ;
then (len (F - (A `))) + k in dom p by A15, A12, FINSEQ_1:28;
hence (F * p) . ((len (F - (A `))) + k) = F . (p . ((len (F - (A `))) + k)) by FUNCT_1:13
.= F . ((Sgm (F " (rng (F - A)))) . k) by A15, A12, A16, FINSEQ_1:def 7
.= (F * (Sgm (F " (rng (F - A))))) . k by A15, A12, FUNCT_1:13
.= (F * (Sgm (F " ((rng F) \ A)))) . k by Th63
.= (F * (Sgm ((F " (rng F)) \ (F " A)))) . k by FUNCT_1:69
.= (F - A) . k by RELAT_1:134 ;
:: thesis: verum
end;
len F3 = (len (F - (A `))) + (len (F - A)) by A1, FINSEQ_2:44;
hence (F - (A `)) ^ (F - A) = F * p by A2, A9, Th36; :: thesis: verum