let p1, p2 be FinSequence; :: thesis: for q1, q2 being FinSubsequence st q2 <> {} & 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; :: thesis: ( q2 <> {} & 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 A1:
( q2 <> {} & q1 c= p1 & q2 c= p2 )
; :: thesis: Sgm ((dom q1) \/ (dom ((len p1) Shift q2))) = (Sgm (dom q1)) ^ (Sgm (dom ((len p1) Shift q2)))
consider k1 being Nat such that
A2:
dom q1 c= Seg k1
by FINSEQ_1:def 12;
consider k2 being Nat such that
A3:
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 ;
:: thesis: ( m in dom q1 & n in dom ((len p1) Shift q2) implies m < n )
assume that A4:
m in dom q1
and A5:
n in dom ((len p1) Shift q2)
;
:: thesis: m < n
A6:
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
;
consider x being
set such that A7:
x in q2
by A1, XBOOLE_0: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 A1, A7, Th54;
A9:
dom q1 c= dom p1
by A1, GRFUNC_1:8;
A10:
dom ((len p1) Shift q2) c= dom ((len p1) Shift p2)
by A1, Lm10;
A11:
m in dom p1
by A4, A9;
A12:
n in dom ((len p1) Shift p2)
by A5, A10;
consider k3 being
Element of
NAT such that A13:
(
k3 = m & 1
<= k3 &
k3 <= len p1 )
by A6, A11;
consider k4 being
Element of
NAT such that A14:
(
k4 = n &
(len p1) + 1
<= k4 &
k4 <= (len p1) + (len p2) )
by A8, A12;
len p1 < (len p1) + 1
by XREAL_1:31;
then
k3 <= (len p1) + 1
by A13, XXREAL_0:2;
then A15:
k3 <= k4
by A14, XXREAL_0:2;
dom p1 misses dom ((len p1) Shift p2)
by Th63;
then
k3 <> k4
by A4, A5, A9, A10, A13, A14, Lm3;
hence
m < n
by A13, A14, A15, XXREAL_0:1;
:: thesis: verum
end;
hence
Sgm ((dom q1) \/ (dom ((len p1) Shift q2))) = (Sgm (dom q1)) ^ (Sgm (dom ((len p1) Shift q2)))
by A2, A3, FINSEQ_3:48; :: thesis: verum