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) = {} ;
A3: (F " A) /\ (F " ((rng F) \ A)) = F " (A /\ ((rng F) \ A)) by FUNCT_1:68
.= {} by A2 ;
then A4: F " A misses F " ((rng F) \ A) ;
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 a6: F " ((rng F) \ A) is included_in_Seg by FINSEQ_1:def 13;
then A7: Sgm (F " ((rng F) \ A)) is one-to-one ;
F " A c= dom F by RELAT_1:132;
then F " A c= Seg (len F) by FINSEQ_1:def 3;
then a9: F " A is included_in_Seg by FINSEQ_1:def 13;
then (rng (Sgm (F " A))) /\ (rng (Sgm (F " ((rng F) \ A)))) = (F " A) /\ (rng (Sgm (F " ((rng F) \ A)))) by FINSEQ_1:def 14
.= {} by a6, A3, FINSEQ_1:def 14 ;
then A10: rng (Sgm (F " A)) misses rng (Sgm (F " ((rng F) \ A))) ;
A11: rng ((Sgm (F " A)) ^ (Sgm (F " ((rng F) \ A)))) = (rng (Sgm (F " A))) \/ (rng (Sgm (F " ((rng F) \ A)))) by FINSEQ_1:31
.= (F " A) \/ (rng (Sgm (F " ((rng F) \ A)))) by a9, FINSEQ_1:def 14
.= (F " A) \/ (F " ((rng F) \ A)) by a6, FINSEQ_1:def 14
.= F " (A \/ ((rng F) \ A)) by RELAT_1:140
.= F " ((rng F) \/ A) by XBOOLE_1:39
.= (F " (rng F)) \/ (F " A) by RELAT_1:140
.= (dom F) \/ (F " A) by RELAT_1:134
.= dom F by RELAT_1:132, XBOOLE_1:12 ;
ww: (F " A) \/ (F " ((rng F) \ A)) is included_in_Seg by a6, a9;
Sgm (F " A) is one-to-one by a9;
then A12: (Sgm (F " A)) ^ (Sgm (F " ((rng F) \ A))) is one-to-one by A7, A10, Th89;
len ((Sgm (F " A)) ^ (Sgm (F " ((rng F) \ A)))) = (len (Sgm (F " A))) + (len (Sgm (F " ((rng F) \ A)))) by FINSEQ_1:22
.= (card (F " A)) + (len (Sgm (F " ((rng F) \ A)))) by a9, Th37
.= (card (F " A)) + (card (F " ((rng F) \ A))) by a6, Th37
.= card ((F " A) \/ (F " ((rng F) \ A))) by A4, CARD_2:40
.= len (Sgm ((F " A) \/ (F " ((rng F) \ A)))) by ww, Th37
.= len (Sgm (F " (A \/ ((rng F) \ A)))) by RELAT_1:140
.= len (Sgm (F " ((rng F) \/ A))) by XBOOLE_1:39
.= len (Sgm ((F " (rng F)) \/ (F " A))) by RELAT_1:140
.= len (Sgm ((dom F) \/ (F " A))) by RELAT_1:134
.= len (Sgm (dom F)) by RELAT_1:132, XBOOLE_1:12
.= card (Seg (len F)) by A1, Th37
.= len F by FINSEQ_1:57 ;
then dom ((Sgm (F " A)) ^ (Sgm (F " ((rng F) \ A)))) = dom F by Th27;
then (Sgm (F " A)) ^ (Sgm (F " ((rng F) \ A))) is Function of (dom F),(dom F) by A11, FUNCT_2:1;
hence (Sgm (F " A)) ^ (Sgm (F " ((rng F) \ A))) is Permutation of (dom F) by A12, A11, FUNCT_2:57; :: thesis: verum