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)

for y being Element of REAL st y in rng (r (#) f) holds

y in r ** (rng f)

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

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

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

for y being Element of REAL st y in rng (r (#) f) holds

y in r ** (rng f)

proof

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

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