let X be set ; 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 ; 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 ; 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); ( 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 )
; ( (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;
hence A5:
(Proj (i,n)) * g is_differentiable_on X
by A2, A4, NDIFF_3:10; (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 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) . xlet x be
Element of
REAL ;
( 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)
;
((Proj (i,n)) * (g `| X)) . x = (((Proj (i,n)) * g) `| X) . xthen 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;
verum end;
hence
(Proj (i,n)) * (g `| X) = ((Proj (i,n)) * g) `| X
by A8, A6, A7, PARTFUN1:5; verum