let it1, it2 be Polynomial of L; :: thesis: ( ( for i being Nat holds it1 . i = p . (n + i) ) & ( for i being Nat holds it2 . i = p . (n + i) ) implies it1 = it2 )
assume that
A4: for i being Nat holds it1 . i = p . (n + i) and
A5: for i being Nat holds it2 . i = p . (n + i) ; :: thesis: it1 = it2

now :: thesis: for x being object st x in NAT holds
it1 . x = it2 . x

let x be object ; :: thesis: ( x in NAT implies it1 . x = it2 . x )
assume x in NAT ; :: thesis: it1 . x = it2 . x
then reconsider i = x as Element of NAT ;
thus it1 . x = p . (n + i) by A4
.= it2 . x by A5 ; :: thesis: verum

end;

hence it1 = it2 by FUNCT_2:12; :: thesis: verum