let L be domRing; :: thesis: for x being Element of L
for n being Element of NAT holds degree (BRoots (<%(- x),(1. L)%> `^ n)) = n
let x be Element of L; :: thesis: for n being Element of NAT holds degree (BRoots (<%(- x),(1. L)%> `^ n)) = n
set r = <%(- x),(1. L)%>;
defpred S₁[ Element of NAT ] means degree (BRoots (<%(- x),(1. L)%> `^ $1)) = $1;
A1: for n being Element of NAT st S₁[n] holds
S₁[n + 1]

proof

let n be Element of NAT ; :: thesis: ( S₁[n] implies S₁[n + 1] )
assume A2: S₁[n] ; :: thesis: S₁[n + 1]
<%(- x),(1. L)%> `^ (n + 1) = (<%(- x),(1. L)%> `^ n) *' <%(- x),(1. L)%> by POLYNOM5:19;
then A3: degree (BRoots (<%(- x),(1. L)%> `^ (n + 1))) = (degree (BRoots (<%(- x),(1. L)%> `^ n))) + (degree (BRoots <%(- x),(1. L)%>)) by Lm2
.= n + (degree (({x},1) -bag)) by A2, Th56 ;
card {x} = 1 by CARD_1:30;
hence S₁[n + 1] by A3, Th15; :: thesis: verum

end;

( len (1_. L) = 1 & <%(- x),(1. L)%> `^ 0 = 1_. L ) by POLYNOM4:4, POLYNOM5:15;
then A4: S₁[ 0 ] by Th59;
thus for n being Element of NAT holds S₁[n] from NAT_1:sch 1(A4, A1); :: thesis: verum