:: MESFUNC3 semantic presentation

theorem Th1: :: MESFUNC3:1
for b1, b2 being Nat
for b3 being Function of [:(Seg b1),(Seg b2):], REAL
for b4, b5 being FinSequence of REAL st dom b4 = Seg b1 & ( for b6 being Nat st b6 in dom b4 holds
ex b7 being FinSequence of REAL st
( dom b7 = Seg b2 & b4 . b6 = Sum b7 & ( for b8 being Nat st b8 in dom b7 holds
b7 . b8 = b3 . [b6,b8] ) ) ) & dom b5 = Seg b2 & ( for b6 being Nat st b6 in dom b5 holds
ex b7 being FinSequence of REAL st
( dom b7 = Seg b1 & b5 . b6 = Sum b7 & ( for b8 being Nat st b8 in dom b7 holds
b7 . b8 = b3 . [b8,b6] ) ) ) holds
Sum b4 = Sum b5
proof end;

theorem Th2: :: MESFUNC3:2
for b1 being FinSequence of ExtREAL
for b2 being FinSequence of REAL st b1 = b2 holds
Sum b1 = Sum b2
proof end;

theorem Th3: :: MESFUNC3:3
for b1 being non empty set
for b2 being sigma_Field_Subset of b1
for b3 being PartFunc of b1, ExtREAL st b3 is_simple_func_in b2 holds
ex b4 being Finite_Sep_Sequence of b2ex b5 being FinSequence of ExtREAL st
( dom b3 = union (rng b4) & dom b4 = dom b5 & ( for b6 being Nat st b6 in dom b4 holds
for b7 being set st b7 in b4 . b6 holds
b3 . b7 = b5 . b6 ) & ( for b6 being set st b6 in dom b3 holds
ex b7 being FinSequence of ExtREAL st
( dom b7 = dom b5 & ( for b8 being Nat st b8 in dom b7 holds
b7 . b8 = (b5 . b8) * ((chi (b4 . b8),b1) . b6) ) ) ) )
proof end;

theorem Th4: :: MESFUNC3:4
for b1 being set
for b2 being FinSequence of b1 holds
( b2 is disjoint_valued iff for b3, b4 being Nat st b3 in dom b2 & b4 in dom b2 & b3 <> b4 holds
b2 . b3 misses b2 . b4 )
proof end;

theorem Th5: :: MESFUNC3:5
for b1 being non empty set
for b2 being set
for b3 being sigma_Field_Subset of b1
for b4 being Finite_Sep_Sequence of b3
for b5 being FinSequence of b3 st dom b5 = dom b4 & ( for b6 being Nat st b6 in dom b5 holds
b5 . b6 = b2 /\ (b4 . b6) ) holds
b5 is Finite_Sep_Sequence of b3
proof end;

theorem Th6: :: MESFUNC3:6
for b1 being non empty set
for b2 being set
for b3, b4 being FinSequence of b1 st dom b4 = dom b3 & ( for b5 being Nat st b5 in dom b4 holds
b4 . b5 = b2 /\ (b3 . b5) ) holds
union (rng b4) = b2 /\ (union (rng b3))
proof end;

theorem Th7: :: MESFUNC3:7
for b1 being set
for b2 being FinSequence of b1
for b3 being Nat st b3 in dom b2 holds
( b2 . b3 c= union (rng b2) & (b2 . b3) /\ (union (rng b2)) = b2 . b3 )
proof end;

theorem Th8: :: MESFUNC3:8
for b1 being non empty set
for b2 being sigma_Field_Subset of b1
for b3 being sigma_Measure of b2
for b4 being Finite_Sep_Sequence of b2 holds dom b4 = dom (b3 * b4)
proof end;

theorem Th9: :: MESFUNC3:9
for b1 being non empty set
for b2 being sigma_Field_Subset of b1
for b3 being sigma_Measure of b2
for b4 being Finite_Sep_Sequence of b2 holds b3 . (union (rng b4)) = Sum (b3 * b4)
proof end;

theorem Th10: :: MESFUNC3:10
for b1, b2 being FinSequence of ExtREAL
for b3 being R_eal st ( ( b3 <> +infty & b3 <> -infty ) or for b4 being Nat st b4 in dom b1 holds
b1 . b4 <' 0. or for b4 being Nat st b4 in dom b1 holds
0. <' b1 . b4 ) & dom b1 = dom b2 & ( for b4 being Nat st b4 in dom b2 holds
b2 . b4 = b3 * (b1 . b4) ) holds
Sum b2 = b3 * (Sum b1)
proof end;

theorem Th11: :: MESFUNC3:11
for b1 being FinSequence of REAL holds b1 is FinSequence of ExtREAL
proof end;

