let X be non empty set ; :: thesis:
let S be SigmaField of X; :: thesis:
let f be PartFunc of X,REAL ; :: thesis:
let M be sigma_Measure of S; :: thesis:
let F be Finite_Sep_Sequence of S; :: thesis:
let a be FinSequence of REAL ; :: thesis:
let x be FinSequence of ExtREAL ; :: thesis:
assume that
A1: f is_simple_func_in S and
A2: dom f <> {} and
A3: f is nonnegative and
A4: ( 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 ) ) and
A5: dom x = dom F and
A6: for n being Nat st n in dom x holds
x . n = (R_EAL (a . n)) * ((M * F) . n) ; :: thesis:
A7: ( R_EAL f is_simple_func_in S & ( for x being set st x in dom (R_EAL f) holds
0 <= (R_EAL f) . x ) ) by A1, A3, MESFUNC6:49, MESFUNC6:51;
reconsider a0 = a as FinSequence of ExtREAL by MESFUNC3:11;
A8: F,a0 are_Re-presentation_of R_EAL f by A4, MESFUNC3:def 1;
A9: for n being Nat st n in dom x holds
x . n = (a0 . n) * ((M * F) . n)

let n be Nat; :: thesis:
assume n in dom x ; :: thesis:
then x . n = (R_EAL (a . n)) * ((M * F) . n) by A6;
hence x . n = (a0 . n) * ((M * F) . n) ; :: thesis:

end;