let X be non empty set ; :: thesis: 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; :: thesis: for E being Element of S holds chi (E,X) is_simple_func_in S
let E be Element of S; :: thesis: 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))
proof
let n be Nat; :: thesis: ( n in dom F implies ex r being Real st F /. n = r (#) (chi ((EE . n),X)) )
assume A4: n in dom F ; :: thesis: ex r being Real st F /. n = r (#) (chi ((EE . n),X))
per cases ( n = 1 or n = 2 ) by A1, A4, TARSKI:def 2;
suppose n = 1 ; :: thesis: ex r being Real st F /. n = r (#) (chi ((EE . n),X))
then ( F . n = 1 (#) (chi (E,X)) & EE . n = E ) by FINSEQ_1:44;
hence ex r being Real st F /. n = r (#) (chi ((EE . n),X)) by A4, PARTFUN1:def 6; :: thesis: verum
end;
suppose n = 2 ; :: thesis: ex r being Real st F /. n = r (#) (chi ((EE . n),X))
then ( F . n = 0 (#) (chi (E2,X)) & EE . n = E2 ) by FINSEQ_1:44;
hence ex r being Real st F /. n = r (#) (chi ((EE . n),X)) by A4, PARTFUN1:def 6; :: thesis: verum
end;
end;
end;
( 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; :: thesis: verum