let R be Ring; :: thesis: for p being Polynomial of R holds p <> [1,2]
let p be Polynomial of R; :: thesis: p <> [1,2]
A1: dom p = NAT by FUNCT_2:def 1;

now :: thesis: not p = [1,2]

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

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

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

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 ( 1 = {3} or 2 = {3} ) by A3, A4;

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

hence contradiction ; :: thesis: verum

end;

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

per cases then ( 3 = 0 or 3 = 1 ) ;

suppose 3 = 0 ; :: thesis: contradiction

hence contradiction ; :: thesis: verum

end;

suppose 3 = 1 ; :: thesis: contradiction

hence contradiction ; :: thesis: verum

end;

end;

end;

end;

end;

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

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;
3 in {3} by TARSKI:def 1;
hence contradiction by A10, TARSKI:def 1; :: thesis: verum

end;

end;

end;

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