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 ;
A5: x in dom (r (#) (f | Z)) by ;
then y = (r (#) (f | Z)) . x by ;
hence y in rng (r (#) (f | Z)) by ; :: 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 ;
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 ;
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