:: 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) - (