for V being RealLinearSpace
for f being Function of the carrier of V,REAL holds f (#) (<*> the carrier of V) = <*> the carrier of V