let E, F, G be RealNormSpace; :: thesis: for f being Lipschitzian BilinearOperator of E,F,G
for Z being Subset of [:E,F:] st Z is open holds
( f is_differentiable_on Z & f `| Z is_continuous_on Z )
let f be Lipschitzian BilinearOperator of E,F,G; :: thesis: for Z being Subset of [:E,F:] st Z is open holds
( f is_differentiable_on Z & f `| Z is_continuous_on Z )
let Z be Subset of [:E,F:]; :: thesis: ( Z is open implies ( f is_differentiable_on Z & f `| Z is_continuous_on Z ) )
assume A1: Z is open ; :: thesis: ( f is_differentiable_on Z & f `| Z is_continuous_on Z )
consider K being Real such that
A2: ( 0 <= K & ( for z being Point of [:E,F:] holds
( f is_differentiable_in z & ( for dx being Point of E
for dy being Point of F holds (diff (f,z)) . (dx,dy) = (f . (dx,(z `2))) + (f . ((z `1),dy)) ) & ||.(diff (f,z)).|| <= K * ||.z.|| ) ) ) by Th11;
A3: dom f = the carrier of [:E,F:] by FUNCT_2:def 1;
for x being Point of [:E,F:] st x in Z holds
f is_differentiable_in x by A2;
hence A4: f is_differentiable_on Z by A1, A3, NDIFF_1:31; :: thesis: f `| Z is_continuous_on Z
set g1 = f `| Z;
A5: dom (f `| Z) = Z by A4, NDIFF_1:def 9;
A6: 0 + 0 < K + 1 by A2, XREAL_1:8;
A7: K + 0 < K + 1 by XREAL_1:8;
for t0 being Point of [:E,F:]
for r being Real st t0 in Z & 0 < r holds
ex s being Real st
( 0 < s & ( for t1 being Point of [:E,F:] st t1 in Z & ||.(t1 - t0).|| < s holds
||.(((f `| Z) /. t1) - ((f `| Z) /. t0)).|| < r ) )

proof

let t0 be Point of [:E,F:]; :: thesis: for r being Real st t0 in Z & 0 < r holds
ex s being Real st
( 0 < s & ( for t1 being Point of [:E,F:] st t1 in Z & ||.(t1 - t0).|| < s holds
||.(((f `| Z) /. t1) - ((f `| Z) /. t0)).|| < r ) )
let r0 be Real; :: thesis: ( t0 in Z & 0 < r0 implies ex s being Real st
( 0 < s & ( for t1 being Point of [:E,F:] st t1 in Z & ||.(t1 - t0).|| < s holds
||.(((f `| Z) /. t1) - ((f `| Z) /. t0)).|| < r0 ) ) )
assume A8: ( t0 in Z & 0 < r0 ) ; :: thesis: ex s being Real st
( 0 < s & ( for t1 being Point of [:E,F:] st t1 in Z & ||.(t1 - t0).|| < s holds
||.(((f `| Z) /. t1) - ((f `| Z) /. t0)).|| < r0 ) )
set r = r0 / 2;
set s = (r0 / 2) / (K + 1);
take (r0 / 2) / (K + 1) ; :: thesis: ( 0 < (r0 / 2) / (K + 1) & ( for t1 being Point of [:E,F:] st t1 in Z & ||.(t1 - t0).|| < (r0 / 2) / (K + 1) holds
||.(((f `| Z) /. t1) - ((f `| Z) /. t0)).|| < r0 ) )
A9: ( 0 < r0 / 2 & r0 / 2 < r0 ) by A8, XREAL_1:215, XREAL_1:216;
hence 0 < (r0 / 2) / (K + 1) by A6, XREAL_1:139; :: thesis: for t1 being Point of [:E,F:] st t1 in Z & ||.(t1 - t0).|| < (r0 / 2) / (K + 1) holds
||.(((f `| Z) /. t1) - ((f `| Z) /. t0)).|| < r0
let t1 be Point of [:E,F:]; :: thesis: ( t1 in Z & ||.(t1 - t0).|| < (r0 / 2) / (K + 1) implies ||.(((f `| Z) /. t1) - ((f `| Z) /. t0)).|| < r0 )
assume A10: ( t1 in Z & ||.(t1 - t0).|| < (r0 / 2) / (K + 1) ) ; :: thesis: ||.(((f `| Z) /. t1) - ((f `| Z) /. t0)).|| < r0
then A11: (f `| Z) /. t1 = diff (f,t1) by A4, NDIFF_1:def 9;
((f `| Z) /. t1) - ((f `| Z) /. t0) = (diff (f,t1)) - (diff (f,t0)) by A4, A8, A11, NDIFF_1:def 9
.= diff (f,(t1 - t0)) by Th13 ;
then A12: ||.(((f `| Z) /. t1) - ((f `| Z) /. t0)).|| <= K * ||.(t1 - t0).|| by A2;
0 <= ||.(t1 - t0).|| by NORMSP_1:4;
then A13: K * ||.(t1 - t0).|| <= (K + 1) * ||.(t1 - t0).|| by A7, XREAL_1:64;
(K + 1) * ||.(t1 - t0).|| <= (K + 1) * ((r0 / 2) / (K + 1)) by A6, A10, XREAL_1:64;
then (K + 1) * ||.(t1 - t0).|| <= r0 / 2 by A6, XCMPLX_1:87;
then (K + 1) * ||.(t1 - t0).|| < r0 by A9, XXREAL_0:2;
then K * ||.(t1 - t0).|| < r0 by A13, XXREAL_0:2;
hence ||.(((f `| Z) /. t1) - ((f `| Z) /. t0)).|| < r0 by A12, XXREAL_0:2; :: thesis: verum

end;

hence f `| Z is_continuous_on Z by A5, NFCONT_1:19; :: thesis: verum