let X be non empty set ; :: thesis: for S being SigmaField of X
for f being PartFunc of X,ExtREAL st f is_simple_func_in S holds
ex F being Finite_Sep_Sequence of S ex a being FinSequence of ExtREAL st F,a are_Re-presentation_of f
let S be SigmaField of X; :: thesis: for f being PartFunc of X,ExtREAL st f is_simple_func_in S holds
ex F being Finite_Sep_Sequence of S ex a being FinSequence of ExtREAL st F,a are_Re-presentation_of f
let f be PartFunc of X,ExtREAL ; :: thesis: ( f is_simple_func_in S implies ex F being Finite_Sep_Sequence of S ex a being FinSequence of ExtREAL st F,a are_Re-presentation_of f )
assume A1: f is_simple_func_in S ; :: thesis: ex F being Finite_Sep_Sequence of S ex a being FinSequence of ExtREAL st F,a are_Re-presentation_of f
consider F being Finite_Sep_Sequence of S, a being FinSequence of ExtREAL such that
A2: ( dom f = union (rng F) & dom F = dom a & ( for n being Nat st n in dom F holds
for x being set st x in F . n holds
f . x = a . n ) & ( for x being set st x in dom f holds
ex ax being FinSequence of ExtREAL st
( dom ax = dom a & ( for n being Nat st n in dom ax holds
ax . n = (a . n) * ((chi (F . n),X) . x) ) ) ) ) by A1, Th3;
take F ; :: thesis: ex a being FinSequence of ExtREAL st F,a are_Re-presentation_of f
take a ; :: thesis: F,a are_Re-presentation_of f
thus F,a are_Re-presentation_of f by A2, Def1; :: thesis: verum