theorem :: MESFUN11:20

for X being non empty set
for r being non zero Real
for f being Function of X,ExtREAL holds
( f is V120() & f is V121() iff ( r (#) f is V120() & r (#) f is V121() ) )