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 \/ (Shift (q2,(len p1))) & (Seq q1) ^ (Seq q2) = Seq ss )
let q1, q2 be FinSubsequence; :: thesis: ( q1 c= p1 & q2 c= p2 implies ex ss being FinSubsequence st
( ss = q1 \/ (Shift (q2,(len p1))) & (Seq q1) ^ (Seq q2) = Seq ss ) )
assume that
A1: q1 c= p1 and
A2: q2 c= p2 ; :: thesis: ex ss being FinSubsequence st
( ss = q1 \/ (Shift (q2,(len p1))) & (Seq q1) ^ (Seq q2) = Seq ss )
consider ss being FinSubsequence such that
A3: ss = q1 \/ (Shift (q2,(len p1))) and
A4: dom (Seq ss) = Seg ((len (Seq q1)) + (len (Seq q2))) and
A5: Seq ss = (Seq q1) \/ (Shift ((Seq q2),(len (Seq q1)))) by A1, A2, Th62;
A6: for j1 being Nat st j1 in dom (Seq q1) holds
(Seq ss) . j1 = (Seq q1) . j1 by A5, GRFUNC_1:15;
for j2 being Nat st j2 in dom (Seq q2) holds
(Seq ss) . ((len (Seq q1)) + j2) = (Seq q2) . j2

proof

let j2 be Nat; :: thesis: ( j2 in dom (Seq q2) implies (Seq ss) . ((len (Seq q1)) + j2) = (Seq q2) . j2 )
assume A7: j2 in dom (Seq q2) ; :: thesis: (Seq ss) . ((len (Seq q1)) + j2) = (Seq q2) . j2
dom (Shift ((Seq q2),(len (Seq q1)))) = { (k + (len (Seq q1))) where k is Nat : k in dom (Seq q2) } by Def12;
then (len (Seq q1)) + j2 in dom (Shift ((Seq q2),(len (Seq q1)))) by A7;
hence (Seq ss) . ((len (Seq q1)) + j2) = (Shift ((Seq q2),(len (Seq q1)))) . ((len (Seq q1)) + j2) by A5, GRFUNC_1:15
.= (Seq q2) . j2 by A7, Def12 ;
:: thesis: verum

end;

then Seq ss = (Seq q1) ^ (Seq q2) by A4, A6, FINSEQ_1:def 7;
hence ex ss being FinSubsequence st
( ss = q1 \/ (Shift (q2,(len p1))) & (Seq q1) ^ (Seq q2) = Seq ss ) by A3; :: thesis: verum