let X be RealNormSpace-Sequence; for Y being RealNormSpace
for g being Lipschitzian MultilinearOperator of X,Y holds PreNorms g is bounded_above
let Y be RealNormSpace; for g being Lipschitzian MultilinearOperator of X,Y holds PreNorms g is bounded_above
let g be Lipschitzian MultilinearOperator of X,Y; PreNorms g is bounded_above
consider K being Real such that
A1:
0 <= K
and
A2:
for x being Point of (product X) holds ||.(g . x).|| <= K * (NrProduct x)
by Def8;
take
K
; XXREAL_2:def 10 K is UpperBound of PreNorms g
let r be ExtReal; XXREAL_2:def 1 ( not r in PreNorms g or r <= K )
assume
r in PreNorms g
; r <= K
then consider t being VECTOR of (product X) such that
A3:
r = ||.(g . t).||
and
A4:
for i being Element of dom X holds ||.(t . i).|| <= 1
;
A5:
||.(g . t).|| <= K * (NrProduct t)
by A2;
( 0 <= NrProduct t & NrProduct t <= 1 )
by A4, LM28;
then
K * (NrProduct t) <= K * 1
by A1, XREAL_1:64;
hence
r <= K
by A3, A5, XXREAL_0:2; verum