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 )

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

hence f is_simple_func_in S by A3; :: thesis: verum

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 )

given F being Finite_Sep_Sequence of S, a being FinSequence of COMPLEX such that A2:
F,a are_Re-presentation_of f
; :: thesis: f is_simple_func_in Sassume
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: F,a are_Re-presentation_of f

thus F,a are_Re-presentation_of f by A1; :: thesis: verum

end;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: F,a are_Re-presentation_of f

thus F,a are_Re-presentation_of f by A1; :: thesis: verum

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

dom f = union (rng F)
by A2;
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;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

hence f is_simple_func_in S by A3; :: thesis: verum