let X be non empty set ; 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; 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; for r being Real st f is_simple_func_in S holds
r (#) f is_simple_func_in S
let r be Real; ( 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
; 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 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) . ylet n be
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) . ylet x,
y be
Element of
X;
( 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
;
(r (#) f) . x = (r (#) f) . yA7:
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;
verum end;
hence
r (#) f is_simple_func_in S
by A3, A1; verum