let p1, p2 be FinSequence; :: thesis: for q1, q2 being FinSubsequence st q1 c= p1 & q2 c= p2 holds
ex ss being FinSubsequence st
( ss = q1 \/ ((len p1) Shift q2) & dom (Seq ss) = Seg ((len (Seq q1)) + (len (Seq q2))) & Seq ss = (Seq q1) \/ ((len (Seq q1)) Shift (Seq q2)) )
let q1, q2 be FinSubsequence; :: thesis: ( q1 c= p1 & q2 c= p2 implies ex ss being FinSubsequence st
( ss = q1 \/ ((len p1) Shift q2) & dom (Seq ss) = Seg ((len (Seq q1)) + (len (Seq q2))) & Seq ss = (Seq q1) \/ ((len (Seq q1)) Shift (Seq q2)) ) )
assume that
A1: q1 c= p1 and
A2: q2 c= p2 ; :: thesis: ex ss being FinSubsequence st
( ss = q1 \/ ((len p1) Shift q2) & dom (Seq ss) = Seg ((len (Seq q1)) + (len (Seq q2))) & Seq ss = (Seq q1) \/ ((len (Seq q1)) Shift (Seq q2)) )
consider ss being FinSubsequence such that
A3: ss = q1 \/ ((len p1) Shift q2) and
A4: dom (Seq ss) = Seg ((len (Seq q1)) + (len (Seq q2))) by A1, A2, Th80;
A12: Seg ((len (Seq q1)) + (len (Seq q2))) = { k where k is Element of NAT : ( 1 <= k & k <= (len (Seq q1)) + (len (Seq q2)) ) } by FINSEQ_1:def 1;
A13: dom (Seq q1) = Seg (len (Seq q1)) by FINSEQ_1:def 3
.= { k where k is Element of NAT : ( 1 <= k & k <= len (Seq q1) ) } by FINSEQ_1:def 1 ;
A14: dom ((len (Seq q1)) Shift (Seq q2)) = { k where k is Element of NAT : ( (len (Seq q1)) + 1 <= k & k <= (len (Seq q1)) + (len (Seq q2)) ) } by Th54;
A15: Seg ((len (Seq q1)) + (len (Seq q2))) = (dom (Seq q1)) \/ (dom ((len (Seq q1)) Shift (Seq q2)))

proof

thus Seg ((len (Seq q1)) + (len (Seq q2))) c= (dom (Seq q1)) \/ (dom ((len (Seq q1)) Shift (Seq q2))) :: according to XBOOLE_0:def 10 :: thesis: (dom (Seq q1)) \/ (dom ((len (Seq q1)) Shift (Seq q2))) c= Seg ((len (Seq q1)) + (len (Seq q2)))

proof

let x be set ; :: according to TARSKI:def 3 :: thesis: ( not x in Seg ((len (Seq q1)) + (len (Seq q2))) or x in (dom (Seq q1)) \/ (dom ((len (Seq q1)) Shift (Seq q2))) )
assume x in Seg ((len (Seq q1)) + (len (Seq q2))) ; :: thesis: x in (dom (Seq q1)) \/ (dom ((len (Seq q1)) Shift (Seq q2)))
then consider k1 being Element of NAT such that
A16: x = k1 and
A17: 1 <= k1 and
A18: k1 <= (len (Seq q1)) + (len (Seq q2)) by A12;
A19: ( 1 <= k1 & k1 <= len (Seq q1) implies k1 in dom (Seq q1) ) by A13;
( (len (Seq q1)) + 1 <= k1 & k1 <= (len (Seq q1)) + (len (Seq q2)) implies k1 in dom ((len (Seq q1)) Shift (Seq q2)) ) by A14;
hence x in (dom (Seq q1)) \/ (dom ((len (Seq q1)) Shift (Seq q2))) by A16, A17, A18, A19, INT_1:20, XBOOLE_0:def 3; :: thesis: verum

end;

