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 `^ 2 = p *' p
let p be Polynomial of L; :: thesis: p `^ 2 = p *' p
reconsider p1 = p as Element of (Polynom-Ring L) by POLYNOM3:def 12;
thus p `^ 2 = (power (Polynom-Ring L)) . p1,(1 + 1)
.= ((power (Polynom-Ring L)) . p1,(0 + 1)) * p1 by GROUP_1:def 8
.= (((power (Polynom-Ring L)) . p1,0 ) * p1) * p1 by GROUP_1:def 8
.= ((1_ (Polynom-Ring L)) * p1) * p1 by GROUP_1:def 8
.= p1 * p1 by GROUP_1:def 5
.= p *' p by POLYNOM3:def 12 ; :: thesis: verum