let r be Real; :: thesis:
let n be non zero Element of NAT ; :: thesis:
let Z be open Subset of REAL; :: thesis:
let f be PartFunc of REAL,(REAL n); :: thesis:
assume that
A1: Z c= dom f and
A2: f is_differentiable_on Z ; :: thesis:
reconsider g = f as PartFunc of REAL,(REAL-NS n) by REAL_NS1:def 4;
A3: dom f = dom (r (#) f) by VALUED_2:def 39;
reconsider r = r as Real ;
A4: r (#) f = r (#) g by NFCONT_4:6;
A5: Z c= dom (r (#) g) by A3, A1, NFCONT_4:6;
A6: Z c= dom g by A2;

let x be Real; :: thesis:
assume x in Z ; :: thesis:
then f | Z is_differentiable_in x by A2;
hence g | Z is_differentiable_in x ; :: thesis:

end;

then g is_differentiable_on Z by A6, NDIFF_3:def 5;
then A7: ( r (#) g is_differentiable_on Z & ( for x being Real st x in Z holds
((r (#) g) `| Z) . x = r * (diff (g,x)) ) ) by A5, NDIFF_3:19;

A8: now :: thesis:

let x be Real; :: thesis:
assume x in Z ; :: thesis:
then (r (#) g) | Z is_differentiable_in x by A7, NDIFF_3:def 5;
hence (r (#) f) | Z is_differentiable_in x by A4; :: thesis:

end;

then A9: r (#) f is_differentiable_on Z by A3, A1;

let x be Real; :: thesis:
assume A10: x in Z ; :: thesis:
then f is_differentiable_in x by A2, Th5;
then ( r (#) f is_differentiable_in x & diff ((r (#) f),x) = r * (diff (f,x)) ) by Th9;
hence ((r (#) f) `| Z) . x = r * (diff (f,x)) by A10, A9, Def4; :: thesis:

end;

hence ( r (#) f is_differentiable_on Z & ( for x being Real st x in Z holds
((r (#) f) `| Z) . x = r * (diff (f,x)) ) ) by A3, A8, A1; :: thesis: