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 \/ (Shift (q2,(len p1))) & dom (Seq ss) = Seg ((len (Seq q1)) + (len (Seq q2))) )
let q1, q2 be FinSubsequence; :: thesis: ( q1 c= p1 & q2 c= p2 implies ex ss being FinSubsequence st
( ss = q1 \/ (Shift (q2,(len p1))) & dom (Seq ss) = Seg ((len (Seq q1)) + (len (Seq q2))) ) )
assume that
A1: q1 c= p1 and
A2: q2 c= p2 ; :: thesis: ex ss being FinSubsequence st
( ss = q1 \/ (Shift (q2,(len p1))) & dom (Seq ss) = Seg ((len (Seq q1)) + (len (Seq q2))) )
consider ss being FinSubsequence such that
A3: ss = q1 \/ (Shift (q2,(len p1))) by A1, Th60;
A4: ex k1 being Nat st dom q1 c= Seg k1 by FINSEQ_1:def 12;
A5: ex k2 being Nat st dom (Shift (q2,(len p1))) c= Seg k2 by FINSEQ_1:def 12;
A6: rng (Sgm (dom ss)) = dom ss by FINSEQ_1:50;
A7: dom (Seq ss) = dom (Sgm (dom ss)) by A6, RELAT_1:27
.= dom (Sgm ((dom q1) \/ (dom (Shift (q2,(len p1)))))) by A3, XTUPLE_0:23
.= dom ((Sgm (dom q1)) ^ (Sgm (dom (Shift (q2,(len p1)))))) by A1, A2, Lm8
.= Seg ((len (Sgm (dom q1))) + (len (Sgm (dom (Shift (q2,(len p1))))))) by FINSEQ_1:def 7 ;
A8: len (Sgm (dom (Shift (q2,(len p1))))) = card (dom (Shift (q2,(len p1)))) by A5, FINSEQ_3:39;
A9: len (Sgm (dom q1)) = card (dom q1) by A4, FINSEQ_3:39;
len (Sgm (dom (Shift (q2,(len p1))))) = card (Shift (q2,(len p1))) by A8, CARD_1:62;
then A10: len (Sgm (dom (Shift (q2,(len p1))))) = card q2 by Th41;
A11: len (Sgm (dom q1)) = card q1 by A9, CARD_1:62;
A12: len (Sgm (dom (Shift (q2,(len p1))))) = len (Seq q2) by A10, FINSEQ_3:158;
len (Sgm (dom q1)) = len (Seq q1) by A11, FINSEQ_3:158;
hence ex ss being FinSubsequence st
( ss = q1 \/ (Shift (q2,(len p1))) & dom (Seq ss) = Seg ((len (Seq q1)) + (len (Seq q2))) ) by A3, A7, A12; :: thesis: verum