let s1, s2 be FinSequence; :: thesis: ( ( 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 :: thesis: ( ( 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 ; :: thesis: ( (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) ; :: thesis: ( (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) ; :: thesis: s1 = s2

now :: thesis: ( 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 ; :: thesis: ( 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; :: thesis: for i being Nat st i in dom s1 holds
s1 . i = s2 . i
let i be Nat; :: thesis: ( i in dom s1 implies s1 . i = s2 . i )
assume A8: i in dom s1 ; :: thesis: s1 . i = s2 . i
A9: 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 ; :: thesis: verum

end;

hence s1 = s2 by FINSEQ_2:9; :: thesis: verum

end;

thus ( ( not 1 <= m or not m <= n or not n <= len p ) & s1 = {} & s2 = {} implies s1 = s2 ) ; :: thesis: verum