let L be Field; :: thesis: for p, q being Polynomial of L
for x being Element of L holds eval ((Subst (p,q)),x) = eval (p,(eval (q,x)))
let p, q be Polynomial of L; :: thesis: for x being Element of L holds eval ((Subst (p,q)),x) = eval (p,(eval (q,x)))
let x be Element of L; :: thesis: eval ((Subst (p,q)),x) = eval (p,(eval (q,x)))
consider F1 being FinSequence of the carrier of L such that
A1: eval (p,(eval (q,x))) = Sum F1 and
A2: len F1 = len p and
A3: for n being Element of NAT st n in dom F1 holds
F1 . n = (p . (n -' 1)) * ((power L) . ((eval (q,x)),(n -' 1))) by POLYNOM4:def 2;
consider F being FinSequence of the carrier of (Polynom-Ring L) such that
A4: Subst (p,q) = Sum F and
A5: len F = len p and
A6: for n being Element of NAT st n in dom F holds
F . n = (p . (n -' 1)) * (q `^ (n -' 1)) by Def6;
defpred S₁[ Nat] means for r being Polynomial of L st r = Sum (F | $1) holds
eval (r,x) = Sum (F1 | $1);
A7: for n being Nat st S₁[n] holds
S₁[n + 1]

proof

let n be Nat; :: thesis: ( S₁[n] implies S₁[n + 1] )
reconsider nn = n as Element of NAT by ORDINAL1:def 12;
assume A8: for r being Polynomial of L st r = Sum (F | n) holds
eval (r,x) = Sum (F1 | n) ; :: thesis: S₁[n + 1]
let r be Polynomial of L; :: thesis: ( r = Sum (F | (n + 1)) implies eval (r,x) = Sum (F1 | (n + 1)) )
assume A9: r = Sum (F | (n + 1)) ; :: thesis: eval (r,x) = Sum (F1 | (n + 1))

per cases ( n + 1 <= len F or n + 1 > len F ) ;

suppose A10: n + 1 <= len F ; :: thesis: eval (r,x) = Sum (F1 | (n + 1))

then A11: F1 | (n + 1) = (F1 | n) ^ <*(F1 /. (n + 1))*> by A5, A2, FINSEQ_5:82;
F | (n + 1) = (F | n) ^ <*(F /. (n + 1))*> by A10, FINSEQ_5:82;
then A12: r = (Sum (F | n)) + (F /. (n + 1)) by A9, FVSUM_1:71;
reconsider r1 = Sum (F | n) as Polynomial of L by POLYNOM3:def 10;
n + 1 >= 1 by NAT_1:11;
then A13: n + 1 in dom F by A10, FINSEQ_3:25;
A14: dom F = dom F1 by A5, A2, FINSEQ_3:29;
then A15: (p . ((n + 1) -' 1)) * ((power L) . ((eval (q,x)),((n + 1) -' 1))) = F1 . (n + 1) by A3, A13
.= F1 /. (n + 1) by A13, A14, PARTFUN1:def 6 ;
F /. (n + 1) = F . (n + 1) by A13, PARTFUN1:def 6
.= (p . ((n + 1) -' 1)) * (q `^ ((n + 1) -' 1)) by A6, A13
.= (p . nn) * (q `^ ((n + 1) -' 1)) by NAT_D:34
.= (p . nn) * (q `^ n) by NAT_D:34 ;
then r = r1 + ((p . nn) * (q `^ n)) by A12, POLYNOM3:def 10;
hence eval (r,x) = (eval (r1,x)) + (eval (((p . nn) * (q `^ n)),x)) by POLYNOM4:19
.= (Sum (F1 | n)) + (eval (((p . nn) * (q `^ n)),x)) by A8
.= (Sum (F1 | n)) + ((p . nn) * (eval ((q `^ n),x))) by Th30
.= (Sum (F1 | n)) + ((p . nn) * ((power L) . ((eval (q,x)),n))) by Th22
.= (Sum (F1 | n)) + ((p . ((n + 1) -' 1)) * ((power L) . ((eval (q,x)),n))) by NAT_D:34
.= (Sum (F1 | n)) + (F1 /. (n + 1)) by A15, NAT_D:34
.= Sum (F1 | (n + 1)) by A11, FVSUM_1:71 ;
:: thesis: verum

end;

suppose A16: n + 1 > len F ; :: thesis: eval (r,x) = Sum (F1 | (n + 1))

then n >= len F by NAT_1:13;
then A17: ( F | n = F & F1 | n = F1 ) by A5, A2, FINSEQ_1:58;
( F | (n + 1) = F & F1 | (n + 1) = F1 ) by A5, A2, A16, FINSEQ_1:58;
hence eval (r,x) = Sum (F1 | (n + 1)) by A8, A9, A17; :: thesis: verum

end;

end;

end;

A18: ( F | (len F) = F & F1 | (len F1) = F1 ) by FINSEQ_1:58;
A19: S₁[ 0 ]

proof

let r be Polynomial of L; :: thesis: ( r = Sum (F | 0) implies eval (r,x) = Sum (F1 | 0) )
A20: F | 0 = <*> the carrier of (Polynom-Ring L) ;
A21: F1 | 0 = <*> the carrier of L ;
assume r = Sum (F | 0) ; :: thesis: eval (r,x) = Sum (F1 | 0)
then r = 0. (Polynom-Ring L) by A20, RLVECT_1:43
.= 0_. L by POLYNOM3:def 10 ;
hence eval (r,x) = 0. L by POLYNOM4:17
.= Sum (F1 | 0) by A21, RLVECT_1:43 ;
:: thesis: verum

end;

for n being Nat holds S₁[n] from NAT_1:sch 2(A19, A7);
hence eval ((Subst (p,q)),x) = eval (p,(eval (q,x))) by A4, A5, A1, A2, A18; :: thesis: verum