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))) & Seq ss = (Seq q1) \/ (Shift ((Seq q2),(len (Seq q1)))) )
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))) & Seq ss = (Seq q1) \/ (Shift ((Seq q2),(len (Seq q1)))) ) )
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))) & Seq ss = (Seq q1) \/ (Shift ((Seq q2),(len (Seq q1)))) )
consider ss being FinSubsequence such that
A3: ss = q1 \/ (Shift (q2,(len p1))) and
A4: dom (Seq ss) = Seg ((len (Seq q1)) + (len (Seq q2))) by A1, A2, Th61;
A5: dom (Seq q1) = Seg (len (Seq q1)) by FINSEQ_1:def 3
.= { k where k is Nat : ( 1 <= k & k <= len (Seq q1) ) } ;
A6: dom (Shift ((Seq q2),(len (Seq q1)))) = { k where k is Nat : ( (len (Seq q1)) + 1 <= k & k <= (len (Seq q1)) + (len (Seq q2)) ) } by Th39;
A7: Seg ((len (Seq q1)) + (len (Seq q2))) = (dom (Seq q1)) \/ (dom (Shift ((Seq q2),(len (Seq q1)))))
proof
thus Seg ((len (Seq q1)) + (len (Seq q2))) c= (dom (Seq q1)) \/ (dom (Shift ((Seq q2),(len (Seq q1))))) :: according to XBOOLE_0:def 10 :: thesis: (dom (Seq q1)) \/ (dom (Shift ((Seq q2),(len (Seq q1))))) c= Seg ((len (Seq q1)) + (len (Seq q2)))
proof
let x be object ; :: according to TARSKI:def 3 :: thesis: ( not x in Seg ((len (Seq q1)) + (len (Seq q2))) or x in (dom (Seq q1)) \/ (dom (Shift ((Seq q2),(len (Seq q1))))) )
assume x in Seg ((len (Seq q1)) + (len (Seq q2))) ; :: thesis: x in (dom (Seq q1)) \/ (dom (Shift ((Seq q2),(len (Seq q1)))))
then consider k1 being Nat such that
A8: x = k1 and
A9: 1 <= k1 and
A10: k1 <= (len (Seq q1)) + (len (Seq q2)) ;
A11: ( 1 <= k1 & k1 <= len (Seq q1) implies k1 in dom (Seq q1) ) by A5;
( (len (Seq q1)) + 1 <= k1 & k1 <= (len (Seq q1)) + (len (Seq q2)) implies k1 in dom (Shift ((Seq q2),(len (Seq q1)))) ) by A6;
hence x in (dom (Seq q1)) \/ (dom (Shift ((Seq q2),(len (Seq q1))))) by A8, A9, A10, A11, INT_1:7, XBOOLE_0:def 3; :: thesis: verum
end;
let x be object ; :: according to TARSKI:def 3 :: thesis: ( not x in (dom (Seq q1)) \/ (dom (Shift ((Seq q2),(len (Seq q1))))) or x in Seg ((len (Seq q1)) + (len (Seq q2))) )
assume A12: x in (dom (Seq q1)) \/ (dom (Shift ((Seq q2),(len (Seq q1))))) ; :: thesis: x in Seg ((len (Seq q1)) + (len (Seq q2)))
A13: now :: thesis: ( x in dom (Seq q1) implies x in Seg ((len (Seq q1)) + (len (Seq q2))) )
assume x in dom (Seq q1) ; :: thesis: x in Seg ((len (Seq q1)) + (len (Seq q2)))
then consider k1 being Nat such that
A14: x = k1 and
A15: 1 <= k1 and
A16: k1 <= len (Seq q1) by A5;
(len (Seq q1)) + 0 <= (len (Seq q1)) + (len (Seq q2)) by XREAL_1:7;
then k1 <= (len (Seq q1)) + (len (Seq q2)) by A16, XXREAL_0:2;
hence x in Seg ((len (Seq q1)) + (len (Seq q2))) by A14, A15; :: thesis: verum
end;
now :: thesis: ( x in dom (Shift ((Seq q2),(len (Seq q1)))) implies x in Seg ((len (Seq q1)) + (len (Seq q2))) )
assume x in dom (Shift ((Seq q2),(len (Seq q1)))) ; :: thesis: x in Seg ((len (Seq q1)) + (len (Seq q2)))
then consider k2 being Nat such that
A17: x = k2 and
A18: (len (Seq q1)) + 1 <= k2 and
A19: k2 <= (len (Seq q1)) + (len (Seq q2)) by A6;
0 + 1 <= (len (Seq q1)) + 1 by XREAL_1:7;
then 1 <= k2 by A18, XXREAL_0:2;
hence x in Seg ((len (Seq q1)) + (len (Seq q2))) by A17, A19; :: thesis: verum
end;
hence x in Seg ((len (Seq q1)) + (len (Seq q2))) by A12, A13, XBOOLE_0:def 3; :: thesis: verum
end;
A20: (dom (Seq q1)) \/ (dom (Shift ((Seq q2),(len (Seq q1))))) = dom ((Seq q1) \/ (Shift ((Seq q2),(len (Seq q1))))) by XTUPLE_0:23;
dom (Seq q1) misses dom (Shift ((Seq q2),(len (Seq q1)))) by Th47;
then reconsider ss1 = (Seq q1) \/ (Shift ((Seq q2),(len (Seq q1)))) as Function by GRFUNC_1:13;
for x being object st x in dom (Seq ss) holds
(Seq ss) . x = ss1 . x
proof
let x be object ; :: thesis: ( x in dom (Seq ss) implies (Seq ss) . x = ss1 . x )
assume A21: x in dom (Seq ss) ; :: thesis: (Seq ss) . x = ss1 . x
A22: (Seq ss) . x = (ss * (Sgm (dom ss))) . x
.= ss . ((Sgm (dom ss)) . x) by A21, FUNCT_1:12
.= ss . ((Sgm ((dom q1) \/ (dom (Shift (q2,(len p1)))))) . x) by A3, XTUPLE_0:23
.= ss . (((Sgm (dom q1)) ^ (Sgm (dom (Shift (q2,(len p1)))))) . x) by A1, A2, Lm8 ;
A23: now :: thesis: ( x in dom (Seq q1) implies (Seq ss) . x = ss1 . x )
assume A24: x in dom (Seq q1) ; :: thesis: (Seq ss) . x = ss1 . x
then A25: x in dom (Sgm (dom q1)) by FINSEQ_1:100;
then (Sgm (dom q1)) . x in rng (Sgm (dom q1)) by FUNCT_1:def 3;
then A26: (Sgm (dom q1)) . x in dom q1 by FINSEQ_1:50;
(Seq ss) . x = ss . ((Sgm (dom q1)) . x) by A22, A25, FINSEQ_1:def 7
.= q1 . ((Sgm (dom q1)) . x) by A3, A26, GRFUNC_1:15
.= (q1 * (Sgm (dom q1))) . x by A25, FUNCT_1:13
.= (Seq q1) . x ;
hence (Seq ss) . x = ss1 . x by A24, GRFUNC_1:15; :: thesis: verum
end;
now :: thesis: ( x in dom (Shift ((Seq q2),(len (Seq q1)))) implies (Seq ss) . x = ss1 . x )
assume A27: x in dom (Shift ((Seq q2),(len (Seq q1)))) ; :: thesis: (Seq ss) . x = ss1 . x
dom (Shift ((Seq q2),(len (Seq q1)))) = { (j + (len (Seq q1))) where j is Nat : j in dom (Seq q2) } by Def12;
then consider j being Nat such that
A28: x = j + (len (Seq q1)) and
A29: j in dom (Seq q2) by A27;
A30: ss1 . x = (Shift ((Seq q2),(len (Seq q1)))) . x by A27, GRFUNC_1:15
.= (Seq q2) . j by A28, A29, Def12 ;
A31: ex l1 being Nat st dom q1 c= Seg l1 by FINSEQ_1:def 12;
A32: ex l2 being Nat st dom (Shift (q2,(len p1))) c= Seg l2 by FINSEQ_1:def 12;
card (dom q1) = len (Sgm (dom q1)) by A31, FINSEQ_3:39;
then A33: card q1 = len (Sgm (dom q1)) by CARD_1:62;
A34: len (Seq q1) = card q1 by FINSEQ_3:158;
A35: dom (Seq q2) = Seg (len (Seq q2)) by FINSEQ_1:def 3;
card q2 = len (Seq q2) by FINSEQ_3:158;
then A36: card (Shift (q2,(len p1))) = len (Seq q2) by Th41;
then A37: card (dom (Shift (q2,(len p1)))) = len (Seq q2) by CARD_1:62;
A38: card (dom (Shift (q2,(len p1)))) = len (Sgm (dom (Shift (q2,(len p1))))) by A32, FINSEQ_3:39;
A39: len (Sgm (dom (Shift (q2,(len p1))))) = len (Seq q2) by A32, A37, FINSEQ_3:39;
A40: dom (Seq q2) = dom (Sgm (dom (Shift (q2,(len p1))))) by A35, A36, A38, CARD_1:62, FINSEQ_1:def 3;
A41: j in dom (Sgm (dom (Shift (q2,(len p1))))) by A29, A35, A39, FINSEQ_1:def 3;
(Sgm (dom (Shift (q2,(len p1))))) . j in rng (Sgm (dom (Shift (q2,(len p1))))) by A29, A40, FUNCT_1:def 3;
then A42: (Sgm (dom (Shift (q2,(len p1))))) . j in dom (Shift (q2,(len p1))) by FINSEQ_1:50;
(Seq ss) . x = ss . ((Sgm (dom (Shift (q2,(len p1))))) . j) by A22, A28, A33, A34, A41, FINSEQ_1:def 7
.= (Shift (q2,(len p1))) . ((Sgm (dom (Shift (q2,(len p1))))) . j) by A3, A42, GRFUNC_1:15
.= ((Shift (q2,(len p1))) * (Sgm (dom (Shift (q2,(len p1)))))) . j by A29, A40, FUNCT_1:13
.= (Seq (Shift (q2,(len p1)))) . j
.= (Seq q2) . j by A29, Th57 ;
hence (Seq ss) . x = ss1 . x by A30; :: thesis: verum
end;
hence (Seq ss) . x = ss1 . x by A4, A7, A21, A23, XBOOLE_0:def 3; :: thesis: verum
end;
then Seq ss = ss1 by A4, A7, A20;
hence ex ss being FinSubsequence st
( ss = q1 \/ (Shift (q2,(len p1))) & dom (Seq ss) = Seg ((len (Seq q1)) + (len (Seq q2))) & Seq ss = (Seq q1) \/ (Shift ((Seq q2),(len (Seq q1)))) ) by A3, A4; :: thesis: verum