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) & 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 \/ ((len p1) Shift q2) & 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 \/ ((len p1) Shift q2) & dom (Seq ss) = Seg ((len (Seq q1)) + (len (Seq q2))) )
consider ss being FinSubsequence such that
A3: ss = q1 \/ ((len p1) Shift q2) by A1, Th79;
A4: ex k1 being Nat st dom q1 c= Seg k1 by FINSEQ_1:def 12;
A5: ex k2 being Nat st dom ((len p1) Shift q2) c= Seg k2 by FINSEQ_1:def 12;
A6: rng (Sgm (dom ss)) = dom ss by FINSEQ_1:50;
dom (Seq ss) = dom (ss * (Sgm (dom ss))) by FINSEQ_1:def 14;
then A7: dom (Seq ss) = dom (Sgm (dom ss)) by A6, RELAT_1:27
.= dom (Sgm ((dom q1) \/ (dom ((len p1) Shift q2)))) by A3, RELAT_1:1
.= dom ((Sgm (dom q1)) ^ (Sgm (dom ((len p1) Shift q2)))) by A1, A2, Lm12
.= Seg ((len (Sgm (dom q1))) + (len (Sgm (dom ((len p1) Shift q2))))) by FINSEQ_1:def 7 ;
A8: len (Sgm (dom ((len p1) Shift q2))) = card (dom ((len p1) Shift q2)) by A5, FINSEQ_3:39;
A9: len (Sgm (dom q1)) = card (dom q1) by A4, FINSEQ_3:39;
len (Sgm (dom ((len p1) Shift q2))) = card ((len p1) Shift q2) by A8, CARD_1:62;
then A10: len (Sgm (dom ((len p1) Shift q2))) = card q2 by Th57;
A11: len (Sgm (dom q1)) = card q1 by A9, CARD_1:62;
A12: len (Sgm (dom ((len p1) Shift q2))) = len (Seq q2) by A10, Th7;
len (Sgm (dom q1)) = len (Seq q1) by A11, Th7;
hence ex ss being FinSubsequence st
( ss = q1 \/ ((len p1) Shift q2) & dom (Seq ss) = Seg ((len (Seq q1)) + (len (Seq q2))) ) by A3, A7, A12; :: thesis: verum