let R be flat Ring; :: thesis: for p being Polynomial of R holds not p in [#] R

let p be Polynomial of R; :: thesis: not p in [#] R

let p be Polynomial of R; :: thesis: not p in [#] R

now :: thesis: not p in [#] R

hence
not p in [#] R
; :: thesis: verumassume A1:
p in [#] R
; :: thesis: contradiction

then reconsider a = p as Element of R ;

A2: the_rank_of p = the_rank_of (p . 0) by A1, Def10;

dom p = NAT by FUNCT_2:def 1;

then A3: [0,(p . 0)] in p by FUNCT_1:def 2;

the_rank_of (p . 0) in the_rank_of [0,(p . 0)] by CLASSES1:84;

hence contradiction by A2, A3, CLASSES1:68; :: thesis: verum

end;then reconsider a = p as Element of R ;

A2: the_rank_of p = the_rank_of (p . 0) by A1, Def10;

dom p = NAT by FUNCT_2:def 1;

then A3: [0,(p . 0)] in p by FUNCT_1:def 2;

the_rank_of (p . 0) in the_rank_of [0,(p . 0)] by CLASSES1:84;

hence contradiction by A2, A3, CLASSES1:68; :: thesis: verum