:: MESFUNC4 semantic presentation

begin

theorem :: MESFUNC4:1
for F, G, H being ( ( ) ( Relation-like NAT : ( ( ) ( non empty V15() V16() V17() V37() V42() V43() V85() V86() V87() V88() V89() V90() V91() ) Element of K19(REAL : ( ( ) ( non empty V37() V85() V86() V87() V91() ) set ) ) : ( ( ) ( V37() ) set ) ) -defined ExtREAL : ( ( ) ( non empty V86() ) set ) -valued Function-like V37() FinSequence-like FinSubsequence-like V62() ) FinSequence of ExtREAL : ( ( ) ( non empty V86() ) set ) ) st ( for i being ( ( V21() ) ( V15() V16() V17() V21() V22() V23() ext-real non negative V37() V42() ) Nat) st i : ( ( V21() ) ( V15() V16() V17() V21() V22() V23() ext-real non negative V37() V42() ) Nat) in dom F : ( ( ) ( Relation-like NAT : ( ( ) ( non empty V15() V16() V17() V37() V42() V43() V85() V86() V87() V88() V89() V90() V91() ) Element of K19(REAL : ( ( ) ( non empty V37() V85() V86() V87() V91() ) set ) ) : ( ( ) ( V37() ) set ) ) -defined ExtREAL : ( ( ) ( non empty V86() ) set ) -valued Function-like V37() FinSequence-like FinSubsequence-like V62() ) FinSequence of ExtREAL : ( ( ) ( non empty V86() ) set ) ) : ( ( ) ( V85() V86() V87() V88() V89() V90() ) Element of K19(NAT : ( ( ) ( non empty V15() V16() V17() V37() V42() V43() V85() V86() V87() V88() V89() V90() V91() ) Element of K19(REAL : ( ( ) ( non empty V37() V85() V86() V87() V91() ) set ) ) : ( ( ) ( V37() ) set ) ) ) : ( ( ) ( V37() ) set ) ) holds
0. : ( ( ) ( ext-real ) Element of ExtREAL : ( ( ) ( non empty V86() ) set ) ) <= F : ( ( ) ( Relation-like NAT : ( ( ) ( non empty V15() V16() V17() V37() V42() V43() V85() V86() V87() V88() V89() V90() V91() ) Element of K19(REAL : ( ( ) ( non empty V37() V85() V86() V87() V91() ) set ) ) : ( ( ) ( V37() ) set ) ) -defined ExtREAL : ( ( ) ( non empty V86() ) set ) -valued Function-like V37() FinSequence-like FinSubsequence-like V62() ) FinSequence of ExtREAL : ( ( ) ( non empty V86() ) set ) ) . i : ( ( V21() ) ( V15() V16() V17() V21() V22() V23() ext-real non negative V37() V42() ) Nat) : ( ( ) ( ext-real ) Element of ExtREAL : ( ( ) ( non empty V86() ) set ) ) ) & ( for i being ( ( V21() ) ( V15() V16() V17() V21() V22() V23() ext-real non negative V37() V42() ) Nat) st i : ( ( V21() ) ( V15() V16() V17() V21() V22() V23() ext-real non negative V37() V42() ) Nat) in dom G : ( ( ) ( Relation-like NAT : ( ( ) ( non empty V15() V16() V17() V37() V42() V43() V85() V86() V87() V88() V89() V90() V91() ) Element of K19(REAL : ( ( ) ( non empty V37() V85() V86() V87() V91() ) set ) ) : ( ( ) ( V37() ) set ) ) -defined ExtREAL : ( ( ) ( non empty V86() ) set ) -valued Function-like V37() FinSequence-like FinSubsequence-like V62() ) FinSequence of ExtREAL : ( ( ) ( non empty V86() ) set ) ) : ( ( ) ( V85() V86() V87() V88() V89() V90() ) Element of K19(NAT : ( ( ) ( non empty V15() V16() V17() V37() V42() V43() V85() V86() V87() V88() V89() V90() V91() ) Element of K19(REAL : ( ( ) ( non empty V37() V85() V86() V87() V91() ) set ) ) : ( ( ) ( V37() ) set ) ) ) : ( ( ) ( V37() ) set ) ) holds
0. : ( ( ) ( ext-real ) Element of ExtREAL : ( ( ) ( non empty V86() ) set ) ) <= G : ( ( ) ( Relation-like NAT : ( ( ) ( non empty V15() V16() V17() V37() V42() V43() V85() V86() V87() V88() V89() V90() V91() ) Element of K19(REAL : ( ( ) ( non empty V37() V85() V86() V87() V91() ) set ) ) : ( ( ) ( V37() ) set ) ) -defined ExtREAL : ( ( ) ( non empty V86() ) set ) -valued Function-like V37() FinSequence-like FinSubsequence-like V62() ) FinSequence of ExtREAL : ( ( ) ( non empty V86() ) set ) ) . i : ( ( V21() ) ( V15() V16() V17() V21() V22() V23() ext-real non negative V37() V42() ) Nat) : ( ( ) ( ext-real ) Element of ExtREAL : ( ( ) ( non empty V86() ) set ) ) ) & dom F : ( ( ) ( Relation-like NAT : ( ( ) ( non empty V15() V16() V17() V37() V42() V43() V85() V86() V87() V88() V89() V90() V91() ) Element of K19(REAL : ( ( ) ( non empty V37() V85() V86() V87() V91() ) set ) ) : ( ( ) ( V37() ) set ) ) -defined ExtREAL : ( ( ) ( non empty V86() ) set ) -valued Function-like V37() FinSequence-like FinSubsequence-like V62() ) FinSequence of ExtREAL : ( ( ) ( non empty V86() ) set ) ) : ( ( ) ( V85() V86() V87() V88() V89() V90() ) Element of K19(NAT : ( ( ) ( non empty V15() V16() V17() V37() V42() V43() V85() V86() V87() V88() V89() V90() V91() ) Element of K19(REAL : ( ( ) ( non empty V37() V85() V86() V87() V91() ) set ) ) : ( ( ) ( V37() ) set ) ) ) : ( ( ) ( V37() ) set ) ) = dom G : ( ( ) ( Relation-like NAT : ( ( ) ( non empty V15() V16() V17() V37() V42() V43() V85() V86() V87() V88() V89() V90() V91() ) Element of K19(REAL : ( ( ) ( non empty V37() V85() V86() V87() V91() ) set ) ) : ( ( ) ( V37() ) set ) ) -defined ExtREAL : ( ( ) ( non empty V86() ) set ) -valued Function-like V37() FinSequence-like FinSubsequence-like V62() ) FinSequence of ExtREAL : ( ( ) ( non empty V86() ) set ) ) : ( ( ) ( V85() V86() V87() V88() V89() V90() ) Element of K19(NAT : ( ( ) ( non empty V15() V16() V17() V37() V42() V43() V85() V86() V87() V88() V89() V90() V91() ) Element of K19(REAL : ( ( ) ( non empty V37() V85() V86() V87() V91() ) set ) ) : ( ( ) ( V37() ) set ) ) ) : ( ( ) ( V37() ) set ) ) & H : ( ( ) ( Relation-like NAT : ( ( ) ( non empty V15() V16() V17() V37() V42() V43() V85() V86() V87() V88() V89() V90() V91() ) Element of K19(REAL : ( ( ) ( non empty V37() V85() V86() V87() V91() ) set ) ) : ( ( ) ( V37() ) set ) ) -defined ExtREAL : ( ( ) ( non empty V86() ) set ) -valued Function-like V37() FinSequence-like FinSubsequence-like V62() ) FinSequence of ExtREAL : ( ( ) ( non empty V86() ) set ) ) = F : ( ( ) ( Relation-like NAT : ( ( ) ( non empty V15() V16() V17() V37() V42() V43() V85() V86() V87() V88() V89() V90() V91() ) Element of K19(REAL : ( ( ) ( non empty V37() V85() V86() V87() V91() ) set ) ) : ( ( ) ( V37() ) set ) ) -defined ExtREAL : ( ( ) ( non empty V86() ) set ) -valued Function-like V37() FinSequence-like FinSubsequence-like V62() ) FinSequence of ExtREAL : ( ( ) ( non empty V86() ) set ) ) + G : ( ( ) ( Relation-like NAT : ( ( ) ( non empty V15() V16() V17() V37() V42() V43() V85() V86() V87() V88() V89() V90() V91() ) Element of K19(REAL : ( ( ) ( non empty V37() V85() V86() V87() V91() ) set ) ) : ( ( ) ( V37() ) set ) ) -defined ExtREAL : ( ( ) ( non empty V86() ) set ) -valued Function-like V37() FinSequence-like FinSubsequence-like V62() ) FinSequence of ExtREAL : ( ( ) ( non empty V86() ) set ) ) : ( ( Function-like ) ( Relation-like NAT : ( ( ) ( non empty V15() V16() V17() V37() V42() V43() V85() V86() V87() V88() V89() V90() V91() ) Element of K19(REAL : ( ( ) ( non empty V37() V85() V86() V87() V91() ) set ) ) : ( ( ) ( V37() ) set ) ) -defined ExtREAL : ( ( ) ( non empty V86() ) set ) -valued Function-like V62() ) Element of K19(K20(NAT : ( ( ) ( non empty V15() V16() V17() V37() V42() V43() V85() V86() V87() V88() V89() V90() V91() ) Element of K19(REAL : ( ( ) ( non empty V37() V85() V86() V87() V91() ) set ) ) : ( ( ) ( V37() ) set ) ) ,ExtREAL : ( ( ) ( non empty V86() ) set ) ) : ( ( ) ( V37() V62() ) set ) ) : ( ( ) ( V37() ) set ) ) holds
Sum H : ( ( ) ( Relation-like NAT : ( ( ) ( non empty V15() V16() V17() V37() V42() V43() V85() V86() V87() V88() V89() V90() V91() ) Element of K19(REAL : ( ( ) ( non empty V37() V85() V86() V87() V91() ) set ) ) : ( ( ) ( V37() ) set ) ) -defined ExtREAL : ( ( ) ( non empty V86() ) set ) -valued Function-like V37() FinSequence-like FinSubsequence-like V62() ) FinSequence of ExtREAL : ( ( ) ( non empty V86() ) set ) ) : ( ( ) ( ext-real ) Element of ExtREAL : ( ( ) ( non empty V86() ) set ) ) = (Sum F : ( ( ) ( Relation-like NAT : ( ( ) ( non empty V15() V16() V17() V37() V42() V43() V85() V86() V87() V88() V89() V90() V91() ) Element of K19(REAL : ( ( ) ( non empty V37() V85() V86() V87() V91() ) set ) ) : ( ( ) ( V37() ) set ) ) -defined ExtREAL : ( ( ) ( non empty V86() ) set ) -valued Function-like V37() FinSequence-like FinSubsequence-like V62() ) FinSequence of ExtREAL : ( ( ) ( non empty V86() ) set ) ) ) : ( ( ) ( ext-real ) Element of ExtREAL : ( ( ) ( non empty V86() ) set ) ) + (Sum G : ( ( ) ( Relation-like NAT : ( ( ) ( non empty V15() V16() V17() V37() V42() V43() V85() V86() V87() V88() V89() V90() V91() ) Element of K19(REAL : ( ( ) ( non empty V37() V85() V86() V87() V91() ) set ) ) : ( ( ) ( V37() ) set ) ) -defined ExtREAL : ( ( ) ( non empty V86() ) set ) -valued Function-like V37() FinSequence-like FinSubsequence-like V62() ) FinSequence of ExtREAL : ( ( ) ( non empty V86() ) set ) ) ) : ( ( ) ( ext-real ) Element of ExtREAL : ( ( ) ( non empty V86() ) set ) ) : ( ( ) ( ext-real ) Element of ExtREAL : ( ( ) ( non empty V86() ) set ) ) ;

