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
( dom f = Bags 0 & Bags 0 = {{}} & rng f = {(f . (EmptyBag 0))} )
let f be Polynomial of 0,R; :: thesis: ( dom f = Bags 0 & Bags 0 = {{}} & rng f = {(f . (EmptyBag 0))} )
dom f = Bags 0 by FUNCT_2:def 1;
hence ( dom f = Bags 0 & Bags 0 = {{}} & rng f = {(f . (EmptyBag 0))} ) by Th15, FUNCT_1:4; :: thesis: verum