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

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