for f1, f2 being ( ( V6() ) ( Relation-like REAL : ( ( ) ( non empty V50() V55() V56() V57() V61() ) set ) -defined REAL : ( ( ) ( non empty V50() V55() V56() V57() V61() ) set ) -valued V6() V34() V35() V36() ) PartFunc of ,)
for Z being ( ( open ) ( V55() V56() V57() open ) Subset of ( ( ) ( ) set ) ) st Z : ( ( open ) ( V55() V56() V57() open ) Subset of ( ( ) ( ) set ) ) c= dom ((f1 : ( ( V6() ) ( Relation-like REAL : ( ( ) ( non empty V50() V55() V56() V57() V61() ) set ) -defined REAL : ( ( ) ( non empty V50() V55() V56() V57() V61() ) set ) -valued V6() V34() V35() V36() ) PartFunc of ,) + f2 : ( ( V6() ) ( Relation-like REAL : ( ( ) ( non empty V50() V55() V56() V57() V61() ) set ) -defined REAL : ( ( ) ( non empty V50() V55() V56() V57() V61() ) set ) -valued V6() V34() V35() V36() ) PartFunc of ,) ) : ( ( V6() ) ( Relation-like REAL : ( ( ) ( non empty V50() V55() V56() V57() V61() ) set ) -defined REAL : ( ( ) ( non empty V50() V55() V56() V57() V61() ) set ) -valued V6() V34() V35() V36() ) Element of K19(K20(REAL : ( ( ) ( non empty V50() V55() V56() V57() V61() ) set ) ,REAL : ( ( ) ( non empty V50() V55() V56() V57() V61() ) set ) ) : ( ( ) ( Relation-like V34() V35() V36() ) set ) ) : ( ( ) ( ) set ) ) ^) : ( ( V6() ) ( Relation-like REAL : ( ( ) ( non empty V50() V55() V56() V57() V61() ) set ) -defined REAL : ( ( ) ( non empty V50() V55() V56() V57() V61() ) set ) -valued V6() V34() V35() V36() ) Element of K19(K20(REAL : ( ( ) ( non empty V50() V55() V56() V57() V61() ) set ) ,REAL : ( ( ) ( non empty V50() V55() V56() V57() V61() ) set ) ) : ( ( ) ( Relation-like V34() V35() V36() ) set ) ) : ( ( ) ( ) set ) ) : ( ( ) ( V55() V56() V57() ) Element of K19(REAL : ( ( ) ( non empty V50() V55() V56() V57() V61() ) set ) ) : ( ( ) ( ) set ) ) & ( for x being ( ( ) ( V28() V29() ext-real ) Real) st x : ( ( ) ( V28() V29() ext-real ) Real) in Z : ( ( open ) ( V55() V56() V57() open ) Subset of ( ( ) ( ) set ) ) holds
f1 : ( ( V6() ) ( Relation-like REAL : ( ( ) ( non empty V50() V55() V56() V57() V61() ) set ) -defined REAL : ( ( ) ( non empty V50() V55() V56() V57() V61() ) set ) -valued V6() V34() V35() V36() ) PartFunc of ,) . x : ( ( ) ( V28() V29() ext-real ) Real) : ( ( ) ( V28() V29() ext-real ) Element of REAL : ( ( ) ( non empty V50() V55() V56() V57() V61() ) set ) ) = 1 : ( ( ) ( non empty V21() V22() V23() V27() V28() V29() V30() ext-real positive non negative V55() V56() V57() V58() V59() V60() V67() ) Element of NAT : ( ( ) ( non empty V21() V22() V23() V55() V56() V57() V58() V59() V60() V61() ) Element of K19(REAL : ( ( ) ( non empty V50() V55() V56() V57() V61() ) set ) ) : ( ( ) ( ) set ) ) ) ) & f2 : ( ( V6() ) ( Relation-like REAL : ( ( ) ( non empty V50() V55() V56() V57() V61() ) set ) -defined REAL : ( ( ) ( non empty V50() V55() V56() V57() V61() ) set ) -valued V6() V34() V35() V36() ) PartFunc of ,) = #Z 2 : ( ( ) ( non empty V21() V22() V23() V27() V28() V29() V30() ext-real positive non negative V55() V56() V57() V58() V59() V60() V67() ) Element of NAT : ( ( ) ( non empty V21() V22() V23() V55() V56() V57() V58() V59() V60() V61() ) Element of K19(REAL : ( ( ) ( non empty V50() V55() V56() V57() V61() ) set ) ) : ( ( ) ( ) set ) ) ) : ( ( V6() V18( REAL : ( ( ) ( non empty V50() V55() V56() V57() V61() ) set ) , REAL : ( ( ) ( non empty V50() V55() V56() V57() V61() ) set ) ) ) ( Relation-like REAL : ( ( ) ( non empty V50() V55() V56() V57() V61() ) set ) -defined REAL : ( ( ) ( non empty V50() V55() V56() V57() V61() ) set ) -valued V6() non empty total V18( REAL : ( ( ) ( non empty V50() V55() V56() V57() V61() ) set ) , REAL : ( ( ) ( non empty V50() V55() V56() V57() V61() ) set ) ) V34() V35() V36() ) Element of K19(K20(REAL : ( ( ) ( non empty V50() V55() V56() V57() V61() ) set ) ,REAL : ( ( ) ( non empty V50() V55() V56() V57() V61() ) set ) ) : ( ( ) ( Relation-like V34() V35() V36() ) set ) ) : ( ( ) ( ) set ) ) holds
( (f1 : ( ( V6() ) ( Relation-like REAL : ( ( ) ( non empty V50() V55() V56() V57() V61() ) set ) -defined REAL : ( ( ) ( non empty V50() V55() V56() V57() V61() ) set ) -valued V6() V34() V35() V36() ) PartFunc of ,) + f2 : ( ( V6() ) ( Relation-like REAL : ( ( ) ( non empty V50() V55() V56() V57() V61() ) set ) -defined REAL : ( ( ) ( non empty V50() V55() V56() V57() V61() ) set ) -valued V6() V34() V35() V36() ) PartFunc of ,) ) : ( ( V6() ) ( Relation-like REAL : ( ( ) ( non empty V50() V55() V56() V57() V61() ) set ) -defined REAL : ( ( ) ( non empty V50() V55() V56() V57() V61() ) set ) -valued V6() V34() V35() V36() ) Element of K19(K20(REAL : ( ( ) ( non empty V50() V55() V56() V57() V61() ) set ) ,REAL : ( ( ) ( non empty V50() V55() V56() V57() V61() ) set ) ) : ( ( ) ( Relation-like V34() V35() V36() ) set ) ) : ( ( ) ( ) set ) ) ^ : ( ( V6() ) ( Relation-like REAL : ( ( ) ( non empty V50() V55() V56() V57() V61() ) set ) -defined REAL : ( ( ) ( non empty V50() V55() V56() V57() V61() ) set ) -valued V6() V34() V35() V36() ) Element of K19(K20(REAL : ( ( ) ( non empty V50() V55() V56() V57() V61() ) set ) ,REAL : ( ( ) ( non empty V50() V55() V56() V57() V61() ) set ) ) : ( ( ) ( Relation-like V34() V35() V36() ) set ) ) : ( ( ) ( ) set ) ) is_differentiable_on Z : ( ( open ) ( V55() V56() V57() open ) Subset of ( ( ) ( ) set ) ) & ( for x being ( ( ) ( V28() V29() ext-real ) Real) st x : ( ( ) ( V28() V29() ext-real ) Real) in Z : ( ( open ) ( V55() V56() V57() open ) Subset of ( ( ) ( ) set ) ) holds
(((f1 : ( ( V6() ) ( Relation-like REAL : ( ( ) ( non empty V50() V55() V56() V57() V61() ) set ) -defined REAL : ( ( ) ( non empty V50() V55() V56() V57() V61() ) set ) -valued V6() V34() V35() V36() ) PartFunc of ,) + f2 : ( ( V6() ) ( Relation-like REAL : ( ( ) ( non empty V50() V55() V56() V57() V61() ) set ) -defined REAL : ( ( ) ( non empty V50() V55() V56() V57() V61() ) set ) -valued V6() V34() V35() V36() ) PartFunc of ,) ) : ( ( V6() ) ( Relation-like REAL : ( ( ) ( non empty V50() V55() V56() V57() V61() ) set ) -defined REAL : ( ( ) ( non empty V50() V55() V56() V57() V61() ) set ) -valued V6() V34() V35() V36() ) Element of K19(K20(REAL : ( ( ) ( non empty V50() V55() V56() V57() V61() ) set ) ,REAL : ( ( ) ( non empty V50() V55() V56() V57() V61() ) set ) ) : ( ( ) ( Relation-like V34() V35() V36() ) set ) ) : ( ( ) ( ) set ) ) ^) : ( ( V6() ) ( Relation-like REAL : ( ( ) ( non empty V50() V55() V56() V57() V61() ) set ) -defined REAL : ( ( ) ( non empty V50() V55() V56() V57() V61() ) set ) -valued V6() V34() V35() V36() ) Element of K19(K20(REAL : ( ( ) ( non empty V50() V55() V56() V57() V61() ) set ) ,REAL : ( ( ) ( non empty V50() V55() V56() V57() V61() ) set ) ) : ( ( ) ( Relation-like V34() V35() V36() ) set ) ) : ( ( ) ( ) set ) ) `| Z : ( ( open ) ( V55() V56() V57() open ) Subset of ( ( ) ( ) set ) ) ) : ( ( V6() ) ( Relation-like REAL : ( ( ) ( non empty V50() V55() V56() V57() V61() ) set ) -defined REAL : ( ( ) ( non empty V50() V55() V56() V57() V61() ) set ) -valued V6() V34() V35() V36() ) Element of K19(K20(REAL : ( ( ) ( non empty V50() V55() V56() V57() V61() ) set ) ,REAL : ( ( ) ( non empty V50() V55() V56() V57() V61() ) set ) ) : ( ( ) ( Relation-like V34() V35() V36() ) set ) ) : ( ( ) ( ) set ) ) . x : ( ( ) ( V28() V29() ext-real ) Real) : ( ( ) ( V28() V29() ext-real ) Element of REAL : ( ( ) ( non empty V50() V55() V56() V57() V61() ) set ) ) = - ((2 : ( ( ) ( non empty V21() V22() V23() V27() V28() V29() V30() ext-real positive non negative V55() V56() V57() V58() V59() V60() V67() ) Element of NAT : ( ( ) ( non empty V21() V22() V23() V55() V56() V57() V58() V59() V60() V61() ) Element of K19(REAL : ( ( ) ( non empty V50() V55() V56() V57() V61() ) set ) ) : ( ( ) ( ) set ) ) ) * x : ( ( ) ( V28() V29() ext-real ) Real) ) : ( ( ) ( V28() V29() ext-real ) Element of REAL : ( ( ) ( non empty V50() V55() V56() V57() V61() ) set ) ) / ((1 : ( ( ) ( non empty V21() V22() V23() V27() V28() V29() V30() ext-real positive non negative V55() V56() V57() V58() V59() V60() V67() ) Element of NAT : ( ( ) ( non empty V21() V22() V23() V55() V56() V57() V58() V59() V60() V61() ) Element of K19(REAL : ( ( ) ( non empty V50() V55() V56() V57() V61() ) set ) ) : ( ( ) ( ) set ) ) ) + (x : ( ( ) ( V28() V29() ext-real ) Real) |^ 2 : ( ( ) ( non empty V21() V22() V23() V27() V28() V29() V30() ext-real positive non negative V55() V56() V57() V58() V59() V60() V67() ) Element of NAT : ( ( ) ( non empty V21() V22() V23() V55() V56() V57() V58() V59() V60() V61() ) Element of K19(REAL : ( ( ) ( non empty V50() V55() V56() V57() V61() ) set ) ) : ( ( ) ( ) set ) ) ) ) : ( ( ) ( V28() V29() ext-real ) Element of REAL : ( ( ) ( non empty V50() V55() V56() V57() V61() ) set ) ) ) : ( ( ) ( V28() V29() ext-real ) Element of REAL : ( ( ) ( non empty V50() V55() V56() V57() V61() ) set ) ) ^2) : ( ( ) ( V28() V29() ext-real ) Element of REAL : ( ( ) ( non empty V50() V55() V56() V57() V61() ) set ) ) ) : ( ( ) ( V28() V29() ext-real ) Element of REAL : ( ( ) ( non empty V50() V55() V56() V57() V61() ) set ) ) : ( ( ) ( V28() V29() ext-real ) Element of REAL : ( ( ) ( non empty V50() V55() V56() V57() V61() ) set ) ) ) ) ;

for A being ( ( non empty closed_interval ) ( non empty V55() V56() V57() closed_interval V86() V87() compact closed ) Subset of ( ( ) ( ) set ) )
for f, g1, g2, f2 being ( ( V6() ) ( Relation-like REAL : ( ( ) ( non empty V50() V55() V56() V57() V61() ) set ) -defined REAL : ( ( ) ( non empty V50() V55() V56() V57() V61() ) set ) -valued V6() V34() V35() V36() ) PartFunc of ,)
for Z being ( ( open ) ( V55() V56() V57() open ) Subset of ( ( ) ( ) set ) ) st A : ( ( non empty closed_interval ) ( non empty V55() V56() V57() closed_interval V86() V87() compact closed ) Subset of ( ( ) ( ) set ) ) c= Z : ( ( open ) ( V55() V56() V57() open ) Subset of ( ( ) ( ) set ) ) & f : ( ( V6() ) ( Relation-like REAL : ( ( ) ( non empty V50() V55() V56() V57() V61() ) set ) -defined REAL : ( ( ) ( non empty V50() V55() V56() V57() V61() ) set ) -valued V6() V34() V35() V36() ) PartFunc of ,) = ((g1 : ( ( V6() ) ( Relation-like REAL : ( ( ) ( non empty V50() V55() V56() V57() V61() ) set ) -defined REAL : ( ( ) ( non empty V50() V55() V56() V57() V61() ) set ) -valued V6() V34() V35() V36() ) PartFunc of ,) + g2 : ( ( V6() ) ( Relation-like REAL : ( ( ) ( non empty V50() V55() V56() V57() V61() ) set ) -defined REAL : ( ( ) ( non empty V50() V55() V56() V57() V61() ) set ) -valued V6() V34() V35() V36() ) PartFunc of ,) ) : ( ( V6() ) ( Relation-like REAL : ( ( ) ( non empty V50() V55() V56() V57() V61() ) set ) -defined REAL : ( ( ) ( non empty V50() V55() V56() V57() V61() ) set ) -valued V6() V34() V35() V36() ) Element of K19(K20(REAL : ( ( ) ( non empty V50() V55() V56() V57() V61() ) set ) ,REAL : ( ( ) ( non empty V50() V55() V56() V57() V61() ) set ) ) : ( ( ) ( Relation-like V34() V35() V36() ) set ) ) : ( ( ) ( ) set ) ) ^) : ( ( V6() ) ( Relation-like REAL : ( ( ) ( non empty V50() V55() V56() V57() V61() ) set ) -defined REAL : ( ( ) ( non empty V50() V55() V56() V57() V61() ) set ) -valued V6() V34() V35() V36() ) Element of K19(K20(REAL : ( ( ) ( non empty V50() V55() V56() V57() V61() ) set ) ,REAL : ( ( ) ( non empty V50() V55() V56() V57() V61() ) set ) ) : ( ( ) ( Relation-like V34() V35() V36() ) set ) ) : ( ( ) ( ) set ) ) / f2 : ( ( V6() ) ( Relation-like REAL : ( ( ) ( non empty V50() V55() V56() V57() V61() ) set ) -defined REAL : ( ( ) ( non empty V50() V55() V56() V57() V61() ) set ) -valued V6() V34() V35() V36() ) PartFunc of ,) : ( ( V6() ) ( Relation-like REAL : ( ( ) ( non empty V50() V55() V56() V57() V61() ) set ) -defined REAL : ( ( ) ( non empty V50() V55() V56() V57() V61() ) set ) -valued V6() V34() V35() V36() ) Element of K19(K20(REAL : ( ( ) ( non empty V50() V55() V56() V57() V61() ) set ) ,REAL : ( ( ) ( non empty V50() V55() V56() V57() V61() ) set ) ) : ( ( ) ( Relation-like V34() V35() V36() ) set ) ) : ( ( ) ( ) set ) ) & f2 : ( ( V6() ) ( Relation-like REAL : ( ( ) ( non empty V50() V55() V56() V57() V61() ) set ) -defined REAL : ( ( ) ( non empty V50() V55() V56() V57() V61() ) set ) -valued V6() V34() V35() V36() ) PartFunc of ,) = arccot : ( ( V6() ) ( Relation-like REAL : ( ( ) ( non empty V50() V55() V56() V57() V61() ) set ) -defined REAL : ( ( ) ( non empty V50() V55() V56() V57() V61() ) set ) -valued V6() V34() V35() V36() ) Element of K19(K20(REAL : ( ( ) ( non empty V50() V55() V56() V57() V61() ) set ) ,REAL : ( ( ) ( non empty V50() V55() V56() V57() V61() ) set ) ) : ( ( ) ( Relation-like V34() V35() V36() ) set ) ) : ( ( ) ( ) set ) ) & Z : ( ( open ) ( V55() V56() V57() open ) Subset of ( ( ) ( ) set ) ) c= ].(- 1 : ( ( ) ( non empty V21() V22() V23() V27() V28() V29() V30() ext-real positive non negative V55() V56() V57() V58() V59() V60() V67() ) Element of NAT : ( ( ) ( non empty V21() V22() V23() V55() V56() V57() V58() V59() V60() V61() ) Element of K19(REAL : ( ( ) ( non empty V50() V55() V56() V57() V61() ) set ) ) : ( ( ) ( ) set ) ) ) ) : ( ( ) ( V28() V29() V30() ext-real non positive V67() ) Element of INT : ( ( ) ( non empty V50() V55() V56() V57() V58() V59() V61() ) set ) ) ,1 : ( ( ) ( non empty V21() V22() V23() V27() V28() V29() V30() ext-real positive non negative V55() V56() V57() V58() V59() V60() V67() ) Element of NAT : ( ( ) ( non empty V21() V22() V23() V55() V56() V57() V58() V59() V60() V61() ) Element of K19(REAL : ( ( ) ( non empty V50() V55() V56() V57() V61() ) set ) ) : ( ( ) ( ) set ) ) ) .[ : ( ( ) ( V55() V56() V57() open ) Element of K19(REAL : ( ( ) ( non empty V50() V55() V56() V57() V61() ) set ) ) : ( ( ) ( ) set ) ) & g2 : ( ( V6() ) ( Relation-like REAL : ( ( ) ( non empty V50() V55() V56() V57() V61() ) set ) -defined REAL : ( ( ) ( non empty V50() V55() V56() V57() V61() ) set ) -valued V6() V34() V35() V36() ) PartFunc of ,) = #Z 2 : ( ( ) ( non empty V21() V22() V23() V27() V28() V29() V30() ext-real positive non negative V55() V56() V57() V58() V59() V60() V67() ) Element of NAT : ( ( ) ( non empty V21() V22() V23() V55() V56() V57() V58() V59() V60() V61() ) Element of K19(REAL : ( ( ) ( non empty V50() V55() V56() V57() V61() ) set ) ) : ( ( ) ( ) set ) ) ) : ( ( V6() V18( REAL : ( ( ) ( non empty V50() V55() V56() V57() V61() ) set ) , REAL : ( ( ) ( non empty V50() V55() V56() V57() V61() ) set ) ) ) ( Relation-like REAL : ( ( ) ( non empty V50() V55() V56() V57() V61() ) set ) -defined REAL : ( ( ) ( non empty V50() V55() V56() V57() V61() ) set ) -valued V6() non empty total V18( REAL : ( ( ) ( non empty V50() V55() V56() V57() V61() ) set ) , REAL : ( ( ) ( non empty V50() V55() V56() V57() V61() ) set ) ) V34() V35() V36() ) Element of K19(K20(REAL : ( ( ) ( non empty V50() V55() V56() V57() V61() ) set ) ,REAL : ( ( ) ( non empty V50() V55() V56() V57() V61() ) set ) ) : ( ( ) ( Relation-like V34() V35() V36() ) set ) ) : ( ( ) ( ) set ) ) & ( for x being ( ( ) ( V28() V29() ext-real ) Real) st x : ( ( ) ( V28() V29() ext-real ) Real) in Z : ( ( open ) ( V55() V56() V57() open ) Subset of ( ( ) ( ) set ) ) holds
( g1 : ( ( V6() ) ( Relation-like REAL : ( ( ) ( non empty V50() V55() V56() V57() V61() ) set ) -defined REAL : ( ( ) ( non empty V50() V55() V56() V57() V61() ) set ) -valued V6() V34() V35() V36() ) PartFunc of ,) . x : ( ( ) ( V28() V29() ext-real ) Real) : ( ( ) ( V28() V29() ext-real ) Element of REAL : ( ( ) ( non empty V50() V55() V56() V57() V61() ) set ) ) = 1 : ( ( ) ( non empty V21() V22() V23() V27() V28() V29() V30() ext-real positive non negative V55() V56() V57() V58() V59() V60() V67() ) Element of NAT : ( ( ) ( non empty V21() V22() V23() V55() V56() V57() V58() V59() V60() V61() ) Element of K19(REAL : ( ( ) ( non empty V50() V55() V56() V57() V61() ) set ) ) : ( ( ) ( ) set ) ) ) & f2 : ( ( V6() ) ( Relation-like REAL : ( ( ) ( non empty V50() V55() V56() V57() V61() ) set ) -defined REAL : ( ( ) ( non empty V50() V55() V56() V57() V61() ) set ) -valued V6() V34() V35() V36() ) PartFunc of ,) . x : ( ( ) ( V28() V29() ext-real ) Real) : ( ( ) ( V28() V29() ext-real ) Element of REAL : ( ( ) ( non empty V50() V55() V56() V57() V61() ) set ) ) > 0 : ( ( ) ( Relation-like non-empty empty-yielding RAT : ( ( ) ( non empty V50() V55() V56() V57() V58() V61() ) set ) -valued V6() V7() V8() V9() empty V21() V22() V23() V25() V26() V27() V28() V29() V30() ext-real non positive non negative V34() V35() V36() V37() V55() V56() V57() V58() V59() V60() V61() V67() bounded ) Element of NAT : ( ( ) ( non empty V21() V22() V23() V55() V56() V57() V58() V59() V60() V61() ) Element of K19(REAL : ( ( ) ( non empty V50() V55() V56() V57() V61() ) set ) ) : ( ( ) ( ) set ) ) ) ) ) & Z : ( ( open ) ( V55() V56() V57() open ) Subset of ( ( ) ( ) set ) ) = dom f : ( ( V6() ) ( Relation-like REAL : ( ( ) ( non empty V50() V55() V56() V57() V61() ) set ) -defined REAL : ( ( ) ( non empty V50() V55() V56() V57() V61() ) set ) -valued V6() V34() V35() V36() ) PartFunc of ,) : ( ( ) ( V55() V56() V57() ) Element of K19(REAL : ( ( ) ( non empty V50() V55() V56() V57() V61() ) set ) ) : ( ( ) ( ) set ) ) holds
integral (f : ( ( V6() ) ( Relation-like REAL : ( ( ) ( non empty V50() V55() V56() V57() V61() ) set ) -defined REAL : ( ( ) ( non empty V50() V55() V56() V57() V61() ) set ) -valued V6() V34() V35() V36() ) PartFunc of ,) ,A : ( ( non empty closed_interval ) ( non empty V55() V56() V57() closed_interval V86() V87() compact closed ) Subset of ( ( ) ( ) set ) ) ) : ( ( ) ( V28() V29() ext-real ) Element of REAL : ( ( ) ( non empty V50() V55() V56() V57() V61() ) set ) ) = ((- (ln : ( ( V6() ) ( Relation-like REAL : ( ( ) ( non empty V50() V55() V56() V57() V61() ) set ) -defined REAL : ( ( ) ( non empty V50() V55() V56() V57() V61() ) set ) -valued V6() V34() V35() V36() ) Element of K19(K20(REAL : ( ( ) ( non empty V50() V55() V56() V57() V61() ) set ) ,REAL : ( ( ) ( non empty V50() V55() V56() V57() V61() ) set ) ) : ( ( ) ( Relation-like V34() V35() V36() ) set ) ) : ( ( ) ( ) set ) ) * arccot : ( ( V6() ) ( Relation-like REAL : ( ( ) ( non empty V50() V55() V56() V57() V61() ) set ) -defined REAL : ( ( ) ( non empty V50() V55() V56() V57() V61() ) set ) -valued V6() V34() V35() V36() ) Element of K19(K20(REAL : ( ( ) ( non empty V50() V55() V56() V57() V61() ) set ) ,REAL : ( ( ) ( non empty V50() V55() V56() V57() V61() ) set ) ) : ( ( ) ( Relation-like V34() V35() V36() ) set ) ) : ( ( ) ( ) set ) ) ) : ( ( V6() ) ( Relation-like REAL : ( ( ) ( non empty V50() V55() V56() V57() V61() ) set ) -defined REAL : ( ( ) ( non empty V50() V55() V56() V57() V61() ) set ) -valued V6() V34() V35() V36() ) Element of K19(K20(REAL : ( ( ) ( non empty V50() V55() V56() V57() V61() ) set ) ,REAL : ( ( ) ( non empty V50() V55() V56() V57() V61() ) set ) ) : ( ( ) ( Relation-like V34() V35() V36() ) set ) ) : ( ( ) ( ) set ) ) ) : ( ( V6() ) ( Relation-like REAL : ( ( ) ( non empty V50() V55() V56() V57() V61() ) set ) -defined REAL : ( ( ) ( non empty V50() V55() V56() V57() V61() ) set ) -valued V6() V34() V35() V36() ) Element of K19(K20(REAL : ( ( ) ( non empty V50() V55() V56() V57() V61() ) set ) ,REAL : ( ( ) ( non empty V50() V55() V56() V57() V61() ) set ) ) : ( ( ) ( Relation-like V34() V35() V36() ) set ) ) : ( ( ) ( ) set ) ) . (upper_bound A : ( ( non empty closed_interval ) ( non empty V55() V56() V57() closed_interval V86() V87() compact closed ) Subset of ( ( ) ( ) set ) ) ) : ( ( ) ( V28() V29() ext-real ) Element of REAL : ( ( ) ( non empty V50() V55() V56() V57() V61() ) set ) ) ) : ( ( ) ( V28() V29() ext-real ) Element of REAL : ( ( ) ( non empty V50() V55() V56() V57() V61() ) set ) ) - ((- (ln : ( ( V6() ) ( Relation-like REAL : ( ( ) ( non empty V50() V55() V56() V57() V61() ) set ) -defined REAL : ( ( ) ( non empty V50() V55() V56() V57() V61() ) set ) -valued V6() V34() V35() V36() ) Element of K19(K20(REAL : ( ( ) ( non empty V50() V55() V56() V57() V61() ) set ) ,REAL : ( ( ) ( non empty V50() V55() V56() V57() V61() ) set ) ) : ( ( ) ( Relation-like V34() V35() V36() ) set ) ) : ( ( ) ( ) set ) ) * arccot : ( ( V6() ) ( Relation-like REAL : ( ( ) ( non empty V50() V55() V56() V57() V61() ) set ) -defined REAL : ( ( ) ( non empty V50() V55() V56() V57() V61() ) set ) -valued V6() V34() V35() V36() ) Element of K19(K20(REAL : ( ( ) ( non empty V50() V55() V56() V57() V61() ) set ) ,REAL : ( ( ) ( non empty V50() V55() V56() V57() V61() ) set ) ) : ( ( ) ( Relation-like V34() V35() V36() ) set ) ) : ( ( ) ( ) set ) ) ) : ( ( V6() ) ( Relation-like REAL : ( ( ) ( non empty V50() V55() V56() V57() V61() ) set ) -defined REAL : ( ( ) ( non empty V50() V55() V56() V57() V61() ) set ) -valued V6() V34() V35() V36() ) Element of K19(K20(REAL : ( ( ) ( non empty V50() V55() V56() V57() V61() ) set ) ,REAL : ( ( ) ( non empty V50() V55() V56() V57() V61() ) set ) ) : ( ( ) ( Relation-like V34() V35() V36() ) set ) ) : ( ( ) ( ) set ) ) ) : ( ( V6() ) ( Relation-like REAL : ( ( ) ( non empty V50() V55() V56() V57() V61() ) set ) -defined REAL : ( ( ) ( non empty V50() V55() V56() V57() V61() ) set ) -valued V6() V34() V35() V36() ) Element of K19(K20(REAL : ( ( ) ( non empty V50() V55() V56() V57() V61() ) set ) ,REAL : ( ( ) ( non empty V50() V55() V56() V57() V61() ) set ) ) : ( ( ) ( Relation-like V34() V35() V36() ) set ) ) : ( ( ) ( ) set ) ) . (lower_bound A : ( ( non empty closed_interval ) ( non empty V55() V56() V57() closed_interval V86() V87() compact closed ) Subset of ( ( ) ( ) set ) ) ) : ( ( ) ( V28() V29() ext-real ) Element of REAL : ( ( ) ( non empty V50() V55() V56() V57() V61() ) set ) ) ) : ( ( ) ( V28() V29() ext-real ) Element of REAL : ( ( ) ( non empty V50() V55() V56() V57() V61() ) set ) ) : ( ( ) ( V28() V29() ext-real ) Element of REAL : ( ( ) ( non empty V50() V55() V56() V57() V61() ) set ) ) ;

for A being ( ( non empty closed_interval ) ( non empty V55() V56() V57() closed_interval V86() V87() compact closed ) Subset of ( ( ) ( ) set ) )
for f1, f being ( ( V6() ) ( Relation-like REAL : ( ( ) ( non empty V50() V55() V56() V57() V61() ) set ) -defined REAL : ( ( ) ( non empty V50() V55() V56() V57() V61() ) set ) -valued V6() V34() V35() V36() ) PartFunc of ,)
for Z being ( ( open ) ( V55() V56() V57() open ) Subset of ( ( ) ( ) set ) ) st A : ( ( non empty closed_interval ) ( non empty V55() V56() V57() closed_interval V86() V87() compact closed ) Subset of ( ( ) ( ) set ) ) c= Z : ( ( open ) ( V55() V56() V57() open ) Subset of ( ( ) ( ) set ) ) & ( for x being ( ( ) ( V28() V29() ext-real ) Real) st x : ( ( ) ( V28() V29() ext-real ) Real) in Z : ( ( open ) ( V55() V56() V57() open ) Subset of ( ( ) ( ) set ) ) holds
( exp_R : ( ( V6() V18( REAL : ( ( ) ( non empty V50() V55() V56() V57() V61() ) set ) , REAL : ( ( ) ( non empty V50() V55() V56() V57() V61() ) set ) ) ) ( Relation-like REAL : ( ( ) ( non empty V50() V55() V56() V57() V61() ) set ) -defined REAL : ( ( ) ( non empty V50() V55() V56() V57() V61() ) set ) -valued V6() non empty total V18( REAL : ( ( ) ( non empty V50() V55() V56() V57() V61() ) set ) , REAL : ( ( ) ( non empty V50() V55() V56() V57() V61() ) set ) ) V34() V35() V36() ) Element of K19(K20(REAL : ( ( ) ( non empty V50() V55() V56() V57() V61() ) set ) ,REAL : ( ( ) ( non empty V50() V55() V56() V57() V61() ) set ) ) : ( ( ) ( Relation-like V34() V35() V36() ) set ) ) : ( ( ) ( ) set ) ) . x : ( ( ) ( V28() V29() ext-real ) Real) : ( ( ) ( V28() V29() ext-real ) Element of REAL : ( ( ) ( non empty V50() V55() V56() V57() V61() ) set ) ) < 1 : ( ( ) ( non empty V21() V22() V23() V27() V28() V29() V30() ext-real positive non negative V55() V56() V57() V58() V59() V60() V67() ) Element of NAT : ( ( ) ( non empty V21() V22() V23() V55() V56() V57() V58() V59() V60() V61() ) Element of K19(REAL : ( ( ) ( non empty V50() V55() V56() V57() V61() ) set ) ) : ( ( ) ( ) set ) ) ) & f1 : ( ( V6() ) ( Relation-like REAL : ( ( ) ( non empty V50() V55() V56() V57() V61() ) set ) -defined REAL : ( ( ) ( non empty V50() V55() V56() V57() V61() ) set ) -valued V6() V34() V35() V36() ) PartFunc of ,) . x : ( ( ) ( V28() V29() ext-real ) Real) : ( ( ) ( V28() V29() ext-real ) Element of REAL : ( ( ) ( non empty V50() V55() V56() V57() V61() ) set ) ) = 1 : ( ( ) ( non empty V21() V22() V23() V27() V28() V29() V30() ext-real positive non negative V55() V56() V57() V58() V59() V60() V67() ) Element of NAT : ( ( ) ( non empty V21() V22() V23() V55() V56() V57() V58() V59() V60() V61() ) Element of K19(REAL : ( ( ) ( non empty V50() V55() V56() V57() V61() ) set ) ) : ( ( ) ( ) set ) ) ) ) ) & Z : ( ( open ) ( V55() V56() V57() open ) Subset of ( ( ) ( ) set ) ) c= dom (arctan : ( ( V6() ) ( Relation-like REAL : ( ( ) ( non empty V50() V55() V56() V57() V61() ) set ) -defined REAL : ( ( ) ( non empty V50() V55() V56() V57() V61() ) set ) -valued V6() V34() V35() V36() ) Element of K19(K20(REAL : ( ( ) ( non empty V50() V55() V56() V57() V61() ) set ) ,REAL : ( ( ) ( non empty V50() V55() V56() V57() V61() ) set ) ) : ( ( ) ( Relation-like V34() V35() V36() ) set ) ) : ( ( ) ( ) set ) ) * exp_R : ( ( V6() V18( REAL : ( ( ) ( non empty V50() V55() V56() V57() V61() ) set ) , REAL : ( ( ) ( non empty V50() V55() V56() V57() V61() ) set ) ) ) ( Relation-like REAL : ( ( ) ( non empty V50() V55() V56() V57() V61() ) set ) -defined REAL : ( ( ) ( non empty V50() V55() V56() V57() V61() ) set ) -valued V6() non empty total V18( REAL : ( ( ) ( non empty V50() V55() V56() V57() V61() ) set ) , REAL : ( ( ) ( non empty V50() V55() V56() V57() V61() ) set ) ) V34() V35() V36() ) Element of K19(K20(REAL : ( ( ) ( non empty V50() V55() V56() V57() V61() ) set ) ,REAL : ( ( ) ( non empty V50() V55() V56() V57() V61() ) set ) ) : ( ( ) ( Relation-like V34() V35() V36() ) set ) ) : ( ( ) ( ) set ) ) ) : ( ( V6() ) ( Relation-like REAL : ( ( ) ( non empty V50() V55() V56() V57() V61() ) set ) -defined REAL : ( ( ) ( non empty V50() V55() V56() V57() V61() ) set ) -valued V6() V34() V35() V36() ) Element of K19(K20(REAL : ( ( ) ( non empty V50() V55() V56() V57() V61() ) set ) ,REAL : ( ( ) ( non empty V50() V55() V56() V57() V61() ) set ) ) : ( ( ) ( Relation-like V34() V35() V36() ) set ) ) : ( ( ) ( ) set ) ) : ( ( ) ( V55() V56() V57() ) Element of K19(REAL : ( ( ) ( non empty V50() V55() V56() V57() V61() ) set ) ) : ( ( ) ( ) set ) ) & Z : ( ( open ) ( V55() V56() V57() open ) Subset of ( ( ) ( ) set ) ) = dom f : ( ( V6() ) ( Relation-like REAL : ( ( ) ( non empty V50() V55() V56() V57() V61() ) set ) -defined REAL : ( ( ) ( non empty V50() V55() V56() V57() V61() ) set ) -valued V6() V34() V35() V36() ) PartFunc of ,) : ( ( ) ( V55() V56() V57() ) Element of K19(REAL : ( ( ) ( non empty V50() V55() V56() V57() V61() ) set ) ) : ( ( ) ( ) set ) ) & f : ( ( V6() ) ( Relation-like REAL : ( ( ) ( non empty V50() V55() V56() V57() V61() ) set ) -defined REAL : ( ( ) ( non empty V50() V55() V56() V57() V61() ) set ) -valued V6() V34() V35() V36() ) PartFunc of ,) = exp_R : ( ( V6() V18( REAL : ( ( ) ( non empty V50() V55() V56() V57() V61() ) set ) , REAL : ( ( ) ( non empty V50() V55() V56() V57() V61() ) set ) ) ) ( Relation-like REAL : ( ( ) ( non empty V50() V55() V56() V57() V61() ) set ) -defined REAL : ( ( ) ( non empty V50() V55() V56() V57() V61() ) set ) -valued V6() non empty total V18( REAL : ( ( ) ( non empty V50() V55() V56() V57() V61() ) set ) , REAL : ( ( ) ( non empty V50() V55() V56() V57() V61() ) set ) ) V34() V35() V36() ) Element of K19(K20(REAL : ( ( ) ( non empty V50() V55() V56() V57() V61() ) set ) ,REAL : ( ( ) ( non empty V50() V55() V56() V57() V61() ) set ) ) : ( ( ) ( Relation-like V34() V35() V36() ) set ) ) : ( ( ) ( ) set ) ) / (f1 : ( ( V6() ) ( Relation-like REAL : ( ( ) ( non empty V50() V55() V56() V57() V61() ) set ) -defined REAL : ( ( ) ( non empty V50() V55() V56() V57() V61() ) set ) -valued V6() V34() V35() V36() ) PartFunc of ,) + (exp_R : ( ( V6() V18( REAL : ( ( ) ( non empty V50() V55() V56() V57() V61() ) set ) , REAL : ( ( ) ( non empty V50() V55() V56() V57() V61() ) set ) ) ) ( Relation-like REAL : ( ( ) ( non empty V50() V55() V56() V57() V61() ) set ) -defined REAL : ( ( ) ( non empty V50() V55() V56() V57() V61() ) set ) -valued V6() non empty total V18( REAL : ( ( ) ( non empty V50() V55() V56() V57() V61() ) set ) , REAL : ( ( ) ( non empty V50() V55() V56() V57() V61() ) set ) ) V34() V35() V36() ) Element of K19(K20(REAL : ( ( ) ( non empty V50() V55() V56() V57() V61() ) set ) ,REAL : ( ( ) ( non empty V50() V55() V56() V57() V61() ) set ) ) : ( ( ) ( Relation-like V34() V35() V36() ) set ) ) : ( ( ) ( ) set ) ) ^2) : ( ( V6() ) ( Relation-like REAL : ( ( ) ( non empty V50() V55() V56() V57() V61() ) set ) -defined REAL : ( ( ) ( non empty V50() V55() V56() V57() V61() ) set ) -valued V6() non empty total V18( REAL : ( ( ) ( non empty V50() V55() V56() V57() V61() ) set ) , REAL : ( ( ) ( non empty V50() V55() V56() V57() V61() ) set ) ) V34() V35() V36() ) Element of K19(K20(REAL : ( ( ) ( non empty V50() V55() V56() V57() V61() ) set ) ,REAL : ( ( ) ( non empty V50() V55() V56() V57() V61() ) set ) ) : ( ( ) ( Relation-like V34() V35() V36() ) set ) ) : ( ( ) ( ) set ) ) ) : ( ( V6() ) ( Relation-like REAL : ( ( ) ( non empty V50() V55() V56() V57() V61() ) set ) -defined REAL : ( ( ) ( non empty V50() V55() V56() V57() V61() ) set ) -valued V6() V34() V35() V36() ) Element of K19(K20(REAL : ( ( ) ( non empty V50() V55() V56() V57() V61() ) set ) ,REAL : ( ( ) ( non empty V50() V55() V56() V57() V61() ) set ) ) : ( ( ) ( Relation-like V34() V35() V36() ) set ) ) : ( ( ) ( ) set ) ) : ( ( V6() ) ( Relation-like REAL : ( ( ) ( non empty V50() V55() V56() V57() V61() ) set ) -defined REAL : ( ( ) ( non empty V50() V55() V56() V57() V61() ) set ) -valued V6() V34() V35() V36() ) Element of K19(K20(REAL : ( ( ) ( non empty V50() V55() V56() V57() V61() ) set ) ,REAL : ( ( ) ( non empty V50() V55() V56() V57() V61() ) set ) ) : ( ( ) ( Relation-like V34() V35() V36() ) set ) ) : ( ( ) ( ) set ) ) holds
integral (f : ( ( V6() ) ( Relation-like REAL : ( ( ) ( non empty V50() V55() V56() V57() V61() ) set ) -defined REAL : ( ( ) ( non empty V50() V55() V56() V57() V61() ) set ) -valued V6() V34() V35() V36() ) PartFunc of ,) ,A : ( ( non empty closed_interval ) ( non empty V55() V56() V57() closed_interval V86() V87() compact closed ) Subset of ( ( ) ( ) set ) ) ) : ( ( ) ( V28() V29() ext-real ) Element of REAL : ( ( ) ( non empty V50() V55() V56() V57() V61() ) set ) ) = ((arctan : ( ( V6() ) ( Relation-like REAL : ( ( ) ( non empty V50() V55() V56() V57() V61() ) set ) -defined REAL : ( ( ) ( non empty V50() V55() V56() V57() V61() ) set ) -valued V6() V34() V35() V36() ) Element of K19(K20(REAL : ( ( ) ( non empty V50() V55() V56() V57() V61() ) set ) ,REAL : ( ( ) ( non empty V50() V55() V56() V57() V61() ) set ) ) : ( ( ) ( Relation-like V34() V35() V36() ) set ) ) : ( ( ) ( ) set ) ) * exp_R : ( ( V6() V18( REAL : ( ( ) ( non empty V50() V55() V56() V57() V61() ) set ) , REAL : ( ( ) ( non empty V50() V55() V56() V57() V61() ) set ) ) ) ( Relation-like REAL : ( ( ) ( non empty V50() V55() V56() V57() V61() ) set ) -defined REAL : ( ( ) ( non empty V50() V55() V56() V57() V61() ) set ) -valued V6() non empty total V18( REAL : ( ( ) ( non empty V50() V55() V56() V57() V61() ) set ) , REAL : ( ( ) ( non empty V50() V55() V56() V57() V61() ) set ) ) V34() V35() V36() ) Element of K19(K20(REAL : ( ( ) ( non empty V50() V55() V56() V57() V61() ) set ) ,REAL : ( ( ) ( non empty V50() V55() V56() V57() V61() ) set ) ) : ( ( ) ( Relation-like V34() V35() V36() ) set ) ) : ( ( ) ( ) set ) ) ) : ( ( V6() ) ( Relation-like REAL : ( ( ) ( non empty V50() V55() V56() V57() V61() ) set ) -defined REAL : ( ( ) ( non empty V50() V55() V56() V57() V61() ) set ) -valued V6() V34() V35() V36() ) Element of K19(K20(REAL : ( ( ) ( non empty V50() V55() V56() V57() V61() ) set ) ,REAL : ( ( ) ( non empty V50() V55() V56() V57() V61() ) set ) ) : ( ( ) ( Relation-like V34() V35() V36() ) set ) ) : ( ( ) ( ) set ) ) . (upper_bound A : ( ( non empty closed_interval ) ( non empty V55() V56() V57() closed_interval V86() V87() compact closed ) Subset of ( ( ) ( ) set ) ) ) : ( ( ) ( V28() V29() ext-real ) Element of REAL : ( ( ) ( non empty V50() V55() V56() V57() V61() ) set ) ) ) : ( ( ) ( V28() V29() ext-real ) Element of REAL : ( ( ) ( non empty V50() V55() V56() V57() V61() ) set ) ) - ((arctan : ( ( V6() ) ( Relation-like REAL : ( ( ) ( non empty V50() V55() V56() V57() V61() ) set ) -defined REAL : ( ( ) ( non empty V50() V55() V56() V57() V61() ) set ) -valued V6() V34() V35() V36() ) Element of K19(K20(REAL : ( ( ) ( non empty V50() V55() V56() V57() V61() ) set ) ,REAL : ( ( ) ( non empty V50() V55() V56() V57() V61() ) set ) ) : ( ( ) ( Relation-like V34() V35() V36() ) set ) ) : ( ( ) ( ) set ) ) * exp_R : ( ( V6() V18( REAL : ( ( ) ( non empty V50() V55() V56() V57() V61() ) set ) , REAL : ( ( ) ( non empty V50() V55() V56() V57() V61() ) set ) ) ) ( Relation-like REAL : ( ( ) ( non empty V50() V55() V56() V57() V61() ) set ) -defined REAL : ( ( ) ( non empty V50() V55() V56() V57() V61() ) set ) -valued V6() non empty total V18( REAL : ( ( ) ( non empty V50() V55() V56() V57() V61() ) set ) , REAL : ( ( ) ( non empty V50() V55() V56() V57() V61() ) set ) ) V34() V35() V36() ) Element of K19(K20(REAL : ( ( ) ( non empty V50() V55() V56() V57() V61() ) set ) ,REAL : ( ( ) ( non empty V50() V55() V56() V57() V61() ) set ) ) : ( ( ) ( Relation-like V34() V35() V36() ) set ) ) : ( ( ) ( ) set ) ) ) : ( ( V6() ) ( Relation-like REAL : ( ( ) ( non empty V50() V55() V56() V57() V61() ) set ) -defined REAL : ( ( ) ( non empty V50() V55() V56() V57() V61() ) set ) -valued V6() V34() V35() V36() ) Element of K19(K20(REAL : ( ( ) ( non empty V50() V55() V56() V57() V61() ) set ) ,REAL : ( ( ) ( non empty V50() V55() V56() V57() V61() ) set ) ) : ( ( ) ( Relation-like V34() V35() V36() ) set ) ) : ( ( ) ( ) set ) ) . (lower_bound A : ( ( non empty closed_interval ) ( non empty V55() V56() V57() closed_interval V86() V87() compact closed ) Subset of ( ( ) ( ) set ) ) ) : ( ( ) ( V28() V29() ext-real ) Element of REAL : ( ( ) ( non empty V50() V55() V56() V57() V61() ) set ) ) ) : ( ( ) ( V28() V29() ext-real ) Element of REAL : ( ( ) ( non empty V50() V55() V56() V57() V61() ) set ) ) : ( ( ) ( V28() V29() ext-real ) Element of REAL : ( ( ) ( non empty V50() V55() V56() V57() V61() ) set ) ) ;

for A being ( ( non empty closed_interval ) ( non empty V55() V56() V57() closed_interval V86() V87() compact closed ) Subset of ( ( ) ( ) set ) )
for f1, f being ( ( V6() ) ( Relation-like REAL : ( ( ) ( non empty V50() V55() V56() V57() V61() ) set ) -defined REAL : ( ( ) ( non empty V50() V55() V56() V57() V61() ) set ) -valued V6() V34() V35() V36() ) PartFunc of ,)
for Z being ( ( open ) ( V55() V56() V57() open ) Subset of ( ( ) ( ) set ) ) st A : ( ( non empty closed_interval ) ( non empty V55() V56() V57() closed_interval V86() V87() compact closed ) Subset of ( ( ) ( ) set ) ) c= Z : ( ( open ) ( V55() V56() V57() open ) Subset of ( ( ) ( ) set ) ) & ( for x being ( ( ) ( V28() V29() ext-real ) Real) st x : ( ( ) ( V28() V29() ext-real ) Real) in Z : ( ( open ) ( V55() V56() V57() open ) Subset of ( ( ) ( ) set ) ) holds
( exp_R : ( ( V6() V18( REAL : ( ( ) ( non empty V50() V55() V56() V57() V61() ) set ) , REAL : ( ( ) ( non empty V50() V55() V56() V57() V61() ) set ) ) ) ( Relation-like REAL : ( ( ) ( non empty V50() V55() V56() V57() V61() ) set ) -defined REAL : ( ( ) ( non empty V50() V55() V56() V57() V61() ) set ) -valued V6() non empty total V18( REAL : ( ( ) ( non empty V50() V55() V56() V57() V61() ) set ) , REAL : ( ( ) ( non empty V50() V55() V56() V57() V61() ) set ) ) V34() V35() V36() ) Element of K19(K20(REAL : ( ( ) ( non empty V50() V55() V56() V57() V61() ) set ) ,REAL : ( ( ) ( non empty V50() V55() V56() V57() V61() ) set ) ) : ( ( ) ( Relation-like V34() V35() V36() ) set ) ) : ( ( ) ( ) set ) ) . x : ( ( ) ( V28() V29() ext-real ) Real) : ( ( ) ( V28() V29() ext-real ) Element of REAL : ( ( ) ( non empty V50() V55() V56() V57() V61() ) set ) ) < 1 : ( ( ) ( non empty V21() V22() V23() V27() V28() V29() V30() ext-real positive non negative V55() V56() V57() V58() V59() V60() V67() ) Element of NAT : ( ( ) ( non empty V21() V22() V23() V55() V56() V57() V58() V59() V60() V61() ) Element of K19(REAL : ( ( ) ( non empty V50() V55() V56() V57() V61() ) set ) ) : ( ( ) ( ) set ) ) ) & f1 : ( ( V6() ) ( Relation-like REAL : ( ( ) ( non empty V50() V55() V56() V57() V61() ) set ) -defined REAL : ( ( ) ( non empty V50() V55() V56() V57() V61() ) set ) -valued V6() V34() V35() V36() ) PartFunc of ,) . x : ( ( ) ( V28() V29() ext-real ) Real) : ( ( ) ( V28() V29() ext-real ) Element of REAL : ( ( ) ( non empty V50() V55() V56() V57() V61() ) set ) ) = 1 : ( ( ) ( non empty V21() V22() V23() V27() V28() V29() V30() ext-real positive non negative V55() V56() V57() V58() V59() V60() V67() ) Element of NAT : ( ( ) ( non empty V21() V22() V23() V55() V56() V57() V58() V59() V60() V61() ) Element of K19(REAL : ( ( ) ( non empty V50() V55() V56() V57() V61() ) set ) ) : ( ( ) ( ) set ) ) ) ) ) & Z : ( ( open ) ( V55() V56() V57() open ) Subset of ( ( ) ( ) set ) ) c= dom (arccot : ( ( V6() ) ( Relation-like REAL : ( ( ) ( non empty V50() V55() V56() V57() V61() ) set ) -defined REAL : ( ( ) ( non empty V50() V55() V56() V57() V61() ) set ) -valued V6() V34() V35() V36() ) Element of K19(K20(REAL : ( ( ) ( non empty V50() V55() V56() V57() V61() ) set ) ,REAL : ( ( ) ( non empty V50() V55() V56() V57() V61() ) set ) ) : ( ( ) ( Relation-like V34() V35() V36() ) set ) ) : ( ( ) ( ) set ) ) * exp_R : ( ( V6() V18( REAL : ( ( ) ( non empty V50() V55() V56() V57() V61() ) set ) , REAL : ( ( ) ( non empty V50() V55() V56() V57() V61() ) set ) ) ) ( Relation-like REAL : ( ( ) ( non empty V50() V55() V56() V57() V61() ) set ) -defined REAL : ( ( ) ( non empty V50() V55() V56() V57() V61() ) set ) -valued V6() non empty total V18( REAL : ( ( ) ( non empty V50() V55() V56() V57() V61() ) set ) , REAL : ( ( ) ( non empty V50() V55() V56() V57() V61() ) set ) ) V34() V35() V36() ) Element of K19(K20(REAL : ( ( ) ( non empty V50() V55() V56() V57() V61() ) set ) ,REAL : ( ( ) ( non empty V50() V55() V56() V57() V61() ) set ) ) : ( ( ) ( Relation-like V34() V35() V36() ) set ) ) : ( ( ) ( ) set ) ) ) : ( ( V6() ) ( Relation-like REAL : ( ( ) ( non empty V50() V55() V56() V57() V61() ) set ) -defined REAL : ( ( ) ( non empty V50() V55() V56() V57() V61() ) set ) -valued V6() V34() V35() V36() ) Element of K19(K20(REAL : ( ( ) ( non empty V50() V55() V56() V57() V61() ) set ) ,REAL : ( ( ) ( non empty V50() V55() V56() V57() V61() ) set ) ) : ( ( ) ( Relation-like V34() V35() V36() ) set ) ) : ( ( ) ( ) set ) ) : ( ( ) ( V55() V56() V57() ) Element of K19(REAL : ( ( ) ( non empty V50() V55() V56() V57() V61() ) set ) ) : ( ( ) ( ) set ) ) & Z : ( ( open ) ( V55() V56() V57() open ) Subset of ( ( ) ( ) set ) ) = dom f : ( ( V6() ) ( Relation-like REAL : ( ( ) ( non empty V50() V55() V56() V57() V61() ) set ) -defined REAL : ( ( ) ( non empty V50() V55() V56() V57() V61() ) set ) -valued V6() V34() V35() V36() ) PartFunc of ,) : ( ( ) ( V55() V56() V57() ) Element of K19(REAL : ( ( ) ( non empty V50() V55() V56() V57() V61() ) set ) ) : ( ( ) ( ) set ) ) & f : ( ( V6() ) ( Relation-like REAL : ( ( ) ( non empty V50() V55() V56() V57() V61() ) set ) -defined REAL : ( ( ) ( non empty V50() V55() V56() V57() V61() ) set ) -valued V6() V34() V35() V36() ) PartFunc of ,) = (- exp_R : ( ( V6() V18( REAL : ( ( ) ( non empty V50() V55() V56() V57() V61() ) set ) , REAL : ( ( ) ( non empty V50() V55() V56() V57() V61() ) set ) ) ) ( Relation-like REAL : ( ( ) ( non empty V50() V55() V56() V57() V61() ) set ) -defined REAL : ( ( ) ( non empty V50() V55() V56() V57() V61() ) set ) -valued V6() non empty total V18( REAL : ( ( ) ( non empty V50() V55() V56() V57() V61() ) set ) , REAL : ( ( ) ( non empty V50() V55() V56() V57() V61() ) set ) ) V34() V35() V36() ) Element of K19(K20(REAL : ( ( ) ( non empty V50() V55() V56() V57() V61() ) set ) ,REAL : ( ( ) ( non empty V50() V55() V56() V57() V61() ) set ) ) : ( ( ) ( Relation-like V34() V35() V36() ) set ) ) : ( ( ) ( ) set ) ) ) : ( ( V6() ) ( Relation-like REAL : ( ( ) ( non empty V50() V55() V56() V57() V61() ) set ) -defined REAL : ( ( ) ( non empty V50() V55() V56() V57() V61() ) set ) -valued V6() non empty total V18( REAL : ( ( ) ( non empty V50() V55() V56() V57() V61() ) set ) , REAL : ( ( ) ( non empty V50() V55() V56() V57() V61() ) set ) ) V34() V35() V36() ) Element of K19(K20(REAL : ( ( ) ( non empty V50() V55() V56() V57() V61() ) set ) ,REAL : ( ( ) ( non empty V50() V55() V56() V57() V61() ) set ) ) : ( ( ) ( Relation-like V34() V35() V36() ) set ) ) : ( ( ) ( ) set ) ) / (f1 : ( ( V6() ) ( Relation-like REAL : ( ( ) ( non empty V50() V55() V56() V57() V61() ) set ) -defined REAL : ( ( ) ( non empty V50() V55() V56() V57() V61() ) set ) -valued V6() V34() V35() V36() ) PartFunc of ,) + (exp_R : ( ( V6() V18( REAL : ( ( ) ( non empty V50() V55() V56() V57() V61() ) set ) , REAL : ( ( ) ( non empty V50() V55() V56() V57() V61() ) set ) ) ) ( Relation-like REAL : ( ( ) ( non empty V50() V55() V56() V57() V61() ) set ) -defined REAL : ( ( ) ( non empty V50() V55() V56() V57() V61() ) set ) -valued V6() non empty total V18( REAL : ( ( ) ( non empty V50() V55() V56() V57() V61() ) set ) , REAL : ( ( ) ( non empty V50() V55() V56() V57() V61() ) set ) ) V34() V35() V36() ) Element of K19(K20(REAL : ( ( ) ( non empty V50() V55() V56() V57() V61() ) set ) ,REAL : ( ( ) ( non empty V50() V55() V56() V57() V61() ) set ) ) : ( ( ) ( Relation-like V34() V35() V36() ) set ) ) : ( ( ) ( ) set ) ) ^2) : ( ( V6() ) ( Relation-like REAL : ( ( ) ( non empty V50() V55() V56() V57() V61() ) set ) -defined REAL : ( ( ) ( non empty V50() V55() V56() V57() V61() ) set ) -valued V6() non empty total V18( REAL : ( ( ) ( non empty V50() V55() V56() V57() V61() ) set ) , REAL : ( ( ) ( non empty V50() V55() V56() V57() V61() ) set ) ) V34() V35() V36() ) Element of K19(K20(REAL : ( ( ) ( non empty V50() V55() V56() V57() V61() ) set ) ,REAL : ( ( ) ( non empty V50() V55() V56() V57() V61() ) set ) ) : ( ( ) ( Relation-like V34() V35() V36() ) set ) ) : ( ( ) ( ) set ) ) ) : ( ( V6() ) ( Relation-like REAL : ( ( ) ( non empty V50() V55() V56() V57() V61() ) set ) -defined REAL : ( ( ) ( non empty V50() V55() V56() V57() V61() ) set ) -valued V6() V34() V35() V36() ) Element of K19(K20(REAL : ( ( ) ( non empty V50() V55() V56() V57() V61() ) set ) ,REAL : ( ( ) ( non empty V50() V55() V56() V57() V61() ) set ) ) : ( ( ) ( Relation-like V34() V35() V36() ) set ) ) : ( ( ) ( ) set ) ) : ( ( V6() ) ( Relation-like REAL : ( ( ) ( non empty V50() V55() V56() V57() V61() ) set ) -defined REAL : ( ( ) ( non empty V50() V55() V56() V57() V61() ) set ) -valued V6() V34() V35() V36() ) Element of K19(K20(REAL : ( ( ) ( non empty V50() V55() V56() V57() V61() ) set ) ,REAL : ( ( ) ( non empty V50() V55() V56() V57() V61() ) set ) ) : ( ( ) ( Relation-like V34() V35() V36() ) set ) ) : ( ( ) ( ) set ) ) holds
integral (f : ( ( V6() ) ( Relation-like REAL : ( ( ) ( non empty V50() V55() V56() V57() V61() ) set ) -defined REAL : ( ( ) ( non empty V50() V55() V56() V57() V61() ) set ) -valued V6() V34() V35() V36() ) PartFunc of ,) ,A : ( ( non empty closed_interval ) ( non empty V55() V56() V57() closed_interval V86() V87() compact closed ) Subset of ( ( ) ( ) set ) ) ) : ( ( ) ( V28() V29() ext-real ) Element of REAL : ( ( ) ( non empty V50() V55() V56() V57() V61() ) set ) ) = ((arccot : ( ( V6() ) ( Relation-like REAL : ( ( ) ( non empty V50() V55() V56() V57() V61() ) set ) -defined REAL : ( ( ) ( non empty V50() V55() V56() V57() V61() ) set ) -valued V6() V34() V35() V36() ) Element of K19(K20(REAL : ( ( ) ( non empty V50() V55() V56() V57() V61() ) set ) ,REAL : ( ( ) ( non empty V50() V55() V56() V57() V61() ) set ) ) : ( ( ) ( Relation-like V34() V35() V36() ) set ) ) : ( ( ) ( ) set ) ) * exp_R : ( ( V6() V18( REAL : ( ( ) ( non empty V50() V55() V56() V57() V61() ) set ) , REAL : ( ( ) ( non empty V50() V55() V56() V57() V61() ) set ) ) ) ( Relation-like REAL : ( ( ) ( non empty V50() V55() V56() V57() V61() ) set ) -defined REAL : ( ( ) ( non empty V50() V55() V56() V57() V61() ) set ) -valued V6() non empty total V18( REAL : ( ( ) ( non empty V50() V55() V56() V57() V61() ) set ) , REAL : ( ( ) ( non empty V50() V55() V56() V57() V61() ) set ) ) V34() V35() V36() ) Element of K19(K20(REAL : ( ( ) ( non empty V50() V55() V56() V57() V61() ) set ) ,REAL : ( ( ) ( non empty V50() V55() V56() V57() V61() ) set ) ) : ( ( ) ( Relation-like V34() V35() V36() ) set ) ) : ( ( ) ( ) set ) ) ) : ( ( V6() ) ( Relation-like REAL : ( ( ) ( non empty V50() V55() V56() V57() V61() ) set ) -defined REAL : ( ( ) ( non empty V50() V55() V56() V57() V61() ) set ) -valued V6() V34() V35() V36() ) Element of K19(K20(REAL : ( ( ) ( non empty V50() V55() V56() V57() V61() ) set ) ,REAL : ( ( ) ( non empty V50() V55() V56() V57() V61() ) set ) ) : ( ( ) ( Relation-like V34() V35() V36() ) set ) ) : ( ( ) ( ) set ) ) . (upper_bound A : ( ( non empty closed_interval ) ( non empty V55() V56() V57() closed_interval V86() V87() compact closed ) Subset of ( ( ) ( ) set ) ) ) : ( ( ) ( V28() V29() ext-real ) Element of REAL : ( ( ) ( non empty V50() V55() V56() V57() V61() ) set ) ) ) : ( ( ) ( V28() V29() ext-real ) Element of REAL : ( ( ) ( non empty V50() V55() V56() V57() V61() ) set ) ) - ((arccot : ( ( V6() ) ( Relation-like REAL : ( ( ) ( non empty V50() V55() V56() V57() V61() ) set ) -defined REAL : ( ( ) ( non empty V50() V55() V56() V57() V61() ) set ) -valued V6() V34() V35() V36() ) Element of K19(K20(REAL : ( ( ) ( non empty V50() V55() V56() V57() V61() ) set ) ,REAL : ( ( ) ( non empty V50() V55() V56() V57() V61() ) set ) ) : ( ( ) ( Relation-like V34() V35() V36() ) set ) ) : ( ( ) ( ) set ) ) * exp_R : ( ( V6() V18( REAL : ( ( ) ( non empty V50() V55() V56() V57() V61() ) set ) , REAL : ( ( ) ( non empty V50() V55() V56() V57() V61() ) set ) ) ) ( Relation-like REAL : ( ( ) ( non empty V50() V55() V56() V57() V61() ) set ) -defined REAL : ( ( ) ( non empty V50() V55() V56() V57() V61() ) set ) -valued V6() non empty total V18( REAL : ( ( ) ( non empty V50() V55() V56() V57() V61() ) set ) , REAL : ( ( ) ( non empty V50() V55() V56() V57() V61() ) set ) ) V34() V35() V36() ) Element of K19(K20(REAL : ( ( ) ( non empty V50() V55() V56() V57() V61() ) set ) ,REAL : ( ( ) ( non empty V50() V55() V56() V57() V61() ) set ) ) : ( ( ) ( Relation-like V34() V35() V36() ) set ) ) : ( ( ) ( ) set ) ) ) : ( ( V6() ) ( Relation-like REAL : ( ( ) ( non empty V50() V55() V56() V57() V61() ) set ) -defined REAL : ( ( ) ( non empty V50() V55() V56() V57() V61() ) set ) -valued V6() V34() V35() V36() ) Element of K19(K20(REAL : ( ( ) ( non empty V50() V55() V56() V57() V61() ) set ) ,REAL : ( ( ) ( non empty V50() V55() V56() V57() V61() ) set ) ) : ( ( ) ( Relation-like V34() V35() V36() ) set ) ) : ( ( ) ( ) set ) ) . (lower_bound A : ( ( non empty closed_interval ) ( non empty V55() V56() V57() closed_interval V86() V87() compact closed ) Subset of ( ( ) ( ) set ) ) ) : ( ( ) ( V28() V29() ext-real ) Element of REAL : ( ( ) ( non empty V50() V55() V56() V57() V61() ) set ) ) ) : ( ( ) ( V28() V29() ext-real ) Element of REAL : ( ( ) ( non empty V50() V55() V56() V57() V61() ) set ) ) : ( ( ) ( V28() V29() ext-real ) Element of REAL : ( ( ) ( non empty V50() V55() V56() V57() V61() ) set ) ) ;

for A being ( ( non empty closed_interval ) ( non empty V55() V56() V57() closed_interval V86() V87() compact closed ) Subset of ( ( ) ( ) set ) )
for f being ( ( V6() ) ( Relation-like REAL : ( ( ) ( non empty V50() V55() V56() V57() V61() ) set ) -defined REAL : ( ( ) ( non empty V50() V55() V56() V57() V61() ) set ) -valued V6() V34() V35() V36() ) PartFunc of ,)
for Z being ( ( open ) ( V55() V56() V57() open ) Subset of ( ( ) ( ) set ) ) st A : ( ( non empty closed_interval ) ( non empty V55() V56() V57() closed_interval V86() V87() compact closed ) Subset of ( ( ) ( ) set ) ) c= Z : ( ( open ) ( V55() V56() V57() open ) Subset of ( ( ) ( ) set ) ) & Z : ( ( open ) ( V55() V56() V57() open ) Subset of ( ( ) ( ) set ) ) = dom f : ( ( V6() ) ( Relation-like REAL : ( ( ) ( non empty V50() V55() V56() V57() V61() ) set ) -defined REAL : ( ( ) ( non empty V50() V55() V56() V57() V61() ) set ) -valued V6() V34() V35() V36() ) PartFunc of ,) : ( ( ) ( V55() V56() V57() ) Element of K19(REAL : ( ( ) ( non empty V50() V55() V56() V57() V61() ) set ) ) : ( ( ) ( ) set ) ) & f : ( ( V6() ) ( Relation-like REAL : ( ( ) ( non empty V50() V55() V56() V57() V61() ) set ) -defined REAL : ( ( ) ( non empty V50() V55() V56() V57() V61() ) set ) -valued V6() V34() V35() V36() ) PartFunc of ,) = (exp_R : ( ( V6() V18( REAL : ( ( ) ( non empty V50() V55() V56() V57() V61() ) set ) , REAL : ( ( ) ( non empty V50() V55() V56() V57() V61() ) set ) ) ) ( Relation-like REAL : ( ( ) ( non empty V50() V55() V56() V57() V61() ) set ) -defined REAL : ( ( ) ( non empty V50() V55() V56() V57() V61() ) set ) -valued V6() non empty total V18( REAL : ( ( ) ( non empty V50() V55() V56() V57() V61() ) set ) , REAL : ( ( ) ( non empty V50() V55() V56() V57() V61() ) set ) ) V34() V35() V36() ) Element of K19(K20(REAL : ( ( ) ( non empty V50() V55() V56() V57() V61() ) set ) ,REAL : ( ( ) ( non empty V50() V55() V56() V57() V61() ) set ) ) : ( ( ) ( Relation-like V34() V35() V36() ) set ) ) : ( ( ) ( ) set ) ) (#) (sin : ( ( V6() V18( REAL : ( ( ) ( non empty V50() V55() V56() V57() V61() ) set ) , REAL : ( ( ) ( non empty V50() V55() V56() V57() V61() ) set ) ) ) ( Relation-like REAL : ( ( ) ( non empty V50() V55() V56() V57() V61() ) set ) -defined REAL : ( ( ) ( non empty V50() V55() V56() V57() V61() ) set ) -valued V6() non empty total V18( REAL : ( ( ) ( non empty V50() V55() V56() V57() V61() ) set ) , REAL : ( ( ) ( non empty V50() V55() V56() V57() V61() ) set ) ) V34() V35() V36() ) Element of K19(K20(REAL : ( ( ) ( non empty V50() V55() V56() V57() V61() ) set ) ,REAL : ( ( ) ( non empty V50() V55() V56() V57() V61() ) set ) ) : ( ( ) ( Relation-like V34() V35() V36() ) set ) ) : ( ( ) ( ) set ) ) / cos : ( ( V6() V18( REAL : ( ( ) ( non empty V50() V55() V56() V57() V61() ) set ) , REAL : ( ( ) ( non empty V50() V55() V56() V57() V61() ) set ) ) ) ( Relation-like REAL : ( ( ) ( non empty V50() V55() V56() V57() V61() ) set ) -defined REAL : ( ( ) ( non empty V50() V55() V56() V57() V61() ) set ) -valued V6() non empty total V18( REAL : ( ( ) ( non empty V50() V55() V56() V57() V61() ) set ) , REAL : ( ( ) ( non empty V50() V55() V56() V57() V61() ) set ) ) V34() V35() V36() ) Element of K19(K20(REAL : ( ( ) ( non empty V50() V55() V56() V57() V61() ) set ) ,REAL : ( ( ) ( non empty V50() V55() V56() V57() V61() ) set ) ) : ( ( ) ( Relation-like V34() V35() V36() ) set ) ) : ( ( ) ( ) set ) ) ) : ( ( V6() ) ( Relation-like REAL : ( ( ) ( non empty V50() V55() V56() V57() V61() ) set ) -defined REAL : ( ( ) ( non empty V50() V55() V56() V57() V61() ) set ) -valued V6() V34() V35() V36() ) Element of K19(K20(REAL : ( ( ) ( non empty V50() V55() V56() V57() V61() ) set ) ,REAL : ( ( ) ( non empty V50() V55() V56() V57() V61() ) set ) ) : ( ( ) ( Relation-like V34() V35() V36() ) set ) ) : ( ( ) ( ) set ) ) ) : ( ( V6() ) ( Relation-like REAL : ( ( ) ( non empty V50() V55() V56() V57() V61() ) set ) -defined REAL : ( ( ) ( non empty V50() V55() V56() V57() V61() ) set ) -valued V6() V34() V35() V36() ) Element of K19(K20(REAL : ( ( ) ( non empty V50() V55() V56() V57() V61() ) set ) ,REAL : ( ( ) ( non empty V50() V55() V56() V57() V61() ) set ) ) : ( ( ) ( Relation-like V34() V35() V36() ) set ) ) : ( ( ) ( ) set ) ) + (exp_R : ( ( V6() V18( REAL : ( ( ) ( non empty V50() V55() V56() V57() V61() ) set ) , REAL : ( ( ) ( non empty V50() V55() V56() V57() V61() ) set ) ) ) ( Relation-like REAL : ( ( ) ( non empty V50() V55() V56() V57() V61() ) set ) -defined REAL : ( ( ) ( non empty V50() V55() V56() V57() V61() ) set ) -valued V6() non empty total V18( REAL : ( ( ) ( non empty V50() V55() V56() V57() V61() ) set ) , REAL : ( ( ) ( non empty V50() V55() V56() V57() V61() ) set ) ) V34() V35() V36() ) Element of K19(K20(REAL : ( ( ) ( non empty V50() V55() V56() V57() V61() ) set ) ,REAL : ( ( ) ( non empty V50() V55() V56() V57() V61() ) set ) ) : ( ( ) ( Relation-like V34() V35() V36() ) set ) ) : ( ( ) ( ) set ) ) / (cos : ( ( V6() V18( REAL : ( ( ) ( non empty V50() V55() V56() V57() V61() ) set ) , REAL : ( ( ) ( non empty V50() V55() V56() V57() V61() ) set ) ) ) ( Relation-like REAL : ( ( ) ( non empty V50() V55() V56() V57() V61() ) set ) -defined REAL : ( ( ) ( non empty V50() V55() V56() V57() V61() ) set ) -valued V6() non empty total V18( REAL : ( ( ) ( non empty V50() V55() V56() V57() V61() ) set ) , REAL : ( ( ) ( non empty V50() V55() V56() V57() V61() ) set ) ) V34() V35() V36() ) Element of K19(K20(REAL : ( ( ) ( non empty V50() V55() V56() V57() V61() ) set ) ,REAL : ( ( ) ( non empty V50() V55() V56() V57() V61() ) set ) ) : ( ( ) ( Relation-like V34() V35() V36() ) set ) ) : ( ( ) ( ) set ) ) ^2) : ( ( V6() ) ( Relation-like REAL : ( ( ) ( non empty V50() V55() V56() V57() V61() ) set ) -defined REAL : ( ( ) ( non empty V50() V55() V56() V57() V61() ) set ) -valued V6() non empty total V18( REAL : ( ( ) ( non empty V50() V55() V56() V57() V61() ) set ) , REAL : ( ( ) ( non empty V50() V55() V56() V57() V61() ) set ) ) V34() V35() V36() ) Element of K19(K20(REAL : ( ( ) ( non empty V50() V55() V56() V57() V61() ) set ) ,REAL : ( ( ) ( non empty V50() V55() V56() V57() V61() ) set ) ) : ( ( ) ( Relation-like V34() V35() V36() ) set ) ) : ( ( ) ( ) set ) ) ) : ( ( V6() ) ( Relation-like REAL : ( ( ) ( non empty V50() V55() V56() V57() V61() ) set ) -defined REAL : ( ( ) ( non empty V50() V55() V56() V57() V61() ) set ) -valued V6() V34() V35() V36() ) Element of K19(K20(REAL : ( ( ) ( non empty V50() V55() V56() V57() V61() ) set ) ,REAL : ( ( ) ( non empty V50() V55() V56() V57() V61() ) set ) ) : ( ( ) ( Relation-like V34() V35() V36() ) set ) ) : ( ( ) ( ) set ) ) : ( ( V6() ) ( Relation-like REAL : ( ( ) ( non empty V50() V55() V56() V57() V61() ) set ) -defined REAL : ( ( ) ( non empty V50() V55() V56() V57() V61() ) set ) -valued V6() V34() V35() V36() ) Element of K19(K20(REAL : ( ( ) ( non empty V50() V55() V56() V57() V61() ) set ) ,REAL : ( ( ) ( non empty V50() V55() V56() V57() V61() ) set ) ) : ( ( ) ( Relation-like V34() V35() V36() ) set ) ) : ( ( ) ( ) set ) ) holds
integral (f : ( ( V6() ) ( Relation-like REAL : ( ( ) ( non empty V50() V55() V56() V57() V61() ) set ) -defined REAL : ( ( ) ( non empty V50() V55() V56() V57() V61() ) set ) -valued V6() V34() V35() V36() ) PartFunc of ,) ,A : ( ( non empty closed_interval ) ( non empty V55() V56() V57() closed_interval V86() V87() compact closed ) Subset of ( ( ) ( ) set ) ) ) : ( ( ) ( V28() V29() ext-real ) Element of REAL : ( ( ) ( non empty V50() V55() V56() V57() V61() ) set ) ) = ((exp_R : ( ( V6() V18( REAL : ( ( ) ( non empty V50() V55() V56() V57() V61() ) set ) , REAL : ( ( ) ( non empty V50() V55() V56() V57() V61() ) set ) ) ) ( Relation-like REAL : ( ( ) ( non empty V50() V55() V56() V57() V61() ) set ) -defined REAL : ( ( ) ( non empty V50() V55() V56() V57() V61() ) set ) -valued V6() non empty total V18( REAL : ( ( ) ( non empty V50() V55() V56() V57() V61() ) set ) , REAL : ( ( ) ( non empty V50() V55() V56() V57() V61() ) set ) ) V34() V35() V36() ) Element of K19(K20(REAL : ( ( ) ( non empty V50() V55() V56() V57() V61() ) set ) ,REAL : ( ( ) ( non empty V50() V55() V56() V57() V61() ) set ) ) : ( ( ) ( Relation-like V34() V35() V36() ) set ) ) : ( ( ) ( ) set ) ) (#) tan : ( ( V6() ) ( Relation-like REAL : ( ( ) ( non empty V50() V55() V56() V57() V61() ) set ) -defined REAL : ( ( ) ( non empty V50() V55() V56() V57() V61() ) set ) -valued V6() V34() V35() V36() ) Element of K19(K20(REAL : ( ( ) ( non empty V50() V55() V56() V57() V61() ) set ) ,REAL : ( ( ) ( non empty V50() V55() V56() V57() V61() ) set ) ) : ( ( ) ( Relation-like V34() V35() V36() ) set ) ) : ( ( ) ( ) set ) ) ) : ( ( V6() ) ( Relation-like REAL : ( ( ) ( non empty V50() V55() V56() V57() V61() ) set ) -defined REAL : ( ( ) ( non empty V50() V55() V56() V57() V61() ) set ) -valued V6() V34() V35() V36() ) Element of K19(K20(REAL : ( ( ) ( non empty V50() V55() V56() V57() V61() ) set ) ,REAL : ( ( ) ( non empty V50() V55() V56() V57() V61() ) set ) ) : ( ( ) ( Relation-like V34() V35() V36() ) set ) ) : ( ( ) ( ) set ) ) . (upper_bound A : ( ( non empty closed_interval ) ( non empty V55() V56() V57() closed_interval V86() V87() compact closed ) Subset of ( ( ) ( ) set ) ) ) : ( ( ) ( V28() V29() ext-real ) Element of REAL : ( ( ) ( non empty V50() V55() V56() V57() V61() ) set ) ) ) : ( ( ) ( V28() V29() ext-real ) Element of REAL : ( ( ) ( non empty V50() V55() V56() V57() V61() ) set ) ) - ((exp_R : ( ( V6() V18( REAL : ( ( ) ( non empty V50() V55() V56() V57() V61() ) set ) , REAL : ( ( ) ( non empty V50() V55() V56() V57() V61() ) set ) ) ) ( Relation-like REAL : ( ( ) ( non empty V50() V55() V56() V57() V61() ) set ) -defined REAL : ( ( ) ( non empty V50() V55() V56() V57() V61() ) set ) -valued V6() non empty total V18( REAL : ( ( ) ( non empty V50() V55() V56() V57() V61() ) set ) , REAL : ( ( ) ( non empty V50() V55() V56() V57() V61() ) set ) ) V34() V35() V36() ) Element of K19(K20(REAL : ( ( ) ( non empty V50() V55() V56() V57() V61() ) set ) ,REAL : ( ( ) ( non empty V50() V55() V56() V57() V61() ) set ) ) : ( ( ) ( Relation-like V34() V35() V36() ) set ) ) : ( ( ) ( ) set ) ) (#) tan : ( ( V6() ) ( Relation-like REAL : ( ( ) ( non empty V50() V55() V56() V57() V61() ) set ) -defined REAL : ( ( ) ( non empty V50() V55() V56() V57() V61() ) set ) -valued V6() V34() V35() V36() ) Element of K19(K20(REAL : ( ( ) ( non empty V50() V55() V56() V57() V61() ) set ) ,REAL : ( ( ) ( non empty V50() V55() V56() V57() V61() ) set ) ) : ( ( ) ( Relation-like V34() V35() V36() ) set ) ) : ( ( ) ( ) set ) ) ) : ( ( V6() ) ( Relation-like REAL : ( ( ) ( non empty V50() V55() V56() V57() V61() ) set ) -defined REAL : ( ( ) ( non empty V50() V55() V56() V57() V61() ) set ) -valued V6() V34() V35() V36() ) Element of K19(K20(REAL : ( ( ) ( non empty V50() V55() V56() V57() V61() ) set ) ,REAL : ( ( ) ( non empty V50() V55() V56() V57() V61() ) set ) ) : ( ( ) ( Relation-like V34() V35() V36() ) set ) ) : ( ( ) ( ) set ) ) . (lower_bound A : ( ( non empty closed_interval ) ( non empty V55() V56() V57() closed_interval V86() V87() compact closed ) Subset of ( ( ) ( ) set ) ) ) : ( ( ) ( V28() V29() ext-real ) Element of REAL : ( ( ) ( non empty V50() V55() V56() V57() V61() ) set ) ) ) : ( ( ) ( V28() V29() ext-real ) Element of REAL : ( ( ) ( non empty V50() V55() V56() V57() V61() ) set ) ) : ( ( ) ( V28() V29() ext-real ) Element of REAL : ( ( ) ( non empty V50() V55() V56() V57() V61() ) set ) ) ;

for A being ( ( non empty closed_interval ) ( non empty V55() V56() V57() closed_interval V86() V87() compact closed ) Subset of ( ( ) ( ) set ) )
for f being ( ( V6() ) ( Relation-like REAL : ( ( ) ( non empty V50() V55() V56() V57() V61() ) set ) -defined REAL : ( ( ) ( non empty V50() V55() V56() V57() V61() ) set ) -valued V6() V34() V35() V36() ) PartFunc of ,)
for Z being ( ( open ) ( V55() V56() V57() open ) Subset of ( ( ) ( ) set ) ) st A : ( ( non empty closed_interval ) ( non empty V55() V56() V57() closed_interval V86() V87() compact closed ) Subset of ( ( ) ( ) set ) ) c= Z : ( ( open ) ( V55() V56() V57() open ) Subset of ( ( ) ( ) set ) ) & Z : ( ( open ) ( V55() V56() V57() open ) Subset of ( ( ) ( ) set ) ) = dom f : ( ( V6() ) ( Relation-like REAL : ( ( ) ( non empty V50() V55() V56() V57() V61() ) set ) -defined REAL : ( ( ) ( non empty V50() V55() V56() V57() V61() ) set ) -valued V6() V34() V35() V36() ) PartFunc of ,) : ( ( ) ( V55() V56() V57() ) Element of K19(REAL : ( ( ) ( non empty V50() V55() V56() V57() V61() ) set ) ) : ( ( ) ( ) set ) ) & f : ( ( V6() ) ( Relation-like REAL : ( ( ) ( non empty V50() V55() V56() V57() V61() ) set ) -defined REAL : ( ( ) ( non empty V50() V55() V56() V57() V61() ) set ) -valued V6() V34() V35() V36() ) PartFunc of ,) = (exp_R : ( ( V6() V18( REAL : ( ( ) ( non empty V50() V55() V56() V57() V61() ) set ) , REAL : ( ( ) ( non empty V50() V55() V56() V57() V61() ) set ) ) ) ( Relation-like REAL : ( ( ) ( non empty V50() V55() V56() V57() V61() ) set ) -defined REAL : ( ( ) ( non empty V50() V55() V56() V57() V61() ) set ) -valued V6() non empty total V18( REAL : ( ( ) ( non empty V50() V55() V56() V57() V61() ) set ) , REAL : ( ( ) ( non empty V50() V55() V56() V57() V61() ) set ) ) V34() V35() V36() ) Element of K19(K20(REAL : ( ( ) ( non empty V50() V55() V56() V57() V61() ) set ) ,REAL : ( ( ) ( non empty V50() V55() V56() V57() V61() ) set ) ) : ( ( ) ( Relation-like V34() V35() V36() ) set ) ) : ( ( ) ( ) set ) ) (#) (cos : ( ( V6() V18( REAL : ( ( ) ( non empty V50() V55() V56() V57() V61() ) set ) , REAL : ( ( ) ( non empty V50() V55() V56() V57() V61() ) set ) ) ) ( Relation-like REAL : ( ( ) ( non empty V50() V55() V56() V57() V61() ) set ) -defined REAL : ( ( ) ( non empty V50() V55() V56() V57() V61() ) set ) -valued V6() non empty total V18( REAL : ( ( ) ( non empty V50() V55() V56() V57() V61() ) set ) , REAL : ( ( ) ( non empty V50() V55() V56() V57() V61() ) set ) ) V34() V35() V36() ) Element of K19(K20(REAL : ( ( ) ( non empty V50() V55() V56() V57() V61() ) set ) ,REAL : ( ( ) ( non empty V50() V55() V56() V57() V61() ) set ) ) : ( ( ) ( Relation-like V34() V35() V36() ) set ) ) : ( ( ) ( ) set ) ) / sin : ( ( V6() V18( REAL : ( ( ) ( non empty V50() V55() V56() V57() V61() ) set ) , REAL : ( ( ) ( non empty V50() V55() V56() V57() V61() ) set ) ) ) ( Relation-like REAL : ( ( ) ( non empty V50() V55() V56() V57() V61() ) set ) -defined REAL : ( ( ) ( non empty V50() V55() V56() V57() V61() ) set ) -valued V6() non empty total V18( REAL : ( ( ) ( non empty V50() V55() V56() V57() V61() ) set ) , REAL : ( ( ) ( non empty V50() V55() V56() V57() V61() ) set ) ) V34() V35() V36() ) Element of K19(K20(REAL : ( ( ) ( non empty V50() V55() V56() V57() V61() ) set ) ,REAL : ( ( ) ( non empty V50() V55() V56() V57() V61() ) set ) ) : ( ( ) ( Relation-like V34() V35() V36() ) set ) ) : ( ( ) ( ) set ) ) ) : ( ( V6() ) ( Relation-like REAL : ( ( ) ( non empty V50() V55() V56() V57() V61() ) set ) -defined REAL : ( ( ) ( non empty V50() V55() V56() V57() V61() ) set ) -valued V6() V34() V35() V36() ) Element of K19(K20(REAL : ( ( ) ( non empty V50() V55() V56() V57() V61() ) set ) ,REAL : ( ( ) ( non empty V50() V55() V56() V57() V61() ) set ) ) : ( ( ) ( Relation-like V34() V35() V36() ) set ) ) : ( ( ) ( ) set ) ) ) : ( ( V6() ) ( Relation-like REAL : ( ( ) ( non empty V50() V55() V56() V57() V61() ) set ) -defined REAL : ( ( ) ( non empty V50() V55() V56() V57() V61() ) set ) -valued V6() V34() V35() V36() ) Element of K19(K20(REAL : ( ( ) ( non empty V50() V55() V56() V57() V61() ) set ) ,REAL : ( ( ) ( non empty V50() V55() V56() V57() V61() ) set ) ) : ( ( ) ( Relation-like V34() V35() V36() ) set ) ) : ( ( ) ( ) set ) ) - (exp_R : ( ( V6() V18( REAL : ( ( ) ( non empty V50() V55() V56() V57() V61() ) set ) , REAL : ( ( ) ( non empty V50() V55() V56() V57() V61() ) set ) ) ) ( Relation-like REAL : ( ( ) ( non empty V50() V55() V56() V57() V61() ) set ) -defined REAL : ( ( ) ( non empty V50() V55() V56() V57() V61() ) set ) -valued V6() non empty total V18( REAL : ( ( ) ( non empty V50() V55() V56() V57() V61() ) set ) , REAL : ( ( ) ( non empty V50() V55() V56() V57() V61() ) set ) ) V34() V35() V36() ) Element of K19(K20(REAL : ( ( ) ( non empty V50() V55() V56() V57() V61() ) set ) ,REAL : ( ( ) ( non empty V50() V55() V56() V57() V61() ) set ) ) : ( ( ) ( Relation-like V34() V35() V36() ) set ) ) : ( ( ) ( ) set ) ) / (sin : ( ( V6() V18( REAL : ( ( ) ( non empty V50() V55() V56() V57() V61() ) set ) , REAL : ( ( ) ( non empty V50() V55() V56() V57() V61() ) set ) ) ) ( Relation-like REAL : ( ( ) ( non empty V50() V55() V56() V57() V61() ) set ) -defined REAL : ( ( ) ( non empty V50() V55() V56() V57() V61() ) set ) -valued V6() non empty total V18( REAL : ( ( ) ( non empty V50() V55() V56() V57() V61() ) set ) , REAL : ( ( ) ( non empty V50() V55() V56() V57() V61() ) set ) ) V34() V35() V36() ) Element of K19(K20(REAL : ( ( ) ( non empty V50() V55() V56() V57() V61() ) set ) ,REAL : ( ( ) ( non empty V50() V55() V56() V57() V61() ) set ) ) : ( ( ) ( Relation-like V34() V35() V36() ) set ) ) : ( ( ) ( ) set ) ) ^2) : ( ( V6() ) ( Relation-like REAL : ( ( ) ( non empty V50() V55() V56() V57() V61() ) set ) -defined REAL : ( ( ) ( non empty V50() V55() V56() V57() V61() ) set ) -valued V6() non empty total V18( REAL : ( ( ) ( non empty V50() V55() V56() V57() V61() ) set ) , REAL : ( ( ) ( non empty V50() V55() V56() V57() V61() ) set ) ) V34() V35() V36() ) Element of K19(K20(REAL : ( ( ) ( non empty V50() V55() V56() V57() V61() ) set ) ,REAL : ( ( ) ( non empty V50() V55() V56() V57() V61() ) set ) ) : ( ( ) ( Relation-like V34() V35() V36() ) set ) ) : ( ( ) ( ) set ) ) ) : ( ( V6() ) ( Relation-like REAL : ( ( ) ( non empty V50() V55() V56() V57() V61() ) set ) -defined REAL : ( ( ) ( non empty V50() V55() V56() V57() V61() ) set ) -valued V6() V34() V35() V36() ) Element of K19(K20(REAL : ( ( ) ( non empty V50() V55() V56() V57() V61() ) set ) ,REAL : ( ( ) ( non empty V50() V55() V56() V57() V61() ) set ) ) : ( ( ) ( Relation-like V34() V35() V36() ) set ) ) : ( ( ) ( ) set ) ) : ( ( V6() ) ( Relation-like REAL : ( ( ) ( non empty V50() V55() V56() V57() V61() ) set ) -defined REAL : ( ( ) ( non empty V50() V55() V56() V57() V61() ) set ) -valued V6() V34() V35() V36() ) Element of K19(K20(REAL : ( ( ) ( non empty V50() V55() V56() V57() V61() ) set ) ,REAL : ( ( ) ( non empty V50() V55() V56() V57() V61() ) set ) ) : ( ( ) ( Relation-like V34() V35() V36() ) set ) ) : ( ( ) ( ) set ) ) holds
integral (f : ( ( V6() ) ( Relation-like REAL : ( ( ) ( non empty V50() V55() V56() V57() V61() ) set ) -defined REAL : ( ( ) ( non empty V50() V55() V56() V57() V61() ) set ) -valued V6() V34() V35() V36() ) PartFunc of ,) ,A : ( ( non empty closed_interval ) ( non empty V55() V56() V57() closed_interval V86() V87() compact closed ) Subset of ( ( ) ( ) set ) ) ) : ( ( ) ( V28() V29() ext-real ) Element of REAL : ( ( ) ( non empty V50() V55() V56() V57() V61() ) set ) ) = ((exp_R : ( ( V6() V18( REAL : ( ( ) ( non empty V50() V55() V56() V57() V61() ) set ) , REAL : ( ( ) ( non empty V50() V55() V56() V57() V61() ) set ) ) ) ( Relation-like REAL : ( ( ) ( non empty V50() V55() V56() V57() V61() ) set ) -defined REAL : ( ( ) ( non empty V50() V55() V56() V57() V61() ) set ) -valued V6() non empty total V18( REAL : ( ( ) ( non empty V50() V55() V56() V57() V61() ) set ) , REAL : ( ( ) ( non empty V50() V55() V56() V57() V61() ) set ) ) V34() V35() V36() ) Element of K19(K20(REAL : ( ( ) ( non empty V50() V55() V56() V57() V61() ) set ) ,REAL : ( ( ) ( non empty V50() V55() V56() V57() V61() ) set ) ) : ( ( ) ( Relation-like V34() V35() V36() ) set ) ) : ( ( ) ( ) set ) ) (#) cot : ( ( V6() ) ( Relation-like REAL : ( ( ) ( non empty V50() V55() V56() V57() V61() ) set ) -defined REAL : ( ( ) ( non empty V50() V55() V56() V57() V61() ) set ) -valued V6() V34() V35() V36() ) Element of K19(K20(REAL : ( ( ) ( non empty V50() V55() V56() V57() V61() ) set ) ,REAL : ( ( ) ( non empty V50() V55() V56() V57() V61() ) set ) ) : ( ( ) ( Relation-like V34() V35() V36() ) set ) ) : ( ( ) ( ) set ) ) ) : ( ( V6() ) ( Relation-like REAL : ( ( ) ( non empty V50() V55() V56() V57() V61() ) set ) -defined REAL : ( ( ) ( non empty V50() V55() V56() V57() V61() ) set ) -valued V6() V34() V35() V36() ) Element of K19(K20(REAL : ( ( ) ( non empty V50() V55() V56() V57() V61() ) set ) ,REAL : ( ( ) ( non empty V50() V55() V56() V57() V61() ) set ) ) : ( ( ) ( Relation-like V34() V35() V36() ) set ) ) : ( ( ) ( ) set ) ) . (upper_bound A : ( ( non empty closed_interval ) ( non empty V55() V56() V57() closed_interval V86() V87() compact closed ) Subset of ( ( ) ( ) set ) ) ) : ( ( ) ( V28() V29() ext-real ) Element of REAL : ( ( ) ( non empty V50() V55() V56() V57() V61() ) set ) ) ) : ( ( ) ( V28() V29() ext-real ) Element of REAL : ( ( ) ( non empty V50() V55() V56() V57() V61() ) set ) ) - ((exp_R : ( ( V6() V18( REAL : ( ( ) ( non empty V50() V55() V56() V57() V61() ) set ) , REAL : ( ( ) ( non empty V50() V55() V56() V57() V61() ) set ) ) ) ( Relation-like REAL : ( ( ) ( non empty V50() V55() V56() V57() V61() ) set ) -defined REAL : ( ( ) ( non empty V50() V55() V56() V57() V61() ) set ) -valued V6() non empty total V18( REAL : ( ( ) ( non empty V50() V55() V56() V57() V61() ) set ) , REAL : ( ( ) ( non empty V50() V55() V56() V57() V61() ) set ) ) V34() V35() V36() ) Element of K19(K20(REAL : ( ( ) ( non empty V50() V55() V56() V57() V61() ) set ) ,REAL : ( ( ) ( non empty V50() V55() V56() V57() V61() ) set ) ) : ( ( ) ( Relation-like V34() V35() V36() ) set ) ) : ( ( ) ( ) set ) ) (#) cot : ( ( V6() ) ( Relation-like REAL : ( ( ) ( non empty V50() V55() V56() V57() V61() ) set ) -defined REAL : ( ( ) ( non empty V50() V55() V56() V57() V61() ) set ) -valued V6() V34() V35() V36() ) Element of K19(K20(REAL : ( ( ) ( non empty V50() V55() V56() V57() V61() ) set ) ,REAL : ( ( ) ( non empty V50() V55() V56() V57() V61() ) set ) ) : ( ( ) ( Relation-like V34() V35() V36() ) set ) ) : ( ( ) ( ) set ) ) ) : ( ( V6() ) ( Relation-like REAL : ( ( ) ( non empty V50() V55() V56() V57() V61() ) set ) -defined REAL : ( ( ) ( non empty V50() V55() V56() V57() V61() ) set ) -valued V6() V34() V35() V36() ) Element of K19(K20(REAL : ( ( ) ( non empty V50() V55() V56() V57() V61() ) set ) ,REAL : ( ( ) ( non empty V50() V55() V56() V57() V61() ) set ) ) : ( ( ) ( Relation-like V34() V35() V36() ) set ) ) : ( ( ) ( ) set ) ) . (lower_bound A : ( ( non empty closed_interval ) ( non empty V55() V56() V57() closed_interval V86() V87() compact closed ) Subset of ( ( ) ( ) set ) ) ) : ( ( ) ( V28() V29() ext-real ) Element of REAL : ( ( ) ( non empty V50() V55() V56() V57() V61() ) set ) ) ) : ( ( ) ( V28() V29() ext-real ) Element of REAL : ( ( ) ( non empty V50() V55() V56() V57() V61() ) set ) ) : ( ( ) ( V28() V29() ext-real ) Element of REAL : ( ( ) ( non empty V50() V55() V56() V57() V61() ) set ) ) ;