let X, Y, Z be RealNormSpace; :: thesis: for V being Subset of Y

for g being PartFunc of Y,Z

for I being LinearOperator of X,Y st I is one-to-one & I is onto & I is isometric & g is_differentiable_on V holds

( g `| V is_continuous_on V iff (g * I) `| (I " V) is_continuous_on I " V )

let V be Subset of Y; :: thesis: for g being PartFunc of Y,Z

for I being LinearOperator of X,Y st I is one-to-one & I is onto & I is isometric & g is_differentiable_on V holds

( g `| V is_continuous_on V iff (g * I) `| (I " V) is_continuous_on I " V )

let g be PartFunc of Y,Z; :: thesis: for I being LinearOperator of X,Y st I is one-to-one & I is onto & I is isometric & g is_differentiable_on V holds

( g `| V is_continuous_on V iff (g * I) `| (I " V) is_continuous_on I " V )

let I be LinearOperator of X,Y; :: thesis: ( I is one-to-one & I is onto & I is isometric & g is_differentiable_on V implies ( g `| V is_continuous_on V iff (g * I) `| (I " V) is_continuous_on I " V ) )

assume that

A1: ( I is one-to-one & I is onto & I is isometric ) and

A2: g is_differentiable_on V ; :: thesis: ( g `| V is_continuous_on V iff (g * I) `| (I " V) is_continuous_on I " V )

consider J being LinearOperator of Y,X such that

A3: ( J = I " & J is one-to-one & J is onto & J is isometric ) by A1, NDIFF_7:9;

set f = g * I;

set U = I " V;

A4: dom J = the carrier of Y by FUNCT_2:def 1;

A5: g * I is_differentiable_on I " V by A1, A2, NDIFF_7:29;

A6: dom ((g * I) `| (I " V)) = I " V by A5, NDIFF_1:def 9;

A7: dom (g `| V) = V by A2, NDIFF_1:def 9;

set F = (g * I) `| (I " V);

set G = g `| V;

A8: ( g `| V is_continuous_on V implies (g * I) `| (I " V) is_continuous_on I " V )

for g being PartFunc of Y,Z

for I being LinearOperator of X,Y st I is one-to-one & I is onto & I is isometric & g is_differentiable_on V holds

( g `| V is_continuous_on V iff (g * I) `| (I " V) is_continuous_on I " V )

let V be Subset of Y; :: thesis: for g being PartFunc of Y,Z

for I being LinearOperator of X,Y st I is one-to-one & I is onto & I is isometric & g is_differentiable_on V holds

( g `| V is_continuous_on V iff (g * I) `| (I " V) is_continuous_on I " V )

let g be PartFunc of Y,Z; :: thesis: for I being LinearOperator of X,Y st I is one-to-one & I is onto & I is isometric & g is_differentiable_on V holds

( g `| V is_continuous_on V iff (g * I) `| (I " V) is_continuous_on I " V )

let I be LinearOperator of X,Y; :: thesis: ( I is one-to-one & I is onto & I is isometric & g is_differentiable_on V implies ( g `| V is_continuous_on V iff (g * I) `| (I " V) is_continuous_on I " V ) )

assume that

A1: ( I is one-to-one & I is onto & I is isometric ) and

A2: g is_differentiable_on V ; :: thesis: ( g `| V is_continuous_on V iff (g * I) `| (I " V) is_continuous_on I " V )

consider J being LinearOperator of Y,X such that

A3: ( J = I " & J is one-to-one & J is onto & J is isometric ) by A1, NDIFF_7:9;

set f = g * I;

set U = I " V;

A4: dom J = the carrier of Y by FUNCT_2:def 1;

A5: g * I is_differentiable_on I " V by A1, A2, NDIFF_7:29;

A6: dom ((g * I) `| (I " V)) = I " V by A5, NDIFF_1:def 9;

A7: dom (g `| V) = V by A2, NDIFF_1:def 9;

set F = (g * I) `| (I " V);

set G = g `| V;

A8: ( g `| V is_continuous_on V implies (g * I) `| (I " V) is_continuous_on I " V )

proof

( (g * I) `| (I " V) is_continuous_on I " V implies g `| V is_continuous_on V )
assume A10:
g `| V is_continuous_on V
; :: thesis: (g * I) `| (I " V) is_continuous_on I " V

for x0 being Point of X

for e being Real st x0 in I " V & 0 < e holds

ex d being Real st

( 0 < d & ( for x1 being Point of X st x1 in I " V & ||.(x1 - x0).|| < d holds

||.((((g * I) `| (I " V)) /. x1) - (((g * I) `| (I " V)) /. x0)).|| < e ) )

end;for x0 being Point of X

for e being Real st x0 in I " V & 0 < e holds

ex d being Real st

( 0 < d & ( for x1 being Point of X st x1 in I " V & ||.(x1 - x0).|| < d holds

||.((((g * I) `| (I " V)) /. x1) - (((g * I) `| (I " V)) /. x0)).|| < e ) )

proof

hence
(g * I) `| (I " V) is_continuous_on I " V
by A6, NFCONT_1:19; :: thesis: verum
let x0 be Point of X; :: thesis: for e being Real st x0 in I " V & 0 < e holds

ex d being Real st

( 0 < d & ( for x1 being Point of X st x1 in I " V & ||.(x1 - x0).|| < d holds

||.((((g * I) `| (I " V)) /. x1) - (((g * I) `| (I " V)) /. x0)).|| < e ) )

let e be Real; :: thesis: ( x0 in I " V & 0 < e implies ex d being Real st

( 0 < d & ( for x1 being Point of X st x1 in I " V & ||.(x1 - x0).|| < d holds

||.((((g * I) `| (I " V)) /. x1) - (((g * I) `| (I " V)) /. x0)).|| < e ) ) )

assume A11: ( x0 in I " V & 0 < e ) ; :: thesis: ex d being Real st

( 0 < d & ( for x1 being Point of X st x1 in I " V & ||.(x1 - x0).|| < d holds

||.((((g * I) `| (I " V)) /. x1) - (((g * I) `| (I " V)) /. x0)).|| < e ) )

consider y0 being Point of Y such that

A12: x0 = J . y0 by A3, FUNCT_2:113;

A13: I . x0 = y0 by A1, A3, A12, FUNCT_1:35;

then A14: y0 in V by A11, FUNCT_2:38;

then consider d being Real such that

A15: ( 0 < d & ( for y1 being Point of Y st y1 in V & ||.(y1 - y0).|| < d holds

||.(((g `| V) /. y1) - ((g `| V) /. y0)).|| < e ) ) by A10, A11, NFCONT_1:19;

take d ; :: thesis: ( 0 < d & ( for x1 being Point of X st x1 in I " V & ||.(x1 - x0).|| < d holds

||.((((g * I) `| (I " V)) /. x1) - (((g * I) `| (I " V)) /. x0)).|| < e ) )

thus 0 < d by A15; :: thesis: for x1 being Point of X st x1 in I " V & ||.(x1 - x0).|| < d holds

||.((((g * I) `| (I " V)) /. x1) - (((g * I) `| (I " V)) /. x0)).|| < e

thus for x1 being Point of X st x1 in I " V & ||.(x1 - x0).|| < d holds

||.((((g * I) `| (I " V)) /. x1) - (((g * I) `| (I " V)) /. x0)).|| < e :: thesis: verum

end;ex d being Real st

( 0 < d & ( for x1 being Point of X st x1 in I " V & ||.(x1 - x0).|| < d holds

||.((((g * I) `| (I " V)) /. x1) - (((g * I) `| (I " V)) /. x0)).|| < e ) )

let e be Real; :: thesis: ( x0 in I " V & 0 < e implies ex d being Real st

( 0 < d & ( for x1 being Point of X st x1 in I " V & ||.(x1 - x0).|| < d holds

||.((((g * I) `| (I " V)) /. x1) - (((g * I) `| (I " V)) /. x0)).|| < e ) ) )

assume A11: ( x0 in I " V & 0 < e ) ; :: thesis: ex d being Real st

( 0 < d & ( for x1 being Point of X st x1 in I " V & ||.(x1 - x0).|| < d holds

||.((((g * I) `| (I " V)) /. x1) - (((g * I) `| (I " V)) /. x0)).|| < e ) )

consider y0 being Point of Y such that

A12: x0 = J . y0 by A3, FUNCT_2:113;

A13: I . x0 = y0 by A1, A3, A12, FUNCT_1:35;

then A14: y0 in V by A11, FUNCT_2:38;

then consider d being Real such that

A15: ( 0 < d & ( for y1 being Point of Y st y1 in V & ||.(y1 - y0).|| < d holds

||.(((g `| V) /. y1) - ((g `| V) /. y0)).|| < e ) ) by A10, A11, NFCONT_1:19;

take d ; :: thesis: ( 0 < d & ( for x1 being Point of X st x1 in I " V & ||.(x1 - x0).|| < d holds

||.((((g * I) `| (I " V)) /. x1) - (((g * I) `| (I " V)) /. x0)).|| < e ) )

thus 0 < d by A15; :: thesis: for x1 being Point of X st x1 in I " V & ||.(x1 - x0).|| < d holds

||.((((g * I) `| (I " V)) /. x1) - (((g * I) `| (I " V)) /. x0)).|| < e

thus for x1 being Point of X st x1 in I " V & ||.(x1 - x0).|| < d holds

||.((((g * I) `| (I " V)) /. x1) - (((g * I) `| (I " V)) /. x0)).|| < e :: thesis: verum

proof

let x1 be Point of X; :: thesis: ( x1 in I " V & ||.(x1 - x0).|| < d implies ||.((((g * I) `| (I " V)) /. x1) - (((g * I) `| (I " V)) /. x0)).|| < e )

assume A16: ( x1 in I " V & ||.(x1 - x0).|| < d ) ; :: thesis: ||.((((g * I) `| (I " V)) /. x1) - (((g * I) `| (I " V)) /. x0)).|| < e

consider y1 being Point of Y such that

A17: x1 = J . y1 by A3, FUNCT_2:113;

A18: I . x1 = y1 by A1, A3, A17, FUNCT_1:35;

then A19: y1 in V by A16, FUNCT_2:38;

||.(y1 - y0).|| = ||.(x1 - x0).|| by A1, A13, A18;

then A20: ||.(((g `| V) /. y1) - ((g `| V) /. y0)).|| < e by A15, A16, A19;

A21: (g `| V) /. y1 = (g `| V) . y1 by A7, A19, PARTFUN1:def 6

.= (((g * I) `| (I " V)) /. x1) * J by A1, A2, A3, A17, A19, Th9 ;

A22: (g `| V) /. y0 = (g `| V) . y0 by A7, A14, PARTFUN1:def 6

.= (((g * I) `| (I " V)) /. x0) * J by A1, A2, A3, A12, A14, Th9 ;

reconsider dF = (((g * I) `| (I " V)) /. x1) - (((g * I) `| (I " V)) /. x0) as Lipschitzian LinearOperator of X,Z by LOPBAN_1:def 9;

reconsider dG = ((g `| V) /. y1) - ((g `| V) /. y0) as Lipschitzian LinearOperator of Y,Z by LOPBAN_1:def 9;

hence ||.((((g * I) `| (I " V)) /. x1) - (((g * I) `| (I " V)) /. x0)).|| < e by A3, A20, NDIFF_7:22; :: thesis: verum

end;assume A16: ( x1 in I " V & ||.(x1 - x0).|| < d ) ; :: thesis: ||.((((g * I) `| (I " V)) /. x1) - (((g * I) `| (I " V)) /. x0)).|| < e

consider y1 being Point of Y such that

A17: x1 = J . y1 by A3, FUNCT_2:113;

A18: I . x1 = y1 by A1, A3, A17, FUNCT_1:35;

then A19: y1 in V by A16, FUNCT_2:38;

||.(y1 - y0).|| = ||.(x1 - x0).|| by A1, A13, A18;

then A20: ||.(((g `| V) /. y1) - ((g `| V) /. y0)).|| < e by A15, A16, A19;

A21: (g `| V) /. y1 = (g `| V) . y1 by A7, A19, PARTFUN1:def 6

.= (((g * I) `| (I " V)) /. x1) * J by A1, A2, A3, A17, A19, Th9 ;

A22: (g `| V) /. y0 = (g `| V) . y0 by A7, A14, PARTFUN1:def 6

.= (((g * I) `| (I " V)) /. x0) * J by A1, A2, A3, A12, A14, Th9 ;

reconsider dF = (((g * I) `| (I " V)) /. x1) - (((g * I) `| (I " V)) /. x0) as Lipschitzian LinearOperator of X,Z by LOPBAN_1:def 9;

reconsider dG = ((g `| V) /. y1) - ((g `| V) /. y0) as Lipschitzian LinearOperator of Y,Z by LOPBAN_1:def 9;

now :: thesis: for v being VECTOR of Y holds (dF * J) . v = dG . v

then
dF * J = dG
;let v be VECTOR of Y; :: thesis: (dF * J) . v = dG . v

A23: (((((g * I) `| (I " V)) /. x1) - (((g * I) `| (I " V)) /. x0)) * J) . v = ((((g * I) `| (I " V)) /. x1) - (((g * I) `| (I " V)) /. x0)) . (J . v) by A4, FUNCT_1:13

.= ((((g * I) `| (I " V)) /. x1) . (J . v)) - ((((g * I) `| (I " V)) /. x0) . (J . v)) by LOPBAN_1:40 ;

A24: ((g `| V) /. y1) . v = (((g * I) `| (I " V)) /. x1) . (J . v) by A4, A21, FUNCT_1:13;

((g `| V) /. y0) . v = (((g * I) `| (I " V)) /. x0) . (J . v) by A4, A22, FUNCT_1:13;

hence (dF * J) . v = dG . v by A23, A24, LOPBAN_1:40; :: thesis: verum

end;A23: (((((g * I) `| (I " V)) /. x1) - (((g * I) `| (I " V)) /. x0)) * J) . v = ((((g * I) `| (I " V)) /. x1) - (((g * I) `| (I " V)) /. x0)) . (J . v) by A4, FUNCT_1:13

.= ((((g * I) `| (I " V)) /. x1) . (J . v)) - ((((g * I) `| (I " V)) /. x0) . (J . v)) by LOPBAN_1:40 ;

A24: ((g `| V) /. y1) . v = (((g * I) `| (I " V)) /. x1) . (J . v) by A4, A21, FUNCT_1:13;

((g `| V) /. y0) . v = (((g * I) `| (I " V)) /. x0) . (J . v) by A4, A22, FUNCT_1:13;

hence (dF * J) . v = dG . v by A23, A24, LOPBAN_1:40; :: thesis: verum

hence ||.((((g * I) `| (I " V)) /. x1) - (((g * I) `| (I " V)) /. x0)).|| < e by A3, A20, NDIFF_7:22; :: thesis: verum

proof

hence
( g `| V is_continuous_on V iff (g * I) `| (I " V) is_continuous_on I " V )
by A8; :: thesis: verum
assume A25:
(g * I) `| (I " V) is_continuous_on I " V
; :: thesis: g `| V is_continuous_on V

for y0 being Point of Y

for e being Real st y0 in V & 0 < e holds

ex d being Real st

( 0 < d & ( for y1 being Point of Y st y1 in V & ||.(y1 - y0).|| < d holds

||.(((g `| V) /. y1) - ((g `| V) /. y0)).|| < e ) )

end;for y0 being Point of Y

for e being Real st y0 in V & 0 < e holds

ex d being Real st

( 0 < d & ( for y1 being Point of Y st y1 in V & ||.(y1 - y0).|| < d holds

||.(((g `| V) /. y1) - ((g `| V) /. y0)).|| < e ) )

proof

hence
g `| V is_continuous_on V
by A7, NFCONT_1:19; :: thesis: verum
let y0 be Point of Y; :: thesis: for e being Real st y0 in V & 0 < e holds

ex d being Real st

( 0 < d & ( for y1 being Point of Y st y1 in V & ||.(y1 - y0).|| < d holds

||.(((g `| V) /. y1) - ((g `| V) /. y0)).|| < e ) )

let e be Real; :: thesis: ( y0 in V & 0 < e implies ex d being Real st

( 0 < d & ( for y1 being Point of Y st y1 in V & ||.(y1 - y0).|| < d holds

||.(((g `| V) /. y1) - ((g `| V) /. y0)).|| < e ) ) )

assume A26: ( y0 in V & 0 < e ) ; :: thesis: ex d being Real st

( 0 < d & ( for y1 being Point of Y st y1 in V & ||.(y1 - y0).|| < d holds

||.(((g `| V) /. y1) - ((g `| V) /. y0)).|| < e ) )

set x0 = J . y0;

I . (J . y0) = y0 by A1, A3, FUNCT_1:35;

then J . y0 in I " V by A26, FUNCT_2:38;

then consider d being Real such that

A27: ( 0 < d & ( for x1 being Point of X st x1 in I " V & ||.(x1 - (J . y0)).|| < d holds

||.((((g * I) `| (I " V)) /. x1) - (((g * I) `| (I " V)) /. (J . y0))).|| < e ) ) by A25, A26, NFCONT_1:19;

take d ; :: thesis: ( 0 < d & ( for y1 being Point of Y st y1 in V & ||.(y1 - y0).|| < d holds

||.(((g `| V) /. y1) - ((g `| V) /. y0)).|| < e ) )

thus 0 < d by A27; :: thesis: for y1 being Point of Y st y1 in V & ||.(y1 - y0).|| < d holds

||.(((g `| V) /. y1) - ((g `| V) /. y0)).|| < e

let y1 be Point of Y; :: thesis: ( y1 in V & ||.(y1 - y0).|| < d implies ||.(((g `| V) /. y1) - ((g `| V) /. y0)).|| < e )

assume A28: ( y1 in V & ||.(y1 - y0).|| < d ) ; :: thesis: ||.(((g `| V) /. y1) - ((g `| V) /. y0)).|| < e

set x1 = J . y1;

I . (J . y1) = y1 by A1, A3, FUNCT_1:35;

then A29: J . y1 in I " V by A28, FUNCT_2:38;

||.((J . y1) - (J . y0)).|| = ||.(y1 - y0).|| by A3;

then A30: ||.((((g * I) `| (I " V)) /. (J . y1)) - (((g * I) `| (I " V)) /. (J . y0))).|| < e by A27, A28, A29;

A31: (g `| V) /. y1 = (g `| V) . y1 by A7, A28, PARTFUN1:def 6

.= (((g * I) `| (I " V)) /. (J . y1)) * J by A1, A2, A3, A28, Th9 ;

A32: (g `| V) /. y0 = (g `| V) . y0 by A7, A26, PARTFUN1:def 6

.= (((g * I) `| (I " V)) /. (J . y0)) * J by A1, A2, A3, A26, Th9 ;

reconsider dF = (((g * I) `| (I " V)) /. (J . y1)) - (((g * I) `| (I " V)) /. (J . y0)) as Lipschitzian LinearOperator of X,Z by LOPBAN_1:def 9;

reconsider dG = ((g `| V) /. y1) - ((g `| V) /. y0) as Lipschitzian LinearOperator of Y,Z by LOPBAN_1:def 9;

hence ||.(((g `| V) /. y1) - ((g `| V) /. y0)).|| < e by A3, A30, NDIFF_7:22; :: thesis: verum

end;ex d being Real st

( 0 < d & ( for y1 being Point of Y st y1 in V & ||.(y1 - y0).|| < d holds

||.(((g `| V) /. y1) - ((g `| V) /. y0)).|| < e ) )

let e be Real; :: thesis: ( y0 in V & 0 < e implies ex d being Real st

( 0 < d & ( for y1 being Point of Y st y1 in V & ||.(y1 - y0).|| < d holds

||.(((g `| V) /. y1) - ((g `| V) /. y0)).|| < e ) ) )

assume A26: ( y0 in V & 0 < e ) ; :: thesis: ex d being Real st

( 0 < d & ( for y1 being Point of Y st y1 in V & ||.(y1 - y0).|| < d holds

||.(((g `| V) /. y1) - ((g `| V) /. y0)).|| < e ) )

set x0 = J . y0;

I . (J . y0) = y0 by A1, A3, FUNCT_1:35;

then J . y0 in I " V by A26, FUNCT_2:38;

then consider d being Real such that

A27: ( 0 < d & ( for x1 being Point of X st x1 in I " V & ||.(x1 - (J . y0)).|| < d holds

||.((((g * I) `| (I " V)) /. x1) - (((g * I) `| (I " V)) /. (J . y0))).|| < e ) ) by A25, A26, NFCONT_1:19;

take d ; :: thesis: ( 0 < d & ( for y1 being Point of Y st y1 in V & ||.(y1 - y0).|| < d holds

||.(((g `| V) /. y1) - ((g `| V) /. y0)).|| < e ) )

thus 0 < d by A27; :: thesis: for y1 being Point of Y st y1 in V & ||.(y1 - y0).|| < d holds

||.(((g `| V) /. y1) - ((g `| V) /. y0)).|| < e

let y1 be Point of Y; :: thesis: ( y1 in V & ||.(y1 - y0).|| < d implies ||.(((g `| V) /. y1) - ((g `| V) /. y0)).|| < e )

assume A28: ( y1 in V & ||.(y1 - y0).|| < d ) ; :: thesis: ||.(((g `| V) /. y1) - ((g `| V) /. y0)).|| < e

set x1 = J . y1;

I . (J . y1) = y1 by A1, A3, FUNCT_1:35;

then A29: J . y1 in I " V by A28, FUNCT_2:38;

||.((J . y1) - (J . y0)).|| = ||.(y1 - y0).|| by A3;

then A30: ||.((((g * I) `| (I " V)) /. (J . y1)) - (((g * I) `| (I " V)) /. (J . y0))).|| < e by A27, A28, A29;

A31: (g `| V) /. y1 = (g `| V) . y1 by A7, A28, PARTFUN1:def 6

.= (((g * I) `| (I " V)) /. (J . y1)) * J by A1, A2, A3, A28, Th9 ;

A32: (g `| V) /. y0 = (g `| V) . y0 by A7, A26, PARTFUN1:def 6

.= (((g * I) `| (I " V)) /. (J . y0)) * J by A1, A2, A3, A26, Th9 ;

reconsider dF = (((g * I) `| (I " V)) /. (J . y1)) - (((g * I) `| (I " V)) /. (J . y0)) as Lipschitzian LinearOperator of X,Z by LOPBAN_1:def 9;

reconsider dG = ((g `| V) /. y1) - ((g `| V) /. y0) as Lipschitzian LinearOperator of Y,Z by LOPBAN_1:def 9;

now :: thesis: for v being VECTOR of Y holds (dF * J) . v = dG . v

then
dF * J = dG
;let v be VECTOR of Y; :: thesis: (dF * J) . v = dG . v

A33: (((((g * I) `| (I " V)) /. (J . y1)) - (((g * I) `| (I " V)) /. (J . y0))) * J) . v = ((((g * I) `| (I " V)) /. (J . y1)) - (((g * I) `| (I " V)) /. (J . y0))) . (J . v) by A4, FUNCT_1:13

.= ((((g * I) `| (I " V)) /. (J . y1)) . (J . v)) - ((((g * I) `| (I " V)) /. (J . y0)) . (J . v)) by LOPBAN_1:40 ;

A34: ((g `| V) /. y1) . v = (((g * I) `| (I " V)) /. (J . y1)) . (J . v) by A4, A31, FUNCT_1:13;

((g `| V) /. y0) . v = (((g * I) `| (I " V)) /. (J . y0)) . (J . v) by A4, A32, FUNCT_1:13;

hence (dF * J) . v = dG . v by A33, A34, LOPBAN_1:40; :: thesis: verum

end;A33: (((((g * I) `| (I " V)) /. (J . y1)) - (((g * I) `| (I " V)) /. (J . y0))) * J) . v = ((((g * I) `| (I " V)) /. (J . y1)) - (((g * I) `| (I " V)) /. (J . y0))) . (J . v) by A4, FUNCT_1:13

.= ((((g * I) `| (I " V)) /. (J . y1)) . (J . v)) - ((((g * I) `| (I " V)) /. (J . y0)) . (J . v)) by LOPBAN_1:40 ;

A34: ((g `| V) /. y1) . v = (((g * I) `| (I " V)) /. (J . y1)) . (J . v) by A4, A31, FUNCT_1:13;

((g `| V) /. y0) . v = (((g * I) `| (I " V)) /. (J . y0)) . (J . v) by A4, A32, FUNCT_1:13;

hence (dF * J) . v = dG . v by A33, A34, LOPBAN_1:40; :: thesis: verum

hence ||.(((g `| V) /. y1) - ((g `| V) /. y0)).|| < e by A3, A30, NDIFF_7:22; :: thesis: verum