let E, F, G be RealNormSpace; :: thesis: for f being BilinearOperator of E,F,G holds
( ( f is_continuous_on the carrier of [:E,F:] implies f is_continuous_in 0. [:E,F:] ) & ( f is_continuous_in 0. [:E,F:] implies f is_continuous_on the carrier of [:E,F:] ) & ( f is_continuous_on the carrier of [:E,F:] implies ex K being Real st
( 0 <= K & ( for x being Point of E
for y being Point of F holds ||.(f . (x,y)).|| <= (K * ||.x.||) * ||.y.|| ) ) ) & ( ex K being Real st
( 0 <= K & ( for x being Point of E
for y being Point of F holds ||.(f . (x,y)).|| <= (K * ||.x.||) * ||.y.|| ) ) implies f is_continuous_on the carrier of [:E,F:] ) )
let f be BilinearOperator of E,F,G; :: thesis: ( ( f is_continuous_on the carrier of [:E,F:] implies f is_continuous_in 0. [:E,F:] ) & ( f is_continuous_in 0. [:E,F:] implies f is_continuous_on the carrier of [:E,F:] ) & ( f is_continuous_on the carrier of [:E,F:] implies ex K being Real st
( 0 <= K & ( for x being Point of E
for y being Point of F holds ||.(f . (x,y)).|| <= (K * ||.x.||) * ||.y.|| ) ) ) & ( ex K being Real st
( 0 <= K & ( for x being Point of E
for y being Point of F holds ||.(f . (x,y)).|| <= (K * ||.x.||) * ||.y.|| ) ) implies f is_continuous_on the carrier of [:E,F:] ) )
A1: dom f = the carrier of [:E,F:] by FUNCT_2:def 1;
A2: f . (0. [:E,F:]) = f . ((0. E),(0. F)) by PRVECT_3:18
.= f . ((0 * (0. E)),(0. F)) by RLVECT_1:10
.= 0 * (f . ((0. E),(0. F))) by LM8
.= 0. G by RLVECT_1:10 ;
A4: ( f is_continuous_in 0. [:E,F:] implies ex K being Real st
( 0 <= K & ( for x being Point of E
for y being Point of F holds ||.(f . (x,y)).|| <= (K * ||.x.||) * ||.y.|| ) ) )

proof

assume f is_continuous_in 0. [:E,F:] ; :: thesis: ex K being Real st
( 0 <= K & ( for x being Point of E
for y being Point of F holds ||.(f . (x,y)).|| <= (K * ||.x.||) * ||.y.|| ) )
then consider s being Real such that
A5: ( 0 < s & ( for z being Point of [:E,F:] st z in dom f & ||.(z - (0. [:E,F:])).|| < s holds
||.((f /. z) - (f /. (0. [:E,F:]))).|| < 1 ) ) by NFCONT_1:7;
consider s1 being Real such that
A7: ( 0 < s1 & s1 < s & [:(Ball ((0. E),s1)),(Ball ((0. F),s1)):] c= Ball ((0. [:E,F:]),s) ) by A5, NDIFF_8:22, PRVECT_3:18;
set s2 = s1 / 2;
A8: ( 0 < s1 / 2 & s1 / 2 < s1 ) by A7, XREAL_1:215, XREAL_1:216;

A9: now :: thesis: for x being Point of E
for y being Point of F st ||.x.|| <= s1 / 2 & ||.y.|| <= s1 / 2 holds
||.(f . (x,y)).|| < 1

