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
P1: ( 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 LM01A;
<*1*> in REAL 1 by FINSEQ_2:98;
then reconsider One = <*1*> as Point of (REAL-NS 1) by REAL_NS1:def 4;
||.(g . One).|| <= ||.f.|| * ||.One.|| by LOPBAN_1:32;
then ||.(g . One).|| <= ||.f.|| * (abs 1) by PDIFF_8:2;
then P2: ||.(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 P1;
then ||.f.|| <= ||.p.|| by LM01CPre2;
hence ex p being Point of (REAL-NS j) st
( p = f . <*1*> & ||.p.|| = ||.f.|| ) by P1, P2, XXREAL_0:1; :: thesis: verum