INTEGRA5

:: INTEGRA5 semantic presentation

begin

for F, F1, F2 being ( ( ) ( Relation-like NAT : ( ( ) ( non empty non trivial ordinal V45() V46() V47() V48() V49() V50() V51() V60() V80() V81() left_end bounded_below ) Element of bool REAL : ( ( ) ( non empty non trivial V45() V46() V47() V51() V60() non bounded_below non bounded_above interval ) set ) : ( ( ) ( non empty non trivial V60() ) set ) ) -defined REAL : ( ( ) ( non empty non trivial V45() V46() V47() V51() V60() non bounded_below non bounded_above interval ) set ) -valued V6() V35() V36() V37() V60() FinSequence-like FinSubsequence-like ) FinSequence of REAL : ( ( ) ( non empty non trivial V45() V46() V47() V51() V60() non bounded_below non bounded_above interval ) set ) )
for r1, r2 being ( ( ) ( V22() real ext-real ) Real) st ( F1 : ( ( ) ( Relation-like NAT : ( ( ) ( non empty non trivial ordinal V45() V46() V47() V48() V49() V50() V51() V60() V80() V81() left_end bounded_below ) Element of bool REAL : ( ( ) ( non empty non trivial V45() V46() V47() V51() V60() non bounded_below non bounded_above interval ) set ) : ( ( ) ( non empty non trivial V60() ) set ) ) -defined REAL : ( ( ) ( non empty non trivial V45() V46() V47() V51() V60() non bounded_below non bounded_above interval ) set ) -valued V6() V35() V36() V37() V60() FinSequence-like FinSubsequence-like ) FinSequence of REAL : ( ( ) ( non empty non trivial V45() V46() V47() V51() V60() non bounded_below non bounded_above interval ) set ) ) = <*r1 : ( ( ) ( V22() real ext-real ) Real) *> : ( ( ) ( Relation-like NAT : ( ( ) ( non empty non trivial ordinal V45() V46() V47() V48() V49() V50() V51() V60() V80() V81() left_end bounded_below ) Element of bool REAL : ( ( ) ( non empty non trivial V45() V46() V47() V51() V60() non bounded_below non bounded_above interval ) set ) : ( ( ) ( non empty non trivial V60() ) set ) ) -defined REAL : ( ( ) ( non empty non trivial V45() V46() V47() V51() V60() non bounded_below non bounded_above interval ) set ) -valued V6() V7() non empty trivial V35() V36() V37() increasing decreasing non-decreasing non-increasing V60() V82(1 : ( ( ) ( non empty ordinal natural V22() real ext-real positive non negative V33() V34() V45() V46() V47() V48() V49() V50() V60() V80() left_end right_end bounded_below bounded_above real-bounded ) Element of NAT : ( ( ) ( non empty non trivial ordinal V45() V46() V47() V48() V49() V50() V51() V60() V80() V81() left_end bounded_below ) Element of bool REAL : ( ( ) ( non empty non trivial V45() V46() V47() V51() V60() non bounded_below non bounded_above interval ) set ) : ( ( ) ( non empty non trivial V60() ) set ) ) ) ) FinSequence-like FinSubsequence-like ) FinSequence of REAL : ( ( ) ( non empty non trivial V45() V46() V47() V51() V60() non bounded_below non bounded_above interval ) set ) ) ^ F : ( ( ) ( Relation-like NAT : ( ( ) ( non empty non trivial ordinal V45() V46() V47() V48() V49() V50() V51() V60() V80() V81() left_end bounded_below ) Element of bool REAL : ( ( ) ( non empty non trivial V45() V46() V47() V51() V60() non bounded_below non bounded_above interval ) set ) : ( ( ) ( non empty non trivial V60() ) set ) ) -defined REAL : ( ( ) ( non empty non trivial V45() V46() V47() V51() V60() non bounded_below non bounded_above interval ) set ) -valued V6() V35() V36() V37() V60() FinSequence-like FinSubsequence-like ) FinSequence of REAL : ( ( ) ( non empty non trivial V45() V46() V47() V51() V60() non bounded_below non bounded_above interval ) set ) ) : ( ( ) ( Relation-like NAT : ( ( ) ( non empty non trivial ordinal V45() V46() V47() V48() V49() V50() V51() V60() V80() V81() left_end bounded_below ) Element of bool REAL : ( ( ) ( non empty non trivial V45() V46() V47() V51() V60() non bounded_below non bounded_above interval ) set ) : ( ( ) ( non empty non trivial V60() ) set ) ) -defined REAL : ( ( ) ( non empty non trivial V45() V46() V47() V51() V60() non bounded_below non bounded_above interval ) set ) -valued V6() non empty V35() V36() V37() V60() FinSequence-like FinSubsequence-like ) FinSequence of REAL : ( ( ) ( non empty non trivial V45() V46() V47() V51() V60() non bounded_below non bounded_above interval ) set ) ) or F1 : ( ( ) ( Relation-like NAT : ( ( ) ( non empty non trivial ordinal V45() V46() V47() V48() V49() V50() V51() V60() V80() V81() left_end bounded_below ) Element of bool REAL : ( ( ) ( non empty non trivial V45() V46() V47() V51() V60() non bounded_below non bounded_above interval ) set ) : ( ( ) ( non empty non trivial V60() ) set ) ) -defined REAL : ( ( ) ( non empty non trivial V45() V46() V47() V51() V60() non bounded_below non bounded_above interval ) set ) -valued V6() V35() V36() V37() V60() FinSequence-like FinSubsequence-like ) FinSequence of REAL : ( ( ) ( non empty non trivial V45() V46() V47() V51() V60() non bounded_below non bounded_above interval ) set ) ) = F : ( ( ) ( Relation-like NAT : ( ( ) ( non empty non trivial ordinal V45() V46() V47() V48() V49() V50() V51() V60() V80() V81() left_end bounded_below ) Element of bool REAL : ( ( ) ( non empty non trivial V45() V46() V47() V51() V60() non bounded_below non bounded_above interval ) set ) : ( ( ) ( non empty non trivial V60() ) set ) ) -defined REAL : ( ( ) ( non empty non trivial V45() V46() V47() V51() V60() non bounded_below non bounded_above interval ) set ) -valued V6() V35() V36() V37() V60() FinSequence-like FinSubsequence-like ) FinSequence of REAL : ( ( ) ( non empty non trivial V45() V46() V47() V51() V60() non bounded_below non bounded_above interval ) set ) ) ^ <*r1 : ( ( ) ( V22() real ext-real ) Real) *> : ( ( ) ( Relation-like NAT : ( ( ) ( non empty non trivial ordinal V45() V46() V47() V48() V49() V50() V51() V60() V80() V81() left_end bounded_below ) Element of bool REAL : ( ( ) ( non empty non trivial V45() V46() V47() V51() V60() non bounded_below non bounded_above interval ) set ) : ( ( ) ( non empty non trivial V60() ) set ) ) -defined REAL : ( ( ) ( non empty non trivial V45() V46() V47() V51() V60() non bounded_below non bounded_above interval ) set ) -valued V6() V7() non empty trivial V35() V36() V37() increasing decreasing non-decreasing non-increasing V60() V82(1 : ( ( ) ( non empty ordinal natural V22() real ext-real positive non negative V33() V34() V45() V46() V47() V48() V49() V50() V60() V80() left_end right_end bounded_below bounded_above real-bounded ) Element of NAT : ( ( ) ( non empty non trivial ordinal V45() V46() V47() V48() V49() V50() V51() V60() V80() V81() left_end bounded_below ) Element of bool REAL : ( ( ) ( non empty non trivial V45() V46() V47() V51() V60() non bounded_below non bounded_above interval ) set ) : ( ( ) ( non empty non trivial V60() ) set ) ) ) ) FinSequence-like FinSubsequence-like ) FinSequence of REAL : ( ( ) ( non empty non trivial V45() V46() V47() V51() V60() non bounded_below non bounded_above interval ) set ) ) : ( ( ) ( Relation-like NAT : ( ( ) ( non empty non trivial ordinal V45() V46() V47() V48() V49() V50() V51() V60() V80() V81() left_end bounded_below ) Element of bool REAL : ( ( ) ( non empty non trivial V45() V46() V47() V51() V60() non bounded_below non bounded_above interval ) set ) : ( ( ) ( non empty non trivial V60() ) set ) ) -defined REAL : ( ( ) ( non empty non trivial V45() V46() V47() V51() V60() non bounded_below non bounded_above interval ) set ) -valued V6() non empty V35() V36() V37() V60() FinSequence-like FinSubsequence-like ) FinSequence of REAL : ( ( ) ( non empty non trivial V45() V46() V47() V51() V60() non bounded_below non bounded_above interval ) set ) ) ) & ( F2 : ( ( ) ( Relation-like NAT : ( ( ) ( non empty non trivial ordinal V45() V46() V47() V48() V49() V50() V51() V60() V80() V81() left_end bounded_below ) Element of bool REAL : ( ( ) ( non empty non trivial V45() V46() V47() V51() V60() non bounded_below non bounded_above interval ) set ) : ( ( ) ( non empty non trivial V60() ) set ) ) -defined REAL : ( ( ) ( non empty non trivial V45() V46() V47() V51() V60() non bounded_below non bounded_above interval ) set ) -valued V6() V35() V36() V37() V60() FinSequence-like FinSubsequence-like ) FinSequence of REAL : ( ( ) ( non empty non trivial V45() V46() V47() V51() V60() non bounded_below non bounded_above interval ) set ) ) = <*r2 : ( ( ) ( V22() real ext-real ) Real) *> : ( ( ) ( Relation-like NAT : ( ( ) ( non empty non trivial ordinal V45() V46() V47() V48() V49() V50() V51() V60() V80() V81() left_end bounded_below ) Element of bool REAL : ( ( ) ( non empty non trivial V45() V46() V47() V51() V60() non bounded_below non bounded_above interval ) set ) : ( ( ) ( non empty non trivial V60() ) set ) ) -defined REAL : ( ( ) ( non empty non trivial V45() V46() V47() V51() V60() non bounded_below non bounded_above interval ) set ) -valued V6() V7() non empty trivial V35() V36() V37() increasing decreasing non-decreasing non-increasing V60() V82(1 : ( ( ) ( non empty ordinal natural V22() real ext-real positive non negative V33() V34() V45() V46() V47() V48() V49() V50() V60() V80() left_end right_end bounded_below bounded_above real-bounded ) Element of NAT : ( ( ) ( non empty non trivial ordinal V45() V46() V47() V48() V49() V50() V51() V60() V80() V81() left_end bounded_below ) Element of bool REAL : ( ( ) ( non empty non trivial V45() V46() V47() V51() V60() non bounded_below non bounded_above interval ) set ) : ( ( ) ( non empty non trivial V60() ) set ) ) ) ) FinSequence-like FinSubsequence-like ) FinSequence of REAL : ( ( ) ( non empty non trivial V45() V46() V47() V51() V60() non bounded_below non bounded_above interval ) set ) ) ^ F : ( ( ) ( Relation-like NAT : ( ( ) ( non empty non trivial ordinal V45() V46() V47() V48() V49() V50() V51() V60() V80() V81() left_end bounded_below ) Element of bool REAL : ( ( ) ( non empty non trivial V45() V46() V47() V51() V60() non bounded_below non bounded_above interval ) set ) : ( ( ) ( non empty non trivial V60() ) set ) ) -defined REAL : ( ( ) ( non empty non trivial V45() V46() V47() V51() V60() non bounded_below non bounded_above interval ) set ) -valued V6() V35() V36() V37() V60() FinSequence-like FinSubsequence-like ) FinSequence of REAL : ( ( ) ( non empty non trivial V45() V46() V47() V51() V60() non bounded_below non bounded_above interval ) set ) ) : ( ( ) ( Relation-like NAT : ( ( ) ( non empty non trivial ordinal V45() V46() V47() V48() V49() V50() V51() V60() V80() V81() left_end bounded_below ) Element of bool REAL : ( ( ) ( non empty non trivial V45() V46() V47() V51() V60() non bounded_below non bounded_above interval ) set ) : ( ( ) ( non empty non trivial V60() ) set ) ) -defined REAL : ( ( ) ( non empty non trivial V45() V46() V47() V51() V60() non bounded_below non bounded_above interval ) set ) -valued V6() non empty V35() V36() V37() V60() FinSequence-like FinSubsequence-like ) FinSequence of REAL : ( ( ) ( non empty non trivial V45() V46() V47() V51() V60() non bounded_below non bounded_above interval ) set ) ) or F2 : ( ( ) ( Relation-like NAT : ( ( ) ( non empty non trivial ordinal V45() V46() V47() V48() V49() V50() V51() V60() V80() V81() left_end bounded_below ) Element of bool REAL : ( ( ) ( non empty non trivial V45() V46() V47() V51() V60() non bounded_below non bounded_above interval ) set ) : ( ( ) ( non empty non trivial V60() ) set ) ) -defined REAL : ( ( ) ( non empty non trivial V45() V46() V47() V51() V60() non bounded_below non bounded_above interval ) set ) -valued V6() V35() V36() V37() V60() FinSequence-like FinSubsequence-like ) FinSequence of REAL : ( ( ) ( non empty non trivial V45() V46() V47() V51() V60() non bounded_below non bounded_above interval ) set ) ) = F : ( ( ) ( Relation-like NAT : ( ( ) ( non empty non trivial ordinal V45() V46() V47() V48() V49() V50() V51() V60() V80() V81() left_end bounded_below ) Element of bool REAL : ( ( ) ( non empty non trivial V45() V46() V47() V51() V60() non bounded_below non bounded_above interval ) set ) : ( ( ) ( non empty non trivial V60() ) set ) ) -defined REAL : ( ( ) ( non empty non trivial V45() V46() V47() V51() V60() non bounded_below non bounded_above interval ) set ) -valued V6() V35() V36() V37() V60() FinSequence-like FinSubsequence-like ) FinSequence of REAL : ( ( ) ( non empty non trivial V45() V46() V47() V51() V60() non bounded_below non bounded_above interval ) set ) ) ^ <*r2 : ( ( ) ( V22() real ext-real ) Real) *> : ( ( ) ( Relation-like NAT : ( ( ) ( non empty non trivial ordinal V45() V46() V47() V48() V49() V50() V51() V60() V80() V81() left_end bounded_below ) Element of bool REAL : ( ( ) ( non empty non trivial V45() V46() V47() V51() V60() non bounded_below non bounded_above interval ) set ) : ( ( ) ( non empty non trivial V60() ) set ) ) -defined REAL : ( ( ) ( non empty non trivial V45() V46() V47() V51() V60() non bounded_below non bounded_above interval ) set ) -valued V6() V7() non empty trivial V35() V36() V37() increasing decreasing non-decreasing non-increasing V60() V82(1 : ( ( ) ( non empty ordinal natural V22() real ext-real positive non negative V33() V34() V45() V46() V47() V48() V49() V50() V60() V80() left_end right_end bounded_below bounded_above real-bounded ) Element of NAT : ( ( ) ( non empty non trivial ordinal V45() V46() V47() V48() V49() V50() V51() V60() V80() V81() left_end bounded_below ) Element of bool REAL : ( ( ) ( non empty non trivial V45() V46() V47() V51() V60() non bounded_below non bounded_above interval ) set ) : ( ( ) ( non empty non trivial V60() ) set ) ) ) ) FinSequence-like FinSubsequence-like ) FinSequence of REAL : ( ( ) ( non empty non trivial V45() V46() V47() V51() V60() non bounded_below non bounded_above interval ) set ) ) : ( ( ) ( Relation-like NAT : ( ( ) ( non empty non trivial ordinal V45() V46() V47() V48() V49() V50() V51() V60() V80() V81() left_end bounded_below ) Element of bool REAL : ( ( ) ( non empty non trivial V45() V46() V47() V51() V60() non bounded_below non bounded_above interval ) set ) : ( ( ) ( non empty non trivial V60() ) set ) ) -defined REAL : ( ( ) ( non empty non trivial V45() V46() V47() V51() V60() non bounded_below non bounded_above interval ) set ) -valued V6() non empty V35() V36() V37() V60() FinSequence-like FinSubsequence-like ) FinSequence of REAL : ( ( ) ( non empty non trivial V45() V46() V47() V51() V60() non bounded_below non bounded_above interval ) set ) ) ) holds
Sum (F1 : ( ( ) ( Relation-like NAT : ( ( ) ( non empty non trivial ordinal V45() V46() V47() V48() V49() V50() V51() V60() V80() V81() left_end bounded_below ) Element of bool REAL : ( ( ) ( non empty non trivial V45() V46() V47() V51() V60() non bounded_below non bounded_above interval ) set ) : ( ( ) ( non empty non trivial V60() ) set ) ) -defined REAL : ( ( ) ( non empty non trivial V45() V46() V47() V51() V60() non bounded_below non bounded_above interval ) set ) -valued V6() V35() V36() V37() V60() FinSequence-like FinSubsequence-like ) FinSequence of REAL : ( ( ) ( non empty non trivial V45() V46() V47() V51() V60() non bounded_below non bounded_above interval ) set ) ) - F2 : ( ( ) ( Relation-like NAT : ( ( ) ( non empty non trivial ordinal V45() V46() V47() V48() V49() V50() V51() V60() V80() V81() left_end bounded_below ) Element of bool REAL : ( ( ) ( non empty non trivial V45() V46() V47() V51() V60() non bounded_below non bounded_above interval ) set ) : ( ( ) ( non empty non trivial V60() ) set ) ) -defined REAL : ( ( ) ( non empty non trivial V45() V46() V47() V51() V60() non bounded_below non bounded_above interval ) set ) -valued V6() V35() V36() V37() V60() FinSequence-like FinSubsequence-like ) FinSequence of REAL : ( ( ) ( non empty non trivial V45() V46() V47() V51() V60() non bounded_below non bounded_above interval ) set ) ) ) : ( ( ) ( Relation-like NAT : ( ( ) ( non empty non trivial ordinal V45() V46() V47() V48() V49() V50() V51() V60() V80() V81() left_end bounded_below ) Element of bool REAL : ( ( ) ( non empty non trivial V45() V46() V47() V51() V60() non bounded_below non bounded_above interval ) set ) : ( ( ) ( non empty non trivial V60() ) set ) ) -defined REAL : ( ( ) ( non empty non trivial V45() V46() V47() V51() V60() non bounded_below non bounded_above interval ) set ) -valued V6() V35() V36() V37() V60() FinSequence-like FinSubsequence-like ) FinSequence of REAL : ( ( ) ( non empty non trivial V45() V46() V47() V51() V60() non bounded_below non bounded_above interval ) set ) ) : ( ( ) ( V22() real ext-real ) Element of REAL : ( ( ) ( non empty non trivial V45() V46() V47() V51() V60() non bounded_below non bounded_above interval ) set ) ) = r1 : ( ( ) ( V22() real ext-real ) Real) - r2 : ( ( ) ( V22() real ext-real ) Real) : ( ( ) ( V22() real ext-real ) Element of REAL : ( ( ) ( non empty non trivial V45() V46() V47() V51() V60() non bounded_below non bounded_above interval ) set ) ) ;