let x be set ; :: according to TARSKI:def 3 :: thesis: ( not x in (dom (Seq q1)) \/ (dom ((len (Seq q1)) Shift (Seq q2))) or x in Seg ((len (Seq q1)) + (len (Seq q2))) )
assume A20: x in (dom (Seq q1)) \/ (dom ((len (Seq q1)) Shift (Seq q2))) ; :: thesis: x in Seg ((len (Seq q1)) + (len (Seq q2)))
A21: 0 <= len (Seq q1) by NAT_1:2;
A22: 0 <= len (Seq q2) by NAT_1:2;

A23: now

assume x in dom (Seq q1) ; :: thesis: x in Seg ((len (Seq q1)) + (len (Seq q2)))
then consider k1 being Element of NAT such that
A24: x = k1 and
A25: 1 <= k1 and
A26: k1 <= len (Seq q1) by A13;
(len (Seq q1)) + 0 <= (len (Seq q1)) + (len (Seq q2)) by A22, XREAL_1:9;
then k1 <= (len (Seq q1)) + (len (Seq q2)) by A26, XXREAL_0:2;
hence x in Seg ((len (Seq q1)) + (len (Seq q2))) by A12, A24, A25; :: thesis: verum

end;

now

assume x in dom ((len (Seq q1)) Shift (Seq q2)) ; :: thesis: x in Seg ((len (Seq q1)) + (len (Seq q2)))
then consider k2 being Element of NAT such that
A27: x = k2 and
A28: (len (Seq q1)) + 1 <= k2 and
A29: k2 <= (len (Seq q1)) + (len (Seq q2)) by A14;
0 + 1 <= (len (Seq q1)) + 1 by A21, XREAL_1:9;
then 1 <= k2 by A28, XXREAL_0:2;
hence x in Seg ((len (Seq q1)) + (len (Seq q2))) by A12, A27, A29; :: thesis: verum

end;

hence x in Seg ((len (Seq q1)) + (len (Seq q2))) by A20, A23, XBOOLE_0:def 3; :: thesis: verum

end;

A30: (dom (Seq q1)) \/ (dom ((len (Seq q1)) Shift (Seq q2))) = dom ((Seq q1) \/ ((len (Seq q1)) Shift (Seq q2))) by RELAT_1:13;
dom (Seq q1) misses dom ((len (Seq q1)) Shift (Seq q2)) by Th63;
then reconsider ss1 = (Seq q1) \/ ((len (Seq q1)) Shift (Seq q2)) as Function by GRFUNC_1:31;
for x being set st x in dom (Seq ss) holds
(Seq ss) . x = ss1 . x

proof

let x be set ; :: thesis: ( x in dom (Seq ss) implies (Seq ss) . x = ss1 . x )
assume A31: x in dom (Seq ss) ; :: thesis: (Seq ss) . x = ss1 . x
then A32: x in dom (ss * (Sgm (dom ss))) by FINSEQ_1:def 14;
A33: (Seq ss) . x = (ss * (Sgm (dom ss))) . x by FINSEQ_1:def 14
.= ss . ((Sgm (dom ss)) . x) by A32, FUNCT_1:22
.= ss . ((Sgm ((dom q1) \/ (dom ((len p1) Shift q2)))) . x) by A3, RELAT_1:13
.= ss . (((Sgm (dom q1)) ^ (Sgm (dom ((len p1) Shift q2)))) . x) by A1, A2, Lm11 ;

A34: now

assume A35: x in dom (Seq q1) ; :: thesis: (Seq ss) . x = ss1 . x
then A36: x in dom (Sgm (dom q1)) by Lm4;
then (Sgm (dom q1)) . x in rng (Sgm (dom q1)) by FUNCT_1:def 5;
then A37: (Sgm (dom q1)) . x in dom q1 by FINSEQ_1:71;
(Seq ss) . x = ss . ((Sgm (dom q1)) . x) by A33, A36, FINSEQ_1:def 7
.= q1 . ((Sgm (dom q1)) . x) by A3, A37, GRFUNC_1:35
.= (q1 * (Sgm (dom q1))) . x by A36, FUNCT_1:23
.= (Seq q1) . x by FINSEQ_1:def 14 ;
hence (Seq ss) . x = ss1 . x by A35, GRFUNC_1:35; :: thesis: verum

