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 * ) * ) ) ) & ( ex K being Real st
( 0 <= K & ( for x being Point of E
for y being Point of F holds ||.(f . (x,y)).|| <= (K * ) * ) ) 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 * ) * ) ) ) & ( ex K being Real st
( 0 <= K & ( for x being Point of E
for y being Point of F holds ||.(f . (x,y)).|| <= (K * ) * ) ) 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 * ) * ) ) )
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 * ) * ) )

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 ;
set s2 = s1 / 2;
A8: ( 0 < s1 / 2 & s1 / 2 < s1 ) by ;
A9: now :: thesis: for x being Point of E
for y being Point of F st <= s1 / 2 & <= s1 / 2 holds
||.(f . (x,y)).|| < 1
let x be Point of E; :: thesis: for y being Point of F st <= s1 / 2 & <= s1 / 2 holds
||.(f . (x,y)).|| < 1

let y be Point of F; :: thesis: ( <= s1 / 2 & <= s1 / 2 implies ||.(f . (x,y)).|| < 1 )
assume ( ||.x.|| <= s1 / 2 & <= s1 / 2 ) ; :: thesis: ||.(f . (x,y)).|| < 1
then A10: ( ||.x.|| < s1 & < s1 ) by ;
[x,y] is set by TARSKI:1;
then reconsider z = [x,y] as Point of [:E,F:] by PRVECT_3:18;
||.(x - (0. E)).|| < s1 by ;
then ||.((0. E) - x).|| < s1 by NORMSP_1:7;
then A12: x in Ball ((0. E),s1) ;
||.(y - (0. F)).|| < s1 by ;
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 ;
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 ; :: thesis: verum
end;
A14: 0 < (s1 / 2) * (s1 / 2) by ;
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 * ) * ) )

thus 0 <= K by A7; :: thesis: for x being Point of E
for y being Point of F holds ||.(f . (x,y)).|| <= (K * ) *

