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 ")

(f `| V) . y = (((f * I) `| (I " V)) /. ((I ") . y)) * (I ") by A4, A5; :: thesis: verum

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

hence
for y being Point of Y st y in V holds
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;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

(f `| V) . y = (((f * I) `| (I " V)) /. ((I ") . y)) * (I ") by A4, A5; :: thesis: verum