let x be Point of E; :: thesis: for y being Point of F st ||.x.|| <= s1 / 2 & ||.y.|| <= s1 / 2 holds
||.(f . (x,y)).|| < 1
let y be Point of F; :: thesis: ( ||.x.|| <= s1 / 2 & ||.y.|| <= s1 / 2 implies ||.(f . (x,y)).|| < 1 )
assume ( ||.x.|| <= s1 / 2 & ||.y.|| <= s1 / 2 ) ; :: thesis: ||.(f . (x,y)).|| < 1
then A10: ( ||.x.|| < s1 & ||.y.|| < s1 ) by A8, XXREAL_0:2;
reconsider z = [x,y] as Point of [:E,F:] ;
||.(x - (0. E)).|| < s1 by A10, RLVECT_1:13;
then ||.((0. E) - x).|| < s1 by NORMSP_1:7;
then A12: x in Ball ((0. E),s1) ;
||.(y - (0. F)).|| < s1 by A10, RLVECT_1:13;
then ||.((0. F) - y).|| < s1 by NORMSP_1:7;
then y in Ball ((0. F),s1) ;
then z in [:(Ball ((0. E),s1)),(Ball ((0. F),s1)):] by A12, ZFMISC_1:87;
then z in Ball ((0. [:E,F:]),s) by A7;
then ex z1 being Point of [:E,F:] st
( z = z1 & ||.((0. [:E,F:]) - z1).|| < s ) ;
then ||.(z - (0. [:E,F:])).|| < s by NORMSP_1:7;
then ||.((f /. z) - (f /. (0. [:E,F:]))).|| < 1 by A5, A1;
hence ||.(f . (x,y)).|| < 1 by A2, RLVECT_1:13; :: thesis: verum

end;

A14: 0 < (s1 / 2) * (s1 / 2) by A8, XREAL_1:129;
take K = 1 / ((s1 / 2) * (s1 / 2)); :: thesis: ( 0 <= K & ( for x being Point of E
for y being Point of F holds ||.(f . (x,y)).|| <= (K * ||.x.||) * ||.y.|| ) )
thus 0 <= K by A7; :: thesis: for x being Point of E
for y being Point of F holds ||.(f . (x,y)).|| <= (K * ||.x.||) * ||.y.||
let x be Point of E; :: thesis: for y being Point of F holds ||.(f . (x,y)).|| <= (K * ||.x.||) * ||.y.||
let y be Point of F; :: thesis: ||.(f . (x,y)).|| <= (K * ||.x.||) * ||.y.||
A15: f . ((0. E),y) = f . ((0 * (0. E)),y) by RLVECT_1:10
.= 0 * (f . ((0. E),y)) by LM8
.= 0. G by RLVECT_1:10 ;
A16: f . (x,(0. F)) = f . (x,(0 * (0. F))) by RLVECT_1:10
.= 0 * (f . (x,(0. F))) by LM8
.= 0. G by RLVECT_1:10 ;
thus ||.(f . (x,y)).|| <= (K * ||.x.||) * ||.y.|| :: thesis: verum

proof

per cases ( ( x <> 0. E & y <> 0. F ) or x = 0. E or y = 0. F ) ;

suppose C16: ( x <> 0. E & y <> 0. F ) ; :: thesis: ||.(f . (x,y)).|| <= (K * ||.x.||) * ||.y.||

