let X be non empty set ; :: thesis: for S being SigmaField of X
for f being PartFunc of X,COMPLEX holds
( f is_simple_func_in S iff ex F being Finite_Sep_Sequence of S ex a being FinSequence of COMPLEX st F,a are_Re-presentation_of f )

let S be SigmaField of X; :: thesis: for f being PartFunc of X,COMPLEX holds
( f is_simple_func_in S iff ex F being Finite_Sep_Sequence of S ex a being FinSequence of COMPLEX st F,a are_Re-presentation_of f )

let f be PartFunc of X,COMPLEX; :: thesis: ( f is_simple_func_in S iff ex F being Finite_Sep_Sequence of S ex a being FinSequence of COMPLEX st F,a are_Re-presentation_of f )
hereby :: thesis: ( ex F being Finite_Sep_Sequence of S ex a being FinSequence of COMPLEX st F,a are_Re-presentation_of f implies f is_simple_func_in S )
assume f is_simple_func_in S ; :: thesis: ex F being Finite_Sep_Sequence of S ex a being FinSequence of COMPLEX st F,a are_Re-presentation_of f
then consider F being Finite_Sep_Sequence of S, a being FinSequence of COMPLEX such that
A1: ( 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 ) ) by Th44;
take F = F; :: thesis: ex a being FinSequence of COMPLEX st F,a are_Re-presentation_of f
take a = a; :: thesis:
thus F,a are_Re-presentation_of f by A1; :: thesis: verum
end;
given F being Finite_Sep_Sequence of S, a being FinSequence of COMPLEX such that A2: F,a are_Re-presentation_of f ; :: thesis:
A3: 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 that
A4: n in dom F and
A5: x in F . n and
A6: y in F . n ; :: thesis: f . x = f . y
f . x = a . n by A2, A4, A5;
hence f . x = f . y by A2, A4, A6; :: thesis: verum
end;
dom f = union (rng F) by A2;
hence f is_simple_func_in S by A3; :: thesis: verum