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 ( 1 <= m & m <= n & 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

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
X: dom s1 = Seg (len s1) by FINSEQ_1:def 3;
let i be Nat; :: thesis: ( i in dom s1 implies s1 . i = s2 . i )
assume i in dom s1 ; :: thesis: s1 . i = s2 . i
then ( 0 + 1 <= i & i <= len s1 ) by X, FINSEQ_1:3;
then consider k being Element of NAT such that
A8: ( 0 <= k & k < len s1 & i = k + 1 ) by Th1;
thus s1 . i = p . (m + k) by A5, A8
.= s2 . i by A4, A6, A7, A8 ; :: thesis: verum

end;

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

end;

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