let L be non empty right_complementable distributive add-associative right_zeroed doubleLoopStr ; :: thesis: 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; :: thesis: 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); :: thesis: ( p = Sum F implies for i being Element of NAT holds p . i = Sum (Coeff (F,i)) )
assume A1: p = Sum F ; :: thesis: for i being Element of NAT holds p . i = Sum (Coeff (F,i))
defpred S₁[ 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 ; :: thesis: p . i = Sum (Coeff (F,i))
A2: ex m being Nat st len F = m ;

A3: now :: thesis: for k being Nat st S₁[k] holds
S₁[k + 1]

let k be Nat; :: thesis: ( S₁[k] implies S₁[k + 1] )
assume A4: S₁[k] ; :: thesis: S₁[k + 1]

now :: thesis: 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; :: thesis: 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); :: thesis: ( 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 ; :: thesis: 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 ; :: thesis: 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 :: thesis: for j being Nat st j in dom (Coeff (F,i)) holds
(Coeff (F,i)) . j = ((Coeff (G,i)) ^ <*(rf . i)*>) . j

A10: 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; :: thesis: ( j in dom (Coeff (F,i)) implies (Coeff (F,i)) . b₁ = ((Coeff (G,i)) ^ <*(rf . i)*>) . b₁ )
assume A11: j in dom (Coeff (F,i)) ; :: thesis: (Coeff (F,i)) . b₁ = ((Coeff (G,i)) ^ <*(rf . i)*>) . b₁

per cases ( j in dom (Coeff (G,i)) or not j in dom (Coeff (G,i)) ) ;

suppose A12: j in dom (Coeff (G,i)) ; :: thesis: (Coeff (F,i)) . b₁ = ((Coeff (G,i)) ^ <*(rf . i)*>) . b₁

then 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; :: thesis: verum

end;

suppose A15: not j in dom (Coeff (G,i)) ; :: thesis: (Coeff (F,i)) . b₁ = ((Coeff (G,i)) ^ <*(rf . i)*>) . b₁

A16: 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 :: thesis: not j < k + 1

assume j < k + 1 ; :: thesis: contradiction
then j <= k by NAT_1:13;
then j in Seg k by A17;
hence contradiction by A8, A10, A15, FINSEQ_1:17; :: thesis: verum

end;

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 ;
hence (Coeff (F,i)) . j = ((Coeff (G,i)) ^ <*(rf . i)*>) . j by A19, A22, A21, PARTFUN1:def 6; :: thesis: verum

end;

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 ;
:: thesis: verum

end;

hence S₁[k + 1] ; :: thesis: verum

end;

now :: thesis: 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; :: thesis: 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); :: thesis: ( 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 ; :: thesis: for i being Element of NAT holds p . i = Sum (Coeff (F,i))
let i be Element of NAT ; :: thesis: 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; :: thesis: verum

end;

then A27: S₁[ 0 ] ;
for k being Nat holds S₁[k] from NAT_1:sch 2(A27, A3);
hence p . i = Sum (Coeff (F,i)) by A1, A2; :: thesis: verum