let X be non empty set ; :: thesis:
let S be SigmaField of X; :: thesis:
let f be PartFunc of X,COMPLEX; :: thesis:

assume f is_simple_func_in S ; :: thesis:
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:
take a = a; :: thesis:
thus F,a are_Re-presentation_of f by A1; :: thesis:

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

let n be Nat; :: thesis:
let x, y be Element of X; :: thesis:
assume that
A4: n in dom F and
A5: x in F . n and
A6: y in F . n ; :: thesis:
f . x = a . n by A2, A4, A5;
hence f . x = f . y by A2, A4, A6; :: thesis:

end;