let p1, p2 be FinSequence; :: thesis: ( ( n <= len f & len p1 = (len f) - n & ( for m being Nat st m in dom p1 holds
p1 . m = f . (m + n) ) & len p2 = (len f) - n & ( for m being Nat st m in dom p2 holds
p2 . m = f . (m + n) ) implies p1 = p2 ) & ( not n <= len f & p1 = {} & p2 = {} implies p1 = p2 ) )
thus ( n <= len f & len p1 = (len f) - n & ( for m being Nat st m in dom p1 holds
p1 . m = f . (m + n) ) & len p2 = (len f) - n & ( for m being Nat st m in dom p2 holds
p2 . m = f . (m + n) ) implies p1 = p2 ) :: thesis: ( not n <= len f & p1 = {} & p2 = {} implies p1 = p2 )

proof

assume that
n <= len f and
A2: len p1 = (len f) - n and
A3: for m being Nat st m in dom p1 holds
p1 . m = f . (m + n) and
A4: len p2 = (len f) - n and
A5: for m being Nat st m in dom p2 holds
p2 . m = f . (m + n) ; :: thesis: p1 = p2
A6: ( dom p1 = Seg (len p1) & Seg (len p2) = dom p2 ) by FINSEQ_1:def 3;

now :: thesis: for m being Nat st m in dom p1 holds
p1 . m = p2 . m

let m be Nat; :: thesis: ( m in dom p1 implies p1 . m = p2 . m )
assume A7: m in dom p1 ; :: thesis: p1 . m = p2 . m
then p1 . m = f . (m + n) by A3;
hence p1 . m = p2 . m by A2, A4, A5, A6, A7; :: thesis: verum

end;

hence p1 = p2 by A2, A4, FINSEQ_2:9; :: thesis: verum

end;

thus ( not n <= len f & p1 = {} & p2 = {} implies p1 = p2 ) ; :: thesis: verum