let s1, s2 be FinSequence; ( ( 1 <= m & m <= n & n <= len p & (len s1) + m = n + 1 & ( for i being Nat st i < len s1 holds
s1 . (i + 1) = p . (m + i) ) & (len s2) + m = n + 1 & ( for i being Nat st i < len s2 holds
s2 . (i + 1) = p . (m + i) ) implies s1 = s2 ) & ( ( not 1 <= m or not m <= n or not n <= len p ) & s1 = {} & s2 = {} implies s1 = s2 ) )
hereby ( ( not 1 <= m or not m <= n or not n <= len p ) & s1 = {} & s2 = {} implies s1 = s2 )
assume that
1
<= m
and
m <= n
and
n <= len p
;
( (len s1) + m = n + 1 & ( for i being Nat st i < len s1 holds
s1 . (i + 1) = p . (m + i) ) & (len s2) + m = n + 1 & ( for i being Nat st i < len s2 holds
s2 . (i + 1) = p . (m + i) ) implies s1 = s2 )assume that A4:
(len s1) + m = n + 1
and A5:
for
i being
Nat st
i < len s1 holds
s1 . (i + 1) = p . (m + i)
;
( (len s2) + m = n + 1 & ( for i being Nat st i < len s2 holds
s2 . (i + 1) = p . (m + i) ) implies s1 = s2 )assume that A6:
(len s2) + m = n + 1
and A7:
for
i being
Nat st
i < len s2 holds
s2 . (i + 1) = p . (m + i)
;
s1 = s2now ( len s1 = len s1 & len s2 = len s1 & ( for i being Nat st i in dom s1 holds
s1 . i = s2 . i ) )thus
len s1 = len s1
;
( len s2 = len s1 & ( for i being Nat st i in dom s1 holds
s1 . i = s2 . i ) )thus
len s2 = len s1
by A4, A6;
for i being Nat st i in dom s1 holds
s1 . i = s2 . ilet i be
Nat;
( i in dom s1 implies s1 . i = s2 . i )assume A8:
i in dom s1
;
s1 . i = s2 . iA9:
dom s1 = Seg (len s1)
by FINSEQ_1:def 3;
A10:
i <= len s1
by A8, FINSEQ_3:25;
0 + 1
<= i
by A9, A8, FINSEQ_1:1;
then consider k being
Nat such that
0 <= k
and A11:
k < len s1
and A12:
i = k + 1
by A10, Th1;
thus s1 . i =
p . (m + k)
by A5, A11, A12
.=
s2 . i
by A4, A6, A7, A11, A12
;
verum end; hence
s1 = s2
by FINSEQ_2:9;
verum
end;
thus
( ( not 1 <= m or not m <= n or not n <= len p ) & s1 = {} & s2 = {} implies s1 = s2 )
; verum