let X be set ; :: thesis: for i being Element of NAT
for n being non zero Element of NAT
for g being PartFunc of REAL,(REAL-NS n) st 1 <= i & i <= n & g is_differentiable_on X holds
( (Proj (i,n)) * g is_differentiable_on X & (Proj (i,n)) * (g `| X) = ((Proj (i,n)) * g) `| X )
let i be Element of NAT ; :: thesis: for n being non zero Element of NAT
for g being PartFunc of REAL,(REAL-NS n) st 1 <= i & i <= n & g is_differentiable_on X holds
( (Proj (i,n)) * g is_differentiable_on X & (Proj (i,n)) * (g `| X) = ((Proj (i,n)) * g) `| X )
let n be non zero Element of NAT ; :: thesis: for g being PartFunc of REAL,(REAL-NS n) st 1 <= i & i <= n & g is_differentiable_on X holds
( (Proj (i,n)) * g is_differentiable_on X & (Proj (i,n)) * (g `| X) = ((Proj (i,n)) * g) `| X )
let g be PartFunc of REAL,(REAL-NS n); :: thesis: ( 1 <= i & i <= n & g is_differentiable_on X implies ( (Proj (i,n)) * g is_differentiable_on X & (Proj (i,n)) * (g `| X) = ((Proj (i,n)) * g) `| X ) )
assume A1: ( 1 <= i & i <= n & g is_differentiable_on X ) ; :: thesis: ( (Proj (i,n)) * g is_differentiable_on X & (Proj (i,n)) * (g `| X) = ((Proj (i,n)) * g) `| X )
then A2: X is open Subset of REAL by NDIFF_3:9, NDIFF_3:11;
A3: dom (Proj (i,n)) = the carrier of (REAL-NS n) by FUNCT_2:def 1;
rng g c= the carrier of (REAL-NS n) ;
then dom ((Proj (i,n)) * g) = dom g by A3, RELAT_1:27;
then A4: X c= dom ((Proj (i,n)) * g) by A2, A1, NDIFF_3:10;

now :: thesis: for x being Real st x in X holds
(Proj (i,n)) * g is_differentiable_in x

let x be Real; :: thesis: ( x in X implies (Proj (i,n)) * g is_differentiable_in x )
assume x in X ; :: thesis: (Proj (i,n)) * g is_differentiable_in x
then g is_differentiable_in x by A2, A1, NDIFF_3:10;
hence (Proj (i,n)) * g is_differentiable_in x by A1, Th24; :: thesis: verum

end;

hence A5: (Proj (i,n)) * g is_differentiable_on X by A2, A4, NDIFF_3:10; :: thesis: (Proj (i,n)) * (g `| X) = ((Proj (i,n)) * g) `| X
then A6: ( dom (((Proj (i,n)) * g) `| X) = X & ( for x being Real st x in X holds
(((Proj (i,n)) * g) `| X) . x = diff (((Proj (i,n)) * g),x) ) ) by NDIFF_3:def 6;
A7: ( dom (g `| X) = X & ( for x being Real st x in X holds
(g `| X) . x = diff (g,x) ) ) by A1, NDIFF_3:def 6;
rng (g `| X) c= the carrier of (REAL-NS n) ;
then A8: dom ((Proj (i,n)) * (g `| X)) = dom (g `| X) by A3, RELAT_1:27;

now :: thesis: for x being Element of REAL st x in dom (((Proj (i,n)) * g) `| X) holds
((Proj (i,n)) * (g `| X)) . x = (((Proj (i,n)) * g) `| X) . x

let x be Element of REAL ; :: thesis: ( x in dom (((Proj (i,n)) * g) `| X) implies ((Proj (i,n)) * (g `| X)) . x = (((Proj (i,n)) * g) `| X) . x )
assume A9: x in dom (((Proj (i,n)) * g) `| X) ; :: thesis: ((Proj (i,n)) * (g `| X)) . x = (((Proj (i,n)) * g) `| X) . x
then A10: x in X by A5, NDIFF_3:def 6;
then g is_differentiable_in x by A2, A1, NDIFF_3:10;
then A11: (Proj (i,n)) . (diff (g,x)) = diff (((Proj (i,n)) * g),x) by A1, Th24;
A12: (((Proj (i,n)) * g) `| X) . x = diff (((Proj (i,n)) * g),x) by A9, A6;
(g `| X) . x = diff (g,x) by A10, A1, NDIFF_3:def 6;
hence ((Proj (i,n)) * (g `| X)) . x = (((Proj (i,n)) * g) `| X) . x by A7, A10, A11, A12, FUNCT_1:13; :: thesis: verum

end;

hence (Proj (i,n)) * (g `| X) = ((Proj (i,n)) * g) `| X by A8, A6, A7, PARTFUN1:5; :: thesis: verum