let n be Nat; :: thesis: for O being Ordinal
for R being non trivial right_complementable add-associative right_zeroed right_unital distributive doubleLoopStr
for p being Polynomial of O,R holds p `^ (n + 1) = (p `^ n) *' p
let O be Ordinal; :: thesis: for R being non trivial right_complementable add-associative right_zeroed right_unital distributive doubleLoopStr
for p being Polynomial of O,R holds p `^ (n + 1) = (p `^ n) *' p
let R be non trivial right_complementable add-associative right_zeroed right_unital distributive doubleLoopStr ; :: thesis: for p being Polynomial of O,R holds p `^ (n + 1) = (p `^ n) *' p
let p be Polynomial of O,R; :: thesis: p `^ (n + 1) = (p `^ n) *' p
set PR = Polynom-Ring (O,R);
reconsider P = p as Element of (Polynom-Ring (O,R)) by POLYNOM1:def 11;
thus p `^ (n + 1) = ((power (Polynom-Ring (O,R))) . (P,n)) * P by GROUP_1:def 7
.= (p `^ n) *' p by POLYNOM1:def 11 ; :: thesis: verum