for r being Real holds r * (<*> REAL) = <*> REAL ;