let p1, p2 be FinSequence; 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; ( 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
; 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
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; verum