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

proof

let n be 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, Th51 ;
card {x} = 1 by CARD_1:30;
hence S₁[n + 1] by A3, Th10; :: thesis: verum

end;

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