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_partial_differentiable_on`1 Z & f is_partial_differentiable_on`2 Z & f `partial`1| Z is_continuous_on Z & f `partial`2| 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_partial_differentiable_on`1 Z & f is_partial_differentiable_on`2 Z & f `partial`1| Z is_continuous_on Z & f `partial`2| Z is_continuous_on Z )
let Z be Subset of [:E,F:]; :: thesis: ( Z is open implies ( f is_partial_differentiable_on`1 Z & f is_partial_differentiable_on`2 Z & f `partial`1| Z is_continuous_on Z & f `partial`2| Z is_continuous_on Z ) )
assume A1: Z is open ; :: thesis: ( f is_partial_differentiable_on`1 Z & f is_partial_differentiable_on`2 Z & f `partial`1| Z is_continuous_on Z & f `partial`2| Z is_continuous_on Z )
A2: 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_partial_differentiable_in`1 x by Th4;
hence A3: f is_partial_differentiable_on`1 Z by A1, A2, NDIFF_7:43; :: thesis: ( f is_partial_differentiable_on`2 Z & f `partial`1| Z is_continuous_on Z & f `partial`2| Z is_continuous_on Z )
for x being Point of [:E,F:] st x in Z holds
f is_partial_differentiable_in`2 x by Th4;
hence A4: f is_partial_differentiable_on`2 Z by A1, A2, NDIFF_7:44; :: thesis: ( f `partial`1| Z is_continuous_on Z & f `partial`2| Z is_continuous_on Z )
set g1 = f `partial`1| Z;
set g2 = f `partial`2| Z;
A5: dom (f `partial`1| Z) = Z by A3, NDIFF_7:def 10;
A6: dom (f `partial`2| Z) = Z by A4, NDIFF_7:def 11;
consider K being Real such that
A7: ( 0 <= K & ( for z being Point of [:E,F:] holds
( ||.(partdiff`1 (f,z)).|| <= K * ||.z.|| & ||.(partdiff`2 (f,z)).|| <= K * ||.z.|| ) ) ) by Th6;
A8: 0 + 0 < K + 1 by A7, XREAL_1:8;
A9: 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 `partial`1| Z) /. t1) - ((f `partial`1| 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 `partial`1| Z) /. t1) - ((f `partial`1| 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 `partial`1| Z) /. t1) - ((f `partial`1| Z) /. t0)).|| < r0 ) ) )
assume A10: ( 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 `partial`1| Z) /. t1) - ((f `partial`1| 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 `partial`1| Z) /. t1) - ((f `partial`1| Z) /. t0)).|| < r0 ) )
A11: ( 0 < r0 / 2 & r0 / 2 < r0 ) by A10, XREAL_1:215, XREAL_1:216;
hence 0 < (r0 / 2) / (K + 1) by A8, XREAL_1:139; :: thesis: for t1 being Point of [:E,F:] st t1 in Z & ||.(t1 - t0).|| < (r0 / 2) / (K + 1) holds
||.(((f `partial`1| Z) /. t1) - ((f `partial`1| Z) /. t0)).|| < r0
let t1 be Point of [:E,F:]; :: thesis: ( t1 in Z & ||.(t1 - t0).|| < (r0 / 2) / (K + 1) implies ||.(((f `partial`1| Z) /. t1) - ((f `partial`1| Z) /. t0)).|| < r0 )
assume A12: ( t1 in Z & ||.(t1 - t0).|| < (r0 / 2) / (K + 1) ) ; :: thesis: ||.(((f `partial`1| Z) /. t1) - ((f `partial`1| Z) /. t0)).|| < r0
A13: (f `partial`1| Z) /. t1 = partdiff`1 (f,t1) by A3, A12, NDIFF_7:def 10;
((f `partial`1| Z) /. t1) - ((f `partial`1| Z) /. t0) = (partdiff`1 (f,t1)) - (partdiff`1 (f,t0)) by A3, A10, A13, NDIFF_7:def 10
.= partdiff`1 (f,(t1 - t0)) by Th7 ;
then A14: ||.(((f `partial`1| Z) /. t1) - ((f `partial`1| Z) /. t0)).|| <= K * ||.(t1 - t0).|| by A7;
0 <= ||.(t1 - t0).|| by NORMSP_1:4;
then A15: K * ||.(t1 - t0).|| <= (K + 1) * ||.(t1 - t0).|| by A9, XREAL_1:64;
(K + 1) * ||.(t1 - t0).|| <= (K + 1) * ((r0 / 2) / (K + 1)) by A8, A12, XREAL_1:64;
then (K + 1) * ||.(t1 - t0).|| <= r0 / 2 by A8, XCMPLX_1:87;
then (K + 1) * ||.(t1 - t0).|| < r0 by A11, XXREAL_0:2;
then K * ||.(t1 - t0).|| < r0 by A15, XXREAL_0:2;
hence ||.(((f `partial`1| Z) /. t1) - ((f `partial`1| Z) /. t0)).|| < r0 by A14, XXREAL_0:2; :: thesis: verum

end;

hence f `partial`1| Z is_continuous_on Z by A5, NFCONT_1:19; :: thesis: f `partial`2| Z is_continuous_on Z
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 `partial`2| Z) /. t1) - ((f `partial`2| 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 `partial`2| Z) /. t1) - ((f `partial`2| 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 `partial`2| Z) /. t1) - ((f `partial`2| Z) /. t0)).|| < r0 ) ) )
assume A16: ( 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 `partial`2| Z) /. t1) - ((f `partial`2| 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 `partial`2| Z) /. t1) - ((f `partial`2| Z) /. t0)).|| < r0 ) )
A17: ( 0 < r0 / 2 & r0 / 2 < r0 ) by A16, XREAL_1:215, XREAL_1:216;
hence 0 < (r0 / 2) / (K + 1) by A8, XREAL_1:139; :: thesis: for t1 being Point of [:E,F:] st t1 in Z & ||.(t1 - t0).|| < (r0 / 2) / (K + 1) holds
||.(((f `partial`2| Z) /. t1) - ((f `partial`2| Z) /. t0)).|| < r0
let t1 be Point of [:E,F:]; :: thesis: ( t1 in Z & ||.(t1 - t0).|| < (r0 / 2) / (K + 1) implies ||.(((f `partial`2| Z) /. t1) - ((f `partial`2| Z) /. t0)).|| < r0 )
assume A18: ( t1 in Z & ||.(t1 - t0).|| < (r0 / 2) / (K + 1) ) ; :: thesis: ||.(((f `partial`2| Z) /. t1) - ((f `partial`2| Z) /. t0)).|| < r0
A19: (f `partial`2| Z) /. t1 = partdiff`2 (f,t1) by A4, A18, NDIFF_7:def 11;
((f `partial`2| Z) /. t1) - ((f `partial`2| Z) /. t0) = (partdiff`2 (f,t1)) - (partdiff`2 (f,t0)) by A4, A16, A19, NDIFF_7:def 11
.= partdiff`2 (f,(t1 - t0)) by Th8 ;
then A20: ||.(((f `partial`2| Z) /. t1) - ((f `partial`2| Z) /. t0)).|| <= K * ||.(t1 - t0).|| by A7;
0 <= ||.(t1 - t0).|| by NORMSP_1:4;
then A21: K * ||.(t1 - t0).|| <= (K + 1) * ||.(t1 - t0).|| by A9, XREAL_1:64;
(K + 1) * ||.(t1 - t0).|| <= (K + 1) * ((r0 / 2) / (K + 1)) by A8, A18, XREAL_1:64;
then (K + 1) * ||.(t1 - t0).|| <= r0 / 2 by A8, XCMPLX_1:87;
then (K + 1) * ||.(t1 - t0).|| < r0 by A17, XXREAL_0:2;
then K * ||.(t1 - t0).|| < r0 by A21, XXREAL_0:2;
hence ||.(((f `partial`2| Z) /. t1) - ((f `partial`2| Z) /. t0)).|| < r0 by A20, XXREAL_0:2; :: thesis: verum

end;

hence f `partial`2| Z is_continuous_on Z by A6, NFCONT_1:19; :: thesis: verum