theorem Th21: :: CSSPACE4:21
for X being non empty set
for Y being ComplexNormSpace
for f, h being Point of (C_NormSpace_of_BoundedFunctions (X,Y))
for f9, h9 being bounded Function of X, the carrier of Y st f9 = f & h9 = h holds
for c being Complex holds
( h = c * f iff for x being Element of X holds h9 . x = c * (f9 . x) )