let R be non trivial right_complementable Abelian add-associative right_zeroed well-unital distributive associative doubleLoopStr ; :: thesis: for f being Polynomial of 0,R holds f is Constant
let f be Polynomial of 0,R; :: thesis: f is Constant
assume not f is Constant ; :: thesis: contradiction
then consider b being bag of 0 such that
A2: ( b <> EmptyBag 0 & f . b <> 0. R ) by POLYNOM7:def 7;
b = EmptyBag 0 ;
hence contradiction by A2; :: thesis: verum