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:
let r, p be Element of REAL n; :: thesis:
assume that
A1: Z c= dom f and
A2: for x being Real st x in Z holds
f /. x = (x * r) + p ; :: thesis:
reconsider g = f as PartFunc of REAL,(REAL-NS n) by REAL_NS1:def 4;
reconsider r1 = r, p1 = p as Point of (REAL-NS n) by REAL_NS1:def 4;

A3: now :: thesis:

let x be Real; :: thesis:
assume x in Z ; :: thesis:
then A4: f /. x = (x * r) + p by A2;
A5: f /. x = g /. x by REAL_NS1:def 4;
x * r = x * r1 by REAL_NS1:3;
hence g /. x = (x * r1) + p1 by A4, A5, REAL_NS1:2; :: thesis:

end;

then A6: ( g is_differentiable_on Z & ( for x being Real st x in Z holds
(g `| Z) . x = r1 ) ) by A1, NDIFF_3:21;

let x be Real; :: thesis:
assume x in Z ; :: thesis:
then g | Z is_differentiable_in x by A6, NDIFF_3:def 5;
hence f | Z is_differentiable_in x ; :: thesis:

end;

hence A7: f is_differentiable_on Z by A1; :: thesis:
let x be Real; :: thesis:
assume A8: x in Z ; :: thesis:
then A9: (g `| Z) . x = diff (g,x) by A6, NDIFF_3:def 6;
A10: (f `| Z) . x = diff (f,x) by A8, A7, Def4;
diff (f,x) = diff (g,x) by Th3;
hence (f `| Z) . x = r by A8, A3, A1, A9, A10, NDIFF_3:21; :: thesis: