let p be FinSequence; :: thesis: for q1, q2 being FinSubsequence st q1 c= p holds
ex ss being FinSubsequence st ss = q1 \/ ((len p) Shift q2)
let q1, q2 be FinSubsequence; :: thesis: ( q1 c= p implies ex ss being FinSubsequence st ss = q1 \/ ((len p) Shift q2) )
assume q1 c= p ; :: thesis: ex ss being FinSubsequence st ss = q1 \/ ((len p) Shift q2)
then A1: dom q1 c= dom p by GRFUNC_1:2;
dom p misses dom ((len p) Shift q2) by Th63;
then reconsider ss = q1 \/ ((len p) Shift q2) 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 ((len p) Shift q2) c= Seg ((len p) + k) by A3, Th78;
0 <= k by NAT_1:2;
then (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, XBOOLE_1:1;
then (dom q1) \/ (dom ((len p) Shift q2)) c= Seg ((len p) + k) by A4, XBOOLE_1:8;
then dom (q1 \/ ((len p) Shift q2)) c= Seg ((len p) + k) by RELAT_1:1;
then reconsider ss = ss as FinSubsequence by FINSEQ_1:def 12;
take ss ; :: thesis: ss = q1 \/ ((len p) Shift q2)
thus ss = q1 \/ ((len p) Shift q2) ; :: thesis: verum