:: SINCOS10 semantic presentation

REAL is non empty V46() V47() V48() V52() V67() V68() V70() V73() set
NAT is non empty epsilon-transitive epsilon-connected ordinal V46() V47() V48() V49() V50() V51() V52() V65() V67() Element of K6(REAL)
K6(REAL) is set
COMPLEX is non empty V46() V52() V73() set
0 is empty epsilon-transitive epsilon-connected ordinal T-Sequence-like c=-linear natural V11() real ext-real non positive non negative Function-like functional V46() V47() V48() V49() V50() V51() V52() V67() V70() V71() set
1 is non empty epsilon-transitive epsilon-connected ordinal natural V11() real ext-real positive non negative V46() V47() V48() V49() V50() V51() V65() V67() V71() Element of NAT
{0,1} is non empty V46() V47() V48() V49() V50() V51() V65() V67() set
INT is non empty V46() V47() V48() V49() V50() V52() V73() set
K7(REAL,REAL) is V36() V37() V38() set
K6(K7(REAL,REAL)) is set
K7(NAT,REAL) is V36() V37() V38() set
K6(K7(NAT,REAL)) is set
K7(NAT,COMPLEX) is V36() set
K6(K7(NAT,COMPLEX)) is set
K7(COMPLEX,COMPLEX) is V36() set
K6(K7(COMPLEX,COMPLEX)) is set
omega is non empty epsilon-transitive epsilon-connected ordinal V46() V47() V48() V49() V50() V51() V52() V65() V67() set
K6(omega) is set
K6(NAT) is set
RAT is non empty V46() V47() V48() V49() V52() V73() set
PI is non empty V11() real ext-real positive non negative Element of REAL
2 is non empty epsilon-transitive epsilon-connected ordinal natural V11() real ext-real positive non negative V46() V47() V48() V49() V50() V51() V65() V67() V71() Element of NAT
PI / 2 is non empty V11() real ext-real positive non negative Element of REAL
K39(2) is non empty V11() real ext-real positive non negative set
K37(PI,K39(2)) is non empty V11() real ext-real positive non negative set
- (PI / 2) is non empty V11() real ext-real non positive negative Element of REAL
2 * PI is non empty V11() real ext-real positive non negative Element of REAL
0 is empty epsilon-transitive epsilon-connected ordinal T-Sequence-like c=-linear natural V11() real ext-real non positive non negative Function-like functional V46() V47() V48() V49() V50() V51() V52() V67() V70() V71() Element of NAT
3 is non empty epsilon-transitive epsilon-connected ordinal natural V11() real ext-real positive non negative V46() V47() V48() V49() V50() V51() V65() V67() V71() Element of NAT
3 / 2 is non empty V11() real ext-real positive non negative Element of REAL
K37(3,K39(2)) is non empty V11() real ext-real positive non negative set
(3 / 2) * PI is non empty V11() real ext-real positive non negative Element of REAL
- 1 is non empty V11() real ext-real non positive negative V71() Element of REAL
sin is V19() V22( REAL ) V23( REAL ) Function-like quasi_total V36() V37() V38() Element of K6(K7(REAL,REAL))
cos is V19() V22( REAL ) V23( REAL ) Function-like quasi_total V36() V37() V38() Element of K6(K7(REAL,REAL))
dom sin is V46() V47() V48() Element of K6(REAL)
dom cos is V46() V47() V48() Element of K6(REAL)
cos . 0 is V11() real ext-real Element of REAL
sin . 0 is V11() real ext-real Element of REAL
4 is non empty epsilon-transitive epsilon-connected ordinal natural V11() real ext-real positive non negative V46() V47() V48() V49() V50() V51() V65() V67() V71() Element of NAT
PI / 4 is non empty V11() real ext-real positive non negative Element of REAL
K39(4) is non empty V11() real ext-real positive non negative set
K37(PI,K39(4)) is non empty V11() real ext-real positive non negative set
sin . (PI / 4) is V11() real ext-real Element of REAL
cos . (PI / 4) is V11() real ext-real Element of REAL
cos . (PI / 2) is V11() real ext-real Element of REAL
sin . (PI / 2) is V11() real ext-real Element of REAL
cos . PI is V11() real ext-real Element of REAL
sin . PI is V11() real ext-real Element of REAL
PI + (PI / 2) is non empty V11() real ext-real positive non negative Element of REAL
cos . (PI + (PI / 2)) is V11() real ext-real Element of REAL
sin . (PI + (PI / 2)) is V11() real ext-real Element of REAL
cos . (2 * PI) is V11() real ext-real Element of REAL
sin . (2 * PI) is V11() real ext-real Element of REAL
].0,PI.[ is open V46() V47() V48() V65() V66() V70() Element of K6(REAL)
{ b₁ where b₁ is V11() real ext-real Element of REAL : ( not b₁ <= 0 & not PI <= b₁ ) } is set
[.0,PI.] is closed V46() V47() V48() V70() Element of K6(REAL)
{ b₁ where b₁ is V11() real ext-real Element of REAL : ( 0 <= b₁ & b₁ <= PI ) } is set
].PI,(2 * PI).[ is open V46() V47() V48() V65() V66() V70() Element of K6(REAL)
{ b₁ where b₁ is V11() real ext-real Element of REAL : ( not b₁ <= PI & not 2 * PI <= b₁ ) } is set
].(- (PI / 2)),(PI / 2).[ is open V46() V47() V48() V65() V66() V70() Element of K6(REAL)
{ b₁ where b₁ is V11() real ext-real Element of REAL : ( not b₁ <= - (PI / 2) & not PI / 2 <= b₁ ) } is set
[.(- (PI / 2)),(PI / 2).] is closed V46() V47() V48() V70() Element of K6(REAL)
{ b₁ where b₁ is V11() real ext-real Element of REAL : ( - (PI / 2) <= b₁ & b₁ <= PI / 2 ) } is set
].(PI / 2),((3 / 2) * PI).[ is open V46() V47() V48() V65() V66() V70() Element of K6(REAL)
{ b₁ where b₁ is V11() real ext-real Element of REAL : ( not b₁ <= PI / 2 & not (3 / 2) * PI <= b₁ ) } is set
sqrt 2 is V11() real ext-real Element of REAL
{0} is non empty V46() V47() V48() V49() V50() V51() V65() V67() set
sec is V19() V22( REAL ) V23( REAL ) Function-like V36() V37() V38() Element of K6(K7(REAL,REAL))
cos ^ is V19() V22( REAL ) V23( REAL ) Function-like V36() V37() V38() Element of K6(K7(REAL,REAL))
dom sec is V46() V47() V48() Element of K6(REAL)
cosec is V19() V22( REAL ) V23( REAL ) Function-like V36() V37() V38() Element of K6(K7(REAL,REAL))
sin ^ is V19() V22( REAL ) V23( REAL ) Function-like V36() V37() V38() Element of K6(K7(REAL,REAL))
dom cosec is V46() V47() V48() Element of K6(REAL)
[.0,(PI / 2).[ is V46() V47() V48() V66() V70() Element of K6(REAL)
{ b₁ where b₁ is V11() real ext-real Element of REAL : ( 0 <= b₁ & not PI / 2 <= b₁ ) } is set
x0 is set
].0,(PI / 2).[ is open V46() V47() V48() V65() V66() V70() Element of K6(REAL)
{ b₁ where b₁ is V11() real ext-real Element of REAL : ( not b₁ <= 0 & not PI / 2 <= b₁ ) } is set
].0,(PI / 2).[ \/ {0} is non empty V46() V47() V48() set
cos " {0} is V46() V47() V48() Element of K6(REAL)
[.0,(PI / 2).[ /\ (cos " {0}) is V46() V47() V48() set
x0 is set
cos . x0 is V11() real ext-real Element of REAL
[.0,(PI / 2).[ \ (cos " {0}) is V46() V47() V48() set
(dom cos) \ (cos " {0}) is V46() V47() V48() set
].(PI / 2),PI.] is V46() V47() V48() V65() V70() Element of K6(REAL)
{ b₁ where b₁ is V11() real ext-real Element of REAL : ( not b₁ <= PI / 2 & b₁ <= PI ) } is set
PI / 1 is non empty V11() real ext-real positive non negative Element of REAL
K39(1) is non empty V11() real ext-real positive non negative set
K37(PI,K39(1)) is non empty V11() real ext-real positive non negative set
{PI} is non empty V46() V47() V48() set
x0 is set
].(PI / 2),PI.[ is open V46() V47() V48() V65() V66() V70() Element of K6(REAL)
{ b₁ where b₁ is V11() real ext-real Element of REAL : ( not b₁ <= PI / 2 & not PI <= b₁ ) } is set
].(PI / 2),PI.[ \/ {PI} is non empty V46() V47() V48() set
cos " {0} is V46() V47() V48() Element of K6(REAL)
].(PI / 2),PI.] /\ (cos " {0}) is V46() V47() V48() set
x0 is set
cos . x0 is V11() real ext-real Element of REAL
].(PI / 2),PI.] \ (cos " {0}) is V46() V47() V48() set
(dom cos) \ (cos " {0}) is V46() V47() V48() set
[.(- (PI / 2)),0.[ is V46() V47() V48() V66() V70() Element of K6(REAL)
{ b₁ where b₁ is V11() real ext-real Element of REAL : ( - (PI / 2) <= b₁ & not 0 <= b₁ ) } is set
- PI is non empty V11() real ext-real non positive negative Element of REAL
].(- PI),0.[ is open V46() V47() V48() V65() V66() V70() Element of K6(REAL)
{ b₁ where b₁ is V11() real ext-real Element of REAL : ( not b₁ <= - PI & not 0 <= b₁ ) } is set
PI / 1 is non empty V11() real ext-real positive non negative Element of REAL
K39(1) is non empty V11() real ext-real positive non negative set
K37(PI,K39(1)) is non empty V11() real ext-real positive non negative set
{(- (PI / 2))} is non empty V46() V47() V48() set
x0 is set
].(- (PI / 2)),0.[ is open V46() V47() V48() V65() V66() V70() Element of K6(REAL)
{ b₁ where b₁ is V11() real ext-real Element of REAL : ( not b₁ <= - (PI / 2) & not 0 <= b₁ ) } is set
].(- (PI / 2)),0.[ \/ {(- (PI / 2))} is non empty V46() V47() V48() set
sin " {0} is V46() V47() V48() Element of K6(REAL)
[.(- (PI / 2)),0.[ /\ (sin " {0}) is V46() V47() V48() set
x0 is set
g1 is V11() real ext-real set
0 + (2 * PI) is non empty V11() real ext-real positive non negative Element of REAL
g1 + (2 * PI) is V11() real ext-real Element of REAL
(- PI) + (2 * PI) is V11() real ext-real Element of REAL
sin . (g1 + (2 * PI)) is V11() real ext-real Element of REAL
sin . g1 is V11() real ext-real Element of REAL
[.(- (PI / 2)),0.[ \ (sin " {0}) is V46() V47() V48() set
(dom sin) \ (sin " {0}) is V46() V47() V48() set
].0,(PI / 2).] is V46() V47() V48() V65() V70() Element of K6(REAL)
{ b₁ where b₁ is V11() real ext-real Element of REAL : ( not b₁ <= 0 & b₁ <= PI / 2 ) } is set
PI / 1 is non empty V11() real ext-real positive non negative Element of REAL
K39(1) is non empty V11() real ext-real positive non negative set
K37(PI,K39(1)) is non empty V11() real ext-real positive non negative set
{(PI / 2)} is non empty V46() V47() V48() set
x0 is set
].0,(PI / 2).[ is open V46() V47() V48() V65() V66() V70() Element of K6(REAL)
{ b₁ where b₁ is V11() real ext-real Element of REAL : ( not b₁ <= 0 & not PI / 2 <= b₁ ) } is set
].0,(PI / 2).[ \/ {(PI / 2)} is non empty V46() V47() V48() set
sin " {0} is V46() V47() V48() Element of K6(REAL)
].0,(PI / 2).] /\ (sin " {0}) is V46() V47() V48() set
x0 is set
sin . x0 is V11() real ext-real Element of REAL
].0,(PI / 2).] \ (sin " {0}) is V46() V47() V48() set
(dom sin) \ (sin " {0}) is V46() V47() V48() set
].0,(PI / 2).[ is open V46() V47() V48() V65() V66() V70() Element of K6(REAL)
{ b₁ where b₁ is V11() real ext-real Element of REAL : ( not b₁ <= 0 & not PI / 2 <= b₁ ) } is set
].0,(PI / 2).[ \/ {0} is non empty V46() V47() V48() set
g1 is V11() real ext-real Element of REAL
diff (sec,g1) is V11() real ext-real Element of REAL
sin . g1 is V11() real ext-real Element of REAL
cos . g1 is V11() real ext-real Element of REAL
(cos . g1) ^2 is V11() real ext-real Element of REAL
K37((cos . g1),(cos . g1)) is V11() real ext-real set
(sin . g1) / ((cos . g1) ^2) is V11() real ext-real Element of REAL
K39(((cos . g1) ^2)) is V11() real ext-real set
K37((sin . g1),K39(((cos . g1) ^2))) is V11() real ext-real set
sec `| ].0,(PI / 2).[ is V19() V22( REAL ) V23( REAL ) Function-like V36() V37() V38() Element of K6(K7(REAL,REAL))
(sec `| ].0,(PI / 2).[) . g1 is V11() real ext-real Element of REAL
g1 is V11() real ext-real Element of REAL
diff (sec,g1) is V11() real ext-real Element of REAL
sin . g1 is V11() real ext-real Element of REAL
cos . g1 is V11() real ext-real Element of REAL
(cos . g1) ^2 is V11() real ext-real Element of REAL
K37((cos . g1),(cos . g1)) is V11() real ext-real set
(sin . g1) / ((cos . g1) ^2) is V11() real ext-real Element of REAL
K39(((cos . g1) ^2)) is V11() real ext-real set
K37((sin . g1),K39(((cos . g1) ^2))) is V11() real ext-real set
].(PI / 2),PI.[ is open V46() V47() V48() V65() V66() V70() Element of K6(REAL)
{ b₁ where b₁ is V11() real ext-real Element of REAL : ( not b₁ <= PI / 2 & not PI <= b₁ ) } is set
PI / 1 is non empty V11() real ext-real positive non negative Element of REAL
K39(1) is non empty V11() real ext-real positive non negative set
K37(PI,K39(1)) is non empty V11() real ext-real positive non negative set
{PI} is non empty V46() V47() V48() set
].(PI / 2),PI.[ \/ {PI} is non empty V46() V47() V48() set
g1 is V11() real ext-real Element of REAL
diff (sec,g1) is V11() real ext-real Element of REAL
sin . g1 is V11() real ext-real Element of REAL
cos . g1 is V11() real ext-real Element of REAL
(cos . g1) ^2 is V11() real ext-real Element of REAL
K37((cos . g1),(cos . g1)) is V11() real ext-real set
(sin . g1) / ((cos . g1) ^2) is V11() real ext-real Element of REAL
K39(((cos . g1) ^2)) is V11() real ext-real set
K37((sin . g1),K39(((cos . g1) ^2))) is V11() real ext-real set
sec `| ].(PI / 2),PI.[ is V19() V22( REAL ) V23( REAL ) Function-like V36() V37() V38() Element of K6(K7(REAL,REAL))
(sec `| ].(PI / 2),PI.[) . g1 is V11() real ext-real Element of REAL
g1 is V11() real ext-real Element of REAL
diff (sec,g1) is V11() real ext-real Element of REAL
sin . g1 is V11() real ext-real Element of REAL
cos . g1 is V11() real ext-real Element of REAL
(cos . g1) ^2 is V11() real ext-real Element of REAL
K37((cos . g1),(cos . g1)) is V11() real ext-real set
(sin . g1) / ((cos . g1) ^2) is V11() real ext-real Element of REAL
K39(((cos . g1) ^2)) is V11() real ext-real set
K37((sin . g1),K39(((cos . g1) ^2))) is V11() real ext-real set
].(- (PI / 2)),0.[ is open V46() V47() V48() V65() V66() V70() Element of K6(REAL)
{ b₁ where b₁ is V11() real ext-real Element of REAL : ( not b₁ <= - (PI / 2) & not 0 <= b₁ ) } is set
{(- (PI / 2))} is non empty V46() V47() V48() set
].(- (PI / 2)),0.[ \/ {(- (PI / 2))} is non empty V46() V47() V48() set
g1 is V11() real ext-real Element of REAL
diff (cosec,g1) is V11() real ext-real Element of REAL
cos . g1 is V11() real ext-real Element of REAL
sin . g1 is V11() real ext-real Element of REAL
(sin . g1) ^2 is V11() real ext-real Element of REAL
K37((sin . g1),(sin . g1)) is V11() real ext-real set
(cos . g1) / ((sin . g1) ^2) is V11() real ext-real Element of REAL
K39(((sin . g1) ^2)) is V11() real ext-real set
K37((cos . g1),K39(((sin . g1) ^2))) is V11() real ext-real set
- ((cos . g1) / ((sin . g1) ^2)) is V11() real ext-real Element of REAL
cosec `| ].(- (PI / 2)),0.[ is V19() V22( REAL ) V23( REAL ) Function-like V36() V37() V38() Element of K6(K7(REAL,REAL))
(cosec `| ].(- (PI / 2)),0.[) . g1 is V11() real ext-real Element of REAL
g1 is V11() real ext-real Element of REAL
diff (cosec,g1) is V11() real ext-real Element of REAL
cos . g1 is V11() real ext-real Element of REAL
sin . g1 is V11() real ext-real Element of REAL
(sin . g1) ^2 is V11() real ext-real Element of REAL
K37((sin . g1),(sin . g1)) is V11() real ext-real set
(cos . g1) / ((sin . g1) ^2) is V11() real ext-real Element of REAL
K39(((sin . g1) ^2)) is V11() real ext-real set
K37((cos . g1),K39(((sin . g1) ^2))) is V11() real ext-real set
- ((cos . g1) / ((sin . g1) ^2)) is V11() real ext-real Element of REAL
{(PI / 2)} is non empty V46() V47() V48() set
].0,(PI / 2).[ \/ {(PI / 2)} is non empty V46() V47() V48() set
g1 is V11() real ext-real Element of REAL
diff (cosec,g1) is V11() real ext-real Element of REAL
cos . g1 is V11() real ext-real Element of REAL
sin . g1 is V11() real ext-real Element of REAL
(sin . g1) ^2 is V11() real ext-real Element of REAL
K37((sin . g1),(sin . g1)) is V11() real ext-real set
(cos . g1) / ((sin . g1) ^2) is V11() real ext-real Element of REAL
K39(((sin . g1) ^2)) is V11() real ext-real set
K37((cos . g1),K39(((sin . g1) ^2))) is V11() real ext-real set
- ((cos . g1) / ((sin . g1) ^2)) is V11() real ext-real Element of REAL
cosec `| ].0,(PI / 2).[ is V19() V22( REAL ) V23( REAL ) Function-like V36() V37() V38() Element of K6(K7(REAL,REAL))
(cosec `| ].0,(PI / 2).[) . g1 is V11() real ext-real Element of REAL
g1 is V11() real ext-real Element of REAL
diff (cosec,g1) is V11() real ext-real Element of REAL
cos . g1 is V11() real ext-real Element of REAL
sin . g1 is V11() real ext-real Element of REAL
(sin . g1) ^2 is V11() real ext-real Element of REAL
K37((sin . g1),(sin . g1)) is V11() real ext-real set
(cos . g1) / ((sin . g1) ^2) is V11() real ext-real Element of REAL
K39(((sin . g1) ^2)) is V11() real ext-real set
K37((cos . g1),K39(((sin . g1) ^2))) is V11() real ext-real set
- ((cos . g1) / ((sin . g1) ^2)) is V11() real ext-real Element of REAL
sec | ].0,(PI / 2).[ is V19() V22( REAL ) V23( REAL ) Function-like V36() V37() V38() Element of K6(K7(REAL,REAL))
sec | ].(PI / 2),PI.[ is V19() V22( REAL ) V23( REAL ) Function-like V36() V37() V38() Element of K6(K7(REAL,REAL))
cosec | ].(- (PI / 2)),0.[ is V19() V22( REAL ) V23( REAL ) Function-like V36() V37() V38() Element of K6(K7(REAL,REAL))
cosec | ].0,(PI / 2).[ is V19() V22( REAL ) V23( REAL ) Function-like V36() V37() V38() Element of K6(K7(REAL,REAL))
3 / 4 is non empty V11() real ext-real positive non negative Element of REAL
K37(3,K39(4)) is non empty V11() real ext-real positive non negative set
(3 / 4) * PI is non empty V11() real ext-real positive non negative Element of REAL
(PI / 4) + (PI / 2) is non empty V11() real ext-real positive non negative Element of REAL
0 + (PI / 2) is non empty V11() real ext-real positive non negative Element of REAL
(PI / 2) + (PI / 2) is non empty V11() real ext-real positive non negative Element of REAL
- (PI / 4) is non empty V11() real ext-real non positive negative Element of REAL
[.0,(PI / 4).] is closed V46() V47() V48() V70() Element of K6(REAL)
{ b₁ where b₁ is V11() real ext-real Element of REAL : ( 0 <= b₁ & b₁ <= PI / 4 ) } is set
[.((3 / 4) * PI),PI.] is closed V46() V47() V48() V70() Element of K6(REAL)
{ b₁ where b₁ is V11() real ext-real Element of REAL : ( (3 / 4) * PI <= b₁ & b₁ <= PI ) } is set
[.(- (PI / 2)),(- (PI / 4)).] is closed V46() V47() V48() V70() Element of K6(REAL)
{ b₁ where b₁ is V11() real ext-real Element of REAL : ( - (PI / 2) <= b₁ & b₁ <= - (PI / 4) ) } is set
[.(PI / 4),(PI / 2).] is closed V46() V47() V48() V70() Element of K6(REAL)
{ b₁ where b₁ is V11() real ext-real Element of REAL : ( PI / 4 <= b₁ & b₁ <= PI / 2 ) } is set
dom (sec | ].0,(PI / 2).[) is V46() V47() V48() Element of K6(REAL)
sec | [.0,(PI / 2).[ is V19() V22( REAL ) V23( REAL ) Function-like V36() V37() V38() Element of K6(K7(REAL,REAL))
(sec | [.0,(PI / 2).[) | ].0,(PI / 2).[ is V19() V22( REAL ) V23( REAL ) Function-like V36() V37() V38() Element of K6(K7(REAL,REAL))
dom ((sec | [.0,(PI / 2).[) | ].0,(PI / 2).[) is V46() V47() V48() Element of K6(REAL)
dom (sec | ].(PI / 2),PI.[) is V46() V47() V48() Element of K6(REAL)
sec | ].(PI / 2),PI.] is V19() V22( REAL ) V23( REAL ) Function-like V36() V37() V38() Element of K6(K7(REAL,REAL))
(sec | ].(PI / 2),PI.]) | ].(PI / 2),PI.[ is V19() V22( REAL ) V23( REAL ) Function-like V36() V37() V38() Element of K6(K7(REAL,REAL))
dom ((sec | ].(PI / 2),PI.]) | ].(PI / 2),PI.[) is V46() V47() V48() Element of K6(REAL)
dom (cosec | ].(- (PI / 2)),0.[) is V46() V47() V48() Element of K6(REAL)
cosec | [.(- (PI / 2)),0.[ is V19() V22( REAL ) V23( REAL ) Function-like V36() V37() V38() Element of K6(K7(REAL,REAL))
(cosec | [.(- (PI / 2)),0.[) | ].(- (PI / 2)),0.[ is V19() V22( REAL ) V23( REAL ) Function-like V36() V37() V38() Element of K6(K7(REAL,REAL))
dom ((cosec | [.(- (PI / 2)),0.[) | ].(- (PI / 2)),0.[) is V46() V47() V48() Element of K6(REAL)
dom (cosec | ].0,(PI / 2).[) is V46() V47() V48() Element of K6(REAL)
cosec | ].0,(PI / 2).] is V19() V22( REAL ) V23( REAL ) Function-like V36() V37() V38() Element of K6(K7(REAL,REAL))
(cosec | ].0,(PI / 2).]) | ].0,(PI / 2).[ is V19() V22( REAL ) V23( REAL ) Function-like V36() V37() V38() Element of K6(K7(REAL,REAL))
dom ((cosec | ].0,(PI / 2).]) | ].0,(PI / 2).[) is V46() V47() V48() Element of K6(REAL)
x0 is V11() real ext-real Element of REAL
diff (sec,x0) is V11() real ext-real Element of REAL
cos . x0 is V11() real ext-real Element of REAL
PI / 1 is non empty V11() real ext-real positive non negative Element of REAL
K39(1) is non empty V11() real ext-real positive non negative set
K37(PI,K39(1)) is non empty V11() real ext-real positive non negative set
sin . x0 is V11() real ext-real Element of REAL
(cos . x0) ^2 is V11() real ext-real Element of REAL
K37((cos . x0),(cos . x0)) is V11() real ext-real set
(sin . x0) / ((cos . x0) ^2) is V11() real ext-real Element of REAL
K39(((cos . x0) ^2)) is V11() real ext-real set
K37((sin . x0),K39(((cos . x0) ^2))) is V11() real ext-real set
0 / ((cos . x0) ^2) is V11() real ext-real Element of REAL
K37(0,K39(((cos . x0) ^2))) is V11() real ext-real set
x0 is V11() real ext-real Element of REAL
diff (sec,x0) is V11() real ext-real Element of REAL
cos . x0 is V11() real ext-real Element of REAL
sin . x0 is V11() real ext-real Element of REAL
(cos . x0) ^2 is V11() real ext-real Element of REAL
K37((cos . x0),(cos . x0)) is V11() real ext-real set
(sin . x0) / ((cos . x0) ^2) is V11() real ext-real Element of REAL
K39(((cos . x0) ^2)) is V11() real ext-real set
K37((sin . x0),K39(((cos . x0) ^2))) is V11() real ext-real set
0 / ((cos . x0) ^2) is V11() real ext-real Element of REAL
K37(0,K39(((cos . x0) ^2))) is V11() real ext-real set
x0 is V11() real ext-real Element of REAL
diff (cosec,x0) is V11() real ext-real Element of REAL
0 + (2 * PI) is non empty V11() real ext-real positive non negative Element of REAL
x0 + (2 * PI) is V11() real ext-real Element of REAL
{(- (PI / 2))} is non empty V46() V47() V48() set
].(- (PI / 2)),0.[ \/ {(- (PI / 2))} is non empty V46() V47() V48() set
(- PI) + (2 * PI) is V11() real ext-real Element of REAL
sin . (x0 + (2 * PI)) is V11() real ext-real Element of REAL
sin . x0 is V11() real ext-real Element of REAL
cos . x0 is V11() real ext-real Element of REAL
- 0 is empty epsilon-transitive epsilon-connected ordinal T-Sequence-like c=-linear natural V11() real ext-real non positive non negative Function-like functional V46() V47() V48() V49() V50() V51() V52() V67() V70() V71() Element of REAL
(sin . x0) ^2 is V11() real ext-real Element of REAL
K37((sin . x0),(sin . x0)) is V11() real ext-real set
(cos . x0) / ((sin . x0) ^2) is V11() real ext-real Element of REAL
K39(((sin . x0) ^2)) is V11() real ext-real set
K37((cos . x0),K39(((sin . x0) ^2))) is V11() real ext-real set
- ((cos . x0) / ((sin . x0) ^2)) is V11() real ext-real Element of REAL
x0 is V11() real ext-real Element of REAL
diff (cosec,x0) is V11() real ext-real Element of REAL
cos . x0 is V11() real ext-real Element of REAL
sin . x0 is V11() real ext-real Element of REAL
- 0 is empty epsilon-transitive epsilon-connected ordinal T-Sequence-like c=-linear natural V11() real ext-real non positive non negative Function-like functional V46() V47() V48() V49() V50() V51() V52() V67() V70() V71() Element of REAL
(sin . x0) ^2 is V11() real ext-real Element of REAL
K37((sin . x0),(sin . x0)) is V11() real ext-real set
(cos . x0) / ((sin . x0) ^2) is V11() real ext-real Element of REAL
K39(((sin . x0) ^2)) is V11() real ext-real set
K37((cos . x0),K39(((sin . x0) ^2))) is V11() real ext-real set
- ((cos . x0) / ((sin . x0) ^2)) is V11() real ext-real Element of REAL
x0 is V11() real ext-real Element of REAL
[.0,(PI / 2).[ /\ (dom sec) is V46() V47() V48() set
g1 is V11() real ext-real Element of REAL
cos g1 is V11() real ext-real Element of REAL
cos . g1 is V11() real ext-real Element of REAL
(2 * PI) * 0 is empty epsilon-transitive epsilon-connected ordinal T-Sequence-like c=-linear natural V11() real ext-real non positive non negative Function-like functional V46() V47() V48() V49() V50() V51() V52() V67() V70() V71() Element of REAL
(- (PI / 2)) + ((2 * PI) * 0) is non empty V11() real ext-real non positive negative Element of REAL
(PI / 2) + ((2 * PI) * 0) is non empty V11() real ext-real positive non negative Element of REAL
1 / (cos . g1) is V11() real ext-real Element of REAL
K39((cos . g1)) is V11() real ext-real set
K37(1,K39((cos . g1))) is V11() real ext-real set
1 / 1 is non empty V11() real ext-real positive non negative Element of REAL
K39(1) is non empty V11() real ext-real positive non negative set
K37(1,K39(1)) is non empty V11() real ext-real positive non negative set
sec . x0 is V11() real ext-real Element of REAL
sec . g1 is V11() real ext-real Element of REAL
].0,(PI / 2).[ /\ (dom sec) is V46() V47() V48() set
sec . g1 is V11() real ext-real Element of REAL
sec . x0 is V11() real ext-real Element of REAL
sec . g1 is V11() real ext-real Element of REAL
sec . x0 is V11() real ext-real Element of REAL
sec . g1 is V11() real ext-real Element of REAL
sec . x0 is V11() real ext-real Element of REAL
x0 is V11() real ext-real Element of REAL
].(PI / 2),PI.] /\ (dom sec) is V46() V47() V48() set
g1 is V11() real ext-real Element of REAL
].(PI / 2),PI.[ /\ (dom sec) is V46() V47() V48() set
sec . g1 is V11() real ext-real Element of REAL
sec . x0 is V11() real ext-real Element of REAL
PI * (3 / 2) is non empty V11() real ext-real positive non negative Element of REAL
PI * 1 is non empty V11() real ext-real positive non negative Element of REAL
(2 * PI) * 0 is empty epsilon-transitive epsilon-connected ordinal T-Sequence-like c=-linear natural V11() real ext-real non positive non negative Function-like functional V46() V47() V48() V49() V50() V51() V52() V67() V70() V71() Element of REAL
((3 / 2) * PI) + ((2 * PI) * 0) is non empty V11() real ext-real positive non negative Element of REAL
(PI / 2) + ((2 * PI) * 0) is non empty V11() real ext-real positive non negative Element of REAL
cos x0 is V11() real ext-real Element of REAL
cos . x0 is V11() real ext-real Element of REAL
(- 1) " is non empty V11() real ext-real non positive negative Element of REAL
(cos . x0) " is V11() real ext-real Element of REAL
sec . g1 is V11() real ext-real Element of REAL
1 / (- 1) is non empty V11() real ext-real non positive negative Element of REAL
K39((- 1)) is non empty V11() real ext-real non positive negative set
K37(1,K39((- 1))) is non empty V11() real ext-real non positive negative set
sec . x0 is V11() real ext-real Element of REAL
sec . g1 is V11() real ext-real Element of REAL
sec . x0 is V11() real ext-real Element of REAL
sec . g1 is V11() real ext-real Element of REAL
sec . x0 is V11() real ext-real Element of REAL
x0 is V11() real ext-real Element of REAL
[.(- (PI / 2)),0.[ /\ (dom cosec) is V46() V47() V48() set
g1 is V11() real ext-real Element of REAL
g1 + (2 * PI) is V11() real ext-real Element of REAL
(- PI) + (2 * PI) is V11() real ext-real Element of REAL
0 + (2 * PI) is non empty V11() real ext-real positive non negative Element of REAL
sin . (g1 + (2 * PI)) is V11() real ext-real Element of REAL
sin . g1 is V11() real ext-real Element of REAL
(2 * PI) * (- 1) is non empty V11() real ext-real non positive negative Element of REAL
(2 * PI) + ((2 * PI) * (- 1)) is V11() real ext-real Element of REAL
((3 / 2) * PI) + ((2 * PI) * (- 1)) is V11() real ext-real Element of REAL
sin g1 is V11() real ext-real Element of REAL
(- 1) " is non empty V11() real ext-real non positive negative Element of REAL
(sin . g1) " is V11() real ext-real Element of REAL
cosec . x0 is V11() real ext-real Element of REAL
sin . (- (PI / 2)) is V11() real ext-real Element of REAL
1 / (sin . (- (PI / 2))) is V11() real ext-real Element of REAL
K39((sin . (- (PI / 2)))) is V11() real ext-real set
K37(1,K39((sin . (- (PI / 2))))) is V11() real ext-real set
1 / (- 1) is non empty V11() real ext-real non positive negative Element of REAL
K39((- 1)) is non empty V11() real ext-real non positive negative set
K37(1,K39((- 1))) is non empty V11() real ext-real non positive negative set
cosec . g1 is V11() real ext-real Element of REAL
].(- (PI / 2)),0.[ /\ (dom cosec) is V46() V47() V48() set
cosec . x0 is V11() real ext-real Element of REAL
cosec . g1 is V11() real ext-real Element of REAL
cosec . x0 is V11() real ext-real Element of REAL
cosec . g1 is V11() real ext-real Element of REAL
cosec . x0 is V11() real ext-real Element of REAL
cosec . g1 is V11() real ext-real Element of REAL
x0 is V11() real ext-real Element of REAL
].0,(PI / 2).] /\ (dom cosec) is V46() V47() V48() set
g1 is V11() real ext-real Element of REAL
].0,(PI / 2).[ /\ (dom cosec) is V46() V47() V48() set
cosec . x0 is V11() real ext-real Element of REAL
cosec . g1 is V11() real ext-real Element of REAL
sin x0 is V11() real ext-real Element of REAL
sin . x0 is V11() real ext-real Element of REAL
1 / (sin . x0) is V11() real ext-real Element of REAL
K39((sin . x0)) is V11() real ext-real set
K37(1,K39((sin . x0))) is V11() real ext-real set
1 / 1 is non empty V11() real ext-real positive non negative Element of REAL
K39(1) is non empty V11() real ext-real positive non negative set
K37(1,K39(1)) is non empty V11() real ext-real positive non negative set
cosec . g1 is V11() real ext-real Element of REAL
cosec . x0 is V11() real ext-real Element of REAL
cosec . x0 is V11() real ext-real Element of REAL
cosec . g1 is V11() real ext-real Element of REAL
cosec . x0 is V11() real ext-real Element of REAL
cosec . g1 is V11() real ext-real Element of REAL
(sec | [.0,(PI / 2).[) " is V19() V22( REAL ) V23( REAL ) Function-like one-to-one V36() V37() V38() Element of K6(K7(REAL,REAL))
(sec | ].(PI / 2),PI.]) " is V19() V22( REAL ) V23( REAL ) Function-like one-to-one V36() V37() V38() Element of K6(K7(REAL,REAL))
(cosec | [.(- (PI / 2)),0.[) " is V19() V22( REAL ) V23( REAL ) Function-like one-to-one V36() V37() V38() Element of K6(K7(REAL,REAL))
(cosec | ].0,(PI / 2).]) " is V19() V22( REAL ) V23( REAL ) Function-like one-to-one V36() V37() V38() Element of K6(K7(REAL,REAL))
() is V19() V22( REAL ) V23( REAL ) Function-like V36() V37() V38() Element of K6(K7(REAL,REAL))
() is V19() V22( REAL ) V23( REAL ) Function-like V36() V37() V38() Element of K6(K7(REAL,REAL))
() is V19() V22( REAL ) V23( REAL ) Function-like V36() V37() V38() Element of K6(K7(REAL,REAL))
() is V19() V22( REAL ) V23( REAL ) Function-like V36() V37() V38() Element of K6(K7(REAL,REAL))
x0 is V11() real ext-real Element of REAL
() . x0 is V11() real ext-real Element of REAL
() . x0 is V11() real ext-real Element of REAL
() . x0 is V11() real ext-real Element of REAL
() . x0 is V11() real ext-real Element of REAL
x0 is V11() real ext-real Element of REAL
(x0) is set
() . x0 is V11() real ext-real Element of REAL
(x0) is set
() . x0 is V11() real ext-real Element of REAL
(x0) is set
() . x0 is V11() real ext-real Element of REAL
(x0) is set
() . x0 is V11() real ext-real Element of REAL
() " is V19() Function-like set
() " is V19() Function-like set
() " is V19() Function-like set
() " is V19() Function-like set
rng () is V46() V47() V48() Element of K6(REAL)
dom (sec | [.0,(PI / 2).[) is V46() V47() V48() Element of K6(REAL)
rng () is V46() V47() V48() Element of K6(REAL)
dom (sec | ].(PI / 2),PI.]) is V46() V47() V48() Element of K6(REAL)
rng () is V46() V47() V48() Element of K6(REAL)
dom (cosec | [.(- (PI / 2)),0.[) is V46() V47() V48() Element of K6(REAL)
rng () is V46() V47() V48() Element of K6(REAL)
dom (cosec | ].0,(PI / 2).]) is V46() V47() V48() Element of K6(REAL)
1 / (sqrt 2) is V11() real ext-real Element of REAL
K39((sqrt 2)) is V11() real ext-real set
K37(1,K39((sqrt 2))) is V11() real ext-real set
1 / 2 is non empty V11() real ext-real positive non negative Element of REAL
K37(1,K39(2)) is non empty V11() real ext-real positive non negative set
sqrt (1 / 2) is V11() real ext-real Element of REAL
(sqrt (1 / 2)) ^2 is V11() real ext-real Element of REAL
K37((sqrt (1 / 2)),(sqrt (1 / 2))) is V11() real ext-real set
(sin . (PI / 4)) ^2 is V11() real ext-real Element of REAL
K37((sin . (PI / 4)),(sin . (PI / 4))) is V11() real ext-real set
((sin . (PI / 4)) ^2) + ((sin . (PI / 4)) ^2) is V11() real ext-real Element of REAL
2 * ((sin . (PI / 4)) ^2) is V11() real ext-real Element of REAL
- (sqrt (1 / 2)) is V11() real ext-real Element of REAL
PI / 1 is non empty V11() real ext-real positive non negative Element of REAL
K39(1) is non empty V11() real ext-real positive non negative set
K37(PI,K39(1)) is non empty V11() real ext-real positive non negative set
sin . (- (PI / 4)) is V11() real ext-real Element of REAL
- (1 / (sqrt 2)) is V11() real ext-real Element of REAL
cos . (- (PI / 4)) is V11() real ext-real Element of REAL
sin . ((3 / 4) * PI) is V11() real ext-real Element of REAL
cos . ((3 / 4) * PI) is V11() real ext-real Element of REAL
PI + (- (PI / 4)) is V11() real ext-real Element of REAL
cos . (PI + (- (PI / 4))) is V11() real ext-real Element of REAL
sin . (PI + (- (PI / 4))) is V11() real ext-real Element of REAL
- (- (1 / (sqrt 2))) is V11() real ext-real Element of REAL
sec . 0 is V11() real ext-real Element of REAL
sec . (PI / 4) is V11() real ext-real Element of REAL
sec . ((3 / 4) * PI) is V11() real ext-real Element of REAL
- (sqrt 2) is V11() real ext-real Element of REAL
sec . PI is V11() real ext-real Element of REAL
1 / (- 1) is non empty V11() real ext-real non positive negative Element of REAL
K39((- 1)) is non empty V11() real ext-real non positive negative set
K37(1,K39((- 1))) is non empty V11() real ext-real non positive negative set
1 / (- (1 / (sqrt 2))) is V11() real ext-real Element of REAL
K39((- (1 / (sqrt 2)))) is V11() real ext-real set
K37(1,K39((- (1 / (sqrt 2))))) is V11() real ext-real set
1 / (1 / (sqrt 2)) is V11() real ext-real Element of REAL
K39((1 / (sqrt 2))) is V11() real ext-real set
K37(1,K39((1 / (sqrt 2)))) is V11() real ext-real set
- (1 / (1 / (sqrt 2))) is V11() real ext-real Element of REAL
1 / 1 is non empty V11() real ext-real positive non negative Element of REAL
K39(1) is non empty V11() real ext-real positive non negative set
K37(1,K39(1)) is non empty V11() real ext-real positive non negative set
cosec . (- (PI / 2)) is V11() real ext-real Element of REAL
cosec . (- (PI / 4)) is V11() real ext-real Element of REAL
cosec . (PI / 4) is V11() real ext-real Element of REAL
cosec . (PI / 2) is V11() real ext-real Element of REAL
1 / 1 is non empty V11() real ext-real positive non negative Element of REAL
K39(1) is non empty V11() real ext-real positive non negative set
K37(1,K39(1)) is non empty V11() real ext-real positive non negative set
1 / (1 / (sqrt 2)) is V11() real ext-real Element of REAL
K39((1 / (sqrt 2))) is V11() real ext-real set
K37(1,K39((1 / (sqrt 2)))) is V11() real ext-real set
sin . (- (PI / 2)) is V11() real ext-real Element of REAL
1 / (sin . (- (PI / 2))) is V11() real ext-real Element of REAL
K39((sin . (- (PI / 2)))) is V11() real ext-real set
K37(1,K39((sin . (- (PI / 2))))) is V11() real ext-real set
1 / (- 1) is non empty V11() real ext-real non positive negative Element of REAL
K39((- 1)) is non empty V11() real ext-real non positive negative set
K37(1,K39((- 1))) is non empty V11() real ext-real non positive negative set
1 / (- (1 / (sqrt 2))) is V11() real ext-real Element of REAL
K39((- (1 / (sqrt 2)))) is V11() real ext-real set
K37(1,K39((- (1 / (sqrt 2))))) is V11() real ext-real set
- (1 / (1 / (sqrt 2))) is V11() real ext-real Element of REAL
[.1,(sqrt 2).] is closed V46() V47() V48() V70() Element of K6(REAL)
{ b₁ where b₁ is V11() real ext-real Element of REAL : ( 1 <= b₁ & b₁ <= sqrt 2 ) } is set
x0 is set
sec . x0 is V11() real ext-real Element of REAL
].0,(PI / 4).[ is open V46() V47() V48() V65() V66() V70() Element of K6(REAL)
{ b₁ where b₁ is V11() real ext-real Element of REAL : ( not b₁ <= 0 & not PI / 4 <= b₁ ) } is set
{0,(PI / 4)} is non empty V46() V47() V48() set
].0,(PI / 4).[ \/ {0,(PI / 4)} is non empty V46() V47() V48() set
sec | [.0,(PI / 4).] is V19() V22( REAL ) V23( REAL ) Function-like V36() V37() V38() Element of K6(K7(REAL,REAL))
[.0,(PI / 4).] /\ (dom sec) is V46() V47() V48() set
g1 is V11() real ext-real Element of REAL
g1 is V11() real ext-real Element of REAL
[.(- (sqrt 2)),(- 1).] is closed V46() V47() V48() V70() Element of K6(REAL)
{ b₁ where b₁ is V11() real ext-real Element of REAL : ( - (sqrt 2) <= b₁ & b₁ <= - 1 ) } is set
x0 is set
sec . x0 is V11() real ext-real Element of REAL
(PI / 2) + (PI / 2) is non empty V11() real ext-real positive non negative Element of REAL
(PI / 4) + (PI / 2) is non empty V11() real ext-real positive non negative Element of REAL
].((3 / 4) * PI),PI.[ is open V46() V47() V48() V65() V66() V70() Element of K6(REAL)
{ b₁ where b₁ is V11() real ext-real Element of REAL : ( not b₁ <= (3 / 4) * PI & not PI <= b₁ ) } is set
{((3 / 4) * PI),PI} is non empty V46() V47() V48() set
].((3 / 4) * PI),PI.[ \/ {((3 / 4) * PI),PI} is non empty V46() V47() V48() set
(PI / 2) + (PI / 4) is non empty V11() real ext-real positive non negative Element of REAL
(PI / 4) + (PI / 4) is non empty V11() real ext-real positive non negative Element of REAL
sec | [.((3 / 4) * PI),PI.] is V19() V22( REAL ) V23( REAL ) Function-like V36() V37() V38() Element of K6(K7(REAL,REAL))
[.((3 / 4) * PI),PI.] /\ (dom sec) is V46() V47() V48() set
g1 is V11() real ext-real Element of REAL
g1 is V11() real ext-real Element of REAL
x0 is set
cosec . x0 is V11() real ext-real Element of REAL
].(- (PI / 2)),(- (PI / 4)).[ is open V46() V47() V48() V65() V66() V70() Element of K6(REAL)
{ b₁ where b₁ is V11() real ext-real Element of REAL : ( not b₁ <= - (PI / 2) & not - (PI / 4) <= b₁ ) } is set
{(- (PI / 2)),(- (PI / 4))} is non empty V46() V47() V48() set
].(- (PI / 2)),(- (PI / 4)).[ \/ {(- (PI / 2)),(- (PI / 4))} is non empty V46() V47() V48() set
cosec | [.(- (PI / 2)),(- (PI / 4)).] is V19() V22( REAL ) V23( REAL ) Function-like V36() V37() V38() Element of K6(K7(REAL,REAL))
[.(- (PI / 2)),(- (PI / 4)).] /\ (dom cosec) is V46() V47() V48() set
g1 is V11() real ext-real Element of REAL
g1 is V11() real ext-real Element of REAL
x0 is set
cosec . x0 is V11() real ext-real Element of REAL
].(PI / 4),(PI / 2).[ is open V46() V47() V48() V65() V66() V70() Element of K6(REAL)
{ b₁ where b₁ is V11() real ext-real Element of REAL : ( not b₁ <= PI / 4 & not PI / 2 <= b₁ ) } is set
{(PI / 4),(PI / 2)} is non empty V46() V47() V48() set
].(PI / 4),(PI / 2).[ \/ {(PI / 4),(PI / 2)} is non empty V46() V47() V48() set
cosec | [.(PI / 4),(PI / 2).] is V19() V22( REAL ) V23( REAL ) Function-like V36() V37() V38() Element of K6(K7(REAL,REAL))
[.(PI / 4),(PI / 2).] /\ (dom cosec) is V46() V47() V48() set
g1 is V11() real ext-real Element of REAL
g1 is V11() real ext-real Element of REAL
sec | [.0,(PI / 4).] is V19() V22( REAL ) V23( REAL ) Function-like V36() V37() V38() Element of K6(K7(REAL,REAL))
dom (sec | [.0,(PI / 4).]) is V46() V47() V48() Element of K6(REAL)
sec | [.((3 / 4) * PI),PI.] is V19() V22( REAL ) V23( REAL ) Function-like V36() V37() V38() Element of K6(K7(REAL,REAL))
dom (sec | [.((3 / 4) * PI),PI.]) is V46() V47() V48() Element of K6(REAL)
cosec | [.(- (PI / 2)),(- (PI / 4)).] is V19() V22( REAL ) V23( REAL ) Function-like V36() V37() V38() Element of K6(K7(REAL,REAL))
dom (cosec | [.(- (PI / 2)),(- (PI / 4)).]) is V46() V47() V48() Element of K6(REAL)
cosec | [.(PI / 4),(PI / 2).] is V19() V22( REAL ) V23( REAL ) Function-like V36() V37() V38() Element of K6(K7(REAL,REAL))
dom (cosec | [.(PI / 4),(PI / 2).]) is V46() V47() V48() Element of K6(REAL)
dom (sec | [.0,(PI / 2).[) is V46() V47() V48() Element of K6(REAL)
(dom sec) /\ [.0,(PI / 2).[ is V46() V47() V48() set
x0 is V11() real ext-real set
(sec | [.0,(PI / 2).[) . x0 is V11() real ext-real Element of REAL
sec . x0 is V11() real ext-real Element of REAL
dom (sec | ].(PI / 2),PI.]) is V46() V47() V48() Element of K6(REAL)
(dom sec) /\ ].(PI / 2),PI.] is V46() V47() V48() set
x0 is V11() real ext-real set
(sec | ].(PI / 2),PI.]) . x0 is V11() real ext-real Element of REAL
sec . x0 is V11() real ext-real Element of REAL
dom (cosec | [.(- (PI / 2)),0.[) is V46() V47() V48() Element of K6(REAL)
(dom cosec) /\ [.(- (PI / 2)),0.[ is V46() V47() V48() set
x0 is V11() real ext-real set
(cosec | [.(- (PI / 2)),0.[) . x0 is V11() real ext-real Element of REAL
cosec . x0 is V11() real ext-real Element of REAL
dom (cosec | ].0,(PI / 2).]) is V46() V47() V48() Element of K6(REAL)
(dom cosec) /\ ].0,(PI / 2).] is V46() V47() V48() set
x0 is V11() real ext-real set
(cosec | ].0,(PI / 2).]) . x0 is V11() real ext-real Element of REAL
cosec . x0 is V11() real ext-real Element of REAL
x0 is V11() real ext-real set
cos . x0 is V11() real ext-real Element of REAL
g1 is V19() V22( NAT ) V23( REAL ) Function-like quasi_total V36() V37() V38() Element of K6(K7(NAT,REAL))
rng g1 is V46() V47() V48() Element of K6(REAL)
lim g1 is V11() real ext-real Element of REAL
dom g1 is V46() V47() V48() V49() V50() V51() V67() Element of K6(NAT)
f is epsilon-transitive epsilon-connected ordinal natural V11() real ext-real V46() V47() V48() V49() V50() V51() V67() V71() Element of NAT
g1 . f is V11() real ext-real Element of REAL
(sec | [.0,(PI / 2).[) . (g1 . f) is V11() real ext-real Element of REAL
sec . (g1 . f) is V11() real ext-real Element of REAL
(sec | [.0,(PI / 2).[) /* g1 is V19() V22( NAT ) V23( REAL ) Function-like quasi_total V36() V37() V38() Element of K6(K7(NAT,REAL))
((sec | [.0,(PI / 2).[) /* g1) . f is V11() real ext-real Element of REAL
sec /* g1 is V19() V22( NAT ) V23( REAL ) Function-like quasi_total V36() V37() V38() Element of K6(K7(NAT,REAL))
(sec /* g1) . f is V11() real ext-real Element of REAL
sec . x0 is V11() real ext-real Element of REAL
lim (sec /* g1) is V11() real ext-real Element of REAL
(sec | [.0,(PI / 2).[) . x0 is V11() real ext-real Element of REAL
lim ((sec | [.0,(PI / 2).[) /* g1) is V11() real ext-real Element of REAL
x0 is V11() real ext-real set
cos . x0 is V11() real ext-real Element of REAL
g1 is V19() V22( NAT ) V23( REAL ) Function-like quasi_total V36() V37() V38() Element of K6(K7(NAT,REAL))
rng g1 is V46() V47() V48() Element of K6(REAL)
lim g1 is V11() real ext-real Element of REAL
dom g1 is V46() V47() V48() V49() V50() V51() V67() Element of K6(NAT)
f is epsilon-transitive epsilon-connected ordinal natural V11() real ext-real V46() V47() V48() V49() V50() V51() V67() V71() Element of NAT
g1 . f is V11() real ext-real Element of REAL
(sec | ].(PI / 2),PI.]) . (g1 . f) is V11() real ext-real Element of REAL
sec . (g1 . f) is V11() real ext-real Element of REAL
(sec | ].(PI / 2),PI.]) /* g1 is V19() V22( NAT ) V23( REAL ) Function-like quasi_total V36() V37() V38() Element of K6(K7(NAT,REAL))
((sec | ].(PI / 2),PI.]) /* g1) . f is V11() real ext-real Element of REAL
sec /* g1 is V19() V22( NAT ) V23( REAL ) Function-like quasi_total V36() V37() V38() Element of K6(K7(NAT,REAL))
(sec /* g1) . f is V11() real ext-real Element of REAL
sec . x0 is V11() real ext-real Element of REAL
lim (sec /* g1) is V11() real ext-real Element of REAL
(sec | ].(PI / 2),PI.]) . x0 is V11() real ext-real Element of REAL
lim ((sec | ].(PI / 2),PI.]) /* g1) is V11() real ext-real Element of REAL
x0 is V11() real ext-real set
0 + (2 * PI) is non empty V11() real ext-real positive non negative Element of REAL
x0 + (2 * PI) is V11() real ext-real Element of REAL
(- PI) + (2 * PI) is V11() real ext-real Element of REAL
sin . (x0 + (2 * PI)) is V11() real ext-real Element of REAL
sin . x0 is V11() real ext-real Element of REAL
g1 is V19() V22( NAT ) V23( REAL ) Function-like quasi_total V36() V37() V38() Element of K6(K7(NAT,REAL))
rng g1 is V46() V47() V48() Element of K6(REAL)
lim g1 is V11() real ext-real Element of REAL
dom g1 is V46() V47() V48() V49() V50() V51() V67() Element of K6(NAT)
f is epsilon-transitive epsilon-connected ordinal natural V11() real ext-real V46() V47() V48() V49() V50() V51() V67() V71() Element of NAT
g1 . f is V11() real ext-real Element of REAL
(cosec | [.(- (PI / 2)),0.[) . (g1 . f) is V11() real ext-real Element of REAL
cosec . (g1 . f) is V11() real ext-real Element of REAL
(cosec | [.(- (PI / 2)),0.[) /* g1 is V19() V22( NAT ) V23( REAL ) Function-like quasi_total V36() V37() V38() Element of K6(K7(NAT,REAL))
((cosec | [.(- (PI / 2)),0.[) /* g1) . f is V11() real ext-real Element of REAL
cosec /* g1 is V19() V22( NAT ) V23( REAL ) Function-like quasi_total V36() V37() V38() Element of K6(K7(NAT,REAL))
(cosec /* g1) . f is V11() real ext-real Element of REAL
cosec . x0 is V11() real ext-real Element of REAL
lim (cosec /* g1) is V11() real ext-real Element of REAL
(cosec | [.(- (PI / 2)),0.[) . x0 is V11() real ext-real Element of REAL
lim ((cosec | [.(- (PI / 2)),0.[) /* g1) is V11() real ext-real Element of REAL
x0 is V11() real ext-real set
sin . x0 is V11() real ext-real Element of REAL
g1 is V19() V22( NAT ) V23( REAL ) Function-like quasi_total V36() V37() V38() Element of K6(K7(NAT,REAL))
rng g1 is V46() V47() V48() Element of K6(REAL)
lim g1 is V11() real ext-real Element of REAL
dom g1 is V46() V47() V48() V49() V50() V51() V67() Element of K6(NAT)
f is epsilon-transitive epsilon-connected ordinal natural V11() real ext-real V46() V47() V48() V49() V50() V51() V67() V71() Element of NAT
g1 . f is V11() real ext-real Element of REAL
(cosec | ].0,(PI / 2).]) . (g1 . f) is V11() real ext-real Element of REAL
cosec . (g1 . f) is V11() real ext-real Element of REAL
(cosec | ].0,(PI / 2).]) /* g1 is V19() V22( NAT ) V23( REAL ) Function-like quasi_total V36() V37() V38() Element of K6(K7(NAT,REAL))
((cosec | ].0,(PI / 2).]) /* g1) . f is V11() real ext-real Element of REAL
cosec /* g1 is V19() V22( NAT ) V23( REAL ) Function-like quasi_total V36() V37() V38() Element of K6(K7(NAT,REAL))
(cosec /* g1) . f is V11() real ext-real Element of REAL
cosec . x0 is V11() real ext-real Element of REAL
lim (cosec /* g1) is V11() real ext-real Element of REAL
(cosec | ].0,(PI / 2).]) . x0 is V11() real ext-real Element of REAL
lim ((cosec | ].0,(PI / 2).]) /* g1) is V11() real ext-real Element of REAL
rng (sec | [.0,(PI / 4).]) is V46() V47() V48() Element of K6(REAL)
x0 is set
g1 is V11() real ext-real Element of REAL
[.(sec . 0),(sec . (PI / 4)).] is closed V46() V47() V48() V70() Element of K6(REAL)
{ b₁ where b₁ is V11() real ext-real Element of REAL : ( sec . 0 <= b₁ & b₁ <= sec . (PI / 4) ) } is set
[.(sec . (PI / 4)),(sec . 0).] is closed V46() V47() V48() V70() Element of K6(REAL)
{ b₁ where b₁ is V11() real ext-real Element of REAL : ( sec . (PI / 4) <= b₁ & b₁ <= sec . 0 ) } is set
[.(sec . 0),(sec . (PI / 4)).] \/ [.(sec . (PI / 4)),(sec . 0).] is V46() V47() V48() set
f is V11() real ext-real Element of REAL
sec . f is V11() real ext-real Element of REAL
(sec | [.0,(PI / 4).]) . f is V11() real ext-real Element of REAL
g1 is set
(sec | [.0,(PI / 4).]) . g1 is V11() real ext-real Element of REAL
f is V11() real ext-real Element of REAL
sec . f is V11() real ext-real Element of REAL
rng (sec | [.((3 / 4) * PI),PI.]) is V46() V47() V48() Element of K6(REAL)
x0 is set
g1 is V11() real ext-real Element of REAL
[.(sec . ((3 / 4) * PI)),(sec . PI).] is closed V46() V47() V48() V70() Element of K6(REAL)
{ b₁ where b₁ is V11() real ext-real Element of REAL : ( sec . ((3 / 4) * PI) <= b₁ & b₁ <= sec . PI ) } is set
[.(sec . PI),(sec . ((3 / 4) * PI)).] is closed V46() V47() V48() V70() Element of K6(REAL)
{ b₁ where b₁ is V11() real ext-real Element of REAL : ( sec . PI <= b₁ & b₁ <= sec . ((3 / 4) * PI) ) } is set
[.(sec . ((3 / 4) * PI)),(sec . PI).] \/ [.(sec . PI),(sec . ((3 / 4) * PI)).] is V46() V47() V48() set
f is V11() real ext-real Element of REAL
sec . f is V11() real ext-real Element of REAL
(sec | [.((3 / 4) * PI),PI.]) . f is V11() real ext-real Element of REAL
g1 is set
(sec | [.((3 / 4) * PI),PI.]) . g1 is V11() real ext-real Element of REAL
f is V11() real ext-real Element of REAL
sec . f is V11() real ext-real Element of REAL
rng (cosec | [.(- (PI / 2)),(- (PI / 4)).]) is V46() V47() V48() Element of K6(REAL)
x0 is set
g1 is V11() real ext-real Element of REAL
[.(cosec . (- (PI / 4))),(cosec . (- (PI / 2))).] is closed V46() V47() V48() V70() Element of K6(REAL)
{ b₁ where b₁ is V11() real ext-real Element of REAL : ( cosec . (- (PI / 4)) <= b₁ & b₁ <= cosec . (- (PI / 2)) ) } is set
[.(cosec . (- (PI / 2))),(cosec . (- (PI / 4))).] is closed V46() V47() V48() V70() Element of K6(REAL)
{ b₁ where b₁ is V11() real ext-real Element of REAL : ( cosec . (- (PI / 2)) <= b₁ & b₁ <= cosec . (- (PI / 4)) ) } is set
[.(cosec . (- (PI / 4))),(cosec . (- (PI / 2))).] \/ [.(cosec . (- (PI / 2))),(cosec . (- (PI / 4))).] is V46() V47() V48() set
f is V11() real ext-real Element of REAL
cosec . f is V11() real ext-real Element of REAL
(cosec | [.(- (PI / 2)),(- (PI / 4)).]) . f is V11() real ext-real Element of REAL
g1 is set
(cosec | [.(- (PI / 2)),(- (PI / 4)).]) . g1 is V11() real ext-real Element of REAL
f is V11() real ext-real Element of REAL
cosec . f is V11() real ext-real Element of REAL
rng (cosec | [.(PI / 4),(PI / 2).]) is V46() V47() V48() Element of K6(REAL)
x0 is set
g1 is V11() real ext-real Element of REAL
[.(cosec . (PI / 2)),(cosec . (PI / 4)).] is closed V46() V47() V48() V70() Element of K6(REAL)
{ b₁ where b₁ is V11() real ext-real Element of REAL : ( cosec . (PI / 2) <= b₁ & b₁ <= cosec . (PI / 4) ) } is set
[.(cosec . (PI / 4)),(cosec . (PI / 2)).] is closed V46() V47() V48() V70() Element of K6(REAL)
{ b₁ where b₁ is V11() real ext-real Element of REAL : ( cosec . (PI / 4) <= b₁ & b₁ <= cosec . (PI / 2) ) } is set
[.(cosec . (PI / 2)),(cosec . (PI / 4)).] \/ [.(cosec . (PI / 4)),(cosec . (PI / 2)).] is V46() V47() V48() set
f is V11() real ext-real Element of REAL
cosec . f is V11() real ext-real Element of REAL
(cosec | [.(PI / 4),(PI / 2).]) . f is V11() real ext-real Element of REAL
g1 is set
(cosec | [.(PI / 4),(PI / 2).]) . g1 is V11() real ext-real Element of REAL
f is V11() real ext-real Element of REAL
cosec . f is V11() real ext-real Element of REAL
dom () is V46() V47() V48() Element of K6(REAL)
rng (sec | [.0,(PI / 2).[) is V46() V47() V48() Element of K6(REAL)
x0 is set
sec .: [.0,(PI / 4).] is V46() V47() V48() Element of K6(REAL)
sec .: [.0,(PI / 2).[ is V46() V47() V48() Element of K6(REAL)
g1 is set
sec . g1 is V11() real ext-real Element of REAL
dom () is V46() V47() V48() Element of K6(REAL)
rng (sec | ].(PI / 2),PI.]) is V46() V47() V48() Element of K6(REAL)
x0 is set
sec .: [.((3 / 4) * PI),PI.] is V46() V47() V48() Element of K6(REAL)
sec .: ].(PI / 2),PI.] is V46() V47() V48() Element of K6(REAL)
g1 is set
sec . g1 is V11() real ext-real Element of REAL
dom () is V46() V47() V48() Element of K6(REAL)
rng (cosec | [.(- (PI / 2)),0.[) is V46() V47() V48() Element of K6(REAL)
x0 is set
cosec .: [.(- (PI / 2)),(- (PI / 4)).] is V46() V47() V48() Element of K6(REAL)
cosec .: [.(- (PI / 2)),0.[ is V46() V47() V48() Element of K6(REAL)
g1 is set
cosec . g1 is V11() real ext-real Element of REAL
dom () is V46() V47() V48() Element of K6(REAL)
rng (cosec | ].0,(PI / 2).]) is V46() V47() V48() Element of K6(REAL)
x0 is set
cosec .: [.(PI / 4),(PI / 2).] is V46() V47() V48() Element of K6(REAL)
cosec .: ].0,(PI / 2).] is V46() V47() V48() Element of K6(REAL)
g1 is set
cosec . g1 is V11() real ext-real Element of REAL
(sec | [.0,(PI / 4).]) | [.0,(PI / 4).] is V19() V22( REAL ) V23( REAL ) Function-like V36() V37() V38() Element of K6(K7(REAL,REAL))
(sec | [.((3 / 4) * PI),PI.]) | [.((3 / 4) * PI),PI.] is V19() V22( REAL ) V23( REAL ) Function-like V36() V37() V38() Element of K6(K7(REAL,REAL))
(cosec | [.(- (PI / 2)),(- (PI / 4)).]) | [.(- (PI / 2)),(- (PI / 4)).] is V19() V22( REAL ) V23( REAL ) Function-like V36() V37() V38() Element of K6(K7(REAL,REAL))
(cosec | [.(PI / 4),(PI / 2).]) | [.(PI / 4),(PI / 2).] is V19() V22( REAL ) V23( REAL ) Function-like V36() V37() V38() Element of K6(K7(REAL,REAL))
(sec | [.0,(PI / 2).[) | [.0,(PI / 4).] is V19() V22( REAL ) V23( REAL ) Function-like one-to-one V36() V37() V38() Element of K6(K7(REAL,REAL))
(sec | ].(PI / 2),PI.]) | [.((3 / 4) * PI),PI.] is V19() V22( REAL ) V23( REAL ) Function-like one-to-one V36() V37() V38() Element of K6(K7(REAL,REAL))
(cosec | [.(- (PI / 2)),0.[) | [.(- (PI / 2)),(- (PI / 4)).] is V19() V22( REAL ) V23( REAL ) Function-like one-to-one V36() V37() V38() Element of K6(K7(REAL,REAL))
(cosec | ].0,(PI / 2).]) | [.(PI / 4),(PI / 2).] is V19() V22( REAL ) V23( REAL ) Function-like one-to-one V36() V37() V38() Element of K6(K7(REAL,REAL))
() | [.1,(sqrt 2).] is V19() V22( REAL ) V23( REAL ) Function-like one-to-one V36() V37() V38() Element of K6(K7(REAL,REAL))
(sec | [.0,(PI / 4).]) " is V19() V22( REAL ) V23( REAL ) Function-like one-to-one V36() V37() V38() Element of K6(K7(REAL,REAL))
(sec | [.0,(PI / 2).[) | [.0,(PI / 4).] is V19() V22( REAL ) V23( REAL ) Function-like one-to-one V36() V37() V38() Element of K6(K7(REAL,REAL))
((sec | [.0,(PI / 2).[) | [.0,(PI / 4).]) " is V19() V22( REAL ) V23( REAL ) Function-like one-to-one V36() V37() V38() Element of K6(K7(REAL,REAL))
(sec | [.0,(PI / 2).[) .: [.0,(PI / 4).] is V46() V47() V48() Element of K6(REAL)
((sec | [.0,(PI / 2).[) ") | ((sec | [.0,(PI / 2).[) .: [.0,(PI / 4).]) is V19() V22( REAL ) V23( REAL ) Function-like one-to-one V36() V37() V38() Element of K6(K7(REAL,REAL))
rng ((sec | [.0,(PI / 2).[) | [.0,(PI / 4).]) is V46() V47() V48() Element of K6(REAL)
((sec | [.0,(PI / 2).[) ") | (rng ((sec | [.0,(PI / 2).[) | [.0,(PI / 4).])) is V19() V22( REAL ) V23( REAL ) Function-like one-to-one V36() V37() V38() Element of K6(K7(REAL,REAL))
((sec | [.0,(PI / 2).[) ") | [.1,(sqrt 2).] is V19() V22( REAL ) V23( REAL ) Function-like one-to-one V36() V37() V38() Element of K6(K7(REAL,REAL))
() | [.(- (sqrt 2)),(- 1).] is V19() V22( REAL ) V23( REAL ) Function-like one-to-one V36() V37() V38() Element of K6(K7(REAL,REAL))
(sec | [.((3 / 4) * PI),PI.]) " is V19() V22( REAL ) V23( REAL ) Function-like one-to-one V36() V37() V38() Element of K6(K7(REAL,REAL))
(sec | ].(PI / 2),PI.]) | [.((3 / 4) * PI),PI.] is V19() V22( REAL ) V23( REAL ) Function-like one-to-one V36() V37() V38() Element of K6(K7(REAL,REAL))
((sec | ].(PI / 2),PI.]) | [.((3 / 4) * PI),PI.]) " is V19() V22( REAL ) V23( REAL ) Function-like one-to-one V36() V37() V38() Element of K6(K7(REAL,REAL))
(sec | ].(PI / 2),PI.]) .: [.((3 / 4) * PI),PI.] is V46() V47() V48() Element of K6(REAL)
((sec | ].(PI / 2),PI.]) ") | ((sec | ].(PI / 2),PI.]) .: [.((3 / 4) * PI),PI.]) is V19() V22( REAL ) V23( REAL ) Function-like one-to-one V36() V37() V38() Element of K6(K7(REAL,REAL))
rng ((sec | ].(PI / 2),PI.]) | [.((3 / 4) * PI),PI.]) is V46() V47() V48() Element of K6(REAL)
((sec | ].(PI / 2),PI.]) ") | (rng ((sec | ].(PI / 2),PI.]) | [.((3 / 4) * PI),PI.])) is V19() V22( REAL ) V23( REAL ) Function-like one-to-one V36() V37() V38() Element of K6(K7(REAL,REAL))
((sec | ].(PI / 2),PI.]) ") | [.(- (sqrt 2)),(- 1).] is V19() V22( REAL ) V23( REAL ) Function-like one-to-one V36() V37() V38() Element of K6(K7(REAL,REAL))
() | [.(- (sqrt 2)),(- 1).] is V19() V22( REAL ) V23( REAL ) Function-like one-to-one V36() V37() V38() Element of K6(K7(REAL,REAL))
(cosec | [.(- (PI / 2)),(- (PI / 4)).]) " is V19() V22( REAL ) V23( REAL ) Function-like one-to-one V36() V37() V38() Element of K6(K7(REAL,REAL))
(cosec | [.(- (PI / 2)),0.[) | [.(- (PI / 2)),(- (PI / 4)).] is V19() V22( REAL ) V23( REAL ) Function-like one-to-one V36() V37() V38() Element of K6(K7(REAL,REAL))
((cosec | [.(- (PI / 2)),0.[) | [.(- (PI / 2)),(- (PI / 4)).]) " is V19() V22( REAL ) V23( REAL ) Function-like one-to-one V36() V37() V38() Element of K6(K7(REAL,REAL))
(cosec | [.(- (PI / 2)),0.[) .: [.(- (PI / 2)),(- (PI / 4)).] is V46() V47() V48() Element of K6(REAL)
((cosec | [.(- (PI / 2)),0.[) ") | ((cosec | [.(- (PI / 2)),0.[) .: [.(- (PI / 2)),(- (PI / 4)).]) is V19() V22( REAL ) V23( REAL ) Function-like one-to-one V36() V37() V38() Element of K6(K7(REAL,REAL))
rng ((cosec | [.(- (PI / 2)),0.[) | [.(- (PI / 2)),(- (PI / 4)).]) is V46() V47() V48() Element of K6(REAL)
((cosec | [.(- (PI / 2)),0.[) ") | (rng ((cosec | [.(- (PI / 2)),0.[) | [.(- (PI / 2)),(- (PI / 4)).])) is V19() V22( REAL ) V23( REAL ) Function-like one-to-one V36() V37() V38() Element of K6(K7(REAL,REAL))
((cosec | [.(- (PI / 2)),0.[) ") | [.(- (sqrt 2)),(- 1).] is V19() V22( REAL ) V23( REAL ) Function-like one-to-one V36() V37() V38() Element of K6(K7(REAL,REAL))
() | [.1,(sqrt 2).] is V19() V22( REAL ) V23( REAL ) Function-like one-to-one V36() V37() V38() Element of K6(K7(REAL,REAL))
(cosec | [.(PI / 4),(PI / 2).]) " is V19() V22( REAL ) V23( REAL ) Function-like one-to-one V36() V37() V38() Element of K6(K7(REAL,REAL))
(cosec | ].0,(PI / 2).]) | [.(PI / 4),(PI / 2).] is V19() V22( REAL ) V23( REAL ) Function-like one-to-one V36() V37() V38() Element of K6(K7(REAL,REAL))
((cosec | ].0,(PI / 2).]) | [.(PI / 4),(PI / 2).]) " is V19() V22( REAL ) V23( REAL ) Function-like one-to-one V36() V37() V38() Element of K6(K7(REAL,REAL))
(cosec | ].0,(PI / 2).]) .: [.(PI / 4),(PI / 2).] is V46() V47() V48() Element of K6(REAL)
((cosec | ].0,(PI / 2).]) ") | ((cosec | ].0,(PI / 2).]) .: [.(PI / 4),(PI / 2).]) is V19() V22( REAL ) V23( REAL ) Function-like one-to-one V36() V37() V38() Element of K6(K7(REAL,REAL))
rng ((cosec | ].0,(PI / 2).]) | [.(PI / 4),(PI / 2).]) is V46() V47() V48() Element of K6(REAL)
((cosec | ].0,(PI / 2).]) ") | (rng ((cosec | ].0,(PI / 2).]) | [.(PI / 4),(PI / 2).])) is V19() V22( REAL ) V23( REAL ) Function-like one-to-one V36() V37() V38() Element of K6(K7(REAL,REAL))
((cosec | ].0,(PI / 2).]) ") | [.1,(sqrt 2).] is V19() V22( REAL ) V23( REAL ) Function-like one-to-one V36() V37() V38() Element of K6(K7(REAL,REAL))
(sec | [.0,(PI / 4).]) * (() | [.1,(sqrt 2).]) is V19() Function-like one-to-one V36() V37() V38() set
id [.1,(sqrt 2).] is V19() V22( REAL ) V23( REAL ) Function-like one-to-one V36() V37() V38() Element of K6(K7(REAL,REAL))
(sec | [.((3 / 4) * PI),PI.]) * (() | [.(- (sqrt 2)),(- 1).]) is V19() Function-like one-to-one V36() V37() V38() set
id [.(- (sqrt 2)),(- 1).] is V19() V22( REAL ) V23( REAL ) Function-like one-to-one V36() V37() V38() Element of K6(K7(REAL,REAL))
(cosec | [.(- (PI / 2)),(- (PI / 4)).]) * (() | [.(- (sqrt 2)),(- 1).]) is V19() Function-like one-to-one V36() V37() V38() set
(cosec | [.(PI / 4),(PI / 2).]) * (() | [.1,(sqrt 2).]) is V19() Function-like one-to-one V36() V37() V38() set
(sec | [.0,(PI / 4).]) * (() | [.1,(sqrt 2).]) is V19() V22( REAL ) V23( REAL ) Function-like one-to-one V36() V37() V38() Element of K6(K7(REAL,REAL))
(sec | [.((3 / 4) * PI),PI.]) * (() | [.(- (sqrt 2)),(- 1).]) is V19() V22( REAL ) V23( REAL ) Function-like one-to-one V36() V37() V38() Element of K6(K7(REAL,REAL))
(cosec | [.(- (PI / 2)),(- (PI / 4)).]) * (() | [.(- (sqrt 2)),(- 1).]) is V19() V22( REAL ) V23( REAL ) Function-like one-to-one V36() V37() V38() Element of K6(K7(REAL,REAL))
(cosec | [.(PI / 4),(PI / 2).]) * (() | [.1,(sqrt 2).]) is V19() V22( REAL ) V23( REAL ) Function-like one-to-one V36() V37() V38() Element of K6(K7(REAL,REAL))
() * (sec | [.0,(PI / 2).[) is V19() Function-like one-to-one V36() V37() V38() set
id [.0,(PI / 2).[ is V19() V22( REAL ) V23( REAL ) Function-like one-to-one V36() V37() V38() Element of K6(K7(REAL,REAL))
() * (sec | ].(PI / 2),PI.]) is V19() Function-like one-to-one V36() V37() V38() set
id ].(PI / 2),PI.] is V19() V22( REAL ) V23( REAL ) Function-like one-to-one V36() V37() V38() Element of K6(K7(REAL,REAL))
() * (cosec | [.(- (PI / 2)),0.[) is V19() Function-like one-to-one V36() V37() V38() set
id [.(- (PI / 2)),0.[ is V19() V22( REAL ) V23( REAL ) Function-like one-to-one V36() V37() V38() Element of K6(K7(REAL,REAL))
() * (cosec | ].0,(PI / 2).]) is V19() Function-like one-to-one V36() V37() V38() set
id ].0,(PI / 2).] is V19() V22( REAL ) V23( REAL ) Function-like one-to-one V36() V37() V38() Element of K6(K7(REAL,REAL))
() * (sec | [.0,(PI / 2).[) is V19() V22( REAL ) V23( REAL ) Function-like one-to-one V36() V37() V38() Element of K6(K7(REAL,REAL))
() * (sec | ].(PI / 2),PI.]) is V19() V22( REAL ) V23( REAL ) Function-like one-to-one V36() V37() V38() Element of K6(K7(REAL,REAL))
() * (cosec | [.(- (PI / 2)),0.[) is V19() V22( REAL ) V23( REAL ) Function-like one-to-one V36() V37() V38() Element of K6(K7(REAL,REAL))
() * (cosec | ].0,(PI / 2).]) is V19() V22( REAL ) V23( REAL ) Function-like one-to-one V36() V37() V38() Element of K6(K7(REAL,REAL))
x0 is V11() real ext-real Element of REAL
sec . x0 is V11() real ext-real Element of REAL
((sec . x0)) is V11() real ext-real Element of REAL
() . (sec . x0) is V11() real ext-real Element of REAL
(sec | [.0,(PI / 2).[) . x0 is V11() real ext-real Element of REAL
() . ((sec | [.0,(PI / 2).[) . x0) is V11() real ext-real Element of REAL
(id [.0,(PI / 2).[) . x0 is V11() real ext-real Element of REAL
x0 is V11() real ext-real Element of REAL
sec . x0 is V11() real ext-real Element of REAL
((sec . x0)) is V11() real ext-real Element of REAL
() . (sec . x0) is V11() real ext-real Element of REAL
(sec | ].(PI / 2),PI.]) . x0 is V11() real ext-real Element of REAL
() . ((sec | ].(PI / 2),PI.]) . x0) is V11() real ext-real Element of REAL
(id ].(PI / 2),PI.]) . x0 is V11() real ext-real Element of REAL
x0 is V11() real ext-real Element of REAL
cosec . x0 is V11() real ext-real Element of REAL
((cosec . x0)) is V11() real ext-real Element of REAL
() . (cosec . x0) is V11() real ext-real Element of REAL
(cosec | [.(- (PI / 2)),0.[) . x0 is V11() real ext-real Element of REAL
() . ((cosec | [.(- (PI / 2)),0.[) . x0) is V11() real ext-real Element of REAL
(id [.(- (PI / 2)),0.[) . x0 is V11() real ext-real Element of REAL
x0 is V11() real ext-real Element of REAL
cosec . x0 is V11() real ext-real Element of REAL
((cosec . x0)) is V11() real ext-real Element of REAL
() . (cosec . x0) is V11() real ext-real Element of REAL
(cosec | ].0,(PI / 2).]) . x0 is V11() real ext-real Element of REAL
() . ((cosec | ].0,(PI / 2).]) . x0) is V11() real ext-real Element of REAL
(id ].0,(PI / 2).]) . x0 is V11() real ext-real Element of REAL
() . 1 is V11() real ext-real Element of REAL
() . (sqrt 2) is V11() real ext-real Element of REAL
(1) is V11() real ext-real Element of REAL
((sqrt 2)) is V11() real ext-real Element of REAL
() . (- (sqrt 2)) is V11() real ext-real Element of REAL
() . (- 1) is V11() real ext-real Element of REAL
((- 1)) is V11() real ext-real Element of REAL
((- (sqrt 2))) is V11() real ext-real Element of REAL
() . (- 1) is V11() real ext-real Element of REAL
() . (- (sqrt 2)) is V11() real ext-real Element of REAL
((- 1)) is V11() real ext-real Element of REAL
((- (sqrt 2))) is V11() real ext-real Element of REAL
() . (sqrt 2) is V11() real ext-real Element of REAL
() . 1 is V11() real ext-real Element of REAL
(1) is V11() real ext-real Element of REAL
((sqrt 2)) is V11() real ext-real Element of REAL
sec .: [.0,(PI / 2).[ is V46() V47() V48() Element of K6(REAL)
() | (sec .: [.0,(PI / 2).[) is V19() V22( REAL ) V23( REAL ) Function-like one-to-one V36() V37() V38() Element of K6(K7(REAL,REAL))
(sec | [.0,(PI / 2).[) .: [.0,(PI / 2).[ is V46() V47() V48() Element of K6(REAL)
(sec | [.0,(PI / 2).[) | [.0,(PI / 2).[ is V19() V22( REAL ) V23( REAL ) Function-like one-to-one V36() V37() V38() Element of K6(K7(REAL,REAL))
rng ((sec | [.0,(PI / 2).[) | [.0,(PI / 2).[) is V46() V47() V48() Element of K6(REAL)
rng (sec | [.0,(PI / 2).[) is V46() V47() V48() Element of K6(REAL)
sec .: ].(PI / 2),PI.] is V46() V47() V48() Element of K6(REAL)
() | (sec .: ].(PI / 2),PI.]) is V19() V22( REAL ) V23( REAL ) Function-like one-to-one V36() V37() V38() Element of K6(K7(REAL,REAL))
(sec | ].(PI / 2),PI.]) .: ].(PI / 2),PI.] is V46() V47() V48() Element of K6(REAL)
(sec | ].(PI / 2),PI.]) | ].(PI / 2),PI.] is V19() V22( REAL ) V23( REAL ) Function-like one-to-one V36() V37() V38() Element of K6(K7(REAL,REAL))
rng ((sec | ].(PI / 2),PI.]) | ].(PI / 2),PI.]) is V46() V47() V48() Element of K6(REAL)
rng (sec | ].(PI / 2),PI.]) is V46() V47() V48() Element of K6(REAL)
cosec .: [.(- (PI / 2)),0.[ is V46() V47() V48() Element of K6(REAL)
() | (cosec .: [.(- (PI / 2)),0.[) is V19() V22( REAL ) V23( REAL ) Function-like one-to-one V36() V37() V38() Element of K6(K7(REAL,REAL))
(cosec | [.(- (PI / 2)),0.[) .: [.(- (PI / 2)),0.[ is V46() V47() V48() Element of K6(REAL)
(cosec | [.(- (PI / 2)),0.[) | [.(- (PI / 2)),0.[ is V19() V22( REAL ) V23( REAL ) Function-like one-to-one V36() V37() V38() Element of K6(K7(REAL,REAL))
rng ((cosec | [.(- (PI / 2)),0.[) | [.(- (PI / 2)),0.[) is V46() V47() V48() Element of K6(REAL)
rng (cosec | [.(- (PI / 2)),0.[) is V46() V47() V48() Element of K6(REAL)
cosec .: ].0,(PI / 2).] is V46() V47() V48() Element of K6(REAL)
() | (cosec .: ].0,(PI / 2).]) is V19() V22( REAL ) V23( REAL ) Function-like one-to-one V36() V37() V38() Element of K6(K7(REAL,REAL))
(cosec | ].0,(PI / 2).]) .: ].0,(PI / 2).] is V46() V47() V48() Element of K6(REAL)
(cosec | ].0,(PI / 2).]) | ].0,(PI / 2).] is V19() V22( REAL ) V23( REAL ) Function-like one-to-one V36() V37() V38() Element of K6(K7(REAL,REAL))
rng ((cosec | ].0,(PI / 2).]) | ].0,(PI / 2).]) is V46() V47() V48() Element of K6(REAL)
rng (cosec | ].0,(PI / 2).]) is V46() V47() V48() Element of K6(REAL)
sec .: [.0,(PI / 4).] is V46() V47() V48() Element of K6(REAL)
sec .: [.((3 / 4) * PI),PI.] is V46() V47() V48() Element of K6(REAL)
cosec .: [.(- (PI / 2)),(- (PI / 4)).] is V46() V47() V48() Element of K6(REAL)
cosec .: [.(PI / 4),(PI / 2).] is V46() V47() V48() Element of K6(REAL)
x0 is set
() . x0 is V11() real ext-real Element of REAL
].1,(sqrt 2).[ is open V46() V47() V48() V65() V66() V70() Element of K6(REAL)
{ b₁ where b₁ is V11() real ext-real Element of REAL : ( not b₁ <= 1 & not sqrt 2 <= b₁ ) } is set
{1,(sqrt 2)} is non empty V46() V47() V48() set
].1,(sqrt 2).[ \/ {1,(sqrt 2)} is non empty V46() V47() V48() set
[.1,(sqrt 2).] /\ (dom ()) is V46() V47() V48() set
g1 is V11() real ext-real Element of REAL
g1 is V11() real ext-real Element of REAL
x0 is set
() . x0 is V11() real ext-real Element of REAL
].(- (sqrt 2)),(- 1).[ is open V46() V47() V48() V65() V66() V70() Element of K6(REAL)
{ b₁ where b₁ is V11() real ext-real Element of REAL : ( not b₁ <= - (sqrt 2) & not - 1 <= b₁ ) } is set
{(- (sqrt 2)),(- 1)} is non empty V46() V47() V48() set
].(- (sqrt 2)),(- 1).[ \/ {(- (sqrt 2)),(- 1)} is non empty V46() V47() V48() set
[.(- (sqrt 2)),(- 1).] /\ (dom ()) is V46() V47() V48() set
g1 is V11() real ext-real Element of REAL
g1 is V11() real ext-real Element of REAL
x0 is set
() . x0 is V11() real ext-real Element of REAL
].(- (sqrt 2)),(- 1).[ is open V46() V47() V48() V65() V66() V70() Element of K6(REAL)
{ b₁ where b₁ is V11() real ext-real Element of REAL : ( not b₁ <= - (sqrt 2) & not - 1 <= b₁ ) } is set
{(- (sqrt 2)),(- 1)} is non empty V46() V47() V48() set
].(- (sqrt 2)),(- 1).[ \/ {(- (sqrt 2)),(- 1)} is non empty V46() V47() V48() set
[.(- (sqrt 2)),(- 1).] /\ (dom ()) is V46() V47() V48() set
g1 is V11() real ext-real Element of REAL
g1 is V11() real ext-real Element of REAL
x0 is set
() . x0 is V11() real ext-real Element of REAL
].1,(sqrt 2).[ is open V46() V47() V48() V65() V66() V70() Element of K6(REAL)
{ b₁ where b₁ is V11() real ext-real Element of REAL : ( not b₁ <= 1 & not sqrt 2 <= b₁ ) } is set
{1,(sqrt 2)} is non empty V46() V47() V48() set
].1,(sqrt 2).[ \/ {1,(sqrt 2)} is non empty V46() V47() V48() set
[.1,(sqrt 2).] /\ (dom ()) is V46() V47() V48() set
g1 is V11() real ext-real Element of REAL
g1 is V11() real ext-real Element of REAL
x0 is V11() real ext-real Element of REAL
(x0) is V11() real ext-real Element of REAL
() . x0 is V11() real ext-real Element of REAL
sec . (x0) is V11() real ext-real Element of REAL
dom (() | [.1,(sqrt 2).]) is V46() V47() V48() Element of K6(REAL)
(sec | [.0,(PI / 4).]) . (() . x0) is V11() real ext-real set
(() | [.1,(sqrt 2).]) . x0 is V11() real ext-real Element of REAL
(sec | [.0,(PI / 4).]) . ((() | [.1,(sqrt 2).]) . x0) is V11() real ext-real set
((sec | [.0,(PI / 4).]) * (() | [.1,(sqrt 2).])) . x0 is V11() real ext-real Element of REAL
(id [.1,(sqrt 2).]) . x0 is V11() real ext-real Element of REAL
x0 is V11() real ext-real Element of REAL
(x0) is V11() real ext-real Element of REAL
() . x0 is V11() real ext-real Element of REAL
sec . (x0) is V11() real ext-real Element of REAL
dom (() | [.(- (sqrt 2)),(- 1).]) is V46() V47() V48() Element of K6(REAL)
(sec | [.((3 / 4) * PI),PI.]) . (() . x0) is V11() real ext-real set
(() | [.(- (sqrt 2)),(- 1).]) . x0 is V11() real ext-real Element of REAL
(sec | [.((3 / 4) * PI),PI.]) . ((() | [.(- (sqrt 2)),(- 1).]) . x0) is V11() real ext-real set
((sec | [.((3 / 4) * PI),PI.]) * (() | [.(- (sqrt 2)),(- 1).])) . x0 is V11() real ext-real Element of REAL
(id [.(- (sqrt 2)),(- 1).]) . x0 is V11() real ext-real Element of REAL
x0 is V11() real ext-real Element of REAL
(x0) is V11() real ext-real Element of REAL
() . x0 is V11() real ext-real Element of REAL
cosec . (x0) is V11() real ext-real Element of REAL
dom (() | [.(- (sqrt 2)),(- 1).]) is V46() V47() V48() Element of K6(REAL)
(cosec | [.(- (PI / 2)),(- (PI / 4)).]) . (() . x0) is V11() real ext-real set
(() | [.(- (sqrt 2)),(- 1).]) . x0 is V11() real ext-real Element of REAL
(cosec | [.(- (PI / 2)),(- (PI / 4)).]) . ((() | [.(- (sqrt 2)),(- 1).]) . x0) is V11() real ext-real set
((cosec | [.(- (PI / 2)),(- (PI / 4)).]) * (() | [.(- (sqrt 2)),(- 1).])) . x0 is V11() real ext-real Element of REAL
(id [.(- (sqrt 2)),(- 1).]) . x0 is V11() real ext-real Element of REAL
x0 is V11() real ext-real Element of REAL
(x0) is V11() real ext-real Element of REAL
() . x0 is V11() real ext-real Element of REAL
cosec . (x0) is V11() real ext-real Element of REAL
dom (() | [.1,(sqrt 2).]) is V46() V47() V48() Element of K6(REAL)
(cosec | [.(PI / 4),(PI / 2).]) . (() . x0) is V11() real ext-real set
(() | [.1,(sqrt 2).]) . x0 is V11() real ext-real Element of REAL
(cosec | [.(PI / 4),(PI / 2).]) . ((() | [.1,(sqrt 2).]) . x0) is V11() real ext-real set
((cosec | [.(PI / 4),(PI / 2).]) * (() | [.1,(sqrt 2).])) . x0 is V11() real ext-real Element of REAL
(id [.1,(sqrt 2).]) . x0 is V11() real ext-real Element of REAL
((sec | [.0,(PI / 4).]) | [.0,(PI / 4).]) " is V19() V22( REAL ) V23( REAL ) Function-like one-to-one V36() V37() V38() Element of K6(K7(REAL,REAL))
(sec | [.0,(PI / 4).]) .: [.0,(PI / 4).] is V46() V47() V48() Element of K6(REAL)
(((sec | [.0,(PI / 4).]) | [.0,(PI / 4).]) ") | ((sec | [.0,(PI / 4).]) .: [.0,(PI / 4).]) is V19() V22( REAL ) V23( REAL ) Function-like one-to-one V36() V37() V38() Element of K6(K7(REAL,REAL))
(() | [.1,(sqrt 2).]) | [.1,(sqrt 2).] is V19() V22( REAL ) V23( REAL ) Function-like one-to-one V36() V37() V38() Element of K6(K7(REAL,REAL))
((sec | [.((3 / 4) * PI),PI.]) | [.((3 / 4) * PI),PI.]) " is V19() V22( REAL ) V23( REAL ) Function-like one-to-one V36() V37() V38() Element of K6(K7(REAL,REAL))
(sec | [.((3 / 4) * PI),PI.]) .: [.((3 / 4) * PI),PI.] is V46() V47() V48() Element of K6(REAL)
(((sec | [.((3 / 4) * PI),PI.]) | [.((3 / 4) * PI),PI.]) ") | ((sec | [.((3 / 4) * PI),PI.]) .: [.((3 / 4) * PI),PI.]) is V19() V22( REAL ) V23( REAL ) Function-like one-to-one V36() V37() V38() Element of K6(K7(REAL,REAL))
(() | [.(- (sqrt 2)),(- 1).]) | [.(- (sqrt 2)),(- 1).] is V19() V22( REAL ) V23( REAL ) Function-like one-to-one V36() V37() V38() Element of K6(K7(REAL,REAL))
((cosec | [.(- (PI / 2)),(- (PI / 4)).]) | [.(- (PI / 2)),(- (PI / 4)).]) " is V19() V22( REAL ) V23( REAL ) Function-like one-to-one V36() V37() V38() Element of K6(K7(REAL,REAL))
(cosec | [.(- (PI / 2)),(- (PI / 4)).]) .: [.(- (PI / 2)),(- (PI / 4)).] is V46() V47() V48() Element of K6(REAL)
(((cosec | [.(- (PI / 2)),(- (PI / 4)).]) | [.(- (PI / 2)),(- (PI / 4)).]) ") | ((cosec | [.(- (PI / 2)),(- (PI / 4)).]) .: [.(- (PI / 2)),(- (PI / 4)).]) is V19() V22( REAL ) V23( REAL ) Function-like one-to-one V36() V37() V38() Element of K6(K7(REAL,REAL))
(() | [.(- (sqrt 2)),(- 1).]) | [.(- (sqrt 2)),(- 1).] is V19() V22( REAL ) V23( REAL ) Function-like one-to-one V36() V37() V38() Element of K6(K7(REAL,REAL))
((cosec | [.(PI / 4),(PI / 2).]) | [.(PI / 4),(PI / 2).]) " is V19() V22( REAL ) V23( REAL ) Function-like one-to-one V36() V37() V38() Element of K6(K7(REAL,REAL))
(cosec | [.(PI / 4),(PI / 2).]) .: [.(PI / 4),(PI / 2).] is V46() V47() V48() Element of K6(REAL)
(((cosec | [.(PI / 4),(PI / 2).]) | [.(PI / 4),(PI / 2).]) ") | ((cosec | [.(PI / 4),(PI / 2).]) .: [.(PI / 4),(PI / 2).]) is V19() V22( REAL ) V23( REAL ) Function-like one-to-one V36() V37() V38() Element of K6(K7(REAL,REAL))
(() | [.1,(sqrt 2).]) | [.1,(sqrt 2).] is V19() V22( REAL ) V23( REAL ) Function-like one-to-one V36() V37() V38() Element of K6(K7(REAL,REAL))
rng (() | [.1,(sqrt 2).]) is V46() V47() V48() Element of K6(REAL)
x0 is set
dom (() | [.1,(sqrt 2).]) is V46() V47() V48() Element of K6(REAL)
g1 is V11() real ext-real Element of REAL
[.(() . 1),(() . (sqrt 2)).] is closed V46() V47() V48() V70() Element of K6(REAL)
{ b₁ where b₁ is V11() real ext-real Element of REAL : ( () . 1 <= b₁ & b₁ <= () . (sqrt 2) ) } is set
[.(() . (sqrt 2)),(() . 1).] is closed V46() V47() V48() V70() Element of K6(REAL)
{ b₁ where b₁ is V11() real ext-real Element of REAL : ( () . (sqrt 2) <= b₁ & b₁ <= () . 1 ) } is set
[.(() . 1),(() . (sqrt 2)).] \/ [.(() . (sqrt 2)),(() . 1).] is V46() V47() V48() set
f is V11() real ext-real Element of REAL
() . f is V11() real ext-real Element of REAL
(() | [.1,(sqrt 2).]) . f is V11() real ext-real Element of REAL
g1 is set
(() | [.1,(sqrt 2).]) . g1 is V11() real ext-real Element of REAL
() . g1 is V11() real ext-real Element of REAL
rng (() | [.(- (sqrt 2)),(- 1).]) is V46() V47() V48() Element of K6(REAL)
x0 is set
dom (() | [.(- (sqrt 2)),(- 1).]) is V46() V47() V48() Element of K6(REAL)
g1 is V11() real ext-real Element of REAL
[.(() . (- (sqrt 2))),(() . (- 1)).] is closed V46() V47() V48() V70() Element of K6(REAL)
{ b₁ where b₁ is V11() real ext-real Element of REAL : ( () . (- (sqrt 2)) <= b₁ & b₁ <= () . (- 1) ) } is set
[.(() . (- 1)),(() . (- (sqrt 2))).] is closed V46() V47() V48() V70() Element of K6(REAL)
{ b₁ where b₁ is V11() real ext-real Element of REAL : ( () . (- 1) <= b₁ & b₁ <= () . (- (sqrt 2)) ) } is set
[.(() . (- (sqrt 2))),(() . (- 1)).] \/ [.(() . (- 1)),(() . (- (sqrt 2))).] is V46() V47() V48() set
f is V11() real ext-real Element of REAL
() . f is V11() real ext-real Element of REAL
(() | [.(- (sqrt 2)),(- 1).]) . f is V11() real ext-real Element of REAL
g1 is set
(() | [.(- (sqrt 2)),(- 1).]) . g1 is V11() real ext-real Element of REAL
() . g1 is V11() real ext-real Element of REAL
rng (() | [.(- (sqrt 2)),(- 1).]) is V46() V47() V48() Element of K6(REAL)
x0 is set
dom (() | [.(- (sqrt 2)),(- 1).]) is V46() V47() V48() Element of K6(REAL)
g1 is V11() real ext-real Element of REAL
[.(() . (- 1)),(() . (- (sqrt 2))).] is closed V46() V47() V48() V70() Element of K6(REAL)
{ b₁ where b₁ is V11() real ext-real Element of REAL : ( () . (- 1) <= b₁ & b₁ <= () . (- (sqrt 2)) ) } is set
[.(() . (- (sqrt 2))),(() . (- 1)).] is closed V46() V47() V48() V70() Element of K6(REAL)
{ b₁ where b₁ is V11() real ext-real Element of REAL : ( () . (- (sqrt 2)) <= b₁ & b₁ <= () . (- 1) ) } is set
[.(() . (- 1)),(() . (- (sqrt 2))).] \/ [.(() . (- (sqrt 2))),(() . (- 1)).] is V46() V47() V48() set
f is V11() real ext-real Element of REAL
() . f is V11() real ext-real Element of REAL
(() | [.(- (sqrt 2)),(- 1).]) . f is V11() real ext-real Element of REAL
g1 is set
(() | [.(- (sqrt 2)),(- 1).]) . g1 is V11() real ext-real Element of REAL
() . g1 is V11() real ext-real Element of REAL
rng (() | [.1,(sqrt 2).]) is V46() V47() V48() Element of K6(REAL)
x0 is set
dom (() | [.1,(sqrt 2).]) is V46() V47() V48() Element of K6(REAL)
g1 is V11() real ext-real Element of REAL
[.(() . (sqrt 2)),(() . 1).] is closed V46() V47() V48() V70() Element of K6(REAL)
{ b₁ where b₁ is V11() real ext-real Element of REAL : ( () . (sqrt 2) <= b₁ & b₁ <= () . 1 ) } is set
[.(() . 1),(() . (sqrt 2)).] is closed V46() V47() V48() V70() Element of K6(REAL)
{ b₁ where b₁ is V11() real ext-real Element of REAL : ( () . 1 <= b₁ & b₁ <= () . (sqrt 2) ) } is set
[.(() . (sqrt 2)),(() . 1).] \/ [.(() . 1),(() . (sqrt 2)).] is V46() V47() V48() set
f is V11() real ext-real Element of REAL
() . f is V11() real ext-real Element of REAL
(() | [.1,(sqrt 2).]) . f is V11() real ext-real Element of REAL
g1 is set
(() | [.1,(sqrt 2).]) . g1 is V11() real ext-real Element of REAL
() . g1 is V11() real ext-real Element of REAL
x0 is V11() real ext-real Element of REAL
(x0) is V11() real ext-real Element of REAL
() . x0 is V11() real ext-real Element of REAL
g1 is V11() real ext-real Element of REAL
(g1) is V11() real ext-real Element of REAL
() . g1 is V11() real ext-real Element of REAL
x0 is V11() real ext-real Element of REAL
(x0) is V11() real ext-real Element of REAL
() . x0 is V11() real ext-real Element of REAL
g1 is V11() real ext-real Element of REAL
(g1) is V11() real ext-real Element of REAL
() . g1 is V11() real ext-real Element of REAL
x0 is V11() real ext-real Element of REAL
(x0) is V11() real ext-real Element of REAL
() . x0 is V11() real ext-real Element of REAL
g1 is V11() real ext-real Element of REAL
(g1) is V11() real ext-real Element of REAL
() . g1 is V11() real ext-real Element of REAL
x0 is V11() real ext-real Element of REAL
(x0) is V11() real ext-real Element of REAL
() . x0 is V11() real ext-real Element of REAL
g1 is V11() real ext-real Element of REAL
(g1) is V11() real ext-real Element of REAL
() . g1 is V11() real ext-real Element of REAL
x0 is V11() real ext-real Element of REAL
(x0) is V11() real ext-real Element of REAL
() . x0 is V11() real ext-real Element of REAL
dom (() | [.1,(sqrt 2).]) is V46() V47() V48() Element of K6(REAL)
(() | [.1,(sqrt 2).]) . x0 is V11() real ext-real Element of REAL
x0 is V11() real ext-real Element of REAL
(x0) is V11() real ext-real Element of REAL
() . x0 is V11() real ext-real Element of REAL
dom (() | [.(- (sqrt 2)),(- 1).]) is V46() V47() V48() Element of K6(REAL)
(() | [.(- (sqrt 2)),(- 1).]) . x0 is V11() real ext-real Element of REAL
x0 is V11() real ext-real Element of REAL
(x0) is V11() real ext-real Element of REAL
() . x0 is V11() real ext-real Element of REAL
dom (() | [.(- (sqrt 2)),(- 1).]) is V46() V47() V48() Element of K6(REAL)
(() | [.(- (sqrt 2)),(- 1).]) . x0 is V11() real ext-real Element of REAL
x0 is V11() real ext-real Element of REAL
(x0) is V11() real ext-real Element of REAL
() . x0 is V11() real ext-real Element of REAL
dom (() | [.1,(sqrt 2).]) is V46() V47() V48() Element of K6(REAL)
(() | [.1,(sqrt 2).]) . x0 is V11() real ext-real Element of REAL
x0 is V11() real ext-real Element of REAL
(x0) is V11() real ext-real Element of REAL
() . x0 is V11() real ext-real Element of REAL
x0 is V11() real ext-real Element of REAL
(x0) is V11() real ext-real Element of REAL
() . x0 is V11() real ext-real Element of REAL
x0 is V11() real ext-real Element of REAL
(x0) is V11() real ext-real Element of REAL
() . x0 is V11() real ext-real Element of REAL
x0 is V11() real ext-real Element of REAL
(x0) is V11() real ext-real Element of REAL
() . x0 is V11() real ext-real Element of REAL
x0 is V11() real ext-real Element of REAL
(x0) is V11() real ext-real Element of REAL
() . x0 is V11() real ext-real Element of REAL
sin . (x0) is V11() real ext-real Element of REAL
x0 ^2 is V11() real ext-real Element of REAL
K37(x0,x0) is V11() real ext-real set
(x0 ^2) - 1 is V11() real ext-real Element of REAL
K38(1) is non empty V11() real ext-real non positive negative V71() set
K36((x0 ^2),K38(1)) is V11() real ext-real set
sqrt ((x0 ^2) - 1) is V11() real ext-real Element of REAL
(sqrt ((x0 ^2) - 1)) / x0 is V11() real ext-real Element of REAL
K39(x0) is V11() real ext-real set
K37((sqrt ((x0 ^2) - 1)),K39(x0)) is V11() real ext-real set
cos . (x0) is V11() real ext-real Element of REAL
1 / x0 is V11() real ext-real Element of REAL
K37(1,K39(x0)) is V11() real ext-real set
PI / 1 is non empty V11() real ext-real positive non negative Element of REAL
K39(1) is non empty V11() real ext-real positive non negative set
K37(PI,K39(1)) is non empty V11() real ext-real positive non negative set
(cos ^) . (x0) is V11() real ext-real Element of REAL
1 / (cos . (x0)) is V11() real ext-real Element of REAL
K39((cos . (x0))) is V11() real ext-real set
K37(1,K39((cos . (x0)))) is V11() real ext-real set
1 ^2 is V11() real ext-real Element of REAL
K37(1,1) is non empty V11() real ext-real positive non negative V71() set
(sin . (x0)) ^2 is V11() real ext-real Element of REAL
K37((sin . (x0)),(sin . (x0))) is V11() real ext-real set
(cos . (x0)) ^2 is V11() real ext-real Element of REAL
K37((cos . (x0)),(cos . (x0))) is V11() real ext-real set
((sin . (x0)) ^2) + ((cos . (x0)) ^2) is V11() real ext-real Element of REAL
1 - ((cos . (x0)) ^2) is V11() real ext-real Element of REAL
K38(((cos . (x0)) ^2)) is V11() real ext-real set
K36(1,K38(((cos . (x0)) ^2))) is V11() real ext-real set
(1 / x0) * (1 / x0) is V11() real ext-real Element of REAL
1 - ((1 / x0) * (1 / x0)) is V11() real ext-real Element of REAL
K38(((1 / x0) * (1 / x0))) is V11() real ext-real set
K36(1,K38(((1 / x0) * (1 / x0)))) is V11() real ext-real set
1 / (x0 ^2) is V11() real ext-real Element of REAL
K39((x0 ^2)) is V11() real ext-real set
K37(1,K39((x0 ^2))) is V11() real ext-real set
1 - (1 / (x0 ^2)) is V11() real ext-real Element of REAL
K38((1 / (x0 ^2))) is V11() real ext-real set
K36(1,K38((1 / (x0 ^2)))) is V11() real ext-real set
(x0 ^2) / (x0 ^2) is V11() real ext-real Element of REAL
K37((x0 ^2),K39((x0 ^2))) is V11() real ext-real set
((x0 ^2) / (x0 ^2)) - (1 / (x0 ^2)) is V11() real ext-real Element of REAL
K36(((x0 ^2) / (x0 ^2)),K38((1 / (x0 ^2)))) is V11() real ext-real set
((x0 ^2) - 1) / (x0 ^2) is V11() real ext-real Element of REAL
K37(((x0 ^2) - 1),K39((x0 ^2))) is V11() real ext-real set
sqrt (((x0 ^2) - 1) / (x0 ^2)) is V11() real ext-real Element of REAL
sqrt (x0 ^2) is V11() real ext-real Element of REAL
(sqrt ((x0 ^2) - 1)) / (sqrt (x0 ^2)) is V11() real ext-real Element of REAL
K39((sqrt (x0 ^2))) is V11() real ext-real set
K37((sqrt ((x0 ^2) - 1)),K39((sqrt (x0 ^2)))) is V11() real ext-real set
x0 is V11() real ext-real Element of REAL
(x0) is V11() real ext-real Element of REAL
() . x0 is V11() real ext-real Element of REAL
sin . (x0) is V11() real ext-real Element of REAL
x0 ^2 is V11() real ext-real Element of REAL
K37(x0,x0) is V11() real ext-real set
(x0 ^2) - 1 is V11() real ext-real Element of REAL
K38(1) is non empty V11() real ext-real non positive negative V71() set
K36((x0 ^2),K38(1)) is V11() real ext-real set
sqrt ((x0 ^2) - 1) is V11() real ext-real Element of REAL
(sqrt ((x0 ^2) - 1)) / x0 is V11() real ext-real Element of REAL
K39(x0) is V11() real ext-real set
K37((sqrt ((x0 ^2) - 1)),K39(x0)) is V11() real ext-real set
- ((sqrt ((x0 ^2) - 1)) / x0) is V11() real ext-real Element of REAL
cos . (x0) is V11() real ext-real Element of REAL
1 / x0 is V11() real ext-real Element of REAL
K37(1,K39(x0)) is V11() real ext-real set
(cos ^) . (x0) is V11() real ext-real Element of REAL
1 / (cos . (x0)) is V11() real ext-real Element of REAL
K39((cos . (x0))) is V11() real ext-real set
K37(1,K39((cos . (x0)))) is V11() real ext-real set
- (- 1) is non empty V11() real ext-real positive non negative V71() Element of REAL
- x0 is V11() real ext-real Element of REAL
1 ^2 is V11() real ext-real Element of REAL
K37(1,1) is non empty V11() real ext-real positive non negative V71() set
(- x0) ^2 is V11() real ext-real Element of REAL
K37((- x0),(- x0)) is V11() real ext-real set
(sin . (x0)) ^2 is V11() real ext-real Element of REAL
K37((sin . (x0)),(sin . (x0))) is V11() real ext-real set
(cos . (x0)) ^2 is V11() real ext-real Element of REAL
K37((cos . (x0)),(cos . (x0))) is V11() real ext-real set
((sin . (x0)) ^2) + ((cos . (x0)) ^2) is V11() real ext-real Element of REAL
1 - ((cos . (x0)) ^2) is V11() real ext-real Element of REAL
K38(((cos . (x0)) ^2)) is V11() real ext-real set
K36(1,K38(((cos . (x0)) ^2))) is V11() real ext-real set
(1 / x0) * (1 / x0) is V11() real ext-real Element of REAL
1 - ((1 / x0) * (1 / x0)) is V11() real ext-real Element of REAL
K38(((1 / x0) * (1 / x0))) is V11() real ext-real set
K36(1,K38(((1 / x0) * (1 / x0)))) is V11() real ext-real set
1 / (x0 ^2) is V11() real ext-real Element of REAL
K39((x0 ^2)) is V11() real ext-real set
K37(1,K39((x0 ^2))) is V11() real ext-real set
1 - (1 / (x0 ^2)) is V11() real ext-real Element of REAL
K38((1 / (x0 ^2))) is V11() real ext-real set
K36(1,K38((1 / (x0 ^2)))) is V11() real ext-real set
(x0 ^2) / (x0 ^2) is V11() real ext-real Element of REAL
K37((x0 ^2),K39((x0 ^2))) is V11() real ext-real set
((x0 ^2) / (x0 ^2)) - (1 / (x0 ^2)) is V11() real ext-real Element of REAL
K36(((x0 ^2) / (x0 ^2)),K38((1 / (x0 ^2)))) is V11() real ext-real set
((x0 ^2) - 1) / (x0 ^2) is V11() real ext-real Element of REAL
K37(((x0 ^2) - 1),K39((x0 ^2))) is V11() real ext-real set
sqrt (((x0 ^2) - 1) / (x0 ^2)) is V11() real ext-real Element of REAL
sqrt (x0 ^2) is V11() real ext-real Element of REAL
(sqrt ((x0 ^2) - 1)) / (sqrt (x0 ^2)) is V11() real ext-real Element of REAL
K39((sqrt (x0 ^2))) is V11() real ext-real set
K37((sqrt ((x0 ^2) - 1)),K39((sqrt (x0 ^2)))) is V11() real ext-real set
(sqrt ((x0 ^2) - 1)) / (- x0) is V11() real ext-real Element of REAL
K39((- x0)) is V11() real ext-real set
K37((sqrt ((x0 ^2) - 1)),K39((- x0))) is V11() real ext-real set
x0 is V11() real ext-real Element of REAL
(x0) is V11() real ext-real Element of REAL
() . x0 is V11() real ext-real Element of REAL
sin . (x0) is V11() real ext-real Element of REAL
1 / x0 is V11() real ext-real Element of REAL
K39(x0) is V11() real ext-real set
K37(1,K39(x0)) is V11() real ext-real set
cos . (x0) is V11() real ext-real Element of REAL
x0 ^2 is V11() real ext-real Element of REAL
K37(x0,x0) is V11() real ext-real set
(x0 ^2) - 1 is V11() real ext-real Element of REAL
K38(1) is non empty V11() real ext-real non positive negative V71() set
K36((x0 ^2),K38(1)) is V11() real ext-real set
sqrt ((x0 ^2) - 1) is V11() real ext-real Element of REAL
(sqrt ((x0 ^2) - 1)) / x0 is V11() real ext-real Element of REAL
K37((sqrt ((x0 ^2) - 1)),K39(x0)) is V11() real ext-real set
- ((sqrt ((x0 ^2) - 1)) / x0) is V11() real ext-real Element of REAL
(sin ^) . (x0) is V11() real ext-real Element of REAL
1 / (sin . (x0)) is V11() real ext-real Element of REAL
K39((sin . (x0))) is V11() real ext-real set
K37(1,K39((sin . (x0)))) is V11() real ext-real set
- (- 1) is non empty V11() real ext-real positive non negative V71() Element of REAL
- x0 is V11() real ext-real Element of REAL
1 ^2 is V11() real ext-real Element of REAL
K37(1,1) is non empty V11() real ext-real positive non negative V71() set
(- x0) ^2 is V11() real ext-real Element of REAL
K37((- x0),(- x0)) is V11() real ext-real set
(sin . (x0)) ^2 is V11() real ext-real Element of REAL
K37((sin . (x0)),(sin . (x0))) is V11() real ext-real set
(cos . (x0)) ^2 is V11() real ext-real Element of REAL
K37((cos . (x0)),(cos . (x0))) is V11() real ext-real set
((sin . (x0)) ^2) + ((cos . (x0)) ^2) is V11() real ext-real Element of REAL
1 - ((sin . (x0)) ^2) is V11() real ext-real Element of REAL
K38(((sin . (x0)) ^2)) is V11() real ext-real set
K36(1,K38(((sin . (x0)) ^2))) is V11() real ext-real set
(1 / x0) * (1 / x0) is V11() real ext-real Element of REAL
1 - ((1 / x0) * (1 / x0)) is V11() real ext-real Element of REAL
K38(((1 / x0) * (1 / x0))) is V11() real ext-real set
K36(1,K38(((1 / x0) * (1 / x0)))) is V11() real ext-real set
1 / (x0 ^2) is V11() real ext-real Element of REAL
K39((x0 ^2)) is V11() real ext-real set
K37(1,K39((x0 ^2))) is V11() real ext-real set
1 - (1 / (x0 ^2)) is V11() real ext-real Element of REAL
K38((1 / (x0 ^2))) is V11() real ext-real set
K36(1,K38((1 / (x0 ^2)))) is V11() real ext-real set
(x0 ^2) / (x0 ^2) is V11() real ext-real Element of REAL
K37((x0 ^2),K39((x0 ^2))) is V11() real ext-real set
((x0 ^2) / (x0 ^2)) - (1 / (x0 ^2)) is V11() real ext-real Element of REAL
K36(((x0 ^2) / (x0 ^2)),K38((1 / (x0 ^2)))) is V11() real ext-real set
((x0 ^2) - 1) / (x0 ^2) is V11() real ext-real Element of REAL
K37(((x0 ^2) - 1),K39((x0 ^2))) is V11() real ext-real set
sqrt (((x0 ^2) - 1) / (x0 ^2)) is V11() real ext-real Element of REAL
sqrt (x0 ^2) is V11() real ext-real Element of REAL
(sqrt ((x0 ^2) - 1)) / (sqrt (x0 ^2)) is V11() real ext-real Element of REAL
K39((sqrt (x0 ^2))) is V11() real ext-real set
K37((sqrt ((x0 ^2) - 1)),K39((sqrt (x0 ^2)))) is V11() real ext-real set
(sqrt ((x0 ^2) - 1)) / (- x0) is V11() real ext-real Element of REAL
K39((- x0)) is V11() real ext-real set
K37((sqrt ((x0 ^2) - 1)),K39((- x0))) is V11() real ext-real set
x0 is V11() real ext-real Element of REAL
(x0) is V11() real ext-real Element of REAL
() . x0 is V11() real ext-real Element of REAL
sin . (x0) is V11() real ext-real Element of REAL
1 / x0 is V11() real ext-real Element of REAL
K39(x0) is V11() real ext-real set
K37(1,K39(x0)) is V11() real ext-real set
cos . (x0) is V11() real ext-real Element of REAL
x0 ^2 is V11() real ext-real Element of REAL
K37(x0,x0) is V11() real ext-real set
(x0 ^2) - 1 is V11() real ext-real Element of REAL
K38(1) is non empty V11() real ext-real non positive negative V71() set
K36((x0 ^2),K38(1)) is V11() real ext-real set
sqrt ((x0 ^2) - 1) is V11() real ext-real Element of REAL
(sqrt ((x0 ^2) - 1)) / x0 is V11() real ext-real Element of REAL
K37((sqrt ((x0 ^2) - 1)),K39(x0)) is V11() real ext-real set
(sin ^) . (x0) is V11() real ext-real Element of REAL
1 / (sin . (x0)) is V11() real ext-real Element of REAL
K39((sin . (x0))) is V11() real ext-real set
K37(1,K39((sin . (x0)))) is V11() real ext-real set
1 ^2 is V11() real ext-real Element of REAL
K37(1,1) is non empty V11() real ext-real positive non negative V71() set
(sin . (x0)) ^2 is V11() real ext-real Element of REAL
K37((sin . (x0)),(sin . (x0))) is V11() real ext-real set
(cos . (x0)) ^2 is V11() real ext-real Element of REAL
K37((cos . (x0)),(cos . (x0))) is V11() real ext-real set
((sin . (x0)) ^2) + ((cos . (x0)) ^2) is V11() real ext-real Element of REAL
1 - ((sin . (x0)) ^2) is V11() real ext-real Element of REAL
K38(((sin . (x0)) ^2)) is V11() real ext-real set
K36(1,K38(((sin . (x0)) ^2))) is V11() real ext-real set
(1 / x0) * (1 / x0) is V11() real ext-real Element of REAL
1 - ((1 / x0) * (1 / x0)) is V11() real ext-real Element of REAL
K38(((1 / x0) * (1 / x0))) is V11() real ext-real set
K36(1,K38(((1 / x0) * (1 / x0)))) is V11() real ext-real set
1 / (x0 ^2) is V11() real ext-real Element of REAL
K39((x0 ^2)) is V11() real ext-real set
K37(1,K39((x0 ^2))) is V11() real ext-real set
1 - (1 / (x0 ^2)) is V11() real ext-real Element of REAL
K38((1 / (x0 ^2))) is V11() real ext-real set
K36(1,K38((1 / (x0 ^2)))) is V11() real ext-real set
(x0 ^2) / (x0 ^2) is V11() real ext-real Element of REAL
K37((x0 ^2),K39((x0 ^2))) is V11() real ext-real set
((x0 ^2) / (x0 ^2)) - (1 / (x0 ^2)) is V11() real ext-real Element of REAL
K36(((x0 ^2) / (x0 ^2)),K38((1 / (x0 ^2)))) is V11() real ext-real set
((x0 ^2) - 1) / (x0 ^2) is V11() real ext-real Element of REAL
K37(((x0 ^2) - 1),K39((x0 ^2))) is V11() real ext-real set
sqrt (((x0 ^2) - 1) / (x0 ^2)) is V11() real ext-real Element of REAL
sqrt (x0 ^2) is V11() real ext-real Element of REAL
(sqrt ((x0 ^2) - 1)) / (sqrt (x0 ^2)) is V11() real ext-real Element of REAL
K39((sqrt (x0 ^2))) is V11() real ext-real set
K37((sqrt ((x0 ^2) - 1)),K39((sqrt (x0 ^2)))) is V11() real ext-real set
x0 is V11() real ext-real Element of REAL
(x0) is V11() real ext-real Element of REAL
() . x0 is V11() real ext-real Element of REAL
cosec . (x0) is V11() real ext-real Element of REAL
x0 ^2 is V11() real ext-real Element of REAL
K37(x0,x0) is V11() real ext-real set
(x0 ^2) - 1 is V11() real ext-real Element of REAL
K38(1) is non empty V11() real ext-real non positive negative V71() set
K36((x0 ^2),K38(1)) is V11() real ext-real set
sqrt ((x0 ^2) - 1) is V11() real ext-real Element of REAL
x0 / (sqrt ((x0 ^2) - 1)) is V11() real ext-real Element of REAL
K39((sqrt ((x0 ^2) - 1))) is V11() real ext-real set
K37(x0,K39((sqrt ((x0 ^2) - 1)))) is V11() real ext-real set
{(PI / 2)} is non empty V46() V47() V48() set
].0,(PI / 2).[ \/ {(PI / 2)} is non empty V46() V47() V48() set
].0,(PI / 4).[ is open V46() V47() V48() V65() V66() V70() Element of K6(REAL)
{ b₁ where b₁ is V11() real ext-real Element of REAL : ( not b₁ <= 0 & not PI / 4 <= b₁ ) } is set
sin . (x0) is V11() real ext-real Element of REAL
1 / (sin . (x0)) is V11() real ext-real Element of REAL
K39((sin . (x0))) is V11() real ext-real set
K37(1,K39((sin . (x0)))) is V11() real ext-real set
(sqrt ((x0 ^2) - 1)) / x0 is V11() real ext-real Element of REAL
K39(x0) is V11() real ext-real set
K37((sqrt ((x0 ^2) - 1)),K39(x0)) is V11() real ext-real set
1 / ((sqrt ((x0 ^2) - 1)) / x0) is V11() real ext-real Element of REAL
K39(((sqrt ((x0 ^2) - 1)) / x0)) is V11() real ext-real set
K37(1,K39(((sqrt ((x0 ^2) - 1)) / x0))) is V11() real ext-real set
x0 is V11() real ext-real Element of REAL
(x0) is V11() real ext-real Element of REAL
() . x0 is V11() real ext-real Element of REAL
cosec . (x0) is V11() real ext-real Element of REAL
x0 ^2 is V11() real ext-real Element of REAL
K37(x0,x0) is V11() real ext-real set
(x0 ^2) - 1 is V11() real ext-real Element of REAL
K38(1) is non empty V11() real ext-real non positive negative V71() set
K36((x0 ^2),K38(1)) is V11() real ext-real set
sqrt ((x0 ^2) - 1) is V11() real ext-real Element of REAL
x0 / (sqrt ((x0 ^2) - 1)) is V11() real ext-real Element of REAL
K39((sqrt ((x0 ^2) - 1))) is V11() real ext-real set
K37(x0,K39((sqrt ((x0 ^2) - 1)))) is V11() real ext-real set
- (x0 / (sqrt ((x0 ^2) - 1))) is V11() real ext-real Element of REAL
].((3 / 4) * PI),PI.[ is open V46() V47() V48() V65() V66() V70() Element of K6(REAL)
{ b₁ where b₁ is V11() real ext-real Element of REAL : ( not b₁ <= (3 / 4) * PI & not PI <= b₁ ) } is set
sin " {0} is V46() V47() V48() Element of K6(REAL)
].((3 / 4) * PI),PI.[ /\ (sin " {0}) is V46() V47() V48() set
f is set
sin . f is V11() real ext-real Element of REAL
].((3 / 4) * PI),PI.[ \ (sin " {0}) is V46() V47() V48() set
(dom sin) \ (sin " {0}) is V46() V47() V48() set
sin . (x0) is V11() real ext-real Element of REAL
1 / (sin . (x0)) is V11() real ext-real Element of REAL
K39((sin . (x0))) is V11() real ext-real set
K37(1,K39((sin . (x0)))) is V11() real ext-real set
(sqrt ((x0 ^2) - 1)) / x0 is V11() real ext-real Element of REAL
K39(x0) is V11() real ext-real set
K37((sqrt ((x0 ^2) - 1)),K39(x0)) is V11() real ext-real set
- ((sqrt ((x0 ^2) - 1)) / x0) is V11() real ext-real Element of REAL
1 / (- ((sqrt ((x0 ^2) - 1)) / x0)) is V11() real ext-real Element of REAL
K39((- ((sqrt ((x0 ^2) - 1)) / x0))) is V11() real ext-real set
K37(1,K39((- ((sqrt ((x0 ^2) - 1)) / x0)))) is V11() real ext-real set
1 / ((sqrt ((x0 ^2) - 1)) / x0) is V11() real ext-real Element of REAL
K39(((sqrt ((x0 ^2) - 1)) / x0)) is V11() real ext-real set
K37(1,K39(((sqrt ((x0 ^2) - 1)) / x0))) is V11() real ext-real set
- (1 / ((sqrt ((x0 ^2) - 1)) / x0)) is V11() real ext-real Element of REAL
x0 is V11() real ext-real Element of REAL
(x0) is V11() real ext-real Element of REAL
() . x0 is V11() real ext-real Element of REAL
sec . (x0) is V11() real ext-real Element of REAL
x0 ^2 is V11() real ext-real Element of REAL
K37(x0,x0) is V11() real ext-real set
(x0 ^2) - 1 is V11() real ext-real Element of REAL
K38(1) is non empty V11() real ext-real non positive negative V71() set
K36((x0 ^2),K38(1)) is V11() real ext-real set
sqrt ((x0 ^2) - 1) is V11() real ext-real Element of REAL
x0 / (sqrt ((x0 ^2) - 1)) is V11() real ext-real Element of REAL
K39((sqrt ((x0 ^2) - 1))) is V11() real ext-real set
K37(x0,K39((sqrt ((x0 ^2) - 1)))) is V11() real ext-real set
- (x0 / (sqrt ((x0 ^2) - 1))) is V11() real ext-real Element of REAL
].(- (PI / 2)),(- (PI / 4)).[ is open V46() V47() V48() V65() V66() V70() Element of K6(REAL)
{ b₁ where b₁ is V11() real ext-real Element of REAL : ( not b₁ <= - (PI / 2) & not - (PI / 4) <= b₁ ) } is set
cos " {0} is V46() V47() V48() Element of K6(REAL)
].(- (PI / 2)),(- (PI / 4)).[ /\ (cos " {0}) is V46() V47() V48() set
f is set
cos . f is V11() real ext-real Element of REAL
].(- (PI / 2)),(- (PI / 4)).[ \ (cos " {0}) is V46() V47() V48() set
(dom cos) \ (cos " {0}) is V46() V47() V48() set
cos . (x0) is V11() real ext-real Element of REAL
1 / (cos . (x0)) is V11() real ext-real Element of REAL
K39((cos . (x0))) is V11() real ext-real set
K37(1,K39((cos . (x0)))) is V11() real ext-real set
(sqrt ((x0 ^2) - 1)) / x0 is V11() real ext-real Element of REAL
K39(x0) is V11() real ext-real set
K37((sqrt ((x0 ^2) - 1)),K39(x0)) is V11() real ext-real set
- ((sqrt ((x0 ^2) - 1)) / x0) is V11() real ext-real Element of REAL
1 / (- ((sqrt ((x0 ^2) - 1)) / x0)) is V11() real ext-real Element of REAL
K39((- ((sqrt ((x0 ^2) - 1)) / x0))) is V11() real ext-real set
K37(1,K39((- ((sqrt ((x0 ^2) - 1)) / x0)))) is V11() real ext-real set
1 / ((sqrt ((x0 ^2) - 1)) / x0) is V11() real ext-real Element of REAL
K39(((sqrt ((x0 ^2) - 1)) / x0)) is V11() real ext-real set
K37(1,K39(((sqrt ((x0 ^2) - 1)) / x0))) is V11() real ext-real set
- (1 / ((sqrt ((x0 ^2) - 1)) / x0)) is V11() real ext-real Element of REAL
x0 is V11() real ext-real Element of REAL
(x0) is V11() real ext-real Element of REAL
() . x0 is V11() real ext-real Element of REAL
sec . (x0) is V11() real ext-real Element of REAL
x0 ^2 is V11() real ext-real Element of REAL
K37(x0,x0) is V11() real ext-real set
(x0 ^2) - 1 is V11() real ext-real Element of REAL
K38(1) is non empty V11() real ext-real non positive negative V71() set
K36((x0 ^2),K38(1)) is V11() real ext-real set
sqrt ((x0 ^2) - 1) is V11() real ext-real Element of REAL
x0 / (sqrt ((x0 ^2) - 1)) is V11() real ext-real Element of REAL
K39((sqrt ((x0 ^2) - 1))) is V11() real ext-real set
K37(x0,K39((sqrt ((x0 ^2) - 1)))) is V11() real ext-real set
].0,(PI / 2).[ \/ {0} is non empty V46() V47() V48() set
].(PI / 4),(PI / 2).[ is open V46() V47() V48() V65() V66() V70() Element of K6(REAL)
{ b₁ where b₁ is V11() real ext-real Element of REAL : ( not b₁ <= PI / 4 & not PI / 2 <= b₁ ) } is set
cos . (x0) is V11() real ext-real Element of REAL
1 / (cos . (x0)) is V11() real ext-real Element of REAL
K39((cos . (x0))) is V11() real ext-real set
K37(1,K39((cos . (x0)))) is V11() real ext-real set
(sqrt ((x0 ^2) - 1)) / x0 is V11() real ext-real Element of REAL
K39(x0) is V11() real ext-real set
K37((sqrt ((x0 ^2) - 1)),K39(x0)) is V11() real ext-real set
1 / ((sqrt ((x0 ^2) - 1)) / x0) is V11() real ext-real Element of REAL
K39(((sqrt ((x0 ^2) - 1)) / x0)) is V11() real ext-real set
K37(1,K39(((sqrt ((x0 ^2) - 1)) / x0))) is V11() real ext-real set
sec .: ].0,(PI / 2).[ is V46() V47() V48() Element of K6(REAL)
() | (sec .: ].0,(PI / 2).[) is V19() V22( REAL ) V23( REAL ) Function-like one-to-one V36() V37() V38() Element of K6(K7(REAL,REAL))
((sec | [.0,(PI / 2).[) | ].0,(PI / 2).[) | ].0,(PI / 2).[ is V19() V22( REAL ) V23( REAL ) Function-like one-to-one V36() V37() V38() Element of K6(K7(REAL,REAL))
(((sec | [.0,(PI / 2).[) | ].0,(PI / 2).[) | ].0,(PI / 2).[) " is V19() V22( REAL ) V23( REAL ) Function-like one-to-one V36() V37() V38() Element of K6(K7(REAL,REAL))
dom ((((sec | [.0,(PI / 2).[) | ].0,(PI / 2).[) | ].0,(PI / 2).[) ") is V46() V47() V48() Element of K6(REAL)
rng (((sec | [.0,(PI / 2).[) | ].0,(PI / 2).[) | ].0,(PI / 2).[) is V46() V47() V48() Element of K6(REAL)
rng (sec | ].0,(PI / 2).[) is V46() V47() V48() Element of K6(REAL)
((sec | [.0,(PI / 2).[) | ].0,(PI / 2).[) " is V19() V22( REAL ) V23( REAL ) Function-like one-to-one V36() V37() V38() Element of K6(K7(REAL,REAL))
(sec | [.0,(PI / 2).[) .: ].0,(PI / 2).[ is V46() V47() V48() Element of K6(REAL)
() | ((sec | [.0,(PI / 2).[) .: ].0,(PI / 2).[) is V19() V22( REAL ) V23( REAL ) Function-like one-to-one V36() V37() V38() Element of K6(K7(REAL,REAL))
rng ((sec | [.0,(PI / 2).[) | ].0,(PI / 2).[) is V46() V47() V48() Element of K6(REAL)
() | (rng ((sec | [.0,(PI / 2).[) | ].0,(PI / 2).[)) is V19() V22( REAL ) V23( REAL ) Function-like one-to-one V36() V37() V38() Element of K6(K7(REAL,REAL))
() | (rng (sec | ].0,(PI / 2).[)) is V19() V22( REAL ) V23( REAL ) Function-like one-to-one V36() V37() V38() Element of K6(K7(REAL,REAL))
x is V11() real ext-real Element of REAL
sin . x is V11() real ext-real Element of REAL
cos . x is V11() real ext-real Element of REAL
(cos . x) ^2 is V11() real ext-real Element of REAL
K37((cos . x),(cos . x)) is V11() real ext-real set
(sin . x) / ((cos . x) ^2) is V11() real ext-real Element of REAL
K39(((cos . x) ^2)) is V11() real ext-real set
K37((sin . x),K39(((cos . x) ^2))) is V11() real ext-real set
x is V11() real ext-real Element of REAL
diff (((sec | [.0,(PI / 2).[) | ].0,(PI / 2).[),x) is V11() real ext-real Element of REAL
((sec | [.0,(PI / 2).[) | ].0,(PI / 2).[) `| ].0,(PI / 2).[ is V19() V22( REAL ) V23( REAL ) Function-like V36() V37() V38() Element of K6(K7(REAL,REAL))
(((sec | [.0,(PI / 2).[) | ].0,(PI / 2).[) `| ].0,(PI / 2).[) . x is V11() real ext-real Element of REAL
(sec | ].0,(PI / 2).[) `| ].0,(PI / 2).[ is V19() V22( REAL ) V23( REAL ) Function-like V36() V37() V38() Element of K6(K7(REAL,REAL))
((sec | ].0,(PI / 2).[) `| ].0,(PI / 2).[) . x is V11() real ext-real Element of REAL
sec `| ].0,(PI / 2).[ is V19() V22( REAL ) V23( REAL ) Function-like V36() V37() V38() Element of K6(K7(REAL,REAL))
(sec `| ].0,(PI / 2).[) . x is V11() real ext-real Element of REAL
diff (sec,x) is V11() real ext-real Element of REAL
sin . x is V11() real ext-real Element of REAL
cos . x is V11() real ext-real Element of REAL
(cos . x) ^2 is V11() real ext-real Element of REAL
K37((cos . x),(cos . x)) is V11() real ext-real set
(sin . x) / ((cos . x) ^2) is V11() real ext-real Element of REAL
K39(((cos . x) ^2)) is V11() real ext-real set
K37((sin . x),K39(((cos . x) ^2))) is V11() real ext-real set
x is V11() real ext-real Element of REAL
(() | (sec .: ].0,(PI / 2).[)) | (sec .: ].0,(PI / 2).[) is V19() V22( REAL ) V23( REAL ) Function-like one-to-one V36() V37() V38() Element of K6(K7(REAL,REAL))
sec .: ].(PI / 2),PI.[ is V46() V47() V48() Element of K6(REAL)
() | (sec .: ].(PI / 2),PI.[) is V19() V22( REAL ) V23( REAL ) Function-like one-to-one V36() V37() V38() Element of K6(K7(REAL,REAL))
((sec | ].(PI / 2),PI.]) | ].(PI / 2),PI.[) | ].(PI / 2),PI.[ is V19() V22( REAL ) V23( REAL ) Function-like one-to-one V36() V37() V38() Element of K6(K7(REAL,REAL))
(((sec | ].(PI / 2),PI.]) | ].(PI / 2),PI.[) | ].(PI / 2),PI.[) " is V19() V22( REAL ) V23( REAL ) Function-like one-to-one V36() V37() V38() Element of K6(K7(REAL,REAL))
dom ((((sec | ].(PI / 2),PI.]) | ].(PI / 2),PI.[) | ].(PI / 2),PI.[) ") is V46() V47() V48() Element of K6(REAL)
rng (((sec | ].(PI / 2),PI.]) | ].(PI / 2),PI.[) | ].(PI / 2),PI.[) is V46() V47() V48() Element of K6(REAL)
rng (sec | ].(PI / 2),PI.[) is V46() V47() V48() Element of K6(REAL)
((sec | ].(PI / 2),PI.]) | ].(PI / 2),PI.[) " is V19() V22( REAL ) V23( REAL ) Function-like one-to-one V36() V37() V38() Element of K6(K7(REAL,REAL))
(sec | ].(PI / 2),PI.]) .: ].(PI / 2),PI.[ is V46() V47() V48() Element of K6(REAL)
() | ((sec | ].(PI / 2),PI.]) .: ].(PI / 2),PI.[) is V19() V22( REAL ) V23( REAL ) Function-like one-to-one V36() V37() V38() Element of K6(K7(REAL,REAL))
rng ((sec | ].(PI / 2),PI.]) | ].(PI / 2),PI.[) is V46() V47() V48() Element of K6(REAL)
() | (rng ((sec | ].(PI / 2),PI.]) | ].(PI / 2),PI.[)) is V19() V22( REAL ) V23( REAL ) Function-like one-to-one V36() V37() V38() Element of K6(K7(REAL,REAL))
() | (rng (sec | ].(PI / 2),PI.[)) is V19() V22( REAL ) V23( REAL ) Function-like one-to-one V36() V37() V38() Element of K6(K7(REAL,REAL))
x is V11() real ext-real Element of REAL
sin . x is V11() real ext-real Element of REAL
cos . x is V11() real ext-real Element of REAL
(cos . x) ^2 is V11() real ext-real Element of REAL
K37((cos . x),(cos . x)) is V11() real ext-real set
(sin . x) / ((cos . x) ^2) is V11() real ext-real Element of REAL
K39(((cos . x) ^2)) is V11() real ext-real set
K37((sin . x),K39(((cos . x) ^2))) is V11() real ext-real set
x is V11() real ext-real Element of REAL
diff (((sec | ].(PI / 2),PI.]) | ].(PI / 2),PI.[),x) is V11() real ext-real Element of REAL
((sec | ].(PI / 2),PI.]) | ].(PI / 2),PI.[) `| ].(PI / 2),PI.[ is V19() V22( REAL ) V23( REAL ) Function-like V36() V37() V38() Element of K6(K7(REAL,REAL))
(((sec | ].(PI / 2),PI.]) | ].(PI / 2),PI.[) `| ].(PI / 2),PI.[) . x is V11() real ext-real Element of REAL
(sec | ].(PI / 2),PI.[) `| ].(PI / 2),PI.[ is V19() V22( REAL ) V23( REAL ) Function-like V36() V37() V38() Element of K6(K7(REAL,REAL))
((sec | ].(PI / 2),PI.[) `| ].(PI / 2),PI.[) . x is V11() real ext-real Element of REAL
sec `| ].(PI / 2),PI.[ is V19() V22( REAL ) V23( REAL ) Function-like V36() V37() V38() Element of K6(K7(REAL,REAL))
(sec `| ].(PI / 2),PI.[) . x is V11() real ext-real Element of REAL
diff (sec,x) is V11() real ext-real Element of REAL
sin . x is V11() real ext-real Element of REAL
cos . x is V11() real ext-real Element of REAL
(cos . x) ^2 is V11() real ext-real Element of REAL
K37((cos . x),(cos . x)) is V11() real ext-real set
(sin . x) / ((cos . x) ^2) is V11() real ext-real Element of REAL
K39(((cos . x) ^2)) is V11() real ext-real set
K37((sin . x),K39(((cos . x) ^2))) is V11() real ext-real set
x is V11() real ext-real Element of REAL
(() | (sec .: ].(PI / 2),PI.[)) | (sec .: ].(PI / 2),PI.[) is V19() V22( REAL ) V23( REAL ) Function-like one-to-one V36() V37() V38() Element of K6(K7(REAL,REAL))
cosec .: ].(- (PI / 2)),0.[ is V46() V47() V48() Element of K6(REAL)
() | (cosec .: ].(- (PI / 2)),0.[) is V19() V22( REAL ) V23( REAL ) Function-like one-to-one V36() V37() V38() Element of K6(K7(REAL,REAL))
((cosec | [.(- (PI / 2)),0.[) | ].(- (PI / 2)),0.[) | ].(- (PI / 2)),0.[ is V19() V22( REAL ) V23( REAL ) Function-like one-to-one V36() V37() V38() Element of K6(K7(REAL,REAL))
(((cosec | [.(- (PI / 2)),0.[) | ].(- (PI / 2)),0.[) | ].(- (PI / 2)),0.[) " is V19() V22( REAL ) V23( REAL ) Function-like one-to-one V36() V37() V38() Element of K6(K7(REAL,REAL))
dom ((((cosec | [.(- (PI / 2)),0.[) | ].(- (PI / 2)),0.[) | ].(- (PI / 2)),0.[) ") is V46() V47() V48() Element of K6(REAL)
rng (((cosec | [.(- (PI / 2)),0.[) | ].(- (PI / 2)),0.[) | ].(- (PI / 2)),0.[) is V46() V47() V48() Element of K6(REAL)
rng (cosec | ].(- (PI / 2)),0.[) is V46() V47() V48() Element of K6(REAL)
((cosec | [.(- (PI / 2)),0.[) | ].(- (PI / 2)),0.[) " is V19() V22( REAL ) V23( REAL ) Function-like one-to-one V36() V37() V38() Element of K6(K7(REAL,REAL))
(cosec | [.(- (PI / 2)),0.[) .: ].(- (PI / 2)),0.[ is V46() V47() V48() Element of K6(REAL)
() | ((cosec | [.(- (PI / 2)),0.[) .: ].(- (PI / 2)),0.[) is V19() V22( REAL ) V23( REAL ) Function-like one-to-one V36() V37() V38() Element of K6(K7(REAL,REAL))
rng ((cosec | [.(- (PI / 2)),0.[) | ].(- (PI / 2)),0.[) is V46() V47() V48() Element of K6(REAL)
() | (rng ((cosec | [.(- (PI / 2)),0.[) | ].(- (PI / 2)),0.[)) is V19() V22( REAL ) V23( REAL ) Function-like one-to-one V36() V37() V38() Element of K6(K7(REAL,REAL))
() | (rng (cosec | ].(- (PI / 2)),0.[)) is V19() V22( REAL ) V23( REAL ) Function-like one-to-one V36() V37() V38() Element of K6(K7(REAL,REAL))
x is V11() real ext-real Element of REAL
cos . x is V11() real ext-real Element of REAL
sin . x is V11() real ext-real Element of REAL
(sin . x) ^2 is V11() real ext-real Element of REAL
K37((sin . x),(sin . x)) is V11() real ext-real set
(cos . x) / ((sin . x) ^2) is V11() real ext-real Element of REAL
K39(((sin . x) ^2)) is V11() real ext-real set
K37((cos . x),K39(((sin . x) ^2))) is V11() real ext-real set
- ((cos . x) / ((sin . x) ^2)) is V11() real ext-real Element of REAL
0 + (2 * PI) is non empty V11() real ext-real positive non negative Element of REAL
x + (2 * PI) is V11() real ext-real Element of REAL
{(- (PI / 2))} is non empty V46() V47() V48() set
].(- (PI / 2)),0.[ \/ {(- (PI / 2))} is non empty V46() V47() V48() set
(- PI) + (2 * PI) is V11() real ext-real Element of REAL
sin . (x + (2 * PI)) is V11() real ext-real Element of REAL
x is V11() real ext-real Element of REAL
diff (((cosec | [.(- (PI / 2)),0.[) | ].(- (PI / 2)),0.[),x) is V11() real ext-real Element of REAL
((cosec | [.(- (PI / 2)),0.[) | ].(- (PI / 2)),0.[) `| ].(- (PI / 2)),0.[ is V19() V22( REAL ) V23( REAL ) Function-like V36() V37() V38() Element of K6(K7(REAL,REAL))
(((cosec | [.(- (PI / 2)),0.[) | ].(- (PI / 2)),0.[) `| ].(- (PI / 2)),0.[) . x is V11() real ext-real Element of REAL
(cosec | ].(- (PI / 2)),0.[) `| ].(- (PI / 2)),0.[ is V19() V22( REAL ) V23( REAL ) Function-like V36() V37() V38() Element of K6(K7(REAL,REAL))
((cosec | ].(- (PI / 2)),0.[) `| ].(- (PI / 2)),0.[) . x is V11() real ext-real Element of REAL
cosec `| ].(- (PI / 2)),0.[ is V19() V22( REAL ) V23( REAL ) Function-like V36() V37() V38() Element of K6(K7(REAL,REAL))
(cosec `| ].(- (PI / 2)),0.[) . x is V11() real ext-real Element of REAL
diff (cosec,x) is V11() real ext-real Element of REAL
cos . x is V11() real ext-real Element of REAL
sin . x is V11() real ext-real Element of REAL
(sin . x) ^2 is V11() real ext-real Element of REAL
K37((sin . x),(sin . x)) is V11() real ext-real set
(cos . x) / ((sin . x) ^2) is V11() real ext-real Element of REAL
K39(((sin . x) ^2)) is V11() real ext-real set
K37((cos . x),K39(((sin . x) ^2))) is V11() real ext-real set
- ((cos . x) / ((sin . x) ^2)) is V11() real ext-real Element of REAL
x is V11() real ext-real Element of REAL
(() | (cosec .: ].(- (PI / 2)),0.[)) | (cosec .: ].(- (PI / 2)),0.[) is V19() V22( REAL ) V23( REAL ) Function-like one-to-one V36() V37() V38() Element of K6(K7(REAL,REAL))
cosec .: ].0,(PI / 2).[ is V46() V47() V48() Element of K6(REAL)
() | (cosec .: ].0,(PI / 2).[) is V19() V22( REAL ) V23( REAL ) Function-like one-to-one V36() V37() V38() Element of K6(K7(REAL,REAL))
((cosec | ].0,(PI / 2).]) | ].0,(PI / 2).[) | ].0,(PI / 2).[ is V19() V22( REAL ) V23( REAL ) Function-like one-to-one V36() V37() V38() Element of K6(K7(REAL,REAL))
(((cosec | ].0,(PI / 2).]) | ].0,(PI / 2).[) | ].0,(PI / 2).[) " is V19() V22( REAL ) V23( REAL ) Function-like one-to-one V36() V37() V38() Element of K6(K7(REAL,REAL))
dom ((((cosec | ].0,(PI / 2).]) | ].0,(PI / 2).[) | ].0,(PI / 2).[) ") is V46() V47() V48() Element of K6(REAL)
rng (((cosec | ].0,(PI / 2).]) | ].0,(PI / 2).[) | ].0,(PI / 2).[) is V46() V47() V48() Element of K6(REAL)
rng (cosec | ].0,(PI / 2).[) is V46() V47() V48() Element of K6(REAL)
((cosec | ].0,(PI / 2).]) | ].0,(PI / 2).[) " is V19() V22( REAL ) V23( REAL ) Function-like one-to-one V36() V37() V38() Element of K6(K7(REAL,REAL))
(cosec | ].0,(PI / 2).]) .: ].0,(PI / 2).[ is V46() V47() V48() Element of K6(REAL)
() | ((cosec | ].0,(PI / 2).]) .: ].0,(PI / 2).[) is V19() V22( REAL ) V23( REAL ) Function-like one-to-one V36() V37() V38() Element of K6(K7(REAL,REAL))
rng ((cosec | ].0,(PI / 2).]) | ].0,(PI / 2).[) is V46() V47() V48() Element of K6(REAL)
() | (rng ((cosec | ].0,(PI / 2).]) | ].0,(PI / 2).[)) is V19() V22( REAL ) V23( REAL ) Function-like one-to-one V36() V37() V38() Element of K6(K7(REAL,REAL))
() | (rng (cosec | ].0,(PI / 2).[)) is V19() V22( REAL ) V23( REAL ) Function-like one-to-one V36() V37() V38() Element of K6(K7(REAL,REAL))
x is V11() real ext-real Element of REAL
cos . x is V11() real ext-real Element of REAL
sin . x is V11() real ext-real Element of REAL
(sin . x) ^2 is V11() real ext-real Element of REAL
K37((sin . x),(sin . x)) is V11() real ext-real set
(cos . x) / ((sin . x) ^2) is V11() real ext-real Element of REAL
K39(((sin . x) ^2)) is V11() real ext-real set
K37((cos . x),K39(((sin . x) ^2))) is V11() real ext-real set
- ((cos . x) / ((sin . x) ^2)) is V11() real ext-real Element of REAL
x is V11() real ext-real Element of REAL
diff (((cosec | ].0,(PI / 2).]) | ].0,(PI / 2).[),x) is V11() real ext-real Element of REAL
((cosec | ].0,(PI / 2).]) | ].0,(PI / 2).[) `| ].0,(PI / 2).[ is V19() V22( REAL ) V23( REAL ) Function-like V36() V37() V38() Element of K6(K7(REAL,REAL))
(((cosec | ].0,(PI / 2).]) | ].0,(PI / 2).[) `| ].0,(PI / 2).[) . x is V11() real ext-real Element of REAL
(cosec | ].0,(PI / 2).[) `| ].0,(PI / 2).[ is V19() V22( REAL ) V23( REAL ) Function-like V36() V37() V38() Element of K6(K7(REAL,REAL))
((cosec | ].0,(PI / 2).[) `| ].0,(PI / 2).[) . x is V11() real ext-real Element of REAL
cosec `| ].0,(PI / 2).[ is V19() V22( REAL ) V23( REAL ) Function-like V36() V37() V38() Element of K6(K7(REAL,REAL))
(cosec `| ].0,(PI / 2).[) . x is V11() real ext-real Element of REAL
diff (cosec,x) is V11() real ext-real Element of REAL
cos . x is V11() real ext-real Element of REAL
sin . x is V11() real ext-real Element of REAL
(sin . x) ^2 is V11() real ext-real Element of REAL
K37((sin . x),(sin . x)) is V11() real ext-real set
(cos . x) / ((sin . x) ^2) is V11() real ext-real Element of REAL
K39(((sin . x) ^2)) is V11() real ext-real set
K37((cos . x),K39(((sin . x) ^2))) is V11() real ext-real set
- ((cos . x) / ((sin . x) ^2)) is V11() real ext-real Element of REAL
x is V11() real ext-real Element of REAL
(() | (cosec .: ].0,(PI / 2).[)) | (cosec .: ].0,(PI / 2).[) is V19() V22( REAL ) V23( REAL ) Function-like one-to-one V36() V37() V38() Element of K6(K7(REAL,REAL))
x0 is V11() real ext-real Element of REAL
diff (sec,x0) is V11() real ext-real Element of REAL
cos . x0 is V11() real ext-real Element of REAL
sin . x0 is V11() real ext-real Element of REAL
(cos . x0) ^2 is V11() real ext-real Element of REAL
K37((cos . x0),(cos . x0)) is V11() real ext-real set
(sin . x0) / ((cos . x0) ^2) is V11() real ext-real Element of REAL
K39(((cos . x0) ^2)) is V11() real ext-real set
K37((sin . x0),K39(((cos . x0) ^2))) is V11() real ext-real set
0 / ((cos . x0) ^2) is V11() real ext-real Element of REAL
K37(0,K39(((cos . x0) ^2))) is V11() real ext-real set
rng (sec | ].0,(PI / 2).[) is V46() V47() V48() Element of K6(REAL)
x0 is V11() real ext-real Element of REAL
diff (sec,x0) is V11() real ext-real Element of REAL
cos . x0 is V11() real ext-real Element of REAL
sin . x0 is V11() real ext-real Element of REAL
(cos . x0) ^2 is V11() real ext-real Element of REAL
K37((cos . x0),(cos . x0)) is V11() real ext-real set
(sin . x0) / ((cos . x0) ^2) is V11() real ext-real Element of REAL
K39(((cos . x0) ^2)) is V11() real ext-real set
K37((sin . x0),K39(((cos . x0) ^2))) is V11() real ext-real set
0 / ((cos . x0) ^2) is V11() real ext-real Element of REAL
K37(0,K39(((cos . x0) ^2))) is V11() real ext-real set
rng (sec | ].(PI / 2),PI.[) is V46() V47() V48() Element of K6(REAL)
x0 is V11() real ext-real Element of REAL
diff (cosec,x0) is V11() real ext-real Element of REAL
0 + (2 * PI) is non empty V11() real ext-real positive non negative Element of REAL
x0 + (2 * PI) is V11() real ext-real Element of REAL
{(- (PI / 2))} is non empty V46() V47() V48() set
].(- (PI / 2)),0.[ \/ {(- (PI / 2))} is non empty V46() V47() V48() set
(- PI) + (2 * PI) is V11() real ext-real Element of REAL
sin . (x0 + (2 * PI)) is V11() real ext-real Element of REAL
sin . x0 is V11() real ext-real Element of REAL
cos . x0 is V11() real ext-real Element of REAL
- 0 is empty epsilon-transitive epsilon-connected ordinal T-Sequence-like c=-linear natural V11() real ext-real non positive non negative Function-like functional V46() V47() V48() V49() V50() V51() V52() V67() V70() V71() Element of REAL
(sin . x0) ^2 is V11() real ext-real Element of REAL
K37((sin . x0),(sin . x0)) is V11() real ext-real set
(cos . x0) / ((sin . x0) ^2) is V11() real ext-real Element of REAL
K39(((sin . x0) ^2)) is V11() real ext-real set
K37((cos . x0),K39(((sin . x0) ^2))) is V11() real ext-real set
- ((cos . x0) / ((sin . x0) ^2)) is V11() real ext-real Element of REAL
rng (cosec | ].(- (PI / 2)),0.[) is V46() V47() V48() Element of K6(REAL)
x0 is V11() real ext-real Element of REAL
diff (cosec,x0) is V11() real ext-real Element of REAL
cos . x0 is V11() real ext-real Element of REAL
sin . x0 is V11() real ext-real Element of REAL
- 0 is empty epsilon-transitive epsilon-connected ordinal T-Sequence-like c=-linear natural V11() real ext-real non positive non negative Function-like functional V46() V47() V48() V49() V50() V51() V52() V67() V70() V71() Element of REAL
(sin . x0) ^2 is V11() real ext-real Element of REAL
K37((sin . x0),(sin . x0)) is V11() real ext-real set
(cos . x0) / ((sin . x0) ^2) is V11() real ext-real Element of REAL
K39(((sin . x0) ^2)) is V11() real ext-real set
K37((cos . x0),K39(((sin . x0) ^2))) is V11() real ext-real set
- ((cos . x0) / ((sin . x0) ^2)) is V11() real ext-real Element of REAL
rng (cosec | ].0,(PI / 2).[) is V46() V47() V48() Element of K6(REAL)
() | (sec .: ].0,(PI / 2).[) is V19() V22( REAL ) V23( REAL ) Function-like one-to-one V36() V37() V38() Element of K6(K7(REAL,REAL))
() | (sec .: ].(PI / 2),PI.[) is V19() V22( REAL ) V23( REAL ) Function-like one-to-one V36() V37() V38() Element of K6(K7(REAL,REAL))
() | (cosec .: ].(- (PI / 2)),0.[) is V19() V22( REAL ) V23( REAL ) Function-like one-to-one V36() V37() V38() Element of K6(K7(REAL,REAL))
() | (cosec .: ].0,(PI / 2).[) is V19() V22( REAL ) V23( REAL ) Function-like one-to-one V36() V37() V38() Element of K6(K7(REAL,REAL))