let X be set ; :: thesis: for i being Element of NAT
for n being non zero Element of NAT
for f being PartFunc of REAL,(REAL n) st 1 <= i & i <= n & f is_differentiable_on X holds
( (Proj (i,n)) * f is_differentiable_on X & (Proj (i,n)) * (f `| X) = ((Proj (i,n)) * f) `| X )
let i be Element of NAT ; :: thesis: for n being non zero Element of NAT
for f being PartFunc of REAL,(REAL n) st 1 <= i & i <= n & f is_differentiable_on X holds
( (Proj (i,n)) * f is_differentiable_on X & (Proj (i,n)) * (f `| X) = ((Proj (i,n)) * f) `| X )
let n be non zero Element of NAT ; :: thesis: for f being PartFunc of REAL,(REAL n) st 1 <= i & i <= n & f is_differentiable_on X holds
( (Proj (i,n)) * f is_differentiable_on X & (Proj (i,n)) * (f `| X) = ((Proj (i,n)) * f) `| X )
let f be PartFunc of REAL,(REAL n); :: thesis: ( 1 <= i & i <= n & f is_differentiable_on X implies ( (Proj (i,n)) * f is_differentiable_on X & (Proj (i,n)) * (f `| X) = ((Proj (i,n)) * f) `| X ) )
assume A1: ( 1 <= i & i <= n & f is_differentiable_on X ) ; :: thesis: ( (Proj (i,n)) * f is_differentiable_on X & (Proj (i,n)) * (f `| X) = ((Proj (i,n)) * f) `| X )
then A2: X is open Subset of REAL by Th4, Th6;
reconsider g = f as PartFunc of REAL,(REAL-NS n) by REAL_NS1:def 4;
A3: X c= dom g by A1;

now :: thesis: for x being Real st x in X holds
g is_differentiable_in x

let x be Real; :: thesis: ( x in X implies g is_differentiable_in x )
assume x in X ; :: thesis: g is_differentiable_in x
then f is_differentiable_in x by A2, A1, Th5;
hence g is_differentiable_in x ; :: thesis: verum

end;

then A4: g is_differentiable_on X by A2, A3, NDIFF_3:10;
hence (Proj (i,n)) * f is_differentiable_on X by A1, Th28; :: thesis: (Proj (i,n)) * (f `| X) = ((Proj (i,n)) * f) `| X
A5: ( dom (g `| X) = X & ( for x being Real st x in X holds
(g `| X) . x = diff (g,x) ) ) by A4, NDIFF_3:def 6;
A6: dom (f `| X) = dom (g `| X) by A1, Def4, A5;

A7: now :: thesis: for x being Element of REAL st x in dom (f `| X) holds
(f `| X) . x = (g `| X) . x

let x be Element of REAL ; :: thesis: ( x in dom (f `| X) implies (f `| X) . x = (g `| X) . x )
assume x in dom (f `| X) ; :: thesis: (f `| X) . x = (g `| X) . x
then A8: x in X by A1, Def4;
then A9: (f `| X) . x = diff (f,x) by A1, Def4;
diff (f,x) = diff (g,x) by Th3;
hence (f `| X) . x = (g `| X) . x by A9, A8, A4, NDIFF_3:def 6; :: thesis: verum

end;

g `| X is PartFunc of REAL,(REAL n) by REAL_NS1:def 4;
then (Proj (i,n)) * (f `| X) = (Proj (i,n)) * (g `| X) by A6, A7, PARTFUN1:5;
hence (Proj (i,n)) * (f `| X) = ((Proj (i,n)) * f) `| X by A4, A1, Th28; :: thesis: verum