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_{1}[ Nat] means degree (BRoots (<%(- x),(1. L)%> `^ $1)) = $1;

A1: for n being Nat st S_{1}[n] holds

S_{1}[n + 1]

then A4: S_{1}[ 0 ]
by Th54;

thus for n being Nat holds S_{1}[n]
from NAT_1:sch 2(A4, A1); :: thesis: verum

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

A1: for n being Nat st S

S

proof

( len (1_. L) = 1 & <%(- x),(1. L)%> `^ 0 = 1_. L )
by POLYNOM4:4, POLYNOM5:15;
let n be Nat; :: thesis: ( S_{1}[n] implies S_{1}[n + 1] )

assume A2: S_{1}[n]
; :: thesis: S_{1}[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_{1}[n + 1]
by A3, Th10; :: thesis: verum

end;assume A2: S

<%(- 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

then A4: S

thus for n being Nat holds S