theorem :: MESFUNC4:2
for X being ( ( non empty ) ( non empty ) set )
for S being ( ( non empty compl-closed sigma-multiplicative ) ( non empty compl-closed sigma-multiplicative V79() V80() V81() sigma-additive ) SigmaField of X : ( ( non empty ) ( non empty ) set ) )
for M being ( ( Function-like V30(b2 : ( ( non empty compl-closed sigma-multiplicative ) ( non empty compl-closed sigma-multiplicative V79() V80() V81() sigma-additive ) SigmaField of b1 : ( ( non empty ) ( non empty ) set ) ) , ExtREAL : ( ( ) ( non empty V86() ) set ) ) V70() nonnegative sigma-additive ) ( Relation-like b2 : ( ( non empty compl-closed sigma-multiplicative ) ( non empty compl-closed sigma-multiplicative V79() V80() V81() sigma-additive ) SigmaField of b1 : ( ( non empty ) ( non empty ) set ) ) -defined ExtREAL : ( ( ) ( non empty V86() ) set ) -valued Function-like V30(b2 : ( ( non empty compl-closed sigma-multiplicative ) ( non empty compl-closed sigma-multiplicative V79() V80() V81() sigma-additive ) SigmaField of b1 : ( ( non empty ) ( non empty ) set ) ) , ExtREAL : ( ( ) ( non empty V86() ) set ) ) V62() V70() nonnegative sigma-additive ) sigma_Measure of S : ( ( non empty compl-closed sigma-multiplicative ) ( non empty compl-closed sigma-multiplicative V79() V80() V81() sigma-additive ) SigmaField of b1 : ( ( non empty ) ( non empty ) set ) ) )
for n being ( ( V21() ) ( V15() V16() V17() V21() V22() V23() ext-real non negative V37() V42() ) Nat)
for f being ( ( Function-like ) ( Relation-like b1 : ( ( non empty ) ( non empty ) set ) -defined ExtREAL : ( ( ) ( non empty V86() ) set ) -valued Function-like V62() ) PartFunc of ,)
for F being ( ( V83() ) ( Relation-like NAT : ( ( ) ( non empty V15() V16() V17() V37() V42() V43() V85() V86() V87() V88() V89() V90() V91() ) Element of K19(REAL : ( ( ) ( non empty V37() V85() V86() V87() V91() ) set ) ) : ( ( ) ( V37() ) set ) ) -defined b2 : ( ( non empty compl-closed sigma-multiplicative ) ( non empty compl-closed sigma-multiplicative V79() V80() V81() sigma-additive ) SigmaField of b1 : ( ( non empty ) ( non empty ) set ) ) -valued Function-like V37() FinSequence-like FinSubsequence-like V83() ) Finite_Sep_Sequence of S : ( ( non empty compl-closed sigma-multiplicative ) ( non empty compl-closed sigma-multiplicative V79() V80() V81() sigma-additive ) SigmaField of b1 : ( ( non empty ) ( non empty ) set ) ) )
for a, x being ( ( ) ( Relation-like NAT : ( ( ) ( non empty V15() V16() V17() V37() V42() V43() V85() V86() V87() V88() V89() V90() V91() ) Element of K19(REAL : ( ( ) ( non empty V37() V85() V86() V87() V91() ) set ) ) : ( ( ) ( V37() ) set ) ) -defined ExtREAL : ( ( ) ( non empty V86() ) set ) -valued Function-like V37() FinSequence-like FinSubsequence-like V62() ) FinSequence of ExtREAL : ( ( ) ( non empty V86() ) set ) ) st f : ( ( Function-like ) ( Relation-like b1 : ( ( non empty ) ( non empty ) set ) -defined ExtREAL : ( ( ) ( non empty V86() ) set ) -valued Function-like V62() ) PartFunc of ,) is_simple_func_in S : ( ( non empty compl-closed sigma-multiplicative ) ( non empty compl-closed sigma-multiplicative V79() V80() V81() sigma-additive ) SigmaField of b1 : ( ( non empty ) ( non empty ) set ) ) & dom f : ( ( Function-like ) ( Relation-like b1 : ( ( non empty ) ( non empty ) set ) -defined ExtREAL : ( ( ) ( non empty V86() ) set ) -valued Function-like V62() ) PartFunc of ,) : ( ( ) ( ) set ) <> {} : ( ( ) ( ) set ) & ( for x being ( ( ) ( ) set ) st x : ( ( V21() ) ( V15() V16() V17() V21() V22() V23() ext-real non negative V37() V42() ) Nat) in dom f : ( ( Function-like ) ( Relation-like b1 : ( ( non empty ) ( non empty ) set ) -defined ExtREAL : ( ( ) ( non empty V86() ) set ) -valued Function-like V62() ) PartFunc of ,) : ( ( ) ( ) set ) holds
0. : ( ( ) ( ext-real ) Element of ExtREAL : ( ( ) ( non empty V86() ) set ) ) <= f : ( ( Function-like ) ( Relation-like b1 : ( ( non empty ) ( non empty ) set ) -defined ExtREAL : ( ( ) ( non empty V86() ) set ) -valued Function-like V62() ) PartFunc of ,) . x : ( ( V21() ) ( V15() V16() V17() V21() V22() V23() ext-real non negative V37() V42() ) Nat) : ( ( ) ( ext-real ) Element of ExtREAL : ( ( ) ( non empty V86() ) set ) ) ) & F : ( ( V83() ) ( Relation-like NAT : ( ( ) ( non empty V15() V16() V17() V37() V42() V43() V85() V86() V87() V88() V89() V90() V91() ) Element of K19(REAL : ( ( ) ( non empty V37() V85() V86() V87() V91() ) set ) ) : ( ( ) ( V37() ) set ) ) -defined b2 : ( ( non empty compl-closed sigma-multiplicative ) ( non empty compl-closed sigma-multiplicative V79() V80() V81() sigma-additive ) SigmaField of b1 : ( ( non empty ) ( non empty ) set ) ) -valued Function-like V37() FinSequence-like FinSubsequence-like V83() ) Finite_Sep_Sequence of b2 : ( ( non empty compl-closed sigma-multiplicative ) ( non empty compl-closed sigma-multiplicative V79() V80() V81() sigma-additive ) SigmaField of b1 : ( ( non empty ) ( non empty ) set ) ) ) ,a : ( ( ) ( Relation-like NAT : ( ( ) ( non empty V15() V16() V17() V37() V42() V43() V85() V86() V87() V88() V89() V90() V91() ) Element of K19(REAL : ( ( ) ( non empty V37() V85() V86() V87() V91() ) set ) ) : ( ( ) ( V37() ) set ) ) -defined ExtREAL : ( ( ) ( non empty V86() ) set ) -valued Function-like V37() FinSequence-like FinSubsequence-like V62() ) FinSequence of ExtREAL : ( ( ) ( non empty V86() ) set ) ) are_Re-presentation_of f : ( ( Function-like ) ( Relation-like b1 : ( ( non empty ) ( non empty ) set ) -defined ExtREAL : ( ( ) ( non empty V86() ) set ) -valued Function-like V62() ) PartFunc of ,) & dom x : ( ( ) ( Relation-like NAT : ( ( ) ( non empty V15() V16() V17() V37() V42() V43() V85() V86() V87() V88() V89() V90() V91() ) Element of K19(REAL : ( ( ) ( non empty V37() V85() V86() V87() V91() ) set ) ) : ( ( ) ( V37() ) set ) ) -defined ExtREAL : ( ( ) ( non empty V86() ) set ) -valued Function-like V37() FinSequence-like FinSubsequence-like V62() ) FinSequence of ExtREAL : ( ( ) ( non empty V86() ) set ) ) : ( ( ) ( V85() V86() V87() V88() V89() V90() ) Element of K19(NAT : ( ( ) ( non empty V15() V16() V17() V37() V42() V43() V85() V86() V87() V88() V89() V90() V91() ) Element of K19(REAL : ( ( ) ( non empty V37() V85() V86() V87() V91() ) set ) ) : ( ( ) ( V37() ) set ) ) ) : ( ( ) ( V37() ) set ) ) = dom F : ( ( V83() ) ( Relation-like NAT : ( ( ) ( non empty V15() V16() V17() V37() V42() V43() V85() V86() V87() V88() V89() V90() V91() ) Element of K19(REAL : ( ( ) ( non empty V37() V85() V86() V87() V91() ) set ) ) : ( ( ) ( V37() ) set ) ) -defined b2 : ( ( non empty compl-closed sigma-multiplicative ) ( non empty compl-closed sigma-multiplicative V79() V80() V81() sigma-additive ) SigmaField of b1 : ( ( non empty ) ( non empty ) set ) ) -valued Function-like V37() FinSequence-like FinSubsequence-like V83() ) Finite_Sep_Sequence of b2 : ( ( non empty compl-closed sigma-multiplicative ) ( non empty compl-closed sigma-multiplicative V79() V80() V81() sigma-additive ) SigmaField of b1 : ( ( non empty ) ( non empty ) set ) ) ) : ( ( ) ( V85() V86() V87() V88() V89() V90() ) Element of K19(NAT : ( ( ) ( non empty V15() V16() V17() V37() V42() V43() V85() V86() V87() V88() V89() V90() V91() ) Element of K19(REAL : ( ( ) ( non empty V37() V85() V86() V87() V91() ) set ) ) : ( ( ) ( V37() ) set ) ) ) : ( ( ) ( V37() ) set ) ) & ( for i being ( ( V21() ) ( V15() V16() V17() V21() V22() V23() ext-real non negative V37() V42() ) Nat) st i : ( ( V21() ) ( V15() V16() V17() V21() V22() V23() ext-real non negative V37() V42() ) Nat) in dom x : ( ( ) ( Relation-like NAT : ( ( ) ( non empty V15() V16() V17() V37() V42() V43() V85() V86() V87() V88() V89() V90() V91() ) Element of K19(REAL : ( ( ) ( non empty V37() V85() V86() V87() V91() ) set ) ) : ( ( ) ( V37() ) set ) ) -defined ExtREAL : ( ( ) ( non empty V86() ) set ) -valued Function-like V37() FinSequence-like FinSubsequence-like V62() ) FinSequence of ExtREAL : ( ( ) ( non empty V86() ) set ) ) : ( ( ) ( V85() V86() V87() V88() V89() V90() ) Element of K19(NAT : ( ( ) ( non empty V15() V16() V17() V37() V42() V43() V85() V86() V87() V88() V89() V90() V91() ) Element of K19(REAL : ( ( ) ( non empty V37() V85() V86() V87() V91() ) set ) ) : ( ( ) ( V37() ) set ) ) ) : ( ( ) ( V37() ) set ) ) holds
x : ( ( ) ( Relation-like NAT : ( ( ) ( non empty V15() V16() V17() V37() V42() V43() V85() V86() V87() V88() V89() V90() V91() ) Element of K19(REAL : ( ( ) ( non empty V37() V85() V86() V87() V91() ) set ) ) : ( ( ) ( V37() ) set ) ) -defined ExtREAL : ( ( ) ( non empty V86() ) set ) -valued Function-like V37() FinSequence-like FinSubsequence-like V62() ) FinSequence of ExtREAL : ( ( ) ( non empty V86() ) set ) ) . i : ( ( V21() ) ( V15() V16() V17() V21() V22() V23() ext-real non negative V37() V42() ) Nat) : ( ( ) ( ext-real ) Element of ExtREAL : ( ( ) ( non empty V86() ) set ) ) = (a : ( ( ) ( Relation-like NAT : ( ( ) ( non empty V15() V16() V17() V37() V42() V43() V85() V86() V87() V88() V89() V90() V91() ) Element of K19(REAL : ( ( ) ( non empty V37() V85() V86() V87() V91() ) set ) ) : ( ( ) ( V37() ) set ) ) -defined ExtREAL : ( ( ) ( non empty V86() ) set ) -valued Function-like V37() FinSequence-like FinSubsequence-like V62() ) FinSequence of ExtREAL : ( ( ) ( non empty V86() ) set ) ) . i : ( ( V21() ) ( V15() V16() V17() V21() V22() V23() ext-real non negative V37() V42() ) Nat) ) : ( ( ) ( ext-real ) Element of ExtREAL : ( ( ) ( non empty V86() ) set ) ) * ((M : ( ( Function-like V30(b2 : ( ( non empty compl-closed sigma-multiplicative ) ( non empty compl-closed sigma-multiplicative V79() V80() V81() sigma-additive ) SigmaField of b1 : ( ( non empty ) ( non empty ) set ) ) , ExtREAL : ( ( ) ( non empty V86() ) set ) ) V70() nonnegative sigma-additive ) ( Relation-like b2 : ( ( non empty compl-closed sigma-multiplicative ) ( non empty compl-closed sigma-multiplicative V79() V80() V81() sigma-additive ) SigmaField of b1 : ( ( non empty ) ( non empty ) set ) ) -defined ExtREAL : ( ( ) ( non empty V86() ) set ) -valued Function-like V30(b2 : ( ( non empty compl-closed sigma-multiplicative ) ( non empty compl-closed sigma-multiplicative V79() V80() V81() sigma-additive ) SigmaField of b1 : ( ( non empty ) ( non empty ) set ) ) , ExtREAL : ( ( ) ( non empty V86() ) set ) ) V62() V70() nonnegative sigma-additive ) sigma_Measure of b2 : ( ( non empty compl-closed sigma-multiplicative ) ( non empty compl-closed sigma-multiplicative V79() V80() V81() sigma-additive ) SigmaField of b1 : ( ( non empty ) ( non empty ) set ) ) ) * F : ( ( V83() ) ( Relation-like NAT : ( ( ) ( non empty V15() V16() V17() V37() V42() V43() V85() V86() V87() V88() V89() V90() V91() ) Element of K19(REAL : ( ( ) ( non empty V37() V85() V86() V87() V91() ) set ) ) : ( ( ) ( V37() ) set ) ) -defined b2 : ( ( non empty compl-closed sigma-multiplicative ) ( non empty compl-closed sigma-multiplicative V79() V80() V81() sigma-additive ) SigmaField of b1 : ( ( non empty ) ( non empty ) set ) ) -valued Function-like V37() FinSequence-like FinSubsequence-like V83() ) Finite_Sep_Sequence of b2 : ( ( non empty compl-closed sigma-multiplicative ) ( non empty compl-closed sigma-multiplicative V79() V80() V81() sigma-additive ) SigmaField of b1 : ( ( non empty ) ( non empty ) set ) ) ) ) : ( ( Function-like ) ( Relation-like NAT : ( ( ) ( non empty V15() V16() V17() V37() V42() V43() V85() V86() V87() V88() V89() V90() V91() ) Element of K19(REAL : ( ( ) ( non empty V37() V85() V86() V87() V91() ) set ) ) : ( ( ) ( V37() ) set ) ) -defined ExtREAL : ( ( ) ( non empty V86() ) set ) -valued Function-like V62() ) Element of K19(K20(NAT : ( ( ) ( non empty V15() V16() V17() V37() V42() V43() V85() V86() V87() V88() V89() V90() V91() ) Element of K19(REAL : ( ( ) ( non empty V37() V85() V86() V87() V91() ) set ) ) : ( ( ) ( V37() ) set ) ) ,ExtREAL : ( ( ) ( non empty V86() ) set ) ) : ( ( ) ( V37() V62() ) set ) ) : ( ( ) ( V37() ) set ) ) . i : ( ( V21() ) ( V15() V16() V17() V21() V22() V23() ext-real non negative V37() V42() ) Nat) ) : ( ( ) ( ext-real ) Element of ExtREAL : ( ( ) ( non empty V86() ) set ) ) : ( ( ) ( ext-real ) Element of ExtREAL : ( ( ) ( non empty V86() ) set ) ) ) & len F : ( ( V83() ) ( Relation-like NAT : ( ( ) ( non empty V15() V16() V17() V37() V42() V43() V85() V86() V87() V88() V89() V90() V91() ) Element of K19(REAL : ( ( ) ( non empty V37() V85() V86() V87() V91() ) set ) ) : ( ( ) ( V37() ) set ) ) -defined b2 : ( ( non empty compl-closed sigma-multiplicative ) ( non empty compl-closed sigma-multiplicative V79() V80() V81() sigma-additive ) SigmaField of b1 : ( ( non empty ) ( non empty ) set ) ) -valued Function-like V37() FinSequence-like FinSubsequence-like V83() ) Finite_Sep_Sequence of b2 : ( ( non empty compl-closed sigma-multiplicative ) ( non empty compl-closed sigma-multiplicative V79() V80() V81() sigma-additive ) SigmaField of b1 : ( ( non empty ) ( non empty ) set ) ) ) : ( ( ) ( V15() V16() V17() V21() V22() V23() ext-real non negative V33() V37() V42() V71() V85() V86() V87() V88() V89() V90() ) Element of NAT : ( ( ) ( non empty V15() V16() V17() V37() V42() V43() V85() V86() V87() V88() V89() V90() V91() ) Element of K19(REAL : ( ( ) ( non empty V37() V85() V86() V87() V91() ) set ) ) : ( ( ) ( V37() ) set ) ) ) = n : ( ( V21() ) ( V15() V16() V17() V21() V22() V23() ext-real non negative V37() V42() ) Nat) holds
integral (X : ( ( non empty ) ( non empty ) set ) ,S : ( ( non empty compl-closed sigma-multiplicative ) ( non empty compl-closed sigma-multiplicative V79() V80() V81() sigma-additive ) SigmaField of b1 : ( ( non empty ) ( non empty ) set ) ) ,M : ( ( Function-like V30(b2 : ( ( non empty compl-closed sigma-multiplicative ) ( non empty compl-closed sigma-multiplicative V79() V80() V81() sigma-additive ) SigmaField of b1 : ( ( non empty ) ( non empty ) set ) ) , ExtREAL : ( ( ) ( non empty V86() ) set ) ) V70() nonnegative sigma-additive ) ( Relation-like b2 : ( ( non empty compl-closed sigma-multiplicative ) ( non empty compl-closed sigma-multiplicative V79() V80() V81() sigma-additive ) SigmaField of b1 : ( ( non empty ) ( non empty ) set ) ) -defined ExtREAL : ( ( ) ( non empty V86() ) set ) -valued Function-like V30(b2 : ( ( non empty compl-closed sigma-multiplicative ) ( non empty compl-closed sigma-multiplicative V79() V80() V81() sigma-additive ) SigmaField of b1 : ( ( non empty ) ( non empty ) set ) ) , ExtREAL : ( ( ) ( non empty V86() ) set ) ) V62() V70() nonnegative sigma-additive ) sigma_Measure of b2 : ( ( non empty compl-closed sigma-multiplicative ) ( non empty compl-closed sigma-multiplicative V79() V80() V81() sigma-additive ) SigmaField of b1 : ( ( non empty ) ( non empty ) set ) ) ) ,f : ( ( Function-like ) ( Relation-like b1 : ( ( non empty ) ( non empty ) set ) -defined ExtREAL : ( ( ) ( non empty V86() ) set ) -valued Function-like V62() ) PartFunc of ,) ) : ( ( ) ( ext-real ) Element of ExtREAL : ( ( ) ( non empty V86() ) set ) ) = Sum x : ( ( ) ( Relation-like NAT : ( ( ) ( non empty V15() V16() V17() V37() V42() V43() V85() V86() V87() V88() V89() V90() V91() ) Element of K19(REAL : ( ( ) ( non empty V37() V85() V86() V87() V91() ) set ) ) : ( ( ) ( V37() ) set ) ) -defined ExtREAL : ( ( ) ( non empty V86() ) set ) -valued Function-like V37() FinSequence-like FinSubsequence-like V62() ) FinSequence of ExtREAL : ( ( ) ( non empty V86() ) set ) ) : ( ( ) ( ext-real ) Element of ExtREAL : ( ( ) ( non empty V86() ) set ) ) ;

theorem :: MESFUNC4:3
for X being ( ( non empty ) ( non empty ) set )
for S being ( ( non empty compl-closed sigma-multiplicative ) ( non empty compl-closed sigma-multiplicative V79() V80() V81() sigma-additive ) SigmaField of X : ( ( non empty ) ( non empty ) set ) )
for f being ( ( Function-like ) ( Relation-like b1 : ( ( non empty ) ( non empty ) set ) -defined ExtREAL : ( ( ) ( non empty V86() ) set ) -valued Function-like V62() ) PartFunc of ,)
for M being ( ( Function-like V30(b2 : ( ( non empty compl-closed sigma-multiplicative ) ( non empty compl-closed sigma-multiplicative V79() V80() V81() sigma-additive ) SigmaField of b1 : ( ( non empty ) ( non empty ) set ) ) , ExtREAL : ( ( ) ( non empty V86() ) set ) ) V70() nonnegative sigma-additive ) ( Relation-like b2 : ( ( non empty compl-closed sigma-multiplicative ) ( non empty compl-closed sigma-multiplicative V79() V80() V81() sigma-additive ) SigmaField of b1 : ( ( non empty ) ( non empty ) set ) ) -defined ExtREAL : ( ( ) ( non empty V86() ) set ) -valued Function-like V30(b2 : ( ( non empty compl-closed sigma-multiplicative ) ( non empty compl-closed sigma-multiplicative V79() V80() V81() sigma-additive ) SigmaField of b1 : ( ( non empty ) ( non empty ) set ) ) , ExtREAL : ( ( ) ( non empty V86() ) set ) ) V62() V70() nonnegative sigma-additive ) sigma_Measure of S : ( ( non empty compl-closed sigma-multiplicative ) ( non empty compl-closed sigma-multiplicative V79() V80() V81() sigma-additive ) SigmaField of b1 : ( ( non empty ) ( non empty ) set ) ) )
for F being ( ( V83() ) ( Relation-like NAT : ( ( ) ( non empty V15() V16() V17() V37() V42() V43() V85() V86() V87() V88() V89() V90() V91() ) Element of K19(REAL : ( ( ) ( non empty V37() V85() V86() V87() V91() ) set ) ) : ( ( ) ( V37() ) set ) ) -defined b2 : ( ( non empty compl-closed sigma-multiplicative ) ( non empty compl-closed sigma-multiplicative V79() V80() V81() sigma-additive ) SigmaField of b1 : ( ( non empty ) ( non empty ) set ) ) -valued Function-like V37() FinSequence-like FinSubsequence-like V83() ) Finite_Sep_Sequence of S : ( ( non empty compl-closed sigma-multiplicative ) ( non empty compl-closed sigma-multiplicative V79() V80() V81() sigma-additive ) SigmaField of b1 : ( ( non empty ) ( non empty ) set ) ) )
for a, x being ( ( ) ( Relation-like NAT : ( ( ) ( non empty V15() V16() V17() V37() V42() V43() V85() V86() V87() V88() V89() V90() V91() ) Element of K19(REAL : ( ( ) ( non empty V37() V85() V86() V87() V91() ) set ) ) : ( ( ) ( V37() ) set ) ) -defined ExtREAL : ( ( ) ( non empty V86() ) set ) -valued Function-like V37() FinSequence-like FinSubsequence-like V62() ) FinSequence of ExtREAL : ( ( ) ( non empty V86() ) set ) ) st f : ( ( Function-like ) ( Relation-like b1 : ( ( non empty ) ( non empty ) set ) -defined ExtREAL : ( ( ) ( non empty V86() ) set ) -valued Function-like V62() ) PartFunc of ,) is_simple_func_in S : ( ( non empty compl-closed sigma-multiplicative ) ( non empty compl-closed sigma-multiplicative V79() V80() V81() sigma-additive ) SigmaField of b1 : ( ( non empty ) ( non empty ) set ) ) & dom f : ( ( Function-like ) ( Relation-like b1 : ( ( non empty ) ( non empty ) set ) -defined ExtREAL : ( ( ) ( non empty V86() ) set ) -valued Function-like V62() ) PartFunc of ,) : ( ( ) ( ) set ) <> {} : ( ( ) ( ) set ) & ( for x being ( ( ) ( ) set ) st x : ( ( V21() ) ( V15() V16() V17() V21() V22() V23() ext-real non negative V37() V42() ) Nat) in dom f : ( ( Function-like ) ( Relation-like b1 : ( ( non empty ) ( non empty ) set ) -defined ExtREAL : ( ( ) ( non empty V86() ) set ) -valued Function-like V62() ) PartFunc of ,) : ( ( ) ( ) set ) holds
0. : ( ( ) ( ext-real ) Element of ExtREAL : ( ( ) ( non empty V86() ) set ) ) <= f : ( ( Function-like ) ( Relation-like b1 : ( ( non empty ) ( non empty ) set ) -defined ExtREAL : ( ( ) ( non empty V86() ) set ) -valued Function-like V62() ) PartFunc of ,) . x : ( ( V21() ) ( V15() V16() V17() V21() V22() V23() ext-real non negative V37() V42() ) Nat) : ( ( ) ( ext-real ) Element of ExtREAL : ( ( ) ( non empty V86() ) set ) ) ) & F : ( ( V83() ) ( Relation-like NAT : ( ( ) ( non empty V15() V16() V17() V37() V42() V43() V85() V86() V87() V88() V89() V90() V91() ) Element of K19(REAL : ( ( ) ( non empty V37() V85() V86() V87() V91() ) set ) ) : ( ( ) ( V37() ) set ) ) -defined b2 : ( ( non empty compl-closed sigma-multiplicative ) ( non empty compl-closed sigma-multiplicative V79() V80() V81() sigma-additive ) SigmaField of b1 : ( ( non empty ) ( non empty ) set ) ) -valued Function-like V37() FinSequence-like FinSubsequence-like V83() ) Finite_Sep_Sequence of b2 : ( ( non empty compl-closed sigma-multiplicative ) ( non empty compl-closed sigma-multiplicative V79() V80() V81() sigma-additive ) SigmaField of b1 : ( ( non empty ) ( non empty ) set ) ) ) ,a : ( ( ) ( Relation-like NAT : ( ( ) ( non empty V15() V16() V17() V37() V42() V43() V85() V86() V87() V88() V89() V90() V91() ) Element of K19(REAL : ( ( ) ( non empty V37() V85() V86() V87() V91() ) set ) ) : ( ( ) ( V37() ) set ) ) -defined ExtREAL : ( ( ) ( non empty V86() ) set ) -valued Function-like V37() FinSequence-like FinSubsequence-like V62() ) FinSequence of ExtREAL : ( ( ) ( non empty V86() ) set ) ) are_Re-presentation_of f : ( ( Function-like ) ( Relation-like b1 : ( ( non empty ) ( non empty ) set ) -defined ExtREAL : ( ( ) ( non empty V86() ) set ) -valued Function-like V62() ) PartFunc of ,) & dom x : ( ( ) ( Relation-like NAT : ( ( ) ( non empty V15() V16() V17() V37() V42() V43() V85() V86() V87() V88() V89() V90() V91() ) Element of K19(REAL : ( ( ) ( non empty V37() V85() V86() V87() V91() ) set ) ) : ( ( ) ( V37() ) set ) ) -defined ExtREAL : ( ( ) ( non empty V86() ) set ) -valued Function-like V37() FinSequence-like FinSubsequence-like V62() ) FinSequence of ExtREAL : ( ( ) ( non empty V86() ) set ) ) : ( ( ) ( V85() V86() V87() V88() V89() V90() ) Element of K19(NAT : ( ( ) ( non empty V15() V16() V17() V37() V42() V43() V85() V86() V87() V88() V89() V90() V91() ) Element of K19(REAL : ( ( ) ( non empty V37() V85() V86() V87() V91() ) set ) ) : ( ( ) ( V37() ) set ) ) ) : ( ( ) ( V37() ) set ) ) = dom F : ( ( V83() ) ( Relation-like NAT : ( ( ) ( non empty V15() V16() V17() V37() V42() V43() V85() V86() V87() V88() V89() V90() V91() ) Element of K19(REAL : ( ( ) ( non empty V37() V85() V86() V87() V91() ) set ) ) : ( ( ) ( V37() ) set ) ) -defined b2 : ( ( non empty compl-closed sigma-multiplicative ) ( non empty compl-closed sigma-multiplicative V79() V80() V81() sigma-additive ) SigmaField of b1 : ( ( non empty ) ( non empty ) set ) ) -valued Function-like V37() FinSequence-like FinSubsequence-like V83() ) Finite_Sep_Sequence of b2 : ( ( non empty compl-closed sigma-multiplicative ) ( non empty compl-closed sigma-multiplicative V79() V80() V81() sigma-additive ) SigmaField of b1 : ( ( non empty ) ( non empty ) set ) ) ) : ( ( ) ( V85() V86() V87() V88() V89() V90() ) Element of K19(NAT : ( ( ) ( non empty V15() V16() V17() V37() V42() V43() V85() V86() V87() V88() V89() V90() V91() ) Element of K19(REAL : ( ( ) ( non empty V37() V85() V86() V87() V91() ) set ) ) : ( ( ) ( V37() ) set ) ) ) : ( ( ) ( V37() ) set ) ) & ( for n being ( ( V21() ) ( V15() V16() V17() V21() V22() V23() ext-real non negative V37() V42() ) Nat) st n : ( ( V21() ) ( V15() V16() V17() V21() V22() V23() ext-real non negative V37() V42() ) Nat) in dom x : ( ( ) ( Relation-like NAT : ( ( ) ( non empty V15() V16() V17() V37() V42() V43() V85() V86() V87() V88() V89() V90() V91() ) Element of K19(REAL : ( ( ) ( non empty V37() V85() V86() V87() V91() ) set ) ) : ( ( ) ( V37() ) set ) ) -defined ExtREAL : ( ( ) ( non empty V86() ) set ) -valued Function-like V37() FinSequence-like FinSubsequence-like V62() ) FinSequence of ExtREAL : ( ( ) ( non empty V86() ) set ) ) : ( ( ) ( V85() V86() V87() V88() V89() V90() ) Element of K19(NAT : ( ( ) ( non empty V15() V16() V17() V37() V42() V43() V85() V86() V87() V88() V89() V90() V91() ) Element of K19(REAL : ( ( ) ( non empty V37() V85() V86() V87() V91() ) set ) ) : ( ( ) ( V37() ) set ) ) ) : ( ( ) ( V37() ) set ) ) holds
x : ( ( ) ( Relation-like NAT : ( ( ) ( non empty V15() V16() V17() V37() V42() V43() V85() V86() V87() V88() V89() V90() V91() ) Element of K19(REAL : ( ( ) ( non empty V37() V85() V86() V87() V91() ) set ) ) : ( ( ) ( V37() ) set ) ) -defined ExtREAL : ( ( ) ( non empty V86() ) set ) -valued Function-like V37() FinSequence-like FinSubsequence-like V62() ) FinSequence of ExtREAL : ( ( ) ( non empty V86() ) set ) ) . n : ( ( V21() ) ( V15() V16() V17() V21() V22() V23() ext-real non negative V37() V42() ) Nat) : ( ( ) ( ext-real ) Element of ExtREAL : ( ( ) ( non empty V86() ) set ) ) = (a : ( ( ) ( Relation-like NAT : ( ( ) ( non empty V15() V16() V17() V37() V42() V43() V85() V86() V87() V88() V89() V90() V91() ) Element of K19(REAL : ( ( ) ( non empty V37() V85() V86() V87() V91() ) set ) ) : ( ( ) ( V37() ) set ) ) -defined ExtREAL : ( ( ) ( non empty V86() ) set ) -valued Function-like V37() FinSequence-like FinSubsequence-like V62() ) FinSequence of ExtREAL : ( ( ) ( non empty V86() ) set ) ) . n : ( ( V21() ) ( V15() V16() V17() V21() V22() V23() ext-real non negative V37() V42() ) Nat) ) : ( ( ) ( ext-real ) Element of ExtREAL : ( ( ) ( non empty V86() ) set ) ) * ((M : ( ( Function-like V30(b2 : ( ( non empty compl-closed sigma-multiplicative ) ( non empty compl-closed sigma-multiplicative V79() V80() V81() sigma-additive ) SigmaField of b1 : ( ( non empty ) ( non empty ) set ) ) , ExtREAL : ( ( ) ( non empty V86() ) set ) ) V70() nonnegative sigma-additive ) ( Relation-like b2 : ( ( non empty compl-closed sigma-multiplicative ) ( non empty compl-closed sigma-multiplicative V79() V80() V81() sigma-additive ) SigmaField of b1 : ( ( non empty ) ( non empty ) set ) ) -defined ExtREAL : ( ( ) ( non empty V86() ) set ) -valued Function-like V30(b2 : ( ( non empty compl-closed sigma-multiplicative ) ( non empty compl-closed sigma-multiplicative V79() V80() V81() sigma-additive ) SigmaField of b1 : ( ( non empty ) ( non empty ) set ) ) , ExtREAL : ( ( ) ( non empty V86() ) set ) ) V62() V70() nonnegative sigma-additive ) sigma_Measure of b2 : ( ( non empty compl-closed sigma-multiplicative ) ( non empty compl-closed sigma-multiplicative V79() V80() V81() sigma-additive ) SigmaField of b1 : ( ( non empty ) ( non empty ) set ) ) ) * F : ( ( V83() ) ( Relation-like NAT : ( ( ) ( non empty V15() V16() V17() V37() V42() V43() V85() V86() V87() V88() V89() V90() V91() ) Element of K19(REAL : ( ( ) ( non empty V37() V85() V86() V87() V91() ) set ) ) : ( ( ) ( V37() ) set ) ) -defined b2 : ( ( non empty compl-closed sigma-multiplicative ) ( non empty compl-closed sigma-multiplicative V79() V80() V81() sigma-additive ) SigmaField of b1 : ( ( non empty ) ( non empty ) set ) ) -valued Function-like V37() FinSequence-like FinSubsequence-like V83() ) Finite_Sep_Sequence of b2 : ( ( non empty compl-closed sigma-multiplicative ) ( non empty compl-closed sigma-multiplicative V79() V80() V81() sigma-additive ) SigmaField of b1 : ( ( non empty ) ( non empty ) set ) ) ) ) : ( ( Function-like ) ( Relation-like NAT : ( ( ) ( non empty V15() V16() V17() V37() V42() V43() V85() V86() V87() V88() V89() V90() V91() ) Element of K19(REAL : ( ( ) ( non empty V37() V85() V86() V87() V91() ) set ) ) : ( ( ) ( V37() ) set ) ) -defined ExtREAL : ( ( ) ( non empty V86() ) set ) -valued Function-like V62() ) Element of K19(K20(NAT : ( ( ) ( non empty V15() V16() V17() V37() V42() V43() V85() V86() V87() V88() V89() V90() V91() ) Element of K19(REAL : ( ( ) ( non empty V37() V85() V86() V87() V91() ) set ) ) : ( ( ) ( V37() ) set ) ) ,ExtREAL : ( ( ) ( non empty V86() ) set ) ) : ( ( ) ( V37() V62() ) set ) ) : ( ( ) ( V37() ) set ) ) . n : ( ( V21() ) ( V15() V16() V17() V21() V22() V23() ext-real non negative V37() V42() ) Nat) ) : ( ( ) ( ext-real ) Element of ExtREAL : ( ( ) ( non empty V86() ) set ) ) : ( ( ) ( ext-real ) Element of ExtREAL : ( ( ) ( non empty V86() ) set ) ) ) holds
integral (X : ( ( non empty ) ( non empty ) set ) ,S : ( ( non empty compl-closed sigma-multiplicative ) ( non empty compl-closed sigma-multiplicative V79() V80() V81() sigma-additive ) SigmaField of b1 : ( ( non empty ) ( non empty ) set ) ) ,M : ( ( Function-like V30(b2 : ( ( non empty compl-closed sigma-multiplicative ) ( non empty compl-closed sigma-multiplicative V79() V80() V81() sigma-additive ) SigmaField of b1 : ( ( non empty ) ( non empty ) set ) ) , ExtREAL : ( ( ) ( non empty V86() ) set ) ) V70() nonnegative sigma-additive ) ( Relation-like b2 : ( ( non empty compl-closed sigma-multiplicative ) ( non empty compl-closed sigma-multiplicative V79() V80() V81() sigma-additive ) SigmaField of b1 : ( ( non empty ) ( non empty ) set ) ) -defined ExtREAL : ( ( ) ( non empty V86() ) set ) -valued Function-like V30(b2 : ( ( non empty compl-closed sigma-multiplicative ) ( non empty compl-closed sigma-multiplicative V79() V80() V81() sigma-additive ) SigmaField of b1 : ( ( non empty ) ( non empty ) set ) ) , ExtREAL : ( ( ) ( non empty V86() ) set ) ) V62() V70() nonnegative sigma-additive ) sigma_Measure of b2 : ( ( non empty compl-closed sigma-multiplicative ) ( non empty compl-closed sigma-multiplicative V79() V80() V81() sigma-additive ) SigmaField of b1 : ( ( non empty ) ( non empty ) set ) ) ) ,f : ( ( Function-like ) ( Relation-like b1 : ( ( non empty ) ( non empty ) set ) -defined ExtREAL : ( ( ) ( non empty V86() ) set ) -valued Function-like V62() ) PartFunc of ,) ) : ( ( ) ( ext-real ) Element of ExtREAL : ( ( ) ( non empty V86() ) set ) ) = Sum x : ( ( ) ( Relation-like NAT : ( ( ) ( non empty V15() V16() V17() V37() V42() V43() V85() V86() V87() V88() V89() V90() V91() ) Element of K19(REAL : ( ( ) ( non empty V37() V85() V86() V87() V91() ) set ) ) : ( ( ) ( V37() ) set ) ) -defined ExtREAL : ( ( ) ( non empty V86() ) set ) -valued Function-like V37() FinSequence-like FinSubsequence-like V62() ) FinSequence of ExtREAL : ( ( ) ( non empty V86() ) set ) ) : ( ( ) ( ext-real ) Element of ExtREAL : ( ( ) ( non empty V86() ) set ) ) ;

