let p1, p2 be FinSequence; for q1, q2 being FinSubsequence st q1 c= p1 & q2 c= p2 holds
Sgm ((dom q1) \/ (dom (Shift (q2,(len p1))))) = (Sgm (dom q1)) ^ (Sgm (dom (Shift (q2,(len p1)))))
let q1, q2 be FinSubsequence; ( q1 c= p1 & q2 c= p2 implies Sgm ((dom q1) \/ (dom (Shift (q2,(len p1))))) = (Sgm (dom q1)) ^ (Sgm (dom (Shift (q2,(len p1))))) )
assume that
A1:
q1 c= p1
and
A2:
q2 c= p2
; Sgm ((dom q1) \/ (dom (Shift (q2,(len p1))))) = (Sgm (dom q1)) ^ (Sgm (dom (Shift (q2,(len p1)))))
for m, n being Nat st m in dom q1 & n in dom (Shift (q2,(len p1))) holds
m < n
proof
let m,
n be
Nat;
( m in dom q1 & n in dom (Shift (q2,(len p1))) implies m < n )
assume that A5:
m in dom q1
and A6:
n in dom (Shift (q2,(len p1)))
;
m < n
A7:
dom p1 =
Seg (len p1)
by FINSEQ_1:def 3
.=
{ k where k is Nat : ( 1 <= k & k <= len p1 ) }
;
A8:
dom (Shift (p2,(len p1))) = { k where k is Nat : ( (len p1) + 1 <= k & k <= (len p1) + (len p2) ) }
by Th39;
A9:
dom q1 c= dom p1
by A1, GRFUNC_1:2;
A10:
dom (Shift (q2,(len p1))) c= dom (Shift (p2,(len p1)))
by A2, Lm7;
A11:
m in dom p1
by A5, A9;
A12:
n in dom (Shift (p2,(len p1)))
by A6, A10;
consider k3 being
Nat such that A13:
k3 = m
and
1
<= k3
and A14:
k3 <= len p1
by A7, A11;
consider k4 being
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;
k3 <> k4
by A5, A6, A9, A13, A15, Th47, XBOOLE_0:3;
hence
m < n
by A13, A15, A17, XXREAL_0:1;
verum
end;
hence
Sgm ((dom q1) \/ (dom (Shift (q2,(len p1))))) = (Sgm (dom q1)) ^ (Sgm (dom (Shift (q2,(len p1)))))
by FINSEQ_3:42; verum