let X, Y be RealNormSpace; :: thesis: BoundedMultilinearOperatorsNorm (<*X*>,Y) = BoundedLinearOperatorsNorm ((product <*X*>),Y)
set n1 = BoundedMultilinearOperatorsNorm (<*X*>,Y);
set n2 = BoundedLinearOperatorsNorm ((product <*X*>),Y);
A1: BoundedMultilinearOperators (<*X*>,Y) = BoundedLinearOperators ((product <*X*>),Y) by Th23;
A2: dom <*X*> = {1} by FINSEQ_1:2, FINSEQ_1:38;
then reconsider i = 1 as Element of dom <*X*> by TARSKI:def 1;
for f being object st f in BoundedMultilinearOperators (<*X*>,Y) holds
(BoundedMultilinearOperatorsNorm (<*X*>,Y)) . f = (BoundedLinearOperatorsNorm ((product <*X*>),Y)) . f

proof

let f be object ; :: thesis: ( f in BoundedMultilinearOperators (<*X*>,Y) implies (BoundedMultilinearOperatorsNorm (<*X*>,Y)) . f = (BoundedLinearOperatorsNorm ((product <*X*>),Y)) . f )
assume A4: f in BoundedMultilinearOperators (<*X*>,Y) ; :: thesis: (BoundedMultilinearOperatorsNorm (<*X*>,Y)) . f = (BoundedLinearOperatorsNorm ((product <*X*>),Y)) . f
reconsider f1 = f as Lipschitzian MultilinearOperator of <*X*>,Y by A4, LOPBAN10:def 11;
A5: modetrans (f,<*X*>,Y) = f1 ;
A6: (BoundedMultilinearOperatorsNorm (<*X*>,Y)) . f = upper_bound (PreNorms f1) by A4, A5, LOPBAN10:def 15;
reconsider f2 = f as Lipschitzian LinearOperator of (product <*X*>),Y by A1, A4, LOPBAN_1:def 9;
A7: modetrans (f,(product <*X*>),Y) = f2 by A1, A4, LOPBAN_1:def 11;
A8: (BoundedLinearOperatorsNorm ((product <*X*>),Y)) . f = upper_bound (PreNorms f2) by A1, A4, A7, LOPBAN_1:def 13;
for n being object holds
( n in PreNorms f1 iff n in PreNorms f2 )

proof

let n be object ; :: thesis: ( n in PreNorms f1 iff n in PreNorms f2 )

hereby :: thesis: ( n in PreNorms f2 implies n in PreNorms f1 )

assume n in PreNorms f1 ; :: thesis: n in PreNorms f2
then consider x being VECTOR of (product <*X*>) such that
A9: ( n = ||.(f1 . x).|| & ( for i being Element of dom <*X*> holds ||.(x . i).|| <= 1 ) ) ;
consider x1 being Point of X such that
A10: x = <*x1*> by Th12;
A11: ||.x.|| = ||.x1.|| by A10, Th12;
||.(x . i).|| <= 1 by A9;
then ||.x1.|| <= 1 by A10;
hence n in PreNorms f2 by A9, A11; :: thesis: verum

end;

assume n in PreNorms f2 ; :: thesis: n in PreNorms f1
then consider s being VECTOR of (product <*X*>) such that
A12: ( n = ||.(f2 . s).|| & ||.s.|| <= 1 ) ;
consider s1 being Point of X such that
A13: s = <*s1*> by Th12;
A14: ||.s.|| = ||.s1.|| by A13, Th12;
for i being Element of dom <*X*> holds ||.(s . i).|| <= 1

proof

let i be Element of dom <*X*>; :: thesis: ||.(s . i).|| <= 1
A15: i = 1 by A2, TARSKI:def 1;
thus ||.(s . i).|| <= 1 by A12, A13, A14, A15; :: thesis: verum

end;

hence n in PreNorms f1 by A12; :: thesis: verum

end;

hence (BoundedMultilinearOperatorsNorm (<*X*>,Y)) . f = (BoundedLinearOperatorsNorm ((product <*X*>),Y)) . f by A6, A8, TARSKI:2; :: thesis: verum

end;

hence BoundedMultilinearOperatorsNorm (<*X*>,Y) = BoundedLinearOperatorsNorm ((product <*X*>),Y) by Th23; :: thesis: verum