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;

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]

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

then A2: p = {{1,2},{1}} by TARSKI:def 5;

end;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;

end;

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;

end;A4: {3} in {{3,(p . 3)},{3}} by TARSKI:def 2;