theorem Th8: :: CONVEX4:8
for V being non empty CLSStruct
for v being VECTOR of V
for f being Function of the carrier of V,COMPLEX holds f (#) <*v*> = <*((f . v) * v)*>