theorem Th18: :: INTEGRA2:18
for r being Real
for X, Z being non empty set
for f being PartFunc of X,REAL holds rng (r (#) (f | Z)) = r ** (rng (f | Z))