defpred S₁[ Nat] means ( not (rpoly (n,a)) `^ R is constant & (rpoly (n,a)) `^ R is monic & (rpoly (n,a)) `^ R is with_roots );
IA: S₁[1] by POLYNOM5:16;

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

let k be Nat; :: thesis: ( 1 <= k & S₁[k] implies S₁[k + 1] )
assume 1 <= k ; :: thesis: ( S₁[k] implies S₁[k + 1] )
assume S₁[k] ; :: thesis: S₁[k + 1]
then ( not ((rpoly (n,a)) `^ k) *' (rpoly (n,a)) is constant & ((rpoly (n,a)) `^ k) *' (rpoly (n,a)) is monic & ((rpoly (n,a)) `^ k) *' (rpoly (n,a)) is with_roots ) ;
hence S₁[k + 1] by POLYNOM5:19; :: thesis: verum

end;

I: for k being Nat st 1 <= k holds
S₁[k] from NAT_1:sch 8(IA, IS);
1 <= k by NAT_1:53;
hence ( not (rpoly (n,a)) `^ k is constant & (rpoly (n,a)) `^ k is monic & (rpoly (n,a)) `^ k is with_roots ) by I; :: thesis: verum