REAL is non empty V35() V57() V58() V59() V63() set
NAT is non empty epsilon-transitive epsilon-connected ordinal V57() V58() V59() V60() V61() V62() V63() Element of bool REAL
bool REAL is set
[:NAT,REAL:] is Relation-like V46() V47() V48() set
bool [:NAT,REAL:] is set
COMPLEX is non empty V35() V57() V63() set
omega is non empty epsilon-transitive epsilon-connected ordinal V57() V58() V59() V60() V61() V62() V63() set
bool omega is set
bool NAT is set
RAT is non empty V35() V57() V58() V59() V60() V63() set
INT is non empty V35() V57() V58() V59() V60() V61() V63() set
ExtREAL is non empty V58() set
{} is Relation-like non-empty empty-yielding RAT -valued Function-like one-to-one constant functional empty epsilon-transitive epsilon-connected ordinal T-Sequence-like c=-linear natural V22() real ext-real non positive non negative V33() V46() V47() V48() V49() V57() V58() V59() V60() V61() V62() V63() V88() V89() V90() V91() V92() V93() V94() V95() V96() V97() V98() V99() set
the Relation-like non-empty empty-yielding RAT -valued Function-like one-to-one constant functional empty epsilon-transitive epsilon-connected ordinal T-Sequence-like c=-linear natural V22() real ext-real non positive non negative V33() V46() V47() V48() V49() V57() V58() V59() V60() V61() V62() V63() V88() V89() V90() V91() V92() V93() V94() V95() V96() V97() V98() V99() set is Relation-like non-empty empty-yielding RAT -valued Function-like one-to-one constant functional empty epsilon-transitive epsilon-connected ordinal T-Sequence-like c=-linear natural V22() real ext-real non positive non negative V33() V46() V47() V48() V49() V57() V58() V59() V60() V61() V62() V63() V88() V89() V90() V91() V92() V93() V94() V95() V96() V97() V98() V99() set
1 is non empty epsilon-transitive epsilon-connected ordinal natural V22() real ext-real positive non negative V33() V56() V57() V58() V59() V60() V61() V62() Element of NAT
{{},1} is non empty V57() V58() V59() V60() V61() V62() set
[:REAL,REAL:] is Relation-like V46() V47() V48() set
bool [:REAL,REAL:] is set
K36(REAL,REAL) is functional non empty V88() V89() V90() set
[:NAT,K36(REAL,REAL):] is Relation-like set
bool [:NAT,K36(REAL,REAL):] is set
[:NAT,COMPLEX:] is Relation-like V46() set
bool [:NAT,COMPLEX:] is set
[:COMPLEX,COMPLEX:] is Relation-like V46() set
bool [:COMPLEX,COMPLEX:] is set
0 is Relation-like non-empty empty-yielding RAT -valued Function-like one-to-one constant functional empty epsilon-transitive epsilon-connected ordinal T-Sequence-like c=-linear natural V22() real ext-real non positive non negative V33() V46() V47() V48() V49() V56() V57() V58() V59() V60() V61() V62() V63() V88() V89() V90() V91() V92() V93() V94() V95() V96() V97() V98() V99() Element of NAT
{0} is functional non empty V57() V58() V59() V60() V61() V62() V88() set
2 is non empty epsilon-transitive epsilon-connected ordinal natural V22() real ext-real positive non negative V33() V56() V57() V58() V59() V60() V61() V62() Element of NAT
1 / 2 is non empty V22() real ext-real positive non negative set
2 " is non empty V22() real ext-real positive non negative set
1 * (2 ") is non empty V22() real ext-real positive non negative set
tan is Relation-like REAL -defined REAL -valued Function-like V46() V47() V48() Element of bool [:REAL,REAL:]
sin is Relation-like REAL -defined REAL -valued Function-like non empty V14( REAL ) V30( REAL , REAL ) V46() V47() V48() Element of bool [:REAL,REAL:]
cos is Relation-like REAL -defined REAL -valued Function-like non empty V14( REAL ) V30( REAL , REAL ) V46() V47() V48() Element of bool [:REAL,REAL:]
sin / cos is Relation-like REAL -defined REAL -valued Function-like V46() V47() V48() Element of bool [:REAL,REAL:]
dom tan is V57() V58() V59() Element of bool REAL
cot is Relation-like REAL -defined REAL -valued Function-like V46() V47() V48() Element of bool [:REAL,REAL:]
cos / sin is Relation-like REAL -defined REAL -valued Function-like V46() V47() V48() Element of bool [:REAL,REAL:]
dom cot is V57() V58() V59() Element of bool REAL
number_e is V22() real ext-real Element of REAL
right_open_halfline 0 is non empty V57() V58() V59() Element of bool REAL
+infty is non empty non real ext-real positive non negative set
K567(0,+infty) is set
ln is Relation-like REAL -defined REAL -valued Function-like V46() V47() V48() Element of bool [:REAL,REAL:]
log_ number_e is Relation-like REAL -defined REAL -valued Function-like V46() V47() V48() Element of bool [:REAL,REAL:]
exp_R is Relation-like REAL -defined REAL -valued Function-like one-to-one non empty V14( REAL ) V30( REAL , REAL ) V46() V47() V48() Element of bool [:REAL,REAL:]
exp_R " is Relation-like REAL -defined REAL -valued Function-like one-to-one V46() V47() V48() Element of bool [:REAL,REAL:]
dom ln is V57() V58() V59() Element of bool REAL
rng ln is V57() V58() V59() Element of bool REAL
dom sin is non empty V57() V58() V59() Element of bool REAL
dom cos is non empty V57() V58() V59() Element of bool REAL
cos 0 is V22() real ext-real Element of REAL
cos . 0 is V22() real ext-real Element of REAL
sin 0 is V22() real ext-real Element of REAL
sin . 0 is V22() real ext-real Element of REAL
x is V22() real ext-real Element of REAL
log (number_e,x) is V22() real ext-real Element of REAL
h is V22() real ext-real Element of REAL
log (number_e,h) is V22() real ext-real Element of REAL
(log (number_e,x)) - (log (number_e,h)) is V22() real ext-real Element of REAL
- (log (number_e,h)) is V22() real ext-real set
(log (number_e,x)) + (- (log (number_e,h))) is V22() real ext-real set
x / h is V22() real ext-real Element of COMPLEX
h " is V22() real ext-real set
x * (h ") is V22() real ext-real set
log (number_e,(x / h)) is V22() real ext-real set
x is V22() real ext-real Element of REAL
log (number_e,x) is V22() real ext-real Element of REAL
h is V22() real ext-real Element of REAL
log (number_e,h) is V22() real ext-real Element of REAL
(log (number_e,x)) + (log (number_e,h)) is V22() real ext-real Element of REAL
x * h is V22() real ext-real Element of REAL
log (number_e,(x * h)) is V22() real ext-real Element of REAL
x is V22() real ext-real Element of REAL
log (number_e,x) is V22() real ext-real Element of REAL
ln . x is V22() real ext-real Element of REAL
{ b1 where b1 is V22() real ext-real Element of REAL : not b1 <= 0 } is set
x is V22() real ext-real Element of REAL
ln . x is V22() real ext-real Element of REAL
h is V22() real ext-real Element of REAL
ln . h is V22() real ext-real Element of REAL
(ln . x) - (ln . h) is V22() real ext-real Element of REAL
- (ln . h) is V22() real ext-real set
(ln . x) + (- (ln . h)) is V22() real ext-real set
x / h is V22() real ext-real Element of COMPLEX
h " is V22() real ext-real set
x * (h ") is V22() real ext-real set
ln . (x / h) is V22() real ext-real Element of REAL
log (number_e,(x / h)) is V22() real ext-real set
{ b1 where b1 is V22() real ext-real Element of REAL : not b1 <= 0 } is set
log (number_e,x) is V22() real ext-real Element of REAL
(log (number_e,x)) - (ln . h) is V22() real ext-real Element of REAL
(log (number_e,x)) + (- (ln . h)) is V22() real ext-real set
log (number_e,h) is V22() real ext-real Element of REAL
(log (number_e,x)) - (log (number_e,h)) is V22() real ext-real Element of REAL
- (log (number_e,h)) is V22() real ext-real set
(log (number_e,x)) + (- (log (number_e,h))) is V22() real ext-real set
x is V22() real ext-real Element of REAL
h is V22() real ext-real Element of REAL
1 / h is V22() real ext-real Element of COMPLEX
h " is V22() real ext-real set
1 * (h ") is V22() real ext-real set
f is V22() real ext-real Element of REAL
1 / f is V22() real ext-real Element of COMPLEX
f " is V22() real ext-real set
1 * (f ") is V22() real ext-real set
f1 is V22() real ext-real Element of REAL
f * f1 is V22() real ext-real Element of REAL
(f * f1) * h is V22() real ext-real Element of REAL
1 / ((f * f1) * h) is V22() real ext-real Element of COMPLEX
((f * f1) * h) " is V22() real ext-real set
1 * (((f * f1) * h) ") is V22() real ext-real set
1 / f1 is V22() real ext-real Element of COMPLEX
f1 " is V22() real ext-real set
1 * (f1 ") is V22() real ext-real set
(1 / h) + (1 / f1) is V22() real ext-real Element of COMPLEX
((1 / h) + (1 / f1)) + (1 / f) is V22() real ext-real Element of COMPLEX
(1 / ((f * f1) * h)) * (((1 / h) + (1 / f1)) + (1 / f)) is V22() real ext-real Element of COMPLEX
f1 * f is V22() real ext-real Element of REAL
f2 is V22() real ext-real Element of REAL
(f1 * f) * f2 is V22() real ext-real Element of REAL
1 / ((f1 * f) * f2) is V22() real ext-real Element of COMPLEX
((f1 * f) * f2) " is V22() real ext-real set
1 * (((f1 * f) * f2) ") is V22() real ext-real set
1 / f2 is V22() real ext-real Element of COMPLEX
f2 " is V22() real ext-real set
1 * (f2 ") is V22() real ext-real set
(1 / f2) + (1 / f) is V22() real ext-real Element of COMPLEX
((1 / f2) + (1 / f)) + (1 / f1) is V22() real ext-real Element of COMPLEX
(1 / ((f1 * f) * f2)) * (((1 / f2) + (1 / f)) + (1 / f1)) is V22() real ext-real Element of COMPLEX
((1 / ((f * f1) * h)) * (((1 / h) + (1 / f1)) + (1 / f))) - ((1 / ((f1 * f) * f2)) * (((1 / f2) + (1 / f)) + (1 / f1))) is V22() real ext-real Element of COMPLEX
- ((1 / ((f1 * f) * f2)) * (((1 / f2) + (1 / f)) + (1 / f1))) is V22() real ext-real set
((1 / ((f * f1) * h)) * (((1 / h) + (1 / f1)) + (1 / f))) + (- ((1 / ((f1 * f) * f2)) * (((1 / f2) + (1 / f)) + (1 / f1)))) is V22() real ext-real set
x * (((1 / ((f * f1) * h)) * (((1 / h) + (1 / f1)) + (1 / f))) - ((1 / ((f1 * f) * f2)) * (((1 / f2) + (1 / f)) + (1 / f1)))) is V22() real ext-real Element of REAL
h - f2 is V22() real ext-real Element of REAL
- f2 is V22() real ext-real set
h + (- f2) is V22() real ext-real set
(x * (((1 / ((f * f1) * h)) * (((1 / h) + (1 / f1)) + (1 / f))) - ((1 / ((f1 * f) * f2)) * (((1 / f2) + (1 / f)) + (1 / f1))))) / (h - f2) is V22() real ext-real Element of COMPLEX
(h - f2) " is V22() real ext-real set
(x * (((1 / ((f * f1) * h)) * (((1 / h) + (1 / f1)) + (1 / f))) - ((1 / ((f1 * f) * f2)) * (((1 / f2) + (1 / f)) + (1 / f1))))) * ((h - f2) ") is V22() real ext-real set
f is Relation-like REAL -defined REAL -valued Function-like non empty V14( REAL ) V30( REAL , REAL ) V46() V47() V48() Element of bool [:REAL,REAL:]
[!f,h,f,f1,f2!] is V22() real ext-real Element of REAL
[!f,h,f,f1!] is V22() real ext-real Element of REAL
[!f,h,f!] is V22() real ext-real Element of REAL
f . h is V22() real ext-real Element of REAL
f . f is V22() real ext-real Element of REAL
(f . h) - (f . f) is V22() real ext-real Element of REAL
- (f . f) is V22() real ext-real set
(f . h) + (- (f . f)) is V22() real ext-real set
h - f is V22() real ext-real set
- f is V22() real ext-real set
h + (- f) is V22() real ext-real set
((f . h) - (f . f)) / (h - f) is V22() real ext-real Element of REAL
(h - f) " is V22() real ext-real set
((f . h) - (f . f)) * ((h - f) ") is V22() real ext-real set
[!f,f,f1!] is V22() real ext-real Element of REAL
f . f1 is V22() real ext-real Element of REAL
(f . f) - (f . f1) is V22() real ext-real Element of REAL
- (f . f1) is V22() real ext-real set
(f . f) + (- (f . f1)) is V22() real ext-real set
f - f1 is V22() real ext-real set
- f1 is V22() real ext-real set
f + (- f1) is V22() real ext-real set
((f . f) - (f . f1)) / (f - f1) is V22() real ext-real Element of REAL
(f - f1) " is V22() real ext-real set
((f . f) - (f . f1)) * ((f - f1) ") is V22() real ext-real set
[!f,h,f!] - [!f,f,f1!] is V22() real ext-real Element of REAL
- [!f,f,f1!] is V22() real ext-real set
[!f,h,f!] + (- [!f,f,f1!]) is V22() real ext-real set
h - f1 is V22() real ext-real set
h + (- f1) is V22() real ext-real set
([!f,h,f!] - [!f,f,f1!]) / (h - f1) is V22() real ext-real Element of REAL
(h - f1) " is V22() real ext-real set
([!f,h,f!] - [!f,f,f1!]) * ((h - f1) ") is V22() real ext-real set
[!f,f,f1,f2!] is V22() real ext-real Element of REAL
[!f,f1,f2!] is V22() real ext-real Element of REAL
f . f2 is V22() real ext-real Element of REAL
(f . f1) - (f . f2) is V22() real ext-real Element of REAL
- (f . f2) is V22() real ext-real set
(f . f1) + (- (f . f2)) is V22() real ext-real set
f1 - f2 is V22() real ext-real set
f1 + (- f2) is V22() real ext-real set
((f . f1) - (f . f2)) / (f1 - f2) is V22() real ext-real Element of REAL
(f1 - f2) " is V22() real ext-real set
((f . f1) - (f . f2)) * ((f1 - f2) ") is V22() real ext-real set
[!f,f,f1!] - [!f,f1,f2!] is V22() real ext-real Element of REAL
- [!f,f1,f2!] is V22() real ext-real set
[!f,f,f1!] + (- [!f,f1,f2!]) is V22() real ext-real set
f - f2 is V22() real ext-real set
f + (- f2) is V22() real ext-real set
([!f,f,f1!] - [!f,f1,f2!]) / (f - f2) is V22() real ext-real Element of REAL
(f - f2) " is V22() real ext-real set
([!f,f,f1!] - [!f,f1,f2!]) * ((f - f2) ") is V22() real ext-real set
[!f,h,f,f1!] - [!f,f,f1,f2!] is V22() real ext-real Element of REAL
- [!f,f,f1,f2!] is V22() real ext-real set
[!f,h,f,f1!] + (- [!f,f,f1,f2!]) is V22() real ext-real set
h - f2 is V22() real ext-real set
([!f,h,f,f1!] - [!f,f,f1,f2!]) / (h - f2) is V22() real ext-real Element of REAL
(h - f2) " is V22() real ext-real set
([!f,h,f,f1!] - [!f,f,f1,f2!]) * ((h - f2) ") is V22() real ext-real set
h * f is V22() real ext-real Element of REAL
(h * f) * f1 is V22() real ext-real Element of REAL
x / ((h * f) * f1) is V22() real ext-real Element of COMPLEX
((h * f) * f1) " is V22() real ext-real set
x * (((h * f) * f1) ") is V22() real ext-real set
(1 / h) + (1 / f) is V22() real ext-real Element of COMPLEX
((1 / h) + (1 / f)) + (1 / f1) is V22() real ext-real Element of COMPLEX
(x / ((h * f) * f1)) * (((1 / h) + (1 / f)) + (1 / f1)) is V22() real ext-real Element of COMPLEX
x * (1 / ((f * f1) * h)) is V22() real ext-real Element of REAL
(x * (1 / ((f * f1) * h))) * (((1 / h) + (1 / f1)) + (1 / f)) is V22() real ext-real Element of REAL
(f * f1) * f2 is V22() real ext-real Element of REAL
x / ((f * f1) * f2) is V22() real ext-real Element of COMPLEX
((f * f1) * f2) " is V22() real ext-real set
x * (((f * f1) * f2) ") is V22() real ext-real set
(1 / f) + (1 / f1) is V22() real ext-real Element of COMPLEX
((1 / f) + (1 / f1)) + (1 / f2) is V22() real ext-real Element of COMPLEX
(x / ((f * f1) * f2)) * (((1 / f) + (1 / f1)) + (1 / f2)) is V22() real ext-real Element of COMPLEX
cot (#) cot is Relation-like REAL -defined REAL -valued Function-like V46() V47() V48() Element of bool [:REAL,REAL:]
x is V22() real ext-real Element of REAL
cos x is V22() real ext-real Element of REAL
cos . x is V22() real ext-real Element of REAL
(cos x) ^2 is V22() real ext-real Element of REAL
(cos x) * (cos x) is V22() real ext-real set
sin x is V22() real ext-real Element of REAL
sin . x is V22() real ext-real Element of REAL
h is V22() real ext-real Element of REAL
[!(cot (#) cot),x,h!] is V22() real ext-real Element of REAL
(cot (#) cot) . x is V22() real ext-real Element of REAL
(cot (#) cot) . h is V22() real ext-real Element of REAL
((cot (#) cot) . x) - ((cot (#) cot) . h) is V22() real ext-real Element of REAL
- ((cot (#) cot) . h) is V22() real ext-real set
((cot (#) cot) . x) + (- ((cot (#) cot) . h)) is V22() real ext-real set
x - h is V22() real ext-real set
- h is V22() real ext-real set
x + (- h) is V22() real ext-real set
(((cot (#) cot) . x) - ((cot (#) cot) . h)) / (x - h) is V22() real ext-real Element of REAL
(x - h) " is V22() real ext-real set
(((cot (#) cot) . x) - ((cot (#) cot) . h)) * ((x - h) ") is V22() real ext-real set
cos h is V22() real ext-real Element of REAL
cos . h is V22() real ext-real Element of REAL
(cos h) ^2 is V22() real ext-real Element of REAL
(cos h) * (cos h) is V22() real ext-real set
((cos h) ^2) - ((cos x) ^2) is V22() real ext-real Element of REAL
- ((cos x) ^2) is V22() real ext-real set
((cos h) ^2) + (- ((cos x) ^2)) is V22() real ext-real set
sin h is V22() real ext-real Element of REAL
sin . h is V22() real ext-real Element of REAL
(sin x) * (sin h) is V22() real ext-real Element of REAL
((sin x) * (sin h)) ^2 is V22() real ext-real Element of REAL
((sin x) * (sin h)) * ((sin x) * (sin h)) is V22() real ext-real set
x - h is V22() real ext-real Element of REAL
(((sin x) * (sin h)) ^2) * (x - h) is V22() real ext-real Element of REAL
(((cos h) ^2) - ((cos x) ^2)) / ((((sin x) * (sin h)) ^2) * (x - h)) is V22() real ext-real Element of COMPLEX
((((sin x) * (sin h)) ^2) * (x - h)) " is V22() real ext-real set
(((cos h) ^2) - ((cos x) ^2)) * (((((sin x) * (sin h)) ^2) * (x - h)) ") is V22() real ext-real set
- ((((cos h) ^2) - ((cos x) ^2)) / ((((sin x) * (sin h)) ^2) * (x - h))) is V22() real ext-real Element of COMPLEX
cot . x is V22() real ext-real Element of REAL
(cot . x) * (cot . x) is V22() real ext-real Element of REAL
((cot . x) * (cot . x)) - ((cot (#) cot) . h) is V22() real ext-real Element of REAL
((cot . x) * (cot . x)) + (- ((cot (#) cot) . h)) is V22() real ext-real set
(((cot . x) * (cot . x)) - ((cot (#) cot) . h)) / (x - h) is V22() real ext-real Element of COMPLEX
(x - h) " is V22() real ext-real set
(((cot . x) * (cot . x)) - ((cot (#) cot) . h)) * ((x - h) ") is V22() real ext-real set
cot . h is V22() real ext-real Element of REAL
(cot . h) * (cot . h) is V22() real ext-real Element of REAL
((cot . x) * (cot . x)) - ((cot . h) * (cot . h)) is V22() real ext-real Element of REAL
- ((cot . h) * (cot . h)) is V22() real ext-real set
((cot . x) * (cot . x)) + (- ((cot . h) * (cot . h))) is V22() real ext-real set
(((cot . x) * (cot . x)) - ((cot . h) * (cot . h))) / (x - h) is V22() real ext-real Element of COMPLEX
(((cot . x) * (cot . x)) - ((cot . h) * (cot . h))) * ((x - h) ") is V22() real ext-real set
cos . x is V22() real ext-real Element of REAL
sin . x is V22() real ext-real Element of REAL
(sin . x) " is V22() real ext-real Element of REAL
(cos . x) * ((sin . x) ") is V22() real ext-real Element of REAL
((cos . x) * ((sin . x) ")) * (cot . x) is V22() real ext-real Element of REAL
(((cos . x) * ((sin . x) ")) * (cot . x)) - ((cot . h) * (cot . h)) is V22() real ext-real Element of REAL
(((cos . x) * ((sin . x) ")) * (cot . x)) + (- ((cot . h) * (cot . h))) is V22() real ext-real set
((((cos . x) * ((sin . x) ")) * (cot . x)) - ((cot . h) * (cot . h))) / (x - h) is V22() real ext-real Element of COMPLEX
((((cos . x) * ((sin . x) ")) * (cot . x)) - ((cot . h) * (cot . h))) * ((x - h) ") is V22() real ext-real set
((cos . x) * ((sin . x) ")) * ((cos . x) * ((sin . x) ")) is V22() real ext-real Element of REAL
(((cos . x) * ((sin . x) ")) * ((cos . x) * ((sin . x) "))) - ((cot . h) * (cot . h)) is V22() real ext-real Element of REAL
(((cos . x) * ((sin . x) ")) * ((cos . x) * ((sin . x) "))) + (- ((cot . h) * (cot . h))) is V22() real ext-real set
((((cos . x) * ((sin . x) ")) * ((cos . x) * ((sin . x) "))) - ((cot . h) * (cot . h))) / (x - h) is V22() real ext-real Element of COMPLEX
((((cos . x) * ((sin . x) ")) * ((cos . x) * ((sin . x) "))) - ((cot . h) * (cot . h))) * ((x - h) ") is V22() real ext-real set
cos . h is V22() real ext-real Element of REAL
sin . h is V22() real ext-real Element of REAL
(sin . h) " is V22() real ext-real Element of REAL
(cos . h) * ((sin . h) ") is V22() real ext-real Element of REAL
((cos . h) * ((sin . h) ")) * (cot . h) is V22() real ext-real Element of REAL
(((cos . x) * ((sin . x) ")) * ((cos . x) * ((sin . x) "))) - (((cos . h) * ((sin . h) ")) * (cot . h)) is V22() real ext-real Element of REAL
- (((cos . h) * ((sin . h) ")) * (cot . h)) is V22() real ext-real set
(((cos . x) * ((sin . x) ")) * ((cos . x) * ((sin . x) "))) + (- (((cos . h) * ((sin . h) ")) * (cot . h))) is V22() real ext-real set
((((cos . x) * ((sin . x) ")) * ((cos . x) * ((sin . x) "))) - (((cos . h) * ((sin . h) ")) * (cot . h))) / (x - h) is V22() real ext-real Element of COMPLEX
((((cos . x) * ((sin . x) ")) * ((cos . x) * ((sin . x) "))) - (((cos . h) * ((sin . h) ")) * (cot . h))) * ((x - h) ") is V22() real ext-real set
cot x is V22() real ext-real Element of REAL
cos x is V22() real ext-real set
sin x is V22() real ext-real set
(cos x) / (sin x) is V22() real ext-real set
(sin x) " is V22() real ext-real set
(cos x) * ((sin x) ") is V22() real ext-real set
(cot x) ^2 is V22() real ext-real Element of REAL
(cot x) * (cot x) is V22() real ext-real set
cot h is V22() real ext-real Element of REAL
cos h is V22() real ext-real set
sin h is V22() real ext-real set
(cos h) / (sin h) is V22() real ext-real set
(sin h) " is V22() real ext-real set
(cos h) * ((sin h) ") is V22() real ext-real set
(cot h) ^2 is V22() real ext-real Element of REAL
(cot h) * (cot h) is V22() real ext-real set
((cot x) ^2) - ((cot h) ^2) is V22() real ext-real Element of REAL
- ((cot h) ^2) is V22() real ext-real set
((cot x) ^2) + (- ((cot h) ^2)) is V22() real ext-real set
(((cot x) ^2) - ((cot h) ^2)) / (x - h) is V22() real ext-real Element of COMPLEX
(((cot x) ^2) - ((cot h) ^2)) * ((x - h) ") is V22() real ext-real set
(cot x) - (cot h) is V22() real ext-real Element of REAL
- (cot h) is V22() real ext-real set
(cot x) + (- (cot h)) is V22() real ext-real set
(cot x) + (cot h) is V22() real ext-real Element of REAL
((cot x) - (cot h)) * ((cot x) + (cot h)) is V22() real ext-real Element of REAL
(((cot x) - (cot h)) * ((cot x) + (cot h))) / (x - h) is V22() real ext-real Element of COMPLEX
(((cot x) - (cot h)) * ((cot x) + (cot h))) * ((x - h) ") is V22() real ext-real set
sin (x - h) is V22() real ext-real Element of REAL
sin . (x - h) is V22() real ext-real Element of REAL
(sin (x - h)) / ((sin x) * (sin h)) is V22() real ext-real Element of COMPLEX
((sin x) * (sin h)) " is V22() real ext-real set
(sin (x - h)) * (((sin x) * (sin h)) ") is V22() real ext-real set
- ((sin (x - h)) / ((sin x) * (sin h))) is V22() real ext-real Element of COMPLEX
(- ((sin (x - h)) / ((sin x) * (sin h)))) * ((cot x) + (cot h)) is V22() real ext-real Element of REAL
((- ((sin (x - h)) / ((sin x) * (sin h)))) * ((cot x) + (cot h))) / (x - h) is V22() real ext-real Element of COMPLEX
((- ((sin (x - h)) / ((sin x) * (sin h)))) * ((cot x) + (cot h))) * ((x - h) ") is V22() real ext-real set
((sin (x - h)) / ((sin x) * (sin h))) * ((cot x) + (cot h)) is V22() real ext-real Element of REAL
- (((sin (x - h)) / ((sin x) * (sin h))) * ((cot x) + (cot h))) is V22() real ext-real Element of REAL
(- (((sin (x - h)) / ((sin x) * (sin h))) * ((cot x) + (cot h)))) / (x - h) is V22() real ext-real Element of COMPLEX
(- (((sin (x - h)) / ((sin x) * (sin h))) * ((cot x) + (cot h)))) * ((x - h) ") is V22() real ext-real set
x + h is V22() real ext-real Element of REAL
sin (x + h) is V22() real ext-real Element of REAL
sin . (x + h) is V22() real ext-real Element of REAL
(sin (x + h)) / ((sin x) * (sin h)) is V22() real ext-real Element of COMPLEX
(sin (x + h)) * (((sin x) * (sin h)) ") is V22() real ext-real set
((sin (x - h)) / ((sin x) * (sin h))) * ((sin (x + h)) / ((sin x) * (sin h))) is V22() real ext-real Element of COMPLEX
- (((sin (x - h)) / ((sin x) * (sin h))) * ((sin (x + h)) / ((sin x) * (sin h)))) is V22() real ext-real Element of COMPLEX
(- (((sin (x - h)) / ((sin x) * (sin h))) * ((sin (x + h)) / ((sin x) * (sin h))))) / (x - h) is V22() real ext-real Element of COMPLEX
(- (((sin (x - h)) / ((sin x) * (sin h))) * ((sin (x + h)) / ((sin x) * (sin h))))) * ((x - h) ") is V22() real ext-real set
(sin (x + h)) * (sin (x - h)) is V22() real ext-real Element of REAL
((sin (x + h)) * (sin (x - h))) / (((sin x) * (sin h)) ^2) is V22() real ext-real Element of COMPLEX
(((sin x) * (sin h)) ^2) " is V22() real ext-real set
((sin (x + h)) * (sin (x - h))) * ((((sin x) * (sin h)) ^2) ") is V22() real ext-real set
- (((sin (x + h)) * (sin (x - h))) / (((sin x) * (sin h)) ^2)) is V22() real ext-real Element of COMPLEX
(- (((sin (x + h)) * (sin (x - h))) / (((sin x) * (sin h)) ^2))) / (x - h) is V22() real ext-real Element of COMPLEX
(- (((sin (x + h)) * (sin (x - h))) / (((sin x) * (sin h)) ^2))) * ((x - h) ") is V22() real ext-real set
(((cos h) ^2) - ((cos x) ^2)) / (((sin x) * (sin h)) ^2) is V22() real ext-real Element of COMPLEX
(((cos h) ^2) - ((cos x) ^2)) * ((((sin x) * (sin h)) ^2) ") is V22() real ext-real set
- ((((cos h) ^2) - ((cos x) ^2)) / (((sin x) * (sin h)) ^2)) is V22() real ext-real Element of COMPLEX
(- ((((cos h) ^2) - ((cos x) ^2)) / (((sin x) * (sin h)) ^2))) / (x - h) is V22() real ext-real Element of COMPLEX
(- ((((cos h) ^2) - ((cos x) ^2)) / (((sin x) * (sin h)) ^2))) * ((x - h) ") is V22() real ext-real set
((((cos h) ^2) - ((cos x) ^2)) / (((sin x) * (sin h)) ^2)) / (x - h) is V22() real ext-real Element of COMPLEX
((((cos h) ^2) - ((cos x) ^2)) / (((sin x) * (sin h)) ^2)) * ((x - h) ") is V22() real ext-real set
- (((((cos h) ^2) - ((cos x) ^2)) / (((sin x) * (sin h)) ^2)) / (x - h)) is V22() real ext-real Element of COMPLEX
1 / 2 is non empty V22() real ext-real positive non negative Element of COMPLEX
x is V22() real ext-real Element of REAL
2 * x is V22() real ext-real Element of REAL
cos (2 * x) is V22() real ext-real Element of REAL
cos . (2 * x) is V22() real ext-real Element of REAL
sin x is V22() real ext-real Element of REAL
sin . x is V22() real ext-real Element of REAL
h is V22() real ext-real Element of REAL
x + h is V22() real ext-real Element of REAL
fD ((cot (#) cot),h) is Relation-like REAL -defined REAL -valued Function-like V46() V47() V48() Element of bool [:REAL,REAL:]
Shift ((cot (#) cot),h) is Relation-like REAL -defined REAL -valued Function-like V46() V47() V48() Element of bool [:REAL,REAL:]
(Shift ((cot (#) cot),h)) - (cot (#) cot) is Relation-like REAL -defined REAL -valued Function-like V46() V47() V48() Element of bool [:REAL,REAL:]
- (cot (#) cot) is Relation-like REAL -defined Function-like V46() V47() V48() set
- 1 is non empty V22() real ext-real non positive negative V33() set
(- 1) (#) (cot (#) cot) is Relation-like REAL -defined Function-like V46() V47() V48() set
(Shift ((cot (#) cot),h)) + (- (cot (#) cot)) is Relation-like REAL -defined Function-like V46() V47() V48() set
(fD ((cot (#) cot),h)) . x is V22() real ext-real Element of REAL
2 * (x + h) is V22() real ext-real Element of REAL
cos (2 * (x + h)) is V22() real ext-real Element of REAL
cos . (2 * (x + h)) is V22() real ext-real Element of REAL
(cos (2 * (x + h))) - (cos (2 * x)) is V22() real ext-real Element of REAL
- (cos (2 * x)) is V22() real ext-real set
(cos (2 * (x + h))) + (- (cos (2 * x))) is V22() real ext-real set
(1 / 2) * ((cos (2 * (x + h))) - (cos (2 * x))) is V22() real ext-real Element of REAL
sin (x + h) is V22() real ext-real Element of REAL
sin . (x + h) is V22() real ext-real Element of REAL
(sin (x + h)) * (sin x) is V22() real ext-real Element of REAL
((sin (x + h)) * (sin x)) ^2 is V22() real ext-real Element of REAL
((sin (x + h)) * (sin x)) * ((sin (x + h)) * (sin x)) is V22() real ext-real set
((1 / 2) * ((cos (2 * (x + h))) - (cos (2 * x)))) / (((sin (x + h)) * (sin x)) ^2) is V22() real ext-real Element of COMPLEX
(((sin (x + h)) * (sin x)) ^2) " is V22() real ext-real set
((1 / 2) * ((cos (2 * (x + h))) - (cos (2 * x)))) * ((((sin (x + h)) * (sin x)) ^2) ") is V22() real ext-real set
dom (cot (#) cot) is V57() V58() V59() Element of bool REAL
(dom cot) /\ (dom cot) is V57() V58() V59() Element of bool REAL
(cot (#) cot) . (x + h) is V22() real ext-real Element of REAL
(cot (#) cot) . x is V22() real ext-real Element of REAL
((cot (#) cot) . (x + h)) - ((cot (#) cot) . x) is V22() real ext-real Element of REAL
- ((cot (#) cot) . x) is V22() real ext-real set
((cot (#) cot) . (x + h)) + (- ((cot (#) cot) . x)) is V22() real ext-real set
cot . (x + h) is V22() real ext-real Element of REAL
(cot . (x + h)) * (cot . (x + h)) is V22() real ext-real Element of REAL
((cot . (x + h)) * (cot . (x + h))) - ((cot (#) cot) . x) is V22() real ext-real Element of REAL
((cot . (x + h)) * (cot . (x + h))) + (- ((cot (#) cot) . x)) is V22() real ext-real set
cot . x is V22() real ext-real Element of REAL
(cot . x) * (cot . x) is V22() real ext-real Element of REAL
((cot . (x + h)) * (cot . (x + h))) - ((cot . x) * (cot . x)) is V22() real ext-real Element of REAL
- ((cot . x) * (cot . x)) is V22() real ext-real set
((cot . (x + h)) * (cot . (x + h))) + (- ((cot . x) * (cot . x))) is V22() real ext-real set
cos . (x + h) is V22() real ext-real Element of REAL
sin . (x + h) is V22() real ext-real Element of REAL
(sin . (x + h)) " is V22() real ext-real Element of REAL
(cos . (x + h)) * ((sin . (x + h)) ") is V22() real ext-real Element of REAL
((cos . (x + h)) * ((sin . (x + h)) ")) * (cot . (x + h)) is V22() real ext-real Element of REAL
(((cos . (x + h)) * ((sin . (x + h)) ")) * (cot . (x + h))) - ((cot . x) * (cot . x)) is V22() real ext-real Element of REAL
(((cos . (x + h)) * ((sin . (x + h)) ")) * (cot . (x + h))) + (- ((cot . x) * (cot . x))) is V22() real ext-real set
((cos . (x + h)) * ((sin . (x + h)) ")) * ((cos . (x + h)) * ((sin . (x + h)) ")) is V22() real ext-real Element of REAL
(((cos . (x + h)) * ((sin . (x + h)) ")) * ((cos . (x + h)) * ((sin . (x + h)) "))) - ((cot . x) * (cot . x)) is V22() real ext-real Element of REAL
(((cos . (x + h)) * ((sin . (x + h)) ")) * ((cos . (x + h)) * ((sin . (x + h)) "))) + (- ((cot . x) * (cot . x))) is V22() real ext-real set
cos . x is V22() real ext-real Element of REAL
sin . x is V22() real ext-real Element of REAL
(sin . x) " is V22() real ext-real Element of REAL
(cos . x) * ((sin . x) ") is V22() real ext-real Element of REAL
((cos . x) * ((sin . x) ")) * (cot . x) is V22() real ext-real Element of REAL
(((cos . (x + h)) * ((sin . (x + h)) ")) * ((cos . (x + h)) * ((sin . (x + h)) "))) - (((cos . x) * ((sin . x) ")) * (cot . x)) is V22() real ext-real Element of REAL
- (((cos . x) * ((sin . x) ")) * (cot . x)) is V22() real ext-real set
(((cos . (x + h)) * ((sin . (x + h)) ")) * ((cos . (x + h)) * ((sin . (x + h)) "))) + (- (((cos . x) * ((sin . x) ")) * (cot . x))) is V22() real ext-real set
cot (x + h) is V22() real ext-real Element of REAL
cos (x + h) is V22() real ext-real set
cos . (x + h) is V22() real ext-real Element of REAL
sin (x + h) is V22() real ext-real set
(cos (x + h)) / (sin (x + h)) is V22() real ext-real set
(sin (x + h)) " is V22() real ext-real set
(cos (x + h)) * ((sin (x + h)) ") is V22() real ext-real set
(cot (x + h)) ^2 is V22() real ext-real Element of REAL
(cot (x + h)) * (cot (x + h)) is V22() real ext-real set
cot x is V22() real ext-real Element of REAL
cos x is V22() real ext-real set
cos . x is V22() real ext-real Element of REAL
sin x is V22() real ext-real set
(cos x) / (sin x) is V22() real ext-real set
(sin x) " is V22() real ext-real set
(cos x) * ((sin x) ") is V22() real ext-real set
(cot x) ^2 is V22() real ext-real Element of REAL
(cot x) * (cot x) is V22() real ext-real set
((cot (x + h)) ^2) - ((cot x) ^2) is V22() real ext-real Element of REAL
- ((cot x) ^2) is V22() real ext-real set
((cot (x + h)) ^2) + (- ((cot x) ^2)) is V22() real ext-real set
(cot (x + h)) - (cot x) is V22() real ext-real Element of REAL
- (cot x) is V22() real ext-real set
(cot (x + h)) + (- (cot x)) is V22() real ext-real set
(cot (x + h)) + (cot x) is V22() real ext-real Element of REAL
((cot (x + h)) - (cot x)) * ((cot (x + h)) + (cot x)) is V22() real ext-real Element of REAL
(x + h) - x is V22() real ext-real Element of REAL
- x is V22() real ext-real set
(x + h) + (- x) is V22() real ext-real set
sin ((x + h) - x) is V22() real ext-real Element of REAL
sin . ((x + h) - x) is V22() real ext-real Element of REAL
(sin ((x + h) - x)) / ((sin (x + h)) * (sin x)) is V22() real ext-real Element of COMPLEX
((sin (x + h)) * (sin x)) " is V22() real ext-real set
(sin ((x + h) - x)) * (((sin (x + h)) * (sin x)) ") is V22() real ext-real set
- ((sin ((x + h) - x)) / ((sin (x + h)) * (sin x))) is V22() real ext-real Element of COMPLEX
(- ((sin ((x + h) - x)) / ((sin (x + h)) * (sin x)))) * ((cot (x + h)) + (cot x)) is V22() real ext-real Element of REAL
(x + h) + x is V22() real ext-real Element of REAL
sin ((x + h) + x) is V22() real ext-real Element of REAL
sin . ((x + h) + x) is V22() real ext-real Element of REAL
(sin ((x + h) + x)) / ((sin (x + h)) * (sin x)) is V22() real ext-real Element of COMPLEX
(sin ((x + h) + x)) * (((sin (x + h)) * (sin x)) ") is V22() real ext-real set
(- ((sin ((x + h) - x)) / ((sin (x + h)) * (sin x)))) * ((sin ((x + h) + x)) / ((sin (x + h)) * (sin x))) is V22() real ext-real Element of COMPLEX
((sin ((x + h) - x)) / ((sin (x + h)) * (sin x))) * ((sin ((x + h) + x)) / ((sin (x + h)) * (sin x))) is V22() real ext-real Element of COMPLEX
- (((sin ((x + h) - x)) / ((sin (x + h)) * (sin x))) * ((sin ((x + h) + x)) / ((sin (x + h)) * (sin x)))) is V22() real ext-real Element of COMPLEX
(2 * x) + h is V22() real ext-real Element of REAL
sin ((2 * x) + h) is V22() real ext-real Element of REAL
sin . ((2 * x) + h) is V22() real ext-real Element of REAL
sin h is V22() real ext-real Element of REAL
sin . h is V22() real ext-real Element of REAL
(sin ((2 * x) + h)) * (sin h) is V22() real ext-real Element of REAL
((sin ((2 * x) + h)) * (sin h)) / (((sin (x + h)) * (sin x)) ^2) is V22() real ext-real Element of COMPLEX
((sin ((2 * x) + h)) * (sin h)) * ((((sin (x + h)) * (sin x)) ^2) ") is V22() real ext-real set
- (((sin ((2 * x) + h)) * (sin h)) / (((sin (x + h)) * (sin x)) ^2)) is V22() real ext-real Element of COMPLEX
((2 * x) + h) + h is V22() real ext-real Element of REAL
cos (((2 * x) + h) + h) is V22() real ext-real Element of REAL
cos . (((2 * x) + h) + h) is V22() real ext-real Element of REAL
((2 * x) + h) - h is V22() real ext-real Element of REAL
- h is V22() real ext-real set
((2 * x) + h) + (- h) is V22() real ext-real set
cos (((2 * x) + h) - h) is V22() real ext-real Element of REAL
cos . (((2 * x) + h) - h) is V22() real ext-real Element of REAL
(cos (((2 * x) + h) + h)) - (cos (((2 * x) + h) - h)) is V22() real ext-real Element of REAL
- (cos (((2 * x) + h) - h)) is V22() real ext-real set
(cos (((2 * x) + h) + h)) + (- (cos (((2 * x) + h) - h))) is V22() real ext-real set
(1 / 2) * ((cos (((2 * x) + h) + h)) - (cos (((2 * x) + h) - h))) is V22() real ext-real Element of REAL
- ((1 / 2) * ((cos (((2 * x) + h) + h)) - (cos (((2 * x) + h) - h)))) is V22() real ext-real Element of REAL
(- ((1 / 2) * ((cos (((2 * x) + h) + h)) - (cos (((2 * x) + h) - h))))) / (((sin (x + h)) * (sin x)) ^2) is V22() real ext-real Element of COMPLEX
(- ((1 / 2) * ((cos (((2 * x) + h) + h)) - (cos (((2 * x) + h) - h))))) * ((((sin (x + h)) * (sin x)) ^2) ") is V22() real ext-real set
- ((- ((1 / 2) * ((cos (((2 * x) + h) + h)) - (cos (((2 * x) + h) - h))))) / (((sin (x + h)) * (sin x)) ^2)) is V22() real ext-real Element of COMPLEX
x is V22() real ext-real Element of REAL
2 * x is V22() real ext-real Element of REAL
cos (2 * x) is V22() real ext-real Element of REAL
cos . (2 * x) is V22() real ext-real Element of REAL
sin x is V22() real ext-real Element of REAL
sin . x is V22() real ext-real Element of REAL
h is V22() real ext-real Element of REAL
x - h is V22() real ext-real Element of REAL
- h is V22() real ext-real set
x + (- h) is V22() real ext-real set
bD ((cot (#) cot),h) is Relation-like REAL -defined REAL -valued Function-like V46() V47() V48() Element of bool [:REAL,REAL:]
Shift ((cot (#) cot),(- h)) is Relation-like REAL -defined REAL -valued Function-like V46() V47() V48() Element of bool [:REAL,REAL:]
(cot (#) cot) - (Shift ((cot (#) cot),(- h))) is Relation-like REAL -defined REAL -valued Function-like V46() V47() V48() Element of bool [:REAL,REAL:]
- (Shift ((cot (#) cot),(- h))) is Relation-like REAL -defined Function-like V46() V47() V48() set
- 1 is non empty V22() real ext-real non positive negative V33() set
(- 1) (#) (Shift ((cot (#) cot),(- h))) is Relation-like REAL -defined Function-like V46() V47() V48() set
(cot (#) cot) + (- (Shift ((cot (#) cot),(- h)))) is Relation-like REAL -defined Function-like V46() V47() V48() set
(bD ((cot (#) cot),h)) . x is V22() real ext-real Element of REAL
h - x is V22() real ext-real Element of REAL
- x is V22() real ext-real set
h + (- x) is V22() real ext-real set
2 * (h - x) is V22() real ext-real Element of REAL
cos (2 * (h - x)) is V22() real ext-real Element of REAL
cos . (2 * (h - x)) is V22() real ext-real Element of REAL
(cos (2 * x)) - (cos (2 * (h - x))) is V22() real ext-real Element of REAL
- (cos (2 * (h - x))) is V22() real ext-real set
(cos (2 * x)) + (- (cos (2 * (h - x)))) is V22() real ext-real set
(1 / 2) * ((cos (2 * x)) - (cos (2 * (h - x)))) is V22() real ext-real Element of REAL
sin (x - h) is V22() real ext-real Element of REAL
sin . (x - h) is V22() real ext-real Element of REAL
(sin x) * (sin (x - h)) is V22() real ext-real Element of REAL
((sin x) * (sin (x - h))) ^2 is V22() real ext-real Element of REAL
((sin x) * (sin (x - h))) * ((sin x) * (sin (x - h))) is V22() real ext-real set
((1 / 2) * ((cos (2 * x)) - (cos (2 * (h - x))))) / (((sin x) * (sin (x - h))) ^2) is V22() real ext-real Element of COMPLEX
(((sin x) * (sin (x - h))) ^2) " is V22() real ext-real set
((1 / 2) * ((cos (2 * x)) - (cos (2 * (h - x))))) * ((((sin x) * (sin (x - h))) ^2) ") is V22() real ext-real set
dom (cot (#) cot) is V57() V58() V59() Element of bool REAL
(dom cot) /\ (dom cot) is V57() V58() V59() Element of bool REAL
(cot (#) cot) . x is V22() real ext-real Element of REAL
(cot (#) cot) . (x - h) is V22() real ext-real Element of REAL
((cot (#) cot) . x) - ((cot (#) cot) . (x - h)) is V22() real ext-real Element of REAL
- ((cot (#) cot) . (x - h)) is V22() real ext-real set
((cot (#) cot) . x) + (- ((cot (#) cot) . (x - h))) is V22() real ext-real set
cot . x is V22() real ext-real Element of REAL
(cot . x) * (cot . x) is V22() real ext-real Element of REAL
((cot . x) * (cot . x)) - ((cot (#) cot) . (x - h)) is V22() real ext-real Element of REAL
((cot . x) * (cot . x)) + (- ((cot (#) cot) . (x - h))) is V22() real ext-real set
cot . (x - h) is V22() real ext-real Element of REAL
(cot . (x - h)) * (cot . (x - h)) is V22() real ext-real Element of REAL
((cot . x) * (cot . x)) - ((cot . (x - h)) * (cot . (x - h))) is V22() real ext-real Element of REAL
- ((cot . (x - h)) * (cot . (x - h))) is V22() real ext-real set
((cot . x) * (cot . x)) + (- ((cot . (x - h)) * (cot . (x - h)))) is V22() real ext-real set
cos . x is V22() real ext-real Element of REAL
sin . x is V22() real ext-real Element of REAL
(sin . x) " is V22() real ext-real Element of REAL
(cos . x) * ((sin . x) ") is V22() real ext-real Element of REAL
((cos . x) * ((sin . x) ")) * (cot . x) is V22() real ext-real Element of REAL
(((cos . x) * ((sin . x) ")) * (cot . x)) - ((cot . (x - h)) * (cot . (x - h))) is V22() real ext-real Element of REAL
(((cos . x) * ((sin . x) ")) * (cot . x)) + (- ((cot . (x - h)) * (cot . (x - h)))) is V22() real ext-real set
((cos . x) * ((sin . x) ")) * ((cos . x) * ((sin . x) ")) is V22() real ext-real Element of REAL
(((cos . x) * ((sin . x) ")) * ((cos . x) * ((sin . x) "))) - ((cot . (x - h)) * (cot . (x - h))) is V22() real ext-real Element of REAL
(((cos . x) * ((sin . x) ")) * ((cos . x) * ((sin . x) "))) + (- ((cot . (x - h)) * (cot . (x - h)))) is V22() real ext-real set
cos . (x - h) is V22() real ext-real Element of REAL
sin . (x - h) is V22() real ext-real Element of REAL
(sin . (x - h)) " is V22() real ext-real Element of REAL
(cos . (x - h)) * ((sin . (x - h)) ") is V22() real ext-real Element of REAL
((cos . (x - h)) * ((sin . (x - h)) ")) * (cot . (x - h)) is V22() real ext-real Element of REAL
(((cos . x) * ((sin . x) ")) * ((cos . x) * ((sin . x) "))) - (((cos . (x - h)) * ((sin . (x - h)) ")) * (cot . (x - h))) is V22() real ext-real Element of REAL
- (((cos . (x - h)) * ((sin . (x - h)) ")) * (cot . (x - h))) is V22() real ext-real set
(((cos . x) * ((sin . x) ")) * ((cos . x) * ((sin . x) "))) + (- (((cos . (x - h)) * ((sin . (x - h)) ")) * (cot . (x - h)))) is V22() real ext-real set
cot x is V22() real ext-real Element of REAL
cos x is V22() real ext-real set
cos . x is V22() real ext-real Element of REAL
sin x is V22() real ext-real set
(cos x) / (sin x) is V22() real ext-real set
(sin x) " is V22() real ext-real set
(cos x) * ((sin x) ") is V22() real ext-real set
(cot x) ^2 is V22() real ext-real Element of REAL
(cot x) * (cot x) is V22() real ext-real set
cot (x - h) is V22() real ext-real Element of REAL
cos (x - h) is V22() real ext-real set
cos . (x - h) is V22() real ext-real Element of REAL
sin (x - h) is V22() real ext-real set
(cos (x - h)) / (sin (x - h)) is V22() real ext-real set
(sin (x - h)) " is V22() real ext-real set
(cos (x - h)) * ((sin (x - h)) ") is V22() real ext-real set
(cot (x - h)) ^2 is V22() real ext-real Element of REAL
(cot (x - h)) * (cot (x - h)) is V22() real ext-real set
((cot x) ^2) - ((cot (x - h)) ^2) is V22() real ext-real Element of REAL
- ((cot (x - h)) ^2) is V22() real ext-real set
((cot x) ^2) + (- ((cot (x - h)) ^2)) is V22() real ext-real set
(cot x) - (cot (x - h)) is V22() real ext-real Element of REAL
- (cot (x - h)) is V22() real ext-real set
(cot x) + (- (cot (x - h))) is V22() real ext-real set
(cot x) + (cot (x - h)) is V22() real ext-real Element of REAL
((cot x) - (cot (x - h))) * ((cot x) + (cot (x - h))) is V22() real ext-real Element of REAL
x - (x - h) is V22() real ext-real Element of REAL
- (x - h) is V22() real ext-real set
x + (- (x - h)) is V22() real ext-real set
sin (x - (x - h)) is V22() real ext-real Element of REAL
sin . (x - (x - h)) is V22() real ext-real Element of REAL
(sin (x - (x - h))) / ((sin x) * (sin (x - h))) is V22() real ext-real Element of COMPLEX
((sin x) * (sin (x - h))) " is V22() real ext-real set
(sin (x - (x - h))) * (((sin x) * (sin (x - h))) ") is V22() real ext-real set
- ((sin (x - (x - h))) / ((sin x) * (sin (x - h)))) is V22() real ext-real Element of COMPLEX
(- ((sin (x - (x - h))) / ((sin x) * (sin (x - h))))) * ((cot x) + (cot (x - h))) is V22() real ext-real Element of REAL
((sin (x - (x - h))) / ((sin x) * (sin (x - h)))) * ((cot x) + (cot (x - h))) is V22() real ext-real Element of REAL
- (((sin (x - (x - h))) / ((sin x) * (sin (x - h)))) * ((cot x) + (cot (x - h)))) is V22() real ext-real Element of REAL
sin h is V22() real ext-real Element of REAL
sin . h is V22() real ext-real Element of REAL
(sin h) / ((sin x) * (sin (x - h))) is V22() real ext-real Element of COMPLEX
(sin h) * (((sin x) * (sin (x - h))) ") is V22() real ext-real set
x + (x - h) is V22() real ext-real Element of REAL
sin (x + (x - h)) is V22() real ext-real Element of REAL
sin . (x + (x - h)) is V22() real ext-real Element of REAL
(sin (x + (x - h))) / ((sin x) * (sin (x - h))) is V22() real ext-real Element of COMPLEX
(sin (x + (x - h))) * (((sin x) * (sin (x - h))) ") is V22() real ext-real set
((sin h) / ((sin x) * (sin (x - h)))) * ((sin (x + (x - h))) / ((sin x) * (sin (x - h)))) is V22() real ext-real Element of COMPLEX
- (((sin h) / ((sin x) * (sin (x - h)))) * ((sin (x + (x - h))) / ((sin x) * (sin (x - h))))) is V22() real ext-real Element of COMPLEX
(2 * x) - h is V22() real ext-real Element of REAL
(2 * x) + (- h) is V22() real ext-real set
sin ((2 * x) - h) is V22() real ext-real Element of REAL
sin . ((2 * x) - h) is V22() real ext-real Element of REAL
(sin h) * (sin ((2 * x) - h)) is V22() real ext-real Element of REAL
((sin h) * (sin ((2 * x) - h))) / (((sin x) * (sin (x - h))) ^2) is V22() real ext-real Element of COMPLEX
((sin h) * (sin ((2 * x) - h))) * ((((sin x) * (sin (x - h))) ^2) ") is V22() real ext-real set
- (((sin h) * (sin ((2 * x) - h))) / (((sin x) * (sin (x - h))) ^2)) is V22() real ext-real Element of COMPLEX
h + ((2 * x) - h) is V22() real ext-real Element of REAL
cos (h + ((2 * x) - h)) is V22() real ext-real Element of REAL
cos . (h + ((2 * x) - h)) is V22() real ext-real Element of REAL
h - ((2 * x) - h) is V22() real ext-real Element of REAL
- ((2 * x) - h) is V22() real ext-real set
h + (- ((2 * x) - h)) is V22() real ext-real set
cos (h - ((2 * x) - h)) is V22() real ext-real Element of REAL
cos . (h - ((2 * x) - h)) is V22() real ext-real Element of REAL
(cos (h + (