then ( ||.x.|| <> 0 & ||.y.|| <> 0 ) by NORMSP_0:def 5;
then A17: ( 0 < ||.x.|| & 0 < ||.y.|| ) ;
set x1 = ((s1 / 2) / ||.x.||) * x;
set y1 = ((s1 / 2) / ||.y.||) * y;
A19: ||.(((s1 / 2) / ||.x.||) * x).|| = |.((s1 / 2) / ||.x.||).| * ||.x.|| by NORMSP_1:def 1
.= ((s1 / 2) / ||.x.||) * ||.x.|| by A7, COMPLEX1:43
.= s1 / 2 by C16, NORMSP_0:def 5, XCMPLX_1:87 ;
A21: ||.(((s1 / 2) / ||.y.||) * y).|| = |.((s1 / 2) / ||.y.||).| * ||.y.|| by NORMSP_1:def 1
.= ((s1 / 2) / ||.y.||) * ||.y.|| by A7, COMPLEX1:43
.= s1 / 2 by C16, NORMSP_0:def 5, XCMPLX_1:87 ;
A23: f . ((((s1 / 2) / ||.x.||) * x),(((s1 / 2) / ||.y.||) * y)) = ((s1 / 2) / ||.x.||) * (f . (x,(((s1 / 2) / ||.y.||) * y))) by LM8;
f . (x,(((s1 / 2) / ||.y.||) * y)) = ((s1 / 2) / ||.y.||) * (f . (x,y)) by LM8;
then A24: f . ((((s1 / 2) / ||.x.||) * x),(((s1 / 2) / ||.y.||) * y)) = (((s1 / 2) / ||.x.||) * ((s1 / 2) / ||.y.||)) * (f . (x,y)) by A23, RLVECT_1:def 7
.= (((s1 / 2) * (s1 / 2)) / (||.x.|| * ||.y.||)) * (f . (x,y)) by XCMPLX_1:76 ;
A25: 0 < ||.x.|| * ||.y.|| by A17, XREAL_1:129;
||.(f . ((((s1 / 2) / ||.x.||) * x),(((s1 / 2) / ||.y.||) * y))).|| = |.(((s1 / 2) * (s1 / 2)) / (||.x.|| * ||.y.||)).| * ||.(f . (x,y)).|| by A24, NORMSP_1:def 1
.= (((s1 / 2) * (s1 / 2)) / (||.x.|| * ||.y.||)) * ||.(f . (x,y)).|| by A7, COMPLEX1:43 ;
then A28: (((s1 / 2) * (s1 / 2)) / (||.x.|| * ||.y.||)) * ||.(f . (x,y)).|| < 1 by A9, A19, A21;
((((s1 / 2) * (s1 / 2)) / (||.x.|| * ||.y.||)) * ||.(f . (x,y)).||) * (||.x.|| * ||.y.||) <= 1 * (||.x.|| * ||.y.||) by A28, XREAL_1:64;
then ((((s1 / 2) * (s1 / 2)) / (||.x.|| * ||.y.||)) * (||.x.|| * ||.y.||)) * ||.(f . (x,y)).|| <= ||.x.|| * ||.y.|| ;
then ((s1 / 2) * (s1 / 2)) * ||.(f . (x,y)).|| <= ||.x.|| * ||.y.|| by A25, XCMPLX_1:87;
then (((s1 / 2) * (s1 / 2)) * ||.(f . (x,y)).||) / ((s1 / 2) * (s1 / 2)) <= (||.x.|| * ||.y.||) / ((s1 / 2) * (s1 / 2)) by A7, XREAL_1:72;
then ||.(f . (x,y)).|| <= (||.x.|| * ||.y.||) / ((s1 / 2) * (s1 / 2)) by A14, XCMPLX_1:89;
then ||.(f . (x,y)).|| <= (1 / ((s1 / 2) * (s1 / 2))) * (||.x.|| * ||.y.||) by XCMPLX_1:99;
hence ||.(f . (x,y)).|| <= (K * ||.x.||) * ||.y.|| ; :: thesis: verum

end;

suppose A29: ( x = 0. E or y = 0. F ) ; :: thesis: ||.(f . (x,y)).|| <= (K * ||.x.||) * ||.y.||

then ( ||.x.|| = 0 or ||.y.|| = 0 ) ;
hence ||.(f . (x,y)).|| <= (K * ||.x.||) * ||.y.|| by A15, A16, A29; :: thesis: verum

end;

end;

end;

end;

( ex K being Real st
( 0 <= K & ( for x being Point of E
for y being Point of F holds ||.(f . (x,y)).|| <= (K * ||.x.||) * ||.y.|| ) ) implies f is_continuous_on the carrier of [:E,F:] )

proof

given K being Real such that A32: ( 0 <= K & ( for x being Point of E
for y being Point of F holds ||.(f . (x,y)).|| <= (K * ||.x.||) * ||.y.|| ) ) ; :: thesis: f is_continuous_on the carrier of [:E,F:]
A33: the carrier of [:E,F:] c= dom f by FUNCT_2:def 1;
for z0 being Point of [:E,F:]
for r1 being Real st z0 in the carrier of [:E,F:] & 0 < r1 holds
ex s being Real st
( 0 < s & ( for z1 being Point of [:E,F:] st z1 in the carrier of [:E,F:] & ||.(z1 - z0).|| < s holds
||.((f /. z1) - (f /. z0)).|| < r1 ) )

proof

