let L be non empty right_complementable Abelian add-associative right_zeroed commutative well-unital distributive doubleLoopStr ; :: thesis: for p being Polynomial of L holds p `^ 0 = 1_. L
let p be Polynomial of L; :: thesis: p `^ 0 = 1_. L
reconsider p1 = p as Element of (Polynom-Ring L) by POLYNOM3:def 12;
thus p `^ 0 = (power (Polynom-Ring L)) . (p1,0)
.= 1_ (Polynom-Ring L) by GROUP_1:def 8
.= 1_. L by POLYNOM3:37 ; :: thesis: verum