let p1, p2 be FinSequence; 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; ( 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
; 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; verum