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))) )
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))) ) )
assume A1: ( q1 c= p1 & 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))) )

per cases ( q2 = {} or q2 <> {} ) ;

suppose A2: q2 = {} ; :: thesis: ex ss being FinSubsequence st
( ss = q1 \/ ((len p1) Shift q2) & dom (Seq ss) = Seg ((len (Seq q1)) + (len (Seq q2))) )

consider ss being FinSubsequence such that
A3: ss = q1 \/ ((len p1) Shift q2) by A1, Th79;
(len p1) Shift q2 = {} by A2, Th55;
then A4: dom (Seq ss) = Seg (len (Seq q1)) by A3, FINSEQ_1:def 3;
Seq q2 = {} by A2, Th2;
then len (Seq q2) = 0 ;
hence ex ss being FinSubsequence st
( ss = q1 \/ ((len p1) Shift q2) & dom (Seq ss) = Seg ((len (Seq q1)) + (len (Seq q2))) ) by A3, A4; :: thesis: verum

end;

suppose A5: q2 <> {} ; :: thesis: ex ss being FinSubsequence st
( ss = q1 \/ ((len p1) Shift q2) & dom (Seq ss) = Seg ((len (Seq q1)) + (len (Seq q2))) )

consider ss being FinSubsequence such that
A6: ss = q1 \/ ((len p1) Shift q2) by A1, Th79;
consider k1 being Nat such that
A7: dom q1 c= Seg k1 by FINSEQ_1:def 12;
consider k2 being Nat such that
A8: dom ((len p1) Shift q2) c= Seg k2 by FINSEQ_1:def 12;
A9: rng (Sgm (dom ss)) = dom ss by FINSEQ_1:71;
dom (Seq ss) = dom (ss * (Sgm (dom ss))) by FINSEQ_1:def 14;
then A10: dom (Seq ss) = dom (Sgm (dom ss)) by A9, RELAT_1:46
.= dom (Sgm ((dom q1) \/ (dom ((len p1) Shift q2)))) by A6, RELAT_1:13
.= dom ((Sgm (dom q1)) ^ (Sgm (dom ((len p1) Shift q2)))) by A1, A5, Lm11
.= Seg ((len (Sgm (dom q1))) + (len (Sgm (dom ((len p1) Shift q2))))) by FINSEQ_1:def 7 ;
( len (Sgm (dom ((len p1) Shift q2))) = card (dom ((len p1) Shift q2)) & len (Sgm (dom q1)) = card (dom q1) ) by A7, A8, FINSEQ_3:44;
then ( len (Sgm (dom ((len p1) Shift q2))) = card ((len p1) Shift q2) & len (Sgm (dom q1)) = card q1 ) by CARD_1:104;
then ( len (Sgm (dom ((len p1) Shift q2))) = card q2 & len (Sgm (dom q1)) = card q1 ) by Th57;
then ( len (Sgm (dom ((len p1) Shift q2))) = len (Seq q2) & len (Sgm (dom q1)) = len (Seq q1) ) by Th7;
hence ex ss being FinSubsequence st
( ss = q1 \/ ((len p1) Shift q2) & dom (Seq ss) = Seg ((len (Seq q1)) + (len (Seq q2))) ) by A6, A10; :: thesis: verum

end;

end;