theorem :: INTEGRA5:2

for F1, F2 being ( ( ) ( Relation-like NAT : ( ( ) ( non empty non trivial ordinal V45() V46() V47() V48() V49() V50() V51() V60() V80() V81() left_end bounded_below ) Element of bool REAL : ( ( ) ( non empty non trivial V45() V46() V47() V51() V60() non bounded_below non bounded_above interval ) set ) : ( ( ) ( non empty non trivial V60() ) set ) ) -defined REAL : ( ( ) ( non empty non trivial V45() V46() V47() V51() V60() non bounded_below non bounded_above interval ) set ) -valued V6() V35() V36() V37() V60() FinSequence-like FinSubsequence-like ) FinSequence of REAL : ( ( ) ( non empty non trivial V45() V46() V47() V51() V60() non bounded_below non bounded_above interval ) set ) ) st len F1 : ( ( ) ( Relation-like NAT : ( ( ) ( non empty non trivial ordinal V45() V46() V47() V48() V49() V50() V51() V60() V80() V81() left_end bounded_below ) Element of bool REAL : ( ( ) ( non empty non trivial V45() V46() V47() V51() V60() non bounded_below non bounded_above interval ) set ) : ( ( ) ( non empty non trivial V60() ) set ) ) -defined REAL : ( ( ) ( non empty non trivial V45() V46() V47() V51() V60() non bounded_below non bounded_above interval ) set ) -valued V6() V35() V36() V37() V60() FinSequence-like FinSubsequence-like ) FinSequence of REAL : ( ( ) ( non empty non trivial V45() V46() V47() V51() V60() non bounded_below non bounded_above interval ) set ) ) : ( ( ) ( ordinal natural V22() real ext-real V33() V34() V45() V46() V47() V48() V49() V50() V60() V80() bounded_below bounded_above real-bounded ) Element of NAT : ( ( ) ( non empty non trivial ordinal V45() V46() V47() V48() V49() V50() V51() V60() V80() V81() left_end bounded_below ) Element of bool REAL : ( ( ) ( non empty non trivial V45() V46() V47() V51() V60() non bounded_below non bounded_above interval ) set ) : ( ( ) ( non empty non trivial V60() ) set ) ) ) = len F2 : ( ( ) ( Relation-like NAT : ( ( ) ( non empty non trivial ordinal V45() V46() V47() V48() V49() V50() V51() V60() V80() V81() left_end bounded_below ) Element of bool REAL : ( ( ) ( non empty non trivial V45() V46() V47() V51() V60() non bounded_below non bounded_above interval ) set ) : ( ( ) ( non empty non trivial V60() ) set ) ) -defined REAL : ( ( ) ( non empty non trivial V45() V46() V47() V51() V60() non bounded_below non bounded_above interval ) set ) -valued V6() V35() V36() V37() V60() FinSequence-like FinSubsequence-like ) FinSequence of REAL : ( ( ) ( non empty non trivial V45() V46() V47() V51() V60() non bounded_below non bounded_above interval ) set ) ) : ( ( ) ( ordinal natural V22() real ext-real V33() V34() V45() V46() V47() V48() V49() V50() V60() V80() bounded_below bounded_above real-bounded ) Element of NAT : ( ( ) ( non empty non trivial ordinal V45() V46() V47() V48() V49() V50() V51() V60() V80() V81() left_end bounded_below ) Element of bool REAL : ( ( ) ( non empty non trivial V45() V46() V47() V51() V60() non bounded_below non bounded_above interval ) set ) : ( ( ) ( non empty non trivial V60() ) set ) ) ) holds
( len (F1 : ( ( ) ( Relation-like NAT : ( ( ) ( non empty non trivial ordinal V45() V46() V47() V48() V49() V50() V51() V60() V80() V81() left_end bounded_below ) Element of bool REAL : ( ( ) ( non empty non trivial V45() V46() V47() V51() V60() non bounded_below non bounded_above interval ) set ) : ( ( ) ( non empty non trivial V60() ) set ) ) -defined REAL : ( ( ) ( non empty non trivial V45() V46() V47() V51() V60() non bounded_below non bounded_above interval ) set ) -valued V6() V35() V36() V37() V60() FinSequence-like FinSubsequence-like ) FinSequence of REAL : ( ( ) ( non empty non trivial V45() V46() V47() V51() V60() non bounded_below non bounded_above interval ) set ) ) + F2 : ( ( ) ( Relation-like NAT : ( ( ) ( non empty non trivial ordinal V45() V46() V47() V48() V49() V50() V51() V60() V80() V81() left_end bounded_below ) Element of bool REAL : ( ( ) ( non empty non trivial V45() V46() V47() V51() V60() non bounded_below non bounded_above interval ) set ) : ( ( ) ( non empty non trivial V60() ) set ) ) -defined REAL : ( ( ) ( non empty non trivial V45() V46() V47() V51() V60() non bounded_below non bounded_above interval ) set ) -valued V6() V35() V36() V37() V60() FinSequence-like FinSubsequence-like ) FinSequence of REAL : ( ( ) ( non empty non trivial V45() V46() V47() V51() V60() non bounded_below non bounded_above interval ) set ) ) ) : ( ( ) ( Relation-like NAT : ( ( ) ( non empty non trivial ordinal V45() V46() V47() V48() V49() V50() V51() V60() V80() V81() left_end bounded_below ) Element of bool REAL : ( ( ) ( non empty non trivial V45() V46() V47() V51() V60() non bounded_below non bounded_above interval ) set ) : ( ( ) ( non empty non trivial V60() ) set ) ) -defined REAL : ( ( ) ( non empty non trivial V45() V46() V47() V51() V60() non bounded_below non bounded_above interval ) set ) -valued V6() V35() V36() V37() V60() FinSequence-like FinSubsequence-like ) FinSequence of REAL : ( ( ) ( non empty non trivial V45() V46() V47() V51() V60() non bounded_below non bounded_above interval ) set ) ) : ( ( ) ( ordinal natural V22() real ext-real V33() V34() V45() V46() V47() V48() V49() V50() V60() V80() bounded_below bounded_above real-bounded ) Element of NAT : ( ( ) ( non empty non trivial ordinal V45() V46() V47() V48() V49() V50() V51() V60() V80() V81() left_end bounded_below ) Element of bool REAL : ( ( ) ( non empty non trivial V45() V46() V47() V51() V60() non bounded_below non bounded_above interval ) set ) : ( ( ) ( non empty non trivial V60() ) set ) ) ) = len F1 : ( ( ) ( Relation-like NAT : ( ( ) ( non empty non trivial ordinal V45() V46() V47() V48() V49() V50() V51() V60() V80() V81() left_end bounded_below ) Element of bool REAL : ( ( ) ( non empty non trivial V45() V46() V47() V51() V60() non bounded_below non bounded_above interval ) set ) : ( ( ) ( non empty non trivial V60() ) set ) ) -defined REAL : ( ( ) ( non empty non trivial V45() V46() V47() V51() V60() non bounded_below non bounded_above interval ) set ) -valued V6() V35() V36() V37() V60() FinSequence-like FinSubsequence-like ) FinSequence of REAL : ( ( ) ( non empty non trivial V45() V46() V47() V51() V60() non bounded_below non bounded_above interval ) set ) ) : ( ( ) ( ordinal natural V22() real ext-real V33() V34() V45() V46() V47() V48() V49() V50() V60() V80() bounded_below bounded_above real-bounded ) Element of NAT : ( ( ) ( non empty non trivial ordinal V45() V46() V47() V48() V49() V50() V51() V60() V80() V81() left_end bounded_below ) Element of bool REAL : ( ( ) ( non empty non trivial V45() V46() V47() V51() V60() non bounded_below non bounded_above interval ) set ) : ( ( ) ( non empty non trivial V60() ) set ) ) ) & len (F1 : ( ( ) ( Relation-like NAT : ( ( ) ( non empty non trivial ordinal V45() V46() V47() V48() V49() V50() V51() V60() V80() V81() left_end bounded_below ) Element of bool REAL : ( ( ) ( non empty non trivial V45() V46() V47() V51() V60() non bounded_below non bounded_above interval ) set ) : ( ( ) ( non empty non trivial V60() ) set ) ) -defined REAL : ( ( ) ( non empty non trivial V45() V46() V47() V51() V60() non bounded_below non bounded_above interval ) set ) -valued V6() V35() V36() V37() V60() FinSequence-like FinSubsequence-like ) FinSequence of REAL : ( ( ) ( non empty non trivial V45() V46() V47() V51() V60() non bounded_below non bounded_above interval ) set ) ) - F2 : ( ( ) ( Relation-like NAT : ( ( ) ( non empty non trivial ordinal V45() V46() V47() V48() V49() V50() V51() V60() V80() V81() left_end bounded_below ) Element of bool REAL : ( ( ) ( non empty non trivial V45() V46() V47() V51() V60() non bounded_below non bounded_above interval ) set ) : ( ( ) ( non empty non trivial V60() ) set ) ) -defined REAL : ( ( ) ( non empty non trivial V45() V46() V47() V51() V60() non bounded_below non bounded_above interval ) set ) -valued V6() V35() V36() V37() V60() FinSequence-like FinSubsequence-like ) FinSequence of REAL : ( ( ) ( non empty non trivial V45() V46() V47() V51() V60() non bounded_below non bounded_above interval ) set ) ) ) : ( ( ) ( Relation-like NAT : ( ( ) ( non empty non trivial ordinal V45() V46() V47() V48() V49() V50() V51() V60() V80() V81() left_end bounded_below ) Element of bool REAL : ( ( ) ( non empty non trivial V45() V46() V47() V51() V60() non bounded_below non bounded_above interval ) set ) : ( ( ) ( non empty non trivial V60() ) set ) ) -defined REAL : ( ( ) ( non empty non trivial V45() V46() V47() V51() V60() non bounded_below non bounded_above interval ) set ) -valued V6() V35() V36() V37() V60() FinSequence-like FinSubsequence-like ) FinSequence of REAL : ( ( ) ( non empty non trivial V45() V46() V47() V51() V60() non bounded_below non bounded_above interval ) set ) ) : ( ( ) ( ordinal natural V22() real ext-real V33() V34() V45() V46() V47() V48() V49() V50() V60() V80() bounded_below bounded_above real-bounded ) Element of NAT : ( ( ) ( non empty non trivial ordinal V45() V46() V47() V48() V49() V50() V51() V60() V80() V81() left_end bounded_below ) Element of bool REAL : ( ( ) ( non empty non trivial V45() V46() V47() V51() V60() non bounded_below non bounded_above interval ) set ) : ( ( ) ( non empty non trivial V60() ) set ) ) ) = len F1 : ( ( ) ( Relation-like NAT : ( ( ) ( non empty non trivial ordinal V45() V46() V47() V48() V49() V50() V51() V60() V80() V81() left_end bounded_below ) Element of bool REAL : ( ( ) ( non empty non trivial V45() V46() V47() V51() V60() non bounded_below non bounded_above interval ) set ) : ( ( ) ( non empty non trivial V60() ) set ) ) -defined REAL : ( ( ) ( non empty non trivial V45() V46() V47() V51() V60() non bounded_below non bounded_above interval ) set ) -valued V6() V35() V36() V37() V60() FinSequence-like FinSubsequence-like ) FinSequence of REAL : ( ( ) ( non empty non trivial V45() V46() V47() V51() V60() non bounded_below non bounded_above interval ) set ) ) : ( ( ) ( ordinal natural V22() real ext-real V33() V34() V45() V46() V47() V48() V49() V50() V60() V80() bounded_below bounded_above real-bounded ) Element of NAT : ( ( ) ( non empty non trivial ordinal V45() V46() V47() V48() V49() V50() V51() V60() V80() V81() left_end bounded_below ) Element of bool REAL : ( ( ) ( non empty non trivial V45() V46() V47() V51() V60() non bounded_below non bounded_above interval ) set ) : ( ( ) ( non empty non trivial V60() ) set ) ) ) & Sum (F1 : ( ( ) ( Relation-like NAT : ( ( ) ( non empty non trivial ordinal V45() V46() V47() V48() V49() V50() V51() V60() V80() V81() left_end bounded_below ) Element of bool REAL : ( ( ) ( non empty non trivial V45() V46() V47() V51() V60() non bounded_below non bounded_above interval ) set ) : ( ( ) ( non empty non trivial V60() ) set ) ) -defined REAL : ( ( ) ( non empty non trivial V45() V46() V47() V51() V60() non bounded_below non bounded_above interval ) set ) -valued V6() V35() V36() V37() V60() FinSequence-like FinSubsequence-like ) FinSequence of REAL : ( ( ) ( non empty non trivial V45() V46() V47() V51() V60() non bounded_below non bounded_above interval ) set ) ) + F2 : ( ( ) ( Relation-like NAT : ( ( ) ( non empty non trivial ordinal V45() V46() V47() V48() V49() V50() V51() V60() V80() V81() left_end bounded_below ) Element of bool REAL : ( ( ) ( non empty non trivial V45() V46() V47() V51() V60() non bounded_below non bounded_above interval ) set ) : ( ( ) ( non empty non trivial V60() ) set ) ) -defined REAL : ( ( ) ( non empty non trivial V45() V46() V47() V51() V60() non bounded_below non bounded_above interval ) set ) -valued V6() V35() V36() V37() V60() FinSequence-like FinSubsequence-like ) FinSequence of REAL : ( ( ) ( non empty non trivial V45() V46() V47() V51() V60() non bounded_below non bounded_above interval ) set ) ) ) : ( ( ) ( Relation-like NAT : ( ( ) ( non empty non trivial ordinal V45() V46() V47() V48() V49() V50() V51() V60() V80() V81() left_end bounded_below ) Element of bool REAL : ( ( ) ( non empty non trivial V45() V46() V47() V51() V60() non bounded_below non bounded_above interval ) set ) : ( ( ) ( non empty non trivial V60() ) set ) ) -defined REAL : ( ( ) ( non empty non trivial V45() V46() V47() V51() V60() non bounded_below non bounded_above interval ) set ) -valued V6() V35() V36() V37() V60() FinSequence-like FinSubsequence-like ) FinSequence of REAL : ( ( ) ( non empty non trivial V45() V46() V47() V51() V60() non bounded_below non bounded_above interval ) set ) ) : ( ( ) ( V22() real ext-real ) Element of REAL : ( ( ) ( non empty non trivial V45() V46() V47() V51() V60() non bounded_below non bounded_above interval ) set ) ) = (Sum F1 : ( ( ) ( Relation-like NAT : ( ( ) ( non empty non trivial ordinal V45() V46() V47() V48() V49() V50() V51() V60() V80() V81() left_end bounded_below ) Element of bool REAL : ( ( ) ( non empty non trivial V45() V46() V47() V51() V60() non bounded_below non bounded_above interval ) set ) : ( ( ) ( non empty non trivial V60() ) set ) ) -defined REAL : ( ( ) ( non empty non trivial V45() V46() V47() V51() V60() non bounded_below non bounded_above interval ) set ) -valued V6() V35() V36() V37() V60() FinSequence-like FinSubsequence-like ) FinSequence of REAL : ( ( ) ( non empty non trivial V45() V46() V47() V51() V60() non bounded_below non bounded_above interval ) set ) ) ) : ( ( ) ( V22() real ext-real ) Element of REAL : ( ( ) ( non empty non trivial V45() V46() V47() V51() V60() non bounded_below non bounded_above interval ) set ) ) + (Sum F2 : ( ( ) ( Relation-like NAT : ( ( ) ( non empty non trivial ordinal V45() V46() V47() V48() V49() V50() V51() V60() V80() V81() left_end bounded_below ) Element of bool REAL : ( ( ) ( non empty non trivial V45() V46() V47() V51() V60() non bounded_below non bounded_above interval ) set ) : ( ( ) ( non empty non trivial V60() ) set ) ) -defined REAL : ( ( ) ( non empty non trivial V45() V46() V47() V51() V60() non bounded_below non bounded_above interval ) set ) -valued V6() V35() V36() V37() V60() FinSequence-like FinSubsequence-like ) FinSequence of REAL : ( ( ) ( non empty non trivial V45() V46() V47() V51() V60() non bounded_below non bounded_above interval ) set ) ) ) : ( ( ) ( V22() real ext-real ) Element of REAL : ( ( ) ( non empty non trivial V45() V46() V47() V51() V60() non bounded_below non bounded_above interval ) set ) ) : ( ( ) ( V22() real ext-real ) Element of REAL : ( ( ) ( non empty non trivial V45() V46() V47() V51() V60() non bounded_below non bounded_above interval ) set ) ) & Sum (F1 : ( ( ) ( Relation-like NAT : ( ( ) ( non empty non trivial ordinal V45() V46() V47() V48() V49() V50() V51() V60() V80() V81() left_end bounded_below ) Element of bool REAL : ( ( ) ( non empty non trivial V45() V46() V47() V51() V60() non bounded_below non bounded_above interval ) set ) : ( ( ) ( non empty non trivial V60() ) set ) ) -defined REAL : ( ( ) ( non empty non trivial V45() V46() V47() V51() V60() non bounded_below non bounded_above interval ) set ) -valued V6() V35() V36() V37() V60() FinSequence-like FinSubsequence-like ) FinSequence of REAL : ( ( ) ( non empty non trivial V45() V46() V47() V51() V60() non bounded_below non bounded_above interval ) set ) ) - F2 : ( ( ) ( Relation-like NAT : ( ( ) ( non empty non trivial ordinal V45() V46() V47() V48() V49() V50() V51() V60() V80() V81() left_end bounded_below ) Element of bool REAL : ( ( ) ( non empty non trivial V45() V46() V47() V51() V60() non bounded_below non bounded_above interval ) set ) : ( ( ) ( non empty non trivial V60() ) set ) ) -defined REAL : ( ( ) ( non empty non trivial V45() V46() V47() V51() V60() non bounded_below non bounded_above interval ) set ) -valued V6() V35() V36() V37() V60() FinSequence-like FinSubsequence-like ) FinSequence of REAL : ( ( ) ( non empty non trivial V45() V46() V47() V51() V60() non bounded_below non bounded_above interval ) set ) ) ) : ( ( ) ( Relation-like NAT : ( ( ) ( non empty non trivial ordinal V45() V46() V47() V48() V49() V50() V51() V60() V80() V81() left_end bounded_below ) Element of bool REAL : ( ( ) ( non empty non trivial V45() V46() V47() V51() V60() non bounded_below non bounded_above interval ) set ) : ( ( ) ( non empty non trivial V60() ) set ) ) -defined REAL : ( ( ) ( non empty non trivial V45() V46() V47() V51() V60() non bounded_below non bounded_above interval ) set ) -valued V6() V35() V36() V37() V60() FinSequence-like FinSubsequence-like ) FinSequence of REAL : ( ( ) ( non empty non trivial V45() V46() V47() V51() V60() non bounded_below non bounded_above interval ) set ) ) : ( ( ) ( V22() real ext-real ) Element of REAL : ( ( ) ( non empty non trivial V45() V46() V47() V51() V60() non bounded_below non bounded_above interval ) set ) ) = (Sum F1 : ( ( ) ( Relation-like NAT : ( ( ) ( non empty non trivial ordinal V45() V46() V47() V48() V49() V50() V51() V60() V80() V81() left_end bounded_below ) Element of bool REAL : ( ( ) ( non empty non trivial V45() V46() V47() V51() V60() non bounded_below non bounded_above interval ) set ) : ( ( ) ( non empty non trivial V60() ) set ) ) -defined REAL : ( ( ) ( non empty non trivial V45() V46() V47() V51() V60() non bounded_below non bounded_above interval ) set ) -valued V6() V35() V36() V37() V60() FinSequence-like FinSubsequence-like ) FinSequence of REAL : ( ( ) ( non empty non trivial V45() V46() V47() V51() V60() non bounded_below non bounded_above interval ) set ) ) ) : ( ( ) ( V22() real ext-real ) Element of REAL : ( ( ) ( non empty non trivial V45() V46() V47() V51() V60() non bounded_below non bounded_above interval ) set ) ) - (Sum F2 : ( ( ) ( Relation-like NAT : ( ( ) ( non empty non trivial ordinal V45() V46() V47() V48() V49() V50() V51() V60() V80() V81() left_end bounded_below ) Element of bool REAL : ( ( ) ( non empty non trivial V45() V46() V47() V51() V60() non bounded_below non bounded_above interval ) set ) : ( ( ) ( non empty non trivial V60() ) set ) ) -defined REAL : ( ( ) ( non empty non trivial V45() V46() V47() V51() V60() non bounded_below non bounded_above interval ) set ) -valued V6() V35() V36() V37() V60() FinSequence-like FinSubsequence-like ) FinSequence of REAL : ( ( ) ( non empty non trivial V45() V46() V47() V51() V60() non bounded_below non bounded_above interval ) set ) ) ) : ( ( ) ( V22() real ext-real ) Element of REAL : ( ( ) ( non empty non trivial V45() V46() V47() V51() V60() non bounded_below non bounded_above interval ) set ) ) : ( ( ) ( V22() real ext-real ) Element of REAL : ( ( ) ( non empty non trivial V45() V46() V47() V51() V60() non bounded_below non bounded_above interval ) set ) ) ) ;