end;

now

assume A38: x in dom ((len (Seq q1)) Shift (Seq q2)) ; :: thesis: (Seq ss) . x = ss1 . x
dom ((len (Seq q1)) Shift (Seq q2)) = { ((len (Seq q1)) + j) where j is Element of NAT : j in dom (Seq q2) } by Def15;
then consider j being Element of NAT such that
A39: x = (len (Seq q1)) + j and
A40: j in dom (Seq q2) by A38;
A41: ss1 . x = ((len (Seq q1)) Shift (Seq q2)) . x by A38, GRFUNC_1:35
.= (Seq q2) . j by A39, A40, Def15 ;
A42: ex l1 being Nat st dom q1 c= Seg l1 by FINSEQ_1:def 12;
A43: ex l2 being Nat st dom ((len p1) Shift q2) c= Seg l2 by FINSEQ_1:def 12;
card (dom q1) = len (Sgm (dom q1)) by A42, FINSEQ_3:44;
then A44: card q1 = len (Sgm (dom q1)) by CARD_1:104;
A45: len (Seq q1) = card q1 by Th7;
A46: dom (Seq q2) = Seg (len (Seq q2)) by FINSEQ_1:def 3;
card q2 = len (Seq q2) by Th7;
then card ((len p1) Shift q2) = len (Seq q2) by Th57;
then A47: card (dom ((len p1) Shift q2)) = len (Seq q2) by CARD_1:104;
A48: card (dom ((len p1) Shift q2)) = len (Sgm (dom ((len p1) Shift q2))) by A43, FINSEQ_3:44;
A49: len (Sgm (dom ((len p1) Shift q2))) = len (Seq q2) by A43, A47, FINSEQ_3:44;
A50: dom (Seq q2) = dom (Sgm (dom ((len p1) Shift q2))) by A46, A47, A48, FINSEQ_1:def 3;
A51: j in dom (Sgm (dom ((len p1) Shift q2))) by A40, A46, A49, FINSEQ_1:def 3;
(Sgm (dom ((len p1) Shift q2))) . j in rng (Sgm (dom ((len p1) Shift q2))) by A40, A50, FUNCT_1:def 5;
then A52: (Sgm (dom ((len p1) Shift q2))) . j in dom ((len p1) Shift q2) by FINSEQ_1:71;
(Seq ss) . x = ss . ((Sgm (dom ((len p1) Shift q2))) . j) by A33, A39, A44, A45, A51, FINSEQ_1:def 7
.= ((len p1) Shift q2) . ((Sgm (dom ((len p1) Shift q2))) . j) by A3, A52, GRFUNC_1:35
.= (((len p1) Shift q2) * (Sgm (dom ((len p1) Shift q2)))) . j by A40, A50, FUNCT_1:23
.= (Seq ((len p1) Shift q2)) . j by FINSEQ_1:def 14
.= (Seq q2) . j by A40, Th76 ;
hence (Seq ss) . x = ss1 . x by A41; :: thesis: verum

end;

hence (Seq ss) . x = ss1 . x by A4, A15, A31, A34, XBOOLE_0:def 3; :: thesis: verum

end;

then Seq ss = ss1 by A4, A15, A30, FUNCT_1:9;
hence ex ss being FinSubsequence st
( ss = q1 \/ ((len p1) Shift q2) & dom (Seq ss) = Seg ((len (Seq q1)) + (len (Seq q2))) & Seq ss = (Seq q1) \/ ((len (Seq q1)) Shift (Seq q2)) ) by A3, A4; :: thesis: verum