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 S1[ Element of NAT ] means degree (BRoots (<%(- x),(1. L)%> `^ $1)) = $1;
A1:
len (1_. L) = 1
by POLYNOM4:7;
<%(- x),(1. L)%> `^ 0 = 1_. L
by POLYNOM5:16;
then A2:
S1[ 0 ]
by A1, Th59;
A3:
for n being Element of NAT st S1[n] holds
S1[n + 1]
proof
let n be
Element of
NAT ;
:: thesis: ( S1[n] implies S1[n + 1] )
assume A4:
S1[
n]
;
:: thesis: S1[n + 1]
A5:
(
card {x} = 1 &
support ({x},1 -bag ) = {x} )
by Th10, CARD_1:50;
<%(- x),(1. L)%> `^ (n + 1) = (<%(- x),(1. L)%> `^ n) *' <%(- x),(1. L)%>
by POLYNOM5:20;
then 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 A4, Th56
;
hence
S1[
n + 1]
by A5, Th15;
:: thesis: verum
end;
thus
for n being Element of NAT holds S1[n]
from NAT_1:sch 1(A2, A3); :: thesis: verum