defpred S_{1}[ 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}[1]
by POLYNOM5:16;

S_{1}[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

IA: S

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

S_{1}[k + 1]

I:
for k being Nat st 1 <= k holds S

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

assume 1 <= k ; :: thesis: ( S_{1}[k] implies S_{1}[k + 1] )

assume S_{1}[k]
; :: thesis: S_{1}[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_{1}[k + 1]
by POLYNOM5:19; :: thesis: verum

end;assume 1 <= k ; :: thesis: ( S

assume S

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

S

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