theorem Th7: :: CC0SP1:7

for X being non empty set
for F, G, H being VECTOR of (C_Algebra_of_BoundedFunctions X)
for f, g, h being Function of X,COMPLEX st f = F & g = G & h = H holds
( H = F * G iff for x being Element of X holds h . x = (f . x) * (g . x) )