let z0 be Point of [:E,F:]; :: thesis: for r1 being Real st z0 in the carrier of [:E,F:] & 0 < r1 holds
ex s being Real st
( 0 < s & ( for z1 being Point of [:E,F:] st z1 in the carrier of [:E,F:] & ||.(z1 - z0).|| < s holds
||.((f /. z1) - (f /. z0)).|| < r1 ) )
let r1 be Real; :: thesis: ( z0 in the carrier of [:E,F:] & 0 < r1 implies ex s being Real st
( 0 < s & ( for z1 being Point of [:E,F:] st z1 in the carrier of [:E,F:] & ||.(z1 - z0).|| < s holds
||.((f /. z1) - (f /. z0)).|| < r1 ) ) )
assume A34: ( z0 in the carrier of [:E,F:] & 0 < r1 ) ; :: thesis: ex s being Real st
( 0 < s & ( for z1 being Point of [:E,F:] st z1 in the carrier of [:E,F:] & ||.(z1 - z0).|| < s holds
||.((f /. z1) - (f /. z0)).|| < r1 ) )
set r = r1 / 2;
A35: ( 0 < r1 / 2 & r1 / 2 < r1 ) by A34, XREAL_1:215, XREAL_1:216;
consider x0 being Point of E, y0 being Point of F such that
A36: z0 = [x0,y0] by PRVECT_3:18;
set KXY0 = (K + 1) * ((||.x0.|| + 1) + ||.y0.||);
set s1 = (r1 / 2) / ((K + 1) * ((||.x0.|| + 1) + ||.y0.||));
K + 0 < K + 1 by XREAL_1:8;
then A39: K * ((||.x0.|| + 1) + ||.y0.||) < (K + 1) * ((||.x0.|| + 1) + ||.y0.||) by XREAL_1:68;
A40: 0 < (K + 1) * ((||.x0.|| + 1) + ||.y0.||) by A32, XREAL_1:129;
then A41: 0 < (r1 / 2) / ((K + 1) * ((||.x0.|| + 1) + ||.y0.||)) by A35, XREAL_1:139;
set s = min (((r1 / 2) / ((K + 1) * ((||.x0.|| + 1) + ||.y0.||))),1);
A42: ( min (((r1 / 2) / ((K + 1) * ((||.x0.|| + 1) + ||.y0.||))),1) <= 1 & min (((r1 / 2) / ((K + 1) * ((||.x0.|| + 1) + ||.y0.||))),1) <= (r1 / 2) / ((K + 1) * ((||.x0.|| + 1) + ||.y0.||)) ) by XXREAL_0:17;
A43: 0 < min (((r1 / 2) / ((K + 1) * ((||.x0.|| + 1) + ||.y0.||))),1) by A41, XXREAL_0:21;
then A44: (K * ((||.x0.|| + 1) + ||.y0.||)) * (min (((r1 / 2) / ((K + 1) * ((||.x0.|| + 1) + ||.y0.||))),1)) <= ((K + 1) * ((||.x0.|| + 1) + ||.y0.||)) * ((r1 / 2) / ((K + 1) * ((||.x0.|| + 1) + ||.y0.||))) by A32, A39, A42, XREAL_1:66;
take min (((r1 / 2) / ((K + 1) * ((||.x0.|| + 1) + ||.y0.||))),1) ; :: thesis: ( 0 < min (((r1 / 2) / ((K + 1) * ((||.x0.|| + 1) + ||.y0.||))),1) & ( for z1 being Point of [:E,F:] st z1 in the carrier of [:E,F:] & ||.(z1 - z0).|| < min (((r1 / 2) / ((K + 1) * ((||.x0.|| + 1) + ||.y0.||))),1) holds
||.((f /. z1) - (f /. z0)).|| < r1 ) )
thus 0 < min (((r1 / 2) / ((K + 1) * ((||.x0.|| + 1) + ||.y0.||))),1) by A41, XXREAL_0:21; :: thesis: for z1 being Point of [:E,F:] st z1 in the carrier of [:E,F:] & ||.(z1 - z0).|| < min (((r1 / 2) / ((K + 1) * ((||.x0.|| + 1) + ||.y0.||))),1) holds
||.((f /. z1) - (f /. z0)).|| < r1
let z1 be Point of [:E,F:]; :: thesis: ( z1 in the carrier of [:E,F:] & ||.(z1 - z0).|| < min (((r1 / 2) / ((K + 1) * ((||.x0.|| + 1) + ||.y0.||))),1) implies ||.((f /. z1) - (f /. z0)).|| < r1 )
assume A45: ( z1 in the carrier of [:E,F:] & ||.(z1 - z0).|| < min (((r1 / 2) / ((K + 1) * ((||.x0.|| + 1) + ||.y0.||))),1) ) ; :: thesis: ||.((f /. z1) - (f /. z0)).|| < r1
consider x1 being Point of E, y1 being Point of F such that
A46: z1 = [x1,y1] by PRVECT_3:18;
A47: (f . z1) - (f . z0) = (((f . (x1,y1)) - (f . (x0,y1))) + (f . (x0,y1))) - (f . (x0,y0)) by A36, A46, RLVECT_4:1
.= ((f . (x1,y1)) - (f . (x0,y1))) + ((f . (x0,y1)) - (f . (x0,y0))) by RLVECT_1:28 ;
A49: (f . (x1,y1)) - (f . (x0,y1)) = (f . (x1,y1)) + ((- 1) * (f . (x0,y1))) by RLVECT_1:16
.= (f . (x1,y1)) + (f . (((- 1) * x0),y1)) by LM8
.= f . ((x1 + ((- 1) * x0)),y1) by LM8
.= f . ((x1 - x0),y1) by RLVECT_1:16 ;
A51: (f . (x0,y1)) - (f . (x0,y0)) = (f . (x0,y1)) + ((- 1) * (f . (x0,y0))) by RLVECT_1:16
.= (f . (x0,y1)) + (f . (x0,((- 1) * y0))) by LM8
.= f . (x0,(y1 + ((- 1) * y0))) by LM8
.= f . (x0,(y1 - y0)) by RLVECT_1:16 ;
A52: ||.(f . ((x1 - x0),y1)).|| <= (K * ||.(x1 - x0).||) * ||.y1.|| by A32;
A53: ||.(f . (x0,(y1 - y0))).|| <= (K * ||.x0.||) * ||.(y1 - y0).|| by A32;
- z0 = [(- x0),(- y0)] by A36, PRVECT_3:18;
then A54: z1 - z0 = [(x1 - x0),(y1 - y0)] by A46, PRVECT_3:18;
then ||.(x1 - x0).|| <= ||.(z1 - z0).|| by NDIFF_8:21;
then A55: ||.(x1 - x0).|| < min (((r1 / 2) / ((K + 1) * ((||.x0.|| + 1) + ||.y0.||))),1) by A45, XXREAL_0:2;
||.(y1 - y0).|| <= ||.(z1 - z0).|| by A54, NDIFF_8:21;
then A56: ||.(y1 - y0).|| < min (((r1 / 2) / ((K + 1) * ((||.x0.|| + 1) + ||.y0.||))),1) by A45, XXREAL_0:2;
||.(x1 - x0).|| * ||.y1.|| <= (min (((r1 / 2) / ((K + 1) * ((||.x0.|| + 1) + ||.y0.||))),1)) * ||.y1.|| by A55, XREAL_1:64;
then K * (||.(x1 - x0).|| * ||.y1.||) <= K * ((min (((r1 / 2) / ((K + 1) * ((||.x0.|| + 1) + ||.y0.||))),1)) * ||.y1.||) by A32, XREAL_1:64;
then A57: ||.(f . ((x1 - x0),y1)).|| <= (K * (min (((r1 / 2) / ((K + 1) * ((||.x0.|| + 1) + ||.y0.||))),1))) * ||.y1.|| by A52, XXREAL_0:2;
||.(y1 - y0).|| * ||.x0.|| <= (min (((r1 / 2) / ((K + 1) * ((||.x0.|| + 1) + ||.y0.||))),1)) * ||.x0.|| by A56, XREAL_1:64;
then K * (||.x0.|| * ||.(y1 - y0).||) <= K * ((min (((r1 / 2) / ((K + 1) * ((||.x0.|| + 1) + ||.y0.||))),1)) * ||.x0.||) by A32, XREAL_1:64;
then ||.(f . (x0,(y1 - y0))).|| <= (K * (min (((r1 / 2) / ((K + 1) * ((||.x0.|| + 1) + ||.y0.||))),1))) * ||.x0.|| by A53, XXREAL_0:2;
then A58: ||.(f . ((x1 - x0),y1)).|| + ||.(f . (x0,(y1 - y0))).|| <= ((K * (min (((r1 / 2) / ((K + 1) * ((||.x0.|| + 1) + ||.y0.||))),1))) * ||.y1.||) + ((K * (min (((r1 / 2) / ((K + 1) * ((||.x0.|| + 1) + ||.y0.||))),1))) * ||.x0.||) by A57, XREAL_1:7;
||.y1.|| = ||.((y1 - y0) + y0).|| by RLVECT_4:1;
then A60: ||.y1.|| <= ||.(y1 - y0).|| + ||.y0.|| by NORMSP_1:def 1;
||.(y1 - y0).|| + ||.y0.|| <= (min (((r1 / 2) / ((K + 1) * ((||.x0.|| + 1) + ||.y0.||))),1)) + ||.y0.|| by A56, XREAL_1:7;
then A61: ||.y1.|| <= (min (((r1 / 2) / ((K + 1) * ((||.x0.|| + 1) + ||.y0.||))),1)) + ||.y0.|| by A60, XXREAL_0:2;
(min (((r1 / 2) / ((K + 1) * ((||.x0.|| + 1) + ||.y0.||))),1)) + ||.y0.|| <= 1 + ||.y0.|| by A42, XREAL_1:7;
then ||.y1.|| <= 1 + ||.y0.|| by A61, XXREAL_0:2;
then ||.y1.|| + ||.x0.|| <= (1 + ||.y0.||) + ||.x0.|| by XREAL_1:7;
then (min (((r1 / 2) / ((K + 1) * ((||.x0.|| + 1) + ||.y0.||))),1)) * (||.y1.|| + ||.x0.||) <= (min (((r1 / 2) / ((K + 1) * ((||.x0.|| + 1) + ||.y0.||))),1)) * ((1 + ||.y0.||) + ||.x0.||) by A43, XREAL_1:64;
then ((min (((r1 / 2) / ((K + 1) * ((||.x0.|| + 1) + ||.y0.||))),1)) * (||.y1.|| + ||.x0.||)) * K <= ((min (((r1 / 2) / ((K + 1) * ((||.x0.|| + 1) + ||.y0.||))),1)) * ((1 + ||.y0.||) + ||.x0.||)) * K by A32, XREAL_1:64;
then ||.(f . ((x1 - x0),y1)).|| + ||.(f . (x0,(y1 - y0))).|| <= (K * (min (((r1 / 2) / ((K + 1) * ((||.x0.|| + 1) + ||.y0.||))),1))) * ((||.x0.|| + 1) + ||.y0.||) by A58, XXREAL_0:2;
then ||.(f . ((x1 - x0),y1)).|| + ||.(f . (x0,(y1 - y0))).|| <= ((K + 1) * ((||.x0.|| + 1) + ||.y0.||)) * ((r1 / 2) / ((K + 1) * ((||.x0.|| + 1) + ||.y0.||))) by A44, XXREAL_0:2;
then A64: ||.(f . ((x1 - x0),y1)).|| + ||.(f . (x0,(y1 - y0))).|| <= r1 / 2 by A40, XCMPLX_1:87;
||.((f . z1) - (f . z0)).|| <= ||.((f . (x1,y1)) - (f . (x0,y1))).|| + ||.((f . (x0,y1)) - (f . (x0,y0))).|| by A47, NORMSP_1:def 1;
then ||.((f /. z1) - (f /. z0)).|| <= r1 / 2 by A49, A51, A64, XXREAL_0:2;
hence ||.((f /. z1) - (f /. z0)).|| < r1 by A35, XXREAL_0:2; :: thesis: verum

end;

hence f is_continuous_on the carrier of [:E,F:] by A33, NFCONT_1:19; :: thesis: verum

end;

hence ( ( f is_continuous_on the carrier of [:E,F:] implies f is_continuous_in 0. [:E,F:] ) & ( f is_continuous_in 0. [:E,F:] implies f is_continuous_on the carrier of [:E,F:] ) & ( f is_continuous_on the carrier of [:E,F:] implies ex K being Real st
( 0 <= K & ( for x being Point of E
for y being Point of F holds ||.(f . (x,y)).|| <= (K * ||.x.||) * ||.y.|| ) ) ) & ( ex K being Real st
( 0 <= K & ( for x being Point of E
for y being Point of F holds ||.(f . (x,y)).|| <= (K * ||.x.||) * ||.y.|| ) ) implies f is_continuous_on the carrier of [:E,F:] ) ) by A4; :: thesis: verum