theorem :: MESFUNC4:4
for X being ( ( non empty ) ( non empty ) set )
for S being ( ( non empty compl-closed sigma-multiplicative ) ( non empty compl-closed sigma-multiplicative V79() V80() V81() sigma-additive ) SigmaField of X : ( ( non empty ) ( non empty ) set ) )
for f being ( ( Function-like ) ( Relation-like b1 : ( ( non empty ) ( non empty ) set ) -defined ExtREAL : ( ( ) ( non empty V86() ) set ) -valued Function-like V62() ) PartFunc of ,)
for M being ( ( Function-like V30(b2 : ( ( non empty compl-closed sigma-multiplicative ) ( non empty compl-closed sigma-multiplicative V79() V80() V81() sigma-additive ) SigmaField of b1 : ( ( non empty ) ( non empty ) set ) ) , ExtREAL : ( ( ) ( non empty V86() ) set ) ) V70() nonnegative sigma-additive ) ( Relation-like b2 : ( ( non empty compl-closed sigma-multiplicative ) ( non empty compl-closed sigma-multiplicative V79() V80() V81() sigma-additive ) SigmaField of b1 : ( ( non empty ) ( non empty ) set ) ) -defined ExtREAL : ( ( ) ( non empty V86() ) set ) -valued Function-like V30(b2 : ( ( non empty compl-closed sigma-multiplicative ) ( non empty compl-closed sigma-multiplicative V79() V80() V81() sigma-additive ) SigmaField of b1 : ( ( non empty ) ( non empty ) set ) ) , ExtREAL : ( ( ) ( non empty V86() ) set ) ) V62() V70() nonnegative sigma-additive ) sigma_Measure of S : ( ( non empty compl-closed sigma-multiplicative ) ( non empty compl-closed sigma-multiplicative V79() V80() V81() sigma-additive ) SigmaField of b1 : ( ( non empty ) ( non empty ) set ) ) ) st f : ( ( Function-like ) ( Relation-like b1 : ( ( non empty ) ( non empty ) set ) -defined ExtREAL : ( ( ) ( non empty V86() ) set ) -valued Function-like V62() ) PartFunc of ,) is_simple_func_in S : ( ( non empty compl-closed sigma-multiplicative ) ( non empty compl-closed sigma-multiplicative V79() V80() V81() sigma-additive ) SigmaField of b1 : ( ( non empty ) ( non empty ) set ) ) & dom f : ( ( Function-like ) ( Relation-like b1 : ( ( non empty ) ( non empty ) set ) -defined ExtREAL : ( ( ) ( non empty V86() ) set ) -valued Function-like V62() ) PartFunc of ,) : ( ( ) ( ) set ) <> {} : ( ( ) ( ) set ) & ( for x being ( ( ) ( ) set ) st x : ( ( V83() ) ( Relation-like NAT : ( ( ) ( non empty V15() V16() V17() V37() V42() V43() V85() V86() V87() V88() V89() V90() V91() ) Element of K19(REAL : ( ( ) ( non empty V37() V85() V86() V87() V91() ) set ) ) : ( ( ) ( V37() ) set ) ) -defined b2 : ( ( non empty compl-closed sigma-multiplicative ) ( non empty compl-closed sigma-multiplicative V79() V80() V81() sigma-additive ) SigmaField of b1 : ( ( non empty ) ( non empty ) set ) ) -valued Function-like V37() FinSequence-like FinSubsequence-like V83() ) Finite_Sep_Sequence of b2 : ( ( non empty compl-closed sigma-multiplicative ) ( non empty compl-closed sigma-multiplicative V79() V80() V81() sigma-additive ) SigmaField of b1 : ( ( non empty ) ( non empty ) set ) ) ) in dom f : ( ( Function-like ) ( Relation-like b1 : ( ( non empty ) ( non empty ) set ) -defined ExtREAL : ( ( ) ( non empty V86() ) set ) -valued Function-like V62() ) PartFunc of ,) : ( ( ) ( ) set ) holds
0. : ( ( ) ( ext-real ) Element of ExtREAL : ( ( ) ( non empty V86() ) set ) ) <= f : ( ( Function-like ) ( Relation-like b1 : ( ( non empty ) ( non empty ) set ) -defined ExtREAL : ( ( ) ( non empty V86() ) set ) -valued Function-like V62() ) PartFunc of ,) . x : ( ( V83() ) ( Relation-like NAT : ( ( ) ( non empty V15() V16() V17() V37() V42() V43() V85() V86() V87() V88() V89() V90() V91() ) Element of K19(REAL : ( ( ) ( non empty V37() V85() V86() V87() V91() ) set ) ) : ( ( ) ( V37() ) set ) ) -defined b2 : ( ( non empty compl-closed sigma-multiplicative ) ( non empty compl-closed sigma-multiplicative V79() V80() V81() sigma-additive ) SigmaField of b1 : ( ( non empty ) ( non empty ) set ) ) -valued Function-like V37() FinSequence-like FinSubsequence-like V83() ) Finite_Sep_Sequence of b2 : ( ( non empty compl-closed sigma-multiplicative ) ( non empty compl-closed sigma-multiplicative V79() V80() V81() sigma-additive ) SigmaField of b1 : ( ( non empty ) ( non empty ) set ) ) ) : ( ( ) ( ext-real ) Element of ExtREAL : ( ( ) ( non empty V86() ) set ) ) ) holds
ex F being ( ( V83() ) ( Relation-like NAT : ( ( ) ( non empty V15() V16() V17() V37() V42() V43() V85() V86() V87() V88() V89() V90() V91() ) Element of K19(REAL : ( ( ) ( non empty V37() V85() V86() V87() V91() ) set ) ) : ( ( ) ( V37() ) set ) ) -defined b2 : ( ( non empty compl-closed sigma-multiplicative ) ( non empty compl-closed sigma-multiplicative V79() V80() V81() sigma-additive ) SigmaField of b1 : ( ( non empty ) ( non empty ) set ) ) -valued Function-like V37() FinSequence-like FinSubsequence-like V83() ) Finite_Sep_Sequence of S : ( ( non empty compl-closed sigma-multiplicative ) ( non empty compl-closed sigma-multiplicative V79() V80() V81() sigma-additive ) SigmaField of b1 : ( ( non empty ) ( non empty ) set ) ) ) ex a, x being ( ( ) ( Relation-like NAT : ( ( ) ( non empty V15() V16() V17() V37() V42() V43() V85() V86() V87() V88() V89() V90() V91() ) Element of K19(REAL : ( ( ) ( non empty V37() V85() V86() V87() V91() ) set ) ) : ( ( ) ( V37() ) set ) ) -defined ExtREAL : ( ( ) ( non empty V86() ) set ) -valued Function-like V37() FinSequence-like FinSubsequence-like V62() ) FinSequence of ExtREAL : ( ( ) ( non empty V86() ) set ) ) st
( F : ( ( V83() ) ( Relation-like NAT : ( ( ) ( non empty V15() V16() V17() V37() V42() V43() V85() V86() V87() V88() V89() V90() V91() ) Element of K19(REAL : ( ( ) ( non empty V37() V85() V86() V87() V91() ) set ) ) : ( ( ) ( V37() ) set ) ) -defined b2 : ( ( non empty compl-closed sigma-multiplicative ) ( non empty compl-closed sigma-multiplicative V79() V80() V81() sigma-additive ) SigmaField of b1 : ( ( non empty ) ( non empty ) set ) ) -valued Function-like V37() FinSequence-like FinSubsequence-like V83() ) Finite_Sep_Sequence of b2 : ( ( non empty compl-closed sigma-multiplicative ) ( non empty compl-closed sigma-multiplicative V79() V80() V81() sigma-additive ) SigmaField of b1 : ( ( non empty ) ( non empty ) set ) ) ) ,a : ( ( ) ( Relation-like NAT : ( ( ) ( non empty V15() V16() V17() V37() V42() V43() V85() V86() V87() V88() V89() V90() V91() ) Element of K19(REAL : ( ( ) ( non empty V37() V85() V86() V87() V91() ) set ) ) : ( ( ) ( V37() ) set ) ) -defined ExtREAL : ( ( ) ( non empty V86() ) set ) -valued Function-like V37() FinSequence-like FinSubsequence-like V62() ) FinSequence of ExtREAL : ( ( ) ( non empty V86() ) set ) ) are_Re-presentation_of f : ( ( Function-like ) ( Relation-like b1 : ( ( non empty ) ( non empty ) set ) -defined ExtREAL : ( ( ) ( non empty V86() ) set ) -valued Function-like V62() ) PartFunc of ,) & dom x : ( ( ) ( Relation-like NAT : ( ( ) ( non empty V15() V16() V17() V37() V42() V43() V85() V86() V87() V88() V89() V90() V91() ) Element of K19(REAL : ( ( ) ( non empty V37() V85() V86() V87() V91() ) set ) ) : ( ( ) ( V37() ) set ) ) -defined ExtREAL : ( ( ) ( non empty V86() ) set ) -valued Function-like V37() FinSequence-like FinSubsequence-like V62() ) FinSequence of ExtREAL : ( ( ) ( non empty V86() ) set ) ) : ( ( ) ( V85() V86() V87() V88() V89() V90() ) Element of K19(NAT : ( ( ) ( non empty V15() V16() V17() V37() V42() V43() V85() V86() V87() V88() V89() V90() V91() ) Element of K19(REAL : ( ( ) ( non empty V37() V85() V86() V87() V91() ) set ) ) : ( ( ) ( V37() ) set ) ) ) : ( ( ) ( V37() ) set ) ) = dom F : ( ( V83() ) ( Relation-like NAT : ( ( ) ( non empty V15() V16() V17() V37() V42() V43() V85() V86() V87() V88() V89() V90() V91() ) Element of K19(REAL : ( ( ) ( non empty V37() V85() V86() V87() V91() ) set ) ) : ( ( ) ( V37() ) set ) ) -defined b2 : ( ( non empty compl-closed sigma-multiplicative ) ( non empty compl-closed sigma-multiplicative V79() V80() V81() sigma-additive ) SigmaField of b1 : ( ( non empty ) ( non empty ) set ) ) -valued Function-like V37() FinSequence-like FinSubsequence-like V83() ) Finite_Sep_Sequence of b2 : ( ( non empty compl-closed sigma-multiplicative ) ( non empty compl-closed sigma-multiplicative V79() V80() V81() sigma-additive ) SigmaField of b1 : ( ( non empty ) ( non empty ) set ) ) ) : ( ( ) ( V85() V86() V87() V88() V89() V90() ) Element of K19(NAT : ( ( ) ( non empty V15() V16() V17() V37() V42() V43() V85() V86() V87() V88() V89() V90() V91() ) Element of K19(REAL : ( ( ) ( non empty V37() V85() V86() V87() V91() ) set ) ) : ( ( ) ( V37() ) set ) ) ) : ( ( ) ( V37() ) set ) ) & ( for n being ( ( V21() ) ( V15() V16() V17() V21() V22() V23() ext-real non negative V37() V42() ) Nat) st n : ( ( V21() ) ( V15() V16() V17() V21() V22() V23() ext-real non negative V37() V42() ) Nat) in dom x : ( ( ) ( Relation-like NAT : ( ( ) ( non empty V15() V16() V17() V37() V42() V43() V85() V86() V87() V88() V89() V90() V91() ) Element of K19(REAL : ( ( ) ( non empty V37() V85() V86() V87() V91() ) set ) ) : ( ( ) ( V37() ) set ) ) -defined ExtREAL : ( ( ) ( non empty V86() ) set ) -valued Function-like V37() FinSequence-like FinSubsequence-like V62() ) FinSequence of ExtREAL : ( ( ) ( non empty V86() ) set ) ) : ( ( ) ( V85() V86() V87() V88() V89() V90() ) Element of K19(NAT : ( ( ) ( non empty V15() V16() V17() V37() V42() V43() V85() V86() V87() V88() V89() V90() V91() ) Element of K19(REAL : ( ( ) ( non empty V37() V85() V86() V87() V91() ) set ) ) : ( ( ) ( V37() ) set ) ) ) : ( ( ) ( V37() ) set ) ) holds
x : ( ( ) ( Relation-like NAT : ( ( ) ( non empty V15() V16() V17() V37() V42() V43() V85() V86() V87() V88() V89() V90() V91() ) Element of K19(REAL : ( ( ) ( non empty V37() V85() V86() V87() V91() ) set ) ) : ( ( ) ( V37() ) set ) ) -defined ExtREAL : ( ( ) ( non empty V86() ) set ) -valued Function-like V37() FinSequence-like FinSubsequence-like V62() ) FinSequence of ExtREAL : ( ( ) ( non empty V86() ) set ) ) . n : ( ( V21() ) ( V15() V16() V17() V21() V22() V23() ext-real non negative V37() V42() ) Nat) : ( ( ) ( ext-real ) Element of ExtREAL : ( ( ) ( non empty V86() ) set ) ) = (a : ( ( ) ( Relation-like NAT : ( ( ) ( non empty V15() V16() V17() V37() V42() V43() V85() V86() V87() V88() V89() V90() V91() ) Element of K19(REAL : ( ( ) ( non empty V37() V85() V86() V87() V91() ) set ) ) : ( ( ) ( V37() ) set ) ) -defined ExtREAL : ( ( ) ( non empty V86() ) set ) -valued Function-like V37() FinSequence-like FinSubsequence-like V62() ) FinSequence of ExtREAL : ( ( ) ( non empty V86() ) set ) ) . n : ( ( V21() ) ( V15() V16() V17() V21() V22() V23() ext-real non negative V37() V42() ) Nat) ) : ( ( ) ( ext-real ) Element of ExtREAL : ( ( ) ( non empty V86() ) set ) ) * ((M : ( ( Function-like V30(b2 : ( ( non empty compl-closed sigma-multiplicative ) ( non empty compl-closed sigma-multiplicative V79() V80() V81() sigma-additive ) SigmaField of b1 : ( ( non empty ) ( non empty ) set ) ) , ExtREAL : ( ( ) ( non empty V86() ) set ) ) V70() nonnegative sigma-additive ) ( Relation-like b2 : ( ( non empty compl-closed sigma-multiplicative ) ( non empty compl-closed sigma-multiplicative V79() V80() V81() sigma-additive ) SigmaField of b1 : ( ( non empty ) ( non empty ) set ) ) -defined ExtREAL : ( ( ) ( non empty V86() ) set ) -valued Function-like V30(b2 : ( ( non empty compl-closed sigma-multiplicative ) ( non empty compl-closed sigma-multiplicative V79() V80() V81() sigma-additive ) SigmaField of b1 : ( ( non empty ) ( non empty ) set ) ) , ExtREAL : ( ( ) ( non empty V86() ) set ) ) V62() V70() nonnegative sigma-additive ) sigma_Measure of b2 : ( ( non empty compl-closed sigma-multiplicative ) ( non empty compl-closed sigma-multiplicative V79() V80() V81() sigma-additive ) SigmaField of b1 : ( ( non empty ) ( non empty ) set ) ) ) * F : ( ( V83() ) ( Relation-like NAT : ( ( ) ( non empty V15() V16() V17() V37() V42() V43() V85() V86() V87() V88() V89() V90() V91() ) Element of K19(REAL : ( ( ) ( non empty V37() V85() V86() V87() V91() ) set ) ) : ( ( ) ( V37() ) set ) ) -defined b2 : ( ( non empty compl-closed sigma-multiplicative ) ( non empty compl-closed sigma-multiplicative V79() V80() V81() sigma-additive ) SigmaField of b1 : ( ( non empty ) ( non empty ) set ) ) -valued Function-like V37() FinSequence-like FinSubsequence-like V83() ) Finite_Sep_Sequence of b2 : ( ( non empty compl-closed sigma-multiplicative ) ( non empty compl-closed sigma-multiplicative V79() V80() V81() sigma-additive ) SigmaField of b1 : ( ( non empty ) ( non empty ) set ) ) ) ) : ( ( Function-like ) ( Relation-like NAT : ( ( ) ( non empty V15() V16() V17() V37() V42() V43() V85() V86() V87() V88() V89() V90() V91() ) Element of K19(REAL : ( ( ) ( non empty V37() V85() V86() V87() V91() ) set ) ) : ( ( ) ( V37() ) set ) ) -defined ExtREAL : ( ( ) ( non empty V86() ) set ) -valued Function-like V62() ) Element of K19(K20(NAT : ( ( ) ( non empty V15() V16() V17() V37() V42() V43() V85() V86() V87() V88() V89() V90() V91() ) Element of K19(REAL : ( ( ) ( non empty V37() V85() V86() V87() V91() ) set ) ) : ( ( ) ( V37() ) set ) ) ,ExtREAL : ( ( ) ( non empty V86() ) set ) ) : ( ( ) ( V37() V62() ) set ) ) : ( ( ) ( V37() ) set ) ) . n : ( ( V21() ) ( V15() V16() V17() V21() V22() V23() ext-real non negative V37() V42() ) Nat) ) : ( ( ) ( ext-real ) Element of ExtREAL : ( ( ) ( non empty V86() ) set ) ) : ( ( ) ( ext-real ) Element of ExtREAL : ( ( ) ( non empty V86() ) set ) ) ) & integral (X : ( ( non empty ) ( non empty ) set ) ,S : ( ( non empty compl-closed sigma-multiplicative ) ( non empty compl-closed sigma-multiplicative V79() V80() V81() sigma-additive ) SigmaField of b1 : ( ( non empty ) ( non empty ) set ) ) ,M : ( ( Function-like V30(b2 : ( ( non empty compl-closed sigma-multiplicative ) ( non empty compl-closed sigma-multiplicative V79() V80() V81() sigma-additive ) SigmaField of b1 : ( ( non empty ) ( non empty ) set ) ) , ExtREAL : ( ( ) ( non empty V86() ) set ) ) V70() nonnegative sigma-additive ) ( Relation-like b2 : ( ( non empty compl-closed sigma-multiplicative ) ( non empty compl-closed sigma-multiplicative V79() V80() V81() sigma-additive ) SigmaField of b1 : ( ( non empty ) ( non empty ) set ) ) -defined ExtREAL : ( ( ) ( non empty V86() ) set ) -valued Function-like V30(b2 : ( ( non empty compl-closed sigma-multiplicative ) ( non empty compl-closed sigma-multiplicative V79() V80() V81() sigma-additive ) SigmaField of b1 : ( ( non empty ) ( non empty ) set ) ) , ExtREAL : ( ( ) ( non empty V86() ) set ) ) V62() V70() nonnegative sigma-additive ) sigma_Measure of b2 : ( ( non empty compl-closed sigma-multiplicative ) ( non empty compl-closed sigma-multiplicative V79() V80() V81() sigma-additive ) SigmaField of b1 : ( ( non empty ) ( non empty ) set ) ) ) ,f : ( ( Function-like ) ( Relation-like b1 : ( ( non empty ) ( non empty ) set ) -defined ExtREAL : ( ( ) ( non empty V86() ) set ) -valued Function-like V62() ) PartFunc of ,) ) : ( ( ) ( ext-real ) Element of ExtREAL : ( ( ) ( non empty V86() ) set ) ) = Sum x : ( ( ) ( Relation-like NAT : ( ( ) ( non empty V15() V16() V17() V37() V42() V43() V85() V86() V87() V88() V89() V90() V91() ) Element of K19(REAL : ( ( ) ( non empty V37() V85() V86() V87() V91() ) set ) ) : ( ( ) ( V37() ) set ) ) -defined ExtREAL : ( ( ) ( non empty V86() ) set ) -valued Function-like V37() FinSequence-like FinSubsequence-like V62() ) FinSequence of ExtREAL : ( ( ) ( non empty V86() ) set ) ) : ( ( ) ( ext-real ) Element of ExtREAL : ( ( ) ( non empty V86() ) set ) ) ) ;

