let L be non empty right_complementable Abelian add-associative right_zeroed well-unital distributive commutative doubleLoopStr ; :: thesis: for p being Polynomial of L
for n being Nat holds p `^ (n + 1) = (p `^ n) *' p
let p be Polynomial of L; :: thesis: for n being Nat holds p `^ (n + 1) = (p `^ n) *' p
let n be Nat; :: thesis: p `^ (n + 1) = (p `^ n) *' p
reconsider nn = n as Element of NAT by ORDINAL1:def 12;
reconsider p1 = p as Element of (Polynom-Ring L) by POLYNOM3:def 10;
thus p `^ (n + 1) = ((power (Polynom-Ring L)) . (p1,nn)) * p1 by GROUP_1:def 7
.= (p `^ n) *' p by POLYNOM3:def 10 ; :: thesis: verum