let F be Field; :: thesis: for p being Polynomial of F
for i, j being Element of NAT holds p `^ (i + j) = (p `^ i) *' (p `^ j)
let p be Polynomial of F; :: thesis: for i, j being Element of NAT holds p `^ (i + j) = (p `^ i) *' (p `^ j)
let i, j be Element of NAT ; :: thesis: p `^ (i + j) = (p `^ i) *' (p `^ j)
set G = Polynom-Ring F;
reconsider p1 = p as Element of (Polynom-Ring F) by POLYNOM3:def 10;
A: ( p `^ i = (power (Polynom-Ring F)) . (p1,i) & p `^ j = (power (Polynom-Ring F)) . (p1,j) ) by POLYNOM5:def 3;
thus p `^ (i + j) = (power (Polynom-Ring F)) . (p1,(i + j)) by POLYNOM5:def 3
.= p1 |^ (i + j) by BINOM:def 2
.= (p1 |^ i) * (p1 |^ j) by BINOM:10
.= ((power (Polynom-Ring F)) . (p1,i)) * (p1 |^ j) by BINOM:def 2
.= ((power (Polynom-Ring F)) . (p1,i)) * ((power (Polynom-Ring F)) . (p1,j)) by BINOM:def 2
.= (p `^ i) *' (p `^ j) by A, POLYNOM3:def 10 ; :: thesis: verum