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 ) )

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 )

thus
( ( not 1 <= m or not m <= n or not n <= len p ) & s1 = {} & s2 = {} implies s1 = s2 )
; :: thesis: verumassume 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

end;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 ) )

hence
s1 = s2
by FINSEQ_2:9; :: thesis: verums1 . 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;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