let X be RealNormSpace-Sequence; :: thesis: for Y being RealNormSpace

for f being MultilinearOperator of X,Y holds

( ( f is_continuous_on the carrier of (product X) implies f is_continuous_in 0. (product X) ) & ( f is_continuous_in 0. (product X) implies f is_continuous_on the carrier of (product X) ) & ( f is_continuous_on the carrier of (product X) implies f is Lipschitzian ) & ( f is Lipschitzian implies f is_continuous_on the carrier of (product X) ) )

let Y be RealNormSpace; :: thesis: for f being MultilinearOperator of X,Y holds

( ( f is_continuous_on the carrier of (product X) implies f is_continuous_in 0. (product X) ) & ( f is_continuous_in 0. (product X) implies f is_continuous_on the carrier of (product X) ) & ( f is_continuous_on the carrier of (product X) implies f is Lipschitzian ) & ( f is Lipschitzian implies f is_continuous_on the carrier of (product X) ) )

let f be MultilinearOperator of X,Y; :: thesis: ( ( f is_continuous_on the carrier of (product X) implies f is_continuous_in 0. (product X) ) & ( f is_continuous_in 0. (product X) implies f is_continuous_on the carrier of (product X) ) & ( f is_continuous_on the carrier of (product X) implies f is Lipschitzian ) & ( f is Lipschitzian implies f is_continuous_on the carrier of (product X) ) )

A1: dom f = the carrier of (product X) by FUNCT_2:def 1;

A2: f /. (0. (product X)) = 0. Y by FXZER;

