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))

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

y in r ** (rng (f | Z))

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

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

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

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

y in r ** (rng (f | Z))

proof

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

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