let F be XFinSequence; :: thesis: for X, Y being set st X misses Y holds
ex P being Permutation of (dom (SubXFinS (F,(X \/ Y)))) st (SubXFinS (F,(X \/ Y))) * P = (SubXFinS (F,X)) ^ (SubXFinS (F,Y))
let X, Y be set ; :: thesis: ( X misses Y implies ex P being Permutation of (dom (SubXFinS (F,(X \/ Y)))) st (SubXFinS (F,(X \/ Y))) * P = (SubXFinS (F,X)) ^ (SubXFinS (F,Y)) )
assume A1: X misses Y ; :: thesis: ex P being Permutation of (dom (SubXFinS (F,(X \/ Y)))) st (SubXFinS (F,(X \/ Y))) * P = (SubXFinS (F,X)) ^ (SubXFinS (F,Y))
set A = (Sgm0 (X /\ (Segm (len F)))) ^ (Sgm0 (Y /\ (Segm (len F))));
set B = Sgm0 ((X \/ Y) /\ (Segm (len F)));
A2: ( rng (Sgm0 (X /\ (Segm (len F)))) = X /\ (len F) & rng (Sgm0 (Y /\ (Segm (len F)))) = Y /\ (len F) ) by AFINSQ_2:def 4;
then reconsider A = (Sgm0 (X /\ (Segm (len F)))) ^ (Sgm0 (Y /\ (Segm (len F)))) as one-to-one Function by A1, XBOOLE_1:76, CARD_FIN:52;
reconsider B = Sgm0 ((X \/ Y) /\ (Segm (len F))) as one-to-one Function ;
A3: (X \/ Y) /\ (len F) = (X /\ (len F)) \/ (Y /\ (len F)) by XBOOLE_1:23;
then A4: rng A = rng B by Th5;
then A5: rng A = dom (B ") by FUNCT_1:33;
set P = (B ") * A;
A6: dom ((B ") * A) = dom A by A5, RELAT_1:27
.= dom B by A3, A1, XBOOLE_1:76, Th4
.= dom (SubXFinS (F,(X \/ Y))) by Th6 ;
A7: rng ((B ") * A) = rng (B ") by A5, RELAT_1:28
.= dom B by FUNCT_1:33
.= dom (SubXFinS (F,(X \/ Y))) by Th6 ;
reconsider P = (B ") * A as Function of (dom (SubXFinS (F,(X \/ Y)))),(dom (SubXFinS (F,(X \/ Y)))) by A6, A7, FUNCT_2:2;
card (dom (SubXFinS (F,(X \/ Y)))) = card (dom (SubXFinS (F,(X \/ Y)))) ;
then P is onto by FINSEQ_4:63;
then reconsider P = P as Permutation of (dom (SubXFinS (F,(X \/ Y)))) ;
take P ; :: thesis: (SubXFinS (F,(X \/ Y))) * P = (SubXFinS (F,X)) ^ (SubXFinS (F,Y))
A8: ( rng (Sgm0 (X /\ (Segm (len F)))) c= len F & rng (Sgm0 (Y /\ (Segm (len F)))) c= len F ) by A2, XBOOLE_1:17;
thus (SubXFinS (F,(X \/ Y))) * P = F * ((Sgm0 ((X \/ Y) /\ (Segm (len F)))) * ((B ") * A)) by RELAT_1:36
.= F * (((Sgm0 ((X \/ Y) /\ (Segm (len F)))) * (B ")) * A) by RELAT_1:36
.= F * ((id (rng A)) * A) by FUNCT_1:39, A4
.= F * A by RELAT_1:54
.= (SubXFinS (F,X)) ^ (SubXFinS (F,Y)) by A8, AFINSQ_2:70 ; :: thesis: verum