:: INTEGR12 semantic presentation

REAL is non empty V50() V55() V56() V57() V61() set
NAT is non empty V21() V22() V23() V55() V56() V57() V58() V59() V60() V61() Element of K19(REAL)
K19(REAL) is set
COMPLEX is non empty V50() V55() V61() set
K20(NAT,REAL) is Relation-like V34() V35() V36() set
K19(K20(NAT,REAL)) is set
K20(NAT,COMPLEX) is Relation-like V34() set
K19(K20(NAT,COMPLEX)) is set

K19(K20(COMPLEX,COMPLEX)) is set
K20(REAL,REAL) is Relation-like V34() V35() V36() set
K19(K20(REAL,REAL)) is set
PFuncs (REAL,REAL) is set
K20(NAT,()) is Relation-like set
K19(K20(NAT,())) is set
ExtREAL is non empty V56() set
+infty is non empty V29() ext-real positive non negative set
-infty is non empty V29() ext-real non positive negative set
0 is Relation-like non-empty empty-yielding RAT -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
RAT is non empty V50() V55() V56() V57() V58() V61() set
the Relation-like non-empty empty-yielding RAT -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() bounded set is Relation-like non-empty empty-yielding RAT -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() bounded set
is set
is non empty set
is V9() non empty V55() V56() V57() V58() V59() V60() set
is non empty set
is non empty V56() set
REAL \/ is non empty V56() set
INT is non empty V50() V55() V56() V57() V58() V59() V61() set

K19(K20(K20(COMPLEX,COMPLEX),COMPLEX)) is set
K20(K20(REAL,REAL),REAL) is Relation-like V34() V35() V36() set
K19(K20(K20(REAL,REAL),REAL)) is set
K20(RAT,RAT) is Relation-like RAT -valued V34() V35() V36() set
K19(K20(RAT,RAT)) is set
K20(K20(RAT,RAT),RAT) is Relation-like RAT -valued V34() V35() V36() set
K19(K20(K20(RAT,RAT),RAT)) is set

K19(K20(INT,INT)) is set
K20(K20(INT,INT),INT) is Relation-like RAT -valued INT -valued V34() V35() V36() set
K19(K20(K20(INT,INT),INT)) is set

