let j be Element of NAT ; :: thesis: for f being Point of (R_NormSpace_of_BoundedLinearOperators ((REAL-NS 1),(REAL-NS j))) ex p being Point of (REAL-NS j) st
( p = f . <*1*> & ||.p.|| = ||.f.|| )
let f be Point of (R_NormSpace_of_BoundedLinearOperators ((REAL-NS 1),(REAL-NS j))); :: thesis: ex p being Point of (REAL-NS j) st
( p = f . <*1*> & ||.p.|| = ||.f.|| )
reconsider g = f as Lipschitzian LinearOperator of (REAL-NS 1),(REAL-NS j) by LOPBAN_1:def 9;
consider p being Point of (REAL-NS j) such that
A1: ( p = f . <*1*> & ( for r being Real
for x being Point of (REAL-NS 1) st x = <*r*> holds
f . x = r * p ) & ( for x being Point of (REAL-NS 1) holds ||.(f . x).|| = ||.p.|| * ||.x.|| ) ) by Th18;
<*jj*> in REAL 1 by FINSEQ_2:98;
then reconsider One = <*jj*> as Point of (REAL-NS 1) by REAL_NS1:def 4;
||.(g . One).|| <= ||.f.|| * ||.One.|| by LOPBAN_1:32;
then ||.(g . One).|| <= ||.f.|| * |.1.| by PDIFF_8:2;
then A2: ||.(f . One).|| <= ||.f.|| * 1 by ABSVALUE:def 1;
for x being Point of (REAL-NS 1) st ||.x.|| <= 1 holds
||.(f . x).|| <= ||.p.|| * ||.x.|| by A1;
then ||.f.|| <= ||.p.|| by Th1;
hence ex p being Point of (REAL-NS j) st
( p = f . <*1*> & ||.p.|| = ||.f.|| ) by A1, A2, XXREAL_0:1; :: thesis: verum