let A be set ; :: thesis: for F being FinSequence holds (Sgm (F " A)) ^ (Sgm (F " ((rng F) \ A))) is Permutation of (dom F)
let F be FinSequence; :: thesis: (Sgm (F " A)) ^ (Sgm (F " ((rng F) \ A))) is Permutation of (dom F)
A1: dom F = Seg (len F) by FINSEQ_1:def 3;
set p = (Sgm (F " A)) ^ (Sgm (F " ((rng F) \ A)));
A misses (rng F) \ A by XBOOLE_1:79;
then A2: A /\ ((rng F) \ A) = {} by XBOOLE_0:def 7;
A3: (F " A) /\ (F " ((rng F) \ A)) = F " (A /\ ((rng F) \ A)) by FUNCT_1:137
.= {} by A2, RELAT_1:171 ;
then A4: F " A misses F " ((rng F) \ A) by XBOOLE_0:def 7;
A5: F " ((rng F) \ A) c= dom F by RELAT_1:167;
then A6: F " ((rng F) \ A) c= Seg (len F) by FINSEQ_1:def 3;
then A7: Sgm (F " ((rng F) \ A)) is one-to-one by Lm1;
A8: F " A c= dom F by RELAT_1:167;
then A9: F " A c= Seg (len F) by FINSEQ_1:def 3;
then (rng (Sgm (F " A))) /\ (rng (Sgm (F " ((rng F) \ A)))) = (F " A) /\ (rng (Sgm (F " ((rng F) \ A)))) by FINSEQ_1:def 13
.= {} by A6, A3, FINSEQ_1:def 13 ;
then A10: rng (Sgm (F " A)) misses rng (Sgm (F " ((rng F) \ A))) by XBOOLE_0:def 7;
A11: rng ((Sgm (F " A)) ^ (Sgm (F " ((rng F) \ A)))) = (rng (Sgm (F " A))) \/ (rng (Sgm (F " ((rng F) \ A)))) by FINSEQ_1:44
.= (F " A) \/ (rng (Sgm (F " ((rng F) \ A)))) by A9, FINSEQ_1:def 13
.= (F " A) \/ (F " ((rng F) \ A)) by A6, FINSEQ_1:def 13
.= F " (A \/ ((rng F) \ A)) by RELAT_1:175
.= F " ((rng F) \/ A) by XBOOLE_1:39
.= (F " (rng F)) \/ (F " A) by RELAT_1:175
.= (dom F) \/ (F " A) by RELAT_1:169
.= dom F by RELAT_1:167, XBOOLE_1:12 ;
Sgm (F " A) is one-to-one by A9, Lm1;
then A12: (Sgm (F " A)) ^ (Sgm (F " ((rng F) \ A))) is one-to-one by A7, A10, Th98;
len ((Sgm (F " A)) ^ (Sgm (F " ((rng F) \ A)))) = (len (Sgm (F " A))) + (len (Sgm (F " ((rng F) \ A)))) by FINSEQ_1:35
.= (card (F " A)) + (len (Sgm (F " ((rng F) \ A)))) by A9, Th44
.= (card (F " A)) + (card (F " ((rng F) \ A))) by A6, Th44
.= card ((F " A) \/ (F " ((rng F) \ A))) by A4, CARD_2:53
.= len (Sgm ((F " A) \/ (F " ((rng F) \ A)))) by A1, A8, A5, Th44, XBOOLE_1:8
.= len (Sgm (F " (A \/ ((rng F) \ A)))) by RELAT_1:175
.= len (Sgm (F " ((rng F) \/ A))) by XBOOLE_1:39
.= len (Sgm ((F " (rng F)) \/ (F " A))) by RELAT_1:175
.= len (Sgm ((dom F) \/ (F " A))) by RELAT_1:169
.= len (Sgm (dom F)) by RELAT_1:167, XBOOLE_1:12
.= card (Seg (len F)) by A1, Th44
.= len F by FINSEQ_1:78 ;
then dom ((Sgm (F " A)) ^ (Sgm (F " ((rng F) \ A)))) = dom F by Th31;
then (Sgm (F " A)) ^ (Sgm (F " ((rng F) \ A))) is Function of (dom F),(dom F) by A11, FUNCT_2:3;
hence (Sgm (F " A)) ^ (Sgm (F " ((rng F) \ A))) is Permutation of (dom F) by A12, A11, FUNCT_2:83; :: thesis: verum