theorem Th9: :: CONVEX4:9

for V being non empty CLSStruct
for v1, v2 being VECTOR of V
for f being Function of the carrier of V,COMPLEX holds f (#) <*v1,v2*> = <*((f . v1) * v1),((f . v2) * v2)*>