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) & (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 \/ ((len p1) Shift q2) & (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 \/ ((len p1) Shift q2) & (Seq q1) ^ (Seq q2) = Seq ss )
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))) and
A5: Seq ss = (Seq q1) \/ ((len (Seq q1)) Shift (Seq q2)) by A1, A2, Th81;
A6: for j1 being Nat st j1 in dom (Seq q1) holds
(Seq ss) . j1 = (Seq q1) . j1 by A5, GRFUNC_1:35;
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 ((len (Seq q1)) Shift (Seq q2)) = { ((len (Seq q1)) + k) where k is Element of NAT : k in dom (Seq q2) } by Def15;
then (len (Seq q1)) + j2 in dom ((len (Seq q1)) Shift (Seq q2)) by A7;
hence (Seq ss) . ((len (Seq q1)) + j2) = ((len (Seq q1)) Shift (Seq q2)) . ((len (Seq q1)) + j2) by A5, GRFUNC_1:35
.= (Seq q2) . j2 by A7, Def15 ;
:: 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 \/ ((len p1) Shift q2) & (Seq q1) ^ (Seq q2) = Seq ss ) by A3; :: thesis: verum