let p1, p2 be FinSequence; for q1, q2 being FinSubsequence st q1 c= p1 & q2 c= p2 holds
Sgm ((dom q1) \/ (dom ((len p1) Shift q2))) = (Sgm (dom q1)) ^ (Sgm (dom ((len p1) Shift q2)))
let q1, q2 be FinSubsequence; ( q1 c= p1 & q2 c= p2 implies Sgm ((dom q1) \/ (dom ((len p1) Shift q2))) = (Sgm (dom q1)) ^ (Sgm (dom ((len p1) Shift q2))) )
assume that
A1:
q1 c= p1
and
A2:
q2 c= p2
; Sgm ((dom q1) \/ (dom ((len p1) Shift q2))) = (Sgm (dom q1)) ^ (Sgm (dom ((len p1) Shift q2)))
A3:
ex k1 being Nat st dom q1 c= Seg k1
by FINSEQ_1:def 12;
A4:
ex k2 being Nat st dom ((len p1) Shift q2) c= Seg k2
by FINSEQ_1:def 12;
for m, n being Element of NAT st m in dom q1 & n in dom ((len p1) Shift q2) holds
m < n
proof
let m,
n be
Element of
NAT ;
( m in dom q1 & n in dom ((len p1) Shift q2) implies m < n )
assume that A5:
m in dom q1
and A6:
n in dom ((len p1) Shift q2)
;
m < n
A7:
dom p1 =
Seg (len p1)
by FINSEQ_1:def 3
.=
{ k where k is Element of NAT : ( 1 <= k & k <= len p1 ) }
by FINSEQ_1:def 1
;
A8:
dom ((len p1) Shift p2) = { k where k is Element of NAT : ( (len p1) + 1 <= k & k <= (len p1) + (len p2) ) }
by Th54;
A9:
dom q1 c= dom p1
by A1, GRFUNC_1:2;
A10:
dom ((len p1) Shift q2) c= dom ((len p1) Shift p2)
by A2, Lm11;
A11:
m in dom p1
by A5, A9;
A12:
n in dom ((len p1) Shift p2)
by A6, A10;
consider k3 being
Element of
NAT such that A13:
k3 = m
and
1
<= k3
and A14:
k3 <= len p1
by A7, A11;
consider k4 being
Element of
NAT such that A15:
k4 = n
and A16:
(len p1) + 1
<= k4
and
k4 <= (len p1) + (len p2)
by A8, A12;
len p1 < (len p1) + 1
by XREAL_1:29;
then
k3 <= (len p1) + 1
by A14, XXREAL_0:2;
then A17:
k3 <= k4
by A16, XXREAL_0:2;
dom p1 misses dom ((len p1) Shift p2)
by Th63;
then
k3 <> k4
by A5, A6, A9, A10, A13, A15, Lm3;
hence
m < n
by A13, A15, A17, XXREAL_0:1;
verum
end;
hence
Sgm ((dom q1) \/ (dom ((len p1) Shift q2))) = (Sgm (dom q1)) ^ (Sgm (dom ((len p1) Shift q2)))
by A3, A4, FINSEQ_3:42; verum