:: SIN_COS8 semantic presentation

REAL is V45() V46() V47() V51() set
NAT is V45() V46() V47() V48() V49() V50() V51() Element of K6(REAL)
K6(REAL) is set
COMPLEX is V45() V51() set
RAT is V45() V46() V47() V48() V51() set
INT is V45() V46() V47() V48() V49() V51() set
K7(COMPLEX,COMPLEX) is V35() set
K6(K7(COMPLEX,COMPLEX)) is set
K7(K7(COMPLEX,COMPLEX),COMPLEX) is V35() set
K6(K7(K7(COMPLEX,COMPLEX),COMPLEX)) is set
K7(REAL,REAL) is V35() V36() V37() set
K6(K7(REAL,REAL)) is set
K7(K7(REAL,REAL),REAL) is V35() V36() V37() set
K6(K7(K7(REAL,REAL),REAL)) is set
K7(RAT,RAT) is V20( RAT ) V35() V36() V37() set
K6(K7(RAT,RAT)) is set
K7(K7(RAT,RAT),RAT) is V20( RAT ) V35() V36() V37() set
K6(K7(K7(RAT,RAT),RAT)) is set
K7(INT,INT) is V20( RAT ) V20( INT ) V35() V36() V37() set
K6(K7(INT,INT)) is set
K7(K7(INT,INT),INT) is V20( RAT ) V20( INT ) V35() V36() V37() set
K6(K7(K7(INT,INT),INT)) is set
K7(NAT,NAT) is V20( RAT ) V20( INT ) V35() V36() V37() V38() set
K7(K7(NAT,NAT),NAT) is V20( RAT ) V20( INT ) V35() V36() V37() V38() set
K6(K7(K7(NAT,NAT),NAT)) is set
K7(NAT,REAL) is V35() V36() V37() set
K6(K7(NAT,REAL)) is set
K7(NAT,COMPLEX) is V35() set
K6(K7(NAT,COMPLEX)) is set
omega is V45() V46() V47() V48() V49() V50() V51() set
K6(omega) is set
K6(NAT) is set
0 is V1() ordinal natural V11() real ext-real non positive non negative V33() V34() V45() V46() V47() V48() V49() V50() V51() Element of NAT
1 is V1() ordinal natural V11() real ext-real positive non negative V33() V34() V45() V46() V47() V48() V49() V50() Element of NAT
sqrt 1 is V11() real ext-real Element of REAL
exp_R is V16() V19( REAL ) V20( REAL ) V21() V30( REAL , REAL ) V35() V36() V37() Element of K6(K7(REAL,REAL))
exp_R 0 is V11() real ext-real Element of REAL
- 1 is V11() real ext-real non positive set
2 is V1() ordinal natural V11() real ext-real positive non negative V33() V34() V45() V46() V47() V48() V49() V50() Element of NAT
sinh is V16() V19( REAL ) V20( REAL ) V21() V30( REAL , REAL ) V35() V36() V37() Element of K6(K7(REAL,REAL))
cosh is V16() V19( REAL ) V20( REAL ) V21() V30( REAL , REAL ) V35() V36() V37() Element of K6(K7(REAL,REAL))
tanh is V16() V19( REAL ) V20( REAL ) V21() V30( REAL , REAL ) V35() V36() V37() Element of K6(K7(REAL,REAL))
cosh . 0 is V11() real ext-real Element of REAL
sinh . 0 is V11() real ext-real Element of REAL
K52(1,2) is V11() real ext-real non negative Element of REAL
3 is V1() ordinal natural V11() real ext-real positive non negative V33() V34() V45() V46() V47() V48() V49() V50() Element of NAT
4 is V1() ordinal natural V11() real ext-real positive non negative V33() V34() V45() V46() V47() V48() V49() V50() Element of NAT
cosh 0 is V11() real ext-real Element of REAL
sinh 0 is V11() real ext-real Element of REAL
y is V11() real ext-real set
cosh y is V11() real ext-real Element of REAL
cosh . y is V11() real ext-real Element of REAL
y is V11() real ext-real set
sinh y is V11() real ext-real Element of REAL
exp_R y is V11() real ext-real set
- y is V11() real ext-real set
exp_R (- y) is V11() real ext-real set
(exp_R y) - (exp_R (- y)) is V11() real ext-real set
((exp_R y) - (exp_R (- y))) / 2 is V11() real ext-real set
cosh y is V11() real ext-real Element of REAL
(exp_R y) + (exp_R (- y)) is V11() real ext-real set
((exp_R y) + (exp_R (- y))) / 2 is V11() real ext-real set
tanh y is V11() real ext-real Element of REAL
((exp_R y) - (exp_R (- y))) / ((exp_R y) + (exp_R (- y))) is V11() real ext-real set
sinh . y is V11() real ext-real Element of REAL
exp_R . y is V11() real ext-real Element of REAL
exp_R . (- y) is V11() real ext-real Element of REAL
(exp_R . y) - (exp_R . (- y)) is V11() real ext-real set
((exp_R . y) - (exp_R . (- y))) / 2 is V11() real ext-real set
(exp_R y) - (exp_R . (- y)) is V11() real ext-real set
((exp_R y) - (exp_R . (- y))) / 2 is V11() real ext-real set
cosh . y is V11() real ext-real Element of REAL
(exp_R . y) + (exp_R . (- y)) is V11() real ext-real set
((exp_R . y) + (exp_R . (- y))) / 2 is V11() real ext-real set
(exp_R y) + (exp_R . (- y)) is V11() real ext-real set
((exp_R y) + (exp_R . (- y))) / 2 is V11() real ext-real set
tanh . y is V11() real ext-real Element of REAL
(sinh . y) / (cosh . y) is V11() real ext-real set
(sinh y) / (cosh . y) is V11() real ext-real set
(((exp_R y) - (exp_R (- y))) / 2) / (((exp_R y) + (exp_R (- y))) / 2) is V11() real ext-real set
y is V11() real ext-real set
cosh y is V11() real ext-real Element of REAL
(cosh y) ^2 is V11() real ext-real Element of REAL
(cosh y) * (cosh y) is V11() real ext-real set
sinh y is V11() real ext-real Element of REAL
(sinh y) ^2 is V11() real ext-real Element of REAL
(sinh y) * (sinh y) is V11() real ext-real set
((cosh y) ^2) - ((sinh y) ^2) is V11() real ext-real set
((cosh y) * (cosh y)) - ((sinh y) * (sinh y)) is V11() real ext-real set
sinh . y is V11() real ext-real Element of REAL
(sinh . y) ^2 is V11() real ext-real Element of REAL
(sinh . y) * (sinh . y) is V11() real ext-real set
((cosh y) ^2) - ((sinh . y) ^2) is V11() real ext-real set
cosh . y is V11() real ext-real Element of REAL
(cosh . y) ^2 is V11() real ext-real Element of REAL
(cosh . y) * (cosh . y) is V11() real ext-real set
((cosh . y) ^2) - ((sinh . y) ^2) is V11() real ext-real set
tanh 0 is V11() real ext-real Element of REAL
y is V11() real ext-real set
tanh y is V11() real ext-real Element of REAL
sinh y is V11() real ext-real Element of REAL
cosh y is V11() real ext-real Element of REAL
(sinh y) / (cosh y) is V11() real ext-real set
tanh . 0 is V11() real ext-real Element of REAL
(sinh . 0) / (cosh . 0) is V11() real ext-real set
tanh . y is V11() real ext-real Element of REAL
sinh . y is V11() real ext-real Element of REAL
cosh . y is V11() real ext-real Element of REAL
(sinh . y) / (cosh . y) is V11() real ext-real set
(sinh y) / (cosh . y) is V11() real ext-real set
y is V11() real ext-real set
sinh y is V11() real ext-real Element of REAL
tanh y is V11() real ext-real Element of REAL
exp_R y is V11() real ext-real set
1 / (exp_R y) is V11() real ext-real set
- y is V11() real ext-real set
exp_R (- y) is V11() real ext-real set
(exp_R y) - (exp_R (- y)) is V11() real ext-real set
((exp_R y) - (exp_R (- y))) / 2 is V11() real ext-real set
cosh y is V11() real ext-real Element of REAL
(sinh y) / (cosh y) is V11() real ext-real set
y is V11() real ext-real set
y / 2 is V11() real ext-real set
z is V11() real ext-real set
y - z is V11() real ext-real set
z / 2 is V11() real ext-real set
(y / 2) - (z / 2) is V11() real ext-real set
sinh ((y / 2) - (z / 2)) is V11() real ext-real Element of REAL
(y - z) / 2 is V11() real ext-real set
y is V11() real ext-real set
y / 2 is V11() real ext-real set
z is V11() real ext-real set
y + z is V11() real ext-real set
z / 2 is V11() real ext-real set
(y / 2) + (z / 2) is V11() real ext-real set
sinh ((y / 2) + (z / 2)) is V11() real ext-real Element of REAL
(y + z) / 2 is V11() real ext-real set
1 / 2 is V11() real ext-real non negative set
y is V11() real ext-real set
sinh y is V11() real ext-real Element of REAL
(sinh y) ^2 is V11() real ext-real Element of REAL
(sinh y) * (sinh y) is V11() real ext-real set
2 * y is V11() real ext-real set
cosh (2 * y) is V11() real ext-real Element of REAL
(cosh (2 * y)) - 1 is V11() real ext-real set
(1 / 2) * ((cosh (2 * y)) - 1) is V11() real ext-real set
cosh y is V11() real ext-real Element of REAL
(cosh y) ^2 is V11() real ext-real Element of REAL
(cosh y) * (cosh y) is V11() real ext-real set
(cosh (2 * y)) + 1 is V11() real ext-real set
(1 / 2) * ((cosh (2 * y)) + 1) is V11() real ext-real set
cosh . y is V11() real ext-real Element of REAL
(cosh . y) ^2 is V11() real ext-real Element of REAL
(cosh . y) * (cosh . y) is V11() real ext-real set
cosh . (2 * y) is V11() real ext-real Element of REAL
(cosh . (2 * y)) + 1 is V11() real ext-real set
(1 / 2) * ((cosh . (2 * y)) + 1) is V11() real ext-real set
sinh . y is V11() real ext-real Element of REAL
(sinh . y) ^2 is V11() real ext-real Element of REAL
(sinh . y) * (sinh . y) is V11() real ext-real set
(cosh . (2 * y)) - 1 is V11() real ext-real set
(1 / 2) * ((cosh . (2 * y)) - 1) is V11() real ext-real set
y is V11() real ext-real set
- y is V11() real ext-real set
sinh (- y) is V11() real ext-real Element of REAL
sinh y is V11() real ext-real Element of REAL
- (sinh y) is V11() real ext-real set
cosh (- y) is V11() real ext-real Element of REAL
cosh y is V11() real ext-real Element of REAL
tanh (- y) is V11() real ext-real Element of REAL
tanh y is V11() real ext-real Element of REAL
- (tanh y) is V11() real ext-real set
coth (- y) is V11() real ext-real Element of REAL
coth y is V11() real ext-real Element of REAL
- (coth y) is V11() real ext-real set
sech (- y) is V11() real ext-real Element of REAL
sech y is V11() real ext-real Element of REAL
cosech (- y) is V11() real ext-real Element of REAL
cosech y is V11() real ext-real Element of REAL
- (cosech y) is V11() real ext-real set
tanh . (- y) is V11() real ext-real Element of REAL
tanh . y is V11() real ext-real Element of REAL
- (tanh . y) is V11() real ext-real set
sinh . (- y) is V11() real ext-real Element of REAL
sinh . y is V11() real ext-real Element of REAL
- (sinh . y) is V11() real ext-real set
1 / (- (sinh y)) is V11() real ext-real set
1 / (sinh y) is V11() real ext-real set
- (1 / (sinh y)) is V11() real ext-real set
cosh . (- y) is V11() real ext-real Element of REAL
cosh . y is V11() real ext-real Element of REAL
1 / (cosh y) is V11() real ext-real set
(cosh y) / (- (sinh y)) is V11() real ext-real set
(cosh y) / (sinh y) is V11() real ext-real set
- ((cosh y) / (sinh y)) is V11() real ext-real set
y is V11() real ext-real set
sinh y is V11() real ext-real Element of REAL
cosech y is V11() real ext-real Element of REAL
1 / (cosech y) is V11() real ext-real set
cosh y is V11() real ext-real Element of REAL
sech y is V11() real ext-real Element of REAL
1 / (sech y) is V11() real ext-real set
tanh y is V11() real ext-real Element of REAL
coth y is V11() real ext-real Element of REAL
1 / (coth y) is V11() real ext-real set
1 / (sinh y) is V11() real ext-real set
1 / (1 / (sinh y)) is V11() real ext-real set
1 / (cosh y) is V11() real ext-real set
1 / (1 / (cosh y)) is V11() real ext-real set
(sinh y) / (cosh y) is V11() real ext-real set
(cosh y) / (sinh y) is V11() real ext-real set
1 / ((cosh y) / (sinh y)) is V11() real ext-real set
y is V11() real ext-real set
exp_R y is V11() real ext-real set
- y is V11() real ext-real set
exp_R (- y) is V11() real ext-real set
(exp_R y) + (exp_R (- y)) is V11() real ext-real set
exp_R . y is V11() real ext-real Element of REAL
exp_R . (- y) is V11() real ext-real Element of REAL
(exp_R y) * (exp_R (- y)) is V11() real ext-real set
sqrt ((exp_R y) * (exp_R (- y))) is V11() real ext-real set
2 * (sqrt ((exp_R y) * (exp_R (- y)))) is V11() real ext-real set
(exp_R y) * (exp_R . (- y)) is V11() real ext-real set
sqrt ((exp_R y) * (exp_R . (- y))) is V11() real ext-real set
2 * (sqrt ((exp_R y) * (exp_R . (- y)))) is V11() real ext-real set
(exp_R . y) * (exp_R . (- y)) is V11() real ext-real set
sqrt ((exp_R . y) * (exp_R . (- y))) is V11() real ext-real set
2 * (sqrt ((exp_R . y) * (exp_R . (- y)))) is V11() real ext-real set
y + (- y) is V11() real ext-real set
exp_R . (y + (- y)) is V11() real ext-real Element of REAL
sqrt (exp_R . (y + (- y))) is V11() real ext-real Element of REAL
2 * (sqrt (exp_R . (y + (- y)))) is V11() real ext-real set
2 * 1 is ordinal natural V11() real ext-real non negative set
sech 0 is V11() real ext-real Element of REAL
y is V11() real ext-real set
sech y is V11() real ext-real Element of REAL
exp_R y is V11() real ext-real set
- y is V11() real ext-real set
exp_R (- y) is V11() real ext-real set
(exp_R y) + (exp_R (- y)) is V11() real ext-real set
2 / ((exp_R y) + (exp_R (- y))) is V11() real ext-real set
2 / 2 is V11() real ext-real non negative set
cosh . y is V11() real ext-real Element of REAL
cosh y is V11() real ext-real Element of REAL
1 / (cosh y) is V11() real ext-real set
1 / 1 is V11() real ext-real non negative set
y is V11() real ext-real set
tanh y is V11() real ext-real Element of REAL
cosh y is V11() real ext-real Element of REAL
sinh y is V11() real ext-real Element of REAL
(sinh y) / (cosh y) is V11() real ext-real set
y is V11() real ext-real set
cosh y is V11() real ext-real Element of REAL
tanh y is V11() real ext-real Element of REAL
(tanh y) ^2 is V11() real ext-real Element of REAL
(tanh y) * (tanh y) is V11() real ext-real set
1 - ((tanh y) ^2) is V11() real ext-real set
sqrt (1 - ((tanh y) ^2)) is V11() real ext-real set
1 / (sqrt (1 - ((tanh y) ^2))) is V11() real ext-real set
sinh y is V11() real ext-real Element of REAL
(tanh y) / (sqrt (1 - ((tanh y) ^2))) is V11() real ext-real set
sech y is V11() real ext-real Element of REAL
(sech y) ^2 is V11() real ext-real Element of REAL
(sech y) * (sech y) is V11() real ext-real set
((sech y) ^2) + ((tanh y) ^2) is V11() real ext-real set
(((sech y) ^2) + ((tanh y) ^2)) - ((tanh y) ^2) is V11() real ext-real set
1 / (cosh y) is V11() real ext-real set
1 / (1 / (cosh y)) is V11() real ext-real set
1 / (sech y) is V11() real ext-real set
(sinh y) / (cosh y) is V11() real ext-real set
((sinh y) / (cosh y)) * (cosh y) is V11() real ext-real set
(tanh y) * (1 / (sqrt (1 - ((tanh y) ^2)))) is V11() real ext-real set
y is V11() real ext-real set
cosh y is V11() real ext-real Element of REAL
sinh y is V11() real ext-real Element of REAL
(cosh y) + (sinh y) is V11() real ext-real set
(cosh y) - (sinh y) is V11() real ext-real set
z is ordinal natural V11() real ext-real non negative V33() V34() V45() V46() V47() V48() V49() V50() Element of NAT
((cosh y) + (sinh y)) |^ z is set
z * y is V11() real ext-real set
cosh (z * y) is V11() real ext-real Element of REAL
sinh (z * y) is V11() real ext-real Element of REAL
(cosh (z * y)) + (sinh (z * y)) is V11() real ext-real set
((cosh y) - (sinh y)) |^ z is set
(cosh (z * y)) - (sinh (z * y)) is V11() real ext-real set
cosh . y is V11() real ext-real Element of REAL
(cosh . y) + (sinh y) is V11() real ext-real set
((cosh . y) + (sinh y)) |^ z is set
sinh . y is V11() real ext-real Element of REAL
(cosh . y) + (sinh . y) is V11() real ext-real set
((cosh . y) + (sinh . y)) |^ z is set
cosh . (z * y) is V11() real ext-real Element of REAL
sinh . (z * y) is V11() real ext-real Element of REAL
(cosh . (z * y)) + (sinh . (z * y)) is V11() real ext-real set
(cosh (z * y)) + (sinh . (z * y)) is V11() real ext-real set
- (sinh y) is V11() real ext-real set
(cosh y) + (- (sinh y)) is V11() real ext-real set
((cosh y) + (- (sinh y))) |^ z is set
- y is V11() real ext-real set
sinh (- y) is V11() real ext-real Element of REAL
(cosh y) + (sinh (- y)) is V11() real ext-real set
((cosh y) + (sinh (- y))) |^ z is set
(cosh . y) + (sinh (- y)) is V11() real ext-real set
((cosh . y) + (sinh (- y))) |^ z is set
sinh . (- y) is V11() real ext-real Element of REAL
(cosh . y) + (sinh . (- y)) is V11() real ext-real set
((cosh . y) + (sinh . (- y))) |^ z is set
cosh . (- y) is V11() real ext-real Element of REAL
(cosh . (- y)) + (sinh . (- y)) is V11() real ext-real set
((cosh . (- y)) + (sinh . (- y))) |^ z is set
z * (- y) is V11() real ext-real set
cosh . (z * (- y)) is V11() real ext-real Element of REAL
- (z * y) is V11() real ext-real set
sinh . (- (z * y)) is V11() real ext-real Element of REAL
(cosh . (z * (- y))) + (sinh . (- (z * y))) is V11() real ext-real set
(cosh . (z * y)) + (sinh . (- (z * y))) is V11() real ext-real set
- (sinh . (z * y)) is V11() real ext-real set
(cosh . (z * y)) + (- (sinh . (z * y))) is V11() real ext-real set
(cosh . (z * y)) - (sinh . (z * y)) is V11() real ext-real set
(cosh (z * y)) - (sinh . (z * y)) is V11() real ext-real set
y is V11() real ext-real set
exp_R y is V11() real ext-real set
cosh y is V11() real ext-real Element of REAL
sinh y is V11() real ext-real Element of REAL
(cosh y) + (sinh y) is V11() real ext-real set
- y is V11() real ext-real set
exp_R (- y) is V11() real ext-real set
(cosh y) - (sinh y) is V11() real ext-real set
y / 2 is V11() real ext-real set
cosh (y / 2) is V11() real ext-real Element of REAL
sinh (y / 2) is V11() real ext-real Element of REAL
(cosh (y / 2)) + (sinh (y / 2)) is V11() real ext-real set
(cosh (y / 2)) - (sinh (y / 2)) is V11() real ext-real set
((cosh (y / 2)) + (sinh (y / 2))) / ((cosh (y / 2)) - (sinh (y / 2))) is V11() real ext-real set
((cosh (y / 2)) - (sinh (y / 2))) / ((cosh (y / 2)) + (sinh (y / 2))) is V11() real ext-real set
tanh (y / 2) is V11() real ext-real Element of REAL
1 + (tanh (y / 2)) is V11() real ext-real set
1 - (tanh (y / 2)) is V11() real ext-real set
(1 + (tanh (y / 2))) / (1 - (tanh (y / 2))) is V11() real ext-real set
(1 - (tanh (y / 2))) / (1 + (tanh (y / 2))) is V11() real ext-real set
exp_R (y / 2) is V11() real ext-real set
- (y / 2) is V11() real ext-real set
(- (y / 2)) + (- (y / 2)) is V11() real ext-real set
exp_R ((- (y / 2)) + (- (y / 2))) is V11() real ext-real set
exp_R (- (y / 2)) is V11() real ext-real set
(exp_R (- (y / 2))) * (exp_R (- (y / 2))) is V11() real ext-real set
(exp_R (- (y / 2))) * (exp_R (y / 2)) is V11() real ext-real set
(exp_R (- (y / 2))) / (exp_R (y / 2)) is V11() real ext-real set
((exp_R (- (y / 2))) * (exp_R (y / 2))) * ((exp_R (- (y / 2))) / (exp_R (y / 2))) is V11() real ext-real set
(- (y / 2)) + (y / 2) is V11() real ext-real set
exp_R ((- (y / 2)) + (y / 2)) is V11() real ext-real set
(exp_R ((- (y / 2)) + (y / 2))) * ((exp_R (- (y / 2))) / (exp_R (y / 2))) is V11() real ext-real set
(exp_R (y / 2)) + (exp_R (- (y / 2))) is V11() real ext-real set
((exp_R (y / 2)) + (exp_R (- (y / 2)))) / 2 is V11() real ext-real set
(exp_R (y / 2)) - (exp_R (- (y / 2))) is V11() real ext-real set
((exp_R (y / 2)) - (exp_R (- (y / 2)))) / 2 is V11() real ext-real set
(((exp_R (y / 2)) + (exp_R (- (y / 2)))) / 2) - (((exp_R (y / 2)) - (exp_R (- (y / 2)))) / 2) is V11() real ext-real set
((((exp_R (y / 2)) + (exp_R (- (y / 2)))) / 2) - (((exp_R (y / 2)) - (exp_R (- (y / 2)))) / 2)) / (exp_R (y / 2)) is V11() real ext-real set
(((exp_R (y / 2)) + (exp_R (- (y / 2)))) / 2) - (sinh (y / 2)) is V11() real ext-real set
((((exp_R (y / 2)) + (exp_R (- (y / 2)))) / 2) - (sinh (y / 2))) / (exp_R (y / 2)) is V11() real ext-real set
(exp_R (y / 2)) / 2 is V11() real ext-real set
(exp_R (- (y / 2))) / 2 is V11() real ext-real set
((exp_R (y / 2)) / 2) - ((exp_R (- (y / 2))) / 2) is V11() real ext-real set
(((exp_R (y / 2)) + (exp_R (- (y / 2)))) / 2) + (((exp_R (y / 2)) / 2) - ((exp_R (- (y / 2))) / 2)) is V11() real ext-real set
((cosh (y / 2)) - (sinh (y / 2))) / ((((exp_R (y / 2)) + (exp_R (- (y / 2)))) / 2) + (((exp_R (y / 2)) / 2) - ((exp_R (- (y / 2))) / 2))) is V11() real ext-real set
(cosh (y / 2)) + (((exp_R (y / 2)) - (exp_R (- (y / 2)))) / 2) is V11() real ext-real set
((cosh (y / 2)) - (sinh (y / 2))) / ((cosh (y / 2)) + (((exp_R (y / 2)) - (exp_R (- (y / 2)))) / 2)) is V11() real ext-real set
((cosh (y / 2)) - (sinh (y / 2))) / (cosh (y / 2)) is V11() real ext-real set
((cosh (y / 2)) + (sinh (y / 2))) / (cosh (y / 2)) is V11() real ext-real set
(((cosh (y / 2)) - (sinh (y / 2))) / (cosh (y / 2))) / (((cosh (y / 2)) + (sinh (y / 2))) / (cosh (y / 2))) is V11() real ext-real set
(cosh (y / 2)) / (cosh (y / 2)) is V11() real ext-real set
(sinh (y / 2)) / (cosh (y / 2)) is V11() real ext-real set
((cosh (y / 2)) / (cosh (y / 2))) - ((sinh (y / 2)) / (cosh (y / 2))) is V11() real ext-real set
(((cosh (y / 2)) / (cosh (y / 2))) - ((sinh (y / 2)) / (cosh (y / 2)))) / (((cosh (y / 2)) + (sinh (y / 2))) / (cosh (y / 2))) is V11() real ext-real set
1 - ((sinh (y / 2)) / (cosh (y / 2))) is V11() real ext-real set
(1 - ((sinh (y / 2)) / (cosh (y / 2)))) / (((cosh (y / 2)) + (sinh (y / 2))) / (cosh (y / 2))) is V11() real ext-real set
(1 - (tanh (y / 2))) / (((cosh (y / 2)) + (sinh (y / 2))) / (cosh (y / 2))) is V11() real ext-real set
((cosh (y / 2)) / (cosh (y / 2))) + ((sinh (y / 2)) / (cosh (y / 2))) is V11() real ext-real set
(1 - (tanh (y / 2))) / (((cosh (y / 2)) / (cosh (y / 2))) + ((sinh (y / 2)) / (cosh (y / 2)))) is V11() real ext-real set
1 + ((sinh (y / 2)) / (cosh (y / 2))) is V11() real ext-real set
(1 - (tanh (y / 2))) / (1 + ((sinh (y / 2)) / (cosh (y / 2)))) is V11() real ext-real set
(exp_R y) + (exp_R (- y)) is V11() real ext-real set
((exp_R y) + (exp_R (- y))) / 2 is V11() real ext-real set
(exp_R y) - (exp_R (- y)) is V11() real ext-real set
((exp_R y) - (exp_R (- y))) / 2 is V11() real ext-real set
(((exp_R y) + (exp_R (- y))) / 2) - (((exp_R y) - (exp_R (- y))) / 2) is V11() real ext-real set
(cosh y) - (((exp_R y) - (exp_R (- y))) / 2) is V11() real ext-real set
(((exp_R y) + (exp_R (- y))) / 2) + (((exp_R y) - (exp_R (- y))) / 2) is V11() real ext-real set
(cosh y) + (((exp_R y) - (exp_R (- y))) / 2) is V11() real ext-real set
(y / 2) + (y / 2) is V11() real ext-real set
exp_R ((y / 2) + (y / 2)) is V11() real ext-real set
(exp_R (y / 2)) * (exp_R (y / 2)) is V11() real ext-real set
(exp_R (y / 2)) * (exp_R (- (y / 2))) is V11() real ext-real set
(exp_R (y / 2)) / (exp_R (- (y / 2))) is V11() real ext-real set
((exp_R (y / 2)) * (exp_R (- (y / 2)))) * ((exp_R (y / 2)) / (exp_R (- (y / 2)))) is V11() real ext-real set
(y / 2) + (- (y / 2)) is V11() real ext-real set
exp_R ((y / 2) + (- (y / 2))) is V11() real ext-real set
(exp_R ((y / 2) + (- (y / 2)))) * ((exp_R (y / 2)) / (exp_R (- (y / 2)))) is V11() real ext-real set
(((exp_R (y / 2)) + (exp_R (- (y / 2)))) / 2) + (((exp_R (y / 2)) - (exp_R (- (y / 2)))) / 2) is V11() real ext-real set
((((exp_R (y / 2)) + (exp_R (- (y / 2)))) / 2) + (((exp_R (y / 2)) - (exp_R (- (y / 2)))) / 2)) / (exp_R (- (y / 2))) is V11() real ext-real set
((cosh (y / 2)) + (((exp_R (y / 2)) - (exp_R (- (y / 2)))) / 2)) / (exp_R (- (y / 2))) is V11() real ext-real set
(exp_R (- (y / 2))) + (exp_R (y / 2)) is V11() real ext-real set
((exp_R (- (y / 2))) + (exp_R (y / 2))) / 2 is V11() real ext-real set
(((exp_R (- (y / 2))) + (exp_R (y / 2))) / 2) - (((exp_R (y / 2)) - (exp_R (- (y / 2)))) / 2) is V11() real ext-real set
((cosh (y / 2)) + (sinh (y / 2))) / ((((exp_R (- (y / 2))) + (exp_R (y / 2))) / 2) - (((exp_R (y / 2)) - (exp_R (- (y / 2)))) / 2)) is V11() real ext-real set
((cosh (y / 2)) + (sinh (y / 2))) / ((((exp_R (y / 2)) + (exp_R (- (y / 2)))) / 2) - (sinh (y / 2))) is V11() real ext-real set
(((cosh (y / 2)) + (sinh (y / 2))) / (cosh (y / 2))) / (((cosh (y / 2)) - (sinh (y / 2))) / (cosh (y / 2))) is V11() real ext-real set
(((cosh (y / 2)) / (cosh (y / 2))) + ((sinh (y / 2)) / (cosh (y / 2)))) / (((cosh (y / 2)) - (sinh (y / 2))) / (cosh (y / 2))) is V11() real ext-real set
(1 + ((sinh (y / 2)) / (cosh (y / 2)))) / (((cosh (y / 2)) - (sinh (y / 2))) / (cosh (y / 2))) is V11() real ext-real set
(1 + (tanh (y / 2))) / (((cosh (y / 2)) - (sinh (y / 2))) / (cosh (y / 2))) is V11() real ext-real set
(1 + (tanh (y / 2))) / (((cosh (y / 2)) / (cosh (y / 2))) - ((sinh (y / 2)) / (cosh (y / 2)))) is V11() real ext-real set
(1 + (tanh (y / 2))) / (1 - ((sinh (y / 2)) / (cosh (y / 2)))) is V11() real ext-real set
y is V11() real ext-real set
exp_R y is V11() real ext-real set
y / 2 is V11() real ext-real set
coth (y / 2) is V11() real ext-real Element of REAL
(coth (y / 2)) + 1 is V11() real ext-real set
(coth (y / 2)) - 1 is V11() real ext-real set
((coth (y / 2)) + 1) / ((coth (y / 2)) - 1) is V11() real ext-real set
- y is V11() real ext-real set
exp_R (- y) is V11() real ext-real set
((coth (y / 2)) - 1) / ((coth (y / 2)) + 1) is V11() real ext-real set
1 / (coth (y / 2)) is V11() real ext-real set
1 / (1 / (coth (y / 2))) is V11() real ext-real set
(1 / (1 / (coth (y / 2)))) - 1 is V11() real ext-real set
tanh (y / 2) is V11() real ext-real Element of REAL
1 / (tanh (y / 2)) is V11() real ext-real set
(1 / (tanh (y / 2))) - 1 is V11() real ext-real set
(tanh (y / 2)) / (tanh (y / 2)) is V11() real ext-real set
(1 / (tanh (y / 2))) - ((tanh (y / 2)) / (tanh (y / 2))) is V11() real ext-real set
1 - (tanh (y / 2)) is V11() real ext-real set
(1 - (tanh (y / 2))) / (tanh (y / 2)) is V11() real ext-real set
(1 / (1 / (coth (y / 2)))) + 1 is V11() real ext-real set
(1 / (tanh (y / 2))) + 1 is V11() real ext-real set
(1 / (tanh (y / 2))) + ((tanh (y / 2)) / (tanh (y / 2))) is V11() real ext-real set
1 + (tanh (y / 2)) is V11() real ext-real set
(1 + (tanh (y / 2))) / (tanh (y / 2)) is V11() real ext-real set
(1 - (tanh (y / 2))) / (1 + (tanh (y / 2))) is V11() real ext-real set
(1 + (tanh (y / 2))) / (1 - (tanh (y / 2))) is V11() real ext-real set
y is V11() real ext-real set
cosh y is V11() real ext-real Element of REAL
sinh y is V11() real ext-real Element of REAL
(cosh y) + (sinh y) is V11() real ext-real set
(cosh y) - (sinh y) is V11() real ext-real set
((cosh y) + (sinh y)) / ((cosh y) - (sinh y)) is V11() real ext-real set
tanh y is V11() real ext-real Element of REAL
1 + (tanh y) is V11() real ext-real set
1 - (tanh y) is V11() real ext-real set
(1 + (tanh y)) / (1 - (tanh y)) is V11() real ext-real set
2 * y is V11() real ext-real set
exp_R (2 * y) is V11() real ext-real set
(2 * y) / 2 is V11() real ext-real set
tanh ((2 * y) / 2) is V11() real ext-real Element of REAL
1 - (tanh ((2 * y) / 2)) is V11() real ext-real set
(1 + (tanh y)) / (1 - (tanh ((2 * y) / 2))) is V11() real ext-real set
cosh ((2 * y) / 2) is V11() real ext-real Element of REAL
sinh ((2 * y) / 2) is V11() real ext-real Element of REAL
(cosh ((2 * y) / 2)) + (sinh ((2 * y) / 2)) is V11() real ext-real set
(cosh ((2 * y) / 2)) - (sinh ((2 * y) / 2)) is V11() real ext-real set
((cosh ((2 * y) / 2)) + (sinh ((2 * y) / 2))) / ((cosh ((2 * y) / 2)) - (sinh ((2 * y) / 2))) is V11() real ext-real set
y is V11() real ext-real set
cosh y is V11() real ext-real Element of REAL
sinh y is V11() real ext-real Element of REAL
tanh y is V11() real ext-real Element of REAL
z is V11() real ext-real set
y + z is V11() real ext-real set
cosh (y + z) is V11() real ext-real Element of REAL
cosh z is V11() real ext-real Element of REAL
(cosh y) * (cosh z) is V11() real ext-real set
sinh z is V11() real ext-real Element of REAL
(sinh y) * (sinh z) is V11() real ext-real set
((cosh y) * (cosh z)) + ((sinh y) * (sinh z)) is V11() real ext-real set
y - z is V11() real ext-real set
cosh (y - z) is V11() real ext-real Element of REAL
((cosh y) * (cosh z)) - ((sinh y) * (sinh z)) is V11() real ext-real set
sinh (y + z) is V11() real ext-real Element of REAL
(sinh y) * (cosh z) is V11() real ext-real set
(cosh y) * (sinh z) is V11() real ext-real set
((sinh y) * (cosh z)) + ((cosh y) * (sinh z)) is V11() real ext-real set
sinh (y - z) is V11() real ext-real Element of REAL
((sinh y) * (cosh z)) - ((cosh y) * (sinh z)) is V11() real ext-real set
tanh (y + z) is V11() real ext-real Element of REAL
tanh z is V11() real ext-real Element of REAL
(tanh y) + (tanh z) is V11() real ext-real set
(tanh y) * (tanh z) is V11() real ext-real set
1 + ((tanh y) * (tanh z)) is V11() real ext-real set
((tanh y) + (tanh z)) / (1 + ((tanh y) * (tanh z))) is V11() real ext-real set
tanh (y - z) is V11() real ext-real Element of REAL
(tanh y) - (tanh z) is V11() real ext-real set
1 - ((tanh y) * (tanh z)) is V11() real ext-real set
((tanh y) - (tanh z)) / (1 - ((tanh y) * (tanh z))) is V11() real ext-real set
cosh . y is V11() real ext-real Element of REAL
(cosh . y) * (cosh z) is V11() real ext-real set
((cosh . y) * (cosh z)) - ((sinh y) * (sinh z)) is V11() real ext-real set
cosh . z is V11() real ext-real Element of REAL
(cosh . y) * (cosh . z) is V11() real ext-real set
((cosh . y) * (cosh . z)) - ((sinh y) * (sinh z)) is V11() real ext-real set
sinh . y is V11() real ext-real Element of REAL
(sinh . y) * (sinh z) is V11() real ext-real set
((cosh . y) * (cosh . z)) - ((sinh . y) * (sinh z)) is V11() real ext-real set
sinh . z is V11() real ext-real Element of REAL
(sinh . y) * (sinh . z) is V11() real ext-real set
((cosh . y) * (cosh . z)) - ((sinh . y) * (sinh . z)) is V11() real ext-real set
cosh . (y - z) is V11() real ext-real Element of REAL
(sinh . y) * (cosh z) is V11() real ext-real set
((sinh . y) * (cosh z)) + ((cosh y) * (sinh z)) is V11() real ext-real set
(cosh y) * (sinh . z) is V11() real ext-real set
((sinh . y) * (cosh z)) + ((cosh y) * (sinh . z)) is V11() real ext-real set
(sinh . y) * (cosh . z) is V11() real ext-real set
((sinh . y) * (cosh . z)) + ((cosh y) * (sinh . z)) is V11() real ext-real set
(cosh . y) * (sinh . z) is V11() real ext-real set
((sinh . y) * (cosh . z)) + ((cosh . y) * (sinh . z)) is V11() real ext-real set
sinh . (y + z) is V11() real ext-real Element of REAL
tanh . (y - z) is V11() real ext-real Element of REAL
tanh . y is V11() real ext-real Element of REAL
tanh . z is V11() real ext-real Element of REAL
(tanh . y) - (tanh . z) is V11() real ext-real set
(tanh . y) * (tanh . z) is V11() real ext-real set
1 - ((tanh . y) * (tanh . z)) is V11() real ext-real set
((tanh . y) - (tanh . z)) / (1 - ((tanh . y) * (tanh . z))) is V11() real ext-real set
(tanh y) - (tanh . z) is V11() real ext-real set
((tanh y) - (tanh . z)) / (1 - ((tanh . y) * (tanh . z))) is V11() real ext-real set
((tanh y) - (tanh z)) / (1 - ((tanh . y) * (tanh . z))) is V11() real ext-real set
(tanh y) * (tanh . z) is V11() real ext-real set
1 - ((tanh y) * (tanh . z)) is V11() real ext-real set
((tanh y) - (tanh z)) / (1 - ((tanh y) * (tanh . z))) is V11() real ext-real set
tanh . (y + z) is V11() real ext-real Element of REAL
(tanh . y) + (tanh . z) is V11() real ext-real set
1 + ((tanh . y) * (tanh . z)) is V11() real ext-real set
((tanh . y) + (tanh . z)) / (1 + ((tanh . y) * (tanh . z))) is V11() real ext-real set
(tanh y) + (tanh . z) is V11() real ext-real set
((tanh y) + (tanh . z)) / (1 + ((tanh . y) * (tanh . z))) is V11() real ext-real set
((tanh y) + (tanh z)) / (1 + ((tanh . y) * (tanh . z))) is V11() real ext-real set
1 + ((tanh y) * (tanh . z)) is V11() real ext-real set
((tanh y) + (tanh z)) / (1 + ((tanh y) * (tanh . z))) is V11() real ext-real set
((sinh . y) * (cosh z)) - ((cosh y) * (sinh z)) is V11() real ext-real set
((sinh . y) * (cosh z)) - ((cosh y) * (sinh . z)) is V11() real ext-real set
((sinh . y) * (cosh . z)) - ((cosh y) * (sinh . z)) is V11() real ext-real set
((sinh . y) * (cosh . z)) - ((cosh . y) * (sinh . z)) is V11() real ext-real set
sinh . (y - z) is V11() real ext-real Element of REAL
((cosh . y) * (cosh z)) + ((sinh y) * (sinh z)) is V11() real ext-real set
((cosh . y) * (cosh . z)) + ((sinh y) * (sinh z)) is V11() real ext-real set
((cosh . y) * (cosh . z)) + ((sinh . y) * (sinh z)) is V11() real ext-real set
((cosh . y) * (cosh . z)) + ((sinh . y) * (sinh . z)) is V11() real ext-real set
cosh . (y + z) is V11() real ext-real Element of REAL
y is V11() real ext-real set
coth y is V11() real ext-real Element of REAL
sinh y is V11() real ext-real Element of REAL
z is V11() real ext-real set
tanh z is V11() real ext-real Element of REAL
(coth y) + (tanh z) is V11() real ext-real set
y + z is V11() real ext-real set
cosh (y + z) is V11() real ext-real Element of REAL
cosh z is V11() real ext-real Element of REAL
(sinh y) * (cosh z) is V11() real ext-real set
(cosh (y + z)) / ((sinh y) * (cosh z)) is V11() real ext-real set
(coth y) - (tanh z) is V11() real ext-real set
y - z is V11() real ext-real set
cosh (y - z) is V11() real ext-real Element of REAL
(cosh (y - z)) / ((sinh y) * (cosh z)) is V11() real ext-real set
cosh y is V11() real ext-real Element of REAL
(cosh y) / (sinh y) is V11() real ext-real set
((cosh y) / (sinh y)) - (tanh z) is V11() real ext-real set
(cosh y) * (cosh z) is V11() real ext-real set
((cosh y) * (cosh z)) / ((sinh y) * (cosh z)) is V11() real ext-real set
(((cosh y) * (cosh z)) / ((sinh y) * (cosh z))) - (tanh z) is V11() real ext-real set
sinh z is V11() real ext-real Element of REAL
(sinh z) / (cosh z) is V11() real ext-real set
(((cosh y) * (cosh z)) / ((sinh y) * (cosh z))) - ((sinh z) / (cosh z)) is V11() real ext-real set
(sinh y) * (sinh z) is V11() real ext-real set
((sinh y) * (sinh z)) / ((sinh y) * (cosh z)) is V11() real ext-real set
(((cosh y) * (cosh z)) / ((sinh y) * (cosh z))) - (((sinh y) * (sinh z)) / ((sinh y) * (cosh z))) is V11() real ext-real set
((cosh y) * (cosh z)) - ((sinh y) * (sinh z)) is V11() real ext-real set
(((cosh y) * (cosh z)) - ((sinh y) * (sinh z))) / ((sinh y) * (cosh z)) is V11() real ext-real set
((cosh y) / (sinh y)) + (tanh z) is V11() real ext-real set
(((cosh y) * (cosh z)) / ((sinh y) * (cosh z))) + (tanh z) is V11() real ext-real set
(((cosh y) * (cosh z)) / ((sinh y) * (cosh z))) + ((sinh z) / (cosh z)) is V11() real ext-real set
(((cosh y) * (cosh z)) / ((sinh y) * (cosh z))) + (((sinh y) * (sinh z)) / ((sinh y) * (cosh z))) is V11() real ext-real set
((cosh y) * (cosh z)) + ((sinh y) * (sinh z)) is V11() real ext-real set
(((cosh y) * (cosh z)) + ((sinh y) * (sinh z))) / ((sinh y) * (cosh z)) is V11() real ext-real set
y is V11() real ext-real set
sinh y is V11() real ext-real Element of REAL
cosh y is V11() real ext-real Element of REAL
z is V11() real ext-real set
sinh z is V11() real ext-real Element of REAL
(sinh y) * (sinh z) is V11() real ext-real set
y + z is V11() real ext-real set
cosh (y + z) is V11() real ext-real Element of REAL
y - z is V11() real ext-real set
cosh (y - z) is V11() real ext-real Element of REAL
(cosh (y + z)) - (cosh (y - z)) is V11() real ext-real set
(1 / 2) * ((cosh (y + z)) - (cosh (y - z))) is V11() real ext-real set
cosh z is V11() real ext-real Element of REAL
(sinh y) * (cosh z) is V11() real ext-real set
sinh (y + z) is V11() real ext-real Element of REAL
sinh (y - z) is V11() real ext-real Element of REAL
(sinh (y + z)) + (sinh (y - z)) is V11() real ext-real set
(1 / 2) * ((sinh (y + z)) + (sinh (y - z))) is V11() real ext-real set
(cosh y) * (sinh z) is V11() real ext-real set
(sinh (y + z)) - (sinh (y - z)) is V11() real ext-real set
(1 / 2) * ((sinh (y + z)) - (sinh (y - z))) is V11() real ext-real set
(cosh y) * (cosh z) is V11() real ext-real set
(cosh (y + z)) + (cosh (y - z)) is V11() real ext-real set
(1 / 2) * ((cosh (y + z)) + (cosh (y - z))) is V11() real ext-real set
((sinh y) * (cosh z)) + ((cosh y) * (sinh z)) is V11() real ext-real set
((sinh y) * (cosh z)) - ((cosh y) * (sinh z)) is V11() real ext-real set
(((sinh y) * (cosh z)) + ((cosh y) * (sinh z))) + (((sinh y) * (cosh z)) - ((cosh y) * (sinh z))) is V11() real ext-real set
(1 / 2) * ((((sinh y) * (cosh z)) + ((cosh y) * (sinh z))) + (((sinh y) * (cosh z)) - ((cosh y) * (sinh z)))) is V11() real ext-real set
(sinh (y + z)) + (((sinh y) * (cosh z)) - ((cosh y) * (sinh z))) is V11() real ext-real set
(1 / 2) * ((sinh (y + z)) + (((sinh y) * (cosh z)) - ((cosh y) * (sinh z)))) is V11() real ext-real set
(((sinh y) * (cosh z)) + ((cosh y) * (sinh z))) - (((sinh y) * (cosh z)) - ((cosh y) * (sinh z))) is V11() real ext-real set
(1 / 2) * ((((sinh y) * (cosh z)) + ((cosh y) * (sinh z))) - (((sinh y) * (cosh z)) - ((cosh y) * (sinh z)))) is V11() real ext-real set
(sinh (y + z)) - (((sinh y) * (cosh z)) - ((cosh y) * (sinh z))) is V11() real ext-real set
(1 / 2) * ((sinh (y + z)) - (((sinh y) * (cosh z)) - ((cosh y) * (sinh z)))) is V11() real ext-real set
((cosh y) * (cosh z)) + ((sinh y) * (sinh z)) is V11() real ext-real set
((cosh y) * (cosh z)) - ((sinh y) * (sinh z)) is V11() real ext-real set
(((cosh y) * (cosh z)) + ((sinh y) * (sinh z))) + (((cosh y) * (cosh z)) - ((sinh y) * (sinh z))) is V11() real ext-real set
(1 / 2) * ((((cosh y) * (cosh z)) + ((sinh y) * (sinh z))) + (((cosh y) * (cosh z)) - ((sinh y) * (sinh z)))) is V11() real ext-real set
(cosh (y + z)) + (((cosh y) * (cosh z)) - ((sinh y) * (sinh z))) is V11() real ext-real set
(1 / 2) * ((cosh (y + z)) + (((cosh y) * (cosh z)) - ((sinh y) * (sinh z)))) is V11() real ext-real set
(((cosh y) * (cosh z)) + ((sinh y) * (sinh z))) - (((cosh y) * (cosh z)) - ((sinh y) * (sinh z))) is V11() real ext-real set
(1 / 2) * ((((cosh y) * (cosh z)) + ((sinh y) * (sinh z))) - (((cosh y) * (cosh z)) - ((sinh y) * (sinh z)))) is V11() real ext-real set
(cosh (y + z)) - (((cosh y) * (cosh z)) - ((sinh y) * (sinh z))) is V11() real ext-real set
(1 / 2) * ((cosh (y + z)) - (((cosh y) * (cosh z)) - ((sinh y) * (sinh z)))) is V11() real ext-real set
y is V11() real ext-real set
sinh y is V11() real ext-real Element of REAL
(sinh y) ^2 is V11() real ext-real Element of REAL
(sinh y) * (sinh y) is V11() real ext-real set
z is V11() real ext-real set
cosh z is V11() real ext-real Element of REAL
(cosh z) ^2 is V11() real ext-real Element of REAL
(cosh z) * (cosh z) is V11() real ext-real set
((sinh y) ^2) - ((cosh z) ^2) is V11() real ext-real set
y + z is V11() real ext-real set
sinh (y + z) is V11() real ext-real Element of REAL
y - z is V11() real ext-real set
sinh (y - z) is V11() real ext-real Element of REAL
(sinh (y + z)) * (sinh (y - z)) is V11() real ext-real set
((sinh (y + z)) * (sinh (y - z))) - 1 is V11() real ext-real set
((cosh z) ^2) * 1 is V11() real ext-real set
((sinh y) ^2) - (((cosh z) ^2) * 1) is V11() real ext-real set
cosh y is V11() real ext-real Element of REAL
(cosh y) ^2 is V11() real ext-real Element of REAL
(cosh y) * (cosh y) is V11() real ext-real set
((cosh y) ^2) - ((sinh y) ^2) is V11() real ext-real set
((cosh z) ^2) * (((cosh y) ^2) - ((sinh y) ^2)) is V11() real ext-real set
((sinh y) ^2) - (((cosh z) ^2) * (((cosh y) ^2) - ((sinh y) ^2))) is V11() real ext-real set
((cosh z) ^2) * ((sinh y) ^2) is V11() real ext-real set
sinh z is V11() real ext-real Element of REAL
(sinh z) ^2 is V11() real ext-real Element of REAL
(sinh z) * (sinh z) is V11() real ext-real set
((cosh z) ^2) - ((sinh z) ^2) is V11() real ext-real set
(((cosh z) ^2) - ((sinh z) ^2)) + ((sinh z) ^2) is V11() real ext-real set
((cosh y) ^2) * ((((cosh z) ^2) - ((sinh z) ^2)) + ((sinh z) ^2)) is V11() real ext-real set
(((cosh z) ^2) * ((sinh y) ^2)) - (((cosh y) ^2) * ((((cosh z) ^2) - ((sinh z) ^2)) + ((sinh z) ^2))) is V11() real ext-real set
((sinh y) ^2) + ((((cosh z) ^2) * ((sinh y) ^2)) - (((cosh y) ^2) * ((((cosh z) ^2) - ((sinh z) ^2)) + ((sinh z) ^2)))) is V11() real ext-real set
1 + ((sinh z) ^2) is V11() real ext-real set
((cosh y) ^2) * (1 + ((sinh z) ^2)) is V11() real ext-real set
(((cosh z) ^2) * ((sinh y) ^2)) - (((cosh y) ^2) * (1 + ((sinh z) ^2))) is V11() real ext-real set
((sinh y) ^2) + ((((cosh z) ^2) * ((sinh y) ^2)) - (((cosh y) ^2) * (1 + ((sinh z) ^2)))) is V11() real ext-real set
(sinh y) * (cosh z) is V11() real ext-real set
(cosh y) * (sinh z) is V11() real ext-real set
((sinh y) * (cosh z)) + ((cosh y) * (sinh z)) is V11() real ext-real set
((sinh y) * (cosh z)) - ((cosh y) * (sinh z)) is V11() real ext-real set
(((sinh y) * (cosh z)) + ((cosh y) * (sinh z))) * (((sinh y) * (cosh z)) - ((cosh y) * (sinh z))) is V11() real ext-real set
((((sinh y) * (cosh z)) + ((cosh y) * (sinh z))) * (((sinh y) * (cosh z)) - ((cosh y) * (sinh z)))) - ((cosh y) ^2) is V11() real ext-real set
((sinh y) ^2) + (((((sinh y) * (cosh z)) + ((cosh y) * (sinh z))) * (((sinh y) * (cosh z)) - ((cosh y) * (sinh z)))) - ((cosh y) ^2)) is V11() real ext-real set
(sinh (y + z)) * (((sinh y) * (cosh z)) - ((cosh y) * (sinh z))) is V11() real ext-real set
((sinh (y + z)) * (((sinh y) * (cosh z)) - ((cosh y) * (sinh z)))) - ((cosh y) ^2) is V11() real ext-real set
((sinh y) ^2) + (((sinh (y + z)) * (((sinh y) * (cosh z)) - ((cosh y) * (sinh z)))) - ((cosh y) ^2)) is V11() real ext-real set
((sinh (y + z)) * (sinh (y - z))) - ((cosh y) ^2) is V11() real ext-real set
(((sinh (y + z)) * (sinh (y - z))) - ((cosh y) ^2)) + ((sinh y) ^2) is V11() real ext-real set
((sinh (y + z)) * (sinh (y - z))) - (((cosh y) ^2) - ((sinh y) ^2)) is V11() real ext-real set
y is V11() real ext-real set
sinh y is V11() real ext-real Element of REAL
y / 2 is V11() real ext-real set
cosh y is V11() real ext-real Element of REAL
tanh y is V11() real ext-real Element of REAL
z is V11() real ext-real set
sinh z is V11() real ext-real Element of REAL
(sinh y) + (sinh z) is V11() real ext-real set
z / 2 is V11() real ext-real set
(y / 2) + (z / 2) is V11() real ext-real set
sinh ((y / 2) + (z / 2)) is V11() real ext-real Element of REAL
2 * (sinh ((y / 2) + (z / 2))) is V11() real ext-real set
(y / 2) - (z / 2) is V11() real ext-real set
cosh ((y / 2) - (z / 2)) is V11() real ext-real Element of REAL
(2 * (sinh ((y / 2) + (z / 2)))) * (cosh ((y / 2) - (z / 2))) is V11() real ext-real set
(sinh y) - (sinh z) is V11() real ext-real set
sinh ((y / 2) - (z / 2)) is V11() real ext-real Element of REAL
2 * (sinh ((y / 2) - (z / 2))) is V11() real ext-real set
cosh ((y / 2) + (z / 2)) is V11() real ext-real Element of REAL
(2 * (sinh ((y / 2) - (z / 2)))) * (cosh ((y / 2) + (z / 2))) is V11() real ext-real set
cosh z is V11() real ext-real Element of REAL
(cosh y) + (cosh z) is V11() real ext-real set
2 * (cosh ((y / 2) + (z / 2))) is V11() real ext-real set
(2 * (cosh ((y / 2) + (z / 2)))) * (cosh ((y / 2) - (z / 2))) is V11() real ext-real set
(cosh y) - (cosh z) is V11() real ext-real set
(2 * (sinh ((y / 2) - (z / 2)))) * (sinh ((y / 2) + (z / 2))) is V11() real ext-real set
tanh z is V11() real ext-real Element of REAL
(tanh y) + (tanh z) is V11() real ext-real set
y + z is V11() real ext-real set
sinh (y + z) is V11() real ext-real Element of REAL
(cosh y) * (cosh z) is V11() real ext-real set
(sinh (y + z)) / ((cosh y) * (cosh z)) is V11() real ext-real set
(tanh y) - (tanh z) is V11() real ext-real set
y - z is V11() real ext-real set
sinh (y - z) is V11() real ext-real Element of REAL
(sinh (y - z)) / ((cosh y) * (cosh z)) is V11() real ext-real set
sinh . ((y / 2) - (z / 2)) is V11() real ext-real Element of REAL
2 * (sinh . ((y / 2) - (z / 2))) is V11() real ext-real set
(2 * (sinh . ((y / 2) - (z / 2)))) * (cosh ((y / 2) + (z / 2))) is V11() real ext-real set
cosh . ((y / 2) + (z / 2)) is V11() real ext-real Element of REAL
(2 * (sinh . ((y / 2) - (z / 2)))) * (cosh . ((y / 2) + (z / 2))) is V11() real ext-real set
sinh . y is V11() real ext-real Element of REAL
sinh . z is V11() real ext-real Element of REAL
(sinh . y) - (sinh . z) is V11() real ext-real set
(sinh y) - (sinh . z) is V11() real ext-real set
2 * (cosh . ((y / 2) + (z / 2))) is V11() real ext-real set
(2 * (cosh . ((y / 2) + (z / 2)))) * (cosh ((y / 2) - (z / 2))) is V11() real ext-real set
cosh . ((y / 2) - (z / 2)) is V11() real ext-real Element of REAL
(2 * (cosh . ((y / 2) + (z / 2)))) * (cosh . ((y / 2) - (z / 2))) is V11() real ext-real set
cosh . y is V11() real ext-real Element of REAL
cosh . z is V11() real ext-real Element of REAL
(cosh . y) + (cosh . z) is V11() real ext-real set
(cosh y) + (cosh . z) is V11() real ext-real set
sinh . (y - z) is V11() real ext-real Element of REAL
(sinh . (y - z)) / ((cosh y) * (cosh z)) is V11() real ext-real set
(cosh . y) * (cosh z) is V11() real ext-real set
(sinh . (y - z)) / ((cosh . y) * (cosh z)) is V11() real ext-real set
(cosh . y) * (cosh . z) is V11() real ext-real set
(sinh . (y - z)) / ((cosh . y) * (cosh . z)) is V11() real ext-real set
tanh . y is V11() real ext-real Element of REAL
tanh . z is V11() real ext-real Element of REAL
(tanh . y) - (tanh . z) is V11() real ext-real set
(tanh y) - (tanh . z) is V11() real ext-real set
sinh . (y + z) is V11() real ext-real Element of REAL
(sinh . (y + z)) / ((cosh y) * (cosh z)) is V11() real ext-real set
(sinh . (y + z)) / ((cosh . y) * (cosh z)) is V11() real ext-real set
(sinh . (y + z)) / ((cosh . y) * (cosh . z)) is V11() real ext-real set
(tanh . y) + (tanh . z) is V11() real ext-real set
(tanh y) + (tanh . z) is V11() real ext-real set
(2 * (sinh . ((y / 2) - (z / 2)))) * (sinh ((y / 2) + (z / 2))) is V11() real ext-real set
sinh . ((y / 2) + (z / 2)) is V11() real ext-real Element of REAL
(2 * (sinh . ((y / 2) - (z / 2)))) * (sinh . ((y / 2) + (z / 2))) is V11() real ext-real set
(cosh . y) - (cosh . z) is V11() real ext-real set
(cosh y) - (cosh . z) is V11() real ext-real set
2 * (sinh . ((y / 2) + (z / 2))) is V11() real ext-real set
(2 * (sinh . ((y / 2) + (z / 2)))) * (cosh ((y / 2) - (z / 2))) is V11() real ext-real set
(2 * (sinh . ((y / 2) + (z / 2)))) * (cosh . ((y / 2) - (z / 2))) is V11() real ext-real set
(sinh . y) + (sinh . z) is V11() real ext-real set
(sinh y) + (sinh . z) is V11() real ext-real set
y is V11() real ext-real set
sinh y is V11() real ext-real Element of REAL
cosh y is V11() real ext-real Element of REAL
z is V11() real ext-real set
sinh z is V11() real ext-real Element of REAL
(sinh y) - (sinh z) is V11() real ext-real set
((sinh y) - (sinh z)) ^2 is V11() real ext-real set
((sinh y) - (sinh z)) * ((sinh y) - (sinh z)) is V11() real ext-real set
cosh z is V11() real ext-real Element of REAL
(cosh y) - (cosh z) is V11() real ext-real set
((cosh y) - (cosh z)) ^2 is V11() real ext-real set
((cosh y) - (cosh z)) * ((cosh y) - (cosh z)) is V11() real ext-real set
(((sinh y) - (sinh z)) ^2) - (((cosh y) - (cosh z)) ^2) is V11() real ext-real set
y - z is V11() real ext-real set
(y - z) / 2 is V11() real ext-real set
sinh ((y - z) / 2) is V11() real ext-real Element of REAL
(sinh ((y - z) / 2)) ^2 is V11() real ext-real Element of REAL
(sinh ((y - z) / 2)) * (sinh ((y - z) / 2)) is V11() real ext-real set
4 * ((sinh ((y - z) / 2)) ^2) is V11() real ext-real set
(cosh y) + (cosh z) is V11() real ext-real set
((cosh y) + (cosh z)) ^2 is V11() real ext-real set
((cosh y) + (cosh z)) * ((cosh y) + (cosh z)) is V11() real ext-real set
(sinh y) + (sinh z) is V11() real ext-real set
((sinh y) + (sinh z)) ^2 is V11() real ext-real set
((sinh y) + (sinh z)) * ((sinh y) + (sinh z)) is V11() real ext-real set
(((cosh y) + (cosh z)) ^2) - (((sinh y) + (sinh z)) ^2) is V11() real ext-real set
cosh ((y - z) / 2) is V11() real ext-real Element of REAL
(cosh ((y - z) / 2)) ^2 is V11() real ext-real Element of REAL
(cosh ((y - z) / 2)) * (cosh ((y - z) / 2)) is V11() real ext-real set
4 * ((cosh ((y - z) / 2)) ^2) is V11() real ext-real set
y / 2 is V11() real ext-real set
z / 2 is V11() real ext-real set
(y / 2) + (z / 2) is V11() real ext-real set
cosh ((y / 2) + (z / 2)) is V11() real ext-real Element of REAL
2 * (cosh ((y / 2) + (z / 2))) is V11() real ext-real set
(y / 2) - (z / 2) is V11() real ext-real set
cosh ((y / 2) - (z / 2)) is V11() real ext-real Element of REAL
(2 * (cosh ((y / 2) + (z / 2)))) * (cosh ((y / 2) - (z / 2))) is V11() real ext-real set
((2 * (cosh ((y / 2) + (z / 2)))) * (cosh ((y / 2) - (z / 2)))) ^2 is V11() real ext-real set
((2 * (cosh ((y / 2) + (z / 2)))) * (cosh ((y / 2) - (z / 2)))) * ((2 * (cosh ((y / 2) + (z / 2)))) * (cosh ((y / 2) - (z / 2)))) is V11() real ext-real set
(((2 * (cosh ((y / 2) + (z / 2)))) * (cosh ((y / 2) - (z / 2)))) ^2) - (((sinh y) + (sinh z)) ^2) is V11() real ext-real set
(cosh ((y / 2) + (z / 2))) * (cosh ((y / 2) - (z / 2))) is V11() real ext-real set
2 * ((cosh ((y / 2) + (z / 2))) * (cosh ((y / 2) - (z / 2)))) is V11() real ext-real set
(2 * ((cosh ((y / 2) + (z / 2))) * (cosh ((y / 2) - (z / 2))))) ^2 is V11() real ext-real set
(2 * ((cosh ((y / 2) + (z / 2))) * (cosh ((y / 2) - (z / 2))))) * (2 * ((cosh ((y / 2) + (z / 2))) * (cosh ((y / 2) - (z / 2))))) is V11() real ext-real set
sinh ((y / 2) + (z / 2)) is V11() real ext-real Element of REAL
2 * (sinh ((y / 2) + (z / 2))) is V11() real ext-real set
(2 * (sinh ((y / 2) + (z / 2)))) * (cosh ((y / 2) - (z / 2))) is V11() real ext-real set
((2 * (sinh ((y / 2) + (z / 2)))) * (cosh ((y / 2) - (z / 2)))) ^2 is V11() real ext-real set
((2 * (sinh ((y / 2) + (z / 2)))) * (cosh ((y / 2) - (z / 2)))) * ((2 * (sinh ((y / 2) + (z / 2)))) * (cosh ((y / 2) - (z / 2)))) is V11() real ext-real set
((2 * ((cosh ((y / 2) + (z / 2))) * (cosh ((y / 2) - (z / 2))))) ^2) - (((2 * (sinh ((y / 2) + (z / 2)))) * (cosh ((y / 2) - (z / 2)))) ^2) is V11() real ext-real set
(cosh ((y / 2) - (z / 2))) ^2 is V11() real ext-real Element of REAL
(cosh ((y / 2) - (z / 2))) * (cosh ((y / 2) - (z / 2))) is V11() real ext-real set
(cosh ((y / 2) + (z / 2))) ^2 is V11() real ext-real Element of REAL
(cosh ((y / 2) + (z / 2))) * (cosh ((y / 2) + (z / 2))) is V11() real ext-real set
(sinh ((y / 2) + (z / 2))) ^2 is V11() real ext-real Element of REAL
(sinh ((y / 2) + (z / 2))) * (sinh ((y / 2) + (z / 2))) is V11() real ext-real set
((cosh ((y / 2) + (z / 2))) ^2) - ((sinh ((y / 2) + (z / 2))) ^2) is V11() real ext-real set
((cosh ((y / 2) - (z / 2))) ^2) * (((cosh ((y / 2) + (z / 2))) ^2) - ((sinh ((y / 2) + (z / 2))) ^2)) is V11() real ext-real set
4 * (((cosh ((y / 2) - (z / 2))) ^2) * (((cosh ((y / 2) + (z / 2))) ^2) - ((sinh ((y / 2) + (z / 2))) ^2))) is V11() real ext-real set
((cosh ((y / 2) - (z / 2))) ^2) * 1 is V11() real ext-real set
4 * (((cosh ((y / 2) - (z / 2))) ^2) * 1) is V11() real ext-real set
sinh ((y / 2) - (z / 2)) is V11() real ext-real Element of REAL
2 * (sinh ((y / 2) - (z / 2))) is V11() real ext-real set
(2 * (sinh ((y / 2) - (z / 2)))) * (cosh ((y / 2) + (z / 2))) is V11() real ext-real set
((2 * (sinh ((y / 2) - (z / 2)))) * (cosh ((y / 2) + (z / 2)))) ^2 is V11() real ext-real set
((2 * (sinh ((y / 2) - (z / 2)))) * (cosh ((y / 2) + (z / 2)))) * ((2 * (sinh ((y / 2) - (z / 2)))) * (cosh ((y / 2) + (z / 2)))) is V11() real ext-real set
(((2 * (sinh ((y / 2) - (z / 2)))) * (cosh ((y / 2) + (z / 2)))) ^2) - (((cosh y) - (cosh z)) ^2) is V11() real ext-real set
(2 * (cosh ((y / 2) + (z / 2)))) * (sinh ((y / 2) - (z / 2))) is V11() real ext-real set
((2 * (cosh ((y / 2) + (z / 2)))) * (sinh ((y / 2) - (z / 2)))) ^2 is V11() real ext-real set
((2 * (cosh ((y / 2) + (z / 2)))) * (sinh ((y / 2) - (z / 2)))) * ((2 * (cosh ((y / 2) + (z / 2)))) * (sinh ((y / 2) - (z / 2)))) is V11() real ext-real set
y + z is V11() real ext-real set
(y + z) / 2 is V11() real ext-real set
sinh ((y + z) / 2) is V11() real ext-real Element of REAL
(2 * (sinh ((y / 2) - (z / 2)))) * (sinh ((y + z) / 2)) is V11() real ext-real set
((2 * (sinh ((y / 2) - (z / 2)))) * (sinh ((y + z) / 2))) ^2 is V11() real ext-real set
((2 * (sinh ((y / 2) - (z / 2)))) * (sinh ((y + z) / 2))) * ((2 * (sinh ((y / 2) - (z / 2)))) * (sinh ((y + z) / 2))) is V11() real ext-real set
(((2 * (cosh ((y / 2) + (z / 2)))) * (sinh ((y / 2) - (z / 2)))) ^2) - (((2 * (sinh ((y / 2) - (z / 2)))) * (sinh ((y + z) / 2))) ^2) is V11() real ext-real set
(sinh ((y / 2) - (z / 2))) ^2 is V11() real ext-real Element of REAL
(sinh ((y / 2) - (z / 2))) * (sinh ((y / 2) - (z / 2))) is V11() real ext-real set
((sinh ((y / 2) - (z / 2))) ^2) * (((cosh ((y / 2) + (z / 2))) ^2) - ((sinh ((y / 2) + (z / 2))) ^2)) is V11() real ext-real set
4 * (((sinh ((y / 2) - (z / 2))) ^2) * (((cosh ((y / 2) + (z / 2))) ^2) - ((sinh ((y / 2) + (z / 2))) ^2))) is V11() real ext-real set
((sinh ((y / 2) - (z / 2))) ^2) * 1 is V11() real ext-real set
4 * (((sinh ((y / 2) - (z / 2))) ^2) * 1) is V11() real ext-real set
y is V11() real ext-real set
sinh y is V11() real ext-real Element of REAL
z is V11() real ext-real set
sinh z is V11() real ext-real Element of REAL
(sinh y) + (sinh z) is V11() real ext-real set
(sinh y) - (sinh z) is V11() real ext-real set
((sinh y) + (sinh z)) / ((sinh y) - (sinh z)) is V11() real ext-real set
y + z is V11() real ext-real set
(y + z) / 2 is V11() real ext-real set
tanh ((y + z) / 2) is V11() real ext-real Element of REAL
y - z is V11() real ext-real set
(y - z) / 2 is V11() real ext-real set
coth ((y - z) / 2) is V11() real ext-real Element of REAL
(tanh ((y + z) / 2)) * (coth ((y - z) / 2)) is V11() real ext-real set
y / 2 is V11() real ext-real set
z / 2 is V11() real ext-real set
(y / 2) + (z / 2) is V11() real ext-real set
sinh ((y / 2) + (z / 2)) is V11() real ext-real Element of REAL
2 * (sinh ((y / 2) + (z / 2))) is V11() real ext-real set
(y / 2) - (z / 2) is V11() real ext-real set
cosh ((y / 2) - (z / 2)) is V11() real ext-real Element of REAL
(2 * (sinh ((y / 2) + (z / 2)))) * (cosh ((y / 2) - (z / 2))) is V11() real ext-real set
((2 * (sinh ((y / 2) + (z / 2)))) * (cosh ((y / 2) - (z / 2)))) / ((sinh y) - (sinh z)) is V11() real ext-real set
sinh ((y / 2) - (z / 2)) is V11() real ext-real Element of REAL
2 * (sinh ((y / 2) - (z / 2))) is V11() real ext-real set
cosh ((y / 2) + (z / 2)) is V11() real ext-real Element of REAL
(2 * (sinh ((y / 2) - (z / 2)))) * (cosh ((y / 2) + (z / 2))) is V11() real ext-real set
((2 * (sinh ((y / 2) + (z / 2)))) * (cosh ((y / 2) - (z / 2)))) / ((2 * (sinh ((y / 2) - (z / 2)))) * (cosh ((y / 2) + (z / 2)))) is V11() real ext-real set
2 * (cosh ((y / 2) + (z / 2))) is V11() real ext-real set
(2 * (cosh ((y / 2) + (z / 2)))) * (sinh ((y / 2) - (z / 2))) is V11() real ext-real set
((2 * (sinh ((y / 2) + (z / 2)))) * (cosh ((y / 2) - (z / 2)))) / ((2 * (cosh ((y / 2) + (z / 2)))) * (sinh ((y / 2) - (z / 2)))) is V11() real ext-real set
(2 * (sinh ((y / 2) + (z / 2)))) / (2 * (cosh ((y / 2) + (z / 2)))) is V11() real ext-real set
(cosh ((y / 2) - (z / 2))) / (sinh ((y / 2) - (z / 2))) is V11() real ext-real set
((2 * (sinh ((y / 2) + (z / 2)))) / (2 * (cosh ((y / 2) + (z / 2))))) * ((cosh ((y / 2) - (z / 2))) / (sinh ((y / 2) - (z / 2)))) is V11() real ext-real set
coth ((y / 2) - (z / 2)) is V11() real ext-real Element of REAL
((2 * (sinh ((y / 2) + (z / 2)))) / (2 * (cosh ((y / 2) + (z / 2))))) * (coth ((y / 2) - (z / 2))) is V11() real ext-real set
2 / 2 is V11() real ext-real non negative set
(sinh ((y / 2) + (z / 2))) / (cosh ((y / 2) + (z / 2))) is V11() real ext-real set
(2 / 2) * ((sinh ((y / 2) + (z / 2))) / (cosh ((y / 2) + (z / 2)))) is V11() real ext-real set
((2 / 2) * ((sinh ((y / 2) + (z / 2))) / (cosh ((y / 2) + (z / 2))))) * (coth ((y / 2) - (z / 2))) is V11() real ext-real set
y is V11() real ext-real set
cosh y is V11() real ext-real Element of REAL
z is V11() real ext-real set
cosh z is V11() real ext-real Element of REAL
(cosh y) + (cosh z) is V11() real ext-real set
(cosh y) - (cosh z) is V11() real ext-real set
((cosh y) + (cosh z)) / ((cosh y) - (cosh z)) is V11() real ext-real set
y + z is V11() real ext-real set
(y + z) / 2 is V11() real ext-real set
coth ((y + z) / 2) is V11() real ext-real Element of REAL
y - z is V11() real ext-real set
(y - z) / 2 is V11() real ext-real set
coth ((y - z) / 2) is V11() real ext-real Element of REAL
(coth ((y + z) / 2)) * (coth ((y - z) / 2)) is V11() real ext-real set
y / 2 is V11() real ext-real set
z / 2 is V11() real ext-real set
(y / 2) + (z / 2) is V11() real ext-real set
cosh ((y / 2) + (z / 2)) is V11() real ext-real Element of REAL
2 * (cosh ((y / 2) + (z / 2))) is V11() real ext-real set
(y / 2) - (z / 2) is V11() real ext-real set
cosh ((y / 2) - (z / 2)) is V11() real ext-real Element of REAL
(2 * (cosh ((y / 2) + (z / 2)))) * (cosh ((y / 2) - (z / 2))) is V11() real ext-real set
((2 * (cosh ((y / 2) + (z / 2)))) * (cosh ((y / 2) - (z / 2)))) / ((cosh y) - (cosh z)) is V11() real ext-real set
sinh ((y / 2) - (z / 2)) is V11() real ext-real Element of REAL
2 * (sinh ((y / 2) - (z / 2))) is V11() real ext-real set
sinh ((y + z) / 2) is V11() real ext-real Element of REAL
(2 * (sinh ((y / 2) - (z / 2)))) * (sinh ((y + z) / 2)) is V11() real ext-real set
((2 * (cosh ((y / 2) + (z / 2)))) * (cosh ((y / 2) - (z / 2)))) / ((2 * (sinh ((y / 2) - (z / 2)))) * (sinh ((y + z) / 2))) is V11() real ext-real set
sinh ((y / 2) + (z / 2)) is V11() real ext-real Element of REAL
2 * (sinh ((y / 2) + (z / 2))) is V11() real ext-real set
sinh ((y - z) / 2) is V11() real ext-real Element of REAL
(2 * (sinh ((y / 2) + (z / 2)))) * (sinh ((y - z) / 2)) is V11() real ext-real set
((2 * (cosh ((y / 2) + (z / 2)))) * (cosh ((y / 2) - (z / 2)))) / ((2 * (sinh ((y / 2) + (z / 2)))) * (sinh ((y - z) / 2))) is V11() real ext-real set
(2 * (cosh ((y / 2) + (z / 2)))) / (2 * (sinh ((y / 2) + (z / 2)))) is V11() real ext-real set
(cosh ((y / 2) - (z / 2))) / (sinh ((y / 2) - (z / 2))) is V11() real ext-real set
((2 * (cosh ((y / 2) + (z / 2)))) / (2 * (sinh ((y / 2) + (z / 2))))) * ((cosh ((y / 2) - (z / 2))) / (sinh ((y / 2) - (z / 2)))) is V11() real ext-real set
coth ((y / 2) - (z / 2)) is V11() real ext-real Element of REAL
((2 * (cosh ((y / 2) + (z / 2)))) / (2 * (sinh ((y / 2) + (z / 2))))) * (coth ((y / 2) - (z / 2))) is V11() real ext-real set
2 / 2 is V11() real ext-real non negative set
(cosh ((y / 2) + (z / 2))) / (sinh ((y / 2) + (z / 2))) is V11() real ext-real set
(2 / 2) * ((cosh ((y / 2) + (z / 2))) / (sinh ((y / 2) + (z / 2)))) is V11() real ext-real set
((2 / 2) * ((cosh ((y / 2) + (z / 2))) / (sinh ((y / 2) + (z / 2))))) * (coth ((y / 2) - (z / 2))) is V11() real ext-real set
y is V11() real ext-real set
sinh y is V11() real ext-real Element of REAL
cosh y is V11() real ext-real Element of REAL
z is V11() real ext-real set
y - z is V11() real ext-real set
sinh z is V11() real ext-real Element of REAL
(sinh y) + (sinh z) is V11() real ext-real set
cosh z is V11() real ext-real Element of REAL
(cosh y) + (cosh z) is V11() real ext-real set
((sinh y) + (sinh z)) / ((cosh y) + (cosh z)) is V11() real ext-real set
(cosh y) - (cosh z) is V11() real ext-real set
(sinh y) - (sinh z) is V11() real ext-real set
((cosh y) - (cosh z)) / ((sinh y) - (sinh z)) is V11() real ext-real set
y / 2 is V11() real ext-real set
z / 2 is V11() real ext-real set
(y / 2) - (z / 2) is V11() real ext-real set
cosh ((y / 2) - (z / 2)) is V11() real ext-real Element of REAL
(y / 2) + (z / 2) is V11() real ext-real set
sinh ((y / 2) + (z / 2)) is V11() real ext-real Element of REAL
2 * (sinh ((y / 2) + (z / 2))) is V11() real ext-real set
(2 * (sinh ((y / 2) + (z / 2)))) * (cosh ((y / 2) - (z / 2))) is V11() real ext-real set
((2 * (sinh ((y / 2) + (z / 2)))) * (cosh ((y / 2) - (z / 2)))) / ((cosh y) + (cosh z)) is V11() real ext-real set
cosh ((y / 2) + (z / 2)) is V11() real ext-real Element of REAL
2 * (cosh ((y / 2) + (z / 2))) is V11() real ext-real set
(2 * (cosh ((y / 2) + (z / 2)))) * (cosh ((y / 2) - (z / 2))) is V11() real ext-real set
((2 * (sinh ((y / 2) + (z / 2)))) * (cosh ((y / 2) - (z / 2)))) / ((2 * (cosh ((y / 2) + (z / 2)))) * (cosh ((y / 2) - (z / 2)))) is V11() real ext-real set
(2 * (sinh ((y / 2) + (z / 2)))) / (2 * (cosh ((y / 2) + (z / 2)))) is V11() real ext-real set
(cosh ((y / 2) - (z / 2))) / (cosh ((y / 2) - (z / 2))) is V11() real ext-real set
((2 * (sinh ((y / 2) + (z / 2)))) / (2 * (cosh ((y / 2) + (z / 2))))) * ((cosh ((y / 2) - (z / 2))) / (cosh ((y / 2) - (z / 2)))) is V11() real ext-real set
((2 * (sinh ((y / 2) + (z / 2)))) / (2 * (cosh ((y / 2) + (z / 2))))) * 1 is V11() real ext-real set
y + z is V11() real ext-real set
(y + z) / 2 is V11() real ext-real set
sinh ((y + z) / 2) is V11() real ext-real Element of REAL
2 * (sinh ((y + z) / 2)) is V11() real ext-real set
(y - z) / 2 is V11() real ext-real set
sinh ((y - z) / 2) is V11() real ext-real Element of REAL
(2 * (sinh ((y + z) / 2))) * (sinh ((y - z) / 2)) is V11() real ext-real set
sinh ((y / 2) - (z / 2)) is V11() real ext-real Element of REAL
(2 * (cosh ((y / 2) + (z / 2)))) * (sinh ((y / 2) - (z / 2))) is V11() real ext-real set
((2 * (sinh ((y + z) / 2))) * (sinh ((y - z) / 2))) / ((2 * (cosh ((y / 2) + (z / 2)))) * (sinh ((y / 2) - (z / 2)))) is V11() real ext-real set
2 * (sinh ((y - z) / 2)) is V11() real ext-real set
(2 * (sinh ((y - z) / 2))) * (sinh ((y + z) / 2)) is V11() real ext-real set
((2 * (sinh ((y - z) / 2))) * (sinh ((y + z) / 2))) / ((2 * (cosh ((y / 2) + (z / 2)))) * (sinh ((y / 2) - (z / 2)))) is V11() real ext-real set
2 * (sinh ((y / 2) - (z / 2))) is V11() real ext-real set
(2 * (sinh ((y / 2) - (z / 2)))) * (cosh ((y / 2) + (z / 2))) is V11() real ext-real set
((cosh y) - (cosh z)) / ((2 * (sinh ((y / 2) - (z / 2)))) * (cosh ((y / 2) + (z / 2)))) is V11() real ext-real set
y is V11() real ext-real set
sinh y is V11() real ext-real Element of REAL
cosh y is V11() real ext-real Element of REAL
z is V11() real ext-real set
y + z is V11() real ext-real set
sinh z is V11() real ext-real Element of REAL
(sinh y) - (sinh z) is V11() real ext-real set
cosh z is V11() real ext-real Element of REAL
(cosh y) + (cosh z) is V11() real ext-real set
((sinh y) - (sinh z)) / ((cosh y) + (cosh z)) is V11() real ext-real set
(cosh y) - (cosh z) is V11() real ext-real set
(sinh y) + (sinh z) is V11() real ext-real set
((cosh y) - (cosh z)) / ((sinh y) + (sinh z)) is V11() real ext-real set
y / 2 is V11() real ext-real set
z / 2 is V11() real ext-real set
(y / 2) + (z / 2) is V11() real ext-real set
cosh ((y / 2) + (z / 2)) is V11() real ext-real Element of REAL
(y / 2) - (z / 2) is V11() real ext-real set
sinh ((y / 2) - (z / 2)) is V11() real ext-real Element of REAL
2 * (sinh ((y / 2) - (z / 2))) is V11() real ext-real set
(2 * (sinh ((y / 2) - (z / 2)))) * (cosh ((y / 2) + (z / 2))) is V11() real ext-real set
((2 * (sinh ((y / 2) - (z / 2)))) * (cosh ((y / 2) + (z / 2)))) / ((cosh y) + (cosh z)) is V11() real ext-real set
2 * (cosh ((y / 2) + (z / 2))) is V11() real ext-real set
(2 * (cosh ((y / 2) + (z / 2)))) * (sinh ((y / 2) - (z / 2))) is V11() real ext-real set
cosh ((y / 2) - (z / 2)) is V11() real ext-real Element of REAL
(2 * (cosh ((y / 2) + (z / 2)))) * (cosh ((y / 2) - (z / 2))) is V11() real ext-real set
((2 * (cosh ((y / 2) + (z / 2)))) * (sinh ((y / 2) - (z / 2)))) / ((2 * (cosh ((y / 2) + (z / 2)))) * (cosh ((y / 2) - (z / 2)))) is V11() real ext-real set
(2 * (cosh ((y / 2) + (z / 2)))) / (2 * (cosh ((y / 2) + (z / 2)))) is V11() real ext-real set
(sinh ((y / 2) - (z / 2))) / (cosh ((y / 2) - (z / 2))) is V11() real ext-real set
((2 * (cosh ((y / 2) + (z / 2)))) / (2 * (cosh ((y / 2) + (z / 2))))) * ((sinh ((y / 2) - (z / 2))) / (cosh ((y / 2) - (z / 2)))) is V11() real ext-real set
(cosh ((y / 2) + (z / 2))) / (cosh ((y / 2) + (z / 2))) is V11() real ext-real set
((cosh ((y / 2) + (z / 2))) / (cosh ((y / 2) + (z / 2)))) * ((sinh ((y / 2) - (z / 2))) / (cosh ((y / 2) - (z / 2)))) is V11() real ext-real set
1 * ((sinh ((y / 2) - (z / 2))) / (cosh ((y / 2) - (z / 2)))) is V11() real ext-real set
sinh ((y / 2) + (z / 2)) is V11() real ext-real Element of REAL
(sinh ((y / 2) + (z / 2))) * (sinh ((y / 2) - (z / 2))) is V11() real ext-real set
(sinh ((y / 2) + (z / 2))) * (cosh ((y / 2) - (z / 2))) is V11() real ext-real set
((sinh ((y / 2) + (z / 2))) * (sinh ((y / 2) - (z / 2)))) / ((sinh ((y / 2) + (z / 2))) * (cosh ((y / 2) - (z / 2)))) is V11() real ext-real set
2 * ((sinh ((y / 2) + (z / 2))) * (sinh ((y / 2) - (z / 2)))) is V11() real ext-real set
2 * ((sinh ((y / 2) + (z / 2))) * (cosh ((y / 2) - (z / 2)))) is V11() real ext-real set
(2 * ((sinh ((y / 2) + (z / 2))) * (sinh ((y / 2) - (z / 2))))) / (2 * ((sinh ((y / 2) + (z / 2))) * (cosh ((y / 2) - (z / 2))))) is V11() real ext-real set
y - z is V11() real ext-real set
(y - z) / 2 is V11() real ext-real set
sinh ((y - z) / 2) is V11() real ext-real Element of REAL
2 * (sinh ((y - z) / 2)) is V11() real ext-real set
(y + z) / 2 is V11() real ext-real set
sinh ((y + z) / 2) is V11() real ext-real Element of REAL
(2 * (sinh ((y - z) / 2))) * (sinh ((y + z) / 2)) is V11() real ext-real set
2 * (sinh ((y / 2) + (z / 2))) is V11() real ext-real set
(2 * (sinh ((y / 2) + (z / 2)))) * (cosh ((y / 2) - (z / 2))) is V11() real ext-real set
((2 * (sinh ((y - z) / 2))) * (sinh ((y + z) / 2))) / ((2 * (sinh ((y / 2) + (z / 2)))) * (cosh ((y / 2) - (z / 2)))) is V11() real ext-real set
((cosh y) - (cosh z)) / ((2 * (sinh ((y / 2) + (z / 2)))) * (cosh ((y / 2) - (z / 2)))) is V11() real ext-real set
y is V11() real ext-real set
sinh y is V11() real ext-real Element of REAL
cosh y is V11() real ext-real Element of REAL
y / 2 is V11() real ext-real set
z is V11() real ext-real set
sinh z is V11() real ext-real Element of REAL
(sinh y) + (sinh z) is V11() real ext-real set
cosh z is V11() real ext-real Element of REAL
(cosh y) + (cosh z) is V11() real ext-real set
((sinh y) + (sinh z)) / ((cosh y) + (cosh z)) is V11() real ext-real set
z / 2 is V11() real ext-real set
(y / 2) + (z / 2) is V11() real ext-real set
tanh ((y / 2) + (z / 2)) is V11() real ext-real Element of REAL
(sinh y) - (sinh z) is V11() real ext-real set
((sinh y) - (sinh z)) / ((cosh y) + (cosh z)) is V11() real ext-real set
(y / 2) - (z / 2) is V11() real ext-real set
tanh ((y / 2) - (z / 2)) is V11() real ext-real Element of REAL
cosh ((y / 2) - (z / 2)) is V11() real ext-real Element of REAL
cosh ((y / 2) + (z / 2)) is V11() real ext-real Element of REAL
sinh ((y / 2) - (z / 2)) is V11() real ext-real Element of REAL
2 * (sinh ((y / 2) - (z / 2))) is V11() real ext-real set
(2 * (sinh ((y / 2) - (z / 2)))) * (cosh ((y / 2) + (z / 2))) is V11() real ext-real set
((2 * (sinh ((y / 2) - (z / 2)))) * (cosh ((y / 2) + (z / 2)))) / ((cosh y) + (cosh z)) is V11() real ext-real set
(sinh ((y / 2) - (z / 2))) * (cosh ((y / 2) + (z / 2))) is V11() real ext-real set
2 * ((sinh ((y / 2) - (z / 2))) * (cosh ((y / 2) + (z / 2)))) is V11() real ext-real set
2 * (cosh ((y / 2) + (z / 2))) is V11() real ext-real set
(2 * (cosh ((y / 2) + (z / 2)))) * (cosh ((y / 2) - (z / 2))) is V11() real ext-real set
(2 * ((sinh ((y / 2) - (z / 2))) * (cosh ((y / 2) + (z / 2))))) / ((2 * (cosh ((y / 2) + (z / 2)))) * (cosh ((y / 2) - (z / 2)))) is V11() real ext-real set
(cosh ((y / 2) + (z / 2))) * (cosh ((y / 2) - (z / 2))) is V11() real ext-real set
2 * ((cosh ((y / 2) + (z / 2))) * (cosh ((y / 2) - (z / 2)))) is V11() real ext-real set
(2 * ((sinh ((y / 2) - (z / 2))) * (cosh ((y / 2) + (z / 2))))) / (2 * ((cosh ((y / 2) + (z / 2))) * (cosh ((y / 2) - (z / 2))))) is V11() real ext-real set
(cosh ((y / 2) + (z / 2))) * (sinh ((y / 2) - (z / 2))) is V11() real ext-real set
((cosh ((y / 2) + (z / 2))) * (sinh ((y / 2) - (z / 2)))) / ((cosh ((y / 2) + (z / 2))) * (cosh ((y / 2) - (z / 2)))) is V11() real ext-real set
(cosh ((y / 2) + (z / 2))) / (cosh ((y / 2) + (z / 2))) is V11() real ext-real set
(sinh ((y / 2) - (z / 2))) / (cosh ((y / 2) - (z / 2))) is V11() real ext-real set
((cosh ((y / 2) + (z / 2))) / (cosh ((y / 2) + (z / 2)))) * ((sinh ((y / 2) - (z / 2))) / (cosh ((y / 2) - (z / 2)))) is V11() real ext-real set
1 * ((sinh ((y / 2) - (z / 2))) / (cosh ((y / 2) - (z / 2)))) is V11() real ext-real set
sinh ((y / 2) + (z / 2)) is V11() real ext-real Element of REAL
2 * (sinh ((y / 2) + (z / 2))) is V11() real ext-real set
(2 * (sinh ((y / 2) + (z / 2)))) * (cosh ((y / 2) - (z / 2))) is V11() real ext-real set
((2 * (sinh ((y / 2) + (z / 2)))) * (cosh ((y / 2) - (z / 2)))) / ((cosh y) + (cosh z)) is V11() real ext-real set
((2 * (sinh ((y / 2) + (z / 2)))) * (cosh ((y / 2) - (z / 2)))) / ((2 * (cosh ((y / 2) + (z / 2)))) * (cosh ((y / 2) - (z / 2)))) is V11() real ext-real set
(2 * (sinh ((y / 2) + (z / 2)))) / (2 * (cosh ((y / 2) + (z / 2)))) is V11() real ext-real set
(cosh ((y / 2) - (z / 2))) / (cosh ((y / 2) - (z / 2))) is V11() real ext-real set
((2 * (sinh ((y / 2) + (z / 2)))) / (2 * (cosh ((y / 2) + (z / 2))))) * ((cosh ((y / 2) - (z / 2))) / (cosh ((y / 2) - (z / 2)))) is V11() real ext-real set
((2 * (sinh ((y / 2) + (z / 2)))) / (2 * (cosh ((y / 2) + (z / 2))))) * 1 is V11() real ext-real set
2 / 2 is V11() real ext-real non negative set
(sinh ((y / 2) + (z / 2))) / (cosh ((y / 2) + (z / 2))) is V11() real ext-real set
(2 / 2) * ((sinh ((y / 2) + (z / 2))) / (cosh ((y / 2) + (z / 2)))) is V11() real ext-real set
y is V11() real ext-real set
tanh y is V11() real ext-real Element of REAL
z is V11() real ext-real set
tanh z is V11() real ext-real Element of REAL
(tanh y) + (tanh z) is V11() real ext-real set
(tanh y) - (tanh z) is V11() real ext-real set
((tanh y) + (tanh z)) / ((tanh y) - (tanh z)) is V11() real ext-real set
y + z is V11() real ext-real set
sinh (y + z) is V11() real ext-real Element of REAL
y - z is V11() real ext-real set
sinh (y - z) is V11() real ext-real Element of REAL
(sinh (y + z)) / (sinh (y - z)) is V11() real ext-real set
cosh y is V11() real ext-real Element of REAL
cosh z is V11() real ext-real Element of REAL
(cosh y) * (cosh z) is V11() real ext-real set
(sinh (y + z)) / ((cosh y) * (cosh z)) is V11() real ext-real set
((sinh (y + z)) / ((cosh y) * (cosh z))) / ((tanh y) - (tanh z)) is V11() real ext-real set
(sinh (y - z)) / ((cosh y) * (cosh z)) is V11() real ext-real set
((sinh (y + z)) / ((cosh y) * (cosh z))) / ((sinh (y - z)) / ((cosh y) * (cosh z))) is V11() real ext-real set
y is V11() real ext-real set
cosh y is V11() real ext-real Element of REAL
(cosh y) + (cosh y) is V11() real ext-real set
1 + ((cosh y) + (cosh y)) is V11() real ext-real set
cosh . y is V11() real ext-real Element of REAL
y is V11() real ext-real set
cosh y is V11() real ext-real Element of REAL
(cosh y) + 1 is V11() real ext-real set
(cosh y) - 1 is V11() real ext-real set
(cosh y) + 2 is V11() real ext-real set
((cosh y) + 2) + (cosh y) is V11() real ext-real set
cosh . y is V11() real ext-real Element of REAL
1 - 1 is V11() real ext-real set
y is V11() real ext-real set
sinh y is V11() real ext-real Element of REAL
cosh y is V11() real ext-real Element of REAL
tanh y is V11() real ext-real Element of REAL
z is V11() real ext-real set
y - z is V11() real ext-real set
sinh (y - z) is V11() real ext-real Element of REAL
(sinh (y - z)) + (sinh y) is V11() real ext-real set
y + z is V11() real ext-real set
sinh (y + z) is V11() real ext-real Element of REAL
((sinh (y - z)) + (sinh y)) + (sinh (y + z)) is V11() real ext-real set
cosh (y - z) is V11() real ext-real Element of REAL
(cosh (y - z)) + (cosh y) is V11() real ext-real set
cosh (y + z) is V11() real ext-real Element of REAL
((cosh (y - z)) + (cosh y)) + (cosh (y + z)) is V11() real ext-real set
(((sinh (y - z)) + (sinh y)) + (sinh (y + z))) / (((cosh (y - z)) + (cosh y)) + (cosh (y + z))) is V11() real ext-real set
cosh z is V11() real ext-real Element of REAL
(sinh y) * (cosh z) is V11() real ext-real set
sinh z is V11() real ext-real Element of REAL
(cosh y) * (sinh z) is V11() real ext-real set
((sinh y) * (cosh z)) - ((cosh y) * (sinh z)) is V11() real ext-real set
(((sinh y) * (cosh z)) - ((cosh y) * (sinh z))) + (sinh y) is V11() real ext-real set
((((sinh y) * (cosh z)) - ((cosh y) * (sinh z))) + (sinh y)) + (sinh (y + z)) is V11() real ext-real set
(((((sinh y) * (cosh z)) - ((cosh y) * (sinh z))) + (sinh y)) + (sinh (y + z))) / (((cosh (y - z)) + (cosh y)) + (cosh (y + z))) is V11() real ext-real set
(sinh y) + (((sinh y) * (cosh z)) - ((cosh y) * (sinh z))) is V11() real ext-real set
((sinh y) * (cosh z)) + ((cosh y) * (sinh z)) is V11() real ext-real set
((sinh y) + (((sinh y) * (cosh z)) - ((cosh y) * (sinh z)))) + (((sinh y) * (cosh z)) + ((cosh y) * (sinh z))) is V11() real ext-real set
(cosh y) + (cosh (y - z)) is V11() real ext-real set
((cosh y) + (cosh (y - z))) + (cosh (y + z)) is V11() real ext-real set
(((sinh y) + (((sinh y) * (cosh z)) - ((cosh y) * (sinh z)))) + (((sinh y) * (cosh z)) + ((cosh y) * (sinh z)))) / (((cosh y) + (cosh (y - z))) + (cosh (y + z))) is V11() real ext-real set
(cosh z) + (cosh z) is V11() real ext-real set
1 + ((cosh z) + (cosh z)) is V11() real ext-real set
(sinh y) * (1 + ((cosh z) + (cosh z))) is V11() real ext-real set
(cosh y) * (cosh z) is V11() real ext-real set
(sinh y) * (sinh z) is V11() real ext-real set
((cosh y) * (cosh z)) - ((sinh y) * (sinh z)) is V11() real ext-real set
(cosh y) + (((cosh y) * (cosh z)) - ((sinh y) * (sinh z))) is V11() real ext-real set
((cosh y) + (((cosh y) * (cosh z)) - ((sinh y) * (sinh z)))) + (cosh (y + z)) is V11() real ext-real set
((sinh y) * (1 + ((cosh z) + (cosh z)))) / (((cosh y) + (((cosh y) * (cosh z)) - ((sinh y) * (sinh z)))) + (cosh (y + z))) is V11() real ext-real set
((cosh y) * (cosh z)) + ((sinh y) * (sinh z)) is V11() real ext-real set
((cosh y) + (((cosh y) * (cosh z)) - ((sinh y) * (sinh z)))) + (((cosh y) * (cosh z)) + ((sinh y) * (sinh z))) is V11() real ext-real set
((sinh y) * (1 + ((cosh z) + (cosh z)))) / (((cosh y) + (((cosh y) * (cosh z)) - ((sinh y) * (sinh z)))) + (((cosh y) * (cosh z)) + ((sinh y) * (sinh z)))) is V11() real ext-real set
(cosh y) * (1 + ((cosh z) + (cosh z))) is V11() real ext-real set
((sinh y) * (1 + ((cosh z) + (cosh z)))) / ((cosh y) * (1 + ((cosh z) + (cosh z)))) is V11() real ext-real set
(sinh y) / (cosh y) is V11() real ext-real set
(1 + ((cosh z) + (cosh z))) / (1 + ((cosh z) + (cosh z))) is V11() real ext-real set
((sinh y) / (cosh y)) * ((1 + ((cosh z) + (cosh z))) / (1 + ((cosh z) + (cosh z)))) is V11() real ext-real set
((sinh y) / (cosh y)) * 1 is V11() real ext-real set
y is V11() real ext-real set
sinh y is V11() real ext-real Element of REAL
cosh y is V11() real ext-real Element of REAL
tanh y is V11() real ext-real Element of REAL
(tanh y) * (cosh y) is V11() real ext-real set
z is V11() real ext-real set
cosh z is V11() real ext-real Element of REAL
(sinh y) * (cosh z) is V11() real ext-real set
(cosh y) * (cosh z) is V11() real ext-real set
((sinh y) * (cosh z)) / ((cosh y) * (cosh z)) is V11() real ext-real set
(tanh y) * ((cosh y) * (cosh z)) is V11() real ext-real set
sinh z is V11() real ext-real Element of REAL
(sinh y) * (sinh z) is V11() real ext-real set
tanh z is V11() real ext-real Element of REAL
(tanh y) * (tanh z) is V11() real ext-real set
((tanh y) * (tanh z)) * ((cosh y) * (cosh z)) is V11() real ext-real set
(sinh y) / (cosh y) is V11() real ext-real set
((sinh y) / (cosh y)) * (cosh y) is V11() real ext-real set
((sinh y) * (sinh z)) / ((cosh y) * (cosh z)) is V11() real ext-real set
(((sinh y) * (sinh z)) / ((cosh y) * (cosh z))) * ((cosh y) * (cosh z)) is V11() real ext-real set
(sinh z) / (cosh z) is V11() real ext-real set
((sinh y) / (cosh y)) * ((sinh z) / (cosh z)) is V11() real ext-real set
(((sinh y) / (cosh y)) * ((sinh z) / (cosh z))) * ((cosh y) * (cosh z)) is V11() real ext-real set
(tanh y) * ((sinh z) / (cosh z)) is V11() real ext-real set
((tanh y) * ((sinh z) / (cosh z))) * ((cosh y) * (cosh z)) is V11() real ext-real set
y is V11() real ext-real set
tanh y is V11() real ext-real Element of REAL
cosh y is V11() real ext-real Element of REAL
z is V11() real ext-real set
y + z is V11() real ext-real set
tanh z is V11() real ext-real Element of REAL
(tanh y) + (tanh z) is V11() real ext-real set
(tanh y) * (tanh z) is V11() real ext-real set
cosh z is V11() real ext-real Element of REAL
1 + ((tanh y) * (tanh z)) is V11() real ext-real set
w is V11() real ext-real set
(y + z) + w is V11() real ext-real set
sinh ((y + z) + w) is V11() real ext-real Element of REAL
tanh w is V11() real ext-real Element of REAL
((tanh y) + (tanh z)) + (tanh w) is V11() real ext-real set
((tanh y) * (tanh z)) * (tanh w) is V11() real ext-real set
(((tanh y) + (tanh z)) + (tanh w)) + (((tanh y) * (tanh z)) * (tanh w)) is V11() real ext-real set
((((tanh y) + (tanh z)) + (tanh w)) + (((tanh y) * (tanh z)) * (tanh w))) * (cosh y) is V11() real ext-real set
(((((tanh y) + (tanh z)) + (tanh w)) + (((tanh y) * (tanh z)) * (tanh w))) * (cosh y)) * (cosh z) is V11() real ext-real set
cosh w is V11() real ext-real Element of REAL
((((((tanh y) + (tanh z)) + (tanh w)) + (((tanh y) * (tanh z)) * (tanh w))) * (cosh y)) * (cosh z)) * (cosh w) is V11() real ext-real set
cosh ((y + z) + w) is V11() real ext-real Element of REAL
(tanh z) * (tanh w) is V11() real ext-real set
(1 + ((tanh y) * (tanh z))) + ((tanh z) * (tanh w)) is V11() real ext-real set
(tanh w) * (tanh y) is V11() real ext-real set
((1 + ((tanh y) * (tanh z))) + ((tanh z) * (tanh w))) + ((tanh w) * (tanh y)) is V11() real ext-real set
(((1 + ((tanh y) * (tanh z))) + ((tanh z) * (tanh w))) + ((tanh w) * (tanh y))) * (cosh y) is V11() real ext-real set
((((1 + ((tanh y) * (tanh z))) + ((tanh z) * (tanh w))) + ((tanh w) * (tanh y))) * (cosh y)) * (cosh z) is V11() real ext-real set
(((((1 + ((tanh y) * (tanh z))) + ((tanh z) * (tanh w))) + ((tanh w) * (tanh y))) * (cosh y)) * (cosh z)) * (cosh w) is V11() real ext-real set
tanh ((y + z) + w) is V11() real ext-real Element of REAL
1 + ((tanh z) * (tanh w)) is V11() real ext-real set
(1 + ((tanh z) * (tanh w))) + ((tanh w) * (tanh y)) is V11() real ext-real set
((1 + ((tanh z) * (tanh w))) + ((tanh w) * (tanh y))) + ((tanh y) * (tanh z)) is V11() real ext-real set
((((tanh y) + (tanh z)) + (tanh w)) + (((tanh y) * (tanh z)) * (tanh w))) / (((1 + ((tanh z) * (tanh w))) + ((tanh w) * (tanh y))) + ((tanh y) * (tanh z))) is V11() real ext-real set
(cosh y) * (cosh z) is V11() real ext-real set
cosh (y + z) is V11() real ext-real Element of REAL
(cosh (y + z)) * (cosh w) is V11() real ext-real set
sinh (y + z) is V11() real ext-real Element of REAL
sinh w is V11() real ext-real Element of REAL
(sinh (y + z)) * (sinh w) is V11() real ext-real set
((cosh (y + z)) * (cosh w)) + ((sinh (y + z)) * (sinh w)) is V11() real ext-real set
sinh y is V11() real ext-real Element of REAL
sinh z is V11() real ext-real Element of REAL
(sinh y) * (sinh z) is V11() real ext-real set
((cosh y) * (cosh z)) + ((sinh y) * (sinh z)) is V11() real ext-real set
(((cosh y) * (cosh z)) + ((sinh y) * (sinh z))) * (cosh w) is V11() real ext-real set
((((cosh y) * (cosh z)) + ((sinh y) * (sinh z))) * (cosh w)) + ((sinh (y + z)) * (sinh w)) is V11() real ext-real set
((cosh y) * (cosh z)) * (cosh w) is V11() real ext-real set
((sinh y) * (sinh z)) * (cosh w) is V11() real ext-real set
(((cosh y) * (cosh z)) * (cosh w)) + (((sinh y) * (sinh z)) * (cosh w)) is V11() real ext-real set
(sinh y) * (cosh z) is V11() real ext-real set
(cosh y) * (sinh z) is V11() real ext-real set
((sinh y) * (cosh z)) + ((cosh y) * (sinh z)) is V11() real ext-real set
(((sinh y) * (cosh z)) + ((cosh y) * (sinh z))) * (sinh w) is V11() real ext-real set
((((cosh y) * (cosh z)) * (cosh w)) + (((sinh y) * (sinh z)) * (cosh w))) + ((((sinh y) * (cosh z)) + ((cosh y) * (sinh z))) * (sinh w)) is V11() real ext-real set
((tanh y) * (tanh z)) * ((cosh y) * (cosh z)) is V11() real ext-real set
(((tanh y) * (tanh z)) * ((cosh y) * (cosh z))) * (cosh w) is V11() real ext-real set
(((cosh y) * (cosh z)) * (cosh w)) + ((((tanh y) * (tanh z)) * ((cosh y) * (cosh z))) * (cosh w)) is V11() real ext-real set
(sinh y) * (sinh w) is V11() real ext-real set
((sinh y) * (sinh w)) * (cosh z) is V11() real ext-real set
(sinh z) * (sinh w) is V11() real ext-real set
((sinh z) * (sinh w)) * (cosh y) is V11() real ext-real set
(((sinh y) * (sinh w)) * (cosh z)) + (((sinh z) * (sinh w)) * (cosh y)) is V11() real ext-real set
((((cosh y) * (cosh z)) * (cosh w)) + ((((tanh y) * (tanh z)) * ((cosh y) * (cosh z))) * (cosh w))) + ((((sinh y) * (sinh w)) * (cosh z)) + (((sinh z) * (sinh w)) * (cosh y))) is V11() real ext-real set
(cosh w) * (cosh y) is V11() real ext-real set
((tanh w) * (tanh y)) * ((cosh w) * (cosh y)) is V11() real ext-real set
(((tanh w) * (tanh y)) * ((cosh w) * (cosh y))) * (cosh z) is V11() real ext-real set
((((tanh w) * (tanh y)) * ((cosh w) * (cosh y))) * (cosh z)) + (((sinh z) * (sinh w)) * (cosh y)) is V11() real ext-real set
((((cosh y) * (cosh z)) * (cosh w)) + ((((tanh y) * (tanh z)) * ((cosh y) * (cosh z))) * (cosh w))) + (((((tanh w) * (tanh y)) * ((cosh w) * (cosh y))) * (cosh z)) + (((sinh z) * (sinh w)) * (cosh y))) is V11() real ext-real set
(1 + ((tanh y) * (tanh z))) * (((cosh y) * (cosh z)) * (cosh w)) is V11() real ext-real set
(cosh z) * (cosh w) is V11() real ext-real set
((tanh z) * (tanh w)) * ((cosh z) * (cosh w)) is V11() real ext-real set
(((tanh z) * (tanh w)) * ((cosh z) * (cosh w))) * (cosh y) is V11() real ext-real set
((tanh w) * (tanh y)) * (((cosh y) * (cosh z)) * (cosh w)) is V11() real ext-real set
((((tanh z) * (tanh w)) * ((cosh z) * (cosh w))) * (cosh y)) + (((tanh w) * (tanh y)) * (((cosh y) * (cosh z)) * (cosh w))) is V11() real ext-real set
((1 + ((tanh y) * (tanh z))) * (((cosh y) * (cosh z)) * (cosh w))) + (((((tanh z) * (tanh w)) * ((cosh z) * (cosh w))) * (cosh y)) + (((tanh w) * (tanh y)) * (((cosh y) * (cosh z)) * (cosh w)))) is V11() real ext-real set
(sinh (y + z)) * (cosh w) is V11() real ext-real set
(cosh (y + z)) * (sinh w) is V11() real ext-real set
((sinh (y + z)) * (cosh w)) + ((cosh (y + z)) * (sinh w)) is V11() real ext-real set
(((sinh y) * (cosh z)) + ((cosh y) * (sinh z))) * (cosh w) is V11() real ext-real set
((((sinh y) * (cosh z)) + ((cosh y) * (sinh z))) * (cosh w)) + ((cosh (y + z)) * (sinh w)) is V11() real ext-real set
(((cosh y) * (cosh z)) + ((sinh y) * (sinh z))) * (sinh w) is V11() real ext-real set
((((sinh y) * (cosh z)) + ((cosh y) * (sinh z))) * (cosh w)) + ((((cosh y) * (cosh z)) + ((sinh y) * (sinh z))) * (sinh w)) is V11() real ext-real set
(tanh y) * ((cosh y) * (cosh z)) is V11() real ext-real set
((tanh y) * ((cosh y) * (cosh z))) + ((cosh y) * (sinh z)) is V11() real ext-real set
(((tanh y) * ((cosh y) * (cosh z))) + ((cosh y) * (sinh z))) * (cosh w) is V11() real ext-real set
((((tanh y) * ((cosh y) * (cosh z))) + ((cosh y) * (sinh z))) * (cosh w)) + ((((cosh y) * (cosh z)) + ((sinh y) * (sinh z))) * (sinh w)) is V11() real ext-real set
(tanh z) * ((cosh y) * (cosh z)) is V11() real ext-real set
((tanh y) * ((cosh y) * (cosh z))) + ((tanh z) * ((cosh y) * (cosh z))) is V11() real ext-real set
(((tanh y) * ((cosh y) * (cosh z))) + ((tanh z) * ((cosh y) * (cosh z)))) * (cosh w) is V11() real ext-real set
((((tanh y) * ((cosh y) * (cosh z))) + ((tanh z) * ((cosh y) * (cosh z)))) * (cosh w)) + ((((cosh y) * (cosh z)) + ((sinh y) * (sinh z))) * (sinh w)) is V11() real ext-real set
((tanh y) + (tanh z)) * (((cosh y) * (cosh z)) * (cosh w)) is V11() real ext-real set
(cosh z) * (sinh w) is V11() real ext-real set
(cosh y) * ((cosh z) * (sinh w)) is V11() real ext-real set
((sinh y) * (sinh z)) * (sinh w) is V11() real ext-real set
((cosh y) * ((cosh z) * (sinh w))) + (((sinh y) * (sinh z)) * (sinh w)) is V11() real ext-real set
(((tanh y) + (tanh z)) * (((cosh y) * (cosh z)) * (cosh w))) + (((cosh y) * ((cosh z) * (sinh w))) + (((sinh y) * (sinh z)) * (sinh w))) is V11() real ext-real set
(tanh w) * ((cosh z) * (cosh w)) is V11() real ext-real set
(cosh y) * ((tanh w) * ((cosh z) * (cosh w))) is V11() real ext-real set
((cosh y) * ((tanh w) * ((cosh z) * (cosh w)))) + (((sinh y) * (sinh z)) * (sinh w)) is V11() real ext-real set
(((tanh y) + (tanh z)) * (((cosh y) * (cosh z)) * (cosh w))) + (((cosh y) * ((tanh w) * ((cosh z) * (cosh w)))) + (((sinh y) * (sinh z)) * (sinh w))) is V11() real ext-real set
(tanh w) * ((cosh y) * (cosh z)) is V11() real ext-real set
((tanh w) * ((cosh y) * (cosh z))) * (cosh w) is V11() real ext-real set
(tanh y) * (cosh y) is V11() real ext-real set
((tanh y) * (cosh y)) * (sinh z) is V11() real ext-real set
(((tanh y) * (cosh y)) * (sinh z)) * (sinh w) is V11() real ext-real set
(((tanh w) * ((cosh y) * (cosh z))) * (cosh w)) + ((((tanh y) * (cosh y)) * (sinh z)) * (sinh w)) is V11() real ext-real set
(((tanh y) + (tanh z)) * (((cosh y) * (cosh z)) * (cosh w))) + ((((tanh w) * ((cosh y) * (cosh z))) * (cosh w)) + ((((tanh y) * (cosh y)) * (sinh z)) * (sinh w))) is V11() real ext-real set
(tanh z) * (cosh z) is V11() real ext-real set
((tanh y) * (cosh y)) * ((tanh z) * (cosh z)) is V11() real ext-real set
(((tanh y) * (cosh y)) * ((tanh z) * (cosh z))) * (sinh w) is V11() real ext-real set
(((tanh w) * ((cosh y) * (cosh z))) * (cosh w)) + ((((tanh y) * (cosh y)) * ((tanh z) * (cosh z))) * (sinh w)) is V11() real ext-real set
(((tanh y) + (tanh z)) * (((cosh y) * (cosh z)) * (cosh w))) + ((((tanh w) * ((cosh y) * (cosh z))) * (cosh w)) + ((((tanh y) * (cosh y)) * ((tanh z) * (cosh z))) * (sinh w))) is V11() real ext-real set
(tanh w) * (cosh w) is V11() real ext-real set
(((tanh y) * (tanh z)) * ((cosh y) * (cosh z))) * ((tanh w) * (cosh w)) is V11() real ext-real set
(((tanh w) * ((cosh y) * (cosh z))) * (cosh w)) + ((((tanh y) * (tanh z)) * ((cosh y) * (cosh z))) * ((tanh w) * (cosh w))) is V11() real ext-real set
(((tanh y) + (tanh z)) * (((cosh y) * (cosh z)) * (cosh w))) + ((((tanh w) * ((cosh y) * (cosh z))) * (cosh w)) + ((((tanh y) * (tanh z)) * ((cosh y) * (cosh z))) * ((tanh w) * (cosh w)))) is V11() real ext-real set
((((tanh y) + (tanh z)) + (tanh w)) + (((tanh y) * (tanh z)) * (tanh w))) * (((cosh y) * (cosh z)) * (cosh w)) is V11() real ext-real set
(((1 + ((tanh y) * (tanh z))) + ((tanh z) * (tanh w))) + ((tanh w) * (tanh y))) * (((cosh y) * (cosh z)) * (cosh w)) is V11() real ext-real set
(((((tanh y) + (tanh z)) + (tanh w)) + (((tanh y) * (tanh z)) * (tanh w))) * (((cosh y) * (cosh z)) * (cosh w))) / ((((1 + ((tanh y) * (tanh z))) + ((tanh z) * (tanh w))) + ((tanh w) * (tanh y))) * (((cosh y) * (cosh z)) * (cosh w))) is V11() real ext-real set
((((tanh y) + (tanh z)) + (tanh w)) + (((tanh y) * (tanh z)) * (tanh w))) / (((1 + ((tanh y) * (tanh z))) + ((tanh z) * (tanh w))) + ((tanh w) * (tanh y))) is V11() real ext-real set
y is V11() real ext-real set
2 * y is V11() real ext-real set
cosh (2 * y) is V11() real ext-real Element of REAL
z is V11() real ext-real set
2 * z is V11() real ext-real set
cosh (2 * z) is V11() real ext-real Element of REAL
(cosh (2 * y)) + (cosh (2 * z)) is V11() real ext-real set
y + z is V11() real ext-real set
cosh (y + z) is V11() real ext-real Element of REAL
w is V11() real ext-real set
2 * w is V11() real ext-real set
cosh (2 * w) is V11() real ext-real Element of REAL
((cosh (2 * y)) + (cosh (2 * z))) + (cosh (2 * w)) is V11() real ext-real set
(y + z) + w is V11() real ext-real set
2 * ((y + z) + w) is V11() real ext-real set
cosh (2 * ((y + z) + w)) is V11() real ext-real Element of REAL
(((cosh (2 * y)) + (cosh (2 * z))) + (cosh (2 * w))) + (cosh (2 * ((y + z) + w))) is V11() real ext-real set
z + w is V11() real ext-real set
cosh (z + w) is V11() real ext-real Element of REAL
4 * (cosh (z + w)) is V11() real ext-real set
w + y is V11() real ext-real set
cosh (w + y) is V11() real ext-real Element of REAL
(4 * (cosh (z + w))) * (cosh (w + y)) is V11() real ext-real set
((4 * (cosh (z + w))) * (cosh (w + y))) * (cosh (y + z)) is V11() real ext-real set
(cosh (2 * ((y + z) + w))) + (cosh (2 * y)) is V11() real ext-real set
(1 / 2) * ((cosh (2 * ((y + z) + w))) + (cosh (2 * y))) is V11() real ext-real set
(cosh (2 * w)) + (cosh (2 * z)) is V11() real ext-real set
(1 / 2) * ((cosh (2 * w)) + (cosh (2 * z))) is V11() real ext-real set
((1 / 2) * ((cosh (2 * ((y + z) + w))) + (cosh (2 * y)))) + ((1 / 2) * ((cosh (2 * w)) + (cosh (2 * z)))) is V11() real ext-real set
2 * (((1 / 2) * ((cosh (2 * ((y + z) + w))) + (cosh (2 * y)))) + ((1 / 2) * ((cosh (2 * w)) + (cosh (2 * z))))) is V11() real ext-real set
(2 * ((y + z) + w)) / 2 is V11() real ext-real set
(2 * y) / 2 is V11() real ext-real set
((2 * ((y + z) + w)) / 2) + ((2 * y) / 2) is V11() real ext-real set
cosh (((2 * ((y + z) + w)) / 2) + ((2 * y) / 2)) is V11() real ext-real Element of REAL
2 * (cosh (((2 * ((y + z) + w)) / 2) + ((2 * y) / 2))) is V11() real ext-real set
((2 * ((y + z) + w)) / 2) - ((2 * y) / 2) is V11() real ext-real set
cosh (((2 * ((y + z) + w)) / 2) - ((2 * y) / 2)) is V11() real ext-real Element of REAL
(2 * (cosh (((2 * ((y + z) + w)) / 2) + ((2 * y) / 2)))) * (cosh (((2 * ((y + z) + w)) / 2) - ((2 * y) / 2))) is V11() real ext-real set
(1 / 2) * ((2 * (cosh (((2 * ((y + z) + w)) / 2) + ((2 * y) / 2)))) * (cosh (((2 * ((y + z) + w)) / 2) - ((2 * y) / 2)))) is V11() real ext-real set
((1 / 2) * ((2 * (cosh (((2 * ((y + z) + w)) / 2) + ((2 * y) / 2)))) * (cosh (((2 * ((y + z) + w)) / 2) - ((2 * y) / 2))))) + ((1 / 2) * ((cosh (2 * w)) + (cosh (2 * z)))) is V11() real ext-real set
2 * (((1 / 2) * ((2 * (cosh (((2 * ((y + z) + w)) / 2) + ((2 * y) / 2)))) * (cosh (((2 * ((y + z) + w)) / 2) - ((2 * y) / 2))))) + ((1 / 2) * ((cosh (2 * w)) + (cosh (2 * z))))) is V11() real ext-real set
((y + z) + w) + y is V11() real ext-real set
cosh (((y + z) + w) + y) is V11() real ext-real Element of REAL
(cosh (z + w)) * (cosh (((y + z) + w) + y)) is V11() real ext-real set
(2 * w) / 2 is V11() real ext-real set
(2 * z) / 2 is V11() real ext-real set
((2 * w) / 2) + ((2 * z) / 2) is V11() real ext-real set
cosh (((2 * w) / 2) + ((2 * z) / 2)) is V11() real ext-real Element of REAL
2 * (cosh (((2 * w) / 2) + ((2 * z) / 2))) is V11() real ext-real set
((2 * w) / 2) - ((2 * z) / 2) is V11() real ext-real set
cosh (((2 * w) / 2) - ((2 * z) / 2)) is V11() real ext-real Element of REAL
(2 * (cosh (((2 * w) / 2) + ((2 * z) / 2)))) * (cosh (((2 * w) / 2) - ((2 * z) / 2))) is V11() real ext-real set
(1 / 2) * ((2 * (cosh (((2 * w) / 2) + ((2 * z) / 2)))) * (cosh (((2 * w) / 2) - ((2 * z) / 2)))) is V11() real ext-real set
((cosh (z + w)) * (cosh (((y + z) + w) + y))) + ((1 / 2) * ((2 * (cosh (((2 * w) / 2) + ((2 * z) / 2)))) * (cosh (((2 * w) / 2) - ((2 * z) / 2))))) is V11() real ext-real set
2 * (((cosh (z + w)) * (cosh (((y + z) + w) + y))) + ((1 / 2) * ((2 * (cosh (((2 * w) / 2) + ((2 * z) / 2)))) * (cosh (((2 * w) / 2) - ((2 * z) / 2)))))) is V11() real ext-real set
(2 * y) + (z + w) is V11() real ext-real set
cosh ((2 * y) + (z + w)) is V11() real ext-real Element of REAL
w - z is V11() real ext-real set
cosh (w - z) is V11() real ext-real Element of REAL
(cosh ((2 * y) + (z + w))) + (cosh (w - z)) is V11() real ext-real set
(cosh (z + w)) * ((cosh ((2 * y) + (z + w))) + (cosh (w - z))) is V11() real ext-real set
2 * ((cosh (z + w)) * ((cosh ((2 * y) + (z + w))) + (cosh (w - z)))) is V11() real ext-real set
((2 * y) + (z + w)) / 2 is V11() real ext-real set
(w - z) / 2 is V11() real ext-real set
(((2 * y) + (z + w)) / 2) + ((w - z) / 2) is V11() real ext-real set
cosh ((((2 * y) + (z + w)) / 2) + ((w - z) / 2)) is V11() real ext-real Element of REAL
2 * (cosh ((((2 * y) + (z + w)) / 2) + ((w - z) / 2))) is V11() real ext-real set
(((2 * y) + (z + w)) / 2) - ((w - z) / 2) is V11() real ext-real set
cosh ((((2 * y) + (z + w)) / 2) - ((w - z) / 2)) is V11() real ext-real Element of REAL
(2 * (cosh ((((2 * y) + (z + w)) / 2) + ((w - z) / 2)))) * (cosh ((((2 * y) + (z + w)) / 2) - ((w - z) / 2))) is V11() real ext-real set
(cosh (z + w)) * ((2 * (cosh ((((2 * y) + (z + w)) / 2) + ((w - z) / 2)))) * (cosh ((((2 * y) + (z + w)) / 2) - ((w - z) / 2)))) is V11() real ext-real set
2 * ((cosh (z + w)) * ((2 * (cosh ((((2 * y) + (z + w)) / 2) + ((w - z) / 2)))) * (cosh ((((2 * y) + (z + w)) / 2) - ((w - z) / 2))))) is V11() real ext-real set
y is V11() real ext-real set
sinh y is V11() real ext-real Element of REAL
z is V11() real ext-real set
sinh z is V11() real ext-real Element of REAL
(sinh y) * (sinh z) is V11() real ext-real set
z - y is V11() real ext-real set
sinh (z - y) is V11() real ext-real Element of REAL
((sinh y) * (sinh z)) * (sinh (z - y)) is V11() real ext-real set
w is V11() real ext-real set
sinh w is V11() real ext-real Element of REAL
(sinh z) * (sinh w) is V11() real ext-real set
w - z is V11() real ext-real set
sinh (w - z) is V11() real ext-real Element of REAL
((sinh z) * (sinh w)) * (sinh (w - z)) is V11() real ext-real set
(((sinh y) * (sinh z)) * (sinh (z - y))) + (((sinh z) * (sinh w)) * (sinh (w - z))) is V11() real ext-real set
(sinh w) * (sinh y) is V11() real ext-real set
y - w is V11() real ext-real set
sinh (y - w) is V11() real ext-real Element of REAL
((sinh w) * (sinh y)) * (sinh (y - w)) is V11() real ext-real set
((((sinh y) * (sinh z)) * (sinh (z - y))) + (((sinh z) * (sinh w)) * (sinh (w - z)))) + (((sinh w) * (sinh y)) * (sinh (y - w))) is V11() real ext-real set
(sinh (z - y)) * (sinh (w - z)) is V11() real ext-real set
((sinh (z - y)) * (sinh (w - z))) * (sinh (y - w)) is V11() real ext-real set
(((((sinh y) * (sinh z)) * (sinh (z - y))) + (((sinh z) * (sinh w)) * (sinh (w - z)))) + (((sinh w) * (sinh y)) * (sinh (y - w)))) + (((sinh (z - y)) * (sinh (w - z))) * (sinh (y - w))) is V11() real ext-real set
y + z is V11() real ext-real set
cosh (y + z) is V11() real ext-real Element of REAL
y - z is V11() real ext-real set
cosh (y - z) is V11() real ext-real Element of REAL
(cosh (y + z)) - (cosh (y - z)) is V11() real ext-real set
(1 / 2) * ((cosh (y + z)) - (cosh (y - z))) is V11() real ext-real set
((1 / 2) * ((cosh (y + z)) - (cosh (y - z)))) * (sinh (z - y)) is V11() real ext-real set
(((1 / 2) * ((cosh (y + z)) - (cosh (y - z)))) * (sinh (z - y))) + (((sinh z) * (sinh w)) * (sinh (w - z))) is V11() real ext-real set
((((1 / 2) * ((cosh (y + z)) - (cosh (y - z)))) * (sinh (z - y))) + (((sinh z) * (sinh w)) * (sinh (w - z)))) + (((sinh w) * (sinh y)) * (sinh (y - w))) is V11() real ext-real set
(((((1 / 2) * ((cosh (y + z)) - (cosh (y - z)))) * (sinh (z - y))) + (((sinh z) * (sinh w)) * (sinh (w - z)))) + (((sinh w) * (sinh y)) * (sinh (y - w)))) + (((sinh (z - y)) * (sinh (w - z))) * (sinh (y - w))) is V11() real ext-real set
(cosh (y + z)) * (sinh (z - y)) is V11() real ext-real set
(cosh (y - z)) * (sinh (z - y)) is V11() real ext-real set
((cosh (y + z)) * (sinh (z - y))) - ((cosh (y - z)) * (sinh (z - y))) is V11() real ext-real set
(1 / 2) * (((cosh (y + z)) * (sinh (z - y))) - ((cosh (y - z)) * (sinh (z - y)))) is V11() real ext-real set
((1 / 2) * (((cosh (y + z)) * (sinh (z - y))) - ((cosh (y - z)) * (sinh (z - y))))) + (((sinh z) * (sinh w)) * (sinh (w - z))) is V11() real ext-real set
(((1 / 2) * (((cosh (y + z)) * (sinh (z - y))) - ((cosh (y - z)) * (sinh (z - y))))) + (((sinh z) * (sinh w)) * (sinh (w - z)))) + (((sinh w) * (sinh y)) * (sinh (y - w))) is V11() real ext-real set
((((1 / 2) * (((cosh (y + z)) * (sinh (z - y))) - ((cosh (y - z)) * (sinh (z - y))))) + (((sinh z) * (sinh w)) * (sinh (w - z)))) + (((sinh w) * (sinh y)) * (sinh (y - w)))) + (((sinh (z - y)) * (sinh (w - z))) * (sinh (y - w))) is V11() real ext-real set
(y + z) + (z - y) is V11() real ext-real set
sinh ((y + z) + (z - y)) is V11() real ext-real Element of REAL
(y + z) - (z - y) is V11() real ext-real set
sinh ((y + z) - (z - y)) is V11() real ext-real Element of REAL
(sinh ((y + z) + (z - y))) - (sinh ((y + z) - (z - y))) is V11() real ext-real set
(1 / 2) * ((sinh ((y + z) + (z - y))) - (sinh ((y + z) - (z - y)))) is V11() real ext-real set
((1 / 2) * ((sinh ((y + z) + (z - y))) - (sinh ((y + z) - (z - y))))) - ((cosh (y - z)) * (sinh (z - y))) is V11() real ext-real set
(1 / 2) * (((1 / 2) * ((sinh ((y + z) + (z - y))) - (sinh ((y + z) - (z - y))))) - ((cosh (y - z)) * (sinh (z - y)))) is V11() real ext-real set
((1 / 2) * (((1 / 2) * ((sinh ((y + z) + (z - y))) - (sinh ((y + z) - (z - y))))) - ((cosh (y - z)) * (sinh (z - y))))) + (((sinh z) * (sinh w)) * (sinh (w - z))) is V11() real ext-real set
(((1 / 2) * (((1 / 2) * ((sinh ((y + z) + (z - y))) - (sinh ((y + z) - (z - y))))) - ((cosh (y - z)) * (sinh (z - y))))) + (((sinh z) * (sinh w)) * (sinh (w - z)))) + (((sinh w) * (sinh y)) * (sinh (y - w))) is V11() real ext-real set
((((1 / 2) * (((1 / 2) * ((sinh ((y + z) + (z - y))) - (sinh ((y + z) - (z - y))))) - ((cosh (y - z)) * (sinh (z - y))))) + (((sinh z) * (sinh w)) * (sinh (w - z)))) + (((sinh w) * (sinh y)) * (sinh (y - w)))) + (((sinh (z - y)) * (sinh (w - z))) * (sinh (y - w))) is V11() real ext-real set
2 * z is V11() real ext-real set
sinh (2 * z) is V11() real ext-real Element of REAL
y + y is V11() real ext-real set
sinh (y + y) is V11() real ext-real Element of REAL
(sinh (2 * z)) - (sinh (y + y)) is V11() real ext-real set
(1 / 2) * ((sinh (2 * z)) - (sinh (y + y))) is V11() real ext-real set
- (y - z) is V11() real ext-real set
(y - z) + (- (y - z)) is V11() real ext-real set
sinh ((y - z) + (- (y - z))) is V11() real ext-real Element of REAL
(y - z) - (z - y) is V11() real ext-real set
sinh ((y - z) - (z - y)) is V11() real ext-real Element of REAL
(sinh ((y - z) + (- (y - z)))) - (sinh ((y - z) - (z - y))) is V11() real ext-real set
(1 / 2) * ((sinh ((y - z) + (- (y - z)))) - (sinh ((y - z) - (z - y)))) is V11() real ext-real set
((1 / 2) * ((sinh (2 * z)) - (sinh (y + y)))) - ((1 / 2) * ((sinh ((y - z) + (- (y - z)))) - (sinh ((y - z) - (z - y))))) is V11() real ext-real set
(1 / 2) * (((1 / 2) * ((sinh (2 * z)) - (sinh (y + y)))) - ((1 / 2) * ((sinh ((y - z) + (- (y - z)))) - (sinh ((y - z) - (z - y)))))) is V11() real ext-real set
((1 / 2) * (((1 / 2) * ((sinh (2 * z)) - (sinh (y + y)))) - ((1 / 2) * ((sinh ((y - z) + (- (y - z)))) - (sinh ((y - z) - (z - y))))))) + (((sinh z) * (sinh w)) * (sinh (w - z))) is V11() real ext-real set
(((1 / 2) * (((1 / 2) * ((sinh (2 * z)) - (sinh (y + y)))) - ((1 / 2) * ((sinh ((y - z) + (- (y - z)))) - (sinh ((y - z) - (z - y))))))) + (((sinh z) * (sinh w)) * (sinh (w - z)))) + (((sinh w) * (sinh y)) * (sinh (y - w))) is V11() real ext-real set
((((1 / 2) * (((1 / 2) * ((sinh (2 * z)) - (sinh (y + y)))) - ((1 / 2) * ((sinh ((y - z) + (- (y - z)))) - (sinh ((y - z) - (z - y))))))) + (((sinh z) * (sinh w)) * (sinh (w - z)))) + (((sinh w) * (sinh y)) * (sinh (y - w)))) + (((sinh (z - y)) * (sinh (w - z))) * (sinh (y - w))) is V11() real ext-real set
2 * y is V11() real ext-real set
sinh (2 * y) is V11() real ext-real Element of REAL
(sinh (2 * z)) - (sinh (2 * y)) is V11() real ext-real set
(1 / 2) * ((sinh (2 * z)) - (sinh (2 * y))) is V11() real ext-real set
2 * (y - z) is V11() real ext-real set
sinh (2 * (y - z)) is V11() real ext-real Element of REAL
(sinh . 0) - (sinh (2 * (y - z))) is V11() real ext-real set
(1 / 2) * ((sinh . 0) - (sinh (2 * (y - z)))) is V11() real ext-real set
((1 / 2) * ((sinh (2 * z)) - (sinh (2 * y)))) - ((1 / 2) * ((sinh . 0) - (sinh (2 * (y - z))))) is V11() real ext-real set
(1 / 2) * (((1 / 2) * ((sinh (2 * z)) - (sinh (2 * y)))) - ((1 / 2) * ((sinh . 0) - (sinh (2 * (y - z)))))) is V11() real ext-real set
((1 / 2) * (((1 / 2) * ((sinh (2 * z)) - (sinh (2 * y)))) - ((1 / 2) * ((sinh . 0) - (sinh (2 * (y - z))))))) + (((sinh z) * (sinh w)) * (sinh (w - z))) is V11() real ext-real set
(((1 / 2) * (((1 / 2) * ((sinh (2 * z)) - (sinh (2 * y)))) - ((1 / 2) * ((sinh . 0) - (sinh (2 * (y - z))))))) + (((sinh z) * (sinh w)) * (sinh (w - z)))) + (((sinh w) * (sinh y)) * (sinh (y - w))) is V11() real ext-real set
((((1 / 2) * (((1 / 2) * ((sinh (2 * z)) - (sinh (2 * y)))) - ((1 / 2) * ((sinh . 0) - (sinh (2 * (y - z))))))) + (((sinh z) * (sinh w)) * (sinh (w - z)))) + (((sinh w) * (sinh y)) * (sinh (y - w)))) + (((sinh (z - y)) * (sinh (w - z))) * (sinh (y - w))) is V11() real ext-real set
- (sinh (2 * (y - z))) is V11() real ext-real set
((sinh (2 * z)) - (sinh (2 * y))) - (- (sinh (2 * (y - z)))) is V11() real ext-real set
(1 / 2) * (((sinh (2 * z)) - (sinh (2 * y))) - (- (sinh (2 * (y - z))))) is V11() real ext-real set
(1 / 2) * ((1 / 2) * (((sinh (2 * z)) - (sinh (2 * y))) - (- (sinh (2 * (y - z)))))) is V11() real ext-real set
z + w is V11() real ext-real set
cosh (z + w) is V11() real ext-real Element of REAL
z - w is V11() real ext-real set
cosh (z - w) is V11() real ext-real Element of REAL
(cosh (z + w)) - (cosh (z - w)) is V11() real ext-real set
(1 / 2) * ((cosh (z + w)) - (cosh (z - w))) is V11() real ext-real set
((1 / 2) * ((cosh (z + w)) - (cosh (z - w)))) * (sinh (w - z)) is V11() real ext-real set
((1 / 2) * ((1 / 2) * (((sinh (2 * z)) - (sinh (2 * y))) - (- (sinh (2 * (y - z))))))) + (((1 / 2) * ((cosh (z + w)) - (cosh (z - w)))) * (sinh (w - z))) is V11() real ext-real set
(((1 / 2) * ((1 / 2) * (((sinh (2 * z)) - (sinh (2 * y))) - (- (sinh (2 * (y - z))))))) + (((1 / 2) * ((cosh (z + w)) - (cosh (z - w)))) * (sinh (w - z)))) + (((sinh w) * (sinh y)) * (sinh (y - w))) is V11() real ext-real set
((((1 / 2) * ((1 / 2) * (((sinh (2 * z)) - (sinh (2 * y))) - (- (sinh (2 * (y - z))))))) + (((1 / 2) * ((cosh (z + w)) - (cosh (z - w)))) * (sinh (w - z)))) + (((sinh w) * (sinh y)) * (sinh (y - w)))) + (((sinh (z - y)) * (sinh (w - z))) * (sinh (y - w))) is V11() real ext-real set
(cosh (z + w)) * (sinh (w - z)) is V11() real ext-real set
(cosh (z - w)) * (sinh (w - z)) is V11() real ext-real set
((cosh (z + w)) * (sinh (w - z))) - ((cosh (z - w)) * (sinh (w - z))) is V11() real ext-real set
((1 / 2) * (((sinh (2 * z)) - (sinh (2 * y))) - (- (sinh (2 * (y - z)))))) + (((cosh (z + w)) * (sinh (w - z))) - ((cosh (z - w)) * (sinh (w - z)))) is V11() real ext-real set
(1 / 2) * (((1 / 2) * (((sinh (2 * z)) - (sinh (2 * y))) - (- (sinh (2 * (y - z)))))) + (((cosh (z + w)) * (sinh (w - z))) - ((cosh (z - w)) * (sinh (w - z))))) is V11() real ext-real set
((1 / 2) * (((1 / 2) * (((sinh (2 * z)) - (sinh (2 * y))) - (- (sinh (2 * (y - z)))))) + (((cosh (z + w)) * (sinh (w - z))) - ((cosh (z - w)) * (sinh (w - z)))))) + (((sinh w) * (sinh y)) * (sinh (y - w))) is V11() real ext-real set
(((1 / 2) * (((1 / 2) * (((sinh (2 * z)) - (sinh (2 * y))) - (- (sinh (2 * (y - z)))))) + (((cosh (z + w)) * (sinh (w - z))) - ((cosh (z - w)) * (sinh (w - z)))))) + (((sinh w) * (sinh y)) * (sinh (y - w)))) + (((sinh (z - y)) * (sinh (w - z))) * (sinh (y - w))) is V11() real ext-real set
(z + w) + (w - z) is V11() real ext-real set
sinh ((z + w) + (w - z)) is V11() real ext-real Element of REAL
(z + w) - (w - z) is V11() real ext-real set
sinh ((z + w) - (w - z)) is V11() real ext-real Element of REAL
(sinh ((z + w) + (w - z))) - (sinh ((z + w) - (w - z))) is V11() real ext-real set
(1 / 2) * ((sinh ((z + w) + (w - z))) - (sinh ((z + w) - (w - z)))) is V11() real ext-real set
((1 / 2) * ((sinh ((z + w) + (w - z))) - (sinh ((z + w) - (w - z))))) - ((cosh (z - w)) * (sinh (w - z))) is V11() real ext-real set
((1 / 2) * (((sinh (2 * z)) - (sinh (2 * y))) - (- (sinh (2 * (y - z)))))) + (((1 / 2) * ((sinh ((z + w) + (w - z))) - (sinh ((z + w) - (w - z))))) - ((cosh (z - w)) * (sinh (w - z)))) is V11() real ext-real set
(1 / 2) * (((1 / 2) * (((sinh (2 * z)) - (sinh (2 * y))) - (- (sinh (2 * (y - z)))))) + (((1 / 2) * ((sinh ((z + w) + (w - z))) - (sinh ((z + w) - (w - z))))) - ((cosh (z - w)) * (sinh (w - z))))) is V11() real ext-real set
((1 / 2) * (((1 / 2) * (((sinh (2 * z)) - (sinh (2 * y))) - (- (sinh (2 * (y - z)))))) + (((1 / 2) * ((sinh ((z + w) + (w - z))) - (sinh ((z + w) - (w - z))))) - ((cosh (z - w)) * (sinh (w - z)))))) + (((sinh w) * (sinh y)) * (sinh (y - w))) is V11() real ext-real set
(((1 / 2) * (((1 / 2) * (((sinh (2 * z)) - (sinh (2 * y))) - (- (sinh (2 * (y - z)))))) + (((1 / 2) * ((sinh ((z + w) + (w - z))) - (sinh ((z + w) - (w - z))))) - ((cosh (z - w)) * (sinh (w - z)))))) + (((sinh w) * (sinh y)) * (sinh (y - w)))) + (((sinh (z - y)) * (sinh (w - z))) * (sinh (y - w))) is V11() real ext-real set
2 * w is V11() real ext-real set
sinh (2 * w) is V11() real ext-real Element of REAL
(sinh (2 * w)) - (sinh (2 * z)) is V11() real ext-real set
(1 / 2) * ((sinh (2 * w)) - (sinh (2 * z))) is V11() real ext-real set
(z - w) + (w - z) is V11() real ext-real set
sinh ((z - w) + (w - z)) is V11() real ext-real Element of REAL
(z - w) - (w - z) is V11() real ext-real set
sinh ((z - w) - (w - z)) is V11() real ext-real Element of REAL
(sinh ((z - w) + (w - z))) - (sinh ((z - w) - (w - z))) is V11() real ext-real set
(1 / 2) * ((sinh ((z - w) + (w - z))) - (sinh ((z - w) - (w - z)))) is V11() real ext-real set
((1 / 2) * ((sinh (2 * w)) - (sinh (2 * z)))) - ((1 / 2) * ((sinh ((z - w) + (w - z))) - (sinh ((z - w) - (w - z))))) is V11() real ext-real set
((1 / 2) * (((sinh (2 * z)) - (sinh (2 * y))) - (- (sinh (2 * (y - z)))))) + (((1 / 2) * ((sinh (2 * w)) - (sinh (2 * z)))) - ((1 / 2) * ((sinh ((z - w) + (w - z))) - (sinh ((z - w) - (w - z)))))) is V11() real ext-real set
(1 / 2) * (((1 / 2) * (((sinh (2 * z)) - (sinh (2 * y))) - (- (sinh (2 * (y - z)))))) + (((1 / 2) * ((sinh (2 * w)) - (sinh (2 * z)))) - ((1 / 2) * ((sinh ((z - w) + (w - z))) - (sinh ((z - w) - (w - z))))))) is V11() real ext-real set
((1 / 2) * (((1 / 2) * (((sinh (2 * z)) - (sinh (2 * y))) - (- (sinh (2 * (y - z)))))) + (((1 / 2) * ((sinh (2 * w)) - (sinh (2 * z)))) - ((1 / 2) * ((sinh ((z - w) + (w - z))) - (sinh ((z - w) - (w - z)))))))) + (((sinh w) * (sinh y)) * (sinh (y - w))) is V11() real ext-real set
(((1 / 2) * (((1 / 2) * (((sinh (2 * z)) - (sinh (2 * y))) - (- (sinh (2 * (y - z)))))) + (((1 / 2) * ((sinh (2 * w)) - (sinh (2 * z)))) - ((1 / 2) * ((sinh ((z - w) + (w - z))) - (sinh ((z - w) - (w - z)))))))) + (((sinh w) * (sinh y)) * (sinh (y - w)))) + (((sinh (z - y)) * (sinh (w - z))) * (sinh (y - w))) is V11() real ext-real set
0 - (sinh ((z - w) - (w - z))) is V11() real ext-real set
(1 / 2) * (0 - (sinh ((z - w) - (w - z)))) is V11() real ext-real set
((1 / 2) * ((sinh (2 * w)) - (sinh (2 * z)))) - ((1 / 2) * (0 - (sinh ((z - w) - (w - z))))) is V11() real ext-real set
((1 / 2) * (((sinh (2 * z)) - (sinh (2 * y))) - (- (sinh (2 * (y - z)))))) + (((1 / 2) * ((sinh (2 * w)) - (sinh (2 * z)))) - ((1 / 2) * (0 - (sinh ((z - w) - (w - z)))))) is V11() real ext-real set
(1 / 2) * (((1 / 2) * (((sinh (2 * z)) - (sinh (2 * y))) - (- (sinh (2 * (y - z)))))) + (((1 / 2) * ((sinh (2 * w)) - (sinh (2 * z)))) - ((1 / 2) * (0 - (sinh ((z - w) - (w - z))))))) is V11() real ext-real set
((1 / 2) * (((1 / 2) * (((sinh (2 * z)) - (sinh (2 * y))) - (- (sinh (2 * (y - z)))))) + (((1 / 2) * ((sinh (2 * w)) - (sinh (2 * z)))) - ((1 / 2) * (0 - (sinh ((z - w) - (w - z)))))))) + (((sinh w) * (sinh y)) * (sinh (y - w))) is V11() real ext-real set
(((1 / 2) * (((1 / 2) * (((sinh (2 * z)) - (sinh (2 * y))) - (- (sinh (2 * (y - z)))))) + (((1 / 2) * ((sinh (2 * w)) - (sinh (2 * z)))) - ((1 / 2) * (0 - (sinh ((z - w) - (w - z)))))))) + (((sinh w) * (sinh y)) * (sinh (y - w)))) + (((sinh (z - y)) * (sinh (w - z))) * (sinh (y - w))) is V11() real ext-real set
2 * (z - w) is V11() real ext-real set
sinh (2 * (z - w)) is V11() real ext-real Element of REAL
- (sinh (2 * (z - w))) is V11() real ext-real set
((sinh (2 * w)) - (sinh (2 * z))) - (- (sinh (2 * (z - w)))) is V11() real ext-real set
(((sinh (2 * z)) - (sinh (2 * y))) - (- (sinh (2 * (y - z))))) + (((sinh (2 * w)) - (sinh (2 * z))) - (- (sinh (2 * (z - w))))) is V11() real ext-real set
(1 / 2) * ((((sinh (2 * z)) - (sinh (2 * y))) - (- (sinh (2 * (y - z))))) + (((sinh (2 * w)) - (sinh (2 * z))) - (- (sinh (2 * (z - w)))))) is V11() real ext-real set
(1 / 2) * ((1 / 2) * ((((sinh (2 * z)) - (sinh (2 * y))) - (- (sinh (2 * (y - z))))) + (((sinh (2 * w)) - (sinh (2 * z))) - (- (sinh (2 * (z - w))))))) is V11() real ext-real set
w + y is V11() real ext-real set
cosh (w + y) is V11() real ext-real Element of REAL
w - y is V11() real ext-real set
cosh (w - y) is V11() real ext-real Element of REAL
(cosh (w + y)) - (cosh (w - y)) is V11() real ext-real set
(1 / 2) * ((cosh (w + y)) - (cosh (w - y))) is V11() real ext-real set
((1 / 2) * ((cosh (w + y)) - (cosh (w - y)))) * (sinh (y - w)) is V11() real ext-real set
((1 / 2) * ((1 / 2) * ((((sinh (2 * z)) - (sinh (2 * y))) - (- (sinh (2 * (y - z))))) + (((sinh (2 * w)) - (sinh (2 * z))) - (- (sinh (2 * (z - w)))))))) + (((1 / 2) * ((cosh (w + y)) - (cosh (w - y)))) * (sinh (y - w))) is V11() real ext-real set
(((1 / 2) * ((1 / 2) * ((((sinh (2 * z)) - (sinh (2 * y))) - (- (sinh (2 * (y - z))))) + (((sinh (2 * w)) - (sinh (2 * z))) - (- (sinh (2 * (z - w)))))))) + (((1 / 2) * ((cosh (w + y)) - (cosh (w - y)))) * (sinh (y - w)))) + (((sinh (z - y)) * (sinh (w - z))) * (sinh (y - w))) is V11() real ext-real set
(cosh (w + y)) * (sinh (y - w)) is V11() real ext-real set
(cosh (w - y)) * (sinh (y - w)) is V11() real ext-real set
((cosh (w + y)) * (sinh (y - w))) - ((cosh (w - y)) * (sinh (y - w))) is V11() real ext-real set
((1 / 2) * ((((sinh (2 * z)) - (sinh (2 * y))) - (- (sinh (2 * (y - z))))) + (((sinh (2 * w)) - (sinh (2 * z))) - (- (sinh (2 * (z - w))))))) + (((cosh (w + y)) * (sinh (y - w))) - ((cosh (w - y)) * (sinh (y - w)))) is V11() real ext-real set
(1 / 2) * (((1 / 2) * ((((sinh (2 * z)) - (sinh (2 * y))) - (- (sinh (2 * (y - z))))) + (((sinh (2 * w)) - (sinh (2 * z))) - (- (sinh (2 * (z - w))))))) + (((cosh (w + y)) * (sinh (y - w))) - ((cosh (w - y)) * (sinh (y - w))))) is V11() real ext-real set
((1 / 2) * (((1 / 2) * ((((sinh (2 * z)) - (sinh (2 * y))) - (- (sinh (2 * (y - z))))) + (((sinh (2 * w)) - (sinh (2 * z))) - (- (sinh (2 * (z - w))))))) + (((cosh (w + y)) * (sinh (y - w))) - ((cosh (w - y)) * (sinh (y - w)))))) + (((sinh (z - y)) * (sinh (w - z))) * (sinh (y - w))) is V11() real ext-real set
(w + y) + (y - w) is V11() real ext-real set
sinh ((w + y) + (y - w)) is V11() real ext-real Element of REAL
(w + y) - (y - w) is V11() real ext-real set
sinh ((w + y) - (y - w)) is V11() real ext-real Element of REAL
(sinh ((w + y) + (y - w))) - (sinh ((w + y) - (y - w))) is V11() real ext-real set
(1 / 2) * ((sinh ((w + y) + (y - w))) - (sinh ((w + y) - (y - w)))) is V11() real ext-real set
((1 / 2) * ((sinh ((w + y) + (y - w))) - (sinh ((w + y) - (y - w))))) - ((cosh (w - y)) * (sinh (y - w))) is V11() real ext-real set
((1 / 2) * ((((sinh (2 * z)) - (sinh (2 * y))) - (- (sinh (2 * (y - z))))) + (((sinh (2 * w)) - (sinh (2 * z))) - (- (sinh (2 * (z - w))))))) + (((1 / 2) * ((sinh ((w + y) + (y - w))) - (sinh ((w + y) - (y - w))))) - ((cosh (w - y)) * (sinh (y - w)))) is V11() real ext-real set
(1 / 2) * (((1 / 2) * ((((sinh (2 * z)) - (sinh (2 * y))) - (- (sinh (2 * (y - z))))) + (((sinh (2 * w)) - (sinh (2 * z))) - (- (sinh (2 * (z - w))))))) + (((1 / 2) * ((sinh ((w + y) + (y - w))) - (sinh ((w + y) - (y - w))))) - ((cosh (w - y)) * (sinh (y - w))))) is V11() real ext-real set
((1 / 2) * (((1 / 2) * ((((sinh (2 * z)) - (sinh (2 * y))) - (- (sinh (2 * (y - z))))) + (((sinh (2 * w)) - (sinh (2 * z))) - (- (sinh (2 * (z - w))))))) + (((1 / 2) * ((sinh ((w + y) + (y - w))) - (sinh ((w + y) - (y - w))))) - ((cosh (w - y)) * (sinh (y - w)))))) + (((sinh (z - y)) * (sinh (w - z))) * (sinh (y - w))) is V11() real ext-real set
(sinh (2 * y)) - (sinh (2 * w)) is V11() real ext-real set
(1 / 2) * ((sinh (2 * y)) - (sinh (2 * w))) is V11() real ext-real set
- (w - y) is V11() real ext-real set
(w - y) + (- (w - y)) is V11() real ext-real set
sinh ((w - y) + (- (w - y))) is V11() real ext-real Element of REAL
(w - y) - (- (w - y)) is V11() real ext-real set
sinh ((w - y) - (- (w - y))) is V11() real ext-real Element of REAL
(sinh ((w - y) + (- (w - y)))) - (sinh ((w - y) - (- (w - y)))) is V11() real ext-real set
(1 / 2) * ((sinh ((w - y) + (- (w - y)))) - (sinh ((w - y) - (- (w - y))))) is V11() real ext-real set
((1 / 2) * ((sinh (2 * y)) - (sinh (2 * w)))) - ((1 / 2) * ((sinh ((w - y) + (- (w - y)))) - (sinh ((w - y) - (- (w - y)))))) is V11() real ext-real set
((1 / 2) * ((((sinh (2 * z)) - (sinh (2 * y))) - (- (sinh (2 * (y - z))))) + (((sinh (2 * w)) - (sinh (2 * z))) - (- (sinh (2 * (z - w))))))) + (((1 / 2) * ((sinh (2 * y)) - (sinh (2 * w)))) - ((1 / 2) * ((sinh ((w - y) + (- (w - y)))) - (sinh ((w - y) - (- (w - y))))))) is V11() real ext-real set
(1 / 2) * (((1 / 2) * ((((sinh (2 * z)) - (sinh (2 * y))) - (- (sinh (2 * (y - z))))) + (((sinh (2 * w)) - (sinh (2 * z))) - (- (sinh (2 * (z - w))))))) + (((1 / 2) * ((sinh (2 * y)) - (sinh (2 * w)))) - ((1 / 2) * ((sinh ((w - y) + (- (w - y)))) - (sinh ((w - y) - (- (w - y)))))))) is V11() real ext-real set
((1 / 2) * (((1 / 2) * ((((sinh (2 * z)) - (sinh (2 * y))) - (- (sinh (2 * (y - z))))) + (((sinh (2 * w)) - (sinh (2 * z))) - (- (sinh (2 * (z - w))))))) + (((1 / 2) * ((sinh (2 * y)) - (sinh (2 * w)))) - ((1 / 2) * ((sinh ((w - y) + (- (w - y)))) - (sinh ((w - y) - (- (w - y))))))))) + (((sinh (z - y)) * (sinh (w - z))) * (sinh (y - w))) is V11() real ext-real set
2 * (w - y) is V11() real ext-real set
sinh (2 * (w - y)) is V11() real ext-real Element of REAL
0 - (sinh (2 * (w - y))) is V11() real ext-real set
(1 / 2) * (0 - (sinh (2 * (w - y)))) is V11() real ext-real set
((1 / 2) * ((sinh (2 * y)) - (sinh (2 * w)))) - ((1 / 2) * (0 - (sinh (2 * (w - y))))) is V11() real ext-real set
((1 / 2) * ((((sinh (2 * z)) - (sinh (2 * y))) - (- (sinh (2 * (y - z))))) + (((sinh (2 * w)) - (sinh (2 * z))) - (- (sinh (2 * (z - w))))))) + (((1 / 2) * ((sinh (2 * y)) - (sinh (2 * w)))) - ((1 / 2) * (0 - (sinh (2 * (w - y)))))) is V11() real ext-real set
(1 / 2) * (((1 / 2) * ((((sinh (2 * z)) - (sinh (2 * y))) - (- (sinh (2 * (y - z))))) + (((sinh (2 * w)) - (sinh (2 * z))) - (- (sinh (2 * (z - w))))))) + (((1 / 2) * ((sinh (2 * y)) - (sinh (2 * w)))) - ((1 / 2) * (0 - (sinh (2 * (w - y))))))) is V11() real ext-real set
((1 / 2) * (((1 / 2) * ((((sinh (2 * z)) - (sinh (2 * y))) - (- (sinh (2 * (y - z))))) + (((sinh (2 * w)) - (sinh (2 * z))) - (- (sinh (2 * (z - w))))))) + (((1 / 2) * ((sinh (2 * y)) - (sinh (2 * w)))) - ((1 / 2) * (0 - (sinh (2 * (w - y)))))))) + (((sinh (z - y)) * (sinh (w - z))) * (sinh (y - w))) is V11() real ext-real set
(sinh (2 * (y - z))) + (sinh (2 * (z - w))) is V11() real ext-real set
((sinh (2 * (y - z))) + (sinh (2 * (z - w)))) + (sinh (2 * (w - y))) is V11() real ext-real set
(1 / 2) * (((sinh (2 * (y - z))) + (sinh (2 * (z - w)))) + (sinh (2 * (w - y)))) is V11() real ext-real set
(1 / 2) * ((1 / 2) * (((sinh (2 * (y - z))) + (sinh (2 * (z - w)))) + (sinh (2 * (w - y))))) is V11() real ext-real set
- (z - w) is V11() real ext-real set
(z - y) + (- (z - w)) is V11() real ext-real set
cosh ((z - y) + (- (z - w))) is V11() real ext-real Element of REAL
(z - y) - (w - z) is V11() real ext-real set
cosh ((z - y) - (w - z)) is V11() real ext-real Element of REAL
(cosh ((z - y) + (- (z - w)))) - (cosh ((z - y) - (w - z))) is V11() real ext-real set
(1 / 2) * ((cosh ((z - y) + (- (z - w)))) - (cosh ((z - y) - (w - z)))) is V11() real ext-real set
((1 / 2) * ((cosh ((z - y) + (- (z - w)))) - (cosh ((z - y) - (w - z))))) * (sinh (y - w)) is V11() real ext-real set
((1 / 2) * ((1 / 2) * (((sinh (2 * (y - z))) + (sinh (2 * (z - w)))) + (sinh (2 * (w - y)))))) + (((1 / 2) * ((cosh ((z - y) + (- (z - w)))) - (cosh ((z - y) - (w - z))))) * (sinh (y - w))) is V11() real ext-real set
(cosh ((z - y) - (w - z))) * (sinh (y - w)) is V11() real ext-real set
((cosh (w - y)) * (sinh (y - w))) - ((cosh ((z - y) - (w - z))) * (sinh (y - w))) is V11() real ext-real set
((1 / 2) * (((sinh (2 * (y - z))) + (sinh (2 * (z - w)))) + (sinh (2 * (w - y))))) + (((cosh (w - y)) * (sinh (y - w))) - ((cosh ((z - y) - (w - z))) * (sinh (y - w)))) is V11() real ext-real set
(1 / 2) * (((1 / 2) * (((sinh (2 * (y - z))) + (sinh (2 * (z - w)))) + (sinh (2 * (w - y))))) + (((cosh (w - y)) * (sinh (y - w))) - ((cosh ((z - y) - (w - z))) * (sinh (y - w))))) is V11() real ext-real set
(w - y) - (y - w) is V11() real ext-real set
sinh ((w - y) - (y - w)) is V11() real ext-real Element of REAL
(sinh ((w - y) + (- (w - y)))) - (sinh ((w - y) - (y - w))) is V11() real ext-real set
(1 / 2) * ((sinh ((w - y) + (- (w - y)))) - (sinh ((w - y) - (y - w)))) is V11() real ext-real set
((1 / 2) * ((sinh ((w - y) + (- (w - y)))) - (sinh ((w - y) - (y - w))))) - ((cosh ((z - y) - (w - z))) * (sinh (y - w))) is V11() real ext-real set
((1 / 2) * (((sinh (2 * (y - z))) + (sinh (2 * (z - w)))) + (sinh (2 * (w - y))))) + (((1 / 2) * ((sinh ((w - y) + (- (w - y)))) - (sinh ((w - y) - (y - w))))) - ((cosh ((z - y) - (w - z))) * (sinh (y - w)))) is V11() real ext-real set
(1 / 2) * (((1 / 2) * (((sinh (2 * (y - z))) + (sinh (2 * (z - w)))) + (sinh (2 * (w - y))))) + (((1 / 2) * ((sinh ((w - y) + (- (w - y)))) - (sinh ((w - y) - (y - w))))) - ((cosh ((z - y) - (w - z))) * (sinh (y - w))))) is V11() real ext-real set
0 - (sinh ((w - y) - (y - w))) is V11() real ext-real set
(1 / 2) * (0 - (sinh ((w - y) - (y - w)))) is V11() real ext-real set
((1 / 2) * (0 - (sinh ((w - y) - (y - w))))) - ((cosh ((z - y) - (w - z))) * (sinh (y - w))) is V11() real ext-real set
((1 / 2) * (((sinh (2 * (y - z))) + (sinh (2 * (z - w)))) + (sinh (2 * (w - y))))) + (((1 / 2) * (0 - (sinh ((w - y) - (y - w))))) - ((cosh ((z - y) - (w - z))) * (sinh (y - w)))) is V11() real ext-real set
(1 / 2) * (((1 / 2) * (((sinh (2 * (y - z))) + (sinh (2 * (z - w)))) + (sinh (2 * (w - y))))) + (((1 / 2) * (0 - (sinh ((w - y) - (y - w))))) - ((cosh ((z - y) - (w - z))) * (sinh (y - w))))) is V11() real ext-real set
- (sinh (2 * (w - y))) is V11() real ext-real set
(1 / 2) * (- (sinh (2 * (w - y)))) is V11() real ext-real set
(z - y) + (z - w) is V11() real ext-real set
((z - y) + (z - w)) + (y - w) is V11() real ext-real set
sinh (((z - y) + (z - w)) + (y - w)) is V11() real ext-real Element of REAL
((z - y) + (z - w)) - (y - w) is V11() real ext-real set
sinh (((z - y) + (z - w)) - (y - w)) is V11() real ext-real Element of REAL
(sinh (((z - y) + (z - w)) + (y - w))) - (sinh (((z - y) + (z - w)) - (y - w))) is V11() real ext-real set
(1 / 2) * ((sinh (((z - y) + (z - w)) + (y - w))) - (sinh (((z - y) + (z - w)) - (y - w)))) is V11() real ext-real set
((1 / 2) * (- (sinh (2 * (w - y))))) - ((1 / 2) * ((sinh (((z - y) + (z - w)) + (y - w))) - (sinh (((z - y) + (z - w)) - (y - w))))) is V11() real ext-real set
((1 / 2) * (((sinh (2 * (y - z))) + (sinh (2 * (z - w)))) + (sinh (2 * (w - y))))) + (((1 / 2) * (- (sinh (2 * (w - y))))) - ((1 / 2) * ((sinh (((z - y) + (z - w)) + (y - w))) - (sinh (((z - y) + (z - w)) - (y - w)))))) is V11() real ext-real set
(1 / 2) * (((1 / 2) * (((sinh (2 * (y - z))) + (sinh (2 * (z - w)))) + (sinh (2 * (w - y))))) + (((1 / 2) * (- (sinh (2 * (w - y))))) - ((1 / 2) * ((sinh (((z - y) + (z - w)) + (y - w))) - (sinh (((z - y) + (z - w)) - (y - w))))))) is V11() real ext-real set
- (2 * (y - z)) is V11() real ext-real set
sinh (- (2 * (y - z))) is V11() real ext-real Element of REAL
(sinh (- (2 * (y - z)))) - (sinh (2 * (z - w))) is V11() real ext-real set
((sinh (- (2 * (y - z)))) - (sinh (2 * (z - w)))) + (- (sinh (2 * (w - y)))) is V11() real ext-real set
(1 / 2) * (((sinh (- (2 * (y - z)))) - (sinh (2 * (z - w)))) + (- (sinh (2 * (w - y))))) is V11() real ext-real set
((1 / 2) * (((sinh (2 * (y - z))) + (sinh (2 * (z - w)))) + (sinh (2 * (w - y))))) + ((1 / 2) * (((sinh (- (2 * (y - z)))) - (sinh (2 * (z - w)))) + (- (sinh (2 * (w - y)))))) is V11() real ext-real set
(1 / 2) * (((1 / 2) * (((sinh (2 * (y - z))) + (sinh (2 * (z - w)))) + (sinh (2 * (w - y))))) + ((1 / 2) * (((sinh (- (2 * (y - z)))) - (sinh (2 * (z - w)))) + (- (sinh (2 * (w - y))))))) is V11() real ext-real set
(- (sinh (2 * (y - z)))) - (sinh (2 * (z - w))) is V11() real ext-real set
((- (sinh (2 * (y - z)))) - (sinh (2 * (z - w)))) + (- (sinh (2 * (w - y)))) is V11() real ext-real set
(1 / 2) * (((- (sinh (2 * (y - z)))) - (sinh (2 * (z - w)))) + (- (sinh (2 * (w - y))))) is V11() real ext-real set
((1 / 2) * (((sinh (2 * (y - z))) + (sinh (2 * (z - w)))) + (sinh (2 * (w - y))))) + ((1 / 2) * (((- (sinh (2 * (y - z)))) - (sinh (2 * (z - w)))) + (- (sinh (2 * (w - y)))))) is V11() real ext-real set
(1 / 2) * (((1 / 2) * (((sinh (2 * (y - z))) + (sinh (2 * (z - w)))) + (sinh (2 * (w - y))))) + ((1 / 2) * (((- (sinh (2 * (y - z)))) - (sinh (2 * (z - w)))) + (- (sinh (2 * (w - y))))))) is V11() real ext-real set
y is V11() real ext-real set
y / 2 is V11() real ext-real set
sinh (y / 2) is V11() real ext-real Element of REAL
cosh y is V11() real ext-real Element of REAL
(cosh y) - 1 is V11() real ext-real set
((cosh y) - 1) / 2 is V11() real ext-real set
sqrt (((cosh y) - 1) / 2) is V11() real ext-real set
(sinh (y / 2)) ^2 is V11() real ext-real Element of REAL
(sinh (y / 2)) * (sinh (y / 2)) is V11() real ext-real set
sqrt ((sinh (y / 2)) ^2) is V11() real ext-real Element of REAL
sinh . (y / 2) is V11() real ext-real Element of REAL
(sinh . (y / 2)) ^2 is V11() real ext-real Element of REAL
(sinh . (y / 2)) * (sinh . (y / 2)) is V11() real ext-real set
sqrt ((sinh . (y / 2)) ^2) is V11() real ext-real Element of REAL
2 * (y / 2) is V11() real ext-real set
cosh . (2 * (y / 2)) is V11() real ext-real Element of REAL
(cosh . (2 * (y / 2))) - 1 is V11() real ext-real set
(1 / 2) * ((cosh . (2 * (y / 2))) - 1) is V11() real ext-real set
sqrt ((1 / 2) * ((cosh . (2 * (y / 2))) - 1)) is V11() real ext-real set
cosh . y is V11() real ext-real Element of REAL
(cosh . y) - 1 is V11() real ext-real set
((cosh . y) - 1) / 2 is V11() real ext-real set
sqrt (((cosh . y) - 1) / 2) is V11() real ext-real set
y is V11() real ext-real set
y / 2 is V11() real ext-real set
sinh (y / 2) is V11() real ext-real Element of REAL
cosh y is V11() real ext-real Element of REAL
(cosh y) - 1 is V11() real ext-real set
((cosh y) - 1) / 2 is V11() real ext-real set
sqrt (((cosh y) - 1) / 2) is V11() real ext-real set
- (sqrt (((cosh y) - 1) / 2)) is V11() real ext-real set
- (sinh (y / 2)) is V11() real ext-real set
- (- (sinh (y / 2))) is V11() real ext-real set
(sinh (y / 2)) ^2 is V11() real ext-real Element of REAL
(sinh (y / 2)) * (sinh (y / 2)) is V11() real ext-real set
sqrt ((sinh (y / 2)) ^2) is V11() real ext-real Element of REAL
- (sqrt ((sinh (y / 2)) ^2)) is V11() real ext-real set
sinh . (y / 2) is V11() real ext-real Element of REAL
(sinh . (y / 2)) ^2 is V11() real ext-real Element of REAL
(sinh . (y / 2)) * (sinh . (y / 2)) is V11() real ext-real set
sqrt ((sinh . (y / 2)) ^2) is V11() real ext-real Element of REAL
- (sqrt ((sinh . (y / 2)) ^2)) is V11() real ext-real set
2 * (y / 2) is V11() real ext-real set
cosh . (2 * (y / 2)) is V11() real ext-real Element of REAL
(cosh . (2 * (y / 2))) - 1 is V11() real ext-real set
(1 / 2) * ((cosh . (2 * (y / 2))) - 1) is V11() real ext-real set
sqrt ((1 / 2) * ((cosh . (2 * (y / 2))) - 1)) is V11() real ext-real set
- (sqrt ((1 / 2) * ((cosh . (2 * (y / 2))) - 1))) is V11() real ext-real set
cosh . y is V11() real ext-real Element of REAL
(cosh . y) - 1 is V11() real ext-real set
((cosh . y) - 1) / 2 is V11() real ext-real set
sqrt (((cosh . y) - 1) / 2) is V11() real ext-real set
- (sqrt (((cosh . y) - 1) / 2)) is V11() real ext-real set
y is V11() real ext-real set
2 * y is V11() real ext-real set
sinh (2 * y) is V11() real ext-real Element of REAL
sinh y is V11() real ext-real Element of REAL
2 * (sinh y) is V11() real ext-real set
cosh y is V11() real ext-real Element of REAL
(2 * (sinh y)) * (cosh y) is V11() real ext-real set
cosh (2 * y) is V11() real ext-real Element of REAL
(cosh y) ^2 is V11() real ext-real Element of REAL
(cosh y) * (cosh y) is V11() real ext-real set
2 * ((cosh y) ^2) is V11() real ext-real set
(2 * ((cosh y) ^2)) - 1 is V11() real ext-real set
tanh (2 * y) is V11() real ext-real Element of REAL
tanh y is V11() real ext-real Element of REAL
2 * (tanh y) is V11() real ext-real set
(tanh y) ^2 is V11() real ext-real Element of REAL
(tanh y) * (tanh y) is V11() real ext-real set
1 + ((tanh y) ^2) is V11() real ext-real set
(2 * (tanh y)) / (1 + ((tanh y) ^2)) is V11() real ext-real set
cosh . (2 * y) is V11() real ext-real Element of REAL
cosh . y is V11() real ext-real Element of REAL
(cosh . y) ^2 is V11() real ext-real Element of REAL
(cosh . y) * (cosh . y) is V11() real ext-real set
2 * ((cosh . y) ^2) is V11() real ext-real set
(2 * ((cosh . y) ^2)) - 1 is V11() real ext-real set
tanh . (2 * y) is V11() real ext-real Element of REAL
tanh . y is V11() real ext-real Element of REAL
2 * (tanh . y) is V11() real ext-real set
(tanh . y) ^2 is V11() real ext-real Element of REAL
(tanh . y) * (tanh . y) is V11() real ext-real set
1 + ((tanh . y) ^2) is V11() real ext-real set
(2 * (tanh . y)) / (1 + ((tanh . y) ^2)) is V11() real ext-real set
(2 * (tanh y)) / (1 + ((tanh . y) ^2)) is V11() real ext-real set
sinh . (2 * y) is V11() real ext-real Element of REAL
sinh . y is V11() real ext-real Element of REAL
2 * (sinh . y) is V11() real ext-real set
(2 * (sinh . y)) * (cosh . y) is V11() real ext-real set
(2 * (sinh y)) * (cosh . y) is V11() real ext-real set
y is V11() real ext-real set
2 * y is V11() real ext-real set
sinh (2 * y) is V11() real ext-real Element of REAL
tanh y is V11() real ext-real Element of REAL
2 * (tanh y) is V11() real ext-real set
(tanh y) ^2 is V11() real ext-real Element of REAL
(tanh y) * (tanh y) is V11() real ext-real set
1 - ((tanh y) ^2) is V11() real ext-real set
(2 * (tanh y)) / (1 - ((tanh y) ^2)) is V11() real ext-real set
3 * y is V11() real ext-real set
sinh (3 * y) is V11() real ext-real Element of REAL
sinh y is V11() real ext-real Element of REAL
cosh y is V11() real ext-real Element of REAL
(cosh y) ^2 is V11() real ext-real Element of REAL
(cosh y) * (cosh y) is V11() real ext-real set
4 * ((cosh y) ^2) is V11() real ext-real set
(4 * ((cosh y) ^2)) - 1 is V11() real ext-real set
(sinh y) * ((4 * ((cosh y) ^2)) - 1) is V11() real ext-real set
3 * (sinh y) is V11() real ext-real set
2 * (sinh y) is V11() real ext-real set
cosh (2 * y) is V11() real ext-real Element of REAL
1 - (cosh (2 * y)) is V11() real ext-real set
(2 * (sinh y)) * (1 - (cosh (2 * y))) is V11() real ext-real set
(3 * (sinh y)) - ((2 * (sinh y)) * (1 - (cosh (2 * y)))) is V11() real ext-real set
(sinh y) ^2 is V11() real ext-real Element of REAL
(sinh y) * (sinh y) is V11() real ext-real set
2 * ((sinh y) ^2) is V11() real ext-real set
1 + (2 * ((sinh y) ^2)) is V11() real ext-real set
((cosh y) ^2) + ((sinh y) ^2) is V11() real ext-real set
1 + ((tanh y) ^2) is V11() real ext-real set
(1 + ((tanh y) ^2)) / (1 - ((tanh y) ^2)) is V11() real ext-real set
cosh (3 * y) is V11() real ext-real Element of REAL
4 * ((sinh y) ^2) is V11() real ext-real set
(4 * ((sinh y) ^2)) + 1 is V11() real ext-real set
(cosh y) * ((4 * ((sinh y) ^2)) + 1) is V11() real ext-real set
tanh (3 * y) is V11() real ext-real Element of REAL
3 * (tanh y) is V11() real ext-real set
(tanh y) |^ 3 is V11() real ext-real Element of REAL
(3 * (tanh y)) + ((tanh y) |^ 3) is V11() real ext-real set
3 * ((tanh y) ^2) is V11() real ext-real set
1 + (3 * ((tanh y) ^2)) is V11() real ext-real set
((3 * (tanh y)) + ((tanh y) |^ 3)) / (1 + (3 * ((tanh y) ^2))) is V11() real ext-real set
(2 * (sinh y)) * (cosh y) is V11() real ext-real set
(cosh y) / (cosh y) is V11() real ext-real set
((2 * (sinh y)) * (cosh y)) * ((cosh y) / (cosh y)) is V11() real ext-real set
((2 * (sinh y)) * (cosh y)) * (cosh y) is V11() real ext-real set
(((2 * (sinh y)) * (cosh y)) * (cosh y)) / (cosh y) is V11() real ext-real set
(2 * (sinh y)) * ((cosh y) * (cosh y)) is V11() real ext-real set
((2 * (sinh y)) * ((cosh y) * (cosh y))) / (cosh y) is V11() real ext-real set
(2 * (sinh y)) / (cosh y) is V11() real ext-real set
((2 * (sinh y)) / (cosh y)) * ((cosh y) * (cosh y)) is V11() real ext-real set
(sinh y) / (cosh y) is V11() real ext-real set
2 * ((sinh y) / (cosh y)) is V11() real ext-real set
(2 * ((sinh y) / (cosh y))) * ((cosh y) * (cosh y)) is V11() real ext-real set
(2 * (tanh y)) * ((cosh y) * (cosh y)) is V11() real ext-real set
1 / ((cosh y) * (cosh y)) is V11() real ext-real set
(2 * (tanh y)) / (1 / ((cosh y) * (cosh y))) is V11() real ext-real set
((cosh y) * (cosh y)) - ((sinh y) ^2) is V11() real ext-real set
(((cosh y) * (cosh y)) - ((sinh y) ^2)) / ((cosh y) * (cosh y)) is V11() real ext-real set
(2 * (tanh y)) / ((((cosh y) * (cosh y)) - ((sinh y) ^2)) / ((cosh y) * (cosh y))) is V11() real ext-real set
((cosh y) * (cosh y)) / ((cosh y) * (cosh y)) is V11() real ext-real set
((sinh y) * (sinh y)) / ((cosh y) * (cosh y)) is V11() real ext-real set
(((cosh y) * (cosh y)) / ((cosh y) * (cosh y))) - (((sinh y) * (sinh y)) / ((cosh y) * (cosh y))) is V11() real ext-real set
(2 * (tanh y)) / ((((cosh y) * (cosh y)) / ((cosh y) * (cosh y))) - (((sinh y) * (sinh y)) / ((cosh y) * (cosh y)))) is V11() real ext-real set
((cosh y) / (cosh y)) * ((cosh y) / (cosh y)) is V11() real ext-real set
(((cosh y) / (cosh y)) * ((cosh y) / (cosh y))) - (((sinh y) * (sinh y)) / ((cosh y) * (cosh y))) is V11() real ext-real set
(2 * (tanh y)) / ((((cosh y) / (cosh y)) * ((cosh y) / (cosh y))) - (((sinh y) * (sinh y)) / ((cosh y) * (cosh y)))) is V11() real ext-real set
1 * ((cosh y) / (cosh y)) is V11() real ext-real set
(1 * ((cosh y) / (cosh y))) - (((sinh y) * (sinh y)) / ((cosh y) * (cosh y))) is V11() real ext-real set
(2 * (tanh y)) / ((1 * ((cosh y) / (cosh y))) - (((sinh y) * (sinh y)) / ((cosh y) * (cosh y)))) is V11() real ext-real set
1 - (((sinh y) * (sinh y)) / ((cosh y) * (cosh y))) is V11() real ext-real set
(2 * (tanh y)) / (1 - (((sinh y) * (sinh y)) / ((cosh y) * (cosh y)))) is V11() real ext-real set
((sinh y) / (cosh y)) * ((sinh y) / (cosh y)) is V11() real ext-real set
1 - (((sinh y) / (cosh y)) * ((sinh y) / (cosh y))) is V11() real ext-real set
(2 * (tanh y)) / (1 - (((sinh y) / (cosh y)) * ((sinh y) / (cosh y)))) is V11() real ext-real set
(tanh y) * ((sinh y) / (cosh y)) is V11() real ext-real set
1 - ((tanh y) * ((sinh y) / (cosh y))) is V11() real ext-real set
(2 * (tanh y)) / (1 - ((tanh y) * ((sinh y) / (cosh y)))) is V11() real ext-real set
2 + 1 is V1() ordinal natural V11() real ext-real positive non negative set
(cosh y) |^ (2 + 1) is V11() real ext-real Element of REAL
4 * ((cosh y) |^ (2 + 1)) is V11() real ext-real set
3 * (cosh y) is V11() real ext-real set
(4 * ((cosh y) |^ (2 + 1))) - (3 * (cosh y)) is V11() real ext-real set
(cosh y) |^ 2 is V11() real ext-real Element of REAL
((cosh y) |^ 2) * (cosh y) is V11() real ext-real set
4 * (((cosh y) |^ 2) * (cosh y)) is V11() real ext-real set
(4 * (((cosh y) |^ 2) * (cosh y))) - (3 * (cosh y)) is V11() real ext-real set
1 + 1 is V1() ordinal natural V11() real ext-real positive non negative set
(cosh y) |^ (1 + 1) is V11() real ext-real Element of REAL
4 * ((cosh y) |^ (1 + 1)) is V11() real ext-real set
(4 * ((cosh y) |^ (1 + 1))) - 3 is V11() real ext-real set
((4 * ((cosh y) |^ (1 + 1))) - 3) * (cosh y) is V11() real ext-real set
(cosh y) |^ 1 is V11() real ext-real Element of REAL
((cosh y) |^ 1) * (cosh y) is V11() real ext-real set
4 * (((cosh y) |^ 1) * (cosh y)) is V11() real ext-real set
(4 * (((cosh y) |^ 1) * (cosh y))) - 3 is V11() real ext-real set
((4 * (((cosh y) |^ 1) * (cosh y))) - 3) * (cosh y) is V11() real ext-real set
((cosh y) ^2) - ((sinh y) ^2) is V11() real ext-real set
(((cosh y) ^2) - ((sinh y) ^2)) + ((sinh y) ^2) is V11() real ext-real set
4 * ((((cosh y) ^2) - ((sinh y) ^2)) + ((sinh y) ^2)) is V11() real ext-real set
(4 * ((((cosh y) ^2) - ((sinh y) ^2)) + ((sinh y) ^2))) - 3 is V11() real ext-real set
((4 * ((((cosh y) ^2) - ((sinh y) ^2)) + ((sinh y) ^2))) - 3) * (cosh y) is V11() real ext-real set
1 + ((sinh y) ^2) is V11() real ext-real set
4 * (1 + ((sinh y) ^2)) is V11() real ext-real set
(4 * (1 + ((sinh y) ^2))) - 3 is V11() real ext-real set
((4 * (1 + ((sinh y) ^2))) - 3) * (cosh y) is V11() real ext-real set
2 * ((((cosh y) ^2) - ((sinh y) ^2)) + ((sinh y) ^2)) is V11() real ext-real set
(2 * ((((cosh y) ^2) - ((sinh y) ^2)) + ((sinh y) ^2))) - 1 is V11() real ext-real set
2 * (1 + ((sinh y) ^2)) is V11() real ext-real set
(2 * (1 + ((sinh y) ^2))) - 1 is V11() real ext-real set
y + y is V11() real ext-real set
(y + y) + y is V11() real ext-real set
tanh ((y + y) + y) is V11() real ext-real Element of REAL
(tanh y) + (tanh y) is V11() real ext-real set
((tanh y) + (tanh y)) + (tanh y) is V11() real ext-real set
((tanh y) * (tanh y)) * (tanh y) is V11() real ext-real set
(((tanh y) + (tanh y)) + (tanh y)) + (((tanh y) * (tanh y)) * (tanh y)) is V11() real ext-real set
1 + ((tanh y) * (tanh y)) is V11() real ext-real set
(1 + ((tanh y) * (tanh y))) + ((tanh y) * (tanh y)) is V11() real ext-real set
((1 + ((tanh y) * (tanh y))) + ((tanh y) * (tanh y))) + ((tanh y) * (tanh y)) is V11() real ext-real set
((((tanh y) + (tanh y)) + (tanh y)) + (((tanh y) * (tanh y)) * (tanh y))) / (((1 + ((tanh y) * (tanh y))) + ((tanh y) * (tanh y))) + ((tanh y) * (tanh y))) is V11() real ext-real set
(tanh y) |^ 1 is V11() real ext-real Element of REAL
((tanh y) |^ 1) * (tanh y) is V11() real ext-real set
(((tanh y) |^ 1) * (tanh y)) * (tanh y) is V11() real ext-real set
(3 * (tanh y)) + ((((tanh y) |^ 1) * (tanh y)) * (tanh y)) is V11() real ext-real set
((3 * (tanh y)) + ((((tanh y) |^ 1) * (tanh y)) * (tanh y))) / (((1 + ((tanh y) * (tanh y))) + ((tanh y) * (tanh y))) + ((tanh y) * (tanh y))) is V11() real ext-real set
(tanh y) |^ (1 + 1) is V11() real ext-real Element of REAL
((tanh y) |^ (1 + 1)) * (tanh y) is V11() real ext-real set
(3 * (tanh y)) + (((tanh y) |^ (1 + 1)) * (tanh y)) is V11() real ext-real set
((3 * (tanh y)) + (((tanh y) |^ (1 + 1)) * (tanh y))) / (((1 + ((tanh y) * (tanh y))) + ((tanh y) * (tanh y))) + ((tanh y) * (tanh y))) is V11() real ext-real set
(1 + 1) + 1 is V1() ordinal natural V11() real ext-real positive non negative set
(tanh y) |^ ((1 + 1) + 1) is V11() real ext-real Element of REAL
(3 * (tanh y)) + ((tanh y) |^ ((1 + 1) + 1)) is V11() real ext-real set
((3 * (tanh y)) + ((tanh y) |^ ((1 + 1) + 1))) / (((1 + ((tanh y) * (tanh y))) + ((tanh y) * (tanh y))) + ((tanh y) * (tanh y))) is V11() real ext-real set
2 * ((cosh y) ^2) is V11() real ext-real set
(2 * ((cosh y) ^2)) - 1 is V11() real ext-real set
(2 * ((cosh y) ^2)) - (((cosh y) ^2) - ((sinh y) ^2)) is V11() real ext-real set
sech y is V11() real ext-real Element of REAL
1 / (sech y) is V11() real ext-real set
(1 / (sech y)) ^2 is V11() real ext-real set
(1 / (sech y)) * (1 / (sech y)) is V11() real ext-real set
((1 / (sech y)) ^2) + ((sinh y) ^2) is V11() real ext-real set
(sech y) ^2 is V11() real ext-real Element of REAL
(sech y) * (sech y) is V11() real ext-real set
1 / ((sech y) ^2) is V11() real ext-real set
1 ^2 is V11() real ext-real Element of REAL
1 * 1 is ordinal natural V11() real ext-real non negative set
((sinh y) ^2) * (1 ^2) is V11() real ext-real set
(1 / ((sech y) ^2)) + (((sinh y) ^2) * (1 ^2)) is V11() real ext-real set
((sinh y) ^2) / ((cosh y) ^2) is V11() real ext-real set
(((sinh y) ^2) / ((cosh y) ^2)) * ((cosh y) ^2) is V11() real ext-real set
(1 / ((sech y) ^2)) + ((((sinh y) ^2) / ((cosh y) ^2)) * ((cosh y) ^2)) is V11() real ext-real set
((sinh y) / (cosh y)) ^2 is V11() real ext-real set
(((sinh y) / (cosh y)) ^2) * ((cosh y) ^2) is V11() real ext-real set
(1 / ((sech y) ^2)) + ((((sinh y) / (cosh y)) ^2) * ((cosh y) ^2)) is V11() real ext-real set
((tanh y) ^2) * ((cosh y) ^2) is V11() real ext-real set
(1 / ((sech y) ^2)) + (((tanh y) ^2) * ((cosh y) ^2)) is V11() real ext-real set
(1 ^2) / ((cosh y) ^2) is V11() real ext-real set
((tanh y) ^2) / ((1 ^2) / ((cosh y) ^2)) is V11() real ext-real set
(1 / ((sech y) ^2)) + (((tanh y) ^2) / ((1 ^2) / ((cosh y) ^2))) is V11() real ext-real set
1 / (cosh y) is V11() real ext-real set
(1 / (cosh y)) ^2 is V11() real ext-real set
(1 / (cosh y)) * (1 / (cosh y)) is V11() real ext-real set
((tanh y) ^2) / ((1 / (cosh y)) ^2) is V11() real ext-real set
(1 / ((sech y) ^2)) + (((tanh y) ^2) / ((1 / (cosh y)) ^2)) is V11() real ext-real set
((tanh y) ^2) / ((sech y) ^2) is V11() real ext-real set
(1 / ((sech y) ^2)) + (((tanh y) ^2) / ((sech y) ^2)) is V11() real ext-real set
((sech y) ^2) + ((tanh y) ^2) is V11() real ext-real set
(((sech y) ^2) + ((tanh y) ^2)) - ((tanh y) ^2) is V11() real ext-real set
(1 + ((tanh y) ^2)) / ((((sech y) ^2) + ((tanh y) ^2)) - ((tanh y) ^2)) is V11() real ext-real set
(sinh y) |^ (2 + 1) is V11() real ext-real Element of REAL
4 * ((sinh y) |^ (2 + 1)) is V11() real ext-real set
(4 * ((sinh y) |^ (2 + 1))) + (3 * (sinh y)) is V11() real ext-real set
(sinh y) |^ 2 is V11() real ext-real Element of REAL
((sinh y) |^ 2) * (sinh y) is V11() real ext-real set
4 * (((sinh y) |^ 2) * (sinh y)) is V11() real ext-real set
(4 * (((sinh y) |^ 2) * (sinh y))) + (3 * (sinh y)) is V11() real ext-real set
(sinh y) |^ (1 + 1) is V11() real ext-real Element of REAL
4 * ((sinh y) |^ (1 + 1)) is V11() real ext-real set
(4 * ((sinh y) |^ (1 + 1))) + 3 is V11() real ext-real set
(sinh y) * ((4 * ((sinh y) |^ (1 + 1))) + 3) is V11() real ext-real set
(sinh y) |^ 1 is V11() real ext-real Element of REAL
((sinh y) |^ 1) * (sinh y) is V11() real ext-real set
4 * (((sinh y) |^ 1) * (sinh y)) is V11() real ext-real set
(4 * (((sinh y) |^ 1) * (sinh y))) + 3 is V11() real ext-real set
(sinh y) * ((4 * (((sinh y) |^ 1) * (sinh y))) + 3) is V11() real ext-real set
((cosh y) ^2) - (((cosh y) ^2) - ((sinh y) ^2)) is V11() real ext-real set
4 * (((cosh y) ^2) - (((cosh y) ^2) - ((sinh y) ^2))) is V11() real ext-real set
(4 * (((cosh y) ^2) - (((cosh y) ^2) - ((sinh y) ^2)))) + 3 is V11() real ext-real set
(sinh y) * ((4 * (((cosh y) ^2) - (((cosh y) ^2) - ((sinh y) ^2)))) + 3) is V11() real ext-real set
((cosh y) ^2) - 1 is V11() real ext-real set
4 * (((cosh y) ^2) - 1) is V11() real ext-real set
(4 * (((cosh y) ^2) - 1)) + 3 is V11() real ext-real set
(sinh y) * ((4 * (((cosh y) ^2) - 1)) + 3) is V11() real ext-real set
(sinh y) * (4 * ((((cosh y) ^2) - ((sinh y) ^2)) + ((sinh y) ^2))) is V11() real ext-real set
((sinh y) * (4 * ((((cosh y) ^2) - ((sinh y) ^2)) + ((sinh y) ^2)))) - (sinh y) is V11() real ext-real set
(sinh y) * (4 * (1 + ((sinh y) ^2))) is V11() real ext-real set
((sinh y) * (4 * (1 + ((sinh y) ^2)))) - (sinh y) is V11() real ext-real set
4 * (sinh y) is V11() real ext-real set
2 * (((cosh y) ^2) - (((cosh y) ^2) - ((sinh y) ^2))) is V11() real ext-real set
(2 * (((cosh y) ^2) - (((cosh y) ^2) - ((sinh y) ^2)))) + (2 * ((sinh y) ^2)) is V11() real ext-real set
(sinh y) * ((2 * (((cosh y) ^2) - (((cosh y) ^2) - ((sinh y) ^2)))) + (2 * ((sinh y) ^2))) is V11() real ext-real set
(4 * (sinh y)) + ((sinh y) * ((2 * (((cosh y) ^2) - (((cosh y) ^2) - ((sinh y) ^2)))) + (2 * ((sinh y) ^2)))) is V11() real ext-real set
((4 * (sinh y)) + ((sinh y) * ((2 * (((cosh y) ^2) - (((cosh y) ^2) - ((sinh y) ^2)))) + (2 * ((sinh y) ^2))))) - (sinh y) is V11() real ext-real set
2 * (((cosh y) ^2) - 1) is V11() real ext-real set
(2 * (((cosh y) ^2) - 1)) + (2 * ((sinh y) ^2)) is V11() real ext-real set
(sinh y) * ((2 * (((cosh y) ^2) - 1)) + (2 * ((sinh y) ^2))) is V11() real ext-real set
(4 * (sinh y)) + ((sinh y) * ((2 * (((cosh y) ^2) - 1)) + (2 * ((sinh y) ^2)))) is V11() real ext-real set
((4 * (sinh y)) + ((sinh y) * ((2 * (((cosh y) ^2) - 1)) + (2 * ((sinh y) ^2))))) - (sinh y) is V11() real ext-real set
((cosh y) * (cosh y)) + ((sinh y) ^2) is V11() real ext-real set
(((cosh y) * (cosh y)) + ((sinh y) ^2)) - 1 is V11() real ext-real set
2 * ((((cosh y) * (cosh y)) + ((sinh y) ^2)) - 1) is V11() real ext-real set
(sinh y) * (2 * ((((cosh y) * (cosh y)) + ((sinh y) ^2)) - 1)) is V11() real ext-real set
(4 * (sinh y)) + ((sinh y) * (2 * ((((cosh y) * (cosh y)) + ((sinh y) ^2)) - 1))) is V11() real ext-real set
((4 * (sinh y)) + ((sinh y) * (2 * ((((cosh y) * (cosh y)) + ((sinh y) ^2)) - 1)))) - (sinh y) is V11() real ext-real set
cosh (y + y) is V11() real ext-real Element of REAL
(cosh (y + y)) - 1 is V11() real ext-real set
2 * ((cosh (y + y)) - 1) is V11() real ext-real set
(sinh y) * (2 * ((cosh (y + y)) - 1)) is V11() real ext-real set
(4 * (sinh y)) + ((sinh y) * (2 * ((cosh (y + y)) - 1))) is V11() real ext-real set
((4 * (sinh y)) + ((sinh y) * (2 * ((cosh (y + y)) - 1)))) - (sinh y) is V11() real ext-real set
5 is V1() ordinal natural V11() real ext-real positive non negative V33() V34() V45() V46() V47() V48() V49() V50() Element of NAT
7 is V1() ordinal natural V11() real ext-real positive non negative V33() V34() V45() V46() V47() V48() V49() V50() Element of NAT
y is V11() real ext-real set
5 * y is V11() real ext-real set
sinh (5 * y) is V11() real ext-real Element of REAL
3 * y is V11() real ext-real set
sinh (3 * y) is V11() real ext-real Element of REAL
2 * (sinh (3 * y)) is V11() real ext-real set
(sinh (5 * y)) + (2 * (sinh (3 * y))) is V11() real ext-real set
sinh y is V11() real ext-real Element of REAL
((sinh (5 * y)) + (2 * (sinh (3 * y)))) + (sinh y) is V11() real ext-real set
7 * y is V11() real ext-real set
sinh (7 * y) is V11() real ext-real Element of REAL
2 * (sinh (5 * y)) is V11() real ext-real set
(sinh (7 * y)) + (2 * (sinh (5 * y))) is V11() real ext-real set
((sinh (7 * y)) + (2 * (sinh (5 * y)))) + (sinh (3 * y)) is V11() real ext-real set
(((sinh (5 * y)) + (2 * (sinh (3 * y)))) + (sinh y)) / (((sinh (7 * y)) + (2 * (sinh (5 * y)))) + (sinh (3 * y))) is V11() real ext-real set
(sinh (3 * y)) / (sinh (5 * y)) is V11() real ext-real set
2 * y is V11() real ext-real set
(3 * y) + (2 * y) is V11() real ext-real set
sinh ((3 * y) + (2 * y)) is V11() real ext-real Element of REAL
(sinh ((3 * y) + (2 * y))) + (2 * (sinh (3 * y))) is V11() real ext-real set
((sinh ((3 * y) + (2 * y))) + (2 * (sinh (3 * y)))) + (sinh y) is V11() real ext-real set
5 + 2 is V1() ordinal natural V11() real ext-real positive non negative set
(5 + 2) * y is V11() real ext-real set
sinh ((5 + 2) * y) is V11() real ext-real Element of REAL
(sinh ((5 + 2) * y)) + (2 * (sinh (5 * y))) is V11() real ext-real set
((sinh ((5 + 2) * y)) + (2 * (sinh (5 * y)))) + (sinh (3 * y)) is V11() real ext-real set
(((sinh ((3 * y) + (2 * y))) + (2 * (sinh (3 * y)))) + (sinh y)) / (((sinh ((5 + 2) * y)) + (2 * (sinh (5 * y)))) + (sinh (3 * y))) is V11() real ext-real set
cosh (2 * y) is V11() real ext-real Element of REAL
(sinh (3 * y)) * (cosh (2 * y)) is V11() real ext-real set
cosh (3 * y) is V11() real ext-real Element of REAL
sinh (2 * y) is V11() real ext-real Element of REAL
(cosh (3 * y)) * (sinh (2 * y)) is V11() real ext-real set
((sinh (3 * y)) * (cosh (2 * y))) + ((cosh (3 * y)) * (sinh (2 * y))) is V11() real ext-real set
(((sinh (3 * y)) * (cosh (2 * y))) + ((cosh (3 * y)) * (sinh (2 * y)))) + (2 * (sinh (3 * y))) is V11() real ext-real set
((((sinh (3 * y)) * (cosh (2 * y))) + ((cosh (3 * y)) * (sinh (2 * y)))) + (2 * (sinh (3 * y)))) + (sinh y) is V11() real ext-real set
(((((sinh (3 * y)) * (cosh (2 * y))) + ((cosh (3 * y)) * (sinh (2 * y)))) + (2 * (sinh (3 * y)))) + (sinh y)) / (((sinh ((5 + 2) * y)) + (2 * (sinh (5 * y)))) + (sinh (3 * y))) is V11() real ext-real set
(cosh (2 * y)) + 2 is V11() real ext-real set
(sinh (3 * y)) * ((cosh (2 * y)) + 2) is V11() real ext-real set
1 * y is V11() real ext-real set
(2 * y) + (1 * y) is V11() real ext-real set
cosh ((2 * y) + (1 * y)) is V11() real ext-real Element of REAL
(cosh ((2 * y) + (1 * y))) * (sinh (2 * y)) is V11() real ext-real set
((cosh ((2 * y) + (1 * y))) * (sinh (2 * y))) + (sinh y) is V11() real ext-real set
((sinh (3 * y)) * ((cosh (2 * y)) + 2)) + (((cosh ((2 * y) + (1 * y))) * (sinh (2 * y))) + (sinh y)) is V11() real ext-real set
(5 * y) + (2 * y) is V11() real ext-real set
sinh ((5 * y) + (2 * y)) is V11() real ext-real Element of REAL
(sinh ((5 * y) + (2 * y))) + (2 * (sinh (5 * y))) is V11() real ext-real set
((sinh ((5 * y) + (2 * y))) + (2 * (sinh (5 * y)))) + (sinh (3 * y)) is V11() real ext-real set
(((sinh (3 * y)) * ((cosh (2 * y)) + 2)) + (((cosh ((2 * y) + (1 * y))) * (sinh (2 * y))) + (sinh y))) / (((sinh ((5 * y) + (2 * y))) + (2 * (sinh (5 * y)))) + (sinh (3 * y))) is V11() real ext-real set
cosh y is V11() real ext-real Element of REAL
(cosh (2 * y)) * (cosh y) is V11() real ext-real set
(sinh (2 * y)) * (sinh y) is V11() real ext-real set
((cosh (2 * y)) * (cosh y)) + ((sinh (2 * y)) * (sinh y)) is V11() real ext-real set
(((cosh (2 * y)) * (cosh y)) + ((sinh (2 * y)) * (sinh y))) * (sinh (2 * y)) is V11() real ext-real set
((((cosh (2 * y)) * (cosh y)) + ((sinh (2 * y)) * (sinh y))) * (sinh (2 * y))) + (sinh y) is V11() real ext-real set
((sinh (3 * y)) * ((cosh (2 * y)) + 2)) + (((((cosh (2 * y)) * (cosh y)) + ((sinh (2 * y)) * (sinh y))) * (sinh (2 * y))) + (sinh y)) is V11() real ext-real set
(((sinh (3 * y)) * ((cosh (2 * y)) + 2)) + (((((cosh (2 * y)) * (cosh y)) + ((sinh (2 * y)) * (sinh y))) * (sinh (2 * y))) + (sinh y))) / (((sinh ((5 * y) + (2 * y))) + (2 * (sinh (5 * y)))) + (sinh (3 * y))) is V11() real ext-real set
((cosh (2 * y)) * (cosh y)) * (sinh (2 * y)) is V11() real ext-real set
(sinh (2 * y)) ^2 is V11() real ext-real Element of REAL
(sinh (2 * y)) * (sinh (2 * y)) is V11() real ext-real set
((sinh (2 * y)) ^2) + 1 is V11() real ext-real set
(((sinh (2 * y)) ^2) + 1) * (sinh y) is V11() real ext-real set
(((cosh (2 * y)) * (cosh y)) * (sinh (2 * y))) + ((((sinh (2 * y)) ^2) + 1) * (sinh y)) is V11() real ext-real set
((sinh (3 * y)) * ((cosh (2 * y)) + 2)) + ((((cosh (2 * y)) * (cosh y)) * (sinh (2 * y))) + ((((sinh (2 * y)) ^2) + 1) * (sinh y))) is V11() real ext-real set
(((sinh (3 * y)) * ((cosh (2 * y)) + 2)) + ((((cosh (2 * y)) * (cosh y)) * (sinh (2 * y))) + ((((sinh (2 * y)) ^2) + 1) * (sinh y)))) / (((sinh ((5 * y) + (2 * y))) + (2 * (sinh (5 * y)))) + (sinh (3 * y))) is V11() real ext-real set
(cosh (2 * y)) ^2 is V11() real ext-real Element of REAL
(cosh (2 * y)) * (cosh (2 * y)) is V11() real ext-real set
((cosh (2 * y)) ^2) - ((sinh (2 * y)) ^2) is V11() real ext-real set
(((cosh (2 * y)) ^2) - ((sinh (2 * y)) ^2)) + ((sinh (2 * y)) ^2) is V11() real ext-real set
((((cosh (2 * y)) ^2) - ((sinh (2 * y)) ^2)) + ((sinh (2 * y)) ^2)) * (sinh y) is V11() real ext-real set
(((cosh (2 * y)) * (cosh y)) * (sinh (2 * y))) + (((((cosh (2 * y)) ^2) - ((sinh (2 * y)) ^2)) + ((sinh (2 * y)) ^2)) * (sinh y)) is V11() real ext-real set
((sinh (3 * y)) * ((cosh (2 * y)) + 2)) + ((((cosh (2 * y)) * (cosh y)) * (sinh (2 * y))) + (((((cosh (2 * y)) ^2) - ((sinh (2 * y)) ^2)) + ((sinh (2 * y)) ^2)) * (sinh y))) is V11() real ext-real set
(((sinh (3 * y)) * ((cosh (2 * y)) + 2)) + ((((cosh (2 * y)) * (cosh y)) * (sinh (2 * y))) + (((((cosh (2 * y)) ^2) - ((sinh (2 * y)) ^2)) + ((sinh (2 * y)) ^2)) * (sinh y)))) / (((sinh ((5 * y) + (2 * y))) + (2 * (sinh (5 * y)))) + (sinh (3 * y))) is V11() real ext-real set
(sinh (2 * y)) * (cosh y) is V11() real ext-real set
(cosh (2 * y)) * (sinh y) is V11() real ext-real set
((sinh (2 * y)) * (cosh y)) + ((cosh (2 * y)) * (sinh y)) is V11() real ext-real set
(cosh (2 * y)) * (((sinh (2 * y)) * (cosh y)) + ((cosh (2 * y)) * (sinh y))) is V11() real ext-real set
((sinh (3 * y)) * ((cosh (2 * y)) + 2)) + ((cosh (2 * y)) * (((sinh (2 * y)) * (cosh y)) + ((cosh (2 * y)) * (sinh y)))) is V11() real ext-real set
(((sinh (3 * y)) * ((cosh (2 * y)) + 2)) + ((cosh (2 * y)) * (((sinh (2 * y)) * (cosh y)) + ((cosh (2 * y)) * (sinh y))))) / (((sinh ((5 * y) + (2 * y))) + (2 * (sinh (5 * y)))) + (sinh (3 * y))) is V11() real ext-real set
sinh ((2 * y) + (1 * y)) is V11() real ext-real Element of REAL
(cosh (2 * y)) * (sinh ((2 * y) + (1 * y))) is V11() real ext-real set
((sinh (3 * y)) * ((cosh (2 * y)) + 2)) + ((cosh (2 * y)) * (sinh ((2 * y) + (1 * y)))) is V11() real ext-real set
(((sinh (3 * y)) * ((cosh (2 * y)) + 2)) + ((cosh (2 * y)) * (sinh ((2 * y) + (1 * y))))) / (((sinh ((5 * y) + (2 * y))) + (2 * (sinh (5 * y)))) + (sinh (3 * y))) is V11() real ext-real set
((cosh (2 * y)) + 2) + (cosh (2 * y)) is V11() real ext-real set
(sinh (3 * y)) * (((cosh (2 * y)) + 2) + (cosh (2 * y))) is V11() real ext-real set
(sinh (5 * y)) * (cosh (2 * y)) is V11() real ext-real set
cosh (5 * y) is V11() real ext-real Element of REAL
(cosh (5 * y)) * (sinh (2 * y)) is V11() real ext-real set
((sinh (5 * y)) * (cosh (2 * y))) + ((cosh (5 * y)) * (sinh (2 * y))) is V11() real ext-real set
(sinh (5 * y)) * 2 is V11() real ext-real set
(((sinh (5 * y)) * (cosh (2 * y))) + ((cosh (5 * y)) * (sinh (2 * y)))) + ((sinh (5 * y)) * 2) is V11() real ext-real set
((((sinh (5 * y)) * (cosh (2 * y))) + ((cosh (5 * y)) * (sinh (2 * y)))) + ((sinh (5 * y)) * 2)) + (sinh (3 * y)) is V11() real ext-real set
((sinh (3 * y)) * (((cosh (2 * y)) + 2) + (cosh (2 * y)))) / (((((sinh (5 * y)) * (cosh (2 * y))) + ((cosh (5 * y)) * (sinh (2 * y)))) + ((sinh (5 * y)) * 2)) + (sinh (3 * y))) is V11() real ext-real set
(sinh (5 * y)) * ((cosh (2 * y)) + 2) is V11() real ext-real set
cosh ((3 * y) + (2 * y)) is V11() real ext-real Element of REAL
(cosh ((3 * y) + (2 * y))) * (sinh (2 * y)) is V11() real ext-real set
((cosh ((3 * y) + (2 * y))) * (sinh (2 * y))) + (sinh (3 * y)) is V11() real ext-real set
((sinh (5 * y)) * ((cosh (2 * y)) + 2)) + (((cosh ((3 * y) + (2 * y))) * (sinh (2 * y))) + (sinh (3 * y))) is V11() real ext-real set
((sinh (3 * y)) * (((cosh (2 * y)) + 2) + (cosh (2 * y)))) / (((sinh (5 * y)) * ((cosh (2 * y)) + 2)) + (((cosh ((3 * y) + (2 * y))) * (sinh (2 * y))) + (sinh (3 * y)))) is V11() real ext-real set
(cosh (3 * y)) * (cosh (2 * y)) is V11() real ext-real set
(sinh (3 * y)) * (sinh (2 * y)) is V11() real ext-real set
((cosh (3 * y)) * (cosh (2 * y))) + ((sinh (3 * y)) * (sinh (2 * y))) is V11() real ext-real set
(((cosh (3 * y)) * (cosh (2 * y))) + ((sinh (3 * y)) * (sinh (2 * y)))) * (sinh (2 * y)) is V11() real ext-real set
((((cosh (3 * y)) * (cosh (2 * y))) + ((sinh (3 * y)) * (sinh (2 * y)))) * (sinh (2 * y))) + (sinh (3 * y)) is V11() real ext-real set
((sinh (5 * y)) * ((cosh (2 * y)) + 2)) + (((((cosh (3 * y)) * (cosh (2 * y))) + ((sinh (3 * y)) * (sinh (2 * y)))) * (sinh (2 * y))) + (sinh (3 * y))) is V11() real ext-real set
((sinh (3 * y)) * (((cosh (2 * y)) + 2) + (cosh (2 * y)))) / (((sinh (5 * y)) * ((cosh (2 * y)) + 2)) + (((((cosh (3 * y)) * (cosh (2 * y))) + ((sinh (3 * y)) * (sinh (2 * y)))) * (sinh (2 * y))) + (sinh (3 * y)))) is V11() real ext-real set
((cosh (3 * y)) * (cosh (2 * y))) * (sinh (2 * y)) is V11() real ext-real set
(sinh (3 * y)) * (((sinh (2 * y)) ^2) + 1) is V11() real ext-real set
(((cosh (3 * y)) * (cosh (2 * y))) * (sinh (2 * y))) + ((sinh (3 * y)) * (((sinh (2 * y)) ^2) + 1)) is V11() real ext-real set
((sinh (5 * y)) * ((cosh (2 * y)) + 2)) + ((((cosh (3 * y)) * (cosh (2 * y))) * (sinh (2 * y))) + ((sinh (3 * y)) * (((sinh (2 * y)) ^2) + 1))) is V11() real ext-real set
((sinh (3 * y)) * (((cosh (2 * y)) + 2) + (cosh (2 * y)))) / (((sinh (5 * y)) * ((cosh (2 * y)) + 2)) + ((((cosh (3 * y)) * (cosh (2 * y))) * (sinh (2 * y))) + ((sinh (3 * y)) * (((sinh (2 * y)) ^2) + 1)))) is V11() real ext-real set
(sinh (3 * y)) * ((((cosh (2 * y)) ^2) - ((sinh (2 * y)) ^2)) + ((sinh (2 * y)) ^2)) is V11() real ext-real set
(((cosh (3 * y)) * (cosh (2 * y))) * (sinh (2 * y))) + ((sinh (3 * y)) * ((((cosh (2 * y)) ^2) - ((sinh (2 * y)) ^2)) + ((sinh (2 * y)) ^2))) is V11() real ext-real set
((sinh (5 * y)) * ((cosh (2 * y)) + 2)) + ((((cosh (3 * y)) * (cosh (2 * y))) * (sinh (2 * y))) + ((sinh (3 * y)) * ((((cosh (2 * y)) ^2) - ((sinh (2 * y)) ^2)) + ((sinh (2 * y)) ^2)))) is V11() real ext-real set
((sinh (3 * y)) * (((cosh (2 * y)) + 2) + (cosh (2 * y)))) / (((sinh (5 * y)) * ((cosh (2 * y)) + 2)) + ((((cosh (3 * y)) * (cosh (2 * y))) * (sinh (2 * y))) + ((sinh (3 * y)) * ((((cosh (2 * y)) ^2) - ((sinh (2 * y)) ^2)) + ((sinh (2 * y)) ^2))))) is V11() real ext-real set
(sinh (2 * y)) * (cosh (3 * y)) is V11() real ext-real set
(cosh (2 * y)) * (sinh (3 * y)) is V11() real ext-real set
((sinh (2 * y)) * (cosh (3 * y))) + ((cosh (2 * y)) * (sinh (3 * y))) is V11() real ext-real set
(cosh (2 * y)) * (((sinh (2 * y)) * (cosh (3 * y))) + ((cosh (2 * y)) * (sinh (3 * y)))) is V11() real ext-real set
((sinh (5 * y)) * ((cosh (2 * y)) + 2)) + ((cosh (2 * y)) * (((sinh (2 * y)) * (cosh (3 * y))) + ((cosh (2 * y)) * (sinh (3 * y))))) is V11() real ext-real set
((sinh (3 * y)) * (((cosh (2 * y)) + 2) + (cosh (2 * y)))) / (((sinh (5 * y)) * ((cosh (2 * y)) + 2)) + ((cosh (2 * y)) * (((sinh (2 * y)) * (cosh (3 * y))) + ((cosh (2 * y)) * (sinh (3 * y)))))) is V11() real ext-real set
(2 * y) + (3 * y) is V11() real ext-real set
sinh ((2 * y) + (3 * y)) is V11() real ext-real Element of REAL
(cosh (2 * y)) * (sinh ((2 * y) + (3 * y))) is V11() real ext-real set
((sinh (5 * y)) * ((cosh (2 * y)) + 2)) + ((cosh (2 * y)) * (sinh ((2 * y) + (3 * y)))) is V11() real ext-real set
((sinh (3 * y)) * (((cosh (2 * y)) + 2) + (cosh (2 * y)))) / (((sinh (5 * y)) * ((cosh (2 * y)) + 2)) + ((cosh (2 * y)) * (sinh ((2 * y) + (3 * y))))) is V11() real ext-real set
(sinh (5 * y)) * (((cosh (2 * y)) + 2) + (cosh (2 * y))) is V11() real ext-real set
((sinh (3 * y)) * (((cosh (2 * y)) + 2) + (cosh (2 * y)))) / ((sinh (5 * y)) * (((cosh (2 * y)) + 2) + (cosh (2 * y)))) is V11() real ext-real set
y is V11() real ext-real set
y / 2 is V11() real ext-real set
tanh (y / 2) is V11() real ext-real Element of REAL
cosh y is V11() real ext-real Element of REAL
(cosh y) - 1 is V11() real ext-real set
(cosh y) + 1 is V11() real ext-real set
((cosh y) - 1) / ((cosh y) + 1) is V11() real ext-real set
sqrt (((cosh y) - 1) / ((cosh y) + 1)) is V11() real ext-real set
sinh (y / 2) is V11() real ext-real Element of REAL
cosh (y / 2) is V11() real ext-real Element of REAL
(sinh (y / 2)) / (cosh (y / 2)) is V11() real ext-real set
((cosh y) - 1) / 2 is V11() real ext-real set
sqrt (((cosh y) - 1) / 2) is V11() real ext-real set
(sqrt (((cosh y) - 1) / 2)) / (cosh (y / 2)) is V11() real ext-real set
((cosh y) + 1) / 2 is V11() real ext-real set
sqrt (((cosh y) + 1) / 2) is V11() real ext-real set
(sqrt (((cosh y) - 1) / 2)) / (sqrt (((cosh y) + 1) / 2)) is V11() real ext-real set
(((cosh y) - 1) / 2) / (((cosh y) + 1) / 2) is V11() real ext-real set
sqrt ((((cosh y) - 1) / 2) / (((cosh y) + 1) / 2)) is V11() real ext-real set
y is V11() real ext-real set
y / 2 is V11() real ext-real set
tanh (y / 2) is V11() real ext-real Element of REAL
cosh y is V11() real ext-real Element of REAL
(cosh y) - 1 is V11() real ext-real set
(cosh y) + 1 is V11() real ext-real set
((cosh y) - 1) / ((cosh y) + 1) is V11() real ext-real set
sqrt (((cosh y) - 1) / ((cosh y) + 1)) is V11() real ext-real set
- (sqrt (((cosh y) - 1) / ((cosh y) + 1))) is V11() real ext-real set
sinh (y / 2) is V11() real ext-real Element of REAL
cosh (y / 2) is V11() real ext-real Element of REAL
(sinh (y / 2)) / (cosh (y / 2)) is V11() real ext-real set
((cosh y) - 1) / 2 is V11() real ext-real set
sqrt (((cosh y) - 1) / 2) is V11() real ext-real set
- (sqrt (((cosh y) - 1) / 2)) is V11() real ext-real set
(- (sqrt (((cosh y) - 1) / 2))) / (cosh (y / 2)) is V11() real ext-real set
(sqrt (((cosh y) - 1) / 2)) / (cosh (y / 2)) is V11() real ext-real set
- ((sqrt (((cosh y) - 1) / 2)) / (cosh (y / 2))) is V11() real ext-real set
((cosh y) + 1) / 2 is V11() real ext-real set
sqrt (((cosh y) + 1) / 2) is V11() real ext-real set
(sqrt (((cosh y) - 1) / 2)) / (sqrt (((cosh y) + 1) / 2)) is V11() real ext-real set
- ((sqrt (((cosh y) - 1) / 2)) / (sqrt (((cosh y) + 1) / 2))) is V11() real ext-real set
(((cosh y) - 1) / 2) / (((cosh y) + 1) / 2) is V11() real ext-real set
sqrt ((((cosh y) - 1) / 2) / (((cosh y) + 1) / 2)) is V11() real ext-real set
- (sqrt ((((cosh y) - 1) / 2) / (((cosh y) + 1) / 2))) is V11() real ext-real set
8 is V1() ordinal natural V11() real ext-real positive non negative V33() V34() V45() V46() V47() V48() V49() V50() Element of NAT
10 is V1() ordinal natural V11() real ext-real positive non negative V33() V34() V45() V46() V47() V48() V49() V50() Element of NAT
16 is V1() ordinal natural V11() real ext-real positive non negative V33() V34() V45() V46() V47() V48() V49() V50() Element of NAT
6 is V1() ordinal natural V11() real ext-real positive non negative V33() V34() V45() V46() V47() V48() V49() V50() Element of NAT
15 is V1() ordinal natural V11() real ext-real positive non negative V33() V34() V45() V46() V47() V48() V49() V50() Element of NAT
32 is V1() ordinal natural V11() real ext-real positive non negative V33() V34() V45() V46() V47() V48() V49() V50() Element of NAT
21 is V1() ordinal natural V11() real ext-real positive non negative V33() V34() V45() V46() V47() V48() V49() V50() Element of NAT
35 is V1() ordinal natural V11() real ext-real positive non negative V33() V34() V45() V46() V47() V48() V49() V50() Element of NAT
64 is V1() ordinal natural V11() real ext-real positive non negative V33() V34() V45() V46() V47() V48() V49() V50() Element of NAT
28 is V1() ordinal natural V11() real ext-real positive non negative V33() V34() V45() V46() V47() V48() V49() V50() Element of NAT
56 is V1() ordinal natural V11() real ext-real positive non negative V33() V34() V45() V46() V47() V48() V49() V50() Element of NAT
128 is V1() ordinal natural V11() real ext-real positive non negative V33() V34() V45() V46() V47() V48() V49() V50() Element of NAT
y is V11() real ext-real set
sinh y is V11() real ext-real Element of REAL
(sinh y) |^ 3 is V11() real ext-real Element of REAL
3 * y is V11() real ext-real set
sinh (3 * y) is V11() real ext-real Element of REAL
3 * (sinh y) is V11() real ext-real set
(sinh (3 * y)) - (3 * (sinh y)) is V11() real ext-real set
((sinh (3 * y)) - (3 * (sinh y))) / 4 is V11() real ext-real set
(sinh y) |^ 4 is V11() real ext-real Element of REAL
4 * y is V11() real ext-real set
cosh (4 * y) is V11() real ext-real Element of REAL
2 * y is V11() real ext-real set
cosh (2 * y) is V11() real ext-real Element of REAL
4 * (cosh (2 * y)) is V11() real ext-real set
(cosh (4 * y)) - (4 * (cosh (2 * y))) is V11() real ext-real set
((cosh (4 * y)) - (4 * (cosh (2 * y)))) + 3 is V11() real ext-real set
(((cosh (4 * y)) - (4 * (cosh (2 * y)))) + 3) / 8 is V11() real ext-real set
(sinh y) |^ 5 is V11() real ext-real Element of REAL
5 * y is V11() real ext-real set
sinh (5 * y) is V11() real ext-real Element of REAL
5 * (sinh (3 * y)) is V11() real ext-real set
(sinh (5 * y)) - (5 * (sinh (3 * y))) is V11() real ext-real set
10 * (sinh y) is V11() real ext-real set
((sinh (5 * y)) - (5 * (sinh (3 * y)))) + (10 * (sinh y)) is V11() real ext-real set
(((sinh (5 * y)) - (5 * (sinh (3 * y)))) + (10 * (sinh y))) / 16 is V11() real ext-real set
(sinh y) |^ 6 is V11() real ext-real Element of REAL
6 * y is V11() real ext-real set
cosh (6 * y) is V11() real ext-real Element of REAL
6 * (cosh (4 * y)) is V11() real ext-real set
(cosh (6 * y)) - (6 * (cosh (4 * y))) is V11() real ext-real set
15 * (cosh (2 * y)) is V11() real ext-real set
((cosh (6 * y)) - (6 * (cosh (4 * y)))) + (15 * (cosh (2 * y))) is V11() real ext-real set
(((cosh (6 * y)) - (6 * (cosh (4 * y)))) + (15 * (cosh (2 * y)))) - 10 is V11() real ext-real set
((((cosh (6 * y)) - (6 * (cosh (4 * y)))) + (15 * (cosh (2 * y)))) - 10) / 32 is V11() real ext-real set
(sinh y) |^ 7 is V11() real ext-real Element of REAL
7 * y is V11() real ext-real set
sinh (7 * y) is V11() real ext-real Element of REAL
7 * (sinh (5 * y)) is V11() real ext-real set
(sinh (7 * y)) - (7 * (sinh (5 * y))) is V11() real ext-real set
21 * (sinh (3 * y)) is V11() real ext-real set
((sinh (7 * y)) - (7 * (sinh (5 * y)))) + (21 * (sinh (3 * y))) is V11() real ext-real set
35 * (sinh y) is V11() real ext-real set
(((sinh (7 * y)) - (7 * (sinh (5 * y)))) + (21 * (sinh (3 * y)))) - (35 * (sinh y)) is V11() real ext-real set
((((sinh (7 * y)) - (7 * (sinh (5 * y)))) + (21 * (sinh (3 * y)))) - (35 * (sinh y))) / 64 is V11() real ext-real set
(sinh y) |^ 8 is V11() real ext-real Element of REAL
8 * y is V11() real ext-real set
cosh (8 * y) is V11() real ext-real Element of REAL
8 * (cosh (6 * y)) is V11() real ext-real set
(cosh (8 * y)) - (8 * (cosh (6 * y))) is V11() real ext-real set
28 * (cosh (4 * y)) is V11() real ext-real set
((cosh (8 * y)) - (8 * (cosh (6 * y)))) + (28 * (cosh (4 * y))) is V11() real ext-real set
56 * (cosh (2 * y)) is V11() real ext-real set
(((cosh (8 * y)) - (8 * (cosh (6 * y)))) + (28 * (cosh (4 * y)))) - (56 * (cosh (2 * y))) is V11() real ext-real set
((((cosh (8 * y)) - (8 * (cosh (6 * y)))) + (28 * (cosh (4 * y)))) - (56 * (cosh (2 * y)))) + 35 is V11() real ext-real set
(((((cosh (8 * y)) - (8 * (cosh (6 * y)))) + (28 * (cosh (4 * y)))) - (56 * (cosh (2 * y)))) + 35) / 128 is V11() real ext-real set
4 * ((sinh y) |^ 3) is V11() real ext-real set
(4 * ((sinh y) |^ 3)) + (3 * (sinh y)) is V11() real ext-real set
((4 * ((sinh y) |^ 3)) + (3 * (sinh y))) - (3 * (sinh y)) is V11() real ext-real set
(((4 * ((sinh y) |^ 3)) + (3 * (sinh y))) - (3 * (sinh y))) / 4 is V11() real ext-real set
(((sinh (3 * y)) - (3 * (sinh y))) / 4) * (sinh y) is V11() real ext-real set
(sinh (3 * y)) * (sinh y) is V11() real ext-real set
(sinh y) * (sinh y) is V11() real ext-real set
3 * ((sinh y) * (sinh y)) is V11() real ext-real set
((sinh (3 * y)) * (sinh y)) - (3 * ((sinh y) * (sinh y))) is V11() real ext-real set
(((sinh (3 * y)) * (sinh y)) - (3 * ((sinh y) * (sinh y)))) / 4 is V11() real ext-real set
1 * y is V11() real ext-real set
(3 * y) + (1 * y) is V11() real ext-real set
cosh ((3 * y) + (1 * y)) is V11() real ext-real Element of REAL
(3 * y) - (1 * y) is V11() real ext-real set
cosh ((3 * y) - (1 * y)) is V11() real ext-real Element of REAL
(cosh ((3 * y) + (1 * y))) - (cosh ((3 * y) - (1 * y))) is V11() real ext-real set
(1 / 2) * ((cosh ((3 * y) + (1 * y))) - (cosh ((3 * y) - (1 * y)))) is V11() real ext-real set
((1 / 2) * ((cosh ((3 * y) + (1 * y))) - (cosh ((3 * y) - (1 * y))))) - (3 * ((sinh y) * (sinh y))) is V11() real ext-real set
(((1 / 2) * ((cosh ((3 * y) + (1 * y))) - (cosh ((3 * y) - (1 * y))))) - (3 * ((sinh y) * (sinh y)))) / 4 is V11() real ext-real set
(cosh (4 * y)) - (cosh (2 * y)) is V11() real ext-real set
(1 / 2) * ((cosh (4 * y)) - (cosh (2 * y))) is V11() real ext-real set
(sinh y) ^2 is V11() real ext-real Element of REAL
((sinh y) ^2) * 3 is V11() real ext-real set
((1 / 2) * ((cosh (4 * y)) - (cosh (2 * y)))) - (((sinh y) ^2) * 3) is V11() real ext-real set
(((1 / 2) * ((cosh (4 * y)) - (cosh (2 * y)))) - (((sinh y) ^2) * 3)) / 4 is V11() real ext-real set
(cosh (2 * y)) - 1 is V11() real ext-real set
(1 / 2) * ((cosh (2 * y)) - 1) is V11() real ext-real set
((1 / 2) * ((cosh (2 * y)) - 1)) * 3 is V11() real ext-real set
((1 / 2) * ((cosh (4 * y)) - (cosh (2 * y)))) - (((1 / 2) * ((cosh (2 * y)) - 1)) * 3) is V11() real ext-real set
(((1 / 2) * ((cosh (4 * y)) - (cosh (2 * y)))) - (((1 / 2) * ((cosh (2 * y)) - 1)) * 3)) / 4 is V11() real ext-real set
4 + 1 is V1() ordinal natural V11() real ext-real positive non negative set
(sinh y) |^ (4 + 1) is V11() real ext-real Element of REAL
((((cosh (4 * y)) - (4 * (cosh (2 * y)))) + 3) / 8) * (sinh y) is V11() real ext-real set
(cosh (4 * y)) * (sinh y) is V11() real ext-real set
(cosh (2 * y)) * (sinh y) is V11() real ext-real set
4 * ((cosh (2 * y)) * (sinh y)) is V11() real ext-real set
((cosh (4 * y)) * (sinh y)) - (4 * ((cosh (2 * y)) * (sinh y))) is V11() real ext-real set
(((cosh (4 * y)) * (sinh y)) - (4 * ((cosh (2 * y)) * (sinh y)))) + (3 * (sinh y)) is V11() real ext-real set
((((cosh (4 * y)) * (sinh y)) - (4 * ((cosh (2 * y)) * (sinh y)))) + (3 * (sinh y))) / 8 is V11() real ext-real set
(4 * y) + (1 * y) is V11() real ext-real set
sinh ((4 * y) + (1 * y)) is V11() real ext-real Element of REAL
(4 * y) - (1 * y) is V11() real ext-real set
sinh ((4 * y) - (1 * y)) is V11() real ext-real Element of REAL
(sinh ((4 * y) + (1 * y))) - (sinh ((4 * y) - (1 * y))) is V11() real ext-real set
(1 / 2) * ((sinh ((4 * y) + (1 * y))) - (sinh ((4 * y) - (1 * y)))) is V11() real ext-real set
((1 / 2) * ((sinh ((4 * y) + (1 * y))) - (sinh ((4 * y) - (1 * y))))) - (4 * ((cosh (2 * y)) * (sinh y))) is V11() real ext-real set
(((1 / 2) * ((sinh ((4 * y) + (1 * y))) - (sinh ((4 * y) - (1 * y))))) - (4 * ((cosh (2 * y)) * (sinh y)))) + (3 * (sinh y)) is V11() real ext-real set
((((1 / 2) * ((sinh ((4 * y) + (1 * y))) - (sinh ((4 * y) - (1 * y))))) - (4 * ((cosh (2 * y)) * (sinh y)))) + (3 * (sinh y))) / 8 is V11() real ext-real set
(sinh (5 * y)) - (sinh (3 * y)) is V11() real ext-real set
(1 / 2) * ((sinh (5 * y)) - (sinh (3 * y))) is V11() real ext-real set
(2 * y) + (1 * y) is V11() real ext-real set
sinh ((2 * y) + (1 * y)) is V11() real ext-real Element of REAL
(2 * y) - (1 * y) is V11() real ext-real set
sinh ((2 * y) - (1 * y)) is V11() real ext-real Element of REAL
(sinh ((2 * y) + (1 * y))) - (sinh ((2 * y) - (1 * y))) is V11() real ext-real set
(1 / 2) * ((sinh ((2 * y) + (1 * y))) - (sinh ((2 * y) - (1 * y)))) is V11() real ext-real set
4 * ((1 / 2) * ((sinh ((2 * y) + (1 * y))) - (sinh ((2 * y) - (1 * y))))) is V11() real ext-real set
((1 / 2) * ((sinh (5 * y)) - (sinh (3 * y)))) - (4 * ((1 / 2) * ((sinh ((2 * y) + (1 * y))) - (sinh ((2 * y) - (1 * y)))))) is V11() real ext-real set
(((1 / 2) * ((sinh (5 * y)) - (sinh (3 * y)))) - (4 * ((1 / 2) * ((sinh ((2 * y) + (1 * y))) - (sinh ((2 * y) - (1 * y))))))) + (3 * (sinh y)) is V11() real ext-real set
((((1 / 2) * ((sinh (5 * y)) - (sinh (3 * y)))) - (4 * ((1 / 2) * ((sinh ((2 * y) + (1 * y))) - (sinh ((2 * y) - (1 * y))))))) + (3 * (sinh y))) / 8 is V11() real ext-real set
5 + 1 is V1() ordinal natural V11() real ext-real positive non negative set
(sinh y) |^ (5 + 1) is V11() real ext-real Element of REAL
((((sinh (5 * y)) - (5 * (sinh (3 * y)))) + (10 * (sinh y))) / 16) * (sinh y) is V11() real ext-real set
(sinh (5 * y)) * (sinh y) is V11() real ext-real set
5 * ((sinh (3 * y)) * (sinh y)) is V11() real ext-real set
((sinh (5 * y)) * (sinh y)) - (5 * ((sinh (3 * y)) * (sinh y))) is V11() real ext-real set
10 * ((sinh y) * (sinh y)) is V11() real ext-real set
(((sinh (5 * y)) * (sinh y)) - (5 * ((sinh (3 * y)) * (sinh y)))) + (10 * ((sinh y) * (sinh y))) is V11() real ext-real set
((((sinh (5 * y)) * (sinh y)) - (5 * ((sinh (3 * y)) * (sinh y)))) + (10 * ((sinh y) * (sinh y)))) / 16 is V11() real ext-real set
(5 * y) + (1 * y) is V11() real ext-real set
cosh ((5 * y) + (1 * y)) is V11() real ext-real Element of REAL
(5 * y) - (1 * y) is V11() real ext-real set
cosh ((5 * y) - (1 * y)) is V11() real ext-real Element of REAL
(cosh ((5 * y) + (1 * y))) - (cosh ((5 * y) - (1 * y))) is V11() real ext-real set
(1 / 2) * ((cosh ((5 * y) + (1 * y))) - (cosh ((5 * y) - (1 * y)))) is V11() real ext-real set
((1 / 2) * ((cosh ((5 * y) + (1 * y))) - (cosh ((5 * y) - (1 * y))))) - (5 * ((sinh (3 * y)) * (sinh y))) is V11() real ext-real set
(((1 / 2) * ((cosh ((5 * y) + (1 * y))) - (cosh ((5 * y) - (1 * y))))) - (5 * ((sinh (3 * y)) * (sinh y)))) + (10 * ((sinh y) * (sinh y))) is V11() real ext-real set
((((1 / 2) * ((cosh ((5 * y) + (1 * y))) - (cosh ((5 * y) - (1 * y))))) - (5 * ((sinh (3 * y)) * (sinh y)))) + (10 * ((sinh y) * (sinh y)))) / 16 is V11() real ext-real set
(cosh (6 * y)) - (cosh (4 * y)) is V11() real ext-real set
(1 / 2) * ((cosh (6 * y)) - (cosh (4 * y))) is V11() real ext-real set
((1 / 2) * ((cosh ((3 * y) + (1 * y))) - (cosh ((3 * y) - (1 * y))))) * 5 is V11() real ext-real set
((1 / 2) * ((cosh (6 * y)) - (cosh (4 * y)))) - (((1 / 2) * ((cosh ((3 * y) + (1 * y))) - (cosh ((3 * y) - (1 * y))))) * 5) is V11() real ext-real set
(((1 / 2) * ((cosh (6 * y)) - (cosh (4 * y)))) - (((1 / 2) * ((cosh ((3 * y) + (1 * y))) - (cosh ((3 * y) - (1 * y))))) * 5)) + (10 * ((sinh y) * (sinh y))) is V11() real ext-real set
((((1 / 2) * ((cosh (6 * y)) - (cosh (4 * y)))) - (((1 / 2) * ((cosh ((3 * y) + (1 * y))) - (cosh ((3 * y) - (1 * y))))) * 5)) + (10 * ((sinh y) * (sinh y)))) / 16 is V11() real ext-real set
(cosh (2 * y)) * 5 is V11() real ext-real set
((cosh (6 * y)) - (6 * (cosh (4 * y)))) + ((cosh (2 * y)) * 5) is V11() real ext-real set
(1 / 2) * (((cosh (6 * y)) - (6 * (cosh (4 * y)))) + ((cosh (2 * y)) * 5)) is V11() real ext-real set
10 * ((sinh y) ^2) is V11() real ext-real set
((1 / 2) * (((cosh (6 * y)) - (6 * (cosh (4 * y)))) + ((cosh (2 * y)) * 5))) + (10 * ((sinh y) ^2)) is V11() real ext-real set
(((1 / 2) * (((cosh (6 * y)) - (6 * (cosh (4 * y)))) + ((cosh (2 * y)) * 5))) + (10 * ((sinh y) ^2))) / 16 is V11() real ext-real set
((1 / 2) * ((cosh (2 * y)) - 1)) * 10 is V11() real ext-real set
((1 / 2) * (((cosh (6 * y)) - (6 * (cosh (4 * y)))) + ((cosh (2 * y)) * 5))) + (((1 / 2) * ((cosh (2 * y)) - 1)) * 10) is V11() real ext-real set
(((1 / 2) * (((cosh (6 * y)) - (6 * (cosh (4 * y)))) + ((cosh (2 * y)) * 5))) + (((1 / 2) * ((cosh (2 * y)) - 1)) * 10)) / 16 is V11() real ext-real set
6 + 1 is V1() ordinal natural V11() real ext-real positive non negative set
(sinh y) |^ (6 + 1) is V11() real ext-real Element of REAL
(((((cosh (6 * y)) - (6 * (cosh (4 * y)))) + (15 * (cosh (2 * y)))) - 10) / 32) * (sinh y) is V11() real ext-real set
(cosh (6 * y)) * (sinh y) is V11() real ext-real set
(6 * (cosh (4 * y))) * (sinh y) is V11() real ext-real set
((cosh (6 * y)) * (sinh y)) - ((6 * (cosh (4 * y))) * (sinh y)) is V11() real ext-real set
(15 * (cosh (2 * y))) * (sinh y) is V11() real ext-real set
(((cosh (6 * y)) * (sinh y)) - ((6 * (cosh (4 * y))) * (sinh y))) + ((15 * (cosh (2 * y))) * (sinh y)) is V11() real ext-real set
((((cosh (6 * y)) * (sinh y)) - ((6 * (cosh (4 * y))) * (sinh y))) + ((15 * (cosh (2 * y))) * (sinh y))) - (10 * (sinh y)) is V11() real ext-real set
(((((cosh (6 * y)) * (sinh y)) - ((6 * (cosh (4 * y))) * (sinh y))) + ((15 * (cosh (2 * y))) * (sinh y))) - (10 * (sinh y))) / 32 is V11() real ext-real set
(6 * y) + (1 * y) is V11() real ext-real set
sinh ((6 * y) + (1 * y)) is V11() real ext-real Element of REAL
(6 * y) - (1 * y) is V11() real ext-real set
sinh ((6 * y) - (1 * y)) is V11() real ext-real Element of REAL
(sinh ((6 * y) + (1 * y))) - (sinh ((6 * y) - (1 * y))) is V11() real ext-real set
(1 / 2) * ((sinh ((6 * y) + (1 * y))) - (sinh ((6 * y) - (1 * y)))) is V11() real ext-real set
((1 / 2) * ((sinh ((6 * y) + (1 * y))) - (sinh ((6 * y) - (1 * y))))) - ((6 * (cosh (4 * y))) * (sinh y)) is V11() real ext-real set
(((1 / 2) * ((sinh ((6 * y) + (1 * y))) - (sinh ((6 * y) - (1 * y))))) - ((6 * (cosh (4 * y))) * (sinh y))) + ((15 * (cosh (2 * y))) * (sinh y)) is V11() real ext-real set
((((1 / 2) * ((sinh ((6 * y) + (1 * y))) - (sinh ((6 * y) - (1 * y))))) - ((6 * (cosh (4 * y))) * (sinh y))) + ((15 * (cosh (2 * y))) * (sinh y))) - (10 * (sinh y)) is V11() real ext-real set
(((((1 / 2) * ((sinh ((6 * y) + (1 * y))) - (sinh ((6 * y) - (1 * y))))) - ((6 * (cosh (4 * y))) * (sinh y))) + ((15 * (cosh (2 * y))) * (sinh y))) - (10 * (sinh y))) / 32 is V11() real ext-real set
(sinh (7 * y)) - (sinh (5 * y)) is V11() real ext-real set
(1 / 2) * ((sinh (7 * y)) - (sinh (5 * y))) is V11() real ext-real set
6 * ((cosh (4 * y)) * (sinh y)) is V11() real ext-real set
((1 / 2) * ((sinh (7 * y)) - (sinh (5 * y)))) - (6 * ((cosh (4 * y)) * (sinh y))) is V11() real ext-real set
(((1 / 2) * ((sinh (7 * y)) - (sinh (5 * y)))) - (6 * ((cosh (4 * y)) * (sinh y)))) + ((15 * (cosh (2 * y))) * (sinh y)) is V11() real ext-real set
((((1 / 2) * ((sinh (7 * y)) - (sinh (5 * y)))) - (6 * ((cosh (4 * y)) * (sinh y)))) + ((15 * (cosh (2 * y))) * (sinh y))) - (10 * (sinh y)) is V11() real ext-real set
(((((1 / 2) * ((sinh (7 * y)) - (sinh (5 * y)))) - (6 * ((cosh (4 * y)) * (sinh y)))) + ((15 * (cosh (2 * y))) * (sinh y))) - (10 * (sinh y))) / 32 is V11() real ext-real set
6 * ((1 / 2) * ((sinh ((4 * y) + (1 * y))) - (sinh ((4 * y) - (1 * y))))) is V11() real ext-real set
((1 / 2) * ((sinh (7 * y)) - (sinh (5 * y)))) - (6 * ((1 / 2) * ((sinh ((4 * y) + (1 * y))) - (sinh ((4 * y) - (1 * y)))))) is V11() real ext-real set
(((1 / 2) * ((sinh (7 * y)) - (sinh (5 * y)))) - (6 * ((1 / 2) * ((sinh ((4 * y) + (1 * y))) - (sinh ((4 * y) - (1 * y))))))) + ((15 * (cosh (2 * y))) * (sinh y)) is V11() real ext-real set
((((1 / 2) * ((sinh (7 * y)) - (sinh (5 * y)))) - (6 * ((1 / 2) * ((sinh ((4 * y) + (1 * y))) - (sinh ((4 * y) - (1 * y))))))) + ((15 * (cosh (2 * y))) * (sinh y))) - (10 * (sinh y)) is V11() real ext-real set
(((((1 / 2) * ((sinh (7 * y)) - (sinh (5 * y)))) - (6 * ((1 / 2) * ((sinh ((4 * y) + (1 * y))) - (sinh ((4 * y) - (1 * y))))))) + ((15 * (cosh (2 * y))) * (sinh y))) - (10 * (sinh y))) / 32 is V11() real ext-real set
(sinh (3 * y)) * 6 is V11() real ext-real set
((sinh (7 * y)) - (7 * (sinh (5 * y)))) + ((sinh (3 * y)) * 6) is V11() real ext-real set
(1 / 2) * (((sinh (7 * y)) - (7 * (sinh (5 * y)))) + ((sinh (3 * y)) * 6)) is V11() real ext-real set
15 * ((cosh (2 * y)) * (sinh y)) is V11() real ext-real set
((1 / 2) * (((sinh (7 * y)) - (7 * (sinh (5 * y)))) + ((sinh (3 * y)) * 6))) + (15 * ((cosh (2 * y)) * (sinh y))) is V11() real ext-real set
(((1 / 2) * (((sinh (7 * y)) - (7 * (sinh (5 * y)))) + ((sinh (3 * y)) * 6))) + (15 * ((cosh (2 * y)) * (sinh y)))) - (10 * (sinh y)) is V11() real ext-real set
((((1 / 2) * (((sinh (7 * y)) - (7 * (sinh (5 * y)))) + ((sinh (3 * y)) * 6))) + (15 * ((cosh (2 * y)) * (sinh y)))) - (10 * (sinh y))) / 32 is V11() real ext-real set
15 * ((1 / 2) * ((sinh ((2 * y) + (1 * y))) - (sinh ((2 * y) - (1 * y))))) is V11() real ext-real set
((1 / 2) * (((sinh (7 * y)) - (7 * (sinh (5 * y)))) + ((sinh (3 * y)) * 6))) + (15 * ((1 / 2) * ((sinh ((2 * y) + (1 * y))) - (sinh ((2 * y) - (1 * y)))))) is V11() real ext-real set
(((1 / 2) * (((sinh (7 * y)) - (7 * (sinh (5 * y)))) + ((sinh (3 * y)) * 6))) + (15 * ((1 / 2) * ((sinh ((2 * y) + (1 * y))) - (sinh ((2 * y) - (1 * y))))))) - (10 * (sinh y)) is V11() real ext-real set
((((1 / 2) * (((sinh (7 * y)) - (7 * (sinh (5 * y)))) + ((sinh (3 * y)) * 6))) + (15 * ((1 / 2) * ((sinh ((2 * y) + (1 * y))) - (sinh ((2 * y) - (1 * y))))))) - (10 * (sinh y))) / 32 is V11() real ext-real set
7 + 1 is V1() ordinal natural V11() real ext-real positive non negative set
(sinh y) |^ (7 + 1) is V11() real ext-real Element of REAL
(((((sinh (7 * y)) - (7 * (sinh (5 * y)))) + (21 * (sinh (3 * y)))) - (35 * (sinh y))) / 64) * (sinh y) is V11() real ext-real set
(sinh (7 * y)) * (sinh y) is V11() real ext-real set
7 * ((sinh (5 * y)) * (sinh y)) is V11() real ext-real set
((sinh (7 * y)) * (sinh y)) - (7 * ((sinh (5 * y)) * (sinh y))) is V11() real ext-real set
21 * ((sinh (3 * y)) * (sinh y)) is V11() real ext-real set
(((sinh (7 * y)) * (sinh y)) - (7 * ((sinh (5 * y)) * (sinh y)))) + (21 * ((sinh (3 * y)) * (sinh y))) is V11() real ext-real set
35 * ((sinh y) * (sinh y)) is V11() real ext-real set
((((sinh (7 * y)) * (sinh y)) - (7 * ((sinh (5 * y)) * (sinh y)))) + (21 * ((sinh (3 * y)) * (sinh y)))) - (35 * ((sinh y) * (sinh y))) is V11() real ext-real set
(((((sinh (7 * y)) * (sinh y)) - (7 * ((sinh (5 * y)) * (sinh y)))) + (21 * ((sinh (3 * y)) * (sinh y)))) - (35 * ((sinh y) * (sinh y)))) / 64 is V11() real ext-real set
(7 * y) + (1 * y) is V11() real ext-real set
cosh ((7 * y) + (1 * y)) is V11() real ext-real Element of REAL
(7 * y) - (1 * y) is V11() real ext-real set
cosh ((7 * y) - (1 * y)) is V11() real ext-real Element of REAL
(cosh ((7 * y) + (1 * y))) - (cosh ((7 * y) - (1 * y))) is V11() real ext-real set
(1 / 2) * ((cosh ((7 * y) + (1 * y))) - (cosh ((7 * y) - (1 * y)))) is V11() real ext-real set
((1 / 2) * ((cosh ((7 * y) + (1 * y))) - (cosh ((7 * y) - (1 * y))))) - (7 * ((sinh (5 * y)) * (sinh y))) is V11() real ext-real set
(((1 / 2) * ((cosh ((7 * y) + (1 * y))) - (cosh ((7 * y) - (1 * y))))) - (7 * ((sinh (5 * y)) * (sinh y)))) + (21 * ((sinh (3 * y)) * (sinh y))) is V11() real ext-real set
((((1 / 2) * ((cosh ((7 * y) + (1 * y))) - (cosh ((7 * y) - (1 * y))))) - (7 * ((sinh (5 * y)) * (sinh y)))) + (21 * ((sinh (3 * y)) * (sinh y)))) - (35 * ((sinh y) * (sinh y))) is V11() real ext-real set
(((((1 / 2) * ((cosh ((7 * y) + (1 * y))) - (cosh ((7 * y) - (1 * y))))) - (7 * ((sinh (5 * y)) * (sinh y)))) + (21 * ((sinh (3 * y)) * (sinh y)))) - (35 * ((sinh y) * (sinh y)))) / 64 is V11() real ext-real set
(cosh (8 * y)) - (cosh (6 * y)) is V11() real ext-real set
(1 / 2) * ((cosh (8 * y)) - (cosh (6 * y))) is V11() real ext-real set
((1 / 2) * ((cosh ((5 * y) + (1 * y))) - (cosh ((5 * y) - (1 * y))))) * 7 is V11() real ext-real set
((1 / 2) * ((cosh (8 * y)) - (cosh (6 * y)))) - (((1 / 2) * ((cosh ((5 * y) + (1 * y))) - (cosh ((5 * y) - (1 * y))))) * 7) is V11() real ext-real set
(((1 / 2) * ((cosh (8 * y)) - (cosh (6 * y)))) - (((1 / 2) * ((cosh ((5 * y) + (1 * y))) - (cosh ((5 * y) - (1 * y))))) * 7)) + (21 * ((sinh (3 * y)) * (sinh y))) is V11() real ext-real set
((((1 / 2) * ((cosh (8 * y)) - (cosh (6 * y)))) - (((1 / 2) * ((cosh ((5 * y) + (1 * y))) - (cosh ((5 * y) - (1 * y))))) * 7)) + (21 * ((sinh (3 * y)) * (sinh y)))) - (35 * ((sinh y) * (sinh y))) is V11() real ext-real set
(((((1 / 2) * ((cosh (8 * y)) - (cosh (6 * y)))) - (((1 / 2) * ((cosh ((5 * y) + (1 * y))) - (cosh ((5 * y) - (1 * y))))) * 7)) + (21 * ((sinh (3 * y)) * (sinh y)))) - (35 * ((sinh y) * (sinh y)))) / 64 is V11() real ext-real set
(cosh (4 * y)) * 7 is V11() real ext-real set
((cosh (8 * y)) - (8 * (cosh (6 * y)))) + ((cosh (4 * y)) * 7) is V11() real ext-real set
(1 / 2) * (((cosh (8 * y)) - (8 * (cosh (6 * y)))) + ((cosh (4 * y)) * 7)) is V11() real ext-real set
((1 / 2) * ((cosh ((3 * y) + (1 * y))) - (cosh ((3 * y) - (1 * y))))) * 21 is V11() real ext-real set
((1 / 2) * (((cosh (8 * y)) - (8 * (cosh (6 * y)))) + ((cosh (4 * y)) * 7))) + (((1 / 2) * ((cosh ((3 * y) + (1 * y))) - (cosh ((3 * y) - (1 * y))))) * 21) is V11() real ext-real set
(((1 / 2) * (((cosh (8 * y)) - (8 * (cosh (6 * y)))) + ((cosh (4 * y)) * 7))) + (((1 / 2) * ((cosh ((3 * y) + (1 * y))) - (cosh ((3 * y) - (1 * y))))) * 21)) - (35 * ((sinh y) * (sinh y))) is V11() real ext-real set
((((1 / 2) * (((cosh (8 * y)) - (8 * (cosh (6 * y)))) + ((cosh (4 * y)) * 7))) + (((1 / 2) * ((cosh ((3 * y) + (1 * y))) - (cosh ((3 * y) - (1 * y))))) * 21)) - (35 * ((sinh y) * (sinh y)))) / 64 is V11() real ext-real set
(cosh (2 * y)) * 21 is V11() real ext-real set
- ((cosh (2 * y)) * 21) is V11() real ext-real set
(((cosh (8 * y)) - (8 * (cosh (6 * y)))) + (28 * (cosh (4 * y)))) + (- ((cosh (2 * y)) * 21)) is V11() real ext-real set
(1 / 2) * ((((cosh (8 * y)) - (8 * (cosh (6 * y)))) + (28 * (cosh (4 * y)))) + (- ((cosh (2 * y)) * 21))) is V11() real ext-real set
35 * ((sinh y) ^2) is V11() real ext-real set
((1 / 2) * ((((cosh (8 * y)) - (8 * (cosh (6 * y)))) + (28 * (cosh (4 * y)))) + (- ((cosh (2 * y)) * 21)))) - (35 * ((sinh y) ^2)) is V11() real ext-real set
(((1 / 2) * ((((cosh (8 * y)) - (8 * (cosh (6 * y)))) + (28 * (cosh (4 * y)))) + (- ((cosh (2 * y)) * 21)))) - (35 * ((sinh y) ^2))) / 64 is V11() real ext-real set
((1 / 2) * ((cosh (2 * y)) - 1)) * 35 is V11() real ext-real set
((1 / 2) * ((((cosh (8 * y)) - (8 * (cosh (6 * y)))) + (28 * (cosh (4 * y)))) + (- ((cosh (2 * y)) * 21)))) - (((1 / 2) * ((cosh (2 * y)) - 1)) * 35) is V11() real ext-real set
(((1 / 2) * ((((cosh (8 * y)) - (8 * (cosh (6 * y)))) + (28 * (cosh (4 * y)))) + (- ((cosh (2 * y)) * 21)))) - (((1 / 2) * ((cosh (2 * y)) - 1)) * 35)) / 64 is V11() real ext-real set
y is V11() real ext-real set
cosh y is V11() real ext-real Element of REAL
(cosh y) |^ 3 is V11() real ext-real Element of REAL
3 * y is V11() real ext-real set
cosh (3 * y) is V11() real ext-real Element of REAL
3 * (cosh y) is V11() real ext-real set
(cosh (3 * y)) + (3 * (cosh y)) is V11() real ext-real set
((cosh (3 * y)) + (3 * (cosh y))) / 4 is V11() real ext-real set
(cosh y) |^ 4 is V11() real ext-real Element of REAL
4 * y is V11() real ext-real set
cosh (4 * y) is V11() real ext-real Element of REAL
2 * y is V11() real ext-real set
cosh (2 * y) is V11() real ext-real Element of REAL
4 * (cosh (2 * y)) is V11() real ext-real set
(cosh (4 * y)) + (4 * (cosh (2 * y))) is V11() real ext-real set
((cosh (4 * y)) + (4 * (cosh (2 * y)))) + 3 is V11() real ext-real set
(((cosh (4 * y)) + (4 * (cosh (2 * y)))) + 3) / 8 is V11() real ext-real set
(cosh y) |^ 5 is V11() real ext-real Element of REAL
5 * y is V11() real ext-real set
cosh (5 * y) is V11() real ext-real Element of REAL
5 * (cosh (3 * y)) is V11() real ext-real set
(cosh (5 * y)) + (5 * (cosh (3 * y))) is V11() real ext-real set
10 * (cosh y) is V11() real ext-real set
((cosh (5 * y)) + (5 * (cosh (3 * y)))) + (10 * (cosh y)) is V11() real ext-real set
(((cosh (5 * y)) + (5 * (cosh (3 * y)))) + (10 * (cosh y))) / 16 is V11() real ext-real set
(cosh y) |^ 6 is V11() real ext-real Element of REAL
6 * y is V11() real ext-real set
cosh (6 * y) is V11() real ext-real Element of REAL
6 * (cosh (4 * y)) is V11() real ext-real set
(cosh (6 * y)) + (6 * (cosh (4 * y))) is V11() real ext-real set
15 * (cosh (2 * y)) is V11() real ext-real set
((cosh (6 * y)) + (6 * (cosh (4 * y)))) + (15 * (cosh (2 * y))) is V11() real ext-real set
(((cosh (6 * y)) + (6 * (cosh (4 * y)))) + (15 * (cosh (2 * y)))) + 10 is V11() real ext-real set
((((cosh (6 * y)) + (6 * (cosh (4 * y)))) + (15 * (cosh (2 * y)))) + 10) / 32 is V11() real ext-real set
(cosh y) |^ 7 is V11() real ext-real Element of REAL
7 * y is V11() real ext-real set
cosh (7 * y) is V11() real ext-real Element of REAL
7 * (cosh (5 * y)) is V11() real ext-real set
(cosh (7 * y)) + (7 * (cosh (5 * y))) is V11() real ext-real set
21 * (cosh (3 * y)) is V11() real ext-real set
((cosh (7 * y)) + (7 * (cosh (5 * y)))) + (21 * (cosh (3 * y))) is V11() real ext-real set
35 * (cosh y) is V11() real ext-real set
(((cosh (7 * y)) + (7 * (cosh (5 * y)))) + (21 * (cosh (3 * y)))) + (35 * (cosh y)) is V11() real ext-real set
((((cosh (7 * y)) + (7 * (cosh (5 * y)))) + (21 * (cosh (3 * y)))) + (35 * (cosh y))) / 64 is V11() real ext-real set
(cosh y) |^ 8 is V11() real ext-real Element of REAL
8 * y is V11() real ext-real set
cosh (8 * y) is V11() real ext-real Element of REAL
8 * (cosh (6 * y)) is V11() real ext-real set
(cosh (8 * y)) + (8 * (cosh (6 * y))) is V11() real ext-real set
28 * (cosh (4 * y)) is V11() real ext-real set
((cosh (8 * y)) + (8 * (cosh (6 * y)))) + (28 * (cosh (4 * y))) is V11() real ext-real set
56 * (cosh (2 * y)) is V11() real ext-real set
(((cosh (8 * y)) + (8 * (cosh (6 * y)))) + (28 * (cosh (4 * y)))) + (56 * (cosh (2 * y))) is V11() real ext-real set
((((cosh (8 * y)) + (8 * (cosh (6 * y)))) + (28 * (cosh (4 * y)))) + (56 * (cosh (2 * y)))) + 35 is V11() real ext-real set
(((((cosh (8 * y)) + (8 * (cosh (6 * y)))) + (28 * (cosh (4 * y)))) + (56 * (cosh (2 * y)))) + 35) / 128 is V11() real ext-real set
1 + 1 is V1() ordinal natural V11() real ext-real positive non negative set
(1 + 1) + 1 is V1() ordinal natural V11() real ext-real positive non negative set
(cosh y) |^ ((1 + 1) + 1) is V11() real ext-real Element of REAL
(cosh y) |^ (1 + 1) is V11() real ext-real Element of REAL
((cosh y) |^ (1 + 1)) * (cosh y) is V11() real ext-real set
(cosh y) |^ 1 is V11() real ext-real Element of REAL
((cosh y) |^ 1) * (cosh y) is V11() real ext-real set
(((cosh y) |^ 1) * (cosh y)) * (cosh y) is V11() real ext-real set
(cosh y) ^2 is V11() real ext-real Element of REAL
(cosh y) * (cosh y) is V11() real ext-real set
((cosh y) ^2) * (cosh y) is V11() real ext-real set
sinh y is V11() real ext-real Element of REAL
(sinh y) ^2 is V11() real ext-real Element of REAL
(sinh y) * (sinh y) is V11() real ext-real set
((cosh y) ^2) - ((sinh y) ^2) is V11() real ext-real set
(((cosh y) ^2) - ((sinh y) ^2)) + ((sinh y) ^2) is V11() real ext-real set
(cosh y) * ((((cosh y) ^2) - ((sinh y) ^2)) + ((sinh y) ^2)) is V11() real ext-real set
3 * ((cosh y) * ((((cosh y) ^2) - ((sinh y) ^2)) + ((sinh y) ^2))) is V11() real ext-real set
(((cosh y) ^2) * (cosh y)) + (3 * ((cosh y) * ((((cosh y) ^2) - ((sinh y) ^2)) + ((sinh y) ^2)))) is V11() real ext-real set
((((cosh y) ^2) * (cosh y)) + (3 * ((cosh y) * ((((cosh y) ^2) - ((sinh y) ^2)) + ((sinh y) ^2))))) / 4 is V11() real ext-real set
1 + ((sinh y) ^2) is V11() real ext-real set
(cosh y) * (1 + ((sinh y) ^2)) is V11() real ext-real set
3 * ((cosh y) * (1 + ((sinh y) ^2))) is V11() real ext-real set
(((cosh y) ^2) * (cosh y)) + (3 * ((cosh y) * (1 + ((sinh y) ^2)))) is V11() real ext-real set
((((cosh y) ^2) * (cosh y)) + (3 * ((cosh y) * (1 + ((sinh y) ^2))))) / 4 is V11() real ext-real set
((cosh y) * (cosh y)) + ((sinh y) ^2) is V11() real ext-real set
(cosh y) * (((cosh y) * (cosh y)) + ((sinh y) ^2)) is V11() real ext-real set
(cosh y) * ((sinh y) ^2) is V11() real ext-real set
2 * ((cosh y) * ((sinh y) ^2)) is V11() real ext-real set
((cosh y) * (((cosh y) * (cosh y)) + ((sinh y) ^2))) + (2 * ((cosh y) * ((sinh y) ^2))) is V11() real ext-real set
(((cosh y) * (((cosh y) * (cosh y)) + ((sinh y) ^2))) + (2 * ((cosh y) * ((sinh y) ^2)))) + (3 * (cosh y)) is V11() real ext-real set
((((cosh y) * (((cosh y) * (cosh y)) + ((sinh y) ^2))) + (2 * ((cosh y) * ((sinh y) ^2)))) + (3 * (cosh y))) / 4 is V11() real ext-real set
y + y is V11() real ext-real set
cosh (y + y) is V11() real ext-real Element of REAL
(cosh y) * (cosh (y + y)) is V11() real ext-real set
((cosh y) * (cosh (y + y))) + (2 * ((cosh y) * ((sinh y) ^2))) is V11() real ext-real set
(((cosh y) * (cosh (y + y))) + (2 * ((cosh y) * ((sinh y) ^2)))) + (3 * (cosh y)) is V11() real ext-real set
((((cosh y) * (cosh (y + y))) + (2 * ((cosh y) * ((sinh y) ^2)))) + (3 * (cosh y))) / 4 is V11() real ext-real set
(cosh y) * (cosh (2 * y)) is V11() real ext-real set
2 * (sinh y) is V11() real ext-real set
(2 * (sinh y)) * (cosh y) is V11() real ext-real set
((2 * (sinh y)) * (cosh y)) * (sinh y) is V11() real ext-real set
((cosh y) * (cosh (2 * y))) + (((2 * (sinh y)) * (cosh y)) * (sinh y)) is V11() real ext-real set
(((cosh y) * (cosh (2 * y))) + (((2 * (sinh y)) * (cosh y)) * (sinh y))) + (3 * (cosh y)) is V11() real ext-real set
((((cosh y) * (cosh (2 * y))) + (((2 * (sinh y)) * (cosh y)) * (sinh y))) + (3 * (cosh y))) / 4 is V11() real ext-real set
(cosh (2 * y)) * (cosh y) is V11() real ext-real set
sinh (2 * y) is V11() real ext-real Element of REAL
(sinh (2 * y)) * (sinh y) is V11() real ext-real set
((cosh (2 * y)) * (cosh y)) + ((sinh (2 * y)) * (sinh y)) is V11() real ext-real set
(((cosh (2 * y)) * (cosh y)) + ((sinh (2 * y)) * (sinh y))) + (3 * (cosh y)) is V11() real ext-real set
((((cosh (2 * y)) * (cosh y)) + ((sinh (2 * y)) * (sinh y))) + (3 * (cosh y))) / 4 is V11() real ext-real set
(y + y) + y is V11() real ext-real set
cosh ((y + y) + y) is V11() real ext-real Element of REAL
(cosh ((y + y) + y)) + (3 * (cosh y)) is V11() real ext-real set
((cosh ((y + y) + y)) + (3 * (cosh y))) / 4 is V11() real ext-real set
(((cosh (3 * y)) + (3 * (cosh y))) / 4) * (cosh y) is V11() real ext-real set
(cosh (3 * y)) * (cosh y) is V11() real ext-real set
3 * ((cosh y) * (cosh y)) is V11() real ext-real set
((cosh (3 * y)) * (cosh y)) + (3 * ((cosh y) * (cosh y))) is V11() real ext-real set
(((cosh (3 * y)) * (cosh y)) + (3 * ((cosh y) * (cosh y)))) / 4 is V11() real ext-real set
1 * y is V11() real ext-real set
(3 * y) + (1 * y) is V11() real ext-real set
cosh ((3 * y) + (1 * y)) is V11() real ext-real Element of REAL
(3 * y) - y is V11() real ext-real set
cosh ((3 * y) - y) is V11() real ext-real Element of REAL
(cosh ((3 * y) + (1 * y))) + (cosh ((3 * y) - y)) is V11() real ext-real set
(1 / 2) * ((cosh ((3 * y) + (1 * y))) + (cosh ((3 * y) - y))) is V11() real ext-real set
((1 / 2) * ((cosh ((3 * y) + (1 * y))) + (cosh ((3 * y) - y)))) + (3 * ((cosh y) * (cosh y))) is V11() real ext-real set
(((1 / 2) * ((cosh ((3 * y) + (1 * y))) + (cosh ((3 * y) - y)))) + (3 * ((cosh y) * (cosh y)))) / 4 is V11() real ext-real set
(cosh (4 * y)) + (cosh (2 * y)) is V11() real ext-real set
(1 / 2) * ((cosh (4 * y)) + (cosh (2 * y))) is V11() real ext-real set
y - y is V11() real ext-real set
cosh (y - y) is V11() real ext-real Element of REAL
(cosh (y + y)) + (cosh (y - y)) is V11() real ext-real set
(1 / 2) * ((cosh (y + y)) + (cosh (y - y))) is V11() real ext-real set
3 * ((1 / 2) * ((cosh (y + y)) + (cosh (y - y)))) is V11() real ext-real set
((1 / 2) * ((cosh (4 * y)) + (cosh (2 * y)))) + (3 * ((1 / 2) * ((cosh (y + y)) + (cosh (y - y))))) is V11() real ext-real set
(((1 / 2) * ((cosh (4 * y)) + (cosh (2 * y)))) + (3 * ((1 / 2) * ((cosh (y + y)) + (cosh (y - y)))))) / 4 is V11() real ext-real set
(cosh (2 * y)) + 1 is V11() real ext-real set
(1 / 2) * ((cosh (2 * y)) + 1) is V11() real ext-real set
((1 / 2) * ((cosh (2 * y)) + 1)) * 3 is V11() real ext-real set
((1 / 2) * ((cosh (4 * y)) + (cosh (2 * y)))) + (((1 / 2) * ((cosh (2 * y)) + 1)) * 3) is V11() real ext-real set
(((1 / 2) * ((cosh (4 * y)) + (cosh (2 * y)))) + (((1 / 2) * ((cosh (2 * y)) + 1)) * 3)) / 4 is V11() real ext-real set
4 + 1 is V1() ordinal natural V11() real ext-real positive non negative set
(cosh y) |^ (4 + 1) is V11() real ext-real Element of REAL
((((cosh (4 * y)) + (4 * (cosh (2 * y)))) + 3) / 8) * (cosh y) is V11() real ext-real set
(cosh (4 * y)) * (cosh y) is V11() real ext-real set
4 * ((cosh (2 * y)) * (cosh y)) is V11() real ext-real set
((cosh (4 * y)) * (cosh y)) + (4 * ((cosh (2 * y)) * (cosh y))) is V11() real ext-real set
(((cosh (4 * y)) * (cosh y)) + (4 * ((cosh (2 * y)) * (cosh y)))) + (3 * (cosh y)) is V11() real ext-real set
((((cosh (4 * y)) * (cosh y)) + (4 * ((cosh (2 * y)) * (cosh y)))) + (3 * (cosh y))) / 8 is V11() real ext-real set
(4 * y) + (1 * y) is V11() real ext-real set
cosh ((4 * y) + (1 * y)) is V11() real ext-real Element of REAL
(4 * y) - y is V11() real ext-real set
cosh ((4 * y) - y) is V11() real ext-real Element of REAL
(cosh ((4 * y) + (1 * y))) + (cosh ((4 * y) - y)) is V11() real ext-real set
(1 / 2) * ((cosh ((4 * y) + (1 * y))) + (cosh ((4 * y) - y))) is V11() real ext-real set
((1 / 2) * ((cosh ((4 * y) + (1 * y))) + (cosh ((4 * y) - y)))) + (4 * ((cosh (2 * y)) * (cosh y))) is V11() real ext-real set
(((1 / 2) * ((cosh ((4 * y) + (1 * y))) + (cosh ((4 * y) - y)))) + (4 * ((cosh (2 * y)) * (cosh y)))) + (3 * (cosh y)) is V11() real ext-real set
((((1 / 2) * ((cosh ((4 * y) + (1 * y))) + (cosh ((4 * y) - y)))) + (4 * ((cosh (2 * y)) * (cosh y)))) + (3 * (cosh y))) / 8 is V11() real ext-real set
(cosh (5 * y)) + (cosh (3 * y)) is V11() real ext-real set
(1 / 2) * ((cosh (5 * y)) + (cosh (3 * y))) is V11() real ext-real set
(2 * y) + (1 * y) is V11() real ext-real set
cosh ((2 * y) + (1 * y)) is V11() real ext-real Element of REAL
(2 * y) - y is V11() real ext-real set
cosh ((2 * y) - y) is V11() real ext-real Element of REAL
(cosh ((2 * y) + (1 * y))) + (cosh ((2 * y) - y)) is V11() real ext-real set
(1 / 2) * ((cosh ((2 * y) + (1 * y))) + (cosh ((2 * y) - y))) is V11() real ext-real set
4 * ((1 / 2) * ((cosh ((2 * y) + (1 * y))) + (cosh ((2 * y) - y)))) is V11() real ext-real set
((1 / 2) * ((cosh (5 * y)) + (cosh (3 * y)))) + (4 * ((1 / 2) * ((cosh ((2 * y) + (1 * y))) + (cosh ((2 * y) - y))))) is V11() real ext-real set
(((1 / 2) * ((cosh (5 * y)) + (cosh (3 * y)))) + (4 * ((1 / 2) * ((cosh ((2 * y) + (1 * y))) + (cosh ((2 * y) - y)))))) + (3 * (cosh y)) is V11() real ext-real set
((((1 / 2) * ((cosh (5 * y)) + (cosh (3 * y)))) + (4 * ((1 / 2) * ((cosh ((2 * y) + (1 * y))) + (cosh ((2 * y) - y)))))) + (3 * (cosh y))) / 8 is V11() real ext-real set
5 + 1 is V1() ordinal natural V11() real ext-real positive non negative set
(cosh y) |^ (5 + 1) is V11() real ext-real Element of REAL
((((cosh (5 * y)) + (5 * (cosh (3 * y)))) + (10 * (cosh y))) / 16) * (cosh y) is V11() real ext-real set
(cosh (5 * y)) * (cosh y) is V11() real ext-real set
5 * ((cosh (3 * y)) * (cosh y)) is V11() real ext-real set
((cosh (5 * y)) * (cosh y)) + (5 * ((cosh (3 * y)) * (cosh y))) is V11() real ext-real set
10 * ((cosh y) * (cosh y)) is V11() real ext-real set
(((cosh (5 * y)) * (cosh y)) + (5 * ((cosh (3 * y)) * (cosh y)))) + (10 * ((cosh y) * (cosh y))) is V11() real ext-real set
((((cosh (5 * y)) * (cosh y)) + (5 * ((cosh (3 * y)) * (cosh y)))) + (10 * ((cosh y) * (cosh y)))) / 16 is V11() real ext-real set
(5 * y) + y is V11() real ext-real set
cosh ((5 * y) + y) is V11() real ext-real Element of REAL
(5 * y) - y is V11() real ext-real set
cosh ((5 * y) - y) is V11() real ext-real Element of REAL
(cosh ((5 * y) + y)) + (cosh ((5 * y) - y)) is V11() real ext-real set
(1 / 2) * ((cosh ((5 * y) + y)) + (cosh ((5 * y) - y))) is V11() real ext-real set
((1 / 2) * ((cosh ((5 * y) + y)) + (cosh ((5 * y) - y)))) + (5 * ((cosh (3 * y)) * (cosh y))) is V11() real ext-real set
(((1 / 2) * ((cosh ((5 * y) + y)) + (cosh ((5 * y) - y)))) + (5 * ((cosh (3 * y)) * (cosh y)))) + (10 * ((cosh y) * (cosh y))) is V11() real ext-real set
((((1 / 2) * ((cosh ((5 * y) + y)) + (cosh ((5 * y) - y)))) + (5 * ((cosh (3 * y)) * (cosh y)))) + (10 * ((cosh y) * (cosh y)))) / 16 is V11() real ext-real set
(3 * y) + y is V11() real ext-real set
cosh ((3 * y) + y) is V11() real ext-real Element of REAL
(cosh ((3 * y) + y)) + (cosh ((3 * y) - y)) is V11() real ext-real set
(1 / 2) * ((cosh ((3 * y) + y)) + (cosh ((3 * y) - y))) is V11() real ext-real set
((1 / 2) * ((cosh ((3 * y) + y)) + (cosh ((3 * y) - y)))) * 5 is V11() real ext-real set
((1 / 2) * ((cosh ((5 * y) + y)) + (cosh ((5 * y) - y)))) + (((1 / 2) * ((cosh ((3 * y) + y)) + (cosh ((3 * y) - y)))) * 5) is V11() real ext-real set
(((1 / 2) * ((cosh ((5 * y) + y)) + (cosh ((5 * y) - y)))) + (((1 / 2) * ((cosh ((3 * y) + y)) + (cosh ((3 * y) - y)))) * 5)) + (10 * ((cosh y) * (cosh y))) is V11() real ext-real set
((((1 / 2) * ((cosh ((5 * y) + y)) + (cosh ((5 * y) - y)))) + (((1 / 2) * ((cosh ((3 * y) + y)) + (cosh ((3 * y) - y)))) * 5)) + (10 * ((cosh y) * (cosh y)))) / 16 is V11() real ext-real set
(cosh (2 * y)) * 5 is V11() real ext-real set
((cosh (6 * y)) + (6 * (cosh (4 * y)))) + ((cosh (2 * y)) * 5) is V11() real ext-real set
(1 / 2) * (((cosh (6 * y)) + (6 * (cosh (4 * y)))) + ((cosh (2 * y)) * 5)) is V11() real ext-real set
10 * ((cosh y) ^2) is V11() real ext-real set
((1 / 2) * (((cosh (6 * y)) + (6 * (cosh (4 * y)))) + ((cosh (2 * y)) * 5))) + (10 * ((cosh y) ^2)) is V11() real ext-real set
(((1 / 2) * (((cosh (6 * y)) + (6 * (cosh (4 * y)))) + ((cosh (2 * y)) * 5))) + (10 * ((cosh y) ^2))) / 16 is V11() real ext-real set
((1 / 2) * ((cosh (2 * y)) + 1)) * 10 is V11() real ext-real set
((1 / 2) * (((cosh (6 * y)) + (6 * (cosh (4 * y)))) + ((cosh (2 * y)) * 5))) + (((1 / 2) * ((cosh (2 * y)) + 1)) * 10) is V11() real ext-real set
(((1 / 2) * (((cosh (6 * y)) + (6 * (cosh (4 * y)))) + ((cosh (2 * y)) * 5))) + (((1 / 2) * ((cosh (2 * y)) + 1)) * 10)) / 16 is V11() real ext-real set
6 + 1 is V1() ordinal natural V11() real ext-real positive non negative set
(cosh y) |^ (6 + 1) is V11() real ext-real Element of REAL
(((((cosh (6 * y)) + (6 * (cosh (4 * y)))) + (15 * (cosh (2 * y)))) + 10) / 32) * (cosh y) is V11() real ext-real set
(cosh (6 * y)) * (cosh y) is V11() real ext-real set
6 * ((cosh (4 * y)) * (cosh y)) is V11() real ext-real set
((cosh (6 * y)) * (cosh y)) + (6 * ((cosh (4 * y)) * (cosh y))) is V11() real ext-real set
15 * ((cosh (2 * y)) * (cosh y)) is V11() real ext-real set
(((cosh (6 * y)) * (cosh y)) + (6 * ((cosh (4 * y)) * (cosh y)))) + (15 * ((cosh (2 * y)) * (cosh y))) is V11() real ext-real set
((((cosh (6 * y)) * (cosh y)) + (6 * ((cosh (4 * y)) * (cosh y)))) + (15 * ((cosh (2 * y)) * (cosh y)))) + (10 * (cosh y)) is V11() real ext-real set
(((((cosh (6 * y)) * (cosh y)) + (6 * ((cosh (4 * y)) * (cosh y)))) + (15 * ((cosh (2 * y)) * (cosh y)))) + (10 * (cosh y))) / 32 is V11() real ext-real set
(6 * y) + (1 * y) is V11() real ext-real set
cosh ((6 * y) + (1 * y)) is V11() real ext-real Element of REAL
(6 * y) - (1 * y) is V11() real ext-real set
cosh ((6 * y) - (1 * y)) is V11() real ext-real Element of REAL
(cosh ((6 * y) + (1 * y))) + (cosh ((6 * y) - (1 * y))) is V11() real ext-real set
(1 / 2) * ((cosh ((6 * y) + (1 * y))) + (cosh ((6 * y) - (1 * y)))) is V11() real ext-real set
((1 / 2) * ((cosh ((6 * y) + (1 * y))) + (cosh ((6 * y) - (1 * y))))) + (6 * ((cosh (4 * y)) * (cosh y))) is V11() real ext-real set
(((1 / 2) * ((cosh ((6 * y) + (1 * y))) + (cosh ((6 * y) - (1 * y))))) + (6 * ((cosh (4 * y)) * (cosh y)))) + (15 * ((cosh (2 * y)) * (cosh y))) is V11() real ext-real set
((((1 / 2) * ((cosh ((6 * y) + (1 * y))) + (cosh ((6 * y) - (1 * y))))) + (6 * ((cosh (4 * y)) * (cosh y)))) + (15 * ((cosh (2 * y)) * (cosh y)))) + (10 * (cosh y)) is V11() real ext-real set
(((((1 / 2) * ((cosh ((6 * y) + (1 * y))) + (cosh ((6 * y) - (1 * y))))) + (6 * ((cosh (4 * y)) * (cosh y)))) + (15 * ((cosh (2 * y)) * (cosh y)))) + (10 * (cosh y))) / 32 is V11() real ext-real set
(cosh (7 * y)) + (cosh (5 * y)) is V11() real ext-real set
(1 / 2) * ((cosh (7 * y)) + (cosh (5 * y))) is V11() real ext-real set
(4 * y) + y is V11() real ext-real set
cosh ((4 * y) + y) is V11() real ext-real Element of REAL
(cosh ((4 * y) + y)) + (cosh ((4 * y) - y)) is V11() real ext-real set
(1 / 2) * ((cosh ((4 * y) + y)) + (cosh ((4 * y) - y))) is V11() real ext-real set
((1 / 2) * ((cosh ((4 * y) + y)) + (cosh ((4 * y) - y)))) * 6 is V11() real ext-real set
((1 / 2) * ((cosh (7 * y)) + (cosh (5 * y)))) + (((1 / 2) * ((cosh ((4 * y) + y)) + (cosh ((4 * y) - y)))) * 6) is V11() real ext-real set
(((1 / 2) * ((cosh (7 * y)) + (cosh (5 * y)))) + (((1 / 2) * ((cosh ((4 * y) + y)) + (cosh ((4 * y) - y)))) * 6)) + (15 * ((cosh (2 * y)) * (cosh y))) is V11() real ext-real set
((((1 / 2) * ((cosh (7 * y)) + (cosh (5 * y)))) + (((1 / 2) * ((cosh ((4 * y) + y)) + (cosh ((4 * y) - y)))) * 6)) + (15 * ((cosh (2 * y)) * (cosh y)))) + (10 * (cosh y)) is V11() real ext-real set
(((((1 / 2) * ((cosh (7 * y)) + (cosh (5 * y)))) + (((1 / 2) * ((cosh ((4 * y) + y)) + (cosh ((4 * y) - y)))) * 6)) + (15 * ((cosh (2 * y)) * (cosh y)))) + (10 * (cosh y))) / 32 is V11() real ext-real set
(cosh (3 * y)) * 6 is V11() real ext-real set
((cosh (7 * y)) + (7 * (cosh (5 * y)))) + ((cosh (3 * y)) * 6) is V11() real ext-real set
(1 / 2) * (((cosh (7 * y)) + (7 * (cosh (5 * y)))) + ((cosh (3 * y)) * 6)) is V11() real ext-real set
(2 * y) + y is V11() real ext-real set
cosh ((2 * y) + y) is V11() real ext-real Element of REAL
(cosh ((2 * y) + y)) + (cosh ((2 * y) - y)) is V11() real ext-real set
(1 / 2) * ((cosh ((2 * y) + y)) + (cosh ((2 * y) - y))) is V11() real ext-real set
((1 / 2) * ((cosh ((2 * y) + y)) + (cosh ((2 * y) - y)))) * 15 is V11() real ext-real set
((1 / 2) * (((cosh (7 * y)) + (7 * (cosh (5 * y)))) + ((cosh (3 * y)) * 6))) + (((1 / 2) * ((cosh ((2 * y) + y)) + (cosh ((2 * y) - y)))) * 15) is V11() real ext-real set
(((1 / 2) * (((cosh (7 * y)) + (7 * (cosh (5 * y)))) + ((cosh (3 * y)) * 6))) + (((1 / 2) * ((cosh ((2 * y) + y)) + (cosh ((2 * y) - y)))) * 15)) + (10 * (cosh y)) is V11() real ext-real set
((((1 / 2) * (((cosh (7 * y)) + (7 * (cosh (5 * y)))) + ((cosh (3 * y)) * 6))) + (((1 / 2) * ((cosh ((2 * y) + y)) + (cosh ((2 * y) - y)))) * 15)) + (10 * (cosh y))) / 32 is V11() real ext-real set
7 + 1 is V1() ordinal natural V11() real ext-real positive non negative set
(cosh y) |^ (7 + 1) is V11() real ext-real Element of REAL
(((((cosh (7 * y)) + (7 * (cosh (5 * y)))) + (21 * (cosh (3 * y)))) + (35 * (cosh y))) / 64) * (cosh y) is V11() real ext-real set
(cosh (7 * y)) * (cosh y) is V11() real ext-real set
(7 * (cosh (5 * y))) * (cosh y) is V11() real ext-real set
((cosh (7 * y)) * (cosh y)) + ((7 * (cosh (5 * y))) * (cosh y)) is V11() real ext-real set
(21 * (cosh (3 * y))) * (cosh y) is V11() real ext-real set
(((cosh (7 * y)) * (cosh y)) + ((7 * (cosh (5 * y))) * (cosh y))) + ((21 * (cosh (3 * y))) * (cosh y)) is V11() real ext-real set
35 * ((cosh y) ^2) is V11() real ext-real set
((((cosh (7 * y)) * (cosh y)) + ((7 * (cosh (5 * y))) * (cosh y))) + ((21 * (cosh (3 * y))) * (cosh y))) + (35 * ((cosh y) ^2)) is V11() real ext-real set
(((((cosh (7 * y)) * (cosh y)) + ((7 * (cosh (5 * y))) * (cosh y))) + ((21 * (cosh (3 * y))) * (cosh y))) + (35 * ((cosh y) ^2))) / 64 is V11() real ext-real set
(7 * y) + (1 * y) is V11() real ext-real set
cosh ((7 * y) + (1 * y)) is V11() real ext-real Element of REAL
(7 * y) - y is V11() real ext-real set
cosh ((7 * y) - y) is V11() real ext-real Element of REAL
(cosh ((7 * y) + (1 * y))) + (cosh ((7 * y) - y)) is V11() real ext-real set
(1 / 2) * ((cosh ((7 * y) + (1 * y))) + (cosh ((7 * y) - y))) is V11() real ext-real set
((1 / 2) * ((cosh ((7 * y) + (1 * y))) + (cosh ((7 * y) - y)))) + ((7 * (cosh (5 * y))) * (cosh y)) is V11() real ext-real set
(((1 / 2) * ((cosh ((7 * y) + (1 * y))) + (cosh ((7 * y) - y)))) + ((7 * (cosh (5 * y))) * (cosh y))) + ((21 * (cosh (3 * y))) * (cosh y)) is V11() real ext-real set
((((1 / 2) * ((cosh ((7 * y) + (1 * y))) + (cosh ((7 * y) - y)))) + ((7 * (cosh (5 * y))) * (cosh y))) + ((21 * (cosh (3 * y))) * (cosh y))) + (35 * ((cosh y) ^2)) is V11() real ext-real set
(((((1 / 2) * ((cosh ((7 * y) + (1 * y))) + (cosh ((7 * y) - y)))) + ((7 * (cosh (5 * y))) * (cosh y))) + ((21 * (cosh (3 * y))) * (cosh y))) + (35 * ((cosh y) ^2))) / 64 is V11() real ext-real set
(cosh (8 * y)) + (cosh (6 * y)) is V11() real ext-real set
(1 / 2) * ((cosh (8 * y)) + (cosh (6 * y))) is V11() real ext-real set
7 * ((cosh (5 * y)) * (cosh y)) is V11() real ext-real set
((1 / 2) * ((cosh (8 * y)) + (cosh (6 * y)))) + (7 * ((cosh (5 * y)) * (cosh y))) is V11() real ext-real set
(((1 / 2) * ((cosh (8 * y)) + (cosh (6 * y)))) + (7 * ((cosh (5 * y)) * (cosh y)))) + ((21 * (cosh (3 * y))) * (cosh y)) is V11() real ext-real set
((((1 / 2) * ((cosh (8 * y)) + (cosh (6 * y)))) + (7 * ((cosh (5 * y)) * (cosh y)))) + ((21 * (cosh (3 * y))) * (cosh y))) + (35 * ((cosh y) ^2)) is V11() real ext-real set
(((((1 / 2) * ((cosh (8 * y)) + (cosh (6 * y)))) + (7 * ((cosh (5 * y)) * (cosh y)))) + ((21 * (cosh (3 * y))) * (cosh y))) + (35 * ((cosh y) ^2))) / 64 is V11() real ext-real set
(5 * y) + (1 * y) is V11() real ext-real set
cosh ((5 * y) + (1 * y)) is V11() real ext-real Element of REAL
(5 * y) - (1 * y) is V11() real ext-real set
cosh ((5 * y) - (1 * y)) is V11() real ext-real Element of REAL
(cosh ((5 * y) + (1 * y))) + (cosh ((5 * y) - (1 * y))) is V11() real ext-real set
(1 / 2) * ((cosh ((5 * y) + (1 * y))) + (cosh ((5 * y) - (1 * y)))) is V11() real ext-real set
7 * ((1 / 2) * ((cosh ((5 * y) + (1 * y))) + (cosh ((5 * y) - (1 * y))))) is V11() real ext-real set
((1 / 2) * ((cosh (8 * y)) + (cosh (6 * y)))) + (7 * ((1 / 2) * ((cosh ((5 * y) + (1 * y))) + (cosh ((5 * y) - (1 * y)))))) is V11() real ext-real set
(((1 / 2) * ((cosh (8 * y)) + (cosh (6 * y)))) + (7 * ((1 / 2) * ((cosh ((5 * y) + (1 * y))) + (cosh ((5 * y) - (1 * y))))))) + ((21 * (cosh (3 * y))) * (cosh y)) is V11() real ext-real set
((((1 / 2) * ((cosh (8 * y)) + (cosh (6 * y)))) + (7 * ((1 / 2) * ((cosh ((5 * y) + (1 * y))) + (cosh ((5 * y) - (1 * y))))))) + ((21 * (cosh (3 * y))) * (cosh y))) + (35 * ((cosh y) ^2)) is V11() real ext-real set
(((((1 / 2) * ((cosh (8 * y)) + (cosh (6 * y)))) + (7 * ((1 / 2) * ((cosh ((5 * y) + (1 * y))) + (cosh ((5 * y) - (1 * y))))))) + ((21 * (cosh (3 * y))) * (cosh y))) + (35 * ((cosh y) ^2))) / 64 is V11() real ext-real set
(cosh (4 * y)) * 7 is V11() real ext-real set
((cosh (8 * y)) + (8 * (cosh (6 * y)))) + ((cosh (4 * y)) * 7) is V11() real ext-real set
(1 / 2) * (((cosh (8 * y)) + (8 * (cosh (6 * y)))) + ((cosh (4 * y)) * 7)) is V11() real ext-real set
21 * ((cosh (3 * y)) * (cosh y)) is V11() real ext-real set
((1 / 2) * (((cosh (8 * y)) + (8 * (cosh (6 * y)))) + ((cosh (4 * y)) * 7))) + (21 * ((cosh (3 * y)) * (cosh y))) is V11() real ext-real set
(((1 / 2) * (((cosh (8 * y)) + (8 * (cosh (6 * y)))) + ((cosh (4 * y)) * 7))) + (21 * ((cosh (3 * y)) * (cosh y)))) + (35 * ((cosh y) ^2)) is V11() real ext-real set
((((1 / 2) * (((cosh (8 * y)) + (8 * (cosh (6 * y)))) + ((cosh (4 * y)) * 7))) + (21 * ((cosh (3 * y)) * (cosh y)))) + (35 * ((cosh y) ^2))) / 64 is V11() real ext-real set
21 * ((1 / 2) * ((cosh ((3 * y) + (1 * y))) + (cosh ((3 * y) - y)))) is V11() real ext-real set
((1 / 2) * (((cosh (8 * y)) + (8 * (cosh (6 * y)))) + ((cosh (4 * y)) * 7))) + (21 * ((1 / 2) * ((cosh ((3 * y) + (1 * y))) + (cosh ((3 * y) - y))))) is V11() real ext-real set
(((1 / 2) * (((cosh (8 * y)) + (8 * (cosh (6 * y)))) + ((cosh (4 * y)) * 7))) + (21 * ((1 / 2) * ((cosh ((3 * y) + (1 * y))) + (cosh ((3 * y) - y)))))) + (35 * ((cosh y) ^2)) is V11() real ext-real set
((((1 / 2) * (((cosh (8 * y)) + (8 * (cosh (6 * y)))) + ((cosh (4 * y)) * 7))) + (21 * ((1 / 2) * ((cosh ((3 * y) + (1 * y))) + (cosh ((3 * y) - y)))))) + (35 * ((cosh y) ^2))) / 64 is V11() real ext-real set
(cosh (2 * y)) * 21 is V11() real ext-real set
(((cosh (8 * y)) + (8 * (cosh (6 * y)))) + (28 * (cosh (4 * y)))) + ((cosh (2 * y)) * 21) is V11() real ext-real set
(1 / 2) * ((((cosh (8 * y)) + (8 * (cosh (6 * y)))) + (28 * (cosh (4 * y)))) + ((cosh (2 * y)) * 21)) is V11() real ext-real set
((1 / 2) * ((cosh (2 * y)) + 1)) * 35 is V11() real ext-real set
((1 / 2) * ((((cosh (8 * y)) + (8 * (cosh (6 * y)))) + (28 * (cosh (4 * y)))) + ((cosh (2 * y)) * 21))) + (((1 / 2) * ((cosh (2 * y)) + 1)) * 35) is V11() real ext-real set
(((1 / 2) * ((((cosh (8 * y)) + (8 * (cosh (6 * y)))) + (28 * (cosh (4 * y)))) + ((cosh (2 * y)) * 21))) + (((1 / 2) * ((cosh (2 * y)) + 1)) * 35)) / 64 is V11() real ext-real set
y is V11() real ext-real set
2 * y is V11() real ext-real set
cosh (2 * y) is V11() real ext-real Element of REAL
sinh y is V11() real ext-real Element of REAL
(sinh y) ^2 is V11() real ext-real Element of REAL
(sinh y) * (sinh y) is V11() real ext-real set
z is V11() real ext-real set
2 * z is V11() real ext-real set
cos (2 * z) is V11() real ext-real set
(cosh (2 * y)) + (cos (2 * z)) is V11() real ext-real set
sin z is V11() real ext-real set
(sin z) ^2 is V11() real ext-real set
(sin z) * (sin z) is V11() real ext-real set
((sinh y) ^2) - ((sin z) ^2) is V11() real ext-real set
2 * (((sinh y) ^2) - ((sin z) ^2)) is V11() real ext-real set
2 + (2 * (((sinh y) ^2) - ((sin z) ^2))) is V11() real ext-real set
(cosh (2 * y)) - (cos (2 * z)) is V11() real ext-real set
((sinh y) ^2) + ((sin z) ^2) is V11() real ext-real set
2 * (((sinh y) ^2) + ((sin z) ^2)) is V11() real ext-real set
2 * ((sinh y) ^2) is V11() real ext-real set
1 + (2 * ((sinh y) ^2)) is V11() real ext-real set
(1 + (2 * ((sinh y) ^2))) - (cos (2 * z)) is V11() real ext-real set
2 * ((sin z) ^2) is V11() real ext-real set
1 - (2 * ((sin z) ^2)) is V11() real ext-real set
(1 + (2 * ((sinh y) ^2))) - (1 - (2 * ((sin z) ^2))) is V11() real ext-real set
(1 + (2 * ((sinh y) ^2))) + (cos (2 * z)) is V11() real ext-real set
(1 + (2 * ((sinh y) ^2))) + (1 - (2 * ((sin z) ^2))) is V11() real ext-real set