theorem :: INTEGRA5:3

begin

notation

end;

definition

let f be ( ( V6() ) ( Relation-like REAL : ( ( ) ( non empty non trivial V45() V46() V47() V51() V60() non bounded_below non bounded_above interval ) set ) -defined REAL : ( ( ) ( non empty non trivial V45() V46() V47() V51() V60() non bounded_below non bounded_above interval ) set ) -valued V6() V35() V36() V37() ) PartFunc of ,) ;
let C be ( ( non empty ) ( non empty V45() V46() V47() ) Subset of ( ( ) ( non empty non trivial V60() ) set ) ) ;
:: original: ||
redefine func f || C -> ( ( V6() ) ( Relation-like C : ( ( ext-real ) ( ext-real ) set ) -defined REAL : ( ( ) ( non empty non trivial V45() V46() V47() V51() V60() non bounded_below non bounded_above interval ) set ) -valued V6() V35() V36() V37() ) PartFunc of ,) ;

end;

theorem :: INTEGRA5:4

for f, g being ( ( V6() ) ( Relation-like REAL : ( ( ) ( non empty non trivial V45() V46() V47() V51() V60() non bounded_below non bounded_above interval ) set ) -defined REAL : ( ( ) ( non empty non trivial V45() V46() V47() V51() V60() non bounded_below non bounded_above interval ) set ) -valued V6() V35() V36() V37() ) PartFunc of ,)
for C being ( ( non empty ) ( non empty V45() V46() V47() ) Subset of ( ( ) ( non empty non trivial V60() ) set ) ) holds (f : ( ( V6() ) ( Relation-like REAL : ( ( ) ( non empty non trivial V45() V46() V47() V51() V60() non bounded_below non bounded_above interval ) set ) -defined REAL : ( ( ) ( non empty non trivial V45() V46() V47() V51() V60() non bounded_below non bounded_above interval ) set ) -valued V6() V35() V36() V37() ) PartFunc of ,) || C : ( ( non empty ) ( non empty V45() V46() V47() ) Subset of ( ( ) ( non empty non trivial V60() ) set ) ) ) : ( ( V6() ) ( Relation-like b₃ : ( ( non empty ) ( non empty V45() V46() V47() ) Subset of ( ( ) ( non empty non trivial V60() ) set ) ) -defined REAL : ( ( ) ( non empty non trivial V45() V46() V47() V51() V60() non bounded_below non bounded_above interval ) set ) -defined REAL : ( ( ) ( non empty non trivial V45() V46() V47() V51() V60() non bounded_below non bounded_above interval ) set ) -valued V6() V35() V36() V37() ) PartFunc of ,) (#) (g : ( ( V6() ) ( Relation-like REAL : ( ( ) ( non empty non trivial V45() V46() V47() V51() V60() non bounded_below non bounded_above interval ) set ) -defined REAL : ( ( ) ( non empty non trivial V45() V46() V47() V51() V60() non bounded_below non bounded_above interval ) set ) -valued V6() V35() V36() V37() ) PartFunc of ,) || C : ( ( non empty ) ( non empty V45() V46() V47() ) Subset of ( ( ) ( non empty non trivial V60() ) set ) ) ) : ( ( V6() ) ( Relation-like b₃ : ( ( non empty ) ( non empty V45() V46() V47() ) Subset of ( ( ) ( non empty non trivial V60() ) set ) ) -defined REAL : ( ( ) ( non empty non trivial V45() V46() V47() V51() V60() non bounded_below non bounded_above interval ) set ) -defined REAL : ( ( ) ( non empty non trivial V45() V46() V47() V51() V60() non bounded_below non bounded_above interval ) set ) -valued V6() V35() V36() V37() ) PartFunc of ,) : ( ( V6() ) ( Relation-like b₃ : ( ( non empty ) ( non empty V45() V46() V47() ) Subset of ( ( ) ( non empty non trivial V60() ) set ) ) -defined REAL : ( ( ) ( non empty non trivial V45() V46() V47() V51() V60() non bounded_below non bounded_above interval ) set ) -valued V6() V35() V36() V37() ) Element of bool [:b₃ : ( ( non empty ) ( non empty V45() V46() V47() ) Subset of ( ( ) ( non empty non trivial V60() ) set ) ) ,REAL : ( ( ) ( non empty non trivial V45() V46() V47() V51() V60() non bounded_below non bounded_above interval ) set ) :] : ( ( ) ( Relation-like non empty non trivial V35() V36() V37() V60() ) set ) : ( ( ) ( non empty non trivial V60() ) set ) ) = (f : ( ( V6() ) ( Relation-like REAL : ( ( ) ( non empty non trivial V45() V46() V47() V51() V60() non bounded_below non bounded_above interval ) set ) -defined REAL : ( ( ) ( non empty non trivial V45() V46() V47() V51() V60() non bounded_below non bounded_above interval ) set ) -valued V6() V35() V36() V37() ) PartFunc of ,) (#) g : ( ( V6() ) ( Relation-like REAL : ( ( ) ( non empty non trivial V45() V46() V47() V51() V60() non bounded_below non bounded_above interval ) set ) -defined REAL : ( ( ) ( non empty non trivial V45() V46() V47() V51() V60() non bounded_below non bounded_above interval ) set ) -valued V6() V35() V36() V37() ) PartFunc of ,) ) : ( ( V6() ) ( Relation-like REAL : ( ( ) ( non empty non trivial V45() V46() V47() V51() V60() non bounded_below non bounded_above interval ) set ) -defined REAL : ( ( ) ( non empty non trivial V45() V46() V47() V51() V60() non bounded_below non bounded_above interval ) set ) -valued V6() V35() V36() V37() ) Element of bool [:REAL : ( ( ) ( non empty non trivial V45() V46() V47() V51() V60() non bounded_below non bounded_above interval ) set ) ,REAL : ( ( ) ( non empty non trivial V45() V46() V47() V51() V60() non bounded_below non bounded_above interval ) set ) :] : ( ( ) ( Relation-like non empty non trivial V35() V36() V37() V60() ) set ) : ( ( ) ( non empty non trivial V60() ) set ) ) || C : ( ( non empty ) ( non empty V45() V46() V47() ) Subset of ( ( ) ( non empty non trivial V60() ) set ) ) : ( ( V6() ) ( Relation-like b₃ : ( ( non empty ) ( non empty V45() V46() V47() ) Subset of ( ( ) ( non empty non trivial V60() ) set ) ) -defined REAL : ( ( ) ( non empty non trivial V45() V46() V47() V51() V60() non bounded_below non bounded_above interval ) set ) -defined REAL : ( ( ) ( non empty non trivial V45() V46() V47() V51() V60() non bounded_below non bounded_above interval ) set ) -valued V6() V35() V36() V37() ) PartFunc of ,) ;

theorem :: INTEGRA5:5

for f, g being ( ( V6() ) ( Relation-like REAL : ( ( ) ( non empty non trivial V45() V46() V47() V51() V60() non bounded_below non bounded_above interval ) set ) -defined REAL : ( ( ) ( non empty non trivial V45() V46() V47() V51() V60() non bounded_below non bounded_above interval ) set ) -valued V6() V35() V36() V37() ) PartFunc of ,)
for C being ( ( non empty ) ( non empty V45() V46() V47() ) Subset of ( ( ) ( non empty non trivial V60() ) set ) ) holds (f : ( ( V6() ) ( Relation-like REAL : ( ( ) ( non empty non trivial V45() V46() V47() V51() V60() non bounded_below non bounded_above interval ) set ) -defined REAL : ( ( ) ( non empty non trivial V45() V46() V47() V51() V60() non bounded_below non bounded_above interval ) set ) -valued V6() V35() V36() V37() ) PartFunc of ,) + g : ( ( V6() ) ( Relation-like REAL : ( ( ) ( non empty non trivial V45() V46() V47() V51() V60() non bounded_below non bounded_above interval ) set ) -defined REAL : ( ( ) ( non empty non trivial V45() V46() V47() V51() V60() non bounded_below non bounded_above interval ) set ) -valued V6() V35() V36() V37() ) PartFunc of ,) ) : ( ( V6() ) ( Relation-like REAL : ( ( ) ( non empty non trivial V45() V46() V47() V51() V60() non bounded_below non bounded_above interval ) set ) -defined REAL : ( ( ) ( non empty non trivial V45() V46() V47() V51() V60() non bounded_below non bounded_above interval ) set ) -valued V6() V35() V36() V37() ) Element of bool [:REAL : ( ( ) ( non empty non trivial V45() V46() V47() V51() V60() non bounded_below non bounded_above interval ) set ) ,REAL : ( ( ) ( non empty non trivial V45() V46() V47() V51() V60() non bounded_below non bounded_above interval ) set ) :] : ( ( ) ( Relation-like non empty non trivial V35() V36() V37() V60() ) set ) : ( ( ) ( non empty non trivial V60() ) set ) ) || C : ( ( non empty ) ( non empty V45() V46() V47() ) Subset of ( ( ) ( non empty non trivial V60() ) set ) ) : ( ( V6() ) ( Relation-like b₃ : ( ( non empty ) ( non empty V45() V46() V47() ) Subset of ( ( ) ( non empty non trivial V60() ) set ) ) -defined REAL : ( ( ) ( non empty non trivial V45() V46() V47() V51() V60() non bounded_below non bounded_above interval ) set ) -defined REAL : ( ( ) ( non empty non trivial V45() V46() V47() V51() V60() non bounded_below non bounded_above interval ) set ) -valued V6() V35() V36() V37() ) PartFunc of ,) = (f : ( ( V6() ) ( Relation-like REAL : ( ( ) ( non empty non trivial V45() V46() V47() V51() V60() non bounded_below non bounded_above interval ) set ) -defined REAL : ( ( ) ( non empty non trivial V45() V46() V47() V51() V60() non bounded_below non bounded_above interval ) set ) -valued V6() V35() V36() V37() ) PartFunc of ,) || C : ( ( non empty ) ( non empty V45() V46() V47() ) Subset of ( ( ) ( non empty non trivial V60() ) set ) ) ) : ( ( V6() ) ( Relation-like b₃ : ( ( non empty ) ( non empty V45() V46() V47() ) Subset of ( ( ) ( non empty non trivial V60() ) set ) ) -defined REAL : ( ( ) ( non empty non trivial V45() V46() V47() V51() V60() non bounded_below non bounded_above interval ) set ) -defined REAL : ( ( ) ( non empty non trivial V45() V46() V47() V51() V60() non bounded_below non bounded_above interval ) set ) -valued V6() V35() V36() V37() ) PartFunc of ,) + (g : ( ( V6() ) ( Relation-like REAL : ( ( ) ( non empty non trivial V45() V46() V47() V51() V60() non bounded_below non bounded_above interval ) set ) -defined REAL : ( ( ) ( non empty non trivial V45() V46() V47() V51() V60() non bounded_below non bounded_above interval ) set ) -valued V6() V35() V36() V37() ) PartFunc of ,) || C : ( ( non empty ) ( non empty V45() V46() V47() ) Subset of ( ( ) ( non empty non trivial V60() ) set ) ) ) : ( ( V6() ) ( Relation-like b₃ : ( ( non empty ) ( non empty V45() V46() V47() ) Subset of ( ( ) ( non empty non trivial V60() ) set ) ) -defined REAL : ( ( ) ( non empty non trivial V45() V46() V47() V51() V60() non bounded_below non bounded_above interval ) set ) -defined REAL : ( ( ) ( non empty non trivial V45() V46() V47() V51() V60() non bounded_below non bounded_above interval ) set ) -valued V6() V35() V36() V37() ) PartFunc of ,) : ( ( V6() ) ( Relation-like b₃ : ( ( non empty ) ( non empty V45() V46() V47() ) Subset of ( ( ) ( non empty non trivial V60() ) set ) ) -defined REAL : ( ( ) ( non empty non trivial V45() V46() V47() V51() V60() non bounded_below non bounded_above interval ) set ) -valued V6() V35() V36() V37() ) Element of bool [:b₃ : ( ( non empty ) ( non empty V45() V46() V47() ) Subset of ( ( ) ( non empty non trivial V60() ) set ) ) ,REAL : ( ( ) ( non empty non trivial V45() V46() V47() V51() V60() non bounded_below non bounded_above interval ) set ) :] : ( ( ) ( Relation-like non empty non trivial V35() V36() V37() V60() ) set ) : ( ( ) ( non empty non trivial V60() ) set ) ) ;

definition

let A be ( ( non empty closed_interval ) ( non empty V45() V46() V47() compact closed closed_interval bounded_below bounded_above real-bounded interval ) Subset of ( ( ) ( non empty non trivial V60() ) set ) ) ;
let f be ( ( V6() ) ( Relation-like REAL : ( ( ) ( non empty non trivial V45() V46() V47() V51() V60() non bounded_below non bounded_above interval ) set ) -defined REAL : ( ( ) ( non empty non trivial V45() V46() V47() V51() V60() non bounded_below non bounded_above interval ) set ) -valued V6() V35() V36() V37() ) PartFunc of ,) ;

pred f is_integrable_on A means :: INTEGRA5:def 1
f : ( ( ext-real ) ( ext-real ) set ) || A : ( ( ext-real ) ( ext-real ) set ) : ( ( V6() ) ( Relation-like A : ( ( ext-real ) ( ext-real ) set ) -defined REAL : ( ( ) ( non empty non trivial V45() V46() V47() V51() V60() non bounded_below non bounded_above interval ) set ) -valued V6() V35() V36() V37() ) PartFunc of ,) is integrable ;

end;

definition

func integral (f,A) -> ( ( ) ( V22() real ext-real ) Real) equals :: INTEGRA5:def 2
integral (f : ( ( ext-real ) ( ext-real ) set ) || A : ( ( ext-real ) ( ext-real ) set ) ) : ( ( V6() ) ( Relation-like A : ( ( ext-real ) ( ext-real ) set ) -defined REAL : ( ( ) ( non empty non trivial V45() V46() V47() V51() V60() non bounded_below non bounded_above interval ) set ) -valued V6() V35() V36() V37() ) PartFunc of ,) : ( ( ) ( V22() real ext-real ) Element of REAL : ( ( ) ( non empty non trivial V45() V46() V47() V51() V60() non bounded_below non bounded_above interval ) set ) ) ;

end;

theorem :: INTEGRA5:6

theorem :: INTEGRA5:7

theorem :: INTEGRA5:8

theorem :: INTEGRA5:9

begin

theorem :: INTEGRA5:10

theorem :: INTEGRA5:11

theorem :: INTEGRA5:12

for A being ( ( non empty closed_interval ) ( non empty V45() V46() V47() compact closed closed_interval bounded_below bounded_above real-bounded interval ) Subset of ( ( ) ( non empty non trivial V60() ) set ) )
for X being ( ( ) ( ) set )
for f being ( ( V6() ) ( Relation-like REAL : ( ( ) ( non empty non trivial V45() V46() V47() V51() V60() non bounded_below non bounded_above interval ) set ) -defined REAL : ( ( ) ( non empty non trivial V45() V46() V47() V51() V60() non bounded_below non bounded_above interval ) set ) -valued V6() V35() V36() V37() ) PartFunc of ,)
for D being ( ( ) ( Relation-like NAT : ( ( ) ( non empty non trivial ordinal V45() V46() V47() V48() V49() V50() V51() V60() V80() V81() left_end bounded_below ) Element of bool REAL : ( ( ) ( non empty non trivial V45() V46() V47() V51() V60() non bounded_below non bounded_above interval ) set ) : ( ( ) ( non empty non trivial V60() ) set ) ) -defined REAL : ( ( ) ( non empty non trivial V45() V46() V47() V51() V60() non bounded_below non bounded_above interval ) set ) -valued V6() V7() non empty V35() V36() V37() increasing non-decreasing V60() FinSequence-like FinSubsequence-like ) Division of A : ( ( non empty closed_interval ) ( non empty V45() V46() V47() compact closed closed_interval bounded_below bounded_above real-bounded interval ) Subset of ( ( ) ( non empty non trivial V60() ) set ) ) ) st A : ( ( non empty closed_interval ) ( non empty V45() V46() V47() compact closed closed_interval bounded_below bounded_above real-bounded interval ) Subset of ( ( ) ( non empty non trivial V60() ) set ) ) c= X : ( ( ) ( ) set ) & f : ( ( V6() ) ( Relation-like REAL : ( ( ) ( non empty non trivial V45() V46() V47() V51() V60() non bounded_below non bounded_above interval ) set ) -defined REAL : ( ( ) ( non empty non trivial V45() V46() V47() V51() V60() non bounded_below non bounded_above interval ) set ) -valued V6() V35() V36() V37() ) PartFunc of ,) is_differentiable_on X : ( ( ) ( ) set ) & (f : ( ( V6() ) ( Relation-like REAL : ( ( ) ( non empty non trivial V45() V46() V47() V51() V60() non bounded_below non bounded_above interval ) set ) -defined REAL : ( ( ) ( non empty non trivial V45() V46() V47() V51() V60() non bounded_below non bounded_above interval ) set ) -valued V6() V35() V36() V37() ) PartFunc of ,) `| X : ( ( ) ( ) set ) ) : ( ( V6() ) ( Relation-like REAL : ( ( ) ( non empty non trivial V45() V46() V47() V51() V60() non bounded_below non bounded_above interval ) set ) -defined REAL : ( ( ) ( non empty non trivial V45() V46() V47() V51() V60() non bounded_below non bounded_above interval ) set ) -valued V6() V35() V36() V37() ) Element of bool [:REAL : ( ( ) ( non empty non trivial V45() V46() V47() V51() V60() non bounded_below non bounded_above interval ) set ) ,REAL : ( ( ) ( non empty non trivial V45() V46() V47() V51() V60() non bounded_below non bounded_above interval ) set ) :] : ( ( ) ( Relation-like non empty non trivial V35() V36() V37() V60() ) set ) : ( ( ) ( non empty non trivial V60() ) set ) ) | A : ( ( non empty closed_interval ) ( non empty V45() V46() V47() compact closed closed_interval bounded_below bounded_above real-bounded interval ) Subset of ( ( ) ( non empty non trivial V60() ) set ) ) : ( ( V6() ) ( Relation-like b₁ : ( ( non empty closed_interval ) ( non empty V45() V46() V47() compact closed closed_interval bounded_below bounded_above real-bounded interval ) Subset of ( ( ) ( non empty non trivial V60() ) set ) ) -defined REAL : ( ( ) ( non empty non trivial V45() V46() V47() V51() V60() non bounded_below non bounded_above interval ) set ) -defined REAL : ( ( ) ( non empty non trivial V45() V46() V47() V51() V60() non bounded_below non bounded_above interval ) set ) -valued V6() V35() V36() V37() ) Element of bool [:REAL : ( ( ) ( non empty non trivial V45() V46() V47() V51() V60() non bounded_below non bounded_above interval ) set ) ,REAL : ( ( ) ( non empty non trivial V45() V46() V47() V51() V60() non bounded_below non bounded_above interval ) set ) :] : ( ( ) ( Relation-like non empty non trivial V35() V36() V37() V60() ) set ) : ( ( ) ( non empty non trivial V60() ) set ) ) is bounded holds
( lower_sum (((f : ( ( V6() ) ( Relation-like REAL : ( ( ) ( non empty non trivial V45() V46() V47() V51() V60() non bounded_below non bounded_above interval ) set ) -defined REAL : ( ( ) ( non empty non trivial V45() V46() V47() V51() V60() non bounded_below non bounded_above interval ) set ) -valued V6() V35() V36() V37() ) PartFunc of ,) `| X : ( ( ) ( ) set ) ) : ( ( V6() ) ( Relation-like REAL : ( ( ) ( non empty non trivial V45() V46() V47() V51() V60() non bounded_below non bounded_above interval ) set ) -defined REAL : ( ( ) ( non empty non trivial V45() V46() V47() V51() V60() non bounded_below non bounded_above interval ) set ) -valued V6() V35() V36() V37() ) Element of bool [:REAL : ( ( ) ( non empty non trivial V45() V46() V47() V51() V60() non bounded_below non bounded_above interval ) set ) ,REAL : ( ( ) ( non empty non trivial V45() V46() V47() V51() V60() non bounded_below non bounded_above interval ) set ) :] : ( ( ) ( Relation-like non empty non trivial V35() V36() V37() V60() ) set ) : ( ( ) ( non empty non trivial V60() ) set ) ) || A : ( ( non empty closed_interval ) ( non empty V45() V46() V47() compact closed closed_interval bounded_below bounded_above real-bounded interval ) Subset of ( ( ) ( non empty non trivial V60() ) set ) ) ) : ( ( V6() ) ( Relation-like b₁ : ( ( non empty closed_interval ) ( non empty V45() V46() V47() compact closed closed_interval bounded_below bounded_above real-bounded interval ) Subset of ( ( ) ( non empty non trivial V60() ) set ) ) -defined REAL : ( ( ) ( non empty non trivial V45() V46() V47() V51() V60() non bounded_below non bounded_above interval ) set ) -defined REAL : ( ( ) ( non empty non trivial V45() V46() V47() V51() V60() non bounded_below non bounded_above interval ) set ) -valued V6() V35() V36() V37() ) PartFunc of ,) ,D : ( ( ) ( Relation-like NAT : ( ( ) ( non empty non trivial ordinal V45() V46() V47() V48() V49() V50() V51() V60() V80() V81() left_end bounded_below ) Element of bool REAL : ( ( ) ( non empty non trivial V45() V46() V47() V51() V60() non bounded_below non bounded_above interval ) set ) : ( ( ) ( non empty non trivial V60() ) set ) ) -defined REAL : ( ( ) ( non empty non trivial V45() V46() V47() V51() V60() non bounded_below non bounded_above interval ) set ) -valued V6() V7() non empty V35() V36() V37() increasing non-decreasing V60() FinSequence-like FinSubsequence-like ) Division of b₁ : ( ( non empty closed_interval ) ( non empty V45() V46() V47() compact closed closed_interval bounded_below bounded_above real-bounded interval ) Subset of ( ( ) ( non empty non trivial V60() ) set ) ) ) ) : ( ( ) ( V22() real ext-real ) Element of REAL : ( ( ) ( non empty non trivial V45() V46() V47() V51() V60() non bounded_below non bounded_above interval ) set ) ) <= (f : ( ( V6() ) ( Relation-like REAL : ( ( ) ( non empty non trivial V45() V46() V47() V51() V60() non bounded_below non bounded_above interval ) set ) -defined REAL : ( ( ) ( non empty non trivial V45() V46() V47() V51() V60() non bounded_below non bounded_above interval ) set ) -valued V6() V35() V36() V37() ) PartFunc of ,) . (upper_bound A : ( ( non empty closed_interval ) ( non empty V45() V46() V47() compact closed closed_interval bounded_below bounded_above real-bounded interval ) Subset of ( ( ) ( non empty non trivial V60() ) set ) ) ) : ( ( ) ( V22() real ext-real ) Element of REAL : ( ( ) ( non empty non trivial V45() V46() V47() V51() V60() non bounded_below non bounded_above interval ) set ) ) ) : ( ( ) ( V22() real ext-real ) Element of REAL : ( ( ) ( non empty non trivial V45() V46() V47() V51() V60() non bounded_below non bounded_above interval ) set ) ) - (f : ( ( V6() ) ( Relation-like REAL : ( ( ) ( non empty non trivial V45() V46() V47() V51() V60() non bounded_below non bounded_above interval ) set ) -defined REAL : ( ( ) ( non empty non trivial V45() V46() V47() V51() V60() non bounded_below non bounded_above interval ) set ) -valued V6() V35() V36() V37() ) PartFunc of ,) . (lower_bound A : ( ( non empty closed_interval ) ( non empty V45() V46() V47() compact closed closed_interval bounded_below bounded_above real-bounded interval ) Subset of ( ( ) ( non empty non trivial V60() ) set ) ) ) : ( ( ) ( V22() real ext-real ) Element of REAL : ( ( ) ( non empty non trivial V45() V46() V47() V51() V60() non bounded_below non bounded_above interval ) set ) ) ) : ( ( ) ( V22() real ext-real ) Element of REAL : ( ( ) ( non empty non trivial V45() V46() V47() V51() V60() non bounded_below non bounded_above interval ) set ) ) : ( ( ) ( V22() real ext-real ) Element of REAL : ( ( ) ( non empty non trivial V45() V46() V47() V51() V60() non bounded_below non bounded_above interval ) set ) ) & (f : ( ( V6() ) ( Relation-like REAL : ( ( ) ( non empty non trivial V45() V46() V47() V51() V60() non bounded_below non bounded_above interval ) set ) -defined REAL : ( ( ) ( non empty non trivial V45() V46() V47() V51() V60() non bounded_below non bounded_above interval ) set ) -valued V6() V35() V36() V37() ) PartFunc of ,) . (upper_bound A : ( ( non empty closed_interval ) ( non empty V45() V46() V47() compact closed closed_interval bounded_below bounded_above real-bounded interval ) Subset of ( ( ) ( non empty non trivial V60() ) set ) ) ) : ( ( ) ( V22() real ext-real ) Element of REAL : ( ( ) ( non empty non trivial V45() V46() V47() V51() V60() non bounded_below non bounded_above interval ) set ) ) ) : ( ( ) ( V22() real ext-real ) Element of REAL : ( ( ) ( non empty non trivial V45() V46() V47() V51() V60() non bounded_below non bounded_above interval ) set ) ) - (f : ( ( V6() ) ( Relation-like REAL : ( ( ) ( non empty non trivial V45() V46() V47() V51() V60() non bounded_below non bounded_above interval ) set ) -defined REAL : ( ( ) ( non empty non trivial V45() V46() V47() V51() V60() non bounded_below non bounded_above interval ) set ) -valued V6() V35() V36() V37() ) PartFunc of ,) . (lower_bound A : ( ( non empty closed_interval ) ( non empty V45() V46() V47() compact closed closed_interval bounded_below bounded_above real-bounded interval ) Subset of ( ( ) ( non empty non trivial V60() ) set ) ) ) : ( ( ) ( V22() real ext-real ) Element of REAL : ( ( ) ( non empty non trivial V45() V46() V47() V51() V60() non bounded_below non bounded_above interval ) set ) ) ) : ( ( ) ( V22() real ext-real ) Element of REAL : ( ( ) ( non empty non trivial V45() V46() V47() V51() V60() non bounded_below non bounded_above interval ) set ) ) : ( ( ) ( V22() real ext-real ) Element of REAL : ( ( ) ( non empty non trivial V45() V46() V47() V51() V60() non bounded_below non bounded_above interval ) set ) ) <= upper_sum (((f : ( ( V6() ) ( Relation-like REAL : ( ( ) ( non empty non trivial V45() V46() V47() V51() V60() non bounded_below non bounded_above interval ) set ) -defined REAL : ( ( ) ( non empty non trivial V45() V46() V47() V51() V60() non bounded_below non bounded_above interval ) set ) -valued V6() V35() V36() V37() ) PartFunc of ,) `| X : ( ( ) ( ) set ) ) : ( ( V6() ) ( Relation-like REAL : ( ( ) ( non empty non trivial V45() V46() V47() V51() V60() non bounded_below non bounded_above interval ) set ) -defined REAL : ( ( ) ( non empty non trivial V45() V46() V47() V51() V60() non bounded_below non bounded_above interval ) set ) -valued V6() V35() V36() V37() ) Element of bool [:REAL : ( ( ) ( non empty non trivial V45() V46() V47() V51() V60() non bounded_below non bounded_above interval ) set ) ,REAL : ( ( ) ( non empty non trivial V45() V46() V47() V51() V60() non bounded_below non bounded_above interval ) set ) :] : ( ( ) ( Relation-like non empty non trivial V35() V36() V37() V60() ) set ) : ( ( ) ( non empty non trivial V60() ) set ) ) || A : ( ( non empty closed_interval ) ( non empty V45() V46() V47() compact closed closed_interval bounded_below bounded_above real-bounded interval ) Subset of ( ( ) ( non empty non trivial V60() ) set ) ) ) : ( ( V6() ) ( Relation-like b₁ : ( ( non empty closed_interval ) ( non empty V45() V46() V47() compact closed closed_interval bounded_below bounded_above real-bounded interval ) Subset of ( ( ) ( non empty non trivial V60() ) set ) ) -defined REAL : ( ( ) ( non empty non trivial V45() V46() V47() V51() V60() non bounded_below non bounded_above interval ) set ) -defined REAL : ( ( ) ( non empty non trivial V45() V46() V47() V51() V60() non bounded_below non bounded_above interval ) set ) -valued V6() V35() V36() V37() ) PartFunc of ,) ,D : ( ( ) ( Relation-like NAT : ( ( ) ( non empty non trivial ordinal V45() V46() V47() V48() V49() V50() V51() V60() V80() V81() left_end bounded_below ) Element of bool REAL : ( ( ) ( non empty non trivial V45() V46() V47() V51() V60() non bounded_below non bounded_above interval ) set ) : ( ( ) ( non empty non trivial V60() ) set ) ) -defined REAL : ( ( ) ( non empty non trivial V45() V46() V47() V51() V60() non bounded_below non bounded_above interval ) set ) -valued V6() V7() non empty V35() V36() V37() increasing non-decreasing V60() FinSequence-like FinSubsequence-like ) Division of b₁ : ( ( non empty closed_interval ) ( non empty V45() V46() V47() compact closed closed_interval bounded_below bounded_above real-bounded interval ) Subset of ( ( ) ( non empty non trivial V60() ) set ) ) ) ) : ( ( ) ( V22() real ext-real ) Element of REAL : ( ( ) ( non empty non trivial V45() V46() V47() V51() V60() non bounded_below non bounded_above interval ) set ) ) ) ;

theorem :: INTEGRA5:13

theorem :: INTEGRA5:14

theorem :: INTEGRA5:15

theorem :: INTEGRA5:16

theorem :: INTEGRA5:17

theorem :: INTEGRA5:18

for f being ( ( V6() ) ( Relation-like REAL : ( ( ) ( non empty non trivial V45() V46() V47() V51() V60() non bounded_below non bounded_above interval ) set ) -defined REAL : ( ( ) ( non empty non trivial V45() V46() V47() V51() V60() non bounded_below non bounded_above interval ) set ) -valued V6() V35() V36() V37() ) PartFunc of ,)
for A, B, C being ( ( non empty closed_interval ) ( non empty V45() V46() V47() compact closed closed_interval bounded_below bounded_above real-bounded interval ) Subset of ( ( ) ( non empty non trivial V60() ) set ) )
for X being ( ( ) ( ) set ) st A : ( ( non empty closed_interval ) ( non empty V45() V46() V47() compact closed closed_interval bounded_below bounded_above real-bounded interval ) Subset of ( ( ) ( non empty non trivial V60() ) set ) ) c= X : ( ( ) ( ) set ) & f : ( ( V6() ) ( Relation-like REAL : ( ( ) ( non empty non trivial V45() V46() V47() V51() V60() non bounded_below non bounded_above interval ) set ) -defined REAL : ( ( ) ( non empty non trivial V45() V46() V47() V51() V60() non bounded_below non bounded_above interval ) set ) -valued V6() V35() V36() V37() ) PartFunc of ,) is_differentiable_on X : ( ( ) ( ) set ) & (f : ( ( V6() ) ( Relation-like REAL : ( ( ) ( non empty non trivial V45() V46() V47() V51() V60() non bounded_below non bounded_above interval ) set ) -defined REAL : ( ( ) ( non empty non trivial V45() V46() V47() V51() V60() non bounded_below non bounded_above interval ) set ) -valued V6() V35() V36() V37() ) PartFunc of ,) `| X : ( ( ) ( ) set ) ) : ( ( V6() ) ( Relation-like REAL : ( ( ) ( non empty non trivial V45() V46() V47() V51() V60() non bounded_below non bounded_above interval ) set ) -defined REAL : ( ( ) ( non empty non trivial V45() V46() V47() V51() V60() non bounded_below non bounded_above interval ) set ) -valued V6() V35() V36() V37() ) Element of bool [:REAL : ( ( ) ( non empty non trivial V45() V46() V47() V51() V60() non bounded_below non bounded_above interval ) set ) ,REAL : ( ( ) ( non empty non trivial V45() V46() V47() V51() V60() non bounded_below non bounded_above interval ) set ) :] : ( ( ) ( Relation-like non empty non trivial V35() V36() V37() V60() ) set ) : ( ( ) ( non empty non trivial V60() ) set ) ) | A : ( ( non empty closed_interval ) ( non empty V45() V46() V47() compact closed closed_interval bounded_below bounded_above real-bounded interval ) Subset of ( ( ) ( non empty non trivial V60() ) set ) ) : ( ( V6() ) ( Relation-like b₂ : ( ( non empty closed_interval ) ( non empty V45() V46() V47() compact closed closed_interval bounded_below bounded_above real-bounded interval ) Subset of ( ( ) ( non empty non trivial V60() ) set ) ) -defined REAL : ( ( ) ( non empty non trivial V45() V46() V47() V51() V60() non bounded_below non bounded_above interval ) set ) -defined REAL : ( ( ) ( non empty non trivial V45() V46() V47() V51() V60() non bounded_below non bounded_above interval ) set ) -valued V6() V35() V36() V37() ) Element of bool [:REAL : ( ( ) ( non empty non trivial V45() V46() V47() V51() V60() non bounded_below non bounded_above interval ) set ) ,REAL : ( ( ) ( non empty non trivial V45() V46() V47() V51() V60() non bounded_below non bounded_above interval ) set ) :] : ( ( ) ( Relation-like non empty non trivial V35() V36() V37() V60() ) set ) : ( ( ) ( non empty non trivial V60() ) set ) ) is continuous & lower_bound A : ( ( non empty closed_interval ) ( non empty V45() V46() V47() compact closed closed_interval bounded_below bounded_above real-bounded interval ) Subset of ( ( ) ( non empty non trivial V60() ) set ) ) : ( ( ) ( V22() real ext-real ) Element of REAL : ( ( ) ( non empty non trivial V45() V46() V47() V51() V60() non bounded_below non bounded_above interval ) set ) ) = lower_bound B : ( ( non empty closed_interval ) ( non empty V45() V46() V47() compact closed closed_interval bounded_below bounded_above real-bounded interval ) Subset of ( ( ) ( non empty non trivial V60() ) set ) ) : ( ( ) ( V22() real ext-real ) Element of REAL : ( ( ) ( non empty non trivial V45() V46() V47() V51() V60() non bounded_below non bounded_above interval ) set ) ) & upper_bound B : ( ( non empty closed_interval ) ( non empty V45() V46() V47() compact closed closed_interval bounded_below bounded_above real-bounded interval ) Subset of ( ( ) ( non empty non trivial V60() ) set ) ) : ( ( ) ( V22() real ext-real ) Element of REAL : ( ( ) ( non empty non trivial V45() V46() V47() V51() V60() non bounded_below non bounded_above interval ) set ) ) = lower_bound C : ( ( non empty closed_interval ) ( non empty V45() V46() V47() compact closed closed_interval bounded_below bounded_above real-bounded interval ) Subset of ( ( ) ( non empty non trivial V60() ) set ) ) : ( ( ) ( V22() real ext-real ) Element of REAL : ( ( ) ( non empty non trivial V45() V46() V47() V51() V60() non bounded_below non bounded_above interval ) set ) ) & upper_bound C : ( ( non empty closed_interval ) ( non empty V45() V46() V47() compact closed closed_interval bounded_below bounded_above real-bounded interval ) Subset of ( ( ) ( non empty non trivial V60() ) set ) ) : ( ( ) ( V22() real ext-real ) Element of REAL : ( ( ) ( non empty non trivial V45() V46() V47() V51() V60() non bounded_below non bounded_above interval ) set ) ) = upper_bound A : ( ( non empty closed_interval ) ( non empty V45() V46() V47() compact closed closed_interval bounded_below bounded_above real-bounded interval ) Subset of ( ( ) ( non empty non trivial V60() ) set ) ) : ( ( ) ( V22() real ext-real ) Element of REAL : ( ( ) ( non empty non trivial V45() V46() V47() V51() V60() non bounded_below non bounded_above interval ) set ) ) holds
( B : ( ( non empty closed_interval ) ( non empty V45() V46() V47() compact closed closed_interval bounded_below bounded_above real-bounded interval ) Subset of ( ( ) ( non empty non trivial V60() ) set ) ) c= A : ( ( non empty closed_interval ) ( non empty V45() V46() V47() compact closed closed_interval bounded_below bounded_above real-bounded interval ) Subset of ( ( ) ( non empty non trivial V60() ) set ) ) & C : ( ( non empty closed_interval ) ( non empty V45() V46() V47() compact closed closed_interval bounded_below bounded_above real-bounded interval ) Subset of ( ( ) ( non empty non trivial V60() ) set ) ) c= A : ( ( non empty closed_interval ) ( non empty V45() V46() V47() compact closed closed_interval bounded_below bounded_above real-bounded interval ) Subset of ( ( ) ( non empty non trivial V60() ) set ) ) & integral ((f : ( ( V6() ) ( Relation-like REAL : ( ( ) ( non empty non trivial V45() V46() V47() V51() V60() non bounded_below non bounded_above interval ) set ) -defined REAL : ( ( ) ( non empty non trivial V45() V46() V47() V51() V60() non bounded_below non bounded_above interval ) set ) -valued V6() V35() V36() V37() ) PartFunc of ,) `| X : ( ( ) ( ) set ) ) : ( ( V6() ) ( Relation-like REAL : ( ( ) ( non empty non trivial V45() V46() V47() V51() V60() non bounded_below non bounded_above interval ) set ) -defined REAL : ( ( ) ( non empty non trivial V45() V46() V47() V51() V60() non bounded_below non bounded_above interval ) set ) -valued V6() V35() V36() V37() ) Element of bool [:REAL : ( ( ) ( non empty non trivial V45() V46() V47() V51() V60() non bounded_below non bounded_above interval ) set ) ,REAL : ( ( ) ( non empty non trivial V45() V46() V47() V51() V60() non bounded_below non bounded_above interval ) set ) :] : ( ( ) ( Relation-like non empty non trivial V35() V36() V37() V60() ) set ) : ( ( ) ( non empty non trivial V60() ) set ) ) ,A : ( ( non empty closed_interval ) ( non empty V45() V46() V47() compact closed closed_interval bounded_below bounded_above real-bounded interval ) Subset of ( ( ) ( non empty non trivial V60() ) set ) ) ) : ( ( ) ( V22() real ext-real ) Real) = (integral ((f : ( ( V6() ) ( Relation-like REAL : ( ( ) ( non empty non trivial V45() V46() V47() V51() V60() non bounded_below non bounded_above interval ) set ) -defined REAL : ( ( ) ( non empty non trivial V45() V46() V47() V51() V60() non bounded_below non bounded_above interval ) set ) -valued V6() V35() V36() V37() ) PartFunc of ,) `| X : ( ( ) ( ) set ) ) : ( ( V6() ) ( Relation-like REAL : ( ( ) ( non empty non trivial V45() V46() V47() V51() V60() non bounded_below non bounded_above interval ) set ) -defined REAL : ( ( ) ( non empty non trivial V45() V46() V47() V51() V60() non bounded_below non bounded_above interval ) set ) -valued V6() V35() V36() V37() ) Element of bool [:REAL : ( ( ) ( non empty non trivial V45() V46() V47() V51() V60() non bounded_below non bounded_above interval ) set ) ,REAL : ( ( ) ( non empty non trivial V45() V46() V47() V51() V60() non bounded_below non bounded_above interval ) set ) :] : ( ( ) ( Relation-like non empty non trivial V35() V36() V37() V60() ) set ) : ( ( ) ( non empty non trivial V60() ) set ) ) ,B : ( ( non empty closed_interval ) ( non empty V45() V46() V47() compact closed closed_interval bounded_below bounded_above real-bounded interval ) Subset of ( ( ) ( non empty non trivial V60() ) set ) ) )) : ( ( ) ( V22() real ext-real ) Real) + (integral ((f : ( ( V6() ) ( Relation-like REAL : ( ( ) ( non empty non trivial V45() V46() V47() V51() V60() non bounded_below non bounded_above interval ) set ) -defined REAL : ( ( ) ( non empty non trivial V45() V46() V47() V51() V60() non bounded_below non bounded_above interval ) set ) -valued V6() V35() V36() V37() ) PartFunc of ,) `| X : ( ( ) ( ) set ) ) : ( ( V6() ) ( Relation-like REAL : ( ( ) ( non empty non trivial V45() V46() V47() V51() V60() non bounded_below non bounded_above interval ) set ) -defined REAL : ( ( ) ( non empty non trivial V45() V46() V47() V51() V60() non bounded_below non bounded_above interval ) set ) -valued V6() V35() V36() V37() ) Element of bool [:REAL : ( ( ) ( non empty non trivial V45() V46() V47() V51() V60() non bounded_below non bounded_above interval ) set ) ,REAL : ( ( ) ( non empty non trivial V45() V46() V47() V51() V60() non bounded_below non bounded_above interval ) set ) :] : ( ( ) ( Relation-like non empty non trivial V35() V36() V37() V60() ) set ) : ( ( ) ( non empty non trivial V60() ) set ) ) ,C : ( ( non empty closed_interval ) ( non empty V45() V46() V47() compact closed closed_interval bounded_below bounded_above real-bounded interval ) Subset of ( ( ) ( non empty non trivial V60() ) set ) ) )) : ( ( ) ( V22() real ext-real ) Real) : ( ( ) ( V22() real ext-real ) Element of REAL : ( ( ) ( non empty non trivial V45() V46() V47() V51() V60() non bounded_below non bounded_above interval ) set ) ) ) ;

definition

let a, b be ( ( real ) ( V22() real ext-real ) number ) ;
assume a : ( ( real ) ( V22() real ext-real ) number ) <= b : ( ( real ) ( V22() real ext-real ) number ) ;

func ['a,b'] -> ( ( non empty closed_interval ) ( non empty V45() V46() V47() compact closed closed_interval bounded_below bounded_above real-bounded interval ) Subset of ( ( ) ( non empty non trivial V60() ) set ) ) equals :: INTEGRA5:def 3
[.a : ( ( ext-real ) ( ext-real ) set ) ,b : ( ( ext-real ) ( ext-real ) set ) .] : ( ( ) ( V45() V46() V47() interval ) Element of bool REAL : ( ( ) ( non empty non trivial V45() V46() V47() V51() V60() non bounded_below non bounded_above interval ) set ) : ( ( ) ( non empty non trivial V60() ) set ) ) ;

end;

definition

let a, b be ( ( real ) ( V22() real ext-real ) number ) ;
let f be ( ( V6() ) ( Relation-like REAL : ( ( ) ( non empty non trivial V45() V46() V47() V51() V60() non bounded_below non bounded_above interval ) set ) -defined REAL : ( ( ) ( non empty non trivial V45() V46() V47() V51() V60() non bounded_below non bounded_above interval ) set ) -valued V6() V35() V36() V37() ) PartFunc of ,) ;

func integral (f,a,b) -> ( ( ) ( V22() real ext-real ) Real) equals :: INTEGRA5:def 4
integral (f : ( ( ) ( ) set ) ,['a : ( ( ext-real ) ( ext-real ) set ) ,b : ( ( ext-real ) ( ext-real ) set ) '] : ( ( non empty closed_interval ) ( non empty V45() V46() V47() compact closed closed_interval bounded_below bounded_above real-bounded interval ) Subset of ( ( ) ( non empty non trivial V60() ) set ) ) ) : ( ( ) ( V22() real ext-real ) Real) if a : ( ( ext-real ) ( ext-real ) set ) <= b : ( ( ext-real ) ( ext-real ) set )
otherwise - (integral (f : ( ( ) ( ) set ) ,['b : ( ( ext-real ) ( ext-real ) set ) ,a : ( ( ext-real ) ( ext-real ) set ) '] : ( ( non empty closed_interval ) ( non empty V45() V46() V47() compact closed closed_interval bounded_below bounded_above real-bounded interval ) Subset of ( ( ) ( non empty non trivial V60() ) set ) ) )) : ( ( ) ( V22() real ext-real ) Real) : ( ( ) ( V22() real ext-real ) Element of REAL : ( ( ) ( non empty non trivial V45() V46() V47() V51() V60() non bounded_below non bounded_above interval ) set ) ) ;

end;

theorem :: INTEGRA5:19

theorem :: INTEGRA5:20

theorem :: INTEGRA5:21

for A being ( ( non empty closed_interval ) ( non empty V45() V46() V47() compact closed closed_interval bounded_below bounded_above real-bounded interval ) Subset of ( ( ) ( non empty non trivial V60() ) set ) )
for f, g being ( ( V6() ) ( Relation-like REAL : ( ( ) ( non empty non trivial V45() V46() V47() V51() V60() non bounded_below non bounded_above interval ) set ) -defined REAL : ( ( ) ( non empty non trivial V45() V46() V47() V51() V60() non bounded_below non bounded_above interval ) set ) -valued V6() V35() V36() V37() ) PartFunc of ,)
for X being ( ( open ) ( V45() V46() V47() open ) Subset of ( ( ) ( non empty non trivial V60() ) set ) ) st f : ( ( V6() ) ( Relation-like REAL : ( ( ) ( non empty non trivial V45() V46() V47() V51() V60() non bounded_below non bounded_above interval ) set ) -defined REAL : ( ( ) ( non empty non trivial V45() V46() V47() V51() V60() non bounded_below non bounded_above interval ) set ) -valued V6() V35() V36() V37() ) PartFunc of ,) is_differentiable_on X : ( ( open ) ( V45() V46() V47() open ) Subset of ( ( ) ( non empty non trivial V60() ) set ) ) & g : ( ( V6() ) ( Relation-like REAL : ( ( ) ( non empty non trivial V45() V46() V47() V51() V60() non bounded_below non bounded_above interval ) set ) -defined REAL : ( ( ) ( non empty non trivial V45() V46() V47() V51() V60() non bounded_below non bounded_above interval ) set ) -valued V6() V35() V36() V37() ) PartFunc of ,) is_differentiable_on X : ( ( open ) ( V45() V46() V47() open ) Subset of ( ( ) ( non empty non trivial V60() ) set ) ) & A : ( ( non empty closed_interval ) ( non empty V45() V46() V47() compact closed closed_interval bounded_below bounded_above real-bounded interval ) Subset of ( ( ) ( non empty non trivial V60() ) set ) ) c= X : ( ( open ) ( V45() V46() V47() open ) Subset of ( ( ) ( non empty non trivial V60() ) set ) ) & f : ( ( V6() ) ( Relation-like REAL : ( ( ) ( non empty non trivial V45() V46() V47() V51() V60() non bounded_below non bounded_above interval ) set ) -defined REAL : ( ( ) ( non empty non trivial V45() V46() V47() V51() V60() non bounded_below non bounded_above interval ) set ) -valued V6() V35() V36() V37() ) PartFunc of ,) `| X : ( ( open ) ( V45() V46() V47() open ) Subset of ( ( ) ( non empty non trivial V60() ) set ) ) : ( ( V6() ) ( Relation-like REAL : ( ( ) ( non empty non trivial V45() V46() V47() V51() V60() non bounded_below non bounded_above interval ) set ) -defined REAL : ( ( ) ( non empty non trivial V45() V46() V47() V51() V60() non bounded_below non bounded_above interval ) set ) -valued V6() V35() V36() V37() ) Element of bool [:REAL : ( ( ) ( non empty non trivial V45() V46() V47() V51() V60() non bounded_below non bounded_above interval ) set ) ,REAL : ( ( ) ( non empty non trivial V45() V46() V47() V51() V60() non bounded_below non bounded_above interval ) set ) :] : ( ( ) ( Relation-like non empty non trivial V35() V36() V37() V60() ) set ) : ( ( ) ( non empty non trivial V60() ) set ) ) is_integrable_on A : ( ( non empty closed_interval ) ( non empty V45() V46() V47() compact closed closed_interval bounded_below bounded_above real-bounded interval ) Subset of ( ( ) ( non empty non trivial V60() ) set ) ) & (f : ( ( V6() ) ( Relation-like REAL : ( ( ) ( non empty non trivial V45() V46() V47() V51() V60() non bounded_below non bounded_above interval ) set ) -defined REAL : ( ( ) ( non empty non trivial V45() V46() V47() V51() V60() non bounded_below non bounded_above interval ) set ) -valued V6() V35() V36() V37() ) PartFunc of ,) `| X : ( ( open ) ( V45() V46() V47() open ) Subset of ( ( ) ( non empty non trivial V60() ) set ) ) ) : ( ( V6() ) ( Relation-like REAL : ( ( ) ( non empty non trivial V45() V46() V47() V51() V60() non bounded_below non bounded_above interval ) set ) -defined REAL : ( ( ) ( non empty non trivial V45() V46() V47() V51() V60() non bounded_below non bounded_above interval ) set ) -valued V6() V35() V36() V37() ) Element of bool [:REAL : ( ( ) ( non empty non trivial V45() V46() V47() V51() V60() non bounded_below non bounded_above interval ) set ) ,REAL : ( ( ) ( non empty non trivial V45() V46() V47() V51() V60() non bounded_below non bounded_above interval ) set ) :] : ( ( ) ( Relation-like non empty non trivial V35() V36() V37() V60() ) set ) : ( ( ) ( non empty non trivial V60() ) set ) ) | A : ( ( non empty closed_interval ) ( non empty V45() V46() V47() compact closed closed_interval bounded_below bounded_above real-bounded interval ) Subset of ( ( ) ( non empty non trivial V60() ) set ) ) : ( ( V6() ) ( Relation-like b₁ : ( ( non empty closed_interval ) ( non empty V45() V46() V47() compact closed closed_interval bounded_below bounded_above real-bounded interval ) Subset of ( ( ) ( non empty non trivial V60() ) set ) ) -defined REAL : ( ( ) ( non empty non trivial V45() V46() V47() V51() V60() non bounded_below non bounded_above interval ) set ) -defined REAL : ( ( ) ( non empty non trivial V45() V46() V47() V51() V60() non bounded_below non bounded_above interval ) set ) -valued V6() V35() V36() V37() ) Element of bool [:REAL : ( ( ) ( non empty non trivial V45() V46() V47() V51() V60() non bounded_below non bounded_above interval ) set ) ,REAL : ( ( ) ( non empty non trivial V45() V46() V47() V51() V60() non bounded_below non bounded_above interval ) set ) :] : ( ( ) ( Relation-like non empty non trivial V35() V36() V37() V60() ) set ) : ( ( ) ( non empty non trivial V60() ) set ) ) is bounded & g : ( ( V6() ) ( Relation-like REAL : ( ( ) ( non empty non trivial V45() V46() V47() V51() V60() non bounded_below non bounded_above interval ) set ) -defined REAL : ( ( ) ( non empty non trivial V45() V46() V47() V51() V60() non bounded_below non bounded_above interval ) set ) -valued V6() V35() V36() V37() ) PartFunc of ,) `| X : ( ( open ) ( V45() V46() V47() open ) Subset of ( ( ) ( non empty non trivial V60() ) set ) ) : ( ( V6() ) ( Relation-like REAL : ( ( ) ( non empty non trivial V45() V46() V47() V51() V60() non bounded_below non bounded_above interval ) set ) -defined REAL : ( ( ) ( non empty non trivial V45() V46() V47() V51() V60() non bounded_below non bounded_above interval ) set ) -valued V6() V35() V36() V37() ) Element of bool [:REAL : ( ( ) ( non empty non trivial V45() V46() V47() V51() V60() non bounded_below non bounded_above interval ) set ) ,REAL : ( ( ) ( non empty non trivial V45() V46() V47() V51() V60() non bounded_below non bounded_above interval ) set ) :] : ( ( ) ( Relation-like non empty non trivial V35() V36() V37() V60() ) set ) : ( ( ) ( non empty non trivial V60() ) set ) ) is_integrable_on A : ( ( non empty closed_interval ) ( non empty V45() V46() V47() compact closed closed_interval bounded_below bounded_above real-bounded interval ) Subset of ( ( ) ( non empty non trivial V60() ) set ) ) & (g : ( ( V6() ) ( Relation-like REAL : ( ( ) ( non empty non trivial V45() V46() V47() V51() V60() non bounded_below non bounded_above interval ) set ) -defined REAL : ( ( ) ( non empty non trivial V45() V46() V47() V51() V60() non bounded_below non bounded_above interval ) set ) -valued V6() V35() V36() V37() ) PartFunc of ,) `| X : ( ( open ) ( V45() V46() V47() open ) Subset of ( ( ) ( non empty non trivial V60() ) set ) ) ) : ( ( V6() ) ( Relation-like REAL : ( ( ) ( non empty non trivial V45() V46() V47() V51() V60() non bounded_below non bounded_above interval ) set ) -defined REAL : ( ( ) ( non empty non trivial V45() V46() V47() V51() V60() non bounded_below non bounded_above interval ) set ) -valued V6() V35() V36() V37() ) Element of bool [:REAL : ( ( ) ( non empty non trivial V45() V46() V47() V51() V60() non bounded_below non bounded_above interval ) set ) ,REAL : ( ( ) ( non empty non trivial V45() V46() V47() V51() V60() non bounded_below non bounded_above interval ) set ) :] : ( ( ) ( Relation-like non empty non trivial V35() V36() V37() V60() ) set ) : ( ( ) ( non empty non trivial V60() ) set ) ) | A : ( ( non empty closed_interval ) ( non empty V45() V46() V47() compact closed closed_interval bounded_below bounded_above real-bounded interval ) Subset of ( ( ) ( non empty non trivial V60() ) set ) ) : ( ( V6() ) ( Relation-like b₁ : ( ( non empty closed_interval ) ( non empty V45() V46() V47() compact closed closed_interval bounded_below bounded_above real-bounded interval ) Subset of ( ( ) ( non empty non trivial V60() ) set ) ) -defined REAL : ( ( ) ( non empty non trivial V45() V46() V47() V51() V60() non bounded_below non bounded_above interval ) set ) -defined REAL : ( ( ) ( non empty non trivial V45() V46() V47() V51() V60() non bounded_below non bounded_above interval ) set ) -valued V6() V35() V36() V37() ) Element of bool [:REAL : ( ( ) ( non empty non trivial V45() V46() V47() V51() V60() non bounded_below non bounded_above interval ) set ) ,REAL : ( ( ) ( non empty non trivial V45() V46() V47() V51() V60() non bounded_below non bounded_above interval ) set ) :] : ( ( ) ( Relation-like non empty non trivial V35() V36() V37() V60() ) set ) : ( ( ) ( non empty non trivial V60() ) set ) ) is bounded holds
integral (((f : ( ( V6() ) ( Relation-like REAL : ( ( ) ( non empty non trivial V45() V46() V47() V51() V60() non bounded_below non bounded_above interval ) set ) -defined REAL : ( ( ) ( non empty non trivial V45() V46() V47() V51() V60() non bounded_below non bounded_above interval ) set ) -valued V6() V35() V36() V37() ) PartFunc of ,) `| X : ( ( open ) ( V45() V46() V47() open ) Subset of ( ( ) ( non empty non trivial V60() ) set ) ) ) : ( ( V6() ) ( Relation-like REAL : ( ( ) ( non empty non trivial V45() V46() V47() V51() V60() non bounded_below non bounded_above interval ) set ) -defined REAL : ( ( ) ( non empty non trivial V45() V46() V47() V51() V60() non bounded_below non bounded_above interval ) set ) -valued V6() V35() V36() V37() ) Element of bool [:REAL : ( ( ) ( non empty non trivial V45() V46() V47() V51() V60() non bounded_below non bounded_above interval ) set ) ,REAL : ( ( ) ( non empty non trivial V45() V46() V47() V51() V60() non bounded_below non bounded_above interval ) set ) :] : ( ( ) ( Relation-like non empty non trivial V35() V36() V37() V60() ) set ) : ( ( ) ( non empty non trivial V60() ) set ) ) (#) g : ( ( V6() ) ( Relation-like REAL : ( ( ) ( non empty non trivial V45() V46() V47() V51() V60() non bounded_below non bounded_above interval ) set ) -defined REAL : ( ( ) ( non empty non trivial V45() V46() V47() V51() V60() non bounded_below non bounded_above interval ) set ) -valued V6() V35() V36() V37() ) PartFunc of ,) ) : ( ( V6() ) ( Relation-like REAL : ( ( ) ( non empty non trivial V45() V46() V47() V51() V60() non bounded_below non bounded_above interval ) set ) -defined REAL : ( ( ) ( non empty non trivial V45() V46() V47() V51() V60() non bounded_below non bounded_above interval ) set ) -valued V6() V35() V36() V37() ) Element of bool [:REAL : ( ( ) ( non empty non trivial V45() V46() V47() V51() V60() non bounded_below non bounded_above interval ) set ) ,REAL : ( ( ) ( non empty non trivial V45() V46() V47() V51() V60() non bounded_below non bounded_above interval ) set ) :] : ( ( ) ( Relation-like non empty non trivial V35() V36() V37() V60() ) set ) : ( ( ) ( non empty non trivial V60() ) set ) ) ,A : ( ( non empty closed_interval ) ( non empty V45() V46() V47() compact closed closed_interval bounded_below bounded_above real-bounded interval ) Subset of ( ( ) ( non empty non trivial V60() ) set ) ) ) : ( ( ) ( V22() real ext-real ) Real) = (((f : ( ( V6() ) ( Relation-like REAL : ( ( ) ( non empty non trivial V45() V46() V47() V51() V60() non bounded_below non bounded_above interval ) set ) -defined REAL : ( ( ) ( non empty non trivial V45() V46() V47() V51() V60() non bounded_below non bounded_above interval ) set ) -valued V6() V35() V36() V37() ) PartFunc of ,) . (upper_bound A : ( ( non empty closed_interval ) ( non empty V45() V46() V47() compact closed closed_interval bounded_below bounded_above real-bounded interval ) Subset of ( ( ) ( non empty non trivial V60() ) set ) ) ) : ( ( ) ( V22() real ext-real ) Element of REAL : ( ( ) ( non empty non trivial V45() V46() V47() V51() V60() non bounded_below non bounded_above interval ) set ) ) ) : ( ( ) ( V22() real ext-real ) Element of REAL : ( ( ) ( non empty non trivial V45() V46() V47() V51() V60() non bounded_below non bounded_above interval ) set ) ) * (g : ( ( V6() ) ( Relation-like REAL : ( ( ) ( non empty non trivial V45() V46() V47() V51() V60() non bounded_below non bounded_above interval ) set ) -defined REAL : ( ( ) ( non empty non trivial V45() V46() V47() V51() V60() non bounded_below non bounded_above interval ) set ) -valued V6() V35() V36() V37() ) PartFunc of ,) . (upper_bound A : ( ( non empty closed_interval ) ( non empty V45() V46() V47() compact closed closed_interval bounded_below bounded_above real-bounded interval ) Subset of ( ( ) ( non empty non trivial V60() ) set ) ) ) : ( ( ) ( V22() real ext-real ) Element of REAL : ( ( ) ( non empty non trivial V45() V46() V47() V51() V60() non bounded_below non bounded_above interval ) set ) ) ) : ( ( ) ( V22() real ext-real ) Element of REAL : ( ( ) ( non empty non trivial V45() V46() V47() V51() V60() non bounded_below non bounded_above interval ) set ) ) ) : ( ( ) ( V22() real ext-real ) Element of REAL : ( ( ) ( non empty non trivial V45() V46() V47() V51() V60() non bounded_below non bounded_above interval ) set ) ) - ((f : ( ( V6() ) ( Relation-like REAL : ( ( ) ( non empty non trivial V45() V46() V47() V51() V60() non bounded_below non bounded_above interval ) set ) -defined REAL : ( ( ) ( non empty non trivial V45() V46() V47() V51() V60() non bounded_below non bounded_above interval ) set ) -valued V6() V35() V36() V37() ) PartFunc of ,) . (lower_bound A : ( ( non empty closed_interval ) ( non empty V45() V46() V47() compact closed closed_interval bounded_below bounded_above real-bounded interval ) Subset of ( ( ) ( non empty non trivial V60() ) set ) ) ) : ( ( ) ( V22() real ext-real ) Element of REAL : ( ( ) ( non empty non trivial V45() V46() V47() V51() V60() non bounded_below non bounded_above interval ) set ) ) ) : ( ( ) ( V22() real ext-real ) Element of REAL : ( ( ) ( non empty non trivial V45() V46() V47() V51() V60() non bounded_below non bounded_above interval ) set ) ) * (g : ( ( V6() ) ( Relation-like REAL : ( ( ) ( non empty non trivial V45() V46() V47() V51() V60() non bounded_below non bounded_above interval ) set ) -defined REAL : ( ( ) ( non empty non trivial V45() V46() V47() V51() V60() non bounded_below non bounded_above interval ) set ) -valued V6() V35() V36() V37() ) PartFunc of ,) . (lower_bound A : ( ( non empty closed_interval ) ( non empty V45() V46() V47() compact closed closed_interval bounded_below bounded_above real-bounded interval ) Subset of ( ( ) ( non empty non trivial V60() ) set ) ) ) : ( ( ) ( V22() real ext-real ) Element of REAL : ( ( ) ( non empty non trivial V45() V46() V47() V51() V60() non bounded_below non bounded_above interval ) set ) ) ) : ( ( ) ( V22() real ext-real ) Element of REAL : ( ( ) ( non empty non trivial V45() V46() V47() V51() V60() non bounded_below non bounded_above interval ) set ) ) ) : ( ( ) ( V22() real ext-real ) Element of REAL : ( ( ) ( non empty non trivial V45() V46() V47() V51() V60() non bounded_below non bounded_above interval ) set ) ) ) : ( ( ) ( V22() real ext-real ) Element of REAL : ( ( ) ( non empty non trivial V45() V46() V47() V51() V60() non bounded_below non bounded_above interval ) set ) ) - (integral ((f : ( ( V6() ) ( Relation-like REAL : ( ( ) ( non empty non trivial V45() V46() V47() V51() V60() non bounded_below non bounded_above interval ) set ) -defined REAL : ( ( ) ( non empty non trivial V45() V46() V47() V51() V60() non bounded_below non bounded_above interval ) set ) -valued V6() V35() V36() V37() ) PartFunc of ,) (#) (g : ( ( V6() ) ( Relation-like REAL : ( ( ) ( non empty non trivial V45() V46() V47() V51() V60() non bounded_below non bounded_above interval ) set ) -defined REAL : ( ( ) ( non empty non trivial V45() V46() V47() V51() V60() non bounded_below non bounded_above interval ) set ) -valued V6() V35() V36() V37() ) PartFunc of ,) `| X : ( ( open ) ( V45() V46() V47() open ) Subset of ( ( ) ( non empty non trivial V60() ) set ) ) ) : ( ( V6() ) ( Relation-like REAL : ( ( ) ( non empty non trivial V45() V46() V47() V51() V60() non bounded_below non bounded_above interval ) set ) -defined REAL : ( ( ) ( non empty non trivial V45() V46() V47() V51() V60() non bounded_below non bounded_above interval ) set ) -valued V6() V35() V36() V37() ) Element of bool [:REAL : ( ( ) ( non empty non trivial V45() V46() V47() V51() V60() non bounded_below non bounded_above interval ) set ) ,REAL : ( ( ) ( non empty non trivial V45() V46() V47() V51() V60() non bounded_below non bounded_above interval ) set ) :] : ( ( ) ( Relation-like non empty non trivial V35() V36() V37() V60() ) set ) : ( ( ) ( non empty non trivial V60() ) set ) ) ) : ( ( V6() ) ( Relation-like REAL : ( ( ) ( non empty non trivial V45() V46() V47() V51() V60() non bounded_below non bounded_above interval ) set ) -defined REAL : ( ( ) ( non empty non trivial V45() V46() V47() V51() V60() non bounded_below non bounded_above interval ) set ) -valued V6() V35() V36() V37() ) Element of bool [:REAL : ( ( ) ( non empty non trivial V45() V46() V47() V51() V60() non bounded_below non bounded_above interval ) set ) ,REAL : ( ( ) ( non empty non trivial V45() V46() V47() V51() V60() non bounded_below non bounded_above interval ) set ) :] : ( ( ) ( Relation-like non empty non trivial V35() V36() V37() V60() ) set ) : ( ( ) ( non empty non trivial V60() ) set ) ) ,A : ( ( non empty closed_interval ) ( non empty V45() V46() V47() compact closed closed_interval bounded_below bounded_above real-bounded interval ) Subset of ( ( ) ( non empty non trivial V60() ) set ) ) )) : ( ( ) ( V22() real ext-real ) Real) : ( ( ) ( V22() real ext-real ) Element of REAL : ( ( ) ( non empty non trivial V45() V46() V47() V51() V60() non bounded_below non bounded_above interval ) set ) ) ;