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;

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;

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

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

then A4:
g is_differentiable_on X
by A2, A3, NDIFF_3:10;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;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

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

g `| X is PartFunc of REAL,(REAL n)
by REAL_NS1:def 4;(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;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

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