theorem Th18: :: PDIFF_9:18

for j being Element of NAT
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.|| ) )