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*> & ( 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.|| ) )
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*> & ( 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.|| ) )
reconsider One = <*jj*> as Element of REAL 1 by FINSEQ_2:98;
reconsider L = f as Lipschitzian LinearOperator of (REAL-NS 1),(REAL-NS j) by LOPBAN_1:def 9;
the carrier of (REAL-NS 1) = REAL 1 by REAL_NS1:def 4;
then dom L = REAL 1 by FUNCT_2:def 1;
then reconsider p = f . <*jj*> as Point of (REAL-NS j) by FINSEQ_2:98, PARTFUN1:4;
reconsider OneNS = One as VECTOR of (REAL-NS 1) by REAL_NS1:def 4;

A1: now :: thesis: for r being Real
for x being Point of (REAL-NS 1) st x = <*r*> holds
f . x = r * p

let r be Real; :: thesis: for x being Point of (REAL-NS 1) st x = <*r*> holds
f . x = r * p
let x be Point of (REAL-NS 1); :: thesis: ( x = <*r*> implies f . x = r * p )
assume x = <*r*> ; :: thesis: f . x = r * p
then A2: f . x = L . <*r*> ;
<*r*> = <*(r * 1)*>
.= r * <*1*> by RVSUM_1:47
.= r * OneNS by REAL_NS1:3 ;
hence f . x = r * p by A2, LOPBAN_1:def 5; :: thesis: verum

end;

now :: thesis: for x being Point of (REAL-NS 1) holds ||.(f . x).|| = ||.p.|| * ||.x.||

let x be Point of (REAL-NS 1); :: thesis: ||.(f . x).|| = ||.p.|| * ||.x.||
A3: the carrier of (REAL-NS 1) = REAL 1 by REAL_NS1:def 4;
then reconsider x0 = x as FinSequence of REAL by FINSEQ_2:def 3;
consider r being Element of REAL such that
A4: x0 = <*r*> by A3, FINSEQ_2:97;
thus ||.(f . x).|| = ||.(r * p).|| by A1, A4
.= |.r.| * ||.p.|| by NORMSP_1:def 1
.= ||.p.|| * ||.x.|| by A4, PDIFF_8:2 ; :: thesis: verum

end;

hence ex p being Point of (REAL-NS j) st
( 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 A1; :: thesis: verum