let R be domRing; for F being non empty FinSequence of (Polynom-Ring R)
for p being Polynomial of R st p = Product F & ( for i being Nat st i in dom F holds
ex a being Element of R st F . i = rpoly (1,a) ) holds
deg p = len F
let F be non empty FinSequence of (Polynom-Ring R); for p being Polynomial of R st p = Product F & ( for i being Nat st i in dom F holds
ex a being Element of R st F . i = rpoly (1,a) ) holds
deg p = len F
let p be Polynomial of R; ( p = Product F & ( for i being Nat st i in dom F holds
ex a being Element of R st F . i = rpoly (1,a) ) implies deg p = len F )
assume AS:
( p = Product F & ( for i being Nat st i in dom F holds
ex a being Element of R st F . i = rpoly (1,a) ) )
; deg p = len F
defpred S1[ Nat] means for F being non empty FinSequence of (Polynom-Ring R)
for p being Polynomial of R st len F = $1 & p = Product F & ( for i being Nat st i in dom F holds
ex a being Element of R st F . i = rpoly (1,a) ) holds
deg p = len F;
IA:
S1[ 0 ]
;
IS:
now for k being Nat st S1[k] holds
S1[k + 1]let k be
Nat;
( S1[k] implies S1[b1 + 1] )assume IV:
S1[
k]
;
S1[b1 + 1]per cases
( k = 0 or k > 0 )
;
suppose S:
k = 0
;
S1[b1 + 1]hence
S1[
k + 1]
by S;
verum end; suppose S:
k > 0
;
S1[b1 + 1]now for F being non empty FinSequence of (Polynom-Ring R)
for p being Polynomial of R st len F = k + 1 & p = Product F & ( for i being Nat st i in dom F holds
ex a being Element of R st F . i = rpoly (1,a) ) holds
deg p = k + 1let F be non
empty FinSequence of
(Polynom-Ring R);
for p being Polynomial of R st len F = k + 1 & p = Product F & ( for i being Nat st i in dom F holds
ex a being Element of R st F . i = rpoly (1,a) ) holds
deg p = k + 1let p be
Polynomial of
R;
( len F = k + 1 & p = Product F & ( for i being Nat st i in dom F holds
ex a being Element of R st F . i = rpoly (1,a) ) implies deg p = k + 1 )assume A:
(
len F = k + 1 &
p = Product F & ( for
i being
Nat st
i in dom F holds
ex
a being
Element of
R st
F . i = rpoly (1,
a) ) )
;
deg p = k + 1consider G being
FinSequence,
y being
object such that B2:
F = G ^ <*y*>
by FINSEQ_1:46;
B2a:
rng G c= rng F
by B2, FINSEQ_1:29;
B2b:
rng F c= the
carrier of
(Polynom-Ring R)
by FINSEQ_1:def 4;
then reconsider G =
G as
FinSequence of
(Polynom-Ring R) by B2a, XBOOLE_1:1, FINSEQ_1:def 4;
reconsider q =
Product G as
Polynomial of
R by POLYNOM3:def 10;
B3:
len F =
(len G) + (len <*y*>)
by B2, FINSEQ_1:22
.=
(len G) + 1
by FINSEQ_1:39
;
then reconsider G =
G as non
empty FinSequence of
(Polynom-Ring R) by S, A;
C:
dom G c= dom F
by B2, FINSEQ_1:26;
then F:
deg q = k
by IV, B3, A;
rng <*y*> = {y}
by FINSEQ_1:39;
then G5:
y in rng <*y*>
by TARSKI:def 1;
rng <*y*> c= rng F
by B2, FINSEQ_1:30;
then reconsider y =
y as
Element of
(Polynom-Ring R) by G5, B2b;
dom <*y*> = {1}
by FINSEQ_1:2, FINSEQ_1:def 8;
then
1
in dom <*y*>
by TARSKI:def 1;
then B6:
F . (k + 1) =
<*y*> . 1
by B2, B3, A, FINSEQ_1:def 7
.=
y
by FINSEQ_1:def 8
;
dom F = Seg (k + 1)
by A, FINSEQ_1:def 3;
then consider a being
Element of
R such that B9:
y = rpoly (1,
a)
by A, B6, FINSEQ_1:4;
B10:
p =
(Product G) * y
by A, B2, GROUP_4:6
.=
q *' (rpoly (1,a))
by B9, POLYNOM3:def 10
;
(
q <> 0_. R &
rpoly (1,
a)
<> 0_. R )
by F, HURWITZ:20;
hence deg p =
(deg q) + (deg (rpoly (1,a)))
by B10, HURWITZ:23
.=
k + 1
by F, HURWITZ:27
;
verum end; hence
S1[
k + 1]
;
verum end; end; end;
I:
for k being Nat holds S1[k]
from NAT_1:sch 2(IA, IS);
thus
deg p = len F
by I, AS; verum