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
A6: ss = q1 \/ ((len p1) Shift q2) by A1, Th79;
A7: ex k1 being Nat st dom q1 c= Seg k1 by FINSEQ_1:def 12;
A8: ex k2 being Nat st dom ((len p1) Shift q2) c= Seg k2 by FINSEQ_1:def 12;
A9: rng (Sgm (dom ss)) = dom ss by FINSEQ_1:71;
dom (Seq ss) = dom (ss * (Sgm (dom ss))) by FINSEQ_1:def 14;
then A10: dom (Seq ss) = dom (Sgm (dom ss)) by A9, RELAT_1:46
.= dom (Sgm ((dom q1) \/ (dom ((len p1) Shift q2)))) by A6, RELAT_1:13
.= dom ((Sgm (dom q1)) ^ (Sgm (dom ((len p1) Shift q2)))) by A1, A2, Lm11
.= Seg ((len (Sgm (dom q1))) + (len (Sgm (dom ((len p1) Shift q2))))) by FINSEQ_1:def 7 ;
A11: len (Sgm (dom ((len p1) Shift q2))) = card (dom ((len p1) Shift q2)) by A8, FINSEQ_3:44;
A12: len (Sgm (dom q1)) = card (dom q1) by A7, FINSEQ_3:44;
len (Sgm (dom ((len p1) Shift q2))) = card ((len p1) Shift q2) by A11, CARD_1:104;
then A13: len (Sgm (dom ((len p1) Shift q2))) = card q2 by Th57;
A14: len (Sgm (dom q1)) = card q1 by A12, CARD_1:104;
A15: len (Sgm (dom ((len p1) Shift q2))) = len (Seq q2) by A13, Th7;
len (Sgm (dom q1)) = len (Seq q1) by A14, Th7;
hence ex ss being FinSubsequence st
( ss = q1 \/ ((len p1) Shift q2) & dom (Seq ss) = Seg ((len (Seq q1)) + (len (Seq q2))) ) by A6, A10, A15; :: thesis: verum