let X be RealNormSpace-Sequence; :: thesis: for Y being RealNormSpace
for f being Point of (R_NormSpace_of_BoundedMultilinearOperators (X,Y))
for g being Lipschitzian MultilinearOperator of X,Y st g = f holds
for t being VECTOR of (product X) holds ||.(g . t).|| <= ||.f.|| * (NrProduct t)
let Y be RealNormSpace; :: thesis: for f being Point of (R_NormSpace_of_BoundedMultilinearOperators (X,Y))
for g being Lipschitzian MultilinearOperator of X,Y st g = f holds
for t being VECTOR of (product X) holds ||.(g . t).|| <= ||.f.|| * (NrProduct t)
let f be Point of (R_NormSpace_of_BoundedMultilinearOperators (X,Y)); :: thesis: for g being Lipschitzian MultilinearOperator of X,Y st g = f holds
for t being VECTOR of (product X) holds ||.(g . t).|| <= ||.f.|| * (NrProduct t)
let g be Lipschitzian MultilinearOperator of X,Y; :: thesis: ( g = f implies for t being VECTOR of (product X) holds ||.(g . t).|| <= ||.f.|| * (NrProduct t) )
assume A1: g = f ; :: thesis: for t being VECTOR of (product X) holds ||.(g . t).|| <= ||.f.|| * (NrProduct t)
A2: ( not PreNorms g is empty & PreNorms g is bounded_above ) by Th27;

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

let t be VECTOR of (product X); :: thesis: ||.(g . t).|| <= ||.f.|| * (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).|| <= ||.f.|| * (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 t . i <> 0. (X . i) ) ;

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

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

end;

suppose A10: for i being Element of dom X holds t . i <> 0. (X . i) ; :: thesis: ||.(g . t).|| <= ||.f.|| * (NrProduct t)

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;
A12: F . j = ||.(t . j).|| by A3;
t . j <> 0. (X . j) by A10;
then F . j <> 0 by A12, NORMSP_0:def 5;
hence F . i > 0 by A12; :: thesis: verum

end;

then A13: 0 < Product F by LM31;
consider d being FinSequence of REAL such that
A14: ( 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
A15: for i being Element of dom X holds t1 . i = (d /. i) * (t . i) by LM33;
A16: for i being Element of dom X holds ||.(t1 . i).|| <= 1

proof

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

end;

A20: (Product d) * (g . t) = g . t1 by A14, A15, LM35;
A23: 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 . i = ||.(t . j).|| " by A14;
hence d . i = (F . i) " by A3; :: thesis: verum

end;

A24: |.(Product d).| * ||.(g . t).|| = ||.(g . t1).|| by A20, NORMSP_1:def 1;
A25: |.((Product F) ").| = |.(1 * ((Product F) ")).|
.= |.(1 / (Product F)).| by XCMPLX_0:def 9
.= 1 / (Product F) by A13, ABSVALUE:def 1 ;
A26: |.(Product d).| * ||.(g . t).|| = (1 / (Product F)) * ||.(g . t).|| by A3, A14, A23, A25, LM36
.= ||.(g . t).|| / (Product F) by XCMPLX_1:99 ;
||.(g . t1).|| in { ||.(g . t).|| where t is VECTOR of (product X) : for i being Element of dom X holds ||.(t . i).|| <= 1 } by A16;
then ||.(g . t).|| / (Product F) <= upper_bound (PreNorms g) by A2, A24, A26, SEQ_4:def 1;
then A28: ||.(g . t).|| / (Product F) <= ||.f.|| by A1, Th30;
(||.(g . t).|| / (Product F)) * (Product F) = ||.(g . t).|| by A13, XCMPLX_1:87;
hence ||.(g . t).|| <= ||.f.|| * (NrProduct t) by A3, A28, XREAL_1:64; :: thesis: verum

end;

end;

end;

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

end;

hence for t being VECTOR of (product X) holds ||.(g . t).|| <= ||.f.|| * (NrProduct t) ; :: thesis: verum