let n be Nat; :: thesis:
let fp be FinSequence of INT ; :: thesis:
assume A1: len fp = n + 2 ; :: thesis:
(n + 1) + 1 in Seg ((n + 1) + 1) by FINSEQ_1:4;
then n + 2 in dom fp by A1, FINSEQ_1:def 3;
then reconsider A = fp . (n + 2) as Element of INT by FINSEQ_2:11;
reconsider n1 = n + 1 as Element of NAT ;
let a be Integer; :: thesis:
defpred S₁[ Nat, Integer, set ] means $3 = (fp . ((n + 2) - $1)) + (a * $2);
A2: for d being Nat st 1 <= d & d < n1 holds
for x being Element of INT ex y being Element of INT st S₁[d,x,y]

proof

let d be Nat; :: thesis:
assume that
1 <= d and
d < n1 ; :: thesis:
let x be Element of INT ; :: thesis:
set y = (fp . ((n + 2) - d)) + (a * x);
reconsider y = (fp . ((n + 2) - d)) + (a * x) as Element of INT by INT_1:def 2;
take y ; :: thesis:
thus S₁[d,x,y] ; :: thesis:

end;

consider p being FinSequence of INT such that
A3: ( len p = n1 & ( p . 1 = A or n1 = 0 ) & ( for d being Nat st 1 <= d & d < n1 holds
S₁[d,p . d,p . (d + 1)] ) ) from RECDEF_1:sch 4(A2);
take fr = Rev p; :: thesis:
take r = (fp . 1) + (a * (fr . 1)); :: thesis:
A4: len fr = n + 1 by A3, FINSEQ_5:def 3;
for x being Element of INT holds (Poly-INT fp) . x = ((x - a) * ((Poly-INT fr) . x)) + r

proof