theorem :: MESFUNC4:5
for X being ( ( non empty ) ( non empty ) set )
for S being ( ( non empty compl-closed sigma-multiplicative ) ( non empty compl-closed sigma-multiplicative V79() V80() V81() sigma-additive ) SigmaField of X : ( ( non empty ) ( non empty ) set ) )
for M being ( ( Function-like V30(b2 : ( ( non empty compl-closed sigma-multiplicative ) ( non empty compl-closed sigma-multiplicative V79() V80() V81() sigma-additive ) SigmaField of b1 : ( ( non empty ) ( non empty ) set ) ) , ExtREAL : ( ( ) ( non empty V86() ) set ) ) V70() nonnegative sigma-additive ) ( Relation-like b2 : ( ( non empty compl-closed sigma-multiplicative ) ( non empty compl-closed sigma-multiplicative V79() V80() V81() sigma-additive ) SigmaField of b1 : ( ( non empty ) ( non empty ) set ) ) -defined ExtREAL : ( ( ) ( non empty V86() ) set ) -valued Function-like V30(b2 : ( ( non empty compl-closed sigma-multiplicative ) ( non empty compl-closed sigma-multiplicative V79() V80() V81() sigma-additive ) SigmaField of b1 : ( ( non empty ) ( non empty ) set ) ) , ExtREAL : ( ( ) ( non empty V86() ) set ) ) V62() V70() nonnegative sigma-additive ) sigma_Measure of S : ( ( non empty compl-closed sigma-multiplicative ) ( non empty compl-closed sigma-multiplicative V79() V80() V81() sigma-additive ) SigmaField of b1 : ( ( non empty ) ( non empty ) set ) ) )
for f, g being ( ( Function-like ) ( Relation-like b1 : ( ( non empty ) ( non empty ) set ) -defined ExtREAL : ( ( ) ( non empty V86() ) set ) -valued Function-like V62() ) PartFunc of ,) st f : ( ( Function-like ) ( Relation-like b1 : ( ( non empty ) ( non empty ) set ) -defined ExtREAL : ( ( ) ( non empty V86() ) set ) -valued Function-like V62() ) PartFunc of ,) is_simple_func_in S : ( ( non empty compl-closed sigma-multiplicative ) ( non empty compl-closed sigma-multiplicative V79() V80() V81() sigma-additive ) SigmaField of b1 : ( ( non empty ) ( non empty ) set ) ) & dom f : ( ( Function-like ) ( Relation-like b1 : ( ( non empty ) ( non empty ) set ) -defined ExtREAL : ( ( ) ( non empty V86() ) set ) -valued Function-like V62() ) PartFunc of ,) : ( ( ) ( ) set ) <> {} : ( ( ) ( ) set ) & ( for x being ( ( ) ( ) set ) st x : ( ( ) ( ) set ) in dom f : ( ( Function-like ) ( Relation-like b1 : ( ( non empty ) ( non empty ) set ) -defined ExtREAL : ( ( ) ( non empty V86() ) set ) -valued Function-like V62() ) PartFunc of ,) : ( ( ) ( ) set ) holds
0. : ( ( ) ( ext-real ) Element of ExtREAL : ( ( ) ( non empty V86() ) set ) ) <= f : ( ( Function-like ) ( Relation-like b1 : ( ( non empty ) ( non empty ) set ) -defined ExtREAL : ( ( ) ( non empty V86() ) set ) -valued Function-like V62() ) PartFunc of ,) . x : ( ( ) ( ) set ) : ( ( ) ( ext-real ) Element of ExtREAL : ( ( ) ( non empty V86() ) set ) ) ) & g : ( ( Function-like ) ( Relation-like b1 : ( ( non empty ) ( non empty ) set ) -defined ExtREAL : ( ( ) ( non empty V86() ) set ) -valued Function-like V62() ) PartFunc of ,) is_simple_func_in S : ( ( non empty compl-closed sigma-multiplicative ) ( non empty compl-closed sigma-multiplicative V79() V80() V81() sigma-additive ) SigmaField of b1 : ( ( non empty ) ( non empty ) set ) ) & dom g : ( ( Function-like ) ( Relation-like b1 : ( ( non empty ) ( non empty ) set ) -defined ExtREAL : ( ( ) ( non empty V86() ) set ) -valued Function-like V62() ) PartFunc of ,) : ( ( ) ( ) set ) = dom f : ( ( Function-like ) ( Relation-like b1 : ( ( non empty ) ( non empty ) set ) -defined ExtREAL : ( ( ) ( non empty V86() ) set ) -valued Function-like V62() ) PartFunc of ,) : ( ( ) ( ) set ) & ( for x being ( ( ) ( ) set ) st x : ( ( ) ( ) set ) in dom g : ( ( Function-like ) ( Relation-like b1 : ( ( non empty ) ( non empty ) set ) -defined ExtREAL : ( ( ) ( non empty V86() ) set ) -valued Function-like V62() ) PartFunc of ,) : ( ( ) ( ) set ) holds
0. : ( ( ) ( ext-real ) Element of ExtREAL : ( ( ) ( non empty V86() ) set ) ) <= g : ( ( Function-like ) ( Relation-like b1 : ( ( non empty ) ( non empty ) set ) -defined ExtREAL : ( ( ) ( non empty V86() ) set ) -valued Function-like V62() ) PartFunc of ,) . x : ( ( ) ( ) set ) : ( ( ) ( ext-real ) Element of ExtREAL : ( ( ) ( non empty V86() ) set ) ) ) holds
( f : ( ( Function-like ) ( Relation-like b1 : ( ( non empty ) ( non empty ) set ) -defined ExtREAL : ( ( ) ( non empty V86() ) set ) -valued Function-like V62() ) PartFunc of ,) + g : ( ( Function-like ) ( Relation-like b1 : ( ( non empty ) ( non empty ) set ) -defined ExtREAL : ( ( ) ( non empty V86() ) set ) -valued Function-like V62() ) PartFunc of ,) : ( ( Function-like ) ( Relation-like b1 : ( ( non empty ) ( non empty ) set ) -defined ExtREAL : ( ( ) ( non empty V86() ) set ) -valued Function-like V62() ) Element of K19(K20(b1 : ( ( non empty ) ( non empty ) set ) ,ExtREAL : ( ( ) ( non empty V86() ) set ) ) : ( ( ) ( V62() ) set ) ) : ( ( ) ( ) set ) ) is_simple_func_in S : ( ( non empty compl-closed sigma-multiplicative ) ( non empty compl-closed sigma-multiplicative V79() V80() V81() sigma-additive ) SigmaField of b1 : ( ( non empty ) ( non empty ) set ) ) & dom (f : ( ( Function-like ) ( Relation-like b1 : ( ( non empty ) ( non empty ) set ) -defined ExtREAL : ( ( ) ( non empty V86() ) set ) -valued Function-like V62() ) PartFunc of ,) + g : ( ( Function-like ) ( Relation-like b1 : ( ( non empty ) ( non empty ) set ) -defined ExtREAL : ( ( ) ( non empty V86() ) set ) -valued Function-like V62() ) PartFunc of ,) ) : ( ( Function-like ) ( Relation-like b1 : ( ( non empty ) ( non empty ) set ) -defined ExtREAL : ( ( ) ( non empty V86() ) set ) -valued Function-like V62() ) Element of K19(K20(b1 : ( ( non empty ) ( non empty ) set ) ,ExtREAL : ( ( ) ( non empty V86() ) set ) ) : ( ( ) ( V62() ) set ) ) : ( ( ) ( ) set ) ) : ( ( ) ( ) set ) <> {} : ( ( ) ( ) set ) & ( for x being ( ( ) ( ) set ) st x : ( ( ) ( ) set ) in dom (f : ( ( Function-like ) ( Relation-like b1 : ( ( non empty ) ( non empty ) set ) -defined ExtREAL : ( ( ) ( non empty V86() ) set ) -valued Function-like V62() ) PartFunc of ,) + g : ( ( Function-like ) ( Relation-like b1 : ( ( non empty ) ( non empty ) set ) -defined ExtREAL : ( ( ) ( non empty V86() ) set ) -valued Function-like V62() ) PartFunc of ,) ) : ( ( Function-like ) ( Relation-like b1 : ( ( non empty ) ( non empty ) set ) -defined ExtREAL : ( ( ) ( non empty V86() ) set ) -valued Function-like V62() ) Element of K19(K20(b1 : ( ( non empty ) ( non empty ) set ) ,ExtREAL : ( ( ) ( non empty V86() ) set ) ) : ( ( ) ( V62() ) set ) ) : ( ( ) ( ) set ) ) : ( ( ) ( ) set ) holds
0. : ( ( ) ( ext-real ) Element of ExtREAL : ( ( ) ( non empty V86() ) set ) ) <= (f : ( ( Function-like ) ( Relation-like b1 : ( ( non empty ) ( non empty ) set ) -defined ExtREAL : ( ( ) ( non empty V86() ) set ) -valued Function-like V62() ) PartFunc of ,) + g : ( ( Function-like ) ( Relation-like b1 : ( ( non empty ) ( non empty ) set ) -defined ExtREAL : ( ( ) ( non empty V86() ) set ) -valued Function-like V62() ) PartFunc of ,) ) : ( ( Function-like ) ( Relation-like b1 : ( ( non empty ) ( non empty ) set ) -defined ExtREAL : ( ( ) ( non empty V86() ) set ) -valued Function-like V62() ) Element of K19(K20(b1 : ( ( non empty ) ( non empty ) set ) ,ExtREAL : ( ( ) ( non empty V86() ) set ) ) : ( ( ) ( V62() ) set ) ) : ( ( ) ( ) set ) ) . x : ( ( ) ( ) set ) : ( ( ) ( ext-real ) Element of ExtREAL : ( ( ) ( non empty V86() ) set ) ) ) & integral (X : ( ( non empty ) ( non empty ) set ) ,S : ( ( non empty compl-closed sigma-multiplicative ) ( non empty compl-closed sigma-multiplicative V79() V80() V81() sigma-additive ) SigmaField of b1 : ( ( non empty ) ( non empty ) set ) ) ,M : ( ( Function-like V30(b2 : ( ( non empty compl-closed sigma-multiplicative ) ( non empty compl-closed sigma-multiplicative V79() V80() V81() sigma-additive ) SigmaField of b1 : ( ( non empty ) ( non empty ) set ) ) , ExtREAL : ( ( ) ( non empty V86() ) set ) ) V70() nonnegative sigma-additive ) ( Relation-like b2 : ( ( non empty compl-closed sigma-multiplicative ) ( non empty compl-closed sigma-multiplicative V79() V80() V81() sigma-additive ) SigmaField of b1 : ( ( non empty ) ( non empty ) set ) ) -defined ExtREAL : ( ( ) ( non empty V86() ) set ) -valued Function-like V30(b2 : ( ( non empty compl-closed sigma-multiplicative ) ( non empty compl-closed sigma-multiplicative V79() V80() V81() sigma-additive ) SigmaField of b1 : ( ( non empty ) ( non empty ) set ) ) , ExtREAL : ( ( ) ( non empty V86() ) set ) ) V62() V70() nonnegative sigma-additive ) sigma_Measure of b2 : ( ( non empty compl-closed sigma-multiplicative ) ( non empty compl-closed sigma-multiplicative V79() V80() V81() sigma-additive ) SigmaField of b1 : ( ( non empty ) ( non empty ) set ) ) ) ,(f : ( ( Function-like ) ( Relation-like b1 : ( ( non empty ) ( non empty ) set ) -defined ExtREAL : ( ( ) ( non empty V86() ) set ) -valued Function-like V62() ) PartFunc of ,) + g : ( ( Function-like ) ( Relation-like b1 : ( ( non empty ) ( non empty ) set ) -defined ExtREAL : ( ( ) ( non empty V86() ) set ) -valued Function-like V62() ) PartFunc of ,) ) : ( ( Function-like ) ( Relation-like b1 : ( ( non empty ) ( non empty ) set ) -defined ExtREAL : ( ( ) ( non empty V86() ) set ) -valued Function-like V62() ) Element of K19(K20(b1 : ( ( non empty ) ( non empty ) set ) ,ExtREAL : ( ( ) ( non empty V86() ) set ) ) : ( ( ) ( V62() ) set ) ) : ( ( ) ( ) set ) ) ) : ( ( ) ( ext-real ) Element of ExtREAL : ( ( ) ( non empty V86() ) set ) ) = (integral (X : ( ( non empty ) ( non empty ) set ) ,S : ( ( non empty compl-closed sigma-multiplicative ) ( non empty compl-closed sigma-multiplicative V79() V80() V81() sigma-additive ) SigmaField of b1 : ( ( non empty ) ( non empty ) set ) ) ,M : ( ( Function-like V30(b2 : ( ( non empty compl-closed sigma-multiplicative ) ( non empty compl-closed sigma-multiplicative V79() V80() V81() sigma-additive ) SigmaField of b1 : ( ( non empty ) ( non empty ) set ) ) , ExtREAL : ( ( ) ( non empty V86() ) set ) ) V70() nonnegative sigma-additive ) ( Relation-like b2 : ( ( non empty compl-closed sigma-multiplicative ) ( non empty compl-closed sigma-multiplicative V79() V80() V81() sigma-additive ) SigmaField of b1 : ( ( non empty ) ( non empty ) set ) ) -defined ExtREAL : ( ( ) ( non empty V86() ) set ) -valued Function-like V30(b2 : ( ( non empty compl-closed sigma-multiplicative ) ( non empty compl-closed sigma-multiplicative V79() V80() V81() sigma-additive ) SigmaField of b1 : ( ( non empty ) ( non empty ) set ) ) , ExtREAL : ( ( ) ( non empty V86() ) set ) ) V62() V70() nonnegative sigma-additive ) sigma_Measure of b2 : ( ( non empty compl-closed sigma-multiplicative ) ( non empty compl-closed sigma-multiplicative V79() V80() V81() sigma-additive ) SigmaField of b1 : ( ( non empty ) ( non empty ) set ) ) ) ,f : ( ( Function-like ) ( Relation-like b1 : ( ( non empty ) ( non empty ) set ) -defined ExtREAL : ( ( ) ( non empty V86() ) set ) -valued Function-like V62() ) PartFunc of ,) )) : ( ( ) ( ext-real ) Element of ExtREAL : ( ( ) ( non empty V86() ) set ) ) + (integral (X : ( ( non empty ) ( non empty ) set ) ,S : ( ( non empty compl-closed sigma-multiplicative ) ( non empty compl-closed sigma-multiplicative V79() V80() V81() sigma-additive ) SigmaField of b1 : ( ( non empty ) ( non empty ) set ) ) ,M : ( ( Function-like V30(b2 : ( ( non empty compl-closed sigma-multiplicative ) ( non empty compl-closed sigma-multiplicative V79() V80() V81() sigma-additive ) SigmaField of b1 : ( ( non empty ) ( non empty ) set ) ) , ExtREAL : ( ( ) ( non empty V86() ) set ) ) V70() nonnegative sigma-additive ) ( Relation-like b2 : ( ( non empty compl-closed sigma-multiplicative ) ( non empty compl-closed sigma-multiplicative V79() V80() V81() sigma-additive ) SigmaField of b1 : ( ( non empty ) ( non empty ) set ) ) -defined ExtREAL : ( ( ) ( non empty V86() ) set ) -valued Function-like V30(b2 : ( ( non empty compl-closed sigma-multiplicative ) ( non empty compl-closed sigma-multiplicative V79() V80() V81() sigma-additive ) SigmaField of b1 : ( ( non empty ) ( non empty ) set ) ) , ExtREAL : ( ( ) ( non empty V86() ) set ) ) V62() V70() nonnegative sigma-additive ) sigma_Measure of b2 : ( ( non empty compl-closed sigma-multiplicative ) ( non empty compl-closed sigma-multiplicative V79() V80() V81() sigma-additive ) SigmaField of b1 : ( ( non empty ) ( non empty ) set ) ) ) ,g : ( ( Function-like ) ( Relation-like b1 : ( ( non empty ) ( non empty ) set ) -defined ExtREAL : ( ( ) ( non empty V86() ) set ) -valued Function-like V62() ) PartFunc of ,) )) : ( ( ) ( ext-real ) Element of ExtREAL : ( ( ) ( non empty V86() ) set ) ) : ( ( ) ( ext-real ) Element of ExtREAL : ( ( ) ( non empty V86() ) set ) ) ) ;

