set f = Eval p;
set L = RealVectSpace REAL;
defpred S1[ Nat, object ] means c2 = FPower ((p . (p -' 1)),(p -' 1));
A1: now :: thesis: for n being Nat st n in Seg (len p) holds
ex x being Element of (RealVectSpace REAL) st S1[n,x]
let n be Nat; :: thesis: ( n in Seg (len p) implies ex x being Element of (RealVectSpace REAL) st S1[n,x] )
reconsider x = FPower ((p . (n -' 1)),(n -' 1)) as Element of (RealVectSpace REAL) by FUNCT_2:9;
assume n in Seg (len p) ; :: thesis: ex x being Element of (RealVectSpace REAL) st S1[n,x]
take x = x; :: thesis: S1[n,x]
thus S1[n,x] ; :: thesis: verum
end;
consider G being FinSequence of (RealVectSpace REAL) such that
A2: dom G = Seg (len p) and
A3: for n being Nat st n in Seg (len p) holds
S1[n,G . n] from FINSEQ_1:sch 5(A1);
 A4: G | (len G) = G by FINSEQ_1:58;
reconsider SF = Sum G as Function of REAL,REAL by FUNCT_2:66;
A5: now :: thesis: for x being Element of REAL holds (Eval p) . x = SF . x
let x be Element of REAL ; :: thesis: (Eval p) . x = SF . x
reconsider x1 = x as Element of F_Real ;
consider H being FinSequence of F_Real such that
A6: eval (p,x1) = Sum H and
A7: len H = len p and
A8: for n being Element of NAT st n in dom H holds
H . n = (p . (n -' 1)) * ((power F_Real) . (x1,(n -' 1))) by POLYNOM4:def 2;
defpred S2[ Nat] means for SFk being Function of REAL,REAL st SFk = Sum (G | p) holds
Sum (H | p) = SFk . x;
A9: len G = len p by A2, FINSEQ_1:def 3;
A10: for k being Nat st S2[k] holds
S2[k + 1]
proof
let k be Nat; :: thesis: ( S2[k] implies S2[k + 1] )
reconsider kk = k as Element of NAT by ORDINAL1:def 12;
assume A11: for SFk being Function of REAL,REAL st SFk = Sum (G | k) holds
Sum (H | k) = SFk . x ; :: thesis: S2[k + 1]
reconsider SFk1 = Sum (G | k) as Function of REAL,REAL by FUNCT_2:66;
let SFk be Function of REAL,REAL; :: thesis: ( SFk = Sum (G | (k + 1)) implies Sum (H | (k + 1)) = SFk . x )
assume A12: SFk = Sum (G | (k + 1)) ; :: thesis: Sum (H | (k + 1)) = SFk . x
per cases ( len G > k or len G <= k ) ;
suppose A13: len G > k ; :: thesis: Sum (H | (k + 1)) = SFk . x
reconsider g2 = FPower ((p . kk),k) as Function of REAL,REAL ;
A14: k + 1 >= 1 by NAT_1:11;
A15: k + 1 <= len G by A13, NAT_1:13;
then A16: k + 1 in dom G by NAT_1:11, FINSEQ_3:25;
then A17: G /. (k + 1) = G . (k + 1) by PARTFUN1:def 6
.= FPower ((p . ((k + 1) -' 1)),((k + 1) -' 1)) by A2, A3, A14, A15, FINSEQ_3:25
.= FPower ((p . kk),((k + 1) -' 1)) by NAT_D:34
.= FPower ((p . kk),k) by NAT_D:34 ;
G | (k + 1) = (G | k) ^ <*(G . (k + 1))*> by A13, FINSEQ_5:83
.= (G | k) ^ <*(G /. (k + 1))*> by A16, PARTFUN1:def 6 ;
then A18: SFk = (Sum (G | k)) + (G /. (k + 1)) by A12, FVSUM_1:71
.= SFk1 + g2 by A17, FUNCSDOM:28 ;
A19: Sum (H | k) = SFk1 . x by A11;
A20: dom G = dom H by A2, A7, FINSEQ_1:def 3;
then A21: H /. (k + 1) = H . (k + 1) by A16, PARTFUN1:def 6
.= (p . ((k + 1) -' 1)) * ((power F_Real) . (x1,((k + 1) -' 1))) by A8, A20, A16
.= (p . kk) * ((power F_Real) . (x1,((k + 1) -' 1))) by NAT_D:34
.= (p . kk) * (power (x1,k)) by NAT_D:34
.= (FPower ((p . kk),k)) . x by POLYNOM5:def 12 ;
H | (k + 1) = (H | k) ^ <*(H . (k + 1))*> by A7, A9, A13, FINSEQ_5:83
.= (H | k) ^ <*(H /. (k + 1))*> by A20, A16, PARTFUN1:def 6 ;
hence Sum (H | (k + 1)) = (Sum (H | k)) + (H /. (k + 1)) by FVSUM_1:71
.= SFk . x by A21, A18, A19, VALUED_1:1 ;
:: thesis: verum
end;
suppose A22: len G <= k ; :: thesis: Sum (H | (k + 1)) = SFk . x
k <= k + 1 by NAT_1:11;
then A23: ( G | (k + 1) = G & H | (k + 1) = H ) by A7, A9, A22, FINSEQ_1:58, XXREAL_0:2;
( G | k = G & H | k = H ) by A7, A9, A22, FINSEQ_1:58;
hence Sum (H | (k + 1)) = SFk . x by A11, A12, A23; :: thesis: verum
end;
end;
end;
A24: S2[ 0 ]
proof
let SFk be Function of REAL,REAL; :: thesis: ( SFk = Sum (G | 0) implies Sum (H | 0) = SFk . x )
A25: G | 0 = <*> the carrier of (RealVectSpace REAL) ;
assume SFk = Sum (G | 0) ; :: thesis: Sum (H | 0) = SFk . x
then A26: SFk = 0. (RealVectSpace REAL) by A25, RLVECT_1:43
.= REAL --> (In (0,REAL)) ;
H | 0 = <*> the carrier of F_Real ;
hence Sum (H | 0) = 0. F_Real by RLVECT_1:43
.= SFk . x by A26 ;
:: thesis: verum
end;
A27: for k being Nat holds S2[k] from NAT_1:sch 2(A24, A10);
A28: Sum (G | (len G)) = SF by FINSEQ_1:58;
thus (Eval p) . x = Sum H by A6, POLYNOM5:def 13
.= Sum (H | (len H)) by FINSEQ_1:58
.= SF . x by A7, A9, A27, A28 ; :: thesis: verum
end;
defpred S2[ Nat] means for g being PartFunc of REAL,REAL st g = Sum (G | p) holds
g is differentiable ;
A29: for k being Nat st S2[k] holds
S2[k + 1]
proof
let k be Nat; :: thesis: ( S2[k] implies S2[k + 1] )
reconsider kk = k as Element of NAT by ORDINAL1:def 12;
reconsider g1 = Sum (G | k) as Function of REAL,REAL by FUNCT_2:66;
assume A30: for g being PartFunc of REAL,REAL st g = Sum (G | k) holds
g is differentiable ; :: thesis: S2[k + 1]
then A31: g1 is differentiable ;
let g be PartFunc of REAL,REAL; :: thesis: ( g = Sum (G | (k + 1)) implies g is differentiable )
assume A32: g = Sum (G | (k + 1)) ; :: thesis: g is differentiable
per cases ( len G > k or len G <= k ) ;
suppose A33: len G > k ; :: thesis: g is differentiable
k + 1 <= len G by A33, NAT_1:13;
then A34: k + 1 in dom G by NAT_1:11, FINSEQ_3:25;
then A35: G /. (k + 1) = G . (k + 1) by PARTFUN1:def 6
.= FPower ((p . ((k + 1) -' 1)),((k + 1) -' 1)) by A2, A3, A34
.= FPower ((p . kk),((k + 1) -' 1)) by NAT_D:34
.= FPower ((p . kk),k) by NAT_D:34 ;
A36: FPower ((p . kk),k) is differentiable Function of REAL,REAL by Th42;
G | (k + 1) = (G | k) ^ <*(G . (k + 1))*> by A33, FINSEQ_5:83
.= (G | k) ^ <*(G /. (k + 1))*> by A34, PARTFUN1:def 6 ;
then g = (Sum (G | k)) + (G /. (k + 1)) by A32, FVSUM_1:71
.= g1 + (FPower ((p . kk),k)) by A35, FUNCSDOM:28 ;
hence g is differentiable by A31, A36; :: thesis: verum
end;
end;
end;
A38: S2[ 0 ]
proof
let g be PartFunc of REAL,REAL; :: thesis: ( g = Sum (G | 0) implies g is differentiable )
A39: G | 0 = <*> the carrier of (RealVectSpace REAL) ;
assume g = Sum (G | 0) ; :: thesis: g is differentiable
then g = 0. (RealVectSpace REAL) by A39, RLVECT_1:43
.= REAL --> (In (0,REAL)) ;
hence g is differentiable ; :: thesis: verum
end;
for k being Nat holds S2[k] from NAT_1:sch 2(A38, A29);
 hence Eval p is differentiable by A4, A5, FUNCT_2:63; :: thesis: verum