theorem Th19: :: PDIFF_9:19

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*> & ||.p.|| = ||.f.|| )