let X be non empty set ; :: thesis: for S being SigmaField of X
for f being PartFunc of X,REAL
for r being Real st f is_simple_func_in S holds
r (#) f is_simple_func_in S
let S be SigmaField of X; :: thesis: for f being PartFunc of X,REAL
for r being Real st f is_simple_func_in S holds
r (#) f is_simple_func_in S
let f be PartFunc of X,REAL; :: thesis: for r being Real st f is_simple_func_in S holds
r (#) f is_simple_func_in S
let r be Real; :: thesis: ( f is_simple_func_in S implies r (#) f is_simple_func_in S )
set g = r (#) f;
assume f is_simple_func_in S ; :: thesis: r (#) f is_simple_func_in S
then consider G being Finite_Sep_Sequence of S such that
A1: dom f = union (rng G) and
A2: for n being Nat
for x, y being Element of X st n in dom G & x in G . n & y in G . n holds
f . x = f . y ;
A3: dom (r (#) f) = dom f by VALUED_1:def 5;

now :: thesis: for n being Nat
for x, y being Element of X st n in dom G & x in G . n & y in G . n holds
(r (#) f) . x = (r (#) f) . y

let n be Nat; :: thesis: for x, y being Element of X st n in dom G & x in G . n & y in G . n holds
(r (#) f) . x = (r (#) f) . y
let x, y be Element of X; :: thesis: ( n in dom G & x in G . n & y in G . n implies (r (#) f) . x = (r (#) f) . y )
assume that
A4: n in dom G and
A5: x in G . n and
A6: y in G . n ; :: thesis: (r (#) f) . x = (r (#) f) . y
A7: G . n in rng G by A4, FUNCT_1:3;
then y in dom (r (#) f) by A3, A1, A6, TARSKI:def 4;
then A8: (r (#) f) . y = r * (f . y) by VALUED_1:def 5;
x in dom (r (#) f) by A3, A1, A5, A7, TARSKI:def 4;
then (r (#) f) . x = r * (f . x) by VALUED_1:def 5;
hence (r (#) f) . x = (r (#) f) . y by A2, A4, A5, A6, A8; :: thesis: verum

end;

hence r (#) f is_simple_func_in S by A3, A1; :: thesis: verum