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

let k be Element of NAT ; :: thesis: ( S₁[k] implies S₁[k + 1] )
assume A4: 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 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 12;
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 A6, Lm1;
A7: len G = k by A6, Lm1;
A8: k <= len F by A6, NAT_1:13;

A9: now

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:70; :: 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:3;

A18: now

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

end;

j <= k + 1 by A6, A11, A16, FINSEQ_1:3;
then A19: j = k + 1 by A18, XXREAL_0:1;
dom <*(rf . i)*> = {1} by FINSEQ_1:4, FINSEQ_1:55;
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:27;
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:57 ;
hence (Coeff F,i) . j = ((Coeff G,i) ^ <*(rf . i)*>) . j by A19, A22, A21, PARTFUN1:def 8; :: thesis: verum

end;

end;

end;

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 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:17;
reconsider pg = Sum G as Polynomial of L by POLYNOM3:def 12;
F = G ^ <*(F /. (k + 1))*> by A6, Lm1;
then Sum F = (Sum G) + (Sum <*(F /. (k + 1))*>) by 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 A5, NORMSP_1:def 5
.= (Sum (Coeff G,i)) + (rf . i) by A4, A7
.= (Sum (Coeff G,i)) + (Sum <*(rf . i)*>) by RLVECT_1:61
.= Sum (Coeff F,i) by A23, RLVECT_1:58 ;
:: thesis: verum

end;

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

end;

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 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:60;
then p = 0_. L by A24, POLYNOM3:def 12;
then A26: p . i = 0. L by FUNCOP_1:13;
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:60; :: thesis: verum

end;

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