defpred S_{1}[ Nat] means ( not (rpoly (1,a)) `^ R is zero & (rpoly (1,a)) `^ R is monic );

(rpoly (1,a)) `^ 0 = 1_. R by POLYNOM5:15;

then IA: S_{1}[ 0 ]
;

_{1}[k]
from NAT_1:sch 2(IA, IS);

hence ( not (rpoly (1,a)) `^ k is zero & (rpoly (1,a)) `^ k is monic ) ; :: thesis: verum

(rpoly (1,a)) `^ 0 = 1_. R by POLYNOM5:15;

then IA: S

IS: now :: thesis: for k being Nat st S_{1}[k] holds

S_{1}[k + 1]

for k being Nat holds SS

let k be Nat; :: thesis: ( S_{1}[k] implies S_{1}[k + 1] )

assume S_{1}[k]
; :: thesis: S_{1}[k + 1]

then ((rpoly (1,a)) `^ k) *' (rpoly (1,a)) is monic ;

hence S_{1}[k + 1]
by POLYNOM5:19; :: thesis: verum

end;assume S

then ((rpoly (1,a)) `^ k) *' (rpoly (1,a)) is monic ;

hence S

hence ( not (rpoly (1,a)) `^ k is zero & (rpoly (1,a)) `^ k is monic ) ; :: thesis: verum