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

proof

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

proof

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

end;

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

end;

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

proof

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

proof

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

end;

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

end;

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