let X be non empty set ; :: thesis:
let S be SigmaField of X; :: thesis:
let f be PartFunc of X,REAL; :: thesis:
assume f is_simple_func_in S ; :: thesis:
then consider F being Finite_Sep_Sequence of S such that
A1: dom f = union (rng F) and
A2: 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 ;
defpred S₁[ Nat, Real] means for x being set st x in F . $1 holds
$2 = f . x;
A3: for k being Nat st k in Seg (len F) holds
ex y being Element of REAL st S₁[k,y]

proof

let k be Nat; :: thesis:
assume k in Seg (len F) ; :: thesis:
then A4: k in dom F by FINSEQ_1:def 3;
then A5: F . k in rng F by FUNCT_1:3;

per cases ;

suppose A6: F . k = {} ; :: thesis:

take In (0,REAL) ; :: thesis:
thus S₁[k, In (0,REAL)] by A6; :: thesis:

end;

suppose F . k <> {} ; :: thesis:

then consider x1 being object such that
A7: x1 in F . k by XBOOLE_0:def 1;
reconsider fx1 = f . x1 as Element of REAL by XREAL_0:def 1;
take fx1 ; :: thesis:
rng F c= bool X by XBOOLE_1:1;
hence S₁[k,fx1] by A2, A4, A5, A7; :: thesis:

end;

end;

end;

consider a being FinSequence of REAL such that
A8: ( dom a = Seg (len F) & ( for k being Nat st k in Seg (len F) holds
S₁[k,a . k] ) ) from FINSEQ_1:sch 5(A3);
take F ; :: thesis:
take a ; :: thesis:
for n being Nat st n in dom F holds
for x being set st x in F . n holds
a . n = f . x

proof

let n be Nat; :: thesis:
assume n in dom F ; :: thesis:
then n in Seg (len F) by FINSEQ_1:def 3;
hence for x being set st x in F . n holds
a . n = f . x by A8; :: thesis:

end;

hence ( 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 A1, A8, FINSEQ_1:def 3; :: thesis: