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

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

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