let F be FinSequence; :: thesis: for A being Subset of (rng F) st F is one-to-one holds
ex p being Permutation of (dom F) st (F - (A ` )) ^ (F - A) = F * p
let A be Subset of (rng F); :: thesis: ( F is one-to-one implies ex p being Permutation of (dom F) st (F - (A ` )) ^ (F - A) = F * p )
assume A1: F is one-to-one ; :: thesis: ex p being Permutation of (dom F) st (F - (A ` )) ^ (F - A) = F * p
set F1 = F - (A ` );
set F2 = F - A;
(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;
take p ; :: thesis: (F - (A ` )) ^ (F - A) = F * p
A2: ( F - (A ` ) is one-to-one & F - A is one-to-one ) by A1, Th94;
A3: A misses (rng F) \ A by XBOOLE_1:79;
A4: rng (F - (A ` )) = (rng F) \ (A ` ) by Th72;
then (rng (F - (A ` ))) /\ (rng (F - A)) = ((rng F) \ (A ` )) /\ ((rng F) \ A) by Th72
.= ((rng F) \ ((rng F) \ A)) /\ ((rng F) \ A) by SUBSET_1:def 5
.= ((rng F) /\ A) /\ ((rng F) \ A) by XBOOLE_1:48
.= A /\ ((rng F) \ A) by XBOOLE_1:28
.= {} by A3, XBOOLE_0:def 7 ;
then A5: rng (F - (A ` )) misses rng (F - A) by XBOOLE_0:def 7;
A6: rng ((F - (A ` )) ^ (F - A)) = (rng (F - (A ` ))) \/ (rng (F - A)) by FINSEQ_1:44
.= ((rng F) \ (A ` )) \/ ((rng F) \ A) by A4, Th72
.= ((rng F) \ ((rng F) \ A)) \/ ((rng F) \ A) by SUBSET_1:def 5
.= ((rng F) /\ A) \/ ((rng F) \ A) by XBOOLE_1:48
.= A \/ ((rng F) \ A) by XBOOLE_1:28
.= A \/ (rng F) by XBOOLE_1:39
.= rng F by XBOOLE_1:12 ;
A7: (F - (A ` )) ^ (F - A) is one-to-one by A2, A5, Th98;
reconsider F3 = F * p as FinSequence by FINSEQ_2:44;
A8: len F3 = len F by FINSEQ_2:48
.= len ((F - (A ` )) ^ (F - A)) by A1, A6, A7, FINSEQ_1:65
.= (len (F - (A ` ))) + (len (F - A)) by FINSEQ_1:35 ;

A9: now

let k be Element of NAT ; :: thesis: ( k in dom (F - (A ` )) implies (F * p) . k = (F - (A ` )) . k )
assume A10: k in dom (F - (A ` )) ; :: thesis: (F * p) . k = (F - (A ` )) . k
A11: 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 ;
A12: F " (rng F) = dom F by RELAT_1:169;
then A13: card ((F " (rng F)) \ (F " (A ` ))) = (card (F " (rng F))) - (card (F " (A ` ))) by A11, CARD_2:63, XBOOLE_1:36
.= (card (Seg (len F))) - (card (F " (A ` ))) by A12, 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 A14: F " (rng (F - (A ` ))) c= Seg (len F) by FINSEQ_1:def 3;
A15: 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 A14, Th44
.= Seg (card (F " ((rng F) \ (A ` )))) by Th72
.= Seg (len (F - (A ` ))) by A13, 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 A10, A15, FUNCT_1:23
.= F . ((Sgm (F " (rng (F - (A ` ))))) . k) by A10, A15, FINSEQ_1:def 7
.= (F * (Sgm (F " (rng (F - (A ` )))))) . k by A10, A15, 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 A11, XBOOLE_1:48 ;
:: thesis: verum

end;

now

let k be Element of NAT ; :: thesis: ( k in dom (F - A) implies (F * p) . ((len (F - (A ` ))) + k) = (F - A) . k )
assume A16: k in dom (F - A) ; :: thesis: (F * p) . ((len (F - (A ` ))) + k) = (F - A) . k
A17: 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 A18: 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 A17, 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 A18, FUNCT_1:138 ;
then A19: dom (Sgm (F " (rng (F - A)))) = dom (F - A) by Th31;
A20: 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 ;
A21: F " (rng F) = dom F by RELAT_1:169;
then A22: card ((F " (rng F)) \ (F " (A ` ))) = (card (F " (rng F))) - (card (F " (A ` ))) by A20, CARD_2:63, XBOOLE_1:36
.= (card (Seg (len F))) - (card (F " (A ` ))) by A21, 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 F " (rng (F - (A ` ))) c= Seg (len F) by FINSEQ_1:def 3;
then A23: len (Sgm (F " (rng (F - (A ` ))))) = card (F " (rng (F - (A ` )))) by Th44
.= card (F " ((rng F) \ (A ` ))) by Th72
.= len (F - (A ` )) by A22, FUNCT_1:138 ;
then (len (F - (A ` ))) + k in dom p by A16, A19, 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 A16, A19, A23, FINSEQ_1:def 7
.= (F * (Sgm (F " (rng (F - A))))) . k by A16, A19, 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;

hence (F - (A ` )) ^ (F - A) = F * p by A8, A9, Th43; :: thesis: verum