let X be non empty set ; :: thesis: for S being SigmaField of X
for f being PartFunc of X,ExtREAL st f is empty holds
f is_simple_func_in S
let S be SigmaField of X; :: thesis: for f being PartFunc of X,ExtREAL st f is empty holds
f is_simple_func_in S
let f be PartFunc of X,ExtREAL; :: thesis: ( f is empty implies f is_simple_func_in S )
reconsider EMP = {} as Element of S by MEASURE1:7;
reconsider F = <*EMP*> as Finite_Sep_Sequence of S ;
assume A1: f is empty ; :: thesis: f is_simple_func_in S
then ( dom f = {} & rng F = {EMP} ) by FINSEQ_1:38;
then A2: dom f = union (rng F) by ZFMISC_1:25;
for n being Nat
for x, y being Element of X st n in dom F & x in F . n & y in F . n holds
f . x = f . y

proof

let n be Nat; :: thesis: for x, y being Element of X st n in dom F & x in F . n & y in F . n holds
f . x = f . y
let x, y be Element of X; :: thesis: ( n in dom F & x in F . n & y in F . n implies f . x = f . y )
assume A3: ( n in dom F & x in F . n & y in F . n ) ; :: thesis: f . x = f . y
then n in {1} by FINSEQ_1:2, FINSEQ_1:38;
then n = 1 by TARSKI:def 1;
hence f . x = f . y by A3; :: thesis: verum

end;

hence f is_simple_func_in S by A1, A2, MESFUNC2:def 4; :: thesis: verum