let j be Element of NAT ; :: thesis: for f being Point of (R_NormSpace_of_BoundedLinearOperators ((REAL-NS 1),(REAL-NS j)))
for x being Point of (REAL-NS 1) holds ||.(f . x).|| = ||.f.|| * ||.x.||
let f be Point of (R_NormSpace_of_BoundedLinearOperators ((REAL-NS 1),(REAL-NS j))); :: thesis: for x being Point of (REAL-NS 1) holds ||.(f . x).|| = ||.f.|| * ||.x.||
let x be Point of (REAL-NS 1); :: thesis: ||.(f . x).|| = ||.f.|| * ||.x.||
A1: 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 Th18;
ex q being Point of (REAL-NS j) st
( q = f . <*1*> & ||.f.|| = ||.q.|| ) by Th19;
hence ||.(f . x).|| = ||.f.|| * ||.x.|| by A1; :: thesis: verum