let R be domRing; :: thesis: for a being Element of R
for m being non zero Nat holds (rpoly (1,a)) `^ m is Ppoly of R
let a be Element of R; :: thesis: for m being non zero Nat holds (rpoly (1,a)) `^ m is Ppoly of R
let m be non zero Nat; :: thesis: (rpoly (1,a)) `^ m is Ppoly of R
defpred S<sub>1</sub>[ Nat] means (rpoly (1,a)) `^ $1 is Ppoly of R;
IA: S₁[1]

proof

(rpoly (1,a)) `^ 1 = rpoly (1,a) by POLYNOM5:16;
hence S₁[1] by RING_5:51; :: thesis: verum

end;

IS: now :: thesis: for j being Nat st 1 <= j & S₁[j] holds
S₁[j + 1]

let j be Nat; :: thesis: ( 1 <= j & S₁[j] implies S₁[j + 1] )
assume 1 <= j ; :: thesis: ( S₁[j] implies S₁[j + 1] )
assume IV: S₁[j] ; :: thesis: S₁[j + 1]
( (rpoly (1,a)) `^ (j + 1) = ((rpoly (1,a)) `^ j) *' (rpoly (1,a)) & rpoly (1,a) is Ppoly of R ) by POLYNOM5:19, RING_5:51;
hence S₁[j + 1] by IV, RING_5:52; :: thesis: verum

end;

for m being Nat st 1 <= m holds
S₁[m] from NAT_1:sch 8(IA, IS);
hence (rpoly (1,a)) `^ m is Ppoly of R by NAT_1:14; :: thesis: verum