let x be Element of INT ; :: thesis:
deffunc H₁( Nat) -> set = (fr . $1) * (x |^ $1);
deffunc H₂( Nat) -> set = (a * (fr . $1)) * (x |^ ($1 -' 1));
consider f1 being FinSequence of INT such that
A5: len f1 = len fp and
A6: for d being Nat st d in dom f1 holds
f1 . d = (fp . d) * (x |^ (d -' 1)) and
A7: (Poly-INT fp) . x = Sum f1 by Def1;
A8: f1 <> {} by A1, A5;
then n + 2 in dom f1 by A1, A5, FINSEQ_5:6;
then f1 . (n + 2) = (fp . (n + 2)) * (x |^ (((n + 1) + 1) -' 1)) by A6;
then A9: f1 . (n + 2) = (fp . (n + 2)) * (x |^ (n + 1)) by NAT_D:34;
f1 . 1 = (fp . 1) * (x |^ (1 -' 1)) by A6, A8, FINSEQ_5:6;
then f1 . 1 = (fp . 1) * (x |^ 0) by XREAL_1:232;
then A10: f1 . 1 = (fp . 1) * 1 by NEWTON:4;
reconsider n = n as Element of NAT by ORDINAL1:def 12;
consider f4 being FinSequence such that
A11: ( len f4 = n + 1 & ( for d being Nat st d in dom f4 holds
f4 . d = H₁(d) ) ) from FINSEQ_1:sch 2();
A12: for d being Nat st d in dom f4 holds
f4 . d in INT

proof

let d be Nat; :: thesis:
reconsider d1 = d as Element of NAT by ORDINAL1:def 12;
assume d in dom f4 ; :: thesis:
then f4 . d1 = (fr . d1) * (x |^ d1) by A11;
hence f4 . d in INT by INT_1:def 2; :: thesis:

end;

f4 <> {} by A11;
then n + 1 in dom f4 by A11, FINSEQ_5:6;
then f4 . (n + 1) = (fr . (n + 1)) * (x |^ (n + 1)) by A11;
then A13: f4 . (n + 1) = (fp . (n + 2)) * (x |^ (n + 1)) by A3, FINSEQ_5:62;
reconsider f4 = f4 as FinSequence of INT by A12, FINSEQ_2:12;
consider f5 being FinSequence such that
A14: ( len f5 = n + 1 & ( for d being Nat st d in dom f5 holds
f5 . d = H₂(d) ) ) from FINSEQ_1:sch 2();
A15: for d being Nat st d in dom f5 holds
f5 . d in INT

proof

let d be Nat; :: thesis:
assume d in dom f5 ; :: thesis:
then f5 . d = (a * (fr . d)) * (x |^ (d -' 1)) by A14;
hence f5 . d in INT by INT_1:def 2; :: thesis:

end;

f5 <> {} by A14;
then 1 in dom f5 by FINSEQ_5:6;
then f5 . 1 = (a * (fr . 1)) * (x |^ (1 -' 1)) by A14;
then f5 . 1 = (a * (fr . 1)) * (x |^ 0) by XREAL_1:232;
then A16: f5 . 1 = (a * (fr . 1)) * 1 by NEWTON:4;
reconsider f5 = f5 as FinSequence of INT by A15, FINSEQ_2:12;
A17: f4 is FinSequence of REAL by FINSEQ_3:117;
consider f2 being FinSequence of INT such that
A18: len f2 = len fr and
A19: for d being Nat st d in dom f2 holds
f2 . d = (fr . d) * (x |^ (d -' 1)) and
A20: (Poly-INT fr) . x = Sum f2 by Def1;
set f3 = (x - a) * f2;
A21: dom ((x - a) * f2) = dom f2 by VALUED_1:def 5;
then A22: len ((x - a) * f2) = len f2 by FINSEQ_3:29;
A23: dom ((x - a) * f2) = dom f4 by A4, A18, A11, A21, FINSEQ_3:29;
A24: for k being Element of NAT st k in dom ((x - a) * f2) holds
((x - a) * f2) . k = ((fr . k) * (x |^ k)) - ((a * (fr . k)) * (x |^ (k -' 1)))

proof

let k be Element of NAT ; :: thesis:
assume A25: k in dom ((x - a) * f2) ; :: thesis:
then A26: k >= 1 by FINSEQ_3:25;
A27: k in dom f2 by A25, VALUED_1:def 5;
thus ((x - a) * f2) . k = (x - a) * (f2 . k) by A25, VALUED_1:def 5
.= (x - a) * ((fr . k) * (x |^ (k -' 1))) by A19, A27
.= ((fr . k) * ((x |^ (k -' 1)) * x)) - ((a * (fr . k)) * (x |^ (k -' 1)))
.= ((fr . k) * (x |^ ((k -' 1) + 1))) - ((a * (fr . k)) * (x |^ (k -' 1))) by NEWTON:6
.= ((fr . k) * (x |^ k)) - ((a * (fr . k)) * (x |^ (k -' 1))) by A26, XREAL_1:235 ; :: thesis:

end;

A28: dom ((x - a) * f2) = dom f5 by A4, A18, A14, A21, FINSEQ_3:29;
A29: for d being Nat st d in dom ((x - a) * f2) holds
((x - a) * f2) . d = (f4 . d) - (f5 . d)

proof

let d be Nat; :: thesis:
assume A30: d in dom ((x - a) * f2) ; :: thesis:
then A31: f5 . d = (a * (fr . d)) * (x |^ (d -' 1)) by A14, A28;
f4 . d = (fr . d) * (x |^ d) by A11, A23, A30;
hence ((x - a) * f2) . d = (f4 . d) - (f5 . d) by A24, A30, A31; :: thesis:

end;

f5 is FinSequence of REAL by FINSEQ_3:117;
then consider f6 being FinSequence of REAL such that
A32: len f6 = (len ((x - a) * f2)) - 1 and
A33: for d being Nat st d in dom f6 holds
f6 . d = (f4 . d) - (f5 . (d + 1)) and
A34: Sum ((x - a) * f2) = ((Sum f6) + (f4 . (n + 1))) - (f5 . 1) by A4, A18, A11, A14, A22, A29, A17, Th5;
A35: len f6 <= len ((x - a) * f2) by A4, A18, A22, A32, XREAL_1:145;
then A36: dom f6 c= dom ((x - a) * f2) by FINSEQ_3:30;
A37: for d being Element of NAT st d in dom f6 holds
f6 . d = f1 . (d + 1)

proof

let d be Element of NAT ; :: thesis:
A38: dom f6 c= dom p by A3, A4, A18, A22, A35, FINSEQ_3:30;
assume A39: d in dom f6 ; :: thesis:
then A40: d in Seg n by A4, A18, A22, A32, FINSEQ_1:def 3;
then A41: d <= n by FINSEQ_1:1;
then A42: n - d >= 0 by XREAL_1:48;
then reconsider d9 = (n - d) + 1 as Element of NAT by INT_1:3;
d >= 1 by A40, FINSEQ_1:1;
then n - d <= n - 1 by XREAL_1:10;
then d9 <= (n - 1) + 1 by XREAL_1:6;
then A43: d9 < n + 1 by XREAL_1:145;
d9 >= 0 + 1 by A42, XREAL_1:6;
then A44: p . (d9 + 1) = (fp . ((n + 2) - d9)) + (a * (p . d9)) by A3, A43;
d < n + 1 by A41, XREAL_1:145;
then A45: d + 1 in Seg (n + 1) by FINSEQ_3:11;
then A46: d + 1 in dom f5 by A14, FINSEQ_1:def 3;
d + 0 < n + 2 by A41, XREAL_1:8;
then d + 1 in Seg (n + 2) by FINSEQ_3:11;
then A47: d + 1 in dom f1 by A1, A5, FINSEQ_1:def 3;
A48: d + 1 in dom p by A3, A45, FINSEQ_1:def 3;
thus f6 . d = (f4 . d) - (f5 . (d + 1)) by A33, A39
.= ((fr . d) * (x |^ d)) - (f5 . (d + 1)) by A11, A23, A36, A39
.= ((fr . d) * (x |^ d)) - ((a * (fr . (d + 1))) * (x |^ ((d + 1) -' 1))) by A14, A46
.= ((fr . d) * (x |^ d)) - ((a * (fr . (d + 1))) * (x |^ d)) by NAT_D:34
.= ((fr . d) - (a * (fr . (d + 1)))) * (x |^ d)
.= ((p . (((n + 1) - d) + 1)) - (a * (fr . (d + 1)))) * (x |^ d) by A3, A39, A38, FINSEQ_5:58
.= ((p . (((n - d) + 1) + 1)) - (a * (p . (((n + 1) - (d + 1)) + 1)))) * (x |^ d) by A3, A48, FINSEQ_5:58
.= (fp . (d + 1)) * (x |^ ((d + 1) -' 1)) by A44, NAT_D:34
.= f1 . (d + 1) by A6, A47 ; :: thesis:

end;

f1 = (<*(f1 . 1)*> ^ f6) ^ <*(f1 . (n + 2))*>

proof

set K = (<*(f1 . 1)*> ^ f6) ^ <*(f1 . (n + 2))*>;
A49: for d being Nat st d in dom f1 holds
f1 . d = ((<*(f1 . 1)*> ^ f6) ^ <*(f1 . (n + 2))*>) . d

proof

let d be Nat; :: thesis:
assume A50: d in dom f1 ; :: thesis:
then A51: d >= 1 by FINSEQ_3:25;
A52: d <= n + 2 by A1, A5, A50, FINSEQ_3:25;

per cases by A51, A52, XXREAL_0:1;

suppose A53: d = 1 ; :: thesis:

hence ((<*(f1 . 1)*> ^ f6) ^ <*(f1 . (n + 2))*>) . d = (<*(f1 . 1)*> ^ (f6 ^ <*(f1 . (n + 2))*>)) . 1 by FINSEQ_1:32
.= f1 . d by A53, FINSEQ_1:41 ;
:: thesis:

end;

suppose A54: ( d > 1 & d < n + 2 ) ; :: thesis:

then reconsider w = d - 1 as Element of NAT by INT_1:3;
d - 1 < (n + 2) - 1 by A54, XREAL_1:9;
then A55: d - 1 <= (n + 1) - 1 by INT_1:7;
d - 1 >= 0 + 1 by A54, INT_1:7, XREAL_1:50;
then w in Seg n by A55, FINSEQ_1:1;
then A56: w in dom f6 by A4, A18, A22, A32, FINSEQ_1:def 3;
then A57: w in dom (f6 ^ <*(f1 . (n + 2))*>) by FINSEQ_2:15;
thus ((<*(f1 . 1)*> ^ f6) ^ <*(f1 . (n + 2))*>) . d = (<*(f1 . 1)*> ^ (f6 ^ <*(f1 . (n + 2))*>)) . (w + 1) by FINSEQ_1:32
.= (f6 ^ <*(f1 . (n + 2))*>) . w by A57, FINSEQ_3:103
.= f6 . w by A56, FINSEQ_1:def 7
.= f1 . (w + 1) by A37, A56
.= f1 . d ; :: thesis:

end;

suppose A58: d = n + 2 ; :: thesis:

set K1 = <*(f1 . 1)*> ^ f6;
thus ((<*(f1 . 1)*> ^ f6) ^ <*(f1 . (n + 2))*>) . d = ((<*(f1 . 1)*> ^ f6) ^ <*(f1 . (n + 2))*>) . ((n + 1) + 1) by A58
.= ((<*(f1 . 1)*> ^ f6) ^ <*(f1 . (n + 2))*>) . ((len (<*(f1 . 1)*> ^ f6)) + 1) by A4, A18, A22, A32, FINSEQ_5:8
.= f1 . d by A58, FINSEQ_1:42 ; :: thesis:

end;

len ((<*(f1 . 1)*> ^ f6) ^ <*(f1 . (n + 2))*>) = len (<*(f1 . 1)*> ^ (f6 ^ <*(f1 . (n + 2))*>)) by FINSEQ_1:32
.= 1 + (len (f6 ^ <*(f1 . (n + 2))*>)) by FINSEQ_5:8
.= (1 + (len f6)) + 1 by FINSEQ_2:16
.= len f1 by A1, A4, A5, A18, A22, A32 ;
hence f1 = (<*(f1 . 1)*> ^ f6) ^ <*(f1 . (n + 2))*> by A49, FINSEQ_3:29; :: thesis:

end;

then Sum f1 = Sum (<*(f1 . 1)*> ^ (f6 ^ <*(f1 . (n + 2))*>)) by FINSEQ_1:32
.= (f1 . 1) + (Sum (f6 ^ <*(f1 . (n + 2))*>)) by RVSUM_1:76
.= (f1 . 1) + ((Sum f6) + (f1 . (n + 2))) by RVSUM_1:74
.= (Sum ((x - a) * f2)) + r by A10, A9, A13, A16, A34
.= ((x - a) * ((Poly-INT fr) . x)) + r by A20, RVSUM_1:87 ;
hence (Poly-INT fp) . x = ((x - a) * ((Poly-INT fr) . x)) + r by A7; :: thesis:

end;

hence ( len fr = n + 1 & ( for x being Element of INT holds (Poly-INT fp) . x = ((x - a) * ((Poly-INT fr) . x)) + r ) & fp . (n + 2) = fr . (n + 1) ) by A3, FINSEQ_5:62, FINSEQ_5:def 3; :: thesis: