let n be Element of NAT ; :: thesis: for Z being open Subset of REAL holds (#Z n) `| Z = (n (#) (#Z (n - 1))) | Z
let Z be open Subset of REAL; :: thesis: (#Z n) `| Z = (n (#) (#Z (n - 1))) | Z
dom (n (#) (#Z (n - 1))) = dom (#Z (n - 1)) by VALUED_1:def 5;
then A1: dom (n (#) (#Z (n - 1))) = REAL by FUNCT_2:def 1;
then n (#) (#Z (n - 1)) is Function of REAL,REAL by FUNCT_2:67;
then A2: dom ((n (#) (#Z (n - 1))) | Z) = Z by Th1;
A3: #Z n is_differentiable_on Z by Th8, FDIFF_1:26;
A4: for x being Element of REAL st x in Z holds
((#Z n) `| Z) . x = ((n (#) (#Z (n - 1))) | Z) . x

proof

let x be Element of REAL ; :: thesis: ( x in Z implies ((#Z n) `| Z) . x = ((n (#) (#Z (n - 1))) | Z) . x )
assume A5: x in Z ; :: thesis: ((#Z n) `| Z) . x = ((n (#) (#Z (n - 1))) | Z) . x
((#Z n) `| Z) . x = diff ((#Z n),x) by A3, A5, FDIFF_1:def 7
.= n * (x #Z (n - 1)) by TAYLOR_1:2
.= n * ((#Z (n - 1)) . x) by TAYLOR_1:def 1
.= (n (#) (#Z (n - 1))) . x by A1, VALUED_1:def 5
.= ((n (#) (#Z (n - 1))) | Z) . x by A2, A5, FUNCT_1:47 ;
hence ((#Z n) `| Z) . x = ((n (#) (#Z (n - 1))) | Z) . x ; :: thesis: verum

end;

dom ((#Z n) `| Z) = Z by A3, FDIFF_1:def 7;
hence (#Z n) `| Z = (n (#) (#Z (n - 1))) | Z by A2, A4, PARTFUN1:5; :: thesis: verum