:: FDIFF_9 semantic presentation

REAL is V1() V62() V63() V64() V68() V70() set
NAT is V1() V4() V5() V6() V62() V63() V64() V65() V66() V67() V68() Element of K6(REAL)
K6(REAL) is set
K7(REAL,REAL) is V52() V53() V54() set
K6(K7(REAL,REAL)) is set
PFuncs (REAL,REAL) is set
K7(NAT,(PFuncs (REAL,REAL))) is set
K6(K7(NAT,(PFuncs (REAL,REAL)))) is set
K7(NAT,REAL) is V52() V53() V54() set
K6(K7(NAT,REAL)) is set
COMPLEX is V1() V62() V68() V70() set
K7(NAT,COMPLEX) is V52() set
K6(K7(NAT,COMPLEX)) is set
K7(COMPLEX,COMPLEX) is V52() set
K6(K7(COMPLEX,COMPLEX)) is set
0 is V1() V4() V5() V6() V8() V9() V10() V11() V12() ext-real non positive non negative V47() V62() V63() V64() V65() V66() V67() V68() set
1 is V1() V4() V5() V6() V10() V11() V12() ext-real positive non negative V47() V62() V63() V64() V65() V66() V67() V69() Element of NAT
{0,1} is V1() V62() V63() V64() V65() V66() V67() set
INT is V1() V62() V63() V64() V65() V66() V68() V70() set
RAT is V1() V62() V63() V64() V65() V68() V70() set
NAT is V1() V4() V5() V6() V62() V63() V64() V65() V66() V67() V68() set
K6(NAT) is set
K6(NAT) is set
0 is V1() V4() V5() V6() V8() V9() V10() V11() V12() ext-real non positive non negative V47() V62() V63() V64() V65() V66() V67() V68() V69() Element of NAT
ln is V13() V16( REAL ) V17( REAL ) V18() V52() V53() V54() Element of K6(K7(REAL,REAL))
exp_R is V13() V16( REAL ) V17( REAL ) V18() V27( REAL , REAL ) V52() V53() V54() Element of K6(K7(REAL,REAL))
exp_R " is V13() V16( REAL ) V17( REAL ) V18() V52() V53() V54() Element of K6(K7(REAL,REAL))
dom ln is V62() V63() V64() Element of K6(REAL)
right_open_halfline 0 is V62() V63() V64() Element of K6(REAL)
+infty is V1() V12() ext-real positive non negative set
K158(0,+infty) is set
rng ln is V62() V63() V64() Element of K6(REAL)
2 is V1() V4() V5() V6() V10() V11() V12() ext-real positive non negative V47() V62() V63() V64() V65() V66() V67() V69() Element of NAT
cos is V13() V16( REAL ) V17( REAL ) V18() V27( REAL , REAL ) V52() V53() V54() Element of K6(K7(REAL,REAL))
sin is V13() V16( REAL ) V17( REAL ) V18() V27( REAL , REAL ) V52() V53() V54() Element of K6(K7(REAL,REAL))
sin / cos is V13() V16( REAL ) V17( REAL ) V18() V52() V53() V54() Element of K6(K7(REAL,REAL))
cos / sin is V13() V16( REAL ) V17( REAL ) V18() V52() V53() V54() Element of K6(K7(REAL,REAL))
#Z 2 is V13() V16( REAL ) V17( REAL ) V18() V27( REAL , REAL ) V52() V53() V54() Element of K6(K7(REAL,REAL))
cos ^ is V13() V16( REAL ) V17( REAL ) V18() V52() V53() V54() Element of K6(K7(REAL,REAL))
sin ^ is V13() V16( REAL ) V17( REAL ) V18() V52() V53() V54() Element of K6(K7(REAL,REAL))
{0} is V1() V62() V63() V64() V65() V66() V67() set
tan is V13() V16( REAL ) V17( REAL ) V18() V52() V53() V54() Element of K6(K7(REAL,REAL))
dom tan is V62() V63() V64() Element of K6(REAL)
cot is V13() V16( REAL ) V17( REAL ) V18() V52() V53() V54() Element of K6(K7(REAL,REAL))
dom cot is V62() V63() V64() Element of K6(REAL)
() is V13() V16( REAL ) V17( REAL ) V18() V52() V53() V54() Element of K6(K7(REAL,REAL))
() is V13() V16( REAL ) V17( REAL ) V18() V52() V53() V54() Element of K6(K7(REAL,REAL))
Z is V11() V12() ext-real Element of REAL
cos . Z is V11() V12() ext-real Element of REAL
diff ((),Z) is V11() V12() ext-real Element of REAL
sin . Z is V11() V12() ext-real Element of REAL
(cos . Z) ^2 is V11() V12() ext-real Element of REAL
K37((cos . Z),(cos . Z)) is V11() V12() ext-real set
(sin . Z) / ((cos . Z) ^2) is V11() V12() ext-real Element of REAL
K39(((cos . Z) ^2)) is V11() V12() ext-real set
K37((sin . Z),K39(((cos . Z) ^2))) is V11() V12() ext-real set
diff ((cos ^),Z) is V11() V12() ext-real Element of REAL
diff (cos,Z) is V11() V12() ext-real Element of REAL
(diff (cos,Z)) / ((cos . Z) ^2) is V11() V12() ext-real Element of REAL
K37((diff (cos,Z)),K39(((cos . Z) ^2))) is V11() V12() ext-real set
- ((diff (cos,Z)) / ((cos . Z) ^2)) is V11() V12() ext-real Element of REAL
- (sin . Z) is V11() V12() ext-real Element of REAL
(- (sin . Z)) / ((cos . Z) ^2) is V11() V12() ext-real Element of REAL
K37((- (sin . Z)),K39(((cos . Z) ^2))) is V11() V12() ext-real set
- ((- (sin . Z)) / ((cos . Z) ^2)) is V11() V12() ext-real Element of REAL
Z is V11() V12() ext-real Element of REAL
sin . Z is V11() V12() ext-real Element of REAL
diff ((),Z) is V11() V12() ext-real Element of REAL
cos . Z is V11() V12() ext-real Element of REAL
(sin . Z) ^2 is V11() V12() ext-real Element of REAL
K37((sin . Z),(sin . Z)) is V11() V12() ext-real set
(cos . Z) / ((sin . Z) ^2) is V11() V12() ext-real Element of REAL
K39(((sin . Z) ^2)) is V11() V12() ext-real set
K37((cos . Z),K39(((sin . Z) ^2))) is V11() V12() ext-real set
- ((cos . Z) / ((sin . Z) ^2)) is V11() V12() ext-real Element of REAL
diff ((sin ^),Z) is V11() V12() ext-real Element of REAL
diff (sin,Z) is V11() V12() ext-real Element of REAL
(diff (sin,Z)) / ((sin . Z) ^2) is V11() V12() ext-real Element of REAL
K37((diff (sin,Z)),K39(((sin . Z) ^2))) is V11() V12() ext-real set
- ((diff (sin,Z)) / ((sin . Z) ^2)) is V11() V12() ext-real Element of REAL
Z is V11() V12() ext-real Element of REAL
1 / Z is V11() V12() ext-real Element of REAL
K39(Z) is V11() V12() ext-real set
K37(1,K39(Z)) is V11() V12() ext-real set
x is V4() V5() V6() V10() V11() V12() ext-real V47() set
(1 / Z) #Z x is V11() V12() ext-real Element of REAL
Z #Z x is V11() V12() ext-real Element of REAL
1 / (Z #Z x) is V11() V12() ext-real Element of REAL
K39((Z #Z x)) is V11() V12() ext-real set
K37(1,K39((Z #Z x))) is V11() V12() ext-real set
(1 / Z) |^ x is V11() V12() ext-real Element of REAL
Z |^ x is V11() V12() ext-real Element of REAL
1 / (Z |^ x) is V11() V12() ext-real Element of REAL
K39((Z |^ x)) is V11() V12() ext-real set
K37(1,K39((Z |^ x))) is V11() V12() ext-real set
dom () is V62() V63() V64() Element of K6(REAL)
Z is open V62() V63() V64() Element of K6(REAL)
() `| Z is V13() V16( REAL ) V17( REAL ) V18() V52() V53() V54() Element of K6(K7(REAL,REAL))
x is V11() V12() ext-real Element of REAL
cos . x is V11() V12() ext-real Element of REAL
x is V11() V12() ext-real Element of REAL
(() `| Z) . x is V11() V12() ext-real Element of REAL
sin . x is V11() V12() ext-real Element of REAL
cos . x is V11() V12() ext-real Element of REAL
(cos . x) ^2 is V11() V12() ext-real Element of REAL
K37((cos . x),(cos . x)) is V11() V12() ext-real set
(sin . x) / ((cos . x) ^2) is V11() V12() ext-real Element of REAL
K39(((cos . x) ^2)) is V11() V12() ext-real set
K37((sin . x),K39(((cos . x) ^2))) is V11() V12() ext-real set
dom () is V62() V63() V64() Element of K6(REAL)
Z is open V62() V63() V64() Element of K6(REAL)
() `| Z is V13() V16( REAL ) V17( REAL ) V18() V52() V53() V54() Element of K6(K7(REAL,REAL))
x is V11() V12() ext-real Element of REAL
sin . x is V11() V12() ext-real Element of REAL
x is V11() V12() ext-real Element of REAL
(() `| Z) . x is V11() V12() ext-real Element of REAL
cos . x is V11() V12() ext-real Element of REAL
sin . x is V11() V12() ext-real Element of REAL
(sin . x) ^2 is V11() V12() ext-real Element of REAL
K37((sin . x),(sin . x)) is V11() V12() ext-real set
(cos . x) / ((sin . x) ^2) is V11() V12() ext-real Element of REAL
K39(((sin . x) ^2)) is V11() V12() ext-real set
K37((cos . x),K39(((sin . x) ^2))) is V11() V12() ext-real set
- ((cos . x) / ((sin . x) ^2)) is V11() V12() ext-real Element of REAL
Z is V11() V12() ext-real Element of REAL
x is V11() V12() ext-real Element of REAL
x is open V62() V63() V64() Element of K6(REAL)
f is V13() V16( REAL ) V17( REAL ) V18() V52() V53() V54() Element of K6(K7(REAL,REAL))
() * f is V13() V16( REAL ) V17( REAL ) V18() V52() V53() V54() Element of K6(K7(REAL,REAL))
dom (() * f) is V62() V63() V64() Element of K6(REAL)
(() * f) `| x is V13() V16( REAL ) V17( REAL ) V18() V52() V53() V54() Element of K6(K7(REAL,REAL))
dom f is V62() V63() V64() Element of K6(REAL)
x is V11() V12() ext-real Element of REAL
f . x is V11() V12() ext-real Element of REAL
cos . (f . x) is V11() V12() ext-real Element of REAL
x is V11() V12() ext-real Element of REAL
f . x is V11() V12() ext-real Element of REAL
cos . (f . x) is V11() V12() ext-real Element of REAL
x is V11() V12() ext-real Element of REAL
((() * f) `| x) . x is V11() V12() ext-real Element of REAL
Z * x is V11() V12() ext-real Element of REAL
(Z * x) + x is V11() V12() ext-real Element of REAL
sin . ((Z * x) + x) is V11() V12() ext-real Element of REAL
Z * (sin . ((Z * x) + x)) is V11() V12() ext-real Element of REAL
cos . ((Z * x) + x) is V11() V12() ext-real Element of REAL
(cos . ((Z * x) + x)) ^2 is V11() V12() ext-real Element of REAL
K37((cos . ((Z * x) + x)),(cos . ((Z * x) + x))) is V11() V12() ext-real set
(Z * (sin . ((Z * x) + x))) / ((cos . ((Z * x) + x)) ^2) is V11() V12() ext-real Element of REAL
K39(((cos . ((Z * x) + x)) ^2)) is V11() V12() ext-real set
K37((Z * (sin . ((Z * x) + x))),K39(((cos . ((Z * x) + x)) ^2))) is V11() V12() ext-real set
f . x is V11() V12() ext-real Element of REAL
cos . (f . x) is V11() V12() ext-real Element of REAL
diff ((() * f),x) is V11() V12() ext-real Element of REAL
diff ((),(f . x)) is V11() V12() ext-real Element of REAL
diff (f,x) is V11() V12() ext-real Element of REAL
(diff ((),(f . x))) * (diff (f,x)) is V11() V12() ext-real Element of REAL
sin . (f . x) is V11() V12() ext-real Element of REAL
(cos . (f . x)) ^2 is V11() V12() ext-real Element of REAL
K37((cos . (f . x)),(cos . (f . x))) is V11() V12() ext-real set
(sin . (f . x)) / ((cos . (f . x)) ^2) is V11() V12() ext-real Element of REAL
K39(((cos . (f . x)) ^2)) is V11() V12() ext-real set
K37((sin . (f . x)),K39(((cos . (f . x)) ^2))) is V11() V12() ext-real set
((sin . (f . x)) / ((cos . (f . x)) ^2)) * (diff (f,x)) is V11() V12() ext-real Element of REAL
(sin . (f . x)) / ((cos . ((Z * x) + x)) ^2) is V11() V12() ext-real Element of REAL
K37((sin . (f . x)),K39(((cos . ((Z * x) + x)) ^2))) is V11() V12() ext-real set
(diff (f,x)) * ((sin . (f . x)) / ((cos . ((Z * x) + x)) ^2)) is V11() V12() ext-real Element of REAL
f `| x is V13() V16( REAL ) V17( REAL ) V18() V52() V53() V54() Element of K6(K7(REAL,REAL))
(f `| x) . x is V11() V12() ext-real Element of REAL
((f `| x) . x) * ((sin . (f . x)) / ((cos . ((Z * x) + x)) ^2)) is V11() V12() ext-real Element of REAL
Z * ((sin . (f . x)) / ((cos . ((Z * x) + x)) ^2)) is V11() V12() ext-real Element of REAL
(sin . ((Z * x) + x)) / ((cos . ((Z * x) + x)) ^2) is V11() V12() ext-real Element of REAL
K37((sin . ((Z * x) + x)),K39(((cos . ((Z * x) + x)) ^2))) is V11() V12() ext-real set
Z * ((sin . ((Z * x) + x)) / ((cos . ((Z * x) + x)) ^2)) is V11() V12() ext-real Element of REAL
x is V11() V12() ext-real Element of REAL
((() * f) `| x) . x is V11() V12() ext-real Element of REAL
Z * x is V11() V12() ext-real Element of REAL
(Z * x) + x is V11() V12() ext-real Element of REAL
sin . ((Z * x) + x) is V11() V12() ext-real Element of REAL
Z * (sin . ((Z * x) + x)) is V11() V12() ext-real Element of REAL
cos . ((Z * x) + x) is V11() V12() ext-real Element of REAL
(cos . ((Z * x) + x)) ^2 is V11() V12() ext-real Element of REAL
K37((cos . ((Z * x) + x)),(cos . ((Z * x) + x))) is V11() V12() ext-real set
(Z * (sin . ((Z * x) + x))) / ((cos . ((Z * x) + x)) ^2) is V11() V12() ext-real Element of REAL
K39(((cos . ((Z * x) + x)) ^2)) is V11() V12() ext-real set
K37((Z * (sin . ((Z * x) + x))),K39(((cos . ((Z * x) + x)) ^2))) is V11() V12() ext-real set
Z is V11() V12() ext-real Element of REAL
x is V11() V12() ext-real Element of REAL
x is open V62() V63() V64() Element of K6(REAL)
f is V13() V16( REAL ) V17( REAL ) V18() V52() V53() V54() Element of K6(K7(REAL,REAL))
() * f is V13() V16( REAL ) V17( REAL ) V18() V52() V53() V54() Element of K6(K7(REAL,REAL))
dom (() * f) is V62() V63() V64() Element of K6(REAL)
(() * f) `| x is V13() V16( REAL ) V17( REAL ) V18() V52() V53() V54() Element of K6(K7(REAL,REAL))
dom f is V62() V63() V64() Element of K6(REAL)
x is V11() V12() ext-real Element of REAL
f . x is V11() V12() ext-real Element of REAL
sin . (f . x) is V11() V12() ext-real Element of REAL
x is V11() V12() ext-real Element of REAL
f . x is V11() V12() ext-real Element of REAL
sin . (f . x) is V11() V12() ext-real Element of REAL
x is V11() V12() ext-real Element of REAL
((() * f) `| x) . x is V11() V12() ext-real Element of REAL
Z * x is V11() V12() ext-real Element of REAL
(Z * x) + x is V11() V12() ext-real Element of REAL
cos . ((Z * x) + x) is V11() V12() ext-real Element of REAL
Z * (cos . ((Z * x) + x)) is V11() V12() ext-real Element of REAL
sin . ((Z * x) + x) is V11() V12() ext-real Element of REAL
(sin . ((Z * x) + x)) ^2 is V11() V12() ext-real Element of REAL
K37((sin . ((Z * x) + x)),(sin . ((Z * x) + x))) is V11() V12() ext-real set
(Z * (cos . ((Z * x) + x))) / ((sin . ((Z * x) + x)) ^2) is V11() V12() ext-real Element of REAL
K39(((sin . ((Z * x) + x)) ^2)) is V11() V12() ext-real set
K37((Z * (cos . ((Z * x) + x))),K39(((sin . ((Z * x) + x)) ^2))) is V11() V12() ext-real set
- ((Z * (cos . ((Z * x) + x))) / ((sin . ((Z * x) + x)) ^2)) is V11() V12() ext-real Element of REAL
f . x is V11() V12() ext-real Element of REAL
sin . (f . x) is V11() V12() ext-real Element of REAL
diff ((() * f),x) is V11() V12() ext-real Element of REAL
diff ((),(f . x)) is V11() V12() ext-real Element of REAL
diff (f,x) is V11() V12() ext-real Element of REAL
(diff ((),(f . x))) * (diff (f,x)) is V11() V12() ext-real Element of REAL
cos . (f . x) is V11() V12() ext-real Element of REAL
(sin . (f . x)) ^2 is V11() V12() ext-real Element of REAL
K37((sin . (f . x)),(sin . (f . x))) is V11() V12() ext-real set
(cos . (f . x)) / ((sin . (f . x)) ^2) is V11() V12() ext-real Element of REAL
K39(((sin . (f . x)) ^2)) is V11() V12() ext-real set
K37((cos . (f . x)),K39(((sin . (f . x)) ^2))) is V11() V12() ext-real set
- ((cos . (f . x)) / ((sin . (f . x)) ^2)) is V11() V12() ext-real Element of REAL
(- ((cos . (f . x)) / ((sin . (f . x)) ^2))) * (diff (f,x)) is V11() V12() ext-real Element of REAL
(cos . (f . x)) / ((sin . ((Z * x) + x)) ^2) is V11() V12() ext-real Element of REAL
K37((cos . (f . x)),K39(((sin . ((Z * x) + x)) ^2))) is V11() V12() ext-real set
- ((cos . (f . x)) / ((sin . ((Z * x) + x)) ^2)) is V11() V12() ext-real Element of REAL
(diff (f,x)) * (- ((cos . (f . x)) / ((sin . ((Z * x) + x)) ^2))) is V11() V12() ext-real Element of REAL
f `| x is V13() V16( REAL ) V17( REAL ) V18() V52() V53() V54() Element of K6(K7(REAL,REAL))
(f `| x) . x is V11() V12() ext-real Element of REAL
((f `| x) . x) * (- ((cos . (f . x)) / ((sin . ((Z * x) + x)) ^2))) is V11() V12() ext-real Element of REAL
Z * (- ((cos . (f . x)) / ((sin . ((Z * x) + x)) ^2))) is V11() V12() ext-real Element of REAL
(cos . ((Z * x) + x)) / ((sin . ((Z * x) + x)) ^2) is V11() V12() ext-real Element of REAL
K37((cos . ((Z * x) + x)),K39(((sin . ((Z * x) + x)) ^2))) is V11() V12() ext-real set
- ((cos . ((Z * x) + x)) / ((sin . ((Z * x) + x)) ^2)) is V11() V12() ext-real Element of REAL
Z * (- ((cos . ((Z * x) + x)) / ((sin . ((Z * x) + x)) ^2))) is V11() V12() ext-real Element of REAL
x is V11() V12() ext-real Element of REAL
((() * f) `| x) . x is V11() V12() ext-real Element of REAL
Z * x is V11() V12() ext-real Element of REAL
(Z * x) + x is V11() V12() ext-real Element of REAL
cos . ((Z * x) + x) is V11() V12() ext-real Element of REAL
Z * (cos . ((Z * x) + x)) is V11() V12() ext-real Element of REAL
sin . ((Z * x) + x) is V11() V12() ext-real Element of REAL
(sin . ((Z * x) + x)) ^2 is V11() V12() ext-real Element of REAL
K37((sin . ((Z * x) + x)),(sin . ((Z * x) + x))) is V11() V12() ext-real set
(Z * (cos . ((Z * x) + x))) / ((sin . ((Z * x) + x)) ^2) is V11() V12() ext-real Element of REAL
K39(((sin . ((Z * x) + x)) ^2)) is V11() V12() ext-real set
K37((Z * (cos . ((Z * x) + x))),K39(((sin . ((Z * x) + x)) ^2))) is V11() V12() ext-real set
- ((Z * (cos . ((Z * x) + x))) / ((sin . ((Z * x) + x)) ^2)) is V11() V12() ext-real Element of REAL
Z is open V62() V63() V64() Element of K6(REAL)
id Z is V13() V16( REAL ) V17( REAL ) V18() V52() V53() V54() Element of K6(K7(REAL,REAL))
(id Z) ^ is V13() V16( REAL ) V17( REAL ) V18() V52() V53() V54() Element of K6(K7(REAL,REAL))
() * ((id Z) ^) is V13() V16( REAL ) V17( REAL ) V18() V52() V53() V54() Element of K6(K7(REAL,REAL))
dom (() * ((id Z) ^)) is V62() V63() V64() Element of K6(REAL)
(() * ((id Z) ^)) `| Z is V13() V16( REAL ) V17( REAL ) V18() V52() V53() V54() Element of K6(K7(REAL,REAL))
dom ((id Z) ^) is V62() V63() V64() Element of K6(REAL)
x is V11() V12() ext-real Element of REAL
((id Z) ^) . x is V11() V12() ext-real Element of REAL
cos . (((id Z) ^) . x) is V11() V12() ext-real Element of REAL
x is V11() V12() ext-real Element of REAL
((id Z) ^) . x is V11() V12() ext-real Element of REAL
cos . (((id Z) ^) . x) is V11() V12() ext-real Element of REAL
x is V11() V12() ext-real Element of REAL
((() * ((id Z) ^)) `| Z) . x is V11() V12() ext-real Element of REAL
1 / x is V11() V12() ext-real Element of REAL
K39(x) is V11() V12() ext-real set
K37(1,K39(x)) is V11() V12() ext-real set
sin . (1 / x) is V11() V12() ext-real Element of REAL
x ^2 is V11() V12() ext-real Element of REAL
K37(x,x) is V11() V12() ext-real set
cos . (1 / x) is V11() V12() ext-real Element of REAL
(cos . (1 / x)) ^2 is V11() V12() ext-real Element of REAL
K37((cos . (1 / x)),(cos . (1 / x))) is V11() V12() ext-real set
(x ^2) * ((cos . (1 / x)) ^2) is V11() V12() ext-real Element of REAL
(sin . (1 / x)) / ((x ^2) * ((cos . (1 / x)) ^2)) is V11() V12() ext-real Element of REAL
K39(((x ^2) * ((cos . (1 / x)) ^2))) is V11() V12() ext-real set
K37((sin . (1 / x)),K39(((x ^2) * ((cos . (1 / x)) ^2)))) is V11() V12() ext-real set
- ((sin . (1 / x)) / ((x ^2) * ((cos . (1 / x)) ^2))) is V11() V12() ext-real Element of REAL
((id Z) ^) . x is V11() V12() ext-real Element of REAL
cos . (((id Z) ^) . x) is V11() V12() ext-real Element of REAL
diff ((() * ((id Z) ^)),x) is V11() V12() ext-real Element of REAL
diff ((),(((id Z) ^) . x)) is V11() V12() ext-real Element of REAL
diff (((id Z) ^),x) is V11() V12() ext-real Element of REAL
(diff ((),(((id Z) ^) . x))) * (diff (((id Z) ^),x)) is V11() V12() ext-real Element of REAL
sin . (((id Z) ^) . x) is V11() V12() ext-real Element of REAL
(cos . (((id Z) ^) . x)) ^2 is V11() V12() ext-real Element of REAL
K37((cos . (((id Z) ^) . x)),(cos . (((id Z) ^) . x))) is V11() V12() ext-real set
(sin . (((id Z) ^) . x)) / ((cos . (((id Z) ^) . x)) ^2) is V11() V12() ext-real Element of REAL
K39(((cos . (((id Z) ^) . x)) ^2)) is V11() V12() ext-real set
K37((sin . (((id Z) ^) . x)),K39(((cos . (((id Z) ^) . x)) ^2))) is V11() V12() ext-real set
((sin . (((id Z) ^) . x)) / ((cos . (((id Z) ^) . x)) ^2)) * (diff (((id Z) ^),x)) is V11() V12() ext-real Element of REAL
(id Z) . x is V11() V12() ext-real Element of REAL
((id Z) . x) " is V11() V12() ext-real Element of REAL
cos . (((id Z) . x) ") is V11() V12() ext-real Element of REAL
(cos . (((id Z) . x) ")) ^2 is V11() V12() ext-real Element of REAL
K37((cos . (((id Z) . x) ")),(cos . (((id Z) . x) "))) is V11() V12() ext-real set
(sin . (((id Z) ^) . x)) / ((cos . (((id Z) . x) ")) ^2) is V11() V12() ext-real Element of REAL
K39(((cos . (((id Z) . x) ")) ^2)) is V11() V12() ext-real set
K37((sin . (((id Z) ^) . x)),K39(((cos . (((id Z) . x) ")) ^2))) is V11() V12() ext-real set
(diff (((id Z) ^),x)) * ((sin . (((id Z) ^) . x)) / ((cos . (((id Z) . x) ")) ^2)) is V11() V12() ext-real Element of REAL
sin . (((id Z) . x) ") is V11() V12() ext-real Element of REAL
(sin . (((id Z) . x) ")) / ((cos . (((id Z) . x) ")) ^2) is V11() V12() ext-real Element of REAL
K37((sin . (((id Z) . x) ")),K39(((cos . (((id Z) . x) ")) ^2))) is V11() V12() ext-real set
(diff (((id Z) ^),x)) * ((sin . (((id Z) . x) ")) / ((cos . (((id Z) . x) ")) ^2)) is V11() V12() ext-real Element of REAL
x " is V11() V12() ext-real Element of REAL
1 * (x ") is V11() V12() ext-real Element of REAL
cos . (1 * (x ")) is V11() V12() ext-real Element of REAL
(cos . (1 * (x "))) ^2 is V11() V12() ext-real Element of REAL
K37((cos . (1 * (x "))),(cos . (1 * (x ")))) is V11() V12() ext-real set
(sin . (((id Z) . x) ")) / ((cos . (1 * (x "))) ^2) is V11() V12() ext-real Element of REAL
K39(((cos . (1 * (x "))) ^2)) is V11() V12() ext-real set
K37((sin . (((id Z) . x) ")),K39(((cos . (1 * (x "))) ^2))) is V11() V12() ext-real set
(diff (((id Z) ^),x)) * ((sin . (((id Z) . x) ")) / ((cos . (1 * (x "))) ^2)) is V11() V12() ext-real Element of REAL
sin . (1 * (x ")) is V11() V12() ext-real Element of REAL
(sin . (1 * (x "))) / ((cos . (1 * (x "))) ^2) is V11() V12() ext-real Element of REAL
K37((sin . (1 * (x "))),K39(((cos . (1 * (x "))) ^2))) is V11() V12() ext-real set
(diff (((id Z) ^),x)) * ((sin . (1 * (x "))) / ((cos . (1 * (x "))) ^2)) is V11() V12() ext-real Element of REAL
((id Z) ^) `| Z is V13() V16( REAL ) V17( REAL ) V18() V52() V53() V54() Element of K6(K7(REAL,REAL))
(((id Z) ^) `| Z) . x is V11() V12() ext-real Element of REAL
((((id Z) ^) `| Z) . x) * ((sin . (1 * (x "))) / ((cos . (1 * (x "))) ^2)) is V11() V12() ext-real Element of REAL
1 / (x ^2) is V11() V12() ext-real Element of REAL
K39((x ^2)) is V11() V12() ext-real set
K37(1,K39((x ^2))) is V11() V12() ext-real set
- (1 / (x ^2)) is V11() V12() ext-real Element of REAL
(- (1 / (x ^2))) * ((sin . (1 * (x "))) / ((cos . (1 * (x "))) ^2)) is V11() V12() ext-real Element of REAL
- 1 is V11() V12() ext-real non positive V47() Element of REAL
(- 1) / (x ^2) is V11() V12() ext-real Element of REAL
K37((- 1),K39((x ^2))) is V11() V12() ext-real set
(sin . (1 / x)) / ((cos . (1 / x)) ^2) is V11() V12() ext-real Element of REAL
K39(((cos . (1 / x)) ^2)) is V11() V12() ext-real set
K37((sin . (1 / x)),K39(((cos . (1 / x)) ^2))) is V11() V12() ext-real set
((- 1) / (x ^2)) * ((sin . (1 / x)) / ((cos . (1 / x)) ^2)) is V11() V12() ext-real Element of REAL
(- 1) * (sin . (1 / x)) is V11() V12() ext-real Element of REAL
((- 1) * (sin . (1 / x))) / ((x ^2) * ((cos . (1 / x)) ^2)) is V11() V12() ext-real Element of REAL
K37(((- 1) * (sin . (1 / x))),K39(((x ^2) * ((cos . (1 / x)) ^2)))) is V11() V12() ext-real set
x is V11() V12() ext-real Element of REAL
((() * ((id Z) ^)) `| Z) . x is V11() V12() ext-real Element of REAL
1 / x is V11() V12() ext-real Element of REAL
K39(x) is V11() V12() ext-real set
K37(1,K39(x)) is V11() V12() ext-real set
sin . (1 / x) is V11() V12() ext-real Element of REAL
x ^2 is V11() V12() ext-real Element of REAL
K37(x,x) is V11() V12() ext-real set
cos . (1 / x) is V11() V12() ext-real Element of REAL
(cos . (1 / x)) ^2 is V11() V12() ext-real Element of REAL
K37((cos . (1 / x)),(cos . (1 / x))) is V11() V12() ext-real set
(x ^2) * ((cos . (1 / x)) ^2) is V11() V12() ext-real Element of REAL
(sin . (1 / x)) / ((x ^2) * ((cos . (1 / x)) ^2)) is V11() V12() ext-real Element of REAL
K39(((x ^2) * ((cos . (1 / x)) ^2))) is V11() V12() ext-real set
K37((sin . (1 / x)),K39(((x ^2) * ((cos . (1 / x)) ^2)))) is V11() V12() ext-real set
- ((sin . (1 / x)) / ((x ^2) * ((cos . (1 / x)) ^2))) is V11() V12() ext-real Element of REAL
Z is open V62() V63() V64() Element of K6(REAL)
id Z is V13() V16( REAL ) V17( REAL ) V18() V52() V53() V54() Element of K6(K7(REAL,REAL))
(id Z) ^ is V13() V16( REAL ) V17( REAL ) V18() V52() V53() V54() Element of K6(K7(REAL,REAL))
() * ((id Z) ^) is V13() V16( REAL ) V17( REAL ) V18() V52() V53() V54() Element of K6(K7(REAL,REAL))
dom (() * ((id Z) ^)) is V62() V63() V64() Element of K6(REAL)
(() * ((id Z) ^)) `| Z is V13() V16( REAL ) V17( REAL ) V18() V52() V53() V54() Element of K6(K7(REAL,REAL))
dom ((id Z) ^) is V62() V63() V64() Element of K6(REAL)
x is V11() V12() ext-real Element of REAL
((id Z) ^) . x is V11() V12() ext-real Element of REAL
sin . (((id Z) ^) . x) is V11() V12() ext-real Element of REAL
x is V11() V12() ext-real Element of REAL
((id Z) ^) . x is V11() V12() ext-real Element of REAL
sin . (((id Z) ^) . x) is V11() V12() ext-real Element of REAL
x is V11() V12() ext-real Element of REAL
((() * ((id Z) ^)) `| Z) . x is V11() V12() ext-real Element of REAL
1 / x is V11() V12() ext-real Element of REAL
K39(x) is V11() V12() ext-real set
K37(1,K39(x)) is V11() V12() ext-real set
cos . (1 / x) is V11() V12() ext-real Element of REAL
x ^2 is V11() V12() ext-real Element of REAL
K37(x,x) is V11() V12() ext-real set
sin . (1 / x) is V11() V12() ext-real Element of REAL
(sin . (1 / x)) ^2 is V11() V12() ext-real Element of REAL
K37((sin . (1 / x)),(sin . (1 / x))) is V11() V12() ext-real set
(x ^2) * ((sin . (1 / x)) ^2) is V11() V12() ext-real Element of REAL
(cos . (1 / x)) / ((x ^2) * ((sin . (1 / x)) ^2)) is V11() V12() ext-real Element of REAL
K39(((x ^2) * ((sin . (1 / x)) ^2))) is V11() V12() ext-real set
K37((cos . (1 / x)),K39(((x ^2) * ((sin . (1 / x)) ^2)))) is V11() V12() ext-real set
((id Z) ^) . x is V11() V12() ext-real Element of REAL
sin . (((id Z) ^) . x) is V11() V12() ext-real Element of REAL
diff ((() * ((id Z) ^)),x) is V11() V12() ext-real Element of REAL
diff ((),(((id Z) ^) . x)) is V11() V12() ext-real Element of REAL
diff (((id Z) ^),x) is V11() V12() ext-real Element of REAL
(diff ((),(((id Z) ^) . x))) * (diff (((id Z) ^),x)) is V11() V12() ext-real Element of REAL
cos . (((id Z) ^) . x) is V11() V12() ext-real Element of REAL
(sin . (((id Z) ^) . x)) ^2 is V11() V12() ext-real Element of REAL
K37((sin . (((id Z) ^) . x)),(sin . (((id Z) ^) . x))) is V11() V12() ext-real set
(cos . (((id Z) ^) . x)) / ((sin . (((id Z) ^) . x)) ^2) is V11() V12() ext-real Element of REAL
K39(((sin . (((id Z) ^) . x)) ^2)) is V11() V12() ext-real set
K37((cos . (((id Z) ^) . x)),K39(((sin . (((id Z) ^) . x)) ^2))) is V11() V12() ext-real set
- ((cos . (((id Z) ^) . x)) / ((sin . (((id Z) ^) . x)) ^2)) is V11() V12() ext-real Element of REAL
(- ((cos . (((id Z) ^) . x)) / ((sin . (((id Z) ^) . x)) ^2))) * (diff (((id Z) ^),x)) is V11() V12() ext-real Element of REAL
(id Z) . x is V11() V12() ext-real Element of REAL
((id Z) . x) " is V11() V12() ext-real Element of REAL
sin . (((id Z) . x) ") is V11() V12() ext-real Element of REAL
(sin . (((id Z) . x) ")) ^2 is V11() V12() ext-real Element of REAL
K37((sin . (((id Z) . x) ")),(sin . (((id Z) . x) "))) is V11() V12() ext-real set
(cos . (((id Z) ^) . x)) / ((sin . (((id Z) . x) ")) ^2) is V11() V12() ext-real Element of REAL
K39(((sin . (((id Z) . x) ")) ^2)) is V11() V12() ext-real set
K37((cos . (((id Z) ^) . x)),K39(((sin . (((id Z) . x) ")) ^2))) is V11() V12() ext-real set
- ((cos . (((id Z) ^) . x)) / ((sin . (((id Z) . x) ")) ^2)) is V11() V12() ext-real Element of REAL
(diff (((id Z) ^),x)) * (- ((cos . (((id Z) ^) . x)) / ((sin . (((id Z) . x) ")) ^2))) is V11() V12() ext-real Element of REAL
cos . (((id Z) . x) ") is V11() V12() ext-real Element of REAL
(cos . (((id Z) . x) ")) / ((sin . (((id Z) . x) ")) ^2) is V11() V12() ext-real Element of REAL
K37((cos . (((id Z) . x) ")),K39(((sin . (((id Z) . x) ")) ^2))) is V11() V12() ext-real set
- ((cos . (((id Z) . x) ")) / ((sin . (((id Z) . x) ")) ^2)) is V11() V12() ext-real Element of REAL
(diff (((id Z) ^),x)) * (- ((cos . (((id Z) . x) ")) / ((sin . (((id Z) . x) ")) ^2))) is V11() V12() ext-real Element of REAL
x " is V11() V12() ext-real Element of REAL
1 * (x ") is V11() V12() ext-real Element of REAL
sin . (1 * (x ")) is V11() V12() ext-real Element of REAL
(sin . (1 * (x "))) ^2 is V11() V12() ext-real Element of REAL
K37((sin . (1 * (x "))),(sin . (1 * (x ")))) is V11() V12() ext-real set
(cos . (((id Z) . x) ")) / ((sin . (1 * (x "))) ^2) is V11() V12() ext-real Element of REAL
K39(((sin . (1 * (x "))) ^2)) is V11() V12() ext-real set
K37((cos . (((id Z) . x) ")),K39(((sin . (1 * (x "))) ^2))) is V11() V12() ext-real set
- ((cos . (((id Z) . x) ")) / ((sin . (1 * (x "))) ^2)) is V11() V12() ext-real Element of REAL
(diff (((id Z) ^),x)) * (- ((cos . (((id Z) . x) ")) / ((sin . (1 * (x "))) ^2))) is V11() V12() ext-real Element of REAL
cos . (1 * (x ")) is V11() V12() ext-real Element of REAL
(cos . (1 * (x "))) / ((sin . (1 * (x "))) ^2) is V11() V12() ext-real Element of REAL
K37((cos . (1 * (x "))),K39(((sin . (1 * (x "))) ^2))) is V11() V12() ext-real set
- ((cos . (1 * (x "))) / ((sin . (1 * (x "))) ^2)) is V11() V12() ext-real Element of REAL
(diff (((id Z) ^),x)) * (- ((cos . (1 * (x "))) / ((sin . (1 * (x "))) ^2))) is V11() V12() ext-real Element of REAL
((id Z) ^) `| Z is V13() V16( REAL ) V17( REAL ) V18() V52() V53() V54() Element of K6(K7(REAL,REAL))
(((id Z) ^) `| Z) . x is V11() V12() ext-real Element of REAL
((((id Z) ^) `| Z) . x) * (- ((cos . (1 * (x "))) / ((sin . (1 * (x "))) ^2))) is V11() V12() ext-real Element of REAL
1 / (x ^2) is V11() V12() ext-real Element of REAL
K39((x ^2)) is V11() V12() ext-real set
K37(1,K39((x ^2))) is V11() V12() ext-real set
- (1 / (x ^2)) is V11() V12() ext-real Element of REAL
(- (1 / (x ^2))) * (- ((cos . (1 * (x "))) / ((sin . (1 * (x "))) ^2))) is V11() V12() ext-real Element of REAL
- 1 is V11() V12() ext-real non positive V47() Element of REAL
(- 1) / (x ^2) is V11() V12() ext-real Element of REAL
K37((- 1),K39((x ^2))) is V11() V12() ext-real set
- (cos . (1 / x)) is V11() V12() ext-real Element of REAL
(- (cos . (1 / x))) / ((sin . (1 / x)) ^2) is V11() V12() ext-real Element of REAL
K39(((sin . (1 / x)) ^2)) is V11() V12() ext-real set
K37((- (cos . (1 / x))),K39(((sin . (1 / x)) ^2))) is V11() V12() ext-real set
((- 1) / (x ^2)) * ((- (cos . (1 / x))) / ((sin . (1 / x)) ^2)) is V11() V12() ext-real Element of REAL
(- 1) * (- (cos . (1 / x))) is V11() V12() ext-real Element of REAL
((- 1) * (- (cos . (1 / x)))) / ((x ^2) * ((sin . (1 / x)) ^2)) is V11() V12() ext-real Element of REAL
K37(((- 1) * (- (cos . (1 / x)))),K39(((x ^2) * ((sin . (1 / x)) ^2)))) is V11() V12() ext-real set
x is V11() V12() ext-real Element of REAL
((() * ((id Z) ^)) `| Z) . x is V11() V12() ext-real Element of REAL
1 / x is V11() V12() ext-real Element of REAL
K39(x) is V11() V12() ext-real set
K37(1,K39(x)) is V11() V12() ext-real set
cos . (1 / x) is V11() V12() ext-real Element of REAL
x ^2 is V11() V12() ext-real Element of REAL
K37(x,x) is V11() V12() ext-real set
sin . (1 / x) is V11() V12() ext-real Element of REAL
(sin . (1 / x)) ^2 is V11() V12() ext-real Element of REAL
K37((sin . (1 / x)),(sin . (1 / x))) is V11() V12() ext-real set
(x ^2) * ((sin . (1 / x)) ^2) is V11() V12() ext-real Element of REAL
(cos . (1 / x)) / ((x ^2) * ((sin . (1 / x)) ^2)) is V11() V12() ext-real Element of REAL
K39(((x ^2) * ((sin . (1 / x)) ^2))) is V11() V12() ext-real set
K37((cos . (1 / x)),K39(((x ^2) * ((sin . (1 / x)) ^2)))) is V11() V12() ext-real set
Z is V11() V12() ext-real Element of REAL
2 * Z is V11() V12() ext-real Element of REAL
x is V11() V12() ext-real Element of REAL
x is V11() V12() ext-real Element of REAL
f is open V62() V63() V64() Element of K6(REAL)
x is V13() V16( REAL ) V17( REAL ) V18() V52() V53() V54() Element of K6(K7(REAL,REAL))
f2 is V13() V16( REAL ) V17( REAL ) V18() V52() V53() V54() Element of K6(K7(REAL,REAL))
Z (#) f2 is V13() V16( REAL ) V17( REAL ) V18() V52() V53() V54() Element of K6(K7(REAL,REAL))
x + (Z (#) f2) is V13() V16( REAL ) V17( REAL ) V18() V52() V53() V54() Element of K6(K7(REAL,REAL))
() * (x + (Z (#) f2)) is V13() V16( REAL ) V17( REAL ) V18() V52() V53() V54() Element of K6(K7(REAL,REAL))
dom (() * (x + (Z (#) f2))) is V62() V63() V64() Element of K6(REAL)
(() * (x + (Z (#) f2))) `| f is V13() V16( REAL ) V17( REAL ) V18() V52() V53() V54() Element of K6(K7(REAL,REAL))
dom (x + (Z (#) f2)) is V62() V63() V64() Element of K6(REAL)
dom x is V62() V63() V64() Element of K6(REAL)
dom (Z (#) f2) is V62() V63() V64() Element of K6(REAL)
(dom x) /\ (dom (Z (#) f2)) is V62() V63() V64() Element of K6(REAL)
x is V11() V12() ext-real Element of REAL
(x + (Z (#) f2)) . x is V11() V12() ext-real Element of REAL
cos . ((x + (Z (#) f2)) . x) is V11() V12() ext-real Element of REAL
x is V11() V12() ext-real Element of REAL
(x + (Z (#) f2)) . x is V11() V12() ext-real Element of REAL
cos . ((x + (Z (#) f2)) . x) is V11() V12() ext-real Element of REAL
x is V11() V12() ext-real Element of REAL
((() * (x + (Z (#) f2))) `| f) . x is V11() V12() ext-real Element of REAL
(2 * Z) * x is V11() V12() ext-real Element of REAL
x + ((2 * Z) * x) is V11() V12() ext-real Element of REAL
x * x is V11() V12() ext-real Element of REAL
x + (x * x) is V11() V12() ext-real Element of REAL
x ^2 is V11() V12() ext-real Element of REAL
K37(x,x) is V11() V12() ext-real set
Z * (x ^2) is V11() V12() ext-real Element of REAL
(x + (x * x)) + (Z * (x ^2)) is V11() V12() ext-real Element of REAL
sin . ((x + (x * x)) + (Z * (x ^2))) is V11() V12() ext-real Element of REAL
(x + ((2 * Z) * x)) * (sin . ((x + (x * x)) + (Z * (x ^2)))) is V11() V12() ext-real Element of REAL
cos . ((x + (x * x)) + (Z * (x ^2))) is V11() V12() ext-real Element of REAL
(cos . ((x + (x * x)) + (Z * (x ^2)))) ^2 is V11() V12() ext-real Element of REAL
K37((cos . ((x + (x * x)) + (Z * (x ^2)))),(cos . ((x + (x * x)) + (Z * (x ^2))))) is V11() V12() ext-real set
((x + ((2 * Z) * x)) * (sin . ((x + (x * x)) + (Z * (x ^2))))) / ((cos . ((x + (x * x)) + (Z * (x ^2)))) ^2) is V11() V12() ext-real Element of REAL
K39(((cos . ((x + (x * x)) + (Z * (x ^2)))) ^2)) is V11() V12() ext-real set
K37(((x + ((2 * Z) * x)) * (sin . ((x + (x * x)) + (Z * (x ^2))))),K39(((cos . ((x + (x * x)) + (Z * (x ^2)))) ^2))) is V11() V12() ext-real set
(x + (Z (#) f2)) . x is V11() V12() ext-real Element of REAL
x . x is V11() V12() ext-real Element of REAL
(Z (#) f2) . x is V11() V12() ext-real Element of REAL
(x . x) + ((Z (#) f2) . x) is V11() V12() ext-real Element of REAL
f2 . x is V11() V12() ext-real Element of REAL
Z * (f2 . x) is V11() V12() ext-real Element of REAL
(x . x) + (Z * (f2 . x)) is V11() V12() ext-real Element of REAL
(x + (x * x)) + (Z * (f2 . x)) is V11() V12() ext-real Element of REAL
x #Z 2 is V11() V12() ext-real Element of REAL
Z * (x #Z 2) is V11() V12() ext-real Element of REAL
(x + (x * x)) + (Z * (x #Z 2)) is V11() V12() ext-real Element of REAL
x |^ 2 is V11() V12() ext-real Element of REAL
Z * (x |^ 2) is V11() V12() ext-real Element of REAL
(x + (x * x)) + (Z * (x |^ 2)) is V11() V12() ext-real Element of REAL
cos . ((x + (Z (#) f2)) . x) is V11() V12() ext-real Element of REAL
diff ((() * (x + (Z (#) f2))),x) is V11() V12() ext-real Element of REAL
diff ((),((x + (Z (#) f2)) . x)) is V11() V12() ext-real Element of REAL
diff ((x + (Z (#) f2)),x) is V11() V12() ext-real Element of REAL
(diff ((),((x + (Z (#) f2)) . x))) * (diff ((x + (Z (#) f2)),x)) is V11() V12() ext-real Element of REAL
sin . ((x + (Z (#) f2)) . x) is V11() V12() ext-real Element of REAL
(cos . ((x + (Z (#) f2)) . x)) ^2 is V11() V12() ext-real Element of REAL
K37((cos . ((x + (Z (#) f2)) . x)),(cos . ((x + (Z (#) f2)) . x))) is V11() V12() ext-real set
(sin . ((x + (Z (#) f2)) . x)) / ((cos . ((x + (Z (#) f2)) . x)) ^2) is V11() V12() ext-real Element of REAL
K39(((cos . ((x + (Z (#) f2)) . x)) ^2)) is V11() V12() ext-real set
K37((sin . ((x + (Z (#) f2)) . x)),K39(((cos . ((x + (Z (#) f2)) . x)) ^2))) is V11() V12() ext-real set
((sin . ((x + (Z (#) f2)) . x)) / ((cos . ((x + (Z (#) f2)) . x)) ^2)) * (diff ((x + (Z (#) f2)),x)) is V11() V12() ext-real Element of REAL
(x + (Z (#) f2)) `| f is V13() V16( REAL ) V17( REAL ) V18() V52() V53() V54() Element of K6(K7(REAL,REAL))
((x + (Z (#) f2)) `| f) . x is V11() V12() ext-real Element of REAL
(sin . ((x + (x * x)) + (Z * (x ^2)))) / ((cos . ((x + (x * x)) + (Z * (x ^2)))) ^2) is V11() V12() ext-real Element of REAL
K37((sin . ((x + (x * x)) + (Z * (x ^2)))),K39(((cos . ((x + (x * x)) + (Z * (x ^2)))) ^2))) is V11() V12() ext-real set
(((x + (Z (#) f2)) `| f) . x) * ((sin . ((x + (x * x)) + (Z * (x ^2)))) / ((cos . ((x + (x * x)) + (Z * (x ^2)))) ^2)) is V11() V12() ext-real Element of REAL
(x + ((2 * Z) * x)) * ((sin . ((x + (x * x)) + (Z * (x ^2)))) / ((cos . ((x + (x * x)) + (Z * (x ^2)))) ^2)) is V11() V12() ext-real Element of REAL
x is V11() V12() ext-real Element of REAL
((() * (x + (Z (#) f2))) `| f) . x is V11() V12() ext-real Element of REAL
(2 * Z) * x is V11() V12() ext-real Element of REAL
x + ((2 * Z) * x) is V11() V12() ext-real Element of REAL
x * x is V11() V12() ext-real Element of REAL
x + (x * x) is V11() V12() ext-real Element of REAL
x ^2 is V11() V12() ext-real Element of REAL
K37(x,x) is V11() V12() ext-real set
Z * (x ^2) is V11() V12() ext-real Element of REAL
(x + (x * x)) + (Z * (x ^2)) is V11() V12() ext-real Element of REAL
sin . ((x + (x * x)) + (Z * (x ^2))) is V11() V12() ext-real Element of REAL
(x + ((2 * Z) * x)) * (sin . ((x + (x * x)) + (Z * (x ^2)))) is V11() V12() ext-real Element of REAL
cos . ((x + (x * x)) + (Z * (x ^2))) is V11() V12() ext-real Element of REAL
(cos . ((x + (x * x)) + (Z * (x ^2)))) ^2 is V11() V12() ext-real Element of REAL
K37((cos . ((x + (x * x)) + (Z * (x ^2)))),(cos . ((x + (x * x)) + (Z * (x ^2))))) is V11() V12() ext-real set
((x + ((2 * Z) * x)) * (sin . ((x + (x * x)) + (Z * (x ^2))))) / ((cos . ((x + (x * x)) + (Z * (x ^2)))) ^2) is V11() V12() ext-real Element of REAL
K39(((cos . ((x + (x * x)) + (Z * (x ^2)))) ^2)) is V11() V12() ext-real set
K37(((x + ((2 * Z) * x)) * (sin . ((x + (x * x)) + (Z * (x ^2))))),K39(((cos . ((x + (x * x)) + (Z * (x ^2)))) ^2))) is V11() V12() ext-real set
Z is V11() V12() ext-real Element of REAL
2 * Z is V11() V12() ext-real Element of REAL
x is V11() V12() ext-real Element of REAL
x is V11() V12() ext-real Element of REAL
f is open V62() V63() V64() Element of K6(REAL)
x is V13() V16( REAL ) V17( REAL ) V18() V52() V53() V54() Element of K6(K7(REAL,REAL))
f2 is V13() V16( REAL ) V17( REAL ) V18() V52() V53() V54() Element of K6(K7(REAL,REAL))
Z (#) f2 is V13() V16( REAL ) V17( REAL ) V18() V52() V53() V54() Element of K6(K7(REAL,REAL))
x + (Z (#) f2) is V13() V16( REAL ) V17( REAL ) V18() V52() V53() V54() Element of K6(K7(REAL,REAL))
() * (x + (Z (#) f2)) is V13() V16( REAL ) V17( REAL ) V18() V52() V53() V54() Element of K6(K7(REAL,REAL))
dom (() * (x + (Z (#) f2))) is V62() V63() V64() Element of K6(REAL)
(() * (x + (Z (#) f2))) `| f is V13() V16( REAL ) V17( REAL ) V18() V52() V53() V54() Element of K6(K7(REAL,REAL))
dom (x + (Z (#) f2)) is V62() V63() V64() Element of K6(REAL)
dom x is V62() V63() V64() Element of K6(REAL)
dom (Z (#) f2) is V62() V63() V64() Element of K6(REAL)
(dom x) /\ (dom (Z (#) f2)) is V62() V63() V64() Element of K6(REAL)
x is V11() V12() ext-real Element of REAL
(x + (Z (#) f2)) . x is V11() V12() ext-real Element of REAL
sin . ((x + (Z (#) f2)) . x) is V11() V12() ext-real Element of REAL
x is V11() V12() ext-real Element of REAL
(x + (Z (#) f2)) . x is V11() V12() ext-real Element of REAL
sin . ((x + (Z (#) f2)) . x) is V11() V12() ext-real Element of REAL
x is V11() V12() ext-real Element of REAL
((() * (x + (Z (#) f2))) `| f) . x is V11() V12() ext-real Element of REAL
(2 * Z) * x is V11() V12() ext-real Element of REAL
x + ((2 * Z) * x) is V11() V12() ext-real Element of REAL
x * x is V11() V12() ext-real Element of REAL
x + (x * x) is V11() V12() ext-real Element of REAL
x ^2 is V11() V12() ext-real Element of REAL
K37(x,x) is V11() V12() ext-real set
Z * (x ^2) is V11() V12() ext-real Element of REAL
(x + (x * x)) + (Z * (x ^2)) is V11() V12() ext-real Element of REAL
cos . ((x + (x * x)) + (Z * (x ^2))) is V11() V12() ext-real Element of REAL
(x + ((2 * Z) * x)) * (cos . ((x + (x * x)) + (Z * (x ^2)))) is V11() V12() ext-real Element of REAL
sin . ((x + (x * x)) + (Z * (x ^2))) is V11() V12() ext-real Element of REAL
(sin . ((x + (x * x)) + (Z * (x ^2)))) ^2 is V11() V12() ext-real Element of REAL
K37((sin . ((x + (x * x)) + (Z * (x ^2)))),(sin . ((x + (x * x)) + (Z * (x ^2))))) is V11() V12() ext-real set
((x + ((2 * Z) * x)) * (cos . ((x + (x * x)) + (Z * (x ^2))))) / ((sin . ((x + (x * x)) + (Z * (x ^2)))) ^2) is V11() V12() ext-real Element of REAL
K39(((sin . ((x + (x * x)) + (Z * (x ^2)))) ^2)) is V11() V12() ext-real set
K37(((x + ((2 * Z) * x)) * (cos . ((x + (x * x)) + (Z * (x ^2))))),K39(((sin . ((x + (x * x)) + (Z * (x ^2)))) ^2))) is V11() V12() ext-real set
- (((x + ((2 * Z) * x)) * (cos . ((x + (x * x)) + (Z * (x ^2))))) / ((sin . ((x + (x * x)) + (Z * (x ^2)))) ^2)) is V11() V12() ext-real Element of REAL
(x + (Z (#) f2)) . x is V11() V12() ext-real Element of REAL
x . x is V11() V12() ext-real Element of REAL
(Z (#) f2) . x is V11() V12() ext-real Element of REAL
(x . x) + ((Z (#) f2) . x) is V11() V12() ext-real Element of REAL
f2 . x is V11() V12() ext-real Element of REAL
Z * (f2 . x) is V11() V12() ext-real Element of REAL
(x . x) + (Z * (f2 . x)) is V11() V12() ext-real Element of REAL
(x + (x * x)) + (Z * (f2 . x)) is V11() V12() ext-real Element of REAL
x #Z 2 is V11() V12() ext-real Element of REAL
Z * (x #Z 2) is V11() V12() ext-real Element of REAL
(x + (x * x)) + (Z * (x #Z 2)) is V11() V12() ext-real Element of REAL
x |^ 2 is V11() V12() ext-real Element of REAL
Z * (x |^ 2) is V11() V12() ext-real Element of REAL
(x + (x * x)) + (Z * (x |^ 2)) is V11() V12() ext-real Element of REAL
sin . ((x + (Z (#) f2)) . x) is V11() V12() ext-real Element of REAL
diff ((() * (x + (Z (#) f2))),x) is V11() V12() ext-real Element of REAL
diff ((),((x + (Z (#) f2)) . x)) is V11() V12() ext-real Element of REAL
diff ((x + (Z (#) f2)),x) is V11() V12() ext-real Element of REAL
(diff ((),((x + (Z (#) f2)) . x))) * (diff ((x + (Z (#) f2)),x)) is V11() V12() ext-real Element of REAL
cos . ((x + (Z (#) f2)) . x) is V11() V12() ext-real Element of REAL
(sin . ((x + (Z (#) f2)) . x)) ^2 is V11() V12() ext-real Element of REAL
K37((sin . ((x + (Z (#) f2)) . x)),(sin . ((x + (Z (#) f2)) . x))) is V11() V12() ext-real set
(cos . ((x + (Z (#) f2)) . x)) / ((sin . ((x + (Z (#) f2)) . x)) ^2) is V11() V12() ext-real Element of REAL
K39(((sin . ((x + (Z (#) f2)) . x)) ^2)) is V11() V12() ext-real set
K37((cos . ((x + (Z (#) f2)) . x)),K39(((sin . ((x + (Z (#) f2)) . x)) ^2))) is V11() V12() ext-real set
- ((cos . ((x + (Z (#) f2)) . x)) / ((sin . ((x + (Z (#) f2)) . x)) ^2)) is V11() V12() ext-real Element of REAL
(- ((cos . ((x + (Z (#) f2)) . x)) / ((sin . ((x + (Z (#) f2)) . x)) ^2))) * (diff ((x + (Z (#) f2)),x)) is V11() V12() ext-real Element of REAL
(x + (Z (#) f2)) `| f is V13() V16( REAL ) V17( REAL ) V18() V52() V53() V54() Element of K6(K7(REAL,REAL))
((x + (Z (#) f2)) `| f) . x is V11() V12() ext-real Element of REAL
(cos . ((x + (x * x)) + (Z * (x ^2)))) / ((sin . ((x + (x * x)) + (Z * (x ^2)))) ^2) is V11() V12() ext-real Element of REAL
K37((cos . ((x + (x * x)) + (Z * (x ^2)))),K39(((sin . ((x + (x * x)) + (Z * (x ^2)))) ^2))) is V11() V12() ext-real set
- ((cos . ((x + (x * x)) + (Z * (x ^2)))) / ((sin . ((x + (x * x)) + (Z * (x ^2)))) ^2)) is V11() V12() ext-real Element of REAL
(((x + (Z (#) f2)) `| f) . x) * (- ((cos . ((x + (x * x)) + (Z * (x ^2)))) / ((sin . ((x + (x * x)) + (Z * (x ^2)))) ^2))) is V11() V12() ext-real Element of REAL
(x + ((2 * Z) * x)) * (- ((cos . ((x + (x * x)) + (Z * (x ^2)))) / ((sin . ((x + (x * x)) + (Z * (x ^2)))) ^2))) is V11() V12() ext-real Element of REAL
x is V11() V12() ext-real Element of REAL
((() * (x + (Z (#) f2))) `| f) . x is V11() V12() ext-real Element of REAL
(2 * Z) * x is V11() V12() ext-real Element of REAL
x + ((2 * Z) * x) is V11() V12() ext-real Element of REAL
x * x is V11() V12() ext-real Element of REAL
x + (x * x) is V11() V12() ext-real Element of REAL
x ^2 is V11() V12() ext-real Element of REAL
K37(x,x) is V11() V12() ext-real set
Z * (x ^2) is V11() V12() ext-real Element of REAL
(x + (x * x)) + (Z * (x ^2)) is V11() V12() ext-real Element of REAL
cos . ((x + (x * x)) + (Z * (x ^2))) is V11() V12() ext-real Element of REAL
(x + ((2 * Z) * x)) * (cos . ((x + (x * x)) + (Z * (x ^2)))) is V11() V12() ext-real Element of REAL
sin . ((x + (x * x)) + (Z * (x ^2))) is V11() V12() ext-real Element of REAL
(sin . ((x + (x * x)) + (Z * (x ^2)))) ^2 is V11() V12() ext-real Element of REAL
K37((sin . ((x + (x * x)) + (Z * (x ^2)))),(sin . ((x + (x * x)) + (Z * (x ^2))))) is V11() V12() ext-real set
((x + ((2 * Z) * x)) * (cos . ((x + (x * x)) + (Z * (x ^2))))) / ((sin . ((x + (x * x)) + (Z * (x ^2)))) ^2) is V11() V12() ext-real Element of REAL
K39(((sin . ((x + (x * x)) + (Z * (x ^2)))) ^2)) is V11() V12() ext-real set
K37(((x + ((2 * Z) * x)) * (cos . ((x + (x * x)) + (Z * (x ^2))))),K39(((sin . ((x + (x * x)) + (Z * (x ^2)))) ^2))) is V11() V12() ext-real set
- (((x + ((2 * Z) * x)) * (cos . ((x + (x * x)) + (Z * (x ^2))))) / ((sin . ((x + (x * x)) + (Z * (x ^2)))) ^2)) is V11() V12() ext-real Element of REAL
() * exp_R is V13() V16( REAL ) V17( REAL ) V18() V52() V53() V54() Element of K6(K7(REAL,REAL))
dom (() * exp_R) is V62() V63() V64() Element of K6(REAL)
Z is open V62() V63() V64() Element of K6(REAL)
(() * exp_R) `| Z is V13() V16( REAL ) V17( REAL ) V18() V52() V53() V54() Element of K6(K7(REAL,REAL))
x is V11() V12() ext-real Element of REAL
exp_R . x is V11() V12() ext-real Element of REAL
cos . (exp_R . x) is V11() V12() ext-real Element of REAL
x is V11() V12() ext-real Element of REAL
exp_R . x is V11() V12() ext-real Element of REAL
cos . (exp_R . x) is V11() V12() ext-real Element of REAL
x is V11() V12() ext-real Element of REAL
((() * exp_R) `| Z) . x is V11() V12() ext-real Element of REAL
exp_R . x is V11() V12() ext-real Element of REAL
sin . (exp_R . x) is V11() V12() ext-real Element of REAL
(exp_R . x) * (sin . (exp_R . x)) is V11() V12() ext-real Element of REAL
cos . (exp_R . x) is V11() V12() ext-real Element of REAL
(cos . (exp_R . x)) ^2 is V11() V12() ext-real Element of REAL
K37((cos . (exp_R . x)),(cos . (exp_R . x))) is V11() V12() ext-real set
((exp_R . x) * (sin . (exp_R . x))) / ((cos . (exp_R . x)) ^2) is V11() V12() ext-real Element of REAL
K39(((cos . (exp_R . x)) ^2)) is V11() V12() ext-real set
K37(((exp_R . x) * (sin . (exp_R . x))),K39(((cos . (exp_R . x)) ^2))) is V11() V12() ext-real set
diff ((() * exp_R),x) is V11() V12() ext-real Element of REAL
diff ((),(exp_R . x)) is V11() V12() ext-real Element of REAL
diff (exp_R,x) is V11() V12() ext-real Element of REAL
(diff ((),(exp_R . x))) * (diff (exp_R,x)) is V11() V12() ext-real Element of REAL
(sin . (exp_R . x)) / ((cos . (exp_R . x)) ^2) is V11() V12() ext-real Element of REAL
K37((sin . (exp_R . x)),K39(((cos . (exp_R . x)) ^2))) is V11() V12() ext-real set
((sin . (exp_R . x)) / ((cos . (exp_R . x)) ^2)) * (diff (exp_R,x)) is V11() V12() ext-real Element of REAL
(exp_R . x) * ((sin . (exp_R . x)) / ((cos . (exp_R . x)) ^2)) is V11() V12() ext-real Element of REAL
x is V11() V12() ext-real Element of REAL
((() * exp_R) `| Z) . x is V11() V12() ext-real Element of REAL
exp_R . x is V11() V12() ext-real Element of REAL
sin . (exp_R . x) is V11() V12() ext-real Element of REAL
(exp_R . x) * (sin . (exp_R . x)) is V11() V12() ext-real Element of REAL
cos . (exp_R . x) is V11() V12() ext-real Element of REAL
(cos . (exp_R . x)) ^2 is V11() V12() ext-real Element of REAL
K37((cos . (exp_R . x)),(cos . (exp_R . x))) is V11() V12() ext-real set
((exp_R . x) * (sin . (exp_R . x))) / ((cos . (exp_R . x)) ^2) is V11() V12() ext-real Element of REAL
K39(((cos . (exp_R . x)) ^2)) is V11() V12() ext-real set
K37(((exp_R . x) * (sin . (exp_R . x))),K39(((cos . (exp_R . x)) ^2))) is V11() V12() ext-real set
() * exp_R is V13() V16( REAL ) V17( REAL ) V18() V52() V53() V54() Element of K6(K7(REAL,REAL))
dom (() * exp_R) is V62() V63() V64() Element of K6(REAL)
Z is open V62() V63() V64() Element of K6(REAL)
(() * exp_R) `| Z is V13() V16( REAL ) V17( REAL ) V18() V52() V53() V54() Element of K6(K7(REAL,REAL))
x is V11() V12() ext-real Element of REAL
exp_R . x is V11() V12() ext-real Element of REAL
sin . (exp_R . x) is V11() V12() ext-real Element of REAL
x is V11() V12() ext-real Element of REAL
exp_R . x is V11() V12() ext-real Element of REAL
sin . (exp_R . x) is V11() V12() ext-real Element of REAL
x is V11() V12() ext-real Element of REAL
((() * exp_R) `| Z) . x is V11() V12() ext-real Element of REAL
exp_R . x is V11() V12() ext-real Element of REAL
cos . (exp_R . x) is V11() V12() ext-real Element of REAL
(exp_R . x) * (cos . (exp_R . x)) is V11() V12() ext-real Element of REAL
sin . (exp_R . x) is V11() V12() ext-real Element of REAL
(sin . (exp_R . x)) ^2 is V11() V12() ext-real Element of REAL
K37((sin . (exp_R . x)),(sin . (exp_R . x))) is V11() V12() ext-real set
((exp_R . x) * (cos . (exp_R . x))) / ((sin . (exp_R . x)) ^2) is V11() V12() ext-real Element of REAL
K39(((sin . (exp_R . x)) ^2)) is V11() V12() ext-real set
K37(((exp_R . x) * (cos . (exp_R . x))),K39(((sin . (exp_R . x)) ^2))) is V11() V12() ext-real set
- (((exp_R . x) * (cos . (exp_R . x))) / ((sin . (exp_R . x)) ^2)) is V11() V12() ext-real Element of REAL
diff ((() * exp_R),x) is V11() V12() ext-real Element of REAL
diff ((),(exp_R . x)) is V11() V12() ext-real Element of REAL
diff (exp_R,x) is V11() V12() ext-real Element of REAL
(diff ((),(exp_R . x))) * (diff (exp_R,x)) is V11() V12() ext-real Element of REAL
(cos . (exp_R . x)) / ((sin . (exp_R . x)) ^2) is V11() V12() ext-real Element of REAL
K37((cos . (exp_R . x)),K39(((sin . (exp_R . x)) ^2))) is V11() V12() ext-real set
- ((cos . (exp_R . x)) / ((sin . (exp_R . x)) ^2)) is V11() V12() ext-real Element of REAL
(- ((cos . (exp_R . x)) / ((sin . (exp_R . x)) ^2))) * (diff (exp_R,x)) is V11() V12() ext-real Element of REAL
(exp_R . x) * (- ((cos . (exp_R . x)) / ((sin . (exp_R . x)) ^2))) is V11() V12() ext-real Element of REAL
x is V11() V12() ext-real Element of REAL
((() * exp_R) `| Z) . x is V11() V12() ext-real Element of REAL
exp_R . x is V11() V12() ext-real Element of REAL
cos . (exp_R . x) is V11() V12() ext-real Element of REAL
(exp_R . x) * (cos . (exp_R . x)) is V11() V12() ext-real Element of REAL
sin . (exp_R . x) is V11() V12() ext-real Element of REAL
(sin . (exp_R . x)) ^2 is V11() V12() ext-real Element of REAL
K37((sin . (exp_R . x)),(sin . (exp_R . x))) is V11() V12() ext-real set
((exp_R . x) * (cos . (exp_R . x))) / ((sin . (exp_R . x)) ^2) is V11() V12() ext-real Element of REAL
K39(((sin . (exp_R . x)) ^2)) is V11() V12() ext-real set
K37(((exp_R . x) * (cos . (exp_R . x))),K39(((sin . (exp_R . x)) ^2))) is V11() V12() ext-real set
- (((exp_R . x) * (cos . (exp_R . x))) / ((sin . (exp_R . x)) ^2)) is V11() V12() ext-real Element of REAL
{ b₁ where b₁ is V11() V12() ext-real Element of REAL : not b₁ <= 0 } is set
() * ln is V13() V16( REAL ) V17( REAL ) V18() V52() V53() V54() Element of K6(K7(REAL,REAL))
dom (() * ln) is V62() V63() V64() Element of K6(REAL)
Z is open V62() V63() V64() Element of K6(REAL)
(() * ln) `| Z is V13() V16( REAL ) V17( REAL ) V18() V52() V53() V54() Element of K6(K7(REAL,REAL))
x is V11() V12() ext-real Element of REAL
x is V11() V12() ext-real Element of REAL
x is V11() V12() ext-real Element of REAL
diff (ln,x) is V11() V12() ext-real Element of REAL
1 / x is V11() V12() ext-real Element of REAL
K39(x) is V11() V12() ext-real set
K37(1,K39(x)) is V11() V12() ext-real set
x is V11() V12() ext-real Element of REAL
ln . x is V11() V12() ext-real Element of REAL
cos . (ln . x) is V11() V12() ext-real Element of REAL
x is V11() V12() ext-real Element of REAL
ln . x is V11() V12() ext-real Element of REAL
cos . (ln . x) is V11() V12() ext-real Element of REAL
x is V11() V12() ext-real Element of REAL
((() * ln) `| Z) . x is V11() V12() ext-real Element of REAL
ln . x is V11() V12() ext-real Element of REAL
sin . (ln . x) is V11() V12() ext-real Element of REAL
cos . (ln . x) is V11() V12() ext-real Element of REAL
(cos . (ln . x)) ^2 is V11() V12() ext-real Element of REAL
K37((cos . (ln . x)),(cos . (ln . x))) is V11() V12() ext-real set
x * ((cos . (ln . x)) ^2) is V11() V12() ext-real Element of REAL
(sin . (ln . x)) / (x * ((cos . (ln . x)) ^2)) is V11() V12() ext-real Element of REAL
K39((x * ((cos . (ln . x)) ^2))) is V11() V12() ext-real set
K37((sin . (ln . x)),K39((x * ((cos . (ln . x)) ^2)))) is V11() V12() ext-real set
diff ((() * ln),x) is V11() V12() ext-real Element of REAL
diff ((),(ln . x)) is V11() V12() ext-real Element of REAL
diff (ln,x) is V11() V12() ext-real Element of REAL
(diff ((),(ln . x))) * (diff (ln,x)) is V11() V12() ext-real Element of REAL
(sin . (ln . x)) / ((cos . (ln . x)) ^2) is V11() V12() ext-real Element of REAL
K39(((cos . (ln . x)) ^2)) is V11() V12() ext-real set
K37((sin . (ln . x)),K39(((cos . (ln . x)) ^2))) is V11() V12() ext-real set
((sin . (ln . x)) / ((cos . (ln . x)) ^2)) * (diff (ln,x)) is V11() V12() ext-real Element of REAL
1 / x is V11() V12() ext-real Element of REAL
K39(x) is V11() V12() ext-real set
K37(1,K39(x)) is V11() V12() ext-real set
(1 / x) * ((sin . (ln . x)) / ((cos . (ln . x)) ^2)) is V11() V12() ext-real Element of REAL
1 * (sin . (ln . x)) is V11() V12() ext-real Element of REAL
(1 * (sin . (ln . x))) / (x * ((cos . (ln . x)) ^2)) is V11() V12() ext-real Element of REAL
K37((1 * (sin . (ln . x))),K39((x * ((cos . (ln . x)) ^2)))) is V11() V12() ext-real set
x is V11() V12() ext-real Element of REAL
((() * ln) `| Z) . x is V11() V12() ext-real Element of REAL
ln . x is V11() V12() ext-real Element of REAL
sin . (ln . x) is V11() V12() ext-real Element of REAL
cos . (ln . x) is V11() V12() ext-real Element of REAL
(cos . (ln . x)) ^2 is V11() V12() ext-real Element of REAL
K37((cos . (ln . x)),(cos . (ln . x))) is V11() V12() ext-real set
x * ((cos . (ln . x)) ^2) is V11() V12() ext-real Element of REAL
(sin . (ln . x)) / (x * ((cos . (ln . x)) ^2)) is V11() V12() ext-real Element of REAL
K39((x * ((cos . (ln . x)) ^2))) is V11() V12() ext-real set
K37((sin . (ln . x)),K39((x * ((cos . (ln . x)) ^2)))) is V11() V12() ext-real set
() * ln is V13() V16( REAL ) V17( REAL ) V18() V52() V53() V54() Element of K6(K7(REAL,REAL))
dom (() * ln) is V62() V63() V64() Element of K6(REAL)
Z is open V62() V63() V64() Element of K6(REAL)
(() * ln) `| Z is V13() V16( REAL ) V17( REAL ) V18() V52() V53() V54() Element of K6(K7(REAL,REAL))
x is V11() V12() ext-real Element of REAL
x is V11() V12() ext-real Element of REAL
x is V11() V12() ext-real Element of REAL
diff (ln,x) is V11() V12() ext-real Element of REAL
1 / x is V11() V12() ext-real Element of REAL
K39(x) is V11() V12() ext-real set
K37(1,K39(x)) is V11() V12() ext-real set
x is V11() V12() ext-real Element of REAL
ln . x is V11() V12() ext-real Element of REAL
sin . (ln . x) is V11() V12() ext-real Element of REAL
x is V11() V12() ext-real Element of REAL
ln . x is V11() V12() ext-real Element of REAL
sin . (ln . x) is V11() V12() ext-real Element of REAL
x is V11() V12() ext-real Element of REAL
((() * ln) `| Z) . x is V11() V12() ext-real Element of REAL
ln . x is V11() V12() ext-real Element of REAL
cos . (ln . x) is V11() V12() ext-real Element of REAL
sin . (ln . x) is V11() V12() ext-real Element of REAL
(sin . (ln . x)) ^2 is V11() V12() ext-real Element of REAL
K37((sin . (ln . x)),(sin . (ln . x))) is V11() V12() ext-real set
x * ((sin . (ln . x)) ^2) is V11() V12() ext-real Element of REAL
(cos . (ln . x)) / (x * ((sin . (ln . x)) ^2)) is V11() V12() ext-real Element of REAL
K39((x * ((sin . (ln . x)) ^2))) is V11() V12() ext-real set
K37((cos . (ln . x)),K39((x * ((sin . (ln . x)) ^2)))) is V11() V12() ext-real set
- ((cos . (ln . x)) / (x * ((sin . (ln . x)) ^2))) is V11() V12() ext-real Element of REAL
diff ((() * ln),x) is V11() V12() ext-real Element of REAL
diff ((),(ln . x)) is V11() V12() ext-real Element of REAL
diff (ln,x) is V11() V12() ext-real Element of REAL
(diff ((),(ln . x))) * (diff (ln,x)) is V11() V12() ext-real Element of REAL
(cos . (ln . x)) / ((sin . (ln . x)) ^2) is V11() V12() ext-real Element of REAL
K39(((sin . (ln . x)) ^2)) is V11() V12() ext-real set
K37((cos . (ln . x)),K39(((sin . (ln . x)) ^2))) is V11() V12() ext-real set
- ((cos . (ln . x)) / ((sin . (ln . x)) ^2)) is V11() V12() ext-real Element of REAL
(- ((cos . (ln . x)) / ((sin . (ln . x)) ^2))) * (diff (ln,x)) is V11() V12() ext-real Element of REAL
1 / x is V11() V12() ext-real Element of REAL
K39(x) is V11() V12() ext-real set
K37(1,K39(x)) is V11() V12() ext-real set
- (cos . (ln . x)) is V11() V12() ext-real Element of REAL
(- (cos . (ln . x))) / ((sin . (ln . x)) ^2) is V11() V12() ext-real Element of REAL
K37((- (cos . (ln . x))),K39(((sin . (ln . x)) ^2))) is V11() V12() ext-real set
(1 / x) * ((- (cos . (ln . x))) / ((sin . (ln . x)) ^2)) is V11() V12() ext-real Element of REAL
1 * (- (cos . (ln . x))) is V11() V12() ext-real Element of REAL
(1 * (- (cos . (ln . x)))) / (x * ((sin . (ln . x)) ^2)) is V11() V12() ext-real Element of REAL
K37((1 * (- (cos . (ln . x)))),K39((x * ((sin . (ln . x)) ^2)))) is V11() V12() ext-real set
x is V11() V12() ext-real Element of REAL
((() * ln) `| Z) . x is V11() V12() ext-real Element of REAL
ln . x is V11() V12() ext-real Element of REAL
cos . (ln . x) is V11() V12() ext-real Element of REAL
sin . (ln . x) is V11() V12() ext-real Element of REAL
(sin . (ln . x)) ^2 is V11() V12() ext-real Element of REAL
K37((sin . (ln . x)),(sin . (ln . x))) is V11() V12() ext-real set
x * ((sin . (ln . x)) ^2) is V11() V12() ext-real Element of REAL
(cos . (ln . x)) / (x * ((sin . (ln . x)) ^2)) is V11() V12() ext-real Element of REAL
K39((x * ((sin . (ln . x)) ^2))) is V11() V12() ext-real set
K37((cos . (ln . x)),K39((x * ((sin . (ln . x)) ^2)))) is V11() V12() ext-real set
- ((cos . (ln . x)) / (x * ((sin . (ln . x)) ^2))) is V11() V12() ext-real Element of REAL
exp_R * () is V13() V16( REAL ) V17( REAL ) V18() V52() V53() V54() Element of K6(K7(REAL,REAL))
dom (exp_R * ()) is V62() V63() V64() Element of K6(REAL)
Z is open V62() V63() V64() Element of K6(REAL)
(exp_R * ()) `| Z is V13() V16( REAL ) V17( REAL ) V18() V52() V53() V54() Element of K6(K7(REAL,REAL))
x is V11() V12() ext-real Element of REAL
cos . x is V11() V12() ext-real Element of REAL
x is V11() V12() ext-real Element of REAL
cos . x is V11() V12() ext-real Element of REAL
() . x is V11() V12() ext-real Element of REAL
x is V11() V12() ext-real Element of REAL
((exp_R * ()) `| Z) . x is V11() V12() ext-real Element of REAL
() . x is V11() V12() ext-real Element of REAL
exp_R . (() . x) is V11() V12() ext-real Element of REAL
sin . x is V11() V12() ext-real Element of REAL
(exp_R . (() . x)) * (sin . x) is V11() V12() ext-real Element of REAL
cos . x is V11() V12() ext-real Element of REAL
(cos . x) ^2 is V11() V12() ext-real Element of REAL
K37((cos . x),(cos . x)) is V11() V12() ext-real set
((exp_R . (() . x)) * (sin . x)) / ((cos . x) ^2) is V11() V12() ext-real Element of REAL
K39(((cos . x) ^2)) is V11() V12() ext-real set
K37(((exp_R . (() . x)) * (sin . x)),K39(((cos . x) ^2))) is V11() V12() ext-real set
diff ((exp_R * ()),x) is V11() V12() ext-real Element of REAL
diff (exp_R,(() . x)) is V11() V12() ext-real Element of REAL
diff ((),x) is V11() V12() ext-real Element of REAL
(diff (exp_R,(() . x))) * (diff ((),x)) is V11() V12() ext-real Element of REAL
(sin . x) / ((cos . x) ^2) is V11() V12() ext-real Element of REAL
K37((sin . x),K39(((cos . x) ^2))) is V11() V12() ext-real set
(diff (exp_R,(() . x))) * ((sin . x) / ((cos . x) ^2)) is V11() V12() ext-real Element of REAL
(exp_R . (() . x)) * ((sin . x) / ((cos . x) ^2)) is V11() V12() ext-real Element of REAL
x is V11() V12() ext-real Element of REAL
((exp_R * ()) `| Z) . x is V11() V12() ext-real Element of REAL
() . x is V11() V12() ext-real Element of REAL
exp_R . (() . x) is V11() V12() ext-real Element of REAL
sin . x is V11() V12() ext-real Element of REAL
(exp_R . (() . x)) * (sin . x) is V11() V12() ext-real Element of REAL
cos . x is V11() V12() ext-real Element of REAL
(cos . x) ^2 is V11() V12() ext-real Element of REAL
K37((cos . x),(cos . x)) is V11() V12() ext-real set
((exp_R . (() . x)) * (sin . x)) / ((cos . x) ^2) is V11() V12() ext-real Element of REAL
K39(((cos . x) ^2)) is V11() V12() ext-real set
K37(((exp_R . (() . x)) * (sin . x)),K39(((cos . x) ^2))) is V11() V12() ext-real set
exp_R * () is V13() V16( REAL ) V17( REAL ) V18() V52() V53() V54() Element of K6(K7(REAL,REAL))
dom (exp_R * ()) is V62() V63() V64() Element of K6(REAL)
Z is open V62() V63() V64() Element of K6(REAL)
(exp_R * ()) `| Z is V13() V16( REAL ) V17( REAL ) V18() V52() V53() V54() Element of K6(K7(REAL,REAL))
x is V11() V12() ext-real Element of REAL
sin . x is V11() V12() ext-real Element of REAL
x is V11() V12() ext-real Element of REAL
sin . x is V11() V12() ext-real Element of REAL
() . x is V11() V12() ext-real Element of REAL
x is V11() V12() ext-real Element of REAL
((exp_R * ()) `| Z) . x is V11() V12() ext-real Element of REAL
() . x is V11() V12() ext-real Element of REAL
exp_R . (() . x) is V11() V12() ext-real Element of REAL
cos . x is V11() V12() ext-real Element of REAL
(exp_R . (() . x)) * (cos . x) is V11() V12() ext-real Element of REAL
sin . x is V11() V12() ext-real Element of REAL
(sin . x) ^2 is V11() V12() ext-real Element of REAL
K37((sin . x),(sin . x)) is V11() V12() ext-real set
((exp_R . (() . x)) * (cos . x)) / ((sin . x) ^2) is V11() V12() ext-real Element of REAL
K39(((sin . x) ^2)) is V11() V12() ext-real set
K37(((exp_R . (() . x)) * (cos . x)),K39(((sin . x) ^2))) is V11() V12() ext-real set
- (((exp_R . (() . x)) * (cos . x)) / ((sin . x) ^2)) is V11() V12() ext-real Element of REAL
diff ((exp_R * ()),x) is V11() V12() ext-real Element of REAL
diff (exp_R,(() . x)) is V11() V12() ext-real Element of REAL
diff ((),x) is V11() V12() ext-real Element of REAL
(diff (exp_R,(() . x))) * (diff ((),x)) is V11() V12() ext-real Element of REAL
(cos . x) / ((sin . x) ^2) is V11() V12() ext-real Element of REAL
K37((cos . x),K39(((sin . x) ^2))) is V11() V12() ext-real set
- ((cos . x) / ((sin . x) ^2)) is V11() V12() ext-real Element of REAL
(diff (exp_R,(() . x))) * (- ((cos . x) / ((sin . x) ^2))) is V11() V12() ext-real Element of REAL
(exp_R . (() . x)) * (- ((cos . x) / ((sin . x) ^2))) is V11() V12() ext-real Element of REAL
x is V11() V12() ext-real Element of REAL
((exp_R * ()) `| Z) . x is V11() V12() ext-real Element of REAL
() . x is V11() V12() ext-real Element of REAL
exp_R . (() . x) is V11() V12() ext-real Element of REAL
cos . x is V11() V12() ext-real Element of REAL
(exp_R . (() . x)) * (cos . x) is V11() V12() ext-real Element of REAL
sin . x is V11() V12() ext-real Element of REAL
(sin . x) ^2 is V11() V12() ext-real Element of REAL
K37((sin . x),(sin . x)) is V11() V12() ext-real set
((exp_R . (() . x)) * (cos . x)) / ((sin . x) ^2) is V11() V12() ext-real Element of REAL
K39(((sin . x) ^2)) is V11() V12() ext-real set
K37(((exp_R . (() . x)) * (cos . x)),K39(((sin . x) ^2))) is V11() V12() ext-real set
- (((exp_R . (() . x)) * (cos . x)) / ((sin . x) ^2)) is V11() V12() ext-real Element of REAL
ln * () is V13() V16( REAL ) V17( REAL ) V18() V52() V53() V54() Element of K6(K7(REAL,REAL))
dom (ln * ()) is V62() V63() V64() Element of K6(REAL)
Z is open V62() V63() V64() Element of K6(REAL)
(ln * ()) `| Z is V13() V16( REAL ) V17( REAL ) V18() V52() V53() V54() Element of K6(K7(REAL,REAL))
x is V11() V12() ext-real Element of REAL
() . x is V11() V12() ext-real Element of REAL
x is V11() V12() ext-real Element of REAL
x is V11() V12() ext-real Element of REAL
cos . x is V11() V12() ext-real Element of REAL
x is V11() V12() ext-real Element of REAL
cos . x is V11() V12() ext-real Element of REAL
x is V11() V12() ext-real Element of REAL
() . x is V11() V12() ext-real Element of REAL
x is V11() V12() ext-real Element of REAL
((ln * ()) `| Z) . x is V11() V12() ext-real Element of REAL
sin . x is V11() V12() ext-real Element of REAL
cos . x is V11() V12() ext-real Element of REAL
(sin . x) / (cos . x) is V11() V12() ext-real Element of REAL
K39((cos . x)) is V11() V12() ext-real set
K37((sin . x),K39((cos . x))) is V11() V12() ext-real set
() . x is V11() V12() ext-real Element of REAL
diff ((ln * ()),x) is V11() V12() ext-real Element of REAL
diff ((),x) is V11() V12() ext-real Element of REAL
(diff ((),x)) / (() . x) is V11() V12() ext-real Element of REAL
K39((() . x)) is V11() V12() ext-real set
K37((diff ((),x)),K39((() . x))) is V11() V12() ext-real set
(cos . x) ^2 is V11() V12() ext-real Element of REAL
K37((cos . x),(cos . x)) is V11() V12() ext-real set
(sin . x) / ((cos . x) ^2) is V11() V12() ext-real Element of REAL
K39(((cos . x) ^2)) is V11() V12() ext-real set
K37((sin . x),K39(((cos . x) ^2))) is V11() V12() ext-real set
((sin . x) / ((cos . x) ^2)) / (() . x) is V11() V12() ext-real Element of REAL
K37(((sin . x) / ((cos . x) ^2)),K39((() . x))) is V11() V12() ext-real set
(cos . x) " is V11() V12() ext-real Element of REAL
((sin . x) / ((cos . x) ^2)) / ((cos . x) ") is V11() V12() ext-real Element of REAL
K39(((cos . x) ")) is V11() V12() ext-real set
K37(((sin . x) / ((cos . x) ^2)),K39(((cos . x) "))) is V11() V12() ext-real set
(sin . x) * (cos . x) is V11() V12() ext-real Element of REAL
(cos . x) * (cos . x) is V11() V12() ext-real Element of REAL
((sin . x) * (cos . x)) / ((cos . x) * (cos . x)) is V11() V12() ext-real Element of REAL
K39(((cos . x) * (cos . x))) is V11() V12() ext-real set
K37(((sin . x) * (cos . x)),K39(((cos . x) * (cos . x)))) is V11() V12() ext-real set
x is V11() V12() ext-real Element of REAL
((ln * ()) `| Z) . x is V11() V12() ext-real Element of REAL
sin . x is V11() V12() ext-real Element of REAL
cos . x is V11() V12() ext-real Element of REAL
(sin . x) / (cos . x) is V11() V12() ext-real Element of REAL
K39((cos . x)) is V11() V12() ext-real set
K37((sin . x),K39((cos . x))) is V11() V12() ext-real set
ln * () is V13() V16( REAL ) V17( REAL ) V18() V52() V53() V54() Element of K6(K7(REAL,REAL))
dom (ln * ()) is V62() V63() V64() Element of K6(REAL)
Z is open V62() V63() V64() Element of K6(REAL)
(ln * ()) `| Z is V13() V16( REAL ) V17( REAL ) V18() V52() V53() V54() Element of K6(K7(REAL,REAL))
x is V11() V12() ext-real Element of REAL
() . x is V11() V12() ext-real Element of REAL
x is V11() V12() ext-real Element of REAL
x is V11() V12() ext-real Element of REAL
sin . x is V11() V12() ext-real Element of REAL
x is V11() V12() ext-real Element of REAL
sin . x is V11() V12() ext-real Element of REAL
x is V11() V12() ext-real Element of REAL
() . x is V11() V12() ext-real Element of REAL
x is V11() V12() ext-real Element of REAL
((ln * ()) `| Z) . x is V11() V12() ext-real Element of REAL
cos . x is V11() V12() ext-real Element of REAL
sin . x is V11() V12() ext-real Element of REAL
(cos . x) / (sin . x) is V11() V12() ext-real Element of REAL
K39((sin . x)) is V11() V12() ext-real set
K37((cos . x),K39((sin . x))) is V11() V12() ext-real set
- ((cos . x) / (sin . x)) is V11() V12() ext-real Element of REAL
() . x is V11() V12() ext-real Element of REAL
diff ((ln * ()),x) is V11() V12() ext-real Element of REAL
diff ((),x) is V11() V12() ext-real Element of REAL
(diff ((),x)) / (() . x) is V11() V12() ext-real Element of REAL
K39((() . x)) is V11() V12() ext-real set
K37((diff ((),x)),K39((() . x))) is V11() V12() ext-real set
(sin . x) ^2 is V11() V12() ext-real Element of REAL
K37((sin . x),(sin . x)) is V11() V12() ext-real set
(cos . x) / ((sin . x) ^2) is V11() V12() ext-real Element of REAL
K39(((sin . x) ^2)) is V11() V12() ext-real set
K37((cos . x),K39(((sin . x) ^2))) is V11() V12() ext-real set
- ((cos . x) / ((sin . x) ^2)) is V11() V12() ext-real Element of REAL
(- ((cos . x) / ((sin . x) ^2))) / (() . x) is V11() V12() ext-real Element of REAL
K37((- ((cos . x) / ((sin . x) ^2))),K39((() . x))) is V11() V12() ext-real set
(sin . x) " is V11() V12() ext-real Element of REAL
(- ((cos . x) / ((sin . x) ^2))) / ((sin . x) ") is V11() V12() ext-real Element of REAL
K39(((sin . x) ")) is V11() V12() ext-real set
K37((- ((cos . x) / ((sin . x) ^2))),K39(((sin . x) "))) is V11() V12() ext-real set
- (cos . x) is V11() V12() ext-real Element of REAL
(- (cos . x)) * (sin . x) is V11() V12() ext-real Element of REAL
(sin . x) * (sin . x) is V11() V12() ext-real Element of REAL
((- (cos . x)) * (sin . x)) / ((sin . x) * (sin . x)) is V11() V12() ext-real Element of REAL
K39(((sin . x) * (sin . x))) is V11() V12() ext-real set
K37(((- (cos . x)) * (sin . x)),K39(((sin . x) * (sin . x)))) is V11() V12() ext-real set
(- (cos . x)) / (sin . x) is V11() V12() ext-real Element of REAL
K37((- (cos . x)),K39((sin . x))) is V11() V12() ext-real set
x is V11() V12() ext-real Element of REAL
((ln * ()) `| Z) . x is V11() V12() ext-real Element of REAL
cos . x is V11() V12() ext-real Element of REAL
sin . x is V11() V12() ext-real Element of REAL
(cos . x) / (sin . x) is V11() V12() ext-real Element of REAL
K39((sin . x)) is V11() V12() ext-real set
K37((cos . x),K39((sin . x))) is V11() V12() ext-real set
- ((cos . x) / (sin . x)) is V11() V12() ext-real Element of REAL
Z is V4() V5() V6() V10() V11() V12() ext-real V47() set
#Z Z is V13() V16( REAL ) V17( REAL ) V18() V27( REAL , REAL ) V52() V53() V54() Element of K6(K7(REAL,REAL))
(#Z Z) * () is V13() V16( REAL ) V17( REAL ) V18() V52() V53() V54() Element of K6(K7(REAL,REAL))
dom ((#Z Z) * ()) is V62() V63() V64() Element of K6(REAL)
Z + 1 is V4() V5() V6() V10() V11() V12() ext-real V47() V62() V63() V64() V65() V66() V67() V69() Element of NAT
x is open V62() V63() V64() Element of K6(REAL)
((#Z Z) * ()) `| x is V13() V16( REAL ) V17( REAL ) V18() V52() V53() V54() Element of K6(K7(REAL,REAL))
x is V11() V12() ext-real Element of REAL
cos . x is V11() V12() ext-real Element of REAL
x is V11() V12() ext-real Element of REAL
cos . x is V11() V12() ext-real Element of REAL
Z - 1 is V11() V12() ext-real V47() Element of REAL
K38(1) is V11() V12() ext-real non positive V47() set
K36(Z,K38(1)) is V11() V12() ext-real V47() set
f is V11() V12() ext-real Element of REAL
(((#Z Z) * ()) `| x) . f is V11() V12() ext-real Element of REAL
sin . f is V11() V12() ext-real Element of REAL
Z * (sin . f) is V11() V12() ext-real Element of REAL
cos . f is V11() V12() ext-real Element of REAL
(cos . f) #Z (Z + 1) is V11() V12() ext-real Element of REAL
(Z * (sin . f)) / ((cos . f) #Z (Z + 1)) is V11() V12() ext-real Element of REAL
K39(((cos . f) #Z (Z + 1))) is V11() V12() ext-real set
K37((Z * (sin . f)),K39(((cos . f) #Z (Z + 1)))) is V11() V12() ext-real set
diff (((#Z Z) * ()),f) is V11() V12() ext-real Element of REAL
() . f is V11() V12() ext-real Element of REAL
(() . f) #Z (Z - 1) is V11() V12() ext-real Element of REAL
Z * ((() . f) #Z (Z - 1)) is V11() V12() ext-real Element of REAL
diff ((),f) is V11() V12() ext-real Element of REAL
(Z * ((() . f) #Z (Z - 1))) * (diff ((),f)) is V11() V12() ext-real Element of REAL
(cos . f) ^2 is V11() V12() ext-real Element of REAL
K37((cos . f),(cos . f)) is V11() V12() ext-real set
(sin . f) / ((cos . f) ^2) is V11() V12() ext-real Element of REAL
K39(((cos . f) ^2)) is V11() V12() ext-real set
K37((sin . f),K39(((cos . f) ^2))) is V11() V12() ext-real set
(Z * ((() . f) #Z (Z - 1))) * ((sin . f) / ((cos . f) ^2)) is V11() V12() ext-real Element of REAL
1 / (cos . f) is V11() V12() ext-real Element of REAL
K39((cos . f)) is V11() V12() ext-real set
K37(1,K39((cos . f))) is V11() V12() ext-real set
(1 / (cos . f)) #Z (Z - 1) is V11() V12() ext-real Element of REAL
Z * ((1 / (cos . f)) #Z (Z - 1)) is V11() V12() ext-real Element of REAL
(Z * ((1 / (cos . f)) #Z (Z - 1))) * ((sin . f) / ((cos . f) ^2)) is V11() V12() ext-real Element of REAL
(cos . f) #Z (Z - 1) is V11() V12() ext-real Element of REAL
1 / ((cos . f) #Z (Z - 1)) is V11() V12() ext-real Element of REAL
K39(((cos . f) #Z (Z - 1))) is V11() V12() ext-real set
K37(1,K39(((cos . f) #Z (Z - 1)))) is V11() V12() ext-real set
Z * (1 / ((cos . f) #Z (Z - 1))) is V11() V12() ext-real Element of REAL
(Z * (1 / ((cos . f) #Z (Z - 1)))) * ((sin . f) / ((cos . f) ^2)) is V11() V12() ext-real Element of REAL
Z / ((cos . f) #Z (Z - 1)) is V11() V12() ext-real Element of REAL
K37(Z,K39(((cos . f) #Z (Z - 1)))) is V11() V12() ext-real set
(Z / ((cos . f) #Z (Z - 1))) * ((sin . f) / ((cos . f) ^2)) is V11() V12() ext-real Element of REAL
((cos . f) #Z (Z - 1)) * ((cos . f) ^2) is V11() V12() ext-real Element of REAL
(Z * (sin . f)) / (((cos . f) #Z (Z - 1)) * ((cos . f) ^2)) is V11() V12() ext-real Element of REAL
K39((((cos . f) #Z (Z - 1)) * ((cos . f) ^2))) is V11() V12() ext-real set
K37((Z * (sin . f)),K39((((cos . f) #Z (Z - 1)) * ((cos . f) ^2)))) is V11() V12() ext-real set
(cos . f) #Z 2 is V11() V12() ext-real Element of REAL
((cos . f) #Z (Z - 1)) * ((cos . f) #Z 2) is V11() V12() ext-real Element of REAL
(Z * (sin . f)) / (((cos . f) #Z (Z - 1)) * ((cos . f) #Z 2)) is V11() V12() ext-real Element of REAL
K39((((cos . f) #Z (Z - 1)) * ((cos . f) #Z 2))) is V11() V12() ext-real set
K37((Z * (sin . f)),K39((((cos . f) #Z (Z - 1)) * ((cos . f) #Z 2)))) is V11() V12() ext-real set
(Z - 1) + 2 is V11() V12() ext-real V47() Element of REAL
(cos . f) #Z ((Z - 1) + 2) is V11() V12() ext-real Element of REAL
(Z * (sin . f)) / ((cos . f) #Z ((Z - 1) + 2)) is V11() V12() ext-real Element of REAL
K39(((cos . f) #Z ((Z - 1) + 2))) is V11() V12() ext-real set
K37((Z * (sin . f)),K39(((cos . f) #Z ((Z - 1) + 2)))) is V11() V12() ext-real set
x is V4() V5() V6() V10() V11() V12() ext-real V47() set
x + 1 is V4() V5() V6() V10() V11() V12() ext-real V47() V62() V63() V64() V65() V66() V67() V69() Element of NAT
x is V11() V12() ext-real Element of REAL
(((#Z Z) * ()) `| x) . x is V11() V12() ext-real Element of REAL
sin . x is V11() V12() ext-real Element of REAL
Z * (sin . x) is V11() V12() ext-real Element of REAL
cos . x is V11() V12() ext-real Element of REAL
(cos . x) #Z (Z + 1) is V11() V12() ext-real Element of REAL
(Z * (sin . x)) / ((cos . x) #Z (Z + 1)) is V11() V12() ext-real Element of REAL
K39(((cos . x) #Z (Z + 1))) is V11() V12() ext-real set
K37((Z * (sin . x)),K39(((cos . x) #Z (Z + 1)))) is V11() V12() ext-real set
Z is V4() V5() V6() V10() V11() V12() ext-real V47() set
#Z Z is V13() V16( REAL ) V17( REAL ) V18() V27( REAL , REAL ) V52() V53() V54() Element of K6(K7(REAL,REAL))
(#Z Z) * () is V13() V16( REAL ) V17( REAL ) V18() V52() V53() V54() Element of K6(K7(REAL,REAL))
dom ((#Z Z) * ()) is V62() V63() V64() Element of K6(REAL)
Z + 1 is V4() V5() V6() V10() V11() V12() ext-real V47() V62() V63() V64() V65() V66() V67() V69() Element of NAT
x is open V62() V63() V64() Element of K6(REAL)
((#Z Z) * ()) `| x is V13() V16( REAL ) V17( REAL ) V18() V52() V53() V54() Element of K6(K7(REAL,REAL))
x is V11() V12() ext-real Element of REAL
sin . x is V11() V12() ext-real Element of REAL
x is V11() V12() ext-real Element of REAL
sin . x is V11() V12() ext-real Element of REAL
Z - 1 is V11() V12() ext-real V47() Element of REAL
K38(1) is V11() V12() ext-real non positive V47() set
K36(Z,K38(1)) is V11() V12() ext-real V47() set
f is V11() V12() ext-real Element of REAL
(((#Z Z) * ()) `| x) . f is V11() V12() ext-real Element of REAL
cos . f is V11() V12() ext-real Element of REAL
Z * (cos . f) is V11() V12() ext-real Element of REAL
sin . f is V11() V12() ext-real Element of REAL
(sin . f) #Z (Z + 1) is V11() V12() ext-real Element of REAL
(Z * (cos . f)) / ((sin . f) #Z (Z + 1)) is V11() V12() ext-real Element of REAL
K39(((sin . f) #Z (Z + 1))) is V11() V12() ext-real set
K37((Z * (cos . f)),K39(((sin . f) #Z (Z + 1)))) is V11() V12() ext-real set
- ((Z * (cos . f)) / ((sin . f) #Z (Z + 1))) is V11() V12() ext-real Element of REAL
diff (((#Z Z) * ()),f) is V11() V12() ext-real Element of REAL
() . f is V11() V12() ext-real Element of REAL
(() . f) #Z (Z - 1) is V11() V12() ext-real Element of REAL
Z * ((() . f) #Z (Z - 1)) is V11() V12() ext-real Element of REAL
diff ((),f) is V11() V12() ext-real Element of REAL
(Z * ((() . f) #Z (Z - 1))) * (diff ((),f)) is V11() V12() ext-real Element of REAL
(sin . f) ^2 is V11() V12() ext-real Element of REAL
K37((sin . f),(sin . f)) is V11() V12() ext-real set
(cos . f) / ((sin . f) ^2) is V11() V12() ext-real Element of REAL
K39(((sin . f) ^2)) is V11() V12() ext-real set
K37((cos . f),K39(((sin . f) ^2))) is V11() V12() ext-real set
- ((cos . f) / ((sin . f) ^2)) is V11() V12() ext-real Element of REAL
(Z * ((() . f) #Z (Z - 1))) * (- ((cos . f) / ((sin . f) ^2))) is V11() V12() ext-real Element of REAL
1 / (sin . f) is V11() V12() ext-real Element of REAL
K39((sin . f)) is V11() V12() ext-real set
K37(1,K39((sin . f))) is V11() V12() ext-real set
(1 / (sin . f)) #Z (Z - 1) is V11() V12() ext-real Element of REAL
Z * ((1 / (sin . f)) #Z (Z - 1)) is V11() V12() ext-real Element of REAL
(Z * ((1 / (sin . f)) #Z (Z - 1))) * (- ((cos . f) / ((sin . f) ^2))) is V11() V12() ext-real Element of REAL
(sin . f) #Z (Z - 1) is V11() V12() ext-real Element of REAL
1 / ((sin . f) #Z (Z - 1)) is V11() V12() ext-real Element of REAL
K39(((sin . f) #Z (Z - 1))) is V11() V12() ext-real set
K37(1,K39(((sin . f) #Z (Z - 1)))) is V11() V12() ext-real set
Z * (1 / ((sin . f) #Z (Z - 1))) is V11() V12() ext-real Element of REAL
(Z * (1 / ((sin . f) #Z (Z - 1)))) * (- ((cos . f) / ((sin . f) ^2))) is V11() V12() ext-real Element of REAL
Z / ((sin . f) #Z (Z - 1)) is V11() V12() ext-real Element of REAL
K37(Z,K39(((sin . f) #Z (Z - 1)))) is V11() V12() ext-real set
- (cos . f) is V11() V12() ext-real Element of REAL
(- (cos . f)) / ((sin . f) ^2) is V11() V12() ext-real Element of REAL
K37((- (cos . f)),K39(((sin . f) ^2))) is V11() V12() ext-real set
(Z / ((sin . f) #Z (Z - 1))) * ((- (cos . f)) / ((sin . f) ^2)) is V11() V12() ext-real Element of REAL
Z * (- (cos . f)) is V11() V12() ext-real Element of REAL
((sin . f) #Z (Z - 1)) * ((sin . f) ^2) is V11() V12() ext-real Element of REAL
(Z * (- (cos . f))) / (((sin . f) #Z (Z - 1)) * ((sin . f) ^2)) is V11() V12() ext-real Element of REAL
K39((((sin . f) #Z (Z - 1)) * ((sin . f) ^2))) is V11() V12() ext-real set
K37((Z * (- (cos . f))),K39((((sin . f) #Z (Z - 1)) * ((sin . f) ^2)))) is V11() V12() ext-real set
(sin . f) #Z 2 is V11() V12() ext-real Element of REAL
((sin . f) #Z (Z - 1)) * ((sin . f) #Z 2) is V11() V12() ext-real Element of REAL
(Z * (- (cos . f))) / (((sin . f) #Z (Z - 1)) * ((sin . f) #Z 2)) is V11() V12() ext-real Element of REAL
K39((((sin . f) #Z (Z - 1)) * ((sin . f) #Z 2))) is V11() V12() ext-real set
K37((Z * (- (cos . f))),K39((((sin . f) #Z (Z - 1)) * ((sin . f) #Z 2)))) is V11() V12() ext-real set
(Z - 1) + 2 is V11() V12() ext-real V47() Element of REAL
(sin . f) #Z ((Z - 1) + 2) is V11() V12() ext-real Element of REAL
(Z * (- (cos . f))) / ((sin . f) #Z ((Z - 1) + 2)) is V11() V12() ext-real Element of REAL
K39(((sin . f) #Z ((Z - 1) + 2))) is V11() V12() ext-real set
K37((Z * (- (cos . f))),K39(((sin . f) #Z ((Z - 1) + 2)))) is V11() V12() ext-real set
(Z * (- (cos . f))) / ((sin . f) #Z (Z + 1)) is V11() V12() ext-real Element of REAL
K37((Z * (- (cos . f))),K39(((sin . f) #Z (Z + 1)))) is V11() V12() ext-real set
x is V4() V5() V6() V10() V11() V12() ext-real V47() set
x + 1 is V4() V5() V6() V10() V11() V12() ext-real V47() V62() V63() V64() V65() V66() V67() V69() Element of NAT
x is V11() V12() ext-real Element of REAL
(((#Z Z) * ()) `| x) . x is V11() V12() ext-real Element of REAL
cos . x is V11() V12() ext-real Element of REAL
Z * (cos . x) is V11() V12() ext-real Element of REAL
sin . x is V11() V12() ext-real Element of REAL
(sin . x) #Z (Z + 1) is V11() V12() ext-real Element of REAL
(Z * (cos . x)) / ((sin . x) #Z (Z + 1)) is V11() V12() ext-real Element of REAL
K39(((sin . x) #Z (Z + 1))) is V11() V12() ext-real set
K37((Z * (cos . x)),K39(((sin . x) #Z (Z + 1)))) is V11() V12() ext-real set
- ((Z * (cos . x)) / ((sin . x) #Z (Z + 1))) is V11() V12() ext-real Element of REAL
Z is open V62() V63() V64() Element of K6(REAL)
id Z is V13() V16( REAL ) V17( REAL ) V18() V52() V53() V54() Element of K6(K7(REAL,REAL))
() - (id Z) is V13() V16( REAL ) V17( REAL ) V18() V52() V53() V54() Element of K6(K7(REAL,REAL))
- (id Z) is V13() V18() V52() set
K38(1) is V11() V12() ext-real non positive V47() set
K38(1) (#) (id Z) is V13() V18() set
() + (- (id Z)) is V13() V18() set
dom (() - (id Z)) is V62() V63() V64() Element of K6(REAL)
(() - (id Z)) `| Z is V13() V16( REAL ) V17( REAL ) V18() V52() V53() V54() Element of K6(K7(REAL,REAL))
x is V11() V12() ext-real Element of REAL
(id Z) . x is V11() V12() ext-real Element of REAL
1 * x is V11() V12() ext-real Element of REAL
(1 * x) + 0 is V11() V12() ext-real Element of REAL
dom (id Z) is V62() V63() V64() Element of K6(REAL)
(dom ()) /\ (dom (id Z)) is V62() V63() V64() Element of K6(REAL)
x is V11() V12() ext-real Element of REAL
cos . x is V11() V12() ext-real Element of REAL
x is V11() V12() ext-real Element of REAL
((() - (id Z)) `| Z) . x is V11() V12() ext-real Element of REAL
sin . x is V11() V12() ext-real Element of REAL
cos . x is V11() V12() ext-real Element of REAL
(cos . x) ^2 is V11() V12() ext-real Element of REAL
K37((cos . x),(cos . x)) is V11() V12() ext-real set
(sin . x) - ((cos . x) ^2) is V11() V12() ext-real Element of REAL
K38(((cos . x) ^2)) is V11() V12() ext-real set
K36((sin . x),K38(((cos . x) ^2))) is V11() V12() ext-real set
((sin . x) - ((cos . x) ^2)) / ((cos . x) ^2) is V11() V12() ext-real Element of REAL
K39(((cos . x) ^2)) is V11() V12() ext-real set
K37(((sin . x) - ((cos . x) ^2)),K39(((cos . x) ^2))) is V11() V12() ext-real set
diff ((),x) is V11() V12() ext-real Element of REAL
diff ((id Z),x) is V11() V12() ext-real Element of REAL
(diff ((),x)) - (diff ((id Z),x)) is V11() V12() ext-real Element of REAL
K38((diff ((id Z),x))) is V11() V12() ext-real set
K36((diff ((),x)),K38((diff ((id Z),x)))) is V11() V12() ext-real set
(sin . x) / ((cos . x) ^2) is V11() V12() ext-real Element of REAL
K37((sin . x),K39(((cos . x) ^2))) is V11() V12() ext-real set
((sin . x) / ((cos . x) ^2)) - (diff ((id Z),x)) is V11() V12() ext-real Element of REAL
K36(((sin . x) / ((cos . x) ^2)),K38((diff ((id Z),x)))) is V11() V12() ext-real set
(id Z) `| Z is V13() V16( REAL ) V17( REAL ) V18() V52() V53() V54() Element of K6(K7(REAL,REAL))
((id Z) `| Z) . x is V11() V12() ext-real Element of REAL
((sin . x) / ((cos . x) ^2)) - (((id Z) `| Z) . x) is V11() V12() ext-real Element of REAL
K38((((id Z) `| Z) . x)) is V11() V12() ext-real set
K36(((sin . x) / ((cos . x) ^2)),K38((((id Z) `| Z) . x))) is V11() V12() ext-real set
((sin . x) / ((cos . x) ^2)) - 1 is V11() V12() ext-real Element of REAL
K36(((sin . x) / ((cos . x) ^2)),K38(1)) is V11() V12() ext-real set
((cos . x) ^2) / ((cos . x) ^2) is V11() V12() ext-real Element of REAL
K37(((cos . x) ^2),K39(((cos . x) ^2))) is V11() V12() ext-real set
((sin . x) / ((cos . x) ^2)) - (((cos . x) ^2) / ((cos . x) ^2)) is V11() V12() ext-real Element of REAL
K38((((cos . x) ^2) / ((cos . x) ^2))) is V11() V12() ext-real set
K36(((sin . x) / ((cos . x) ^2)),K38((((cos . x) ^2) / ((cos . x) ^2)))) is V11() V12() ext-real set
x is V11() V12() ext-real Element of REAL
((() - (id Z)) `| Z) . x is V11() V12() ext-real Element of REAL
sin . x is V11() V12() ext-real Element of REAL
cos . x is V11() V12() ext-real Element of REAL
(cos . x) ^2 is V11() V12() ext-real Element of REAL
K37((cos . x),(cos . x)) is V11() V12() ext-real set
(sin . x) - ((cos . x) ^2) is V11() V12() ext-real Element of REAL
K38(((cos . x) ^2)) is V11() V12() ext-real set
K36((sin . x),K38(((cos . x) ^2))) is V11() V12() ext-real set
((sin . x) - ((cos . x) ^2)) / ((cos . x) ^2) is V11() V12() ext-real Element of REAL
K39(((cos . x) ^2)) is V11() V12() ext-real set
K37(((sin . x) - ((cos . x) ^2)),K39(((cos . x) ^2))) is V11() V12() ext-real set
- () is V13() V16( REAL ) V17( REAL ) V18() V52() V53() V54() Element of K6(K7(REAL,REAL))
K38(1) is V11() V12() ext-real non positive V47() set
K38(1) (#) () is V13() V18() set
Z is open V62() V63() V64() Element of K6(REAL)
id Z is V13() V16( REAL ) V17( REAL ) V18() V52() V53() V54() Element of K6(K7(REAL,REAL))
(- ()) - (id Z) is V13() V16( REAL ) V17( REAL ) V18() V52() V53() V54() Element of K6(K7(REAL,REAL))
- (id Z) is V13() V18() V52() set
K38(1) (#) (id Z) is V13() V18() set
(- ()) + (- (id Z)) is V13() V18() set
dom ((- ()) - (id Z)) is V62() V63() V64() Element of K6(REAL)
((- ()) - (id Z)) `| Z is V13() V16( REAL ) V17( REAL ) V18() V52() V53() V54() Element of K6(K7(REAL,REAL))
x is V11() V12() ext-real Element of REAL
(id Z) . x is V11() V12() ext-real Element of REAL
1 * x is V11() V12() ext-real Element of REAL
(1 * x) + 0 is V11() V12() ext-real Element of REAL
dom (- ()) is V62() V63() V64() Element of K6(REAL)
dom (id Z) is V62() V63() V64() Element of K6(REAL)
(dom (- ())) /\ (dom (id Z)) is V62() V63() V64() Element of K6(REAL)
x is V11() V12() ext-real Element of REAL
sin . x is V11() V12() ext-real Element of REAL
- 1 is V11() V12() ext-real non positive V47() Element of REAL
(- 1) (#) () is V13() V16( REAL ) V17( REAL ) V18() V52() V53() V54() Element of K6(K7(REAL,REAL))
x is V11() V12() ext-real Element of REAL
(((- ()) - (id Z)) `| Z) . x is V11() V12() ext-real Element of REAL
cos . x is V11() V12() ext-real Element of REAL
sin . x is V11() V12() ext-real Element of REAL
(sin . x) ^2 is V11() V12() ext-real Element of REAL
K37((sin . x),(sin . x)) is V11() V12() ext-real set
(cos . x) - ((sin . x) ^2) is V11() V12() ext-real Element of REAL
K38(((sin . x) ^2)) is V11() V12() ext-real set
K36((cos . x),K38(((sin . x) ^2))) is V11() V12() ext-real set
((cos . x) - ((sin . x) ^2)) / ((sin . x) ^2) is V11() V12() ext-real Element of REAL
K39(((sin . x) ^2)) is V11() V12() ext-real set
K37(((cos . x) - ((sin . x) ^2)),K39(((sin . x) ^2))) is V11() V12() ext-real set
diff ((- ()),x) is V11() V12() ext-real Element of REAL
diff ((id Z),x) is V11() V12() ext-real Element of REAL
(diff ((- ()),x)) - (diff ((id Z),x)) is V11() V12() ext-real Element of REAL
K38((diff ((id Z),x))) is V11() V12() ext-real set
K36((diff ((- ()),x)),K38((diff ((id Z),x)))) is V11() V12() ext-real set
((- 1) (#) ()) `| Z is V13() V16( REAL ) V17( REAL ) V18() V52() V53() V54() Element of K6(K7(REAL,REAL))
(((- 1) (#) ()) `| Z) . x is V11() V12() ext-real Element of REAL
((((- 1) (#) ()) `| Z) . x) - (diff ((id Z),x)) is V11() V12() ext-real Element of REAL
K36(((((- 1) (#) ()) `| Z) . x),K38((diff ((id Z),x)))) is V11() V12() ext-real set
diff ((),x) is V11() V12() ext-real Element of REAL
(- 1) * (diff ((),x)) is V11() V12() ext-real Element of REAL
((- 1) * (diff ((),x))) - (diff ((id Z),x)) is V11() V12() ext-real Element of REAL
K36(((- 1) * (diff ((),x))),K38((diff ((id Z),x)))) is V11() V12() ext-real set
(cos . x) / ((sin . x) ^2) is V11() V12() ext-real Element of REAL
K37((cos . x),K39(((sin . x) ^2))) is V11() V12() ext-real set
- ((cos . x) / ((sin . x) ^2)) is V11() V12() ext-real Element of REAL
(- 1) * (- ((cos . x) / ((sin . x) ^2))) is V11() V12() ext-real Element of REAL
((- 1) * (- ((cos . x) / ((sin . x) ^2)))) - (diff ((id Z),x)) is V11() V12() ext-real Element of REAL
K36(((- 1) * (- ((cos . x) / ((sin . x) ^2)))),K38((diff ((id Z),x)))) is V11() V12() ext-real set
(id Z) `| Z is V13() V16( REAL ) V17( REAL ) V18() V52() V53() V54() Element of K6(K7(REAL,REAL))
((id Z) `| Z) . x is V11() V12() ext-real Element of REAL
((cos . x) / ((sin . x) ^2)) - (((id Z) `| Z) . x) is V11() V12() ext-real Element of REAL
K38((((id Z) `| Z) . x)) is V11() V12() ext-real set
K36(((cos . x) / ((sin . x) ^2)),K38((((id Z) `| Z) . x))) is V11() V12() ext-real set
((cos . x) / ((sin . x) ^2)) - 1 is V11() V12() ext-real Element of REAL
K36(((cos . x) / ((sin . x) ^2)),K38(1)) is V11() V12() ext-real set
((sin . x) ^2) / ((sin . x) ^2) is V11() V12() ext-real Element of REAL
K37(((sin . x) ^2),K39(((sin . x) ^2))) is V11() V12() ext-real set
((cos . x) / ((sin . x) ^2)) - (((sin . x) ^2) / ((sin . x) ^2)) is V11() V12() ext-real Element of REAL
K38((((sin . x) ^2) / ((sin . x) ^2))) is V11() V12() ext-real set
K36(((cos . x) / ((sin . x) ^2)),K38((((sin . x) ^2) / ((sin . x) ^2)))) is V11() V12() ext-real set
x is V11() V12() ext-real Element of REAL
(((- ()) - (id Z)) `| Z) . x is V11() V12() ext-real Element of REAL
cos . x is V11() V12() ext-real Element of REAL
sin . x is V11() V12() ext-real Element of REAL
(sin . x) ^2 is V11() V12() ext-real Element of REAL
K37((sin . x),(sin . x)) is V11() V12() ext-real set
(cos . x) - ((sin . x) ^2) is V11() V12() ext-real Element of REAL
K38(((sin . x) ^2)) is V11() V12() ext-real set
K36((cos . x),K38(((sin . x) ^2))) is V11() V12() ext-real set
((cos . x) - ((sin . x) ^2)) / ((sin . x) ^2) is V11() V12() ext-real Element of REAL
K39(((sin . x) ^2)) is V11() V12() ext-real set
K37(((cos . x) - ((sin . x) ^2)),K39(((sin . x) ^2))) is V11() V12() ext-real set
exp_R (#) () is V13() V16( REAL ) V17( REAL ) V18() V52() V53() V54() Element of K6(K7(REAL,REAL))
dom (exp_R (#) ()) is V62() V63() V64() Element of K6(REAL)
Z is open V62() V63() V64() Element of K6(REAL)
(exp_R (#) ()) `| Z is V13() V16( REAL ) V17( REAL ) V18() V52() V53() V54() Element of K6(K7(REAL,REAL))
x is V11() V12() ext-real Element of REAL
dom exp_R is V62() V63() V64() Element of K6(REAL)
(dom exp_R) /\ (dom ()) is V62() V63() V64() Element of K6(REAL)
x is V11() V12() ext-real Element of REAL
diff ((),x) is V11() V12() ext-real Element of REAL
sin . x is V11() V12() ext-real Element of REAL
cos . x is V11() V12() ext-real Element of REAL
(cos . x) ^2 is V11() V12() ext-real Element of REAL
K37((cos . x),(cos . x)) is V11() V12() ext-real set
(sin . x) / ((cos . x) ^2) is V11() V12() ext-real Element of REAL
K39(((cos . x) ^2)) is V11() V12() ext-real set
K37((sin . x),K39(((cos . x) ^2))) is V11() V12() ext-real set
x is V11() V12() ext-real Element of REAL
x is V11() V12() ext-real Element of REAL
((exp_R (#) ()) `| Z) . x is V11() V12() ext-real Element of REAL
exp_R . x is V11() V12() ext-real Element of REAL
cos . x is V11() V12() ext-real Element of REAL
(exp_R . x) / (cos . x) is V11() V12() ext-real Element of REAL
K39((cos . x)) is V11() V12() ext-real set
K37((exp_R . x),K39((cos . x))) is V11() V12() ext-real set
sin . x is V11() V12() ext-real Element of REAL
(exp_R . x) * (sin . x) is V11() V12() ext-real Element of REAL
(cos . x) ^2 is V11() V12() ext-real Element of REAL
K37((cos . x),(cos . x)) is V11() V12() ext-real set
((exp_R . x) * (sin . x)) / ((cos . x) ^2) is V11() V12() ext-real Element of REAL
K39(((cos . x) ^2)) is V11() V12() ext-real set
K37(((exp_R . x) * (sin . x)),K39(((cos . x) ^2))) is V11() V12() ext-real set
((exp_R . x) / (cos . x)) + (((exp_R . x) * (sin . x)) / ((cos . x) ^2)) is V11() V12() ext-real Element of REAL
() . x is V11() V12() ext-real Element of REAL
diff (exp_R,x) is V11() V12() ext-real Element of REAL
(() . x) * (diff (exp_R,x)) is V11() V12() ext-real Element of REAL
diff ((),x) is V11() V12() ext-real Element of REAL
(exp_R . x) * (diff ((),x)) is V11() V12() ext-real Element of REAL
((() . x) * (diff (exp_R,x))) + ((exp_R . x) * (diff ((),x))) is V11() V12() ext-real Element of REAL
(() . x) * (exp_R . x) is V11() V12() ext-real Element of REAL
((() . x) * (exp_R . x)) + ((exp_R . x) * (diff ((),x))) is V11() V12() ext-real Element of REAL
(sin . x) / ((cos . x) ^2) is V11() V12() ext-real Element of REAL
K37((sin . x),K39(((cos . x) ^2))) is V11() V12() ext-real set
(exp_R . x) * ((sin . x) / ((cos . x) ^2)) is V11() V12() ext-real Element of REAL
((() . x) * (exp_R . x)) + ((exp_R . x) * ((sin . x) / ((cos . x) ^2))) is V11() V12() ext-real Element of REAL
x is V11() V12() ext-real Element of REAL
((exp_R (#) ()) `| Z) . x is V11() V12() ext-real Element of REAL
exp_R . x is V11() V12() ext-real Element of REAL
cos . x is V11() V12() ext-real Element of REAL
(exp_R . x) / (cos . x) is V11() V12() ext-real Element of REAL
K39((cos . x)) is V11() V12() ext-real set
K37((exp_R . x),K39((cos . x))) is V11() V12() ext-real set
sin . x is V11() V12() ext-real Element of REAL
(exp_R . x) * (sin . x) is V11() V12() ext-real Element of REAL
(cos . x) ^2 is V11() V12() ext-real Element of REAL
K37((cos . x),(cos . x)) is V11() V12() ext-real set
((exp_R . x) * (sin . x)) / ((cos . x) ^2) is V11() V12() ext-real Element of REAL
K39(((cos . x) ^2)) is V11() V12() ext-real set
K37(((exp_R . x) * (sin . x)),K39(((cos . x) ^2))) is V11() V12() ext-real set
((exp_R . x) / (cos . x)) + (((exp_R . x) * (sin . x)) / ((cos . x) ^2)) is V11() V12() ext-real Element of REAL
exp_R (#) () is V13() V16( REAL ) V17( REAL ) V18() V52() V53() V54() Element of K6(K7(REAL,REAL))
dom (exp_R (#) ()) is V62() V63() V64() Element of K6(REAL)
Z is open V62() V63() V64() Element of K6(REAL)
(exp_R (#) ()) `| Z is V13() V16( REAL ) V17( REAL ) V18() V52() V53() V54() Element of K6(K7(REAL,REAL))
x is V11() V12() ext-real Element of REAL
dom exp_R is V62() V63() V64() Element of K6(REAL)
(dom exp_R) /\ (dom ()) is V62() V63() V64() Element of K6(REAL)
x is V11() V12() ext-real Element of REAL
diff ((),x) is V11() V12() ext-real Element of REAL
cos . x is V11() V12() ext-real Element of REAL
sin . x is V11() V12() ext-real Element of REAL
(sin . x) ^2 is V11() V12() ext-real Element of REAL
K37((sin . x),(sin . x)) is V11() V12() ext-real set
(cos . x) / ((sin . x) ^2) is V11() V12() ext-real Element of REAL
K39(((sin . x) ^2)) is V11() V12() ext-real set
K37((cos . x),K39(((sin . x) ^2))) is V11() V12() ext-real set
- ((cos . x) / ((sin . x) ^2)) is V11() V12() ext-real Element of REAL
x is V11() V12() ext-real Element of REAL
x is V11() V12() ext-real Element of REAL
((exp_R (#) ()) `| Z) . x is V11() V12() ext-real Element of REAL
exp_R . x is V11() V12() ext-real Element of REAL
sin . x is V11() V12() ext-real Element of REAL
(exp_R . x) / (sin . x) is V11() V12() ext-real Element of REAL
K39((sin . x)) is V11() V12() ext-real set
K37((exp_R . x),K39((sin . x))) is V11() V12() ext-real set
cos . x is V11() V12() ext-real Element of REAL
(exp_R . x) * (cos . x) is V11() V12() ext-real Element of REAL
(sin . x) ^2 is V11() V12() ext-real Element of REAL
K37((sin . x),(sin . x)) is V11() V12() ext-real set
((exp_R . x) * (cos . x)) / ((sin . x) ^2) is V11() V12() ext-real Element of REAL
K39(((sin . x) ^2)) is V11() V12() ext-real set
K37(((exp_R . x) * (cos . x)),K39(((sin . x) ^2))) is V11() V12() ext-real set
((exp_R . x) / (sin . x)) - (((exp_R . x) * (cos . x)) / ((sin . x) ^2)) is V11() V12() ext-real Element of REAL
K38((((exp_R . x) * (cos . x)) / ((sin . x) ^2))) is V11() V12() ext-real set
K36(((exp_R . x) / (sin . x)),K38((((exp_R . x) * (cos . x)) / ((sin . x) ^2)))) is V11() V12() ext-real set
() . x is V11() V12() ext-real Element of REAL
diff (exp_R,x) is V11() V12() ext-real Element of REAL
(() . x) * (diff (exp_R,x)) is V11() V12() ext-real Element of REAL
diff ((),x) is V11() V12() ext-real Element of REAL
(exp_R . x) * (diff ((),x)) is V11() V12() ext-real Element of REAL
((() . x) * (diff (exp_R,x))) + ((exp_R . x) * (diff ((),x))) is V11() V12() ext-real Element of REAL
(() . x) * (exp_R . x) is V11() V12() ext-real Element of REAL
((() . x) * (exp_R . x)) + ((exp_R . x) * (diff ((),x))) is V11() V12() ext-real Element of REAL
(cos . x) / ((sin . x) ^2) is V11() V12() ext-real Element of REAL
K37((cos . x),K39(((sin . x) ^2))) is V11() V12() ext-real set
- ((cos . x) / ((sin . x) ^2)) is V11() V12() ext-real Element of REAL
(exp_R . x) * (- ((cos . x) / ((sin . x) ^2))) is V11() V12() ext-real Element of REAL
((() . x) * (exp_R . x)) + ((exp_R . x) * (- ((cos . x) / ((sin . x) ^2)))) is V11() V12() ext-real Element of REAL
- (cos . x) is V11() V12() ext-real Element of REAL
(exp_R . x) * (- (cos . x)) is V11() V12() ext-real Element of REAL
((exp_R . x) * (- (cos . x))) / ((sin . x) ^2) is V11() V12() ext-real Element of REAL
K37(((exp_R . x) * (- (cos . x))),K39(((sin . x) ^2))) is V11() V12() ext-real set
((exp_R . x) / (sin . x)) + (((exp_R . x) * (- (cos . x))) / ((sin . x) ^2)) is V11() V12() ext-real Element of REAL
x is V11() V12() ext-real Element of REAL
((exp_R (#) ()) `| Z) . x is V11() V12() ext-real Element of REAL
exp_R . x is V11() V12() ext-real Element of REAL
sin . x is V11() V12() ext-real Element of REAL
(exp_R . x) / (sin . x) is V11() V12() ext-real Element of REAL
K39((sin . x)) is V11() V12() ext-real set
K37((exp_R . x),K39((sin . x))) is V11() V12() ext-real set
cos . x is V11() V12() ext-real Element of REAL
(exp_R . x) * (cos . x) is V11() V12() ext-real Element of REAL
(sin . x) ^2 is V11() V12() ext-real Element of REAL
K37((sin . x),(sin . x)) is V11() V12() ext-real set
((exp_R . x) * (cos . x)) / ((sin . x) ^2) is V11() V12() ext-real Element of REAL
K39(((sin . x) ^2)) is V11() V12() ext-real set
K37(((exp_R . x) * (cos . x)),K39(((sin . x) ^2))) is V11() V12() ext-real set
((exp_R . x) / (sin . x)) - (((exp_R . x) * (cos . x)) / ((sin . x) ^2)) is V11() V12() ext-real Element of REAL
K38((((exp_R . x) * (cos . x)) / ((sin . x) ^2))) is V11() V12() ext-real set
K36(((exp_R . x) / (sin . x)),K38((((exp_R . x) * (cos . x)) / ((sin . x) ^2)))) is V11() V12() ext-real set
Z is V11() V12() ext-real Element of REAL
1 / Z is V11() V12() ext-real Element of REAL
K39(Z) is V11() V12() ext-real set
K37(1,K39(Z)) is V11() V12() ext-real set
x is open V62() V63() V64() Element of K6(REAL)
id x is V13() V16( REAL ) V17( REAL ) V18() V52() V53() V54() Element of K6(K7(REAL,REAL))
x is V13() V16( REAL ) V17( REAL ) V18() V52() V53() V54() Element of K6(K7(REAL,REAL))
() * x is V13() V16( REAL ) V17( REAL ) V18() V52() V53() V54() Element of K6(K7(REAL,REAL))
(1 / Z) (#) (() * x) is V13() V16( REAL ) V17( REAL ) V18() V52() V53() V54() Element of K6(K7(REAL,REAL))
((1 / Z) (#) (() * x)) - (id x) is V13() V16( REAL ) V17( REAL ) V18() V52() V53() V54() Element of K6(K7(REAL,REAL))
- (id x) is V13() V18() V52() set
K38(1) (#) (id x) is V13() V18() set
((1 / Z) (#) (() * x)) + (- (id x)) is V13() V18() set
dom (((1 / Z) (#) (() * x)) - (id x)) is V62() V63() V64() Element of K6(REAL)
(((1 / Z) (#) (() * x)) - (id x)) `| x is V13() V16( REAL ) V17( REAL ) V18() V52() V53() V54() Element of K6(K7(REAL,REAL))
dom ((1 / Z) (#) (() * x)) is V62() V63() V64() Element of K6(REAL)
dom (id x) is V62() V63() V64() Element of K6(REAL)
(dom ((1 / Z) (#) (() * x))) /\ (dom (id x)) is V62() V63() V64() Element of K6(REAL)
dom (() * x) is V62() V63() V64() Element of K6(REAL)
f is V11() V12() ext-real Element of REAL
x . f is V11() V12() ext-real Element of REAL
Z * f is V11() V12() ext-real Element of REAL
(Z * f) + 0 is V11() V12() ext-real Element of REAL
x is V11() V12() ext-real Element of REAL
(id x) . x is V11() V12() ext-real Element of REAL
1 * x is V11() V12() ext-real Element of REAL
(1 * x) + 0 is V11() V12() ext-real Element of REAL
x is V11() V12() ext-real Element of REAL
x . x is V11() V12() ext-real Element of REAL
cos . (x . x) is V11() V12() ext-real Element of REAL
x is V11() V12() ext-real Element of REAL
((((1 / Z) (#) (() * x)) - (id x)) `| x) . x is V11() V12() ext-real Element of REAL
Z * x is V11() V12() ext-real Element of REAL
sin . (Z * x) is V11() V12() ext-real Element of REAL
cos . (Z * x) is V11() V12() ext-real Element of REAL
(cos . (Z * x)) ^2 is V11() V12() ext-real Element of REAL
K37((cos . (Z * x)),(cos . (Z * x))) is V11() V12() ext-real set
(sin . (Z * x)) - ((cos . (Z * x)) ^2) is V11() V12() ext-real Element of REAL
K38(((cos . (Z * x)) ^2)) is V11() V12() ext-real set
K36((sin . (Z * x)),K38(((cos . (Z * x)) ^2))) is V11() V12() ext-real set
((sin . (Z * x)) - ((cos . (Z * x)) ^2)) / ((cos . (Z * x)) ^2) is V11() V12() ext-real Element of REAL
K39(((cos . (Z * x)) ^2)) is V11() V12() ext-real set
K37(((sin . (Z * x)) - ((cos . (Z * x)) ^2)),K39(((cos . (Z * x)) ^2))) is V11() V12() ext-real set
x . x is V11() V12() ext-real Element of REAL
(Z * x) + 0 is V11() V12() ext-real Element of REAL
cos . (x . x) is V11() V12() ext-real Element of REAL
diff (((1 / Z) (#) (() * x)),x) is V11() V12() ext-real Element of REAL
diff ((id x),x) is V11() V12() ext-real Element of REAL
(diff (((1 / Z) (#) (() * x)),x)) - (diff ((id x),x)) is V11() V12() ext-real Element of REAL
K38((diff ((id x),x))) is V11() V12() ext-real set
K36((diff (((1 / Z) (#) (() * x)),x)),K38((diff ((id x),x)))) is V11() V12() ext-real set
((1 / Z) (#) (() * x)) `| x is V13() V16( REAL ) V17( REAL ) V18() V52() V53() V54() Element of K6(K7(REAL,REAL))
(((1 / Z) (#) (() * x)) `| x) . x is V11() V12() ext-real Element of REAL
((((1 / Z) (#) (() * x)) `| x) . x) - (diff ((id x),x)) is V11() V12() ext-real Element of REAL
K36(((((1 / Z) (#) (() * x)) `| x) . x),K38((diff ((id x),x)))) is V11() V12() ext-real set
diff ((() * x),x) is V11() V12() ext-real Element of REAL
(1 / Z) * (diff ((() * x),x)) is V11() V12() ext-real Element of REAL
((1 / Z) * (diff ((() * x),x))) - (diff ((id x),x)) is V11() V12() ext-real Element of REAL
K36(((1 / Z) * (diff ((() * x),x))),K38((diff ((id x),x)))) is V11() V12() ext-real set
(() * x) `| x is V13() V16( REAL ) V17( REAL ) V18() V52() V53() V54() Element of K6(K7(REAL,REAL))
((() * x) `| x) . x is V11() V12() ext-real Element of REAL
(1 / Z) * (((() * x) `| x) . x) is V11() V12() ext-real Element of REAL
((1 / Z) * (((() * x) `| x) . x)) - (diff ((id x),x)) is V11() V12() ext-real Element of REAL
K36(((1 / Z) * (((() * x) `| x) . x)),K38((diff ((id x),x)))) is V11() V12() ext-real set
(id x) `| x is V13() V16( REAL ) V17( REAL ) V18() V52() V53() V54() Element of K6(K7(REAL,REAL))
((id x) `| x) . x is V11() V12() ext-real Element of REAL
((1 / Z) * (((() * x) `| x) . x)) - (((id x) `| x) . x) is V11() V12() ext-real Element of REAL
K38((((id x) `| x) . x)) is V11() V12() ext-real set
K36(((1 / Z) * (((() * x) `| x) . x)),K38((((id x) `| x) . x))) is V11() V12() ext-real set
Z * (sin . (Z * x)) is V11() V12() ext-real Element of REAL
(Z * (sin . (Z * x))) / ((cos . (Z * x)) ^2) is V11() V12() ext-real Element of REAL
K37((Z * (sin . (Z * x))),K39(((cos . (Z * x)) ^2))) is V11() V12() ext-real set
(1 / Z) * ((Z * (sin . (Z * x))) / ((cos . (Z * x)) ^2)) is V11() V12() ext-real Element of REAL
((1 / Z) * ((Z * (sin . (Z * x))) / ((cos . (Z * x)) ^2))) - (((id x) `| x) . x) is V11() V12() ext-real Element of REAL
K36(((1 / Z) * ((Z * (sin . (Z * x))) / ((cos . (Z * x)) ^2))),K38((((id x) `| x) . x))) is V11() V12() ext-real set
((1 / Z) * ((Z * (sin . (Z * x))) / ((cos . (Z * x)) ^2))) - 1 is V11() V12() ext-real Element of REAL
K36(((1 / Z) * ((Z * (sin . (Z * x))) / ((cos . (Z * x)) ^2))),K38(1)) is V11() V12() ext-real set
1 * (Z * (sin . (Z * x))) is V11() V12() ext-real Element of REAL
Z * ((cos . (Z * x)) ^2) is V11() V12() ext-real Element of REAL
(1 * (Z * (sin . (Z * x)))) / (Z * ((cos . (Z * x)) ^2)) is V11() V12() ext-real Element of REAL
K39((Z * ((cos . (Z * x)) ^2))) is V11() V12() ext-real set
K37((1 * (Z * (sin . (Z * x)))),K39((Z * ((cos . (Z * x)) ^2)))) is V11() V12() ext-real set
((1 * (Z * (sin . (Z * x)))) / (Z * ((cos . (Z * x)) ^2))) - 1 is V11() V12() ext-real Element of REAL
K36(((1 * (Z * (sin . (Z * x)))) / (Z * ((cos . (Z * x)) ^2))),K38(1)) is V11() V12() ext-real set
(sin . (Z * x)) / ((cos . (Z * x)) ^2) is V11() V12() ext-real Element of REAL
K37((sin . (Z * x)),K39(((cos . (Z * x)) ^2))) is V11() V12() ext-real set
((sin . (Z * x)) / ((cos . (Z * x)) ^2)) - 1 is V11() V12() ext-real Element of REAL
K36(((sin . (Z * x)) / ((cos . (Z * x)) ^2)),K38(1)) is V11() V12() ext-real set
((cos . (Z * x)) ^2) / ((cos . (Z * x)) ^2) is V11() V12() ext-real Element of REAL
K37(((cos . (Z * x)) ^2),K39(((cos . (Z * x)) ^2))) is V11() V12() ext-real set
((sin . (Z * x)) / ((cos . (Z * x)) ^2)) - (((cos . (Z * x)) ^2) / ((cos . (Z * x)) ^2)) is V11() V12() ext-real Element of REAL
K38((((cos . (Z * x)) ^2) / ((cos . (Z * x)) ^2))) is V11() V12() ext-real set
K36(((sin . (Z * x)) / ((cos . (Z * x)) ^2)),K38((((cos . (Z * x)) ^2) / ((cos . (Z * x)) ^2)))) is V11() V12() ext-real set
x is V11() V12() ext-real Element of REAL
((((1 / Z) (#) (() * x)) - (id x)) `| x) . x is V11() V12() ext-real Element of REAL
Z * x is V11() V12() ext-real Element of REAL
sin . (Z * x) is V11() V12() ext-real Element of REAL
cos . (Z * x) is V11() V12() ext-real Element of REAL
(cos . (Z * x)) ^2 is V11() V12() ext-real Element of REAL
K37((cos . (Z * x)),(cos . (Z * x))) is V11() V12() ext-real set
(sin . (Z * x)) - ((cos . (Z * x)) ^2) is V11() V12() ext-real Element of REAL
K38(((cos . (Z * x)) ^2)) is V11() V12() ext-real set
K36((sin . (Z * x)),K38(((cos . (Z * x)) ^2))) is V11() V12() ext-real set
((sin . (Z * x)) - ((cos . (Z * x)) ^2)) / ((cos . (Z * x)) ^2) is V11() V12() ext-real Element of REAL
K39(((cos . (Z * x)) ^2)) is V11() V12() ext-real set
K37(((sin . (Z * x)) - ((cos . (Z * x)) ^2)),K39(((cos . (Z * x)) ^2))) is V11() V12() ext-real set
Z is V11() V12() ext-real Element of REAL
1 / Z is V11() V12() ext-real Element of REAL
K39(Z) is V11() V12() ext-real set
K37(1,K39(Z)) is V11() V12() ext-real set
- (1 / Z) is V11() V12() ext-real Element of REAL
x is open V62() V63() V64() Element of K6(REAL)
id x is V13() V16( REAL ) V17( REAL ) V18() V52() V53() V54() Element of K6(K7(REAL,REAL))
x is V13() V16( REAL ) V17( REAL ) V18() V52() V53() V54() Element of K6(K7(REAL,REAL))
() * x is V13() V16( REAL ) V17( REAL ) V18() V52() V53() V54() Element of K6(K7(REAL,REAL))
(- (1 / Z)) (#) (() * x) is V13() V16( REAL ) V17( REAL ) V18() V52() V53() V54() Element of K6(K7(REAL,REAL))
((- (1 / Z)) (#) (() * x)) - (id x) is V13() V16( REAL ) V17( REAL ) V18() V52() V53() V54() Element of K6(K7(REAL,REAL))
- (id x) is V13() V18() V52() set
K38(1) (#) (id x) is V13() V18() set
((- (1 / Z)) (#) (() * x)) + (- (id x)) is V13() V18() set
dom (((- (1 / Z)) (#) (() * x)) - (id x)) is V62() V63() V64() Element of K6(REAL)
(((- (1 / Z)) (#) (() * x)) - (id x)) `| x is V13() V16( REAL ) V17( REAL ) V18() V52() V53() V54() Element of K6(K7(REAL,REAL))
dom ((- (1 / Z)) (#) (() * x)) is V62() V63() V64() Element of K6(REAL)
dom (id x) is V62() V63() V64() Element of K6(REAL)
(dom ((- (1 / Z)) (#) (() * x))) /\ (dom (id x)) is V62() V63() V64() Element of K6(REAL)
dom (() * x) is V62() V63() V64() Element of K6(REAL)
f is V11() V12() ext-real Element of REAL
x . f is V11() V12() ext-real Element of REAL
Z * f is V11() V12() ext-real Element of REAL
(Z * f) + 0 is V11() V12() ext-real Element of REAL
x is V11() V12() ext-real Element of REAL
(id x) . x is V11() V12() ext-real Element of REAL
1 * x is V11() V12() ext-real Element of REAL
(1 * x) + 0 is V11() V12() ext-real Element of REAL
x is V11() V12() ext-real Element of REAL
x . x is V11() V12() ext-real Element of REAL
sin . (x . x) is V11() V12() ext-real Element of REAL
x is V11() V12() ext-real Element of REAL
((((- (1 / Z)) (#) (() * x)) - (id x)) `| x) . x is V11() V12() ext-real Element of REAL
Z * x is V11() V12() ext-real Element of REAL
cos . (Z * x) is V11() V12() ext-real Element of REAL
sin . (Z * x) is V11() V12() ext-real Element of REAL
(sin . (Z * x)) ^2 is V11() V12() ext-real Element of REAL
K37((sin . (Z * x)),(sin . (Z * x))) is V11() V12() ext-real set
(cos . (Z * x)) - ((sin . (Z * x)) ^2) is V11() V12() ext-real Element of REAL
K38(((sin . (Z * x)) ^2)) is V11() V12() ext-real set
K36((cos . (Z * x)),K38(((sin . (Z * x)) ^2))) is V11() V12() ext-real set
((cos . (Z * x)) - ((sin . (Z * x)) ^2)) / ((sin . (Z * x)) ^2) is V11() V12() ext-real Element of REAL
K39(((sin . (Z * x)) ^2)) is V11() V12() ext-real set
K37(((cos . (Z * x)) - ((sin . (Z * x)) ^2)),K39(((sin . (Z * x)) ^2))) is V11() V12() ext-real set
x . x is V11() V12() ext-real Element of REAL
(Z * x) + 0 is V11() V12() ext-real Element of REAL
sin . (x . x) is V11() V12() ext-real Element of REAL
diff (((- (1 / Z)) (#) (() * x)),x) is V11() V12() ext-real Element of REAL
diff ((id x),x) is V11() V12() ext-real Element of REAL
(diff (((- (1 / Z)) (#) (() * x)),x)) - (diff ((id x),x)) is V11() V12() ext-real Element of REAL
K38((diff ((id x),x))) is V11() V12() ext-real set
K36((diff (((- (1 / Z)) (#) (() * x)),x)),K38((diff ((id x),x)))) is V11() V12() ext-real set
((- (1 / Z)) (#) (() * x)) `| x is V13() V16( REAL ) V17( REAL ) V18() V52() V53() V54() Element of K6(K7(REAL,REAL))
(((- (1 / Z)) (#) (() * x)) `| x) . x is V11() V12() ext-real Element of REAL
((((- (1 / Z)) (#) (() * x)) `| x) . x) - (diff ((id x),x)) is V11() V12() ext-real Element of REAL
K36(((((- (1 / Z)) (#) (() * x)) `| x) . x),K38((diff ((id x),x)))) is V11() V12() ext-real set
diff ((() * x),x) is V11() V12() ext-real Element of REAL
(- (1 / Z)) * (diff ((() * x),x)) is V11() V12() ext-real Element of REAL
((- (1 / Z)) * (diff ((() * x),x))) - (diff ((id x),x)) is V11() V12() ext-real Element of REAL
K36(((- (1 / Z)) * (diff ((() * x),x))),K38((diff ((id x),x)))) is V11() V12() ext-real set
(() * x) `| x is V13() V16( REAL ) V17( REAL ) V18() V52() V53() V54() Element of K6(K7(REAL,REAL))
((() * x) `| x) . x is V11() V12() ext-real Element of REAL
(- (1 / Z)) * (((() * x) `| x) . x) is V11() V12() ext-real Element of REAL
((- (1 / Z)) * (((() * x) `| x) . x)) - (diff ((id x),x)) is V11() V12() ext-real Element of REAL
K36(((- (1 / Z)) * (((() * x) `| x) . x)),K38((diff ((id x),x)))) is V11() V12() ext-real set
(id x) `| x is V13() V16( REAL ) V17( REAL ) V18() V52() V53() V54() Element of K6(K7(REAL,REAL))
((id x) `| x) . x is V11() V12() ext-real Element of REAL
((- (1 / Z)) * (((() * x) `| x) . x)) - (((id x) `| x) . x) is V11() V12() ext-real Element of REAL
K38((((id x) `| x) . x)) is V11() V12() ext-real set
K36(((- (1 / Z)) * (((() * x) `| x) . x)),K38((((id x) `| x) . x))) is V11() V12() ext-real set
Z * (cos . (Z * x)) is V11() V12() ext-real Element of REAL
(Z * (cos . (Z * x))) / ((sin . (Z * x)) ^2) is V11() V12() ext-real Element of REAL
K37((Z * (cos . (Z * x))),K39(((sin . (Z * x)) ^2))) is V11() V12() ext-real set
- ((Z * (cos . (Z * x))) / ((sin . (Z * x)) ^2)) is V11() V12() ext-real Element of REAL
(- (1 / Z)) * (- ((Z * (cos . (Z * x))) / ((sin . (Z * x)) ^2))) is V11() V12() ext-real Element of REAL
((- (1 / Z)) * (- ((Z * (cos . (Z * x))) / ((sin . (Z * x)) ^2)))) - (((id x) `| x) . x) is V11() V12() ext-real Element of REAL
K36(((- (1 / Z)) * (- ((Z * (cos . (Z * x))) / ((sin . (Z * x)) ^2)))),K38((((id x) `| x) . x))) is V11() V12() ext-real set
- 1 is V11() V12() ext-real non positive V47() Element of REAL
(- 1) / Z is V11() V12() ext-real Element of REAL
K37((- 1),K39(Z)) is V11() V12() ext-real set
- (cos . (Z * x)) is V11() V12() ext-real Element of REAL
Z * (- (cos . (Z * x))) is V11() V12() ext-real Element of REAL
(Z * (- (cos . (Z * x)))) / ((sin . (Z * x)) ^2) is V11() V12() ext-real Element of REAL
K37((Z * (- (cos . (Z * x)))),K39(((sin . (Z * x)) ^2))) is V11() V12() ext-real set
((- 1) / Z) * ((Z * (- (cos . (Z * x)))) / ((sin . (Z * x)) ^2)) is V11() V12() ext-real Element of REAL
(((- 1) / Z) * ((Z * (- (cos . (Z * x)))) / ((sin . (Z * x)) ^2))) - 1 is V11() V12() ext-real Element of REAL
K36((((- 1) / Z) * ((Z * (- (cos . (Z * x)))) / ((sin . (Z * x)) ^2))),K38(1)) is V11() V12() ext-real set
(- 1) * (Z * (- (cos . (Z * x)))) is V11() V12() ext-real Element of REAL
Z * ((sin . (Z * x)) ^2) is V11() V12() ext-real Element of REAL
((- 1) * (Z * (- (cos . (Z * x))))) / (Z * ((sin . (Z * x)) ^2)) is V11() V12() ext-real Element of REAL
K39((Z * ((sin . (Z * x)) ^2))) is V11() V12() ext-real set
K37(((- 1) * (Z * (- (cos . (Z * x))))),K39((Z * ((sin . (Z * x)) ^2)))) is V11() V12() ext-real set
(((- 1) * (Z * (- (cos . (Z * x))))) / (Z * ((sin . (Z * x)) ^2))) - 1 is V11() V12() ext-real Element of REAL
K36((((- 1) * (Z * (- (cos . (Z * x))))) / (Z * ((sin . (Z * x)) ^2))),K38(1)) is V11() V12() ext-real set
(cos . (Z * x)) * Z is V11() V12() ext-real Element of REAL
((sin . (Z * x)) ^2) * Z is V11() V12() ext-real Element of REAL
((cos . (Z * x)) * Z) / (((sin . (Z * x)) ^2) * Z) is V11() V12() ext-real Element of REAL
K39((((sin . (Z * x)) ^2) * Z)) is V11() V12() ext-real set
K37(((cos . (Z * x)) * Z),K39((((sin . (Z * x)) ^2) * Z))) is V11() V12() ext-real set
(((cos . (Z * x)) * Z) / (((sin . (Z * x)) ^2) * Z)) - 1 is V11() V12() ext-real Element of REAL
K36((((cos . (Z * x)) * Z) / (((sin . (Z * x)) ^2) * Z)),K38(1)) is V11() V12() ext-real set
(cos . (Z * x)) / ((sin . (Z * x)) ^2) is V11() V12() ext-real Element of REAL
K37((cos . (Z * x)),K39(((sin . (Z * x)) ^2))) is V11() V12() ext-real set
((cos . (Z * x)) / ((sin . (Z * x)) ^2)) - 1 is V11() V12() ext-real Element of REAL
K36(((cos . (Z * x)) / ((sin . (Z * x)) ^2)),K38(1)) is V11() V12() ext-real set
((sin . (Z * x)) ^2) / ((sin . (Z * x)) ^2) is V11() V12() ext-real Element of REAL
K37(((sin . (Z * x)) ^2),K39(((sin . (Z * x)) ^2))) is V11() V12() ext-real set
((cos . (Z * x)) / ((sin . (Z * x)) ^2)) - (((sin . (Z * x)) ^2) / ((sin . (Z * x)) ^2)) is V11() V12() ext-real Element of REAL
K38((((sin . (Z * x)) ^2) / ((sin . (Z * x)) ^2))) is V11() V12() ext-real set
K36(((cos . (Z * x)) / ((sin . (Z * x)) ^2)),K38((((sin . (Z * x)) ^2) / ((sin . (Z * x)) ^2)))) is V11() V12() ext-real set
x is V11() V12() ext-real Element of REAL
((((- (1 / Z)) (#) (() * x)) - (id x)) `| x) . x is V11() V12() ext-real Element of REAL
Z * x is V11() V12() ext-real Element of REAL
cos . (Z * x) is V11() V12() ext-real Element of REAL
sin . (Z * x) is V11() V12() ext-real Element of REAL
(sin . (Z * x)) ^2 is V11() V12() ext-real Element of REAL
K37((sin . (Z * x)),(sin . (Z * x))) is V11() V12() ext-real set
(cos . (Z * x)) - ((sin . (Z * x)) ^2) is V11() V12() ext-real Element of REAL
K38(((sin . (Z * x)) ^2)) is V11() V12() ext-real set
K36((cos . (Z * x)),K38(((sin . (Z * x)) ^2))) is V11() V12() ext-real set
((cos . (Z * x)) - ((sin . (Z * x)) ^2)) / ((sin . (Z * x)) ^2) is V11() V12() ext-real Element of REAL
K39(((sin . (Z * x)) ^2)) is V11() V12() ext-real set
K37(((cos . (Z * x)) - ((sin . (Z * x)) ^2)),K39(((sin . (Z * x)) ^2))) is V11() V12() ext-real set
Z is V11() V12() ext-real Element of REAL
x is V11() V12() ext-real Element of REAL
x is open V62() V63() V64() Element of K6(REAL)
f is V13() V16( REAL ) V17( REAL ) V18() V52() V53() V54() Element of K6(K7(REAL,REAL))
f (#) () is V13() V16( REAL ) V17( REAL ) V18() V52() V53() V54() Element of K6(K7(REAL,REAL))
dom (f (#) ()) is V62() V63() V64() Element of K6(REAL)
(f (#) ()) `| x is V13() V16( REAL ) V17( REAL ) V18() V52() V53() V54() Element of K6(K7(REAL,REAL))
dom f is V62() V63() V64() Element of K6(REAL)
(dom f) /\ (dom ()) is V62() V63() V64() Element of K6(REAL)
x is V11() V12() ext-real Element of REAL
diff ((),x) is V11() V12() ext-real Element of REAL
sin . x is V11() V12() ext-real Element of REAL
cos . x is V11() V12() ext-real Element of REAL
(cos . x) ^2 is V11() V12() ext-real Element of REAL
K37((cos . x),(cos . x)) is V11() V12() ext-real set
(sin . x) / ((cos . x) ^2) is V11() V12() ext-real Element of REAL
K39(((cos . x) ^2)) is V11() V12() ext-real set
K37((sin . x),K39(((cos . x) ^2))) is V11() V12() ext-real set
x is V11() V12() ext-real Element of REAL
x is V11() V12() ext-real Element of REAL
((f (#) ()) `| x) . x is V11() V12() ext-real Element of REAL
cos . x is V11() V12() ext-real Element of REAL
Z / (cos . x) is V11() V12() ext-real Element of REAL
K39((cos . x)) is V11() V12() ext-real set
K37(Z,K39((cos . x))) is V11() V12() ext-real set
Z * x is V11() V12() ext-real Element of REAL
(Z * x) + x is V11() V12() ext-real Element of REAL
sin . x is V11() V12() ext-real Element of REAL
((Z * x) + x) * (sin . x) is V11() V12() ext-real Element of REAL
(cos . x) ^2 is V11() V12() ext-real Element of REAL
K37((cos . x),(cos . x)) is V11() V12() ext-real set
(((Z * x) + x) * (sin . x)) / ((cos . x) ^2) is V11() V12() ext-real Element of REAL
K39(((cos . x) ^2)) is V11() V12() ext-real set
K37((((Z * x) + x) * (sin . x)),K39(((cos . x) ^2))) is V11() V12() ext-real set
(Z / (cos . x)) + ((((Z * x) + x) * (sin . x)) / ((cos . x) ^2)) is V11() V12() ext-real Element of REAL
() . x is V11() V12() ext-real Element of REAL
diff (f,x) is V11() V12() ext-real Element of REAL
(() . x) * (diff (f,x)) is V11() V12() ext-real Element of REAL
f . x is V11() V12() ext-real Element of REAL
diff ((),x) is V11() V12() ext-real Element of REAL
(f . x) * (diff ((),x)) is V11() V12() ext-real Element of REAL
((() . x) * (diff (f,x))) + ((f . x) * (diff ((),x))) is V11() V12() ext-real Element of REAL
f `| x is V13() V16( REAL ) V17( REAL ) V18() V52() V53() V54() Element of K6(K7(REAL,REAL))
(f `| x) . x is V11() V12() ext-real Element of REAL
(() . x) * ((f `| x) . x) is V11() V12() ext-real Element of REAL
((() . x) * ((f `| x) . x)) + ((f . x) * (diff ((),x))) is V11() V12() ext-real Element of REAL
(() . x) * Z is V11() V12() ext-real Element of REAL
((() . x) * Z) + ((f . x) * (diff ((),x))) is V11() V12() ext-real Element of REAL
((Z * x) + x) * (diff ((),x)) is V11() V12() ext-real Element of REAL
((() . x) * Z) + (((Z * x) + x) * (diff ((),x))) is V11() V12() ext-real Element of REAL
(sin . x) / ((cos . x) ^2) is V11() V12() ext-real Element of REAL
K37((sin . x),K39(((cos . x) ^2))) is V11() V12() ext-real set
((Z * x) + x) * ((sin . x) / ((cos . x) ^2)) is V11() V12() ext-real Element of REAL
((() . x) * Z) + (((Z * x) + x) * ((sin . x) / ((cos . x) ^2))) is V11() V12() ext-real Element of REAL
x is V11() V12() ext-real Element of REAL
((f (#) ()) `| x) . x is V11() V12() ext-real Element of REAL
cos . x is V11() V12() ext-real Element of REAL
Z / (cos . x) is V11() V12() ext-real Element of REAL
K39((cos . x)) is V11() V12() ext-real set
K37(Z,K39((cos . x))) is V11() V12() ext-real set
Z * x is V11() V12() ext-real Element of REAL
(Z * x) + x is V11() V12() ext-real Element of REAL
sin . x is V11() V12() ext-real Element of REAL
((Z * x) + x) * (sin . x) is V11() V12() ext-real Element of REAL
(cos . x) ^2 is V11() V12() ext-real Element of REAL
K37((cos . x),(cos . x)) is V11() V12() ext-real set
(((Z * x) + x) * (sin . x)) / ((cos . x) ^2) is V11() V12() ext-real Element of REAL
K39(((cos . x) ^2)) is V11() V12() ext-real set
K37((((Z * x) + x) * (sin . x)),K39(((cos . x) ^2))) is V11() V12() ext-real set
(Z / (cos . x)) + ((((Z * x) + x) * (sin . x)) / ((cos . x) ^2)) is V11() V12() ext-real Element of REAL
Z is V11() V12() ext-real Element of REAL
x is V11() V12() ext-real Element of REAL
x is open V62() V63() V64() Element of K6(REAL)
f is V13() V16( REAL ) V17( REAL ) V18() V52() V53() V54() Element of K6(K7(REAL,REAL))
f (#) () is V13() V16( REAL ) V17( REAL ) V18() V52() V53() V54() Element of K6(K7(REAL,REAL))
dom (f (#) ()) is V62() V63() V64() Element of K6(REAL)
(f (#) ()) `| x is V13() V16( REAL ) V17( REAL ) V18() V52() V53() V54() Element of K6(K7(REAL,REAL))
dom f is V62() V63() V64() Element of K6(REAL)
(dom f) /\ (dom ()) is V62() V63() V64() Element of K6(REAL)
x is V11() V12() ext-real Element of REAL
diff ((),x) is V11() V12() ext-real Element of REAL
cos . x is V11() V12() ext-real Element of REAL
sin . x is V11() V12() ext-real Element of REAL
(sin . x) ^2 is V11() V12() ext-real Element of REAL
K37((sin . x),(sin . x)) is V11() V12() ext-real set
(cos . x) / ((sin . x) ^2) is V11() V12() ext-real Element of REAL
K39(((sin . x) ^2)) is V11() V12() ext-real set
K37((cos . x),K39(((sin . x) ^2))) is V11() V12() ext-real set
- ((cos . x) / ((sin . x) ^2)) is V11() V12() ext-real Element of REAL
x is V11() V12() ext-real Element of REAL
x is V11() V12() ext-real Element of REAL
((f (#) ()) `| x) . x is V11() V12() ext-real Element of REAL
sin . x is V11() V12() ext-real Element of REAL
Z / (sin . x) is V11() V12() ext-real Element of REAL
K39((sin . x)) is V11() V12() ext-real set
K37(Z,K39((sin . x))) is V11() V12() ext-real set
Z * x is V11() V12() ext-real Element of REAL
(Z * x) + x is V11() V12() ext-real Element of REAL
cos . x is V11() V12() ext-real Element of REAL
((Z * x) + x) * (cos . x) is V11() V12() ext-real Element of REAL
(sin . x) ^2 is V11() V12() ext-real Element of REAL
K37((sin . x),(sin . x)) is V11() V12() ext-real set
(((Z * x) + x) * (cos . x)) / ((sin . x) ^2) is V11() V12() ext-real Element of REAL
K39(((sin . x) ^2)) is V11() V12() ext-real set
K37((((Z * x) + x) * (cos . x)),K39(((sin . x) ^2))) is V11() V12() ext-real set
(Z / (sin . x)) - ((((Z * x) + x) * (cos . x)) / ((sin . x) ^2)) is V11() V12() ext-real Element of REAL
K38(((((Z * x) + x) * (cos . x)) / ((sin . x) ^2))) is V11() V12() ext-real set
K36((Z / (sin . x)),K38(((((Z * x) + x) * (cos . x)) / ((sin . x) ^2)))) is V11() V12() ext-real set
() . x is V11() V12() ext-real Element of REAL
diff (f,x) is V11() V12() ext-real Element of REAL
(() . x) * (diff (f,x)) is V11() V12() ext-real Element of REAL
f . x is V11() V12() ext-real Element of REAL
diff ((),x) is V11() V12() ext-real Element of REAL
(f . x) * (diff ((),x)) is V11() V12() ext-real Element of REAL
((() . x) * (diff (f,x))) + ((f . x) * (diff ((),x))) is V11() V12() ext-real Element of REAL
f `| x is V13() V16( REAL ) V17( REAL ) V18() V52() V53() V54() Element of K6(K7(REAL,REAL))
(f `| x) . x is V11() V12() ext-real Element of REAL
(() . x) * ((f `| x) . x) is V11() V12() ext-real Element of REAL
((() . x) * ((f `| x) . x)) + ((f . x) * (diff ((),x))) is V11() V12() ext-real Element of REAL
(() . x) * Z is V11() V12() ext-real Element of REAL
((() . x) * Z) + ((f . x) * (diff ((),x))) is V11() V12() ext-real Element of REAL
((Z * x) + x) * (diff ((),x)) is V11() V12() ext-real Element of REAL
((() . x) * Z) + (((Z * x) + x) * (diff ((),x))) is V11() V12() ext-real Element of REAL
(cos . x) / ((sin . x) ^2) is V11() V12() ext-real Element of REAL
K37((cos . x),K39(((sin . x) ^2))) is V11() V12() ext-real set
- ((cos . x) / ((sin . x) ^2)) is V11() V12() ext-real Element of REAL
((Z * x) + x) * (- ((cos . x) / ((sin . x) ^2))) is V11() V12() ext-real Element of REAL
((() . x) * Z) + (((Z * x) + x) * (- ((cos . x) / ((sin . x) ^2)))) is V11() V12() ext-real Element of REAL
x is V11() V12() ext-real Element of REAL
((f (#) ()) `| x) . x is V11() V12() ext-real Element of REAL
sin . x is V11() V12() ext-real Element of REAL
Z / (sin . x) is V11() V12() ext-real Element of REAL
K39((sin . x)) is V11() V12() ext-real set
K37(Z,K39((sin . x))) is V11() V12() ext-real set
Z * x is V11() V12() ext-real Element of REAL
(Z * x) + x is V11() V12() ext-real Element of REAL
cos . x is V11() V12() ext-real Element of REAL
((Z * x) + x) * (cos . x) is V11() V12() ext-real Element of REAL
(sin . x) ^2 is V11() V12() ext-real Element of REAL
K37((sin . x),(sin . x)) is V11() V12() ext-real set
(((Z * x) + x) * (cos . x)) / ((sin . x) ^2) is V11() V12() ext-real Element of REAL
K39(((sin . x) ^2)) is V11() V12() ext-real set
K37((((Z * x) + x) * (cos . x)),K39(((sin . x) ^2))) is V11() V12() ext-real set
(Z / (sin . x)) - ((((Z * x) + x) * (cos . x)) / ((sin . x) ^2)) is V11() V12() ext-real Element of REAL
K38(((((Z * x) + x) * (cos . x)) / ((sin . x) ^2))) is V11() V12() ext-real set
K36((Z / (sin . x)),K38(((((Z * x) + x) * (cos . x)) / ((sin . x) ^2)))) is V11() V12() ext-real set
ln (#) () is V13() V16( REAL ) V17( REAL ) V18() V52() V53() V54() Element of K6(K7(REAL,REAL))
dom (ln (#) ()) is V62() V63() V64() Element of K6(REAL)
Z is open V62() V63() V64() Element of K6(REAL)
(ln (#) ()) `| Z is V13() V16( REAL ) V17( REAL ) V18() V52() V53() V54() Element of K6(K7(REAL,REAL))
(dom ln) /\ (dom ()) is V62() V63() V64() Element of K6(REAL)
x is V11() V12() ext-real Element of REAL
diff ((),x) is V11() V12() ext-real Element of REAL
sin . x is V11() V12() ext-real Element of REAL
cos . x is V11() V12() ext-real Element of REAL
(cos . x) ^2 is V11() V12() ext-real Element of REAL
K37((cos . x),(cos . x)) is V11() V12() ext-real set
(sin . x) / ((cos . x) ^2) is V11() V12() ext-real Element of REAL
K39(((cos . x) ^2)) is V11() V12() ext-real set
K37((sin . x),K39(((cos . x) ^2))) is V11() V12() ext-real set
x is V11() V12() ext-real Element of REAL
x is V11() V12() ext-real Element of REAL
x is V11() V12() ext-real Element of REAL
x is V11() V12() ext-real Element of REAL
x is V11() V12() ext-real Element of REAL
diff (ln,x) is V11() V12() ext-real Element of REAL
1 / x is V11() V12() ext-real Element of REAL
K39(x) is V11() V12() ext-real set
K37(1,K39(x)) is V11() V12() ext-real set
x is V11() V12() ext-real Element of REAL
((ln (#) ()) `| Z) . x is V11() V12() ext-real Element of REAL
cos . x is V11() V12() ext-real Element of REAL
1 / (cos . x) is V11() V12() ext-real Element of REAL
K39((cos . x)) is V11() V12() ext-real set
K37(1,K39((cos . x))) is V11() V12() ext-real set
(1 / (cos . x)) / x is V11() V12() ext-real Element of REAL
K39(x) is V11() V12() ext-real set
K37((1 / (cos . x)),K39(x)) is V11() V12() ext-real set
ln . x is V11() V12() ext-real Element of REAL
sin . x is V11() V12() ext-real Element of REAL
(ln . x) * (sin . x) is V11() V12() ext-real Element of REAL
(cos . x) ^2 is V11() V12() ext-real Element of REAL
K37((cos . x),(cos . x)) is V11() V12() ext-real set
((ln . x) * (sin . x)) / ((cos . x) ^2) is V11() V12() ext-real Element of REAL
K39(((cos . x) ^2)) is V11() V12() ext-real set
K37(((ln . x) * (sin . x)),K39(((cos . x) ^2))) is V11() V12() ext-real set
((1 / (cos . x)) / x) + (((ln . x) * (sin . x)) / ((cos . x) ^2)) is V11() V12() ext-real Element of REAL
() . x is V11() V12() ext-real Element of REAL
diff (ln,x) is V11() V12() ext-real Element of REAL
(() . x) * (diff (ln,x)) is V11() V12() ext-real Element of REAL
diff ((),x) is V11() V12() ext-real Element of REAL
(ln . x) * (diff ((),x)) is V11() V12() ext-real Element of REAL
((() . x) * (diff (ln,x))) + ((ln . x) * (diff ((),x))) is V11() V12() ext-real Element of REAL
1 / x is V11() V12() ext-real Element of REAL
K37(1,K39(x)) is V11() V12() ext-real set
(() . x) * (1 / x) is V11() V12() ext-real Element of REAL
((() . x) * (1 / x)) + ((ln . x) * (diff ((),x))) is V11() V12() ext-real Element of REAL
(sin . x) / ((cos . x) ^2) is V11() V12() ext-real Element of REAL
K37((sin . x),K39(((cos . x) ^2))) is V11() V12() ext-real set
(ln . x) * ((sin . x) / ((cos . x) ^2)) is V11() V12() ext-real Element of REAL
((() . x) * (1 / x)) + ((ln . x) * ((sin . x) / ((cos . x) ^2))) is V11() V12() ext-real Element of REAL
x is V11() V12() ext-real Element of REAL
((ln (#) ()) `| Z) . x is V11() V12() ext-real Element of REAL
cos . x is V11() V12() ext-real Element of REAL
1 / (cos . x) is V11() V12() ext-real Element of REAL
K39((cos . x)) is V11() V12() ext-real set
K37(1,K39((cos . x))) is V11() V12() ext-real set
(1 / (cos . x)) / x is V11() V12() ext-real Element of REAL
K39(x) is V11() V12() ext-real set
K37((1 / (cos . x)),K39(x)) is V11() V12() ext-real set
ln . x is V11() V12() ext-real Element of REAL
sin . x is V11() V12() ext-real Element of REAL
(ln . x) * (sin . x) is V11() V12() ext-real Element of REAL
(cos . x) ^2 is V11() V12() ext-real Element of REAL
K37((cos . x),(cos . x)) is V11() V12() ext-real set
((ln . x) * (sin . x)) / ((cos . x) ^2) is V11() V12() ext-real Element of REAL
K39(((cos . x) ^2)) is V11() V12() ext-real set
K37(((ln . x) * (sin . x)),K39(((cos . x) ^2))) is V11() V12() ext-real set
((1 / (cos . x)) / x) + (((ln . x) * (sin . x)) / ((cos . x) ^2)) is V11() V12() ext-real Element of REAL
ln (#) () is V13() V16( REAL ) V17( REAL ) V18() V52() V53() V54() Element of K6(K7(REAL,REAL))
dom (ln (#) ()) is V62() V63() V64() Element of K6(REAL)
Z is open V62() V63() V64() Element of K6(REAL)
(ln (#) ()) `| Z is V13() V16( REAL ) V17( REAL ) V18() V52() V53() V54() Element of K6(K7(REAL,REAL))
(dom ln) /\ (dom ()) is V62() V63() V64() Element of K6(REAL)
x is V11() V12() ext-real Element of REAL
diff ((),x) is V11() V12() ext-real Element of REAL
cos . x is V11() V12() ext-real Element of REAL
sin . x is V11() V12() ext-real Element of REAL
(sin . x) ^2 is V11() V12() ext-real Element of REAL
K37((sin . x),(sin . x)) is V11() V12() ext-real set
(cos . x) / ((sin . x) ^2) is V11() V12() ext-real Element of REAL
K39(((sin . x) ^2)) is V11() V12() ext-real set
K37((cos . x),K39(((sin . x) ^2))) is V11() V12() ext-real set
- ((cos . x) / ((sin . x) ^2)) is V11() V12() ext-real Element of REAL
x is V11() V12() ext-real Element of REAL
x is V11() V12() ext-real Element of REAL
x is V11() V12() ext-real Element of REAL
x is V11() V12() ext-real Element of REAL
x is V11() V12() ext-real Element of REAL
diff (ln,x) is V11() V12() ext-real Element of REAL
1 / x is V11() V12() ext-real Element of REAL
K39(x) is V11() V12() ext-real set
K37(1,K39(x)) is V11() V12() ext-real set
x is V11() V12() ext-real Element of REAL
((ln (#) ()) `| Z) . x is V11() V12() ext-real Element of REAL
sin . x is V11() V12() ext-real Element of REAL
1 / (sin . x) is V11() V12() ext-real Element of REAL
K39((sin . x)) is V11() V12() ext-real set
K37(1,K39((sin . x))) is V11() V12() ext-real set
(1 / (sin . x)) / x is V11() V12() ext-real Element of REAL
K39(x) is V11() V12() ext-real set
K37((1 / (sin . x)),K39(x)) is V11() V12() ext-real set
ln . x is V11() V12() ext-real Element of REAL
cos . x is V11() V12() ext-real Element of REAL
(ln . x) * (cos . x) is V11() V12() ext-real Element of REAL
(sin . x) ^2 is V11() V12() ext-real Element of REAL
K37((sin . x),(sin . x)) is V11() V12() ext-real set
((ln . x) * (cos . x)) / ((sin . x) ^2) is V11() V12() ext-real Element of REAL
K39(((sin . x) ^2)) is V11() V12() ext-real set
K37(((ln . x) * (cos . x)),K39(((sin . x) ^2))) is V11() V12() ext-real set
((1 / (sin . x)) / x) - (((ln . x) * (cos . x)) / ((sin . x) ^2)) is V11() V12() ext-real Element of REAL
K38((((ln . x) * (cos . x)) / ((sin . x) ^2))) is V11() V12() ext-real set
K36(((1 / (sin . x)) / x),K38((((ln . x) * (cos . x)) / ((sin . x) ^2)))) is V11() V12() ext-real set
() . x is V11() V12() ext-real Element of REAL
diff (ln,x) is V11() V12() ext-real Element of REAL
(() . x) * (diff (ln,x)) is V11() V12() ext-real Element of REAL
diff ((),x) is V11() V12() ext-real Element of REAL
(ln . x) * (diff ((),x)) is V11() V12() ext-real Element of REAL
((() . x) * (diff (ln,x))) + ((ln . x) * (diff ((),x))) is V11() V12() ext-real Element of REAL
1 / x is V11() V12() ext-real Element of REAL
K37(1,K39(x)) is V11() V12() ext-real set
(() . x) * (1 / x) is V11() V12() ext-real Element of REAL
((() . x) * (1 / x)) + ((ln . x) * (diff ((),x))) is V11() V12() ext-real Element of REAL
(cos . x) / ((sin . x) ^2) is V11() V12() ext-real Element of REAL
K37((cos . x),K39(((sin . x) ^2))) is V11() V12() ext-real set
- ((cos . x) / ((sin . x) ^2)) is V11() V12() ext-real Element of REAL
(ln . x) * (- ((cos . x) / ((sin . x) ^2))) is V11() V12() ext-real Element of REAL
((() . x) * (1 / x)) + ((ln . x) * (- ((cos . x) / ((sin . x) ^2)))) is V11() V12() ext-real Element of REAL
x is V11() V12() ext-real Element of REAL
((ln (#) ()) `| Z) . x is V11() V12() ext-real Element of REAL
sin . x is V11() V12() ext-real Element of REAL
1 / (sin . x) is V11() V12() ext-real Element of REAL
K39((sin . x)) is V11() V12() ext-real set
K37(1,K39((sin . x))) is V11() V12() ext-real set
(1 / (sin . x)) / x is V11() V12() ext-real Element of REAL
K39(x) is V11() V12() ext-real set
K37((1 / (sin . x)),K39(x)) is V11() V12() ext-real set
ln . x is V11() V12() ext-real Element of REAL
cos . x is V11() V12() ext-real Element of REAL
(ln . x) * (cos . x) is V11() V12() ext-real Element of REAL
(sin . x) ^2 is V11() V12() ext-real Element of REAL
K37((sin . x),(sin . x)) is V11() V12() ext-real set
((ln . x) * (cos . x)) / ((sin . x) ^2) is V11() V12() ext-real Element of REAL
K39(((sin . x) ^2)) is V11() V12() ext-real set
K37(((ln . x) * (cos . x)),K39(((sin . x) ^2))) is V11() V12() ext-real set
((1 / (sin . x)) / x) - (((ln . x) * (cos . x)) / ((sin . x) ^2)) is V11() V12() ext-real Element of REAL
K38((((ln . x) * (cos . x)) / ((sin . x) ^2))) is V11() V12() ext-real set
K36(((1 / (sin . x)) / x),K38((((ln . x) * (cos . x)) / ((sin . x) ^2)))) is V11() V12() ext-real set
Z is open V62() V63() V64() Element of K6(REAL)
id Z is V13() V16( REAL ) V17( REAL ) V18() V52() V53() V54() Element of K6(K7(REAL,REAL))
(id Z) ^ is V13() V16( REAL ) V17( REAL ) V18() V52() V53() V54() Element of K6(K7(REAL,REAL))
((id Z) ^) (#) () is V13() V16( REAL ) V17( REAL ) V18() V52() V53() V54() Element of K6(K7(REAL,REAL))
dom (((id Z) ^) (#) ()) is V62() V63() V64() Element of K6(REAL)
(((id Z) ^) (#) ()) `| Z is V13() V16( REAL ) V17( REAL ) V18() V52() V53() V54() Element of K6(K7(REAL,REAL))
dom ((id Z) ^) is V62() V63() V64() Element of K6(REAL)
(dom ((id Z) ^)) /\ (dom ()) is V62() V63() V64() Element of K6(REAL)
x is V11() V12() ext-real Element of REAL
diff ((),x) is V11() V12() ext-real Element of REAL
sin . x is V11() V12() ext-real Element of REAL
cos . x is V11() V12() ext-real Element of REAL
(cos . x) ^2 is V11() V12() ext-real Element of REAL
K37((cos . x),(cos . x)) is V11() V12() ext-real set
(sin . x) / ((cos . x) ^2) is V11() V12() ext-real Element of REAL
K39(((cos . x) ^2)) is V11() V12() ext-real set
K37((sin . x),K39(((cos . x) ^2))) is V11() V12() ext-real set
x is V11() V12() ext-real Element of REAL
x is V11() V12() ext-real Element of REAL
((((id Z) ^) (#) ()) `| Z) . x is V11() V12() ext-real Element of REAL
cos . x is V11() V12() ext-real Element of REAL
1 / (cos . x) is V11() V12() ext-real Element of REAL
K39((cos . x)) is V11() V12() ext-real set
K37(1,K39((cos . x))) is V11() V12() ext-real set
x ^2 is V11() V12() ext-real Element of REAL
K37(x,x) is V11() V12() ext-real set
(1 / (cos . x)) / (x ^2) is V11() V12() ext-real Element of REAL
K39((x ^2)) is V11() V12() ext-real set
K37((1 / (cos . x)),K39((x ^2))) is V11() V12() ext-real set
- ((1 / (cos . x)) / (x ^2)) is V11() V12() ext-real Element of REAL
sin . x is V11() V12() ext-real Element of REAL
(sin . x) / x is V11() V12() ext-real Element of REAL
K39(x) is V11() V12() ext-real set
K37((sin . x),K39(x)) is V11() V12() ext-real set
(cos . x) ^2 is V11() V12() ext-real Element of REAL
K37((cos . x),(cos . x)) is V11() V12() ext-real set
((sin . x) / x) / ((cos . x) ^2) is V11() V12() ext-real Element of REAL
K39(((cos . x) ^2)) is V11() V12() ext-real set
K37(((sin . x) / x),K39(((cos . x) ^2))) is V11() V12() ext-real set
(- ((1 / (cos . x)) / (x ^2))) + (((sin . x) / x) / ((cos . x) ^2)) is V11() V12() ext-real Element of REAL
() . x is V11() V12() ext-real Element of REAL
diff (((id Z) ^),x) is V11() V12() ext-real Element of REAL
(() . x) * (diff (((id Z) ^),x)) is V11() V12() ext-real Element of REAL
((id Z) ^) . x is V11() V12() ext-real Element of REAL
diff ((),x) is V11() V12() ext-real Element of REAL
(((id Z) ^) . x) * (diff ((),x)) is V11() V12() ext-real Element of REAL
((() . x) * (diff (((id Z) ^),x))) + ((((id Z) ^) . x) * (diff ((),x))) is V11() V12() ext-real Element of REAL
((id Z) ^) `| Z is V13() V16( REAL ) V17( REAL ) V18() V52() V53() V54() Element of K6(K7(REAL,REAL))
(((id Z) ^) `| Z) . x is V11() V12() ext-real Element of REAL
(() . x) * ((((id Z) ^) `| Z) . x) is V11() V12() ext-real Element of REAL
((() . x) * ((((id Z) ^) `| Z) . x)) + ((((id Z) ^) . x) * (diff ((),x))) is V11() V12() ext-real Element of REAL
1 / (x ^2) is V11() V12() ext-real Element of REAL
K37(1,K39((x ^2))) is V11() V12() ext-real set
- (1 / (x ^2)) is V11() V12() ext-real Element of REAL
(() . x) * (- (1 / (x ^2))) is V11() V12() ext-real Element of REAL
((() . x) * (- (1 / (x ^2)))) + ((((id Z) ^) . x) * (diff ((),x))) is V11() V12() ext-real Element of REAL
(() . x) * (1 / (x ^2)) is V11() V12() ext-real Element of REAL
- ((() . x) * (1 / (x ^2))) is V11() V12() ext-real Element of REAL
(sin . x) / ((cos . x) ^2) is V11() V12() ext-real Element of REAL
K37((sin . x),K39(((cos . x) ^2))) is V11() V12() ext-real set
(((id Z) ^) . x) * ((sin . x) / ((cos . x) ^2)) is V11() V12() ext-real Element of REAL
(- ((() . x) * (1 / (x ^2)))) + ((((id Z) ^) . x) * ((sin . x) / ((cos . x) ^2))) is V11() V12() ext-real Element of REAL
(cos . x) " is V11() V12() ext-real Element of REAL
((cos . x) ") * (1 / (x ^2)) is V11() V12() ext-real Element of REAL
- (((cos . x) ") * (1 / (x ^2))) is V11() V12() ext-real Element of REAL
(- (((cos . x) ") * (1 / (x ^2)))) + ((((id Z) ^) . x) * ((sin . x) / ((cos . x) ^2))) is V11() V12() ext-real Element of REAL
(id Z) . x is V11() V12() ext-real Element of REAL
((id Z) . x) " is V11() V12() ext-real Element of REAL
(((id Z) . x) ") * ((sin . x) / ((cos . x) ^2)) is V11() V12() ext-real Element of REAL
(- ((1 / (cos . x)) / (x ^2))) + ((((id Z) . x) ") * ((sin . x) / ((cos . x) ^2))) is V11() V12() ext-real Element of REAL
1 / x is V11() V12() ext-real Element of REAL
K37(1,K39(x)) is V11() V12() ext-real set
(1 / x) * ((sin . x) / ((cos . x) ^2)) is V11() V12() ext-real Element of REAL
(- ((1 / (cos . x)) / (x ^2))) + ((1 / x) * ((sin . x) / ((cos . x) ^2))) is V11() V12() ext-real Element of REAL
x is V11() V12() ext-real Element of REAL
((((id Z) ^) (#) ()) `| Z) . x is V11() V12() ext-real Element of REAL
cos . x is V11() V12() ext-real Element of REAL
1 / (cos . x) is V11() V12() ext-real Element of REAL
K39((cos . x)) is V11() V12() ext-real set
K37(1,K39((cos . x))) is V11() V12() ext-real set
x ^2 is V11() V12() ext-real Element of REAL
K37(x,x) is V11() V12() ext-real set
(1 / (cos . x)) / (x ^2) is V11() V12() ext-real Element of REAL
K39((x ^2)) is V11() V12() ext-real set
K37((1 / (cos . x)),K39((x ^2))) is V11() V12() ext-real set
- ((1 / (cos . x)) / (x ^2)) is V11() V12() ext-real Element of REAL
sin . x is V11() V12() ext-real Element of REAL
(sin . x) / x is V11() V12() ext-real Element of REAL
K39(x) is V11() V12() ext-real set
K37((sin . x),K39(x)) is V11() V12() ext-real set
(cos . x) ^2 is V11() V12() ext-real Element of REAL
K37((cos . x),(cos . x)) is V11() V12() ext-real set
((sin . x) / x) / ((cos . x) ^2) is V11() V12() ext-real Element of REAL
K39(((cos . x) ^2)) is V11() V12() ext-real set
K37(((sin . x) / x),K39(((cos . x) ^2))) is V11() V12() ext-real set
(- ((1 / (cos . x)) / (x ^2))) + (((sin . x) / x) / ((cos . x) ^2)) is V11() V12() ext-real Element of REAL
Z is open V62() V63() V64() Element of K6(REAL)
id Z is V13() V16( REAL ) V17( REAL ) V18() V52() V53() V54() Element of K6(K7(REAL,REAL))
(id Z) ^ is V13() V16( REAL ) V17( REAL ) V18() V52() V53() V54() Element of K6(K7(REAL,REAL))
((id Z) ^) (#) () is V13() V16( REAL ) V17( REAL ) V18() V52() V53() V54() Element of K6(K7(REAL,REAL))
dom (((id Z) ^) (#) ()) is V62() V63() V64() Element of K6(REAL)
(((id Z) ^) (#) ()) `| Z is V13() V16( REAL ) V17( REAL ) V18() V52() V53() V54() Element of K6(K7(REAL,REAL))
dom ((id Z) ^) is V62() V63() V64() Element of K6(REAL)
(dom ((id Z) ^)) /\ (dom ()) is V62() V63() V64() Element of K6(REAL)
x is V11() V12() ext-real Element of REAL
diff ((),x) is V11() V12() ext-real Element of REAL
cos . x is V11() V12() ext-real Element of REAL
sin . x is V11() V12() ext-real Element of REAL
(sin . x) ^2 is V11() V12() ext-real Element of REAL
K37((sin . x),(sin . x)) is V11() V12() ext-real set
(cos . x) / ((sin . x) ^2) is V11() V12() ext-real Element of REAL
K39(((sin . x) ^2)) is V11() V12() ext-real set
K37((cos . x),K39(((sin . x) ^2))) is V11() V12() ext-real set
- ((cos . x) / ((sin . x) ^2)) is V11() V12() ext-real Element of REAL
x is V11() V12() ext-real Element of REAL
x is V11() V12() ext-real Element of REAL
((((id Z) ^) (#) ()) `| Z) . x is V11() V12() ext-real Element of REAL
sin . x is V11() V12() ext-real Element of REAL
1 / (sin . x) is V11() V12() ext-real Element of REAL
K39((sin . x)) is V11() V12() ext-real set
K37(1,K39((sin . x))) is V11() V12() ext-real set
x ^2 is V11() V12() ext-real Element of REAL
K37(x,x) is V11() V12() ext-real set
(1 / (sin . x)) / (x ^2) is V11() V12() ext-real Element of REAL
K39((x ^2)) is V11() V12() ext-real set
K37((1 / (sin . x)),K39((x ^2))) is V11() V12() ext-real set
- ((1 / (sin . x)) / (x ^2)) is V11() V12() ext-real Element of REAL
cos . x is V11() V12() ext-real Element of REAL
(cos . x) / x is V11() V12() ext-real Element of REAL
K39(x) is V11() V12() ext-real set
K37((cos . x),K39(x)) is V11() V12() ext-real set
(sin . x) ^2 is V11() V12() ext-real Element of REAL
K37((sin . x),(sin . x)) is V11() V12() ext-real set
((cos . x) / x) / ((sin . x) ^2) is V11() V12() ext-real Element of REAL
K39(((sin . x) ^2)) is V11() V12() ext-real set
K37(((cos . x) / x),K39(((sin . x) ^2))) is V11() V12() ext-real set
(- ((1 / (sin . x)) / (x ^2))) - (((cos . x) / x) / ((sin . x) ^2)) is V11() V12() ext-real Element of REAL
K38((((cos . x) / x) / ((sin . x) ^2))) is V11() V12() ext-real set
K36((- ((1 / (sin . x)) / (x ^2))),K38((((cos . x) / x) / ((sin . x) ^2)))) is V11() V12() ext-real set
() . x is V11() V12() ext-real Element of REAL
diff (((id Z) ^),x) is V11() V12() ext-real Element of REAL
(() . x) * (diff (((id Z) ^),x)) is V11() V12() ext-real Element of REAL
((id Z) ^) . x is V11() V12() ext-real Element of REAL
diff ((),x) is V11() V12() ext-real Element of REAL
(((id Z) ^) . x) * (diff ((),x)) is V11() V12() ext-real Element of REAL
((() . x) * (diff (((id Z) ^),x))) + ((((id Z) ^) . x) * (diff ((),x))) is V11() V12() ext-real Element of REAL
((id Z) ^) `| Z is V13() V16( REAL ) V17( REAL ) V18() V52() V53() V54() Element of K6(K7(REAL,REAL))
(((id Z) ^) `| Z) . x is V11() V12() ext-real Element of REAL
(() . x) * ((((id Z) ^) `| Z) . x) is V11() V12() ext-real Element of REAL
((() . x) * ((((id Z) ^) `| Z) . x)) + ((((id Z) ^) . x) * (diff ((),x))) is V11() V12() ext-real Element of REAL
1 / (x ^2) is V11() V12() ext-real Element of REAL
K37(1,K39((x ^2))) is V11() V12() ext-real set
- (1 / (x ^2)) is V11() V12() ext-real Element of REAL
(() . x) * (- (1 / (x ^2))) is V11() V12() ext-real Element of REAL
((() . x) * (- (1 / (x ^2)))) + ((((id Z) ^) . x) * (diff ((),x))) is V11() V12() ext-real Element of REAL
(() . x) * (1 / (x ^2)) is V11() V12() ext-real Element of REAL
- ((() . x) * (1 / (x ^2))) is V11() V12() ext-real Element of REAL
(cos . x) / ((sin . x) ^2) is V11() V12() ext-real Element of REAL
K37((cos . x),K39(((sin . x) ^2))) is V11() V12() ext-real set
- ((cos . x) / ((sin . x) ^2)) is V11() V12() ext-real Element of REAL
(((id Z) ^) . x) * (- ((cos . x) / ((sin . x) ^2))) is V11() V12() ext-real Element of REAL
(- ((() . x) * (1 / (x ^2)))) + ((((id Z) ^) . x) * (- ((cos . x) / ((sin . x) ^2)))) is V11() V12() ext-real Element of REAL
(sin . x) " is V11() V12() ext-real Element of REAL
((sin . x) ") * (1 / (x ^2)) is V11() V12() ext-real Element of REAL
- (((sin . x) ") * (1 / (x ^2))) is V11() V12() ext-real Element of REAL
- (cos . x) is V11() V12() ext-real Element of REAL
(- (cos . x)) / ((sin . x) ^2) is V11() V12() ext-real Element of REAL
K37((- (cos . x)),K39(((sin . x) ^2))) is V11() V12() ext-real set
(((id Z) ^) . x) * ((- (cos . x)) / ((sin . x) ^2)) is V11() V12() ext-real Element of REAL
(- (((sin . x) ") * (1 / (x ^2)))) + ((((id Z) ^) . x) * ((- (cos . x)) / ((sin . x) ^2))) is V11() V12() ext-real Element of REAL
(id Z) . x is V11() V12() ext-real Element of REAL
((id Z) . x) " is V11() V12() ext-real Element of REAL
(((id Z) . x) ") * ((- (cos . x)) / ((sin . x) ^2)) is V11() V12() ext-real Element of REAL
(- ((1 / (sin . x)) / (x ^2))) + ((((id Z) . x) ") * ((- (cos . x)) / ((sin . x) ^2))) is V11() V12() ext-real Element of REAL
1 / x is V11() V12() ext-real Element of REAL
K37(1,K39(x)) is V11() V12() ext-real set
(1 / x) * ((- (cos . x)) / ((sin . x) ^2)) is V11() V12() ext-real Element of REAL
(- ((1 / (sin . x)) / (x ^2))) + ((1 / x) * ((- (cos . x)) / ((sin . x) ^2))) is V11() V12() ext-real Element of REAL
(- (cos . x)) / x is V11() V12() ext-real Element of REAL
K37((- (cos . x)),K39(x)) is V11() V12() ext-real set
((- (cos . x)) / x) / ((sin . x) ^2) is V11() V12() ext-real Element of REAL
K37(((- (cos . x)) / x),K39(((sin . x) ^2))) is V11() V12() ext-real set
(- ((1 / (sin . x)) / (x ^2))) + (((- (cos . x)) / x) / ((sin . x) ^2)) is V11() V12() ext-real Element of REAL
x is V11() V12() ext-real Element of REAL
((((id Z) ^) (#) ()) `| Z) . x is V11() V12() ext-real Element of REAL
sin . x is V11() V12() ext-real Element of REAL
1 / (sin . x) is V11() V12() ext-real Element of REAL
K39((sin . x)) is V11() V12() ext-real set
K37(1,K39((sin . x))) is V11() V12() ext-real set
x ^2 is V11() V12() ext-real Element of REAL
K37(x,x) is V11() V12() ext-real set
(1 / (sin . x)) / (x ^2) is V11() V12() ext-real Element of REAL
K39((x ^2)) is V11() V12() ext-real set
K37((1 / (sin . x)),K39((x ^2))) is V11() V12() ext-real set
- ((1 / (sin . x)) / (x ^2)) is V11() V12() ext-real Element of REAL
cos . x is V11() V12() ext-real Element of REAL
(cos . x) / x is V11() V12() ext-real Element of REAL
K39(x) is V11() V12() ext-real set
K37((cos . x),K39(x)) is V11() V12() ext-real set
(sin . x) ^2 is V11() V12() ext-real Element of REAL
K37((sin . x),(sin . x)) is V11() V12() ext-real set
((cos . x) / x) / ((sin . x) ^2) is V11() V12() ext-real Element of REAL
K39(((sin . x) ^2)) is V11() V12() ext-real set
K37(((cos . x) / x),K39(((sin . x) ^2))) is V11() V12() ext-real set
(- ((1 / (sin . x)) / (x ^2))) - (((cos . x) / x) / ((sin . x) ^2)) is V11() V12() ext-real Element of REAL
K38((((cos . x) / x) / ((sin . x) ^2))) is V11() V12() ext-real set
K36((- ((1 / (sin . x)) / (x ^2))),K38((((cos . x) / x) / ((sin . x) ^2)))) is V11() V12() ext-real set
() * sin is V13() V16( REAL ) V17( REAL ) V18() V52() V53() V54() Element of K6(K7(REAL,REAL))
dom (() * sin) is V62() V63() V64() Element of K6(REAL)
Z is open V62() V63() V64() Element of K6(REAL)
(() * sin) `| Z is V13() V16( REAL ) V17( REAL ) V18() V52() V53() V54() Element of K6(K7(REAL,REAL))
x is V11() V12() ext-real Element of REAL
sin . x is V11() V12() ext-real Element of REAL
cos . (sin . x) is V11() V12() ext-real Element of REAL
x is V11() V12() ext-real Element of REAL
sin . x is V11() V12() ext-real Element of REAL
cos . (sin . x) is V11() V12() ext-real Element of REAL
x is V11() V12() ext-real Element of REAL
((() * sin) `| Z) . x is V11() V12() ext-real Element of REAL
cos . x is V11() V12() ext-real Element of REAL
sin . x is V11() V12() ext-real Element of REAL
sin . (sin . x) is V11() V12() ext-real Element of REAL
(cos . x) * (sin . (sin . x)) is V11() V12() ext-real Element of REAL
cos . (sin . x) is V11() V12() ext-real Element of REAL
(cos . (sin . x)) ^2 is V11() V12() ext-real Element of REAL
K37((cos . (sin . x)),(cos . (sin . x))) is V11() V12() ext-real set
((cos . x) * (sin . (sin . x))) / ((cos . (sin . x)) ^2) is V11() V12() ext-real Element of REAL
K39(((cos . (sin . x)) ^2)) is V11() V12() ext-real set
K37(((cos . x) * (sin . (sin . x))),K39(((cos . (sin . x)) ^2))) is V11() V12() ext-real set
diff ((() * sin),x) is V11() V12() ext-real Element of REAL
diff ((),(sin . x)) is V11() V12() ext-real Element of REAL
diff (sin,x) is V11() V12() ext-real Element of REAL
(diff ((),(sin . x))) * (diff (sin,x)) is V11() V12() ext-real Element of REAL
(sin . (sin . x)) / ((cos . (sin . x)) ^2) is V11() V12() ext-real Element of REAL
K37((sin . (sin . x)),K39(((cos . (sin . x)) ^2))) is V11() V12() ext-real set
((sin . (sin . x)) / ((cos . (sin . x)) ^2)) * (diff (sin,x)) is V11() V12() ext-real Element of REAL
(cos . x) * ((sin . (sin . x)) / ((cos . (sin . x)) ^2)) is V11() V12() ext-real Element of REAL
x is V11() V12() ext-real Element of REAL
((() * sin) `| Z) . x is V11() V12() ext-real Element of REAL
cos . x is V11() V12() ext-real Element of REAL
sin . x is V11() V12() ext-real Element of REAL
sin . (sin . x) is V11() V12() ext-real Element of REAL
(cos . x) * (sin . (sin . x)) is V11() V12() ext-real Element of REAL
cos . (sin . x) is V11() V12() ext-real Element of REAL
(cos . (sin . x)) ^2 is V11() V12() ext-real Element of REAL
K37((cos . (sin . x)),(cos . (sin . x))) is V11() V12() ext-real set
((cos . x) * (sin . (sin . x))) / ((cos . (sin . x)) ^2) is V11() V12() ext-real Element of REAL
K39(((cos . (sin . x)) ^2)) is V11() V12() ext-real set
K37(((cos . x) * (sin . (sin . x))),K39(((cos . (sin . x)) ^2))) is V11() V12() ext-real set
() * cos is V13() V16( REAL ) V17( REAL ) V18() V52() V53() V54() Element of K6(K7(REAL,REAL))
dom (() * cos) is V62() V63() V64() Element of K6(REAL)
Z is open V62() V63() V64() Element of K6(REAL)
(() * cos) `| Z is V13() V16( REAL ) V17( REAL ) V18() V52() V53() V54() Element of K6(K7(REAL,REAL))
x is V11() V12() ext-real Element of REAL
cos . x is V11() V12() ext-real Element of REAL
cos . (cos . x) is V11() V12() ext-real Element of REAL
x is V11() V12() ext-real Element of REAL
cos . x is V11() V12() ext-real Element of REAL
cos . (cos . x) is V11() V12() ext-real Element of REAL
x is V11() V12() ext-real Element of REAL
((() * cos) `| Z) . x is V11() V12() ext-real Element of REAL
sin . x is V11() V12() ext-real Element of REAL
cos . x is V11() V12() ext-real Element of REAL
sin . (cos . x) is V11() V12() ext-real Element of REAL
(sin . x) * (sin . (cos . x)) is V11() V12() ext-real Element of REAL
cos . (cos . x) is V11() V12() ext-real Element of REAL
(cos . (cos . x)) ^2 is V11() V12() ext-real Element of REAL
K37((cos . (cos . x)),(cos . (cos . x))) is V11() V12() ext-real set
((sin . x) * (sin . (cos . x))) / ((cos . (cos . x)) ^2) is V11() V12() ext-real Element of REAL
K39(((cos . (cos . x)) ^2)) is V11() V12() ext-real set
K37(((sin . x) * (sin . (cos . x))),K39(((cos . (cos . x)) ^2))) is V11() V12() ext-real set
- (((sin . x) * (sin . (cos . x))) / ((cos . (cos . x)) ^2)) is V11() V12() ext-real Element of REAL
diff ((() * cos),x) is V11() V12() ext-real Element of REAL
diff ((),(cos . x)) is V11() V12() ext-real Element of REAL
diff (cos,x) is V11() V12() ext-real Element of REAL
(diff ((),(cos . x))) * (diff (cos,x)) is V11() V12() ext-real Element of REAL
(sin . (cos . x)) / ((cos . (cos . x)) ^2) is V11() V12() ext-real Element of REAL
K37((sin . (cos . x)),K39(((cos . (cos . x)) ^2))) is V11() V12() ext-real set
((sin . (cos . x)) / ((cos . (cos . x)) ^2)) * (diff (cos,x)) is V11() V12() ext-real Element of REAL
- (sin . x) is V11() V12() ext-real Element of REAL
(- (sin . x)) * ((sin . (cos . x)) / ((cos . (cos . x)) ^2)) is V11() V12() ext-real Element of REAL
x is V11() V12() ext-real Element of REAL
((() * cos) `| Z) . x is V11() V12() ext-real Element of REAL
sin . x is V11() V12() ext-real Element of REAL
cos . x is V11() V12() ext-real Element of REAL
sin . (cos . x) is V11() V12() ext-real Element of REAL
(sin . x) * (sin . (cos . x)) is V11() V12() ext-real Element of REAL
cos . (cos . x) is V11() V12() ext-real Element of REAL
(cos . (cos . x)) ^2 is V11() V12() ext-real Element of REAL
K37((cos . (cos . x)),(cos . (cos . x))) is V11() V12() ext-real set
((sin . x) * (sin . (cos . x))) / ((cos . (cos . x)) ^2) is V11() V12() ext-real Element of REAL
K39(((cos . (cos . x)) ^2)) is V11() V12() ext-real set
K37(((sin . x) * (sin . (cos . x))),K39(((cos . (cos . x)) ^2))) is V11() V12() ext-real set
- (((sin . x) * (sin . (cos . x))) / ((cos . (cos . x)) ^2)) is V11() V12() ext-real Element of REAL
() * sin is V13() V16( REAL ) V17( REAL ) V18() V52() V53() V54() Element of K6(K7(REAL,REAL))
dom (() * sin) is V62() V63() V64() Element of K6(REAL)
Z is open V62() V63() V64() Element of K6(REAL)
(() * sin) `| Z is V13() V16( REAL ) V17( REAL ) V18() V52() V53() V54() Element of K6(K7(REAL,REAL))
x is V11() V12() ext-real Element of REAL
sin . x is V11() V12() ext-real Element of REAL
sin . (sin . x) is V11() V12() ext-real Element of REAL
x is V11() V12() ext-real Element of REAL
sin . x is V11() V12() ext-real Element of REAL
sin . (sin . x) is V11() V12() ext-real Element of REAL
x is V11() V12() ext-real Element of REAL
((() * sin) `| Z) . x is V11() V12() ext-real Element of REAL
cos . x is V11() V12() ext-real Element of REAL
sin . x is V11() V12() ext-real Element of REAL
cos . (sin . x) is V11() V12() ext-real Element of REAL
(cos . x) * (cos . (sin . x)) is V11() V12() ext-real Element of REAL
sin . (sin . x) is V11() V12() ext-real Element of REAL
(sin . (sin . x)) ^2 is V11() V12() ext-real Element of REAL
K37((sin . (sin . x)),(sin . (sin . x))) is V11() V12() ext-real set
((cos . x) * (cos . (sin . x))) / ((sin . (sin . x)) ^2) is V11() V12() ext-real Element of REAL
K39(((sin . (sin . x)) ^2)) is V11() V12() ext-real set
K37(((cos . x) * (cos . (sin . x))),K39(((sin . (sin . x)) ^2))) is V11() V12() ext-real set
- (((cos . x) * (cos . (sin . x))) / ((sin . (sin . x)) ^2)) is V11() V12() ext-real Element of REAL
diff ((() * sin),x) is V11() V12() ext-real Element of REAL
diff ((),(sin . x)) is V11() V12() ext-real Element of REAL
diff (sin,x) is V11() V12() ext-real Element of REAL
(diff ((),(sin . x))) * (diff (sin,x)) is V11() V12() ext-real Element of REAL
(cos . (sin . x)) / ((sin . (sin . x)) ^2) is V11() V12() ext-real Element of REAL
K37((cos . (sin . x)),K39(((sin . (sin . x)) ^2))) is V11() V12() ext-real set
- ((cos . (sin . x)) / ((sin . (sin . x)) ^2)) is V11() V12() ext-real Element of REAL
(- ((cos . (sin . x)) / ((sin . (sin . x)) ^2))) * (diff (sin,x)) is V11() V12() ext-real Element of REAL
(cos . x) * (- ((cos . (sin . x)) / ((sin . (sin . x)) ^2))) is V11() V12() ext-real Element of REAL
x is V11() V12() ext-real Element of REAL
((() * sin) `| Z) . x is V11() V12() ext-real Element of REAL
cos . x is V11() V12() ext-real Element of REAL
sin . x is V11() V12() ext-real Element of REAL
cos . (sin . x) is V11() V12() ext-real Element of REAL
(cos . x) * (cos . (sin . x)) is V11() V12() ext-real Element of REAL
sin . (sin . x) is V11() V12() ext-real Element of REAL
(sin . (sin . x)) ^2 is V11() V12() ext-real Element of REAL
K37((sin . (sin . x)),(sin . (sin . x))) is V11() V12() ext-real set
((cos . x) * (cos . (sin . x))) / ((sin . (sin . x)) ^2) is V11() V12() ext-real Element of REAL
K39(((sin . (sin . x)) ^2)) is V11() V12() ext-real set
K37(((cos . x) * (cos . (sin . x))),K39(((sin . (sin . x)) ^2))) is V11() V12() ext-real set
- (((cos . x) * (cos . (sin . x))) / ((sin . (sin . x)) ^2)) is V11() V12() ext-real Element of REAL
() * cos is V13() V16( REAL ) V17( REAL ) V18() V52() V53() V54() Element of K6(K7(REAL,REAL))
dom (() * cos) is V62() V63() V64() Element of K6(REAL)
Z is open V62() V63() V64() Element of K6(REAL)
(() * cos) `| Z is V13() V16( REAL ) V17( REAL ) V18() V52() V53() V54() Element of K6(K7(REAL,REAL))
x is V11() V12() ext-real Element of REAL
cos . x is V11() V12() ext-real Element of REAL
sin . (cos . x) is V11() V12() ext-real Element of REAL
x is V11() V12() ext-real Element of REAL
cos . x is V11() V12() ext-real Element of REAL
sin . (cos . x) is V11() V12() ext-real Element of REAL
x is V11() V12() ext-real Element of REAL
((() * cos) `| Z) . x is V11() V12() ext-real Element of REAL
sin . x is V11() V12() ext-real Element of REAL
cos . x is V11() V12() ext-real Element of REAL
cos . (cos . x) is V11() V12() ext-real Element of REAL
(sin . x) * (cos . (cos . x)) is V11() V12() ext-real Element of REAL
sin . (cos . x) is V11() V12() ext-real Element of REAL
(sin . (cos . x)) ^2 is V11() V12() ext-real Element of REAL
K37((sin . (cos . x)),(sin . (cos . x))) is V11() V12() ext-real set
((sin . x) * (cos . (cos . x))) / ((sin . (cos . x)) ^2) is V11() V12() ext-real Element of REAL
K39(((sin . (cos . x)) ^2)) is V11() V12() ext-real set
K37(((sin . x) * (cos . (cos . x))),K39(((sin . (cos . x)) ^2))) is V11() V12() ext-real set
diff ((() * cos),x) is V11() V12() ext-real Element of REAL
diff ((),(cos . x)) is V11() V12() ext-real Element of REAL
diff (cos,x) is V11() V12() ext-real Element of REAL
(diff ((),(cos . x))) * (diff (cos,x)) is V11() V12() ext-real Element of REAL
(cos . (cos . x)) / ((sin . (cos . x)) ^2) is V11() V12() ext-real Element of REAL
K37((cos . (cos . x)),K39(((sin . (cos . x)) ^2))) is V11() V12() ext-real set
- ((cos . (cos . x)) / ((sin . (cos . x)) ^2)) is V11() V12() ext-real Element of REAL
(- ((cos . (cos . x)) / ((sin . (cos . x)) ^2))) * (diff (cos,x)) is V11() V12() ext-real Element of REAL
- (sin . x) is V11() V12() ext-real Element of REAL
(- (sin . x)) * (- ((cos . (cos . x)) / ((sin . (cos . x)) ^2))) is V11() V12() ext-real Element of REAL
x is V11() V12() ext-real Element of REAL
((() * cos) `| Z) . x is V11() V12() ext-real Element of REAL
sin . x is V11() V12() ext-real Element of REAL
cos . x is V11() V12() ext-real Element of REAL
cos . (cos . x) is V11() V12() ext-real Element of REAL
(sin . x) * (cos . (cos . x)) is V11() V12() ext-real Element of REAL
sin . (cos . x) is V11() V12() ext-real Element of REAL
(sin . (cos . x)) ^2 is V11() V12() ext-real Element of REAL
K37((sin . (cos . x)),(sin . (cos . x))) is V11() V12() ext-real set
((sin . x) * (cos . (cos . x))) / ((sin . (cos . x)) ^2) is V11() V12() ext-real Element of REAL
K39(((sin . (cos . x)) ^2)) is V11() V12() ext-real set
K37(((sin . x) * (cos . (cos . x))),K39(((sin . (cos . x)) ^2))) is V11() V12() ext-real set
() * tan is V13() V16( REAL ) V17( REAL ) V18() V52() V53() V54() Element of K6(K7(REAL,REAL))
dom (() * tan) is V62() V63() V64() Element of K6(REAL)
Z is open V62() V63() V64() Element of K6(REAL)
(() * tan) `| Z is V13() V16( REAL ) V17( REAL ) V18() V52() V53() V54() Element of K6(K7(REAL,REAL))
x is V11() V12() ext-real Element of REAL
tan . x is V11() V12() ext-real Element of REAL
cos . (tan . x) is V11() V12() ext-real Element of REAL
x is V11() V12() ext-real Element of REAL
cos . x is V11() V12() ext-real Element of REAL
tan . x is V11() V12() ext-real Element of REAL
cos . (tan . x) is V11() V12() ext-real Element of REAL
x is V11() V12() ext-real Element of REAL
((() * tan) `| Z) . x is V11() V12() ext-real Element of REAL
tan . x is V11() V12() ext-real Element of REAL
sin . (tan . x) is V11() V12() ext-real Element of REAL
cos . x is V11() V12() ext-real Element of REAL
(cos . x) ^2 is V11() V12() ext-real Element of REAL
K37((cos . x),(cos . x)) is V11() V12() ext-real set
(sin . (tan . x)) / ((cos . x) ^2) is V11() V12() ext-real Element of REAL
K39(((cos . x) ^2)) is V11() V12() ext-real set
K37((sin . (tan . x)),K39(((cos . x) ^2))) is V11() V12() ext-real set
cos . (tan . x) is V11() V12() ext-real Element of REAL
(cos . (tan . x)) ^2 is V11() V12() ext-real Element of REAL
K37((cos . (tan . x)),(cos . (tan . x))) is V11() V12() ext-real set
((sin . (tan . x)) / ((cos . x) ^2)) / ((cos . (tan . x)) ^2) is V11() V12() ext-real Element of REAL
K39(((cos . (tan . x)) ^2)) is V11() V12() ext-real set
K37(((sin . (tan . x)) / ((cos . x) ^2)),K39(((cos . (tan . x)) ^2))) is V11() V12() ext-real set
diff ((() * tan),x) is V11() V12() ext-real Element of REAL
diff ((),(tan . x)) is V11() V12() ext-real Element of REAL
diff (tan,x) is V11() V12() ext-real Element of REAL
(diff ((),(tan . x))) * (diff (tan,x)) is V11() V12() ext-real Element of REAL
(sin . (tan . x)) / ((cos . (tan . x)) ^2) is V11() V12() ext-real Element of REAL
K37((sin . (tan . x)),K39(((cos . (tan . x)) ^2))) is V11() V12() ext-real set
((sin . (tan . x)) / ((cos . (tan . x)) ^2)) * (diff (tan,x)) is V11() V12() ext-real Element of REAL
1 / ((cos . x) ^2) is V11() V12() ext-real Element of REAL
K37(1,K39(((cos . x) ^2))) is V11() V12() ext-real set
(1 / ((cos . x) ^2)) * ((sin . (tan . x)) / ((cos . (tan . x)) ^2)) is V11() V12() ext-real Element of REAL
x is V11() V12() ext-real Element of REAL
((() * tan) `| Z) . x is V11() V12() ext-real Element of REAL
tan . x is V11() V12() ext-real Element of REAL
sin . (tan . x) is V11() V12() ext-real Element of REAL
cos . x is V11() V12() ext-real Element of REAL
(cos . x) ^2 is V11() V12() ext-real Element of REAL
K37((cos . x),(cos . x)) is V11() V12() ext-real set
(sin . (tan . x)) / ((cos . x) ^2) is V11() V12() ext-real Element of REAL
K39(((cos . x) ^2)) is V11() V12() ext-real set
K37((sin . (tan . x)),K39(((cos . x) ^2))) is V11() V12() ext-real set
cos . (tan . x) is V11() V12() ext-real Element of REAL
(cos . (tan . x)) ^2 is V11() V12() ext-real Element of REAL
K37((cos . (tan . x)),(cos . (tan . x))) is V11() V12() ext-real set
((sin . (tan . x)) / ((cos . x) ^2)) / ((cos . (tan . x)) ^2) is V11() V12() ext-real Element of REAL
K39(((cos . (tan . x)) ^2)) is V11() V12() ext-real set
K37(((sin . (tan . x)) / ((cos . x) ^2)),K39(((cos . (tan . x)) ^2))) is V11() V12() ext-real set
() * cot is V13() V16( REAL ) V17( REAL ) V18() V52() V53() V54() Element of K6(K7(REAL,REAL))
dom (() * cot) is V62() V63() V64() Element of K6(REAL)
Z is open V62() V63() V64() Element of K6(REAL)
(() * cot) `| Z is V13() V16( REAL ) V17( REAL ) V18() V52() V53() V54() Element of K6(K7(REAL,REAL))
x is V11() V12() ext-real Element of REAL
cot . x is V11() V12() ext-real Element of REAL
cos . (cot . x) is V11() V12() ext-real Element of REAL
x is V11() V12() ext-real Element of REAL
sin . x is V11() V12() ext-real Element of REAL
cot . x is V11() V12() ext-real Element of REAL
cos . (cot . x) is V11() V12() ext-real Element of REAL
x is V11() V12() ext-real Element of REAL
((() * cot) `| Z) . x is V11() V12() ext-real Element of REAL
cot . x is V11() V12() ext-real Element of REAL
sin . (cot . x) is V11() V12() ext-real Element of REAL
sin . x is V11() V12() ext-real Element of REAL
(sin . x) ^2 is V11() V12() ext-real Element of REAL
K37((sin . x),(sin . x)) is V11() V12() ext-real set
(sin . (cot . x)) / ((sin . x) ^2) is V11() V12() ext-real Element of REAL
K39(((sin . x) ^2)) is V11() V12() ext-real set
K37((sin . (cot . x)),K39(((sin . x) ^2))) is V11() V12() ext-real set
cos . (cot . x) is V11() V12() ext-real Element of REAL
(cos . (cot . x)) ^2 is V11() V12() ext-real Element of REAL
K37((cos . (cot . x)),(cos . (cot . x))) is V11() V12() ext-real set
((sin . (cot . x)) / ((sin . x) ^2)) / ((cos . (cot . x)) ^2) is V11() V12() ext-real Element of REAL
K39(((cos . (cot . x)) ^2)) is V11() V12() ext-real set
K37(((sin . (cot . x)) / ((sin . x) ^2)),K39(((cos . (cot . x)) ^2))) is V11() V12() ext-real set
- (((sin . (cot . x)) / ((sin . x) ^2)) / ((cos . (cot . x)) ^2)) is V11() V12() ext-real Element of REAL
diff ((() * cot),x) is V11() V12() ext-real Element of REAL
diff ((),(cot . x)) is V11() V12() ext-real Element of REAL
diff (cot,x) is V11() V12() ext-real Element of REAL
(diff ((),(cot . x))) * (diff (cot,x)) is V11() V12() ext-real Element of REAL
(sin . (cot . x)) / ((cos . (cot . x)) ^2) is V11() V12() ext-real Element of REAL
K37((sin . (cot . x)),K39(((cos . (cot . x)) ^2))) is V11() V12() ext-real set
((sin . (cot . x)) / ((cos . (cot . x)) ^2)) * (diff (cot,x)) is V11() V12() ext-real Element of REAL
1 / ((sin . x) ^2) is V11() V12() ext-real Element of REAL
K37(1,K39(((sin . x) ^2))) is V11() V12() ext-real set
- (1 / ((sin . x) ^2)) is V11() V12() ext-real Element of REAL
(- (1 / ((sin . x) ^2))) * ((sin . (cot . x)) / ((cos . (cot . x)) ^2)) is V11() V12() ext-real Element of REAL
x is V11() V12() ext-real Element of REAL
((() * cot) `| Z) . x is V11() V12() ext-real Element of REAL
cot . x is V11() V12() ext-real Element of REAL
sin . (cot . x) is V11() V12() ext-real Element of REAL
sin . x is V11() V12() ext-real Element of REAL
(sin . x) ^2 is V11() V12() ext-real Element of REAL
K37((sin . x),(sin . x)) is V11() V12() ext-real set
(sin . (cot . x)) / ((sin . x) ^2) is V11() V12() ext-real Element of REAL
K39(((sin . x) ^2)) is V11() V12() ext-real set
K37((sin . (cot . x)),K39(((sin . x) ^2))) is V11() V12() ext-real set
cos . (cot . x) is V11() V12() ext-real Element of REAL
(cos . (cot . x)) ^2 is V11() V12() ext-real Element of REAL
K37((cos . (cot . x)),(cos . (cot . x))) is V11() V12() ext-real set
((sin . (cot . x)) / ((sin . x) ^2)) / ((cos . (cot . x)) ^2) is V11() V12() ext-real Element of REAL
K39(((cos . (cot . x)) ^2)) is V11() V12() ext-real set
K37(((sin . (cot . x)) / ((sin . x) ^2)),K39(((cos . (cot . x)) ^2))) is V11() V12() ext-real set
- (((sin . (cot . x)) / ((sin . x) ^2)) / ((cos . (cot . x)) ^2)) is V11() V12() ext-real Element of REAL
() * tan is V13() V16( REAL ) V17( REAL ) V18() V52() V53() V54() Element of K6(K7(REAL,REAL))
dom (() * tan) is V62() V63() V64() Element of K6(REAL)
Z is open V62() V63() V64() Element of K6(REAL)
(() * tan) `| Z is V13() V16( REAL ) V17( REAL ) V18() V52() V53() V54() Element of K6(K7(REAL,REAL))
x is V11() V12() ext-real Element of REAL
tan . x is V11() V12() ext-real Element of REAL
sin . (tan . x) is V11() V12() ext-real Element of REAL
x is V11() V12() ext-real Element of REAL
cos . x is V11() V12() ext-real Element of REAL
tan . x is V11() V12() ext-real Element of REAL
sin . (tan . x) is V11() V12() ext-real Element of REAL
x is V11() V12() ext-real Element of REAL
((() * tan) `| Z) . x is V11() V12() ext-real Element of REAL
tan . x is V11() V12() ext-real Element of REAL
cos . (tan . x) is V11() V12() ext-real Element of REAL
cos . x is V11() V12() ext-real Element of REAL
(cos . x) ^2 is V11() V12() ext-real Element of REAL
K37((cos . x),(cos . x)) is V11() V12() ext-real set
(cos . (tan . x)) / ((cos . x) ^2) is V11() V12() ext-real Element of REAL
K39(((cos . x) ^2)) is V11() V12() ext-real set
K37((cos . (tan . x)),K39(((cos . x) ^2))) is V11() V12() ext-real set
sin . (tan . x) is V11() V12() ext-real Element of REAL
(sin . (tan . x)) ^2 is V11() V12() ext-real Element of REAL
K37((sin . (tan . x)),(sin . (tan . x))) is V11() V12() ext-real set
((cos . (tan . x)) / ((cos . x) ^2)) / ((sin . (tan . x)) ^2) is V11() V12() ext-real Element of REAL
K39(((sin . (tan . x)) ^2)) is V11() V12() ext-real set
K37(((cos . (tan . x)) / ((cos . x) ^2)),K39(((sin . (tan . x)) ^2))) is V11() V12() ext-real set
- (((cos . (tan . x)) / ((cos . x) ^2)) / ((sin . (tan . x)) ^2)) is V11() V12() ext-real Element of REAL
diff ((() * tan),x) is V11() V12() ext-real Element of REAL
diff ((),(tan . x)) is V11() V12() ext-real Element of REAL
diff (tan,x) is V11() V12() ext-real Element of REAL
(diff ((),(tan . x))) * (diff (tan,x)) is V11() V12() ext-real Element of REAL
(cos . (tan . x)) / ((sin . (tan . x)) ^2) is V11() V12() ext-real Element of REAL
K37((cos . (tan . x)),K39(((sin . (tan . x)) ^2))) is V11() V12() ext-real set
- ((cos . (tan . x)) / ((sin . (tan . x)) ^2)) is V11() V12() ext-real Element of REAL
(- ((cos . (tan . x)) / ((sin . (tan . x)) ^2))) * (diff (tan,x)) is V11() V12() ext-real Element of REAL
1 / ((cos . x) ^2) is V11() V12() ext-real Element of REAL
K37(1,K39(((cos . x) ^2))) is V11() V12() ext-real set
(1 / ((cos . x) ^2)) * (- ((cos . (tan . x)) / ((sin . (tan . x)) ^2))) is V11() V12() ext-real Element of REAL
x is V11() V12() ext-real Element of REAL
((() * tan) `| Z) . x is V11() V12() ext-real Element of REAL
tan . x is V11() V12() ext-real Element of REAL
cos . (tan . x) is V11() V12() ext-real Element of REAL
cos . x is V11() V12() ext-real Element of REAL
(cos . x) ^2 is V11() V12() ext-real Element of REAL
K37((cos . x),(cos . x)) is V11() V12() ext-real set
(cos . (tan . x)) / ((cos . x) ^2) is V11() V12() ext-real Element of REAL
K39(((cos . x) ^2)) is V11() V12() ext-real set
K37((cos . (tan . x)),K39(((cos . x) ^2))) is V11() V12() ext-real set
sin . (tan . x) is V11() V12() ext-real Element of REAL
(sin . (tan . x)) ^2 is V11() V12() ext-real Element of REAL
K37((sin . (tan . x)),(sin . (tan . x))) is V11() V12() ext-real set
((cos . (tan . x)) / ((cos . x) ^2)) / ((sin . (tan . x)) ^2) is V11() V12() ext-real Element of REAL
K39(((sin . (tan . x)) ^2)) is V11() V12() ext-real set
K37(((cos . (tan . x)) / ((cos . x) ^2)),K39(((sin . (tan . x)) ^2))) is V11() V12() ext-real set
- (((cos . (tan . x)) / ((cos . x) ^2)) / ((sin . (tan . x)) ^2)) is V11() V12() ext-real Element of REAL
() * cot is V13() V16( REAL ) V17( REAL ) V18() V52() V53() V54() Element of K6(K7(REAL,REAL))
dom (() * cot) is V62() V63() V64() Element of K6(REAL)
Z is open V62() V63() V64() Element of K6(REAL)
(() * cot) `| Z is V13() V16( REAL ) V17( REAL ) V18() V52() V53() V54() Element of K6(K7(REAL,REAL))
x is V11() V12() ext-real Element of REAL
cot . x is V11() V12() ext-real Element of REAL
sin . (cot . x) is V11() V12() ext-real Element of REAL
x is V11() V12() ext-real Element of REAL
sin . x is V11() V12() ext-real Element of REAL
cot . x is V11() V12() ext-real Element of REAL
sin . (cot . x) is V11() V12() ext-real Element of REAL
x is V11() V12() ext-real Element of REAL
((() * cot) `| Z) . x is V11() V12() ext-real Element of REAL
cot . x is V11() V12() ext-real Element of REAL
cos . (cot . x) is V11() V12() ext-real Element of REAL
sin . x is V11() V12() ext-real Element of REAL
(sin . x) ^2 is V11() V12() ext-real Element of REAL
K37((sin . x),(sin . x)) is V11() V12() ext-real set
(cos . (cot . x)) / ((sin . x) ^2) is V11() V12() ext-real Element of REAL
K39(((sin . x) ^2)) is V11() V12() ext-real set
K37((cos . (cot . x)),K39(((sin . x) ^2))) is V11() V12() ext-real set
sin . (cot . x) is V11() V12() ext-real Element of REAL
(sin . (cot . x)) ^2 is V11() V12() ext-real Element of REAL
K37((sin . (cot . x)),(sin . (cot . x))) is V11() V12() ext-real set
((cos . (cot . x)) / ((sin . x) ^2)) / ((sin . (cot . x)) ^2) is V11() V12() ext-real Element of REAL
K39(((sin . (cot . x)) ^2)) is V11() V12() ext-real set
K37(((cos . (cot . x)) / ((sin . x) ^2)),K39(((sin . (cot . x)) ^2))) is V11() V12() ext-real set
diff ((() * cot),x) is V11() V12() ext-real Element of REAL
diff ((),(cot . x)) is V11() V12() ext-real Element of REAL
diff (cot,x) is V11() V12() ext-real Element of REAL
(diff ((),(cot . x))) * (diff (cot,x)) is V11() V12() ext-real Element of REAL
(cos . (cot . x)) / ((sin . (cot . x)) ^2) is V11() V12() ext-real Element of REAL
K37((cos . (cot . x)),K39(((sin . (cot . x)) ^2))) is V11() V12() ext-real set
- ((cos . (cot . x)) / ((sin . (cot . x)) ^2)) is V11() V12() ext-real Element of REAL
(- ((cos . (cot . x)) / ((sin . (cot . x)) ^2))) * (diff (cot,x)) is V11() V12() ext-real Element of REAL
1 / ((sin . x) ^2) is V11() V12() ext-real Element of REAL
K37(1,K39(((sin . x) ^2))) is V11() V12() ext-real set
- (1 / ((sin . x) ^2)) is V11() V12() ext-real Element of REAL
(- (1 / ((sin . x) ^2))) * (- ((cos . (cot . x)) / ((sin . (cot . x)) ^2))) is V11() V12() ext-real Element of REAL
x is V11() V12() ext-real Element of REAL
((() * cot) `| Z) . x is V11() V12() ext-real Element of REAL
cot . x is V11() V12() ext-real Element of REAL
cos . (cot . x) is V11() V12() ext-real Element of REAL
sin . x is V11() V12() ext-real Element of REAL
(sin . x) ^2 is V11() V12() ext-real Element of REAL
K37((sin . x),(sin . x)) is V11() V12() ext-real set
(cos . (cot . x)) / ((sin . x) ^2) is V11() V12() ext-real Element of REAL
K39(((sin . x) ^2)) is V11() V12() ext-real set
K37((cos . (cot . x)),K39(((sin . x) ^2))) is V11() V12() ext-real set
sin . (cot . x) is V11() V12() ext-real Element of REAL
(sin . (cot . x)) ^2 is V11() V12() ext-real Element of REAL
K37((sin . (cot . x)),(sin . (cot . x))) is V11() V12() ext-real set
((cos . (cot . x)) / ((sin . x) ^2)) / ((sin . (cot . x)) ^2) is V11() V12() ext-real Element of REAL
K39(((sin . (cot . x)) ^2)) is V11() V12() ext-real set
K37(((cos . (cot . x)) / ((sin . x) ^2)),K39(((sin . (cot . x)) ^2))) is V11() V12() ext-real set
tan (#) () is V13() V16( REAL ) V17( REAL ) V18() V52() V53() V54() Element of K6(K7(REAL,REAL))
dom (tan (#) ()) is V62() V63() V64() Element of K6(REAL)
Z is open V62() V63() V64() Element of K6(REAL)
(tan (#) ()) `| Z is V13() V16( REAL ) V17( REAL ) V18() V52() V53() V54() Element of K6(K7(REAL,REAL))
(dom tan) /\ (dom ()) is V62() V63() V64() Element of K6(REAL)
x is V11() V12() ext-real Element of REAL
cos . x is V11() V12() ext-real Element of REAL
x is V11() V12() ext-real Element of REAL
diff ((),x) is V11() V12() ext-real Element of REAL
sin . x is V11() V12() ext-real Element of REAL
cos . x is V11() V12() ext-real Element of REAL
(cos . x) ^2 is V11() V12() ext-real Element of REAL
K37((cos . x),(cos . x)) is V11() V12() ext-real set
(sin . x) / ((cos . x) ^2) is V11() V12() ext-real Element of REAL
K39(((cos . x) ^2)) is V11() V12() ext-real set
K37((sin . x),K39(((cos . x) ^2))) is V11() V12() ext-real set
x is V11() V12() ext-real Element of REAL
x is V11() V12() ext-real Element of REAL
((tan (#) ()) `| Z) . x is V11() V12() ext-real Element of REAL
cos . x is V11() V12() ext-real Element of REAL
(cos . x) ^2 is V11() V12() ext-real Element of REAL
K37((cos . x),(cos . x)) is V11() V12() ext-real set
1 / ((cos . x) ^2) is V11() V12() ext-real Element of REAL
K39(((cos . x) ^2)) is V11() V12() ext-real set
K37(1,K39(((cos . x) ^2))) is V11() V12() ext-real set
(1 / ((cos . x) ^2)) / (cos . x) is V11() V12() ext-real Element of REAL
K39((cos . x)) is V11() V12() ext-real set
K37((1 / ((cos . x) ^2)),K39((cos . x))) is V11() V12() ext-real set
tan . x is V11() V12() ext-real Element of REAL
sin . x is V11() V12() ext-real Element of REAL
(tan . x) * (sin . x) is V11() V12() ext-real Element of REAL
((tan . x) * (sin . x)) / ((cos . x) ^2) is V11() V12() ext-real Element of REAL
K37(((tan . x) * (sin . x)),K39(((cos . x) ^2))) is V11() V12() ext-real set
((1 / ((cos . x) ^2)) / (cos . x)) + (((tan . x) * (sin . x)) / ((cos . x) ^2)) is V11() V12() ext-real Element of REAL
() . x is V11() V12() ext-real Element of REAL
diff (tan,x) is V11() V12() ext-real Element of REAL
(() . x) * (diff (tan,x)) is V11() V12() ext-real Element of REAL
diff ((),x) is V11() V12() ext-real Element of REAL
(tan . x) * (diff ((),x)) is V11() V12() ext-real Element of REAL
((() . x) * (diff (tan,x))) + ((tan . x) * (diff ((),x))) is V11() V12() ext-real Element of REAL
(() . x) * (1 / ((cos . x) ^2)) is V11() V12() ext-real Element of REAL
((() . x) * (1 / ((cos . x) ^2))) + ((tan . x) * (diff ((),x))) is V11() V12() ext-real Element of REAL
(sin . x) / ((cos . x) ^2) is V11() V12() ext-real Element of REAL
K37((sin . x),K39(((cos . x) ^2))) is V11() V12() ext-real set
(tan . x) * ((sin . x) / ((cos . x) ^2)) is V11() V12() ext-real Element of REAL
((() . x) * (1 / ((cos . x) ^2))) + ((tan . x) * ((sin . x) / ((cos . x) ^2))) is V11() V12() ext-real Element of REAL
x is V11() V12() ext-real Element of REAL
((tan (#) ()) `| Z) . x is V11() V12() ext-real Element of REAL
cos . x is V11() V12() ext-real Element of REAL
(cos . x) ^2 is V11() V12() ext-real Element of REAL
K37((cos . x),(cos . x)) is V11() V12() ext-real set
1 / ((cos . x) ^2) is V11() V12() ext-real Element of REAL
K39(((cos . x) ^2)) is V11() V12() ext-real set
K37(1,K39(((cos . x) ^2))) is V11() V12() ext-real set
(1 / ((cos . x) ^2)) / (cos . x) is V11() V12() ext-real Element of REAL
K39((cos . x)) is V11() V12() ext-real set
K37((1 / ((cos . x) ^2)),K39((cos . x))) is V11() V12() ext-real set
tan . x is V11() V12() ext-real Element of REAL
sin . x is V11() V12() ext-real Element of REAL
(tan . x) * (sin . x) is V11() V12() ext-real Element of REAL
((tan . x) * (sin . x)) / ((cos . x) ^2) is V11() V12() ext-real Element of REAL
K37(((tan . x) * (sin . x)),K39(((cos . x) ^2))) is V11() V12() ext-real set
((1 / ((cos . x) ^2)) / (cos . x)) + (((tan . x) * (sin . x)) / ((cos . x) ^2)) is V11() V12() ext-real Element of REAL
cot (#) () is V13() V16( REAL ) V17( REAL ) V18() V52() V53() V54() Element of K6(K7(REAL,REAL))
dom (cot (#) ()) is V62() V63() V64() Element of K6(REAL)
Z is open V62() V63() V64() Element of K6(REAL)
(cot (#) ()) `| Z is V13() V16( REAL ) V17( REAL ) V18() V52() V53() V54() Element of K6(K7(REAL,REAL))
(dom cot) /\ (dom ()) is V62() V63() V64() Element of K6(REAL)
x is V11() V12() ext-real Element of REAL
sin . x is V11() V12() ext-real Element of REAL
x is V11() V12() ext-real Element of REAL
diff ((),x) is V11() V12() ext-real Element of REAL
sin . x is V11() V12() ext-real Element of REAL
cos . x is V11() V12() ext-real Element of REAL
(cos . x) ^2 is V11() V12() ext-real Element of REAL
K37((cos . x),(cos . x)) is V11() V12() ext-real set
(sin . x) / ((cos . x) ^2) is V11() V12() ext-real Element of REAL
K39(((cos . x) ^2)) is V11() V12() ext-real set
K37((sin . x),K39(((cos . x) ^2))) is V11() V12() ext-real set
x is V11() V12() ext-real Element of REAL
x is V11() V12() ext-real Element of REAL
((cot (#) ()) `| Z) . x is V11() V12() ext-real Element of REAL
sin . x is V11() V12() ext-real Element of REAL
(sin . x) ^2 is V11() V12() ext-real Element of REAL
K37((sin . x),(sin . x)) is V11() V12() ext-real set
1 / ((sin . x) ^2) is V11() V12() ext-real Element of REAL
K39(((sin . x) ^2)) is V11() V12() ext-real set
K37(1,K39(((sin . x) ^2))) is V11() V12() ext-real set
cos . x is V11() V12() ext-real Element of REAL
(1 / ((sin . x) ^2)) / (cos . x) is V11() V12() ext-real Element of REAL
K39((cos . x)) is V11() V12() ext-real set
K37((1 / ((sin . x) ^2)),K39((cos . x))) is V11() V12() ext-real set
- ((1 / ((sin . x) ^2)) / (cos . x)) is V11() V12() ext-real Element of REAL
cot . x is V11() V12() ext-real Element of REAL
(cot . x) * (sin . x) is V11() V12() ext-real Element of REAL
(cos . x) ^2 is V11() V12() ext-real Element of REAL
K37((cos . x),(cos . x)) is V11() V12() ext-real set
((cot . x) * (sin . x)) / ((cos . x) ^2) is V11() V12() ext-real Element of REAL
K39(((cos . x) ^2)) is V11() V12() ext-real set
K37(((cot . x) * (sin . x)),K39(((cos . x) ^2))) is V11() V12() ext-real set
(- ((1 / ((sin . x) ^2)) / (cos . x))) + (((cot . x) * (sin . x)) / ((cos . x) ^2)) is V11() V12() ext-real Element of REAL
() . x is V11() V12() ext-real Element of REAL
diff (cot,x) is V11() V12() ext-real Element of REAL
(() . x) * (diff (cot,x)) is V11() V12() ext-real Element of REAL
diff ((),x) is V11() V12() ext-real Element of REAL
(cot . x) * (diff ((),x)) is V11() V12() ext-real Element of REAL
((() . x) * (diff (cot,x))) + ((cot . x) * (diff ((),x))) is V11() V12() ext-real Element of REAL
- (1 / ((sin . x) ^2)) is V11() V12() ext-real Element of REAL
(() . x) * (- (1 / ((sin . x) ^2))) is V11() V12() ext-real Element of REAL
((() . x) * (- (1 / ((sin . x) ^2)))) + ((cot . x) * (diff ((),x))) is V11() V12() ext-real Element of REAL
(sin . x) / ((cos . x) ^2) is V11() V12() ext-real Element of REAL
K37((sin . x),K39(((cos . x) ^2))) is V11() V12() ext-real set
(cot . x) * ((sin . x) / ((cos . x) ^2)) is V11() V12() ext-real Element of REAL
((() . x) * (- (1 / ((sin . x) ^2)))) + ((cot . x) * ((sin . x) / ((cos . x) ^2))) is V11() V12() ext-real Element of REAL
(- (1 / ((sin . x) ^2))) / (cos . x) is V11() V12() ext-real Element of REAL
K37((- (1 / ((sin . x) ^2))),K39((cos . x))) is V11() V12() ext-real set
((- (1 / ((sin . x) ^2))) / (cos . x)) + (((cot . x) * (sin . x)) / ((cos . x) ^2)) is V11() V12() ext-real Element of REAL
x is V11() V12() ext-real Element of REAL
((cot (#) ()) `| Z) . x is V11() V12() ext-real Element of REAL
sin . x is V11() V12() ext-real Element of REAL
(sin . x) ^2 is V11() V12() ext-real Element of REAL
K37((sin . x),(sin . x)) is V11() V12() ext-real set
1 / ((sin . x) ^2) is V11() V12() ext-real Element of REAL
K39(((sin . x) ^2)) is V11() V12() ext-real set
K37(1,K39(((sin . x) ^2))) is V11() V12() ext-real set
cos . x is V11() V12() ext-real Element of REAL
(1 / ((sin . x) ^2)) / (cos . x) is V11() V12() ext-real Element of REAL
K39((cos . x)) is V11() V12() ext-real set
K37((1 / ((sin . x) ^2)),K39((cos . x))) is V11() V12() ext-real set
- ((1 / ((sin . x) ^2)) / (cos . x)) is V11() V12() ext-real Element of REAL
cot . x is V11() V12() ext-real Element of REAL
(cot . x) * (sin . x) is V11() V12() ext-real Element of REAL
(cos . x) ^2 is V11() V12() ext-real Element of REAL
K37((cos . x),(cos . x)) is V11() V12() ext-real set
((cot . x) * (sin . x)) / ((cos . x) ^2) is V11() V12() ext-real Element of REAL
K39(((cos . x) ^2)) is V11() V12() ext-real set
K37(((cot . x) * (sin . x)),K39(((cos . x) ^2))) is V11() V12() ext-real set
(- ((1 / ((sin . x) ^2)) / (cos . x))) + (((cot . x) * (sin . x)) / ((cos . x) ^2)) is V11() V12() ext-real Element of REAL
tan (#) () is V13() V16( REAL ) V17( REAL ) V18() V52() V53() V54() Element of K6(K7(REAL,REAL))
dom (tan (#) ()) is V62() V63() V64() Element of K6(REAL)
Z is open V62() V63() V64() Element of K6(REAL)
(tan (#) ()) `| Z is V13() V16( REAL ) V17( REAL ) V18() V52() V53() V54() Element of K6(K7(REAL,REAL))
(dom tan) /\ (dom ()) is V62() V63() V64() Element of K6(REAL)
x is V11() V12() ext-real Element of REAL
cos . x is V11() V12() ext-real Element of REAL
x is V11() V12() ext-real Element of REAL
diff ((),x) is V11() V12() ext-real Element of REAL
cos . x is V11() V12() ext-real Element of REAL
sin . x is V11() V12() ext-real Element of REAL
(sin . x) ^2 is V11() V12() ext-real Element of REAL
K37((sin . x),(sin . x)) is V11() V12() ext-real set
(cos . x) / ((sin . x) ^2) is V11() V12() ext-real Element of REAL
K39(((sin . x) ^2)) is V11() V12() ext-real set
K37((cos . x),K39(((sin . x) ^2))) is V11() V12() ext-real set
- ((cos . x) / ((sin . x) ^2)) is V11() V12() ext-real Element of REAL
x is V11() V12() ext-real Element of REAL
x is V11() V12() ext-real Element of REAL
((tan (#) ()) `| Z) . x is V11() V12() ext-real Element of REAL
cos . x is V11() V12() ext-real Element of REAL
(cos . x) ^2 is V11() V12() ext-real Element of REAL
K37((cos . x),(cos . x)) is V11() V12() ext-real set
1 / ((cos . x) ^2) is V11() V12() ext-real Element of REAL
K39(((cos . x) ^2)) is V11() V12() ext-real set
K37(1,K39(((cos . x) ^2))) is V11() V12() ext-real set
sin . x is V11() V12() ext-real Element of REAL
(1 / ((cos . x) ^2)) / (sin . x) is V11() V12() ext-real Element of REAL
K39((sin . x)) is V11() V12() ext-real set
K37((1 / ((cos . x) ^2)),K39((sin . x))) is V11() V12() ext-real set
tan . x is V11() V12() ext-real Element of REAL
(tan . x) * (cos . x) is V11() V12() ext-real Element of REAL
(sin . x) ^2 is V11() V12() ext-real Element of REAL
K37((sin . x),(sin . x)) is V11() V12() ext-real set
((tan . x) * (cos . x)) / ((sin . x) ^2) is V11() V12() ext-real Element of REAL
K39(((sin . x) ^2)) is V11() V12() ext-real set
K37(((tan . x) * (cos . x)),K39(((sin . x) ^2))) is V11() V12() ext-real set
((1 / ((cos . x) ^2)) / (sin . x)) - (((tan . x) * (cos . x)) / ((sin . x) ^2)) is V11() V12() ext-real Element of REAL
K38((((tan . x) * (cos . x)) / ((sin . x) ^2))) is V11() V12() ext-real set
K36(((1 / ((cos . x) ^2)) / (sin . x)),K38((((tan . x) * (cos . x)) / ((sin . x) ^2)))) is V11() V12() ext-real set
() . x is V11() V12() ext-real Element of REAL
diff (tan,x) is V11() V12() ext-real Element of REAL
(() . x) * (diff (tan,x)) is V11() V12() ext-real Element of REAL
diff ((),x) is V11() V12() ext-real Element of REAL
(tan . x) * (diff ((),x)) is V11() V12() ext-real Element of REAL
((() . x) * (diff (tan,x))) + ((tan . x) * (diff ((),x))) is V11() V12() ext-real Element of REAL
(() . x) * (1 / ((cos . x) ^2)) is V11() V12() ext-real Element of REAL
((() . x) * (1 / ((cos . x) ^2))) + ((tan . x) * (diff ((),x))) is V11() V12() ext-real Element of REAL
(cos . x) / ((sin . x) ^2) is V11() V12() ext-real Element of REAL
K37((cos . x),K39(((sin . x) ^2))) is V11() V12() ext-real set
- ((cos . x) / ((sin . x) ^2)) is V11() V12() ext-real Element of REAL
(tan . x) * (- ((cos . x) / ((sin . x) ^2))) is V11() V12() ext-real Element of REAL
((() . x) * (1 / ((cos . x) ^2))) + ((tan . x) * (- ((cos . x) / ((sin . x) ^2)))) is V11() V12() ext-real Element of REAL
((1 / ((cos . x) ^2)) / (sin . x)) + ((tan . x) * (- ((cos . x) / ((sin . x) ^2)))) is V11() V12() ext-real Element of REAL
x is V11() V12() ext-real Element of REAL
((tan (#) ()) `| Z) . x is V11() V12() ext-real Element of REAL
cos . x is V11() V12() ext-real Element of REAL
(cos . x) ^2 is V11() V12() ext-real Element of REAL
K37((cos . x),(cos . x)) is V11() V12() ext-real set
1 / ((cos . x) ^2) is V11() V12() ext-real Element of REAL
K39(((cos . x) ^2)) is V11() V12() ext-real set
K37(1,K39(((cos . x) ^2))) is V11() V12() ext-real set
sin . x is V11() V12() ext-real Element of REAL
(1 / ((cos . x) ^2)) / (sin . x) is V11() V12() ext-real Element of REAL
K39((sin . x)) is V11() V12() ext-real set
K37((1 / ((cos . x) ^2)),K39((sin . x))) is V11() V12() ext-real set
tan . x is V11() V12() ext-real Element of REAL
(tan . x) * (cos . x) is V11() V12() ext-real Element of REAL
(sin . x) ^2 is V11() V12() ext-real Element of REAL
K37((sin . x),(sin . x)) is V11() V12() ext-real set
((tan . x) * (cos . x)) / ((sin . x) ^2) is V11() V12() ext-real Element of REAL
K39(((sin . x) ^2)) is V11() V12() ext-real set
K37(((tan . x) * (cos . x)),K39(((sin . x) ^2))) is V11() V12() ext-real set
((1 / ((cos . x) ^2)) / (sin . x)) - (((tan . x) * (cos . x)) / ((sin . x) ^2)) is V11() V12() ext-real Element of REAL
K38((((tan . x) * (cos . x)) / ((sin . x) ^2))) is V11() V12() ext-real set
K36(((1 / ((cos . x) ^2)) / (sin . x)),K38((((tan . x) * (cos . x)) / ((sin . x) ^2)))) is V11() V12() ext-real set
cot (#) () is V13() V16( REAL ) V17( REAL ) V18() V52() V53() V54() Element of K6(K7(REAL,REAL))
dom (cot (#) ()) is V62() V63() V64() Element of K6(REAL)
Z is open V62() V63() V64() Element of K6(REAL)
(cot (#) ()) `| Z is V13() V16( REAL ) V17( REAL ) V18() V52() V53() V54() Element of K6(K7(REAL,REAL))
(dom cot) /\ (dom ()) is V62() V63() V64() Element of K6(REAL)
x is V11() V12() ext-real Element of REAL
sin . x is V11() V12() ext-real Element of REAL
x is V11() V12() ext-real Element of REAL
diff ((),x) is V11() V12() ext-real Element of REAL
cos . x is V11() V12() ext-real Element of REAL
sin . x is V11() V12() ext-real Element of REAL
(sin . x) ^2 is V11() V12() ext-real Element of REAL
K37((sin . x),(sin . x)) is V11() V12() ext-real set
(cos . x) / ((sin . x) ^2) is V11() V12() ext-real Element of REAL
K39(((sin . x) ^2)) is V11() V12() ext-real set
K37((cos . x),K39(((sin . x) ^2))) is V11() V12() ext-real set
- ((cos . x) / ((sin . x) ^2)) is V11() V12() ext-real Element of REAL
x is V11() V12() ext-real Element of REAL
x is V11() V12() ext-real Element of REAL
((cot (#) ()) `| Z) . x is V11() V12() ext-real Element of REAL
sin . x is V11() V12() ext-real Element of REAL
(sin . x) ^2 is V11() V12() ext-real Element of REAL
K37((sin . x),(sin . x)) is V11() V12() ext-real set
1 / ((sin . x) ^2) is V11() V12() ext-real Element of REAL
K39(((sin . x) ^2)) is V11() V12() ext-real set
K37(1,K39(((sin . x) ^2))) is V11() V12() ext-real set
(1 / ((sin . x) ^2)) / (sin . x) is V11() V12() ext-real Element of REAL
K39((sin . x)) is V11() V12() ext-real set
K37((1 / ((sin . x) ^2)),K39((sin . x))) is V11() V12() ext-real set
- ((1 / ((sin . x) ^2)) / (sin . x)) is V11() V12() ext-real Element of REAL
cot . x is V11() V12() ext-real Element of REAL
cos . x is V11() V12() ext-real Element of REAL
(cot . x) * (cos . x) is V11() V12() ext-real Element of REAL
((cot . x) * (cos . x)) / ((sin . x) ^2) is V11() V12() ext-real Element of REAL
K37(((cot . x) * (cos . x)),K39(((sin . x) ^2))) is V11() V12() ext-real set
(- ((1 / ((sin . x) ^2)) / (sin . x))) - (((cot . x) * (cos . x)) / ((sin . x) ^2)) is V11() V12() ext-real Element of REAL
K38((((cot . x) * (cos . x)) / ((sin . x) ^2))) is V11() V12() ext-real set
K36((- ((1 / ((sin . x) ^2)) / (sin . x))),K38((((cot . x) * (cos . x)) / ((sin . x) ^2)))) is V11() V12() ext-real set
() . x is V11() V12() ext-real Element of REAL
diff (cot,x) is V11() V12() ext-real Element of REAL
(() . x) * (diff (cot,x)) is V11() V12() ext-real Element of REAL
diff ((),x) is V11() V12() ext-real Element of REAL
(cot . x) * (diff ((),x)) is V11() V12() ext-real Element of REAL
((() . x) * (diff (cot,x))) + ((cot . x) * (diff ((),x))) is V11() V12() ext-real Element of REAL
- (1 / ((sin . x) ^2)) is V11() V12() ext-real Element of REAL
(() . x) * (- (1 / ((sin . x) ^2))) is V11() V12() ext-real Element of REAL
((() . x) * (- (1 / ((sin . x) ^2)))) + ((cot . x) * (diff ((),x))) is V11() V12() ext-real Element of REAL
(cos . x) / ((sin . x) ^2) is V11() V12() ext-real Element of REAL
K37((cos . x),K39(((sin . x) ^2))) is V11() V12() ext-real set
- ((cos . x) / ((sin . x) ^2)) is V11() V12() ext-real Element of REAL
(cot . x) * (- ((cos . x) / ((sin . x) ^2))) is V11() V12() ext-real Element of REAL
((() . x) * (- (1 / ((sin . x) ^2)))) + ((cot . x) * (- ((cos . x) / ((sin . x) ^2)))) is V11() V12() ext-real Element of REAL
(- (1 / ((sin . x) ^2))) / (sin . x) is V11() V12() ext-real Element of REAL
K37((- (1 / ((sin . x) ^2))),K39((sin . x))) is V11() V12() ext-real set
((- (1 / ((sin . x) ^2))) / (sin . x)) + ((cot . x) * (- ((cos . x) / ((sin . x) ^2)))) is V11() V12() ext-real Element of REAL
x is V11() V12() ext-real Element of REAL
((cot (#) ()) `| Z) . x is V11() V12() ext-real Element of REAL
sin . x is V11() V12() ext-real Element of REAL
(sin . x) ^2 is V11() V12() ext-real Element of REAL
K37((sin . x),(sin . x)) is V11() V12() ext-real set
1 / ((sin . x) ^2) is V11() V12() ext-real Element of REAL
K39(((sin . x) ^2)) is V11() V12() ext-real set
K37(1,K39(((sin . x) ^2))) is V11() V12() ext-real set
(1 / ((sin . x) ^2)) / (sin . x) is V11() V12() ext-real Element of REAL
K39((sin . x)) is V11() V12() ext-real set
K37((1 / ((sin . x) ^2)),K39((sin . x))) is V11() V12() ext-real set
- ((1 / ((sin . x) ^2)) / (sin . x)) is V11() V12() ext-real Element of REAL
cot . x is V11() V12() ext-real Element of REAL
cos . x is V11() V12() ext-real Element of REAL
(cot . x) * (cos . x) is V11() V12() ext-real Element of REAL
((cot . x) * (cos . x)) / ((sin . x) ^2) is V11() V12() ext-real Element of REAL
K37(((cot . x) * (cos . x)),K39(((sin . x) ^2))) is V11() V12() ext-real set
(- ((1 / ((sin . x) ^2)) / (sin . x))) - (((cot . x) * (cos . x)) / ((sin . x) ^2)) is V11() V12() ext-real Element of REAL
K38((((cot . x) * (cos . x)) / ((sin . x) ^2))) is V11() V12() ext-real set
K36((- ((1 / ((sin . x) ^2)) / (sin . x))),K38((((cot . x) * (cos . x)) / ((sin . x) ^2)))) is V11() V12() ext-real set