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 () implies f is_continuous_in 0. () ) & ( f is_continuous_in 0. () implies f is_continuous_on the carrier of () ) & ( f is_continuous_on the carrier of () implies f is Lipschitzian ) & ( f is Lipschitzian implies f is_continuous_on the carrier of () ) )

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

let f be MultilinearOperator of X,Y; :: thesis: ( ( f is_continuous_on the carrier of () implies f is_continuous_in 0. () ) & ( f is_continuous_in 0. () implies f is_continuous_on the carrier of () ) & ( f is_continuous_on the carrier of () implies f is Lipschitzian ) & ( f is Lipschitzian implies f is_continuous_on the carrier of () ) )
A1: dom f = the carrier of () by FUNCT_2:def 1;
A2: f /. (0. ()) = 0. Y by FXZER;
A3: product X = NORMSTR(# (product (carr X)),(),[:():],[:():],() #) by PRVECT_2:6;
A4: ( f is_continuous_in 0. () implies f is Lipschitzian )
proof
assume f is_continuous_in 0. () ; :: thesis: f is Lipschitzian
then consider s being Real such that
A5: ( 0 < s & ( for z being Point of () st z in dom f & ||.(z - (0. ())).|| < s holds
||.((f /. z) - (f /. (0. ()))).|| < 1 ) ) by NFCONT_1:7;
set z = 0. ();
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. ()),s) & ( for i being Element of dom X holds
( 0 < s1 . i & s1 . i < s & Balls . i = Ball (((0. ()) . i),(s1 . i)) ) ) ) by ;
defpred S1[ 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 S1[n,d]
proof
let n be Nat; :: thesis: ( n in Seg (len X) implies ex d being Element of REAL st S1[n,d] )
assume n in Seg (len X) ; :: thesis: ex d being Element of REAL st S1[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: S1[n,si]
thus S1[n,si] ; :: thesis: verum
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
S1[n,s2 /. n] ) ) from A9: dom s2 = Seg (len X) by
.= 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: 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 ; :: thesis: verum
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: ( 0 < s2 . i & s2 . i < s1 . i )
( s2 . i = (s1 . i) / 2 & 0 < s1 . i ) by ;
hence ( 0 < s2 . i & s2 . i < s1 . i ) by XREAL_1:216; :: thesis: verum
end;
dom s2 = Seg (len X) by ;
then A13: len s2 = len X by FINSEQ_1:def 3;
A14: now :: thesis: for x being Point of () st ( for i being Element of dom X holds ||.(x . i).|| <= s2 . i ) holds
||.(f /. x).|| < 1
let x be Point of (); :: 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 ;
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
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. ()) . 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 ;
then ( 0 < s2 . i & s2 . i < s1 . i ) by XREAL_1:216;
then ||.((0. (X . i)) - (x . i)).|| < s1 . i by ;
then x . i in Ball ((0. (X . i)),(s1 . i)) ;
hence x . i0 in Balls . i0 by ; :: thesis: verum
end;
then x in product Balls by ;
then x in Ball ((0. ()),s) by A6;
then ex p being Point of () st
( x = p & ||.((0. ()) - p).|| < s ) ;
then A20: ||.(x - (0. ())).|| < s by NORMSP_1:7;
||.((f /. x) - (f /. (0. ()))).|| < 1 by A1, A5, A20;
hence ||.(f /. x).|| < 1 by A2; :: thesis: verum
end;
A21: 0 < Product s2 by ;
set K = 1 / (Product s2);
now :: thesis: for x being Point of () holds ||.(f . x).|| <= (1 / (Product s2)) * ()
let x be Point of (); :: thesis: ||.(f . x).|| <= (1 / (Product s2)) * ()
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)) * () :: thesis: verum
proof
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) ) ;
suppose A24: for i being Element of dom X holds x . i <> 0. (X . i) ; :: thesis: ||.(f . x).|| <= (1 / (Product s2)) * ()
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 ;
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: 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;
A32: dom (mlt (s2,d)) = (dom X) /\ (dom X) by
.= dom X ;
( s2 is Element of (len X) -tuples_on REAL & d is Element of (len X) -tuples_on REAL ) by ;
then A33: Product (mlt (s2,d)) = (Product s2) * () by RVSUM_1:107
.= (Product s2) * (() ") by ;
consider x1 being Element of () 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: ||.(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
.= (s2 . i) * (d . i) by RVSUM_1:60
.= (s2 . i) * ((F . i) ") by ;
A39: x1 . i = ((s2 . i) * (||.(x . i).|| ")) * (x . i) by ;
A41: 0 <= s2 . i by A12;
A42: |.((s2 . i) * (||.(x . i).|| ")).| = (s2 . i) * (||.(x . i).|| ") by ;
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
.= (s2 . i) * ((||.(x . i).|| ") * ||.(x . i).||)
.= (s2 . i) * 1 by ;
hence ||.(x1 . i).|| <= s2 . i ; :: thesis: verum
end;
A44: ||.(f /. x1).|| < 1 by ;
A45: |.(() ").| = () " by ;
A46: |.((Product s2) * (() ")).| = |.(Product s2).| * |.(() ").| by COMPLEX1:65
.= (Product s2) * (() ") by ;
f . x1 = ((Product s2) * (() ")) * (f . x) by ;
then ||.(f . x1).|| = ((Product s2) * (() ")) * ||.(f . x).|| by ;
then ((Product s2) * ((() ") * ||.(f . x).||)) / (Product s2) < 1 / (Product s2) by ;
then ((Product F) ") * ||.(f . x).|| < 1 / (Product s2) by ;
then (Product F) * ((() ") * ||.(f . x).||) < (1 / (Product s2)) * () by ;
then ((Product F) * (() ")) * ||.(f . x).|| < (1 / (Product s2)) * () ;
then 1 * ||.(f . x).|| < (1 / (Product s2)) * () by ;
hence ||.(f . x).|| <= (1 / (Product s2)) * () by A23; :: thesis: verum
end;
suppose A47: ex i being Element of dom X st x . i = 0. (X . i) ; :: thesis: ||.(f . x).|| <= (1 / (Product s2)) * ()
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 ;
then Product F = 0 by ;
hence ||.(f . x).|| <= (1 / (Product s2)) * () by ; :: thesis: verum
end;
end;
end;
end;
hence f is Lipschitzian by A21; :: thesis: verum
end;
( f is Lipschitzian implies f is_continuous_on the carrier of () )
proof
assume f is Lipschitzian ; :: thesis: f is_continuous_on the carrier of ()
then consider K being Real such that
A52: 0 <= K and
A53: for x being Point of () holds ||.(f . x).|| <= K * () ;
for v0 being Point of ()
for r being Real st v0 in the carrier of () & 0 < r holds
ex s being Real st
( 0 < s & ( for v1 being Point of () st v1 in the carrier of () & ||.(v1 - v0).|| < s holds
||.((f /. v1) - (f /. v0)).|| < r ) )
proof
let v0 be Point of (); :: thesis: for r being Real st v0 in the carrier of () & 0 < r holds
ex s being Real st
( 0 < s & ( for v1 being Point of () st v1 in the carrier of () & ||.(v1 - v0).|| < s holds
||.((f /. v1) - (f /. v0)).|| < r ) )

let r0 be Real; :: thesis: ( v0 in the carrier of () & 0 < r0 implies ex s being Real st
( 0 < s & ( for v1 being Point of () st v1 in the carrier of () & ||.(v1 - v0).|| < s holds
||.((f /. v1) - (f /. v0)).|| < r0 ) ) )

assume A54: ( v0 in the carrier of () & 0 < r0 ) ; :: thesis: ex s being Real st
( 0 < s & ( for v1 being Point of () st v1 in the carrier of () & ||.(v1 - v0).|| < s holds
||.((f /. v1) - (f /. v0)).|| < r0 ) )

set r = r0 / 2;
A58: ( 0 < r0 / 2 & r0 / 2 < r0 ) by ;
set L = ||.v0.|| + 1;
consider M being Real such that
A59: ( 0 <= M & ( for v1 being Point of () 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 ;
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 ;
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 ;
then A65: ((M * K) * (len X)) * (min (((r0 / 2) / (((M * K) * (len X)) + 1)),1)) <= r0 / 2 by ;
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 () st v1 in the carrier of () & ||.(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 ; :: thesis: for v1 being Point of () st v1 in the carrier of () & ||.(v1 - v0).|| < min (((r0 / 2) / (((M * K) * (len X)) + 1)),1) holds
||.((f /. v1) - (f /. v0)).|| < r0

let v1 be Point of (); :: thesis: ( v1 in the carrier of () & ||.(v1 - v0).|| < min (((r0 / 2) / (((M * K) * (len X)) + 1)),1) implies ||.((f /. v1) - (f /. v0)).|| < r0 )
assume A66: ( v1 in the carrier of () & ||.(v1 - v0).|| < min (((r0 / 2) / (((M * K) * (len X)) + 1)),1) ) ; :: thesis: ||.((f /. v1) - (f /. v0)).|| < r0
reconsider w1 = v1 - v0 as Element of () ;
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 ;
for i being Nat st i in dom H holds
0 <= H . i
proof
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;
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).|| < min (((r0 / 2) / (((M * K) * (len X)) + 1)),1)
||.(w1 . i).|| <= ||.(v1 - v0).|| by ;
hence ||.(w1 . i).|| < min (((r0 / 2) / (((M * K) * (len X)) + 1)),1) by ; :: thesis: verum
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 ;
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: ( 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 ;
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 ;
hence H . i0 <= CST . i0 by ; :: thesis: verum
end;
then Sum H <= Sum CST by ;
then Sum H <= (min (((r0 / 2) / (((M * K) * (len X)) + 1)),1)) * (len X) by ;
then (M * K) * (Sum H) <= (M * K) * ((min (((r0 / 2) / (((M * K) * (len X)) + 1)),1)) * (len X)) by ;
then ||.((f /. v1) - (f /. v0)).|| <= (M * K) * ((min (((r0 / 2) / (((M * K) * (len X)) + 1)),1)) * (len X)) by ;
then ||.((f /. v1) - (f /. v0)).|| <= r0 / 2 by ;
hence ||.((f /. v1) - (f /. v0)).|| < r0 by ; :: thesis: verum
end;
hence f is_continuous_on the carrier of () by ; :: thesis: verum
end;
hence ( ( f is_continuous_on the carrier of () implies f is_continuous_in 0. () ) & ( f is_continuous_in 0. () implies f is_continuous_on the carrier of () ) & ( f is_continuous_on the carrier of () implies f is Lipschitzian ) & ( f is Lipschitzian implies f is_continuous_on the carrier of () ) ) by A4; :: thesis: verum