let X be non empty set ; for S being SigmaField of X
for E being Element of S holds chi (E,X) is_simple_func_in S
let S be SigmaField of X; for E being Element of S holds chi (E,X) is_simple_func_in S
let E be Element of S; chi (E,X) is_simple_func_in S
X in S
by MEASURE1:7;
then reconsider E2 = X \ E as Element of S by MEASURE1:6;
E misses E2
by XBOOLE_1:79;
then reconsider EE = <*E,E2*> as Finite_Sep_Sequence of S by Th6;
( 1 (#) (chi (E,X)) = chi (1,E,X) & 0 (#) (chi (E2,X)) = chi (0,E2,X) )
by Th1;
then reconsider F = <*(1 (#) (chi (E,X))),(0 (#) (chi (E2,X)))*> as summable FinSequence of Funcs (X,ExtREAL) by Th7;
A1:
( dom EE = {1,2} & dom F = {1,2} )
by FINSEQ_1:92;
rng EE = (rng <*E*>) \/ (rng <*E2*>)
by FINSEQ_1:31;
then
rng EE = {E} \/ (rng <*E2*>)
by FINSEQ_1:38;
then
rng EE = {E} \/ {E2}
by FINSEQ_1:38;
then
rng EE = {E,E2}
by ENUMSET1:1;
then
union (rng EE) = E \/ E2
by ZFMISC_1:75;
then
union (rng EE) = E \/ X
by XBOOLE_1:39;
then
union (rng EE) = X
by XBOOLE_1:12;
then A2:
dom (chi (E,X)) = union (rng EE)
by FUNCT_2:def 1;
A3:
for n being Nat st n in dom F holds
ex r being Real st F /. n = r (#) (chi ((EE . n),X))
( 1 in dom F & 2 in dom F )
by A1, TARSKI:def 2;
then
( F /. 1 = F . 1 & F /. 2 = F . 2 )
by PARTFUN1:def 6;
then
( F /. 1 = 1 (#) (chi (E,X)) & F /. 2 = 0 (#) (chi (E2,X)) )
by FINSEQ_1:44;
then A4:
( F /. 1 = chi (E,X) & F /. 2 = X --> 0 )
by MESFUNC2:1, MESFUN11:22;
len F = 2
by FINSEQ_1:44;
then
(Partial_Sums F) /. (len F) = (F /. 1) + (F /. 2)
by Th8;
then
(Partial_Sums F) /. (len F) = chi (E,X)
by A4, Th9;
hence
chi (E,X) is_simple_func_in S
by A1, A2, A3, Th11; verum