:: SIN_COS8 semantic presentation
begin
theorem
:: SIN_COS8:1
for
x
being ( (
real
) (
V11
()
real
ext-real
)
number
) holds
(
tanh
x
: ( (
real
) (
V11
()
real
ext-real
)
number
) : ( ( ) (
V11
()
real
ext-real
)
Element
of
REAL
: ( ( ) (
V45
()
V46
()
V47
()
V51
() )
set
) )
=
(
sinh
x
: ( (
real
) (
V11
()
real
ext-real
)
number
)
)
: ( ( ) (
V11
()
real
ext-real
)
Element
of
REAL
: ( ( ) (
V45
()
V46
()
V47
()
V51
() )
set
) )
/
(
cosh
x
: ( (
real
) (
V11
()
real
ext-real
)
number
)
)
: ( ( ) (
V11
()
real
ext-real
)
Element
of
REAL
: ( ( ) (
V45
()
V46
()
V47
()
V51
() )
set
) ) : ( ( ) (
V11
()
real
ext-real
)
set
) &
tanh
0
: ( ( ) (
V1
()
ordinal
natural
V11
()
real
ext-real
non
positive
non
negative
V33
()
V34
()
V45
()
V46
()
V47
()
V48
()
V49
()
V50
()
V51
() )
Element
of
NAT
: ( ( ) (
V45
()
V46
()
V47
()
V48
()
V49
()
V50
()
V51
() )
Element
of
K6
(
REAL
: ( ( ) (
V45
()
V46
()
V47
()
V51
() )
set
) ) : ( ( ) ( )
set
) ) ) : ( ( ) (
V11
()
real
ext-real
)
Element
of
REAL
: ( ( ) (
V45
()
V46
()
V47
()
V51
() )
set
) )
=
0
: ( ( ) (
V1
()
ordinal
natural
V11
()
real
ext-real
non
positive
non
negative
V33
()
V34
()
V45
()
V46
()
V47
()
V48
()
V49
()
V50
()
V51
() )
Element
of
NAT
: ( ( ) (
V45
()
V46
()
V47
()
V48
()
V49
()
V50
()
V51
() )
Element
of
K6
(
REAL
: ( ( ) (
V45
()
V46
()
V47
()
V51
() )
set
) ) : ( ( ) ( )
set
) ) ) ) ;
theorem
:: SIN_COS8:2
for
x
being ( (
real
) (
V11
()
real
ext-real
)
number
) holds
(
sinh
x
: ( (
real
) (
V11
()
real
ext-real
)
number
) : ( ( ) (
V11
()
real
ext-real
)
Element
of
REAL
: ( ( ) (
V45
()
V46
()
V47
()
V51
() )
set
) )
=
1 : ( ( ) (
V1
()
ordinal
natural
V11
()
real
ext-real
positive
non
negative
V33
()
V34
()
V45
()
V46
()
V47
()
V48
()
V49
()
V50
() )
Element
of
NAT
: ( ( ) (
V45
()
V46
()
V47
()
V48
()
V49
()
V50
()
V51
() )
Element
of
K6
(
REAL
: ( ( ) (
V45
()
V46
()
V47
()
V51
() )
set
) ) : ( ( ) ( )
set
) ) )
/
(
cosech
x
: ( (
real
) (
V11
()
real
ext-real
)
number
)
)
: ( ( ) (
V11
()
real
ext-real
)
Element
of
REAL
: ( ( ) (
V45
()
V46
()
V47
()
V51
() )
set
) ) : ( ( ) (
V11
()
real
ext-real
)
set
) &
cosh
x
: ( (
real
) (
V11
()
real
ext-real
)
number
) : ( ( ) (
V11
()
real
ext-real
)
Element
of
REAL
: ( ( ) (
V45
()
V46
()
V47
()
V51
() )
set
) )
=
1 : ( ( ) (
V1
()
ordinal
natural
V11
()
real
ext-real
positive
non
negative
V33
()
V34
()
V45
()
V46
()
V47
()
V48
()
V49
()
V50
() )
Element
of
NAT
: ( ( ) (
V45
()
V46
()
V47
()
V48
()
V49
()
V50
()
V51
() )
Element
of
K6
(
REAL
: ( ( ) (
V45
()
V46
()
V47
()
V51
() )
set
) ) : ( ( ) ( )
set
) ) )
/
(
sech
x
: ( (
real
) (
V11
()
real
ext-real
)
number
)
)
: ( ( ) (
V11
()
real
ext-real
)
Element
of
REAL
: ( ( ) (
V45
()
V46
()
V47
()
V51
() )
set
) ) : ( ( ) (
V11
()
real
ext-real
)
set
) &
tanh
x
: ( (
real
) (
V11
()
real
ext-real
)
number
) : ( ( ) (
V11
()
real
ext-real
)
Element
of
REAL
: ( ( ) (
V45
()
V46
()
V47
()
V51
() )
set
) )
=
1 : ( ( ) (
V1
()
ordinal
natural
V11
()
real
ext-real
positive
non
negative
V33
()
V34
()
V45
()
V46
()
V47
()
V48
()
V49
()
V50
() )
Element
of
NAT
: ( ( ) (
V45
()
V46
()
V47
()
V48
()
V49
()
V50
()
V51
() )
Element
of
K6
(
REAL
: ( ( ) (
V45
()
V46
()
V47
()
V51
() )
set
) ) : ( ( ) ( )
set
) ) )
/
(
coth
x
: ( (
real
) (
V11
()
real
ext-real
)
number
)
)
: ( ( ) (
V11
()
real
ext-real
)
Element
of
REAL
: ( ( ) (
V45
()
V46
()
V47
()
V51
() )
set
) ) : ( ( ) (
V11
()
real
ext-real
)
set
) ) ;
theorem
:: SIN_COS8:3
for
x
being ( (
real
) (
V11
()
real
ext-real
)
number
) holds
(
sech
x
: ( (
real
) (
V11
()
real
ext-real
)
number
) : ( ( ) (
V11
()
real
ext-real
)
Element
of
REAL
: ( ( ) (
V45
()
V46
()
V47
()
V51
() )
set
) )
<=
1 : ( ( ) (
V1
()
ordinal
natural
V11
()
real
ext-real
positive
non
negative
V33
()
V34
()
V45
()
V46
()
V47
()
V48
()
V49
()
V50
() )
Element
of
NAT
: ( ( ) (
V45
()
V46
()
V47
()
V48
()
V49
()
V50
()
V51
() )
Element
of
K6
(
REAL
: ( ( ) (
V45
()
V46
()
V47
()
V51
() )
set
) ) : ( ( ) ( )
set
) ) ) &
0
: ( ( ) (
V1
()
ordinal
natural
V11
()
real
ext-real
non
positive
non
negative
V33
()
V34
()
V45
()
V46
()
V47
()
V48
()
V49
()
V50
()
V51
() )
Element
of
NAT
: ( ( ) (
V45
()
V46
()
V47
()
V48
()
V49
()
V50
()
V51
() )
Element
of
K6
(
REAL
: ( ( ) (
V45
()
V46
()
V47
()
V51
() )
set
) ) : ( ( ) ( )
set
) ) )
<
sech
x
: ( (
real
) (
V11
()
real
ext-real
)
number
) : ( ( ) (
V11
()
real
ext-real
)
Element
of
REAL
: ( ( ) (
V45
()
V46
()
V47
()
V51
() )
set
) ) &
sech
0
: ( ( ) (
V1
()
ordinal
natural
V11
()
real
ext-real
non
positive
non
negative
V33
()
V34
()
V45
()
V46
()
V47
()
V48
()
V49
()
V50
()
V51
() )
Element
of
NAT
: ( ( ) (
V45
()
V46
()
V47
()
V48
()
V49
()
V50
()
V51
() )
Element
of
K6
(
REAL
: ( ( ) (
V45
()
V46
()
V47
()
V51
() )
set
) ) : ( ( ) ( )
set
) ) ) : ( ( ) (
V11
()
real
ext-real
)
Element
of
REAL
: ( ( ) (
V45
()
V46
()
V47
()
V51
() )
set
) )
=
1 : ( ( ) (
V1
()
ordinal
natural
V11
()
real
ext-real
positive
non
negative
V33
()
V34
()
V45
()
V46
()
V47
()
V48
()
V49
()
V50
() )
Element
of
NAT
: ( ( ) (
V45
()
V46
()
V47
()
V48
()
V49
()
V50
()
V51
() )
Element
of
K6
(
REAL
: ( ( ) (
V45
()
V46
()
V47
()
V51
() )
set
) ) : ( ( ) ( )
set
) ) ) ) ;
theorem
:: SIN_COS8:4
for
x
being ( (
real
) (
V11
()
real
ext-real
)
number
) st
x
: ( (
real
) (
V11
()
real
ext-real
)
number
)
>=
0
: ( ( ) (
V1
()
ordinal
natural
V11
()
real
ext-real
non
positive
non
negative
V33
()
V34
()
V45
()
V46
()
V47
()
V48
()
V49
()
V50
()
V51
() )
Element
of
NAT
: ( ( ) (
V45
()
V46
()
V47
()
V48
()
V49
()
V50
()
V51
() )
Element
of
K6
(
REAL
: ( ( ) (
V45
()
V46
()
V47
()
V51
() )
set
) ) : ( ( ) ( )
set
) ) ) holds
tanh
x
: ( (
real
) (
V11
()
real
ext-real
)
number
) : ( ( ) (
V11
()
real
ext-real
)
Element
of
REAL
: ( ( ) (
V45
()
V46
()
V47
()
V51
() )
set
) )
>=
0
: ( ( ) (
V1
()
ordinal
natural
V11
()
real
ext-real
non
positive
non
negative
V33
()
V34
()
V45
()
V46
()
V47
()
V48
()
V49
()
V50
()
V51
() )
Element
of
NAT
: ( ( ) (
V45
()
V46
()
V47
()
V48
()
V49
()
V50
()
V51
() )
Element
of
K6
(
REAL
: ( ( ) (
V45
()
V46
()
V47
()
V51
() )
set
) ) : ( ( ) ( )
set
) ) ) ;
theorem
:: SIN_COS8:5
for
x
being ( (
real
) (
V11
()
real
ext-real
)
number
) holds
(
cosh
x
: ( (
real
) (
V11
()
real
ext-real
)
number
) : ( ( ) (
V11
()
real
ext-real
)
Element
of
REAL
: ( ( ) (
V45
()
V46
()
V47
()
V51
() )
set
) )
=
1 : ( ( ) (
V1
()
ordinal
natural
V11
()
real
ext-real
positive
non
negative
V33
()
V34
()
V45
()
V46
()
V47
()
V48
()
V49
()
V50
() )
Element
of
NAT
: ( ( ) (
V45
()
V46
()
V47
()
V48
()
V49
()
V50
()
V51
() )
Element
of
K6
(
REAL
: ( ( ) (
V45
()
V46
()
V47
()
V51
() )
set
) ) : ( ( ) ( )
set
) ) )
/
(
sqrt
(
1 : ( ( ) (
V1
()
ordinal
natural
V11
()
real
ext-real
positive
non
negative
V33
()
V34
()
V45
()
V46
()
V47
()
V48
()
V49
()
V50
() )
Element
of
NAT
: ( ( ) (
V45
()
V46
()
V47
()
V48
()
V49
()
V50
()
V51
() )
Element
of
K6
(
REAL
: ( ( ) (
V45
()
V46
()
V47
()
V51
() )
set
) ) : ( ( ) ( )
set
) ) )
-
(
(
tanh
x
: ( (
real
) (
V11
()
real
ext-real
)
number
)
)
: ( ( ) (
V11
()
real
ext-real
)
Element
of
REAL
: ( ( ) (
V45
()
V46
()
V47
()
V51
() )
set
) )
^2
)
: ( ( ) (
V11
()
real
ext-real
)
Element
of
REAL
: ( ( ) (
V45
()
V46
()
V47
()
V51
() )
set
) )
)
: ( ( ) (
V11
()
real
ext-real
)
set
)
)
: ( (
real
) (
V11
()
real
ext-real
)
set
) : ( ( ) (
V11
()
real
ext-real
)
set
) &
sinh
x
: ( (
real
) (
V11
()
real
ext-real
)
number
) : ( ( ) (
V11
()
real
ext-real
)
Element
of
REAL
: ( ( ) (
V45
()
V46
()
V47
()
V51
() )
set
) )
=
(
tanh
x
: ( (
real
) (
V11
()
real
ext-real
)
number
)
)
: ( ( ) (
V11
()
real
ext-real
)
Element
of
REAL
: ( ( ) (
V45
()
V46
()
V47
()
V51
() )
set
) )
/
(
sqrt
(
1 : ( ( ) (
V1
()
ordinal
natural
V11
()
real
ext-real
positive
non
negative
V33
()
V34
()
V45
()
V46
()
V47
()
V48
()
V49
()
V50
() )
Element
of
NAT
: ( ( ) (
V45
()
V46
()
V47
()
V48
()
V49
()
V50
()
V51
() )
Element
of
K6
(
REAL
: ( ( ) (
V45
()
V46
()
V47
()
V51
() )
set
) ) : ( ( ) ( )
set
) ) )
-
(
(
tanh
x
: ( (
real
) (
V11
()
real
ext-real
)
number
)
)
: ( ( ) (
V11
()
real
ext-real
)
Element
of
REAL
: ( ( ) (
V45
()
V46
()
V47
()
V51
() )
set
) )
^2
)
: ( ( ) (
V11
()
real
ext-real
)
Element
of
REAL
: ( ( ) (
V45
()
V46
()
V47
()
V51
() )
set
) )
)
: ( ( ) (
V11
()
real
ext-real
)
set
)
)
: ( (
real
) (
V11
()
real
ext-real
)
set
) : ( ( ) (
V11
()
real
ext-real
)
set
) ) ;
theorem
:: SIN_COS8:6
for
x
being ( (
real
) (
V11
()
real
ext-real
)
number
)
for
n
being ( ( ) (
ordinal
natural
V11
()
real
ext-real
non
negative
V33
()
V34
()
V45
()
V46
()
V47
()
V48
()
V49
()
V50
() )
Element
of
NAT
: ( ( ) (
V45
()
V46
()
V47
()
V48
()
V49
()
V50
()
V51
() )
Element
of
K6
(
REAL
: ( ( ) (
V45
()
V46
()
V47
()
V51
() )
set
) ) : ( ( ) ( )
set
) ) ) holds
(
(
(
cosh
x
: ( (
real
) (
V11
()
real
ext-real
)
number
)
)
: ( ( ) (
V11
()
real
ext-real
)
Element
of
REAL
: ( ( ) (
V45
()
V46
()
V47
()
V51
() )
set
) )
+
(
sinh
x
: ( (
real
) (
V11
()
real
ext-real
)
number
)
)
: ( ( ) (
V11
()
real
ext-real
)
Element
of
REAL
: ( ( ) (
V45
()
V46
()
V47
()
V51
() )
set
) )
)
: ( ( ) (
V11
()
real
ext-real
)
set
)
|^
n
: ( ( ) (
ordinal
natural
V11
()
real
ext-real
non
negative
V33
()
V34
()
V45
()
V46
()
V47
()
V48
()
V49
()
V50
() )
Element
of
NAT
: ( ( ) (
V45
()
V46
()
V47
()
V48
()
V49
()
V50
()
V51
() )
Element
of
K6
(
REAL
: ( ( ) (
V45
()
V46
()
V47
()
V51
() )
set
) ) : ( ( ) ( )
set
) ) ) : ( ( ) ( )
set
)
=
(
cosh
(
n
: ( ( ) (
ordinal
natural
V11
()
real
ext-real
non
negative
V33
()
V34
()
V45
()
V46
()
V47
()
V48
()
V49
()
V50
() )
Element
of
NAT
: ( ( ) (
V45
()
V46
()
V47
()
V48
()
V49
()
V50
()
V51
() )
Element
of
K6
(
REAL
: ( ( ) (
V45
()
V46
()
V47
()
V51
() )
set
) ) : ( ( ) ( )
set
) ) )
*
x
: ( (
real
) (
V11
()
real
ext-real
)
number
)
)
: ( ( ) (
V11
()
real
ext-real
)
set
)
)
: ( ( ) (
V11
()
real
ext-real
)
Element
of
REAL
: ( ( ) (
V45
()
V46
()
V47
()
V51
() )
set
) )
+
(
sinh
(
n
: ( ( ) (
ordinal
natural
V11
()
real
ext-real
non
negative
V33
()
V34
()
V45
()
V46
()
V47
()
V48
()
V49
()
V50
() )
Element
of
NAT
: ( ( ) (
V45
()
V46
()
V47
()
V48
()
V49
()
V50
()
V51
() )
Element
of
K6
(
REAL
: ( ( ) (
V45
()
V46
()
V47
()
V51
() )
set
) ) : ( ( ) ( )
set
) ) )
*
x
: ( (
real
) (
V11
()
real
ext-real
)
number
)
)
: ( ( ) (
V11
()
real
ext-real
)
set
)
)
: ( ( ) (
V11
()
real
ext-real
)
Element
of
REAL
: ( ( ) (
V45
()
V46
()
V47
()
V51
() )
set
) ) : ( ( ) (
V11
()
real
ext-real
)
set
) &
(
(
cosh
x
: ( (
real
) (
V11
()
real
ext-real
)
number
)
)
: ( ( ) (
V11
()
real
ext-real
)
Element
of
REAL
: ( ( ) (
V45
()
V46
()
V47
()
V51
() )
set
) )
-
(
sinh
x
: ( (
real
) (
V11
()
real
ext-real
)
number
)
)
: ( ( ) (
V11
()
real
ext-real
)
Element
of
REAL
: ( ( ) (
V45
()
V46
()
V47
()
V51
() )
set
) )
)
: ( ( ) (
V11
()
real
ext-real
)
set
)
|^
n
: ( ( ) (
ordinal
natural
V11
()
real
ext-real
non
negative
V33
()
V34
()
V45
()
V46
()
V47
()
V48
()
V49
()
V50
() )
Element
of
NAT
: ( ( ) (
V45
()
V46
()
V47
()
V48
()
V49
()
V50
()
V51
() )
Element
of
K6
(
REAL
: ( ( ) (
V45
()
V46
()
V47
()
V51
() )
set
) ) : ( ( ) ( )
set
) ) ) : ( ( ) ( )
set
)
=
(
cosh
(
n
: ( ( ) (
ordinal
natural
V11
()
real
ext-real
non
negative
V33
()
V34
()
V45
()
V46
()
V47
()
V48
()
V49
()
V50
() )
Element
of
NAT
: ( ( ) (
V45
()
V46
()
V47
()
V48
()
V49
()
V50
()
V51
() )
Element
of
K6
(
REAL
: ( ( ) (
V45
()
V46
()
V47
()
V51
() )
set
) ) : ( ( ) ( )
set
) ) )
*
x
: ( (
real
) (
V11
()
real
ext-real
)
number
)
)
: ( ( ) (
V11
()
real
ext-real
)
set
)
)
: ( ( ) (
V11
()
real
ext-real
)
Element
of
REAL
: ( ( ) (
V45
()
V46
()
V47
()
V51
() )
set
) )
-
(
sinh
(
n
: ( ( ) (
ordinal
natural
V11
()
real
ext-real
non
negative
V33
()
V34
()
V45
()
V46
()
V47
()
V48
()
V49
()
V50
() )
Element
of
NAT
: ( ( ) (
V45
()
V46
()
V47
()
V48
()
V49
()
V50
()
V51
() )
Element
of
K6
(
REAL
: ( ( ) (
V45
()
V46
()
V47
()
V51
() )
set
) ) : ( ( ) ( )
set
) ) )
*
x
: ( (
real
) (
V11
()
real
ext-real
)
number
)
)
: ( ( ) (
V11
()
real
ext-real
)
set
)
)
: ( ( ) (
V11
()
real
ext-real
)
Element
of
REAL
: ( ( ) (
V45
()
V46
()
V47
()
V51
() )
set
) ) : ( ( ) (
V11
()
real
ext-real
)
set
) ) ;
theorem
:: SIN_COS8:7
for
x
being ( (
real
) (
V11
()
real
ext-real
)
number
) holds
(
exp_R
x
: ( (
real
) (
V11
()
real
ext-real
)
number
) : ( ( ) (
V11
()
real
ext-real
)
set
)
=
(
cosh
x
: ( (
real
) (
V11
()
real
ext-real
)
number
)
)
: ( ( ) (
V11
()
real
ext-real
)
Element
of
REAL
: ( ( ) (
V45
()
V46
()
V47
()
V51
() )
set
) )
+
(
sinh
x
: ( (
real
) (
V11
()
real
ext-real
)
number
)
)
: ( ( ) (
V11
()
real
ext-real
)
Element
of
REAL
: ( ( ) (
V45
()
V46
()
V47
()
V51
() )
set
) ) : ( ( ) (
V11
()
real
ext-real
)
set
) &
exp_R
(
-
x
: ( (
real
) (
V11
()
real
ext-real
)
number
)
)
: ( (
V11
() ) (
V11
()
real
ext-real
)
set
) : ( ( ) (
V11
()
real
ext-real
)
set
)
=
(
cosh
x
: ( (
real
) (
V11
()
real
ext-real
)
number
)
)
: ( ( ) (
V11
()
real
ext-real
)
Element
of
REAL
: ( ( ) (
V45
()
V46
()
V47
()
V51
() )
set
) )
-
(
sinh
x
: ( (
real
) (
V11
()
real
ext-real
)
number
)
)
: ( ( ) (
V11
()
real
ext-real
)
Element
of
REAL
: ( ( ) (
V45
()
V46
()
V47
()
V51
() )
set
) ) : ( ( ) (
V11
()
real
ext-real
)
set
) &
exp_R
x
: ( (
real
) (
V11
()
real
ext-real
)
number
) : ( ( ) (
V11
()
real
ext-real
)
set
)
=
(
(
cosh
(
x
: ( (
real
) (
V11
()
real
ext-real
)
number
)
/
2 : ( ( ) (
V1
()
ordinal
natural
V11
()
real
ext-real
positive
non
negative
V33
()
V34
()
V45
()
V46
()
V47
()
V48
()
V49
()
V50
() )
Element
of
NAT
: ( ( ) (
V45
()
V46
()
V47
()
V48
()
V49
()
V50
()
V51
() )
Element
of
K6
(
REAL
: ( ( ) (
V45
()
V46
()
V47
()
V51
() )
set
) ) : ( ( ) ( )
set
) ) )
)
: ( ( ) (
V11
()
real
ext-real
)
set
)
)
: ( ( ) (
V11
()
real
ext-real
)
Element
of
REAL
: ( ( ) (
V45
()
V46
()
V47
()
V51
() )
set
) )
+
(
sinh
(
x
: ( (
real
) (
V11
()
real
ext-real
)
number
)
/
2 : ( ( ) (
V1
()
ordinal
natural
V11
()
real
ext-real
positive
non
negative
V33
()
V34
()
V45
()
V46
()
V47
()
V48
()
V49
()
V50
() )
Element
of
NAT
: ( ( ) (
V45
()
V46
()
V47
()
V48
()
V49
()
V50
()
V51
() )
Element
of
K6
(
REAL
: ( ( ) (
V45
()
V46
()
V47
()
V51
() )
set
) ) : ( ( ) ( )
set
) ) )
)
: ( ( ) (
V11
()
real
ext-real
)
set
)
)
: ( ( ) (
V11
()
real
ext-real
)
Element
of
REAL
: ( ( ) (
V45
()
V46
()
V47
()
V51
() )
set
) )
)
: ( ( ) (
V11
()
real
ext-real
)
set
)
/
(
(
cosh
(
x
: ( (
real
) (
V11
()
real
ext-real
)
number
)
/
2 : ( ( ) (
V1
()
ordinal
natural
V11
()
real
ext-real
positive
non
negative
V33
()
V34
()
V45
()
V46
()
V47
()
V48
()
V49
()
V50
() )
Element
of
NAT
: ( ( ) (
V45
()
V46
()
V47
()
V48
()
V49
()
V50
()
V51
() )
Element
of
K6
(
REAL
: ( ( ) (
V45
()
V46
()
V47
()
V51
() )
set
) ) : ( ( ) ( )
set
) ) )
)
: ( ( ) (
V11
()
real
ext-real
)
set
)
)
: ( ( ) (
V11
()
real
ext-real
)
Element
of
REAL
: ( ( ) (
V45
()
V46
()
V47
()
V51
() )
set
) )
-
(
sinh
(
x
: ( (
real
) (
V11
()
real
ext-real
)
number
)
/
2 : ( ( ) (
V1
()
ordinal
natural
V11
()
real
ext-real
positive
non
negative
V33
()
V34
()
V45
()
V46
()
V47
()
V48
()
V49
()
V50
() )
Element
of
NAT
: ( ( ) (
V45
()
V46
()
V47
()
V48
()
V49
()
V50
()
V51
() )
Element
of
K6
(
REAL
: ( ( ) (
V45
()
V46
()
V47
()
V51
() )
set
) ) : ( ( ) ( )
set
) ) )
)
: ( ( ) (
V11
()
real
ext-real
)
set
)
)
: ( ( ) (
V11
()
real
ext-real
)
Element
of
REAL
: ( ( ) (
V45
()
V46
()
V47
()
V51
() )
set
) )
)
: ( ( ) (
V11
()
real
ext-real
)
set
) : ( ( ) (
V11
()
real
ext-real
)
set
) &
exp_R
(
-
x
: ( (
real
) (
V11
()
real
ext-real
)
number
)
)
: ( (
V11
() ) (
V11
()
real
ext-real
)
set
) : ( ( ) (
V11
()
real
ext-real
)
set
)
=
(
(
cosh
(
x
: ( (
real
) (
V11
()
real
ext-real
)
number
)
/
2 : ( ( ) (
V1
()
ordinal
natural
V11
()
real
ext-real
positive
non
negative
V33
()
V34
()
V45
()
V46
()
V47
()
V48
()
V49
()
V50
() )
Element
of
NAT
: ( ( ) (
V45
()
V46
()
V47
()
V48
()
V49
()
V50
()
V51
() )
Element
of
K6
(
REAL
: ( ( ) (
V45
()
V46
()
V47
()
V51
() )
set
) ) : ( ( ) ( )
set
) ) )
)
: ( ( ) (
V11
()
real
ext-real
)
set
)
)
: ( ( ) (
V11
()
real
ext-real
)
Element
of
REAL
: ( ( ) (
V45
()
V46
()
V47
()
V51
() )
set
) )
-
(
sinh
(
x
: ( (
real
) (
V11
()
real
ext-real
)
number
)
/
2 : ( ( ) (
V1
()
ordinal
natural
V11
()
real
ext-real
positive
non
negative
V33
()
V34
()
V45
()
V46
()
V47
()
V48
()
V49
()
V50
() )
Element
of
NAT
: ( ( ) (
V45
()
V46
()
V47
()
V48
()
V49
()
V50
()
V51
() )
Element
of
K6
(
REAL
: ( ( ) (
V45
()
V46
()
V47
()
V51
() )
set
) ) : ( ( ) ( )
set
) ) )
)
: ( ( ) (
V11
()
real
ext-real
)
set
)
)
: ( ( ) (
V11
()
real
ext-real
)
Element
of
REAL
: ( ( ) (
V45
()
V46
()
V47
()
V51
() )
set
) )
)
: ( ( ) (
V11
()
real
ext-real
)
set
)
/
(
(
cosh
(
x
: ( (
real
) (
V11
()
real
ext-real
)
number
)
/
2 : ( ( ) (
V1
()
ordinal
natural
V11
()
real
ext-real
positive
non
negative
V33
()
V34
()
V45
()
V46
()
V47
()
V48
()
V49
()
V50
() )
Element
of
NAT
: ( ( ) (
V45
()
V46
()
V47
()
V48
()
V49
()
V50
()
V51
() )
Element
of
K6
(
REAL
: ( ( ) (
V45
()
V46
()
V47
()
V51
() )
set
) ) : ( ( ) ( )
set
) ) )
)
: ( ( ) (
V11
()
real
ext-real
)
set
)
)
: ( ( ) (
V11
()
real
ext-real
)
Element
of
REAL
: ( ( ) (
V45
()
V46
()
V47
()
V51
() )
set
) )
+
(
sinh
(
x
: ( (
real
) (
V11
()
real
ext-real
)
number
)
/
2 : ( ( ) (
V1
()
ordinal
natural
V11
()
real
ext-real
positive
non
negative
V33
()
V34
()
V45
()
V46
()
V47
()
V48
()
V49
()
V50
() )
Element
of
NAT
: ( ( ) (
V45
()
V46
()
V47
()
V48
()
V49
()
V50
()
V51
() )
Element
of
K6
(
REAL
: ( ( ) (
V45
()
V46
()
V47
()
V51
() )
set
) ) : ( ( ) ( )
set
) ) )
)
: ( ( ) (
V11
()
real
ext-real
)
set
)
)
: ( ( ) (
V11
()
real
ext-real
)
Element
of
REAL
: ( ( ) (
V45
()
V46
()
V47
()
V51
() )
set
) )
)
: ( ( ) (
V11
()
real
ext-real
)
set
) : ( ( ) (
V11
()
real
ext-real
)
set
) &
exp_R
x
: ( (
real
) (
V11
()
real
ext-real
)
number
) : ( ( ) (
V11
()
real
ext-real
)
set
)
=
(
1 : ( ( ) (
V1
()
ordinal
natural
V11
()
real
ext-real
positive
non
negative
V33
()
V34
()
V45
()
V46
()
V47
()
V48
()
V49
()
V50
() )
Element
of
NAT
: ( ( ) (
V45
()
V46
()
V47
()
V48
()
V49
()
V50
()
V51
() )
Element
of
K6
(
REAL
: ( ( ) (
V45
()
V46
()
V47
()
V51
() )
set
) ) : ( ( ) ( )
set
) ) )
+
(
tanh
(
x
: ( (
real
) (
V11
()
real
ext-real
)
number
)
/
2 : ( ( ) (
V1
()
ordinal
natural
V11
()
real
ext-real
positive
non
negative
V33
()
V34
()
V45
()
V46
()
V47
()
V48
()
V49
()
V50
() )
Element
of
NAT
: ( ( ) (
V45
()
V46
()
V47
()
V48
()
V49
()
V50
()
V51
() )
Element
of
K6
(
REAL
: ( ( ) (
V45
()
V46
()
V47
()
V51
() )
set
) ) : ( ( ) ( )
set
) ) )
)
: ( ( ) (
V11
()
real
ext-real
)
set
)
)
: ( ( ) (
V11
()
real
ext-real
)
Element
of
REAL
: ( ( ) (
V45
()
V46
()
V47
()
V51
() )
set
) )
)
: ( ( ) (
V11
()
real
ext-real
)
set
)
/
(
1 : ( ( ) (
V1
()
ordinal
natural
V11
()
real
ext-real
positive
non
negative
V33
()
V34
()
V45
()
V46
()
V47
()
V48
()
V49
()
V50
() )
Element
of
NAT
: ( ( ) (
V45
()
V46
()
V47
()
V48
()
V49
()
V50
()
V51
() )
Element
of
K6
(
REAL
: ( ( ) (
V45
()
V46
()
V47
()
V51
() )
set
) ) : ( ( ) ( )
set
) ) )
-
(
tanh
(
x
: ( (
real
) (
V11
()
real
ext-real
)
number
)
/
2 : ( ( ) (
V1
()
ordinal
natural
V11
()
real
ext-real
positive
non
negative
V33
()
V34
()
V45
()
V46
()
V47
()
V48
()
V49
()
V50
() )
Element
of
NAT
: ( ( ) (
V45
()
V46
()
V47
()
V48
()
V49
()
V50
()
V51
() )
Element
of
K6
(
REAL
: ( ( ) (
V45
()
V46
()
V47
()
V51
() )
set
) ) : ( ( ) ( )
set
) ) )
)
: ( ( ) (
V11
()
real
ext-real
)
set
)
)
: ( ( ) (
V11
()
real
ext-real
)
Element
of
REAL
: ( ( ) (
V45
()
V46
()
V47
()
V51
() )
set
) )
)
: ( ( ) (
V11
()
real
ext-real
)
set
) : ( ( ) (
V11
()
real
ext-real
)
set
) &
exp_R
(
-
x
: ( (
real
) (
V11
()
real
ext-real
)
number
)
)
: ( (
V11
() ) (
V11
()
real
ext-real
)
set
) : ( ( ) (
V11
()
real
ext-real
)
set
)
=
(
1 : ( ( ) (
V1
()
ordinal
natural
V11
()
real
ext-real
positive
non
negative
V33
()
V34
()
V45
()
V46
()
V47
()
V48
()
V49
()
V50
() )
Element
of
NAT
: ( ( ) (
V45
()
V46
()
V47
()
V48
()
V49
()
V50
()
V51
() )
Element
of
K6
(
REAL
: ( ( ) (
V45
()
V46
()
V47
()
V51
() )
set
) ) : ( ( ) ( )
set
) ) )
-
(
tanh
(
x
: ( (
real
) (
V11
()
real
ext-real
)
number
)
/
2 : ( ( ) (
V1
()
ordinal
natural
V11
()
real
ext-real
positive
non
negative
V33
()
V34
()
V45
()
V46
()
V47
()
V48
()
V49
()
V50
() )
Element
of
NAT
: ( ( ) (
V45
()
V46
()
V47
()
V48
()
V49
()
V50
()
V51
() )
Element
of
K6
(
REAL
: ( ( ) (
V45
()
V46
()
V47
()
V51
() )
set
) ) : ( ( ) ( )
set
) ) )
)
: ( ( ) (
V11
()
real
ext-real
)
set
)
)
: ( ( ) (
V11
()
real
ext-real
)
Element
of
REAL
: ( ( ) (
V45
()
V46
()
V47
()
V51
() )
set
) )
)
: ( ( ) (
V11
()
real
ext-real
)
set
)
/
(
1 : ( ( ) (
V1
()
ordinal
natural
V11
()
real
ext-real
positive
non
negative
V33
()
V34
()
V45
()
V46
()
V47
()
V48
()
V49
()
V50
() )
Element
of
NAT
: ( ( ) (
V45
()
V46
()
V47
()
V48
()
V49
()
V50
()
V51
() )
Element
of
K6
(
REAL
: ( ( ) (
V45
()
V46
()
V47
()
V51
() )
set
) ) : ( ( ) ( )
set
) ) )
+
(
tanh
(
x
: ( (
real
) (
V11
()
real
ext-real
)
number
)
/
2 : ( ( ) (
V1
()
ordinal
natural
V11
()
real
ext-real
positive
non
negative
V33
()
V34
()
V45
()
V46
()
V47
()
V48
()
V49
()
V50
() )
Element
of
NAT
: ( ( ) (
V45
()
V46
()
V47
()
V48
()
V49
()
V50
()
V51
() )
Element
of
K6
(
REAL
: ( ( ) (
V45
()
V46
()
V47
()
V51
() )
set
) ) : ( ( ) ( )
set
) ) )
)
: ( ( ) (
V11
()
real
ext-real
)
set
)
)
: ( ( ) (
V11
()
real
ext-real
)
Element
of
REAL
: ( ( ) (
V45
()
V46
()
V47
()
V51
() )
set
) )
)
: ( ( ) (
V11
()
real
ext-real
)
set
) : ( ( ) (
V11
()
real
ext-real
)
set
) ) ;
theorem
:: SIN_COS8:8
for
x
being ( (
real
) (
V11
()
real
ext-real
)
number
) st
x
: ( (
real
) (
V11
()
real
ext-real
)
number
)
<>
0
: ( ( ) (
V1
()
ordinal
natural
V11
()
real
ext-real
non
positive
non
negative
V33
()
V34
()
V45
()
V46
()
V47
()
V48
()
V49
()
V50
()
V51
() )
Element
of
NAT
: ( ( ) (
V45
()
V46
()
V47
()
V48
()
V49
()
V50
()
V51
() )
Element
of
K6
(
REAL
: ( ( ) (
V45
()
V46
()
V47
()
V51
() )
set
) ) : ( ( ) ( )
set
) ) ) holds
(
exp_R
x
: ( (
real
) (
V11
()
real
ext-real
)
number
) : ( ( ) (
V11
()
real
ext-real
)
set
)
=
(
(
coth
(
x
: ( (
real
) (
V11
()
real
ext-real
)
number
)
/
2 : ( ( ) (
V1
()
ordinal
natural
V11
()
real
ext-real
positive
non
negative
V33
()
V34
()
V45
()
V46
()
V47
()
V48
()
V49
()
V50
() )
Element
of
NAT
: ( ( ) (
V45
()
V46
()
V47
()
V48
()
V49
()
V50
()
V51
() )
Element
of
K6
(
REAL
: ( ( ) (
V45
()
V46
()
V47
()
V51
() )
set
) ) : ( ( ) ( )
set
) ) )
)
: ( ( ) (
V11
()
real
ext-real
)
set
)
)
: ( ( ) (
V11
()
real
ext-real
)
Element
of
REAL
: ( ( ) (
V45
()
V46
()
V47
()
V51
() )
set
) )
+
1 : ( ( ) (
V1
()
ordinal
natural
V11
()
real
ext-real
positive
non
negative
V33
()
V34
()
V45
()
V46
()
V47
()
V48
()
V49
()
V50
() )
Element
of
NAT
: ( ( ) (
V45
()
V46
()
V47
()
V48
()
V49
()
V50
()
V51
() )
Element
of
K6
(
REAL
: ( ( ) (
V45
()
V46
()
V47
()
V51
() )
set
) ) : ( ( ) ( )
set
) ) )
)
: ( ( ) (
V11
()
real
ext-real
)
set
)
/
(
(
coth
(
x
: ( (
real
) (
V11
()
real
ext-real
)
number
)
/
2 : ( ( ) (
V1
()
ordinal
natural
V11
()
real
ext-real
positive
non
negative
V33
()
V34
()
V45
()
V46
()
V47
()
V48
()
V49
()
V50
() )
Element
of
NAT
: ( ( ) (
V45
()
V46
()
V47
()
V48
()
V49
()
V50
()
V51
() )
Element
of
K6
(
REAL
: ( ( ) (
V45
()
V46
()
V47
()
V51
() )
set
) ) : ( ( ) ( )
set
) ) )
)
: ( ( ) (
V11
()
real
ext-real
)
set
)
)
: ( ( ) (
V11
()
real
ext-real
)
Element
of
REAL
: ( ( ) (
V45
()
V46
()
V47
()
V51
() )
set
) )
-
1 : ( ( ) (
V1
()
ordinal
natural
V11
()
real
ext-real
positive
non
negative
V33
()
V34
()
V45
()
V46
()
V47
()
V48
()
V49
()
V50
() )
Element
of
NAT
: ( ( ) (
V45
()
V46
()
V47
()
V48
()
V49
()
V50
()
V51
() )
Element
of
K6
(
REAL
: ( ( ) (
V45
()
V46
()
V47
()
V51
() )
set
) ) : ( ( ) ( )
set
) ) )
)
: ( ( ) (
V11
()
real
ext-real
)
set
) : ( ( ) (
V11
()
real
ext-real
)
set
) &
exp_R
(
-
x
: ( (
real
) (
V11
()
real
ext-real
)
number
)
)
: ( (
V11
() ) (
V11
()
real
ext-real
)
set
) : ( ( ) (
V11
()
real
ext-real
)
set
)
=
(
(
coth
(
x
: ( (
real
) (
V11
()
real
ext-real
)
number
)
/
2 : ( ( ) (
V1
()
ordinal
natural
V11
()
real
ext-real
positive
non
negative
V33
()
V34
()
V45
()
V46
()
V47
()
V48
()
V49
()
V50
() )
Element
of
NAT
: ( ( ) (
V45
()
V46
()
V47
()
V48
()
V49
()
V50
()
V51
() )
Element
of
K6
(
REAL
: ( ( ) (
V45
()
V46
()
V47
()
V51
() )
set
) ) : ( ( ) ( )
set
) ) )
)
: ( ( ) (
V11
()
real
ext-real
)
set
)
)
: ( ( ) (
V11
()
real
ext-real
)
Element
of
REAL
: ( ( ) (
V45
()
V46
()
V47
()
V51
() )
set
) )
-
1 : ( ( ) (
V1
()
ordinal
natural
V11
()
real
ext-real
positive
non
negative
V33
()
V34
()
V45
()
V46
()
V47
()
V48
()
V49
()
V50
() )
Element
of
NAT
: ( ( ) (
V45
()
V46
()
V47
()
V48
()
V49
()
V50
()
V51
() )
Element
of
K6
(
REAL
: ( ( ) (
V45
()
V46
()
V47
()
V51
() )
set
) ) : ( ( ) ( )
set
) ) )
)
: ( ( ) (
V11
()
real
ext-real
)
set
)
/
(
(
coth
(
x
: ( (
real
) (
V11
()
real
ext-real
)
number
)
/
2 : ( ( ) (
V1
()
ordinal
natural
V11
()
real
ext-real
positive
non
negative
V33
()
V34
()
V45
()
V46
()
V47
()
V48
()
V49
()
V50
() )
Element
of
NAT
: ( ( ) (
V45
()
V46
()
V47
()
V48
()
V49
()
V50
()
V51
() )
Element
of
K6
(
REAL
: ( ( ) (
V45
()
V46
()
V47
()
V51
() )
set
) ) : ( ( ) ( )
set
) ) )
)
: ( ( ) (
V11
()
real
ext-real
)
set
)
)
: ( ( ) (
V11
()
real
ext-real
)
Element
of
REAL
: ( ( ) (
V45
()
V46
()
V47
()
V51
() )
set
) )
+
1 : ( ( ) (
V1
()
ordinal
natural
V11
()
real
ext-real
positive
non
negative
V33
()
V34
()
V45
()
V46
()
V47
()
V48
()
V49
()
V50
() )
Element
of
NAT
: ( ( ) (
V45
()
V46
()
V47
()
V48
()
V49
()
V50
()
V51
() )
Element
of
K6
(
REAL
: ( ( ) (
V45
()
V46
()
V47
()
V51
() )
set
) ) : ( ( ) ( )
set
) ) )
)
: ( ( ) (
V11
()
real
ext-real
)
set
) : ( ( ) (
V11
()
real
ext-real
)
set
) ) ;
theorem
:: SIN_COS8:9
for
x
being ( (
real
) (
V11
()
real
ext-real
)
number
) holds
(
(
cosh
x
: ( (
real
) (
V11
()
real
ext-real
)
number
)
)
: ( ( ) (
V11
()
real
ext-real
)
Element
of
REAL
: ( ( ) (
V45
()
V46
()
V47
()
V51
() )
set
) )
+
(
sinh
x
: ( (
real
) (
V11
()
real
ext-real
)
number
)
)
: ( ( ) (
V11
()
real
ext-real
)
Element
of
REAL
: ( ( ) (
V45
()
V46
()
V47
()
V51
() )
set
) )
)
: ( ( ) (
V11
()
real
ext-real
)
set
)
/
(
(
cosh
x
: ( (
real
) (
V11
()
real
ext-real
)
number
)
)
: ( ( ) (
V11
()
real
ext-real
)
Element
of
REAL
: ( ( ) (
V45
()
V46
()
V47
()
V51
() )
set
) )
-
(
sinh
x
: ( (
real
) (
V11
()
real
ext-real
)
number
)
)
: ( ( ) (
V11
()
real
ext-real
)
Element
of
REAL
: ( ( ) (
V45
()
V46
()
V47
()
V51
() )
set
) )
)
: ( ( ) (
V11
()
real
ext-real
)
set
) : ( ( ) (
V11
()
real
ext-real
)
set
)
=
(
1 : ( ( ) (
V1
()
ordinal
natural
V11
()
real
ext-real
positive
non
negative
V33
()
V34
()
V45
()
V46
()
V47
()
V48
()
V49
()
V50
() )
Element
of
NAT
: ( ( ) (
V45
()
V46
()
V47
()
V48
()
V49
()
V50
()
V51
() )
Element
of
K6
(
REAL
: ( ( ) (
V45
()
V46
()
V47
()
V51
() )
set
) ) : ( ( ) ( )
set
) ) )
+
(
tanh
x
: ( (
real
) (
V11
()
real
ext-real
)
number
)
)
: ( ( ) (
V11
()
real
ext-real
)
Element
of
REAL
: ( ( ) (
V45
()
V46
()
V47
()
V51
() )
set
) )
)
: ( ( ) (
V11
()
real
ext-real
)
set
)
/
(
1 : ( ( ) (
V1
()
ordinal
natural
V11
()
real
ext-real
positive
non
negative
V33
()
V34
()
V45
()
V46
()
V47
()
V48
()
V49
()
V50
() )
Element
of
NAT
: ( ( ) (
V45
()
V46
()
V47
()
V48
()
V49
()
V50
()
V51
() )
Element
of
K6
(
REAL
: ( ( ) (
V45
()
V46
()
V47
()
V51
() )
set
) ) : ( ( ) ( )
set
) ) )
-
(
tanh
x
: ( (
real
) (
V11
()
real
ext-real
)
number
)
)
: ( ( ) (
V11
()
real
ext-real
)
Element
of
REAL
: ( ( ) (
V45
()
V46
()
V47
()
V51
() )
set
) )
)
: ( ( ) (
V11
()
real
ext-real
)
set
) : ( ( ) (
V11
()
real
ext-real
)
set
) ;
theorem
:: SIN_COS8:10
for
y
,
z
being ( (
real
) (
V11
()
real
ext-real
)
number
) st
y
: ( (
real
) (
V11
()
real
ext-real
)
number
)
<>
0
: ( ( ) (
V1
()
ordinal
natural
V11
()
real
ext-real
non
positive
non
negative
V33
()
V34
()
V45
()
V46
()
V47
()
V48
()
V49
()
V50
()
V51
() )
Element
of
NAT
: ( ( ) (
V45
()
V46
()
V47
()
V48
()
V49
()
V50
()
V51
() )
Element
of
K6
(
REAL
: ( ( ) (
V45
()
V46
()
V47
()
V51
() )
set
) ) : ( ( ) ( )
set
) ) ) holds
(
(
coth
y
: ( (
real
) (
V11
()
real
ext-real
)
number
)
)
: ( ( ) (
V11
()
real
ext-real
)
Element
of
REAL
: ( ( ) (
V45
()
V46
()
V47
()
V51
() )
set
) )
+
(
tanh
z
: ( (
real
) (
V11
()
real
ext-real
)
number
)
)
: ( ( ) (
V11
()
real
ext-real
)
Element
of
REAL
: ( ( ) (
V45
()
V46
()
V47
()
V51
() )
set
) ) : ( ( ) (
V11
()
real
ext-real
)
set
)
=
(
cosh
(
y
: ( (
real
) (
V11
()
real
ext-real
)
number
)
+
z
: ( (
real
) (
V11
()
real
ext-real
)
number
)
)
: ( ( ) (
V11
()
real
ext-real
)
set
)
)
: ( ( ) (
V11
()
real
ext-real
)
Element
of
REAL
: ( ( ) (
V45
()
V46
()
V47
()
V51
() )
set
) )
/
(
(
sinh
y
: ( (
real
) (
V11
()
real
ext-real
)
number
)
)
: ( ( ) (
V11
()
real
ext-real
)
Element
of
REAL
: ( ( ) (
V45
()
V46
()
V47
()
V51
() )
set
) )
*
(
cosh
z
: ( (
real
) (
V11
()
real
ext-real
)
number
)
)
: ( ( ) (
V11
()
real
ext-real
)
Element
of
REAL
: ( ( ) (
V45
()
V46
()
V47
()
V51
() )
set
) )
)
: ( ( ) (
V11
()
real
ext-real
)
set
) : ( ( ) (
V11
()
real
ext-real
)
set
) &
(
coth
y
: ( (
real
) (
V11
()
real
ext-real
)
number
)
)
: ( ( ) (
V11
()
real
ext-real
)
Element
of
REAL
: ( ( ) (
V45
()
V46
()
V47
()
V51
() )
set
) )
-
(
tanh
z
: ( (
real
) (
V11
()
real
ext-real
)
number
)
)
: ( ( ) (
V11
()
real
ext-real
)
Element
of
REAL
: ( ( ) (
V45
()
V46
()
V47
()
V51
() )
set
) ) : ( ( ) (
V11
()
real
ext-real
)
set
)
=
(
cosh
(
y
: ( (
real
) (
V11
()
real
ext-real
)
number
)
-
z
: ( (
real
) (
V11
()
real
ext-real
)
number
)
)
: ( ( ) (
V11
()
real
ext-real
)
set
)
)
: ( ( ) (
V11
()
real
ext-real
)
Element
of
REAL
: ( ( ) (
V45
()
V46
()
V47
()
V51
() )
set
) )
/
(
(
sinh
y
: ( (
real
) (
V11
()
real
ext-real
)
number
)
)
: ( ( ) (
V11
()
real
ext-real
)
Element
of
REAL
: ( ( ) (
V45
()
V46
()
V47
()
V51
() )
set
) )
*
(
cosh
z
: ( (
real
) (
V11
()
real
ext-real
)
number
)
)
: ( ( ) (
V11
()
real
ext-real
)
Element
of
REAL
: ( ( ) (
V45
()
V46
()
V47
()
V51
() )
set
) )
)
: ( ( ) (
V11
()
real
ext-real
)
set
) : ( ( ) (
V11
()
real
ext-real
)
set
) ) ;
theorem
:: SIN_COS8:11
for
y
,
z
being ( (
real
) (
V11
()
real
ext-real
)
number
) holds
(
(
sinh
y
: ( (
real
) (
V11
()
real
ext-real
)
number
)
)
: ( ( ) (
V11
()
real
ext-real
)
Element
of
REAL
: ( ( ) (
V45
()
V46
()
V47
()
V51
() )
set
) )
*
(
sinh
z
: ( (
real
) (
V11
()
real
ext-real
)
number
)
)
: ( ( ) (
V11
()
real
ext-real
)
Element
of
REAL
: ( ( ) (
V45
()
V46
()
V47
()
V51
() )
set
) ) : ( ( ) (
V11
()
real
ext-real
)
set
)
=
(
1 : ( ( ) (
V1
()
ordinal
natural
V11
()
real
ext-real
positive
non
negative
V33
()
V34
()
V45
()
V46
()
V47
()
V48
()
V49
()
V50
() )
Element
of
NAT
: ( ( ) (
V45
()
V46
()
V47
()
V48
()
V49
()
V50
()
V51
() )
Element
of
K6
(
REAL
: ( ( ) (
V45
()
V46
()
V47
()
V51
() )
set
) ) : ( ( ) ( )
set
) ) )
/
2 : ( ( ) (
V1
()
ordinal
natural
V11
()
real
ext-real
positive
non
negative
V33
()
V34
()
V45
()
V46
()
V47
()
V48
()
V49
()
V50
() )
Element
of
NAT
: ( ( ) (
V45
()
V46
()
V47
()
V48
()
V49
()
V50
()
V51
() )
Element
of
K6
(
REAL
: ( ( ) (
V45
()
V46
()
V47
()
V51
() )
set
) ) : ( ( ) ( )
set
) ) )
)
: ( ( ) (
V11
()
real
ext-real
non
negative
)
set
)
*
(
(
cosh
(
y
: ( (
real
) (
V11
()
real
ext-real
)
number
)
+
z
: ( (
real
) (
V11
()
real
ext-real
)
number
)
)
: ( ( ) (
V11
()
real
ext-real
)
set
)
)
: ( ( ) (
V11
()
real
ext-real
)
Element
of
REAL
: ( ( ) (
V45
()
V46
()
V47
()
V51
() )
set
) )
-
(
cosh
(
y
: ( (
real
) (
V11
()
real
ext-real
)
number
)
-
z
: ( (
real
) (
V11
()
real
ext-real
)
number
)
)
: ( ( ) (
V11
()
real
ext-real
)
set
)
)
: ( ( ) (
V11
()
real
ext-real
)
Element
of
REAL
: ( ( ) (
V45
()
V46
()
V47
()
V51
() )
set
) )
)
: ( ( ) (
V11
()
real
ext-real
)
set
) : ( ( ) (
V11
()
real
ext-real
)
set
) &
(
sinh
y
: ( (
real
) (
V11
()
real
ext-real
)
number
)
)
: ( ( ) (
V11
()
real
ext-real
)
Element
of
REAL
: ( ( ) (
V45
()
V46
()
V47
()
V51
() )
set
) )
*
(
cosh
z
: ( (
real
) (
V11
()
real
ext-real
)
number
)
)
: ( ( ) (
V11
()
real
ext-real
)
Element
of
REAL
: ( ( ) (
V45
()
V46
()
V47
()
V51
() )
set
) ) : ( ( ) (
V11
()
real
ext-real
)
set
)
=
(
1 : ( ( ) (
V1
()
ordinal
natural
V11
()
real
ext-real
positive
non
negative
V33
()
V34
()
V45
()
V46
()
V47
()
V48
()
V49
()
V50
() )
Element
of
NAT
: ( ( ) (
V45
()
V46
()
V47
()
V48
()
V49
()
V50
()
V51
() )
Element
of
K6
(
REAL
: ( ( ) (
V45
()
V46
()
V47
()
V51
() )
set
) ) : ( ( ) ( )
set
) ) )
/
2 : ( ( ) (
V1
()
ordinal
natural
V11
()
real
ext-real
positive
non
negative
V33
()
V34
()
V45
()
V46
()
V47
()
V48
()
V49
()
V50
() )
Element
of
NAT
: ( ( ) (
V45
()
V46
()
V47
()
V48
()
V49
()
V50
()
V51
() )
Element
of
K6
(
REAL
: ( ( ) (
V45
()
V46
()
V47
()
V51
() )
set
) ) : ( ( ) ( )
set
) ) )
)
: ( ( ) (
V11
()
real
ext-real
non
negative
)
set
)
*
(
(
sinh
(
y
: ( (
real
) (
V11
()
real
ext-real
)
number
)
+
z
: ( (
real
) (
V11
()
real
ext-real
)
number
)
)
: ( ( ) (
V11
()
real
ext-real
)
set
)
)
: ( ( ) (
V11
()
real
ext-real
)
Element
of
REAL
: ( ( ) (
V45
()
V46
()
V47
()
V51
() )
set
) )
+
(
sinh
(
y
: ( (
real
) (
V11
()
real
ext-real
)
number
)
-
z
: ( (
real
) (
V11
()
real
ext-real
)
number
)
)
: ( ( ) (
V11
()
real
ext-real
)
set
)
)
: ( ( ) (
V11
()
real
ext-real
)
Element
of
REAL
: ( ( ) (
V45
()
V46
()
V47
()
V51
() )
set
) )
)
: ( ( ) (
V11
()
real
ext-real
)
set
) : ( ( ) (
V11
()
real
ext-real
)
set
) &
(
cosh
y
: ( (
real
) (
V11
()
real
ext-real
)
number
)
)
: ( ( ) (
V11
()
real
ext-real
)
Element
of
REAL
: ( ( ) (
V45
()
V46
()
V47
()
V51
() )
set
) )
*
(
sinh
z
: ( (
real
) (
V11
()
real
ext-real
)
number
)
)
: ( ( ) (
V11
()
real
ext-real
)
Element
of
REAL
: ( ( ) (
V45
()
V46
()
V47
()
V51
() )
set
) ) : ( ( ) (
V11
()
real
ext-real
)
set
)
=
(
1 : ( ( ) (
V1
()
ordinal
natural
V11
()
real
ext-real
positive
non
negative
V33
()
V34
()
V45
()
V46
()
V47
()
V48
()
V49
()
V50
() )
Element
of
NAT
: ( ( ) (
V45
()
V46
()
V47
()
V48
()
V49
()
V50
()
V51
() )
Element
of
K6
(
REAL
: ( ( ) (
V45
()
V46
()
V47
()
V51
() )
set
) ) : ( ( ) ( )
set
) ) )
/
2 : ( ( ) (
V1
()
ordinal
natural
V11
()
real
ext-real
positive
non
negative
V33
()
V34
()
V45
()
V46
()
V47
()
V48
()
V49
()
V50
() )
Element
of
NAT
: ( ( ) (
V45
()
V46
()
V47
()
V48
()
V49
()
V50
()
V51
() )
Element
of
K6
(
REAL
: ( ( ) (
V45
()
V46
()
V47
()
V51
() )
set
) ) : ( ( ) ( )
set
) ) )
)
: ( ( ) (
V11
()
real
ext-real
non
negative
)
set
)
*
(
(
sinh
(
y
: ( (
real
) (
V11
()
real
ext-real
)
number
)
+
z
: ( (
real
) (
V11
()
real
ext-real
)
number
)
)
: ( ( ) (
V11
()
real
ext-real
)
set
)
)
: ( ( ) (
V11
()
real
ext-real
)
Element
of
REAL
: ( ( ) (
V45
()
V46
()
V47
()
V51
() )
set
) )
-
(
sinh
(
y
: ( (
real
) (
V11
()
real
ext-real
)
number
)
-
z
: ( (
real
) (
V11
()
real
ext-real
)
number
)
)
: ( ( ) (
V11
()
real
ext-real
)
set
)
)
: ( ( ) (
V11
()
real
ext-real
)
Element
of
REAL
: ( ( ) (
V45
()
V46
()
V47
()
V51
() )
set
) )
)
: ( ( ) (
V11
()
real
ext-real
)
set
) : ( ( ) (
V11
()
real
ext-real
)
set
) &
(
cosh
y
: ( (
real
) (
V11
()
real
ext-real
)
number
)
)
: ( ( ) (
V11
()
real
ext-real
)
Element
of
REAL
: ( ( ) (
V45
()
V46
()
V47
()
V51
() )
set
) )
*
(
cosh
z
: ( (
real
) (
V11
()
real
ext-real
)
number
)
)
: ( ( ) (
V11
()
real
ext-real
)
Element
of
REAL
: ( ( ) (
V45
()
V46
()
V47
()
V51
() )
set
) ) : ( ( ) (
V11
()
real
ext-real
)
set
)
=
(
1 : ( ( ) (
V1
()
ordinal
natural
V11
()
real
ext-real
positive
non
negative
V33
()
V34
()
V45
()
V46
()
V47
()
V48
()
V49
()
V50
() )
Element
of
NAT
: ( ( ) (
V45
()
V46
()
V47
()
V48
()
V49
()
V50
()
V51
() )
Element
of
K6
(
REAL
: ( ( ) (
V45
()
V46
()
V47
()
V51
() )
set
) ) : ( ( ) ( )
set
) ) )
/
2 : ( ( ) (
V1
()
ordinal
natural
V11
()
real
ext-real
positive
non
negative
V33
()
V34
()
V45
()
V46
()
V47
()
V48
()
V49
()
V50
() )
Element
of
NAT
: ( ( ) (
V45
()
V46
()
V47
()
V48
()
V49
()
V50
()
V51
() )
Element
of
K6
(
REAL
: ( ( ) (
V45
()
V46
()
V47
()
V51
() )
set
) ) : ( ( ) ( )
set
) ) )
)
: ( ( ) (
V11
()
real
ext-real
non
negative
)
set
)
*
(
(
cosh
(
y
: ( (
real
) (
V11
()
real
ext-real
)
number
)
+
z
: ( (
real
) (
V11
()
real
ext-real
)
number
)
)
: ( ( ) (
V11
()
real
ext-real
)
set
)
)
: ( ( ) (
V11
()
real
ext-real
)
Element
of
REAL
: ( ( ) (
V45
()
V46
()
V47
()
V51
() )
set
) )
+
(
cosh
(
y
: ( (
real
) (
V11
()
real
ext-real
)
number
)
-
z
: ( (
real
) (
V11
()
real
ext-real
)
number
)
)
: ( ( ) (
V11
()
real
ext-real
)
set
)
)
: ( ( ) (
V11
()
real
ext-real
)
Element
of
REAL
: ( ( ) (
V45
()
V46
()
V47
()
V51
() )
set
) )
)
: ( ( ) (
V11
()
real
ext-real
)
set
) : ( ( ) (
V11
()
real
ext-real
)
set
) ) ;
theorem
:: SIN_COS8:12
for
y
,
z
being ( (
real
) (
V11
()
real
ext-real
)
number
) holds
(
(
sinh
y
: ( (
real
) (
V11
()
real
ext-real
)
number
)
)
: ( ( ) (
V11
()
real
ext-real
)
Element
of
REAL
: ( ( ) (
V45
()
V46
()
V47
()
V51
() )
set
) )
^2
)
: ( ( ) (
V11
()
real
ext-real
)
Element
of
REAL
: ( ( ) (
V45
()
V46
()
V47
()
V51
() )
set
) )
-
(
(
cosh
z
: ( (
real
) (
V11
()
real
ext-real
)
number
)
)
: ( ( ) (
V11
()
real
ext-real
)
Element
of
REAL
: ( ( ) (
V45
()
V46
()
V47
()
V51
() )
set
) )
^2
)
: ( ( ) (
V11
()
real
ext-real
)
Element
of
REAL
: ( ( ) (
V45
()
V46
()
V47
()
V51
() )
set
) ) : ( ( ) (
V11
()
real
ext-real
)
set
)
=
(
(
sinh
(
y
: ( (
real
) (
V11
()
real
ext-real
)
number
)
+
z
: ( (
real
) (
V11
()
real
ext-real
)
number
)
)
: ( ( ) (
V11
()
real
ext-real
)
set
)
)
: ( ( ) (
V11
()
real
ext-real
)
Element
of
REAL
: ( ( ) (
V45
()
V46
()
V47
()
V51
() )
set
) )
*
(
sinh
(
y
: ( (
real
) (
V11
()
real
ext-real
)
number
)
-
z
: ( (
real
) (
V11
()
real
ext-real
)
number
)
)
: ( ( ) (
V11
()
real
ext-real
)
set
)
)
: ( ( ) (
V11
()
real
ext-real
)
Element
of
REAL
: ( ( ) (
V45
()
V46
()
V47
()
V51
() )
set
) )
)
: ( ( ) (
V11
()
real
ext-real
)
set
)
-
1 : ( ( ) (
V1
()
ordinal
natural
V11
()
real
ext-real
positive
non
negative
V33
()
V34
()
V45
()
V46
()
V47
()
V48
()
V49
()
V50
() )
Element
of
NAT
: ( ( ) (
V45
()
V46
()
V47
()
V48
()
V49
()
V50
()
V51
() )
Element
of
K6
(
REAL
: ( ( ) (
V45
()
V46
()
V47
()
V51
() )
set
) ) : ( ( ) ( )
set
) ) ) : ( ( ) (
V11
()
real
ext-real
)
set
) ;
theorem
:: SIN_COS8:13
for
y
,
z
being ( (
real
) (
V11
()
real
ext-real
)
number
) holds
(
(
(
(
sinh
y
: ( (
real
) (
V11
()
real
ext-real
)
number
)
)
: ( ( ) (
V11
()
real
ext-real
)
Element
of
REAL
: ( ( ) (
V45
()
V46
()
V47
()
V51
() )
set
) )
-
(
sinh
z
: ( (
real
) (
V11
()
real
ext-real
)
number
)
)
: ( ( ) (
V11
()
real
ext-real
)
Element
of
REAL
: ( ( ) (
V45
()
V46
()
V47
()
V51
() )
set
) )
)
: ( ( ) (
V11
()
real
ext-real
)
set
)
^2
)
: ( ( ) (
V11
()
real
ext-real
)
set
)
-
(
(
(
cosh
y
: ( (
real
) (
V11
()
real
ext-real
)
number
)
)
: ( ( ) (
V11
()
real
ext-real
)
Element
of
REAL
: ( ( ) (
V45
()
V46
()
V47
()
V51
() )
set
) )
-
(
cosh
z
: ( (
real
) (
V11
()
real
ext-real
)
number
)
)
: ( ( ) (
V11
()
real
ext-real
)
Element
of
REAL
: ( ( ) (
V45
()
V46
()
V47
()
V51
() )
set
) )
)
: ( ( ) (
V11
()
real
ext-real
)
set
)
^2
)
: ( ( ) (
V11
()
real
ext-real
)
set
) : ( ( ) (
V11
()
real
ext-real
)
set
)
=
4 : ( ( ) (
V1
()
ordinal
natural
V11
()
real
ext-real
positive
non
negative
V33
()
V34
()
V45
()
V46
()
V47
()
V48
()
V49
()
V50
() )
Element
of
NAT
: ( ( ) (
V45
()
V46
()
V47
()
V48
()
V49
()
V50
()
V51
() )
Element
of
K6
(
REAL
: ( ( ) (
V45
()
V46
()
V47
()
V51
() )
set
) ) : ( ( ) ( )
set
) ) )
*
(
(
sinh
(
(
y
: ( (
real
) (
V11
()
real
ext-real
)
number
)
-
z
: ( (
real
) (
V11
()
real
ext-real
)
number
)
)
: ( ( ) (
V11
()
real
ext-real
)
set
)
/
2 : ( ( ) (
V1
()
ordinal
natural
V11
()
real
ext-real
positive
non
negative
V33
()
V34
()
V45
()
V46
()
V47
()
V48
()
V49
()
V50
() )
Element
of
NAT
: ( ( ) (
V45
()
V46
()
V47
()
V48
()
V49
()
V50
()
V51
() )
Element
of
K6
(
REAL
: ( ( ) (
V45
()
V46
()
V47
()
V51
() )
set
) ) : ( ( ) ( )
set
) ) )
)
: ( ( ) (
V11
()
real
ext-real
)
set
)
)
: ( ( ) (
V11
()
real
ext-real
)
Element
of
REAL
: ( ( ) (
V45
()
V46
()
V47
()
V51
() )
set
) )
^2
)
: ( ( ) (
V11
()
real
ext-real
)
Element
of
REAL
: ( ( ) (
V45
()
V46
()
V47
()
V51
() )
set
) ) : ( ( ) (
V11
()
real
ext-real
)
set
) &
(
(
(
cosh
y
: ( (
real
) (
V11
()
real
ext-real
)
number
)
)
: ( ( ) (
V11
()
real
ext-real
)
Element
of
REAL
: ( ( ) (
V45
()
V46
()
V47
()
V51
() )
set
) )
+
(
cosh
z
: ( (
real
) (
V11
()
real
ext-real
)
number
)
)
: ( ( ) (
V11
()
real
ext-real
)
Element
of
REAL
: ( ( ) (
V45
()
V46
()
V47
()
V51
() )
set
) )
)
: ( ( ) (
V11
()
real
ext-real
)
set
)
^2
)
: ( ( ) (
V11
()
real
ext-real
)
set
)
-
(
(
(
sinh
y
: ( (
real
) (
V11
()
real
ext-real
)
number
)
)
: ( ( ) (
V11
()
real
ext-real
)
Element
of
REAL
: ( ( ) (
V45
()
V46
()
V47
()
V51
() )
set
) )
+
(
sinh
z
: ( (
real
) (
V11
()
real
ext-real
)
number
)
)
: ( ( ) (
V11
()
real
ext-real
)
Element
of
REAL
: ( ( ) (
V45
()
V46
()
V47
()
V51
() )
set
) )
)
: ( ( ) (
V11
()
real
ext-real
)
set
)
^2
)
: ( ( ) (
V11
()
real
ext-real
)
set
) : ( ( ) (
V11
()
real
ext-real
)
set
)
=
4 : ( ( ) (
V1
()
ordinal
natural
V11
()
real
ext-real
positive
non
negative
V33
()
V34
()
V45
()
V46
()
V47
()
V48
()
V49
()
V50
() )
Element
of
NAT
: ( ( ) (
V45
()
V46
()
V47
()
V48
()
V49
()
V50
()
V51
() )
Element
of
K6
(
REAL
: ( ( ) (
V45
()
V46
()
V47
()
V51
() )
set
) ) : ( ( ) ( )
set
) ) )
*
(
(
cosh
(
(
y
: ( (
real
) (
V11
()
real
ext-real
)
number
)
-
z
: ( (
real
) (
V11
()
real
ext-real
)
number
)
)
: ( ( ) (
V11
()
real
ext-real
)
set
)
/
2 : ( ( ) (
V1
()
ordinal
natural
V11
()
real
ext-real
positive
non
negative
V33
()
V34
()
V45
()
V46
()
V47
()
V48
()
V49
()
V50
() )
Element
of
NAT
: ( ( ) (
V45
()
V46
()
V47
()
V48
()
V49
()
V50
()
V51
() )
Element
of
K6
(
REAL
: ( ( ) (
V45
()
V46
()
V47
()
V51
() )
set
) ) : ( ( ) ( )
set
) ) )
)
: ( ( ) (
V11
()
real
ext-real
)
set
)
)
: ( ( ) (
V11
()
real
ext-real
)
Element
of
REAL
: ( ( ) (
V45
()
V46
()
V47
()
V51
() )
set
) )
^2
)
: ( ( ) (
V11
()
real
ext-real
)
Element
of
REAL
: ( ( ) (
V45
()
V46
()
V47
()
V51
() )
set
) ) : ( ( ) (
V11
()
real
ext-real
)
set
) ) ;
theorem
:: SIN_COS8:14
for
y
,
z
being ( (
real
) (
V11
()
real
ext-real
)
number
) holds
(
(
sinh
y
: ( (
real
) (
V11
()
real
ext-real
)
number
)
)
: ( ( ) (
V11
()
real
ext-real
)
Element
of
REAL
: ( ( ) (
V45
()
V46
()
V47
()
V51
() )
set
) )
+
(
sinh
z
: ( (
real
) (
V11
()
real
ext-real
)
number
)
)
: ( ( ) (
V11
()
real
ext-real
)
Element
of
REAL
: ( ( ) (
V45
()
V46
()
V47
()
V51
() )
set
) )
)
: ( ( ) (
V11
()
real
ext-real
)
set
)
/
(
(
sinh
y
: ( (
real
) (
V11
()
real
ext-real
)
number
)
)
: ( ( ) (
V11
()
real
ext-real
)
Element
of
REAL
: ( ( ) (
V45
()
V46
()
V47
()
V51
() )
set
) )
-
(
sinh
z
: ( (
real
) (
V11
()
real
ext-real
)
number
)
)
: ( ( ) (
V11
()
real
ext-real
)
Element
of
REAL
: ( ( ) (
V45
()
V46
()
V47
()
V51
() )
set
) )
)
: ( ( ) (
V11
()
real
ext-real
)
set
) : ( ( ) (
V11
()
real
ext-real
)
set
)
=
(
tanh
(
(
y
: ( (
real
) (
V11
()
real
ext-real
)
number
)
+
z
: ( (
real
) (
V11
()
real
ext-real
)
number
)
)
: ( ( ) (
V11
()
real
ext-real
)
set
)
/
2 : ( ( ) (
V1
()
ordinal
natural
V11
()
real
ext-real
positive
non
negative
V33
()
V34
()
V45
()
V46
()
V47
()
V48
()
V49
()
V50
() )
Element
of
NAT
: ( ( ) (
V45
()
V46
()
V47
()
V48
()
V49
()
V50
()
V51
() )
Element
of
K6
(
REAL
: ( ( ) (
V45
()
V46
()
V47
()
V51
() )
set
) ) : ( ( ) ( )
set
) ) )
)
: ( ( ) (
V11
()
real
ext-real
)
set
)
)
: ( ( ) (
V11
()
real
ext-real
)
Element
of
REAL
: ( ( ) (
V45
()
V46
()
V47
()
V51
() )
set
) )
*
(
coth
(
(
y
: ( (
real
) (
V11
()
real
ext-real
)
number
)
-
z
: ( (
real
) (
V11
()
real
ext-real
)
number
)
)
: ( ( ) (
V11
()
real
ext-real
)
set
)
/
2 : ( ( ) (
V1
()
ordinal
natural
V11
()
real
ext-real
positive
non
negative
V33
()
V34
()
V45
()
V46
()
V47
()
V48
()
V49
()
V50
() )
Element
of
NAT
: ( ( ) (
V45
()
V46
()
V47
()
V48
()
V49
()
V50
()
V51
() )
Element
of
K6
(
REAL
: ( ( ) (
V45
()
V46
()
V47
()
V51
() )
set
) ) : ( ( ) ( )
set
) ) )
)
: ( ( ) (
V11
()
real
ext-real
)
set
)
)
: ( ( ) (
V11
()
real
ext-real
)
Element
of
REAL
: ( ( ) (
V45
()
V46
()
V47
()
V51
() )
set
) ) : ( ( ) (
V11
()
real
ext-real
)
set
) ;
theorem
:: SIN_COS8:15
for
y
,
z
being ( (
real
) (
V11
()
real
ext-real
)
number
) holds
(
(
cosh
y
: ( (
real
) (
V11
()
real
ext-real
)
number
)
)
: ( ( ) (
V11
()
real
ext-real
)
Element
of
REAL
: ( ( ) (
V45
()
V46
()
V47
()
V51
() )
set
) )
+
(
cosh
z
: ( (
real
) (
V11
()
real
ext-real
)
number
)
)
: ( ( ) (
V11
()
real
ext-real
)
Element
of
REAL
: ( ( ) (
V45
()
V46
()
V47
()
V51
() )
set
) )
)
: ( ( ) (
V11
()
real
ext-real
)
set
)
/
(
(
cosh
y
: ( (
real
) (
V11
()
real
ext-real
)
number
)
)
: ( ( ) (
V11
()
real
ext-real
)
Element
of
REAL
: ( ( ) (
V45
()
V46
()
V47
()
V51
() )
set
) )
-
(
cosh
z
: ( (
real
) (
V11
()
real
ext-real
)
number
)
)
: ( ( ) (
V11
()
real
ext-real
)
Element
of
REAL
: ( ( ) (
V45
()
V46
()
V47
()
V51
() )
set
) )
)
: ( ( ) (
V11
()
real
ext-real
)
set
) : ( ( ) (
V11
()
real
ext-real
)
set
)
=
(
coth
(
(
y
: ( (
real
) (
V11
()
real
ext-real
)
number
)
+
z
: ( (
real
) (
V11
()
real
ext-real
)
number
)
)
: ( ( ) (
V11
()
real
ext-real
)
set
)
/
2 : ( ( ) (
V1
()
ordinal
natural
V11
()
real
ext-real
positive
non
negative
V33
()
V34
()
V45
()
V46
()
V47
()
V48
()
V49
()
V50
() )
Element
of
NAT
: ( ( ) (
V45
()
V46
()
V47
()
V48
()
V49
()
V50
()
V51
() )
Element
of
K6
(
REAL
: ( ( ) (
V45
()
V46
()
V47
()
V51
() )
set
) ) : ( ( ) ( )
set
) ) )
)
: ( ( ) (
V11
()
real
ext-real
)
set
)
)
: ( ( ) (
V11
()
real
ext-real
)
Element
of
REAL
: ( ( ) (
V45
()
V46
()
V47
()
V51
() )
set
) )
*
(
coth
(
(
y
: ( (
real
) (
V11
()
real
ext-real
)
number
)
-
z
: ( (
real
) (
V11
()
real
ext-real
)
number
)
)
: ( ( ) (
V11
()
real
ext-real
)
set
)
/
2 : ( ( ) (
V1
()
ordinal
natural
V11
()
real
ext-real
positive
non
negative
V33
()
V34
()
V45
()
V46
()
V47
()
V48
()
V49
()
V50
() )
Element
of
NAT
: ( ( ) (
V45
()
V46
()
V47
()
V48
()
V49
()
V50
()
V51
() )
Element
of
K6
(
REAL
: ( ( ) (
V45
()
V46
()
V47
()
V51
() )
set
) ) : ( ( ) ( )
set
) ) )
)
: ( ( ) (
V11
()
real
ext-real
)
set
)
)
: ( ( ) (
V11
()
real
ext-real
)
Element
of
REAL
: ( ( ) (
V45
()
V46
()
V47
()
V51
() )
set
) ) : ( ( ) (
V11
()
real
ext-real
)
set
) ;
theorem
:: SIN_COS8:16
for
y
,
z
being ( (
real
) (
V11
()
real
ext-real
)
number
) st
y
: ( (
real
) (
V11
()
real
ext-real
)
number
)
-
z
: ( (
real
) (
V11
()
real
ext-real
)
number
) : ( ( ) (
V11
()
real
ext-real
)
set
)
<>
0
: ( ( ) (
V1
()
ordinal
natural
V11
()
real
ext-real
non
positive
non
negative
V33
()
V34
()
V45
()
V46
()
V47
()
V48
()
V49
()
V50
()
V51
() )
Element
of
NAT
: ( ( ) (
V45
()
V46
()
V47
()
V48
()
V49
()
V50
()
V51
() )
Element
of
K6
(
REAL
: ( ( ) (
V45
()
V46
()
V47
()
V51
() )
set
) ) : ( ( ) ( )
set
) ) ) holds
(
(
sinh
y
: ( (
real
) (
V11
()
real
ext-real
)
number
)
)
: ( ( ) (
V11
()
real
ext-real
)
Element
of
REAL
: ( ( ) (
V45
()
V46
()
V47
()
V51
() )
set
) )
+
(
sinh
z
: ( (
real
) (
V11
()
real
ext-real
)
number
)
)
: ( ( ) (
V11
()
real
ext-real
)
Element
of
REAL
: ( ( ) (
V45
()
V46
()
V47
()
V51
() )
set
) )
)
: ( ( ) (
V11
()
real
ext-real
)
set
)
/
(
(
cosh
y
: ( (
real
) (
V11
()
real
ext-real
)
number
)
)
: ( ( ) (
V11
()
real
ext-real
)
Element
of
REAL
: ( ( ) (
V45
()
V46
()
V47
()
V51
() )
set
) )
+
(
cosh
z
: ( (
real
) (
V11
()
real
ext-real
)
number
)
)
: ( ( ) (
V11
()
real
ext-real
)
Element
of
REAL
: ( ( ) (
V45
()
V46
()
V47
()
V51
() )
set
) )
)
: ( ( ) (
V11
()
real
ext-real
)
set
) : ( ( ) (
V11
()
real
ext-real
)
set
)
=
(
(
cosh
y
: ( (
real
) (
V11
()
real
ext-real
)
number
)
)
: ( ( ) (
V11
()
real
ext-real
)
Element
of
REAL
: ( ( ) (
V45
()
V46
()
V47
()
V51
() )
set
) )
-
(
cosh
z
: ( (
real
) (
V11
()
real
ext-real
)
number
)
)
: ( ( ) (
V11
()
real
ext-real
)
Element
of
REAL
: ( ( ) (
V45
()
V46
()
V47
()
V51
() )
set
) )
)
: ( ( ) (
V11
()
real
ext-real
)
set
)
/
(
(
sinh
y
: ( (
real
) (
V11
()
real
ext-real
)
number
)
)
: ( ( ) (
V11
()
real
ext-real
)
Element
of
REAL
: ( ( ) (
V45
()
V46
()
V47
()
V51
() )
set
) )
-
(
sinh
z
: ( (
real
) (
V11
()
real
ext-real
)
number
)
)
: ( ( ) (
V11
()
real
ext-real
)
Element
of
REAL
: ( ( ) (
V45
()
V46
()
V47
()
V51
() )
set
) )
)
: ( ( ) (
V11
()
real
ext-real
)
set
) : ( ( ) (
V11
()
real
ext-real
)
set
) ;
theorem
:: SIN_COS8:17
for
y
,
z
being ( (
real
) (
V11
()
real
ext-real
)
number
) st
y
: ( (
real
) (
V11
()
real
ext-real
)
number
)
+
z
: ( (
real
) (
V11
()
real
ext-real
)
number
) : ( ( ) (
V11
()
real
ext-real
)
set
)
<>
0
: ( ( ) (
V1
()
ordinal
natural
V11
()
real
ext-real
non
positive
non
negative
V33
()
V34
()
V45
()
V46
()
V47
()
V48
()
V49
()
V50
()
V51
() )
Element
of
NAT
: ( ( ) (
V45
()
V46
()
V47
()
V48
()
V49
()
V50
()
V51
() )
Element
of
K6
(
REAL
: ( ( ) (
V45
()
V46
()
V47
()
V51
() )
set
) ) : ( ( ) ( )
set
) ) ) holds
(
(
sinh
y
: ( (
real
) (
V11
()
real
ext-real
)
number
)
)
: ( ( ) (
V11
()
real
ext-real
)
Element
of
REAL
: ( ( ) (
V45
()
V46
()
V47
()
V51
() )
set
) )
-
(
sinh
z
: ( (
real
) (
V11
()
real
ext-real
)
number
)
)
: ( ( ) (
V11
()
real
ext-real
)
Element
of
REAL
: ( ( ) (
V45
()
V46
()
V47
()
V51
() )
set
) )
)
: ( ( ) (
V11
()
real
ext-real
)
set
)
/
(
(
cosh
y
: ( (
real
) (
V11
()
real
ext-real
)
number
)
)
: ( ( ) (
V11
()
real
ext-real
)
Element
of
REAL
: ( ( ) (
V45
()
V46
()
V47
()
V51
() )
set
) )
+
(
cosh
z
: ( (
real
) (
V11
()
real
ext-real
)
number
)
)
: ( ( ) (
V11
()
real
ext-real
)
Element
of
REAL
: ( ( ) (
V45
()
V46
()
V47
()
V51
() )
set
) )
)
: ( ( ) (
V11
()
real
ext-real
)
set
) : ( ( ) (
V11
()
real
ext-real
)
set
)
=
(
(
cosh
y
: ( (
real
) (
V11
()
real
ext-real
)
number
)
)
: ( ( ) (
V11
()
real
ext-real
)
Element
of
REAL
: ( ( ) (
V45
()
V46
()
V47
()
V51
() )
set
) )
-
(
cosh
z
: ( (
real
) (
V11
()
real
ext-real
)
number
)
)
: ( ( ) (
V11
()
real
ext-real
)
Element
of
REAL
: ( ( ) (
V45
()
V46
()
V47
()
V51
() )
set
) )
)
: ( ( ) (
V11
()
real
ext-real
)
set
)
/
(
(
sinh
y
: ( (
real
) (
V11
()
real
ext-real
)
number
)
)
: ( ( ) (
V11
()
real
ext-real
)
Element
of
REAL
: ( ( ) (
V45
()
V46
()
V47
()
V51
() )
set
) )
+
(
sinh
z
: ( (
real
) (
V11
()
real
ext-real
)
number
)
)
: ( ( ) (
V11
()
real
ext-real
)
Element
of
REAL
: ( ( ) (
V45
()
V46
()
V47
()
V51
() )
set
) )
)
: ( ( ) (
V11
()
real
ext-real
)
set
) : ( ( ) (
V11
()
real
ext-real
)
set
) ;
theorem
:: SIN_COS8:18
for
y
,
z
being ( (
real
) (
V11
()
real
ext-real
)
number
) holds
(
(
(
sinh
y
: ( (
real
) (
V11
()
real
ext-real
)
number
)
)
: ( ( ) (
V11
()
real
ext-real
)
Element
of
REAL
: ( ( ) (
V45
()
V46
()
V47
()
V51
() )
set
) )
+
(
sinh
z
: ( (
real
) (
V11
()
real
ext-real
)
number
)
)
: ( ( ) (
V11
()
real
ext-real
)
Element
of
REAL
: ( ( ) (
V45
()
V46
()
V47
()
V51
() )
set
) )
)
: ( ( ) (
V11
()
real
ext-real
)
set
)
/
(
(
cosh
y
: ( (
real
) (
V11
()
real
ext-real
)
number
)
)
: ( ( ) (
V11
()
real
ext-real
)
Element
of
REAL
: ( ( ) (
V45
()
V46
()
V47
()
V51
() )
set
) )
+
(
cosh
z
: ( (
real
) (
V11
()
real
ext-real
)
number
)
)
: ( ( ) (
V11
()
real
ext-real
)
Element
of
REAL
: ( ( ) (
V45
()
V46
()
V47
()
V51
() )
set
) )
)
: ( ( ) (
V11
()
real
ext-real
)
set
) : ( ( ) (
V11
()
real
ext-real
)
set
)
=
tanh
(
(
y
: ( (
real
) (
V11
()
real
ext-real
)
number
)
/
2 : ( ( ) (
V1
()
ordinal
natural
V11
()
real
ext-real
positive
non
negative
V33
()
V34
()
V45
()
V46
()
V47
()
V48
()
V49
()
V50
() )
Element
of
NAT
: ( ( ) (
V45
()
V46
()
V47
()
V48
()
V49
()
V50
()
V51
() )
Element
of
K6
(
REAL
: ( ( ) (
V45
()
V46
()
V47
()
V51
() )
set
) ) : ( ( ) ( )
set
) ) )
)
: ( ( ) (
V11
()
real
ext-real
)
set
)
+
(
z
: ( (
real
) (
V11
()
real
ext-real
)
number
)
/
2 : ( ( ) (
V1
()
ordinal
natural
V11
()
real
ext-real
positive
non
negative
V33
()
V34
()
V45
()
V46
()
V47
()
V48
()
V49
()
V50
() )
Element
of
NAT
: ( ( ) (
V45
()
V46
()
V47
()
V48
()
V49
()
V50
()
V51
() )
Element
of
K6
(
REAL
: ( ( ) (
V45
()
V46
()
V47
()
V51
() )
set
) ) : ( ( ) ( )
set
) ) )
)
: ( ( ) (
V11
()
real
ext-real
)
set
)
)
: ( ( ) (
V11
()
real
ext-real
)
set
) : ( ( ) (
V11
()
real
ext-real
)
Element
of
REAL
: ( ( ) (
V45
()
V46
()
V47
()
V51
() )
set
) ) &
(
(
sinh
y
: ( (
real
) (
V11
()
real
ext-real
)
number
)
)
: ( ( ) (
V11
()
real
ext-real
)
Element
of
REAL
: ( ( ) (
V45
()
V46
()
V47
()
V51
() )
set
) )
-
(
sinh
z
: ( (
real
) (
V11
()
real
ext-real
)
number
)
)
: ( ( ) (
V11
()
real
ext-real
)
Element
of
REAL
: ( ( ) (
V45
()
V46
()
V47
()
V51
() )
set
) )
)
: ( ( ) (
V11
()
real
ext-real
)
set
)
/
(
(
cosh
y
: ( (
real
) (
V11
()
real
ext-real
)
number
)
)
: ( ( ) (
V11
()
real
ext-real
)
Element
of
REAL
: ( ( ) (
V45
()
V46
()
V47
()
V51
() )
set
) )
+
(
cosh
z
: ( (
real
) (
V11
()
real
ext-real
)
number
)
)
: ( ( ) (
V11
()
real
ext-real
)
Element
of
REAL
: ( ( ) (
V45
()
V46
()
V47
()
V51
() )
set
) )
)
: ( ( ) (
V11
()
real
ext-real
)
set
) : ( ( ) (
V11
()
real
ext-real
)
set
)
=
tanh
(
(
y
: ( (
real
) (
V11
()
real
ext-real
)
number
)
/
2 : ( ( ) (
V1
()
ordinal
natural
V11
()
real
ext-real
positive
non
negative
V33
()
V34
()
V45
()
V46
()
V47
()
V48
()
V49
()
V50
() )
Element
of
NAT
: ( ( ) (
V45
()
V46
()
V47
()
V48
()
V49
()
V50
()
V51
() )
Element
of
K6
(
REAL
: ( ( ) (
V45
()
V46
()
V47
()
V51
() )
set
) ) : ( ( ) ( )
set
) ) )
)
: ( ( ) (
V11
()
real
ext-real
)
set
)
-
(
z
: ( (
real
) (
V11
()
real
ext-real
)
number
)
/
2 : ( ( ) (
V1
()
ordinal
natural
V11
()
real
ext-real
positive
non
negative
V33
()
V34
()
V45
()
V46
()
V47
()
V48
()
V49
()
V50
() )
Element
of
NAT
: ( ( ) (
V45
()
V46
()
V47
()
V48
()
V49
()
V50
()
V51
() )
Element
of
K6
(
REAL
: ( ( ) (
V45
()
V46
()
V47
()
V51
() )
set
) ) : ( ( ) ( )
set
) ) )
)
: ( ( ) (
V11
()
real
ext-real
)
set
)
)
: ( ( ) (
V11
()
real
ext-real
)
set
) : ( ( ) (
V11
()
real
ext-real
)
Element
of
REAL
: ( ( ) (
V45
()
V46
()
V47
()
V51
() )
set
) ) ) ;
theorem
:: SIN_COS8:19
for
y
,
z
being ( (
real
) (
V11
()
real
ext-real
)
number
) holds
(
(
tanh
y
: ( (
real
) (
V11
()
real
ext-real
)
number
)
)
: ( ( ) (
V11
()
real
ext-real
)
Element
of
REAL
: ( ( ) (
V45
()
V46
()
V47
()
V51
() )
set
) )
+
(
tanh
z
: ( (
real
) (
V11
()
real
ext-real
)
number
)
)
: ( ( ) (
V11
()
real
ext-real
)
Element
of
REAL
: ( ( ) (
V45
()
V46
()
V47
()
V51
() )
set
) )
)
: ( ( ) (
V11
()
real
ext-real
)
set
)
/
(
(
tanh
y
: ( (
real
) (
V11
()
real
ext-real
)
number
)
)
: ( ( ) (
V11
()
real
ext-real
)
Element
of
REAL
: ( ( ) (
V45
()
V46
()
V47
()
V51
() )
set
) )
-
(
tanh
z
: ( (
real
) (
V11
()
real
ext-real
)
number
)
)
: ( ( ) (
V11
()
real
ext-real
)
Element
of
REAL
: ( ( ) (
V45
()
V46
()
V47
()
V51
() )
set
) )
)
: ( ( ) (
V11
()
real
ext-real
)
set
) : ( ( ) (
V11
()
real
ext-real
)
set
)
=
(
sinh
(
y
: ( (
real
) (
V11
()
real
ext-real
)
number
)
+
z
: ( (
real
) (
V11
()
real
ext-real
)
number
)
)
: ( ( ) (
V11
()
real
ext-real
)
set
)
)
: ( ( ) (
V11
()
real
ext-real
)
Element
of
REAL
: ( ( ) (
V45
()
V46
()
V47
()
V51
() )
set
) )
/
(
sinh
(
y
: ( (
real
) (
V11
()
real
ext-real
)
number
)
-
z
: ( (
real
) (
V11
()
real
ext-real
)
number
)
)
: ( ( ) (
V11
()
real
ext-real
)
set
)
)
: ( ( ) (
V11
()
real
ext-real
)
Element
of
REAL
: ( ( ) (
V45
()
V46
()
V47
()
V51
() )
set
) ) : ( ( ) (
V11
()
real
ext-real
)
set
) ;
theorem
:: SIN_COS8:20
for
y
,
z
being ( (
real
) (
V11
()
real
ext-real
)
number
) holds
(
(
(
sinh
(
y
: ( (
real
) (
V11
()
real
ext-real
)
number
)
-
z
: ( (
real
) (
V11
()
real
ext-real
)
number
)
)
: ( ( ) (
V11
()
real
ext-real
)
set
)
)
: ( ( ) (
V11
()
real
ext-real
)
Element
of
REAL
: ( ( ) (
V45
()
V46
()
V47
()
V51
() )
set
) )
+
(
sinh
y
: ( (
real
) (
V11
()
real
ext-real
)
number
)
)
: ( ( ) (
V11
()
real
ext-real
)
Element
of
REAL
: ( ( ) (
V45
()
V46
()
V47
()
V51
() )
set
) )
)
: ( ( ) (
V11
()
real
ext-real
)
set
)
+
(
sinh
(
y
: ( (
real
) (
V11
()
real
ext-real
)
number
)
+
z
: ( (
real
) (
V11
()
real
ext-real
)
number
)
)
: ( ( ) (
V11
()
real
ext-real
)
set
)
)
: ( ( ) (
V11
()
real
ext-real
)
Element
of
REAL
: ( ( ) (
V45
()
V46
()
V47
()
V51
() )
set
) )
)
: ( ( ) (
V11
()
real
ext-real
)
set
)
/
(
(
(
cosh
(
y
: ( (
real
) (
V11
()
real
ext-real
)
number
)
-
z
: ( (
real
) (
V11
()
real
ext-real
)
number
)
)
: ( ( ) (
V11
()
real
ext-real
)
set
)
)
: ( ( ) (
V11
()
real
ext-real
)
Element
of
REAL
: ( ( ) (
V45
()
V46
()
V47
()
V51
() )
set
) )
+
(
cosh
y
: ( (
real
) (
V11
()
real
ext-real
)
number
)
)
: ( ( ) (
V11
()
real
ext-real
)
Element
of
REAL
: ( ( ) (
V45
()
V46
()
V47
()
V51
() )
set
) )
)
: ( ( ) (
V11
()
real
ext-real
)
set
)
+
(
cosh
(
y
: ( (
real
) (
V11
()
real
ext-real
)
number
)
+
z
: ( (
real
) (
V11
()
real
ext-real
)
number
)
)
: ( ( ) (
V11
()
real
ext-real
)
set
)
)
: ( ( ) (
V11
()
real
ext-real
)
Element
of
REAL
: ( ( ) (
V45
()
V46
()
V47
()
V51
() )
set
) )
)
: ( ( ) (
V11
()
real
ext-real
)
set
) : ( ( ) (
V11
()
real
ext-real
)
set
)
=
tanh
y
: ( (
real
) (
V11
()
real
ext-real
)
number
) : ( ( ) (
V11
()
real
ext-real
)
Element
of
REAL
: ( ( ) (
V45
()
V46
()
V47
()
V51
() )
set
) ) ;
theorem
:: SIN_COS8:21
for
y
,
z
,
w
being ( (
real
) (
V11
()
real
ext-real
)
number
) holds
(
sinh
(
(
y
: ( (
real
) (
V11
()
real
ext-real
)
number
)
+
z
: ( (
real
) (
V11
()
real
ext-real
)
number
)
)
: ( ( ) (
V11
()
real
ext-real
)
set
)
+
w
: ( (
real
) (
V11
()
real
ext-real
)
number
)
)
: ( ( ) (
V11
()
real
ext-real
)
set
) : ( ( ) (
V11
()
real
ext-real
)
Element
of
REAL
: ( ( ) (
V45
()
V46
()
V47
()
V51
() )
set
) )
=
(
(
(
(
(
(
tanh
y
: ( (
real
) (
V11
()
real
ext-real
)
number
)
)
: ( ( ) (
V11
()
real
ext-real
)
Element
of
REAL
: ( ( ) (
V45
()
V46
()
V47
()
V51
() )
set
) )
+
(
tanh
z
: ( (
real
) (
V11
()
real
ext-real
)
number
)
)
: ( ( ) (
V11
()
real
ext-real
)
Element
of
REAL
: ( ( ) (
V45
()
V46
()
V47
()
V51
() )
set
) )
)
: ( ( ) (
V11
()
real
ext-real
)
set
)
+
(
tanh
w
: ( (
real
) (
V11
()
real
ext-real
)
number
)
)
: ( ( ) (
V11
()
real
ext-real
)
Element
of
REAL
: ( ( ) (
V45
()
V46
()
V47
()
V51
() )
set
) )
)
: ( ( ) (
V11
()
real
ext-real
)
set
)
+
(
(
(
tanh
y
: ( (
real
) (
V11
()
real
ext-real
)
number
)
)
: ( ( ) (
V11
()
real
ext-real
)
Element
of
REAL
: ( ( ) (
V45
()
V46
()
V47
()
V51
() )
set
) )
*
(
tanh
z
: ( (
real
) (
V11
()
real
ext-real
)
number
)
)
: ( ( ) (
V11
()
real
ext-real
)
Element
of
REAL
: ( ( ) (
V45
()
V46
()
V47
()
V51
() )
set
) )
)
: ( ( ) (
V11
()
real
ext-real
)
set
)
*
(
tanh
w
: ( (
real
) (
V11
()
real
ext-real
)
number
)
)
: ( ( ) (
V11
()
real
ext-real
)
Element
of
REAL
: ( ( ) (
V45
()
V46
()
V47
()
V51
() )
set
) )
)
: ( ( ) (
V11
()
real
ext-real
)
set
)
)
: ( ( ) (
V11
()
real
ext-real
)
set
)
*
(
cosh
y
: ( (
real
) (
V11
()
real
ext-real
)
number
)
)
: ( ( ) (
V11
()
real
ext-real
)
Element
of
REAL
: ( ( ) (
V45
()
V46
()
V47
()
V51
() )
set
) )
)
: ( ( ) (
V11
()
real
ext-real
)
set
)
*
(
cosh
z
: ( (
real
) (
V11
()
real
ext-real
)
number
)
)
: ( ( ) (
V11
()
real
ext-real
)
Element
of
REAL
: ( ( ) (
V45
()
V46
()
V47
()
V51
() )
set
) )
)
: ( ( ) (
V11
()
real
ext-real
)
set
)
*
(
cosh
w
: ( (
real
) (
V11
()
real
ext-real
)
number
)
)
: ( ( ) (
V11
()
real
ext-real
)
Element
of
REAL
: ( ( ) (
V45
()
V46
()
V47
()
V51
() )
set
) ) : ( ( ) (
V11
()
real
ext-real
)
set
) &
cosh
(
(
y
: ( (
real
) (
V11
()
real
ext-real
)
number
)
+
z
: ( (
real
) (
V11
()
real
ext-real
)
number
)
)
: ( ( ) (
V11
()
real
ext-real
)
set
)
+
w
: ( (
real
) (
V11
()
real
ext-real
)
number
)
)
: ( ( ) (
V11
()
real
ext-real
)
set
) : ( ( ) (
V11
()
real
ext-real
)
Element
of
REAL
: ( ( ) (
V45
()
V46
()
V47
()
V51
() )
set
) )
=
(
(
(
(
(
1 : ( ( ) (
V1
()
ordinal
natural
V11
()
real
ext-real
positive
non
negative
V33
()
V34
()
V45
()
V46
()
V47
()
V48
()
V49
()
V50
() )
Element
of
NAT
: ( ( ) (
V45
()
V46
()
V47
()
V48
()
V49
()
V50
()
V51
() )
Element
of
K6
(
REAL
: ( ( ) (
V45
()
V46
()
V47
()
V51
() )
set
) ) : ( ( ) ( )
set
) ) )
+
(
(
tanh
y
: ( (
real
) (
V11
()
real
ext-real
)
number
)
)
: ( ( ) (
V11
()
real
ext-real
)
Element
of
REAL
: ( ( ) (
V45
()
V46
()
V47
()
V51
() )
set
) )
*
(
tanh
z
: ( (
real
) (
V11
()
real
ext-real
)
number
)
)
: ( ( ) (
V11
()
real
ext-real
)
Element
of
REAL
: ( ( ) (
V45
()
V46
()
V47
()
V51
() )
set
) )
)
: ( ( ) (
V11
()
real
ext-real
)
set
)
)
: ( ( ) (
V11
()
real
ext-real
)
set
)
+
(
(
tanh
z
: ( (
real
) (
V11
()
real
ext-real
)
number
)
)
: ( ( ) (
V11
()
real
ext-real
)
Element
of
REAL
: ( ( ) (
V45
()
V46
()
V47
()
V51
() )
set
) )
*
(
tanh
w
: ( (
real
) (
V11
()
real
ext-real
)
number
)
)
: ( ( ) (
V11
()
real
ext-real
)
Element
of
REAL
: ( ( ) (
V45
()
V46
()
V47
()
V51
() )
set
) )
)
: ( ( ) (
V11
()
real
ext-real
)
set
)
)
: ( ( ) (
V11
()
real
ext-real
)
set
)
+
(
(
tanh
w
: ( (
real
) (
V11
()
real
ext-real
)
number
)
)
: ( ( ) (
V11
()
real
ext-real
)
Element
of
REAL
: ( ( ) (
V45
()
V46
()
V47
()
V51
() )
set
) )
*
(
tanh
y
: ( (
real
) (
V11
()
real
ext-real
)
number
)
)
: ( ( ) (
V11
()
real
ext-real
)
Element
of
REAL
: ( ( ) (
V45
()
V46
()
V47
()
V51
() )
set
) )
)
: ( ( ) (
V11
()
real
ext-real
)
set
)
)
: ( ( ) (
V11
()
real
ext-real
)
set
)
*
(
cosh
y
: ( (
real
) (
V11
()
real
ext-real
)
number
)
)
: ( ( ) (
V11
()
real
ext-real
)
Element
of
REAL
: ( ( ) (
V45
()
V46
()
V47
()
V51
() )
set
) )
)
: ( ( ) (
V11
()
real
ext-real
)
set
)
*
(
cosh
z
: ( (
real
) (
V11
()
real
ext-real
)
number
)
)
: ( ( ) (
V11
()
real
ext-real
)
Element
of
REAL
: ( ( ) (
V45
()
V46
()
V47
()
V51
() )
set
) )
)
: ( ( ) (
V11
()
real
ext-real
)
set
)
*
(
cosh
w
: ( (
real
) (
V11
()
real
ext-real
)
number
)
)
: ( ( ) (
V11
()
real
ext-real
)
Element
of
REAL
: ( ( ) (
V45
()
V46
()
V47
()
V51
() )
set
) ) : ( ( ) (
V11
()
real
ext-real
)
set
) &
tanh
(
(
y
: ( (
real
) (
V11
()
real
ext-real
)
number
)
+
z
: ( (
real
) (
V11
()
real
ext-real
)
number
)
)
: ( ( ) (
V11
()
real
ext-real
)
set
)
+
w
: ( (
real
) (
V11
()
real
ext-real
)
number
)
)
: ( ( ) (
V11
()
real
ext-real
)
set
) : ( ( ) (
V11
()
real
ext-real
)
Element
of
REAL
: ( ( ) (
V45
()
V46
()
V47
()
V51
() )
set
) )
=
(
(
(
(
tanh
y
: ( (
real
) (
V11
()
real
ext-real
)
number
)
)
: ( ( ) (
V11
()
real
ext-real
)
Element
of
REAL
: ( ( ) (
V45
()
V46
()
V47
()
V51
() )
set
) )
+
(
tanh
z
: ( (
real
) (
V11
()
real
ext-real
)
number
)
)
: ( ( ) (
V11
()
real
ext-real
)
Element
of
REAL
: ( ( ) (
V45
()
V46
()
V47
()
V51
() )
set
) )
)
: ( ( ) (
V11
()
real
ext-real
)
set
)
+
(
tanh
w
: ( (
real
) (
V11
()
real
ext-real
)
number
)
)
: ( ( ) (
V11
()
real
ext-real
)
Element
of
REAL
: ( ( ) (
V45
()
V46
()
V47
()
V51
() )
set
) )
)
: ( ( ) (
V11
()
real
ext-real
)
set
)
+
(
(
(
tanh
y
: ( (
real
) (
V11
()
real
ext-real
)
number
)
)
: ( ( ) (
V11
()
real
ext-real
)
Element
of
REAL
: ( ( ) (
V45
()
V46
()
V47
()
V51
() )
set
) )
*
(
tanh
z
: ( (
real
) (
V11
()
real
ext-real
)
number
)
)
: ( ( ) (
V11
()
real
ext-real
)
Element
of
REAL
: ( ( ) (
V45
()
V46
()
V47
()
V51
() )
set
) )
)
: ( ( ) (
V11
()
real
ext-real
)
set
)
*
(
tanh
w
: ( (
real
) (
V11
()
real
ext-real
)
number
)
)
: ( ( ) (
V11
()
real
ext-real
)
Element
of
REAL
: ( ( ) (
V45
()
V46
()
V47
()
V51
() )
set
) )
)
: ( ( ) (
V11
()
real
ext-real
)
set
)
)
: ( ( ) (
V11
()
real
ext-real
)
set
)
/
(
(
(
1 : ( ( ) (
V1
()
ordinal
natural
V11
()
real
ext-real
positive
non
negative
V33
()
V34
()
V45
()
V46
()
V47
()
V48
()
V49
()
V50
() )
Element
of
NAT
: ( ( ) (
V45
()
V46
()
V47
()
V48
()
V49
()
V50
()
V51
() )
Element
of
K6
(
REAL
: ( ( ) (
V45
()
V46
()
V47
()
V51
() )
set
) ) : ( ( ) ( )
set
) ) )
+
(
(
tanh
z
: ( (
real
) (
V11
()
real
ext-real
)
number
)
)
: ( ( ) (
V11
()
real
ext-real
)
Element
of
REAL
: ( ( ) (
V45
()
V46
()
V47
()
V51
() )
set
) )
*
(
tanh
w
: ( (
real
) (
V11
()
real
ext-real
)
number
)
)
: ( ( ) (
V11
()
real
ext-real
)
Element
of
REAL
: ( ( ) (
V45
()
V46
()
V47
()
V51
() )
set
) )
)
: ( ( ) (
V11
()
real
ext-real
)
set
)
)
: ( ( ) (
V11
()
real
ext-real
)
set
)
+
(
(
tanh
w
: ( (
real
) (
V11
()
real
ext-real
)
number
)
)
: ( ( ) (
V11
()
real
ext-real
)
Element
of
REAL
: ( ( ) (
V45
()
V46
()
V47
()
V51
() )
set
) )
*
(
tanh
y
: ( (
real
) (
V11
()
real
ext-real
)
number
)
)
: ( ( ) (
V11
()
real
ext-real
)
Element
of
REAL
: ( ( ) (
V45
()
V46
()
V47
()
V51
() )
set
) )
)
: ( ( ) (
V11
()
real
ext-real
)
set
)
)
: ( ( ) (
V11
()
real
ext-real
)
set
)
+
(
(
tanh
y
: ( (
real
) (
V11
()
real
ext-real
)
number
)
)
: ( ( ) (
V11
()
real
ext-real
)
Element
of
REAL
: ( ( ) (
V45
()
V46
()
V47
()
V51
() )
set
) )
*
(
tanh
z
: ( (
real
) (
V11
()
real
ext-real
)
number
)
)
: ( ( ) (
V11
()
real
ext-real
)
Element
of
REAL
: ( ( ) (
V45
()
V46
()
V47
()
V51
() )
set
) )
)
: ( ( ) (
V11
()
real
ext-real
)
set
)
)
: ( ( ) (
V11
()
real
ext-real
)
set
) : ( ( ) (
V11
()
real
ext-real
)
set
) ) ;
theorem
:: SIN_COS8:22
for
y
,
z
,
w
being ( (
real
) (
V11
()
real
ext-real
)
number
) holds
(
(
(
cosh
(
2 : ( ( ) (
V1
()
ordinal
natural
V11
()
real
ext-real
positive
non
negative
V33
()
V34
()
V45
()
V46
()
V47
()
V48
()
V49
()
V50
() )
Element
of
NAT
: ( ( ) (
V45
()
V46
()
V47
()
V48
()
V49
()
V50
()
V51
() )
Element
of
K6
(
REAL
: ( ( ) (
V45
()
V46
()
V47
()
V51
() )
set
) ) : ( ( ) ( )
set
) ) )
*
y
: ( (
real
) (
V11
()
real
ext-real
)
number
)
)
: ( ( ) (
V11
()
real
ext-real
)
set
)
)
: ( ( ) (
V11
()
real
ext-real
)
Element
of
REAL
: ( ( ) (
V45
()
V46
()
V47
()
V51
() )
set
) )
+
(
cosh
(
2 : ( ( ) (
V1
()
ordinal
natural
V11
()
real
ext-real
positive
non
negative
V33
()
V34
()
V45
()
V46
()
V47
()
V48
()
V49
()
V50
() )
Element
of
NAT
: ( ( ) (
V45
()
V46
()
V47
()
V48
()
V49
()
V50
()
V51
() )
Element
of
K6
(
REAL
: ( ( ) (
V45
()
V46
()
V47
()
V51
() )
set
) ) : ( ( ) ( )
set
) ) )
*
z
: ( (
real
) (
V11
()
real
ext-real
)
number
)
)
: ( ( ) (
V11
()
real
ext-real
)
set
)
)
: ( ( ) (
V11
()
real
ext-real
)
Element
of
REAL
: ( ( ) (
V45
()
V46
()
V47
()
V51
() )
set
) )
)
: ( ( ) (
V11
()
real
ext-real
)
set
)
+
(
cosh
(
2 : ( ( ) (
V1
()
ordinal
natural
V11
()
real
ext-real
positive
non
negative
V33
()
V34
()
V45
()
V46
()
V47
()
V48
()
V49
()
V50
() )
Element
of
NAT
: ( ( ) (
V45
()
V46
()
V47
()
V48
()
V49
()
V50
()
V51
() )
Element
of
K6
(
REAL
: ( ( ) (
V45
()
V46
()
V47
()
V51
() )
set
) ) : ( ( ) ( )
set
) ) )
*
w
: ( (
real
) (
V11
()
real
ext-real
)
number
)
)
: ( ( ) (
V11
()
real
ext-real
)
set
)
)
: ( ( ) (
V11
()
real
ext-real
)
Element
of
REAL
: ( ( ) (
V45
()
V46
()
V47
()
V51
() )
set
) )
)
: ( ( ) (
V11
()
real
ext-real
)
set
)
+
(
cosh
(
2 : ( ( ) (
V1
()
ordinal
natural
V11
()
real
ext-real
positive
non
negative
V33
()
V34
()
V45
()
V46
()
V47
()
V48
()
V49
()
V50
() )
Element
of
NAT
: ( ( ) (
V45
()
V46
()
V47
()
V48
()
V49
()
V50
()
V51
() )
Element
of
K6
(
REAL
: ( ( ) (
V45
()
V46
()
V47
()
V51
() )
set
) ) : ( ( ) ( )
set
) ) )
*
(
(
y
: ( (
real
) (
V11
()
real
ext-real
)
number
)
+
z
: ( (
real
) (
V11
()
real
ext-real
)
number
)
)
: ( ( ) (
V11
()
real
ext-real
)
set
)
+
w
: ( (
real
) (
V11
()
real
ext-real
)
number
)
)
: ( ( ) (
V11
()
real
ext-real
)
set
)
)
: ( ( ) (
V11
()
real
ext-real
)
set
)
)
: ( ( ) (
V11
()
real
ext-real
)
Element
of
REAL
: ( ( ) (
V45
()
V46
()
V47
()
V51
() )
set
) ) : ( ( ) (
V11
()
real
ext-real
)
set
)
=
(
(
4 : ( ( ) (
V1
()
ordinal
natural
V11
()
real
ext-real
positive
non
negative
V33
()
V34
()
V45
()
V46
()
V47
()
V48
()
V49
()
V50
() )
Element
of
NAT
: ( ( ) (
V45
()
V46
()
V47
()
V48
()
V49
()
V50
()
V51
() )
Element
of
K6
(
REAL
: ( ( ) (
V45
()
V46
()
V47
()
V51
() )
set
) ) : ( ( ) ( )
set
) ) )
*
(
cosh
(
z
: ( (
real
) (
V11
()
real
ext-real
)
number
)
+
w
: ( (
real
) (
V11
()
real
ext-real
)
number
)
)
: ( ( ) (
V11
()
real
ext-real
)
set
)
)
: ( ( ) (
V11
()
real
ext-real
)
Element
of
REAL
: ( ( ) (
V45
()
V46
()
V47
()
V51
() )
set
) )
)
: ( ( ) (
V11
()
real
ext-real
)
set
)
*
(
cosh
(
w
: ( (
real
) (
V11
()
real
ext-real
)
number
)
+
y
: ( (
real
) (
V11
()
real
ext-real
)
number
)
)
: ( ( ) (
V11
()
real
ext-real
)
set
)
)
: ( ( ) (
V11
()
real
ext-real
)
Element
of
REAL
: ( ( ) (
V45
()
V46
()
V47
()
V51
() )
set
) )
)
: ( ( ) (
V11
()
real
ext-real
)
set
)
*
(
cosh
(
y
: ( (
real
) (
V11
()
real
ext-real
)
number
)
+
z
: ( (
real
) (
V11
()
real
ext-real
)
number
)
)
: ( ( ) (
V11
()
real
ext-real
)
set
)
)
: ( ( ) (
V11
()
real
ext-real
)
Element
of
REAL
: ( ( ) (
V45
()
V46
()
V47
()
V51
() )
set
) ) : ( ( ) (
V11
()
real
ext-real
)
set
) ;
theorem
:: SIN_COS8:23
for
y
,
z
,
w
being ( (
real
) (
V11
()
real
ext-real
)
number
) holds
(
(
(
(
(
sinh
y
: ( (
real
) (
V11
()
real
ext-real
)
number
)
)
: ( ( ) (
V11
()
real
ext-real
)
Element
of
REAL
: ( ( ) (
V45
()
V46
()
V47
()
V51
() )
set
) )
*
(
sinh
z
: ( (
real
) (
V11
()
real
ext-real
)
number
)
)
: ( ( ) (
V11
()
real
ext-real
)
Element
of
REAL
: ( ( ) (
V45
()
V46
()
V47
()
V51
() )
set
) )
)
: ( ( ) (
V11
()
real
ext-real
)
set
)
*
(
sinh
(
z
: ( (
real
) (
V11
()
real
ext-real
)
number
)
-
y
: ( (
real
) (
V11
()
real
ext-real
)
number
)
)
: ( ( ) (
V11
()
real
ext-real
)
set
)
)
: ( ( ) (
V11
()
real
ext-real
)
Element
of
REAL
: ( ( ) (
V45
()
V46
()
V47
()
V51
() )
set
) )
)
: ( ( ) (
V11
()
real
ext-real
)
set
)
+
(
(
(
sinh
z
: ( (
real
) (
V11
()
real
ext-real
)
number
)
)
: ( ( ) (
V11
()
real
ext-real
)
Element
of
REAL
: ( ( ) (
V45
()
V46
()
V47
()
V51
() )
set
) )
*
(
sinh
w
: ( (
real
) (
V11
()
real
ext-real
)
number
)
)
: ( ( ) (
V11
()
real
ext-real
)
Element
of
REAL
: ( ( ) (
V45
()
V46
()
V47
()
V51
() )
set
) )
)
: ( ( ) (
V11
()
real
ext-real
)
set
)
*
(
sinh
(
w
: ( (
real
) (
V11
()
real
ext-real
)
number
)
-
z
: ( (
real
) (
V11
()
real
ext-real
)
number
)
)
: ( ( ) (
V11
()
real
ext-real
)
set
)
)
: ( ( ) (
V11
()
real
ext-real
)
Element
of
REAL
: ( ( ) (
V45
()
V46
()
V47
()
V51
() )
set
) )
)
: ( ( ) (
V11
()
real
ext-real
)
set
)
)
: ( ( ) (
V11
()
real
ext-real
)
set
)
+
(
(
(
sinh
w
: ( (
real
) (
V11
()
real
ext-real
)
number
)
)
: ( ( ) (
V11
()
real
ext-real
)
Element
of
REAL
: ( ( ) (
V45
()
V46
()
V47
()
V51
() )
set
) )
*
(
sinh
y
: ( (
real
) (
V11
()
real
ext-real
)
number
)
)
: ( ( ) (
V11
()
real
ext-real
)
Element
of
REAL
: ( ( ) (
V45
()
V46
()
V47
()
V51
() )
set
) )
)
: ( ( ) (
V11
()
real
ext-real
)
set
)
*
(
sinh
(
y
: ( (
real
) (
V11
()
real
ext-real
)
number
)
-
w
: ( (
real
) (
V11
()
real
ext-real
)
number
)
)
: ( ( ) (
V11
()
real
ext-real
)
set
)
)
: ( ( ) (
V11
()
real
ext-real
)
Element
of
REAL
: ( ( ) (
V45
()
V46
()
V47
()
V51
() )
set
) )
)
: ( ( ) (
V11
()
real
ext-real
)
set
)
)
: ( ( ) (
V11
()
real
ext-real
)
set
)
+
(
(
(
sinh
(
z
: ( (
real
) (
V11
()
real
ext-real
)
number
)
-
y
: ( (
real
) (
V11
()
real
ext-real
)
number
)
)
: ( ( ) (
V11
()
real
ext-real
)
set
)
)
: ( ( ) (
V11
()
real
ext-real
)
Element
of
REAL
: ( ( ) (
V45
()
V46
()
V47
()
V51
() )
set
) )
*
(
sinh
(
w
: ( (
real
) (
V11
()
real
ext-real
)
number
)
-
z
: ( (
real
) (
V11
()
real
ext-real
)
number
)
)
: ( ( ) (
V11
()
real
ext-real
)
set
)
)
: ( ( ) (
V11
()
real
ext-real
)
Element
of
REAL
: ( ( ) (
V45
()
V46
()
V47
()
V51
() )
set
) )
)
: ( ( ) (
V11
()
real
ext-real
)
set
)
*
(
sinh
(
y
: ( (
real
) (
V11
()
real
ext-real
)
number
)
-
w
: ( (
real
) (
V11
()
real
ext-real
)
number
)
)
: ( ( ) (
V11
()
real
ext-real
)
set
)
)
: ( ( ) (
V11
()
real
ext-real
)
Element
of
REAL
: ( ( ) (
V45
()
V46
()
V47
()
V51
() )
set
) )
)
: ( ( ) (
V11
()
real
ext-real
)
set
) : ( ( ) (
V11
()
real
ext-real
)
set
)
=
0
: ( ( ) (
V1
()
ordinal
natural
V11
()
real
ext-real
non
positive
non
negative
V33
()
V34
()
V45
()
V46
()
V47
()
V48
()
V49
()
V50
()
V51
() )
Element
of
NAT
: ( ( ) (
V45
()
V46
()
V47
()
V48
()
V49
()
V50
()
V51
() )
Element
of
K6
(
REAL
: ( ( ) (
V45
()
V46
()
V47
()
V51
() )
set
) ) : ( ( ) ( )
set
) ) ) ;
theorem
:: SIN_COS8:24
for
x
being ( (
real
) (
V11
()
real
ext-real
)
number
) st
x
: ( (
real
) (
V11
()
real
ext-real
)
number
)
>=
0
: ( ( ) (
V1
()
ordinal
natural
V11
()
real
ext-real
non
positive
non
negative
V33
()
V34
()
V45
()
V46
()
V47
()
V48
()
V49
()
V50
()
V51
() )
Element
of
NAT
: ( ( ) (
V45
()
V46
()
V47
()
V48
()
V49
()
V50
()
V51
() )
Element
of
K6
(
REAL
: ( ( ) (
V45
()
V46
()
V47
()
V51
() )
set
) ) : ( ( ) ( )
set
) ) ) holds
sinh
(
x
: ( (
real
) (
V11
()
real
ext-real
)
number
)
/
2 : ( ( ) (
V1
()
ordinal
natural
V11
()
real
ext-real
positive
non
negative
V33
()
V34
()
V45
()
V46
()
V47
()
V48
()
V49
()
V50
() )
Element
of
NAT
: ( ( ) (
V45
()
V46
()
V47
()
V48
()
V49
()
V50
()
V51
() )
Element
of
K6
(
REAL
: ( ( ) (
V45
()
V46
()
V47
()
V51
() )
set
) ) : ( ( ) ( )
set
) ) )
)
: ( ( ) (
V11
()
real
ext-real
)
set
) : ( ( ) (
V11
()
real
ext-real
)
Element
of
REAL
: ( ( ) (
V45
()
V46
()
V47
()
V51
() )
set
) )
=
sqrt
(
(
(
cosh
x
: ( (
real
) (
V11
()
real
ext-real
)
number
)
)
: ( ( ) (
V11
()
real
ext-real
)
Element
of
REAL
: ( ( ) (
V45
()
V46
()
V47
()
V51
() )
set
) )
-
1 : ( ( ) (
V1
()
ordinal
natural
V11
()
real
ext-real
positive
non
negative
V33
()
V34
()
V45
()
V46
()
V47
()
V48
()
V49
()
V50
() )
Element
of
NAT
: ( ( ) (
V45
()
V46
()
V47
()
V48
()
V49
()
V50
()
V51
() )
Element
of
K6
(
REAL
: ( ( ) (
V45
()
V46
()
V47
()
V51
() )
set
) ) : ( ( ) ( )
set
) ) )
)
: ( ( ) (
V11
()
real
ext-real
)
set
)
/
2 : ( ( ) (
V1
()
ordinal
natural
V11
()
real
ext-real
positive
non
negative
V33
()
V34
()
V45
()
V46
()
V47
()
V48
()
V49
()
V50
() )
Element
of
NAT
: ( ( ) (
V45
()
V46
()
V47
()
V48
()
V49
()
V50
()
V51
() )
Element
of
K6
(
REAL
: ( ( ) (
V45
()
V46
()
V47
()
V51
() )
set
) ) : ( ( ) ( )
set
) ) )
)
: ( ( ) (
V11
()
real
ext-real
)
set
) : ( (
real
) (
V11
()
real
ext-real
)
set
) ;
theorem
:: SIN_COS8:25
for
x
being ( (
real
) (
V11
()
real
ext-real
)
number
) st
x
: ( (
real
) (
V11
()
real
ext-real
)
number
)
<
0
: ( ( ) (
V1
()
ordinal
natural
V11
()
real
ext-real
non
positive
non
negative
V33
()
V34
()
V45
()
V46
()
V47
()
V48
()
V49
()
V50
()
V51
() )
Element
of
NAT
: ( ( ) (
V45
()
V46
()
V47
()
V48
()
V49
()
V50
()
V51
() )
Element
of
K6
(
REAL
: ( ( ) (
V45
()
V46
()
V47
()
V51
() )
set
) ) : ( ( ) ( )
set
) ) ) holds
sinh
(
x
: ( (
real
) (
V11
()
real
ext-real
)
number
)
/
2 : ( ( ) (
V1
()
ordinal
natural
V11
()
real
ext-real
positive
non
negative
V33
()
V34
()
V45
()
V46
()
V47
()
V48
()
V49
()
V50
() )
Element
of
NAT
: ( ( ) (
V45
()
V46
()
V47
()
V48
()
V49
()
V50
()
V51
() )
Element
of
K6
(
REAL
: ( ( ) (
V45
()
V46
()
V47
()
V51
() )
set
) ) : ( ( ) ( )
set
) ) )
)
: ( ( ) (
V11
()
real
ext-real
)
set
) : ( ( ) (
V11
()
real
ext-real
)
Element
of
REAL
: ( ( ) (
V45
()
V46
()
V47
()
V51
() )
set
) )
=
-
(
sqrt
(
(
(
cosh
x
: ( (
real
) (
V11
()
real
ext-real
)
number
)
)
: ( ( ) (
V11
()
real
ext-real
)
Element
of
REAL
: ( ( ) (
V45
()
V46
()
V47
()
V51
() )
set
) )
-
1 : ( ( ) (
V1
()
ordinal
natural
V11
()
real
ext-real
positive
non
negative
V33
()
V34
()
V45
()
V46
()
V47
()
V48
()
V49
()
V50
() )
Element
of
NAT
: ( ( ) (
V45
()
V46
()
V47
()
V48
()
V49
()
V50
()
V51
() )
Element
of
K6
(
REAL
: ( ( ) (
V45
()
V46
()
V47
()
V51
() )
set
) ) : ( ( ) ( )
set
) ) )
)
: ( ( ) (
V11
()
real
ext-real
)
set
)
/
2 : ( ( ) (
V1
()
ordinal
natural
V11
()
real
ext-real
positive
non
negative
V33
()
V34
()
V45
()
V46
()
V47
()
V48
()
V49
()
V50
() )
Element
of
NAT
: ( ( ) (
V45
()
V46
()
V47
()
V48
()
V49
()
V50
()
V51
() )
Element
of
K6
(
REAL
: ( ( ) (
V45
()
V46
()
V47
()
V51
() )
set
) ) : ( ( ) ( )
set
) ) )
)
: ( ( ) (
V11
()
real
ext-real
)
set
)
)
: ( (
real
) (
V11
()
real
ext-real
)
set
) : ( (
V11
() ) (
V11
()
real
ext-real
)
set
) ;
theorem
:: SIN_COS8:26
for
x
being ( (
real
) (
V11
()
real
ext-real
)
number
) holds
(
sinh
(
2 : ( ( ) (
V1
()
ordinal
natural
V11
()
real
ext-real
positive
non
negative
V33
()
V34
()
V45
()
V46
()
V47
()
V48
()
V49
()
V50
() )
Element
of
NAT
: ( ( ) (
V45
()
V46
()
V47
()
V48
()
V49
()
V50
()
V51
() )
Element
of
K6
(
REAL
: ( ( ) (
V45
()
V46
()
V47
()
V51
() )
set
) ) : ( ( ) ( )
set
) ) )
*
x
: ( (
real
) (
V11
()
real
ext-real
)
number
)
)
: ( ( ) (
V11
()
real
ext-real
)
set
) : ( ( ) (
V11
()
real
ext-real
)
Element
of
REAL
: ( ( ) (
V45
()
V46
()
V47
()
V51
() )
set
) )
=
(
2 : ( ( ) (
V1
()
ordinal
natural
V11
()
real
ext-real
positive
non
negative
V33
()
V34
()
V45
()
V46
()
V47
()
V48
()
V49
()
V50
() )
Element
of
NAT
: ( ( ) (
V45
()
V46
()
V47
()
V48
()
V49
()
V50
()
V51
() )
Element
of
K6
(
REAL
: ( ( ) (
V45
()
V46
()
V47
()
V51
() )
set
) ) : ( ( ) ( )
set
) ) )
*
(
sinh
x
: ( (
real
) (
V11
()
real
ext-real
)
number
)
)
: ( ( ) (
V11
()
real
ext-real
)
Element
of
REAL
: ( ( ) (
V45
()
V46
()
V47
()
V51
() )
set
) )
)
: ( ( ) (
V11
()
real
ext-real
)
set
)
*
(
cosh
x
: ( (
real
) (
V11
()
real
ext-real
)
number
)
)
: ( ( ) (
V11
()
real
ext-real
)
Element
of
REAL
: ( ( ) (
V45
()
V46
()
V47
()
V51
() )
set
) ) : ( ( ) (
V11
()
real
ext-real
)
set
) &
cosh
(
2 : ( ( ) (
V1
()
ordinal
natural
V11
()
real
ext-real
positive
non
negative
V33
()
V34
()
V45
()
V46
()
V47
()
V48
()
V49
()
V50
() )
Element
of
NAT
: ( ( ) (
V45
()
V46
()
V47
()
V48
()
V49
()
V50
()
V51
() )
Element
of
K6
(
REAL
: ( ( ) (
V45
()
V46
()
V47
()
V51
() )
set
) ) : ( ( ) ( )
set
) ) )
*
x
: ( (
real
) (
V11
()
real
ext-real
)
number
)
)
: ( ( ) (
V11
()
real
ext-real
)
set
) : ( ( ) (
V11
()
real
ext-real
)
Element
of
REAL
: ( ( ) (
V45
()
V46
()
V47
()
V51
() )
set
) )
=
(
2 : ( ( ) (
V1
()
ordinal
natural
V11
()
real
ext-real
positive
non
negative
V33
()
V34
()
V45
()
V46
()
V47
()
V48
()
V49
()
V50
() )
Element
of
NAT
: ( ( ) (
V45
()
V46
()
V47
()
V48
()
V49
()
V50
()
V51
() )
Element
of
K6
(
REAL
: ( ( ) (
V45
()
V46
()
V47
()
V51
() )
set
) ) : ( ( ) ( )
set
) ) )
*
(
(
cosh
x
: ( (
real
) (
V11
()
real
ext-real
)
number
)
)
: ( ( ) (
V11
()
real
ext-real
)
Element
of
REAL
: ( ( ) (
V45
()
V46
()
V47
()
V51
() )
set
) )
^2
)
: ( ( ) (
V11
()
real
ext-real
)
Element
of
REAL
: ( ( ) (
V45
()
V46
()
V47
()
V51
() )
set
) )
)
: ( ( ) (
V11
()
real
ext-real
)
set
)
-
1 : ( ( ) (
V1
()
ordinal
natural
V11
()
real
ext-real
positive
non
negative
V33
()
V34
()
V45
()
V46
()
V47
()
V48
()
V49
()
V50
() )
Element
of
NAT
: ( ( ) (
V45
()
V46
()
V47
()
V48
()
V49
()
V50
()
V51
() )
Element
of
K6
(
REAL
: ( ( ) (
V45
()
V46
()
V47
()
V51
() )
set
) ) : ( ( ) ( )
set
) ) ) : ( ( ) (
V11
()
real
ext-real
)
set
) &
tanh
(
2 : ( ( ) (
V1
()
ordinal
natural
V11
()
real
ext-real
positive
non
negative
V33
()
V34
()
V45
()
V46
()
V47
()
V48
()
V49
()
V50
() )
Element
of
NAT
: ( ( ) (
V45
()
V46
()
V47
()
V48
()
V49
()
V50
()
V51
() )
Element
of
K6
(
REAL
: ( ( ) (
V45
()
V46
()
V47
()
V51
() )
set
) ) : ( ( ) ( )
set
) ) )
*
x
: ( (
real
) (
V11
()
real
ext-real
)
number
)
)
: ( ( ) (
V11
()
real
ext-real
)
set
) : ( ( ) (
V11
()
real
ext-real
)
Element
of
REAL
: ( ( ) (
V45
()
V46
()
V47
()
V51
() )
set
) )
=
(
2 : ( ( ) (
V1
()
ordinal
natural
V11
()
real
ext-real
positive
non
negative
V33
()
V34
()
V45
()
V46
()
V47
()
V48
()
V49
()
V50
() )
Element
of
NAT
: ( ( ) (
V45
()
V46
()
V47
()
V48
()
V49
()
V50
()
V51
() )
Element
of
K6
(
REAL
: ( ( ) (
V45
()
V46
()
V47
()
V51
() )
set
) ) : ( ( ) ( )
set
) ) )
*
(
tanh
x
: ( (
real
) (
V11
()
real
ext-real
)
number
)
)
: ( ( ) (
V11
()
real
ext-real
)
Element
of
REAL
: ( ( ) (
V45
()
V46
()
V47
()
V51
() )
set
) )
)
: ( ( ) (
V11
()
real
ext-real
)
set
)
/
(
1 : ( ( ) (
V1
()
ordinal
natural
V11
()
real
ext-real
positive
non
negative
V33
()
V34
()
V45
()
V46
()
V47
()
V48
()
V49
()
V50
() )
Element
of
NAT
: ( ( ) (
V45
()
V46
()
V47
()
V48
()
V49
()
V50
()
V51
() )
Element
of
K6
(
REAL
: ( ( ) (
V45
()
V46
()
V47
()
V51
() )
set
) ) : ( ( ) ( )
set
) ) )
+
(
(
tanh
x
: ( (
real
) (
V11
()
real
ext-real
)
number
)
)
: ( ( ) (
V11
()
real
ext-real
)
Element
of
REAL
: ( ( ) (
V45
()
V46
()
V47
()
V51
() )
set
) )
^2
)
: ( ( ) (
V11
()
real
ext-real
)
Element
of
REAL
: ( ( ) (
V45
()
V46
()
V47
()
V51
() )
set
) )
)
: ( ( ) (
V11
()
real
ext-real
)
set
) : ( ( ) (
V11
()
real
ext-real
)
set
) ) ;
theorem
:: SIN_COS8:27
for
x
being ( (
real
) (
V11
()
real
ext-real
)
number
) holds
(
sinh
(
2 : ( ( ) (
V1
()
ordinal
natural
V11
()
real
ext-real
positive
non
negative
V33
()
V34
()
V45
()
V46
()
V47
()
V48
()
V49
()
V50
() )
Element
of
NAT
: ( ( ) (
V45
()
V46
()
V47
()
V48
()
V49
()
V50
()
V51
() )
Element
of
K6
(
REAL
: ( ( ) (
V45
()
V46
()
V47
()
V51
() )
set
) ) : ( ( ) ( )
set
) ) )
*
x
: ( (
real
) (
V11
()
real
ext-real
)
number
)
)
: ( ( ) (
V11
()
real
ext-real
)
set
) : ( ( ) (
V11
()
real
ext-real
)
Element
of
REAL
: ( ( ) (
V45
()
V46
()
V47
()
V51
() )
set
) )
=
(
2 : ( ( ) (
V1
()
ordinal
natural
V11
()
real
ext-real
positive
non
negative
V33
()
V34
()
V45
()
V46
()
V47
()
V48
()
V49
()
V50
() )
Element
of
NAT
: ( ( ) (
V45
()
V46
()
V47
()
V48
()
V49
()
V50
()
V51
() )
Element
of
K6
(
REAL
: ( ( ) (
V45
()
V46
()
V47
()
V51
() )
set
) ) : ( ( ) ( )
set
) ) )
*
(
tanh
x
: ( (
real
) (
V11
()
real
ext-real
)
number
)
)
: ( ( ) (
V11
()
real
ext-real
)
Element
of
REAL
: ( ( ) (
V45
()
V46
()
V47
()
V51
() )
set
) )
)
: ( ( ) (
V11
()
real
ext-real
)
set
)
/
(
1 : ( ( ) (
V1
()
ordinal
natural
V11
()
real
ext-real
positive
non
negative
V33
()
V34
()
V45
()
V46
()
V47
()
V48
()
V49
()
V50
() )
Element
of
NAT
: ( ( ) (
V45
()
V46
()
V47
()
V48
()
V49
()
V50
()
V51
() )
Element
of
K6
(
REAL
: ( ( ) (
V45
()
V46
()
V47
()
V51
() )
set
) ) : ( ( ) ( )
set
) ) )
-
(
(
tanh
x
: ( (
real
) (
V11
()
real
ext-real
)
number
)
)
: ( ( ) (
V11
()
real
ext-real
)
Element
of
REAL
: ( ( ) (
V45
()
V46
()
V47
()
V51
() )
set
) )
^2
)
: ( ( ) (
V11
()
real
ext-real
)
Element
of
REAL
: ( ( ) (
V45
()
V46
()
V47
()
V51
() )
set
) )
)
: ( ( ) (
V11
()
real
ext-real
)
set
) : ( ( ) (
V11
()
real
ext-real
)
set
) &
sinh
(
3 : ( ( ) (
V1
()
ordinal
natural
V11
()
real
ext-real
positive
non
negative
V33
()
V34
()
V45
()
V46
()
V47
()
V48
()
V49
()
V50
() )
Element
of
NAT
: ( ( ) (
V45
()
V46
()
V47
()
V48
()
V49
()
V50
()
V51
() )
Element
of
K6
(
REAL
: ( ( ) (
V45
()
V46
()
V47
()
V51
() )
set
) ) : ( ( ) ( )
set
) ) )
*
x
: ( (
real
) (
V11
()
real
ext-real
)
number
)
)
: ( ( ) (
V11
()
real
ext-real
)
set
) : ( ( ) (
V11
()
real
ext-real
)
Element
of
REAL
: ( ( ) (
V45
()
V46
()
V47
()
V51
() )
set
) )
=
(
sinh
x
: ( (
real
) (
V11
()
real
ext-real
)
number
)
)
: ( ( ) (
V11
()
real
ext-real
)
Element
of
REAL
: ( ( ) (
V45
()
V46
()
V47
()
V51
() )
set
) )
*
(
(
4 : ( ( ) (
V1
()
ordinal
natural
V11
()
real
ext-real
positive
non
negative
V33
()
V34
()
V45
()
V46
()
V47
()
V48
()
V49
()
V50
() )
Element
of
NAT
: ( ( ) (
V45
()
V46
()
V47
()
V48
()
V49
()
V50
()
V51
() )
Element
of
K6
(
REAL
: ( ( ) (
V45
()
V46
()
V47
()
V51
() )
set
) ) : ( ( ) ( )
set
) ) )
*
(
(
cosh
x
: ( (
real
) (
V11
()
real
ext-real
)
number
)
)
: ( ( ) (
V11
()
real
ext-real
)
Element
of
REAL
: ( ( ) (
V45
()
V46
()
V47
()
V51
() )
set
) )
^2
)
: ( ( ) (
V11
()
real
ext-real
)
Element
of
REAL
: ( ( ) (
V45
()
V46
()
V47
()
V51
() )
set
) )
)
: ( ( ) (
V11
()
real
ext-real
)
set
)
-
1 : ( ( ) (
V1
()
ordinal
natural
V11
()
real
ext-real
positive
non
negative
V33
()
V34
()
V45
()
V46
()
V47
()
V48
()
V49
()
V50
() )
Element
of
NAT
: ( ( ) (
V45
()
V46
()
V47
()
V48
()
V49
()
V50
()
V51
() )
Element
of
K6
(
REAL
: ( ( ) (
V45
()
V46
()
V47
()
V51
() )
set
) ) : ( ( ) ( )
set
) ) )
)
: ( ( ) (
V11
()
real
ext-real
)
set
) : ( ( ) (
V11
()
real
ext-real
)
set
) &
sinh
(
3 : ( ( ) (
V1
()
ordinal
natural
V11
()
real
ext-real
positive
non
negative
V33
()
V34
()
V45
()
V46
()
V47
()
V48
()
V49
()
V50
() )
Element
of
NAT
: ( ( ) (
V45
()
V46
()
V47
()
V48
()
V49
()
V50
()
V51
() )
Element
of
K6
(
REAL
: ( ( ) (
V45
()
V46
()
V47
()
V51
() )
set
) ) : ( ( ) ( )
set
) ) )
*
x
: ( (
real
) (
V11
()
real
ext-real
)
number
)
)
: ( ( ) (
V11
()
real
ext-real
)
set
) : ( ( ) (
V11
()
real
ext-real
)
Element
of
REAL
: ( ( ) (
V45
()
V46
()
V47
()
V51
() )
set
) )
=
(
3 : ( ( ) (
V1
()
ordinal
natural
V11
()
real
ext-real
positive
non
negative
V33
()
V34
()
V45
()
V46
()
V47
()
V48
()
V49
()
V50
() )
Element
of
NAT
: ( ( ) (
V45
()
V46
()
V47
()
V48
()
V49
()
V50
()
V51
() )
Element
of
K6
(
REAL
: ( ( ) (
V45
()
V46
()
V47
()
V51
() )
set
) ) : ( ( ) ( )
set
) ) )
*
(
sinh
x
: ( (
real
) (
V11
()
real
ext-real
)
number
)
)
: ( ( ) (
V11
()
real
ext-real
)
Element
of
REAL
: ( ( ) (
V45
()
V46
()
V47
()
V51
() )
set
) )
)
: ( ( ) (
V11
()
real
ext-real
)
set
)
-
(
(
2 : ( ( ) (
V1
()
ordinal
natural
V11
()
real
ext-real
positive
non
negative
V33
()
V34
()
V45
()
V46
()
V47
()
V48
()
V49
()
V50
() )
Element
of
NAT
: ( ( ) (
V45
()
V46
()
V47
()
V48
()
V49
()
V50
()
V51
() )
Element
of
K6
(
REAL
: ( ( ) (
V45
()
V46
()
V47
()
V51
() )
set
) ) : ( ( ) ( )
set
) ) )
*
(
sinh
x
: ( (
real
) (
V11
()
real
ext-real
)
number
)
)
: ( ( ) (
V11
()
real
ext-real
)
Element
of
REAL
: ( ( ) (
V45
()
V46
()
V47
()
V51
() )
set
) )
)
: ( ( ) (
V11
()
real
ext-real
)
set
)
*
(
1 : ( ( ) (
V1
()
ordinal
natural
V11
()
real
ext-real
positive
non
negative
V33
()
V34
()
V45
()
V46
()
V47
()
V48
()
V49
()
V50
() )
Element
of
NAT
: ( ( ) (
V45
()
V46
()
V47
()
V48
()
V49
()
V50
()
V51
() )
Element
of
K6
(
REAL
: ( ( ) (
V45
()
V46
()
V47
()
V51
() )
set
) ) : ( ( ) ( )
set
) ) )
-
(
cosh
(
2 : ( ( ) (
V1
()
ordinal
natural
V11
()
real
ext-real
positive
non
negative
V33
()
V34
()
V45
()
V46
()
V47
()
V48
()
V49
()
V50
() )
Element
of
NAT
: ( ( ) (
V45
()
V46
()
V47
()
V48
()
V49
()
V50
()
V51
() )
Element
of
K6
(
REAL
: ( ( ) (
V45
()
V46
()
V47
()
V51
() )
set
) ) : ( ( ) ( )
set
) ) )
*
x
: ( (
real
) (
V11
()
real
ext-real
)
number
)
)
: ( ( ) (
V11
()
real
ext-real
)
set
)
)
: ( ( ) (
V11
()
real
ext-real
)
Element
of
REAL
: ( ( ) (
V45
()
V46
()
V47
()
V51
() )
set
) )
)
: ( ( ) (
V11
()
real
ext-real
)
set
)
)
: ( ( ) (
V11
()
real
ext-real
)
set
) : ( ( ) (
V11
()
real
ext-real
)
set
) &
cosh
(
2 : ( ( ) (
V1
()
ordinal
natural
V11
()
real
ext-real
positive
non
negative
V33
()
V34
()
V45
()
V46
()
V47
()
V48
()
V49
()
V50
() )
Element
of
NAT
: ( ( ) (
V45
()
V46
()
V47
()
V48
()
V49
()
V50
()
V51
() )
Element
of
K6
(
REAL
: ( ( ) (
V45
()
V46
()
V47
()
V51
() )
set
) ) : ( ( ) ( )
set
) ) )
*
x
: ( (
real
) (
V11
()
real
ext-real
)
number
)
)
: ( ( ) (
V11
()
real
ext-real
)
set
) : ( ( ) (
V11
()
real
ext-real
)
Element
of
REAL
: ( ( ) (
V45
()
V46
()
V47
()
V51
() )
set
) )
=
1 : ( ( ) (
V1
()
ordinal
natural
V11
()
real
ext-real
positive
non
negative
V33
()
V34
()
V45
()
V46
()
V47
()
V48
()
V49
()
V50
() )
Element
of
NAT
: ( ( ) (
V45
()
V46
()
V47
()
V48
()
V49
()
V50
()
V51
() )
Element
of
K6
(
REAL
: ( ( ) (
V45
()
V46
()
V47
()
V51
() )
set
) ) : ( ( ) ( )
set
) ) )
+
(
2 : ( ( ) (
V1
()
ordinal
natural
V11
()
real
ext-real
positive
non
negative
V33
()
V34
()
V45
()
V46
()
V47
()
V48
()
V49
()
V50
() )
Element
of
NAT
: ( ( ) (
V45
()
V46
()
V47
()
V48
()
V49
()
V50
()
V51
() )
Element
of
K6
(
REAL
: ( ( ) (
V45
()
V46
()
V47
()
V51
() )
set
) ) : ( ( ) ( )
set
) ) )
*
(
(
sinh
x
: ( (
real
) (
V11
()
real
ext-real
)
number
)
)
: ( ( ) (
V11
()
real
ext-real
)
Element
of
REAL
: ( ( ) (
V45
()
V46
()
V47
()
V51
() )
set
) )
^2
)
: ( ( ) (
V11
()
real
ext-real
)
Element
of
REAL
: ( ( ) (
V45
()
V46
()
V47
()
V51
() )
set
) )
)
: ( ( ) (
V11
()
real
ext-real
)
set
) : ( ( ) (
V11
()
real
ext-real
)
set
) &
cosh
(
2 : ( ( ) (
V1
()
ordinal
natural
V11
()
real
ext-real
positive
non
negative
V33
()
V34
()
V45
()
V46
()
V47
()
V48
()
V49
()
V50
() )
Element
of
NAT
: ( ( ) (
V45
()
V46
()
V47
()
V48
()
V49
()
V50
()
V51
() )
Element
of
K6
(
REAL
: ( ( ) (
V45
()
V46
()
V47
()
V51
() )
set
) ) : ( ( ) ( )
set
) ) )
*
x
: ( (
real
) (
V11
()
real
ext-real
)
number
)
)
: ( ( ) (
V11
()
real
ext-real
)
set
) : ( ( ) (
V11
()
real
ext-real
)
Element
of
REAL
: ( ( ) (
V45
()
V46
()
V47
()
V51
() )
set
) )
=
(
(
cosh
x
: ( (
real
) (
V11
()
real
ext-real
)
number
)
)
: ( ( ) (
V11
()
real
ext-real
)
Element
of
REAL
: ( ( ) (
V45
()
V46
()
V47
()
V51
() )
set
) )
^2
)
: ( ( ) (
V11
()
real
ext-real
)
Element
of
REAL
: ( ( ) (
V45
()
V46
()
V47
()
V51
() )
set
) )
+
(
(
sinh
x
: ( (
real
) (
V11
()
real
ext-real
)
number
)
)
: ( ( ) (
V11
()
real
ext-real
)
Element
of
REAL
: ( ( ) (
V45
()
V46
()
V47
()
V51
() )
set
) )
^2
)
: ( ( ) (
V11
()
real
ext-real
)
Element
of
REAL
: ( ( ) (
V45
()
V46
()
V47
()
V51
() )
set
) ) : ( ( ) (
V11
()
real
ext-real
)
set
) &
cosh
(
2 : ( ( ) (
V1
()
ordinal
natural
V11
()
real
ext-real
positive
non
negative
V33
()
V34
()
V45
()
V46
()
V47
()
V48
()
V49
()
V50
() )
Element
of
NAT
: ( ( ) (
V45
()
V46
()
V47
()
V48
()
V49
()
V50
()
V51
() )
Element
of
K6
(
REAL
: ( ( ) (
V45
()
V46
()
V47
()
V51
() )
set
) ) : ( ( ) ( )
set
) ) )
*
x
: ( (
real
) (
V11
()
real
ext-real
)
number
)
)
: ( ( ) (
V11
()
real
ext-real
)
set
) : ( ( ) (
V11
()
real
ext-real
)
Element
of
REAL
: ( ( ) (
V45
()
V46
()
V47
()
V51
() )
set
) )
=
(
1 : ( ( ) (
V1
()
ordinal
natural
V11
()
real
ext-real
positive
non
negative
V33
()
V34
()
V45
()
V46
()
V47
()
V48
()
V49
()
V50
() )
Element
of
NAT
: ( ( ) (
V45
()
V46
()
V47
()
V48
()
V49
()
V50
()
V51
() )
Element
of
K6
(
REAL
: ( ( ) (
V45
()
V46
()
V47
()
V51
() )
set
) ) : ( ( ) ( )
set
) ) )
+
(
(
tanh
x
: ( (
real
) (
V11
()
real
ext-real
)
number
)
)
: ( ( ) (
V11
()
real
ext-real
)
Element
of
REAL
: ( ( ) (
V45
()
V46
()
V47
()
V51
() )
set
) )
^2
)
: ( ( ) (
V11
()
real
ext-real
)
Element
of
REAL
: ( ( ) (
V45
()
V46
()
V47
()
V51
() )
set
) )
)
: ( ( ) (
V11
()
real
ext-real
)
set
)
/
(
1 : ( ( ) (
V1
()
ordinal
natural
V11
()
real
ext-real
positive
non
negative
V33
()
V34
()
V45
()
V46
()
V47
()
V48
()
V49
()
V50
() )
Element
of
NAT
: ( ( ) (
V45
()
V46
()
V47
()
V48
()
V49
()
V50
()
V51
() )
Element
of
K6
(
REAL
: ( ( ) (
V45
()
V46
()
V47
()
V51
() )
set
) ) : ( ( ) ( )
set
) ) )
-
(
(
tanh
x
: ( (
real
) (
V11
()
real
ext-real
)
number
)
)
: ( ( ) (
V11
()
real
ext-real
)
Element
of
REAL
: ( ( ) (
V45
()
V46
()
V47
()
V51
() )
set
) )
^2
)
: ( ( ) (
V11
()
real
ext-real
)
Element
of
REAL
: ( ( ) (
V45
()
V46
()
V47
()
V51
() )
set
) )
)
: ( ( ) (
V11
()
real
ext-real
)
set
) : ( ( ) (
V11
()
real
ext-real
)
set
) &
cosh
(
3 : ( ( ) (
V1
()
ordinal
natural
V11
()
real
ext-real
positive
non
negative
V33
()
V34
()
V45
()
V46
()
V47
()
V48
()
V49
()
V50
() )
Element
of
NAT
: ( ( ) (
V45
()
V46
()
V47
()
V48
()
V49
()
V50
()
V51
() )
Element
of
K6
(
REAL
: ( ( ) (
V45
()
V46
()
V47
()
V51
() )
set
) ) : ( ( ) ( )
set
) ) )
*
x
: ( (
real
) (
V11
()
real
ext-real
)
number
)
)
: ( ( ) (
V11
()
real
ext-real
)
set
) : ( ( ) (
V11
()
real
ext-real
)
Element
of
REAL
: ( ( ) (
V45
()
V46
()
V47
()
V51
() )
set
) )
=
(
cosh
x
: ( (
real
) (
V11
()
real
ext-real
)
number
)
)
: ( ( ) (
V11
()
real
ext-real
)
Element
of
REAL
: ( ( ) (
V45
()
V46
()
V47
()
V51
() )
set
) )
*
(
(
4 : ( ( ) (
V1
()
ordinal
natural
V11
()
real
ext-real
positive
non
negative
V33
()
V34
()
V45
()
V46
()
V47
()
V48
()
V49
()
V50
() )
Element
of
NAT
: ( ( ) (
V45
()
V46
()
V47
()
V48
()
V49
()
V50
()
V51
() )
Element
of
K6
(
REAL
: ( ( ) (
V45
()
V46
()
V47
()
V51
() )
set
) ) : ( ( ) ( )
set
) ) )
*
(
(
sinh
x
: ( (
real
) (
V11
()
real
ext-real
)
number
)
)
: ( ( ) (
V11
()
real
ext-real
)
Element
of
REAL
: ( ( ) (
V45
()
V46
()
V47
()
V51
() )
set
) )
^2
)
: ( ( ) (
V11
()
real
ext-real
)
Element
of
REAL
: ( ( ) (
V45
()
V46
()
V47
()
V51
() )
set
) )
)
: ( ( ) (
V11
()
real
ext-real
)
set
)
+
1 : ( ( ) (
V1
()
ordinal
natural
V11
()
real
ext-real
positive
non
negative
V33
()
V34
()
V45
()
V46
()
V47
()
V48
()
V49
()
V50
() )
Element
of
NAT
: ( ( ) (
V45
()
V46
()
V47
()
V48
()
V49
()
V50
()
V51
() )
Element
of
K6
(
REAL
: ( ( ) (
V45
()
V46
()
V47
()
V51
() )
set
) ) : ( ( ) ( )
set
) ) )
)
: ( ( ) (
V11
()
real
ext-real
)
set
) : ( ( ) (
V11
()
real
ext-real
)
set
) &
tanh
(
3 : ( ( ) (
V1
()
ordinal
natural
V11
()
real
ext-real
positive
non
negative
V33
()
V34
()
V45
()
V46
()
V47
()
V48
()
V49
()
V50
() )
Element
of
NAT
: ( ( ) (
V45
()
V46
()
V47
()
V48
()
V49
()
V50
()
V51
() )
Element
of
K6
(
REAL
: ( ( ) (
V45
()
V46
()
V47
()
V51
() )
set
) ) : ( ( ) ( )
set
) ) )
*
x
: ( (
real
) (
V11
()
real
ext-real
)
number
)
)
: ( ( ) (
V11
()
real
ext-real
)
set
) : ( ( ) (
V11
()
real
ext-real
)
Element
of
REAL
: ( ( ) (
V45
()
V46
()
V47
()
V51
() )
set
) )
=
(
(
3 : ( ( ) (
V1
()
ordinal
natural
V11
()
real
ext-real
positive
non
negative
V33
()
V34
()
V45
()
V46
()
V47
()
V48
()
V49
()
V50
() )
Element
of
NAT
: ( ( ) (
V45
()
V46
()
V47
()
V48
()
V49
()
V50
()
V51
() )
Element
of
K6
(
REAL
: ( ( ) (
V45
()
V46
()
V47
()
V51
() )
set
) ) : ( ( ) ( )
set
) ) )
*
(
tanh
x
: ( (
real
) (
V11
()
real
ext-real
)
number
)
)
: ( ( ) (
V11
()
real
ext-real
)
Element
of
REAL
: ( ( ) (
V45
()
V46
()
V47
()
V51
() )
set
) )
)
: ( ( ) (
V11
()
real
ext-real
)
set
)
+
(
(
tanh
x
: ( (
real
) (
V11
()
real
ext-real
)
number
)
)
: ( ( ) (
V11
()
real
ext-real
)
Element
of
REAL
: ( ( ) (
V45
()
V46
()
V47
()
V51
() )
set
) )
|^
3 : ( ( ) (
V1
()
ordinal
natural
V11
()
real
ext-real
positive
non
negative
V33
()
V34
()
V45
()
V46
()
V47
()
V48
()
V49
()
V50
() )
Element
of
NAT
: ( ( ) (
V45
()
V46
()
V47
()
V48
()
V49
()
V50
()
V51
() )
Element
of
K6
(
REAL
: ( ( ) (
V45
()
V46
()
V47
()
V51
() )
set
) ) : ( ( ) ( )
set
) ) )
)
: ( ( ) (
V11
()
real
ext-real
)
Element
of
REAL
: ( ( ) (
V45
()
V46
()
V47
()
V51
() )
set
) )
)
: ( ( ) (
V11
()
real
ext-real
)
set
)
/
(
1 : ( ( ) (
V1
()
ordinal
natural
V11
()
real
ext-real
positive
non
negative
V33
()
V34
()
V45
()
V46
()
V47
()
V48
()
V49
()
V50
() )
Element
of
NAT
: ( ( ) (
V45
()
V46
()
V47
()
V48
()
V49
()
V50
()
V51
() )
Element
of
K6
(
REAL
: ( ( ) (
V45
()
V46
()
V47
()
V51
() )
set
) ) : ( ( ) ( )
set
) ) )
+
(
3 : ( ( ) (
V1
()
ordinal
natural
V11
()
real
ext-real
positive
non
negative
V33
()
V34
()
V45
()
V46
()
V47
()
V48
()
V49
()
V50
() )
Element
of
NAT
: ( ( ) (
V45
()
V46
()
V47
()
V48
()
V49
()
V50
()
V51
() )
Element
of
K6
(
REAL
: ( ( ) (
V45
()
V46
()
V47
()
V51
() )
set
) ) : ( ( ) ( )
set
) ) )
*
(
(
tanh
x
: ( (
real
) (
V11
()
real
ext-real
)
number
)
)
: ( ( ) (
V11
()
real
ext-real
)
Element
of
REAL
: ( ( ) (
V45
()
V46
()
V47
()
V51
() )
set
) )
^2
)
: ( ( ) (
V11
()
real
ext-real
)
Element
of
REAL
: ( ( ) (
V45
()
V46
()
V47
()
V51
() )
set
) )
)
: ( ( ) (
V11
()
real
ext-real
)
set
)
)
: ( ( ) (
V11
()
real
ext-real
)
set
) : ( ( ) (
V11
()
real
ext-real
)
set
) ) ;
theorem
:: SIN_COS8:28
for
x
being ( (
real
) (
V11
()
real
ext-real
)
number
) holds
(
(
(
sinh
(
5 : ( ( ) (
V1
()
ordinal
natural
V11
()
real
ext-real
positive
non
negative
V33
()
V34
()
V45
()
V46
()
V47
()
V48
()
V49
()
V50
() )
Element
of
NAT
: ( ( ) (
V45
()
V46
()
V47
()
V48
()
V49
()
V50
()
V51
() )
Element
of
K6
(
REAL
: ( ( ) (
V45
()
V46
()
V47
()
V51
() )
set
) ) : ( ( ) ( )
set
) ) )
*
x
: ( (
real
) (
V11
()
real
ext-real
)
number
)
)
: ( ( ) (
V11
()
real
ext-real
)
set
)
)
: ( ( ) (
V11
()
real
ext-real
)
Element
of
REAL
: ( ( ) (
V45
()
V46
()
V47
()
V51
() )
set
) )
+
(
2 : ( ( ) (
V1
()
ordinal
natural
V11
()
real
ext-real
positive
non
negative
V33
()
V34
()
V45
()
V46
()
V47
()
V48
()
V49
()
V50
() )
Element
of
NAT
: ( ( ) (
V45
()
V46
()
V47
()
V48
()
V49
()
V50
()
V51
() )
Element
of
K6
(
REAL
: ( ( ) (
V45
()
V46
()
V47
()
V51
() )
set
) ) : ( ( ) ( )
set
) ) )
*
(
sinh
(
3 : ( ( ) (
V1
()
ordinal
natural
V11
()
real
ext-real
positive
non
negative
V33
()
V34
()
V45
()
V46
()
V47
()
V48
()
V49
()
V50
() )
Element
of
NAT
: ( ( ) (
V45
()
V46
()
V47
()
V48
()
V49
()
V50
()
V51
() )
Element
of
K6
(
REAL
: ( ( ) (
V45
()
V46
()
V47
()
V51
() )
set
) ) : ( ( ) ( )
set
) ) )
*
x
: ( (
real
) (
V11
()
real
ext-real
)
number
)
)
: ( ( ) (
V11
()
real
ext-real
)
set
)
)
: ( ( ) (
V11
()
real
ext-real
)
Element
of
REAL
: ( ( ) (
V45
()
V46
()
V47
()
V51
() )
set
) )
)
: ( ( ) (
V11
()
real
ext-real
)
set
)
)
: ( ( ) (
V11
()
real
ext-real
)
set
)
+
(
sinh
x
: ( (
real
) (
V11
()
real
ext-real
)
number
)
)
: ( ( ) (
V11
()
real
ext-real
)
Element
of
REAL
: ( ( ) (
V45
()
V46
()
V47
()
V51
() )
set
) )
)
: ( ( ) (
V11
()
real
ext-real
)
set
)
/
(
(
(
sinh
(
7 : ( ( ) (
V1
()
ordinal
natural
V11
()
real
ext-real
positive
non
negative
V33
()
V34
()
V45
()
V46
()
V47
()
V48
()
V49
()
V50
() )
Element
of
NAT
: ( ( ) (
V45
()
V46
()
V47
()
V48
()
V49
()
V50
()
V51
() )
Element
of
K6
(
REAL
: ( ( ) (
V45
()
V46
()
V47
()
V51
() )
set
) ) : ( ( ) ( )
set
) ) )
*
x
: ( (
real
) (
V11
()
real
ext-real
)
number
)
)
: ( ( ) (
V11
()
real
ext-real
)
set
)
)
: ( ( ) (
V11
()
real
ext-real
)
Element
of
REAL
: ( ( ) (
V45
()
V46
()
V47
()
V51
() )
set
) )
+
(
2 : ( ( ) (
V1
()
ordinal
natural
V11
()
real
ext-real
positive
non
negative
V33
()
V34
()
V45
()
V46
()
V47
()
V48
()
V49
()
V50
() )
Element
of
NAT
: ( ( ) (
V45
()
V46
()
V47
()
V48
()
V49
()
V50
()
V51
() )
Element
of
K6
(
REAL
: ( ( ) (
V45
()
V46
()
V47
()
V51
() )
set
) ) : ( ( ) ( )
set
) ) )
*
(
sinh
(
5 : ( ( ) (
V1
()
ordinal
natural
V11
()
real
ext-real
positive
non
negative
V33
()
V34
()
V45
()
V46
()
V47
()
V48
()
V49
()
V50
() )
Element
of
NAT
: ( ( ) (
V45
()
V46
()
V47
()
V48
()
V49
()
V50
()
V51
() )
Element
of
K6
(
REAL
: ( ( ) (
V45
()
V46
()
V47
()
V51
() )
set
) ) : ( ( ) ( )
set
) ) )
*
x
: ( (
real
) (
V11
()
real
ext-real
)
number
)
)
: ( ( ) (
V11
()
real
ext-real
)
set
)
)
: ( ( ) (
V11
()
real
ext-real
)
Element
of
REAL
: ( ( ) (
V45
()
V46
()
V47
()
V51
() )
set
) )
)
: ( ( ) (
V11
()
real
ext-real
)
set
)
)
: ( ( ) (
V11
()
real
ext-real
)
set
)
+
(
sinh
(
3 : ( ( ) (
V1
()
ordinal
natural
V11
()
real
ext-real
positive
non
negative
V33
()
V34
()
V45
()
V46
()
V47
()
V48
()
V49
()
V50
() )
Element
of
NAT
: ( ( ) (
V45
()
V46
()
V47
()
V48
()
V49
()
V50
()
V51
() )
Element
of
K6
(
REAL
: ( ( ) (
V45
()
V46
()
V47
()
V51
() )
set
) ) : ( ( ) ( )
set
) ) )
*
x
: ( (
real
) (
V11
()
real
ext-real
)
number
)
)
: ( ( ) (
V11
()
real
ext-real
)
set
)
)
: ( ( ) (
V11
()
real
ext-real
)
Element
of
REAL
: ( ( ) (
V45
()
V46
()
V47
()
V51
() )
set
) )
)
: ( ( ) (
V11
()
real
ext-real
)
set
) : ( ( ) (
V11
()
real
ext-real
)
set
)
=
(
sinh
(
3 : ( ( ) (
V1
()
ordinal
natural
V11
()
real
ext-real
positive
non
negative
V33
()
V34
()
V45
()
V46
()
V47
()
V48
()
V49
()
V50
() )
Element
of
NAT
: ( ( ) (
V45
()
V46
()
V47
()
V48
()
V49
()
V50
()
V51
() )
Element
of
K6
(
REAL
: ( ( ) (
V45
()
V46
()
V47
()
V51
() )
set
) ) : ( ( ) ( )
set
) ) )
*
x
: ( (
real
) (
V11
()
real
ext-real
)
number
)
)
: ( ( ) (
V11
()
real
ext-real
)
set
)
)
: ( ( ) (
V11
()
real
ext-real
)
Element
of
REAL
: ( ( ) (
V45
()
V46
()
V47
()
V51
() )
set
) )
/
(
sinh
(
5 : ( ( ) (
V1
()
ordinal
natural
V11
()
real
ext-real
positive
non
negative
V33
()
V34
()
V45
()
V46
()
V47
()
V48
()
V49
()
V50
() )
Element
of
NAT
: ( ( ) (
V45
()
V46
()
V47
()
V48
()
V49
()
V50
()
V51
() )
Element
of
K6
(
REAL
: ( ( ) (
V45
()
V46
()
V47
()
V51
() )
set
) ) : ( ( ) ( )
set
) ) )
*
x
: ( (
real
) (
V11
()
real
ext-real
)
number
)
)
: ( ( ) (
V11
()
real
ext-real
)
set
)
)
: ( ( ) (
V11
()
real
ext-real
)
Element
of
REAL
: ( ( ) (
V45
()
V46
()
V47
()
V51
() )
set
) ) : ( ( ) (
V11
()
real
ext-real
)
set
) ;
theorem
:: SIN_COS8:29
for
x
being ( (
real
) (
V11
()
real
ext-real
)
number
) st
x
: ( (
real
) (
V11
()
real
ext-real
)
number
)
>=
0
: ( ( ) (
V1
()
ordinal
natural
V11
()
real
ext-real
non
positive
non
negative
V33
()
V34
()
V45
()
V46
()
V47
()
V48
()
V49
()
V50
()
V51
() )
Element
of
NAT
: ( ( ) (
V45
()
V46
()
V47
()
V48
()
V49
()
V50
()
V51
() )
Element
of
K6
(
REAL
: ( ( ) (
V45
()
V46
()
V47
()
V51
() )
set
) ) : ( ( ) ( )
set
) ) ) holds
tanh
(
x
: ( (
real
) (
V11
()
real
ext-real
)
number
)
/
2 : ( ( ) (
V1
()
ordinal
natural
V11
()
real
ext-real
positive
non
negative
V33
()
V34
()
V45
()
V46
()
V47
()
V48
()
V49
()
V50
() )
Element
of
NAT
: ( ( ) (
V45
()
V46
()
V47
()
V48
()
V49
()
V50
()
V51
() )
Element
of
K6
(
REAL
: ( ( ) (
V45
()
V46
()
V47
()
V51
() )
set
) ) : ( ( ) ( )
set
) ) )
)
: ( ( ) (
V11
()
real
ext-real
)
set
) : ( ( ) (
V11
()
real
ext-real
)
Element
of
REAL
: ( ( ) (
V45
()
V46
()
V47
()
V51
() )
set
) )
=
sqrt
(
(
(
cosh
x
: ( (
real
) (
V11
()
real
ext-real
)
number
)
)
: ( ( ) (
V11
()
real
ext-real
)
Element
of
REAL
: ( ( ) (
V45
()
V46
()
V47
()
V51
() )
set
) )
-
1 : ( ( ) (
V1
()
ordinal
natural
V11
()
real
ext-real
positive
non
negative
V33
()
V34
()
V45
()
V46
()
V47
()
V48
()
V49
()
V50
() )
Element
of
NAT
: ( ( ) (
V45
()
V46
()
V47
()
V48
()
V49
()
V50
()
V51
() )
Element
of
K6
(
REAL
: ( ( ) (
V45
()
V46
()
V47
()
V51
() )
set
) ) : ( ( ) ( )
set
) ) )
)
: ( ( ) (
V11
()
real
ext-real
)
set
)
/
(
(
cosh
x
: ( (
real
) (
V11
()
real
ext-real
)
number
)
)
: ( ( ) (
V11
()
real
ext-real
)
Element
of
REAL
: ( ( ) (
V45
()
V46
()
V47
()
V51
() )
set
) )
+
1 : ( ( ) (
V1
()
ordinal
natural
V11
()
real
ext-real
positive
non
negative
V33
()
V34
()
V45
()
V46
()
V47
()
V48
()
V49
()
V50
() )
Element
of
NAT
: ( ( ) (
V45
()
V46
()
V47
()
V48
()
V49
()
V50
()
V51
() )
Element
of
K6
(
REAL
: ( ( ) (
V45
()
V46
()
V47
()
V51
() )
set
) ) : ( ( ) ( )
set
) ) )
)
: ( ( ) (
V11
()
real
ext-real
)
set
)
)
: ( ( ) (
V11
()
real
ext-real
)
set
) : ( (
real
) (
V11
()
real
ext-real
)
set
) ;
theorem
:: SIN_COS8:30
for
x
being ( (
real
) (
V11
()
real
ext-real
)
number
) st
x
: ( (
real
) (
V11
()
real
ext-real
)
number
)
<
0
: ( ( ) (
V1
()
ordinal
natural
V11
()
real
ext-real
non
positive
non
negative
V33
()
V34
()
V45
()
V46
()
V47
()
V48
()
V49
()
V50
()
V51
() )
Element
of
NAT
: ( ( ) (
V45
()
V46
()
V47
()
V48
()
V49
()
V50
()
V51
() )
Element
of
K6
(
REAL
: ( ( ) (
V45
()
V46
()
V47
()
V51
() )
set
) ) : ( ( ) ( )
set
) ) ) holds
tanh
(
x
: ( (
real
) (
V11
()
real
ext-real
)
number
)
/
2 : ( ( ) (
V1
()
ordinal
natural
V11
()
real
ext-real
positive
non
negative
V33
()
V34
()
V45
()
V46
()
V47
()
V48
()
V49
()
V50
() )
Element
of
NAT
: ( ( ) (
V45
()
V46
()
V47
()
V48
()
V49
()
V50
()
V51
() )
Element
of
K6
(
REAL
: ( ( ) (
V45
()
V46
()
V47
()
V51
() )
set
) ) : ( ( ) ( )
set
) ) )
)
: ( ( ) (
V11
()
real
ext-real
)
set
) : ( ( ) (
V11
()
real
ext-real
)
Element
of
REAL
: ( ( ) (
V45
()
V46
()
V47
()
V51
() )
set
) )
=
-
(
sqrt
(
(
(
cosh
x
: ( (
real
) (
V11
()
real
ext-real
)
number
)
)
: ( ( ) (
V11
()
real
ext-real
)
Element
of
REAL
: ( ( ) (
V45
()
V46
()
V47
()
V51
() )
set
) )
-
1 : ( ( ) (
V1
()
ordinal
natural
V11
()
real
ext-real
positive
non
negative
V33
()
V34
()
V45
()
V46
()
V47
()
V48
()
V49
()
V50
() )
Element
of
NAT
: ( ( ) (
V45
()
V46
()
V47
()
V48
()
V49
()
V50
()
V51
() )
Element
of
K6
(
REAL
: ( ( ) (
V45
()
V46
()
V47
()
V51
() )
set
) ) : ( ( ) ( )
set
) ) )
)
: ( ( ) (
V11
()
real
ext-real
)
set
)
/
(
(
cosh
x
: ( (
real
) (
V11
()
real
ext-real
)
number
)
)
: ( ( ) (
V11
()
real
ext-real
)
Element
of
REAL
: ( ( ) (
V45
()
V46
()
V47
()
V51
() )
set
) )
+
1 : ( ( ) (
V1
()
ordinal
natural
V11
()
real
ext-real
positive
non
negative
V33
()
V34
()
V45
()
V46
()
V47
()
V48
()
V49
()
V50
() )
Element
of
NAT
: ( ( ) (
V45
()
V46
()
V47
()
V48
()
V49
()
V50
()
V51
() )
Element
of
K6
(
REAL
: ( ( ) (
V45
()
V46
()
V47
()
V51
() )
set
) ) : ( ( ) ( )
set
) ) )
)
: ( ( ) (
V11
()
real
ext-real
)
set
)
)
: ( ( ) (
V11
()
real
ext-real
)
set
)
)
: ( (
real
) (
V11
()
real
ext-real
)
set
) : ( (
V11
() ) (
V11
()
real
ext-real
)
set
) ;
theorem
:: SIN_COS8:31
for
x
being ( (
real
) (
V11
()
real
ext-real
)
number
) holds
(
(
sinh
x
: ( (
real
) (
V11
()
real
ext-real
)
number
)
)
: ( ( ) (
V11
()
real
ext-real
)
Element
of
REAL
: ( ( ) (
V45
()
V46
()
V47
()
V51
() )
set
) )
|^
3 : ( ( ) (
V1
()
ordinal
natural
V11
()
real
ext-real
positive
non
negative
V33
()
V34
()
V45
()
V46
()
V47
()
V48
()
V49
()
V50
() )
Element
of
NAT
: ( ( ) (
V45
()
V46
()
V47
()
V48
()
V49
()
V50
()
V51
() )
Element
of
K6
(
REAL
: ( ( ) (
V45
()
V46
()
V47
()
V51
() )
set
) ) : ( ( ) ( )
set
) ) ) : ( ( ) (
V11
()
real
ext-real
)
Element
of
REAL
: ( ( ) (
V45
()
V46
()
V47
()
V51
() )
set
) )
=
(
(
sinh
(
3 : ( ( ) (
V1
()
ordinal
natural
V11
()
real
ext-real
positive
non
negative
V33
()
V34
()
V45
()
V46
()
V47
()
V48
()
V49
()
V50
() )
Element
of
NAT
: ( ( ) (
V45
()
V46
()
V47
()
V48
()
V49
()
V50
()
V51
() )
Element
of
K6
(
REAL
: ( ( ) (
V45
()
V46
()
V47
()
V51
() )
set
) ) : ( ( ) ( )
set
) ) )
*
x
: ( (
real
) (
V11
()
real
ext-real
)
number
)
)
: ( ( ) (
V11
()
real
ext-real
)
set
)
)
: ( ( ) (
V11
()
real
ext-real
)
Element
of
REAL
: ( ( ) (
V45
()
V46
()
V47
()
V51
() )
set
) )
-
(
3 : ( ( ) (
V1
()
ordinal
natural
V11
()
real
ext-real
positive
non
negative
V33
()
V34
()
V45
()
V46
()
V47
()
V48
()
V49
()
V50
() )
Element
of
NAT
: ( ( ) (
V45
()
V46
()
V47
()
V48
()
V49
()
V50
()
V51
() )
Element
of
K6
(
REAL
: ( ( ) (
V45
()
V46
()
V47
()
V51
() )
set
) ) : ( ( ) ( )
set
) ) )
*
(
sinh
x
: ( (
real
) (
V11
()
real
ext-real
)
number
)
)
: ( ( ) (
V11
()
real
ext-real
)
Element
of
REAL
: ( ( ) (
V45
()
V46
()
V47
()
V51
() )
set
) )
)
: ( ( ) (
V11
()
real
ext-real
)
set
)
)
: ( ( ) (
V11
()
real
ext-real
)
set
)
/
4 : ( ( ) (
V1
()
ordinal
natural
V11
()
real
ext-real
positive
non
negative
V33
()
V34
()
V45
()
V46
()
V47
()
V48
()
V49
()
V50
() )
Element
of
NAT
: ( ( ) (
V45
()
V46
()
V47
()
V48
()
V49
()
V50
()
V51
() )
Element
of
K6
(
REAL
: ( ( ) (
V45
()
V46
()
V47
()
V51
() )
set
) ) : ( ( ) ( )
set
) ) ) : ( ( ) (
V11
()
real
ext-real
)
set
) &
(
sinh
x
: ( (
real
) (
V11
()
real
ext-real
)
number
)
)
: ( ( ) (
V11
()
real
ext-real
)
Element
of
REAL
: ( ( ) (
V45
()
V46
()
V47
()
V51
() )
set
) )
|^
4 : ( ( ) (
V1
()
ordinal
natural
V11
()
real
ext-real
positive
non
negative
V33
()
V34
()
V45
()
V46
()
V47
()
V48
()
V49
()
V50
() )
Element
of
NAT
: ( ( ) (
V45
()
V46
()
V47
()
V48
()
V49
()
V50
()
V51
() )
Element
of
K6
(
REAL
: ( ( ) (
V45
()
V46
()
V47
()
V51
() )
set
) ) : ( ( ) ( )
set
) ) ) : ( ( ) (
V11
()
real
ext-real
)
Element
of
REAL
: ( ( ) (
V45
()
V46
()
V47
()
V51
() )
set
) )
=
(
(
(
cosh
(
4 : ( ( ) (
V1
()
ordinal
natural
V11
()
real
ext-real
positive
non
negative
V33
()
V34
()
V45
()
V46
()
V47
()
V48
()
V49
()
V50
() )
Element
of
NAT
: ( ( ) (
V45
()
V46
()
V47
()
V48
()
V49
()
V50
()
V51
() )
Element
of
K6
(
REAL
: ( ( ) (
V45
()
V46
()
V47
()
V51
() )
set
) ) : ( ( ) ( )
set
) ) )
*
x
: ( (
real
) (
V11
()
real
ext-real
)
number
)
)
: ( ( ) (
V11
()
real
ext-real
)
set
)
)
: ( ( ) (
V11
()
real
ext-real
)
Element
of
REAL
: ( ( ) (
V45
()
V46
()
V47
()
V51
() )
set
) )
-
(
4 : ( ( ) (
V1
()
ordinal
natural
V11
()
real
ext-real
positive
non
negative
V33
()
V34
()
V45
()
V46
()
V47
()
V48
()
V49
()
V50
() )
Element
of
NAT
: ( ( ) (
V45
()
V46
()
V47
()
V48
()
V49
()
V50
()
V51
() )
Element
of
K6
(
REAL
: ( ( ) (
V45
()
V46
()
V47
()
V51
() )
set
) ) : ( ( ) ( )
set
) ) )
*
(
cosh
(
2 : ( ( ) (
V1
()
ordinal
natural
V11
()
real
ext-real
positive
non
negative
V33
()
V34
()
V45
()
V46
()
V47
()
V48
()
V49
()
V50
() )
Element
of
NAT
: ( ( ) (
V45
()
V46
()
V47
()
V48
()
V49
()
V50
()
V51
() )
Element
of
K6
(
REAL
: ( ( ) (
V45
()
V46
()
V47
()
V51
() )
set
) ) : ( ( ) ( )
set
) ) )
*
x
: ( (
real
) (
V11
()
real
ext-real
)
number
)
)
: ( ( ) (
V11
()
real
ext-real
)
set
)
)
: ( ( ) (
V11
()
real
ext-real
)
Element
of
REAL
: ( ( ) (
V45
()
V46
()
V47
()
V51
() )
set
) )
)
: ( ( ) (
V11
()
real
ext-real
)
set
)
)
: ( ( ) (
V11
()
real
ext-real
)
set
)
+
3 : ( ( ) (
V1
()
ordinal
natural
V11
()
real
ext-real
positive
non
negative
V33
()
V34
()
V45
()
V46
()
V47
()
V48
()
V49
()
V50
() )
Element
of
NAT
: ( ( ) (
V45
()
V46
()
V47
()
V48
()
V49
()
V50
()
V51
() )
Element
of
K6
(
REAL
: ( ( ) (
V45
()
V46
()
V47
()
V51
() )
set
) ) : ( ( ) ( )
set
) ) )
)
: ( ( ) (
V11
()
real
ext-real
)
set
)
/
8 : ( ( ) (
V1
()
ordinal
natural
V11
()
real
ext-real
positive
non
negative
V33
()
V34
()
V45
()
V46
()
V47
()
V48
()
V49
()
V50
() )
Element
of
NAT
: ( ( ) (
V45
()
V46
()
V47
()
V48
()
V49
()
V50
()
V51
() )
Element
of
K6
(
REAL
: ( ( ) (
V45
()
V46
()
V47
()
V51
() )
set
) ) : ( ( ) ( )
set
) ) ) : ( ( ) (
V11
()
real
ext-real
)
set
) &
(
sinh
x
: ( (
real
) (
V11
()
real
ext-real
)
number
)
)
: ( ( ) (
V11
()
real
ext-real
)
Element
of
REAL
: ( ( ) (
V45
()
V46
()
V47
()
V51
() )
set
) )
|^
5 : ( ( ) (
V1
()
ordinal
natural
V11
()
real
ext-real
positive
non
negative
V33
()
V34
()
V45
()
V46
()
V47
()
V48
()
V49
()
V50
() )
Element
of
NAT
: ( ( ) (
V45
()
V46
()
V47
()
V48
()
V49
()
V50
()
V51
() )
Element
of
K6
(
REAL
: ( ( ) (
V45
()
V46
()
V47
()
V51
() )
set
) ) : ( ( ) ( )
set
) ) ) : ( ( ) (
V11
()
real
ext-real
)
Element
of
REAL
: ( ( ) (
V45
()
V46
()
V47
()
V51
() )
set
) )
=
(
(
(
sinh
(
5 : ( ( ) (
V1
()
ordinal
natural
V11
()
real
ext-real
positive
non
negative
V33
()
V34
()
V45
()
V46
()
V47
()
V48
()
V49
()
V50
() )
Element
of
NAT
: ( ( ) (
V45
()
V46
()
V47
()
V48
()
V49
()
V50
()
V51
() )
Element
of
K6
(
REAL
: ( ( ) (
V45
()
V46
()
V47
()
V51
() )
set
) ) : ( ( ) ( )
set
) ) )
*
x
: ( (
real
) (
V11
()
real
ext-real
)
number
)
)
: ( ( ) (
V11
()
real
ext-real
)
set
)
)
: ( ( ) (
V11
()
real
ext-real
)
Element
of
REAL
: ( ( ) (
V45
()
V46
()
V47
()
V51
() )
set
) )
-
(
5 : ( ( ) (
V1
()
ordinal
natural
V11
()
real
ext-real
positive
non
negative
V33
()
V34
()
V45
()
V46
()
V47
()
V48
()
V49
()
V50
() )
Element
of
NAT
: ( ( ) (
V45
()
V46
()
V47
()
V48
()
V49
()
V50
()
V51
() )
Element
of
K6
(
REAL
: ( ( ) (
V45
()
V46
()
V47
()
V51
() )
set
) ) : ( ( ) ( )
set
) ) )
*
(
sinh
(
3 : ( ( ) (
V1
()
ordinal
natural
V11
()
real
ext-real
positive
non
negative
V33
()
V34
()
V45
()
V46
()
V47
()
V48
()
V49
()
V50
() )
Element
of
NAT
: ( ( ) (
V45
()
V46
()
V47
()
V48
()
V49
()
V50
()
V51
() )
Element
of
K6
(
REAL
: ( ( ) (
V45
()
V46
()
V47
()
V51
() )
set
) ) : ( ( ) ( )
set
) ) )
*
x
: ( (
real
) (
V11
()
real
ext-real
)
number
)
)
: ( ( ) (
V11
()
real
ext-real
)
set
)
)
: ( ( ) (
V11
()
real
ext-real
)
Element
of
REAL
: ( ( ) (
V45
()
V46
()
V47
()
V51
() )
set
) )
)
: ( ( ) (
V11
()
real
ext-real
)
set
)
)
: ( ( ) (
V11
()
real
ext-real
)
set
)
+
(
10 : ( ( ) (
V1
()
ordinal
natural
V11
()
real
ext-real
positive
non
negative
V33
()
V34
()
V45
()
V46
()
V47
()
V48
()
V49
()
V50
() )
Element
of
NAT
: ( ( ) (
V45
()
V46
()
V47
()
V48
()
V49
()
V50
()
V51
() )
Element
of
K6
(
REAL
: ( ( ) (
V45
()
V46
()
V47
()
V51
() )
set
) ) : ( ( ) ( )
set
) ) )
*
(
sinh
x
: ( (
real
) (
V11
()
real
ext-real
)
number
)
)
: ( ( ) (
V11
()
real
ext-real
)
Element
of
REAL
: ( ( ) (
V45
()
V46
()
V47
()
V51
() )
set
) )
)
: ( ( ) (
V11
()
real
ext-real
)
set
)
)
: ( ( ) (
V11
()
real
ext-real
)
set
)
/
16 : ( ( ) (
V1
()
ordinal
natural
V11
()
real
ext-real
positive
non
negative
V33
()
V34
()
V45
()
V46
()
V47
()
V48
()
V49
()
V50
() )
Element
of
NAT
: ( ( ) (
V45
()
V46
()
V47
()
V48
()
V49
()
V50
()
V51
() )
Element
of
K6
(
REAL
: ( ( ) (
V45
()
V46
()
V47
()
V51
() )
set
) ) : ( ( ) ( )
set
) ) ) : ( ( ) (
V11
()
real
ext-real
)
set
) &
(
sinh
x
: ( (
real
) (
V11
()
real
ext-real
)
number
)
)
: ( ( ) (
V11
()
real
ext-real
)
Element
of
REAL
: ( ( ) (
V45
()
V46
()
V47
()
V51
() )
set
) )
|^
6 : ( ( ) (
V1
()
ordinal
natural
V11
()
real
ext-real
positive
non
negative
V33
()
V34
()
V45
()
V46
()
V47
()
V48
()
V49
()
V50
() )
Element
of
NAT
: ( ( ) (
V45
()
V46
()
V47
()
V48
()
V49
()
V50
()
V51
() )
Element
of
K6
(
REAL
: ( ( ) (
V45
()
V46
()
V47
()
V51
() )
set
) ) : ( ( ) ( )
set
) ) ) : ( ( ) (
V11
()
real
ext-real
)
Element
of
REAL
: ( ( ) (
V45
()
V46
()
V47
()
V51
() )
set
) )
=
(
(
(
(
cosh
(
6 : ( ( ) (
V1
()
ordinal
natural
V11
()
real
ext-real
positive
non
negative
V33
()
V34
()
V45
()
V46
()
V47
()
V48
()
V49
()
V50
() )
Element
of
NAT
: ( ( ) (
V45
()
V46
()
V47
()
V48
()
V49
()
V50
()
V51
() )
Element
of
K6
(
REAL
: ( ( ) (
V45
()
V46
()
V47
()
V51
() )
set
) ) : ( ( ) ( )
set
) ) )
*
x
: ( (
real
) (
V11
()
real
ext-real
)
number
)
)
: ( ( ) (
V11
()
real
ext-real
)
set
)
)
: ( ( ) (
V11
()
real
ext-real
)
Element
of
REAL
: ( ( ) (
V45
()
V46
()
V47
()
V51
() )
set
) )
-
(
6 : ( ( ) (
V1
()
ordinal
natural
V11
()
real
ext-real
positive
non
negative
V33
()
V34
()
V45
()
V46
()
V47
()
V48
()
V49
()
V50
() )
Element
of
NAT
: ( ( ) (
V45
()
V46
()
V47
()
V48
()
V49
()
V50
()
V51
() )
Element
of
K6
(
REAL
: ( ( ) (
V45
()
V46
()
V47
()
V51
() )
set
) ) : ( ( ) ( )
set
) ) )
*
(
cosh
(
4 : ( ( ) (
V1
()
ordinal
natural
V11
()
real
ext-real
positive
non
negative
V33
()
V34
()
V45
()
V46
()
V47
()
V48
()
V49
()
V50
() )
Element
of
NAT
: ( ( ) (
V45
()
V46
()
V47
()
V48
()
V49
()
V50
()
V51
() )
Element
of
K6
(
REAL
: ( ( ) (
V45
()
V46
()
V47
()
V51
() )
set
) ) : ( ( ) ( )
set
) ) )
*
x
: ( (
real
) (
V11
()
real
ext-real
)
number
)
)
: ( ( ) (
V11
()
real
ext-real
)
set
)
)
: ( ( ) (
V11
()
real
ext-real
)
Element
of
REAL
: ( ( ) (
V45
()
V46
()
V47
()
V51
() )
set
) )
)
: ( ( ) (
V11
()
real
ext-real
)
set
)
)
: ( ( ) (
V11
()
real
ext-real
)
set
)
+
(
15 : ( ( ) (
V1
()
ordinal
natural
V11
()
real
ext-real
positive
non
negative
V33
()
V34
()
V45
()
V46
()
V47
()
V48
()
V49
()
V50
() )
Element
of
NAT
: ( ( ) (
V45
()
V46
()
V47
()
V48
()
V49
()
V50
()
V51
() )
Element
of
K6
(
REAL
: ( ( ) (
V45
()
V46
()
V47
()
V51
() )
set
) ) : ( ( ) ( )
set
) ) )
*
(
cosh
(
2 : ( ( ) (
V1
()
ordinal
natural
V11
()
real
ext-real
positive
non
negative
V33
()
V34
()
V45
()
V46
()
V47
()
V48
()
V49
()
V50
() )
Element
of
NAT
: ( ( ) (
V45
()
V46
()
V47
()
V48
()
V49
()
V50
()
V51
() )
Element
of
K6
(
REAL
: ( ( ) (
V45
()
V46
()
V47
()
V51
() )
set
) ) : ( ( ) ( )
set
) ) )
*
x
: ( (
real
) (
V11
()
real
ext-real
)
number
)
)
: ( ( ) (
V11
()
real
ext-real
)
set
)
)
: ( ( ) (
V11
()
real
ext-real
)
Element
of
REAL
: ( ( ) (
V45
()
V46
()
V47
()
V51
() )
set
) )
)
: ( ( ) (
V11
()
real
ext-real
)
set
)
)
: ( ( ) (
V11
()
real
ext-real
)
set
)
-
10 : ( ( ) (
V1
()
ordinal
natural
V11
()
real
ext-real
positive
non
negative
V33
()
V34
()
V45
()
V46
()
V47
()
V48
()
V49
()
V50
() )
Element
of
NAT
: ( ( ) (
V45
()
V46
()
V47
()
V48
()
V49
()
V50
()
V51
() )
Element
of
K6
(
REAL
: ( ( ) (
V45
()
V46
()
V47
()
V51
() )
set
) ) : ( ( ) ( )
set
) ) )
)
: ( ( ) (
V11
()
real
ext-real
)
set
)
/
32 : ( ( ) (
V1
()
ordinal
natural
V11
()
real
ext-real
positive
non
negative
V33
()
V34
()
V45
()
V46
()
V47
()
V48
()
V49
()
V50
() )
Element
of
NAT
: ( ( ) (
V45
()
V46
()
V47
()
V48
()
V49
()
V50
()
V51
() )
Element
of
K6
(
REAL
: ( ( ) (
V45
()
V46
()
V47
()
V51
() )
set
) ) : ( ( ) ( )
set
) ) ) : ( ( ) (
V11
()
real
ext-real
)
set
) &
(
sinh
x
: ( (
real
) (
V11
()
real
ext-real
)
number
)
)
: ( ( ) (
V11
()
real
ext-real
)
Element
of
REAL
: ( ( ) (
V45
()
V46
()
V47
()
V51
() )
set
) )
|^
7 : ( ( ) (
V1
()
ordinal
natural
V11
()
real
ext-real
positive
non
negative
V33
()
V34
()
V45
()
V46
()
V47
()
V48
()
V49
()
V50
() )
Element
of
NAT
: ( ( ) (
V45
()
V46
()
V47
()
V48
()
V49
()
V50
()
V51
() )
Element
of
K6
(
REAL
: ( ( ) (
V45
()
V46
()
V47
()
V51
() )
set
) ) : ( ( ) ( )
set
) ) ) : ( ( ) (
V11
()
real
ext-real
)
Element
of
REAL
: ( ( ) (
V45
()
V46
()
V47
()
V51
() )
set
) )
=
(
(
(
(
sinh
(
7 : ( ( ) (
V1
()
ordinal
natural
V11
()
real
ext-real
positive
non
negative
V33
()
V34
()
V45
()
V46
()
V47
()
V48
()
V49
()
V50
() )
Element
of
NAT
: ( ( ) (
V45
()
V46
()
V47
()
V48
()
V49
()
V50
()
V51
() )
Element
of
K6
(
REAL
: ( ( ) (
V45
()
V46
()
V47
()
V51
() )
set
) ) : ( ( ) ( )
set
) ) )
*
x
: ( (
real
) (
V11
()
real
ext-real
)
number
)
)
: ( ( ) (
V11
()
real
ext-real
)
set
)
)
: ( ( ) (
V11
()
real
ext-real
)
Element
of
REAL
: ( ( ) (
V45
()
V46
()
V47
()
V51
() )
set
) )
-
(
7 : ( ( ) (
V1
()
ordinal
natural
V11
()
real
ext-real
positive
non
negative
V33
()
V34
()
V45
()
V46
()
V47
()
V48
()
V49
()
V50
() )
Element
of
NAT
: ( ( ) (
V45
()
V46
()
V47
()
V48
()
V49
()
V50
()
V51
() )
Element
of
K6
(
REAL
: ( ( ) (
V45
()
V46
()
V47
()
V51
() )
set
) ) : ( ( ) ( )
set
) ) )
*
(
sinh
(
5 : ( ( ) (
V1
()
ordinal
natural
V11
()
real
ext-real
positive
non
negative
V33
()
V34
()
V45
()
V46
()
V47
()
V48
()
V49
()
V50
() )
Element
of
NAT
: ( ( ) (
V45
()
V46
()
V47
()
V48
()
V49
()
V50
()
V51
() )
Element
of
K6
(
REAL
: ( ( ) (
V45
()
V46
()
V47
()
V51
() )
set
) ) : ( ( ) ( )
set
) ) )
*
x
: ( (
real
) (
V11
()
real
ext-real
)
number
)
)
: ( ( ) (
V11
()
real
ext-real
)
set
)
)
: ( ( ) (
V11
()
real
ext-real
)
Element
of
REAL
: ( ( ) (
V45
()
V46
()
V47
()
V51
() )
set
) )
)
: ( ( ) (
V11
()
real
ext-real
)
set
)
)
: ( ( ) (
V11
()
real
ext-real
)
set
)
+
(
21 : ( ( ) (
V1
()
ordinal
natural
V11
()
real
ext-real
positive
non
negative
V33
()
V34
()
V45
()
V46
()
V47
()
V48
()
V49
()
V50
() )
Element
of
NAT
: ( ( ) (
V45
()
V46
()
V47
()
V48
()
V49
()
V50
()
V51
() )
Element
of
K6
(
REAL
: ( ( ) (
V45
()
V46
()
V47
()
V51
() )
set
) ) : ( ( ) ( )
set
) ) )
*
(
sinh
(
3 : ( ( ) (
V1
()
ordinal
natural
V11
()
real
ext-real
positive
non
negative
V33
()
V34
()
V45
()
V46
()
V47
()
V48
()
V49
()
V50
() )
Element
of
NAT
: ( ( ) (
V45
()
V46
()
V47
()
V48
()
V49
()
V50
()
V51
() )
Element
of
K6
(
REAL
: ( ( ) (
V45
()
V46
()
V47
()
V51
() )
set
) ) : ( ( ) ( )
set
) ) )
*
x
: ( (
real
) (
V11
()
real
ext-real
)
number
)
)
: ( ( ) (
V11
()
real
ext-real
)
set
)
)
: ( ( ) (
V11
()
real
ext-real
)
Element
of
REAL
: ( ( ) (
V45
()
V46
()
V47
()
V51
() )
set
) )
)
: ( ( ) (
V11
()
real
ext-real
)
set
)
)
: ( ( ) (
V11
()
real
ext-real
)
set
)
-
(
35 : ( ( ) (
V1
()
ordinal
natural
V11
()
real
ext-real
positive
non
negative
V33
()
V34
()
V45
()
V46
()
V47
()
V48
()
V49
()
V50
() )
Element
of
NAT
: ( ( ) (
V45
()
V46
()
V47
()
V48
()
V49
()
V50
()
V51
() )
Element
of
K6
(
REAL
: ( ( ) (
V45
()
V46
()
V47
()
V51
() )
set
) ) : ( ( ) ( )
set
) ) )
*
(
sinh
x
: ( (
real
) (
V11
()
real
ext-real
)
number
)
)
: ( ( ) (
V11
()
real
ext-real
)
Element
of
REAL
: ( ( ) (
V45
()
V46
()
V47
()
V51
() )
set
) )
)
: ( ( ) (
V11
()
real
ext-real
)
set
)
)
: ( ( ) (
V11
()
real
ext-real
)
set
)
/
64 : ( ( ) (
V1
()
ordinal
natural
V11
()
real
ext-real
positive
non
negative
V33
()
V34
()
V45
()
V46
()
V47
()
V48
()
V49
()
V50
() )
Element
of
NAT
: ( ( ) (
V45
()
V46
()
V47
()
V48
()
V49
()
V50
()
V51
() )
Element
of
K6
(
REAL
: ( ( ) (
V45
()
V46
()
V47
()
V51
() )
set
) ) : ( ( ) ( )
set
) ) ) : ( ( ) (
V11
()
real
ext-real
)
set
) &
(
sinh
x
: ( (
real
) (
V11
()
real
ext-real
)
number
)
)
: ( ( ) (
V11
()
real
ext-real
)
Element
of
REAL
: ( ( ) (
V45
()
V46
()
V47
()
V51
() )
set
) )
|^
8 : ( ( ) (
V1
()
ordinal
natural
V11
()
real
ext-real
positive
non
negative
V33
()
V34
()
V45
()
V46
()
V47
()
V48
()
V49
()
V50
() )
Element
of
NAT
: ( ( ) (
V45
()
V46
()
V47
()
V48
()
V49
()
V50
()
V51
() )
Element
of
K6
(
REAL
: ( ( ) (
V45
()
V46
()
V47
()
V51
() )
set
) ) : ( ( ) ( )
set
) ) ) : ( ( ) (
V11
()
real
ext-real
)
Element
of
REAL
: ( ( ) (
V45
()
V46
()
V47
()
V51
() )
set
) )
=
(
(
(
(
(
cosh
(
8 : ( ( ) (
V1
()
ordinal
natural
V11
()
real
ext-real
positive
non
negative
V33
()
V34
()
V45
()
V46
()
V47
()
V48
()
V49
()
V50
() )
Element
of
NAT
: ( ( ) (
V45
()
V46
()
V47
()
V48
()
V49
()
V50
()
V51
() )
Element
of
K6
(
REAL
: ( ( ) (
V45
()
V46
()
V47
()
V51
() )
set
) ) : ( ( ) ( )
set
) ) )
*
x
: ( (
real
) (
V11
()
real
ext-real
)
number
)
)
: ( ( ) (
V11
()
real
ext-real
)
set
)
)
: ( ( ) (
V11
()
real
ext-real
)
Element
of
REAL
: ( ( ) (
V45
()
V46
()
V47
()
V51
() )
set
) )
-
(
8 : ( ( ) (
V1
()
ordinal
natural
V11
()
real
ext-real
positive
non
negative
V33
()
V34
()
V45
()
V46
()
V47
()
V48
()
V49
()
V50
() )
Element
of
NAT
: ( ( ) (
V45
()
V46
()
V47
()
V48
()
V49
()
V50
()
V51
() )
Element
of
K6
(
REAL
: ( ( ) (
V45
()
V46
()
V47
()
V51
() )
set
) ) : ( ( ) ( )
set
) ) )
*
(
cosh
(
6 : ( ( ) (
V1
()
ordinal
natural
V11
()
real
ext-real
positive
non
negative
V33
()
V34
()
V45
()
V46
()
V47
()
V48
()
V49
()
V50
() )
Element
of
NAT
: ( ( ) (
V45
()
V46
()
V47
()
V48
()
V49
()
V50
()
V51
() )
Element
of
K6
(
REAL
: ( ( ) (
V45
()
V46
()
V47
()
V51
() )
set
) ) : ( ( ) ( )
set
) ) )
*
x
: ( (
real
) (
V11
()
real
ext-real
)
number
)
)
: ( ( ) (
V11
()
real
ext-real
)
set
)
)
: ( ( ) (
V11
()
real
ext-real
)
Element
of
REAL
: ( ( ) (
V45
()
V46
()
V47
()
V51
() )
set
) )
)
: ( ( ) (
V11
()
real
ext-real
)
set
)
)
: ( ( ) (
V11
()
real
ext-real
)
set
)
+
(
28 : ( ( ) (
V1
()
ordinal
natural
V11
()
real
ext-real
positive
non
negative
V33
()
V34
()
V45
()
V46
()
V47
()
V48
()
V49
()
V50
() )
Element
of
NAT
: ( ( ) (
V45
()
V46
()
V47
()
V48
()
V49
()
V50
()
V51
() )
Element
of
K6
(
REAL
: ( ( ) (
V45
()
V46
()
V47
()
V51
() )
set
) ) : ( ( ) ( )
set
) ) )
*
(
cosh
(
4 : ( ( ) (
V1
()
ordinal
natural
V11
()
real
ext-real
positive
non
negative
V33
()
V34
()
V45
()
V46
()
V47
()
V48
()
V49
()
V50
() )
Element
of
NAT
: ( ( ) (
V45
()
V46
()
V47
()
V48
()
V49
()
V50
()
V51
() )
Element
of
K6
(
REAL
: ( ( ) (
V45
()
V46
()
V47
()
V51
() )
set
) ) : ( ( ) ( )
set
) ) )
*
x
: ( (
real
) (
V11
()
real
ext-real
)
number
)
)
: ( ( ) (
V11
()
real
ext-real
)
set
)
)
: ( ( ) (
V11
()
real
ext-real
)
Element
of
REAL
: ( ( ) (
V45
()
V46
()
V47
()
V51
() )
set
) )
)
: ( ( ) (
V11
()
real
ext-real
)
set
)
)
: ( ( ) (
V11
()
real
ext-real
)
set
)
-
(
56 : ( ( ) (
V1
()
ordinal
natural
V11
()
real
ext-real
positive
non
negative
V33
()
V34
()
V45
()
V46
()
V47
()
V48
()
V49
()
V50
() )
Element
of
NAT
: ( ( ) (
V45
()
V46
()
V47
()
V48
()
V49
()
V50
()
V51
() )
Element
of
K6
(
REAL
: ( ( ) (
V45
()
V46
()
V47
()
V51
() )
set
) ) : ( ( ) ( )
set
) ) )
*
(
cosh
(
2 : ( ( ) (
V1
()
ordinal
natural
V11
()
real
ext-real
positive
non
negative
V33
()
V34
()
V45
()
V46
()
V47
()
V48
()
V49
()
V50
() )
Element
of
NAT
: ( ( ) (
V45
()
V46
()
V47
()
V48
()
V49
()
V50
()
V51
() )
Element
of
K6
(
REAL
: ( ( ) (
V45
()
V46
()
V47
()
V51
() )
set
) ) : ( ( ) ( )
set
) ) )
*
x
: ( (
real
) (
V11
()
real
ext-real
)
number
)
)
: ( ( ) (
V11
()
real
ext-real
)
set
)
)
: ( ( ) (
V11
()
real
ext-real
)
Element
of
REAL
: ( ( ) (
V45
()
V46
()
V47
()
V51
() )
set
) )
)
: ( ( ) (
V11
()
real
ext-real
)
set
)
)
: ( ( ) (
V11
()
real
ext-real
)
set
)
+
35 : ( ( ) (
V1
()
ordinal
natural
V11
()
real
ext-real
positive
non
negative
V33
()
V34
()
V45
()
V46
()
V47
()
V48
()
V49
()
V50
() )
Element
of
NAT
: ( ( ) (
V45
()
V46
()
V47
()
V48
()
V49
()
V50
()
V51
() )
Element
of
K6
(
REAL
: ( ( ) (
V45
()
V46
()
V47
()
V51
() )
set
) ) : ( ( ) ( )
set
) ) )
)
: ( ( ) (
V11
()
real
ext-real
)
set
)
/
128 : ( ( ) (
V1
()
ordinal
natural
V11
()
real
ext-real
positive
non
negative
V33
()
V34
()
V45
()
V46
()
V47
()
V48
()
V49
()
V50
() )
Element
of
NAT
: ( ( ) (
V45
()
V46
()
V47
()
V48
()
V49
()
V50
()
V51
() )
Element
of
K6
(
REAL
: ( ( ) (
V45
()
V46
()
V47
()
V51
() )
set
) ) : ( ( ) ( )
set
) ) ) : ( ( ) (
V11
()
real
ext-real
)
set
) ) ;
theorem
:: SIN_COS8:32
for
x
being ( (
real
) (
V11
()
real
ext-real
)
number
) holds
(
(
cosh
x
: ( (
real
) (
V11
()
real
ext-real
)
number
)
)
: ( ( ) (
V11
()
real
ext-real
)
Element
of
REAL
: ( ( ) (
V45
()
V46
()
V47
()
V51
() )
set
) )
|^
3 : ( ( ) (
V1
()
ordinal
natural
V11
()
real
ext-real
positive
non
negative
V33
()
V34
()
V45
()
V46
()
V47
()
V48
()
V49
()
V50
() )
Element
of
NAT
: ( ( ) (
V45
()
V46
()
V47
()
V48
()
V49
()
V50
()
V51
() )
Element
of
K6
(
REAL
: ( ( ) (
V45
()
V46
()
V47
()
V51
() )
set
) ) : ( ( ) ( )
set
) ) ) : ( ( ) (
V11
()
real
ext-real
)
Element
of
REAL
: ( ( ) (
V45
()
V46
()
V47
()
V51
() )
set
) )
=
(
(
cosh
(
3 : ( ( ) (
V1
()
ordinal
natural
V11
()
real
ext-real
positive
non
negative
V33
()
V34
()
V45
()
V46
()
V47
()
V48
()
V49
()
V50
() )
Element
of
NAT
: ( ( ) (
V45
()
V46
()
V47
()
V48
()
V49
()
V50
()
V51
() )
Element
of
K6
(
REAL
: ( ( ) (
V45
()
V46
()
V47
()
V51
() )
set
) ) : ( ( ) ( )
set
) ) )
*
x
: ( (
real
) (
V11
()
real
ext-real
)
number
)
)
: ( ( ) (
V11
()
real
ext-real
)
set
)
)
: ( ( ) (
V11
()
real
ext-real
)
Element
of
REAL
: ( ( ) (
V45
()
V46
()
V47
()
V51
() )
set
) )
+
(
3 : ( ( ) (
V1
()
ordinal
natural
V11
()
real
ext-real
positive
non
negative
V33
()
V34
()
V45
()
V46
()
V47
()
V48
()
V49
()
V50
() )
Element
of
NAT
: ( ( ) (
V45
()
V46
()
V47
()
V48
()
V49
()
V50
()
V51
() )
Element
of
K6
(
REAL
: ( ( ) (
V45
()
V46
()
V47
()
V51
() )
set
) ) : ( ( ) ( )
set
) ) )
*
(
cosh
x
: ( (
real
) (
V11
()
real
ext-real
)
number
)
)
: ( ( ) (
V11
()
real
ext-real
)
Element
of
REAL
: ( ( ) (
V45
()
V46
()
V47
()
V51
() )
set
) )
)
: ( ( ) (
V11
()
real
ext-real
)
set
)
)
: ( ( ) (
V11
()
real
ext-real
)
set
)
/
4 : ( ( ) (
V1
()
ordinal
natural
V11
()
real
ext-real
positive
non
negative
V33
()
V34
()
V45
()
V46
()
V47
()
V48
()
V49
()
V50
() )
Element
of
NAT
: ( ( ) (
V45
()
V46
()
V47
()
V48
()
V49
()
V50
()
V51
() )
Element
of
K6
(
REAL
: ( ( ) (
V45
()
V46
()
V47
()
V51
() )
set
) ) : ( ( ) ( )
set
) ) ) : ( ( ) (
V11
()
real
ext-real
)
set
) &
(
cosh
x
: ( (
real
) (
V11
()
real
ext-real
)
number
)
)
: ( ( ) (
V11
()
real
ext-real
)
Element
of
REAL
: ( ( ) (
V45
()
V46
()
V47
()
V51
() )
set
) )
|^
4 : ( ( ) (
V1
()
ordinal
natural
V11
()
real
ext-real
positive
non
negative
V33
()
V34
()
V45
()
V46
()
V47
()
V48
()
V49
()
V50
() )
Element
of
NAT
: ( ( ) (
V45
()
V46
()
V47
()
V48
()
V49
()
V50
()
V51
() )
Element
of
K6
(
REAL
: ( ( ) (
V45
()
V46
()
V47
()
V51
() )
set
) ) : ( ( ) ( )
set
) ) ) : ( ( ) (
V11
()
real
ext-real
)
Element
of
REAL
: ( ( ) (
V45
()
V46
()
V47
()
V51
() )
set
) )
=
(
(
(
cosh
(
4 : ( ( ) (
V1
()
ordinal
natural
V11
()
real
ext-real
positive
non
negative
V33
()
V34
()
V45
()
V46
()
V47
()
V48
()
V49
()
V50
() )
Element
of
NAT
: ( ( ) (
V45
()
V46
()
V47
()
V48
()
V49
()
V50
()
V51
() )
Element
of
K6
(
REAL
: ( ( ) (
V45
()
V46
()
V47
()
V51
() )
set
) ) : ( ( ) ( )
set
) ) )
*
x
: ( (
real
) (
V11
()
real
ext-real
)
number
)
)
: ( ( ) (
V11
()
real
ext-real
)
set
)
)
: ( ( ) (
V11
()
real
ext-real
)
Element
of
REAL
: ( ( ) (
V45
()
V46
()
V47
()
V51
() )
set
) )
+
(
4 : ( ( ) (
V1
()
ordinal
natural
V11
()
real
ext-real
positive
non
negative
V33
()
V34
()
V45
()
V46
()
V47
()
V48
()
V49
()
V50
() )
Element
of
NAT
: ( ( ) (
V45
()
V46
()
V47
()
V48
()
V49
()
V50
()
V51
() )
Element
of
K6
(
REAL
: ( ( ) (
V45
()
V46
()
V47
()
V51
() )
set
) ) : ( ( ) ( )
set
) ) )
*
(
cosh
(
2 : ( ( ) (
V1
()
ordinal
natural
V11
()
real
ext-real
positive
non
negative
V33
()
V34
()
V45
()
V46
()
V47
()
V48
()
V49
()
V50
() )
Element
of
NAT
: ( ( ) (
V45
()
V46
()
V47
()
V48
()
V49
()
V50
()
V51
() )
Element
of
K6
(
REAL
: ( ( ) (
V45
()
V46
()
V47
()
V51
() )
set
) ) : ( ( ) ( )
set
) ) )
*
x
: ( (
real
) (
V11
()
real
ext-real
)
number
)
)
: ( ( ) (
V11
()
real
ext-real
)
set
)
)
: ( ( ) (
V11
()
real
ext-real
)
Element
of
REAL
: ( ( ) (
V45
()
V46
()
V47
()
V51
() )
set
) )
)
: ( ( ) (
V11
()
real
ext-real
)
set
)
)
: ( ( ) (
V11
()
real
ext-real
)
set
)
+
3 : ( ( ) (
V1
()
ordinal
natural
V11
()
real
ext-real
positive
non
negative
V33
()
V34
()
V45
()
V46
()
V47
()
V48
()
V49
()
V50
() )
Element
of
NAT
: ( ( ) (
V45
()
V46
()
V47
()
V48
()
V49
()
V50
()
V51
() )
Element
of
K6
(
REAL
: ( ( ) (
V45
()
V46
()
V47
()
V51
() )
set
) ) : ( ( ) ( )
set
) ) )
)
: ( ( ) (
V11
()
real
ext-real
)
set
)
/
8 : ( ( ) (
V1
()
ordinal
natural
V11
()
real
ext-real
positive
non
negative
V33
()
V34
()
V45
()
V46
()
V47
()
V48
()
V49
()
V50
() )
Element
of
NAT
: ( ( ) (
V45
()
V46
()
V47
()
V48
()
V49
()
V50
()
V51
() )
Element
of
K6
(
REAL
: ( ( ) (
V45
()
V46
()
V47
()
V51
() )
set
) ) : ( ( ) ( )
set
) ) ) : ( ( ) (
V11
()
real
ext-real
)
set
) &
(
cosh
x
: ( (
real
) (
V11
()
real
ext-real
)
number
)
)
: ( ( ) (
V11
()
real
ext-real
)
Element
of
REAL
: ( ( ) (
V45
()
V46
()
V47
()
V51
() )
set
) )
|^
5 : ( ( ) (
V1
()
ordinal
natural
V11
()
real
ext-real
positive
non
negative
V33
()
V34
()
V45
()
V46
()
V47
()
V48
()
V49
()
V50
() )
Element
of
NAT
: ( ( ) (
V45
()
V46
()
V47
()
V48
()
V49
()
V50
()
V51
() )
Element
of
K6
(
REAL
: ( ( ) (
V45
()
V46
()
V47
()
V51
() )
set
) ) : ( ( ) ( )
set
) ) ) : ( ( ) (
V11
()
real
ext-real
)
Element
of
REAL
: ( ( ) (
V45
()
V46
()
V47
()
V51
() )
set
) )
=
(
(
(
cosh
(
5 : ( ( ) (
V1
()
ordinal
natural
V11
()
real
ext-real
positive
non
negative
V33
()
V34
()
V45
()
V46
()
V47
()
V48
()
V49
()
V50
() )
Element
of
NAT
: ( ( ) (
V45
()
V46
()
V47
()
V48
()
V49
()
V50
()
V51
() )
Element
of
K6
(
REAL
: ( ( ) (
V45
()
V46
()
V47
()
V51
() )
set
) ) : ( ( ) ( )
set
) ) )
*
x
: ( (
real
) (
V11
()
real
ext-real
)
number
)
)
: ( ( ) (
V11
()
real
ext-real
)
set
)
)
: ( ( ) (
V11
()
real
ext-real
)
Element
of
REAL
: ( ( ) (
V45
()
V46
()
V47
()
V51
() )
set
) )
+
(
5 : ( ( ) (
V1
()
ordinal
natural
V11
()
real
ext-real
positive
non
negative
V33
()
V34
()
V45
()
V46
()
V47
()
V48
()
V49
()
V50
() )
Element
of
NAT
: ( ( ) (
V45
()
V46
()
V47
()
V48
()
V49
()
V50
()
V51
() )
Element
of
K6
(
REAL
: ( ( ) (
V45
()
V46
()
V47
()
V51
() )
set
) ) : ( ( ) ( )
set
) ) )
*
(
cosh
(
3 : ( ( ) (
V1
()
ordinal
natural
V11
()
real
ext-real
positive
non
negative
V33
()
V34
()
V45
()
V46
()
V47
()
V48
()
V49
()
V50
() )
Element
of
NAT
: ( ( ) (
V45
()
V46
()
V47
()
V48
()
V49
()
V50
()
V51
() )
Element
of
K6
(
REAL
: ( ( ) (
V45
()
V46
()
V47
()
V51
() )
set
) ) : ( ( ) ( )
set
) ) )
*
x
: ( (
real
) (
V11
()
real
ext-real
)
number
)
)
: ( ( ) (
V11
()
real
ext-real
)
set
)
)
: ( ( ) (
V11
()
real
ext-real
)
Element
of
REAL
: ( ( ) (
V45
()
V46
()
V47
()
V51
() )
set
) )
)
: ( ( ) (
V11
()
real
ext-real
)
set
)
)
: ( ( ) (
V11
()
real
ext-real
)
set
)
+
(
10 : ( ( ) (
V1
()
ordinal
natural
V11
()
real
ext-real
positive
non
negative
V33
()
V34
()
V45
()
V46
()
V47
()
V48
()
V49
()
V50
() )
Element
of
NAT
: ( ( ) (
V45
()
V46
()
V47
()
V48
()
V49
()
V50
()
V51
() )
Element
of
K6
(
REAL
: ( ( ) (
V45
()
V46
()
V47
()
V51
() )
set
) ) : ( ( ) ( )
set
) ) )
*
(
cosh
x
: ( (
real
) (
V11
()
real
ext-real
)
number
)
)
: ( ( ) (
V11
()
real
ext-real
)
Element
of
REAL
: ( ( ) (
V45
()
V46
()
V47
()
V51
() )
set
) )
)
: ( ( ) (
V11
()
real
ext-real
)
set
)
)
: ( ( ) (
V11
()
real
ext-real
)
set
)
/
16 : ( ( ) (
V1
()
ordinal
natural
V11
()
real
ext-real
positive
non
negative
V33
()
V34
()
V45
()
V46
()
V47
()
V48
()
V49
()
V50
() )
Element
of
NAT
: ( ( ) (
V45
()
V46
()
V47
()
V48
()
V49
()
V50
()
V51
() )
Element
of
K6
(
REAL
: ( ( ) (
V45
()
V46
()
V47
()
V51
() )
set
) ) : ( ( ) ( )
set
) ) ) : ( ( ) (
V11
()
real
ext-real
)
set
) &
(
cosh
x
: ( (
real
) (
V11
()
real
ext-real
)
number
)
)
: ( ( ) (
V11
()
real
ext-real
)
Element
of
REAL
: ( ( ) (
V45
()
V46
()
V47
()
V51
() )
set
) )
|^
6 : ( ( ) (
V1
()
ordinal
natural
V11
()
real
ext-real
positive
non
negative
V33
()
V34
()
V45
()
V46
()
V47
()
V48
()
V49
()
V50
() )
Element
of
NAT
: ( ( ) (
V45
()
V46
()
V47
()
V48
()
V49
()
V50
()
V51
() )
Element
of
K6
(
REAL
: ( ( ) (
V45
()
V46
()
V47
()
V51
() )
set
) ) : ( ( ) ( )
set
) ) ) : ( ( ) (
V11
()
real
ext-real
)
Element
of
REAL
: ( ( ) (
V45
()
V46
()
V47
()
V51
() )
set
) )
=
(
(
(
(
cosh
(
6 : ( ( ) (
V1
()
ordinal
natural
V11
()
real
ext-real
positive
non
negative
V33
()
V34
()
V45
()
V46
()
V47
()
V48
()
V49
()
V50
() )
Element
of
NAT
: ( ( ) (
V45
()
V46
()
V47
()
V48
()
V49
()
V50
()
V51
() )
Element
of
K6
(
REAL
: ( ( ) (
V45
()
V46
()
V47
()
V51
() )
set
) ) : ( ( ) ( )
set
) ) )
*
x
: ( (
real
) (
V11
()
real
ext-real
)
number
)
)
: ( ( ) (
V11
()
real
ext-real
)
set
)
)
: ( ( ) (
V11
()
real
ext-real
)
Element
of
REAL
: ( ( ) (
V45
()
V46
()
V47
()
V51
() )
set
) )
+
(
6 : ( ( ) (
V1
()
ordinal
natural
V11
()
real
ext-real
positive
non
negative
V33
()
V34
()
V45
()
V46
()
V47
()
V48
()
V49
()
V50
() )
Element
of
NAT
: ( ( ) (
V45
()
V46
()
V47
()
V48
()
V49
()
V50
()
V51
() )
Element
of
K6
(
REAL
: ( ( ) (
V45
()
V46
()
V47
()
V51
() )
set
) ) : ( ( ) ( )
set
) ) )
*
(
cosh
(
4 : ( ( ) (
V1
()
ordinal
natural
V11
()
real
ext-real
positive
non
negative
V33
()
V34
()
V45
()
V46
()
V47
()
V48
()
V49
()
V50
() )
Element
of
NAT
: ( ( ) (
V45
()
V46
()
V47
()
V48
()
V49
()
V50
()
V51
() )
Element
of
K6
(
REAL
: ( ( ) (
V45
()
V46
()
V47
()
V51
() )
set
) ) : ( ( ) ( )
set
) ) )
*
x
: ( (
real
) (
V11
()
real
ext-real
)
number
)
)
: ( ( ) (
V11
()
real
ext-real
)
set
)
)
: ( ( ) (
V11
()
real
ext-real
)
Element
of
REAL
: ( ( ) (
V45
()
V46
()
V47
()
V51
() )
set
) )
)
: ( ( ) (
V11
()
real
ext-real
)
set
)
)
: ( ( ) (
V11
()
real
ext-real
)
set
)
+
(
15 : ( ( ) (
V1
()
ordinal
natural
V11
()
real
ext-real
positive
non
negative
V33
()
V34
()
V45
()
V46
()
V47
()
V48
()
V49
()
V50
() )
Element
of
NAT
: ( ( ) (
V45
()
V46
()
V47
()
V48
()
V49
()
V50
()
V51
() )
Element
of
K6
(
REAL
: ( ( ) (
V45
()
V46
()
V47
()
V51
() )
set
) ) : ( ( ) ( )
set
) ) )
*
(
cosh
(
2 : ( ( ) (
V1
()
ordinal
natural
V11
()
real
ext-real
positive
non
negative
V33
()
V34
()
V45
()
V46
()
V47
()
V48
()
V49
()
V50
() )
Element
of
NAT
: ( ( ) (
V45
()
V46
()
V47
()
V48
()
V49
()
V50
()
V51
() )
Element
of
K6
(
REAL
: ( ( ) (
V45
()
V46
()
V47
()
V51
() )
set
) ) : ( ( ) ( )
set
) ) )
*
x
: ( (
real
) (
V11
()
real
ext-real
)
number
)
)
: ( ( ) (
V11
()
real
ext-real
)
set
)
)
: ( ( ) (
V11
()
real
ext-real
)
Element
of
REAL
: ( ( ) (
V45
()
V46
()
V47
()
V51
() )
set
) )
)
: ( ( ) (
V11
()
real
ext-real
)
set
)
)
: ( ( ) (
V11
()
real
ext-real
)
set
)
+
10 : ( ( ) (
V1
()
ordinal
natural
V11
()
real
ext-real
positive
non
negative
V33
()
V34
()
V45
()
V46
()
V47
()
V48
()
V49
()
V50
() )
Element
of
NAT
: ( ( ) (
V45
()
V46
()
V47
()
V48
()
V49
()
V50
()
V51
() )
Element
of
K6
(
REAL
: ( ( ) (
V45
()
V46
()
V47
()
V51
() )
set
) ) : ( ( ) ( )
set
) ) )
)
: ( ( ) (
V11
()
real
ext-real
)
set
)
/
32 : ( ( ) (
V1
()
ordinal
natural
V11
()
real
ext-real
positive
non
negative
V33
()
V34
()
V45
()
V46
()
V47
()
V48
()
V49
()
V50
() )
Element
of
NAT
: ( ( ) (
V45
()
V46
()
V47
()
V48
()
V49
()
V50
()
V51
() )
Element
of
K6
(
REAL
: ( ( ) (
V45
()
V46
()
V47
()
V51
() )
set
) ) : ( ( ) ( )
set
) ) ) : ( ( ) (
V11
()
real
ext-real
)
set
) &
(
cosh
x
: ( (
real
) (
V11
()
real
ext-real
)
number
)
)
: ( ( ) (
V11
()
real
ext-real
)
Element
of
REAL
: ( ( ) (
V45
()
V46
()
V47
()
V51
() )
set
) )
|^
7 : ( ( ) (
V1
()
ordinal
natural
V11
()
real
ext-real
positive
non
negative
V33
()
V34
()
V45
()
V46
()
V47
()
V48
()
V49
()
V50
() )
Element
of
NAT
: ( ( ) (
V45
()
V46
()
V47
()
V48
()
V49
()
V50
()
V51
() )
Element
of
K6
(
REAL
: ( ( ) (
V45
()
V46
()
V47
()
V51
() )
set
) ) : ( ( ) ( )
set
) ) ) : ( ( ) (
V11
()
real
ext-real
)
Element
of
REAL
: ( ( ) (
V45
()
V46
()
V47
()
V51
() )
set
) )
=
(
(
(
(
cosh
(
7 : ( ( ) (
V1
()
ordinal
natural
V11
()
real
ext-real
positive
non
negative
V33
()
V34
()
V45
()
V46
()
V47
()
V48
()
V49
()
V50
() )
Element
of
NAT
: ( ( ) (
V45
()
V46
()
V47
()
V48
()
V49
()
V50
()
V51
() )
Element
of
K6
(
REAL
: ( ( ) (
V45
()
V46
()
V47
()
V51
() )
set
) ) : ( ( ) ( )
set
) ) )
*
x
: ( (
real
) (
V11
()
real
ext-real
)
number
)
)
: ( ( ) (
V11
()
real
ext-real
)
set
)
)
: ( ( ) (
V11
()
real
ext-real
)
Element
of
REAL
: ( ( ) (
V45
()
V46
()
V47
()
V51
() )
set
) )
+
(
7 : ( ( ) (
V1
()
ordinal
natural
V11
()
real
ext-real
positive
non
negative
V33
()
V34
()
V45
()
V46
()
V47
()
V48
()
V49
()
V50
() )
Element
of
NAT
: ( ( ) (
V45
()
V46
()
V47
()
V48
()
V49
()
V50
()
V51
() )
Element
of
K6
(
REAL
: ( ( ) (
V45
()
V46
()
V47
()
V51
() )
set
) ) : ( ( ) ( )
set
) ) )
*
(
cosh
(
5 : ( ( ) (
V1
()
ordinal
natural
V11
()
real
ext-real
positive
non
negative
V33
()
V34
()
V45
()
V46
()
V47
()
V48
()
V49
()
V50
() )
Element
of
NAT
: ( ( ) (
V45
()
V46
()
V47
()
V48
()
V49
()
V50
()
V51
() )
Element
of
K6
(
REAL
: ( ( ) (
V45
()
V46
()
V47
()
V51
() )
set
) ) : ( ( ) ( )
set
) ) )
*
x
: ( (
real
) (
V11
()
real
ext-real
)
number
)
)
: ( ( ) (
V11
()
real
ext-real
)
set
)
)
: ( ( ) (
V11
()
real
ext-real
)
Element
of
REAL
: ( ( ) (
V45
()
V46
()
V47
()
V51
() )
set
) )
)
: ( ( ) (
V11
()
real
ext-real
)
set
)
)
: ( ( ) (
V11
()
real
ext-real
)
set
)
+
(
21 : ( ( ) (
V1
()
ordinal
natural
V11
()
real
ext-real
positive
non
negative
V33
()
V34
()
V45
()
V46
()
V47
()
V48
()
V49
()
V50
() )
Element
of
NAT
: ( ( ) (
V45
()
V46
()
V47
()
V48
()
V49
()
V50
()
V51
() )
Element
of
K6
(
REAL
: ( ( ) (
V45
()
V46
()
V47
()
V51
() )
set
) ) : ( ( ) ( )
set
) ) )
*
(
cosh
(
3 : ( ( ) (
V1
()
ordinal
natural
V11
()
real
ext-real
positive
non
negative
V33
()
V34
()
V45
()
V46
()
V47
()
V48
()
V49
()
V50
() )
Element
of
NAT
: ( ( ) (
V45
()
V46
()
V47
()
V48
()
V49
()
V50
()
V51
() )
Element
of
K6
(
REAL
: ( ( ) (
V45
()
V46
()
V47
()
V51
() )
set
) ) : ( ( ) ( )
set
) ) )
*
x
: ( (
real
) (
V11
()
real
ext-real
)
number
)
)
: ( ( ) (
V11
()
real
ext-real
)
set
)
)
: ( ( ) (
V11
()
real
ext-real
)
Element
of
REAL
: ( ( ) (
V45
()
V46
()
V47
()
V51
() )
set
) )
)
: ( ( ) (
V11
()
real
ext-real
)
set
)
)
: ( ( ) (
V11
()
real
ext-real
)
set
)
+
(
35 : ( ( ) (
V1
()
ordinal
natural
V11
()
real
ext-real
positive
non
negative
V33
()
V34
()
V45
()
V46
()
V47
()
V48
()
V49
()
V50
() )
Element
of
NAT
: ( ( ) (
V45
()
V46
()
V47
()
V48
()
V49
()
V50
()
V51
() )
Element
of
K6
(
REAL
: ( ( ) (
V45
()
V46
()
V47
()
V51
() )
set
) ) : ( ( ) ( )
set
) ) )
*
(
cosh
x
: ( (
real
) (
V11
()
real
ext-real
)
number
)
)
: ( ( ) (
V11
()
real
ext-real
)
Element
of
REAL
: ( ( ) (
V45
()
V46
()
V47
()
V51
() )
set
) )
)
: ( ( ) (
V11
()
real
ext-real
)
set
)
)
: ( ( ) (
V11
()
real
ext-real
)
set
)
/
64 : ( ( ) (
V1
()
ordinal
natural
V11
()
real
ext-real
positive
non
negative
V33
()
V34
()
V45
()
V46
()
V47
()
V48
()
V49
()
V50
() )
Element
of
NAT
: ( ( ) (
V45
()
V46
()
V47
()
V48
()
V49
()
V50
()
V51
() )
Element
of
K6
(
REAL
: ( ( ) (
V45
()
V46
()
V47
()
V51
() )
set
) ) : ( ( ) ( )
set
) ) ) : ( ( ) (
V11
()
real
ext-real
)
set
) &
(
cosh
x
: ( (
real
) (
V11
()
real
ext-real
)
number
)
)
: ( ( ) (
V11
()
real
ext-real
)
Element
of
REAL
: ( ( ) (
V45
()
V46
()
V47
()
V51
() )
set
) )
|^
8 : ( ( ) (
V1
()
ordinal
natural
V11
()
real
ext-real
positive
non
negative
V33
()
V34
()
V45
()
V46
()
V47
()
V48
()
V49
()
V50
() )
Element
of
NAT
: ( ( ) (
V45
()
V46
()
V47
()
V48
()
V49
()
V50
()
V51
() )
Element
of
K6
(
REAL
: ( ( ) (
V45
()
V46
()
V47
()
V51
() )
set
) ) : ( ( ) ( )
set
) ) ) : ( ( ) (
V11
()
real
ext-real
)
Element
of
REAL
: ( ( ) (
V45
()
V46
()
V47
()
V51
() )
set
) )
=
(
(
(
(
(
cosh
(
8 : ( ( ) (
V1
()
ordinal
natural
V11
()
real
ext-real
positive
non
negative
V33
()
V34
()
V45
()
V46
()
V47
()
V48
()
V49
()
V50
() )
Element
of
NAT
: ( ( ) (
V45
()
V46
()
V47
()
V48
()
V49
()
V50
()
V51
() )
Element
of
K6
(
REAL
: ( ( ) (
V45
()
V46
()
V47
()
V51
() )
set
) ) : ( ( ) ( )
set
) ) )
*
x
: ( (
real
) (
V11
()
real
ext-real
)
number
)
)
: ( ( ) (
V11
()
real
ext-real
)
set
)
)
: ( ( ) (
V11
()
real
ext-real
)
Element
of
REAL
: ( ( ) (
V45
()
V46
()
V47
()
V51
() )
set
) )
+
(
8 : ( ( ) (
V1
()
ordinal
natural
V11
()
real
ext-real
positive
non
negative
V33
()
V34
()
V45
()
V46
()
V47
()
V48
()
V49
()
V50
() )
Element
of
NAT
: ( ( ) (
V45
()
V46
()
V47
()
V48
()
V49
()
V50
()
V51
() )
Element
of
K6
(
REAL
: ( ( ) (
V45
()
V46
()
V47
()
V51
() )
set
) ) : ( ( ) ( )
set
) ) )
*
(
cosh
(
6 : ( ( ) (
V1
()
ordinal
natural
V11
()
real
ext-real
positive
non
negative
V33
()
V34
()
V45
()
V46
()
V47
()
V48
()
V49
()
V50
() )
Element
of
NAT
: ( ( ) (
V45
()
V46
()
V47
()
V48
()
V49
()
V50
()
V51
() )
Element
of
K6
(
REAL
: ( ( ) (
V45
()
V46
()
V47
()
V51
() )
set
) ) : ( ( ) ( )
set
) ) )
*
x
: ( (
real
) (
V11
()
real
ext-real
)
number
)
)
: ( ( ) (
V11
()
real
ext-real
)
set
)
)
: ( ( ) (
V11
()
real
ext-real
)
Element
of
REAL
: ( ( ) (
V45
()
V46
()
V47
()
V51
() )
set
) )
)
: ( ( ) (
V11
()
real
ext-real
)
set
)
)
: ( ( ) (
V11
()
real
ext-real
)
set
)
+
(
28 : ( ( ) (
V1
()
ordinal
natural
V11
()
real
ext-real
positive
non
negative
V33
()
V34
()
V45
()
V46
()
V47
()
V48
()
V49
()
V50
() )
Element
of
NAT
: ( ( ) (
V45
()
V46
()
V47
()
V48
()
V49
()
V50
()
V51
() )
Element
of
K6
(
REAL
: ( ( ) (
V45
()
V46
()
V47
()
V51
() )
set
) ) : ( ( ) ( )
set
) ) )
*
(
cosh
(
4 : ( ( ) (
V1
()
ordinal
natural
V11
()
real
ext-real
positive
non
negative
V33
()
V34
()
V45
()
V46
()
V47
()
V48
()
V49
()
V50
() )
Element
of
NAT
: ( ( ) (
V45
()
V46
()
V47
()
V48
()
V49
()
V50
()
V51
() )
Element
of
K6
(
REAL
: ( ( ) (
V45
()
V46
()
V47
()
V51
() )
set
) ) : ( ( ) ( )
set
) ) )
*
x
: ( (
real
) (
V11
()
real
ext-real
)
number
)
)
: ( ( ) (
V11
()
real
ext-real
)
set
)
)
: ( ( ) (
V11
()
real
ext-real
)
Element
of
REAL
: ( ( ) (
V45
()
V46
()
V47
()
V51
() )
set
) )
)
: ( ( ) (
V11
()
real
ext-real
)
set
)
)
: ( ( ) (
V11
()
real
ext-real
)
set
)
+
(
56 : ( ( ) (
V1
()
ordinal
natural
V11
()
real
ext-real
positive
non
negative
V33
()
V34
()
V45
()
V46
()
V47
()
V48
()
V49
()
V50
() )
Element
of
NAT
: ( ( ) (
V45
()
V46
()
V47
()
V48
()
V49
()
V50
()
V51
() )
Element
of
K6
(
REAL
: ( ( ) (
V45
()
V46
()
V47
()
V51
() )
set
) ) : ( ( ) ( )
set
) ) )
*
(
cosh
(
2 : ( ( ) (
V1
()
ordinal
natural
V11
()
real
ext-real
positive
non
negative
V33
()
V34
()
V45
()
V46
()
V47
()
V48
()
V49
()
V50
() )
Element
of
NAT
: ( ( ) (
V45
()
V46
()
V47
()
V48
()
V49
()
V50
()
V51
() )
Element
of
K6
(
REAL
: ( ( ) (
V45
()
V46
()
V47
()
V51
() )
set
) ) : ( ( ) ( )
set
) ) )
*
x
: ( (
real
) (
V11
()
real
ext-real
)
number
)
)
: ( ( ) (
V11
()
real
ext-real
)
set
)
)
: ( ( ) (
V11
()
real
ext-real
)
Element
of
REAL
: ( ( ) (
V45
()
V46
()
V47
()
V51
() )
set
) )
)
: ( ( ) (
V11
()
real
ext-real
)
set
)
)
: ( ( ) (
V11
()
real
ext-real
)
set
)
+
35 : ( ( ) (
V1
()
ordinal
natural
V11
()
real
ext-real
positive
non
negative
V33
()
V34
()
V45
()
V46
()
V47
()
V48
()
V49
()
V50
() )
Element
of
NAT
: ( ( ) (
V45
()
V46
()
V47
()
V48
()
V49
()
V50
()
V51
() )
Element
of
K6
(
REAL
: ( ( ) (
V45
()
V46
()
V47
()
V51
() )
set
) ) : ( ( ) ( )
set
) ) )
)
: ( ( ) (
V11
()
real
ext-real
)
set
)
/
128 : ( ( ) (
V1
()
ordinal
natural
V11
()
real
ext-real
positive
non
negative
V33
()
V34
()
V45
()
V46
()
V47
()
V48
()
V49
()
V50
() )
Element
of
NAT
: ( ( ) (
V45
()
V46
()
V47
()
V48
()
V49
()
V50
()
V51
() )
Element
of
K6
(
REAL
: ( ( ) (
V45
()
V46
()
V47
()
V51
() )
set
) ) : ( ( ) ( )
set
) ) ) : ( ( ) (
V11
()
real
ext-real
)
set
) ) ;
theorem
:: SIN_COS8:33
for
y
,
z
being ( (
real
) (
V11
()
real
ext-real
)
number
) holds
(
(
cosh
(
2 : ( ( ) (
V1
()
ordinal
natural
V11
()
real
ext-real
positive
non
negative
V33
()
V34
()
V45
()
V46
()
V47
()
V48
()
V49
()
V50
() )
Element
of
NAT
: ( ( ) (
V45
()
V46
()
V47
()
V48
()
V49
()
V50
()
V51
() )
Element
of
K6
(
REAL
: ( ( ) (
V45
()
V46
()
V47
()
V51
() )
set
) ) : ( ( ) ( )
set
) ) )
*
y
: ( (
real
) (
V11
()
real
ext-real
)
number
)
)
: ( ( ) (
V11
()
real
ext-real
)
set
)
)
: ( ( ) (
V11
()
real
ext-real
)
Element
of
REAL
: ( ( ) (
V45
()
V46
()
V47
()
V51
() )
set
) )
+
(
cos
(
2 : ( ( ) (
V1
()
ordinal
natural
V11
()
real
ext-real
positive
non
negative
V33
()
V34
()
V45
()
V46
()
V47
()
V48
()
V49
()
V50
() )
Element
of
NAT
: ( ( ) (
V45
()
V46
()
V47
()
V48
()
V49
()
V50
()
V51
() )
Element
of
K6
(
REAL
: ( ( ) (
V45
()
V46
()
V47
()
V51
() )
set
) ) : ( ( ) ( )
set
) ) )
*
z
: ( (
real
) (
V11
()
real
ext-real
)
number
)
)
: ( ( ) (
V11
()
real
ext-real
)
set
)
)
: ( ( ) (
V11
()
real
ext-real
)
set
) : ( ( ) (
V11
()
real
ext-real
)
set
)
=
2 : ( ( ) (
V1
()
ordinal
natural
V11
()
real
ext-real
positive
non
negative
V33
()
V34
()
V45
()
V46
()
V47
()
V48
()
V49
()
V50
() )
Element
of
NAT
: ( ( ) (
V45
()
V46
()
V47
()
V48
()
V49
()
V50
()
V51
() )
Element
of
K6
(
REAL
: ( ( ) (
V45
()
V46
()
V47
()
V51
() )
set
) ) : ( ( ) ( )
set
) ) )
+
(
2 : ( ( ) (
V1
()
ordinal
natural
V11
()
real
ext-real
positive
non
negative
V33
()
V34
()
V45
()
V46
()
V47
()
V48
()
V49
()
V50
() )
Element
of
NAT
: ( ( ) (
V45
()
V46
()
V47
()
V48
()
V49
()
V50
()
V51
() )
Element
of
K6
(
REAL
: ( ( ) (
V45
()
V46
()
V47
()
V51
() )
set
) ) : ( ( ) ( )
set
) ) )
*
(
(
(
sinh
y
: ( (
real
) (
V11
()
real
ext-real
)
number
)
)
: ( ( ) (
V11
()
real
ext-real
)
Element
of
REAL
: ( ( ) (
V45
()
V46
()
V47
()
V51
() )
set
) )
^2
)
: ( ( ) (
V11
()
real
ext-real
)
Element
of
REAL
: ( ( ) (
V45
()
V46
()
V47
()
V51
() )
set
) )
-
(
(
sin
z
: ( (
real
) (
V11
()
real
ext-real
)
number
)
)
: ( ( ) (
V11
()
real
ext-real
)
set
)
^2
)
: ( ( ) (
V11
()
real
ext-real
)
set
)
)
: ( ( ) (
V11
()
real
ext-real
)
set
)
)
: ( ( ) (
V11
()
real
ext-real
)
set
) : ( ( ) (
V11
()
real
ext-real
)
set
) &
(
cosh
(
2 : ( ( ) (
V1
()
ordinal
natural
V11
()
real
ext-real
positive
non
negative
V33
()
V34
()
V45
()
V46
()
V47
()
V48
()
V49
()
V50
() )
Element
of
NAT
: ( ( ) (
V45
()
V46
()
V47
()
V48
()
V49
()
V50
()
V51
() )
Element
of
K6
(
REAL
: ( ( ) (
V45
()
V46
()
V47
()
V51
() )
set
) ) : ( ( ) ( )
set
) ) )
*
y
: ( (
real
) (
V11
()
real
ext-real
)
number
)
)
: ( ( ) (
V11
()
real
ext-real
)
set
)
)
: ( ( ) (
V11
()
real
ext-real
)
Element
of
REAL
: ( ( ) (
V45
()
V46
()
V47
()
V51
() )
set
) )
-
(
cos
(
2 : ( ( ) (
V1
()
ordinal
natural
V11
()
real
ext-real
positive
non
negative
V33
()
V34
()
V45
()
V46
()
V47
()
V48
()
V49
()
V50
() )
Element
of
NAT
: ( ( ) (
V45
()
V46
()
V47
()
V48
()
V49
()
V50
()
V51
() )
Element
of
K6
(
REAL
: ( ( ) (
V45
()
V46
()
V47
()
V51
() )
set
) ) : ( ( ) ( )
set
) ) )
*
z
: ( (
real
) (
V11
()
real
ext-real
)
number
)
)
: ( ( ) (
V11
()
real
ext-real
)
set
)
)
: ( ( ) (
V11
()
real
ext-real
)
set
) : ( ( ) (
V11
()
real
ext-real
)
set
)
=
2 : ( ( ) (
V1
()
ordinal
natural
V11
()
real
ext-real
positive
non
negative
V33
()
V34
()
V45
()
V46
()
V47
()
V48
()
V49
()
V50
() )
Element
of
NAT
: ( ( ) (
V45
()
V46
()
V47
()
V48
()
V49
()
V50
()
V51
() )
Element
of
K6
(
REAL
: ( ( ) (
V45
()
V46
()
V47
()
V51
() )
set
) ) : ( ( ) ( )
set
) ) )
*
(
(
(
sinh
y
: ( (
real
) (
V11
()
real
ext-real
)
number
)
)
: ( ( ) (
V11
()
real
ext-real
)
Element
of
REAL
: ( ( ) (
V45
()
V46
()
V47
()
V51
() )
set
) )
^2
)
: ( ( ) (
V11
()
real
ext-real
)
Element
of
REAL
: ( ( ) (
V45
()
V46
()
V47
()
V51
() )
set
) )
+
(
(
sin
z
: ( (
real
) (
V11
()
real
ext-real
)
number
)
)
: ( ( ) (
V11
()
real
ext-real
)
set
)
^2
)
: ( ( ) (
V11
()
real
ext-real
)
set
)
)
: ( ( ) (
V11
()
real
ext-real
)
set
) : ( ( ) (
V11
()
real
ext-real
)
set
) ) ;