let L be comRing; :: thesis: for i, j being Element of NAT
for p being Polynomial of L holds (p `^ i) *' (p `^ j) = p `^ (i + j)
let i, j be Element of NAT ; :: thesis: for p being Polynomial of L holds (p `^ i) *' (p `^ j) = p `^ (i + j)
let p be Polynomial of L; :: thesis: (p `^ i) *' (p `^ j) = p `^ (i + j)
defpred S<sub>1</sub>[ Element of NAT ] means (p `^ i) *' (p `^ $1) = p `^ (i + $1);
A1: for j being Element of NAT st S₁[j] holds
S₁[j + 1]

proof

let j be Element of NAT ; :: thesis: ( S₁[j] implies S₁[j + 1] )
assume A2: S₁[j] ; :: thesis: S₁[j + 1]
(p `^ i) *' (p `^ (j + 1)) = (p `^ i) *' ((p `^ j) *' p) by POLYNOM5:19
.= (p `^ (i + j)) *' p by A2, POLYNOM3:33
.= p `^ ((i + j) + 1) by POLYNOM5:19
.= p `^ (i + (j + 1)) ;
hence S₁[j + 1] ; :: thesis: verum

end;

(p `^ i) *' (p `^ 0) = (p `^ i) *' (1_. L) by POLYNOM5:15
.= p `^ (i + 0) by POLYNOM3:35 ;
then A3: S₁[ 0 ] ;
for j being Element of NAT holds S₁[j] from NAT_1:sch 1(A3, A1);
hence (p `^ i) *' (p `^ j) = p `^ (i + j) ; :: thesis: verum