let X, Y, Z be RealNormSpace; :: thesis: for f being PartFunc of Y,Z
for I being LinearOperator of X,Y
for V being Subset of Y st f is_differentiable_on V & I is one-to-one & I is onto & I is isometric holds
for y being Point of Y st y in V holds
(f `| V) . y = (((f * I) `| (I " V)) /. ((I ") . y)) * (I ")
let f be PartFunc of Y,Z; :: thesis: for I being LinearOperator of X,Y
for V being Subset of Y st f is_differentiable_on V & I is one-to-one & I is onto & I is isometric holds
for y being Point of Y st y in V holds
(f `| V) . y = (((f * I) `| (I " V)) /. ((I ") . y)) * (I ")
let I be LinearOperator of X,Y; :: thesis: for V being Subset of Y st f is_differentiable_on V & I is one-to-one & I is onto & I is isometric holds
for y being Point of Y st y in V holds
(f `| V) . y = (((f * I) `| (I " V)) /. ((I ") . y)) * (I ")
let V be Subset of Y; :: thesis: ( f is_differentiable_on V & I is one-to-one & I is onto & I is isometric implies for y being Point of Y st y in V holds
(f `| V) . y = (((f * I) `| (I " V)) /. ((I ") . y)) * (I ") )
assume that
A1: f is_differentiable_on V and
A2: ( I is one-to-one & I is onto & I is isometric ) ; :: thesis: for y being Point of Y st y in V holds
(f `| V) . y = (((f * I) `| (I " V)) /. ((I ") . y)) * (I ")
A3: V is open by A1, NDIFF_1:32;
consider J being LinearOperator of Y,X such that
A4: ( J = I " & J is one-to-one & J is onto & J is isometric ) by A2, NDIFF_7:9;
A5: ( dom (f `| V) = V & ( for x being Point of Y st x in V holds
(f `| V) /. x = diff (f,x) ) ) by A1, NDIFF_1:def 9;
set g = f * I;
set U = I " V;
A6: f * I is_differentiable_on I " V by A1, A2, NDIFF_7:29;
for y being Point of Y st y in dom (f `| V) holds
(f `| V) . y = (((f * I) `| (I " V)) /. (J . y)) * (I ")

proof

let y be Point of Y; :: thesis: ( y in dom (f `| V) implies (f `| V) . y = (((f * I) `| (I " V)) /. (J . y)) * (I ") )
assume A7: y in dom (f `| V) ; :: thesis: (f `| V) . y = (((f * I) `| (I " V)) /. (J . y)) * (I ")
then A8: (f `| V) . y = (f `| V) /. y by PARTFUN1:def 6
.= diff (f,y) by A5, A7 ;
A9: f is_differentiable_in y by A1, A3, A5, A7, NDIFF_1:31;
consider x being Point of X such that
A10: y = I . x by A2, FUNCT_2:113;
reconsider I0 = I as Point of (R_NormSpace_of_BoundedLinearOperators (X,Y)) by A2, LOPBAN_1:def 9;
A11: ((diff (f,y)) * I0) * (I0 ") = (modetrans ((diff (f,y)),Y,Z)) * ((modetrans (I0,X,Y)) * (I0 ")) by RELAT_1:36
.= (modetrans ((diff (f,y)),Y,Z)) * (I * (I ")) by LOPBAN_1:def 11
.= (modetrans ((diff (f,y)),Y,Z)) * (id (rng I0)) by A2, FUNCT_1:39
.= modetrans ((diff (f,y)),Y,Z) by A2, FUNCT_2:17
.= (f `| V) . y by A8, LOPBAN_1:def 11 ;
x in I " V by A5, A10, A7, FUNCT_2:38;
then A12: (((f * I) `| (I " V)) /. x) * (I0 ") = (diff ((f * I),x)) * (I0 ") by A6, NDIFF_1:def 9;
x = J . y by A2, A4, A10, FUNCT_2:26;
hence (f `| V) . y = (((f * I) `| (I " V)) /. (J . y)) * (I ") by A2, A9, A10, A11, A12, NDIFF_7:27; :: thesis: verum

end;

hence for y being Point of Y st y in V holds
(f `| V) . y = (((f * I) `| (I " V)) /. ((I ") . y)) * (I ") by A4, A5; :: thesis: verum