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.|| ) ) )

( 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:] )

( 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

( ( 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

( ex K being Real st
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;

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

end;( 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

A14:
0 < (s1 / 2) * (s1 / 2)
by A8, XREAL_1:129;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;

[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 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;||.(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;

[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 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

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
end;

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

end;

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;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

( 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

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
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 ) )

end;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

hence
f is_continuous_on the carrier of [:E,F:]
by A33, NFCONT_1:19; :: thesis: verum
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;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

( 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