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);
(p `^ i) *' (p `^ 0 ) = (p `^ i) *' (1_. L) by POLYNOM5:16
.= p `^ (i + 0 ) by POLYNOM3:36 ;
then A1: S₁[ 0 ] ;
A2: 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 A3: S₁[j] ; :: thesis: S₁[j + 1]
(p `^ i) *' (p `^ (j + 1)) = (p `^ i) *' ((p `^ j) *' p) by POLYNOM5:20
.= (p `^ (i + j)) *' p by A3, POLYNOM3:34
.= p `^ ((i + j) + 1) by POLYNOM5:20
.= p `^ (i + (j + 1)) ;
hence S₁[j + 1] ; :: thesis: verum

end;

for j being Element of NAT holds S₁[j] from NAT_1:sch 1(A1, A2);
hence (p `^ i) *' (p `^ j) = p `^ (i + j) ; :: thesis: verum