let p be FinSequence; :: thesis: for q1, q2 being FinSubsequence st q1 c= p holds
ex ss being FinSubsequence st ss = q1 \/ (Shift (q2,(len p)))
let q1, q2 be FinSubsequence; :: thesis: ( q1 c= p implies ex ss being FinSubsequence st ss = q1 \/ (Shift (q2,(len p))) )
assume q1 c= p ; :: thesis: ex ss being FinSubsequence st ss = q1 \/ (Shift (q2,(len p)))
then A1: dom q1 c= dom p by GRFUNC_1:2;
dom p misses dom (Shift (q2,(len p))) by Th47;
then reconsider ss = q1 \/ (Shift (q2,(len p))) as Function by A1, GRFUNC_1:13, XBOOLE_1:63;
A2: dom p = Seg (len p) by FINSEQ_1:def 3;
consider k being Nat such that
A3: dom q2 c= Seg k by FINSEQ_1:def 12;
k in NAT by ORDINAL1:def 12;
then A4: dom (Shift (q2,(len p))) c= Seg ((len p) + k) by A3, Th59;
(len p) + 0 <= (len p) + k by XREAL_1:7;
then Seg (len p) c= Seg ((len p) + k) by FINSEQ_1:5;
then dom q1 c= Seg ((len p) + k) by A1, A2;
then (dom q1) \/ (dom (Shift (q2,(len p)))) c= Seg ((len p) + k) by A4, XBOOLE_1:8;
then dom (q1 \/ (Shift (q2,(len p)))) c= Seg ((len p) + k) by XTUPLE_0:23;
then reconsider ss = ss as FinSubsequence by FINSEQ_1:def 12;
take ss ; :: thesis: ss = q1 \/ (Shift (q2,(len p)))
thus ss = q1 \/ (Shift (q2,(len p))) ; :: thesis: verum