let X be RealNormSpace-Sequence; :: thesis: for Y being RealNormSpace
for g being MultilinearOperator of X,Y holds
( g is Lipschitzian iff PreNorms g is bounded_above )
let Y be RealNormSpace; :: thesis: for g being MultilinearOperator of X,Y holds
( g is Lipschitzian iff PreNorms g is bounded_above )
let g be MultilinearOperator of X,Y; :: thesis: ( g is Lipschitzian iff PreNorms g is bounded_above )

now :: thesis: ( PreNorms g is bounded_above implies ex K being Real st g is Lipschitzian )

reconsider K = upper_bound (PreNorms g) as Real ;
assume A1: PreNorms g is bounded_above ; :: thesis: ex K being Real st g is Lipschitzian

A2: now :: thesis: for t being VECTOR of (product X) holds ||.(g . t).|| <= K * (NrProduct t)

let t be VECTOR of (product X); :: thesis: ||.(g . t).|| <= K * (NrProduct t)
consider F being FinSequence of REAL such that
A3: ( dom F = dom X & ( for i being Element of dom X holds F . i = ||.(t . i).|| ) & NrProduct t = Product F ) by DefNrPro;

now :: thesis: ||.(g . t).|| <= K * (NrProduct t)

per cases ( ex i being Element of dom X st t . i = 0. (X . i) or for i being Element of dom X holds not t . i = 0. (X . i) ) ;

suppose ex i being Element of dom X st t . i = 0. (X . i) ; :: thesis: ||.(g . t).|| <= K * (NrProduct t)

then consider i being Element of dom X such that
A6: t . i = 0. (X . i) ;
A7: F . i = ||.(t . i).|| by A3;
F . i = 0 by A6, A7;
then A10: Product F = 0 by A3, RVSUM_1:103;
g . t = 0. Y by A6, LM32;
hence ||.(g . t).|| <= K * (NrProduct t) by A3, A10; :: thesis: verum

end;

suppose A11: for i being Element of dom X holds not t . i = 0. (X . i) ; :: thesis: ||.(g . t).|| <= K * (NrProduct t)

A12: for i being Element of dom F holds F . i > 0

proof

let i be Element of dom F; :: thesis: F . i > 0
reconsider j = i as Element of dom X by A3;
A13: F . j = ||.(t . j).|| by A3;
t . j <> 0. (X . j) by A11;
then F . j <> 0 by A13, NORMSP_0:def 5;
hence F . i > 0 by A13; :: thesis: verum

end;

A15: 0 < Product F by A12, LM31;
consider d being FinSequence of REAL such that
A16: ( dom d = dom X & ( for i being Element of dom X holds d . i = ||.(t . i).|| " ) ) by LM34;
consider t1 being Element of (product X) such that
A17: for i being Element of dom X holds t1 . i = (d /. i) * (t . i) by LM33;
A18: (Product d) * (g . t) = g . t1 by A16, A17, LM35;
A22: 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 A3;
d . j = ||.(t . j).|| " by A16;
hence d . i = (F . i) " by A3; :: thesis: verum

end;

A23: |.(Product d).| * ||.(g . t).|| = ||.(g . t1).|| by A18, NORMSP_1:def 1;
|.((Product F) ").| = |.(1 * ((Product F) ")).|
.= |.(1 / (Product F)).| by XCMPLX_0:def 9
.= 1 / (Product F) by A15, ABSVALUE:def 1 ;
then A25: |.(Product d).| * ||.(g . t).|| = (1 / (Product F)) * ||.(g . t).|| by A3, A16, A22, LM36
.= ||.(g . t).|| / (Product F) by XCMPLX_1:99 ;
A26: for i being Element of dom X holds ||.(t1 . i).|| <= 1

proof

let i be Element of dom X; :: thesis: ||.(t1 . i).|| <= 1
A27: d . i = ||.(t . i).|| " by A16;
A28: t1 . i = (d /. i) * (t . i) by A17;
t . i <> 0. (X . i) by A11;
then A29: ||.(t . i).|| <> 0 by NORMSP_0:def 5;
||.(t1 . i).|| = |.(d /. i).| * ||.(t . i).|| by A28, NORMSP_1:def 1
.= |.(||.(t . i).|| ").| * ||.(t . i).|| by A16, A27, PARTFUN1:def 6
.= (||.(t . i).|| ") * ||.(t . i).|| by ABSVALUE:def 1
.= 1 by A29, XCMPLX_0:def 7 ;
hence ||.(t1 . i).|| <= 1 ; :: thesis: verum

end;

||.(g . t1).|| in { ||.(g . t).|| where t is VECTOR of (product X) : for i being Element of dom X holds ||.(t . i).|| <= 1 } by A26;
then ||.(g . t).|| / (Product F) <= K by A1, A23, A25, SEQ_4:def 1;
then (||.(g . t).|| / (Product F)) * (Product F) <= K * (Product F) by A15, XREAL_1:64;
hence ||.(g . t).|| <= K * (NrProduct t) by A3, A15, XCMPLX_1:87; :: thesis: verum

end;

end;

end;

hence ||.(g . t).|| <= K * (NrProduct t) ; :: thesis: verum

end;

take K = K; :: thesis: g is Lipschitzian
0 <= K

proof

consider r0 being object such that
A30: r0 in PreNorms g by XBOOLE_0:def 1;
reconsider r0 = r0 as Real by A30;

now :: thesis: for r being Real st r in PreNorms g holds
0 <= r

let r be Real; :: thesis: ( r in PreNorms g implies 0 <= r )
assume r in PreNorms g ; :: thesis: 0 <= r
then ex t being VECTOR of (product X) st
( r = ||.(g . t).|| & ( for i being Element of dom X holds ||.(t . i).|| <= 1 ) ) ;
hence 0 <= r ; :: thesis: verum

end;

then 0 <= r0 by A30;
hence 0 <= K by A1, A30, SEQ_4:def 1; :: thesis: verum

end;

hence g is Lipschitzian by A2; :: thesis: verum

end;

hence ( g is Lipschitzian iff PreNorms g is bounded_above ) by Th27; :: thesis: verum