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 ;
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 ;
A6: dom ((g * I) `| (I " V)) = I " V by ;
A7: dom (g `| V) = V by ;
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
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 ) )
proof
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 ;
A13: I . x0 = y0 by ;
then A14: y0 in V by ;
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 ;
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 ;
A18: I . x1 = y1 by ;
then A19: y1 in V by ;
||.(y1 - y0).|| = ||.(x1 - x0).|| by A1, A13, A18;
then A20: ||.(((g `| V) /. y1) - ((g `| V) /. y0)).|| < e by ;
A21: (g `| V) /. y1 = (g `| V) . y1 by
.= (((g * I) `| (I " V)) /. x1) * J by A1, A2, A3, A17, A19, Th9 ;
A22: (g `| V) /. y0 = (g `| V) . y0 by
.= (((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
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
.= ((((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 ;
((g `| V) /. y0) . v = (((g * I) `| (I " V)) /. x0) . (J . v) by ;
hence (dF * J) . v = dG . v by ; :: thesis: verum
end;
then dF * J = dG ;
hence ||.((((g * I) `| (I " V)) /. x1) - (((g * I) `| (I " V)) /. x0)).|| < e by ; :: thesis: verum
end;
end;
hence (g * I) `| (I " V) is_continuous_on I " V by ; :: thesis: verum
end;
( (g * I) `| (I " V) is_continuous_on I " V implies g `| V is_continuous_on V )
proof
assume A25: (g * I) `| (I " V) is_continuous_on I " V ; :: thesis:
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
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 ;
then J . y0 in I " V by ;
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 ;
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 ;
then A29: J . y1 in I " V by ;
||.((J . y1) - (J . y0)).|| = ||.(y1 - y0).|| by A3;
then A30: ||.((((g * I) `| (I " V)) /. (J . y1)) - (((g * I) `| (I " V)) /. (J . y0))).|| < e by ;
A31: (g `| V) /. y1 = (g `| V) . y1 by
.= (((g * I) `| (I " V)) /. (J . y1)) * J by A1, A2, A3, A28, Th9 ;
A32: (g `| V) /. y0 = (g `| V) . y0 by
.= (((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
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
.= ((((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 ;
((g `| V) /. y0) . v = (((g * I) `| (I " V)) /. (J . y0)) . (J . v) by ;
hence (dF * J) . v = dG . v by ; :: thesis: verum
end;
then dF * J = dG ;
hence ||.(((g `| V) /. y1) - ((g `| V) /. y0)).|| < e by ; :: thesis: verum
end;
hence g `| V is_continuous_on V by ; :: thesis: verum
end;
hence ( g `| V is_continuous_on V iff (g * I) `| (I " V) is_continuous_on I " V ) by A8; :: thesis: verum