let x be Point of E; :: thesis: for y being Point of F holds ||.(f . (x,y)).|| <= (K * ) *
let y be Point of F; :: thesis: ||.(f . (x,y)).|| <= (K * ) *
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 * ) * :: 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 * ) *
then ( ||.x.|| <> 0 & <> 0 ) by NORMSP_0:def 5;
then A17: ( 0 < & 0 < ) ;
set x1 = ((s1 / 2) / ) * x;
set y1 = ((s1 / 2) / ) * y;
A19: ||.(((s1 / 2) / ) * x).|| = |.((s1 / 2) / ).| * by NORMSP_1:def 1
.= ((s1 / 2) / ) * by
.= s1 / 2 by ;
A21: ||.(((s1 / 2) / ) * y).|| = |.((s1 / 2) / ).| * by NORMSP_1:def 1
.= ((s1 / 2) / ) * by
.= s1 / 2 by ;
A23: f . ((((s1 / 2) / ) * x),(((s1 / 2) / ) * y)) = ((s1 / 2) / ) * (f . (x,(((s1 / 2) / ) * y))) by LM8;
f . (x,(((s1 / 2) / ) * y)) = ((s1 / 2) / ) * (f . (x,y)) by LM8;
then A24: f . ((((s1 / 2) / ) * x),(((s1 / 2) / ) * y)) = (((s1 / 2) / ) * ((s1 / 2) / )) * (f . (x,y)) by
.= (((s1 / 2) * (s1 / 2)) / ()) * (f . (x,y)) by XCMPLX_1:76 ;
A25: 0 < * by ;
||.(f . ((((s1 / 2) / ) * x),(((s1 / 2) / ) * y))).|| = |.(((s1 / 2) * (s1 / 2)) / ()).| * ||.(f . (x,y)).|| by
.= (((s1 / 2) * (s1 / 2)) / ()) * ||.(f . (x,y)).|| by ;
then A28: (((s1 / 2) * (s1 / 2)) / ()) * ||.(f . (x,y)).|| < 1 by A9, A19, A21;
((((s1 / 2) * (s1 / 2)) / ()) * ||.(f . (x,y)).||) * () <= 1 * () by ;
then ((((s1 / 2) * (s1 / 2)) / ()) * ()) * ||.(f . (x,y)).|| <= * ;
then ((s1 / 2) * (s1 / 2)) * ||.(f . (x,y)).|| <= * by ;
then (((s1 / 2) * (s1 / 2)) * ||.(f . (x,y)).||) / ((s1 / 2) * (s1 / 2)) <= () / ((s1 / 2) * (s1 / 2)) by ;
then ||.(f . (x,y)).|| <= () / ((s1 / 2) * (s1 / 2)) by ;
then ||.(f . (x,y)).|| <= (1 / ((s1 / 2) * (s1 / 2))) * () by XCMPLX_1:99;
hence ||.(f . (x,y)).|| <= (K * ) * ; :: thesis: verum
end;
suppose A29: ( x = 0. E or y = 0. F ) ; :: thesis: ||.(f . (x,y)).|| <= (K * ) *
then ( ||.x.|| = 0 or = 0 ) ;
hence ||.(f . (x,y)).|| <= (K * ) * by ; :: 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 * ) * ) ) 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 * ) * ) ) ; :: 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 ;
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 ;
then A41: 0 < (r1 / 2) / ((K + 1) * ((||.x0.|| + 1) + ||.y0.||)) by ;
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 ;
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 ;
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 ; :: 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
.= ((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 ;
then A54: z1 - z0 = [(x1 - x0),(y1 - y0)] by ;
then ||.(x1 - x0).|| <= ||.(z1 - z0).|| by NDIFF_8:21;
then A55: ||.(x1 - x0).|| < min (((r1 / 2) / ((K + 1) * ((||.x0.|| + 1) + ||.y0.||))),1) by ;
||.(y1 - y0).|| <= ||.(z1 - z0).|| by ;
then A56: ||.(y1 - y0).|| < min (((r1 / 2) / ((K + 1) * ((||.x0.|| + 1) + ||.y0.||))),1) by ;
||.(x1 - x0).|| * ||.y1.|| <= (min (((r1 / 2) / ((K + 1) * ((||.x0.|| + 1) + ||.y0.||))),1)) * ||.y1.|| by ;
then K * (||.(x1 - x0).|| * ||.y1.||) <= K * ((min (((r1 / 2) / ((K + 1) * ((||.x0.|| + 1) + ||.y0.||))),1)) * ||.y1.||) by ;
then A57: ||.(f . ((x1 - x0),y1)).|| <= (K * (min (((r1 / 2) / ((K + 1) * ((||.x0.|| + 1) + ||.y0.||))),1))) * ||.y1.|| by ;
||.(y1 - y0).|| * ||.x0.|| <= (min (((r1 / 2) / ((K + 1) * ((||.x0.|| + 1) + ||.y0.||))),1)) * ||.x0.|| by ;
then K * (||.x0.|| * ||.(y1 - y0).||) <= K * ((min (((r1 / 2) / ((K + 1) * ((||.x0.|| + 1) + ||.y0.||))),1)) * ||.x0.||) by ;
then ||.(f . (x0,(y1 - y0))).|| <= (K * (min (((r1 / 2) / ((K + 1) * ((||.x0.|| + 1) + ||.y0.||))),1))) * ||.x0.|| by ;
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 ;
||.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 ;
then A61: ||.y1.|| <= (min (((r1 / 2) / ((K + 1) * ((||.x0.|| + 1) + ||.y0.||))),1)) + ||.y0.|| by ;
(min (((r1 / 2) / ((K + 1) * ((||.x0.|| + 1) + ||.y0.||))),1)) + ||.y0.|| <= 1 + ||.y0.|| by ;
then ||.y1.|| <= 1 + ||.y0.|| by ;
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 ;
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 ;
then ||.(f . ((x1 - x0),y1)).|| + ||.(f . (x0,(y1 - y0))).|| <= (K * (min (((r1 / 2) / ((K + 1) * ((||.x0.|| + 1) + ||.y0.||))),1))) * ((||.x0.|| + 1) + ||.y0.||) by ;
then ||.(f . ((x1 - x0),y1)).|| + ||.(f . (x0,(y1 - y0))).|| <= ((K + 1) * ((||.x0.|| + 1) + ||.y0.||)) * ((r1 / 2) / ((K + 1) * ((||.x0.|| + 1) + ||.y0.||))) by ;
then A64: ||.(f . ((x1 - x0),y1)).|| + ||.(f . (x0,(y1 - y0))).|| <= r1 / 2 by ;
||.((f . z1) - (f . z0)).|| <= ||.((f . (x1,y1)) - (f . (x0,y1))).|| + ||.((f . (x0,y1)) - (f . (x0,y0))).|| by ;
then ||.((f /. z1) - (f /. z0)).|| <= r1 / 2 by ;
hence ||.((f /. z1) - (f /. z0)).|| < r1 by ; :: thesis: verum
end;
hence f is_continuous_on the carrier of [:E,F:] by ; :: 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 * ) * ) ) ) & ( ex K being Real st
( 0 <= K & ( for x being Point of E
for y being Point of F holds ||.(f . (x,y)).|| <= (K * ) * ) ) implies f is_continuous_on the carrier of [:E,F:] ) ) by A4; :: thesis: verum