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;
A5: 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;
A6: 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 ;
A7: 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;
A8: 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
A9: x = k1 and
A10: 1 <= k1 and
A11: k1 <= (len (Seq q1)) + (len (Seq q2)) by A5;
A12: ( 1 <= k1 & k1 <= len (Seq q1) implies k1 in dom (Seq q1) ) by A6;
( (len (Seq q1)) + 1 <= k1 & k1 <= (len (Seq q1)) + (len (Seq q2)) implies k1 in dom ((len (Seq q1)) Shift (Seq q2)) ) by A7;
hence x in (dom (Seq q1)) \/ (dom ((len (Seq q1)) Shift (Seq q2))) by A9, A10, A11, A12, INT_1:7, 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 A13: x in (dom (Seq q1)) \/ (dom ((len (Seq q1)) Shift (Seq q2))) ; :: thesis: x in Seg ((len (Seq q1)) + (len (Seq q2)))
A14: 0 <= len (Seq q1) by NAT_1:2;
A15: 0 <= len (Seq q2) by NAT_1:2;

A16: 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
A17: x = k1 and
A18: 1 <= k1 and
A19: k1 <= len (Seq q1) by A6;
(len (Seq q1)) + 0 <= (len (Seq q1)) + (len (Seq q2)) by A15, XREAL_1:7;
then k1 <= (len (Seq q1)) + (len (Seq q2)) by A19, XXREAL_0:2;
hence x in Seg ((len (Seq q1)) + (len (Seq q2))) by A5, A17, A18; :: 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
A20: x = k2 and
A21: (len (Seq q1)) + 1 <= k2 and
A22: k2 <= (len (Seq q1)) + (len (Seq q2)) by A7;
0 + 1 <= (len (Seq q1)) + 1 by A14, XREAL_1:7;
then 1 <= k2 by A21, XXREAL_0:2;
hence x in Seg ((len (Seq q1)) + (len (Seq q2))) by A5, A20, A22; :: thesis: verum

end;

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

end;

A23: (dom (Seq q1)) \/ (dom ((len (Seq q1)) Shift (Seq q2))) = dom ((Seq q1) \/ ((len (Seq q1)) Shift (Seq q2))) by RELAT_1:1;
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:13;
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 A24: x in dom (Seq ss) ; :: thesis: (Seq ss) . x = ss1 . x
then A25: x in dom (ss * (Sgm (dom ss))) by FINSEQ_1:def 14;
A26: (Seq ss) . x = (ss * (Sgm (dom ss))) . x by FINSEQ_1:def 14
.= ss . ((Sgm (dom ss)) . x) by A25, FUNCT_1:12
.= ss . ((Sgm ((dom q1) \/ (dom ((len p1) Shift q2)))) . x) by A3, RELAT_1:1
.= ss . (((Sgm (dom q1)) ^ (Sgm (dom ((len p1) Shift q2)))) . x) by A1, A2, Lm12 ;

A27: now

assume A28: x in dom (Seq q1) ; :: thesis: (Seq ss) . x = ss1 . x
then A29: x in dom (Sgm (dom q1)) by Lm5;
then (Sgm (dom q1)) . x in rng (Sgm (dom q1)) by FUNCT_1:def 3;
then A30: (Sgm (dom q1)) . x in dom q1 by FINSEQ_1:50;
(Seq ss) . x = ss . ((Sgm (dom q1)) . x) by A26, A29, FINSEQ_1:def 7
.= q1 . ((Sgm (dom q1)) . x) by A3, A30, GRFUNC_1:15
.= (q1 * (Sgm (dom q1))) . x by A29, FUNCT_1:13
.= (Seq q1) . x by FINSEQ_1:def 14 ;
hence (Seq ss) . x = ss1 . x by A28, GRFUNC_1:15; :: thesis: verum

end;

now

assume A31: 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
A32: x = (len (Seq q1)) + j and
A33: j in dom (Seq q2) by A31;
A34: ss1 . x = ((len (Seq q1)) Shift (Seq q2)) . x by A31, GRFUNC_1:15
.= (Seq q2) . j by A32, A33, Def15 ;
A35: ex l1 being Nat st dom q1 c= Seg l1 by FINSEQ_1:def 12;
A36: 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 A35, FINSEQ_3:39;
then A37: card q1 = len (Sgm (dom q1)) by CARD_1:62;
A38: len (Seq q1) = card q1 by Th7;
A39: 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 A40: card (dom ((len p1) Shift q2)) = len (Seq q2) by CARD_1:62;
A41: card (dom ((len p1) Shift q2)) = len (Sgm (dom ((len p1) Shift q2))) by A36, FINSEQ_3:39;
A42: len (Sgm (dom ((len p1) Shift q2))) = len (Seq q2) by A36, A40, FINSEQ_3:39;
A43: dom (Seq q2) = dom (Sgm (dom ((len p1) Shift q2))) by A39, A40, A41, FINSEQ_1:def 3;
A44: j in dom (Sgm (dom ((len p1) Shift q2))) by A33, A39, A42, FINSEQ_1:def 3;
(Sgm (dom ((len p1) Shift q2))) . j in rng (Sgm (dom ((len p1) Shift q2))) by A33, A43, FUNCT_1:def 3;
then A45: (Sgm (dom ((len p1) Shift q2))) . j in dom ((len p1) Shift q2) by FINSEQ_1:50;
(Seq ss) . x = ss . ((Sgm (dom ((len p1) Shift q2))) . j) by A26, A32, A37, A38, A44, FINSEQ_1:def 7
.= ((len p1) Shift q2) . ((Sgm (dom ((len p1) Shift q2))) . j) by A3, A45, GRFUNC_1:15
.= (((len p1) Shift q2) * (Sgm (dom ((len p1) Shift q2)))) . j by A33, A43, FUNCT_1:13
.= (Seq ((len p1) Shift q2)) . j by FINSEQ_1:def 14
.= (Seq q2) . j by A33, Th76 ;
hence (Seq ss) . x = ss1 . x by A34; :: thesis: verum

end;

hence (Seq ss) . x = ss1 . x by A4, A8, A24, A27, XBOOLE_0:def 3; :: thesis: verum

end;

then Seq ss = ss1 by A4, A8, A23, FUNCT_1:2;
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