let X be RealNormSpace-Sequence; :: thesis:
let Y be RealNormSpace; :: thesis:
let f be MultilinearOperator of X,Y; :: thesis:
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

assume f is_continuous_in 0. (product X) ; :: thesis:
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₁[ 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₁[n,d]

proof

let n be Nat; :: thesis:
assume n in Seg (len X) ; :: thesis:
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:
thus S₁[n,si] ; :: thesis:

end;

consider s2 being FinSequence of REAL such that
A8: ( len s2 = len X & ( for n being Nat st n in Seg (len X) holds
S₁[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

proof

let i be Element of dom X; :: thesis:
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:

end;

A12: for i being Element of dom X holds
( 0 < s2 . i & s2 . i < s1 . i )

proof

let i be Element of dom X; :: thesis:
( s2 . i = (s1 . i) / 2 & 0 < s1 . i ) by A6, A11;
hence ( 0 < s2 . i & s2 . i < s1 . i ) by XREAL_1:216; :: thesis:

end;

dom s2 = Seg (len X) by A9, FINSEQ_1:def 3;
then A13: len s2 = len X by FINSEQ_1:def 3;

A14: now :: thesis:

let x be Point of (product X); :: thesis:
assume A15: for i being Element of dom X holds ||.(x . i).|| <= s2 . i ; :: thesis:
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:

let i0 be object ; :: thesis:
assume i0 in dom X ; :: thesis:
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:

end;

then x in product Balls by A6, A16, CARD_3:def 5;
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:

end;

A21: 0 < Product s2 by A9, A12, PSPROD;
set K = 1 / (Product s2);

now :: thesis:

let x be Point of (product X); :: thesis:
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:

proof

per cases ;

suppose A24: for i being Element of dom X holds x . i <> 0. (X . i) ; :: thesis:

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

proof

let i be Element of dom F; :: thesis:
reconsider j = i as Element of dom X by A23;
d . j = ||.(x . j).|| " by A26;
hence d . i = (F . i) " by A23; :: thesis:

end;

A32: dom (mlt (s2,d)) = (dom X) /\ (dom X) by A9, A26, VALUED_1:def 4
.= 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

let i be Element of dom X; :: thesis:
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:

end;

A44: ||.(f /. x1).|| < 1 by A14, A35;
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:

end;

suppose A47: ex i being Element of dom X st x . i = 0. (X . i) ; :: thesis:

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:

end;

hence f is Lipschitzian by A21; :: thesis:

end;

( f is Lipschitzian implies f is_continuous_on the carrier of (product X) )

proof

assume f is Lipschitzian ; :: thesis:
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

let v0 be Point of (product X); :: thesis:
let r0 be Real; :: thesis:
assume A54: ( v0 in the carrier of (product X) & 0 < r0 ) ; :: thesis:
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:
thus 0 < min (((r0 / 2) / (((M * K) * (len X)) + 1)),1) by A52, A54, A59, XXREAL_0:21; :: thesis:
let v1 be Point of (product X); :: thesis:
assume A66: ( v1 in the carrier of (product X) & ||.(v1 - v0).|| < min (((r0 / 2) / (((M * K) * (len X)) + 1)),1) ) ; :: thesis:
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

let i be Nat; :: thesis:
assume i in dom H ; :: thesis:
then reconsider j = i as Element of dom X by A67;
H . j = ||.(w1 . j).|| by A67;
hence 0 <= H . i ; :: thesis:

end;

then A68: 0 <= Sum H by RVSUM_1:84;
A69: for i being Element of dom X holds ||.(w1 . i).|| < min (((r0 / 2) / (((M * K) * (len X)) + 1)),1)

proof

let i be Element of dom X; :: thesis:
||.(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:

end;

set CST = (len H) |-> (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

proof

let i0 be Nat; :: thesis:
assume A73: i0 in Seg (len H) ; :: thesis:
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:

end;

then Sum H <= Sum CST by A71, RVSUM_1:82;
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:

end;

hence f is_continuous_on the carrier of (product X) by A1, NFCONT_1:19; :: thesis:

end;

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: