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)
let i be Element of NAT ; :: thesis: 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);

now

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 A2: ( p = Sum F & 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 A2, FINSEQ_1:32;
then Sum F = 0. (Polynom-Ring L) by RLVECT_1:60;
then p = 0_. L by A2, POLYNOM3:def 12;
then A3: p . i = 0. L by FUNCOP_1:13;
len (Coeff F,i) = 0 by A2, Def1;
then Coeff F,i = <*> the carrier of L by FINSEQ_1:32;
hence p . i = Sum (Coeff F,i) by A3, RLVECT_1:60; :: thesis: verum

end;

then A4: S₁[ 0 ] ;

A5: now

let k be Element of NAT ; :: thesis: ( S₁[k] implies S₁[k + 1] )
assume A6: S₁[k] ; :: thesis: S₁[k + 1]

now

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 A7: ( p = Sum F & len F = k + 1 ) ; :: 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)
set G = F | (Seg k);
reconsider G = F | (Seg k) as FinSequence by FINSEQ_1:19;
reconsider G = G as FinSequence of (Polynom-Ring L) by A7, Lm1;
reconsider pg = Sum G as Polynomial of L by POLYNOM3:def 12;
reconsider rf = F /. (k + 1) as Polynomial of L by POLYNOM3:def 12;
A8: len G = k by A7, Lm1;
A9: k <= len F by A7, NAT_1:13;
A10: F = G ^ <*(F /. (k + 1))*> by A7, Lm1;
len ((Coeff G,i) ^ <*(rf . i)*>) = (len (Coeff G,i)) + (len <*(rf . i)*>) by FINSEQ_1:35
.= (len (Coeff G,i)) + 1 by FINSEQ_1:56
.= k + 1 by A8, Def1
.= len (Coeff F,i) by A7, Def1 ;
then A11: 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 ;

now

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

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

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

then A15: ((Coeff G,i) ^ <*(rf . i)*>) . j = (Coeff G,i) . j by FINSEQ_1:def 7;
consider p1 being Polynomial of L such that
A16: ( p1 = G . j & (Coeff G,i) . j = p1 . i ) by A14, Def1;
consider p being Polynomial of L such that
A17: ( p = F . j & (Coeff F,i) . j = p . i ) by A12, Def1;
thus (Coeff F,i) . j = ((Coeff G,i) ^ <*(rf . i)*>) . j by A13, A14, A15, A16, A17, FUNCT_1:70; :: thesis: verum

end;

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

A19: j = k + 1

proof

dom (Coeff F,i) = Seg (len (Coeff F,i)) by FINSEQ_1:def 3
.= Seg (len F) by Def1 ;
then A20: ( 1 <= j & j <= k + 1 ) by A7, A12, FINSEQ_1:3;

now

assume j < k + 1 ; :: thesis: contradiction
then j <= k by NAT_1:13;
then j in Seg k by A12, A20;
hence contradiction by A9, A13, A18, FINSEQ_1:21; :: thesis: verum

end;

hence j = k + 1 by A20, XXREAL_0:1; :: thesis: verum

end;

A21: len (Coeff G,i) = k by A8, Def1;
dom <*(rf . i)*> = {1} by FINSEQ_1:4, FINSEQ_1:55;
then 1 in dom <*(rf . i)*> by TARSKI:def 1;
then A22: ((Coeff G,i) ^ <*(rf . i)*>) . j = <*(rf . i)*> . 1 by A19, A21, FINSEQ_1:def 7
.= rf . i by FINSEQ_1:57 ;
consider p being Polynomial of L such that
A23: ( p = F . j & (Coeff F,i) . j = p . i ) by A12, Def1;
1 <= k + 1 by NAT_1:11;
then k + 1 in dom F by A7, FINSEQ_3:27;
hence (Coeff F,i) . j = ((Coeff G,i) ^ <*(rf . i)*>) . j by A19, A22, A23, PARTFUN1:def 8; :: thesis: verum

end;

end;

end;

then A24: Coeff F,i = (Coeff G,i) ^ <*(rf . i)*> by A11, FINSEQ_1:17;
Sum F = (Sum G) + (Sum <*(F /. (k + 1))*>) by A10, RLVECT_1:58
.= (Sum G) + (F /. (k + 1)) by RLVECT_1:61
.= pg + rf by POLYNOM3:def 12 ;
hence p . i = (pg . i) + (rf . i) by A7, NORMSP_1:def 5
.= (Sum (Coeff G,i)) + (rf . i) by A6, A8
.= (Sum (Coeff G,i)) + (Sum <*(rf . i)*>) by RLVECT_1:61
.= Sum (Coeff F,i) by A24, RLVECT_1:58 ;
:: thesis: verum

end;

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

end;

A25: for k being Element of NAT holds S₁[k] from NAT_1:sch 1(A4, A5);
consider m being Nat such that
A26: len F = m ;
thus p . i = Sum (Coeff F,i) by A1, A25, A26; :: thesis: verum