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 ex a being Element of R st f = a | (0,R)
let f be Polynomial of 0,R; :: thesis: ex a being Element of R st f = a | (0,R)
f is Constant by Th17;
hence ex a being Element of R st f = a | (0,R) by POLYNOM7:17; :: thesis: verum