let it1, it2 be FinSequence of (Polynom-Ring L); :: thesis: ( len it1 = n & ( for i being Element of NAT st i in dom it1 holds
it1 . i = <%(- c),(1. L)%> ) & len it2 = n & ( for i being Element of NAT st i in dom it2 holds
it2 . i = <%(- c),(1. L)%> ) implies it1 = it2 )
assume that
A2: len it1 = n and
A3: for i being Element of NAT st i in dom it1 holds
it1 . i = <%(- c),(1. L)%> and
A4: len it2 = n and
A5: for i being Element of NAT st i in dom it2 holds
it2 . i = <%(- c),(1. L)%> ; :: thesis: it1 = it2
A6: dom it1 = dom it2 by A2, A4, FINSEQ_3:29;

now :: thesis: for x being Nat st x in dom it1 holds
it1 . x = it2 . x

let x be Nat; :: thesis: ( x in dom it1 implies it1 . x = it2 . x )
assume A7: x in dom it1 ; :: thesis: it1 . x = it2 . x
hence it1 . x = <%(- c),(1. L)%> by A3
.= it2 . x by A5, A6, A7 ;
:: thesis: verum

end;

hence it1 = it2 by A6; :: thesis: verum