let Omega be non empty finite set ; :: thesis: for f being PartFunc of Omega,REAL holds
( f is_simple_func_in Trivial-SigmaField Omega & dom f is Element of Trivial-SigmaField Omega )
let f be PartFunc of Omega,REAL; :: thesis: ( f is_simple_func_in Trivial-SigmaField Omega & dom f is Element of Trivial-SigmaField Omega )
set Sigma = Trivial-SigmaField Omega;
set D = dom f;
ex F being Finite_Sep_Sequence of Trivial-SigmaField Omega st
( dom f = union (rng F) & dom F = dom (canFS (dom f)) & ( for k being Nat st k in dom F holds
F . k = {((canFS (dom f)) . k)} ) & ( for n being Nat
for x, y being Element of Omega st n in dom F & x in F . n & y in F . n holds
f . x = f . y ) ) by Lm6;
hence ( f is_simple_func_in Trivial-SigmaField Omega & dom f is Element of Trivial-SigmaField Omega ) ; :: thesis: verum