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
A3: #Z n is_differentiable_on Z by Th18, FDIFF_1:34;
then A4: dom ((#Z n) `| Z) = Z by FDIFF_1:def 8;
A6: dom (n (#) (#Z (n - 1))) = dom (#Z (n - 1)) by VALUED_1:def 5;
A7: dom (n (#) (#Z (n - 1))) = REAL by A6, FUNCT_2:def 1;
then n (#) (#Z (n - 1)) is Function of REAL ,REAL by FUNCT_2:130;
then A8: dom ((n (#) (#Z (n - 1))) | Z) = Z by LemX;
for x being Real st x in Z holds
((#Z n) `| Z) . x = ((n (#) (#Z (n - 1))) | Z) . x

proof

let x be Real; :: thesis: ( x in Z implies ((#Z n) `| Z) . x = ((n (#) (#Z (n - 1))) | Z) . x )
assume A10: x in Z ; :: thesis: ((#Z n) `| Z) . x = ((n (#) (#Z (n - 1))) | Z) . x
((#Z n) `| Z) . x = diff (#Z n),x by A3, A10, FDIFF_1:def 8
.= 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 A7, VALUED_1:def 5
.= ((n (#) (#Z (n - 1))) | Z) . x by A8, A10, FUNCT_1:70 ;
hence ((#Z n) `| Z) . x = ((n (#) (#Z (n - 1))) | Z) . x ; :: thesis: verum

end;

hence (#Z n) `| Z = (n (#) (#Z (n - 1))) | Z by A4, A8, PARTFUN1:34; :: thesis: verum