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))) & Seq ss = (Seq q1) \/ ((len (Seq q1)) Shift (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))) & Seq ss = (Seq q1) \/ ((len (Seq q1)) Shift (Seq q2)) ) )
assume A1:
( q1 c= p1 & 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))) & Seq ss = (Seq q1) \/ ((len (Seq q1)) Shift (Seq q2)) )
then consider ss being FinSubsequence such that
A2:
ss = q1 \/ ((len p1) Shift q2)
and
A3:
dom (Seq ss) = Seg ((len (Seq q1)) + (len (Seq q2)))
by Th80;
per cases
( ( q1 = {} & q2 = {} ) or ( q1 = {} & q2 <> {} ) or ( q1 <> {} & q2 = {} ) or ( q1 <> {} & q2 <> {} ) )
;
suppose A11:
(
q1 <> {} &
q2 <> {} )
;
:: thesis: ex ss being FinSubsequence st
( ss = q1 \/ ((len p1) Shift q2) & dom (Seq ss) = Seg ((len (Seq q1)) + (len (Seq q2))) & Seq ss = (Seq q1) \/ ((len (Seq q1)) Shift (Seq q2)) )A12:
Seg ((len (Seq q1)) + (len (Seq q2))) = { k where k is Element of NAT : ( 1 <= k & k <= (len (Seq q1)) + (len (Seq q2)) ) }
by FINSEQ_1:def 1;
A13:
dom (Seq q1) =
Seg (len (Seq q1))
by FINSEQ_1:def 3
.=
{ k where k is Element of NAT : ( 1 <= k & k <= len (Seq q1) ) }
by FINSEQ_1:def 1
;
Seq q2 <> {}
by A11, Th2;
then A14:
dom ((len (Seq q1)) Shift (Seq q2)) = { k where k is Element of NAT : ( (len (Seq q1)) + 1 <= k & k <= (len (Seq q1)) + (len (Seq q2)) ) }
by Th54;
A15:
Seg ((len (Seq q1)) + (len (Seq q2))) = (dom (Seq q1)) \/ (dom ((len (Seq q1)) Shift (Seq q2)))
A23:
(dom (Seq q1)) \/ (dom ((len (Seq q1)) Shift (Seq q2))) = dom ((Seq q1) \/ ((len (Seq q1)) Shift (Seq q2)))
by RELAT_1:13;
dom (Seq q1) misses dom ((len (Seq q1)) Shift (Seq q2))
by Th63;
then reconsider ss1 =
(Seq q1) \/ ((len (Seq q1)) Shift (Seq q2)) as
Function by GRFUNC_1:31;
for
x being
set st
x in dom (Seq ss) holds
(Seq ss) . x = ss1 . x
proof
let x be
set ;
:: thesis: ( x in dom (Seq ss) implies (Seq ss) . x = ss1 . x )
assume A24:
x in dom (Seq ss)
;
:: thesis: (Seq ss) . x = ss1 . x
then A25:
x in dom (ss * (Sgm (dom ss)))
by FINSEQ_1:def 14;
A26:
(Seq ss) . x =
(ss * (Sgm (dom ss))) . x
by FINSEQ_1:def 14
.=
ss . ((Sgm (dom ss)) . x)
by A25, FUNCT_1:22
.=
ss . ((Sgm ((dom q1) \/ (dom ((len p1) Shift q2)))) . x)
by A2, RELAT_1:13
.=
ss . (((Sgm (dom q1)) ^ (Sgm (dom ((len p1) Shift q2)))) . x)
by A1, A11, Lm11
;
now assume A31:
x in dom ((len (Seq q1)) Shift (Seq q2))
;
:: thesis: (Seq ss) . x = ss1 . x
dom ((len (Seq q1)) Shift (Seq q2)) = { ((len (Seq q1)) + j) where j is Element of NAT : j in dom (Seq q2) }
by Def15;
then consider j being
Element of
NAT such that A32:
(
x = (len (Seq q1)) + j &
j in dom (Seq q2) )
by A31;
A33:
ss1 . x =
((len (Seq q1)) Shift (Seq q2)) . x
by A31, GRFUNC_1:35
.=
(Seq q2) . j
by A32, Def15
;
consider l1 being
Nat such that A34:
dom q1 c= Seg l1
by FINSEQ_1:def 12;
consider l2 being
Nat such that A35:
dom ((len p1) Shift q2) c= Seg l2
by FINSEQ_1:def 12;
card (dom q1) = len (Sgm (dom q1))
by A34, FINSEQ_3:44;
then A36:
card q1 = len (Sgm (dom q1))
by CARD_1:104;
A37:
len (Seq q1) = card q1
by Th7;
A38:
dom (Seq q2) = Seg (len (Seq q2))
by FINSEQ_1:def 3;
card q2 = len (Seq q2)
by Th7;
then
card ((len p1) Shift q2) = len (Seq q2)
by Th57;
then A39:
card (dom ((len p1) Shift q2)) = len (Seq q2)
by CARD_1:104;
A40:
card (dom ((len p1) Shift q2)) = len (Sgm (dom ((len p1) Shift q2)))
by A35, FINSEQ_3:44;
A41:
len (Sgm (dom ((len p1) Shift q2))) = len (Seq q2)
by A35, A39, FINSEQ_3:44;
A42:
dom (Seq q2) = dom (Sgm (dom ((len p1) Shift q2)))
by A38, A39, A40, FINSEQ_1:def 3;
A43:
j in dom (Sgm (dom ((len p1) Shift q2)))
by A32, A38, A41, FINSEQ_1:def 3;
(Sgm (dom ((len p1) Shift q2))) . j in rng (Sgm (dom ((len p1) Shift q2)))
by A32, A42, FUNCT_1:def 5;
then A44:
(Sgm (dom ((len p1) Shift q2))) . j in dom ((len p1) Shift q2)
by FINSEQ_1:71;
(Seq ss) . x =
ss . ((Sgm (dom ((len p1) Shift q2))) . j)
by A26, A32, A36, A37, A43, FINSEQ_1:def 7
.=
((len p1) Shift q2) . ((Sgm (dom ((len p1) Shift q2))) . j)
by A2, A44, GRFUNC_1:35
.=
(((len p1) Shift q2) * (Sgm (dom ((len p1) Shift q2)))) . j
by A32, A42, FUNCT_1:23
.=
(Seq ((len p1) Shift q2)) . j
by FINSEQ_1:def 14
.=
(Seq q2) . j
by A32, Th76
;
hence
(Seq ss) . x = ss1 . x
by A33;
:: thesis: verum end;
hence
(Seq ss) . x = ss1 . x
by A3, A15, A24, A27, XBOOLE_0:def 3;
:: thesis: verum
end; then
Seq ss = ss1
by A3, A15, A23, FUNCT_1:9;
hence
ex
ss being
FinSubsequence st
(
ss = q1 \/ ((len p1) Shift q2) &
dom (Seq ss) = Seg ((len (Seq q1)) + (len (Seq q2))) &
Seq ss = (Seq q1) \/ ((len (Seq q1)) Shift (Seq q2)) )
by A2, A3;
:: thesis: verum end;