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;

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

hence
it1 = it2
by A6; :: thesis: verumit1 . 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;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