definition
let c1 be non empty set ;
let c2 be sigma_Field_Subset of c1;
let c3 be PartFunc of c1, ExtREAL ;
let c4 be Finite_Sep_Sequence of c2;
let c5 be FinSequence of ExtREAL ;
pred c4,c5 are_Re-presentation_of c3 means :Def1: :: MESFUNC3:def 1
( dom a3 = union (rng a4) & dom a4 = dom a5 & ( for b1 being Nat st b1 in dom a4 holds
for b2 being set st b2 in a4 . b1 holds
a3 . b2 = a5 . b1 ) );
end;

:: deftheorem Def1 defines are_Re-presentation_of MESFUNC3:def 1 :
for b1 being non empty set
for b2 being sigma_Field_Subset of b1
for b3 being PartFunc of b1, ExtREAL
for b4 being Finite_Sep_Sequence of b2
for b5 being FinSequence of ExtREAL holds
( b4,b5 are_Re-presentation_of b3 iff ( dom b3 = union (rng b4) & dom b4 = dom b5 & ( for b6 being Nat st b6 in dom b4 holds
for b7 being set st b7 in b4 . b6 holds
b3 . b7 = b5 . b6 ) ) );

theorem Th12: :: MESFUNC3:12
for b1 being non empty set
for b2 being sigma_Field_Subset of b1
for b3 being PartFunc of b1, ExtREAL st b3 is_simple_func_in b2 holds
ex b4 being Finite_Sep_Sequence of b2ex b5 being FinSequence of ExtREAL st b4,b5 are_Re-presentation_of b3
proof end;

theorem Th13: :: MESFUNC3:13
for b1 being non empty set
for b2 being sigma_Field_Subset of b1
for b3 being Finite_Sep_Sequence of b2 ex b4 being Finite_Sep_Sequence of b2 st
( union (rng b3) = union (rng b4) & ( for b5 being Nat st b5 in dom b4 holds
( b4 . b5 <> {} & ex b6 being Nat st
( b6 in dom b3 & b3 . b6 = b4 . b5 ) ) ) )
proof end;

Lemma14: for b1 being FinSequence of ExtREAL
for b2, b3 being Element of ExtREAL st b3 = len b1 & ( for b4 being Nat st b4 in dom b1 holds
b1 . b4 = b2 ) holds
Sum b1 = b3 * b2
proof end;

Lemma15: for b1 being non empty set
for b2 being sigma_Field_Subset of b1
for b3 being PartFunc of b1, ExtREAL st b3 is_simple_func_in b2 & ( for b4 being set st b4 in dom b3 holds
0. <=' b3 . b4 ) & ( for b4 being set st b4 in dom b3 holds
0. <> b3 . b4 ) holds
ex b4 being Finite_Sep_Sequence of b2ex b5 being FinSequence of ExtREAL st
( b4,b5 are_Re-presentation_of b3 & b5 . 1 = 0. & ( for b6 being Nat st 2 <= b6 & b6 in dom b5 holds
( 0. <' b5 . b6 & b5 . b6 <' +infty ) ) )
proof end;

