:: SIN_COS4 semantic presentation
begin
definition
let
th
be ( (
real
) (
V11
()
V12
()
real
)
number
) ;
func
tan
th
->
( ( ) (
V11
()
V12
()
real
)
Real
)
equals
:: SIN_COS4:def 1
(
sin
th
: ( (
V11
() ) (
V11
() )
set
)
)
: ( ( ) ( )
set
)
/
(
cos
th
: ( (
V11
() ) (
V11
() )
set
)
)
: ( ( ) ( )
set
) : ( ( ) ( )
set
) ;
end;
definition
let
th
be ( (
real
) (
V11
()
V12
()
real
)
number
) ;
func
cot
th
->
( ( ) (
V11
()
V12
()
real
)
Real
)
equals
:: SIN_COS4:def 2
(
cos
th
: ( (
V11
() ) (
V11
() )
set
)
)
: ( ( ) ( )
set
)
/
(
sin
th
: ( (
V11
() ) (
V11
() )
set
)
)
: ( ( ) ( )
set
) : ( ( ) ( )
set
) ;
end;
definition
let
th
be ( (
real
) (
V11
()
V12
()
real
)
number
) ;
func
cosec
th
->
( ( ) (
V11
()
V12
()
real
)
Real
)
equals
:: SIN_COS4:def 3
1 : ( ( ) (
epsilon-transitive
epsilon-connected
ordinal
natural
V11
()
V12
()
real
V29
() )
M3
(
K28
() : ( ( ) ( )
set
) ,
K32
() : ( ( ) (
V1
()
epsilon-transitive
epsilon-connected
ordinal
)
M2
(
K6
(
K28
() : ( ( ) ( )
set
) ) : ( ( ) ( )
set
) )) ))
/
(
sin
th
: ( (
V11
() ) (
V11
() )
set
)
)
: ( ( ) ( )
set
) : ( ( ) ( )
set
) ;
end;
definition
let
th
be ( (
real
) (
V11
()
V12
()
real
)
number
) ;
func
sec
th
->
( ( ) (
V11
()
V12
()
real
)
Real
)
equals
:: SIN_COS4:def 4
1 : ( ( ) (
epsilon-transitive
epsilon-connected
ordinal
natural
V11
()
V12
()
real
V29
() )
M3
(
K28
() : ( ( ) ( )
set
) ,
K32
() : ( ( ) (
V1
()
epsilon-transitive
epsilon-connected
ordinal
)
M2
(
K6
(
K28
() : ( ( ) ( )
set
) ) : ( ( ) ( )
set
) )) ))
/
(
cos
th
: ( (
V11
() ) (
V11
() )
set
)
)
: ( ( ) ( )
set
) : ( ( ) ( )
set
) ;
end;
theorem
:: SIN_COS4:1
for
th
being ( (
real
) (
V11
()
V12
()
real
)
number
) holds
tan
(
-
th
: ( (
real
) (
V11
()
V12
()
real
)
number
)
)
: ( (
V11
() ) (
V11
()
V12
()
real
)
set
) : ( ( ) (
V11
()
V12
()
real
)
Real
)
=
-
(
tan
th
: ( (
real
) (
V11
()
V12
()
real
)
number
)
)
: ( ( ) (
V11
()
V12
()
real
)
Real
) : ( (
V11
() ) (
V11
()
V12
()
real
)
set
) ;
theorem
:: SIN_COS4:2
for
th
being ( (
real
) (
V11
()
V12
()
real
)
number
) holds
cosec
(
-
th
: ( (
real
) (
V11
()
V12
()
real
)
number
)
)
: ( (
V11
() ) (
V11
()
V12
()
real
)
set
) : ( ( ) (
V11
()
V12
()
real
)
Real
)
=
-
(
1 : ( ( ) (
epsilon-transitive
epsilon-connected
ordinal
natural
V11
()
V12
()
real
V29
() )
M3
(
K28
() : ( ( ) ( )
set
) ,
K32
() : ( ( ) (
V1
()
epsilon-transitive
epsilon-connected
ordinal
)
M2
(
K6
(
K28
() : ( ( ) ( )
set
) ) : ( ( ) ( )
set
) )) ))
/
(
sin
th
: ( (
real
) (
V11
()
V12
()
real
)
number
)
)
: ( ( ) (
V11
()
V12
()
real
)
set
)
)
: ( ( ) (
V11
()
V12
()
real
)
set
) : ( (
V11
() ) (
V11
()
V12
()
real
)
set
) ;
theorem
:: SIN_COS4:3
for
th
being ( (
real
) (
V11
()
V12
()
real
)
number
) holds
cot
(
-
th
: ( (
real
) (
V11
()
V12
()
real
)
number
)
)
: ( (
V11
() ) (
V11
()
V12
()
real
)
set
) : ( ( ) (
V11
()
V12
()
real
)
Real
)
=
-
(
cot
th
: ( (
real
) (
V11
()
V12
()
real
)
number
)
)
: ( ( ) (
V11
()
V12
()
real
)
Real
) : ( (
V11
() ) (
V11
()
V12
()
real
)
set
) ;
theorem
:: SIN_COS4:4
for
th
being ( (
real
) (
V11
()
V12
()
real
)
number
) holds
(
sin
th
: ( (
real
) (
V11
()
V12
()
real
)
number
)
)
: ( ( ) (
V11
()
V12
()
real
)
set
)
*
(
sin
th
: ( (
real
) (
V11
()
V12
()
real
)
number
)
)
: ( ( ) (
V11
()
V12
()
real
)
set
) : ( ( ) (
V11
()
V12
()
real
)
set
)
=
1 : ( ( ) (
epsilon-transitive
epsilon-connected
ordinal
natural
V11
()
V12
()
real
V29
() )
M3
(
K28
() : ( ( ) ( )
set
) ,
K32
() : ( ( ) (
V1
()
epsilon-transitive
epsilon-connected
ordinal
)
M2
(
K6
(
K28
() : ( ( ) ( )
set
) ) : ( ( ) ( )
set
) )) ))
-
(
(
cos
th
: ( (
real
) (
V11
()
V12
()
real
)
number
)
)
: ( ( ) (
V11
()
V12
()
real
)
set
)
*
(
cos
th
: ( (
real
) (
V11
()
V12
()
real
)
number
)
)
: ( ( ) (
V11
()
V12
()
real
)
set
)
)
: ( ( ) (
V11
()
V12
()
real
)
set
) : ( ( ) (
V11
()
V12
()
real
)
set
) ;
theorem
:: SIN_COS4:5
for
th
being ( (
real
) (
V11
()
V12
()
real
)
number
) holds
(
cos
th
: ( (
real
) (
V11
()
V12
()
real
)
number
)
)
: ( ( ) (
V11
()
V12
()
real
)
set
)
*
(
cos
th
: ( (
real
) (
V11
()
V12
()
real
)
number
)
)
: ( ( ) (
V11
()
V12
()
real
)
set
) : ( ( ) (
V11
()
V12
()
real
)
set
)
=
1 : ( ( ) (
epsilon-transitive
epsilon-connected
ordinal
natural
V11
()
V12
()
real
V29
() )
M3
(
K28
() : ( ( ) ( )
set
) ,
K32
() : ( ( ) (
V1
()
epsilon-transitive
epsilon-connected
ordinal
)
M2
(
K6
(
K28
() : ( ( ) ( )
set
) ) : ( ( ) ( )
set
) )) ))
-
(
(
sin
th
: ( (
real
) (
V11
()
V12
()
real
)
number
)
)
: ( ( ) (
V11
()
V12
()
real
)
set
)
*
(
sin
th
: ( (
real
) (
V11
()
V12
()
real
)
number
)
)
: ( ( ) (
V11
()
V12
()
real
)
set
)
)
: ( ( ) (
V11
()
V12
()
real
)
set
) : ( ( ) (
V11
()
V12
()
real
)
set
) ;
theorem
:: SIN_COS4:6
for
th
being ( (
real
) (
V11
()
V12
()
real
)
number
) st
cos
th
: ( (
real
) (
V11
()
V12
()
real
)
number
) : ( ( ) (
V11
()
V12
()
real
)
set
)
<>
0
: ( ( ) (
epsilon-transitive
epsilon-connected
ordinal
natural
V11
()
V12
()
real
V29
() )
M3
(
K28
() : ( ( ) ( )
set
) ,
K32
() : ( ( ) (
V1
()
epsilon-transitive
epsilon-connected
ordinal
)
M2
(
K6
(
K28
() : ( ( ) ( )
set
) ) : ( ( ) ( )
set
) )) )) holds
sin
th
: ( (
real
) (
V11
()
V12
()
real
)
number
) : ( ( ) (
V11
()
V12
()
real
)
set
)
=
(
cos
th
: ( (
real
) (
V11
()
V12
()
real
)
number
)
)
: ( ( ) (
V11
()
V12
()
real
)
set
)
*
(
tan
th
: ( (
real
) (
V11
()
V12
()
real
)
number
)
)
: ( ( ) (
V11
()
V12
()
real
)
Real
) : ( ( ) (
V11
()
V12
()
real
)
set
) ;
theorem
:: SIN_COS4:7
for
th1
,
th2
being ( (
real
) (
V11
()
V12
()
real
)
number
) st
cos
th1
: ( (
real
) (
V11
()
V12
()
real
)
number
) : ( ( ) (
V11
()
V12
()
real
)
set
)
<>
0
: ( ( ) (
epsilon-transitive
epsilon-connected
ordinal
natural
V11
()
V12
()
real
V29
() )
M3
(
K28
() : ( ( ) ( )
set
) ,
K32
() : ( ( ) (
V1
()
epsilon-transitive
epsilon-connected
ordinal
)
M2
(
K6
(
K28
() : ( ( ) ( )
set
) ) : ( ( ) ( )
set
) )) )) &
cos
th2
: ( (
real
) (
V11
()
V12
()
real
)
number
) : ( ( ) (
V11
()
V12
()
real
)
set
)
<>
0
: ( ( ) (
epsilon-transitive
epsilon-connected
ordinal
natural
V11
()
V12
()
real
V29
() )
M3
(
K28
() : ( ( ) ( )
set
) ,
K32
() : ( ( ) (
V1
()
epsilon-transitive
epsilon-connected
ordinal
)
M2
(
K6
(
K28
() : ( ( ) ( )
set
) ) : ( ( ) ( )
set
) )) )) holds
tan
(
th1
: ( (
real
) (
V11
()
V12
()
real
)
number
)
+
th2
: ( (
real
) (
V11
()
V12
()
real
)
number
)
)
: ( ( ) (
V11
()
V12
()
real
)
set
) : ( ( ) (
V11
()
V12
()
real
)
Real
)
=
(
(
tan
th1
: ( (
real
) (
V11
()
V12
()
real
)
number
)
)
: ( ( ) (
V11
()
V12
()
real
)
Real
)
+
(
tan
th2
: ( (
real
) (
V11
()
V12
()
real
)
number
)
)
: ( ( ) (
V11
()
V12
()
real
)
Real
)
)
: ( ( ) (
V11
()
V12
()
real
)
set
)
/
(
1 : ( ( ) (
epsilon-transitive
epsilon-connected
ordinal
natural
V11
()
V12
()
real
V29
() )
M3
(
K28
() : ( ( ) ( )
set
) ,
K32
() : ( ( ) (
V1
()
epsilon-transitive
epsilon-connected
ordinal
)
M2
(
K6
(
K28
() : ( ( ) ( )
set
) ) : ( ( ) ( )
set
) )) ))
-
(
(
tan
th1
: ( (
real
) (
V11
()
V12
()
real
)
number
)
)
: ( ( ) (
V11
()
V12
()
real
)
Real
)
*
(
tan
th2
: ( (
real
) (
V11
()
V12
()
real
)
number
)
)
: ( ( ) (
V11
()
V12
()
real
)
Real
)
)
: ( ( ) (
V11
()
V12
()
real
)
set
)
)
: ( ( ) (
V11
()
V12
()
real
)
set
) : ( ( ) (
V11
()
V12
()
real
)
set
) ;
theorem
:: SIN_COS4:8
for
th1
,
th2
being ( (
real
) (
V11
()
V12
()
real
)
number
) st
cos
th1
: ( (
real
) (
V11
()
V12
()
real
)
number
) : ( ( ) (
V11
()
V12
()
real
)
set
)
<>
0
: ( ( ) (
epsilon-transitive
epsilon-connected
ordinal
natural
V11
()
V12
()
real
V29
() )
M3
(
K28
() : ( ( ) ( )
set
) ,
K32
() : ( ( ) (
V1
()
epsilon-transitive
epsilon-connected
ordinal
)
M2
(
K6
(
K28
() : ( ( ) ( )
set
) ) : ( ( ) ( )
set
) )) )) &
cos
th2
: ( (
real
) (
V11
()
V12
()
real
)
number
) : ( ( ) (
V11
()
V12
()
real
)
set
)
<>
0
: ( ( ) (
epsilon-transitive
epsilon-connected
ordinal
natural
V11
()
V12
()
real
V29
() )
M3
(
K28
() : ( ( ) ( )
set
) ,
K32
() : ( ( ) (
V1
()
epsilon-transitive
epsilon-connected
ordinal
)
M2
(
K6
(
K28
() : ( ( ) ( )
set
) ) : ( ( ) ( )
set
) )) )) holds
tan
(
th1
: ( (
real
) (
V11
()
V12
()
real
)
number
)
-
th2
: ( (
real
) (
V11
()
V12
()
real
)
number
)
)
: ( ( ) (
V11
()
V12
()
real
)
set
) : ( ( ) (
V11
()
V12
()
real
)
Real
)
=
(
(
tan
th1
: ( (
real
) (
V11
()
V12
()
real
)
number
)
)
: ( ( ) (
V11
()
V12
()
real
)
Real
)
-
(
tan
th2
: ( (
real
) (
V11
()
V12
()
real
)
number
)
)
: ( ( ) (
V11
()
V12
()
real
)
Real
)
)
: ( ( ) (
V11
()
V12
()
real
)
set
)
/
(
1 : ( ( ) (
epsilon-transitive
epsilon-connected
ordinal
natural
V11
()
V12
()
real
V29
() )
M3
(
K28
() : ( ( ) ( )
set
) ,
K32
() : ( ( ) (
V1
()
epsilon-transitive
epsilon-connected
ordinal
)
M2
(
K6
(
K28
() : ( ( ) ( )
set
) ) : ( ( ) ( )
set
) )) ))
+
(
(
tan
th1
: ( (
real
) (
V11
()
V12
()
real
)
number
)
)
: ( ( ) (
V11
()
V12
()
real
)
Real
)
*
(
tan
th2
: ( (
real
) (
V11
()
V12
()
real
)
number
)
)
: ( ( ) (
V11
()
V12
()
real
)
Real
)
)
: ( ( ) (
V11
()
V12
()
real
)
set
)
)
: ( ( ) (
V11
()
V12
()
real
)
set
) : ( ( ) (
V11
()
V12
()
real
)
set
) ;
theorem
:: SIN_COS4:9
for
th1
,
th2
being ( (
real
) (
V11
()
V12
()
real
)
number
) st
sin
th1
: ( (
real
) (
V11
()
V12
()
real
)
number
) : ( ( ) (
V11
()
V12
()
real
)
set
)
<>
0
: ( ( ) (
epsilon-transitive
epsilon-connected
ordinal
natural
V11
()
V12
()
real
V29
() )
M3
(
K28
() : ( ( ) ( )
set
) ,
K32
() : ( ( ) (
V1
()
epsilon-transitive
epsilon-connected
ordinal
)
M2
(
K6
(
K28
() : ( ( ) ( )
set
) ) : ( ( ) ( )
set
) )) )) &
sin
th2
: ( (
real
) (
V11
()
V12
()
real
)
number
) : ( ( ) (
V11
()
V12
()
real
)
set
)
<>
0
: ( ( ) (
epsilon-transitive
epsilon-connected
ordinal
natural
V11
()
V12
()
real
V29
() )
M3
(
K28
() : ( ( ) ( )
set
) ,
K32
() : ( ( ) (
V1
()
epsilon-transitive
epsilon-connected
ordinal
)
M2
(
K6
(
K28
() : ( ( ) ( )
set
) ) : ( ( ) ( )
set
) )) )) holds
cot
(
th1
: ( (
real
) (
V11
()
V12
()
real
)
number
)
+
th2
: ( (
real
) (
V11
()
V12
()
real
)
number
)
)
: ( ( ) (
V11
()
V12
()
real
)
set
) : ( ( ) (
V11
()
V12
()
real
)
Real
)
=
(
(
(
cot
th1
: ( (
real
) (
V11
()
V12
()
real
)
number
)
)
: ( ( ) (
V11
()
V12
()
real
)
Real
)
*
(
cot
th2
: ( (
real
) (
V11
()
V12
()
real
)
number
)
)
: ( ( ) (
V11
()
V12
()
real
)
Real
)
)
: ( ( ) (
V11
()
V12
()
real
)
set
)
-
1 : ( ( ) (
epsilon-transitive
epsilon-connected
ordinal
natural
V11
()
V12
()
real
V29
() )
M3
(
K28
() : ( ( ) ( )
set
) ,
K32
() : ( ( ) (
V1
()
epsilon-transitive
epsilon-connected
ordinal
)
M2
(
K6
(
K28
() : ( ( ) ( )
set
) ) : ( ( ) ( )
set
) )) ))
)
: ( ( ) (
V11
()
V12
()
real
)
set
)
/
(
(
cot
th2
: ( (
real
) (
V11
()
V12
()
real
)
number
)
)
: ( ( ) (
V11
()
V12
()
real
)
Real
)
+
(
cot
th1
: ( (
real
) (
V11
()
V12
()
real
)
number
)
)
: ( ( ) (
V11
()
V12
()
real
)
Real
)
)
: ( ( ) (
V11
()
V12
()
real
)
set
) : ( ( ) (
V11
()
V12
()
real
)
set
) ;
theorem
:: SIN_COS4:10
for
th1
,
th2
being ( (
real
) (
V11
()
V12
()
real
)
number
) st
sin
th1
: ( (
real
) (
V11
()
V12
()
real
)
number
) : ( ( ) (
V11
()
V12
()
real
)
set
)
<>
0
: ( ( ) (
epsilon-transitive
epsilon-connected
ordinal
natural
V11
()
V12
()
real
V29
() )
M3
(
K28
() : ( ( ) ( )
set
) ,
K32
() : ( ( ) (
V1
()
epsilon-transitive
epsilon-connected
ordinal
)
M2
(
K6
(
K28
() : ( ( ) ( )
set
) ) : ( ( ) ( )
set
) )) )) &
sin
th2
: ( (
real
) (
V11
()
V12
()
real
)
number
) : ( ( ) (
V11
()
V12
()
real
)
set
)
<>
0
: ( ( ) (
epsilon-transitive
epsilon-connected
ordinal
natural
V11
()
V12
()
real
V29
() )
M3
(
K28
() : ( ( ) ( )
set
) ,
K32
() : ( ( ) (
V1
()
epsilon-transitive
epsilon-connected
ordinal
)
M2
(
K6
(
K28
() : ( ( ) ( )
set
) ) : ( ( ) ( )
set
) )) )) holds
cot
(
th1
: ( (
real
) (
V11
()
V12
()
real
)
number
)
-
th2
: ( (
real
) (
V11
()
V12
()
real
)
number
)
)
: ( ( ) (
V11
()
V12
()
real
)
set
) : ( ( ) (
V11
()
V12
()
real
)
Real
)
=
(
(
(
cot
th1
: ( (
real
) (
V11
()
V12
()
real
)
number
)
)
: ( ( ) (
V11
()
V12
()
real
)
Real
)
*
(
cot
th2
: ( (
real
) (
V11
()
V12
()
real
)
number
)
)
: ( ( ) (
V11
()
V12
()
real
)
Real
)
)
: ( ( ) (
V11
()
V12
()
real
)
set
)
+
1 : ( ( ) (
epsilon-transitive
epsilon-connected
ordinal
natural
V11
()
V12
()
real
V29
() )
M3
(
K28
() : ( ( ) ( )
set
) ,
K32
() : ( ( ) (
V1
()
epsilon-transitive
epsilon-connected
ordinal
)
M2
(
K6
(
K28
() : ( ( ) ( )
set
) ) : ( ( ) ( )
set
) )) ))
)
: ( ( ) (
V11
()
V12
()
real
)
set
)
/
(
(
cot
th2
: ( (
real
) (
V11
()
V12
()
real
)
number
)
)
: ( ( ) (
V11
()
V12
()
real
)
Real
)
-
(
cot
th1
: ( (
real
) (
V11
()
V12
()
real
)
number
)
)
: ( ( ) (
V11
()
V12
()
real
)
Real
)
)
: ( ( ) (
V11
()
V12
()
real
)
set
) : ( ( ) (
V11
()
V12
()
real
)
set
) ;
theorem
:: SIN_COS4:11
for
th1
,
th2
,
th3
being ( (
real
) (
V11
()
V12
()
real
)
number
) st
cos
th1
: ( (
real
) (
V11
()
V12
()
real
)
number
) : ( ( ) (
V11
()
V12
()
real
)
set
)
<>
0
: ( ( ) (
epsilon-transitive
epsilon-connected
ordinal
natural
V11
()
V12
()
real
V29
() )
M3
(
K28
() : ( ( ) ( )
set
) ,
K32
() : ( ( ) (
V1
()
epsilon-transitive
epsilon-connected
ordinal
)
M2
(
K6
(
K28
() : ( ( ) ( )
set
) ) : ( ( ) ( )
set
) )) )) &
cos
th2
: ( (
real
) (
V11
()
V12
()
real
)
number
) : ( ( ) (
V11
()
V12
()
real
)
set
)
<>
0
: ( ( ) (
epsilon-transitive
epsilon-connected
ordinal
natural
V11
()
V12
()
real
V29
() )
M3
(
K28
() : ( ( ) ( )
set
) ,
K32
() : ( ( ) (
V1
()
epsilon-transitive
epsilon-connected
ordinal
)
M2
(
K6
(
K28
() : ( ( ) ( )
set
) ) : ( ( ) ( )
set
) )) )) &
cos
th3
: ( (
real
) (
V11
()
V12
()
real
)
number
) : ( ( ) (
V11
()
V12
()
real
)
set
)
<>
0
: ( ( ) (
epsilon-transitive
epsilon-connected
ordinal
natural
V11
()
V12
()
real
V29
() )
M3
(
K28
() : ( ( ) ( )
set
) ,
K32
() : ( ( ) (
V1
()
epsilon-transitive
epsilon-connected
ordinal
)
M2
(
K6
(
K28
() : ( ( ) ( )
set
) ) : ( ( ) ( )
set
) )) )) holds
sin
(
(
th1
: ( (
real
) (
V11
()
V12
()
real
)
number
)
+
th2
: ( (
real
) (
V11
()
V12
()
real
)
number
)
)
: ( ( ) (
V11
()
V12
()
real
)
set
)
+
th3
: ( (
real
) (
V11
()
V12
()
real
)
number
)
)
: ( ( ) (
V11
()
V12
()
real
)
set
) : ( ( ) (
V11
()
V12
()
real
)
set
)
=
(
(
(
cos
th1
: ( (
real
) (
V11
()
V12
()
real
)
number
)
)
: ( ( ) (
V11
()
V12
()
real
)
set
)
*
(
cos
th2
: ( (
real
) (
V11
()
V12
()
real
)
number
)
)
: ( ( ) (
V11
()
V12
()
real
)
set
)
)
: ( ( ) (
V11
()
V12
()
real
)
set
)
*
(
cos
th3
: ( (
real
) (
V11
()
V12
()
real
)
number
)
)
: ( ( ) (
V11
()
V12
()
real
)
set
)
)
: ( ( ) (
V11
()
V12
()
real
)
set
)
*
(
(
(
(
tan
th1
: ( (
real
) (
V11
()
V12
()
real
)
number
)
)
: ( ( ) (
V11
()
V12
()
real
)
Real
)
+
(
tan
th2
: ( (
real
) (
V11
()
V12
()
real
)
number
)
)
: ( ( ) (
V11
()
V12
()
real
)
Real
)
)
: ( ( ) (
V11
()
V12
()
real
)
set
)
+
(
tan
th3
: ( (
real
) (
V11
()
V12
()
real
)
number
)
)
: ( ( ) (
V11
()
V12
()
real
)
Real
)
)
: ( ( ) (
V11
()
V12
()
real
)
set
)
-
(
(
(
tan
th1
: ( (
real
) (
V11
()
V12
()
real
)
number
)
)
: ( ( ) (
V11
()
V12
()
real
)
Real
)
*
(
tan
th2
: ( (
real
) (
V11
()
V12
()
real
)
number
)
)
: ( ( ) (
V11
()
V12
()
real
)
Real
)
)
: ( ( ) (
V11
()
V12
()
real
)
set
)
*
(
tan
th3
: ( (
real
) (
V11
()
V12
()
real
)
number
)
)
: ( ( ) (
V11
()
V12
()
real
)
Real
)
)
: ( ( ) (
V11
()
V12
()
real
)
set
)
)
: ( ( ) (
V11
()
V12
()
real
)
set
) : ( ( ) (
V11
()
V12
()
real
)
set
) ;
theorem
:: SIN_COS4:12
for
th1
,
th2
,
th3
being ( (
real
) (
V11
()
V12
()
real
)
number
) st
cos
th1
: ( (
real
) (
V11
()
V12
()
real
)
number
) : ( ( ) (
V11
()
V12
()
real
)
set
)
<>
0
: ( ( ) (
epsilon-transitive
epsilon-connected
ordinal
natural
V11
()
V12
()
real
V29
() )
M3
(
K28
() : ( ( ) ( )
set
) ,
K32
() : ( ( ) (
V1
()
epsilon-transitive
epsilon-connected
ordinal
)
M2
(
K6
(
K28
() : ( ( ) ( )
set
) ) : ( ( ) ( )
set
) )) )) &
cos
th2
: ( (
real
) (
V11
()
V12
()
real
)
number
) : ( ( ) (
V11
()
V12
()
real
)
set
)
<>
0
: ( ( ) (
epsilon-transitive
epsilon-connected
ordinal
natural
V11
()
V12
()
real
V29
() )
M3
(
K28
() : ( ( ) ( )
set
) ,
K32
() : ( ( ) (
V1
()
epsilon-transitive
epsilon-connected
ordinal
)
M2
(
K6
(
K28
() : ( ( ) ( )
set
) ) : ( ( ) ( )
set
) )) )) &
cos
th3
: ( (
real
) (
V11
()
V12
()
real
)
number
) : ( ( ) (
V11
()
V12
()
real
)
set
)
<>
0
: ( ( ) (
epsilon-transitive
epsilon-connected
ordinal
natural
V11
()
V12
()
real
V29
() )
M3
(
K28
() : ( ( ) ( )
set
) ,
K32
() : ( ( ) (
V1
()
epsilon-transitive
epsilon-connected
ordinal
)
M2
(
K6
(
K28
() : ( ( ) ( )
set
) ) : ( ( ) ( )
set
) )) )) holds
cos
(
(
th1
: ( (
real
) (
V11
()
V12
()
real
)
number
)
+
th2
: ( (
real
) (
V11
()
V12
()
real
)
number
)
)
: ( ( ) (
V11
()
V12
()
real
)
set
)
+
th3
: ( (
real
) (
V11
()
V12
()
real
)
number
)
)
: ( ( ) (
V11
()
V12
()
real
)
set
) : ( ( ) (
V11
()
V12
()
real
)
set
)
=
(
(
(
cos
th1
: ( (
real
) (
V11
()
V12
()
real
)
number
)
)
: ( ( ) (
V11
()
V12
()
real
)
set
)
*
(
cos
th2
: ( (
real
) (
V11
()
V12
()
real
)
number
)
)
: ( ( ) (
V11
()
V12
()
real
)
set
)
)
: ( ( ) (
V11
()
V12
()
real
)
set
)
*
(
cos
th3
: ( (
real
) (
V11
()
V12
()
real
)
number
)
)
: ( ( ) (
V11
()
V12
()
real
)
set
)
)
: ( ( ) (
V11
()
V12
()
real
)
set
)
*
(
(
(
1 : ( ( ) (
epsilon-transitive
epsilon-connected
ordinal
natural
V11
()
V12
()
real
V29
() )
M3
(
K28
() : ( ( ) ( )
set
) ,
K32
() : ( ( ) (
V1
()
epsilon-transitive
epsilon-connected
ordinal
)
M2
(
K6
(
K28
() : ( ( ) ( )
set
) ) : ( ( ) ( )
set
) )) ))
-
(
(
tan
th2
: ( (
real
) (
V11
()
V12
()
real
)
number
)
)
: ( ( ) (
V11
()
V12
()
real
)
Real
)
*
(
tan
th3
: ( (
real
) (
V11
()
V12
()
real
)
number
)
)
: ( ( ) (
V11
()
V12
()
real
)
Real
)
)
: ( ( ) (
V11
()
V12
()
real
)
set
)
)
: ( ( ) (
V11
()
V12
()
real
)
set
)
-
(
(
tan
th3
: ( (
real
) (
V11
()
V12
()
real
)
number
)
)
: ( ( ) (
V11
()
V12
()
real
)
Real
)
*
(
tan
th1
: ( (
real
) (
V11
()
V12
()
real
)
number
)
)
: ( ( ) (
V11
()
V12
()
real
)
Real
)
)
: ( ( ) (
V11
()
V12
()
real
)
set
)
)
: ( ( ) (
V11
()
V12
()
real
)
set
)
-
(
(
tan
th1
: ( (
real
) (
V11
()
V12
()
real
)
number
)
)
: ( ( ) (
V11
()
V12
()
real
)
Real
)
*
(
tan
th2
: ( (
real
) (
V11
()
V12
()
real
)
number
)
)
: ( ( ) (
V11
()
V12
()
real
)
Real
)
)
: ( ( ) (
V11
()
V12
()
real
)
set
)
)
: ( ( ) (
V11
()
V12
()
real
)
set
) : ( ( ) (
V11
()
V12
()
real
)
set
) ;
theorem
:: SIN_COS4:13
for
th1
,
th2
,
th3
being ( (
real
) (
V11
()
V12
()
real
)
number
) st
cos
th1
: ( (
real
) (
V11
()
V12
()
real
)
number
) : ( ( ) (
V11
()
V12
()
real
)
set
)
<>
0
: ( ( ) (
epsilon-transitive
epsilon-connected
ordinal
natural
V11
()
V12
()
real
V29
() )
M3
(
K28
() : ( ( ) ( )
set
) ,
K32
() : ( ( ) (
V1
()
epsilon-transitive
epsilon-connected
ordinal
)
M2
(
K6
(
K28
() : ( ( ) ( )
set
) ) : ( ( ) ( )
set
) )) )) &
cos
th2
: ( (
real
) (
V11
()
V12
()
real
)
number
) : ( ( ) (
V11
()
V12
()
real
)
set
)
<>
0
: ( ( ) (
epsilon-transitive
epsilon-connected
ordinal
natural
V11
()
V12
()
real
V29
() )
M3
(
K28
() : ( ( ) ( )
set
) ,
K32
() : ( ( ) (
V1
()
epsilon-transitive
epsilon-connected
ordinal
)
M2
(
K6
(
K28
() : ( ( ) ( )
set
) ) : ( ( ) ( )
set
) )) )) &
cos
th3
: ( (
real
) (
V11
()
V12
()
real
)
number
) : ( ( ) (
V11
()
V12
()
real
)
set
)
<>
0
: ( ( ) (
epsilon-transitive
epsilon-connected
ordinal
natural
V11
()
V12
()
real
V29
() )
M3
(
K28
() : ( ( ) ( )
set
) ,
K32
() : ( ( ) (
V1
()
epsilon-transitive
epsilon-connected
ordinal
)
M2
(
K6
(
K28
() : ( ( ) ( )
set
) ) : ( ( ) ( )
set
) )) )) holds
tan
(
(
th1
: ( (
real
) (
V11
()
V12
()
real
)
number
)
+
th2
: ( (
real
) (
V11
()
V12
()
real
)
number
)
)
: ( ( ) (
V11
()
V12
()
real
)
set
)
+
th3
: ( (
real
) (
V11
()
V12
()
real
)
number
)
)
: ( ( ) (
V11
()
V12
()
real
)
set
) : ( ( ) (
V11
()
V12
()
real
)
Real
)
=
(
(
(
(
tan
th1
: ( (
real
) (
V11
()
V12
()
real
)
number
)
)
: ( ( ) (
V11
()
V12
()
real
)
Real
)
+
(
tan
th2
: ( (
real
) (
V11
()
V12
()
real
)
number
)
)
: ( ( ) (
V11
()
V12
()
real
)
Real
)
)
: ( ( ) (
V11
()
V12
()
real
)
set
)
+
(
tan
th3
: ( (
real
) (
V11
()
V12
()
real
)
number
)
)
: ( ( ) (
V11
()
V12
()
real
)
Real
)
)
: ( ( ) (
V11
()
V12
()
real
)
set
)
-
(
(
(
tan
th1
: ( (
real
) (
V11
()
V12
()
real
)
number
)
)
: ( ( ) (
V11
()
V12
()
real
)
Real
)
*
(
tan
th2
: ( (
real
) (
V11
()
V12
()
real
)
number
)
)
: ( ( ) (
V11
()
V12
()
real
)
Real
)
)
: ( ( ) (
V11
()
V12
()
real
)
set
)
*
(
tan
th3
: ( (
real
) (
V11
()
V12
()
real
)
number
)
)
: ( ( ) (
V11
()
V12
()
real
)
Real
)
)
: ( ( ) (
V11
()
V12
()
real
)
set
)
)
: ( ( ) (
V11
()
V12
()
real
)
set
)
/
(
(
(
1 : ( ( ) (
epsilon-transitive
epsilon-connected
ordinal
natural
V11
()
V12
()
real
V29
() )
M3
(
K28
() : ( ( ) ( )
set
) ,
K32
() : ( ( ) (
V1
()
epsilon-transitive
epsilon-connected
ordinal
)
M2
(
K6
(
K28
() : ( ( ) ( )
set
) ) : ( ( ) ( )
set
) )) ))
-
(
(
tan
th2
: ( (
real
) (
V11
()
V12
()
real
)
number
)
)
: ( ( ) (
V11
()
V12
()
real
)
Real
)
*
(
tan
th3
: ( (
real
) (
V11
()
V12
()
real
)
number
)
)
: ( ( ) (
V11
()
V12
()
real
)
Real
)
)
: ( ( ) (
V11
()
V12
()
real
)
set
)
)
: ( ( ) (
V11
()
V12
()
real
)
set
)
-
(
(
tan
th3
: ( (
real
) (
V11
()
V12
()
real
)
number
)
)
: ( ( ) (
V11
()
V12
()
real
)
Real
)
*
(
tan
th1
: ( (
real
) (
V11
()
V12
()
real
)
number
)
)
: ( ( ) (
V11
()
V12
()
real
)
Real
)
)
: ( ( ) (
V11
()
V12
()
real
)
set
)
)
: ( ( ) (
V11
()
V12
()
real
)
set
)
-
(
(
tan
th1
: ( (
real
) (
V11
()
V12
()
real
)
number
)
)
: ( ( ) (
V11
()
V12
()
real
)
Real
)
*
(
tan
th2
: ( (
real
) (
V11
()
V12
()
real
)
number
)
)
: ( ( ) (
V11
()
V12
()
real
)
Real
)
)
: ( ( ) (
V11
()
V12
()
real
)
set
)
)
: ( ( ) (
V11
()
V12
()
real
)
set
) : ( ( ) (
V11
()
V12
()
real
)
set
) ;
theorem
:: SIN_COS4:14
for
th1
,
th2
,
th3
being ( (
real
) (
V11
()
V12
()
real
)
number
) st
sin
th1
: ( (
real
) (
V11
()
V12
()
real
)
number
) : ( ( ) (
V11
()
V12
()
real
)
set
)
<>
0
: ( ( ) (
epsilon-transitive
epsilon-connected
ordinal
natural
V11
()
V12
()
real
V29
() )
M3
(
K28
() : ( ( ) ( )
set
) ,
K32
() : ( ( ) (
V1
()
epsilon-transitive
epsilon-connected
ordinal
)
M2
(
K6
(
K28
() : ( ( ) ( )
set
) ) : ( ( ) ( )
set
) )) )) &
sin
th2
: ( (
real
) (
V11
()
V12
()
real
)
number
) : ( ( ) (
V11
()
V12
()
real
)
set
)
<>
0
: ( ( ) (
epsilon-transitive
epsilon-connected
ordinal
natural
V11
()
V12
()
real
V29
() )
M3
(
K28
() : ( ( ) ( )
set
) ,
K32
() : ( ( ) (
V1
()
epsilon-transitive
epsilon-connected
ordinal
)
M2
(
K6
(
K28
() : ( ( ) ( )
set
) ) : ( ( ) ( )
set
) )) )) &
sin
th3
: ( (
real
) (
V11
()
V12
()
real
)
number
) : ( ( ) (
V11
()
V12
()
real
)
set
)
<>
0
: ( ( ) (
epsilon-transitive
epsilon-connected
ordinal
natural
V11
()
V12
()
real
V29
() )
M3
(
K28
() : ( ( ) ( )
set
) ,
K32
() : ( ( ) (
V1
()
epsilon-transitive
epsilon-connected
ordinal
)
M2
(
K6
(
K28
() : ( ( ) ( )
set
) ) : ( ( ) ( )
set
) )) )) holds
cot
(
(
th1
: ( (
real
) (
V11
()
V12
()
real
)
number
)
+
th2
: ( (
real
) (
V11
()
V12
()
real
)
number
)
)
: ( ( ) (
V11
()
V12
()
real
)
set
)
+
th3
: ( (
real
) (
V11
()
V12
()
real
)
number
)
)
: ( ( ) (
V11
()
V12
()
real
)
set
) : ( ( ) (
V11
()
V12
()
real
)
Real
)
=
(
(
(
(
(
(
cot
th1
: ( (
real
) (
V11
()
V12
()
real
)
number
)
)
: ( ( ) (
V11
()
V12
()
real
)
Real
)
*
(
cot
th2
: ( (
real
) (
V11
()
V12
()
real
)
number
)
)
: ( ( ) (
V11
()
V12
()
real
)
Real
)
)
: ( ( ) (
V11
()
V12
()
real
)
set
)
*
(
cot
th3
: ( (
real
) (
V11
()
V12
()
real
)
number
)
)
: ( ( ) (
V11
()
V12
()
real
)
Real
)
)
: ( ( ) (
V11
()
V12
()
real
)
set
)
-
(
cot
th1
: ( (
real
) (
V11
()
V12
()
real
)
number
)
)
: ( ( ) (
V11
()
V12
()
real
)
Real
)
)
: ( ( ) (
V11
()
V12
()
real
)
set
)
-
(
cot
th2
: ( (
real
) (
V11
()
V12
()
real
)
number
)
)
: ( ( ) (
V11
()
V12
()
real
)
Real
)
)
: ( ( ) (
V11
()
V12
()
real
)
set
)
-
(
cot
th3
: ( (
real
) (
V11
()
V12
()
real
)
number
)
)
: ( ( ) (
V11
()
V12
()
real
)
Real
)
)
: ( ( ) (
V11
()
V12
()
real
)
set
)
/
(
(
(
(
(
cot
th2
: ( (
real
) (
V11
()
V12
()
real
)
number
)
)
: ( ( ) (
V11
()
V12
()
real
)
Real
)
*
(
cot
th3
: ( (
real
) (
V11
()
V12
()
real
)
number
)
)
: ( ( ) (
V11
()
V12
()
real
)
Real
)
)
: ( ( ) (
V11
()
V12
()
real
)
set
)
+
(
(
cot
th3
: ( (
real
) (
V11
()
V12
()
real
)
number
)
)
: ( ( ) (
V11
()
V12
()
real
)
Real
)
*
(
cot
th1
: ( (
real
) (
V11
()
V12
()
real
)
number
)
)
: ( ( ) (
V11
()
V12
()
real
)
Real
)
)
: ( ( ) (
V11
()
V12
()
real
)
set
)
)
: ( ( ) (
V11
()
V12
()
real
)
set
)
+
(
(
cot
th1
: ( (
real
) (
V11
()
V12
()
real
)
number
)
)
: ( ( ) (
V11
()
V12
()
real
)
Real
)
*
(
cot
th2
: ( (
real
) (
V11
()
V12
()
real
)
number
)
)
: ( ( ) (
V11
()
V12
()
real
)
Real
)
)
: ( ( ) (
V11
()
V12
()
real
)
set
)
)
: ( ( ) (
V11
()
V12
()
real
)
set
)
-
1 : ( ( ) (
epsilon-transitive
epsilon-connected
ordinal
natural
V11
()
V12
()
real
V29
() )
M3
(
K28
() : ( ( ) ( )
set
) ,
K32
() : ( ( ) (
V1
()
epsilon-transitive
epsilon-connected
ordinal
)
M2
(
K6
(
K28
() : ( ( ) ( )
set
) ) : ( ( ) ( )
set
) )) ))
)
: ( ( ) (
V11
()
V12
()
real
)
set
) : ( ( ) (
V11
()
V12
()
real
)
set
) ;
theorem
:: SIN_COS4:15
for
th1
,
th2
being ( (
real
) (
V11
()
V12
()
real
)
number
) holds
(
sin
th1
: ( (
real
) (
V11
()
V12
()
real
)
number
)
)
: ( ( ) (
V11
()
V12
()
real
)
set
)
+
(
sin
th2
: ( (
real
) (
V11
()
V12
()
real
)
number
)
)
: ( ( ) (
V11
()
V12
()
real
)
set
) : ( ( ) (
V11
()
V12
()
real
)
set
)
=
2 : ( ( ) (
epsilon-transitive
epsilon-connected
ordinal
natural
V11
()
V12
()
real
V29
() )
M3
(
K28
() : ( ( ) ( )
set
) ,
K32
() : ( ( ) (
V1
()
epsilon-transitive
epsilon-connected
ordinal
)
M2
(
K6
(
K28
() : ( ( ) ( )
set
) ) : ( ( ) ( )
set
) )) ))
*
(
(
cos
(
(
th1
: ( (
real
) (
V11
()
V12
()
real
)
number
)
-
th2
: ( (
real
) (
V11
()
V12
()
real
)
number
)
)
: ( ( ) (
V11
()
V12
()
real
)
set
)
/
2 : ( ( ) (
epsilon-transitive
epsilon-connected
ordinal
natural
V11
()
V12
()
real
V29
() )
M3
(
K28
() : ( ( ) ( )
set
) ,
K32
() : ( ( ) (
V1
()
epsilon-transitive
epsilon-connected
ordinal
)
M2
(
K6
(
K28
() : ( ( ) ( )
set
) ) : ( ( ) ( )
set
) )) ))
)
: ( ( ) (
V11
()
V12
()
real
)
set
)
)
: ( ( ) (
V11
()
V12
()
real
)
set
)
*
(
sin
(
(
th1
: ( (
real
) (
V11
()
V12
()
real
)
number
)
+
th2
: ( (
real
) (
V11
()
V12
()
real
)
number
)
)
: ( ( ) (
V11
()
V12
()
real
)
set
)
/
2 : ( ( ) (
epsilon-transitive
epsilon-connected
ordinal
natural
V11
()
V12
()
real
V29
() )
M3
(
K28
() : ( ( ) ( )
set
) ,
K32
() : ( ( ) (
V1
()
epsilon-transitive
epsilon-connected
ordinal
)
M2
(
K6
(
K28
() : ( ( ) ( )
set
) ) : ( ( ) ( )
set
) )) ))
)
: ( ( ) (
V11
()
V12
()
real
)
set
)
)
: ( ( ) (
V11
()
V12
()
real
)
set
)
)
: ( ( ) (
V11
()
V12
()
real
)
set
) : ( ( ) (
V11
()
V12
()
real
)
set
) ;
theorem
:: SIN_COS4:16
for
th1
,
th2
being ( (
real
) (
V11
()
V12
()
real
)
number
) holds
(
sin
th1
: ( (
real
) (
V11
()
V12
()
real
)
number
)
)
: ( ( ) (
V11
()
V12
()
real
)
set
)
-
(
sin
th2
: ( (
real
) (
V11
()
V12
()
real
)
number
)
)
: ( ( ) (
V11
()
V12
()
real
)
set
) : ( ( ) (
V11
()
V12
()
real
)
set
)
=
2 : ( ( ) (
epsilon-transitive
epsilon-connected
ordinal
natural
V11
()
V12
()
real
V29
() )
M3
(
K28
() : ( ( ) ( )
set
) ,
K32
() : ( ( ) (
V1
()
epsilon-transitive
epsilon-connected
ordinal
)
M2
(
K6
(
K28
() : ( ( ) ( )
set
) ) : ( ( ) ( )
set
) )) ))
*
(
(
cos
(
(
th1
: ( (
real
) (
V11
()
V12
()
real
)
number
)
+
th2
: ( (
real
) (
V11
()
V12
()
real
)
number
)
)
: ( ( ) (
V11
()
V12
()
real
)
set
)
/
2 : ( ( ) (
epsilon-transitive
epsilon-connected
ordinal
natural
V11
()
V12
()
real
V29
() )
M3
(
K28
() : ( ( ) ( )
set
) ,
K32
() : ( ( ) (
V1
()
epsilon-transitive
epsilon-connected
ordinal
)
M2
(
K6
(
K28
() : ( ( ) ( )
set
) ) : ( ( ) ( )
set
) )) ))
)
: ( ( ) (
V11
()
V12
()
real
)
set
)
)
: ( ( ) (
V11
()
V12
()
real
)
set
)
*
(
sin
(
(
th1
: ( (
real
) (
V11
()
V12
()
real
)
number
)
-
th2
: ( (
real
) (
V11
()
V12
()
real
)
number
)
)
: ( ( ) (
V11
()
V12
()
real
)
set
)
/
2 : ( ( ) (
epsilon-transitive
epsilon-connected
ordinal
natural
V11
()
V12
()
real
V29
() )
M3
(
K28
() : ( ( ) ( )
set
) ,
K32
() : ( ( ) (
V1
()
epsilon-transitive
epsilon-connected
ordinal
)
M2
(
K6
(
K28
() : ( ( ) ( )
set
) ) : ( ( ) ( )
set
) )) ))
)
: ( ( ) (
V11
()
V12
()
real
)
set
)
)
: ( ( ) (
V11
()
V12
()
real
)
set
)
)
: ( ( ) (
V11
()
V12
()
real
)
set
) : ( ( ) (
V11
()
V12
()
real
)
set
) ;
theorem
:: SIN_COS4:17
for
th1
,
th2
being ( (
real
) (
V11
()
V12
()
real
)
number
) holds
(
cos
th1
: ( (
real
) (
V11
()
V12
()
real
)
number
)
)
: ( ( ) (
V11
()
V12
()
real
)
set
)
+
(
cos
th2
: ( (
real
) (
V11
()
V12
()
real
)
number
)
)
: ( ( ) (
V11
()
V12
()
real
)
set
) : ( ( ) (
V11
()
V12
()
real
)
set
)
=
2 : ( ( ) (
epsilon-transitive
epsilon-connected
ordinal
natural
V11
()
V12
()
real
V29
() )
M3
(
K28
() : ( ( ) ( )
set
) ,
K32
() : ( ( ) (
V1
()
epsilon-transitive
epsilon-connected
ordinal
)
M2
(
K6
(
K28
() : ( ( ) ( )
set
) ) : ( ( ) ( )
set
) )) ))
*
(
(
cos
(
(
th1
: ( (
real
) (
V11
()
V12
()
real
)
number
)
+
th2
: ( (
real
) (
V11
()
V12
()
real
)
number
)
)
: ( ( ) (
V11
()
V12
()
real
)
set
)
/
2 : ( ( ) (
epsilon-transitive
epsilon-connected
ordinal
natural
V11
()
V12
()
real
V29
() )
M3
(
K28
() : ( ( ) ( )
set
) ,
K32
() : ( ( ) (
V1
()
epsilon-transitive
epsilon-connected
ordinal
)
M2
(
K6
(
K28
() : ( ( ) ( )
set
) ) : ( ( ) ( )
set
) )) ))
)
: ( ( ) (
V11
()
V12
()
real
)
set
)
)
: ( ( ) (
V11
()
V12
()
real
)
set
)
*
(
cos
(
(
th1
: ( (
real
) (
V11
()
V12
()
real
)
number
)
-
th2
: ( (
real
) (
V11
()
V12
()
real
)
number
)
)
: ( ( ) (
V11
()
V12
()
real
)
set
)
/
2 : ( ( ) (
epsilon-transitive
epsilon-connected
ordinal
natural
V11
()
V12
()
real
V29
() )
M3
(
K28
() : ( ( ) ( )
set
) ,
K32
() : ( ( ) (
V1
()
epsilon-transitive
epsilon-connected
ordinal
)
M2
(
K6
(
K28
() : ( ( ) ( )
set
) ) : ( ( ) ( )
set
) )) ))
)
: ( ( ) (
V11
()
V12
()
real
)
set
)
)
: ( ( ) (
V11
()
V12
()
real
)
set
)
)
: ( ( ) (
V11
()
V12
()
real
)
set
) : ( ( ) (
V11
()
V12
()
real
)
set
) ;
theorem
:: SIN_COS4:18
for
th1
,
th2
being ( (
real
) (
V11
()
V12
()
real
)
number
) holds
(
cos
th1
: ( (
real
) (
V11
()
V12
()
real
)
number
)
)
: ( ( ) (
V11
()
V12
()
real
)
set
)
-
(
cos
th2
: ( (
real
) (
V11
()
V12
()
real
)
number
)
)
: ( ( ) (
V11
()
V12
()
real
)
set
) : ( ( ) (
V11
()
V12
()
real
)
set
)
=
-
(
2 : ( ( ) (
epsilon-transitive
epsilon-connected
ordinal
natural
V11
()
V12
()
real
V29
() )
M3
(
K28
() : ( ( ) ( )
set
) ,
K32
() : ( ( ) (
V1
()
epsilon-transitive
epsilon-connected
ordinal
)
M2
(
K6
(
K28
() : ( ( ) ( )
set
) ) : ( ( ) ( )
set
) )) ))
*
(
(
sin
(
(
th1
: ( (
real
) (
V11
()
V12
()
real
)
number
)
+
th2
: ( (
real
) (
V11
()
V12
()
real
)
number
)
)
: ( ( ) (
V11
()
V12
()
real
)
set
)
/
2 : ( ( ) (
epsilon-transitive
epsilon-connected
ordinal
natural
V11
()
V12
()
real
V29
() )
M3
(
K28
() : ( ( ) ( )
set
) ,
K32
() : ( ( ) (
V1
()
epsilon-transitive
epsilon-connected
ordinal
)
M2
(
K6
(
K28
() : ( ( ) ( )
set
) ) : ( ( ) ( )
set
) )) ))
)
: ( ( ) (
V11
()
V12
()
real
)
set
)
)
: ( ( ) (
V11
()
V12
()
real
)
set
)
*
(
sin
(
(
th1
: ( (
real
) (
V11
()
V12
()
real
)
number
)
-
th2
: ( (
real
) (
V11
()
V12
()
real
)
number
)
)
: ( ( ) (
V11
()
V12
()
real
)
set
)
/
2 : ( ( ) (
epsilon-transitive
epsilon-connected
ordinal
natural
V11
()
V12
()
real
V29
() )
M3
(
K28
() : ( ( ) ( )
set
) ,
K32
() : ( ( ) (
V1
()
epsilon-transitive
epsilon-connected
ordinal
)
M2
(
K6
(
K28
() : ( ( ) ( )
set
) ) : ( ( ) ( )
set
) )) ))
)
: ( ( ) (
V11
()
V12
()
real
)
set
)
)
: ( ( ) (
V11
()
V12
()
real
)
set
)
)
: ( ( ) (
V11
()
V12
()
real
)
set
)
)
: ( ( ) (
V11
()
V12
()
real
)
set
) : ( (
V11
() ) (
V11
()
V12
()
real
)
set
) ;
theorem
:: SIN_COS4:19
for
th1
,
th2
being ( (
real
) (
V11
()
V12
()
real
)
number
) st
cos
th1
: ( (
real
) (
V11
()
V12
()
real
)
number
) : ( ( ) (
V11
()
V12
()
real
)
set
)
<>
0
: ( ( ) (
epsilon-transitive
epsilon-connected
ordinal
natural
V11
()
V12
()
real
V29
() )
M3
(
K28
() : ( ( ) ( )
set
) ,
K32
() : ( ( ) (
V1
()
epsilon-transitive
epsilon-connected
ordinal
)
M2
(
K6
(
K28
() : ( ( ) ( )
set
) ) : ( ( ) ( )
set
) )) )) &
cos
th2
: ( (
real
) (
V11
()
V12
()
real
)
number
) : ( ( ) (
V11
()
V12
()
real
)
set
)
<>
0
: ( ( ) (
epsilon-transitive
epsilon-connected
ordinal
natural
V11
()
V12
()
real
V29
() )
M3
(
K28
() : ( ( ) ( )
set
) ,
K32
() : ( ( ) (
V1
()
epsilon-transitive
epsilon-connected
ordinal
)
M2
(
K6
(
K28
() : ( ( ) ( )
set
) ) : ( ( ) ( )
set
) )) )) holds
(
tan
th1
: ( (
real
) (
V11
()
V12
()
real
)
number
)
)
: ( ( ) (
V11
()
V12
()
real
)
Real
)
+
(
tan
th2
: ( (
real
) (
V11
()
V12
()
real
)
number
)
)
: ( ( ) (
V11
()
V12
()
real
)
Real
) : ( ( ) (
V11
()
V12
()
real
)
set
)
=
(
sin
(
th1
: ( (
real
) (
V11
()
V12
()
real
)
number
)
+
th2
: ( (
real
) (
V11
()
V12
()
real
)
number
)
)
: ( ( ) (
V11
()
V12
()
real
)
set
)
)
: ( ( ) (
V11
()
V12
()
real
)
set
)
/
(
(
cos
th1
: ( (
real
) (
V11
()
V12
()
real
)
number
)
)
: ( ( ) (
V11
()
V12
()
real
)
set
)
*
(
cos
th2
: ( (
real
) (
V11
()
V12
()
real
)
number
)
)
: ( ( ) (
V11
()
V12
()
real
)
set
)
)
: ( ( ) (
V11
()
V12
()
real
)
set
) : ( ( ) (
V11
()
V12
()
real
)
set
) ;
theorem
:: SIN_COS4:20
for
th1
,
th2
being ( (
real
) (
V11
()
V12
()
real
)
number
) st
cos
th1
: ( (
real
) (
V11
()
V12
()
real
)
number
) : ( ( ) (
V11
()
V12
()
real
)
set
)
<>
0
: ( ( ) (
epsilon-transitive
epsilon-connected
ordinal
natural
V11
()
V12
()
real
V29
() )
M3
(
K28
() : ( ( ) ( )
set
) ,
K32
() : ( ( ) (
V1
()
epsilon-transitive
epsilon-connected
ordinal
)
M2
(
K6
(
K28
() : ( ( ) ( )
set
) ) : ( ( ) ( )
set
) )) )) &
cos
th2
: ( (
real
) (
V11
()
V12
()
real
)
number
) : ( ( ) (
V11
()
V12
()
real
)
set
)
<>
0
: ( ( ) (
epsilon-transitive
epsilon-connected
ordinal
natural
V11
()
V12
()
real
V29
() )
M3
(
K28
() : ( ( ) ( )
set
) ,
K32
() : ( ( ) (
V1
()
epsilon-transitive
epsilon-connected
ordinal
)
M2
(
K6
(
K28
() : ( ( ) ( )
set
) ) : ( ( ) ( )
set
) )) )) holds
(
tan
th1
: ( (
real
) (
V11
()
V12
()
real
)
number
)
)
: ( ( ) (
V11
()
V12
()
real
)
Real
)
-
(
tan
th2
: ( (
real
) (
V11
()
V12
()
real
)
number
)
)
: ( ( ) (
V11
()
V12
()
real
)
Real
) : ( ( ) (
V11
()
V12
()
real
)
set
)
=
(
sin
(
th1
: ( (
real
) (
V11
()
V12
()
real
)
number
)
-
th2
: ( (
real
) (
V11
()
V12
()
real
)
number
)
)
: ( ( ) (
V11
()
V12
()
real
)
set
)
)
: ( ( ) (
V11
()
V12
()
real
)
set
)
/
(
(
cos
th1
: ( (
real
) (
V11
()
V12
()
real
)
number
)
)
: ( ( ) (
V11
()
V12
()
real
)
set
)
*
(
cos
th2
: ( (
real
) (
V11
()
V12
()
real
)
number
)
)
: ( ( ) (
V11
()
V12
()
real
)
set
)
)
: ( ( ) (
V11
()
V12
()
real
)
set
) : ( ( ) (
V11
()
V12
()
real
)
set
) ;
theorem
:: SIN_COS4:21
for
th1
,
th2
being ( (
real
) (
V11
()
V12
()
real
)
number
) st
cos
th1
: ( (
real
) (
V11
()
V12
()
real
)
number
) : ( ( ) (
V11
()
V12
()
real
)
set
)
<>
0
: ( ( ) (
epsilon-transitive
epsilon-connected
ordinal
natural
V11
()
V12
()
real
V29
() )
M3
(
K28
() : ( ( ) ( )
set
) ,
K32
() : ( ( ) (
V1
()
epsilon-transitive
epsilon-connected
ordinal
)
M2
(
K6
(
K28
() : ( ( ) ( )
set
) ) : ( ( ) ( )
set
) )) )) &
sin
th2
: ( (
real
) (
V11
()
V12
()
real
)
number
) : ( ( ) (
V11
()
V12
()
real
)
set
)
<>
0
: ( ( ) (
epsilon-transitive
epsilon-connected
ordinal
natural
V11
()
V12
()
real
V29
() )
M3
(
K28
() : ( ( ) ( )
set
) ,
K32
() : ( ( ) (
V1
()
epsilon-transitive
epsilon-connected
ordinal
)
M2
(
K6
(
K28
() : ( ( ) ( )
set
) ) : ( ( ) ( )
set
) )) )) holds
(
tan
th1
: ( (
real
) (
V11
()
V12
()
real
)
number
)
)
: ( ( ) (
V11
()
V12
()
real
)
Real
)
+
(
cot
th2
: ( (
real
) (
V11
()
V12
()
real
)
number
)
)
: ( ( ) (
V11
()
V12
()
real
)
Real
) : ( ( ) (
V11
()
V12
()
real
)
set
)
=
(
cos
(
th1
: ( (
real
) (
V11
()
V12
()
real
)
number
)
-
th2
: ( (
real
) (
V11
()
V12
()
real
)
number
)
)
: ( ( ) (
V11
()
V12
()
real
)
set
)
)
: ( ( ) (
V11
()
V12
()
real
)
set
)
/
(
(
cos
th1
: ( (
real
) (
V11
()
V12
()
real
)
number
)
)
: ( ( ) (
V11
()
V12
()
real
)
set
)
*
(
sin
th2
: ( (
real
) (
V11
()
V12
()
real
)
number
)
)
: ( ( ) (
V11
()
V12
()
real
)
set
)
)
: ( ( ) (
V11
()
V12
()
real
)
set
) : ( ( ) (
V11
()
V12
()
real
)
set
) ;
theorem
:: SIN_COS4:22
for
th1
,
th2
being ( (
real
) (
V11
()
V12
()
real
)
number
) st
cos
th1
: ( (
real
) (
V11
()
V12
()
real
)
number
) : ( ( ) (
V11
()
V12
()
real
)
set
)
<>
0
: ( ( ) (
epsilon-transitive
epsilon-connected
ordinal
natural
V11
()
V12
()
real
V29
() )
M3
(
K28
() : ( ( ) ( )
set
) ,
K32
() : ( ( ) (
V1
()
epsilon-transitive
epsilon-connected
ordinal
)
M2
(
K6
(
K28
() : ( ( ) ( )
set
) ) : ( ( ) ( )
set
) )) )) &
sin
th2
: ( (
real
) (
V11
()
V12
()
real
)
number
) : ( ( ) (
V11
()
V12
()
real
)
set
)
<>
0
: ( ( ) (
epsilon-transitive
epsilon-connected
ordinal
natural
V11
()
V12
()
real
V29
() )
M3
(
K28
() : ( ( ) ( )
set
) ,
K32
() : ( ( ) (
V1
()
epsilon-transitive
epsilon-connected
ordinal
)
M2
(
K6
(
K28
() : ( ( ) ( )
set
) ) : ( ( ) ( )
set
) )) )) holds
(
tan
th1
: ( (
real
) (
V11
()
V12
()
real
)
number
)
)
: ( ( ) (
V11
()
V12
()
real
)
Real
)
-
(
cot
th2
: ( (
real
) (
V11
()
V12
()
real
)
number
)
)
: ( ( ) (
V11
()
V12
()
real
)
Real
) : ( ( ) (
V11
()
V12
()
real
)
set
)
=
-
(
(
cos
(
th1
: ( (
real
) (
V11
()
V12
()
real
)
number
)
+
th2
: ( (
real
) (
V11
()
V12
()
real
)
number
)
)
: ( ( ) (
V11
()
V12
()
real
)
set
)
)
: ( ( ) (
V11
()
V12
()
real
)
set
)
/
(
(
cos
th1
: ( (
real
) (
V11
()
V12
()
real
)
number
)
)
: ( ( ) (
V11
()
V12
()
real
)
set
)
*
(
sin
th2
: ( (
real
) (
V11
()
V12
()
real
)
number
)
)
: ( ( ) (
V11
()
V12
()
real
)
set
)
)
: ( ( ) (
V11
()
V12
()
real
)
set
)
)
: ( ( ) (
V11
()
V12
()
real
)
set
) : ( (
V11
() ) (
V11
()
V12
()
real
)
set
) ;
theorem
:: SIN_COS4:23
for
th1
,
th2
being ( (
real
) (
V11
()
V12
()
real
)
number
) st
sin
th1
: ( (
real
) (
V11
()
V12
()
real
)
number
) : ( ( ) (
V11
()
V12
()
real
)
set
)
<>
0
: ( ( ) (
epsilon-transitive
epsilon-connected
ordinal
natural
V11
()
V12
()
real
V29
() )
M3
(
K28
() : ( ( ) ( )
set
) ,
K32
() : ( ( ) (
V1
()
epsilon-transitive
epsilon-connected
ordinal
)
M2
(
K6
(
K28
() : ( ( ) ( )
set
) ) : ( ( ) ( )
set
) )) )) &
sin
th2
: ( (
real
) (
V11
()
V12
()
real
)
number
) : ( ( ) (
V11
()
V12
()
real
)
set
)
<>
0
: ( ( ) (
epsilon-transitive
epsilon-connected
ordinal
natural
V11
()
V12
()
real
V29
() )
M3
(
K28
() : ( ( ) ( )
set
) ,
K32
() : ( ( ) (
V1
()
epsilon-transitive
epsilon-connected
ordinal
)
M2
(
K6
(
K28
() : ( ( ) ( )
set
) ) : ( ( ) ( )
set
) )) )) holds
(
cot
th1
: ( (
real
) (
V11
()
V12
()
real
)
number
)
)
: ( ( ) (
V11
()
V12
()
real
)
Real
)
+
(
cot
th2
: ( (
real
) (
V11
()
V12
()
real
)
number
)
)
: ( ( ) (
V11
()
V12
()
real
)
Real
) : ( ( ) (
V11
()
V12
()
real
)
set
)
=
(
sin
(
th1
: ( (
real
) (
V11
()
V12
()
real
)
number
)
+
th2
: ( (
real
) (
V11
()
V12
()
real
)
number
)
)
: ( ( ) (
V11
()
V12
()
real
)
set
)
)
: ( ( ) (
V11
()
V12
()
real
)
set
)
/
(
(
sin
th1
: ( (
real
) (
V11
()
V12
()
real
)
number
)
)
: ( ( ) (
V11
()
V12
()
real
)
set
)
*
(
sin
th2
: ( (
real
) (
V11
()
V12
()
real
)
number
)
)
: ( ( ) (
V11
()
V12
()
real
)
set
)
)
: ( ( ) (
V11
()
V12
()
real
)
set
) : ( ( ) (
V11
()
V12
()
real
)
set
) ;
theorem
:: SIN_COS4:24
for
th1
,
th2
being ( (
real
) (
V11
()
V12
()
real
)
number
) st
sin
th1
: ( (
real
) (
V11
()
V12
()
real
)
number
) : ( ( ) (
V11
()
V12
()
real
)
set
)
<>
0
: ( ( ) (
epsilon-transitive
epsilon-connected
ordinal
natural
V11
()
V12
()
real
V29
() )
M3
(
K28
() : ( ( ) ( )
set
) ,
K32
() : ( ( ) (
V1
()
epsilon-transitive
epsilon-connected
ordinal
)
M2
(
K6
(
K28
() : ( ( ) ( )
set
) ) : ( ( ) ( )
set
) )) )) &
sin
th2
: ( (
real
) (
V11
()
V12
()
real
)
number
) : ( ( ) (
V11
()
V12
()
real
)
set
)
<>
0
: ( ( ) (
epsilon-transitive
epsilon-connected
ordinal
natural
V11
()
V12
()
real
V29
() )
M3
(
K28
() : ( ( ) ( )
set
) ,
K32
() : ( ( ) (
V1
()
epsilon-transitive
epsilon-connected
ordinal
)
M2
(
K6
(
K28
() : ( ( ) ( )
set
) ) : ( ( ) ( )
set
) )) )) holds
(
cot
th1
: ( (
real
) (
V11
()
V12
()
real
)
number
)
)
: ( ( ) (
V11
()
V12
()
real
)
Real
)
-
(
cot
th2
: ( (
real
) (
V11
()
V12
()
real
)
number
)
)
: ( ( ) (
V11
()
V12
()
real
)
Real
) : ( ( ) (
V11
()
V12
()
real
)
set
)
=
-
(
(
sin
(
th1
: ( (
real
) (
V11
()
V12
()
real
)
number
)
-
th2
: ( (
real
) (
V11
()
V12
()
real
)
number
)
)
: ( ( ) (
V11
()
V12
()
real
)
set
)
)
: ( ( ) (
V11
()
V12
()
real
)
set
)
/
(
(
sin
th1
: ( (
real
) (
V11
()
V12
()
real
)
number
)
)
: ( ( ) (
V11
()
V12
()
real
)
set
)
*
(
sin
th2
: ( (
real
) (
V11
()
V12
()
real
)
number
)
)
: ( ( ) (
V11
()
V12
()
real
)
set
)
)
: ( ( ) (
V11
()
V12
()
real
)
set
)
)
: ( ( ) (
V11
()
V12
()
real
)
set
) : ( (
V11
() ) (
V11
()
V12
()
real
)
set
) ;
theorem
:: SIN_COS4:25
for
th1
,
th2
being ( (
real
) (
V11
()
V12
()
real
)
number
) holds
(
sin
(
th1
: ( (
real
) (
V11
()
V12
()
real
)
number
)
+
th2
: ( (
real
) (
V11
()
V12
()
real
)
number
)
)
: ( ( ) (
V11
()
V12
()
real
)
set
)
)
: ( ( ) (
V11
()
V12
()
real
)
set
)
+
(
sin
(
th1
: ( (
real
) (
V11
()
V12
()
real
)
number
)
-
th2
: ( (
real
) (
V11
()
V12
()
real
)
number
)
)
: ( ( ) (
V11
()
V12
()
real
)
set
)
)
: ( ( ) (
V11
()
V12
()
real
)
set
) : ( ( ) (
V11
()
V12
()
real
)
set
)
=
2 : ( ( ) (
epsilon-transitive
epsilon-connected
ordinal
natural
V11
()
V12
()
real
V29
() )
M3
(
K28
() : ( ( ) ( )
set
) ,
K32
() : ( ( ) (
V1
()
epsilon-transitive
epsilon-connected
ordinal
)
M2
(
K6
(
K28
() : ( ( ) ( )
set
) ) : ( ( ) ( )
set
) )) ))
*
(
(
sin
th1
: ( (
real
) (
V11
()
V12
()
real
)
number
)
)
: ( ( ) (
V11
()
V12
()
real
)
set
)
*
(
cos
th2
: ( (
real
) (
V11
()
V12
()
real
)
number
)
)
: ( ( ) (
V11
()
V12
()
real
)
set
)
)
: ( ( ) (
V11
()
V12
()
real
)
set
) : ( ( ) (
V11
()
V12
()
real
)
set
) ;
theorem
:: SIN_COS4:26
for
th1
,
th2
being ( (
real
) (
V11
()
V12
()
real
)
number
) holds
(
sin
(
th1
: ( (
real
) (
V11
()
V12
()
real
)
number
)
+
th2
: ( (
real
) (
V11
()
V12
()
real
)
number
)
)
: ( ( ) (
V11
()
V12
()
real
)
set
)
)
: ( ( ) (
V11
()
V12
()
real
)
set
)
-
(
sin
(
th1
: ( (
real
) (
V11
()
V12
()
real
)
number
)
-
th2
: ( (
real
) (
V11
()
V12
()
real
)
number
)
)
: ( ( ) (
V11
()
V12
()
real
)
set
)
)
: ( ( ) (
V11
()
V12
()
real
)
set
) : ( ( ) (
V11
()
V12
()
real
)
set
)
=
2 : ( ( ) (
epsilon-transitive
epsilon-connected
ordinal
natural
V11
()
V12
()
real
V29
() )
M3
(
K28
() : ( ( ) ( )
set
) ,
K32
() : ( ( ) (
V1
()
epsilon-transitive
epsilon-connected
ordinal
)
M2
(
K6
(
K28
() : ( ( ) ( )
set
) ) : ( ( ) ( )
set
) )) ))
*
(
(
cos
th1
: ( (
real
) (
V11
()
V12
()
real
)
number
)
)
: ( ( ) (
V11
()
V12
()
real
)
set
)
*
(
sin
th2
: ( (
real
) (
V11
()
V12
()
real
)
number
)
)
: ( ( ) (
V11
()
V12
()
real
)
set
)
)
: ( ( ) (
V11
()
V12
()
real
)
set
) : ( ( ) (
V11
()
V12
()
real
)
set
) ;
theorem
:: SIN_COS4:27
for
th1
,
th2
being ( (
real
) (
V11
()
V12
()
real
)
number
) holds
(
cos
(
th1
: ( (
real
) (
V11
()
V12
()
real
)
number
)
+
th2
: ( (
real
) (
V11
()
V12
()
real
)
number
)
)
: ( ( ) (
V11
()
V12
()
real
)
set
)
)
: ( ( ) (
V11
()
V12
()
real
)
set
)
+
(
cos
(
th1
: ( (
real
) (
V11
()
V12
()
real
)
number
)
-
th2
: ( (
real
) (
V11
()
V12
()
real
)
number
)
)
: ( ( ) (
V11
()
V12
()
real
)
set
)
)
: ( ( ) (
V11
()
V12
()
real
)
set
) : ( ( ) (
V11
()
V12
()
real
)
set
)
=
2 : ( ( ) (
epsilon-transitive
epsilon-connected
ordinal
natural
V11
()
V12
()
real
V29
() )
M3
(
K28
() : ( ( ) ( )
set
) ,
K32
() : ( ( ) (
V1
()
epsilon-transitive
epsilon-connected
ordinal
)
M2
(
K6
(
K28
() : ( ( ) ( )
set
) ) : ( ( ) ( )
set
) )) ))
*
(
(
cos
th1
: ( (
real
) (
V11
()
V12
()
real
)
number
)
)
: ( ( ) (
V11
()
V12
()
real
)
set
)
*
(
cos
th2
: ( (
real
) (
V11
()
V12
()
real
)
number
)
)
: ( ( ) (
V11
()
V12
()
real
)
set
)
)
: ( ( ) (
V11
()
V12
()
real
)
set
) : ( ( ) (
V11
()
V12
()
real
)
set
) ;
theorem
:: SIN_COS4:28
for
th1
,
th2
being ( (
real
) (
V11
()
V12
()
real
)
number
) holds
(
cos
(
th1
: ( (
real
) (
V11
()
V12
()
real
)
number
)
+
th2
: ( (
real
) (
V11
()
V12
()
real
)
number
)
)
: ( ( ) (
V11
()
V12
()
real
)
set
)
)
: ( ( ) (
V11
()
V12
()
real
)
set
)
-
(
cos
(
th1
: ( (
real
) (
V11
()
V12
()
real
)
number
)
-
th2
: ( (
real
) (
V11
()
V12
()
real
)
number
)
)
: ( ( ) (
V11
()
V12
()
real
)
set
)
)
: ( ( ) (
V11
()
V12
()
real
)
set
) : ( ( ) (
V11
()
V12
()
real
)
set
)
=
-
(
2 : ( ( ) (
epsilon-transitive
epsilon-connected
ordinal
natural
V11
()
V12
()
real
V29
() )
M3
(
K28
() : ( ( ) ( )
set
) ,
K32
() : ( ( ) (
V1
()
epsilon-transitive
epsilon-connected
ordinal
)
M2
(
K6
(
K28
() : ( ( ) ( )
set
) ) : ( ( ) ( )
set
) )) ))
*
(
(
sin
th1
: ( (
real
) (
V11
()
V12
()
real
)
number
)
)
: ( ( ) (
V11
()
V12
()
real
)
set
)
*
(
sin
th2
: ( (
real
) (
V11
()
V12
()
real
)
number
)
)
: ( ( ) (
V11
()
V12
()
real
)
set
)
)
: ( ( ) (
V11
()
V12
()
real
)
set
)
)
: ( ( ) (
V11
()
V12
()
real
)
set
) : ( (
V11
() ) (
V11
()
V12
()
real
)
set
) ;
theorem
:: SIN_COS4:29
for
th1
,
th2
being ( (
real
) (
V11
()
V12
()
real
)
number
) holds
(
sin
th1
: ( (
real
) (
V11
()
V12
()
real
)
number
)
)
: ( ( ) (
V11
()
V12
()
real
)
set
)
*
(
sin
th2
: ( (
real
) (
V11
()
V12
()
real
)
number
)
)
: ( ( ) (
V11
()
V12
()
real
)
set
) : ( ( ) (
V11
()
V12
()
real
)
set
)
=
-
(
(
1 : ( ( ) (
epsilon-transitive
epsilon-connected
ordinal
natural
V11
()
V12
()
real
V29
() )
M3
(
K28
() : ( ( ) ( )
set
) ,
K32
() : ( ( ) (
V1
()
epsilon-transitive
epsilon-connected
ordinal
)
M2
(
K6
(
K28
() : ( ( ) ( )
set
) ) : ( ( ) ( )
set
) )) ))
/
2 : ( ( ) (
epsilon-transitive
epsilon-connected
ordinal
natural
V11
()
V12
()
real
V29
() )
M3
(
K28
() : ( ( ) ( )
set
) ,
K32
() : ( ( ) (
V1
()
epsilon-transitive
epsilon-connected
ordinal
)
M2
(
K6
(
K28
() : ( ( ) ( )
set
) ) : ( ( ) ( )
set
) )) ))
)
: ( ( ) (
V11
()
V12
()
real
)
set
)
*
(
(
cos
(
th1
: ( (
real
) (
V11
()
V12
()
real
)
number
)
+
th2
: ( (
real
) (
V11
()
V12
()
real
)
number
)
)
: ( ( ) (
V11
()
V12
()
real
)
set
)
)
: ( ( ) (
V11
()
V12
()
real
)
set
)
-
(
cos
(
th1
: ( (
real
) (
V11
()
V12
()
real
)
number
)
-
th2
: ( (
real
) (
V11
()
V12
()
real
)
number
)
)
: ( ( ) (
V11
()
V12
()
real
)
set
)
)
: ( ( ) (
V11
()
V12
()
real
)
set
)
)
: ( ( ) (
V11
()
V12
()
real
)
set
)
)
: ( ( ) (
V11
()
V12
()
real
)
set
) : ( (
V11
() ) (
V11
()
V12
()
real
)
set
) ;
theorem
:: SIN_COS4:30
for
th1
,
th2
being ( (
real
) (
V11
()
V12
()
real
)
number
) holds
(
sin
th1
: ( (
real
) (
V11
()
V12
()
real
)
number
)
)
: ( ( ) (
V11
()
V12
()
real
)
set
)
*
(
cos
th2
: ( (
real
) (
V11
()
V12
()
real
)
number
)
)
: ( ( ) (
V11
()
V12
()
real
)
set
) : ( ( ) (
V11
()
V12
()
real
)
set
)
=
(
1 : ( ( ) (
epsilon-transitive
epsilon-connected
ordinal
natural
V11
()
V12
()
real
V29
() )
M3
(
K28
() : ( ( ) ( )
set
) ,
K32
() : ( ( ) (
V1
()
epsilon-transitive
epsilon-connected
ordinal
)
M2
(
K6
(
K28
() : ( ( ) ( )
set
) ) : ( ( ) ( )
set
) )) ))
/
2 : ( ( ) (
epsilon-transitive
epsilon-connected
ordinal
natural
V11
()
V12
()
real
V29
() )
M3
(
K28
() : ( ( ) ( )
set
) ,
K32
() : ( ( ) (
V1
()
epsilon-transitive
epsilon-connected
ordinal
)
M2
(
K6
(
K28
() : ( ( ) ( )
set
) ) : ( ( ) ( )
set
) )) ))
)
: ( ( ) (
V11
()
V12
()
real
)
set
)
*
(
(
sin
(
th1
: ( (
real
) (
V11
()
V12
()
real
)
number
)
+
th2
: ( (
real
) (
V11
()
V12
()
real
)
number
)
)
: ( ( ) (
V11
()
V12
()
real
)
set
)
)
: ( ( ) (
V11
()
V12
()
real
)
set
)
+
(
sin
(
th1
: ( (
real
) (
V11
()
V12
()
real
)
number
)
-
th2
: ( (
real
) (
V11
()
V12
()
real
)
number
)
)
: ( ( ) (
V11
()
V12
()
real
)
set
)
)
: ( ( ) (
V11
()
V12
()
real
)
set
)
)
: ( ( ) (
V11
()
V12
()
real
)
set
) : ( ( ) (
V11
()
V12
()
real
)
set
) ;
theorem
:: SIN_COS4:31
for
th1
,
th2
being ( (
real
) (
V11
()
V12
()
real
)
number
) holds
(
cos
th1
: ( (
real
) (
V11
()
V12
()
real
)
number
)
)
: ( ( ) (
V11
()
V12
()
real
)
set
)
*
(
sin
th2
: ( (
real
) (
V11
()
V12
()
real
)
number
)
)
: ( ( ) (
V11
()
V12
()
real
)
set
) : ( ( ) (
V11
()
V12
()
real
)
set
)
=
(
1 : ( ( ) (
epsilon-transitive
epsilon-connected
ordinal
natural
V11
()
V12
()
real
V29
() )
M3
(
K28
() : ( ( ) ( )
set
) ,
K32
() : ( ( ) (
V1
()
epsilon-transitive
epsilon-connected
ordinal
)
M2
(
K6
(
K28
() : ( ( ) ( )
set
) ) : ( ( ) ( )
set
) )) ))
/
2 : ( ( ) (
epsilon-transitive
epsilon-connected
ordinal
natural
V11
()
V12
()
real
V29
() )
M3
(
K28
() : ( ( ) ( )
set
) ,
K32
() : ( ( ) (
V1
()
epsilon-transitive
epsilon-connected
ordinal
)
M2
(
K6
(
K28
() : ( ( ) ( )
set
) ) : ( ( ) ( )
set
) )) ))
)
: ( ( ) (
V11
()
V12
()
real
)
set
)
*
(
(
sin
(
th1
: ( (
real
) (
V11
()
V12
()
real
)
number
)
+
th2
: ( (
real
) (
V11
()
V12
()
real
)
number
)
)
: ( ( ) (
V11
()
V12
()
real
)
set
)
)
: ( ( ) (
V11
()
V12
()
real
)
set
)
-
(
sin
(
th1
: ( (
real
) (
V11
()
V12
()
real
)
number
)
-
th2
: ( (
real
) (
V11
()
V12
()
real
)
number
)
)
: ( ( ) (
V11
()
V12
()
real
)
set
)
)
: ( ( ) (
V11
()
V12
()
real
)
set
)
)
: ( ( ) (
V11
()
V12
()
real
)
set
) : ( ( ) (
V11
()
V12
()
real
)
set
) ;
theorem
:: SIN_COS4:32
for
th1
,
th2
being ( (
real
) (
V11
()
V12
()
real
)
number
) holds
(
cos
th1
: ( (
real
) (
V11
()
V12
()
real
)
number
)
)
: ( ( ) (
V11
()
V12
()
real
)
set
)
*
(
cos
th2
: ( (
real
) (
V11
()
V12
()
real
)
number
)
)
: ( ( ) (
V11
()
V12
()
real
)
set
) : ( ( ) (
V11
()
V12
()
real
)
set
)
=
(
1 : ( ( ) (
epsilon-transitive
epsilon-connected
ordinal
natural
V11
()
V12
()
real
V29
() )
M3
(
K28
() : ( ( ) ( )
set
) ,
K32
() : ( ( ) (
V1
()
epsilon-transitive
epsilon-connected
ordinal
)
M2
(
K6
(
K28
() : ( ( ) ( )
set
) ) : ( ( ) ( )
set
) )) ))
/
2 : ( ( ) (
epsilon-transitive
epsilon-connected
ordinal
natural
V11
()
V12
()
real
V29
() )
M3
(
K28
() : ( ( ) ( )
set
) ,
K32
() : ( ( ) (
V1
()
epsilon-transitive
epsilon-connected
ordinal
)
M2
(
K6
(
K28
() : ( ( ) ( )
set
) ) : ( ( ) ( )
set
) )) ))
)
: ( ( ) (
V11
()
V12
()
real
)
set
)
*
(
(
cos
(
th1
: ( (
real
) (
V11
()
V12
()
real
)
number
)
+
th2
: ( (
real
) (
V11
()
V12
()
real
)
number
)
)
: ( ( ) (
V11
()
V12
()
real
)
set
)
)
: ( ( ) (
V11
()
V12
()
real
)
set
)
+
(
cos
(
th1
: ( (
real
) (
V11
()
V12
()
real
)
number
)
-
th2
: ( (
real
) (
V11
()
V12
()
real
)
number
)
)
: ( ( ) (
V11
()
V12
()
real
)
set
)
)
: ( ( ) (
V11
()
V12
()
real
)
set
)
)
: ( ( ) (
V11
()
V12
()
real
)
set
) : ( ( ) (
V11
()
V12
()
real
)
set
) ;
theorem
:: SIN_COS4:33
for
th1
,
th2
,
th3
being ( (
real
) (
V11
()
V12
()
real
)
number
) holds
(
(
sin
th1
: ( (
real
) (
V11
()
V12
()
real
)
number
)
)
: ( ( ) (
V11
()
V12
()
real
)
set
)
*
(
sin
th2
: ( (
real
) (
V11
()
V12
()
real
)
number
)
)
: ( ( ) (
V11
()
V12
()
real
)
set
)
)
: ( ( ) (
V11
()
V12
()
real
)
set
)
*
(
sin
th3
: ( (
real
) (
V11
()
V12
()
real
)
number
)
)
: ( ( ) (
V11
()
V12
()
real
)
set
) : ( ( ) (
V11
()
V12
()
real
)
set
)
=
(
1 : ( ( ) (
epsilon-transitive
epsilon-connected
ordinal
natural
V11
()
V12
()
real
V29
() )
M3
(
K28
() : ( ( ) ( )
set
) ,
K32
() : ( ( ) (
V1
()
epsilon-transitive
epsilon-connected
ordinal
)
M2
(
K6
(
K28
() : ( ( ) ( )
set
) ) : ( ( ) ( )
set
) )) ))
/
4 : ( ( ) (
epsilon-transitive
epsilon-connected
ordinal
natural
V11
()
V12
()
real
V29
() )
M3
(
K28
() : ( ( ) ( )
set
) ,
K32
() : ( ( ) (
V1
()
epsilon-transitive
epsilon-connected
ordinal
)
M2
(
K6
(
K28
() : ( ( ) ( )
set
) ) : ( ( ) ( )
set
) )) ))
)
: ( ( ) (
V11
()
V12
()
real
)
set
)
*
(
(
(
(
sin
(
(
th1
: ( (
real
) (
V11
()
V12
()
real
)
number
)
+
th2
: ( (
real
) (
V11
()
V12
()
real
)
number
)
)
: ( ( ) (
V11
()
V12
()
real
)
set
)
-
th3
: ( (
real
) (
V11
()
V12
()
real
)
number
)
)
: ( ( ) (
V11
()
V12
()
real
)
set
)
)
: ( ( ) (
V11
()
V12
()
real
)
set
)
+
(
sin
(
(
th2
: ( (
real
) (
V11
()
V12
()
real
)
number
)
+
th3
: ( (
real
) (
V11
()
V12
()
real
)
number
)
)
: ( ( ) (
V11
()
V12
()
real
)
set
)
-
th1
: ( (
real
) (
V11
()
V12
()
real
)
number
)
)
: ( ( ) (
V11
()
V12
()
real
)
set
)
)
: ( ( ) (
V11
()
V12
()
real
)
set
)
)
: ( ( ) (
V11
()
V12
()
real
)
set
)
+
(
sin
(
(
th3
: ( (
real
) (
V11
()
V12
()
real
)
number
)
+
th1
: ( (
real
) (
V11
()
V12
()
real
)
number
)
)
: ( ( ) (
V11
()
V12
()
real
)
set
)
-
th2
: ( (
real
) (
V11
()
V12
()
real
)
number
)
)
: ( ( ) (
V11
()
V12
()
real
)
set
)
)
: ( ( ) (
V11
()
V12
()
real
)
set
)
)
: ( ( ) (
V11
()
V12
()
real
)
set
)
-
(
sin
(
(
th1
: ( (
real
) (
V11
()
V12
()
real
)
number
)
+
th2
: ( (
real
) (
V11
()
V12
()
real
)
number
)
)
: ( ( ) (
V11
()
V12
()
real
)
set
)
+
th3
: ( (
real
) (
V11
()
V12
()
real
)
number
)
)
: ( ( ) (
V11
()
V12
()
real
)
set
)
)
: ( ( ) (
V11
()
V12
()
real
)
set
)
)
: ( ( ) (
V11
()
V12
()
real
)
set
) : ( ( ) (
V11
()
V12
()
real
)
set
) ;
theorem
:: SIN_COS4:34
for
th1
,
th2
,
th3
being ( (
real
) (
V11
()
V12
()
real
)
number
) holds
(
(
sin
th1
: ( (
real
) (
V11
()
V12
()
real
)
number
)
)
: ( ( ) (
V11
()
V12
()
real
)
set
)
*
(
sin
th2
: ( (
real
) (
V11
()
V12
()
real
)
number
)
)
: ( ( ) (
V11
()
V12
()
real
)
set
)
)
: ( ( ) (
V11
()
V12
()
real
)
set
)
*
(
cos
th3
: ( (
real
) (
V11
()
V12
()
real
)
number
)
)
: ( ( ) (
V11
()
V12
()
real
)
set
) : ( ( ) (
V11
()
V12
()
real
)
set
)
=
(
1 : ( ( ) (
epsilon-transitive
epsilon-connected
ordinal
natural
V11
()
V12
()
real
V29
() )
M3
(
K28
() : ( ( ) ( )
set
) ,
K32
() : ( ( ) (
V1
()
epsilon-transitive
epsilon-connected
ordinal
)
M2
(
K6
(
K28
() : ( ( ) ( )
set
) ) : ( ( ) ( )
set
) )) ))
/
4 : ( ( ) (
epsilon-transitive
epsilon-connected
ordinal
natural
V11
()
V12
()
real
V29
() )
M3
(
K28
() : ( ( ) ( )
set
) ,
K32
() : ( ( ) (
V1
()
epsilon-transitive
epsilon-connected
ordinal
)
M2
(
K6
(
K28
() : ( ( ) ( )
set
) ) : ( ( ) ( )
set
) )) ))
)
: ( ( ) (
V11
()
V12
()
real
)
set
)
*
(
(
(
(
-
(
cos
(
(
th1
: ( (
real
) (
V11
()
V12
()
real
)
number
)
+
th2
: ( (
real
) (
V11
()
V12
()
real
)
number
)
)
: ( ( ) (
V11
()
V12
()
real
)
set
)
-
th3
: ( (
real
) (
V11
()
V12
()
real
)
number
)
)
: ( ( ) (
V11
()
V12
()
real
)
set
)
)
: ( ( ) (
V11
()
V12
()
real
)
set
)
)
: ( (
V11
() ) (
V11
()
V12
()
real
)
set
)
+
(
cos
(
(
th2
: ( (
real
) (
V11
()
V12
()
real
)
number
)
+
th3
: ( (
real
) (
V11
()
V12
()
real
)
number
)
)
: ( ( ) (
V11
()
V12
()
real
)
set
)
-
th1
: ( (
real
) (
V11
()
V12
()
real
)
number
)
)
: ( ( ) (
V11
()
V12
()
real
)
set
)
)
: ( ( ) (
V11
()
V12
()
real
)
set
)
)
: ( ( ) (
V11
()
V12
()
real
)
set
)
+
(
cos
(
(
th3
: ( (
real
) (
V11
()
V12
()
real
)
number
)
+
th1
: ( (
real
) (
V11
()
V12
()
real
)
number
)
)
: ( ( ) (
V11
()
V12
()
real
)
set
)
-
th2
: ( (
real
) (
V11
()
V12
()
real
)
number
)
)
: ( ( ) (
V11
()
V12
()
real
)
set
)
)
: ( ( ) (
V11
()
V12
()
real
)
set
)
)
: ( ( ) (
V11
()
V12
()
real
)
set
)
-
(
cos
(
(
th1
: ( (
real
) (
V11
()
V12
()
real
)
number
)
+
th2
: ( (
real
) (
V11
()
V12
()
real
)
number
)
)
: ( ( ) (
V11
()
V12
()
real
)
set
)
+
th3
: ( (
real
) (
V11
()
V12
()
real
)
number
)
)
: ( ( ) (
V11
()
V12
()
real
)
set
)
)
: ( ( ) (
V11
()
V12
()
real
)
set
)
)
: ( ( ) (
V11
()
V12
()
real
)
set
) : ( ( ) (
V11
()
V12
()
real
)
set
) ;
theorem
:: SIN_COS4:35
for
th1
,
th2
,
th3
being ( (
real
) (
V11
()
V12
()
real
)
number
) holds
(
(
sin
th1
: ( (
real
) (
V11
()
V12
()
real
)
number
)
)
: ( ( ) (
V11
()
V12
()
real
)
set
)
*
(
cos
th2
: ( (
real
) (
V11
()
V12
()
real
)
number
)
)
: ( ( ) (
V11
()
V12
()
real
)
set
)
)
: ( ( ) (
V11
()
V12
()
real
)
set
)
*
(
cos
th3
: ( (
real
) (
V11
()
V12
()
real
)
number
)
)
: ( ( ) (
V11
()
V12
()
real
)
set
) : ( ( ) (
V11
()
V12
()
real
)
set
)
=
(
1 : ( ( ) (
epsilon-transitive
epsilon-connected
ordinal
natural
V11
()
V12
()
real
V29
() )
M3
(
K28
() : ( ( ) ( )
set
) ,
K32
() : ( ( ) (
V1
()
epsilon-transitive
epsilon-connected
ordinal
)
M2
(
K6
(
K28
() : ( ( ) ( )
set
) ) : ( ( ) ( )
set
) )) ))
/
4 : ( ( ) (
epsilon-transitive
epsilon-connected
ordinal
natural
V11
()
V12
()
real
V29
() )
M3
(
K28
() : ( ( ) ( )
set
) ,
K32
() : ( ( ) (
V1
()
epsilon-transitive
epsilon-connected
ordinal
)
M2
(
K6
(
K28
() : ( ( ) ( )
set
) ) : ( ( ) ( )
set
) )) ))
)
: ( ( ) (
V11
()
V12
()
real
)
set
)
*
(
(
(
(
sin
(
(
th1
: ( (
real
) (
V11
()
V12
()
real
)
number
)
+
th2
: ( (
real
) (
V11
()
V12
()
real
)
number
)
)
: ( ( ) (
V11
()
V12
()
real
)
set
)
-
th3
: ( (
real
) (
V11
()
V12
()
real
)
number
)
)
: ( ( ) (
V11
()
V12
()
real
)
set
)
)
: ( ( ) (
V11
()
V12
()
real
)
set
)
-
(
sin
(
(
th2
: ( (
real
) (
V11
()
V12
()
real
)
number
)
+
th3
: ( (
real
) (
V11
()
V12
()
real
)
number
)
)
: ( ( ) (
V11
()
V12
()
real
)
set
)
-
th1
: ( (
real
) (
V11
()
V12
()
real
)
number
)
)
: ( ( ) (
V11
()
V12
()
real
)
set
)
)
: ( ( ) (
V11
()
V12
()
real
)
set
)
)
: ( ( ) (
V11
()
V12
()
real
)
set
)
+
(
sin
(
(
th3
: ( (
real
) (
V11
()
V12
()
real
)
number
)
+
th1
: ( (
real
) (
V11
()
V12
()
real
)
number
)
)
: ( ( ) (
V11
()
V12
()
real
)
set
)
-
th2
: ( (
real
) (
V11
()
V12
()
real
)
number
)
)
: ( ( ) (
V11
()
V12
()
real
)
set
)
)
: ( ( ) (
V11
()
V12
()
real
)
set
)
)
: ( ( ) (
V11
()
V12
()
real
)
set
)
+
(
sin
(
(
th1
: ( (
real
) (
V11
()
V12
()
real
)
number
)
+
th2
: ( (
real
) (
V11
()
V12
()
real
)
number
)
)
: ( ( ) (
V11
()
V12
()
real
)
set
)
+
th3
: ( (
real
) (
V11
()
V12
()
real
)
number
)
)
: ( ( ) (
V11
()
V12
()
real
)
set
)
)
: ( ( ) (
V11
()
V12
()
real
)
set
)
)
: ( ( ) (
V11
()
V12
()
real
)
set
) : ( ( ) (
V11
()
V12
()
real
)
set
) ;
theorem
:: SIN_COS4:36
for
th1
,
th2
,
th3
being ( (
real
) (
V11
()
V12
()
real
)
number
) holds
(
(
cos
th1
: ( (
real
) (
V11
()
V12
()
real
)
number
)
)
: ( ( ) (
V11
()
V12
()
real
)
set
)
*
(
cos
th2
: ( (
real
) (
V11
()
V12
()
real
)
number
)
)
: ( ( ) (
V11
()
V12
()
real
)
set
)
)
: ( ( ) (
V11
()
V12
()
real
)
set
)
*
(
cos
th3
: ( (
real
) (
V11
()
V12
()
real
)
number
)
)
: ( ( ) (
V11
()
V12
()
real
)
set
) : ( ( ) (
V11
()
V12
()
real
)
set
)
=
(
1 : ( ( ) (
epsilon-transitive
epsilon-connected
ordinal
natural
V11
()
V12
()
real
V29
() )
M3
(
K28
() : ( ( ) ( )
set
) ,
K32
() : ( ( ) (
V1
()
epsilon-transitive
epsilon-connected
ordinal
)
M2
(
K6
(
K28
() : ( ( ) ( )
set
) ) : ( ( ) ( )
set
) )) ))
/
4 : ( ( ) (
epsilon-transitive
epsilon-connected
ordinal
natural
V11
()
V12
()
real
V29
() )
M3
(
K28
() : ( ( ) ( )
set
) ,
K32
() : ( ( ) (
V1
()
epsilon-transitive
epsilon-connected
ordinal
)
M2
(
K6
(
K28
() : ( ( ) ( )
set
) ) : ( ( ) ( )
set
) )) ))
)
: ( ( ) (
V11
()
V12
()
real
)
set
)
*
(
(
(
(
cos
(
(
th1
: ( (
real
) (
V11
()
V12
()
real
)
number
)
+
th2
: ( (
real
) (
V11
()
V12
()
real
)
number
)
)
: ( ( ) (
V11
()
V12
()
real
)
set
)
-
th3
: ( (
real
) (
V11
()
V12
()
real
)
number
)
)
: ( ( ) (
V11
()
V12
()
real
)
set
)
)
: ( ( ) (
V11
()
V12
()
real
)
set
)
+
(
cos
(
(
th2
: ( (
real
) (
V11
()
V12
()
real
)
number
)
+
th3
: ( (
real
) (
V11
()
V12
()
real
)
number
)
)
: ( ( ) (
V11
()
V12
()
real
)
set
)
-
th1
: ( (
real
) (
V11
()
V12
()
real
)
number
)
)
: ( ( ) (
V11
()
V12
()
real
)
set
)
)
: ( ( ) (
V11
()
V12
()
real
)
set
)
)
: ( ( ) (
V11
()
V12
()
real
)
set
)
+
(
cos
(
(
th3
: ( (
real
) (
V11
()
V12
()
real
)
number
)
+
th1
: ( (
real
) (
V11
()
V12
()
real
)
number
)
)
: ( ( ) (
V11
()
V12
()
real
)
set
)
-
th2
: ( (
real
) (
V11
()
V12
()
real
)
number
)
)
: ( ( ) (
V11
()
V12
()
real
)
set
)
)
: ( ( ) (
V11
()
V12
()
real
)
set
)
)
: ( ( ) (
V11
()
V12
()
real
)
set
)
+
(
cos
(
(
th1
: ( (
real
) (
V11
()
V12
()
real
)
number
)
+
th2
: ( (
real
) (
V11
()
V12
()
real
)
number
)
)
: ( ( ) (
V11
()
V12
()
real
)
set
)
+
th3
: ( (
real
) (
V11
()
V12
()
real
)
number
)
)
: ( ( ) (
V11
()
V12
()
real
)
set
)
)
: ( ( ) (
V11
()
V12
()
real
)
set
)
)
: ( ( ) (
V11
()
V12
()
real
)
set
) : ( ( ) (
V11
()
V12
()
real
)
set
) ;
theorem
:: SIN_COS4:37
for
th1
,
th2
being ( (
real
) (
V11
()
V12
()
real
)
number
) holds
(
sin
(
th1
: ( (
real
) (
V11
()
V12
()
real
)
number
)
+
th2
: ( (
real
) (
V11
()
V12
()
real
)
number
)
)
: ( ( ) (
V11
()
V12
()
real
)
set
)
)
: ( ( ) (
V11
()
V12
()
real
)
set
)
*
(
sin
(
th1
: ( (
real
) (
V11
()
V12
()
real
)
number
)
-
th2
: ( (
real
) (
V11
()
V12
()
real
)
number
)
)
: ( ( ) (
V11
()
V12
()
real
)
set
)
)
: ( ( ) (
V11
()
V12
()
real
)
set
) : ( ( ) (
V11
()
V12
()
real
)
set
)
=
(
(
sin
th1
: ( (
real
) (
V11
()
V12
()
real
)
number
)
)
: ( ( ) (
V11
()
V12
()
real
)
set
)
*
(
sin
th1
: ( (
real
) (
V11
()
V12
()
real
)
number
)
)
: ( ( ) (
V11
()
V12
()
real
)
set
)
)
: ( ( ) (
V11
()
V12
()
real
)
set
)
-
(
(
sin
th2
: ( (
real
) (
V11
()
V12
()
real
)
number
)
)
: ( ( ) (
V11
()
V12
()
real
)
set
)
*
(
sin
th2
: ( (
real
) (
V11
()
V12
()
real
)
number
)
)
: ( ( ) (
V11
()
V12
()
real
)
set
)
)
: ( ( ) (
V11
()
V12
()
real
)
set
) : ( ( ) (
V11
()
V12
()
real
)
set
) ;
theorem
:: SIN_COS4:38
for
th1
,
th2
being ( (
real
) (
V11
()
V12
()
real
)
number
) holds
(
sin
(
th1
: ( (
real
) (
V11
()
V12
()
real
)
number
)
+
th2
: ( (
real
) (
V11
()
V12
()
real
)
number
)
)
: ( ( ) (
V11
()
V12
()
real
)
set
)
)
: ( ( ) (
V11
()
V12
()
real
)
set
)
*
(
sin
(
th1
: ( (
real
) (
V11
()
V12
()
real
)
number
)
-
th2
: ( (
real
) (
V11
()
V12
()
real
)
number
)
)
: ( ( ) (
V11
()
V12
()
real
)
set
)
)
: ( ( ) (
V11
()
V12
()
real
)
set
) : ( ( ) (
V11
()
V12
()
real
)
set
)
=
(
(
cos
th2
: ( (
real
) (
V11
()
V12
()
real
)
number
)
)
: ( ( ) (
V11
()
V12
()
real
)
set
)
*
(
cos
th2
: ( (
real
) (
V11
()
V12
()
real
)
number
)
)
: ( ( ) (
V11
()
V12
()
real
)
set
)
)
: ( ( ) (
V11
()
V12
()
real
)
set
)
-
(
(
cos
th1
: ( (
real
) (
V11
()
V12
()
real
)
number
)
)
: ( ( ) (
V11
()
V12
()
real
)
set
)
*
(
cos
th1
: ( (
real
) (
V11
()
V12
()
real
)
number
)
)
: ( ( ) (
V11
()
V12
()
real
)
set
)
)
: ( ( ) (
V11
()
V12
()
real
)
set
) : ( ( ) (
V11
()
V12
()
real
)
set
) ;
theorem
:: SIN_COS4:39
for
th1
,
th2
being ( (
real
) (
V11
()
V12
()
real
)
number
) holds
(
sin
(
th1
: ( (
real
) (
V11
()
V12
()
real
)
number
)
+
th2
: ( (
real
) (
V11
()
V12
()
real
)
number
)
)
: ( ( ) (
V11
()
V12
()
real
)
set
)
)
: ( ( ) (
V11
()
V12
()
real
)
set
)
*
(
cos
(
th1
: ( (
real
) (
V11
()
V12
()
real
)
number
)
-
th2
: ( (
real
) (
V11
()
V12
()
real
)
number
)
)
: ( ( ) (
V11
()
V12
()
real
)
set
)
)
: ( ( ) (
V11
()
V12
()
real
)
set
) : ( ( ) (
V11
()
V12
()
real
)
set
)
=
(
(
sin
th1
: ( (
real
) (
V11
()
V12
()
real
)
number
)
)
: ( ( ) (
V11
()
V12
()
real
)
set
)
*
(
cos
th1
: ( (
real
) (
V11
()
V12
()
real
)
number
)
)
: ( ( ) (
V11
()
V12
()
real
)
set
)
)
: ( ( ) (
V11
()
V12
()
real
)
set
)
+
(
(
sin
th2
: ( (
real
) (
V11
()
V12
()
real
)
number
)
)
: ( ( ) (
V11
()
V12
()
real
)
set
)
*
(
cos
th2
: ( (
real
) (
V11
()
V12
()
real
)
number
)
)
: ( ( ) (
V11
()
V12
()
real
)
set
)
)
: ( ( ) (
V11
()
V12
()
real
)
set
) : ( ( ) (
V11
()
V12
()
real
)
set
) ;
theorem
:: SIN_COS4:40
for
th1
,
th2
being ( (
real
) (
V11
()
V12
()
real
)
number
) holds
(
cos
(
th1
: ( (
real
) (
V11
()
V12
()
real
)
number
)
+
th2
: ( (
real
) (
V11
()
V12
()
real
)
number
)
)
: ( ( ) (
V11
()
V12
()
real
)
set
)
)
: ( ( ) (
V11
()
V12
()
real
)
set
)
*
(
sin
(
th1
: ( (
real
) (
V11
()
V12
()
real
)
number
)
-
th2
: ( (
real
) (
V11
()
V12
()
real
)
number
)
)
: ( ( ) (
V11
()
V12
()
real
)
set
)
)
: ( ( ) (
V11
()
V12
()
real
)
set
) : ( ( ) (
V11
()
V12
()
real
)
set
)
=
(
(
sin
th1
: ( (
real
) (
V11
()
V12
()
real
)
number
)
)
: ( ( ) (
V11
()
V12
()
real
)
set
)
*
(
cos
th1
: ( (
real
) (
V11
()
V12
()
real
)
number
)
)
: ( ( ) (
V11
()
V12
()
real
)
set
)
)
: ( ( ) (
V11
()
V12
()
real
)
set
)
-
(
(
sin
th2
: ( (
real
) (
V11
()
V12
()
real
)
number
)
)
: ( ( ) (
V11
()
V12
()
real
)
set
)
*
(
cos
th2
: ( (
real
) (
V11
()
V12
()
real
)
number
)
)
: ( ( ) (
V11
()
V12
()
real
)
set
)
)
: ( ( ) (
V11
()
V12
()
real
)
set
) : ( ( ) (
V11
()
V12
()
real
)
set
) ;
theorem
:: SIN_COS4:41
for
th1
,
th2
being ( (
real
) (
V11
()
V12
()
real
)
number
) holds
(
cos
(
th1
: ( (
real
) (
V11
()
V12
()
real
)
number
)
+
th2
: ( (
real
) (
V11
()
V12
()
real
)
number
)
)
: ( ( ) (
V11
()
V12
()
real
)
set
)
)
: ( ( ) (
V11
()
V12
()
real
)
set
)
*
(
cos
(
th1
: ( (
real
) (
V11
()
V12
()
real
)
number
)
-
th2
: ( (
real
) (
V11
()
V12
()
real
)
number
)
)
: ( ( ) (
V11
()
V12
()
real
)
set
)
)
: ( ( ) (
V11
()
V12
()
real
)
set
) : ( ( ) (
V11
()
V12
()
real
)
set
)
=
(
(
cos
th1
: ( (
real
) (
V11
()
V12
()
real
)
number
)
)
: ( ( ) (
V11
()
V12
()
real
)
set
)
*
(
cos
th1
: ( (
real
) (
V11
()
V12
()
real
)
number
)
)
: ( ( ) (
V11
()
V12
()
real
)
set
)
)
: ( ( ) (
V11
()
V12
()
real
)
set
)
-
(
(
sin
th2
: ( (
real
) (
V11
()
V12
()
real
)
number
)
)
: ( ( ) (
V11
()
V12
()
real
)
set
)
*
(
sin
th2
: ( (
real
) (
V11
()
V12
()
real
)
number
)
)
: ( ( ) (
V11
()
V12
()
real
)
set
)
)
: ( ( ) (
V11
()
V12
()
real
)
set
) : ( ( ) (
V11
()
V12
()
real
)
set
) ;
theorem
:: SIN_COS4:42
for
th1
,
th2
being ( (
real
) (
V11
()
V12
()
real
)
number
) holds
(
cos
(
th1
: ( (
real
) (
V11
()
V12
()
real
)
number
)
+
th2
: ( (
real
) (
V11
()
V12
()
real
)
number
)
)
: ( ( ) (
V11
()
V12
()
real
)
set
)
)
: ( ( ) (
V11
()
V12
()
real
)
set
)
*
(
cos
(
th1
: ( (
real
) (
V11
()
V12
()
real
)
number
)
-
th2
: ( (
real
) (
V11
()
V12
()
real
)
number
)
)
: ( ( ) (
V11
()
V12
()
real
)
set
)
)
: ( ( ) (
V11
()
V12
()
real
)
set
) : ( ( ) (
V11
()
V12
()
real
)
set
)
=
(
(
cos
th2
: ( (
real
) (
V11
()
V12
()
real
)
number
)
)
: ( ( ) (
V11
()
V12
()
real
)
set
)
*
(
cos
th2
: ( (
real
) (
V11
()
V12
()
real
)
number
)
)
: ( ( ) (
V11
()
V12
()
real
)
set
)
)
: ( ( ) (
V11
()
V12
()
real
)
set
)
-
(
(
sin
th1
: ( (
real
) (
V11
()
V12
()
real
)
number
)
)
: ( ( ) (
V11
()
V12
()
real
)
set
)
*
(
sin
th1
: ( (
real
) (
V11
()
V12
()
real
)
number
)
)
: ( ( ) (
V11
()
V12
()
real
)
set
)
)
: ( ( ) (
V11
()
V12
()
real
)
set
) : ( ( ) (
V11
()
V12
()
real
)
set
) ;
theorem
:: SIN_COS4:43
for
th1
,
th2
being ( (
real
) (
V11
()
V12
()
real
)
number
) st
cos
th1
: ( (
real
) (
V11
()
V12
()
real
)
number
) : ( ( ) (
V11
()
V12
()
real
)
set
)
<>
0
: ( ( ) (
epsilon-transitive
epsilon-connected
ordinal
natural
V11
()
V12
()
real
V29
() )
M3
(
K28
() : ( ( ) ( )
set
) ,
K32
() : ( ( ) (
V1
()
epsilon-transitive
epsilon-connected
ordinal
)
M2
(
K6
(
K28
() : ( ( ) ( )
set
) ) : ( ( ) ( )
set
) )) )) &
cos
th2
: ( (
real
) (
V11
()
V12
()
real
)
number
) : ( ( ) (
V11
()
V12
()
real
)
set
)
<>
0
: ( ( ) (
epsilon-transitive
epsilon-connected
ordinal
natural
V11
()
V12
()
real
V29
() )
M3
(
K28
() : ( ( ) ( )
set
) ,
K32
() : ( ( ) (
V1
()
epsilon-transitive
epsilon-connected
ordinal
)
M2
(
K6
(
K28
() : ( ( ) ( )
set
) ) : ( ( ) ( )
set
) )) )) holds
(
sin
(
th1
: ( (
real
) (
V11
()
V12
()
real
)
number
)
+
th2
: ( (
real
) (
V11
()
V12
()
real
)
number
)
)
: ( ( ) (
V11
()
V12
()
real
)
set
)
)
: ( ( ) (
V11
()
V12
()
real
)
set
)
/
(
sin
(
th1
: ( (
real
) (
V11
()
V12
()
real
)
number
)
-
th2
: ( (
real
) (
V11
()
V12
()
real
)
number
)
)
: ( ( ) (
V11
()
V12
()
real
)
set
)
)
: ( ( ) (
V11
()
V12
()
real
)
set
) : ( ( ) (
V11
()
V12
()
real
)
set
)
=
(
(
tan
th1
: ( (
real
) (
V11
()
V12
()
real
)
number
)
)
: ( ( ) (
V11
()
V12
()
real
)
Real
)
+
(
tan
th2
: ( (
real
) (
V11
()
V12
()
real
)
number
)
)
: ( ( ) (
V11
()
V12
()
real
)
Real
)
)
: ( ( ) (
V11
()
V12
()
real
)
set
)
/
(
(
tan
th1
: ( (
real
) (
V11
()
V12
()
real
)
number
)
)
: ( ( ) (
V11
()
V12
()
real
)
Real
)
-
(
tan
th2
: ( (
real
) (
V11
()
V12
()
real
)
number
)
)
: ( ( ) (
V11
()
V12
()
real
)
Real
)
)
: ( ( ) (
V11
()
V12
()
real
)
set
) : ( ( ) (
V11
()
V12
()
real
)
set
) ;
theorem
:: SIN_COS4:44
for
th1
,
th2
being ( (
real
) (
V11
()
V12
()
real
)
number
) st
cos
th1
: ( (
real
) (
V11
()
V12
()
real
)
number
) : ( ( ) (
V11
()
V12
()
real
)
set
)
<>
0
: ( ( ) (
epsilon-transitive
epsilon-connected
ordinal
natural
V11
()
V12
()
real
V29
() )
M3
(
K28
() : ( ( ) ( )
set
) ,
K32
() : ( ( ) (
V1
()
epsilon-transitive
epsilon-connected
ordinal
)
M2
(
K6
(
K28
() : ( ( ) ( )
set
) ) : ( ( ) ( )
set
) )) )) &
cos
th2
: ( (
real
) (
V11
()
V12
()
real
)
number
) : ( ( ) (
V11
()
V12
()
real
)
set
)
<>
0
: ( ( ) (
epsilon-transitive
epsilon-connected
ordinal
natural
V11
()
V12
()
real
V29
() )
M3
(
K28
() : ( ( ) ( )
set
) ,
K32
() : ( ( ) (
V1
()
epsilon-transitive
epsilon-connected
ordinal
)
M2
(
K6
(
K28
() : ( ( ) ( )
set
) ) : ( ( ) ( )
set
) )) )) holds
(
cos
(
th1
: ( (
real
) (
V11
()
V12
()
real
)
number
)
+
th2
: ( (
real
) (
V11
()
V12
()
real
)
number
)
)
: ( ( ) (
V11
()
V12
()
real
)
set
)
)
: ( ( ) (
V11
()
V12
()
real
)
set
)
/
(
cos
(
th1
: ( (
real
) (
V11
()
V12
()
real
)
number
)
-
th2
: ( (
real
) (
V11
()
V12
()
real
)
number
)
)
: ( ( ) (
V11
()
V12
()
real
)
set
)
)
: ( ( ) (
V11
()
V12
()
real
)
set
) : ( ( ) (
V11
()
V12
()
real
)
set
)
=
(
1 : ( ( ) (
epsilon-transitive
epsilon-connected
ordinal
natural
V11
()
V12
()
real
V29
() )
M3
(
K28
() : ( ( ) ( )
set
) ,
K32
() : ( ( ) (
V1
()
epsilon-transitive
epsilon-connected
ordinal
)
M2
(
K6
(
K28
() : ( ( ) ( )
set
) ) : ( ( ) ( )
set
) )) ))
-
(
(
tan
th1
: ( (
real
) (
V11
()
V12
()
real
)
number
)
)
: ( ( ) (
V11
()
V12
()
real
)
Real
)
*
(
tan
th2
: ( (
real
) (
V11
()
V12
()
real
)
number
)
)
: ( ( ) (
V11
()
V12
()
real
)
Real
)
)
: ( ( ) (
V11
()
V12
()
real
)
set
)
)
: ( ( ) (
V11
()
V12
()
real
)
set
)
/
(
1 : ( ( ) (
epsilon-transitive
epsilon-connected
ordinal
natural
V11
()
V12
()
real
V29
() )
M3
(
K28
() : ( ( ) ( )
set
) ,
K32
() : ( ( ) (
V1
()
epsilon-transitive
epsilon-connected
ordinal
)
M2
(
K6
(
K28
() : ( ( ) ( )
set
) ) : ( ( ) ( )
set
) )) ))
+
(
(
tan
th1
: ( (
real
) (
V11
()
V12
()
real
)
number
)
)
: ( ( ) (
V11
()
V12
()
real
)
Real
)
*
(
tan
th2
: ( (
real
) (
V11
()
V12
()
real
)
number
)
)
: ( ( ) (
V11
()
V12
()
real
)
Real
)
)
: ( ( ) (
V11
()
V12
()
real
)
set
)
)
: ( ( ) (
V11
()
V12
()
real
)
set
) : ( ( ) (
V11
()
V12
()
real
)
set
) ;
theorem
:: SIN_COS4:45
for
th1
,
th2
being ( (
real
) (
V11
()
V12
()
real
)
number
) holds
(
(
sin
th1
: ( (
real
) (
V11
()
V12
()
real
)
number
)
)
: ( ( ) (
V11
()
V12
()
real
)
set
)
+
(
sin
th2
: ( (
real
) (
V11
()
V12
()
real
)
number
)
)
: ( ( ) (
V11
()
V12
()
real
)
set
)
)
: ( ( ) (
V11
()
V12
()
real
)
set
)
/
(
(
sin
th1
: ( (
real
) (
V11
()
V12
()
real
)
number
)
)
: ( ( ) (
V11
()
V12
()
real
)
set
)
-
(
sin
th2
: ( (
real
) (
V11
()
V12
()
real
)
number
)
)
: ( ( ) (
V11
()
V12
()
real
)
set
)
)
: ( ( ) (
V11
()
V12
()
real
)
set
) : ( ( ) (
V11
()
V12
()
real
)
set
)
=
(
tan
(
(
th1
: ( (
real
) (
V11
()
V12
()
real
)
number
)
+
th2
: ( (
real
) (
V11
()
V12
()
real
)
number
)
)
: ( ( ) (
V11
()
V12
()
real
)
set
)
/
2 : ( ( ) (
epsilon-transitive
epsilon-connected
ordinal
natural
V11
()
V12
()
real
V29
() )
M3
(
K28
() : ( ( ) ( )
set
) ,
K32
() : ( ( ) (
V1
()
epsilon-transitive
epsilon-connected
ordinal
)
M2
(
K6
(
K28
() : ( ( ) ( )
set
) ) : ( ( ) ( )
set
) )) ))
)
: ( ( ) (
V11
()
V12
()
real
)
set
)
)
: ( ( ) (
V11
()
V12
()
real
)
Real
)
*
(
cot
(
(
th1
: ( (
real
) (
V11
()
V12
()
real
)
number
)
-
th2
: ( (
real
) (
V11
()
V12
()
real
)
number
)
)
: ( ( ) (
V11
()
V12
()
real
)
set
)
/
2 : ( ( ) (
epsilon-transitive
epsilon-connected
ordinal
natural
V11
()
V12
()
real
V29
() )
M3
(
K28
() : ( ( ) ( )
set
) ,
K32
() : ( ( ) (
V1
()
epsilon-transitive
epsilon-connected
ordinal
)
M2
(
K6
(
K28
() : ( ( ) ( )
set
) ) : ( ( ) ( )
set
) )) ))
)
: ( ( ) (
V11
()
V12
()
real
)
set
)
)
: ( ( ) (
V11
()
V12
()
real
)
Real
) : ( ( ) (
V11
()
V12
()
real
)
set
) ;
theorem
:: SIN_COS4:46
for
th1
,
th2
being ( (
real
) (
V11
()
V12
()
real
)
number
) st
cos
(
(
th1
: ( (
real
) (
V11
()
V12
()
real
)
number
)
-
th2
: ( (
real
) (
V11
()
V12
()
real
)
number
)
)
: ( ( ) (
V11
()
V12
()
real
)
set
)
/
2 : ( ( ) (
epsilon-transitive
epsilon-connected
ordinal
natural
V11
()
V12
()
real
V29
() )
M3
(
K28
() : ( ( ) ( )
set
) ,
K32
() : ( ( ) (
V1
()
epsilon-transitive
epsilon-connected
ordinal
)
M2
(
K6
(
K28
() : ( ( ) ( )
set
) ) : ( ( ) ( )
set
) )) ))
)
: ( ( ) (
V11
()
V12
()
real
)
set
) : ( ( ) (
V11
()
V12
()
real
)
set
)
<>
0
: ( ( ) (
epsilon-transitive
epsilon-connected
ordinal
natural
V11
()
V12
()
real
V29
() )
M3
(
K28
() : ( ( ) ( )
set
) ,
K32
() : ( ( ) (
V1
()
epsilon-transitive
epsilon-connected
ordinal
)
M2
(
K6
(
K28
() : ( ( ) ( )
set
) ) : ( ( ) ( )
set
) )) )) holds
(
(
sin
th1
: ( (
real
) (
V11
()
V12
()
real
)
number
)
)
: ( ( ) (
V11
()
V12
()
real
)
set
)
+
(
sin
th2
: ( (
real
) (
V11
()
V12
()
real
)
number
)
)
: ( ( ) (
V11
()
V12
()
real
)
set
)
)
: ( ( ) (
V11
()
V12
()
real
)
set
)
/
(
(
cos
th1
: ( (
real
) (
V11
()
V12
()
real
)
number
)
)
: ( ( ) (
V11
()
V12
()
real
)
set
)
+
(
cos
th2
: ( (
real
) (
V11
()
V12
()
real
)
number
)
)
: ( ( ) (
V11
()
V12
()
real
)
set
)
)
: ( ( ) (
V11
()
V12
()
real
)
set
) : ( ( ) (
V11
()
V12
()
real
)
set
)
=
tan
(
(
th1
: ( (
real
) (
V11
()
V12
()
real
)
number
)
+
th2
: ( (
real
) (
V11
()
V12
()
real
)
number
)
)
: ( ( ) (
V11
()
V12
()
real
)
set
)
/
2 : ( ( ) (
epsilon-transitive
epsilon-connected
ordinal
natural
V11
()
V12
()
real
V29
() )
M3
(
K28
() : ( ( ) ( )
set
) ,
K32
() : ( ( ) (
V1
()
epsilon-transitive
epsilon-connected
ordinal
)
M2
(
K6
(
K28
() : ( ( ) ( )
set
) ) : ( ( ) ( )
set
) )) ))
)
: ( ( ) (
V11
()
V12
()
real
)
set
) : ( ( ) (
V11
()
V12
()
real
)
Real
) ;
theorem
:: SIN_COS4:47
for
th1
,
th2
being ( (
real
) (
V11
()
V12
()
real
)
number
) st
cos
(
(
th1
: ( (
real
) (
V11
()
V12
()
real
)
number
)
+
th2
: ( (
real
) (
V11
()
V12
()
real
)
number
)
)
: ( ( ) (
V11
()
V12
()
real
)
set
)
/
2 : ( ( ) (
epsilon-transitive
epsilon-connected
ordinal
natural
V11
()
V12
()
real
V29
() )
M3
(
K28
() : ( ( ) ( )
set
) ,
K32
() : ( ( ) (
V1
()
epsilon-transitive
epsilon-connected
ordinal
)
M2
(
K6
(
K28
() : ( ( ) ( )
set
) ) : ( ( ) ( )
set
) )) ))
)
: ( ( ) (
V11
()
V12
()
real
)
set
) : ( ( ) (
V11
()
V12
()
real
)
set
)
<>
0
: ( ( ) (
epsilon-transitive
epsilon-connected
ordinal
natural
V11
()
V12
()
real
V29
() )
M3
(
K28
() : ( ( ) ( )
set
) ,
K32
() : ( ( ) (
V1
()
epsilon-transitive
epsilon-connected
ordinal
)
M2
(
K6
(
K28
() : ( ( ) ( )
set
) ) : ( ( ) ( )
set
) )) )) holds
(
(
sin
th1
: ( (
real
) (
V11
()
V12
()
real
)
number
)
)
: ( ( ) (
V11
()
V12
()
real
)
set
)
-
(
sin
th2
: ( (
real
) (
V11
()
V12
()
real
)
number
)
)
: ( ( ) (
V11
()
V12
()
real
)
set
)
)
: ( ( ) (
V11
()
V12
()
real
)
set
)
/
(
(
cos
th1
: ( (
real
) (
V11
()
V12
()
real
)
number
)
)
: ( ( ) (
V11
()
V12
()
real
)
set
)
+
(
cos
th2
: ( (
real
) (
V11
()
V12
()
real
)
number
)
)
: ( ( ) (
V11
()
V12
()
real
)
set
)
)
: ( ( ) (
V11
()
V12
()
real
)
set
) : ( ( ) (
V11
()
V12
()
real
)
set
)
=
tan
(
(
th1
: ( (
real
) (
V11
()
V12
()
real
)
number
)
-
th2
: ( (
real
) (
V11
()
V12
()
real
)
number
)
)
: ( ( ) (
V11
()
V12
()
real
)
set
)
/
2 : ( ( ) (
epsilon-transitive
epsilon-connected
ordinal
natural
V11
()
V12
()
real
V29
() )
M3
(
K28
() : ( ( ) ( )
set
) ,
K32
() : ( ( ) (
V1
()
epsilon-transitive
epsilon-connected
ordinal
)
M2
(
K6
(
K28
() : ( ( ) ( )
set
) ) : ( ( ) ( )
set
) )) ))
)
: ( ( ) (
V11
()
V12
()
real
)
set
) : ( ( ) (
V11
()
V12
()
real
)
Real
) ;
theorem
:: SIN_COS4:48
for
th1
,
th2
being ( (
real
) (
V11
()
V12
()
real
)
number
) st
sin
(
(
th1
: ( (
real
) (
V11
()
V12
()
real
)
number
)
+
th2
: ( (
real
) (
V11
()
V12
()
real
)
number
)
)
: ( ( ) (
V11
()
V12
()
real
)
set
)
/
2 : ( ( ) (
epsilon-transitive
epsilon-connected
ordinal
natural
V11
()
V12
()
real
V29
() )
M3
(
K28
() : ( ( ) ( )
set
) ,
K32
() : ( ( ) (
V1
()
epsilon-transitive
epsilon-connected
ordinal
)
M2
(
K6
(
K28
() : ( ( ) ( )
set
) ) : ( ( ) ( )
set
) )) ))
)
: ( ( ) (
V11
()
V12
()
real
)
set
) : ( ( ) (
V11
()
V12
()
real
)
set
)
<>
0
: ( ( ) (
epsilon-transitive
epsilon-connected
ordinal
natural
V11
()
V12
()
real
V29
() )
M3
(
K28
() : ( ( ) ( )
set
) ,
K32
() : ( ( ) (
V1
()
epsilon-transitive
epsilon-connected
ordinal
)
M2
(
K6
(
K28
() : ( ( ) ( )
set
) ) : ( ( ) ( )
set
) )) )) holds
(
(
sin
th1
: ( (
real
) (
V11
()
V12
()
real
)
number
)
)
: ( ( ) (
V11
()
V12
()
real
)
set
)
+
(
sin
th2
: ( (
real
) (
V11
()
V12
()
real
)
number
)
)
: ( ( ) (
V11
()
V12
()
real
)
set
)
)
: ( ( ) (
V11
()
V12
()
real
)
set
)
/
(
(
cos
th2
: ( (
real
) (
V11
()
V12
()
real
)
number
)
)
: ( ( ) (
V11
()
V12
()
real
)
set
)
-
(
cos
th1
: ( (
real
) (
V11
()
V12
()
real
)
number
)
)
: ( ( ) (
V11
()
V12
()
real
)
set
)
)
: ( ( ) (
V11
()
V12
()
real
)
set
) : ( ( ) (
V11
()
V12
()
real
)
set
)
=
cot
(
(
th1
: ( (
real
) (
V11
()
V12
()
real
)
number
)
-
th2
: ( (
real
) (
V11
()
V12
()
real
)
number
)
)
: ( ( ) (
V11
()
V12
()
real
)
set
)
/
2 : ( ( ) (
epsilon-transitive
epsilon-connected
ordinal
natural
V11
()
V12
()
real
V29
() )
M3
(
K28
() : ( ( ) ( )
set
) ,
K32
() : ( ( ) (
V1
()
epsilon-transitive
epsilon-connected
ordinal
)
M2
(
K6
(
K28
() : ( ( ) ( )
set
) ) : ( ( ) ( )
set
) )) ))
)
: ( ( ) (
V11
()
V12
()
real
)
set
) : ( ( ) (
V11
()
V12
()
real
)
Real
) ;
theorem
:: SIN_COS4:49
for
th1
,
th2
being ( (
real
) (
V11
()
V12
()
real
)
number
) st
sin
(
(
th1
: ( (
real
) (
V11
()
V12
()
real
)
number
)
-
th2
: ( (
real
) (
V11
()
V12
()
real
)
number
)
)
: ( ( ) (
V11
()
V12
()
real
)
set
)
/
2 : ( ( ) (
epsilon-transitive
epsilon-connected
ordinal
natural
V11
()
V12
()
real
V29
() )
M3
(
K28
() : ( ( ) ( )
set
) ,
K32
() : ( ( ) (
V1
()
epsilon-transitive
epsilon-connected
ordinal
)
M2
(
K6
(
K28
() : ( ( ) ( )
set
) ) : ( ( ) ( )
set
) )) ))
)
: ( ( ) (
V11
()
V12
()
real
)
set
) : ( ( ) (
V11
()
V12
()
real
)
set
)
<>
0
: ( ( ) (
epsilon-transitive
epsilon-connected
ordinal
natural
V11
()
V12
()
real
V29
() )
M3
(
K28
() : ( ( ) ( )
set
) ,
K32
() : ( ( ) (
V1
()
epsilon-transitive
epsilon-connected
ordinal
)
M2
(
K6
(
K28
() : ( ( ) ( )
set
) ) : ( ( ) ( )
set
) )) )) holds
(
(
sin
th1
: ( (
real
) (
V11
()
V12
()
real
)
number
)
)
: ( ( ) (
V11
()
V12
()
real
)
set
)
-
(
sin
th2
: ( (
real
) (
V11
()
V12
()
real
)
number
)
)
: ( ( ) (
V11
()
V12
()
real
)
set
)
)
: ( ( ) (
V11
()
V12
()
real
)
set
)
/
(
(
cos
th2
: ( (
real
) (
V11
()
V12
()
real
)
number
)
)
: ( ( ) (
V11
()
V12
()
real
)
set
)
-
(
cos
th1
: ( (
real
) (
V11
()
V12
()
real
)
number
)
)
: ( ( ) (
V11
()
V12
()
real
)
set
)
)
: ( ( ) (
V11
()
V12
()
real
)
set
) : ( ( ) (
V11
()
V12
()
real
)
set
)
=
cot
(
(
th1
: ( (
real
) (
V11
()
V12
()
real
)
number
)
+
th2
: ( (
real
) (
V11
()
V12
()
real
)
number
)
)
: ( ( ) (
V11
()
V12
()
real
)
set
)
/
2 : ( ( ) (
epsilon-transitive
epsilon-connected
ordinal
natural
V11
()
V12
()
real
V29
() )
M3
(
K28
() : ( ( ) ( )
set
) ,
K32
() : ( ( ) (
V1
()
epsilon-transitive
epsilon-connected
ordinal
)
M2
(
K6
(
K28
() : ( ( ) ( )
set
) ) : ( ( ) ( )
set
) )) ))
)
: ( ( ) (
V11
()
V12
()
real
)
set
) : ( ( ) (
V11
()
V12
()
real
)
Real
) ;
theorem
:: SIN_COS4:50
for
th1
,
th2
being ( (
real
) (
V11
()
V12
()
real
)
number
) holds
(
(
cos
th1
: ( (
real
) (
V11
()
V12
()
real
)
number
)
)
: ( ( ) (
V11
()
V12
()
real
)
set
)
+
(
cos
th2
: ( (
real
) (
V11
()
V12
()
real
)
number
)
)
: ( ( ) (
V11
()
V12
()
real
)
set
)
)
: ( ( ) (
V11
()
V12
()
real
)
set
)
/
(
(
cos
th1
: ( (
real
) (
V11
()
V12
()
real
)
number
)
)
: ( ( ) (
V11
()
V12
()
real
)
set
)
-
(
cos
th2
: ( (
real
) (
V11
()
V12
()
real
)
number
)
)
: ( ( ) (
V11
()
V12
()
real
)
set
)
)
: ( ( ) (
V11
()
V12
()
real
)
set
) : ( ( ) (
V11
()
V12
()
real
)
set
)
=
(
cot
(
(
th1
: ( (
real
) (
V11
()
V12
()
real
)
number
)
+
th2
: ( (
real
) (
V11
()
V12
()
real
)
number
)
)
: ( ( ) (
V11
()
V12
()
real
)
set
)
/
2 : ( ( ) (
epsilon-transitive
epsilon-connected
ordinal
natural
V11
()
V12
()
real
V29
() )
M3
(
K28
() : ( ( ) ( )
set
) ,
K32
() : ( ( ) (
V1
()
epsilon-transitive
epsilon-connected
ordinal
)
M2
(
K6
(
K28
() : ( ( ) ( )
set
) ) : ( ( ) ( )
set
) )) ))
)
: ( ( ) (
V11
()
V12
()
real
)
set
)
)
: ( ( ) (
V11
()
V12
()
real
)
Real
)
*
(
cot
(
(
th2
: ( (
real
) (
V11
()
V12
()
real
)
number
)
-
th1
: ( (
real
) (
V11
()
V12
()
real
)
number
)
)
: ( ( ) (
V11
()
V12
()
real
)
set
)
/
2 : ( ( ) (
epsilon-transitive
epsilon-connected
ordinal
natural
V11
()
V12
()
real
V29
() )
M3
(
K28
() : ( ( ) ( )
set
) ,
K32
() : ( ( ) (
V1
()
epsilon-transitive
epsilon-connected
ordinal
)
M2
(
K6
(
K28
() : ( ( ) ( )
set
) ) : ( ( ) ( )
set
) )) ))
)
: ( ( ) (
V11
()
V12
()
real
)
set
)
)
: ( ( ) (
V11
()
V12
()
real
)
Real
) : ( ( ) (
V11
()
V12
()
real
)
set
) ;