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

proof

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

end;

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

proof

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

end;

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