Lemma16: for b1 being non empty set
for b2 being sigma_Field_Subset of b1
for b3 being PartFunc of b1, ExtREAL st b3 is_simple_func_in b2 & ( for b4 being set st b4 in dom b3 holds
0. <=' b3 . b4 ) & ex b4 being set st
( b4 in dom b3 & 0. = b3 . b4 ) holds
ex b4 being Finite_Sep_Sequence of b2ex b5 being FinSequence of ExtREAL st
( b4,b5 are_Re-presentation_of b3 & b5 . 1 = 0. & ( for b6 being Nat st 2 <= b6 & b6 in dom b5 holds
( 0. <' b5 . b6 & b5 . b6 <' +infty ) ) )
proof end;

theorem Th14: :: MESFUNC3:14
for b1 being non empty set
for b2 being sigma_Field_Subset of b1
for b3 being PartFunc of b1, ExtREAL st b3 is_simple_func_in b2 & ( for b4 being set st b4 in dom b3 holds
0. <=' b3 . b4 ) holds
ex b4 being Finite_Sep_Sequence of b2ex b5 being FinSequence of ExtREAL st
( b4,b5 are_Re-presentation_of b3 & b5 . 1 = 0. & ( for b6 being Nat st 2 <= b6 & b6 in dom b5 holds
( 0. <' b5 . b6 & b5 . b6 <' +infty ) ) )
proof end;

theorem Th15: :: MESFUNC3:15
for b1 being non empty set
for b2 being sigma_Field_Subset of b1
for b3 being PartFunc of b1, ExtREAL
for b4 being Finite_Sep_Sequence of b2
for b5 being FinSequence of ExtREAL
for b6 being Element of b1 st b4,b5 are_Re-presentation_of b3 & b6 in dom b3 holds
ex b7 being FinSequence of ExtREAL st
( dom b7 = dom b5 & ( for b8 being Nat st b8 in dom b7 holds
b7 . b8 = (b5 . b8) * ((chi (b4 . b8),b1) . b6) ) & b3 . b6 = Sum b7 )
proof end;

theorem Th16: :: MESFUNC3:16
for b1 being FinSequence of ExtREAL
for b2 being FinSequence of REAL st b1 = b2 holds
Sum b1 = Sum b2
proof end;

theorem Th17: :: MESFUNC3:17
for b1 being FinSequence of ExtREAL st ( for b2 being Nat st b2 in dom b1 holds
0. <=' b1 . b2 ) & ex b2 being Nat st
( b2 in dom b1 & b1 . b2 = +infty ) holds
Sum b1 = +infty
proof end;

definition
let c1 be non empty set ;
let c2 be sigma_Field_Subset of c1;
let c3 be sigma_Measure of c2;
let c4 be PartFunc of c1, ExtREAL ;
assume E19: ( c4 is_simple_func_in c2 & dom c4 <> {} & ( for b1 being set st b1 in dom c4 holds
0. <=' c4 . b1 ) ) ;
func integral c1,c2,c3,c4 -> Element of ExtREAL means :: MESFUNC3:def 2
ex b1 being Finite_Sep_Sequence of a2ex b2, b3 being FinSequence of ExtREAL st
( b1,b2 are_Re-presentation_of a4 & b2 . 1 = 0. & ( for b4 being Nat st 2 <= b4 & b4 in dom b2 holds
( 0. <' b2 . b4 & b2 . b4 <' +infty ) ) & dom b3 = dom b1 & ( for b4 being Nat st b4 in dom b3 holds
b3 . b4 = (b2 . b4) * ((a3 * b1) . b4) ) & a5 = Sum b3 );
existence
ex b1 being Element of ExtREAL ex b2 being Finite_Sep_Sequence of c2ex b3, b4 being FinSequence of ExtREAL st
( b2,b3 are_Re-presentation_of c4 & b3 . 1 = 0. & ( for b5 being Nat st 2 <= b5 & b5 in dom b3 holds
( 0. <' b3 . b5 & b3 . b5 <' +infty ) ) & dom b4 = dom b2 & ( for b5 being Nat st b5 in dom b4 holds
b4 . b5 = (b3 . b5) * ((c3 * b2) . b5) ) & b1 = Sum b4 )
proof end;
uniqueness
for b1, b2 being Element of ExtREAL st ex b3 being Finite_Sep_Sequence of c2ex b4, b5 being FinSequence of ExtREAL st
( b3,b4 are_Re-presentation_of c4 & b4 . 1 = 0. & ( for b6 being Nat st 2 <= b6 & b6 in dom b4 holds
( 0. <' b4 . b6 & b4 . b6 <' +infty ) ) & dom b5 = dom b3 & ( for b6 being Nat st b6 in dom b5 holds
b5 . b6 = (b4 . b6) * ((c3 * b3) . b6) ) & b1 = Sum b5 ) & ex b3 being Finite_Sep_Sequence of c2ex b4, b5 being FinSequence of ExtREAL st
( b3,b4 are_Re-presentation_of c4 & b4 . 1 = 0. & ( for b6 being Nat st 2 <= b6 & b6 in dom b4 holds
( 0. <' b4 . b6 & b4 . b6 <' +infty ) ) & dom b5 = dom b3 & ( for b6 being Nat st b6 in dom b5 holds
b5 . b6 = (b4 . b6) * ((c3 * b3) . b6) ) & b2 = Sum b5 ) holds
b1 = b2
proof end;
end;

:: deftheorem Def2 defines integral MESFUNC3:def 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 PartFunc of b1, ExtREAL st b4 is_simple_func_in b2 & dom b4 <> {} & ( for b5 being set st b5 in dom b4 holds
0. <=' b4 . b5 ) holds
for b5 being Element of ExtREAL holds
( b5 = integral b1,b2,b3,b4 iff ex b6 being Finite_Sep_Sequence of b2ex b7, b8 being FinSequence of ExtREAL st
( b6,b7 are_Re-presentation_of b4 & b7 . 1 = 0. & ( for b9 being Nat st 2 <= b9 & b9 in dom b7 holds
( 0. <' b7 . b9 & b7 . b9 <' +infty ) ) & dom b8 = dom b6 & ( for b9 being Nat st b9 in dom b8 holds
b8 . b9 = (b7 . b9) * ((b3 * b6) . b9) ) & b5 = Sum b8 ) );

theorem Th18: :: MESFUNC3:18
for b1 being FinSequence of ExtREAL
for b2, b3 being Element of ExtREAL st b3 = len b1 & ( for b4 being Nat st b4 in dom b1 holds
b1 . b4 = b2 ) holds
Sum b1 = b3 * b2 by Lemma14;