theorem :: MESFUNC4:6
for X being ( ( non empty ) ( non empty ) set )
for S being ( ( non empty compl-closed sigma-multiplicative ) ( non empty compl-closed sigma-multiplicative V79() V80() V81() sigma-additive ) SigmaField of X : ( ( non empty ) ( non empty ) set ) )
for M being ( ( Function-like V30(b2 : ( ( non empty compl-closed sigma-multiplicative ) ( non empty compl-closed sigma-multiplicative V79() V80() V81() sigma-additive ) SigmaField of b1 : ( ( non empty ) ( non empty ) set ) ) , ExtREAL : ( ( ) ( non empty V86() ) set ) ) V70() nonnegative sigma-additive ) ( Relation-like b2 : ( ( non empty compl-closed sigma-multiplicative ) ( non empty compl-closed sigma-multiplicative V79() V80() V81() sigma-additive ) SigmaField of b1 : ( ( non empty ) ( non empty ) set ) ) -defined ExtREAL : ( ( ) ( non empty V86() ) set ) -valued Function-like V30(b2 : ( ( non empty compl-closed sigma-multiplicative ) ( non empty compl-closed sigma-multiplicative V79() V80() V81() sigma-additive ) SigmaField of b1 : ( ( non empty ) ( non empty ) set ) ) , ExtREAL : ( ( ) ( non empty V86() ) set ) ) V62() V70() nonnegative sigma-additive ) sigma_Measure of S : ( ( non empty compl-closed sigma-multiplicative ) ( non empty compl-closed sigma-multiplicative V79() V80() V81() sigma-additive ) SigmaField of b1 : ( ( non empty ) ( non empty ) set ) ) )
for f, g being ( ( Function-like ) ( Relation-like b1 : ( ( non empty ) ( non empty ) set ) -defined ExtREAL : ( ( ) ( non empty V86() ) set ) -valued Function-like V62() ) PartFunc of ,)
for c being ( ( ) ( ext-real ) R_eal) st f : ( ( Function-like ) ( Relation-like b1 : ( ( non empty ) ( non empty ) set ) -defined ExtREAL : ( ( ) ( non empty V86() ) set ) -valued Function-like V62() ) PartFunc of ,) is_simple_func_in S : ( ( non empty compl-closed sigma-multiplicative ) ( non empty compl-closed sigma-multiplicative V79() V80() V81() sigma-additive ) SigmaField of b1 : ( ( non empty ) ( non empty ) set ) ) & dom f : ( ( Function-like ) ( Relation-like b1 : ( ( non empty ) ( non empty ) set ) -defined ExtREAL : ( ( ) ( non empty V86() ) set ) -valued Function-like V62() ) PartFunc of ,) : ( ( ) ( ) set ) <> {} : ( ( ) ( ) set ) & ( for x being ( ( ) ( ) set ) st x : ( ( ) ( ) set ) in dom f : ( ( Function-like ) ( Relation-like b1 : ( ( non empty ) ( non empty ) set ) -defined ExtREAL : ( ( ) ( non empty V86() ) set ) -valued Function-like V62() ) PartFunc of ,) : ( ( ) ( ) set ) holds
0. : ( ( ) ( ext-real ) Element of ExtREAL : ( ( ) ( non empty V86() ) set ) ) <= f : ( ( Function-like ) ( Relation-like b1 : ( ( non empty ) ( non empty ) set ) -defined ExtREAL : ( ( ) ( non empty V86() ) set ) -valued Function-like V62() ) PartFunc of ,) . x : ( ( ) ( ) set ) : ( ( ) ( ext-real ) Element of ExtREAL : ( ( ) ( non empty V86() ) set ) ) ) & 0. : ( ( ) ( ext-real ) Element of ExtREAL : ( ( ) ( non empty V86() ) set ) ) <= c : ( ( ) ( ext-real ) R_eal) & c : ( ( ) ( ext-real ) R_eal) < +infty : ( ( ) ( non empty V23() ext-real positive non negative ) Element of ExtREAL : ( ( ) ( non empty V86() ) set ) ) & dom g : ( ( Function-like ) ( Relation-like b1 : ( ( non empty ) ( non empty ) set ) -defined ExtREAL : ( ( ) ( non empty V86() ) set ) -valued Function-like V62() ) PartFunc of ,) : ( ( ) ( ) set ) = dom f : ( ( Function-like ) ( Relation-like b1 : ( ( non empty ) ( non empty ) set ) -defined ExtREAL : ( ( ) ( non empty V86() ) set ) -valued Function-like V62() ) PartFunc of ,) : ( ( ) ( ) set ) & ( for x being ( ( ) ( ) set ) st x : ( ( ) ( ) set ) in dom g : ( ( Function-like ) ( Relation-like b1 : ( ( non empty ) ( non empty ) set ) -defined ExtREAL : ( ( ) ( non empty V86() ) set ) -valued Function-like V62() ) PartFunc of ,) : ( ( ) ( ) set ) holds
g : ( ( Function-like ) ( Relation-like b1 : ( ( non empty ) ( non empty ) set ) -defined ExtREAL : ( ( ) ( non empty V86() ) set ) -valued Function-like V62() ) PartFunc of ,) . x : ( ( ) ( ) set ) : ( ( ) ( ext-real ) Element of ExtREAL : ( ( ) ( non empty V86() ) set ) ) = c : ( ( ) ( ext-real ) R_eal) * (f : ( ( Function-like ) ( Relation-like b1 : ( ( non empty ) ( non empty ) set ) -defined ExtREAL : ( ( ) ( non empty V86() ) set ) -valued Function-like V62() ) PartFunc of ,) . x : ( ( ) ( ) set ) ) : ( ( ) ( ext-real ) Element of ExtREAL : ( ( ) ( non empty V86() ) set ) ) : ( ( ) ( ext-real ) Element of ExtREAL : ( ( ) ( non empty V86() ) set ) ) ) holds
integral (X : ( ( non empty ) ( non empty ) set ) ,S : ( ( non empty compl-closed sigma-multiplicative ) ( non empty compl-closed sigma-multiplicative V79() V80() V81() sigma-additive ) SigmaField of b1 : ( ( non empty ) ( non empty ) set ) ) ,M : ( ( Function-like V30(b2 : ( ( non empty compl-closed sigma-multiplicative ) ( non empty compl-closed sigma-multiplicative V79() V80() V81() sigma-additive ) SigmaField of b1 : ( ( non empty ) ( non empty ) set ) ) , ExtREAL : ( ( ) ( non empty V86() ) set ) ) V70() nonnegative sigma-additive ) ( Relation-like b2 : ( ( non empty compl-closed sigma-multiplicative ) ( non empty compl-closed sigma-multiplicative V79() V80() V81() sigma-additive ) SigmaField of b1 : ( ( non empty ) ( non empty ) set ) ) -defined ExtREAL : ( ( ) ( non empty V86() ) set ) -valued Function-like V30(b2 : ( ( non empty compl-closed sigma-multiplicative ) ( non empty compl-closed sigma-multiplicative V79() V80() V81() sigma-additive ) SigmaField of b1 : ( ( non empty ) ( non empty ) set ) ) , ExtREAL : ( ( ) ( non empty V86() ) set ) ) V62() V70() nonnegative sigma-additive ) sigma_Measure of b2 : ( ( non empty compl-closed sigma-multiplicative ) ( non empty compl-closed sigma-multiplicative V79() V80() V81() sigma-additive ) SigmaField of b1 : ( ( non empty ) ( non empty ) set ) ) ) ,g : ( ( Function-like ) ( Relation-like b1 : ( ( non empty ) ( non empty ) set ) -defined ExtREAL : ( ( ) ( non empty V86() ) set ) -valued Function-like V62() ) PartFunc of ,) ) : ( ( ) ( ext-real ) Element of ExtREAL : ( ( ) ( non empty V86() ) set ) ) = c : ( ( ) ( ext-real ) R_eal) * (integral (X : ( ( non empty ) ( non empty ) set ) ,S : ( ( non empty compl-closed sigma-multiplicative ) ( non empty compl-closed sigma-multiplicative V79() V80() V81() sigma-additive ) SigmaField of b1 : ( ( non empty ) ( non empty ) set ) ) ,M : ( ( Function-like V30(b2 : ( ( non empty compl-closed sigma-multiplicative ) ( non empty compl-closed sigma-multiplicative V79() V80() V81() sigma-additive ) SigmaField of b1 : ( ( non empty ) ( non empty ) set ) ) , ExtREAL : ( ( ) ( non empty V86() ) set ) ) V70() nonnegative sigma-additive ) ( Relation-like b2 : ( ( non empty compl-closed sigma-multiplicative ) ( non empty compl-closed sigma-multiplicative V79() V80() V81() sigma-additive ) SigmaField of b1 : ( ( non empty ) ( non empty ) set ) ) -defined ExtREAL : ( ( ) ( non empty V86() ) set ) -valued Function-like V30(b2 : ( ( non empty compl-closed sigma-multiplicative ) ( non empty compl-closed sigma-multiplicative V79() V80() V81() sigma-additive ) SigmaField of b1 : ( ( non empty ) ( non empty ) set ) ) , ExtREAL : ( ( ) ( non empty V86() ) set ) ) V62() V70() nonnegative sigma-additive ) sigma_Measure of b2 : ( ( non empty compl-closed sigma-multiplicative ) ( non empty compl-closed sigma-multiplicative V79() V80() V81() sigma-additive ) SigmaField of b1 : ( ( non empty ) ( non empty ) set ) ) ) ,f : ( ( Function-like ) ( Relation-like b1 : ( ( non empty ) ( non empty ) set ) -defined ExtREAL : ( ( ) ( non empty V86() ) set ) -valued Function-like V62() ) PartFunc of ,) )) : ( ( ) ( ext-real ) Element of ExtREAL : ( ( ) ( non empty V86() ) set ) ) : ( ( ) ( ext-real ) Element of ExtREAL : ( ( ) ( non empty V86() ) set ) ) ;