let n be Nat; :: thesis: for fp being FinSequence of INT st len fp = n + 2 holds
for a being Integer ex fr being FinSequence of INT ex r being Integer st
( 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) )

let fp be FinSequence of INT ; :: thesis: ( len fp = n + 2 implies for a being Integer ex fr being FinSequence of INT ex r being Integer st
( 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) ) )

assume A1: len fp = n + 2 ; :: thesis: for a being Integer ex fr being FinSequence of INT ex r being Integer st
( 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) )

(n + 1) + 1 in Seg ((n + 1) + 1) by FINSEQ_1:4;
then n + 2 in dom fp by ;
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: ex fr being FinSequence of INT ex r being Integer st
( 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) )

defpred S1[ 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 S1[d,x,y]
proof
let d be Nat; :: thesis: ( 1 <= d & d < n1 implies for x being Element of INT ex y being Element of INT st S1[d,x,y] )
assume that
1 <= d and
d < n1 ; :: thesis: for x being Element of INT ex y being Element of INT st S1[d,x,y]
let x be Element of INT ; :: thesis: ex y being Element of INT st S1[d,x,y]
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: S1[d,x,y]
thus S1[d,x,y] ; :: thesis: verum
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
S1[d,p . d,p . (d + 1)] ) ) from take fr = Rev p; :: thesis: ex r being Integer st
( 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) )

take r = (fp . 1) + (a * (fr . 1)); :: thesis: ( 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) )
A4: len fr = n + 1 by ;
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: (Poly-INT fp) . x = ((x - a) * ((Poly-INT fr) . x)) + r
deffunc H1( Nat) -> set = (fr . \$1) * (x |^ \$1);
deffunc H2( 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 ;
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 ;
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 = H1(d) ) ) from A12: for d being Nat st d in dom f4 holds
f4 . d in INT
proof
let d be Nat; :: thesis: ( d in dom f4 implies f4 . d in INT )
reconsider d1 = d as Element of NAT by ORDINAL1:def 12;
assume d in dom f4 ; :: thesis: f4 . d in INT
then f4 . d1 = (fr . d1) * (x |^ d1) by A11;
hence f4 . d in INT by INT_1:def 2; :: thesis: verum
end;
f4 <> {} by A11;
then n + 1 in dom f4 by ;
then f4 . (n + 1) = (fr . (n + 1)) * (x |^ (n + 1)) by A11;
then A13: f4 . (n + 1) = (fp . (n + 2)) * (x |^ (n + 1)) by ;
reconsider f4 = f4 as FinSequence of INT by ;
consider f5 being FinSequence such that
A14: ( len f5 = n + 1 & ( for d being Nat st d in dom f5 holds
f5 . d = H2(d) ) ) from A15: for d being Nat st d in dom f5 holds
f5 . d in INT
proof
let d be Nat; :: thesis: ( d in dom f5 implies f5 . d in INT )
assume d in dom f5 ; :: thesis: f5 . d in INT
then f5 . d = (a * (fr . d)) * (x |^ (d -' 1)) by A14;
hence f5 . d in INT by INT_1:def 2; :: thesis: verum
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 ;
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 ;
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: ( k in dom ((x - a) * f2) implies ((x - a) * f2) . k = ((fr . k) * (x |^ k)) - ((a * (fr . k)) * (x |^ (k -' 1))) )
assume A25: k in dom ((x - a) * f2) ; :: thesis: ((x - a) * f2) . k = ((fr . k) * (x |^ k)) - ((a * (fr . k)) * (x |^ (k -' 1)))
then A26: k >= 1 by FINSEQ_3:25;
A27: k in dom f2 by ;
thus ((x - a) * f2) . k = (x - a) * (f2 . k) by
.= (x - a) * ((fr . k) * (x |^ (k -' 1))) by
.= ((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 ; :: thesis: verum
end;
A28: dom ((x - a) * f2) = dom f5 by ;
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: ( d in dom ((x - a) * f2) implies ((x - a) * f2) . d = (f4 . d) - (f5 . d) )
assume A30: d in dom ((x - a) * f2) ; :: thesis: ((x - a) * f2) . d = (f4 . d) - (f5 . d)
then A31: f5 . d = (a * (fr . d)) * (x |^ (d -' 1)) by ;
f4 . d = (fr . d) * (x |^ d) by ;
hence ((x - a) * f2) . d = (f4 . d) - (f5 . d) by ; :: thesis: verum
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 ;
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: ( d in dom f6 implies f6 . d = f1 . (d + 1) )
A38: dom f6 c= dom p by ;
assume A39: d in dom f6 ; :: thesis: f6 . d = f1 . (d + 1)
then A40: d in Seg n by ;
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 ;
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 ;
then A44: p . (d9 + 1) = (fp . ((n + 2) - d9)) + (a * (p . d9)) by ;
d < n + 1 by ;
then A45: d + 1 in Seg (n + 1) by FINSEQ_3:11;
then A46: d + 1 in dom f5 by ;
d + 0 < n + 2 by ;
then d + 1 in Seg (n + 2) by FINSEQ_3:11;
then A47: d + 1 in dom f1 by ;
A48: d + 1 in dom p by ;
thus f6 . d = (f4 . d) - (f5 . (d + 1)) by
.= ((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
.= ((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
.= ((p . (((n - d) + 1) + 1)) - (a * (p . (((n + 1) - (d + 1)) + 1)))) * (x |^ d) by
.= (fp . (d + 1)) * (x |^ ((d + 1) -' 1)) by
.= f1 . (d + 1) by ; :: thesis: verum
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: ( d in dom f1 implies f1 . d = ((<*(f1 . 1)*> ^ f6) ^ <*(f1 . (n + 2))*>) . d )
assume A50: d in dom f1 ; :: thesis: f1 . d = ((<*(f1 . 1)*> ^ f6) ^ <*(f1 . (n + 2))*>) . d
then A51: d >= 1 by FINSEQ_3:25;
A52: d <= n + 2 by ;
per cases ( d = 1 or ( d > 1 & d < n + 2 ) or d = n + 2 ) by ;
suppose A53: d = 1 ; :: thesis: f1 . d = ((<*(f1 . 1)*> ^ f6) ^ <*(f1 . (n + 2))*>) . d
hence ((<*(f1 . 1)*> ^ f6) ^ <*(f1 . (n + 2))*>) . d = (<*(f1 . 1)*> ^ (f6 ^ <*(f1 . (n + 2))*>)) . 1 by FINSEQ_1:32
.= f1 . d by ;
:: thesis: verum
end;
suppose A54: ( d > 1 & d < n + 2 ) ; :: thesis: f1 . d = ((<*(f1 . 1)*> ^ f6) ^ <*(f1 . (n + 2))*>) . d
then reconsider w = d - 1 as Element of NAT by INT_1:3;
d - 1 < (n + 2) - 1 by ;
then A55: d - 1 <= (n + 1) - 1 by INT_1:7;
d - 1 >= 0 + 1 by ;
then w in Seg n by ;
then A56: w in dom f6 by ;
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
.= f6 . w by
.= f1 . (w + 1) by
.= f1 . d ; :: thesis: verum
end;
suppose A58: d = n + 2 ; :: thesis: f1 . d = ((<*(f1 . 1)*> ^ f6) ^ <*(f1 . (n + 2))*>) . d
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
.= f1 . d by ; :: thesis: verum
end;
end;
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 ; :: thesis: verum
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 ;
hence (Poly-INT fp) . x = ((x - a) * ((Poly-INT fr) . x)) + r by A7; :: thesis: verum
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 ; :: thesis: verum