A3: product X = NORMSTR(# (product (carr X)),(zeros X),[:(addop X):],[:(multop X):],(productnorm X) #) by PRVECT_2:6;

A4: ( f is_continuous_in 0. (product X) implies f is Lipschitzian )

for f being MultilinearOperator of X,Y holds

( ( f is_continuous_on the carrier of (product X) implies f is_continuous_in 0. (product X) ) & ( f is_continuous_in 0. (product X) implies f is_continuous_on the carrier of (product X) ) & ( f is_continuous_on the carrier of (product X) implies f is Lipschitzian ) & ( f is Lipschitzian implies f is_continuous_on the carrier of (product X) ) )

let Y be RealNormSpace; :: thesis: for f being MultilinearOperator of X,Y holds

( ( f is_continuous_on the carrier of (product X) implies f is_continuous_in 0. (product X) ) & ( f is_continuous_in 0. (product X) implies f is_continuous_on the carrier of (product X) ) & ( f is_continuous_on the carrier of (product X) implies f is Lipschitzian ) & ( f is Lipschitzian implies f is_continuous_on the carrier of (product X) ) )

let f be MultilinearOperator of X,Y; :: thesis: ( ( f is_continuous_on the carrier of (product X) implies f is_continuous_in 0. (product X) ) & ( f is_continuous_in 0. (product X) implies f is_continuous_on the carrier of (product X) ) & ( f is_continuous_on the carrier of (product X) implies f is Lipschitzian ) & ( f is Lipschitzian implies f is_continuous_on the carrier of (product X) ) )

A1: dom f = the carrier of (product X) by FUNCT_2:def 1;

A2: f /. (0. (product X)) = 0. Y by FXZER;

A3: product X = NORMSTR(# (product (carr X)),(zeros X),[:(addop X):],[:(multop X):],(productnorm X) #) by PRVECT_2:6;

A4: ( f is_continuous_in 0. (product X) implies f is Lipschitzian )

proof

( f is Lipschitzian implies f is_continuous_on the carrier of (product X) )
assume
f is_continuous_in 0. (product X)
; :: thesis: f is Lipschitzian

then consider s being Real such that

A5: ( 0 < s & ( for z being Point of (product X) st z in dom f & ||.(z - (0. (product X))).|| < s holds

||.((f /. z) - (f /. (0. (product X)))).|| < 1 ) ) by NFCONT_1:7;

set z = 0. (product X);

consider s1 being FinSequence of REAL , Balls being non-empty non empty FinSequence such that

A6: ( dom s1 = dom X & dom X = dom Balls & product Balls c= Ball ((0. (product X)),s) & ( for i being Element of dom X holds

( 0 < s1 . i & s1 . i < s & Balls . i = Ball (((0. (product X)) . i),(s1 . i)) ) ) ) by A5, NDIFF824;

defpred S_{1}[ object , object ] means ex i being Element of dom X st

( $1 = i & $2 = (s1 . i) / 2 );

A7: for n being Nat st n in Seg (len X) holds

ex d being Element of REAL st S_{1}[n,d]

A8: ( len s2 = len X & ( for n being Nat st n in Seg (len X) holds

S_{1}[n,s2 /. n] ) )
from FINSEQ_4:sch 1(A7);

A9: dom s2 = Seg (len X) by A8, FINSEQ_1:def 3

.= dom X by FINSEQ_1:def 3 ;

A11: for i being Element of dom X holds s2 . i = (s1 . i) / 2

( 0 < s2 . i & s2 . i < s1 . i )

then A13: len s2 = len X by FINSEQ_1:def 3;

set K = 1 / (Product s2);

end;then consider s being Real such that

A5: ( 0 < s & ( for z being Point of (product X) st z in dom f & ||.(z - (0. (product X))).|| < s holds

||.((f /. z) - (f /. (0. (product X)))).|| < 1 ) ) by NFCONT_1:7;

set z = 0. (product X);

consider s1 being FinSequence of REAL , Balls being non-empty non empty FinSequence such that

A6: ( dom s1 = dom X & dom X = dom Balls & product Balls c= Ball ((0. (product X)),s) & ( for i being Element of dom X holds

( 0 < s1 . i & s1 . i < s & Balls . i = Ball (((0. (product X)) . i),(s1 . i)) ) ) ) by A5, NDIFF824;

defpred S

( $1 = i & $2 = (s1 . i) / 2 );

A7: for n being Nat st n in Seg (len X) holds

ex d being Element of REAL st S

proof

consider s2 being FinSequence of REAL such that
let n be Nat; :: thesis: ( n in Seg (len X) implies ex d being Element of REAL st S_{1}[n,d] )

assume n in Seg (len X) ; :: thesis: ex d being Element of REAL st S_{1}[n,d]

then reconsider i = n as Element of dom X by FINSEQ_1:def 3;

reconsider si = (s1 . i) / 2 as Element of REAL by XREAL_0:def 1;

take si ; :: thesis: S_{1}[n,si]

thus S_{1}[n,si]
; :: thesis: verum

end;assume n in Seg (len X) ; :: thesis: ex d being Element of REAL st S

then reconsider i = n as Element of dom X by FINSEQ_1:def 3;

reconsider si = (s1 . i) / 2 as Element of REAL by XREAL_0:def 1;

take si ; :: thesis: S

thus S

A8: ( len s2 = len X & ( for n being Nat st n in Seg (len X) holds

S

A9: dom s2 = Seg (len X) by A8, FINSEQ_1:def 3

.= dom X by FINSEQ_1:def 3 ;

A11: for i being Element of dom X holds s2 . i = (s1 . i) / 2

proof

A12:
for i being Element of dom X holds
let i be Element of dom X; :: thesis: s2 . i = (s1 . i) / 2

i in dom X ;

then i in Seg (len X) by FINSEQ_1:def 3;

then ex j being Element of dom X st

( i = j & s2 /. i = (s1 . j) / 2 ) by A8;

hence s2 . i = (s1 . i) / 2 by A9, PARTFUN1:def 6; :: thesis: verum

end;i in dom X ;

then i in Seg (len X) by FINSEQ_1:def 3;

then ex j being Element of dom X st

( i = j & s2 /. i = (s1 . j) / 2 ) by A8;

hence s2 . i = (s1 . i) / 2 by A9, PARTFUN1:def 6; :: thesis: verum

( 0 < s2 . i & s2 . i < s1 . i )

proof

dom s2 = Seg (len X)
by A9, FINSEQ_1:def 3;
let i be Element of dom X; :: thesis: ( 0 < s2 . i & s2 . i < s1 . i )

( s2 . i = (s1 . i) / 2 & 0 < s1 . i ) by A6, A11;

hence ( 0 < s2 . i & s2 . i < s1 . i ) by XREAL_1:216; :: thesis: verum

end;( s2 . i = (s1 . i) / 2 & 0 < s1 . i ) by A6, A11;

hence ( 0 < s2 . i & s2 . i < s1 . i ) by XREAL_1:216; :: thesis: verum

then A13: len s2 = len X by FINSEQ_1:def 3;

A14: now :: thesis: for x being Point of (product X) st ( for i being Element of dom X holds ||.(x . i).|| <= s2 . i ) holds

||.(f /. x).|| < 1

A21:
0 < Product s2
by A9, A12, PSPROD;||.(f /. x).|| < 1

let x be Point of (product X); :: thesis: ( ( for i being Element of dom X holds ||.(x . i).|| <= s2 . i ) implies ||.(f /. x).|| < 1 )

assume A15: for i being Element of dom X holds ||.(x . i).|| <= s2 . i ; :: thesis: ||.(f /. x).|| < 1

ex g being Function st

( x = g & dom g = dom (carr X) & ( for i being object st i in dom (carr X) holds

g . i in (carr X) . i ) ) by A3, CARD_3:def 5;

then A16: dom x = dom X by DCARXX;

then x in Ball ((0. (product X)),s) by A6;

then ex p being Point of (product X) st

( x = p & ||.((0. (product X)) - p).|| < s ) ;

then A20: ||.(x - (0. (product X))).|| < s by NORMSP_1:7;

||.((f /. x) - (f /. (0. (product X)))).|| < 1 by A1, A5, A20;

hence ||.(f /. x).|| < 1 by A2; :: thesis: verum

end;assume A15: for i being Element of dom X holds ||.(x . i).|| <= s2 . i ; :: thesis: ||.(f /. x).|| < 1

ex g being Function st

( x = g & dom g = dom (carr X) & ( for i being object st i in dom (carr X) holds

g . i in (carr X) . i ) ) by A3, CARD_3:def 5;

then A16: dom x = dom X by DCARXX;

now :: thesis: for i0 being object st i0 in dom X holds

x . i0 in Balls . i0

then
x in product Balls
by A6, A16, CARD_3:def 5;x . i0 in Balls . i0

let i0 be object ; :: thesis: ( i0 in dom X implies x . i0 in Balls . i0 )

assume i0 in dom X ; :: thesis: x . i0 in Balls . i0

then reconsider i = i0 as Element of dom X ;

A18: (0. (product X)) . i = 0. (X . i) by ZERXI;

||.((x . i) - (0. (X . i))).|| <= s2 . i by A15;

then A19: ||.((0. (X . i)) - (x . i)).|| <= s2 . i by NORMSP_1:7;

( s2 . i = (s1 . i) / 2 & 0 < s1 . i ) by A6, A11;

then ( 0 < s2 . i & s2 . i < s1 . i ) by XREAL_1:216;

then ||.((0. (X . i)) - (x . i)).|| < s1 . i by A19, XXREAL_0:2;

then x . i in Ball ((0. (X . i)),(s1 . i)) ;

hence x . i0 in Balls . i0 by A6, A18; :: thesis: verum

end;assume i0 in dom X ; :: thesis: x . i0 in Balls . i0

then reconsider i = i0 as Element of dom X ;

A18: (0. (product X)) . i = 0. (X . i) by ZERXI;

||.((x . i) - (0. (X . i))).|| <= s2 . i by A15;

then A19: ||.((0. (X . i)) - (x . i)).|| <= s2 . i by NORMSP_1:7;

( s2 . i = (s1 . i) / 2 & 0 < s1 . i ) by A6, A11;

then ( 0 < s2 . i & s2 . i < s1 . i ) by XREAL_1:216;

then ||.((0. (X . i)) - (x . i)).|| < s1 . i by A19, XXREAL_0:2;

then x . i in Ball ((0. (X . i)),(s1 . i)) ;

hence x . i0 in Balls . i0 by A6, A18; :: thesis: verum

then x in Ball ((0. (product X)),s) by A6;

then ex p being Point of (product X) st

( x = p & ||.((0. (product X)) - p).|| < s ) ;

then A20: ||.(x - (0. (product X))).|| < s by NORMSP_1:7;

||.((f /. x) - (f /. (0. (product X)))).|| < 1 by A1, A5, A20;

hence ||.(f /. x).|| < 1 by A2; :: thesis: verum

set K = 1 / (Product s2);

now :: thesis: for x being Point of (product X) holds ||.(f . x).|| <= (1 / (Product s2)) * (NrProduct x)

hence
f is Lipschitzian
by A21; :: thesis: verumlet x be Point of (product X); :: thesis: ||.(f . x).|| <= (1 / (Product s2)) * (NrProduct x)

consider F being FinSequence of REAL such that

A23: ( dom F = dom X & ( for i being Element of dom X holds F . i = ||.(x . i).|| ) & NrProduct x = Product F ) by LOPBAN10:def 9;

thus ||.(f . x).|| <= (1 / (Product s2)) * (NrProduct x) :: thesis: verum

end;consider F being FinSequence of REAL such that

A23: ( dom F = dom X & ( for i being Element of dom X holds F . i = ||.(x . i).|| ) & NrProduct x = Product F ) by LOPBAN10:def 9;

thus ||.(f . x).|| <= (1 / (Product s2)) * (NrProduct x) :: thesis: verum

proof
end;

per cases
( for i being Element of dom X holds x . i <> 0. (X . i) or ex i being Element of dom X st x . i = 0. (X . i) )
;

end;

suppose A24:
for i being Element of dom X holds x . i <> 0. (X . i)
; :: thesis: ||.(f . x).|| <= (1 / (Product s2)) * (NrProduct x)

then A25:
0 < NrProduct x
by LOPBAN10:27;

consider d being FinSequence of REAL such that

A26: ( dom d = dom X & ( for i being Element of dom X holds d . i = ||.(x . i).|| " ) ) by LOPBAN10:37;

dom d = Seg (len X) by A26, FINSEQ_1:def 3;

then A27: len d = len X by FINSEQ_1:def 3;

set F1 = mlt (s2,d);

A28: for i being Element of dom F holds d . i = (F . i) "

.= dom X ;

( s2 is Element of (len X) -tuples_on REAL & d is Element of (len X) -tuples_on REAL ) by A13, A27, FINSEQ_2:92;

then A33: Product (mlt (s2,d)) = (Product s2) * (Product d) by RVSUM_1:107

.= (Product s2) * ((Product F) ") by A23, A26, LOPBAN10:40, A28 ;

consider x1 being Element of (product X) such that

A34: for i being Element of dom X holds x1 . i = ((mlt (s2,d)) /. i) * (x . i) by LOPBAN10:38;

A35: for i being Element of dom X holds ||.(x1 . i).|| <= s2 . i

A45: |.((Product F) ").| = (Product F) " by A23, ABSVALUE:def 1;

A46: |.((Product s2) * ((Product F) ")).| = |.(Product s2).| * |.((Product F) ").| by COMPLEX1:65

.= (Product s2) * ((Product F) ") by A21, A45, COMPLEX1:43 ;

f . x1 = ((Product s2) * ((Product F) ")) * (f . x) by A32, A33, A34, LOPBAN10:39;

then ||.(f . x1).|| = ((Product s2) * ((Product F) ")) * ||.(f . x).|| by A46, NORMSP_1:def 1;

then ((Product s2) * (((Product F) ") * ||.(f . x).||)) / (Product s2) < 1 / (Product s2) by A21, A44, XREAL_1:74;

then ((Product F) ") * ||.(f . x).|| < 1 / (Product s2) by A21, XCMPLX_1:89;

then (Product F) * (((Product F) ") * ||.(f . x).||) < (1 / (Product s2)) * (Product F) by A23, A25, XREAL_1:68;

then ((Product F) * ((Product F) ")) * ||.(f . x).|| < (1 / (Product s2)) * (Product F) ;

then 1 * ||.(f . x).|| < (1 / (Product s2)) * (Product F) by A23, A25, XCMPLX_0:def 7;

hence ||.(f . x).|| <= (1 / (Product s2)) * (NrProduct x) by A23; :: thesis: verum

end;consider d being FinSequence of REAL such that

A26: ( dom d = dom X & ( for i being Element of dom X holds d . i = ||.(x . i).|| " ) ) by LOPBAN10:37;

dom d = Seg (len X) by A26, FINSEQ_1:def 3;

then A27: len d = len X by FINSEQ_1:def 3;

set F1 = mlt (s2,d);

A28: for i being Element of dom F holds d . i = (F . i) "

proof

A32: dom (mlt (s2,d)) =
(dom X) /\ (dom X)
by A9, A26, VALUED_1:def 4
let i be Element of dom F; :: thesis: d . i = (F . i) "

reconsider j = i as Element of dom X by A23;

d . j = ||.(x . j).|| " by A26;

hence d . i = (F . i) " by A23; :: thesis: verum

end;reconsider j = i as Element of dom X by A23;

d . j = ||.(x . j).|| " by A26;

hence d . i = (F . i) " by A23; :: thesis: verum

.= dom X ;

( s2 is Element of (len X) -tuples_on REAL & d is Element of (len X) -tuples_on REAL ) by A13, A27, FINSEQ_2:92;

then A33: Product (mlt (s2,d)) = (Product s2) * (Product d) by RVSUM_1:107

.= (Product s2) * ((Product F) ") by A23, A26, LOPBAN10:40, A28 ;

consider x1 being Element of (product X) such that

A34: for i being Element of dom X holds x1 . i = ((mlt (s2,d)) /. i) * (x . i) by LOPBAN10:38;

A35: for i being Element of dom X holds ||.(x1 . i).|| <= s2 . i

proof

A44:
||.(f /. x1).|| < 1
by A14, A35;
let i be Element of dom X; :: thesis: ||.(x1 . i).|| <= s2 . i

A36: x1 . i = ((mlt (s2,d)) /. i) * (x . i) by A34;

A37: (mlt (s2,d)) /. i = (mlt (s2,d)) . i by A32, PARTFUN1:def 6

.= (s2 . i) * (d . i) by RVSUM_1:60

.= (s2 . i) * ((F . i) ") by A23, A28 ;

A39: x1 . i = ((s2 . i) * (||.(x . i).|| ")) * (x . i) by A23, A36, A37;

A41: 0 <= s2 . i by A12;

A42: |.((s2 . i) * (||.(x . i).|| ")).| = (s2 . i) * (||.(x . i).|| ") by A41, COMPLEX1:43;

x . i <> 0. (X . i) by A24;

then A43: ||.(x . i).|| <> 0 by NORMSP_0:def 5;

||.(x1 . i).|| = ((s2 . i) * (||.(x . i).|| ")) * ||.(x . i).|| by A39, A42, NORMSP_1:def 1

.= (s2 . i) * ((||.(x . i).|| ") * ||.(x . i).||)

.= (s2 . i) * 1 by A43, XCMPLX_0:def 7 ;

hence ||.(x1 . i).|| <= s2 . i ; :: thesis: verum

end;A36: x1 . i = ((mlt (s2,d)) /. i) * (x . i) by A34;

A37: (mlt (s2,d)) /. i = (mlt (s2,d)) . i by A32, PARTFUN1:def 6

.= (s2 . i) * (d . i) by RVSUM_1:60

.= (s2 . i) * ((F . i) ") by A23, A28 ;

A39: x1 . i = ((s2 . i) * (||.(x . i).|| ")) * (x . i) by A23, A36, A37;

A41: 0 <= s2 . i by A12;

A42: |.((s2 . i) * (||.(x . i).|| ")).| = (s2 . i) * (||.(x . i).|| ") by A41, COMPLEX1:43;

x . i <> 0. (X . i) by A24;

then A43: ||.(x . i).|| <> 0 by NORMSP_0:def 5;

||.(x1 . i).|| = ((s2 . i) * (||.(x . i).|| ")) * ||.(x . i).|| by A39, A42, NORMSP_1:def 1

.= (s2 . i) * ((||.(x . i).|| ") * ||.(x . i).||)

.= (s2 . i) * 1 by A43, XCMPLX_0:def 7 ;

hence ||.(x1 . i).|| <= s2 . i ; :: thesis: verum

A45: |.((Product F) ").| = (Product F) " by A23, ABSVALUE:def 1;

A46: |.((Product s2) * ((Product F) ")).| = |.(Product s2).| * |.((Product F) ").| by COMPLEX1:65

.= (Product s2) * ((Product F) ") by A21, A45, COMPLEX1:43 ;

f . x1 = ((Product s2) * ((Product F) ")) * (f . x) by A32, A33, A34, LOPBAN10:39;

then ||.(f . x1).|| = ((Product s2) * ((Product F) ")) * ||.(f . x).|| by A46, NORMSP_1:def 1;

then ((Product s2) * (((Product F) ") * ||.(f . x).||)) / (Product s2) < 1 / (Product s2) by A21, A44, XREAL_1:74;

then ((Product F) ") * ||.(f . x).|| < 1 / (Product s2) by A21, XCMPLX_1:89;

then (Product F) * (((Product F) ") * ||.(f . x).||) < (1 / (Product s2)) * (Product F) by A23, A25, XREAL_1:68;

then ((Product F) * ((Product F) ")) * ||.(f . x).|| < (1 / (Product s2)) * (Product F) ;

then 1 * ||.(f . x).|| < (1 / (Product s2)) * (Product F) by A23, A25, XCMPLX_0:def 7;

hence ||.(f . x).|| <= (1 / (Product s2)) * (NrProduct x) by A23; :: thesis: verum

suppose A47:
ex i being Element of dom X st x . i = 0. (X . i)
; :: thesis: ||.(f . x).|| <= (1 / (Product s2)) * (NrProduct x)

then A48:
f . x = 0. Y
by LOPBAN10:36;

consider i being Element of dom X such that

A49: x . i = 0. (X . i) by A47;

A50: F . i = ||.(x . i).|| by A23;

F . i = 0 by A49, A50;

then Product F = 0 by A23, RVSUM_1:103;

hence ||.(f . x).|| <= (1 / (Product s2)) * (NrProduct x) by A23, A48; :: thesis: verum

end;consider i being Element of dom X such that

A49: x . i = 0. (X . i) by A47;

A50: F . i = ||.(x . i).|| by A23;

F . i = 0 by A49, A50;

then Product F = 0 by A23, RVSUM_1:103;

hence ||.(f . x).|| <= (1 / (Product s2)) * (NrProduct x) by A23, A48; :: thesis: verum

proof

hence
( ( f is_continuous_on the carrier of (product X) implies f is_continuous_in 0. (product X) ) & ( f is_continuous_in 0. (product X) implies f is_continuous_on the carrier of (product X) ) & ( f is_continuous_on the carrier of (product X) implies f is Lipschitzian ) & ( f is Lipschitzian implies f is_continuous_on the carrier of (product X) ) )
by A4; :: thesis: verum
assume
f is Lipschitzian
; :: thesis: f is_continuous_on the carrier of (product X)

then consider K being Real such that

A52: 0 <= K and

A53: for x being Point of (product X) holds ||.(f . x).|| <= K * (NrProduct x) ;

for v0 being Point of (product X)

for r being Real st v0 in the carrier of (product X) & 0 < r holds

ex s being Real st

( 0 < s & ( for v1 being Point of (product X) st v1 in the carrier of (product X) & ||.(v1 - v0).|| < s holds

||.((f /. v1) - (f /. v0)).|| < r ) )

end;then consider K being Real such that

A52: 0 <= K and

A53: for x being Point of (product X) holds ||.(f . x).|| <= K * (NrProduct x) ;

for v0 being Point of (product X)

for r being Real st v0 in the carrier of (product X) & 0 < r holds

ex s being Real st

( 0 < s & ( for v1 being Point of (product X) st v1 in the carrier of (product X) & ||.(v1 - v0).|| < s holds

||.((f /. v1) - (f /. v0)).|| < r ) )

proof

hence
f is_continuous_on the carrier of (product X)
by A1, NFCONT_1:19; :: thesis: verum
let v0 be Point of (product X); :: thesis: for r being Real st v0 in the carrier of (product X) & 0 < r holds

ex s being Real st

( 0 < s & ( for v1 being Point of (product X) st v1 in the carrier of (product X) & ||.(v1 - v0).|| < s holds

||.((f /. v1) - (f /. v0)).|| < r ) )

let r0 be Real; :: thesis: ( v0 in the carrier of (product X) & 0 < r0 implies ex s being Real st

( 0 < s & ( for v1 being Point of (product X) st v1 in the carrier of (product X) & ||.(v1 - v0).|| < s holds

||.((f /. v1) - (f /. v0)).|| < r0 ) ) )

assume A54: ( v0 in the carrier of (product X) & 0 < r0 ) ; :: thesis: ex s being Real st

( 0 < s & ( for v1 being Point of (product X) st v1 in the carrier of (product X) & ||.(v1 - v0).|| < s holds

||.((f /. v1) - (f /. v0)).|| < r0 ) )

set r = r0 / 2;

A58: ( 0 < r0 / 2 & r0 / 2 < r0 ) by A54, XREAL_1:216;

set L = ||.v0.|| + 1;

consider M being Real such that

A59: ( 0 <= M & ( for v1 being Point of (product X) st ||.(v1 - v0).|| <= 1 holds

ex F being FinSequence of REAL st

( dom F = dom X & ||.((f /. v1) - (f /. v0)).|| <= (M * K) * (Sum F) & ( for i being Element of dom X holds F . i = ||.((v1 - v0) . i).|| ) ) ) ) by A52, A53, LM01;

set BL = ((M * K) * (len X)) + 1;

set s = min (((r0 / 2) / (((M * K) * (len X)) + 1)),1);

A64: ( 0 < min (((r0 / 2) / (((M * K) * (len X)) + 1)),1) & min (((r0 / 2) / (((M * K) * (len X)) + 1)),1) <= 1 & min (((r0 / 2) / (((M * K) * (len X)) + 1)),1) <= (r0 / 2) / (((M * K) * (len X)) + 1) ) by A52, A54, A59, XXREAL_0:17, XXREAL_0:21;

0 + ((M * K) * (len X)) <= ((M * K) * (len X)) + 1 by XREAL_1:7;

then ((M * K) * (len X)) * (min (((r0 / 2) / (((M * K) * (len X)) + 1)),1)) <= ((r0 / 2) / (((M * K) * (len X)) + 1)) * (((M * K) * (len X)) + 1) by A52, A59, A64, XREAL_1:66;

then A65: ((M * K) * (len X)) * (min (((r0 / 2) / (((M * K) * (len X)) + 1)),1)) <= r0 / 2 by A52, A59, XCMPLX_1:87;

take min (((r0 / 2) / (((M * K) * (len X)) + 1)),1) ; :: thesis: ( 0 < min (((r0 / 2) / (((M * K) * (len X)) + 1)),1) & ( for v1 being Point of (product X) st v1 in the carrier of (product X) & ||.(v1 - v0).|| < min (((r0 / 2) / (((M * K) * (len X)) + 1)),1) holds

||.((f /. v1) - (f /. v0)).|| < r0 ) )

thus 0 < min (((r0 / 2) / (((M * K) * (len X)) + 1)),1) by A52, A54, A59, XXREAL_0:21; :: thesis: for v1 being Point of (product X) st v1 in the carrier of (product X) & ||.(v1 - v0).|| < min (((r0 / 2) / (((M * K) * (len X)) + 1)),1) holds

||.((f /. v1) - (f /. v0)).|| < r0

let v1 be Point of (product X); :: thesis: ( v1 in the carrier of (product X) & ||.(v1 - v0).|| < min (((r0 / 2) / (((M * K) * (len X)) + 1)),1) implies ||.((f /. v1) - (f /. v0)).|| < r0 )

assume A66: ( v1 in the carrier of (product X) & ||.(v1 - v0).|| < min (((r0 / 2) / (((M * K) * (len X)) + 1)),1) ) ; :: thesis: ||.((f /. v1) - (f /. v0)).|| < r0

reconsider w1 = v1 - v0 as Element of (product X) ;

consider H being FinSequence of REAL such that

A67: ( dom H = dom X & ||.((f /. v1) - (f /. v0)).|| <= (M * K) * (Sum H) & ( for i being Element of dom X holds H . i = ||.(w1 . i).|| ) ) by A59, A64, A66, XXREAL_0:2;

for i being Nat st i in dom H holds

0 <= H . i

A69: for i being Element of dom X holds ||.(w1 . i).|| < min (((r0 / 2) / (((M * K) * (len X)) + 1)),1)

A71: H is Element of (len H) -tuples_on REAL by FINSEQ_2:92;

( len H is natural Number & min (((r0 / 2) / (((M * K) * (len X)) + 1)),1) is Element of REAL ) by XREAL_0:def 1;

then reconsider CST = (len H) |-> (min (((r0 / 2) / (((M * K) * (len X)) + 1)),1)) as Element of (len H) -tuples_on REAL by FINSEQ_2:112;

dom H = Seg (len X) by A67, FINSEQ_1:def 3;

then A72: len H = len X by FINSEQ_1:def 3;

for i being Nat st i in Seg (len H) holds

H . i <= CST . i

then Sum H <= (min (((r0 / 2) / (((M * K) * (len X)) + 1)),1)) * (len X) by A72, RVSUM_1:80;

then (M * K) * (Sum H) <= (M * K) * ((min (((r0 / 2) / (((M * K) * (len X)) + 1)),1)) * (len X)) by A52, A59, A68, XREAL_1:66;

then ||.((f /. v1) - (f /. v0)).|| <= (M * K) * ((min (((r0 / 2) / (((M * K) * (len X)) + 1)),1)) * (len X)) by A67, XXREAL_0:2;

then ||.((f /. v1) - (f /. v0)).|| <= r0 / 2 by A65, XXREAL_0:2;

hence ||.((f /. v1) - (f /. v0)).|| < r0 by A58, XXREAL_0:2; :: thesis: verum

end;ex s being Real st

( 0 < s & ( for v1 being Point of (product X) st v1 in the carrier of (product X) & ||.(v1 - v0).|| < s holds

||.((f /. v1) - (f /. v0)).|| < r ) )

let r0 be Real; :: thesis: ( v0 in the carrier of (product X) & 0 < r0 implies ex s being Real st

( 0 < s & ( for v1 being Point of (product X) st v1 in the carrier of (product X) & ||.(v1 - v0).|| < s holds

||.((f /. v1) - (f /. v0)).|| < r0 ) ) )

assume A54: ( v0 in the carrier of (product X) & 0 < r0 ) ; :: thesis: ex s being Real st

( 0 < s & ( for v1 being Point of (product X) st v1 in the carrier of (product X) & ||.(v1 - v0).|| < s holds

||.((f /. v1) - (f /. v0)).|| < r0 ) )

set r = r0 / 2;

A58: ( 0 < r0 / 2 & r0 / 2 < r0 ) by A54, XREAL_1:216;

set L = ||.v0.|| + 1;

consider M being Real such that

A59: ( 0 <= M & ( for v1 being Point of (product X) st ||.(v1 - v0).|| <= 1 holds

ex F being FinSequence of REAL st

( dom F = dom X & ||.((f /. v1) - (f /. v0)).|| <= (M * K) * (Sum F) & ( for i being Element of dom X holds F . i = ||.((v1 - v0) . i).|| ) ) ) ) by A52, A53, LM01;

set BL = ((M * K) * (len X)) + 1;

set s = min (((r0 / 2) / (((M * K) * (len X)) + 1)),1);

A64: ( 0 < min (((r0 / 2) / (((M * K) * (len X)) + 1)),1) & min (((r0 / 2) / (((M * K) * (len X)) + 1)),1) <= 1 & min (((r0 / 2) / (((M * K) * (len X)) + 1)),1) <= (r0 / 2) / (((M * K) * (len X)) + 1) ) by A52, A54, A59, XXREAL_0:17, XXREAL_0:21;

0 + ((M * K) * (len X)) <= ((M * K) * (len X)) + 1 by XREAL_1:7;

then ((M * K) * (len X)) * (min (((r0 / 2) / (((M * K) * (len X)) + 1)),1)) <= ((r0 / 2) / (((M * K) * (len X)) + 1)) * (((M * K) * (len X)) + 1) by A52, A59, A64, XREAL_1:66;

then A65: ((M * K) * (len X)) * (min (((r0 / 2) / (((M * K) * (len X)) + 1)),1)) <= r0 / 2 by A52, A59, XCMPLX_1:87;

take min (((r0 / 2) / (((M * K) * (len X)) + 1)),1) ; :: thesis: ( 0 < min (((r0 / 2) / (((M * K) * (len X)) + 1)),1) & ( for v1 being Point of (product X) st v1 in the carrier of (product X) & ||.(v1 - v0).|| < min (((r0 / 2) / (((M * K) * (len X)) + 1)),1) holds

||.((f /. v1) - (f /. v0)).|| < r0 ) )

thus 0 < min (((r0 / 2) / (((M * K) * (len X)) + 1)),1) by A52, A54, A59, XXREAL_0:21; :: thesis: for v1 being Point of (product X) st v1 in the carrier of (product X) & ||.(v1 - v0).|| < min (((r0 / 2) / (((M * K) * (len X)) + 1)),1) holds

||.((f /. v1) - (f /. v0)).|| < r0

let v1 be Point of (product X); :: thesis: ( v1 in the carrier of (product X) & ||.(v1 - v0).|| < min (((r0 / 2) / (((M * K) * (len X)) + 1)),1) implies ||.((f /. v1) - (f /. v0)).|| < r0 )

assume A66: ( v1 in the carrier of (product X) & ||.(v1 - v0).|| < min (((r0 / 2) / (((M * K) * (len X)) + 1)),1) ) ; :: thesis: ||.((f /. v1) - (f /. v0)).|| < r0

reconsider w1 = v1 - v0 as Element of (product X) ;

consider H being FinSequence of REAL such that

A67: ( dom H = dom X & ||.((f /. v1) - (f /. v0)).|| <= (M * K) * (Sum H) & ( for i being Element of dom X holds H . i = ||.(w1 . i).|| ) ) by A59, A64, A66, XXREAL_0:2;

for i being Nat st i in dom H holds

0 <= H . i

proof

then A68:
0 <= Sum H
by RVSUM_1:84;
let i be Nat; :: thesis: ( i in dom H implies 0 <= H . i )

assume i in dom H ; :: thesis: 0 <= H . i

then reconsider j = i as Element of dom X by A67;

H . j = ||.(w1 . j).|| by A67;

hence 0 <= H . i ; :: thesis: verum

end;assume i in dom H ; :: thesis: 0 <= H . i

then reconsider j = i as Element of dom X by A67;

H . j = ||.(w1 . j).|| by A67;

hence 0 <= H . i ; :: thesis: verum

A69: for i being Element of dom X holds ||.(w1 . i).|| < min (((r0 / 2) / (((M * K) * (len X)) + 1)),1)

proof

set CST = (len H) |-> (min (((r0 / 2) / (((M * K) * (len X)) + 1)),1));
let i be Element of dom X; :: thesis: ||.(w1 . i).|| < min (((r0 / 2) / (((M * K) * (len X)) + 1)),1)

||.(w1 . i).|| <= ||.(v1 - v0).|| by A3, PRVECT_2:10;

hence ||.(w1 . i).|| < min (((r0 / 2) / (((M * K) * (len X)) + 1)),1) by A66, XXREAL_0:2; :: thesis: verum

end;||.(w1 . i).|| <= ||.(v1 - v0).|| by A3, PRVECT_2:10;

hence ||.(w1 . i).|| < min (((r0 / 2) / (((M * K) * (len X)) + 1)),1) by A66, XXREAL_0:2; :: thesis: verum

A71: H is Element of (len H) -tuples_on REAL by FINSEQ_2:92;

( len H is natural Number & min (((r0 / 2) / (((M * K) * (len X)) + 1)),1) is Element of REAL ) by XREAL_0:def 1;

then reconsider CST = (len H) |-> (min (((r0 / 2) / (((M * K) * (len X)) + 1)),1)) as Element of (len H) -tuples_on REAL by FINSEQ_2:112;

dom H = Seg (len X) by A67, FINSEQ_1:def 3;

then A72: len H = len X by FINSEQ_1:def 3;

for i being Nat st i in Seg (len H) holds

H . i <= CST . i

proof

then
Sum H <= Sum CST
by A71, RVSUM_1:82;
let i0 be Nat; :: thesis: ( i0 in Seg (len H) implies H . i0 <= CST . i0 )

assume A73: i0 in Seg (len H) ; :: thesis: H . i0 <= CST . i0

then reconsider i = i0 as Element of dom X by A67, FINSEQ_1:def 3;

A74: ||.(w1 . i).|| < min (((r0 / 2) / (((M * K) * (len X)) + 1)),1) by A69;

H . i <= min (((r0 / 2) / (((M * K) * (len X)) + 1)),1) by A67, A74;

hence H . i0 <= CST . i0 by A73, FINSEQ_2:57; :: thesis: verum

end;assume A73: i0 in Seg (len H) ; :: thesis: H . i0 <= CST . i0

then reconsider i = i0 as Element of dom X by A67, FINSEQ_1:def 3;

A74: ||.(w1 . i).|| < min (((r0 / 2) / (((M * K) * (len X)) + 1)),1) by A69;

H . i <= min (((r0 / 2) / (((M * K) * (len X)) + 1)),1) by A67, A74;

hence H . i0 <= CST . i0 by A73, FINSEQ_2:57; :: thesis: verum

then Sum H <= (min (((r0 / 2) / (((M * K) * (len X)) + 1)),1)) * (len X) by A72, RVSUM_1:80;

then (M * K) * (Sum H) <= (M * K) * ((min (((r0 / 2) / (((M * K) * (len X)) + 1)),1)) * (len X)) by A52, A59, A68, XREAL_1:66;

then ||.((f /. v1) - (f /. v0)).|| <= (M * K) * ((min (((r0 / 2) / (((M * K) * (len X)) + 1)),1)) * (len X)) by A67, XXREAL_0:2;

then ||.((f /. v1) - (f /. v0)).|| <= r0 / 2 by A65, XXREAL_0:2;

hence ||.((f /. v1) - (f /. v0)).|| < r0 by A58, XXREAL_0:2; :: thesis: verum