:: MESFUNC4 semantic presentation

theorem Th1: :: MESFUNC4:1
for b1, b2, b3 being FinSequence of ExtREAL st ( for b4 being Nat st b4 in dom b1 holds
0. <=' b1 . b4 ) & ( for b4 being Nat st b4 in dom b2 holds
0. <=' b2 . b4 ) & dom b1 = dom b2 & b3 = b1 + b2 holds
Sum b3 = (Sum b1) + (Sum b2)
proof end;

theorem Th2: :: MESFUNC4:2
for b1 being non empty set
for b2 being sigma_Field_Subset of b1
for b3 being sigma_Measure of b2
for b4 being Nat
for b5 being PartFunc of b1, ExtREAL
for b6 being Finite_Sep_Sequence of b2
for b7, b8 being FinSequence of ExtREAL st b5 is_simple_func_in b2 & dom b5 <> {} & ( for b9 being set st b9 in dom b5 holds
0. <=' b5 . b9 ) & b6,b7 are_Re-presentation_of b5 & dom b8 = dom b6 & ( for b9 being Nat st b9 in dom b8 holds
b8 . b9 = (b7 . b9) * ((b3 * b6) . b9) ) & len b6 = b4 holds
integral b1,b2,b3,b5 = Sum b8
proof end;

theorem Th3: :: MESFUNC4:3
for b1 being non empty set
for b2 being sigma_Field_Subset of b1
for b3 being PartFunc of b1, ExtREAL
for b4 being sigma_Measure of b2
for b5 being Finite_Sep_Sequence of b2
for b6, b7 being FinSequence of ExtREAL st b3 is_simple_func_in b2 & dom b3 <> {} & ( for b8 being set st b8 in dom b3 holds
0. <=' b3 . b8 ) & b5,b6 are_Re-presentation_of b3 & dom b7 = dom b5 & ( for b8 being Nat st b8 in dom b7 holds
b7 . b8 = (b6 . b8) * ((b4 * b5) . b8) ) holds
integral b1,b2,b4,b3 = Sum b7
proof end;

theorem Th4: :: MESFUNC4:4
for b1 being non empty set
for b2 being sigma_Field_Subset of b1
for b3 being PartFunc of b1, ExtREAL
for b4 being sigma_Measure of b2 st b3 is_simple_func_in b2 & dom b3 <> {} & ( for b5 being set st b5 in dom b3 holds
0. <=' b3 . b5 ) holds
ex b5 being Finite_Sep_Sequence of b2ex b6, b7 being FinSequence of ExtREAL st
( b5,b6 are_Re-presentation_of b3 & dom b7 = dom b5 & ( for b8 being Nat st b8 in dom b7 holds
b7 . b8 = (b6 . b8) * ((b4 * b5) . b8) ) & integral b1,b2,b4,b3 = Sum b7 )
proof end;

theorem Th5: :: MESFUNC4:5
for b1 being non empty set
for b2 being sigma_Field_Subset of b1
for b3 being sigma_Measure of b2
for b4, b5 being PartFunc of b1, ExtREAL st b4 is_simple_func_in b2 & dom b4 <> {} & ( for b6 being set st b6 in dom b4 holds
0. <=' b4 . b6 ) & b5 is_simple_func_in b2 & dom b5 = dom b4 & ( for b6 being set st b6 in dom b5 holds
0. <=' b5 . b6 ) holds
( b4 + b5 is_simple_func_in b2 & dom (b4 + b5) <> {} & ( for b6 being set st b6 in dom (b4 + b5) holds
0. <=' (b4 + b5) . b6 ) & integral b1,b2,b3,(b4 + b5) = (integral b1,b2,b3,b4) + (integral b1,b2,b3,b5) )
proof end;

theorem Th6: :: MESFUNC4:6
for b1 being non empty set
for b2 being sigma_Field_Subset of b1
for b3 being sigma_Measure of b2
for b4, b5 being PartFunc of b1, ExtREAL
for b6 being R_eal st b4 is_simple_func_in b2 & dom b4 <> {} & ( for b7 being set st b7 in dom b4 holds
0. <=' b4 . b7 ) & 0. <=' b6 & b6 <' +infty & dom b5 = dom b4 & ( for b7 being set st b7 in dom b5 holds
b5 . b7 = b6 * (b4 . b7) ) holds
integral b1,b2,b3,b5 = b6 * (integral b1,b2,b3,b4)
proof end;