let O be Ordinal; :: thesis: for L being non trivial right_complementable Abelian add-associative right_zeroed well-unital distributive doubleLoopStr
for p being Polynomial of O,L
for x being Function of O,L
for P being FinSequence of (Polynom-Ring (O,L)) st p = Sum P holds
for E being FinSequence of L st len E = len P & ( for s being Polynomial of O,L
for i being Nat st i in dom E & s = P . i holds
E . i = eval (s,x) ) holds
eval (p,x) = Sum E
let L be non trivial right_complementable Abelian add-associative right_zeroed well-unital distributive doubleLoopStr ; :: thesis: for p being Polynomial of O,L
for x being Function of O,L
for P being FinSequence of (Polynom-Ring (O,L)) st p = Sum P holds
for E being FinSequence of L st len E = len P & ( for s being Polynomial of O,L
for i being Nat st i in dom E & s = P . i holds
E . i = eval (s,x) ) holds
eval (p,x) = Sum E
let p be Polynomial of O,L; :: thesis: for x being Function of O,L
for P being FinSequence of (Polynom-Ring (O,L)) st p = Sum P holds
for E being FinSequence of L st len E = len P & ( for s being Polynomial of O,L
for i being Nat st i in dom E & s = P . i holds
E . i = eval (s,x) ) holds
eval (p,x) = Sum E
let x be Function of O,L; :: thesis: for P being FinSequence of (Polynom-Ring (O,L)) st p = Sum P holds
for E being FinSequence of L st len E = len P & ( for s being Polynomial of O,L
for i being Nat st i in dom E & s = P . i holds
E . i = eval (s,x) ) holds
eval (p,x) = Sum E
set PR = Polynom-Ring (O,L);
let P be FinSequence of (Polynom-Ring (O,L)); :: thesis: ( p = Sum P implies for E being FinSequence of L st len E = len P & ( for s being Polynomial of O,L
for i being Nat st i in dom E & s = P . i holds
E . i = eval (s,x) ) holds
eval (p,x) = Sum E )
assume A1: p = Sum P ; :: thesis: for E being FinSequence of L st len E = len P & ( for s being Polynomial of O,L
for i being Nat st i in dom E & s = P . i holds
E . i = eval (s,x) ) holds
eval (p,x) = Sum E
let E be FinSequence of the carrier of L; :: thesis: ( len E = len P & ( for s being Polynomial of O,L
for i being Nat st i in dom E & s = P . i holds
E . i = eval (s,x) ) implies eval (p,x) = Sum E )
assume A2: ( len E = len P & ( for s being Polynomial of O,L
for i being Nat st i in dom E & s = P . i holds
E . i = eval (s,x) ) ) ; :: thesis: eval (p,x) = Sum E
defpred S₁[ Nat] means for i being Nat st $1 = i & i <= len P holds
for q being Polynomial of O,L st q = Sum (P | i) holds
Sum (E | i) = eval (q,x);
A3: S₁[ 0 ]

proof

let i be Nat; :: thesis: ( 0 = i & i <= len P implies for q being Polynomial of O,L st q = Sum (P | i) holds
Sum (E | i) = eval (q,x) )
assume A4: ( 0 = i & i <= len P ) ; :: thesis: for q being Polynomial of O,L st q = Sum (P | i) holds
Sum (E | i) = eval (q,x)
let q be Polynomial of O,L; :: thesis: ( q = Sum (P | i) implies Sum (E | i) = eval (q,x) )
assume A5: q = Sum (P | i) ; :: thesis: Sum (E | i) = eval (q,x)
P | i = <*> the carrier of (Polynom-Ring (O,L)) by A4;
then q = 0. (Polynom-Ring (O,L)) by A5, RLVECT_1:43
.= 0_ (O,L) by POLYNOM1:def 11 ;
then A6: eval (q,x) = 0. L by POLYNOM2:20;
E | 0 = <*> the carrier of L ;
hence Sum (E | i) = eval (q,x) by A4, A6, RLVECT_1:43; :: thesis: verum

end;

A7: for n being Nat st S₁[n] holds
S₁[n + 1]

proof

let n be Nat; :: thesis: ( S₁[n] implies S₁[n + 1] )
assume A8: S₁[n] ; :: thesis: S₁[n + 1]
let n1 be Nat; :: thesis: ( n + 1 = n1 & n1 <= len P implies for q being Polynomial of O,L st q = Sum (P | n1) holds
Sum (E | n1) = eval (q,x) )
assume A9: ( n1 = n + 1 & n1 <= len P ) ; :: thesis: for q being Polynomial of O,L st q = Sum (P | n1) holds
Sum (E | n1) = eval (q,x)
let q be Polynomial of O,L; :: thesis: ( q = Sum (P | n1) implies Sum (E | n1) = eval (q,x) )
assume A10: q = Sum (P | n1) ; :: thesis: Sum (E | n1) = eval (q,x)
reconsider q1 = Sum (P | n), Pn1 = P /. n1 as Polynomial of O,L by POLYNOM1:def 11;
A11: ( n1 in dom P & n1 in dom E ) by A2, A9, FINSEQ_3:25, NAT_1:11;
then A12: ( P | n1 = (P | n) ^ <*(P . n1)*> & P . n1 = P /. n1 & E | n1 = (E | n) ^ <*(E . n1)*> ) by A9, FINSEQ_5:10, PARTFUN1:def 6;
then A13: q = (Sum (P | n)) + (Sum <*(P /. n1)*>) by A10, RLVECT_1:41
.= (Sum (P | n)) + (P /. n1) by RLVECT_1:44
.= q1 + Pn1 by POLYNOM1:def 11 ;
A14: n < len P by NAT_1:13, A9;
E . n1 = eval (Pn1,x) by A11, A12, A2;
hence Sum (E | n1) = (Sum (E | n)) + (Sum <*(eval (Pn1,x))*>) by A12, RLVECT_1:41
.= (Sum (E | n)) + (eval (Pn1,x)) by RLVECT_1:44
.= (eval (q1,x)) + (eval (Pn1,x)) by A14, A8
.= eval (q,x) by A13, POLYNOM2:23 ;
:: thesis: verum

end;

A15: P | (len P) = P ;
for n being Nat holds S₁[n] from NAT_1:sch 2(A3, A7);
then Sum (E | (len E)) = eval (p,x) by A1, A2, A15;
hence eval (p,x) = Sum E ; :: thesis: verum