let L be non empty right_complementable distributive add-associative right_zeroed doubleLoopStr ; for p being Polynomial of L
for F being FinSequence of (Polynom-Ring L) st p = Sum F holds
for i being Element of NAT holds p . i = Sum (Coeff (F,i))
let p be Polynomial of L; for F being FinSequence of (Polynom-Ring L) st p = Sum F holds
for i being Element of NAT holds p . i = Sum (Coeff (F,i))
let F be FinSequence of (Polynom-Ring L); ( p = Sum F implies for i being Element of NAT holds p . i = Sum (Coeff (F,i)) )
assume A1:
p = Sum F
; for i being Element of NAT holds p . i = Sum (Coeff (F,i))
defpred S1[ Nat] means for p being Polynomial of L
for F being FinSequence of (Polynom-Ring L) st p = Sum F & len F = $1 holds
for i being Element of NAT holds p . i = Sum (Coeff (F,i));
let i be Element of NAT ; p . i = Sum (Coeff (F,i))
A2:
ex m being Nat st len F = m
;
A3:
now for k being Nat st S1[k] holds
S1[k + 1]let k be
Nat;
( S1[k] implies S1[k + 1] )assume A4:
S1[
k]
;
S1[k + 1]now for p being Polynomial of L
for F being FinSequence of (Polynom-Ring L) st p = Sum F & len F = k + 1 holds
for i being Element of NAT holds p . i = Sum (Coeff (F,i))let p be
Polynomial of
L;
for F being FinSequence of (Polynom-Ring L) st p = Sum F & len F = k + 1 holds
for i being Element of NAT holds p . i = Sum (Coeff (F,i))let F be
FinSequence of
(Polynom-Ring L);
( p = Sum F & len F = k + 1 implies for i being Element of NAT holds p . i = Sum (Coeff (F,i)) )assume that A5:
p = Sum F
and A6:
len F = k + 1
;
for i being Element of NAT holds p . i = Sum (Coeff (F,i))reconsider rf =
F /. (k + 1) as
Polynomial of
L by POLYNOM3:def 10;
let i be
Element of
NAT ;
p . i = Sum (Coeff (F,i))set G =
F | (Seg k);
reconsider G =
F | (Seg k) as
FinSequence by FINSEQ_1:15;
reconsider G =
G as
FinSequence of
(Polynom-Ring L) by A6, Lm1;
A7:
len G = k
by A6, Lm1;
A8:
k <= len F
by A6, NAT_1:13;
A9:
now for j being Nat st j in dom (Coeff (F,i)) holds
(Coeff (F,i)) . j = ((Coeff (G,i)) ^ <*(rf . i)*>) . jA10:
dom (Coeff (G,i)) =
Seg (len (Coeff (G,i)))
by FINSEQ_1:def 3
.=
Seg (len G)
by Def1
.=
dom G
by FINSEQ_1:def 3
;
let j be
Nat;
( j in dom (Coeff (F,i)) implies (Coeff (F,i)) . b1 = ((Coeff (G,i)) ^ <*(rf . i)*>) . b1 )assume A11:
j in dom (Coeff (F,i))
;
(Coeff (F,i)) . b1 = ((Coeff (G,i)) ^ <*(rf . i)*>) . b1per cases
( j in dom (Coeff (G,i)) or not j in dom (Coeff (G,i)) )
;
suppose A12:
j in dom (Coeff (G,i))
;
(Coeff (F,i)) . b1 = ((Coeff (G,i)) ^ <*(rf . i)*>) . b1then A13:
((Coeff (G,i)) ^ <*(rf . i)*>) . j = (Coeff (G,i)) . j
by FINSEQ_1:def 7;
A14:
ex
p being
Polynomial of
L st
(
p = F . j &
(Coeff (F,i)) . j = p . i )
by A11, Def1;
ex
p1 being
Polynomial of
L st
(
p1 = G . j &
(Coeff (G,i)) . j = p1 . i )
by A12, Def1;
hence
(Coeff (F,i)) . j = ((Coeff (G,i)) ^ <*(rf . i)*>) . j
by A10, A12, A13, A14, FUNCT_1:47;
verum end; suppose A15:
not
j in dom (Coeff (G,i))
;
(Coeff (F,i)) . b1 = ((Coeff (G,i)) ^ <*(rf . i)*>) . b1A16:
dom (Coeff (F,i)) =
Seg (len (Coeff (F,i)))
by FINSEQ_1:def 3
.=
Seg (len F)
by Def1
;
then A17:
1
<= j
by A11, FINSEQ_1:1;
A18:
now not j < k + 1end;
j <= k + 1
by A6, A11, A16, FINSEQ_1:1;
then A19:
j = k + 1
by A18, XXREAL_0:1;
dom <*(rf . i)*> = {1}
by FINSEQ_1:2, FINSEQ_1:38;
then A20:
1
in dom <*(rf . i)*>
by TARSKI:def 1;
1
<= k + 1
by NAT_1:11;
then A21:
k + 1
in dom F
by A6, FINSEQ_3:25;
A22:
ex
p being
Polynomial of
L st
(
p = F . j &
(Coeff (F,i)) . j = p . i )
by A11, Def1;
len (Coeff (G,i)) = k
by A7, Def1;
then ((Coeff (G,i)) ^ <*(rf . i)*>) . j =
<*(rf . i)*> . 1
by A19, A20, FINSEQ_1:def 7
.=
rf . i
by FINSEQ_1:40
;
hence
(Coeff (F,i)) . j = ((Coeff (G,i)) ^ <*(rf . i)*>) . j
by A19, A22, A21, PARTFUN1:def 6;
verum end; end; len ((Coeff (G,i)) ^ <*(rf . i)*>) =
(len (Coeff (G,i))) + (len <*(rf . i)*>)
by FINSEQ_1:22
.=
(len (Coeff (G,i))) + 1
by FINSEQ_1:39
.=
k + 1
by A7, Def1
.=
len (Coeff (F,i))
by A6, Def1
;
then dom (Coeff (F,i)) =
Seg (len ((Coeff (G,i)) ^ <*(rf . i)*>))
by FINSEQ_1:def 3
.=
dom ((Coeff (G,i)) ^ <*(rf . i)*>)
by FINSEQ_1:def 3
;
then A23:
Coeff (
F,
i)
= (Coeff (G,i)) ^ <*(rf . i)*>
by A9, FINSEQ_1:13;
reconsider pg =
Sum G as
Polynomial of
L by POLYNOM3:def 10;
F = G ^ <*(F /. (k + 1))*>
by A6, Lm1;
then Sum F =
(Sum G) + (Sum <*(F /. (k + 1))*>)
by RLVECT_1:41
.=
(Sum G) + (F /. (k + 1))
by RLVECT_1:44
.=
pg + rf
by POLYNOM3:def 10
;
hence p . i =
(pg . i) + (rf . i)
by A5, NORMSP_1:def 2
.=
(Sum (Coeff (G,i))) + (rf . i)
by A4, A7
.=
(Sum (Coeff (G,i))) + (Sum <*(rf . i)*>)
by RLVECT_1:44
.=
Sum (Coeff (F,i))
by A23, RLVECT_1:41
;
verum end; hence
S1[
k + 1]
;
verum end;
now for p being Polynomial of L
for F being FinSequence of (Polynom-Ring L) st p = Sum F & len F = 0 holds
for i being Element of NAT holds p . i = Sum (Coeff (F,i))let p be
Polynomial of
L;
for F being FinSequence of (Polynom-Ring L) st p = Sum F & len F = 0 holds
for i being Element of NAT holds p . i = Sum (Coeff (F,i))let F be
FinSequence of
(Polynom-Ring L);
( p = Sum F & len F = 0 implies for i being Element of NAT holds p . i = Sum (Coeff (F,i)) )assume that A24:
p = Sum F
and A25:
len F = 0
;
for i being Element of NAT holds p . i = Sum (Coeff (F,i))let i be
Element of
NAT ;
p . i = Sum (Coeff (F,i))
F = <*> the
carrier of
(Polynom-Ring L)
by A25;
then
Sum F = 0. (Polynom-Ring L)
by RLVECT_1:43;
then
p = 0_. L
by A24, POLYNOM3:def 10;
then A26:
p . i = 0. L
;
len (Coeff (F,i)) = 0
by A25, Def1;
then
Coeff (
F,
i)
= <*> the
carrier of
L
;
hence
p . i = Sum (Coeff (F,i))
by A26, RLVECT_1:43;
verum end;
then A27:
S1[ 0 ]
;
for k being Nat holds S1[k]
from NAT_1:sch 2(A27, A3);
hence
p . i = Sum (Coeff (F,i))
by A1, A2; verum