K20(K20(NAT,NAT),NAT) is Relation-like RAT -valued INT -valued V34() V35() V36() V37() set
K19(K20(K20(NAT,NAT),NAT)) is set
NAT is non empty V21() V22() V23() V55() V56() V57() V58() V59() V60() V61() set
K19(NAT) is set
K19(NAT) is set
K20(COMPLEX,REAL) is Relation-like V34() V35() V36() set
K19(K20(COMPLEX,REAL)) is set
{} is Relation-like non-empty empty-yielding RAT -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() bounded set
1 is non empty V21() V22() V23() V27() V28() V29() V30() ext-real positive non negative V55() V56() V57() V58() V59() V60() V67() Element of NAT
{{},1} is non empty V55() V56() V57() V58() V59() V60() set
sin is Relation-like REAL -defined REAL -valued V6() non empty total V18( REAL , REAL ) V34() V35() V36() Element of K19(K20(REAL,REAL))
dom sin is non empty V55() V56() V57() Element of K19(REAL)
cos is Relation-like REAL -defined REAL -valued V6() non empty total V18( REAL , REAL ) V34() V35() V36() Element of K19(K20(REAL,REAL))
dom cos is non empty V55() V56() V57() Element of K19(REAL)
exp_R is Relation-like REAL -defined REAL -valued V6() non empty total V18( REAL , REAL ) V34() V35() V36() Element of K19(K20(REAL,REAL))
2 is non empty V21() V22() V23() V27() V28() V29() V30() ext-real positive non negative V55() V56() V57() V58() V59() V60() V67() Element of NAT
#Z 2 is Relation-like REAL -defined REAL -valued V6() non empty total V18( REAL , REAL ) V34() V35() V36() Element of K19(K20(REAL,REAL))
[#] REAL is V55() V56() V57() Element of K19(REAL)
dom exp_R is non empty V55() V56() V57() Element of K19(REAL)
rng exp_R is non empty V55() V56() V57() Element of K19(REAL)
right_open_halfline 0 is V55() V56() V57() Element of K19(REAL)
K363(0,+infty) is set
{ b1 where b1 is V28() V29() ext-real Element of REAL : ( not b1 <= 0 & not +infty <= b1 ) } is set

dom ln is V55() V56() V57() Element of K19(REAL)
rng ln is V55() V56() V57() Element of K19(REAL)

PI is V28() V29() ext-real Element of REAL
PI / 2 is V28() V29() ext-real Element of REAL
K99(2) is non empty V28() V29() ext-real positive non negative set
K97(PI,K99(2)) is V28() V29() ext-real set
- (PI / 2) is V28() V29() ext-real Element of REAL
[.(- (PI / 2)),(PI / 2).] is V55() V56() V57() closed Element of K19(REAL)
{ b1 where b1 is V28() V29() ext-real Element of REAL : ( - (PI / 2) <= b1 & b1 <= PI / 2 ) } is set
sin | [.(- (PI / 2)),(PI / 2).] is Relation-like REAL -defined [.(- (PI / 2)),(PI / 2).] -defined REAL -defined REAL -valued V6() V34() V35() V36() Element of K19(K20(REAL,REAL))
(sin | [.(- (PI / 2)),(PI / 2).]) " is Relation-like REAL -defined REAL -valued V6() V34() V35() V36() Element of K19(K20(REAL,REAL))
- 1 is V28() V29() V30() ext-real non positive Element of REAL
].(- 1),1.[ is V55() V56() V57() open Element of K19(REAL)
{ b1 where b1 is V28() V29() ext-real Element of REAL : ( not b1 <= - 1 & not 1 <= b1 ) } is set

is V55() V56() V57() closed Element of K19(REAL)
{ b1 where b1 is V28() V29() ext-real Element of REAL : ( 0 <= b1 & b1 <= PI ) } is set

() " is Relation-like REAL -defined REAL -valued V6() V34() V35() V36() Element of K19(K20(REAL,REAL))
K98(1) is V28() V29() V30() ext-real non positive set
1 / 2 is V28() V29() ext-real non negative Element of REAL
K97(1,K99(2)) is V28() V29() ext-real non negative set

dom () is V55() V56() V57() Element of K19(REAL)

dom () is V55() V56() V57() Element of K19(REAL)
#R (1 / 2) is Relation-like REAL -defined REAL -valued V6() V34() V35() V36() Element of K19(K20(REAL,REAL))
- (1 / 2) is V28() V29() ext-real non positive Element of REAL

dom () is V55() V56() V57() Element of K19(REAL)

dom () is V55() V56() V57() Element of K19(REAL)
sin * exp_R is Relation-like REAL -defined REAL -valued V6() non empty total V18( REAL , REAL ) V34() V35() V36() Element of K19(K20(REAL,REAL))
dom () is non empty V55() V56() V57() Element of K19(REAL)
cos * exp_R is Relation-like REAL -defined REAL -valued V6() non empty total V18( REAL , REAL ) V34() V35() V36() Element of K19(K20(REAL,REAL))
dom () is non empty V55() V56() V57() Element of K19(REAL)
exp_R * cos is Relation-like REAL -defined REAL -valued V6() non empty total V18( REAL , REAL ) V34() V35() V36() Element of K19(K20(REAL,REAL))
dom () is non empty V55() V56() V57() Element of K19(REAL)
exp_R * sin is Relation-like REAL -defined REAL -valued V6() non empty total V18( REAL , REAL ) V34() V35() V36() Element of K19(K20(REAL,REAL))
dom () is non empty V55() V56() V57() Element of K19(REAL)

dom tan is V55() V56() V57() Element of K19(REAL)

dom cot is V55() V56() V57() Element of K19(REAL)

K98(1) (#) cot is Relation-like REAL -defined V6() V34() V35() V36() set

dom () is V55() V56() V57() Element of K19(REAL)

dom () is V55() V56() V57() Element of K19(REAL)

is V55() V56() V57() open Element of K19(REAL)
{ b1 where b1 is V28() V29() ext-real Element of REAL : ( not b1 <= 0 & not PI <= b1 ) } is set

() " is Relation-like REAL -defined REAL -valued V6() V34() V35() V36() Element of K19(K20(REAL,REAL))

].(- (PI / 2)),(PI / 2).[ is V55() V56() V57() open Element of K19(REAL)
{ b1 where b1 is V28() V29() ext-real Element of REAL : ( not b1 <= - (PI / 2) & not PI / 2 <= b1 ) } is set
tan | ].(- (PI / 2)),(PI / 2).[ is Relation-like REAL -defined ].(- (PI / 2)),(PI / 2).[ -defined REAL -defined REAL -valued V6() V34() V35() V36() Element of K19(K20(REAL,REAL))
(tan | ].(- (PI / 2)),(PI / 2).[) " is Relation-like REAL -defined REAL -valued V6() V34() V35() V36() Element of K19(K20(REAL,REAL))

dom () is V55() V56() V57() Element of K19(REAL)

dom () is V55() V56() V57() Element of K19(REAL)

dom () is V55() V56() V57() Element of K19(REAL)

dom () is V55() V56() V57() Element of K19(REAL)

dom () is V55() V56() V57() Element of K19(REAL)

- 1 is V28() V29() V30() ext-real non positive V67() Element of INT
A is Relation-like REAL -defined REAL -valued V6() V34() V35() V36() Element of K19(K20(REAL,REAL))
f1 is Relation-like REAL -defined REAL -valued V6() V34() V35() V36() Element of K19(K20(REAL,REAL))
A + f1 is Relation-like REAL -defined REAL -valued V6() V34() V35() V36() Element of K19(K20(REAL,REAL))
(A + f1) ^ is Relation-like REAL -defined REAL -valued V6() V34() V35() V36() Element of K19(K20(REAL,REAL))
dom ((A + f1) ^) is V55() V56() V57() Element of K19(REAL)
f is V55() V56() V57() open Element of K19(REAL)
((A + f1) ^) `| f is Relation-like REAL -defined REAL -valued V6() V34() V35() V36() Element of K19(K20(REAL,REAL))
dom (A + f1) is V55() V56() V57() Element of K19(REAL)
(A + f1) `| f is Relation-like REAL -defined REAL -valued V6() V34() V35() V36() Element of K19(K20(REAL,REAL))
Z is V28() V29() ext-real Element of REAL
((A + f1) `| f) . Z is V28() V29() ext-real Element of REAL
2 * Z is V28() V29() ext-real Element of REAL
Z is V28() V29() ext-real Element of REAL
(A + f1) . Z is V28() V29() ext-real Element of REAL
Z is V28() V29() ext-real Element of REAL
(((A + f1) ^) `| f) . Z is V28() V29() ext-real Element of REAL
2 * Z is V28() V29() ext-real Element of REAL
Z |^ 2 is V28() V29() ext-real Element of REAL
1 + (Z |^ 2) is V28() V29() ext-real Element of REAL
(1 + (Z |^ 2)) ^2 is V28() V29() ext-real Element of REAL
K97((1 + (Z |^ 2)),(1 + (Z |^ 2))) is V28() V29() ext-real set
(2 * Z) / ((1 + (Z |^ 2)) ^2) is V28() V29() ext-real Element of REAL
K99(((1 + (Z |^ 2)) ^2)) is V28() V29() ext-real set
K97((2 * Z),K99(((1 + (Z |^ 2)) ^2))) is V28() V29() ext-real set
- ((2 * Z) / ((1 + (Z |^ 2)) ^2)) is V28() V29() ext-real Element of REAL
(A + f1) . Z is V28() V29() ext-real Element of REAL
f1 . Z is V28() V29() ext-real Element of REAL
Z #Z 2 is V28() V29() ext-real Element of REAL
A . Z is V28() V29() ext-real Element of REAL
(A . Z) + (f1 . Z) is V28() V29() ext-real Element of REAL
diff (((A + f1) ^),Z) is V28() V29() ext-real Element of REAL
diff ((A + f1),Z) is V28() V29() ext-real Element of REAL
((A + f1) . Z) ^2 is V28() V29() ext-real Element of REAL
K97(((A + f1) . Z),((A + f1) . Z)) is V28() V29() ext-real set
(diff ((A + f1),Z)) / (((A + f1) . Z) ^2) is V28() V29() ext-real Element of REAL
K99((((A + f1) . Z) ^2)) is V28() V29() ext-real set
K97((diff ((A + f1),Z)),K99((((A + f1) . Z) ^2))) is V28() V29() ext-real set
- ((diff ((A + f1),Z)) / (((A + f1) . Z) ^2)) is V28() V29() ext-real Element of REAL
((A + f1) `| f) . Z is V28() V29() ext-real Element of REAL
(((A + f1) `| f) . Z) / (((A + f1) . Z) ^2) is V28() V29() ext-real Element of REAL
K97((((A + f1) `| f) . Z),K99((((A + f1) . Z) ^2))) is V28() V29() ext-real set
- ((((A + f1) `| f) . Z) / (((A + f1) . Z) ^2)) is V28() V29() ext-real Element of REAL
Z is V28() V29() ext-real Element of REAL
(((A + f1) ^) `| f) . Z is V28() V29() ext-real Element of REAL
2 * Z is V28() V29() ext-real Element of REAL
Z |^ 2 is V28() V29() ext-real Element of REAL
1 + (Z |^ 2) is V28() V29() ext-real Element of REAL
(1 + (Z |^ 2)) ^2 is V28() V29() ext-real Element of REAL
K97((1 + (Z |^ 2)),(1 + (Z |^ 2))) is V28() V29() ext-real set
(2 * Z) / ((1 + (Z |^ 2)) ^2) is V28() V29() ext-real Element of REAL
K99(((1 + (Z |^ 2)) ^2)) is V28() V29() ext-real set
K97((2 * Z),K99(((1 + (Z |^ 2)) ^2))) is V28() V29() ext-real set
- ((2 * Z) / ((1 + (Z |^ 2)) ^2)) is V28() V29() ext-real Element of REAL
].(- 1),1.[ is V55() V56() V57() open Element of K19(REAL)
{ b1 where b1 is V28() V29() ext-real Element of REAL : ( not b1 <= - 1 & not 1 <= b1 ) } is set
- () is Relation-like REAL -defined REAL -valued V6() V34() V35() V36() Element of K19(K20(REAL,REAL))
K98(1) (#) () is Relation-like REAL -defined V6() V34() V35() V36() set
A is non empty V55() V56() V57() closed_interval V86() V87() compact closed Element of K19(REAL)
upper_bound A is V28() V29() ext-real Element of REAL
(- ()) . () is V28() V29() ext-real Element of REAL
lower_bound A is V28() V29() ext-real Element of REAL
(- ()) . () is V28() V29() ext-real Element of REAL
((- ()) . ()) - ((- ()) . ()) is V28() V29() ext-real Element of REAL
K98(((- ()) . ())) is V28() V29() ext-real set
K96(((- ()) . ()),K98(((- ()) . ()))) is V28() V29() ext-real set
f1 is Relation-like REAL -defined REAL -valued V6() V34() V35() V36() Element of K19(K20(REAL,REAL))
dom f1 is V55() V56() V57() Element of K19(REAL)
integral (f1,A) is V28() V29() ext-real Element of REAL
f is Relation-like REAL -defined REAL -valued V6() V34() V35() V36() Element of K19(K20(REAL,REAL))
Z is Relation-like REAL -defined REAL -valued V6() V34() V35() V36() Element of K19(K20(REAL,REAL))
f + Z is Relation-like REAL -defined REAL -valued V6() V34() V35() V36() Element of K19(K20(REAL,REAL))
(f + Z) ^ is Relation-like REAL -defined REAL -valued V6() V34() V35() V36() Element of K19(K20(REAL,REAL))
g is Relation-like REAL -defined REAL -valued V6() V34() V35() V36() Element of K19(K20(REAL,REAL))
((f + Z) ^) / g is Relation-like REAL -defined REAL -valued V6() V34() V35() V36() Element of K19(K20(REAL,REAL))
f2 is V55() V56() V57() open Element of K19(REAL)
dom ((f + Z) ^) is V55() V56() V57() Element of K19(REAL)
dom g is V55() V56() V57() Element of K19(REAL)
is V9() non empty V55() V56() V57() V58() V59() V60() Element of K19(REAL)
g " is V55() V56() V57() Element of K19(REAL)
(dom g) \ (g " ) is V55() V56() V57() Element of K19(REAL)
(dom ((f + Z) ^)) /\ ((dom g) \ (g " )) is V55() V56() V57() Element of K19(REAL)
dom (f + Z) is V55() V56() V57() Element of K19(REAL)
x is V28() V29() ext-real Element of REAL
f . x is V28() V29() ext-real Element of REAL
x is V28() V29() ext-real Element of REAL
g . x is V28() V29() ext-real Element of REAL
f1 | f2 is Relation-like REAL -defined f2 -defined REAL -defined REAL -valued V6() V34() V35() V36() Element of K19(K20(REAL,REAL))

g ^ is Relation-like REAL -defined REAL -valued V6() V34() V35() V36() Element of K19(K20(REAL,REAL))
dom (g ^) is V55() V56() V57() Element of K19(REAL)
x is V28() V29() ext-real Element of REAL
g . x is V28() V29() ext-real Element of REAL

rng (g | f2) is V55() V56() V57() Element of K19(REAL)
x is set
dom (g | f2) is V55() V56() V57() Element of K19(f2)
K19(f2) is set
y is set
(g | f2) . y is V28() V29() ext-real Element of REAL
g . y is V28() V29() ext-real Element of REAL
g .: f2 is V55() V56() V57() Element of K19(REAL)
dom (- ()) is V55() V56() V57() Element of K19(REAL)
(- ()) `| f2 is Relation-like REAL -defined REAL -valued V6() V34() V35() V36() Element of K19(K20(REAL,REAL))
x is V28() V29() ext-real Element of REAL
((- ()) `| f2) . x is V28() V29() ext-real Element of REAL
x ^2 is V28() V29() ext-real Element of REAL
K97(x,x) is V28() V29() ext-real set
1 + (x ^2) is V28() V29() ext-real Element of REAL
arccot . x is V28() V29() ext-real Element of REAL
(1 + (x ^2)) * () is V28() V29() ext-real Element of REAL
1 / ((1 + (x ^2)) * ()) is V28() V29() ext-real Element of REAL
K99(((1 + (x ^2)) * ())) is V28() V29() ext-real set
K97(1,K99(((1 + (x ^2)) * ()))) is V28() V29() ext-real set
diff ((- ()),x) is V28() V29() ext-real Element of REAL
diff ((),x) is V28() V29() ext-real Element of REAL
(- 1) * (diff ((),x)) is V28() V29() ext-real Element of REAL
diff (arccot,x) is V28() V29() ext-real Element of REAL
(diff (arccot,x)) / () is V28() V29() ext-real Element of REAL
K99(()) is V28() V29() ext-real set
K97((diff (arccot,x)),K99(())) is V28() V29() ext-real set
(- 1) * ((diff (arccot,x)) / ()) is V28() V29() ext-real Element of REAL
1 / (1 + (x ^2)) is V28() V29() ext-real Element of REAL
K99((1 + (x ^2))) is V28() V29() ext-real set
K97(1,K99((1 + (x ^2)))) is V28() V29() ext-real set
- (1 / (1 + (x ^2))) is V28() V29() ext-real Element of REAL
(- (1 / (1 + (x ^2)))) / () is V28() V29() ext-real Element of REAL
K97((- (1 / (1 + (x ^2)))),K99(())) is V28() V29() ext-real set
(- 1) * ((- (1 / (1 + (x ^2)))) / ()) is V28() V29() ext-real Element of REAL
(1 / (1 + (x ^2))) / () is V28() V29() ext-real Element of REAL
K97((1 / (1 + (x ^2))),K99(())) is V28() V29() ext-real set
x is V28() V29() ext-real Element of REAL
f1 . x is V28() V29() ext-real Element of REAL
x ^2 is V28() V29() ext-real Element of REAL
K97(x,x) is V28() V29() ext-real set
1 + (x ^2) is V28() V29() ext-real Element of REAL
arccot . x is V28() V29() ext-real Element of REAL
(1 + (x ^2)) * () is V28() V29() ext-real Element of REAL
1 / ((1 + (x ^2)) * ()) is V28() V29() ext-real Element of REAL
K99(((1 + (x ^2)) * ())) is V28() V29() ext-real set
K97(1,K99(((1 + (x ^2)) * ()))) is V28() V29() ext-real set
(((f + Z) ^) / g) . x is V28() V29() ext-real Element of REAL
((f + Z) ^) . x is V28() V29() ext-real Element of REAL
g . x is V28() V29() ext-real Element of REAL
(((f + Z) ^) . x) / (g . x) is V28() V29() ext-real Element of REAL
K99((g . x)) is V28() V29() ext-real set
K97((((f + Z) ^) . x),K99((g . x))) is V28() V29() ext-real set
(f + Z) . x is V28() V29() ext-real Element of REAL
((f + Z) . x) " is V28() V29() ext-real Element of REAL
(((f + Z) . x) ") / (g . x) is V28() V29() ext-real Element of REAL
K97((((f + Z) . x) "),K99((g . x))) is V28() V29() ext-real set
f . x is V28() V29() ext-real Element of REAL
Z . x is V28() V29() ext-real Element of REAL
(f . x) + (Z . x) is V28() V29() ext-real Element of REAL
((f . x) + (Z . x)) " is V28() V29() ext-real Element of REAL
(((f . x) + (Z . x)) ") / (g . x) is V28() V29() ext-real Element of REAL
K97((((f . x) + (Z . x)) "),K99((g . x))) is V28() V29() ext-real set
((f . x) + (Z . x)) * (g . x) is V28() V29() ext-real Element of REAL
1 / (((f . x) + (Z . x)) * (g . x)) is V28() V29() ext-real Element of REAL
K99((((f . x) + (Z . x)) * (g . x))) is V28() V29() ext-real set
K97(1,K99((((f . x) + (Z . x)) * (g . x)))) is V28() V29() ext-real set
(#Z 2) . x is V28() V29() ext-real Element of REAL
1 + ((#Z 2) . x) is V28() V29() ext-real Element of REAL
(1 + ((#Z 2) . x)) * (g . x) is V28() V29() ext-real Element of REAL
1 / ((1 + ((#Z 2) . x)) * (g . x)) is V28() V29() ext-real Element of REAL
K99(((1 + ((#Z 2) . x)) * (g . x))) is V28() V29() ext-real set
K97(1,K99(((1 + ((#Z 2) . x)) * (g . x)))) is V28() V29() ext-real set
x #Z 2 is V28() V29() ext-real Element of REAL
1 + (x #Z 2) is V28() V29() ext-real Element of REAL
(1 + (x #Z 2)) * (g . x) is V28() V29() ext-real Element of REAL
1 / ((1 + (x #Z 2)) * (g . x)) is V28() V29() ext-real Element of REAL
K99(((1 + (x #Z 2)) * (g . x))) is V28() V29() ext-real set
K97(1,K99(((1 + (x #Z 2)) * (g . x)))) is V28() V29() ext-real set
dom ((- ()) `| f2) is V55() V56() V57() Element of K19(REAL)
x is V28() V29() ext-real Element of REAL
((- ()) `| f2) . x is V28() V29() ext-real Element of REAL
f1 . x is V28() V29() ext-real Element of REAL
x ^2 is V28() V29() ext-real Element of REAL
K97(x,x) is V28() V29() ext-real set
1 + (x ^2) is V28() V29() ext-real Element of REAL
arccot . x is V28() V29() ext-real Element of REAL
(1 + (x ^2)) * () is V28() V29() ext-real Element of REAL
1 / ((1 + (x ^2)) * ()) is V28() V29() ext-real Element of REAL
K99(((1 + (x ^2)) * ())) is V28() V29() ext-real set
K97(1,K99(((1 + (x ^2)) * ()))) is V28() V29() ext-real set
exp_R ^2 is Relation-like REAL -defined REAL -valued V6() non empty total V18( REAL , REAL ) V34() V35() V36() Element of K19(K20(REAL,REAL))

A is non empty V55() V56() V57() closed_interval V86() V87() compact closed Element of K19(REAL)
upper_bound A is V28() V29() ext-real Element of REAL
() . () is V28() V29() ext-real Element of REAL
lower_bound A is V28() V29() ext-real Element of REAL
() . () is V28() V29() ext-real Element of REAL
(() . ()) - (() . ()) is V28() V29() ext-real Element of REAL
K98((() . ())) is V28() V29() ext-real set
K96((() . ()),K98((() . ()))) is V28() V29() ext-real set
f1 is Relation-like REAL -defined REAL -valued V6() V34() V35() V36() Element of K19(K20(REAL,REAL))
f1 + () is Relation-like REAL -defined REAL -valued V6() V34() V35() V36() Element of K19(K20(REAL,REAL))
exp_R / (f1 + ()) is Relation-like REAL -defined REAL -valued V6() V34() V35() V36() Element of K19(K20(REAL,REAL))
f is Relation-like REAL -defined REAL -valued V6() V34() V35() V36() Element of K19(K20(REAL,REAL))
dom f is V55() V56() V57() Element of K19(REAL)
integral (f,A) is V28() V29() ext-real Element of REAL
Z is V55() V56() V57() open Element of K19(REAL)
dom (f1 + ()) is V55() V56() V57() Element of K19(REAL)
is V9() non empty V55() V56() V57() V58() V59() V60() Element of K19(REAL)
(f1 + ()) " is V55() V56() V57() Element of K19(REAL)
(dom (f1 + ())) \ ((f1 + ()) " ) is V55() V56() V57() Element of K19(REAL)
() /\ ((dom (f1 + ())) \ ((f1 + ()) " )) is V55() V56() V57() Element of K19(REAL)
(f1 + ()) ^ is Relation-like REAL -defined REAL -valued V6() V34() V35() V36() Element of K19(K20(REAL,REAL))
dom ((f1 + ()) ^) is V55() V56() V57() Element of K19(REAL)
dom f1 is V55() V56() V57() Element of K19(REAL)
dom () is non empty V55() V56() V57() Element of K19(REAL)
(dom f1) /\ (dom ()) is V55() V56() V57() Element of K19(REAL)

dom () is non empty V55() V56() V57() Element of K19(REAL)
g is V28() V29() ext-real Element of REAL
f1 . g is V28() V29() ext-real Element of REAL
0 * g is V28() V29() ext-real Element of REAL
(0 * g) + 1 is V28() V29() ext-real Element of REAL
g is V28() V29() ext-real Element of REAL
(f1 + ()) . g is V28() V29() ext-real Element of REAL

g is V28() V29() ext-real Element of REAL
exp_R . g is V28() V29() ext-real Element of REAL
g is V28() V29() ext-real Element of REAL
f . g is V28() V29() ext-real Element of REAL
exp_R . g is V28() V29() ext-real Element of REAL
() ^2 is V28() V29() ext-real Element of REAL
K97((),()) is V28() V29() ext-real set
1 + (() ^2) is V28() V29() ext-real Element of REAL
() / (1 + (() ^2)) is V28() V29() ext-real Element of REAL
K99((1 + (() ^2))) is V28() V29() ext-real set
K97((),K99((1 + (() ^2)))) is V28() V29() ext-real set
(exp_R / (f1 + ())) . g is V28() V29() ext-real Element of REAL
(f1 + ()) . g is V28() V29() ext-real Element of REAL
((f1 + ()) . g) " is V28() V29() ext-real Element of REAL
() * (((f1 + ()) . g) ") is V28() V29() ext-real Element of REAL
f1 . g is V28() V29() ext-real Element of REAL
() . g is V28() V29() ext-real Element of REAL
(f1 . g) + (() . g) is V28() V29() ext-real Element of REAL
((f1 . g) + (() . g)) " is V28() V29() ext-real Element of REAL
() * (((f1 . g) + (() . g)) ") is V28() V29() ext-real Element of REAL
(f1 . g) + (() ^2) is V28() V29() ext-real Element of REAL
((f1 . g) + (() ^2)) " is V28() V29() ext-real Element of REAL
() * (((f1 . g) + (() ^2)) ") is V28() V29() ext-real Element of REAL
() `| Z is Relation-like REAL -defined REAL -valued V6() V34() V35() V36() Element of K19(K20(REAL,REAL))
dom (() `| Z) is V55() V56() V57() Element of K19(REAL)
g is V28() V29() ext-real Element of REAL
(() `| Z) . g is V28() V29() ext-real Element of REAL
f . g is V28() V29() ext-real Element of REAL
exp_R . g is V28() V29() ext-real Element of REAL
() ^2 is V28() V29() ext-real Element of REAL
K97((),()) is V28() V29() ext-real set
1 + (() ^2) is V28() V29() ext-real Element of REAL
() / (1 + (() ^2)) is V28() V29() ext-real Element of REAL
K99((1 + (() ^2))) is V28() V29() ext-real set
K97((),K99((1 + (() ^2)))) is V28() V29() ext-real set
- exp_R is Relation-like REAL -defined REAL -valued V6() non empty total V18( REAL , REAL ) V34() V35() V36() Element of K19(K20(REAL,REAL))

A is non empty V55() V56() V57() closed_interval V86() V87() compact closed Element of K19(REAL)
upper_bound A is V28() V29() ext-real Element of REAL
() . () is V28() V29() ext-real Element of REAL
lower_bound A is V28() V29() ext-real Element of REAL
() . () is V28() V29() ext-real Element of REAL
(() . ()) - (() . ()) is V28() V29() ext-real Element of REAL
K98((() . ())) is V28() V29() ext-real set
K96((() . ()),K98((() . ()))) is V28() V29() ext-real set
f1 is Relation-like REAL -defined REAL -valued V6() V34() V35() V36() Element of K19(K20(REAL,REAL))
f1 + () is Relation-like REAL -defined REAL -valued V6() V34() V35() V36() Element of K19(K20(REAL,REAL))
() / (f1 + ()) is Relation-like REAL -defined REAL -valued V6() V34() V35() V36() Element of K19(K20(REAL,REAL))
f is Relation-like REAL -defined REAL -valued V6() V34() V35() V36() Element of K19(K20(REAL,REAL))
dom f is V55() V56() V57() Element of K19(REAL)
integral (f,A) is V28() V29() ext-real Element of REAL
Z is V55() V56() V57() open Element of K19(REAL)
dom () is non empty V55() V56() V57() Element of K19(REAL)
dom (f1 + ()) is V55() V56() V57() Element of K19(REAL)
is V9() non empty V55() V56() V57() V58() V59() V60() Element of K19(REAL)
(f1 + ()) " is V55() V56() V57() Element of K19(REAL)
(dom (f1 + ())) \ ((f1 + ()) " ) is V55() V56() V57() Element of K19(REAL)
(dom ()) /\ ((dom (f1 + ())) \ ((f1 + ()) " )) is V55() V56() V57() Element of K19(REAL)
(f1 + ()) ^ is Relation-like REAL -defined REAL -valued V6() V34() V35() V36() Element of K19(K20(REAL,REAL))
dom ((f1 + ()) ^) is V55() V56() V57() Element of K19(REAL)
dom f1 is V55() V56() V57() Element of K19(REAL)
dom () is non empty V55() V56() V57() Element of K19(REAL)
(dom f1) /\ (dom ()) is V55() V56() V57() Element of K19(REAL)

dom () is non empty V55() V56() V57() Element of K19(REAL)
(- 1) (#) exp_R is Relation-like REAL -defined REAL -valued V6() non empty total V18( REAL , REAL ) V34() V35() V36() Element of K19(K20(REAL,REAL))
g is V28() V29() ext-real Element of REAL
f1 . g is V28() V29() ext-real Element of REAL
0 * g is V28() V29() ext-real Element of REAL
(0 * g) + 1 is V28() V29() ext-real Element of REAL
g is V28() V29() ext-real Element of REAL
(f1 + ()) . g is V28() V29() ext-real Element of REAL

g is V28() V29() ext-real Element of REAL
exp_R . g is V28() V29() ext-real Element of REAL
g is V28() V29() ext-real Element of REAL
f . g is V28() V29() ext-real Element of REAL
exp_R . g is V28() V29() ext-real Element of REAL
() ^2 is V28() V29() ext-real Element of REAL
K97((),()) is V28() V29() ext-real set
1 + (() ^2) is V28() V29() ext-real Element of REAL
() / (1 + (() ^2)) is V28() V29() ext-real Element of REAL
K99((1 + (() ^2))) is V28() V29() ext-real set
K97((),K99((1 + (() ^2)))) is V28() V29() ext-real set
- (() / (1 + (() ^2))) is V28() V29() ext-real Element of REAL
(() / (f1 + ())) . g is V28() V29() ext-real Element of REAL
() . g is V28() V29() ext-real Element of REAL
(f1 + ()) . g is V28() V29() ext-real Element of REAL
((f1 + ()) . g) " is V28() V29() ext-real Element of REAL
(() . g) * (((f1 + ()) . g) ") is V28() V29() ext-real Element of REAL
- () is V28() V29() ext-real Element of REAL
(- ()) * (((f1 + ()) . g) ") is V28() V29() ext-real Element of REAL
f1 . g is V28() V29() ext-real Element of REAL
() . g is V28() V29() ext-real Element of REAL
(f1 . g) + (() . g) is V28() V29() ext-real Element of REAL
((f1 . g) + (() . g)) " is V28() V29() ext-real Element of REAL
(- ()) * (((f1 . g) + (() . g)) ") is V28() V29() ext-real Element of REAL
(f1 . g) + (() ^2) is V28() V29() ext-real Element of REAL
((f1 . g) + (() ^2)) " is V28() V29() ext-real Element of REAL
(- ()) * (((f1 . g) + (() ^2)) ") is V28() V29() ext-real Element of REAL
(- ()) / (1 + (() ^2)) is V28() V29() ext-real Element of REAL
K97((- ()),K99((1 + (() ^2)))) is V28() V29() ext-real set
() `| Z is Relation-like REAL -defined REAL -valued V6() V34() V35() V36() Element of K19(K20(REAL,REAL))
dom (() `| Z) is V55() V56() V57() Element of K19(REAL)
g is V28() V29() ext-real Element of REAL
(() `| Z) . g is V28() V29() ext-real Element of REAL
f . g is V28() V29() ext-real Element of REAL
exp_R . g is V28() V29() ext-real Element of REAL
() ^2 is V28() V29() ext-real Element of REAL
K97((),()) is V28() V29() ext-real set
1 + (() ^2) is V28() V29() ext-real Element of REAL
() / (1 + (() ^2)) is V28() V29() ext-real Element of REAL
K99((1 + (() ^2))) is V28() V29() ext-real set
K97((),K99((1 + (() ^2)))) is V28() V29() ext-real set
- (() / (1 + (() ^2))) is V28() V29() ext-real Element of REAL
exp_R (#) () is Relation-like REAL -defined REAL -valued V6() V34() V35() V36() Element of K19(K20(REAL,REAL))
cos ^2 is Relation-like REAL -defined REAL -valued V6() non empty total V18( REAL , REAL ) V34() V35() V36() Element of K19(K20(REAL,REAL))

exp_R / () is Relation-like REAL -defined REAL -valued V6() V34() V35() V36() Element of K19(K20(REAL,REAL))
(exp_R (#) ()) + (exp_R / ()) is Relation-like REAL -defined REAL -valued V6() V34() V35() V36() Element of K19(K20(REAL,REAL))
A is non empty V55() V56() V57() closed_interval V86() V87() compact closed Element of K19(REAL)
upper_bound A is V28() V29() ext-real Element of REAL
() . () is V28() V29() ext-real Element of REAL
lower_bound A is V28() V29() ext-real Element of REAL
() . () is V28() V29() ext-real Element of REAL
(() . ()) - (() . ()) is V28() V29() ext-real Element of REAL
K98((() . ())) is V28() V29() ext-real set
K96((() . ()),K98((() . ()))) is V28() V29() ext-real set
f1 is Relation-like REAL -defined REAL -valued V6() V34() V35() V36() Element of K19(K20(REAL,REAL))
dom f1 is V55() V56() V57() Element of K19(REAL)
integral (f1,A) is V28() V29() ext-real Element of REAL
f is V55() V56() V57() open Element of K19(REAL)
dom (exp_R (#) ()) is V55() V56() V57() Element of K19(REAL)
dom (exp_R / ()) is V55() V56() V57() Element of K19(REAL)
(dom (exp_R (#) ())) /\ (dom (exp_R / ())) is V55() V56() V57() Element of K19(REAL)
dom () is V55() V56() V57() Element of K19(REAL)
() /\ (dom ()) is V55() V56() V57() Element of K19(REAL)
dom () is non empty V55() V56() V57() Element of K19(REAL)
is V9() non empty V55() V56() V57() V58() V59() V60() Element of K19(REAL)
() " is V55() V56() V57() Element of K19(REAL)
(dom ()) \ (() " ) is V55() V56() V57() Element of K19(REAL)
() /\ ((dom ()) \ (() " )) is V55() V56() V57() Element of K19(REAL)
Z is V28() V29() ext-real Element of REAL
cos . Z is V28() V29() ext-real Element of REAL
Z is V28() V29() ext-real Element of REAL
() . Z is V28() V29() ext-real Element of REAL
() ^ is Relation-like REAL -defined REAL -valued V6() V34() V35() V36() Element of K19(K20(REAL,REAL))
dom (() ^) is V55() V56() V57() Element of K19(REAL)

Z is V28() V29() ext-real Element of REAL
f1 . Z is V28() V29() ext-real Element of REAL
exp_R . Z is V28() V29() ext-real Element of REAL
sin . Z is V28() V29() ext-real Element of REAL
() * (sin . Z) is V28() V29() ext-real Element of REAL
cos . Z is V28() V29() ext-real Element of REAL
(() * (sin . Z)) / (cos . Z) is V28() V29() ext-real Element of REAL
K99((cos . Z)) is V28() V29() ext-real set
K97((() * (sin . Z)),K99((cos . Z))) is V28() V29() ext-real set
(cos . Z) ^2 is V28() V29() ext-real Element of REAL
K97((cos . Z),(cos . Z)) is V28() V29() ext-real set
() / ((cos . Z) ^2) is V28() V29() ext-real Element of REAL
K99(((cos . Z) ^2)) is V28() V29() ext-real set
K97((),K99(((cos . Z) ^2))) is V28() V29() ext-real set
((() * (sin . Z)) / (cos . Z)) + (() / ((cos . Z) ^2)) is V28() V29() ext-real Element of REAL
((exp_R (#) ()) + (exp_R / ())) . Z is V28() V29() ext-real Element of REAL
(exp_R (#) ()) . Z is V28() V29() ext-real Element of REAL
(exp_R / ()) . Z is V28() V29() ext-real Element of REAL
((exp_R (#) ()) . Z) + ((exp_R / ()) . Z) is V28() V29() ext-real Element of REAL
() . Z is V28() V29() ext-real Element of REAL
() * (() . Z) is V28() V29() ext-real Element of REAL
(() * (() . Z)) + ((exp_R / ()) . Z) is V28() V29() ext-real Element of REAL
(cos . Z) " is V28() V29() ext-real Element of REAL
(sin . Z) * ((cos . Z) ") is V28() V29() ext-real Element of REAL
() * ((sin . Z) * ((cos . Z) ")) is V28() V29() ext-real Element of REAL
(() * ((sin . Z) * ((cos . Z) "))) + ((exp_R / ()) . Z) is V28() V29() ext-real Element of REAL
() . Z is V28() V29() ext-real Element of REAL
() / (() . Z) is V28() V29() ext-real Element of REAL
K99((() . Z)) is V28() V29() ext-real set
K97((),K99((() . Z))) is V28() V29() ext-real set
((() * (sin . Z)) / (cos . Z)) + (() / (() . Z)) is V28() V29() ext-real Element of REAL
() `| f is Relation-like REAL -defined REAL -valued V6() V34() V35() V36() Element of K19(K20(REAL,REAL))
dom (() `| f) is V55() V56() V57() Element of K19(REAL)
Z is V28() V29() ext-real Element of REAL
(() `| f) . Z is V28() V29() ext-real Element of REAL
f1 . Z is V28() V29() ext-real Element of REAL
exp_R . Z is V28() V29() ext-real Element of REAL
sin . Z is V28() V29() ext-real Element of REAL
() * (sin . Z) is V28() V29() ext-real Element of REAL
cos . Z is V28() V29() ext-real Element of REAL
(() * (sin . Z)) / (cos . Z) is V28() V29() ext-real Element of REAL
K99((cos . Z)) is V28() V29() ext-real set
K97((() * (sin . Z)),K99((cos . Z))) is V28() V29() ext-real set
(cos . Z) ^2 is V28() V29() ext-real Element of REAL
K97((cos . Z),(cos . Z)) is V28() V29() ext-real set
() / ((cos . Z) ^2) is V28() V29() ext-real Element of REAL
K99(((cos . Z) ^2)) is V28() V29() ext-real set
K97((),K99(((cos . Z) ^2))) is V28() V29() ext-real set
((() * (sin . Z)) / (cos . Z)) + (() / ((cos . Z) ^2)) is V28() V29() ext-real Element of REAL
exp_R (#) () is Relation-like REAL -defined REAL -valued V6() V34() V35() V36() Element of K19(K20(REAL,REAL))
sin ^2 is Relation-like REAL -defined REAL -valued V6() non empty total V18( REAL , REAL ) V34() V35() V36() Element of K19(K20(REAL,REAL))

exp_R / () is Relation-like REAL -defined REAL -valued V6() V34() V35() V36() Element of K19(K20(REAL,REAL))
(exp_R (#) ()) - (exp_R / ()) is Relation-like REAL -defined REAL -valued V6() V34() V35() V36() Element of K19(K20(REAL,REAL))
- (exp_R / ()) is Relation-like REAL -defined V6() V34() V35() V36() set
K98(1) (#) (exp_R / ()) is Relation-like REAL -defined V6() V34() V35() V36() set
(exp_R (#) ()) + (- (exp_R / ())) is Relation-like REAL -defined V6() V34() V35() V36() set
A is non empty V55() V56() V57() closed_interval V86() V87() compact closed Element of K19(REAL)
upper_bound A is V28() V29() ext-real Element of REAL
() . () is V28() V29() ext-real Element of REAL
lower_bound A is V28() V29() ext-real Element of REAL
() . () is V28() V29() ext-real Element of REAL
(() . ()) - (() . ()) is V28() V29() ext-real Element of REAL
K98((() . ())) is V28() V29() ext-real set
K96((() . ()),K98((() . ()))) is V28() V29() ext-real set
f1 is Relation-like REAL -defined REAL -valued V6() V34() V35() V36() Element of K19(K20(REAL,REAL))
dom f1 is V55() V56() V57() Element of K19(REAL)
integral (f1,A) is V28() V29() ext-real Element of REAL
f is V55() V56() V57() open Element of K19(REAL)
dom (exp_R (#) ()) is V55() V56() V57() Element of K19(REAL)
dom (exp_R / ()) is V55() V56() V57() Element of K19(REAL)
(dom (exp_R (#) ())) /\ (dom (exp_R / ())) is V55() V56() V57() Element of K19(REAL)
dom () is V55() V56() V57() Element of K19(REAL)
() /\ (dom ()) is V55() V56() V57() Element of K19(REAL)
dom () is non empty V55() V56() V57() Element of K19(REAL)
is V9() non empty V55() V56() V57() V58() V59() V60() Element of K19(REAL)
() " is V55() V56() V57() Element of K19(REAL)
(dom ()) \ (() " ) is V55() V56() V57() Element of K19(REAL)
() /\ ((dom ()) \ (() " )) is V55() V56() V57() Element of K19(REAL)
Z is V28() V29() ext-real Element of REAL
sin . Z is V28() V29() ext-real Element of REAL
Z is V28() V29() ext-real Element of REAL
() . Z is V28() V29() ext-real Element of REAL
() ^ is Relation-like REAL -defined REAL -valued V6() V34() V35() V36() Element of K19(K20(REAL,REAL))
dom (() ^) is V55() V56() V57() Element of K19(REAL)

Z is V28() V29() ext-real Element of REAL
f1 . Z is V28() V29() ext-real Element of REAL
exp_R . Z is V28() V29() ext-real Element of REAL
cos . Z is V28() V29() ext-real Element of REAL
() * (cos . Z) is V28() V29() ext-real Element of REAL
sin . Z is V28() V29() ext-real Element of REAL
(() * (cos . Z)) / (sin . Z) is V28() V29() ext-real Element of REAL
K99((sin . Z)) is V28() V29() ext-real set
K97((() * (cos . Z)),K99((sin . Z))) is V28() V29() ext-real set
(sin . Z) ^2 is V28() V29() ext-real Element of REAL
K97((sin . Z),(sin . Z)) is V28() V29() ext-real set
() / ((sin . Z) ^2) is V28() V29() ext-real Element of REAL
K99(((sin . Z) ^2)) is V28() V29() ext-real set
K97((),K99(((sin . Z) ^2))) is V28() V29() ext-real set
((() * (cos . Z)) / (sin . Z)) - (() / ((sin . Z) ^2)) is V28() V29() ext-real Element of REAL
K98((() / ((sin . Z) ^2))) is V28() V29() ext-real set
K96(((() * (cos . Z)) / (sin . Z)),K98((() / ((sin . Z) ^2)))) is V28() V29() ext-real set
((exp_R (#) ()) - (exp_R / ())) . Z is V28() V29() ext-real Element of REAL
(exp_R (#) ()) . Z is V28() V29() ext-real Element of REAL
(exp_R / ()) . Z is V28() V29() ext-real Element of REAL
((exp_R (#) ()) . Z) - ((exp_R / ()) . Z) is V28() V29() ext-real Element of REAL
K98(((exp_R / ()) . Z)) is V28() V29() ext-real set
K96(((exp_R (#) ()) . Z),K98(((exp_R / ()) . Z))) is V28() V29() ext-real set
() . Z is V28() V29() ext-real Element of REAL
() * (() . Z) is V28() V29() ext-real Element of REAL
(() * (() . Z)) - ((exp_R / ()) . Z) is V28() V29() ext-real Element of REAL
K96((() * (() . Z)),K98(((exp_R / ()) . Z))) is V28() V29() ext-real set
(sin . Z) " is V28() V29() ext-real Element of REAL
(cos . Z) * ((sin . Z) ") is V28() V29() ext-real Element of REAL
() * ((cos . Z) * ((sin . Z) ")) is V28() V29() ext-real Element of REAL
(() * ((cos . Z) * ((sin . Z) "))) - ((exp_R / ()) . Z) is V28() V29() ext-real Element of REAL
K96((() * ((cos . Z) * ((sin . Z) "))),K98(((exp_R / ()) . Z))) is V28() V29() ext-real set
() . Z is V28() V29() ext-real Element of REAL
() / (() . Z) is V28() V29() ext-real Element of REAL
K99((() . Z)) is V28() V29() ext-real set
K97((),K99((() . Z))) is V28() V29() ext-real set
((() * (cos . Z)) / (sin . Z)) - (() / (() . Z)) is V28() V29() ext-real Element of REAL
K98((() / (() . Z))) is V28() V29() ext-real set
K96(((() * (cos . Z)) / (sin . Z)),K98((() / (() . Z)))) is V28() V29() ext-real set
() `| f is Relation-like REAL -defined REAL -valued V6() V34() V35() V36() Element of K19(K20(REAL,REAL))
dom (() `| f) is V55() V56() V57() Element of K19(REAL)
Z is V28() V29() ext-real Element of REAL
(() `| f) . Z is V28() V29() ext-real Element of REAL
f1 . Z is V28() V29() ext-real Element of REAL
exp_R . Z is V28() V29() ext-real Element of REAL
cos . Z is V28() V29() ext-real Element of REAL
() * (cos . Z) is V28() V29() ext-real Element of REAL
sin . Z is V28() V29() ext-real Element of REAL
(() * (cos . Z)) / (sin . Z) is V28() V29() ext-real Element of REAL
K99((sin . Z)) is V28() V29() ext-real set
K97((() * (cos . Z)),K99((sin . Z))) is V28() V29() ext-real set
(sin . Z) ^2 is V28() V29() ext-real Element of REAL
K97((sin . Z),(sin . Z)) is V28() V29() ext-real set
() / ((sin . Z) ^2) is V28() V29() ext-real Element of REAL
K99(((sin . Z) ^2)) is V28() V29() ext-real set
K97((),K99(((sin . Z) ^2))) is V28() V29() ext-real set
((() * (cos . Z)) / (sin . Z)) - (() / ((sin . Z) ^2)) is V28() V29() ext-real Element of REAL
K98((() / ((sin . Z) ^2))) is V28() V29() ext-real set
K96(((() * (cos . Z)) / (sin . Z)),K98((() / ((sin . Z) ^2)))) is V28() V29() ext-real set
A is non empty V55() V56() V57() closed_interval V86() V87() compact closed Element of K19(REAL)
upper_bound A is V28() V29() ext-real Element of REAL
() . () is V28() V29() ext-real Element of REAL
lower_bound A is V28() V29() ext-real Element of REAL
() . () is V28() V29() ext-real Element of REAL
(() . ()) - (() . ()) is V28() V29() ext-real Element of REAL
K98((() . ())) is V28() V29() ext-real set
K96((() . ()),K98((() . ()))) is V28() V29() ext-real set
f1 is Relation-like REAL -defined REAL -valued V6() V34() V35() V36() Element of K19(K20(REAL,REAL))
f1 + (#Z 2) is Relation-like REAL -defined REAL -valued V6() V34() V35() V36() Element of K19(K20(REAL,REAL))
exp_R / (f1 + (#Z 2)) is Relation-like REAL -defined REAL -valued V6() V34() V35() V36() Element of K19(K20(REAL,REAL))
() + (exp_R / (f1 + (#Z 2))) is Relation-like REAL -defined REAL -valued V6() V34() V35() V36() Element of K19(K20(REAL,REAL))
f is Relation-like REAL -defined REAL -valued V6() V34() V35() V36() Element of K19(K20(REAL,REAL))
dom f is V55() V56() V57() Element of K19(REAL)
integral (f,A) is V28() V29() ext-real Element of REAL
Z is V55() V56() V57() open Element of K19(REAL)
dom () is V55() V56() V57() Element of K19(REAL)
dom (exp_R / (f1 + (#Z 2))) is V55() V56() V57() Element of K19(REAL)
() /\ (dom (exp_R / (f1 + (#Z 2)))) is V55() V56() V57() Element of K19(REAL)
(f1 + (#Z 2)) ^ is Relation-like REAL -defined REAL -valued V6() V34() V35() V36() Element of K19(K20(