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