:: SINCOS10 semantic presentation begin theorem :: SINCOS10:1 (Bool (Set ($#k3_rcomp_1 :::"[."::: ) (Set ($#k6_numbers :::"0"::: ) ) "," (Set "(" (Set ($#k32_sin_cos :::"PI"::: ) ) ($#k10_real_1 :::"/"::: ) (Num 2) ")" ) ($#k3_rcomp_1 :::".["::: ) ) ($#r1_tarski :::"c="::: ) (Set ($#k1_relset_1 :::"dom"::: ) (Set ($#k1_fdiff_9 :::"sec"::: ) ))) ; theorem :: SINCOS10:2 (Bool (Set ($#k4_rcomp_1 :::"]."::: ) (Set "(" (Set ($#k32_sin_cos :::"PI"::: ) ) ($#k10_real_1 :::"/"::: ) (Num 2) ")" ) "," (Set ($#k32_sin_cos :::"PI"::: ) ) ($#k4_rcomp_1 :::".]"::: ) ) ($#r1_tarski :::"c="::: ) (Set ($#k1_relset_1 :::"dom"::: ) (Set ($#k1_fdiff_9 :::"sec"::: ) ))) ; theorem :: SINCOS10:3 (Bool (Set ($#k3_rcomp_1 :::"[."::: ) (Set "(" ($#k1_real_1 :::"-"::: ) (Set "(" (Set ($#k32_sin_cos :::"PI"::: ) ) ($#k10_real_1 :::"/"::: ) (Num 2) ")" ) ")" ) "," (Set ($#k6_numbers :::"0"::: ) ) ($#k3_rcomp_1 :::".["::: ) ) ($#r1_tarski :::"c="::: ) (Set ($#k1_relset_1 :::"dom"::: ) (Set ($#k2_fdiff_9 :::"cosec"::: ) ))) ; theorem :: SINCOS10:4 (Bool (Set ($#k4_rcomp_1 :::"]."::: ) (Set ($#k6_numbers :::"0"::: ) ) "," (Set "(" (Set ($#k32_sin_cos :::"PI"::: ) ) ($#k10_real_1 :::"/"::: ) (Num 2) ")" ) ($#k4_rcomp_1 :::".]"::: ) ) ($#r1_tarski :::"c="::: ) (Set ($#k1_relset_1 :::"dom"::: ) (Set ($#k2_fdiff_9 :::"cosec"::: ) ))) ; theorem :: SINCOS10:5 (Bool "(" (Bool (Set ($#k1_fdiff_9 :::"sec"::: ) ) ($#r2_fdiff_1 :::"is_differentiable_on"::: ) (Set ($#k2_rcomp_1 :::"]."::: ) (Set ($#k6_numbers :::"0"::: ) ) "," (Set "(" (Set ($#k32_sin_cos :::"PI"::: ) ) ($#k10_real_1 :::"/"::: ) (Num 2) ")" ) ($#k2_rcomp_1 :::".["::: ) )) & (Bool "(" "for" (Set (Var "x")) "being" ($#m1_subset_1 :::"Real":::) "st" (Bool (Bool (Set (Var "x")) ($#r2_hidden :::"in"::: ) (Set ($#k2_rcomp_1 :::"]."::: ) (Set ($#k6_numbers :::"0"::: ) ) "," (Set "(" (Set ($#k32_sin_cos :::"PI"::: ) ) ($#k10_real_1 :::"/"::: ) (Num 2) ")" ) ($#k2_rcomp_1 :::".["::: ) ))) "holds" (Bool (Set ($#k1_fdiff_1 :::"diff"::: ) "(" (Set ($#k1_fdiff_9 :::"sec"::: ) ) "," (Set (Var "x")) ")" ) ($#r1_hidden :::"="::: ) (Set (Set "(" (Set ($#k16_sin_cos :::"sin"::: ) ) ($#k1_seq_1 :::"."::: ) (Set (Var "x")) ")" ) ($#k10_real_1 :::"/"::: ) (Set "(" (Set "(" (Set ($#k19_sin_cos :::"cos"::: ) ) ($#k1_seq_1 :::"."::: ) (Set (Var "x")) ")" ) ($#k5_square_1 :::"^2"::: ) ")" ))) ")" ) ")" ) ; theorem :: SINCOS10:6 (Bool "(" (Bool (Set ($#k1_fdiff_9 :::"sec"::: ) ) ($#r2_fdiff_1 :::"is_differentiable_on"::: ) (Set ($#k2_rcomp_1 :::"]."::: ) (Set "(" (Set ($#k32_sin_cos :::"PI"::: ) ) ($#k10_real_1 :::"/"::: ) (Num 2) ")" ) "," (Set ($#k32_sin_cos :::"PI"::: ) ) ($#k2_rcomp_1 :::".["::: ) )) & (Bool "(" "for" (Set (Var "x")) "being" ($#m1_subset_1 :::"Real":::) "st" (Bool (Bool (Set (Var "x")) ($#r2_hidden :::"in"::: ) (Set ($#k2_rcomp_1 :::"]."::: ) (Set "(" (Set ($#k32_sin_cos :::"PI"::: ) ) ($#k10_real_1 :::"/"::: ) (Num 2) ")" ) "," (Set ($#k32_sin_cos :::"PI"::: ) ) ($#k2_rcomp_1 :::".["::: ) ))) "holds" (Bool (Set ($#k1_fdiff_1 :::"diff"::: ) "(" (Set ($#k1_fdiff_9 :::"sec"::: ) ) "," (Set (Var "x")) ")" ) ($#r1_hidden :::"="::: ) (Set (Set "(" (Set ($#k16_sin_cos :::"sin"::: ) ) ($#k1_seq_1 :::"."::: ) (Set (Var "x")) ")" ) ($#k10_real_1 :::"/"::: ) (Set "(" (Set "(" (Set ($#k19_sin_cos :::"cos"::: ) ) ($#k1_seq_1 :::"."::: ) (Set (Var "x")) ")" ) ($#k5_square_1 :::"^2"::: ) ")" ))) ")" ) ")" ) ; theorem :: SINCOS10:7 (Bool "(" (Bool (Set ($#k2_fdiff_9 :::"cosec"::: ) ) ($#r2_fdiff_1 :::"is_differentiable_on"::: ) (Set ($#k2_rcomp_1 :::"]."::: ) (Set "(" ($#k1_real_1 :::"-"::: ) (Set "(" (Set ($#k32_sin_cos :::"PI"::: ) ) ($#k10_real_1 :::"/"::: ) (Num 2) ")" ) ")" ) "," (Set ($#k6_numbers :::"0"::: ) ) ($#k2_rcomp_1 :::".["::: ) )) & (Bool "(" "for" (Set (Var "x")) "being" ($#m1_subset_1 :::"Real":::) "st" (Bool (Bool (Set (Var "x")) ($#r2_hidden :::"in"::: ) (Set ($#k2_rcomp_1 :::"]."::: ) (Set "(" ($#k1_real_1 :::"-"::: ) (Set "(" (Set ($#k32_sin_cos :::"PI"::: ) ) ($#k10_real_1 :::"/"::: ) (Num 2) ")" ) ")" ) "," (Set ($#k6_numbers :::"0"::: ) ) ($#k2_rcomp_1 :::".["::: ) ))) "holds" (Bool (Set ($#k1_fdiff_1 :::"diff"::: ) "(" (Set ($#k2_fdiff_9 :::"cosec"::: ) ) "," (Set (Var "x")) ")" ) ($#r1_hidden :::"="::: ) (Set ($#k1_real_1 :::"-"::: ) (Set "(" (Set "(" (Set ($#k19_sin_cos :::"cos"::: ) ) ($#k1_seq_1 :::"."::: ) (Set (Var "x")) ")" ) ($#k10_real_1 :::"/"::: ) (Set "(" (Set "(" (Set ($#k16_sin_cos :::"sin"::: ) ) ($#k1_seq_1 :::"."::: ) (Set (Var "x")) ")" ) ($#k5_square_1 :::"^2"::: ) ")" ) ")" ))) ")" ) ")" ) ; theorem :: SINCOS10:8 (Bool "(" (Bool (Set ($#k2_fdiff_9 :::"cosec"::: ) ) ($#r2_fdiff_1 :::"is_differentiable_on"::: ) (Set ($#k2_rcomp_1 :::"]."::: ) (Set ($#k6_numbers :::"0"::: ) ) "," (Set "(" (Set ($#k32_sin_cos :::"PI"::: ) ) ($#k10_real_1 :::"/"::: ) (Num 2) ")" ) ($#k2_rcomp_1 :::".["::: ) )) & (Bool "(" "for" (Set (Var "x")) "being" ($#m1_subset_1 :::"Real":::) "st" (Bool (Bool (Set (Var "x")) ($#r2_hidden :::"in"::: ) (Set ($#k2_rcomp_1 :::"]."::: ) (Set ($#k6_numbers :::"0"::: ) ) "," (Set "(" (Set ($#k32_sin_cos :::"PI"::: ) ) ($#k10_real_1 :::"/"::: ) (Num 2) ")" ) ($#k2_rcomp_1 :::".["::: ) ))) "holds" (Bool (Set ($#k1_fdiff_1 :::"diff"::: ) "(" (Set ($#k2_fdiff_9 :::"cosec"::: ) ) "," (Set (Var "x")) ")" ) ($#r1_hidden :::"="::: ) (Set ($#k1_real_1 :::"-"::: ) (Set "(" (Set "(" (Set ($#k19_sin_cos :::"cos"::: ) ) ($#k1_seq_1 :::"."::: ) (Set (Var "x")) ")" ) ($#k10_real_1 :::"/"::: ) (Set "(" (Set "(" (Set ($#k16_sin_cos :::"sin"::: ) ) ($#k1_seq_1 :::"."::: ) (Set (Var "x")) ")" ) ($#k5_square_1 :::"^2"::: ) ")" ) ")" ))) ")" ) ")" ) ; theorem :: SINCOS10:9 (Bool (Set (Set ($#k1_fdiff_9 :::"sec"::: ) ) ($#k2_partfun1 :::"|"::: ) (Set ($#k2_rcomp_1 :::"]."::: ) (Set ($#k6_numbers :::"0"::: ) ) "," (Set "(" (Set ($#k32_sin_cos :::"PI"::: ) ) ($#k10_real_1 :::"/"::: ) (Num 2) ")" ) ($#k2_rcomp_1 :::".["::: ) )) "is" ($#v1_fcont_1 :::"continuous"::: ) ) ; theorem :: SINCOS10:10 (Bool (Set (Set ($#k1_fdiff_9 :::"sec"::: ) ) ($#k2_partfun1 :::"|"::: ) (Set ($#k2_rcomp_1 :::"]."::: ) (Set "(" (Set ($#k32_sin_cos :::"PI"::: ) ) ($#k10_real_1 :::"/"::: ) (Num 2) ")" ) "," (Set ($#k32_sin_cos :::"PI"::: ) ) ($#k2_rcomp_1 :::".["::: ) )) "is" ($#v1_fcont_1 :::"continuous"::: ) ) ; theorem :: SINCOS10:11 (Bool (Set (Set ($#k2_fdiff_9 :::"cosec"::: ) ) ($#k2_partfun1 :::"|"::: ) (Set ($#k2_rcomp_1 :::"]."::: ) (Set "(" ($#k1_real_1 :::"-"::: ) (Set "(" (Set ($#k32_sin_cos :::"PI"::: ) ) ($#k10_real_1 :::"/"::: ) (Num 2) ")" ) ")" ) "," (Set ($#k6_numbers :::"0"::: ) ) ($#k2_rcomp_1 :::".["::: ) )) "is" ($#v1_fcont_1 :::"continuous"::: ) ) ; theorem :: SINCOS10:12 (Bool (Set (Set ($#k2_fdiff_9 :::"cosec"::: ) ) ($#k2_partfun1 :::"|"::: ) (Set ($#k2_rcomp_1 :::"]."::: ) (Set ($#k6_numbers :::"0"::: ) ) "," (Set "(" (Set ($#k32_sin_cos :::"PI"::: ) ) ($#k10_real_1 :::"/"::: ) (Num 2) ")" ) ($#k2_rcomp_1 :::".["::: ) )) "is" ($#v1_fcont_1 :::"continuous"::: ) ) ; theorem :: SINCOS10:13 (Bool (Set (Set ($#k1_fdiff_9 :::"sec"::: ) ) ($#k2_partfun1 :::"|"::: ) (Set ($#k2_rcomp_1 :::"]."::: ) (Set ($#k6_numbers :::"0"::: ) ) "," (Set "(" (Set ($#k32_sin_cos :::"PI"::: ) ) ($#k10_real_1 :::"/"::: ) (Num 2) ")" ) ($#k2_rcomp_1 :::".["::: ) )) "is" ($#v5_valued_0 :::"increasing"::: ) ) ; theorem :: SINCOS10:14 (Bool (Set (Set ($#k1_fdiff_9 :::"sec"::: ) ) ($#k2_partfun1 :::"|"::: ) (Set ($#k2_rcomp_1 :::"]."::: ) (Set "(" (Set ($#k32_sin_cos :::"PI"::: ) ) ($#k10_real_1 :::"/"::: ) (Num 2) ")" ) "," (Set ($#k32_sin_cos :::"PI"::: ) ) ($#k2_rcomp_1 :::".["::: ) )) "is" ($#v5_valued_0 :::"increasing"::: ) ) ; theorem :: SINCOS10:15 (Bool (Set (Set ($#k2_fdiff_9 :::"cosec"::: ) ) ($#k2_partfun1 :::"|"::: ) (Set ($#k2_rcomp_1 :::"]."::: ) (Set "(" ($#k1_real_1 :::"-"::: ) (Set "(" (Set ($#k32_sin_cos :::"PI"::: ) ) ($#k10_real_1 :::"/"::: ) (Num 2) ")" ) ")" ) "," (Set ($#k6_numbers :::"0"::: ) ) ($#k2_rcomp_1 :::".["::: ) )) "is" ($#v6_valued_0 :::"decreasing"::: ) ) ; theorem :: SINCOS10:16 (Bool (Set (Set ($#k2_fdiff_9 :::"cosec"::: ) ) ($#k2_partfun1 :::"|"::: ) (Set ($#k2_rcomp_1 :::"]."::: ) (Set ($#k6_numbers :::"0"::: ) ) "," (Set "(" (Set ($#k32_sin_cos :::"PI"::: ) ) ($#k10_real_1 :::"/"::: ) (Num 2) ")" ) ($#k2_rcomp_1 :::".["::: ) )) "is" ($#v6_valued_0 :::"decreasing"::: ) ) ; theorem :: SINCOS10:17 (Bool (Set (Set ($#k1_fdiff_9 :::"sec"::: ) ) ($#k2_partfun1 :::"|"::: ) (Set ($#k3_rcomp_1 :::"[."::: ) (Set ($#k6_numbers :::"0"::: ) ) "," (Set "(" (Set ($#k32_sin_cos :::"PI"::: ) ) ($#k10_real_1 :::"/"::: ) (Num 2) ")" ) ($#k3_rcomp_1 :::".["::: ) )) "is" ($#v5_valued_0 :::"increasing"::: ) ) ; theorem :: SINCOS10:18 (Bool (Set (Set ($#k1_fdiff_9 :::"sec"::: ) ) ($#k2_partfun1 :::"|"::: ) (Set ($#k4_rcomp_1 :::"]."::: ) (Set "(" (Set ($#k32_sin_cos :::"PI"::: ) ) ($#k10_real_1 :::"/"::: ) (Num 2) ")" ) "," (Set ($#k32_sin_cos :::"PI"::: ) ) ($#k4_rcomp_1 :::".]"::: ) )) "is" ($#v5_valued_0 :::"increasing"::: ) ) ; theorem :: SINCOS10:19 (Bool (Set (Set ($#k2_fdiff_9 :::"cosec"::: ) ) ($#k2_partfun1 :::"|"::: ) (Set ($#k3_rcomp_1 :::"[."::: ) (Set "(" ($#k1_real_1 :::"-"::: ) (Set "(" (Set ($#k32_sin_cos :::"PI"::: ) ) ($#k10_real_1 :::"/"::: ) (Num 2) ")" ) ")" ) "," (Set ($#k6_numbers :::"0"::: ) ) ($#k3_rcomp_1 :::".["::: ) )) "is" ($#v6_valued_0 :::"decreasing"::: ) ) ; theorem :: SINCOS10:20 (Bool (Set (Set ($#k2_fdiff_9 :::"cosec"::: ) ) ($#k2_partfun1 :::"|"::: ) (Set ($#k4_rcomp_1 :::"]."::: ) (Set ($#k6_numbers :::"0"::: ) ) "," (Set "(" (Set ($#k32_sin_cos :::"PI"::: ) ) ($#k10_real_1 :::"/"::: ) (Num 2) ")" ) ($#k4_rcomp_1 :::".]"::: ) )) "is" ($#v6_valued_0 :::"decreasing"::: ) ) ; theorem :: SINCOS10:21 (Bool (Set (Set ($#k1_fdiff_9 :::"sec"::: ) ) ($#k2_partfun1 :::"|"::: ) (Set ($#k3_rcomp_1 :::"[."::: ) (Set ($#k6_numbers :::"0"::: ) ) "," (Set "(" (Set ($#k32_sin_cos :::"PI"::: ) ) ($#k10_real_1 :::"/"::: ) (Num 2) ")" ) ($#k3_rcomp_1 :::".["::: ) )) "is" ($#v2_funct_1 :::"one-to-one"::: ) ) ; theorem :: SINCOS10:22 (Bool (Set (Set ($#k1_fdiff_9 :::"sec"::: ) ) ($#k2_partfun1 :::"|"::: ) (Set ($#k4_rcomp_1 :::"]."::: ) (Set "(" (Set ($#k32_sin_cos :::"PI"::: ) ) ($#k10_real_1 :::"/"::: ) (Num 2) ")" ) "," (Set ($#k32_sin_cos :::"PI"::: ) ) ($#k4_rcomp_1 :::".]"::: ) )) "is" ($#v2_funct_1 :::"one-to-one"::: ) ) ; theorem :: SINCOS10:23 (Bool (Set (Set ($#k2_fdiff_9 :::"cosec"::: ) ) ($#k2_partfun1 :::"|"::: ) (Set ($#k3_rcomp_1 :::"[."::: ) (Set "(" ($#k1_real_1 :::"-"::: ) (Set "(" (Set ($#k32_sin_cos :::"PI"::: ) ) ($#k10_real_1 :::"/"::: ) (Num 2) ")" ) ")" ) "," (Set ($#k6_numbers :::"0"::: ) ) ($#k3_rcomp_1 :::".["::: ) )) "is" ($#v2_funct_1 :::"one-to-one"::: ) ) ; theorem :: SINCOS10:24 (Bool (Set (Set ($#k2_fdiff_9 :::"cosec"::: ) ) ($#k2_partfun1 :::"|"::: ) (Set ($#k4_rcomp_1 :::"]."::: ) (Set ($#k6_numbers :::"0"::: ) ) "," (Set "(" (Set ($#k32_sin_cos :::"PI"::: ) ) ($#k10_real_1 :::"/"::: ) (Num 2) ")" ) ($#k4_rcomp_1 :::".]"::: ) )) "is" ($#v2_funct_1 :::"one-to-one"::: ) ) ; registration cluster (Set bbbadK5_RELAT_1((Set ($#k1_fdiff_9 :::"sec"::: ) ) "," (Set ($#k3_rcomp_1 :::"[."::: ) (Set ($#k6_numbers :::"0"::: ) ) "," (Set "(" (Set ($#k32_sin_cos :::"PI"::: ) ) ($#k10_real_1 :::"/"::: ) (Num 2) ")" ) ($#k3_rcomp_1 :::".["::: ) ))) -> ($#v2_funct_1 :::"one-to-one"::: ) ; cluster (Set bbbadK5_RELAT_1((Set ($#k1_fdiff_9 :::"sec"::: ) ) "," (Set ($#k4_rcomp_1 :::"]."::: ) (Set "(" (Set ($#k32_sin_cos :::"PI"::: ) ) ($#k10_real_1 :::"/"::: ) (Num 2) ")" ) "," (Set ($#k32_sin_cos :::"PI"::: ) ) ($#k4_rcomp_1 :::".]"::: ) ))) -> ($#v2_funct_1 :::"one-to-one"::: ) ; cluster (Set bbbadK5_RELAT_1((Set ($#k2_fdiff_9 :::"cosec"::: ) ) "," (Set ($#k3_rcomp_1 :::"[."::: ) (Set "(" ($#k1_real_1 :::"-"::: ) (Set "(" (Set ($#k32_sin_cos :::"PI"::: ) ) ($#k10_real_1 :::"/"::: ) (Num 2) ")" ) ")" ) "," (Set ($#k6_numbers :::"0"::: ) ) ($#k3_rcomp_1 :::".["::: ) ))) -> ($#v2_funct_1 :::"one-to-one"::: ) ; cluster (Set bbbadK5_RELAT_1((Set ($#k2_fdiff_9 :::"cosec"::: ) ) "," (Set ($#k4_rcomp_1 :::"]."::: ) (Set ($#k6_numbers :::"0"::: ) ) "," (Set "(" (Set ($#k32_sin_cos :::"PI"::: ) ) ($#k10_real_1 :::"/"::: ) (Num 2) ")" ) ($#k4_rcomp_1 :::".]"::: ) ))) -> ($#v2_funct_1 :::"one-to-one"::: ) ; end; definitionfunc :::"arcsec1"::: -> ($#m1_subset_1 :::"PartFunc":::) "of" (Set ($#k1_numbers :::"REAL"::: ) ) "," (Set ($#k1_numbers :::"REAL"::: ) ) equals :: SINCOS10:def 1 (Set (Set "(" (Set ($#k1_fdiff_9 :::"sec"::: ) ) ($#k2_partfun1 :::"|"::: ) (Set ($#k3_rcomp_1 :::"[."::: ) (Set ($#k6_numbers :::"0"::: ) ) "," (Set "(" (Set ($#k32_sin_cos :::"PI"::: ) ) ($#k10_real_1 :::"/"::: ) (Num 2) ")" ) ($#k3_rcomp_1 :::".["::: ) ) ")" ) ($#k2_partfun2 :::"""::: ) ); func :::"arcsec2"::: -> ($#m1_subset_1 :::"PartFunc":::) "of" (Set ($#k1_numbers :::"REAL"::: ) ) "," (Set ($#k1_numbers :::"REAL"::: ) ) equals :: SINCOS10:def 2 (Set (Set "(" (Set ($#k1_fdiff_9 :::"sec"::: ) ) ($#k2_partfun1 :::"|"::: ) (Set ($#k4_rcomp_1 :::"]."::: ) (Set "(" (Set ($#k32_sin_cos :::"PI"::: ) ) ($#k10_real_1 :::"/"::: ) (Num 2) ")" ) "," (Set ($#k32_sin_cos :::"PI"::: ) ) ($#k4_rcomp_1 :::".]"::: ) ) ")" ) ($#k2_partfun2 :::"""::: ) ); func :::"arccosec1"::: -> ($#m1_subset_1 :::"PartFunc":::) "of" (Set ($#k1_numbers :::"REAL"::: ) ) "," (Set ($#k1_numbers :::"REAL"::: ) ) equals :: SINCOS10:def 3 (Set (Set "(" (Set ($#k2_fdiff_9 :::"cosec"::: ) ) ($#k2_partfun1 :::"|"::: ) (Set ($#k3_rcomp_1 :::"[."::: ) (Set "(" ($#k1_real_1 :::"-"::: ) (Set "(" (Set ($#k32_sin_cos :::"PI"::: ) ) ($#k10_real_1 :::"/"::: ) (Num 2) ")" ) ")" ) "," (Set ($#k6_numbers :::"0"::: ) ) ($#k3_rcomp_1 :::".["::: ) ) ")" ) ($#k2_partfun2 :::"""::: ) ); func :::"arccosec2"::: -> ($#m1_subset_1 :::"PartFunc":::) "of" (Set ($#k1_numbers :::"REAL"::: ) ) "," (Set ($#k1_numbers :::"REAL"::: ) ) equals :: SINCOS10:def 4 (Set (Set "(" (Set ($#k2_fdiff_9 :::"cosec"::: ) ) ($#k2_partfun1 :::"|"::: ) (Set ($#k4_rcomp_1 :::"]."::: ) (Set ($#k6_numbers :::"0"::: ) ) "," (Set "(" (Set ($#k32_sin_cos :::"PI"::: ) ) ($#k10_real_1 :::"/"::: ) (Num 2) ")" ) ($#k4_rcomp_1 :::".]"::: ) ) ")" ) ($#k2_partfun2 :::"""::: ) ); end; :: deftheorem defines :::"arcsec1"::: SINCOS10:def 1 : (Bool (Set ($#k1_sincos10 :::"arcsec1"::: ) ) ($#r1_hidden :::"="::: ) (Set (Set "(" (Set ($#k1_fdiff_9 :::"sec"::: ) ) ($#k2_partfun1 :::"|"::: ) (Set ($#k3_rcomp_1 :::"[."::: ) (Set ($#k6_numbers :::"0"::: ) ) "," (Set "(" (Set ($#k32_sin_cos :::"PI"::: ) ) ($#k10_real_1 :::"/"::: ) (Num 2) ")" ) ($#k3_rcomp_1 :::".["::: ) ) ")" ) ($#k2_partfun2 :::"""::: ) )); :: deftheorem defines :::"arcsec2"::: SINCOS10:def 2 : (Bool (Set ($#k2_sincos10 :::"arcsec2"::: ) ) ($#r1_hidden :::"="::: ) (Set (Set "(" (Set ($#k1_fdiff_9 :::"sec"::: ) ) ($#k2_partfun1 :::"|"::: ) (Set ($#k4_rcomp_1 :::"]."::: ) (Set "(" (Set ($#k32_sin_cos :::"PI"::: ) ) ($#k10_real_1 :::"/"::: ) (Num 2) ")" ) "," (Set ($#k32_sin_cos :::"PI"::: ) ) ($#k4_rcomp_1 :::".]"::: ) ) ")" ) ($#k2_partfun2 :::"""::: ) )); :: deftheorem defines :::"arccosec1"::: SINCOS10:def 3 : (Bool (Set ($#k3_sincos10 :::"arccosec1"::: ) ) ($#r1_hidden :::"="::: ) (Set (Set "(" (Set ($#k2_fdiff_9 :::"cosec"::: ) ) ($#k2_partfun1 :::"|"::: ) (Set ($#k3_rcomp_1 :::"[."::: ) (Set "(" ($#k1_real_1 :::"-"::: ) (Set "(" (Set ($#k32_sin_cos :::"PI"::: ) ) ($#k10_real_1 :::"/"::: ) (Num 2) ")" ) ")" ) "," (Set ($#k6_numbers :::"0"::: ) ) ($#k3_rcomp_1 :::".["::: ) ) ")" ) ($#k2_partfun2 :::"""::: ) )); :: deftheorem defines :::"arccosec2"::: SINCOS10:def 4 : (Bool (Set ($#k4_sincos10 :::"arccosec2"::: ) ) ($#r1_hidden :::"="::: ) (Set (Set "(" (Set ($#k2_fdiff_9 :::"cosec"::: ) ) ($#k2_partfun1 :::"|"::: ) (Set ($#k4_rcomp_1 :::"]."::: ) (Set ($#k6_numbers :::"0"::: ) ) "," (Set "(" (Set ($#k32_sin_cos :::"PI"::: ) ) ($#k10_real_1 :::"/"::: ) (Num 2) ")" ) ($#k4_rcomp_1 :::".]"::: ) ) ")" ) ($#k2_partfun2 :::"""::: ) )); definitionlet "r" be ($#m1_subset_1 :::"Real":::); func :::"arcsec1"::: "r" -> ($#m1_hidden :::"set"::: ) equals :: SINCOS10:def 5 (Set (Set ($#k1_sincos10 :::"arcsec1"::: ) ) ($#k1_seq_1 :::"."::: ) "r"); func :::"arcsec2"::: "r" -> ($#m1_hidden :::"set"::: ) equals :: SINCOS10:def 6 (Set (Set ($#k2_sincos10 :::"arcsec2"::: ) ) ($#k1_seq_1 :::"."::: ) "r"); func :::"arccosec1"::: "r" -> ($#m1_hidden :::"set"::: ) equals :: SINCOS10:def 7 (Set (Set ($#k3_sincos10 :::"arccosec1"::: ) ) ($#k1_seq_1 :::"."::: ) "r"); func :::"arccosec2"::: "r" -> ($#m1_hidden :::"set"::: ) equals :: SINCOS10:def 8 (Set (Set ($#k4_sincos10 :::"arccosec2"::: ) ) ($#k1_seq_1 :::"."::: ) "r"); end; :: deftheorem defines :::"arcsec1"::: SINCOS10:def 5 : (Bool "for" (Set (Var "r")) "being" ($#m1_subset_1 :::"Real":::) "holds" (Bool (Set ($#k5_sincos10 :::"arcsec1"::: ) (Set (Var "r"))) ($#r1_hidden :::"="::: ) (Set (Set ($#k1_sincos10 :::"arcsec1"::: ) ) ($#k1_seq_1 :::"."::: ) (Set (Var "r"))))); :: deftheorem defines :::"arcsec2"::: SINCOS10:def 6 : (Bool "for" (Set (Var "r")) "being" ($#m1_subset_1 :::"Real":::) "holds" (Bool (Set ($#k6_sincos10 :::"arcsec2"::: ) (Set (Var "r"))) ($#r1_hidden :::"="::: ) (Set (Set ($#k2_sincos10 :::"arcsec2"::: ) ) ($#k1_seq_1 :::"."::: ) (Set (Var "r"))))); :: deftheorem defines :::"arccosec1"::: SINCOS10:def 7 : (Bool "for" (Set (Var "r")) "being" ($#m1_subset_1 :::"Real":::) "holds" (Bool (Set ($#k7_sincos10 :::"arccosec1"::: ) (Set (Var "r"))) ($#r1_hidden :::"="::: ) (Set (Set ($#k3_sincos10 :::"arccosec1"::: ) ) ($#k1_seq_1 :::"."::: ) (Set (Var "r"))))); :: deftheorem defines :::"arccosec2"::: SINCOS10:def 8 : (Bool "for" (Set (Var "r")) "being" ($#m1_subset_1 :::"Real":::) "holds" (Bool (Set ($#k8_sincos10 :::"arccosec2"::: ) (Set (Var "r"))) ($#r1_hidden :::"="::: ) (Set (Set ($#k4_sincos10 :::"arccosec2"::: ) ) ($#k1_seq_1 :::"."::: ) (Set (Var "r"))))); definitionlet "r" be ($#m1_subset_1 :::"Real":::); :: original: :::"arcsec1"::: redefine func :::"arcsec1"::: "r" -> ($#m1_subset_1 :::"Real":::); :: original: :::"arcsec2"::: redefine func :::"arcsec2"::: "r" -> ($#m1_subset_1 :::"Real":::); :: original: :::"arccosec1"::: redefine func :::"arccosec1"::: "r" -> ($#m1_subset_1 :::"Real":::); :: original: :::"arccosec2"::: redefine func :::"arccosec2"::: "r" -> ($#m1_subset_1 :::"Real":::); end; theorem :: SINCOS10:25 (Bool (Set ($#k2_relset_1 :::"rng"::: ) (Set ($#k1_sincos10 :::"arcsec1"::: ) )) ($#r1_hidden :::"="::: ) (Set ($#k3_rcomp_1 :::"[."::: ) (Set ($#k6_numbers :::"0"::: ) ) "," (Set "(" (Set ($#k32_sin_cos :::"PI"::: ) ) ($#k10_real_1 :::"/"::: ) (Num 2) ")" ) ($#k3_rcomp_1 :::".["::: ) )) ; theorem :: SINCOS10:26 (Bool (Set ($#k2_relset_1 :::"rng"::: ) (Set ($#k2_sincos10 :::"arcsec2"::: ) )) ($#r1_hidden :::"="::: ) (Set ($#k4_rcomp_1 :::"]."::: ) (Set "(" (Set ($#k32_sin_cos :::"PI"::: ) ) ($#k10_real_1 :::"/"::: ) (Num 2) ")" ) "," (Set ($#k32_sin_cos :::"PI"::: ) ) ($#k4_rcomp_1 :::".]"::: ) )) ; theorem :: SINCOS10:27 (Bool (Set ($#k2_relset_1 :::"rng"::: ) (Set ($#k3_sincos10 :::"arccosec1"::: ) )) ($#r1_hidden :::"="::: ) (Set ($#k3_rcomp_1 :::"[."::: ) (Set "(" ($#k1_real_1 :::"-"::: ) (Set "(" (Set ($#k32_sin_cos :::"PI"::: ) ) ($#k10_real_1 :::"/"::: ) (Num 2) ")" ) ")" ) "," (Set ($#k6_numbers :::"0"::: ) ) ($#k3_rcomp_1 :::".["::: ) )) ; theorem :: SINCOS10:28 (Bool (Set ($#k2_relset_1 :::"rng"::: ) (Set ($#k4_sincos10 :::"arccosec2"::: ) )) ($#r1_hidden :::"="::: ) (Set ($#k4_rcomp_1 :::"]."::: ) (Set ($#k6_numbers :::"0"::: ) ) "," (Set "(" (Set ($#k32_sin_cos :::"PI"::: ) ) ($#k10_real_1 :::"/"::: ) (Num 2) ")" ) ($#k4_rcomp_1 :::".]"::: ) )) ; registration cluster (Set ($#k1_sincos10 :::"arcsec1"::: ) ) -> ($#v2_funct_1 :::"one-to-one"::: ) ; cluster (Set ($#k2_sincos10 :::"arcsec2"::: ) ) -> ($#v2_funct_1 :::"one-to-one"::: ) ; cluster (Set ($#k3_sincos10 :::"arccosec1"::: ) ) -> ($#v2_funct_1 :::"one-to-one"::: ) ; cluster (Set ($#k4_sincos10 :::"arccosec2"::: ) ) -> ($#v2_funct_1 :::"one-to-one"::: ) ; end; theorem :: SINCOS10:29 (Bool "(" (Bool (Set (Set ($#k16_sin_cos :::"sin"::: ) ) ($#k1_seq_1 :::"."::: ) (Set "(" (Set ($#k32_sin_cos :::"PI"::: ) ) ($#k10_real_1 :::"/"::: ) (Num 4) ")" )) ($#r1_hidden :::"="::: ) (Set (Num 1) ($#k10_real_1 :::"/"::: ) (Set "(" ($#k7_square_1 :::"sqrt"::: ) (Num 2) ")" ))) & (Bool (Set (Set ($#k19_sin_cos :::"cos"::: ) ) ($#k1_seq_1 :::"."::: ) (Set "(" (Set ($#k32_sin_cos :::"PI"::: ) ) ($#k10_real_1 :::"/"::: ) (Num 4) ")" )) ($#r1_hidden :::"="::: ) (Set (Num 1) ($#k10_real_1 :::"/"::: ) (Set "(" ($#k7_square_1 :::"sqrt"::: ) (Num 2) ")" ))) ")" ) ; theorem :: SINCOS10:30 (Bool "(" (Bool (Set (Set ($#k16_sin_cos :::"sin"::: ) ) ($#k1_seq_1 :::"."::: ) (Set "(" ($#k1_real_1 :::"-"::: ) (Set "(" (Set ($#k32_sin_cos :::"PI"::: ) ) ($#k10_real_1 :::"/"::: ) (Num 4) ")" ) ")" )) ($#r1_hidden :::"="::: ) (Set ($#k1_real_1 :::"-"::: ) (Set "(" (Num 1) ($#k10_real_1 :::"/"::: ) (Set "(" ($#k7_square_1 :::"sqrt"::: ) (Num 2) ")" ) ")" ))) & (Bool (Set (Set ($#k19_sin_cos :::"cos"::: ) ) ($#k1_seq_1 :::"."::: ) (Set "(" ($#k1_real_1 :::"-"::: ) (Set "(" (Set ($#k32_sin_cos :::"PI"::: ) ) ($#k10_real_1 :::"/"::: ) (Num 4) ")" ) ")" )) ($#r1_hidden :::"="::: ) (Set (Num 1) ($#k10_real_1 :::"/"::: ) (Set "(" ($#k7_square_1 :::"sqrt"::: ) (Num 2) ")" ))) & (Bool (Set (Set ($#k16_sin_cos :::"sin"::: ) ) ($#k1_seq_1 :::"."::: ) (Set "(" (Set "(" (Num 3) ($#k10_real_1 :::"/"::: ) (Num 4) ")" ) ($#k8_real_1 :::"*"::: ) (Set ($#k32_sin_cos :::"PI"::: ) ) ")" )) ($#r1_hidden :::"="::: ) (Set (Num 1) ($#k10_real_1 :::"/"::: ) (Set "(" ($#k7_square_1 :::"sqrt"::: ) (Num 2) ")" ))) & (Bool (Set (Set ($#k19_sin_cos :::"cos"::: ) ) ($#k1_seq_1 :::"."::: ) (Set "(" (Set "(" (Num 3) ($#k10_real_1 :::"/"::: ) (Num 4) ")" ) ($#k8_real_1 :::"*"::: ) (Set ($#k32_sin_cos :::"PI"::: ) ) ")" )) ($#r1_hidden :::"="::: ) (Set ($#k1_real_1 :::"-"::: ) (Set "(" (Num 1) ($#k10_real_1 :::"/"::: ) (Set "(" ($#k7_square_1 :::"sqrt"::: ) (Num 2) ")" ) ")" ))) ")" ) ; theorem :: SINCOS10:31 (Bool "(" (Bool (Set (Set ($#k1_fdiff_9 :::"sec"::: ) ) ($#k1_seq_1 :::"."::: ) (Set ($#k6_numbers :::"0"::: ) )) ($#r1_hidden :::"="::: ) (Num 1)) & (Bool (Set (Set ($#k1_fdiff_9 :::"sec"::: ) ) ($#k1_seq_1 :::"."::: ) (Set "(" (Set ($#k32_sin_cos :::"PI"::: ) ) ($#k10_real_1 :::"/"::: ) (Num 4) ")" )) ($#r1_hidden :::"="::: ) (Set ($#k7_square_1 :::"sqrt"::: ) (Num 2))) & (Bool (Set (Set ($#k1_fdiff_9 :::"sec"::: ) ) ($#k1_seq_1 :::"."::: ) (Set "(" (Set "(" (Num 3) ($#k10_real_1 :::"/"::: ) (Num 4) ")" ) ($#k8_real_1 :::"*"::: ) (Set ($#k32_sin_cos :::"PI"::: ) ) ")" )) ($#r1_hidden :::"="::: ) (Set ($#k1_real_1 :::"-"::: ) (Set "(" ($#k7_square_1 :::"sqrt"::: ) (Num 2) ")" ))) & (Bool (Set (Set ($#k1_fdiff_9 :::"sec"::: ) ) ($#k1_seq_1 :::"."::: ) (Set ($#k32_sin_cos :::"PI"::: ) )) ($#r1_hidden :::"="::: ) (Set ($#k1_real_1 :::"-"::: ) (Num 1))) ")" ) ; theorem :: SINCOS10:32 (Bool "(" (Bool (Set (Set ($#k2_fdiff_9 :::"cosec"::: ) ) ($#k1_seq_1 :::"."::: ) (Set "(" ($#k1_real_1 :::"-"::: ) (Set "(" (Set ($#k32_sin_cos :::"PI"::: ) ) ($#k10_real_1 :::"/"::: ) (Num 2) ")" ) ")" )) ($#r1_hidden :::"="::: ) (Set ($#k1_real_1 :::"-"::: ) (Num 1))) & (Bool (Set (Set ($#k2_fdiff_9 :::"cosec"::: ) ) ($#k1_seq_1 :::"."::: ) (Set "(" ($#k1_real_1 :::"-"::: ) (Set "(" (Set ($#k32_sin_cos :::"PI"::: ) ) ($#k10_real_1 :::"/"::: ) (Num 4) ")" ) ")" )) ($#r1_hidden :::"="::: ) (Set ($#k1_real_1 :::"-"::: ) (Set "(" ($#k7_square_1 :::"sqrt"::: ) (Num 2) ")" ))) & (Bool (Set (Set ($#k2_fdiff_9 :::"cosec"::: ) ) ($#k1_seq_1 :::"."::: ) (Set "(" (Set ($#k32_sin_cos :::"PI"::: ) ) ($#k10_real_1 :::"/"::: ) (Num 4) ")" )) ($#r1_hidden :::"="::: ) (Set ($#k7_square_1 :::"sqrt"::: ) (Num 2))) & (Bool (Set (Set ($#k2_fdiff_9 :::"cosec"::: ) ) ($#k1_seq_1 :::"."::: ) (Set "(" (Set ($#k32_sin_cos :::"PI"::: ) ) ($#k10_real_1 :::"/"::: ) (Num 2) ")" )) ($#r1_hidden :::"="::: ) (Num 1)) ")" ) ; theorem :: SINCOS10:33 (Bool "for" (Set (Var "x")) "being" ($#m1_hidden :::"set"::: ) "st" (Bool (Bool (Set (Var "x")) ($#r2_hidden :::"in"::: ) (Set ($#k1_rcomp_1 :::"[."::: ) (Set ($#k6_numbers :::"0"::: ) ) "," (Set "(" (Set ($#k32_sin_cos :::"PI"::: ) ) ($#k10_real_1 :::"/"::: ) (Num 4) ")" ) ($#k1_rcomp_1 :::".]"::: ) ))) "holds" (Bool (Set (Set ($#k1_fdiff_9 :::"sec"::: ) ) ($#k1_seq_1 :::"."::: ) (Set (Var "x"))) ($#r2_hidden :::"in"::: ) (Set ($#k1_rcomp_1 :::"[."::: ) (Num 1) "," (Set "(" ($#k7_square_1 :::"sqrt"::: ) (Num 2) ")" ) ($#k1_rcomp_1 :::".]"::: ) ))) ; theorem :: SINCOS10:34 (Bool "for" (Set (Var "x")) "being" ($#m1_hidden :::"set"::: ) "st" (Bool (Bool (Set (Var "x")) ($#r2_hidden :::"in"::: ) (Set ($#k1_rcomp_1 :::"[."::: ) (Set "(" (Set "(" (Num 3) ($#k10_real_1 :::"/"::: ) (Num 4) ")" ) ($#k8_real_1 :::"*"::: ) (Set ($#k32_sin_cos :::"PI"::: ) ) ")" ) "," (Set ($#k32_sin_cos :::"PI"::: ) ) ($#k1_rcomp_1 :::".]"::: ) ))) "holds" (Bool (Set (Set ($#k1_fdiff_9 :::"sec"::: ) ) ($#k1_seq_1 :::"."::: ) (Set (Var "x"))) ($#r2_hidden :::"in"::: ) (Set ($#k1_rcomp_1 :::"[."::: ) (Set "(" ($#k1_real_1 :::"-"::: ) (Set "(" ($#k7_square_1 :::"sqrt"::: ) (Num 2) ")" ) ")" ) "," (Set "(" ($#k1_real_1 :::"-"::: ) (Num 1) ")" ) ($#k1_rcomp_1 :::".]"::: ) ))) ; theorem :: SINCOS10:35 (Bool "for" (Set (Var "x")) "being" ($#m1_hidden :::"set"::: ) "st" (Bool (Bool (Set (Var "x")) ($#r2_hidden :::"in"::: ) (Set ($#k1_rcomp_1 :::"[."::: ) (Set "(" ($#k1_real_1 :::"-"::: ) (Set "(" (Set ($#k32_sin_cos :::"PI"::: ) ) ($#k10_real_1 :::"/"::: ) (Num 2) ")" ) ")" ) "," (Set "(" ($#k1_real_1 :::"-"::: ) (Set "(" (Set ($#k32_sin_cos :::"PI"::: ) ) ($#k10_real_1 :::"/"::: ) (Num 4) ")" ) ")" ) ($#k1_rcomp_1 :::".]"::: ) ))) "holds" (Bool (Set (Set ($#k2_fdiff_9 :::"cosec"::: ) ) ($#k1_seq_1 :::"."::: ) (Set (Var "x"))) ($#r2_hidden :::"in"::: ) (Set ($#k1_rcomp_1 :::"[."::: ) (Set "(" ($#k1_real_1 :::"-"::: ) (Set "(" ($#k7_square_1 :::"sqrt"::: ) (Num 2) ")" ) ")" ) "," (Set "(" ($#k1_real_1 :::"-"::: ) (Num 1) ")" ) ($#k1_rcomp_1 :::".]"::: ) ))) ; theorem :: SINCOS10:36 (Bool "for" (Set (Var "x")) "being" ($#m1_hidden :::"set"::: ) "st" (Bool (Bool (Set (Var "x")) ($#r2_hidden :::"in"::: ) (Set ($#k1_rcomp_1 :::"[."::: ) (Set "(" (Set ($#k32_sin_cos :::"PI"::: ) ) ($#k10_real_1 :::"/"::: ) (Num 4) ")" ) "," (Set "(" (Set ($#k32_sin_cos :::"PI"::: ) ) ($#k10_real_1 :::"/"::: ) (Num 2) ")" ) ($#k1_rcomp_1 :::".]"::: ) ))) "holds" (Bool (Set (Set ($#k2_fdiff_9 :::"cosec"::: ) ) ($#k1_seq_1 :::"."::: ) (Set (Var "x"))) ($#r2_hidden :::"in"::: ) (Set ($#k1_rcomp_1 :::"[."::: ) (Num 1) "," (Set "(" ($#k7_square_1 :::"sqrt"::: ) (Num 2) ")" ) ($#k1_rcomp_1 :::".]"::: ) ))) ; theorem :: SINCOS10:37 (Bool (Set (Set ($#k1_fdiff_9 :::"sec"::: ) ) ($#k2_partfun1 :::"|"::: ) (Set ($#k3_rcomp_1 :::"[."::: ) (Set ($#k6_numbers :::"0"::: ) ) "," (Set "(" (Set ($#k32_sin_cos :::"PI"::: ) ) ($#k10_real_1 :::"/"::: ) (Num 2) ")" ) ($#k3_rcomp_1 :::".["::: ) )) "is" ($#v1_fcont_1 :::"continuous"::: ) ) ; theorem :: SINCOS10:38 (Bool (Set (Set ($#k1_fdiff_9 :::"sec"::: ) ) ($#k2_partfun1 :::"|"::: ) (Set ($#k4_rcomp_1 :::"]."::: ) (Set "(" (Set ($#k32_sin_cos :::"PI"::: ) ) ($#k10_real_1 :::"/"::: ) (Num 2) ")" ) "," (Set ($#k32_sin_cos :::"PI"::: ) ) ($#k4_rcomp_1 :::".]"::: ) )) "is" ($#v1_fcont_1 :::"continuous"::: ) ) ; theorem :: SINCOS10:39 (Bool (Set (Set ($#k2_fdiff_9 :::"cosec"::: ) ) ($#k2_partfun1 :::"|"::: ) (Set ($#k3_rcomp_1 :::"[."::: ) (Set "(" ($#k1_real_1 :::"-"::: ) (Set "(" (Set ($#k32_sin_cos :::"PI"::: ) ) ($#k10_real_1 :::"/"::: ) (Num 2) ")" ) ")" ) "," (Set ($#k6_numbers :::"0"::: ) ) ($#k3_rcomp_1 :::".["::: ) )) "is" ($#v1_fcont_1 :::"continuous"::: ) ) ; theorem :: SINCOS10:40 (Bool (Set (Set ($#k2_fdiff_9 :::"cosec"::: ) ) ($#k2_partfun1 :::"|"::: ) (Set ($#k4_rcomp_1 :::"]."::: ) (Set ($#k6_numbers :::"0"::: ) ) "," (Set "(" (Set ($#k32_sin_cos :::"PI"::: ) ) ($#k10_real_1 :::"/"::: ) (Num 2) ")" ) ($#k4_rcomp_1 :::".]"::: ) )) "is" ($#v1_fcont_1 :::"continuous"::: ) ) ; theorem :: SINCOS10:41 (Bool (Set ($#k2_relset_1 :::"rng"::: ) (Set "(" (Set ($#k1_fdiff_9 :::"sec"::: ) ) ($#k2_partfun1 :::"|"::: ) (Set ($#k1_rcomp_1 :::"[."::: ) (Set ($#k6_numbers :::"0"::: ) ) "," (Set "(" (Set ($#k32_sin_cos :::"PI"::: ) ) ($#k10_real_1 :::"/"::: ) (Num 4) ")" ) ($#k1_rcomp_1 :::".]"::: ) ) ")" )) ($#r1_hidden :::"="::: ) (Set ($#k1_rcomp_1 :::"[."::: ) (Num 1) "," (Set "(" ($#k7_square_1 :::"sqrt"::: ) (Num 2) ")" ) ($#k1_rcomp_1 :::".]"::: ) )) ; theorem :: SINCOS10:42 (Bool (Set ($#k2_relset_1 :::"rng"::: ) (Set "(" (Set ($#k1_fdiff_9 :::"sec"::: ) ) ($#k2_partfun1 :::"|"::: ) (Set ($#k1_rcomp_1 :::"[."::: ) (Set "(" (Set "(" (Num 3) ($#k10_real_1 :::"/"::: ) (Num 4) ")" ) ($#k8_real_1 :::"*"::: ) (Set ($#k32_sin_cos :::"PI"::: ) ) ")" ) "," (Set ($#k32_sin_cos :::"PI"::: ) ) ($#k1_rcomp_1 :::".]"::: ) ) ")" )) ($#r1_hidden :::"="::: ) (Set ($#k1_rcomp_1 :::"[."::: ) (Set "(" ($#k1_real_1 :::"-"::: ) (Set "(" ($#k7_square_1 :::"sqrt"::: ) (Num 2) ")" ) ")" ) "," (Set "(" ($#k1_real_1 :::"-"::: ) (Num 1) ")" ) ($#k1_rcomp_1 :::".]"::: ) )) ; theorem :: SINCOS10:43 (Bool (Set ($#k2_relset_1 :::"rng"::: ) (Set "(" (Set ($#k2_fdiff_9 :::"cosec"::: ) ) ($#k2_partfun1 :::"|"::: ) (Set ($#k1_rcomp_1 :::"[."::: ) (Set "(" ($#k1_real_1 :::"-"::: ) (Set "(" (Set ($#k32_sin_cos :::"PI"::: ) ) ($#k10_real_1 :::"/"::: ) (Num 2) ")" ) ")" ) "," (Set "(" ($#k1_real_1 :::"-"::: ) (Set "(" (Set ($#k32_sin_cos :::"PI"::: ) ) ($#k10_real_1 :::"/"::: ) (Num 4) ")" ) ")" ) ($#k1_rcomp_1 :::".]"::: ) ) ")" )) ($#r1_hidden :::"="::: ) (Set ($#k1_rcomp_1 :::"[."::: ) (Set "(" ($#k1_real_1 :::"-"::: ) (Set "(" ($#k7_square_1 :::"sqrt"::: ) (Num 2) ")" ) ")" ) "," (Set "(" ($#k1_real_1 :::"-"::: ) (Num 1) ")" ) ($#k1_rcomp_1 :::".]"::: ) )) ; theorem :: SINCOS10:44 (Bool (Set ($#k2_relset_1 :::"rng"::: ) (Set "(" (Set ($#k2_fdiff_9 :::"cosec"::: ) ) ($#k2_partfun1 :::"|"::: ) (Set ($#k1_rcomp_1 :::"[."::: ) (Set "(" (Set ($#k32_sin_cos :::"PI"::: ) ) ($#k10_real_1 :::"/"::: ) (Num 4) ")" ) "," (Set "(" (Set ($#k32_sin_cos :::"PI"::: ) ) ($#k10_real_1 :::"/"::: ) (Num 2) ")" ) ($#k1_rcomp_1 :::".]"::: ) ) ")" )) ($#r1_hidden :::"="::: ) (Set ($#k1_rcomp_1 :::"[."::: ) (Num 1) "," (Set "(" ($#k7_square_1 :::"sqrt"::: ) (Num 2) ")" ) ($#k1_rcomp_1 :::".]"::: ) )) ; theorem :: SINCOS10:45 (Bool (Set ($#k1_rcomp_1 :::"[."::: ) (Num 1) "," (Set "(" ($#k7_square_1 :::"sqrt"::: ) (Num 2) ")" ) ($#k1_rcomp_1 :::".]"::: ) ) ($#r1_tarski :::"c="::: ) (Set ($#k1_relset_1 :::"dom"::: ) (Set ($#k1_sincos10 :::"arcsec1"::: ) ))) ; theorem :: SINCOS10:46 (Bool (Set ($#k1_rcomp_1 :::"[."::: ) (Set "(" ($#k1_real_1 :::"-"::: ) (Set "(" ($#k7_square_1 :::"sqrt"::: ) (Num 2) ")" ) ")" ) "," (Set "(" ($#k1_real_1 :::"-"::: ) (Num 1) ")" ) ($#k1_rcomp_1 :::".]"::: ) ) ($#r1_tarski :::"c="::: ) (Set ($#k1_relset_1 :::"dom"::: ) (Set ($#k2_sincos10 :::"arcsec2"::: ) ))) ; theorem :: SINCOS10:47 (Bool (Set ($#k1_rcomp_1 :::"[."::: ) (Set "(" ($#k1_real_1 :::"-"::: ) (Set "(" ($#k7_square_1 :::"sqrt"::: ) (Num 2) ")" ) ")" ) "," (Set "(" ($#k1_real_1 :::"-"::: ) (Num 1) ")" ) ($#k1_rcomp_1 :::".]"::: ) ) ($#r1_tarski :::"c="::: ) (Set ($#k1_relset_1 :::"dom"::: ) (Set ($#k3_sincos10 :::"arccosec1"::: ) ))) ; theorem :: SINCOS10:48 (Bool (Set ($#k1_rcomp_1 :::"[."::: ) (Num 1) "," (Set "(" ($#k7_square_1 :::"sqrt"::: ) (Num 2) ")" ) ($#k1_rcomp_1 :::".]"::: ) ) ($#r1_tarski :::"c="::: ) (Set ($#k1_relset_1 :::"dom"::: ) (Set ($#k4_sincos10 :::"arccosec2"::: ) ))) ; registration cluster (Set bbbadK5_RELAT_1((Set ($#k1_fdiff_9 :::"sec"::: ) ) "," (Set ($#k1_rcomp_1 :::"[."::: ) (Set ($#k6_numbers :::"0"::: ) ) "," (Set "(" (Set ($#k32_sin_cos :::"PI"::: ) ) ($#k10_real_1 :::"/"::: ) (Num 4) ")" ) ($#k1_rcomp_1 :::".]"::: ) ))) -> ($#v2_funct_1 :::"one-to-one"::: ) ; cluster (Set bbbadK5_RELAT_1((Set ($#k1_fdiff_9 :::"sec"::: ) ) "," (Set ($#k1_rcomp_1 :::"[."::: ) (Set "(" (Set "(" (Num 3) ($#k10_real_1 :::"/"::: ) (Num 4) ")" ) ($#k8_real_1 :::"*"::: ) (Set ($#k32_sin_cos :::"PI"::: ) ) ")" ) "," (Set ($#k32_sin_cos :::"PI"::: ) ) ($#k1_rcomp_1 :::".]"::: ) ))) -> ($#v2_funct_1 :::"one-to-one"::: ) ; cluster (Set bbbadK5_RELAT_1((Set ($#k2_fdiff_9 :::"cosec"::: ) ) "," (Set ($#k1_rcomp_1 :::"[."::: ) (Set "(" ($#k1_real_1 :::"-"::: ) (Set "(" (Set ($#k32_sin_cos :::"PI"::: ) ) ($#k10_real_1 :::"/"::: ) (Num 2) ")" ) ")" ) "," (Set "(" ($#k1_real_1 :::"-"::: ) (Set "(" (Set ($#k32_sin_cos :::"PI"::: ) ) ($#k10_real_1 :::"/"::: ) (Num 4) ")" ) ")" ) ($#k1_rcomp_1 :::".]"::: ) ))) -> ($#v2_funct_1 :::"one-to-one"::: ) ; cluster (Set bbbadK5_RELAT_1((Set ($#k2_fdiff_9 :::"cosec"::: ) ) "," (Set ($#k1_rcomp_1 :::"[."::: ) (Set "(" (Set ($#k32_sin_cos :::"PI"::: ) ) ($#k10_real_1 :::"/"::: ) (Num 4) ")" ) "," (Set "(" (Set ($#k32_sin_cos :::"PI"::: ) ) ($#k10_real_1 :::"/"::: ) (Num 2) ")" ) ($#k1_rcomp_1 :::".]"::: ) ))) -> ($#v2_funct_1 :::"one-to-one"::: ) ; end; theorem :: SINCOS10:49 (Bool (Set (Set ($#k1_sincos10 :::"arcsec1"::: ) ) ($#k2_partfun1 :::"|"::: ) (Set ($#k1_rcomp_1 :::"[."::: ) (Num 1) "," (Set "(" ($#k7_square_1 :::"sqrt"::: ) (Num 2) ")" ) ($#k1_rcomp_1 :::".]"::: ) )) ($#r1_hidden :::"="::: ) (Set (Set "(" (Set ($#k1_fdiff_9 :::"sec"::: ) ) ($#k2_partfun1 :::"|"::: ) (Set ($#k1_rcomp_1 :::"[."::: ) (Set ($#k6_numbers :::"0"::: ) ) "," (Set "(" (Set ($#k32_sin_cos :::"PI"::: ) ) ($#k10_real_1 :::"/"::: ) (Num 4) ")" ) ($#k1_rcomp_1 :::".]"::: ) ) ")" ) ($#k2_partfun2 :::"""::: ) )) ; theorem :: SINCOS10:50 (Bool (Set (Set ($#k2_sincos10 :::"arcsec2"::: ) ) ($#k2_partfun1 :::"|"::: ) (Set ($#k1_rcomp_1 :::"[."::: ) (Set "(" ($#k1_real_1 :::"-"::: ) (Set "(" ($#k7_square_1 :::"sqrt"::: ) (Num 2) ")" ) ")" ) "," (Set "(" ($#k1_real_1 :::"-"::: ) (Num 1) ")" ) ($#k1_rcomp_1 :::".]"::: ) )) ($#r1_hidden :::"="::: ) (Set (Set "(" (Set ($#k1_fdiff_9 :::"sec"::: ) ) ($#k2_partfun1 :::"|"::: ) (Set ($#k1_rcomp_1 :::"[."::: ) (Set "(" (Set "(" (Num 3) ($#k10_real_1 :::"/"::: ) (Num 4) ")" ) ($#k8_real_1 :::"*"::: ) (Set ($#k32_sin_cos :::"PI"::: ) ) ")" ) "," (Set ($#k32_sin_cos :::"PI"::: ) ) ($#k1_rcomp_1 :::".]"::: ) ) ")" ) ($#k2_partfun2 :::"""::: ) )) ; theorem :: SINCOS10:51 (Bool (Set (Set ($#k3_sincos10 :::"arccosec1"::: ) ) ($#k2_partfun1 :::"|"::: ) (Set ($#k1_rcomp_1 :::"[."::: ) (Set "(" ($#k1_real_1 :::"-"::: ) (Set "(" ($#k7_square_1 :::"sqrt"::: ) (Num 2) ")" ) ")" ) "," (Set "(" ($#k1_real_1 :::"-"::: ) (Num 1) ")" ) ($#k1_rcomp_1 :::".]"::: ) )) ($#r1_hidden :::"="::: ) (Set (Set "(" (Set ($#k2_fdiff_9 :::"cosec"::: ) ) ($#k2_partfun1 :::"|"::: ) (Set ($#k1_rcomp_1 :::"[."::: ) (Set "(" ($#k1_real_1 :::"-"::: ) (Set "(" (Set ($#k32_sin_cos :::"PI"::: ) ) ($#k10_real_1 :::"/"::: ) (Num 2) ")" ) ")" ) "," (Set "(" ($#k1_real_1 :::"-"::: ) (Set "(" (Set ($#k32_sin_cos :::"PI"::: ) ) ($#k10_real_1 :::"/"::: ) (Num 4) ")" ) ")" ) ($#k1_rcomp_1 :::".]"::: ) ) ")" ) ($#k2_partfun2 :::"""::: ) )) ; theorem :: SINCOS10:52 (Bool (Set (Set ($#k4_sincos10 :::"arccosec2"::: ) ) ($#k2_partfun1 :::"|"::: ) (Set ($#k1_rcomp_1 :::"[."::: ) (Num 1) "," (Set "(" ($#k7_square_1 :::"sqrt"::: ) (Num 2) ")" ) ($#k1_rcomp_1 :::".]"::: ) )) ($#r1_hidden :::"="::: ) (Set (Set "(" (Set ($#k2_fdiff_9 :::"cosec"::: ) ) ($#k2_partfun1 :::"|"::: ) (Set ($#k1_rcomp_1 :::"[."::: ) (Set "(" (Set ($#k32_sin_cos :::"PI"::: ) ) ($#k10_real_1 :::"/"::: ) (Num 4) ")" ) "," (Set "(" (Set ($#k32_sin_cos :::"PI"::: ) ) ($#k10_real_1 :::"/"::: ) (Num 2) ")" ) ($#k1_rcomp_1 :::".]"::: ) ) ")" ) ($#k2_partfun2 :::"""::: ) )) ; theorem :: SINCOS10:53 (Bool (Set (Set "(" (Set ($#k1_fdiff_9 :::"sec"::: ) ) ($#k2_partfun1 :::"|"::: ) (Set ($#k1_rcomp_1 :::"[."::: ) (Set ($#k6_numbers :::"0"::: ) ) "," (Set "(" (Set ($#k32_sin_cos :::"PI"::: ) ) ($#k10_real_1 :::"/"::: ) (Num 4) ")" ) ($#k1_rcomp_1 :::".]"::: ) ) ")" ) ($#k3_relat_1 :::"*"::: ) (Set "(" (Set ($#k1_sincos10 :::"arcsec1"::: ) ) ($#k2_partfun1 :::"|"::: ) (Set ($#k1_rcomp_1 :::"[."::: ) (Num 1) "," (Set "(" ($#k7_square_1 :::"sqrt"::: ) (Num 2) ")" ) ($#k1_rcomp_1 :::".]"::: ) ) ")" )) ($#r1_hidden :::"="::: ) (Set ($#k1_partfun2 :::"id"::: ) (Set ($#k1_rcomp_1 :::"[."::: ) (Num 1) "," (Set "(" ($#k7_square_1 :::"sqrt"::: ) (Num 2) ")" ) ($#k1_rcomp_1 :::".]"::: ) ))) ; theorem :: SINCOS10:54 (Bool (Set (Set "(" (Set ($#k1_fdiff_9 :::"sec"::: ) ) ($#k2_partfun1 :::"|"::: ) (Set ($#k1_rcomp_1 :::"[."::: ) (Set "(" (Set "(" (Num 3) ($#k10_real_1 :::"/"::: ) (Num 4) ")" ) ($#k8_real_1 :::"*"::: ) (Set ($#k32_sin_cos :::"PI"::: ) ) ")" ) "," (Set ($#k32_sin_cos :::"PI"::: ) ) ($#k1_rcomp_1 :::".]"::: ) ) ")" ) ($#k3_relat_1 :::"*"::: ) (Set "(" (Set ($#k2_sincos10 :::"arcsec2"::: ) ) ($#k2_partfun1 :::"|"::: ) (Set ($#k1_rcomp_1 :::"[."::: ) (Set "(" ($#k1_real_1 :::"-"::: ) (Set "(" ($#k7_square_1 :::"sqrt"::: ) (Num 2) ")" ) ")" ) "," (Set "(" ($#k1_real_1 :::"-"::: ) (Num 1) ")" ) ($#k1_rcomp_1 :::".]"::: ) ) ")" )) ($#r1_hidden :::"="::: ) (Set ($#k1_partfun2 :::"id"::: ) (Set ($#k1_rcomp_1 :::"[."::: ) (Set "(" ($#k1_real_1 :::"-"::: ) (Set "(" ($#k7_square_1 :::"sqrt"::: ) (Num 2) ")" ) ")" ) "," (Set "(" ($#k1_real_1 :::"-"::: ) (Num 1) ")" ) ($#k1_rcomp_1 :::".]"::: ) ))) ; theorem :: SINCOS10:55 (Bool (Set (Set "(" (Set ($#k2_fdiff_9 :::"cosec"::: ) ) ($#k2_partfun1 :::"|"::: ) (Set ($#k1_rcomp_1 :::"[."::: ) (Set "(" ($#k1_real_1 :::"-"::: ) (Set "(" (Set ($#k32_sin_cos :::"PI"::: ) ) ($#k10_real_1 :::"/"::: ) (Num 2) ")" ) ")" ) "," (Set "(" ($#k1_real_1 :::"-"::: ) (Set "(" (Set ($#k32_sin_cos :::"PI"::: ) ) ($#k10_real_1 :::"/"::: ) (Num 4) ")" ) ")" ) ($#k1_rcomp_1 :::".]"::: ) ) ")" ) ($#k3_relat_1 :::"*"::: ) (Set "(" (Set ($#k3_sincos10 :::"arccosec1"::: ) ) ($#k2_partfun1 :::"|"::: ) (Set ($#k1_rcomp_1 :::"[."::: ) (Set "(" ($#k1_real_1 :::"-"::: ) (Set "(" ($#k7_square_1 :::"sqrt"::: ) (Num 2) ")" ) ")" ) "," (Set "(" ($#k1_real_1 :::"-"::: ) (Num 1) ")" ) ($#k1_rcomp_1 :::".]"::: ) ) ")" )) ($#r1_hidden :::"="::: ) (Set ($#k1_partfun2 :::"id"::: ) (Set ($#k1_rcomp_1 :::"[."::: ) (Set "(" ($#k1_real_1 :::"-"::: ) (Set "(" ($#k7_square_1 :::"sqrt"::: ) (Num 2) ")" ) ")" ) "," (Set "(" ($#k1_real_1 :::"-"::: ) (Num 1) ")" ) ($#k1_rcomp_1 :::".]"::: ) ))) ; theorem :: SINCOS10:56 (Bool (Set (Set "(" (Set ($#k2_fdiff_9 :::"cosec"::: ) ) ($#k2_partfun1 :::"|"::: ) (Set ($#k1_rcomp_1 :::"[."::: ) (Set "(" (Set ($#k32_sin_cos :::"PI"::: ) ) ($#k10_real_1 :::"/"::: ) (Num 4) ")" ) "," (Set "(" (Set ($#k32_sin_cos :::"PI"::: ) ) ($#k10_real_1 :::"/"::: ) (Num 2) ")" ) ($#k1_rcomp_1 :::".]"::: ) ) ")" ) ($#k3_relat_1 :::"*"::: ) (Set "(" (Set ($#k4_sincos10 :::"arccosec2"::: ) ) ($#k2_partfun1 :::"|"::: ) (Set ($#k1_rcomp_1 :::"[."::: ) (Num 1) "," (Set "(" ($#k7_square_1 :::"sqrt"::: ) (Num 2) ")" ) ($#k1_rcomp_1 :::".]"::: ) ) ")" )) ($#r1_hidden :::"="::: ) (Set ($#k1_partfun2 :::"id"::: ) (Set ($#k1_rcomp_1 :::"[."::: ) (Num 1) "," (Set "(" ($#k7_square_1 :::"sqrt"::: ) (Num 2) ")" ) ($#k1_rcomp_1 :::".]"::: ) ))) ; theorem :: SINCOS10:57 (Bool (Set (Set "(" (Set ($#k1_fdiff_9 :::"sec"::: ) ) ($#k2_partfun1 :::"|"::: ) (Set ($#k1_rcomp_1 :::"[."::: ) (Set ($#k6_numbers :::"0"::: ) ) "," (Set "(" (Set ($#k32_sin_cos :::"PI"::: ) ) ($#k10_real_1 :::"/"::: ) (Num 4) ")" ) ($#k1_rcomp_1 :::".]"::: ) ) ")" ) ($#k1_partfun1 :::"*"::: ) (Set "(" (Set ($#k1_sincos10 :::"arcsec1"::: ) ) ($#k2_partfun1 :::"|"::: ) (Set ($#k1_rcomp_1 :::"[."::: ) (Num 1) "," (Set "(" ($#k7_square_1 :::"sqrt"::: ) (Num 2) ")" ) ($#k1_rcomp_1 :::".]"::: ) ) ")" )) ($#r1_hidden :::"="::: ) (Set ($#k1_partfun2 :::"id"::: ) (Set ($#k1_rcomp_1 :::"[."::: ) (Num 1) "," (Set "(" ($#k7_square_1 :::"sqrt"::: ) (Num 2) ")" ) ($#k1_rcomp_1 :::".]"::: ) ))) ; theorem :: SINCOS10:58 (Bool (Set (Set "(" (Set ($#k1_fdiff_9 :::"sec"::: ) ) ($#k2_partfun1 :::"|"::: ) (Set ($#k1_rcomp_1 :::"[."::: ) (Set "(" (Set "(" (Num 3) ($#k10_real_1 :::"/"::: ) (Num 4) ")" ) ($#k8_real_1 :::"*"::: ) (Set ($#k32_sin_cos :::"PI"::: ) ) ")" ) "," (Set ($#k32_sin_cos :::"PI"::: ) ) ($#k1_rcomp_1 :::".]"::: ) ) ")" ) ($#k1_partfun1 :::"*"::: ) (Set "(" (Set ($#k2_sincos10 :::"arcsec2"::: ) ) ($#k2_partfun1 :::"|"::: ) (Set ($#k1_rcomp_1 :::"[."::: ) (Set "(" ($#k1_real_1 :::"-"::: ) (Set "(" ($#k7_square_1 :::"sqrt"::: ) (Num 2) ")" ) ")" ) "," (Set "(" ($#k1_real_1 :::"-"::: ) (Num 1) ")" ) ($#k1_rcomp_1 :::".]"::: ) ) ")" )) ($#r1_hidden :::"="::: ) (Set ($#k1_partfun2 :::"id"::: ) (Set ($#k1_rcomp_1 :::"[."::: ) (Set "(" ($#k1_real_1 :::"-"::: ) (Set "(" ($#k7_square_1 :::"sqrt"::: ) (Num 2) ")" ) ")" ) "," (Set "(" ($#k1_real_1 :::"-"::: ) (Num 1) ")" ) ($#k1_rcomp_1 :::".]"::: ) ))) ; theorem :: SINCOS10:59 (Bool (Set (Set "(" (Set ($#k2_fdiff_9 :::"cosec"::: ) ) ($#k2_partfun1 :::"|"::: ) (Set ($#k1_rcomp_1 :::"[."::: ) (Set "(" ($#k1_real_1 :::"-"::: ) (Set "(" (Set ($#k32_sin_cos :::"PI"::: ) ) ($#k10_real_1 :::"/"::: ) (Num 2) ")" ) ")" ) "," (Set "(" ($#k1_real_1 :::"-"::: ) (Set "(" (Set ($#k32_sin_cos :::"PI"::: ) ) ($#k10_real_1 :::"/"::: ) (Num 4) ")" ) ")" ) ($#k1_rcomp_1 :::".]"::: ) ) ")" ) ($#k1_partfun1 :::"*"::: ) (Set "(" (Set ($#k3_sincos10 :::"arccosec1"::: ) ) ($#k2_partfun1 :::"|"::: ) (Set ($#k1_rcomp_1 :::"[."::: ) (Set "(" ($#k1_real_1 :::"-"::: ) (Set "(" ($#k7_square_1 :::"sqrt"::: ) (Num 2) ")" ) ")" ) "," (Set "(" ($#k1_real_1 :::"-"::: ) (Num 1) ")" ) ($#k1_rcomp_1 :::".]"::: ) ) ")" )) ($#r1_hidden :::"="::: ) (Set ($#k1_partfun2 :::"id"::: ) (Set ($#k1_rcomp_1 :::"[."::: ) (Set "(" ($#k1_real_1 :::"-"::: ) (Set "(" ($#k7_square_1 :::"sqrt"::: ) (Num 2) ")" ) ")" ) "," (Set "(" ($#k1_real_1 :::"-"::: ) (Num 1) ")" ) ($#k1_rcomp_1 :::".]"::: ) ))) ; theorem :: SINCOS10:60 (Bool (Set (Set "(" (Set ($#k2_fdiff_9 :::"cosec"::: ) ) ($#k2_partfun1 :::"|"::: ) (Set ($#k1_rcomp_1 :::"[."::: ) (Set "(" (Set ($#k32_sin_cos :::"PI"::: ) ) ($#k10_real_1 :::"/"::: ) (Num 4) ")" ) "," (Set "(" (Set ($#k32_sin_cos :::"PI"::: ) ) ($#k10_real_1 :::"/"::: ) (Num 2) ")" ) ($#k1_rcomp_1 :::".]"::: ) ) ")" ) ($#k1_partfun1 :::"*"::: ) (Set "(" (Set ($#k4_sincos10 :::"arccosec2"::: ) ) ($#k2_partfun1 :::"|"::: ) (Set ($#k1_rcomp_1 :::"[."::: ) (Num 1) "," (Set "(" ($#k7_square_1 :::"sqrt"::: ) (Num 2) ")" ) ($#k1_rcomp_1 :::".]"::: ) ) ")" )) ($#r1_hidden :::"="::: ) (Set ($#k1_partfun2 :::"id"::: ) (Set ($#k1_rcomp_1 :::"[."::: ) (Num 1) "," (Set "(" ($#k7_square_1 :::"sqrt"::: ) (Num 2) ")" ) ($#k1_rcomp_1 :::".]"::: ) ))) ; theorem :: SINCOS10:61 (Bool (Set (Set ($#k1_sincos10 :::"arcsec1"::: ) ) ($#k3_relat_1 :::"*"::: ) (Set "(" (Set ($#k1_fdiff_9 :::"sec"::: ) ) ($#k2_partfun1 :::"|"::: ) (Set ($#k3_rcomp_1 :::"[."::: ) (Set ($#k6_numbers :::"0"::: ) ) "," (Set "(" (Set ($#k32_sin_cos :::"PI"::: ) ) ($#k10_real_1 :::"/"::: ) (Num 2) ")" ) ($#k3_rcomp_1 :::".["::: ) ) ")" )) ($#r1_hidden :::"="::: ) (Set ($#k1_partfun2 :::"id"::: ) (Set ($#k3_rcomp_1 :::"[."::: ) (Set ($#k6_numbers :::"0"::: ) ) "," (Set "(" (Set ($#k32_sin_cos :::"PI"::: ) ) ($#k10_real_1 :::"/"::: ) (Num 2) ")" ) ($#k3_rcomp_1 :::".["::: ) ))) ; theorem :: SINCOS10:62 (Bool (Set (Set ($#k2_sincos10 :::"arcsec2"::: ) ) ($#k3_relat_1 :::"*"::: ) (Set "(" (Set ($#k1_fdiff_9 :::"sec"::: ) ) ($#k2_partfun1 :::"|"::: ) (Set ($#k4_rcomp_1 :::"]."::: ) (Set "(" (Set ($#k32_sin_cos :::"PI"::: ) ) ($#k10_real_1 :::"/"::: ) (Num 2) ")" ) "," (Set ($#k32_sin_cos :::"PI"::: ) ) ($#k4_rcomp_1 :::".]"::: ) ) ")" )) ($#r1_hidden :::"="::: ) (Set ($#k1_partfun2 :::"id"::: ) (Set ($#k4_rcomp_1 :::"]."::: ) (Set "(" (Set ($#k32_sin_cos :::"PI"::: ) ) ($#k10_real_1 :::"/"::: ) (Num 2) ")" ) "," (Set ($#k32_sin_cos :::"PI"::: ) ) ($#k4_rcomp_1 :::".]"::: ) ))) ; theorem :: SINCOS10:63 (Bool (Set (Set ($#k3_sincos10 :::"arccosec1"::: ) ) ($#k3_relat_1 :::"*"::: ) (Set "(" (Set ($#k2_fdiff_9 :::"cosec"::: ) ) ($#k2_partfun1 :::"|"::: ) (Set ($#k3_rcomp_1 :::"[."::: ) (Set "(" ($#k1_real_1 :::"-"::: ) (Set "(" (Set ($#k32_sin_cos :::"PI"::: ) ) ($#k10_real_1 :::"/"::: ) (Num 2) ")" ) ")" ) "," (Set ($#k6_numbers :::"0"::: ) ) ($#k3_rcomp_1 :::".["::: ) ) ")" )) ($#r1_hidden :::"="::: ) (Set ($#k1_partfun2 :::"id"::: ) (Set ($#k3_rcomp_1 :::"[."::: ) (Set "(" ($#k1_real_1 :::"-"::: ) (Set "(" (Set ($#k32_sin_cos :::"PI"::: ) ) ($#k10_real_1 :::"/"::: ) (Num 2) ")" ) ")" ) "," (Set ($#k6_numbers :::"0"::: ) ) ($#k3_rcomp_1 :::".["::: ) ))) ; theorem :: SINCOS10:64 (Bool (Set (Set ($#k4_sincos10 :::"arccosec2"::: ) ) ($#k3_relat_1 :::"*"::: ) (Set "(" (Set ($#k2_fdiff_9 :::"cosec"::: ) ) ($#k2_partfun1 :::"|"::: ) (Set ($#k4_rcomp_1 :::"]."::: ) (Set ($#k6_numbers :::"0"::: ) ) "," (Set "(" (Set ($#k32_sin_cos :::"PI"::: ) ) ($#k10_real_1 :::"/"::: ) (Num 2) ")" ) ($#k4_rcomp_1 :::".]"::: ) ) ")" )) ($#r1_hidden :::"="::: ) (Set ($#k1_partfun2 :::"id"::: ) (Set ($#k4_rcomp_1 :::"]."::: ) (Set ($#k6_numbers :::"0"::: ) ) "," (Set "(" (Set ($#k32_sin_cos :::"PI"::: ) ) ($#k10_real_1 :::"/"::: ) (Num 2) ")" ) ($#k4_rcomp_1 :::".]"::: ) ))) ; theorem :: SINCOS10:65 (Bool (Set (Set ($#k1_sincos10 :::"arcsec1"::: ) ) ($#k1_partfun1 :::"*"::: ) (Set "(" (Set ($#k1_fdiff_9 :::"sec"::: ) ) ($#k2_partfun1 :::"|"::: ) (Set ($#k3_rcomp_1 :::"[."::: ) (Set ($#k6_numbers :::"0"::: ) ) "," (Set "(" (Set ($#k32_sin_cos :::"PI"::: ) ) ($#k10_real_1 :::"/"::: ) (Num 2) ")" ) ($#k3_rcomp_1 :::".["::: ) ) ")" )) ($#r1_hidden :::"="::: ) (Set ($#k1_partfun2 :::"id"::: ) (Set ($#k3_rcomp_1 :::"[."::: ) (Set ($#k6_numbers :::"0"::: ) ) "," (Set "(" (Set ($#k32_sin_cos :::"PI"::: ) ) ($#k10_real_1 :::"/"::: ) (Num 2) ")" ) ($#k3_rcomp_1 :::".["::: ) ))) ; theorem :: SINCOS10:66 (Bool (Set (Set ($#k2_sincos10 :::"arcsec2"::: ) ) ($#k1_partfun1 :::"*"::: ) (Set "(" (Set ($#k1_fdiff_9 :::"sec"::: ) ) ($#k2_partfun1 :::"|"::: ) (Set ($#k4_rcomp_1 :::"]."::: ) (Set "(" (Set ($#k32_sin_cos :::"PI"::: ) ) ($#k10_real_1 :::"/"::: ) (Num 2) ")" ) "," (Set ($#k32_sin_cos :::"PI"::: ) ) ($#k4_rcomp_1 :::".]"::: ) ) ")" )) ($#r1_hidden :::"="::: ) (Set ($#k1_partfun2 :::"id"::: ) (Set ($#k4_rcomp_1 :::"]."::: ) (Set "(" (Set ($#k32_sin_cos :::"PI"::: ) ) ($#k10_real_1 :::"/"::: ) (Num 2) ")" ) "," (Set ($#k32_sin_cos :::"PI"::: ) ) ($#k4_rcomp_1 :::".]"::: ) ))) ; theorem :: SINCOS10:67 (Bool (Set (Set ($#k3_sincos10 :::"arccosec1"::: ) ) ($#k1_partfun1 :::"*"::: ) (Set "(" (Set ($#k2_fdiff_9 :::"cosec"::: ) ) ($#k2_partfun1 :::"|"::: ) (Set ($#k3_rcomp_1 :::"[."::: ) (Set "(" ($#k1_real_1 :::"-"::: ) (Set "(" (Set ($#k32_sin_cos :::"PI"::: ) ) ($#k10_real_1 :::"/"::: ) (Num 2) ")" ) ")" ) "," (Set ($#k6_numbers :::"0"::: ) ) ($#k3_rcomp_1 :::".["::: ) ) ")" )) ($#r1_hidden :::"="::: ) (Set ($#k1_partfun2 :::"id"::: ) (Set ($#k3_rcomp_1 :::"[."::: ) (Set "(" ($#k1_real_1 :::"-"::: ) (Set "(" (Set ($#k32_sin_cos :::"PI"::: ) ) ($#k10_real_1 :::"/"::: ) (Num 2) ")" ) ")" ) "," (Set ($#k6_numbers :::"0"::: ) ) ($#k3_rcomp_1 :::".["::: ) ))) ; theorem :: SINCOS10:68 (Bool (Set (Set ($#k4_sincos10 :::"arccosec2"::: ) ) ($#k1_partfun1 :::"*"::: ) (Set "(" (Set ($#k2_fdiff_9 :::"cosec"::: ) ) ($#k2_partfun1 :::"|"::: ) (Set ($#k4_rcomp_1 :::"]."::: ) (Set ($#k6_numbers :::"0"::: ) ) "," (Set "(" (Set ($#k32_sin_cos :::"PI"::: ) ) ($#k10_real_1 :::"/"::: ) (Num 2) ")" ) ($#k4_rcomp_1 :::".]"::: ) ) ")" )) ($#r1_hidden :::"="::: ) (Set ($#k1_partfun2 :::"id"::: ) (Set ($#k4_rcomp_1 :::"]."::: ) (Set ($#k6_numbers :::"0"::: ) ) "," (Set "(" (Set ($#k32_sin_cos :::"PI"::: ) ) ($#k10_real_1 :::"/"::: ) (Num 2) ")" ) ($#k4_rcomp_1 :::".]"::: ) ))) ; theorem :: SINCOS10:69 (Bool "for" (Set (Var "r")) "being" ($#m1_subset_1 :::"Real":::) "st" (Bool (Bool (Set ($#k6_numbers :::"0"::: ) ) ($#r1_xxreal_0 :::"<="::: ) (Set (Var "r"))) & (Bool (Set (Var "r")) ($#r1_xxreal_0 :::"<"::: ) (Set (Set ($#k32_sin_cos :::"PI"::: ) ) ($#k10_real_1 :::"/"::: ) (Num 2)))) "holds" (Bool (Set ($#k9_sincos10 :::"arcsec1"::: ) (Set "(" (Set ($#k1_fdiff_9 :::"sec"::: ) ) ($#k1_seq_1 :::"."::: ) (Set (Var "r")) ")" )) ($#r1_hidden :::"="::: ) (Set (Var "r")))) ; theorem :: SINCOS10:70 (Bool "for" (Set (Var "r")) "being" ($#m1_subset_1 :::"Real":::) "st" (Bool (Bool (Set (Set ($#k32_sin_cos :::"PI"::: ) ) ($#k10_real_1 :::"/"::: ) (Num 2)) ($#r1_xxreal_0 :::"<"::: ) (Set (Var "r"))) & (Bool (Set (Var "r")) ($#r1_xxreal_0 :::"<="::: ) (Set ($#k32_sin_cos :::"PI"::: ) ))) "holds" (Bool (Set ($#k10_sincos10 :::"arcsec2"::: ) (Set "(" (Set ($#k1_fdiff_9 :::"sec"::: ) ) ($#k1_seq_1 :::"."::: ) (Set (Var "r")) ")" )) ($#r1_hidden :::"="::: ) (Set (Var "r")))) ; theorem :: SINCOS10:71 (Bool "for" (Set (Var "r")) "being" ($#m1_subset_1 :::"Real":::) "st" (Bool (Bool (Set ($#k1_real_1 :::"-"::: ) (Set "(" (Set ($#k32_sin_cos :::"PI"::: ) ) ($#k10_real_1 :::"/"::: ) (Num 2) ")" )) ($#r1_xxreal_0 :::"<="::: ) (Set (Var "r"))) & (Bool (Set (Var "r")) ($#r1_xxreal_0 :::"<"::: ) (Set ($#k6_numbers :::"0"::: ) ))) "holds" (Bool (Set ($#k11_sincos10 :::"arccosec1"::: ) (Set "(" (Set ($#k2_fdiff_9 :::"cosec"::: ) ) ($#k1_seq_1 :::"."::: ) (Set (Var "r")) ")" )) ($#r1_hidden :::"="::: ) (Set (Var "r")))) ; theorem :: SINCOS10:72 (Bool "for" (Set (Var "r")) "being" ($#m1_subset_1 :::"Real":::) "st" (Bool (Bool (Set ($#k6_numbers :::"0"::: ) ) ($#r1_xxreal_0 :::"<"::: ) (Set (Var "r"))) & (Bool (Set (Var "r")) ($#r1_xxreal_0 :::"<="::: ) (Set (Set ($#k32_sin_cos :::"PI"::: ) ) ($#k10_real_1 :::"/"::: ) (Num 2)))) "holds" (Bool (Set ($#k12_sincos10 :::"arccosec2"::: ) (Set "(" (Set ($#k2_fdiff_9 :::"cosec"::: ) ) ($#k1_seq_1 :::"."::: ) (Set (Var "r")) ")" )) ($#r1_hidden :::"="::: ) (Set (Var "r")))) ; theorem :: SINCOS10:73 (Bool "(" (Bool (Set (Set ($#k1_sincos10 :::"arcsec1"::: ) ) ($#k1_seq_1 :::"."::: ) (Num 1)) ($#r1_hidden :::"="::: ) (Set ($#k6_numbers :::"0"::: ) )) & (Bool (Set (Set ($#k1_sincos10 :::"arcsec1"::: ) ) ($#k1_seq_1 :::"."::: ) (Set "(" ($#k7_square_1 :::"sqrt"::: ) (Num 2) ")" )) ($#r1_hidden :::"="::: ) (Set (Set ($#k32_sin_cos :::"PI"::: ) ) ($#k10_real_1 :::"/"::: ) (Num 4))) ")" ) ; theorem :: SINCOS10:74 (Bool "(" (Bool (Set (Set ($#k2_sincos10 :::"arcsec2"::: ) ) ($#k1_seq_1 :::"."::: ) (Set "(" ($#k1_real_1 :::"-"::: ) (Set "(" ($#k7_square_1 :::"sqrt"::: ) (Num 2) ")" ) ")" )) ($#r1_hidden :::"="::: ) (Set (Set "(" (Num 3) ($#k10_real_1 :::"/"::: ) (Num 4) ")" ) ($#k8_real_1 :::"*"::: ) (Set ($#k32_sin_cos :::"PI"::: ) ))) & (Bool (Set (Set ($#k2_sincos10 :::"arcsec2"::: ) ) ($#k1_seq_1 :::"."::: ) (Set "(" ($#k1_real_1 :::"-"::: ) (Num 1) ")" )) ($#r1_hidden :::"="::: ) (Set ($#k32_sin_cos :::"PI"::: ) )) ")" ) ; theorem :: SINCOS10:75 (Bool "(" (Bool (Set (Set ($#k3_sincos10 :::"arccosec1"::: ) ) ($#k1_seq_1 :::"."::: ) (Set "(" ($#k1_real_1 :::"-"::: ) (Num 1) ")" )) ($#r1_hidden :::"="::: ) (Set ($#k1_real_1 :::"-"::: ) (Set "(" (Set ($#k32_sin_cos :::"PI"::: ) ) ($#k10_real_1 :::"/"::: ) (Num 2) ")" ))) & (Bool (Set (Set ($#k3_sincos10 :::"arccosec1"::: ) ) ($#k1_seq_1 :::"."::: ) (Set "(" ($#k1_real_1 :::"-"::: ) (Set "(" ($#k7_square_1 :::"sqrt"::: ) (Num 2) ")" ) ")" )) ($#r1_hidden :::"="::: ) (Set ($#k1_real_1 :::"-"::: ) (Set "(" (Set ($#k32_sin_cos :::"PI"::: ) ) ($#k10_real_1 :::"/"::: ) (Num 4) ")" ))) ")" ) ; theorem :: SINCOS10:76 (Bool "(" (Bool (Set (Set ($#k4_sincos10 :::"arccosec2"::: ) ) ($#k1_seq_1 :::"."::: ) (Set "(" ($#k7_square_1 :::"sqrt"::: ) (Num 2) ")" )) ($#r1_hidden :::"="::: ) (Set (Set ($#k32_sin_cos :::"PI"::: ) ) ($#k10_real_1 :::"/"::: ) (Num 4))) & (Bool (Set (Set ($#k4_sincos10 :::"arccosec2"::: ) ) ($#k1_seq_1 :::"."::: ) (Num 1)) ($#r1_hidden :::"="::: ) (Set (Set ($#k32_sin_cos :::"PI"::: ) ) ($#k10_real_1 :::"/"::: ) (Num 2))) ")" ) ; theorem :: SINCOS10:77 (Bool (Set (Set ($#k1_sincos10 :::"arcsec1"::: ) ) ($#k2_partfun1 :::"|"::: ) (Set "(" (Set ($#k1_fdiff_9 :::"sec"::: ) ) ($#k7_relset_1 :::".:"::: ) (Set ($#k3_rcomp_1 :::"[."::: ) (Set ($#k6_numbers :::"0"::: ) ) "," (Set "(" (Set ($#k32_sin_cos :::"PI"::: ) ) ($#k10_real_1 :::"/"::: ) (Num 2) ")" ) ($#k3_rcomp_1 :::".["::: ) ) ")" )) "is" ($#v5_valued_0 :::"increasing"::: ) ) ; theorem :: SINCOS10:78 (Bool (Set (Set ($#k2_sincos10 :::"arcsec2"::: ) ) ($#k2_partfun1 :::"|"::: ) (Set "(" (Set ($#k1_fdiff_9 :::"sec"::: ) ) ($#k7_relset_1 :::".:"::: ) (Set ($#k4_rcomp_1 :::"]."::: ) (Set "(" (Set ($#k32_sin_cos :::"PI"::: ) ) ($#k10_real_1 :::"/"::: ) (Num 2) ")" ) "," (Set ($#k32_sin_cos :::"PI"::: ) ) ($#k4_rcomp_1 :::".]"::: ) ) ")" )) "is" ($#v5_valued_0 :::"increasing"::: ) ) ; theorem :: SINCOS10:79 (Bool (Set (Set ($#k3_sincos10 :::"arccosec1"::: ) ) ($#k2_partfun1 :::"|"::: ) (Set "(" (Set ($#k2_fdiff_9 :::"cosec"::: ) ) ($#k7_relset_1 :::".:"::: ) (Set ($#k3_rcomp_1 :::"[."::: ) (Set "(" ($#k1_real_1 :::"-"::: ) (Set "(" (Set ($#k32_sin_cos :::"PI"::: ) ) ($#k10_real_1 :::"/"::: ) (Num 2) ")" ) ")" ) "," (Set ($#k6_numbers :::"0"::: ) ) ($#k3_rcomp_1 :::".["::: ) ) ")" )) "is" ($#v6_valued_0 :::"decreasing"::: ) ) ; theorem :: SINCOS10:80 (Bool (Set (Set ($#k4_sincos10 :::"arccosec2"::: ) ) ($#k2_partfun1 :::"|"::: ) (Set "(" (Set ($#k2_fdiff_9 :::"cosec"::: ) ) ($#k7_relset_1 :::".:"::: ) (Set ($#k4_rcomp_1 :::"]."::: ) (Set ($#k6_numbers :::"0"::: ) ) "," (Set "(" (Set ($#k32_sin_cos :::"PI"::: ) ) ($#k10_real_1 :::"/"::: ) (Num 2) ")" ) ($#k4_rcomp_1 :::".]"::: ) ) ")" )) "is" ($#v6_valued_0 :::"decreasing"::: ) ) ; theorem :: SINCOS10:81 (Bool (Set (Set ($#k1_sincos10 :::"arcsec1"::: ) ) ($#k2_partfun1 :::"|"::: ) (Set ($#k1_rcomp_1 :::"[."::: ) (Num 1) "," (Set "(" ($#k7_square_1 :::"sqrt"::: ) (Num 2) ")" ) ($#k1_rcomp_1 :::".]"::: ) )) "is" ($#v5_valued_0 :::"increasing"::: ) ) ; theorem :: SINCOS10:82 (Bool (Set (Set ($#k2_sincos10 :::"arcsec2"::: ) ) ($#k2_partfun1 :::"|"::: ) (Set ($#k1_rcomp_1 :::"[."::: ) (Set "(" ($#k1_real_1 :::"-"::: ) (Set "(" ($#k7_square_1 :::"sqrt"::: ) (Num 2) ")" ) ")" ) "," (Set "(" ($#k1_real_1 :::"-"::: ) (Num 1) ")" ) ($#k1_rcomp_1 :::".]"::: ) )) "is" ($#v5_valued_0 :::"increasing"::: ) ) ; theorem :: SINCOS10:83 (Bool (Set (Set ($#k3_sincos10 :::"arccosec1"::: ) ) ($#k2_partfun1 :::"|"::: ) (Set ($#k1_rcomp_1 :::"[."::: ) (Set "(" ($#k1_real_1 :::"-"::: ) (Set "(" ($#k7_square_1 :::"sqrt"::: ) (Num 2) ")" ) ")" ) "," (Set "(" ($#k1_real_1 :::"-"::: ) (Num 1) ")" ) ($#k1_rcomp_1 :::".]"::: ) )) "is" ($#v6_valued_0 :::"decreasing"::: ) ) ; theorem :: SINCOS10:84 (Bool (Set (Set ($#k4_sincos10 :::"arccosec2"::: ) ) ($#k2_partfun1 :::"|"::: ) (Set ($#k1_rcomp_1 :::"[."::: ) (Num 1) "," (Set "(" ($#k7_square_1 :::"sqrt"::: ) (Num 2) ")" ) ($#k1_rcomp_1 :::".]"::: ) )) "is" ($#v6_valued_0 :::"decreasing"::: ) ) ; theorem :: SINCOS10:85 (Bool "for" (Set (Var "x")) "being" ($#m1_hidden :::"set"::: ) "st" (Bool (Bool (Set (Var "x")) ($#r2_hidden :::"in"::: ) (Set ($#k1_rcomp_1 :::"[."::: ) (Num 1) "," (Set "(" ($#k7_square_1 :::"sqrt"::: ) (Num 2) ")" ) ($#k1_rcomp_1 :::".]"::: ) ))) "holds" (Bool (Set (Set ($#k1_sincos10 :::"arcsec1"::: ) ) ($#k1_seq_1 :::"."::: ) (Set (Var "x"))) ($#r2_hidden :::"in"::: ) (Set ($#k1_rcomp_1 :::"[."::: ) (Set ($#k6_numbers :::"0"::: ) ) "," (Set "(" (Set ($#k32_sin_cos :::"PI"::: ) ) ($#k10_real_1 :::"/"::: ) (Num 4) ")" ) ($#k1_rcomp_1 :::".]"::: ) ))) ; theorem :: SINCOS10:86 (Bool "for" (Set (Var "x")) "being" ($#m1_hidden :::"set"::: ) "st" (Bool (Bool (Set (Var "x")) ($#r2_hidden :::"in"::: ) (Set ($#k1_rcomp_1 :::"[."::: ) (Set "(" ($#k1_real_1 :::"-"::: ) (Set "(" ($#k7_square_1 :::"sqrt"::: ) (Num 2) ")" ) ")" ) "," (Set "(" ($#k1_real_1 :::"-"::: ) (Num 1) ")" ) ($#k1_rcomp_1 :::".]"::: ) ))) "holds" (Bool (Set (Set ($#k2_sincos10 :::"arcsec2"::: ) ) ($#k1_seq_1 :::"."::: ) (Set (Var "x"))) ($#r2_hidden :::"in"::: ) (Set ($#k1_rcomp_1 :::"[."::: ) (Set "(" (Set "(" (Num 3) ($#k10_real_1 :::"/"::: ) (Num 4) ")" ) ($#k8_real_1 :::"*"::: ) (Set ($#k32_sin_cos :::"PI"::: ) ) ")" ) "," (Set ($#k32_sin_cos :::"PI"::: ) ) ($#k1_rcomp_1 :::".]"::: ) ))) ; theorem :: SINCOS10:87 (Bool "for" (Set (Var "x")) "being" ($#m1_hidden :::"set"::: ) "st" (Bool (Bool (Set (Var "x")) ($#r2_hidden :::"in"::: ) (Set ($#k1_rcomp_1 :::"[."::: ) (Set "(" ($#k1_real_1 :::"-"::: ) (Set "(" ($#k7_square_1 :::"sqrt"::: ) (Num 2) ")" ) ")" ) "," (Set "(" ($#k1_real_1 :::"-"::: ) (Num 1) ")" ) ($#k1_rcomp_1 :::".]"::: ) ))) "holds" (Bool (Set (Set ($#k3_sincos10 :::"arccosec1"::: ) ) ($#k1_seq_1 :::"."::: ) (Set (Var "x"))) ($#r2_hidden :::"in"::: ) (Set ($#k1_rcomp_1 :::"[."::: ) (Set "(" ($#k1_real_1 :::"-"::: ) (Set "(" (Set ($#k32_sin_cos :::"PI"::: ) ) ($#k10_real_1 :::"/"::: ) (Num 2) ")" ) ")" ) "," (Set "(" ($#k1_real_1 :::"-"::: ) (Set "(" (Set ($#k32_sin_cos :::"PI"::: ) ) ($#k10_real_1 :::"/"::: ) (Num 4) ")" ) ")" ) ($#k1_rcomp_1 :::".]"::: ) ))) ; theorem :: SINCOS10:88 (Bool "for" (Set (Var "x")) "being" ($#m1_hidden :::"set"::: ) "st" (Bool (Bool (Set (Var "x")) ($#r2_hidden :::"in"::: ) (Set ($#k1_rcomp_1 :::"[."::: ) (Num 1) "," (Set "(" ($#k7_square_1 :::"sqrt"::: ) (Num 2) ")" ) ($#k1_rcomp_1 :::".]"::: ) ))) "holds" (Bool (Set (Set ($#k4_sincos10 :::"arccosec2"::: ) ) ($#k1_seq_1 :::"."::: ) (Set (Var "x"))) ($#r2_hidden :::"in"::: ) (Set ($#k1_rcomp_1 :::"[."::: ) (Set "(" (Set ($#k32_sin_cos :::"PI"::: ) ) ($#k10_real_1 :::"/"::: ) (Num 4) ")" ) "," (Set "(" (Set ($#k32_sin_cos :::"PI"::: ) ) ($#k10_real_1 :::"/"::: ) (Num 2) ")" ) ($#k1_rcomp_1 :::".]"::: ) ))) ; theorem :: SINCOS10:89 (Bool "for" (Set (Var "r")) "being" ($#m1_subset_1 :::"Real":::) "st" (Bool (Bool (Num 1) ($#r1_xxreal_0 :::"<="::: ) (Set (Var "r"))) & (Bool (Set (Var "r")) ($#r1_xxreal_0 :::"<="::: ) (Set ($#k7_square_1 :::"sqrt"::: ) (Num 2)))) "holds" (Bool (Set (Set ($#k1_fdiff_9 :::"sec"::: ) ) ($#k1_seq_1 :::"."::: ) (Set "(" ($#k9_sincos10 :::"arcsec1"::: ) (Set (Var "r")) ")" )) ($#r1_hidden :::"="::: ) (Set (Var "r")))) ; theorem :: SINCOS10:90 (Bool "for" (Set (Var "r")) "being" ($#m1_subset_1 :::"Real":::) "st" (Bool (Bool (Set ($#k1_real_1 :::"-"::: ) (Set "(" ($#k7_square_1 :::"sqrt"::: ) (Num 2) ")" )) ($#r1_xxreal_0 :::"<="::: ) (Set (Var "r"))) & (Bool (Set (Var "r")) ($#r1_xxreal_0 :::"<="::: ) (Set ($#k1_real_1 :::"-"::: ) (Num 1)))) "holds" (Bool (Set (Set ($#k1_fdiff_9 :::"sec"::: ) ) ($#k1_seq_1 :::"."::: ) (Set "(" ($#k10_sincos10 :::"arcsec2"::: ) (Set (Var "r")) ")" )) ($#r1_hidden :::"="::: ) (Set (Var "r")))) ; theorem :: SINCOS10:91 (Bool "for" (Set (Var "r")) "being" ($#m1_subset_1 :::"Real":::) "st" (Bool (Bool (Set ($#k1_real_1 :::"-"::: ) (Set "(" ($#k7_square_1 :::"sqrt"::: ) (Num 2) ")" )) ($#r1_xxreal_0 :::"<="::: ) (Set (Var "r"))) & (Bool (Set (Var "r")) ($#r1_xxreal_0 :::"<="::: ) (Set ($#k1_real_1 :::"-"::: ) (Num 1)))) "holds" (Bool (Set (Set ($#k2_fdiff_9 :::"cosec"::: ) ) ($#k1_seq_1 :::"."::: ) (Set "(" ($#k11_sincos10 :::"arccosec1"::: ) (Set (Var "r")) ")" )) ($#r1_hidden :::"="::: ) (Set (Var "r")))) ; theorem :: SINCOS10:92 (Bool "for" (Set (Var "r")) "being" ($#m1_subset_1 :::"Real":::) "st" (Bool (Bool (Num 1) ($#r1_xxreal_0 :::"<="::: ) (Set (Var "r"))) & (Bool (Set (Var "r")) ($#r1_xxreal_0 :::"<="::: ) (Set ($#k7_square_1 :::"sqrt"::: ) (Num 2)))) "holds" (Bool (Set (Set ($#k2_fdiff_9 :::"cosec"::: ) ) ($#k1_seq_1 :::"."::: ) (Set "(" ($#k12_sincos10 :::"arccosec2"::: ) (Set (Var "r")) ")" )) ($#r1_hidden :::"="::: ) (Set (Var "r")))) ; theorem :: SINCOS10:93 (Bool (Set (Set ($#k1_sincos10 :::"arcsec1"::: ) ) ($#k2_partfun1 :::"|"::: ) (Set ($#k1_rcomp_1 :::"[."::: ) (Num 1) "," (Set "(" ($#k7_square_1 :::"sqrt"::: ) (Num 2) ")" ) ($#k1_rcomp_1 :::".]"::: ) )) "is" ($#v1_fcont_1 :::"continuous"::: ) ) ; theorem :: SINCOS10:94 (Bool (Set (Set ($#k2_sincos10 :::"arcsec2"::: ) ) ($#k2_partfun1 :::"|"::: ) (Set ($#k1_rcomp_1 :::"[."::: ) (Set "(" ($#k1_real_1 :::"-"::: ) (Set "(" ($#k7_square_1 :::"sqrt"::: ) (Num 2) ")" ) ")" ) "," (Set "(" ($#k1_real_1 :::"-"::: ) (Num 1) ")" ) ($#k1_rcomp_1 :::".]"::: ) )) "is" ($#v1_fcont_1 :::"continuous"::: ) ) ; theorem :: SINCOS10:95 (Bool (Set (Set ($#k3_sincos10 :::"arccosec1"::: ) ) ($#k2_partfun1 :::"|"::: ) (Set ($#k1_rcomp_1 :::"[."::: ) (Set "(" ($#k1_real_1 :::"-"::: ) (Set "(" ($#k7_square_1 :::"sqrt"::: ) (Num 2) ")" ) ")" ) "," (Set "(" ($#k1_real_1 :::"-"::: ) (Num 1) ")" ) ($#k1_rcomp_1 :::".]"::: ) )) "is" ($#v1_fcont_1 :::"continuous"::: ) ) ; theorem :: SINCOS10:96 (Bool (Set (Set ($#k4_sincos10 :::"arccosec2"::: ) ) ($#k2_partfun1 :::"|"::: ) (Set ($#k1_rcomp_1 :::"[."::: ) (Num 1) "," (Set "(" ($#k7_square_1 :::"sqrt"::: ) (Num 2) ")" ) ($#k1_rcomp_1 :::".]"::: ) )) "is" ($#v1_fcont_1 :::"continuous"::: ) ) ; theorem :: SINCOS10:97 (Bool (Set ($#k2_relset_1 :::"rng"::: ) (Set "(" (Set ($#k1_sincos10 :::"arcsec1"::: ) ) ($#k2_partfun1 :::"|"::: ) (Set ($#k1_rcomp_1 :::"[."::: ) (Num 1) "," (Set "(" ($#k7_square_1 :::"sqrt"::: ) (Num 2) ")" ) ($#k1_rcomp_1 :::".]"::: ) ) ")" )) ($#r1_hidden :::"="::: ) (Set ($#k1_rcomp_1 :::"[."::: ) (Set ($#k6_numbers :::"0"::: ) ) "," (Set "(" (Set ($#k32_sin_cos :::"PI"::: ) ) ($#k10_real_1 :::"/"::: ) (Num 4) ")" ) ($#k1_rcomp_1 :::".]"::: ) )) ; theorem :: SINCOS10:98 (Bool (Set ($#k2_relset_1 :::"rng"::: ) (Set "(" (Set ($#k2_sincos10 :::"arcsec2"::: ) ) ($#k2_partfun1 :::"|"::: ) (Set ($#k1_rcomp_1 :::"[."::: ) (Set "(" ($#k1_real_1 :::"-"::: ) (Set "(" ($#k7_square_1 :::"sqrt"::: ) (Num 2) ")" ) ")" ) "," (Set "(" ($#k1_real_1 :::"-"::: ) (Num 1) ")" ) ($#k1_rcomp_1 :::".]"::: ) ) ")" )) ($#r1_hidden :::"="::: ) (Set ($#k1_rcomp_1 :::"[."::: ) (Set "(" (Set "(" (Num 3) ($#k10_real_1 :::"/"::: ) (Num 4) ")" ) ($#k8_real_1 :::"*"::: ) (Set ($#k32_sin_cos :::"PI"::: ) ) ")" ) "," (Set ($#k32_sin_cos :::"PI"::: ) ) ($#k1_rcomp_1 :::".]"::: ) )) ; theorem :: SINCOS10:99 (Bool (Set ($#k2_relset_1 :::"rng"::: ) (Set "(" (Set ($#k3_sincos10 :::"arccosec1"::: ) ) ($#k2_partfun1 :::"|"::: ) (Set ($#k1_rcomp_1 :::"[."::: ) (Set "(" ($#k1_real_1 :::"-"::: ) (Set "(" ($#k7_square_1 :::"sqrt"::: ) (Num 2) ")" ) ")" ) "," (Set "(" ($#k1_real_1 :::"-"::: ) (Num 1) ")" ) ($#k1_rcomp_1 :::".]"::: ) ) ")" )) ($#r1_hidden :::"="::: ) (Set ($#k1_rcomp_1 :::"[."::: ) (Set "(" ($#k1_real_1 :::"-"::: ) (Set "(" (Set ($#k32_sin_cos :::"PI"::: ) ) ($#k10_real_1 :::"/"::: ) (Num 2) ")" ) ")" ) "," (Set "(" ($#k1_real_1 :::"-"::: ) (Set "(" (Set ($#k32_sin_cos :::"PI"::: ) ) ($#k10_real_1 :::"/"::: ) (Num 4) ")" ) ")" ) ($#k1_rcomp_1 :::".]"::: ) )) ; theorem :: SINCOS10:100 (Bool (Set ($#k2_relset_1 :::"rng"::: ) (Set "(" (Set ($#k4_sincos10 :::"arccosec2"::: ) ) ($#k2_partfun1 :::"|"::: ) (Set ($#k1_rcomp_1 :::"[."::: ) (Num 1) "," (Set "(" ($#k7_square_1 :::"sqrt"::: ) (Num 2) ")" ) ($#k1_rcomp_1 :::".]"::: ) ) ")" )) ($#r1_hidden :::"="::: ) (Set ($#k1_rcomp_1 :::"[."::: ) (Set "(" (Set ($#k32_sin_cos :::"PI"::: ) ) ($#k10_real_1 :::"/"::: ) (Num 4) ")" ) "," (Set "(" (Set ($#k32_sin_cos :::"PI"::: ) ) ($#k10_real_1 :::"/"::: ) (Num 2) ")" ) ($#k1_rcomp_1 :::".]"::: ) )) ; theorem :: SINCOS10:101 (Bool "for" (Set (Var "r")) "being" ($#m1_subset_1 :::"Real":::) "holds" (Bool "(" "(" (Bool (Bool (Num 1) ($#r1_xxreal_0 :::"<="::: ) (Set (Var "r"))) & (Bool (Set (Var "r")) ($#r1_xxreal_0 :::"<="::: ) (Set ($#k7_square_1 :::"sqrt"::: ) (Num 2))) & (Bool (Set ($#k9_sincos10 :::"arcsec1"::: ) (Set (Var "r"))) ($#r1_hidden :::"="::: ) (Set ($#k6_numbers :::"0"::: ) ))) "implies" (Bool (Set (Var "r")) ($#r1_hidden :::"="::: ) (Num 1)) ")" & "(" (Bool (Bool (Num 1) ($#r1_xxreal_0 :::"<="::: ) (Set (Var "r"))) & (Bool (Set (Var "r")) ($#r1_xxreal_0 :::"<="::: ) (Set ($#k7_square_1 :::"sqrt"::: ) (Num 2))) & (Bool (Set ($#k9_sincos10 :::"arcsec1"::: ) (Set (Var "r"))) ($#r1_hidden :::"="::: ) (Set (Set ($#k32_sin_cos :::"PI"::: ) ) ($#k10_real_1 :::"/"::: ) (Num 4)))) "implies" (Bool (Set (Var "r")) ($#r1_hidden :::"="::: ) (Set ($#k7_square_1 :::"sqrt"::: ) (Num 2))) ")" ")" )) ; theorem :: SINCOS10:102 (Bool "for" (Set (Var "r")) "being" ($#m1_subset_1 :::"Real":::) "holds" (Bool "(" "(" (Bool (Bool (Set ($#k1_real_1 :::"-"::: ) (Set "(" ($#k7_square_1 :::"sqrt"::: ) (Num 2) ")" )) ($#r1_xxreal_0 :::"<="::: ) (Set (Var "r"))) & (Bool (Set (Var "r")) ($#r1_xxreal_0 :::"<="::: ) (Set ($#k1_real_1 :::"-"::: ) (Num 1))) & (Bool (Set ($#k10_sincos10 :::"arcsec2"::: ) (Set (Var "r"))) ($#r1_hidden :::"="::: ) (Set (Set "(" (Num 3) ($#k10_real_1 :::"/"::: ) (Num 4) ")" ) ($#k8_real_1 :::"*"::: ) (Set ($#k32_sin_cos :::"PI"::: ) )))) "implies" (Bool (Set (Var "r")) ($#r1_hidden :::"="::: ) (Set ($#k1_real_1 :::"-"::: ) (Set "(" ($#k7_square_1 :::"sqrt"::: ) (Num 2) ")" ))) ")" & "(" (Bool (Bool (Set ($#k1_real_1 :::"-"::: ) (Set "(" ($#k7_square_1 :::"sqrt"::: ) (Num 2) ")" )) ($#r1_xxreal_0 :::"<="::: ) (Set (Var "r"))) & (Bool (Set (Var "r")) ($#r1_xxreal_0 :::"<="::: ) (Set ($#k1_real_1 :::"-"::: ) (Num 1))) & (Bool (Set ($#k10_sincos10 :::"arcsec2"::: ) (Set (Var "r"))) ($#r1_hidden :::"="::: ) (Set ($#k32_sin_cos :::"PI"::: ) ))) "implies" (Bool (Set (Var "r")) ($#r1_hidden :::"="::: ) (Set ($#k1_real_1 :::"-"::: ) (Num 1))) ")" ")" )) ; theorem :: SINCOS10:103 (Bool "for" (Set (Var "r")) "being" ($#m1_subset_1 :::"Real":::) "holds" (Bool "(" "(" (Bool (Bool (Set ($#k1_real_1 :::"-"::: ) (Set "(" ($#k7_square_1 :::"sqrt"::: ) (Num 2) ")" )) ($#r1_xxreal_0 :::"<="::: ) (Set (Var "r"))) & (Bool (Set (Var "r")) ($#r1_xxreal_0 :::"<="::: ) (Set ($#k1_real_1 :::"-"::: ) (Num 1))) & (Bool (Set ($#k11_sincos10 :::"arccosec1"::: ) (Set (Var "r"))) ($#r1_hidden :::"="::: ) (Set ($#k1_real_1 :::"-"::: ) (Set "(" (Set ($#k32_sin_cos :::"PI"::: ) ) ($#k10_real_1 :::"/"::: ) (Num 2) ")" )))) "implies" (Bool (Set (Var "r")) ($#r1_hidden :::"="::: ) (Set ($#k1_real_1 :::"-"::: ) (Num 1))) ")" & "(" (Bool (Bool (Set ($#k1_real_1 :::"-"::: ) (Set "(" ($#k7_square_1 :::"sqrt"::: ) (Num 2) ")" )) ($#r1_xxreal_0 :::"<="::: ) (Set (Var "r"))) & (Bool (Set (Var "r")) ($#r1_xxreal_0 :::"<="::: ) (Set ($#k1_real_1 :::"-"::: ) (Num 1))) & (Bool (Set ($#k11_sincos10 :::"arccosec1"::: ) (Set (Var "r"))) ($#r1_hidden :::"="::: ) (Set ($#k1_real_1 :::"-"::: ) (Set "(" (Set ($#k32_sin_cos :::"PI"::: ) ) ($#k10_real_1 :::"/"::: ) (Num 4) ")" )))) "implies" (Bool (Set (Var "r")) ($#r1_hidden :::"="::: ) (Set ($#k1_real_1 :::"-"::: ) (Set "(" ($#k7_square_1 :::"sqrt"::: ) (Num 2) ")" ))) ")" ")" )) ; theorem :: SINCOS10:104 (Bool "for" (Set (Var "r")) "being" ($#m1_subset_1 :::"Real":::) "holds" (Bool "(" "(" (Bool (Bool (Num 1) ($#r1_xxreal_0 :::"<="::: ) (Set (Var "r"))) & (Bool (Set (Var "r")) ($#r1_xxreal_0 :::"<="::: ) (Set ($#k7_square_1 :::"sqrt"::: ) (Num 2))) & (Bool (Set ($#k12_sincos10 :::"arccosec2"::: ) (Set (Var "r"))) ($#r1_hidden :::"="::: ) (Set (Set ($#k32_sin_cos :::"PI"::: ) ) ($#k10_real_1 :::"/"::: ) (Num 4)))) "implies" (Bool (Set (Var "r")) ($#r1_hidden :::"="::: ) (Set ($#k7_square_1 :::"sqrt"::: ) (Num 2))) ")" & "(" (Bool (Bool (Num 1) ($#r1_xxreal_0 :::"<="::: ) (Set (Var "r"))) & (Bool (Set (Var "r")) ($#r1_xxreal_0 :::"<="::: ) (Set ($#k7_square_1 :::"sqrt"::: ) (Num 2))) & (Bool (Set ($#k12_sincos10 :::"arccosec2"::: ) (Set (Var "r"))) ($#r1_hidden :::"="::: ) (Set (Set ($#k32_sin_cos :::"PI"::: ) ) ($#k10_real_1 :::"/"::: ) (Num 2)))) "implies" (Bool (Set (Var "r")) ($#r1_hidden :::"="::: ) (Num 1)) ")" ")" )) ; theorem :: SINCOS10:105 (Bool "for" (Set (Var "r")) "being" ($#m1_subset_1 :::"Real":::) "st" (Bool (Bool (Num 1) ($#r1_xxreal_0 :::"<="::: ) (Set (Var "r"))) & (Bool (Set (Var "r")) ($#r1_xxreal_0 :::"<="::: ) (Set ($#k7_square_1 :::"sqrt"::: ) (Num 2)))) "holds" (Bool "(" (Bool (Set ($#k6_numbers :::"0"::: ) ) ($#r1_xxreal_0 :::"<="::: ) (Set ($#k9_sincos10 :::"arcsec1"::: ) (Set (Var "r")))) & (Bool (Set ($#k9_sincos10 :::"arcsec1"::: ) (Set (Var "r"))) ($#r1_xxreal_0 :::"<="::: ) (Set (Set ($#k32_sin_cos :::"PI"::: ) ) ($#k10_real_1 :::"/"::: ) (Num 4))) ")" )) ; theorem :: SINCOS10:106 (Bool "for" (Set (Var "r")) "being" ($#m1_subset_1 :::"Real":::) "st" (Bool (Bool (Set ($#k1_real_1 :::"-"::: ) (Set "(" ($#k7_square_1 :::"sqrt"::: ) (Num 2) ")" )) ($#r1_xxreal_0 :::"<="::: ) (Set (Var "r"))) & (Bool (Set (Var "r")) ($#r1_xxreal_0 :::"<="::: ) (Set ($#k1_real_1 :::"-"::: ) (Num 1)))) "holds" (Bool "(" (Bool (Set (Set "(" (Num 3) ($#k10_real_1 :::"/"::: ) (Num 4) ")" ) ($#k8_real_1 :::"*"::: ) (Set ($#k32_sin_cos :::"PI"::: ) )) ($#r1_xxreal_0 :::"<="::: ) (Set ($#k10_sincos10 :::"arcsec2"::: ) (Set (Var "r")))) & (Bool (Set ($#k10_sincos10 :::"arcsec2"::: ) (Set (Var "r"))) ($#r1_xxreal_0 :::"<="::: ) (Set ($#k32_sin_cos :::"PI"::: ) )) ")" )) ; theorem :: SINCOS10:107 (Bool "for" (Set (Var "r")) "being" ($#m1_subset_1 :::"Real":::) "st" (Bool (Bool (Set ($#k1_real_1 :::"-"::: ) (Set "(" ($#k7_square_1 :::"sqrt"::: ) (Num 2) ")" )) ($#r1_xxreal_0 :::"<="::: ) (Set (Var "r"))) & (Bool (Set (Var "r")) ($#r1_xxreal_0 :::"<="::: ) (Set ($#k1_real_1 :::"-"::: ) (Num 1)))) "holds" (Bool "(" (Bool (Set ($#k1_real_1 :::"-"::: ) (Set "(" (Set ($#k32_sin_cos :::"PI"::: ) ) ($#k10_real_1 :::"/"::: ) (Num 2) ")" )) ($#r1_xxreal_0 :::"<="::: ) (Set ($#k11_sincos10 :::"arccosec1"::: ) (Set (Var "r")))) & (Bool (Set ($#k11_sincos10 :::"arccosec1"::: ) (Set (Var "r"))) ($#r1_xxreal_0 :::"<="::: ) (Set ($#k1_real_1 :::"-"::: ) (Set "(" (Set ($#k32_sin_cos :::"PI"::: ) ) ($#k10_real_1 :::"/"::: ) (Num 4) ")" ))) ")" )) ; theorem :: SINCOS10:108 (Bool "for" (Set (Var "r")) "being" ($#m1_subset_1 :::"Real":::) "st" (Bool (Bool (Num 1) ($#r1_xxreal_0 :::"<="::: ) (Set (Var "r"))) & (Bool (Set (Var "r")) ($#r1_xxreal_0 :::"<="::: ) (Set ($#k7_square_1 :::"sqrt"::: ) (Num 2)))) "holds" (Bool "(" (Bool (Set (Set ($#k32_sin_cos :::"PI"::: ) ) ($#k10_real_1 :::"/"::: ) (Num 4)) ($#r1_xxreal_0 :::"<="::: ) (Set ($#k12_sincos10 :::"arccosec2"::: ) (Set (Var "r")))) & (Bool (Set ($#k12_sincos10 :::"arccosec2"::: ) (Set (Var "r"))) ($#r1_xxreal_0 :::"<="::: ) (Set (Set ($#k32_sin_cos :::"PI"::: ) ) ($#k10_real_1 :::"/"::: ) (Num 2))) ")" )) ; theorem :: SINCOS10:109 (Bool "for" (Set (Var "r")) "being" ($#m1_subset_1 :::"Real":::) "st" (Bool (Bool (Num 1) ($#r1_xxreal_0 :::"<"::: ) (Set (Var "r"))) & (Bool (Set (Var "r")) ($#r1_xxreal_0 :::"<"::: ) (Set ($#k7_square_1 :::"sqrt"::: ) (Num 2)))) "holds" (Bool "(" (Bool (Set ($#k6_numbers :::"0"::: ) ) ($#r1_xxreal_0 :::"<"::: ) (Set ($#k9_sincos10 :::"arcsec1"::: ) (Set (Var "r")))) & (Bool (Set ($#k9_sincos10 :::"arcsec1"::: ) (Set (Var "r"))) ($#r1_xxreal_0 :::"<"::: ) (Set (Set ($#k32_sin_cos :::"PI"::: ) ) ($#k10_real_1 :::"/"::: ) (Num 4))) ")" )) ; theorem :: SINCOS10:110 (Bool "for" (Set (Var "r")) "being" ($#m1_subset_1 :::"Real":::) "st" (Bool (Bool (Set ($#k1_real_1 :::"-"::: ) (Set "(" ($#k7_square_1 :::"sqrt"::: ) (Num 2) ")" )) ($#r1_xxreal_0 :::"<"::: ) (Set (Var "r"))) & (Bool (Set (Var "r")) ($#r1_xxreal_0 :::"<"::: ) (Set ($#k1_real_1 :::"-"::: ) (Num 1)))) "holds" (Bool "(" (Bool (Set (Set "(" (Num 3) ($#k10_real_1 :::"/"::: ) (Num 4) ")" ) ($#k8_real_1 :::"*"::: ) (Set ($#k32_sin_cos :::"PI"::: ) )) ($#r1_xxreal_0 :::"<"::: ) (Set ($#k10_sincos10 :::"arcsec2"::: ) (Set (Var "r")))) & (Bool (Set ($#k10_sincos10 :::"arcsec2"::: ) (Set (Var "r"))) ($#r1_xxreal_0 :::"<"::: ) (Set ($#k32_sin_cos :::"PI"::: ) )) ")" )) ; theorem :: SINCOS10:111 (Bool "for" (Set (Var "r")) "being" ($#m1_subset_1 :::"Real":::) "st" (Bool (Bool (Set ($#k1_real_1 :::"-"::: ) (Set "(" ($#k7_square_1 :::"sqrt"::: ) (Num 2) ")" )) ($#r1_xxreal_0 :::"<"::: ) (Set (Var "r"))) & (Bool (Set (Var "r")) ($#r1_xxreal_0 :::"<"::: ) (Set ($#k1_real_1 :::"-"::: ) (Num 1)))) "holds" (Bool "(" (Bool (Set ($#k1_real_1 :::"-"::: ) (Set "(" (Set ($#k32_sin_cos :::"PI"::: ) ) ($#k10_real_1 :::"/"::: ) (Num 2) ")" )) ($#r1_xxreal_0 :::"<"::: ) (Set ($#k11_sincos10 :::"arccosec1"::: ) (Set (Var "r")))) & (Bool (Set ($#k11_sincos10 :::"arccosec1"::: ) (Set (Var "r"))) ($#r1_xxreal_0 :::"<"::: ) (Set ($#k1_real_1 :::"-"::: ) (Set "(" (Set ($#k32_sin_cos :::"PI"::: ) ) ($#k10_real_1 :::"/"::: ) (Num 4) ")" ))) ")" )) ; theorem :: SINCOS10:112 (Bool "for" (Set (Var "r")) "being" ($#m1_subset_1 :::"Real":::) "st" (Bool (Bool (Num 1) ($#r1_xxreal_0 :::"<"::: ) (Set (Var "r"))) & (Bool (Set (Var "r")) ($#r1_xxreal_0 :::"<"::: ) (Set ($#k7_square_1 :::"sqrt"::: ) (Num 2)))) "holds" (Bool "(" (Bool (Set (Set ($#k32_sin_cos :::"PI"::: ) ) ($#k10_real_1 :::"/"::: ) (Num 4)) ($#r1_xxreal_0 :::"<"::: ) (Set ($#k12_sincos10 :::"arccosec2"::: ) (Set (Var "r")))) & (Bool (Set ($#k12_sincos10 :::"arccosec2"::: ) (Set (Var "r"))) ($#r1_xxreal_0 :::"<"::: ) (Set (Set ($#k32_sin_cos :::"PI"::: ) ) ($#k10_real_1 :::"/"::: ) (Num 2))) ")" )) ; theorem :: SINCOS10:113 (Bool "for" (Set (Var "r")) "being" ($#m1_subset_1 :::"Real":::) "st" (Bool (Bool (Num 1) ($#r1_xxreal_0 :::"<="::: ) (Set (Var "r"))) & (Bool (Set (Var "r")) ($#r1_xxreal_0 :::"<="::: ) (Set ($#k7_square_1 :::"sqrt"::: ) (Num 2)))) "holds" (Bool "(" (Bool (Set (Set ($#k16_sin_cos :::"sin"::: ) ) ($#k1_seq_1 :::"."::: ) (Set "(" ($#k9_sincos10 :::"arcsec1"::: ) (Set (Var "r")) ")" )) ($#r1_hidden :::"="::: ) (Set (Set "(" ($#k7_square_1 :::"sqrt"::: ) (Set "(" (Set "(" (Set (Var "r")) ($#k5_square_1 :::"^2"::: ) ")" ) ($#k9_real_1 :::"-"::: ) (Num 1) ")" ) ")" ) ($#k10_real_1 :::"/"::: ) (Set (Var "r")))) & (Bool (Set (Set ($#k19_sin_cos :::"cos"::: ) ) ($#k1_seq_1 :::"."::: ) (Set "(" ($#k9_sincos10 :::"arcsec1"::: ) (Set (Var "r")) ")" )) ($#r1_hidden :::"="::: ) (Set (Num 1) ($#k10_real_1 :::"/"::: ) (Set (Var "r")))) ")" )) ; theorem :: SINCOS10:114 (Bool "for" (Set (Var "r")) "being" ($#m1_subset_1 :::"Real":::) "st" (Bool (Bool (Set ($#k1_real_1 :::"-"::: ) (Set "(" ($#k7_square_1 :::"sqrt"::: ) (Num 2) ")" )) ($#r1_xxreal_0 :::"<="::: ) (Set (Var "r"))) & (Bool (Set (Var "r")) ($#r1_xxreal_0 :::"<="::: ) (Set ($#k1_real_1 :::"-"::: ) (Num 1)))) "holds" (Bool "(" (Bool (Set (Set ($#k16_sin_cos :::"sin"::: ) ) ($#k1_seq_1 :::"."::: ) (Set "(" ($#k10_sincos10 :::"arcsec2"::: ) (Set (Var "r")) ")" )) ($#r1_hidden :::"="::: ) (Set ($#k1_real_1 :::"-"::: ) (Set "(" (Set "(" ($#k7_square_1 :::"sqrt"::: ) (Set "(" (Set "(" (Set (Var "r")) ($#k5_square_1 :::"^2"::: ) ")" ) ($#k9_real_1 :::"-"::: ) (Num 1) ")" ) ")" ) ($#k10_real_1 :::"/"::: ) (Set (Var "r")) ")" ))) & (Bool (Set (Set ($#k19_sin_cos :::"cos"::: ) ) ($#k1_seq_1 :::"."::: ) (Set "(" ($#k10_sincos10 :::"arcsec2"::: ) (Set (Var "r")) ")" )) ($#r1_hidden :::"="::: ) (Set (Num 1) ($#k10_real_1 :::"/"::: ) (Set (Var "r")))) ")" )) ; theorem :: SINCOS10:115 (Bool "for" (Set (Var "r")) "being" ($#m1_subset_1 :::"Real":::) "st" (Bool (Bool (Set ($#k1_real_1 :::"-"::: ) (Set "(" ($#k7_square_1 :::"sqrt"::: ) (Num 2) ")" )) ($#r1_xxreal_0 :::"<="::: ) (Set (Var "r"))) & (Bool (Set (Var "r")) ($#r1_xxreal_0 :::"<="::: ) (Set ($#k1_real_1 :::"-"::: ) (Num 1)))) "holds" (Bool "(" (Bool (Set (Set ($#k16_sin_cos :::"sin"::: ) ) ($#k1_seq_1 :::"."::: ) (Set "(" ($#k11_sincos10 :::"arccosec1"::: ) (Set (Var "r")) ")" )) ($#r1_hidden :::"="::: ) (Set (Num 1) ($#k10_real_1 :::"/"::: ) (Set (Var "r")))) & (Bool (Set (Set ($#k19_sin_cos :::"cos"::: ) ) ($#k1_seq_1 :::"."::: ) (Set "(" ($#k11_sincos10 :::"arccosec1"::: ) (Set (Var "r")) ")" )) ($#r1_hidden :::"="::: ) (Set ($#k1_real_1 :::"-"::: ) (Set "(" (Set "(" ($#k7_square_1 :::"sqrt"::: ) (Set "(" (Set "(" (Set (Var "r")) ($#k5_square_1 :::"^2"::: ) ")" ) ($#k9_real_1 :::"-"::: ) (Num 1) ")" ) ")" ) ($#k10_real_1 :::"/"::: ) (Set (Var "r")) ")" ))) ")" )) ; theorem :: SINCOS10:116 (Bool "for" (Set (Var "r")) "being" ($#m1_subset_1 :::"Real":::) "st" (Bool (Bool (Num 1) ($#r1_xxreal_0 :::"<="::: ) (Set (Var "r"))) & (Bool (Set (Var "r")) ($#r1_xxreal_0 :::"<="::: ) (Set ($#k7_square_1 :::"sqrt"::: ) (Num 2)))) "holds" (Bool "(" (Bool (Set (Set ($#k16_sin_cos :::"sin"::: ) ) ($#k1_seq_1 :::"."::: ) (Set "(" ($#k12_sincos10 :::"arccosec2"::: ) (Set (Var "r")) ")" )) ($#r1_hidden :::"="::: ) (Set (Num 1) ($#k10_real_1 :::"/"::: ) (Set (Var "r")))) & (Bool (Set (Set ($#k19_sin_cos :::"cos"::: ) ) ($#k1_seq_1 :::"."::: ) (Set "(" ($#k12_sincos10 :::"arccosec2"::: ) (Set (Var "r")) ")" )) ($#r1_hidden :::"="::: ) (Set (Set "(" ($#k7_square_1 :::"sqrt"::: ) (Set "(" (Set "(" (Set (Var "r")) ($#k5_square_1 :::"^2"::: ) ")" ) ($#k9_real_1 :::"-"::: ) (Num 1) ")" ) ")" ) ($#k10_real_1 :::"/"::: ) (Set (Var "r")))) ")" )) ; theorem :: SINCOS10:117 (Bool "for" (Set (Var "r")) "being" ($#m1_subset_1 :::"Real":::) "st" (Bool (Bool (Num 1) ($#r1_xxreal_0 :::"<"::: ) (Set (Var "r"))) & (Bool (Set (Var "r")) ($#r1_xxreal_0 :::"<"::: ) (Set ($#k7_square_1 :::"sqrt"::: ) (Num 2)))) "holds" (Bool (Set (Set ($#k2_fdiff_9 :::"cosec"::: ) ) ($#k1_seq_1 :::"."::: ) (Set "(" ($#k9_sincos10 :::"arcsec1"::: ) (Set (Var "r")) ")" )) ($#r1_hidden :::"="::: ) (Set (Set (Var "r")) ($#k10_real_1 :::"/"::: ) (Set "(" ($#k7_square_1 :::"sqrt"::: ) (Set "(" (Set "(" (Set (Var "r")) ($#k5_square_1 :::"^2"::: ) ")" ) ($#k9_real_1 :::"-"::: ) (Num 1) ")" ) ")" )))) ; theorem :: SINCOS10:118 (Bool "for" (Set (Var "r")) "being" ($#m1_subset_1 :::"Real":::) "st" (Bool (Bool (Set ($#k1_real_1 :::"-"::: ) (Set "(" ($#k7_square_1 :::"sqrt"::: ) (Num 2) ")" )) ($#r1_xxreal_0 :::"<"::: ) (Set (Var "r"))) & (Bool (Set (Var "r")) ($#r1_xxreal_0 :::"<"::: ) (Set ($#k1_real_1 :::"-"::: ) (Num 1)))) "holds" (Bool (Set (Set ($#k2_fdiff_9 :::"cosec"::: ) ) ($#k1_seq_1 :::"."::: ) (Set "(" ($#k10_sincos10 :::"arcsec2"::: ) (Set (Var "r")) ")" )) ($#r1_hidden :::"="::: ) (Set ($#k1_real_1 :::"-"::: ) (Set "(" (Set (Var "r")) ($#k10_real_1 :::"/"::: ) (Set "(" ($#k7_square_1 :::"sqrt"::: ) (Set "(" (Set "(" (Set (Var "r")) ($#k5_square_1 :::"^2"::: ) ")" ) ($#k9_real_1 :::"-"::: ) (Num 1) ")" ) ")" ) ")" )))) ; theorem :: SINCOS10:119 (Bool "for" (Set (Var "r")) "being" ($#m1_subset_1 :::"Real":::) "st" (Bool (Bool (Set ($#k1_real_1 :::"-"::: ) (Set "(" ($#k7_square_1 :::"sqrt"::: ) (Num 2) ")" )) ($#r1_xxreal_0 :::"<"::: ) (Set (Var "r"))) & (Bool (Set (Var "r")) ($#r1_xxreal_0 :::"<"::: ) (Set ($#k1_real_1 :::"-"::: ) (Num 1)))) "holds" (Bool (Set (Set ($#k1_fdiff_9 :::"sec"::: ) ) ($#k1_seq_1 :::"."::: ) (Set "(" ($#k11_sincos10 :::"arccosec1"::: ) (Set (Var "r")) ")" )) ($#r1_hidden :::"="::: ) (Set ($#k1_real_1 :::"-"::: ) (Set "(" (Set (Var "r")) ($#k10_real_1 :::"/"::: ) (Set "(" ($#k7_square_1 :::"sqrt"::: ) (Set "(" (Set "(" (Set (Var "r")) ($#k5_square_1 :::"^2"::: ) ")" ) ($#k9_real_1 :::"-"::: ) (Num 1) ")" ) ")" ) ")" )))) ; theorem :: SINCOS10:120 (Bool "for" (Set (Var "r")) "being" ($#m1_subset_1 :::"Real":::) "st" (Bool (Bool (Num 1) ($#r1_xxreal_0 :::"<"::: ) (Set (Var "r"))) & (Bool (Set (Var "r")) ($#r1_xxreal_0 :::"<"::: ) (Set ($#k7_square_1 :::"sqrt"::: ) (Num 2)))) "holds" (Bool (Set (Set ($#k1_fdiff_9 :::"sec"::: ) ) ($#k1_seq_1 :::"."::: ) (Set "(" ($#k12_sincos10 :::"arccosec2"::: ) (Set (Var "r")) ")" )) ($#r1_hidden :::"="::: ) (Set (Set (Var "r")) ($#k10_real_1 :::"/"::: ) (Set "(" ($#k7_square_1 :::"sqrt"::: ) (Set "(" (Set "(" (Set (Var "r")) ($#k5_square_1 :::"^2"::: ) ")" ) ($#k9_real_1 :::"-"::: ) (Num 1) ")" ) ")" )))) ; theorem :: SINCOS10:121 (Bool (Set ($#k1_sincos10 :::"arcsec1"::: ) ) ($#r2_fdiff_1 :::"is_differentiable_on"::: ) (Set (Set ($#k1_fdiff_9 :::"sec"::: ) ) ($#k7_relset_1 :::".:"::: ) (Set ($#k2_rcomp_1 :::"]."::: ) (Set ($#k6_numbers :::"0"::: ) ) "," (Set "(" (Set ($#k32_sin_cos :::"PI"::: ) ) ($#k10_real_1 :::"/"::: ) (Num 2) ")" ) ($#k2_rcomp_1 :::".["::: ) ))) ; theorem :: SINCOS10:122 (Bool (Set ($#k2_sincos10 :::"arcsec2"::: ) ) ($#r2_fdiff_1 :::"is_differentiable_on"::: ) (Set (Set ($#k1_fdiff_9 :::"sec"::: ) ) ($#k7_relset_1 :::".:"::: ) (Set ($#k2_rcomp_1 :::"]."::: ) (Set "(" (Set ($#k32_sin_cos :::"PI"::: ) ) ($#k10_real_1 :::"/"::: ) (Num 2) ")" ) "," (Set ($#k32_sin_cos :::"PI"::: ) ) ($#k2_rcomp_1 :::".["::: ) ))) ; theorem :: SINCOS10:123 (Bool (Set ($#k3_sincos10 :::"arccosec1"::: ) ) ($#r2_fdiff_1 :::"is_differentiable_on"::: ) (Set (Set ($#k2_fdiff_9 :::"cosec"::: ) ) ($#k7_relset_1 :::".:"::: ) (Set ($#k2_rcomp_1 :::"]."::: ) (Set "(" ($#k1_real_1 :::"-"::: ) (Set "(" (Set ($#k32_sin_cos :::"PI"::: ) ) ($#k10_real_1 :::"/"::: ) (Num 2) ")" ) ")" ) "," (Set ($#k6_numbers :::"0"::: ) ) ($#k2_rcomp_1 :::".["::: ) ))) ; theorem :: SINCOS10:124 (Bool (Set ($#k4_sincos10 :::"arccosec2"::: ) ) ($#r2_fdiff_1 :::"is_differentiable_on"::: ) (Set (Set ($#k2_fdiff_9 :::"cosec"::: ) ) ($#k7_relset_1 :::".:"::: ) (Set ($#k2_rcomp_1 :::"]."::: ) (Set ($#k6_numbers :::"0"::: ) ) "," (Set "(" (Set ($#k32_sin_cos :::"PI"::: ) ) ($#k10_real_1 :::"/"::: ) (Num 2) ")" ) ($#k2_rcomp_1 :::".["::: ) ))) ; theorem :: SINCOS10:125 (Bool (Set (Set ($#k1_fdiff_9 :::"sec"::: ) ) ($#k7_relset_1 :::".:"::: ) (Set ($#k2_rcomp_1 :::"]."::: ) (Set ($#k6_numbers :::"0"::: ) ) "," (Set "(" (Set ($#k32_sin_cos :::"PI"::: ) ) ($#k10_real_1 :::"/"::: ) (Num 2) ")" ) ($#k2_rcomp_1 :::".["::: ) )) "is" ($#v3_rcomp_1 :::"open"::: ) ) ; theorem :: SINCOS10:126 (Bool (Set (Set ($#k1_fdiff_9 :::"sec"::: ) ) ($#k7_relset_1 :::".:"::: ) (Set ($#k2_rcomp_1 :::"]."::: ) (Set "(" (Set ($#k32_sin_cos :::"PI"::: ) ) ($#k10_real_1 :::"/"::: ) (Num 2) ")" ) "," (Set ($#k32_sin_cos :::"PI"::: ) ) ($#k2_rcomp_1 :::".["::: ) )) "is" ($#v3_rcomp_1 :::"open"::: ) ) ; theorem :: SINCOS10:127 (Bool (Set (Set ($#k2_fdiff_9 :::"cosec"::: ) ) ($#k7_relset_1 :::".:"::: ) (Set ($#k2_rcomp_1 :::"]."::: ) (Set "(" ($#k1_real_1 :::"-"::: ) (Set "(" (Set ($#k32_sin_cos :::"PI"::: ) ) ($#k10_real_1 :::"/"::: ) (Num 2) ")" ) ")" ) "," (Set ($#k6_numbers :::"0"::: ) ) ($#k2_rcomp_1 :::".["::: ) )) "is" ($#v3_rcomp_1 :::"open"::: ) ) ; theorem :: SINCOS10:128 (Bool (Set (Set ($#k2_fdiff_9 :::"cosec"::: ) ) ($#k7_relset_1 :::".:"::: ) (Set ($#k2_rcomp_1 :::"]."::: ) (Set ($#k6_numbers :::"0"::: ) ) "," (Set "(" (Set ($#k32_sin_cos :::"PI"::: ) ) ($#k10_real_1 :::"/"::: ) (Num 2) ")" ) ($#k2_rcomp_1 :::".["::: ) )) "is" ($#v3_rcomp_1 :::"open"::: ) ) ; theorem :: SINCOS10:129 (Bool (Set (Set ($#k1_sincos10 :::"arcsec1"::: ) ) ($#k2_partfun1 :::"|"::: ) (Set "(" (Set ($#k1_fdiff_9 :::"sec"::: ) ) ($#k7_relset_1 :::".:"::: ) (Set ($#k2_rcomp_1 :::"]."::: ) (Set ($#k6_numbers :::"0"::: ) ) "," (Set "(" (Set ($#k32_sin_cos :::"PI"::: ) ) ($#k10_real_1 :::"/"::: ) (Num 2) ")" ) ($#k2_rcomp_1 :::".["::: ) ) ")" )) "is" ($#v1_fcont_1 :::"continuous"::: ) ) ; theorem :: SINCOS10:130 (Bool (Set (Set ($#k2_sincos10 :::"arcsec2"::: ) ) ($#k2_partfun1 :::"|"::: ) (Set "(" (Set ($#k1_fdiff_9 :::"sec"::: ) ) ($#k7_relset_1 :::".:"::: ) (Set ($#k2_rcomp_1 :::"]."::: ) (Set "(" (Set ($#k32_sin_cos :::"PI"::: ) ) ($#k10_real_1 :::"/"::: ) (Num 2) ")" ) "," (Set ($#k32_sin_cos :::"PI"::: ) ) ($#k2_rcomp_1 :::".["::: ) ) ")" )) "is" ($#v1_fcont_1 :::"continuous"::: ) ) ; theorem :: SINCOS10:131 (Bool (Set (Set ($#k3_sincos10 :::"arccosec1"::: ) ) ($#k2_partfun1 :::"|"::: ) (Set "(" (Set ($#k2_fdiff_9 :::"cosec"::: ) ) ($#k7_relset_1 :::".:"::: ) (Set ($#k2_rcomp_1 :::"]."::: ) (Set "(" ($#k1_real_1 :::"-"::: ) (Set "(" (Set ($#k32_sin_cos :::"PI"::: ) ) ($#k10_real_1 :::"/"::: ) (Num 2) ")" ) ")" ) "," (Set ($#k6_numbers :::"0"::: ) ) ($#k2_rcomp_1 :::".["::: ) ) ")" )) "is" ($#v1_fcont_1 :::"continuous"::: ) ) ; theorem :: SINCOS10:132 (Bool (Set (Set ($#k4_sincos10 :::"arccosec2"::: ) ) ($#k2_partfun1 :::"|"::: ) (Set "(" (Set ($#k2_fdiff_9 :::"cosec"::: ) ) ($#k7_relset_1 :::".:"::: ) (Set ($#k2_rcomp_1 :::"]."::: ) (Set ($#k6_numbers :::"0"::: ) ) "," (Set "(" (Set ($#k32_sin_cos :::"PI"::: ) ) ($#k10_real_1 :::"/"::: ) (Num 2) ")" ) ($#k2_rcomp_1 :::".["::: ) ) ")" )) "is" ($#v1_fcont_1 :::"continuous"::: ) ) ;