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

end;

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