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 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: 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 S_{1}[ 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_{1}[d,x,y]

A3: ( len p = n1 & ( p . 1 = A or n1 = 0 ) & ( for d being Nat st 1 <= d & d < n1 holds

S_{1}[d,p . d,p . (d + 1)] ) )
from RECDEF_1:sch 4(A2);

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 A3, FINSEQ_5:def 3;

for x being Element of INT holds (Poly-INT fp) . x = ((x - a) * ((Poly-INT fr) . x)) + r

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 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: 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 S

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

proof

consider p being FinSequence of INT such that
let d be Nat; :: thesis: ( 1 <= d & d < n1 implies for x being Element of INT ex y being Element of INT st S_{1}[d,x,y] )

assume that

1 <= d and

d < n1 ; :: thesis: for x being Element of INT ex y being Element of INT st S_{1}[d,x,y]

let x be Element of INT ; :: thesis: ex y being Element of INT st S_{1}[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: S_{1}[d,x,y]

thus S_{1}[d,x,y]
; :: thesis: verum

end;assume that

1 <= d and

d < n1 ; :: thesis: for x being Element of INT ex y being Element of INT st S

let x be Element of INT ; :: thesis: ex y being Element of INT st S

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: S

thus S

A3: ( len p = n1 & ( p . 1 = A or n1 = 0 ) & ( for d being Nat st 1 <= d & d < n1 holds

S

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 A3, FINSEQ_5:def 3;

for x being Element of INT holds (Poly-INT fp) . x = ((x - a) * ((Poly-INT fr) . x)) + r

proof

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: verum
let x be Element of INT ; :: thesis: (Poly-INT fp) . x = ((x - a) * ((Poly-INT fr) . x)) + r

deffunc H_{1}( Nat) -> set = (fr . $1) * (x |^ $1);

deffunc H_{2}( 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_{1}(d) ) )
from FINSEQ_1:sch 2();

A12: for d being Nat st d in dom f4 holds

f4 . d in INT

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_{2}(d) ) )
from FINSEQ_1:sch 2();

A15: for d being Nat st d in dom f5 holds

f5 . d in INT

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)))

A29: for d being Nat st d in dom ((x - a) * f2) holds

((x - a) * f2) . d = (f4 . d) - (f5 . d)

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)

.= (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: verum

end;deffunc H

deffunc H

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

A12: for d being Nat st d in dom f4 holds

f4 . d in INT

proof

f4 <> {}
by A11;
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;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

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

A15: for d being Nat st d in dom f5 holds

f5 . d in INT

proof

f5 <> {}
by A14;
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;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

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

A28:
dom ((x - a) * f2) = dom f5
by A4, A18, A14, A21, FINSEQ_3:29;
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 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: verum

end;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 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: verum

A29: for d being Nat st d in dom ((x - a) * f2) holds

((x - a) * f2) . d = (f4 . d) - (f5 . d)

proof

f5 is FinSequence of REAL
by FINSEQ_3:117;
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 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: verum

end;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 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: verum

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

f1 = (<*(f1 . 1)*> ^ f6) ^ <*(f1 . (n + 2))*>
let d be Element of NAT ; :: thesis: ( d in dom f6 implies f6 . d = f1 . (d + 1) )

A38: dom f6 c= dom p by A3, A4, A18, A22, A35, FINSEQ_3:30;

assume A39: d in dom f6 ; :: thesis: f6 . d = f1 . (d + 1)

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: verum

end;A38: dom f6 c= dom p by A3, A4, A18, A22, A35, FINSEQ_3:30;

assume A39: d in dom f6 ; :: thesis: f6 . d = f1 . (d + 1)

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: verum

proof

then Sum f1 =
Sum (<*(f1 . 1)*> ^ (f6 ^ <*(f1 . (n + 2))*>))
by FINSEQ_1:32
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

.= 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: verum

end;A49: for d being Nat st d in dom f1 holds

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

proof

len ((<*(f1 . 1)*> ^ f6) ^ <*(f1 . (n + 2))*>) =
len (<*(f1 . 1)*> ^ (f6 ^ <*(f1 . (n + 2))*>))
by FINSEQ_1:32
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 A1, A5, A50, FINSEQ_3:25;

end;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 A1, A5, A50, FINSEQ_3:25;

per cases
( d = 1 or ( d > 1 & d < n + 2 ) or d = n + 2 )
by A51, A52, XXREAL_0:1;

end;

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 A53, FINSEQ_1:41 ;

:: thesis: verum

end;.= f1 . d by A53, FINSEQ_1:41 ;

:: thesis: verum

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 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: verum

end;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: verum

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 A4, A18, A22, A32, FINSEQ_5:8

.= f1 . d by A58, FINSEQ_1:42 ; :: thesis: verum

end;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: verum

.= 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: verum

.= (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: verum