let r be Real; :: thesis: for X being non empty set
for f being Function of X,REAL holds rng (r (#) f) = r ** (rng f)
let X be non empty set ; :: thesis: for f being Function of X,REAL holds rng (r (#) f) = r ** (rng f)
let f be Function of X,REAL; :: thesis: rng (r (#) f) = r ** (rng f)
for y being Element of REAL st y in r ** (rng f) holds
y in rng (r (#) f)

proof

let y be Element of REAL ; :: thesis: ( y in r ** (rng f) implies y in rng (r (#) f) )
assume y in r ** (rng f) ; :: thesis: y in rng (r (#) f)
then y in { (r * b) where b is Real : b in rng f } by Th8;
then consider b being Real such that
A1: y = r * b and
A2: b in rng f ;
consider x being Element of X such that
A3: x in dom f and
A4: b = f . x by A2, PARTFUN1:3;
x in dom (r (#) f) by A3, VALUED_1:def 5;
then (r (#) f) . x in rng (r (#) f) by FUNCT_1:def 3;
hence y in rng (r (#) f) by A1, A4, RFUNCT_1:57; :: thesis: verum

end;

then A5: r ** (rng f) c= rng (r (#) f) ;
for y being Element of REAL st y in rng (r (#) f) holds
y in r ** (rng f)

proof

let y be Element of REAL ; :: thesis: ( y in rng (r (#) f) implies y in r ** (rng f) )
assume y in rng (r (#) f) ; :: thesis: y in r ** (rng f)
then consider x being Element of X such that
A6: x in dom (r (#) f) and
A7: y = (r (#) f) . x by PARTFUN1:3;
x in dom f by A6, VALUED_1:def 5;
then A8: f . x in rng f by FUNCT_1:def 3;
reconsider fx = f . x as Real ;
y = r * fx by A7, RFUNCT_1:57;
then y in { (r * b) where b is Real : b in rng f } by A8;
hence y in r ** (rng f) by Th8; :: thesis: verum

end;

then rng (r (#) f) c= r ** (rng f) ;
hence rng (r (#) f) = r ** (rng f) by A5; :: thesis: verum