let n be Element of NAT ; :: thesis: for Z being open Subset of REAL holds #Z n is_differentiable_on n,Z
let Z be open Subset of REAL ; :: thesis: #Z n is_differentiable_on n,Z
let i be Element of NAT ; :: according to TAYLOR_1:def 6 :: thesis: ( not i <= n - 1 or (diff (#Z n),Z) . i is_differentiable_on Z )
assume A1: i <= n - 1 ; :: thesis: (diff (#Z n),Z) . i is_differentiable_on Z
reconsider i = i as Element of NAT ;
dom (#Z (n - i)) = REAL by FUNCT_2:def 1;
then A3: dom (((n choose i) * (i ! )) (#) (#Z (n - i))) = REAL by VALUED_1:def 5;
(- 1) + n < 0 + n by XREAL_1:8;
then A7: i < n by A1, XXREAL_0:2;
A8: dom ((diff (#Z n),Z) . i) = dom ((((n choose i) * (i ! )) (#) (#Z (n - i))) | Z) by Th23, A7
.= REAL /\ Z by A3, RELAT_1:90
.= Z by XBOOLE_1:28 ;
for x being Real st x in Z holds
((diff (#Z n),Z) . i) | Z is_differentiable_in x

proof

let x be Real; :: thesis: ( x in Z implies ((diff (#Z n),Z) . i) | Z is_differentiable_in x )
assume A10: x in Z ; :: thesis: ((diff (#Z n),Z) . i) | Z is_differentiable_in x
i + 0 <= (n - 1) + 1 by A1, XREAL_1:10;
then reconsider m = n - i as Element of NAT by INT_1:18;
A12: ((diff (#Z n),Z) . i) | Z = ((((n choose i) * (i ! )) (#) (#Z m)) | Z) | Z by Th23, A7
.= (((n choose i) * (i ! )) (#) (#Z m)) | Z by FUNCT_1:82
.= ((n choose i) * (i ! )) (#) ((#Z m) | Z) by RFUNCT_1:65 ;
#Z m is_differentiable_on Z by Th18, FDIFF_1:34;
then (#Z m) | Z is_differentiable_in x by A10, FDIFF_1:def 7;
hence ((diff (#Z n),Z) . i) | Z is_differentiable_in x by A12, FDIFF_1:23; :: thesis: verum

end;

hence (diff (#Z n),Z) . i is_differentiable_on Z by A8, FDIFF_1:def 7; :: thesis: verum