let R be Ring; :: thesis:
let p be Polynomial of R; :: thesis:
A1: dom p = NAT by FUNCT_2:def 1;

now :: thesis:

assume p = [1,2] ; :: thesis:
then A2: p = {{1,2},{1}} by TARSKI:def 5;

per cases = {1,2} or [3,(p . 3)] = {1} ) by A2, A1;

suppose [3,(p . 3)] = {1,2} ; :: thesis:

then A3: {{3,(p . 3)},{3}} = {1,2} by TARSKI:def 5;
A4: {3} in {{3,(p . 3)},{3}} by TARSKI:def 2;

per cases by A3, A4, TARSKI:def 2;

suppose A5: 1 = {3} ; :: thesis:

3 in {3} by TARSKI:def 1;
hence contradiction by A5, CARD_1:49, TARSKI:def 1; :: thesis:

end;

suppose A7: 2 = {3} ; :: thesis:

A8: 3 in {3} by TARSKI:def 1;

per cases by A7, A8, CARD_1:50, TARSKI:def 2;

suppose 3 = 0 ; :: thesis:

hence contradiction ; :: thesis:

end;

suppose 3 = 1 ; :: thesis:

hence contradiction ; :: thesis:

end;

end;

end;

end;

end;

suppose [3,(p . 3)] = {1} ; :: thesis:

then A9: {{3,(p . 3)},{3}} = {1} by TARSKI:def 5;
{3} in {{3,(p . 3)},{3}} by TARSKI:def 2;
then A10: {3} = {0} by A9, TARSKI:def 1, CARD_1:49;
3 in {3} by TARSKI:def 1;
hence contradiction by A10, TARSKI:def 1; :: thesis:

end;

end;

end;

hence p <> [1,2] ; :: thesis: