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)
A1: rng (r (#) f) c= r ** (rng f)

proof

for y being Real st y in rng (r (#) f) holds
y in r ** (rng f)

proof

let y be 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
A2: ( x in dom (r (#) f) & y = (r (#) f) . x ) by PARTFUN1:26;
A3: y = r * (f . x) by A2, RFUNCT_1:73;
x in dom f by A2, VALUED_1:def 5;
then f . x in rng f by FUNCT_1:def 5;
then y in { (r * b) where b is Real : b in rng f } by A3;
hence y in r ** (rng f) by Th8; :: thesis: verum

end;

hence rng (r (#) f) c= r ** (rng f) by SUBSET_1:7; :: thesis: verum

end;

r ** (rng f) c= rng (r (#) f)

proof

for y being Real st y in r ** (rng f) holds
y in rng (r (#) f)

proof

let y be 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
A4: ( y = r * b & b in rng f ) ;
consider x being Element of X such that
A5: ( x in dom f & b = f . x ) by A4, PARTFUN1:26;
x in dom (r (#) f) by A5, VALUED_1:def 5;
then (r (#) f) . x in rng (r (#) f) by FUNCT_1:def 5;
hence y in rng (r (#) f) by A4, A5, RFUNCT_1:73; :: thesis: verum

end;

hence r ** (rng f) c= rng (r (#) f) by SUBSET_1:7; :: thesis: verum

end;

hence rng (r (#) f) = r ** (rng f) by A1, XBOOLE_0:def 10; :: thesis: verum