theorem Th20: :: PDIFF_9:20

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