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 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 by ORDINAL1:def 12;
(- 1) + n < 0 + n by XREAL_1:6;
then A2: i < n by A1, XXREAL_0:2;
A3: for x being Real st x in Z holds
((diff ((#Z n),Z)) . i) | Z is_differentiable_in x
proof
i + 0 <= (n - 1) + 1 by A1, XREAL_1:8;
then reconsider m = n - i as Element of NAT by INT_1:5;
A4: #Z m is_differentiable_on Z by Th8, FDIFF_1:26;
let x be Real; :: thesis: ( x in Z implies ((diff ((#Z n),Z)) . i) | Z is_differentiable_in x )
assume x in Z ; :: thesis: ((diff ((#Z n),Z)) . i) | Z is_differentiable_in x
then A5: (#Z m) | Z is_differentiable_in x by A4, FDIFF_1:def 6;
((diff ((#Z n),Z)) . i) | Z = ((((n choose i) * (i !)) (#) (#Z m)) | Z) | Z by A2, Th32
.= (((n choose i) * (i !)) (#) (#Z m)) | Z by FUNCT_1:51
.= ((n choose i) * (i !)) (#) ((#Z m) | Z) by RFUNCT_1:49 ;
hence ((diff ((#Z n),Z)) . i) | Z is_differentiable_in x by A5, FDIFF_1:15; :: thesis: verum
end;
dom (#Z (n - i)) = REAL by FUNCT_2:def 1;
then A6: dom (((n choose i) * (i !)) (#) (#Z (n - i))) = REAL by VALUED_1:def 5;
dom ((diff ((#Z n),Z)) . i) = dom ((((n choose i) * (i !)) (#) (#Z (n - i))) | Z) by A2, Th32
.= REAL /\ Z by A6, RELAT_1:61
.= Z by XBOOLE_1:28 ;
hence (diff ((#Z n),Z)) . i is_differentiable_on Z by A3, FDIFF_1:def 6; :: thesis: verum