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

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

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

hence not p in [#] R ; :: thesis: verum