:: FUNCT_9 semantic presentation

REAL is non empty V45() V134() V135() V136() V140() set

NAT is V134() V135() V136() V137() V138() V139() V140() Element of K6(REAL)

K6(REAL) is set

omega is V134() V135() V136() V137() V138() V139() V140() set

K6(omega) is set

K6(NAT) is set

RAT is non empty V45() V134() V135() V136() V137() V140() set

1 is non empty ordinal natural complex real V30() V31() V32() integer V44() V134() V135() V136() V137() V138() V139() Element of NAT

K7(1,1) is Relation-like RAT -valued INT -valued complex-valued ext-real-valued real-valued natural-valued set

INT is non empty V45() V134() V135() V136() V137() V138() V140() set

K6(K7(1,1)) is set

K7(K7(1,1),1) is Relation-like RAT -valued INT -valued complex-valued ext-real-valued real-valued natural-valued set

K6(K7(K7(1,1),1)) is set

K7(K7(1,1),REAL) is Relation-like complex-valued ext-real-valued real-valued set

K6(K7(K7(1,1),REAL)) is set

K7(REAL,REAL) is Relation-like complex-valued ext-real-valued real-valued set

K7(K7(REAL,REAL),REAL) is Relation-like complex-valued ext-real-valued real-valued set

K6(K7(K7(REAL,REAL),REAL)) is set

2 is non empty ordinal natural complex real V30() V31() V32() integer V44() V134() V135() V136() V137() V138() V139() Element of NAT

K7(2,2) is Relation-like RAT -valued INT -valued complex-valued ext-real-valued real-valued natural-valued set

K7(K7(2,2),REAL) is Relation-like complex-valued ext-real-valued real-valued set

K6(K7(K7(2,2),REAL)) is set

COMPLEX is non empty V45() V134() V140() set

K6(K7(REAL,REAL)) is set

K312(2) is V158() L15()

the U1 of K312(2) is set

{} is set

the empty Relation-like non-empty empty-yielding RAT -valued complex-valued ext-real-valued real-valued natural-valued V134() V135() V136() V137() V138() V139() V140() set is empty Relation-like non-empty empty-yielding RAT -valued complex-valued ext-real-valued real-valued natural-valued V134() V135() V136() V137() V138() V139() V140() set

{{},1} is set

K7(NAT,REAL) is Relation-like complex-valued ext-real-valued real-valued set

K6(K7(NAT,REAL)) is set

K7(NAT,COMPLEX) is Relation-like complex-valued set

K6(K7(NAT,COMPLEX)) is set

K7(COMPLEX,COMPLEX) is Relation-like complex-valued set

K6(K7(COMPLEX,COMPLEX)) is set

sin is Relation-like Function-like V27( REAL , REAL ) complex-valued ext-real-valued real-valued Element of K6(K7(REAL,REAL))

K411(REAL,sin) is V134() V135() V136() Element of K6(REAL)

cos is Relation-like Function-like V27( REAL , REAL ) complex-valued ext-real-valued real-valued Element of K6(K7(REAL,REAL))

K411(REAL,cos) is V134() V135() V136() Element of K6(REAL)

PI is non empty complex real V30() V31() V32() Element of REAL

2 * PI is non empty complex real V30() V31() V32() Element of REAL

PI / 2 is non empty complex real V30() V31() V32() Element of REAL

2 " is non empty complex real V30() V31() V32() set

PI * (2 ") is non empty complex real V30() V31() V32() set

0 is ordinal natural complex real V30() V32() integer V44() V134() V135() V136() V137() V138() V139() Element of NAT

{0} is V134() V135() V136() V137() V138() V139() set

t is complex real V30() set

c

dom c

i is complex real V30() set

i + t is complex real V30() set

i - t is complex real V30() set

- t is complex real V30() set

i + (- t) is complex real V30() set

c

c

(i - t) + t is complex real V30() set

i is complex real V30() set

i + t is complex real V30() set

i - t is complex real V30() set

- t is complex real V30() set

i + (- t) is complex real V30() set

c

c

i is complex real V30() set

i + t is complex real V30() set

c

c

(i + t) - t is complex real V30() set

- t is complex real V30() set

(i + t) + (- t) is complex real V30() set

t is complex real V30() set

c

i is Relation-like Function-like complex-valued ext-real-valued real-valued set

c

dom c

k is complex real V30() set

k + t is complex real V30() set

k - t is complex real V30() set

- t is complex real V30() set

k + (- t) is complex real V30() set

c

c

dom (c

k is complex real V30() set

k + t is complex real V30() set

k - t is complex real V30() set

- t is complex real V30() set

k + (- t) is complex real V30() set

(c

(c

dom i is set

(dom c

c

i . k is complex real V30() set

(c

c

(c

i . (k + t) is complex real V30() set

(c

t is complex real V30() set

c

REAL --> c

{c

K7(REAL,{c

K6(K7(REAL,{c

dom (REAL --> c

k is complex real V30() set

k + t is complex real V30() set

(REAL --> c

(REAL --> c

t is complex real V30() set

c

i is Relation-like Function-like complex-valued ext-real-valued real-valued set

c

- i is Relation-like Function-like complex-valued ext-real-valued real-valued set

- 1 is non empty complex real V30() V31() V32() integer set

(- 1) (#) i is Relation-like Function-like complex-valued ext-real-valued real-valued set

c

dom c

k is complex real V30() set

k + t is complex real V30() set

k - t is complex real V30() set

- t is complex real V30() set

k + (- t) is complex real V30() set

c

c

dom (c

k is complex real V30() set

k + t is complex real V30() set

k - t is complex real V30() set

- t is complex real V30() set

k + (- t) is complex real V30() set

(c

(c

dom i is set

(dom c

c

i . k is complex real V30() set

(c

- (i . k) is complex real V30() set

(c

c

(c

(c

i . (k + t) is complex real V30() set

(c

- (i . (k + t)) is complex real V30() set

(c

t is complex real V30() set

c

i is Relation-like Function-like complex-valued ext-real-valued real-valued set

c

dom c

k is complex real V30() set

k + t is complex real V30() set

k - t is complex real V30() set

- t is complex real V30() set

k + (- t) is complex real V30() set

c

c

dom (c

k is complex real V30() set

k + t is complex real V30() set

k - t is complex real V30() set

- t is complex real V30() set

k + (- t) is complex real V30() set

(c

(c

dom i is set

(dom c

c

i . k is complex real V30() set

(c

c

(c

i . (k + t) is complex real V30() set

(c

t is complex real V30() set

c

i is Relation-like Function-like complex-valued ext-real-valued real-valued set

c

i " is Relation-like Function-like complex-valued ext-real-valued real-valued set

c

dom c

k is complex real V30() set

k + t is complex real V30() set

k - t is complex real V30() set

- t is complex real V30() set

k + (- t) is complex real V30() set

c

c

dom (c

k is complex real V30() set

k + t is complex real V30() set

k - t is complex real V30() set

- t is complex real V30() set

k + (- t) is complex real V30() set

(c

(c

dom i is set

(dom c

c

i . k is complex real V30() set

(c

(i . k) " is complex real V30() set

(c

c

(c

(c

i . (k + t) is complex real V30() set

(c

(i . (k + t)) " is complex real V30() set

(c

t is complex real V30() set

c

- c

- 1 is non empty complex real V30() V31() V32() integer set

(- 1) (#) c

dom c

i is complex real V30() set

i + t is complex real V30() set

i - t is complex real V30() set

- t is complex real V30() set

i + (- t) is complex real V30() set

c

c

dom (- c

i is complex real V30() set

i + t is complex real V30() set

i - t is complex real V30() set

- t is complex real V30() set

i + (- t) is complex real V30() set

(- c

(- c

c

- (c

c

- (c

t is complex real V30() set

c

i is Relation-like Function-like complex-valued ext-real-valued real-valued set

c

dom i is set

k is complex real V30() set

k + t is complex real V30() set

k - t is complex real V30() set

- t is complex real V30() set

k + (- t) is complex real V30() set

i . k is complex real V30() set

i . (k + t) is complex real V30() set

dom (c

k is complex real V30() set

k + t is complex real V30() set

k - t is complex real V30() set

- t is complex real V30() set

k + (- t) is complex real V30() set

(c

(c

i . k is complex real V30() set

c

i . (k + t) is complex real V30() set

c

t is complex real V30() set

c

i is Relation-like Function-like complex-valued ext-real-valued real-valued set

c

dom i is set

k is complex real V30() set

k + t is complex real V30() set

k - t is complex real V30() set

- t is complex real V30() set

k + (- t) is complex real V30() set

i . k is complex real V30() set

i . (k + t) is complex real V30() set

dom (c

k is complex real V30() set

k + t is complex real V30() set

k - t is complex real V30() set

- t is complex real V30() set

k + (- t) is complex real V30() set

(c

(c

i . k is complex real V30() set

c

i . (k + t) is complex real V30() set

c

t is complex real V30() set

i is Relation-like Function-like complex-valued ext-real-valued real-valued set

c

i - c

- c

(- c

t is complex real V30() set

c

|.c

dom c

i is complex real V30() set

i + t is complex real V30() set

i - t is complex real V30() set

- t is complex real V30() set

i + (- t) is complex real V30() set

c

c

dom |.c

i is complex real V30() set

i + t is complex real V30() set

i - t is complex real V30() set

- t is complex real V30() set

i + (- t) is complex real V30() set

|.c

|.c

c

|.(c

c

|.(c

t is complex real V30() set

c

c

dom c

i is complex real V30() set

i + t is complex real V30() set

i - t is complex real V30() set

- t is complex real V30() set

i + (- t) is complex real V30() set

c

c

dom (c

i is complex real V30() set

i + t is complex real V30() set

i - t is complex real V30() set

- t is complex real V30() set

i + (- t) is complex real V30() set

(c

(c

c

(c

c

(c

t is complex real V30() set

c

c

c

t is complex real V30() set

c

dom c

i is complex real V30() set

c

i - t is complex real V30() set

- t is complex real V30() set

i + (- t) is complex real V30() set

c

i + t is complex real V30() set

(i - t) + t is complex real V30() set

c

t is complex real V30() set

- t is complex real V30() set

c

dom c

i is complex real V30() set

i + (- t) is complex real V30() set

i - (- t) is complex real V30() set

- (- t) is complex real V30() set

i + (- (- t)) is complex real V30() set

c

c

i + t is complex real V30() set

i - t is complex real V30() set

t is complex real V30() set

c

t + c

i is Relation-like Function-like complex-valued ext-real-valued real-valued set

dom i is set

k is complex real V30() set

k + (t + c

k - (t + c

- (t + c

k + (- (t + c

i . k is complex real V30() set

i . (k + (t + c

k + t is complex real V30() set

k - t is complex real V30() set

- t is complex real V30() set

k + (- t) is complex real V30() set

(k + t) + c

(k - t) - c

- c

(k - t) + (- c

i . (k + t) is complex real V30() set

i . ((k + t) + c

t is complex real V30() set

c

t - c

- c

t + (- c

i is Relation-like Function-like complex-valued ext-real-valued real-valued set

dom i is set

k is complex real V30() set

k + (t - c

k - (t - c

- (t - c

k + (- (t - c

i . k is complex real V30() set

i . (k + (t - c

k + t is complex real V30() set

k - t is complex real V30() set

- t is complex real V30() set

k + (- t) is complex real V30() set

(k + t) - c

(k + t) + (- c

(k - t) + c

k - c

k + (- c

(k - c

i . ((k - c

i . (k - c

(k - c

i . ((k - c

t is complex real V30() set

2 * t is complex real V30() Element of REAL

c

dom c

i is complex real V30() set

i + (2 * t) is complex real V30() Element of REAL

i - (2 * t) is complex real V30() Element of REAL

- (2 * t) is complex real V30() set

i + (- (2 * t)) is complex real V30() set

c

c

i + t is complex real V30() set

i - t is complex real V30() set

- t is complex real V30() set

i + (- t) is complex real V30() set

(i + t) + t is complex real V30() set

(i - t) - t is complex real V30() set

(i - t) + (- t) is complex real V30() set

c

(i + t) - t is complex real V30() set

(i + t) + (- t) is complex real V30() set

c

t is complex real V30() set

c

t + c

i is Relation-like Function-like complex-valued ext-real-valued real-valued set

dom i is set

k is complex real V30() set

k + (t + c

k - (t + c

- (t + c

k + (- (t + c

i . k is complex real V30() set

i . (k + (t + c

k + t is complex real V30() set

k - t is complex real V30() set

- t is complex real V30() set

k + (- t) is complex real V30() set

k + c

k - c

- c

k + (- c

(k + t) + c

(k - t) - c

(k - t) + (- c

(k + c

i . ((k + c

(k + c

(k + c

i . ((k + c

t is complex real V30() set

c

t - c

- c

t + (- c

i is Relation-like Function-like complex-valued ext-real-valued real-valued set

dom i is set

k is complex real V30() set

k + (t - c

k - (t - c

- (t - c

k + (- (t - c

i . k is complex real V30() set

i . (k + (t - c

k + t is complex real V30() set

k - t is complex real V30() set

- t is complex real V30() set

k + (- t) is complex real V30() set

k + c

k - c

k + (- c

(k + t) - c

(k + t) + (- c

(k - t) + c

(k - c

i . ((k - c

(k - c

i . ((k - c

t is complex real V30() set

2 * t is complex real V30() Element of REAL

c

dom c

i is complex real V30() set

i + (2 * t) is complex real V30() Element of REAL

i - (2 * t) is complex real V30() Element of REAL

- (2 * t) is complex real V30() set

i + (- (2 * t)) is complex real V30() set

c

c

i + t is complex real V30() set

i - t is complex real V30() set

- t is complex real V30() set

i + (- t) is complex real V30() set

(i + t) + t is complex real V30() set

(i - t) - t is complex real V30() set

(i - t) + (- t) is complex real V30() set

c

c

(c

(c

((c

dom sin is set

t is complex real V30() set

t + (2 * PI) is complex real V30() Element of REAL

t - (2 * PI) is complex real V30() Element of REAL

- (2 * PI) is non empty complex real V30() V31() V32() set

t + (- (2 * PI)) is complex real V30() set

sin . t is complex real V30() set

sin . (t + (2 * PI)) is complex real V30() Element of REAL

t is non empty complex real V30() set

REAL --> t is non empty Relation-like non-empty REAL -defined Function-like constant total V27( REAL ,{t}) complex-valued ext-real-valued real-valued Element of K6(K7(REAL,{t}))

{t} is V134() V135() V136() set

K7(REAL,{t}) is Relation-like complex-valued ext-real-valued real-valued set

K6(K7(REAL,{t})) is set

t is non empty complex real V30() set

c

i is Relation-like Function-like complex-valued ext-real-valued real-valued (t) set

c

c

- i is Relation-like Function-like complex-valued ext-real-valued real-valued set

- 1 is non empty complex real V30() V31() V32() integer set

(- 1) (#) i is Relation-like Function-like complex-valued ext-real-valued real-valued set

c

c

c

i " is Relation-like Function-like complex-valued ext-real-valued real-valued set

c

t is Relation-like Function-like complex-valued ext-real-valued real-valued () set

- t is Relation-like Function-like complex-valued ext-real-valued real-valued set

(- 1) (#) t is Relation-like Function-like complex-valued ext-real-valued real-valued set

c

t is Relation-like Function-like complex-valued ext-real-valued real-valued () set

c

c

i is complex real V30() set

c

i is complex real V30() set

t - c

- c

(- c

t is Relation-like Function-like complex-valued ext-real-valued real-valued () set

|.t.| is Relation-like Function-like complex-valued ext-real-valued real-valued set

c

t " is Relation-like Function-like complex-valued ext-real-valued real-valued set

c

t ^2 is Relation-like Function-like complex-valued ext-real-valued real-valued set

t (#) t is Relation-like Function-like complex-valued ext-real-valued real-valued set

c

dom cos is set

t is complex real V30() set

t + (2 * PI) is complex real V30() Element of REAL

t - (2 * PI) is complex real V30() Element of REAL

- (2 * PI) is non empty complex real V30() V31() V32() set

t + (- (2 * PI)) is complex real V30() set

cos . t is complex real V30() set

cos . (t + (2 * PI)) is complex real V30() Element of REAL

t is ordinal natural complex real V30() V32() integer set

t + 1 is non empty ordinal natural complex real V30() V31() V32() integer Element of REAL

(2 * PI) * (t + 1) is non empty complex real V30() V31() V32() Element of REAL

0 + 1 is non empty ordinal natural complex real V30() V31() V32() integer Element of REAL

(2 * PI) * (0 + 1) is non empty complex real V30() V31() V32() Element of REAL

c

c

(2 * PI) * (c

(c

(2 * PI) * ((c

(c

(2 * PI) * ((c

dom sin is set

i is complex real V30() set

sin . i is complex real V30() set

i + ((2 * PI) * ((c

sin . (i + ((2 * PI) * ((c

i + ((2 * PI) * (c

sin . (i + ((2 * PI) * (c

(i + ((2 * PI) * (c

sin . ((i + ((2 * PI) * (c

i is complex real V30() set

i + ((2 * PI) * ((c

i - ((2 * PI) * ((c

- ((2 * PI) * ((c

i + (- ((2 * PI) * ((c

sin . i is complex real V30() set

sin . (i + ((2 * PI) * ((c

t is non empty complex real V30() integer set

(2 * PI) * t is non empty complex real V30() Element of REAL

c

- c

i is ordinal natural complex real V30() V32() integer set

i + 1 is non empty ordinal natural complex real V30() V31() V32() integer Element of REAL

- t is non empty complex real V30() integer set

i is ordinal natural complex real V30() V32() integer set

i + 1 is non empty ordinal natural complex real V30() V31() V32() integer Element of REAL

(2 * PI) * (i + 1) is non empty complex real V30() V31() V32() Element of REAL

- ((2 * PI) * (i + 1)) is non empty complex real V30() V31() V32() Element of REAL

t is ordinal natural complex real V30() V32() integer set

t + 1 is non empty ordinal natural complex real V30() V31() V32() integer Element of REAL

(2 * PI) * (t + 1) is non empty complex real V30() V31() V32() Element of REAL

0 + 1 is non empty ordinal natural complex real V30() V31() V32() integer Element of REAL

(2 * PI) * (0 + 1) is non empty complex real V30() V31() V32() Element of REAL

c

c

(2 * PI) * (c

(c

(2 * PI) * ((c

(c

(2 * PI) * ((c

dom cos is set

i is complex real V30() set

cos . i is complex real V30() set

i + ((2 * PI) * ((c

cos . (i + ((2 * PI) * ((c

i + ((2 * PI) * (c

cos . (i + ((2 * PI) * (c

(i + ((2 * PI) * (c

cos . ((i + ((2 * PI) * (c

i is complex real V30() set

i + ((2 * PI) * ((c

i - ((2 * PI) * ((c

- ((2 * PI) * ((c

i + (- ((2 * PI) * ((c

cos . i is complex real V30() set

cos . (i + ((2 * PI) * ((c

t is non empty complex real V30() integer set

(2 * PI) * t is non empty complex real V30() Element of REAL

c

- c

i is ordinal natural complex real V30() V32() integer set

i + 1 is non empty ordinal natural complex real V30() V31() V32() integer Element of REAL

- t is non empty complex real V30() integer set

i is ordinal natural complex real V30() V32() integer set

i + 1 is non empty ordinal natural complex real V30() V31() V32() integer Element of REAL

(2 * PI) * (i + 1) is non empty complex real V30() V31() V32() Element of REAL

- ((2 * PI) * (i + 1)) is non empty complex real V30() V31() V32() Element of REAL

cosec is Relation-like Function-like complex-valued ext-real-valued real-valued Element of K6(K7(REAL,REAL))

K375(REAL,REAL,sin) is Relation-like Function-like complex-valued ext-real-valued real-valued Element of K6(K7(REAL,REAL))

dom cosec is set

t is complex real V30() set

t + (2 * PI) is complex real V30() Element of REAL

t - (2 * PI) is complex real V30() Element of REAL

- (2 * PI) is non empty complex real V30() V31() V32() set

t + (- (2 * PI)) is complex real V30() set

cosec . t is complex real V30() set

cosec . (t + (2 * PI)) is complex real V30() set

dom sin is set

sin " {0} is set

(dom sin) \ (sin " {0}) is Element of K6((dom sin))

K6((dom sin)) is set

sin . t is complex real V30() set

sin . (t + (2 * PI)) is complex real V30() Element of REAL

sin . (t - (2 * PI)) is complex real V30() Element of REAL

(t - (2 * PI)) + (2 * PI) is complex real V30() Element of REAL

sin . ((t - (2 * PI)) + (2 * PI)) is complex real V30() Element of REAL

(sin . (t + (2 * PI))) " is complex real V30() Element of REAL

(sin . t) " is complex real V30() set

sec is Relation-like Function-like complex-valued ext-real-valued real-valued Element of K6(K7(REAL,REAL))

K375(REAL,REAL,cos) is Relation-like Function-like complex-valued ext-real-valued real-valued Element of K6(K7(REAL,REAL))

dom sec is set

t is complex real V30() set

t + (2 * PI) is complex real V30() Element of REAL

t - (2 * PI) is complex real V30() Element of REAL

- (2 * PI) is non empty complex real V30() V31() V32() set

t + (- (2 * PI)) is complex real V30() set

sec . t is complex real V30() set

sec . (t + (2 * PI)) is complex real V30() set

dom cos is set

cos " {0} is set

(dom cos) \ (cos " {0}) is Element of K6((dom cos))

K6((dom cos)) is set

cos . t is complex real V30() set

cos . (t + (2 * PI)) is complex real V30() Element of REAL

cos . (t - (2 * PI)) is complex real V30() Element of REAL

(t - (2 * PI)) + (2 * PI) is complex real V30() Element of REAL

cos . ((t - (2 * PI)) + (2 * PI)) is complex real V30() Element of REAL

(cos . (t + (2 * PI))) " is complex real V30() Element of REAL

(cos . t) " is complex real V30() set

t is ordinal natural complex real V30() V32() integer set

t + 1 is non empty ordinal natural complex real V30() V31() V32() integer Element of REAL

(2 * PI) * (t + 1) is non empty complex real V30() V31() V32() Element of REAL

0 + 1 is non empty ordinal natural complex real V30() V31() V32() integer Element of REAL

(2 * PI) * (0 + 1) is non empty complex real V30() V31() V32() Element of REAL

c

c

(2 * PI) * (c

(c

(2 * PI) * ((c

(c

(2 * PI) * ((c

dom sec is set

i is complex real V30() set

i + ((2 * PI) * ((c

i - ((2 * PI) * ((c

- ((2 * PI) * ((c

i + (- ((2 * PI) * ((c

sec . i is complex real V30() set

sec . (i + ((2 * PI) * ((c

i + ((2 * PI) * (c

i - ((2 * PI) * (c

- ((2 * PI) * (c

i + (- ((2 * PI) * (c

sec . (i + ((2 * PI) * (c

dom cos is set

cos " {0} is set

(dom cos) \ (cos " {0}) is Element of K6((dom cos))

K6((dom cos)) is set

cos . (i + ((2 * PI) * (c

cos . (i - ((2 * PI) * (c

(i + ((2 * PI) * (c

cos . ((i + ((2 * PI) * (c

cos . (i - ((2 * PI) * ((c

(i - ((2 * PI) * ((c

cos . ((i - ((2 * PI) * ((c

(cos . ((i + ((2 * PI) * (c

(cos . (i + ((2 * PI) * (c

t is non empty complex real V30() integer set

(2 * PI) * t is non empty complex real V30() Element of REAL

c

- c

i is ordinal natural complex real V30() V32() integer set

i + 1 is non empty ordinal natural complex real V30() V31() V32() integer Element of REAL

- t is non empty complex real V30() integer set

i is ordinal natural complex real V30() V32() integer set

i + 1 is non empty ordinal natural complex real V30() V31() V32() integer Element of REAL

(2 * PI) * (i + 1) is non empty complex real V30() V31() V32() Element of REAL

- ((2 * PI) * (i + 1)) is non empty complex real V30() V31() V32() Element of REAL

t is ordinal natural complex real V30() V32() integer set

t + 1 is non empty ordinal natural complex real V30() V31() V32() integer Element of REAL

(2 * PI) * (t + 1) is non empty complex real V30() V31() V32() Element of REAL

0 + 1 is non empty ordinal natural complex real V30() V31() V32() integer Element of REAL

(2 * PI) * (0 + 1) is non empty complex real V30() V31() V32() Element of REAL

c

c

(2 * PI) * (c

(c

(2 * PI) * ((c

(c

(2 * PI) * ((c

dom cosec is set

i is complex real V30() set

i + ((2 * PI) * ((c

i - ((2 * PI) * ((c

- ((2 * PI) * ((c

i + (- ((2 * PI) * ((c

cosec . i is complex real V30() set

cosec . (i + ((2 * PI) * ((c

i + ((2 * PI) * (c

i - ((2 * PI) * (c

- ((2 * PI) * (c

i + (- ((2 * PI) * (c

cosec . (i + ((2 * PI) * (c

dom sin is set

sin " {0} is set

(dom sin) \ (sin " {0}) is Element of K6((dom sin))

K6((dom sin)) is set

sin . (i + ((2 * PI) * (c

sin . (i - ((2 * PI) * (c

(i + ((2 * PI) * (c

sin . ((i + ((2 * PI) * (c

sin . (i - ((2 * PI) * ((c

(i - ((2 * PI) * ((c

sin . ((i - ((2 * PI) * ((c

(sin . ((i + ((2 * PI) * (c

(sin . (i + ((2 * PI) * (c

t is non empty complex real V30() integer set

(2 * PI) * t is non empty complex real V30() Element of REAL

c

- c

i is ordinal natural complex real V30() V32() integer set

i + 1 is non empty ordinal natural complex real V30() V31() V32() integer Element of REAL

- t is non empty complex real V30() integer set

i is ordinal natural complex real V30() V32() integer set

i + 1 is non empty ordinal natural complex real V30() V31() V32() integer Element of REAL

(2 * PI) * (i + 1) is non empty complex real V30() V31() V32() Element of REAL

- ((2 * PI) * (i + 1)) is non empty complex real V30() V31() V32() Element of REAL

tan is Relation-like Function-like complex-valued ext-real-valued real-valued Element of K6(K7(REAL,REAL))

K372(REAL,REAL,sin,cos) is Relation-like Function-like complex-valued ext-real-valued real-valued Element of K6(K7(REAL,REAL))

dom tan is set

t is complex real V30() set

t + PI is complex real V30() Element of REAL

t - PI is complex real V30() Element of REAL

- PI is non empty complex real V30() V31() V32() set

t + (- PI) is complex real V30() set

tan . t is complex real V30() set

tan . (t + PI) is complex real V30() set

dom cos is set

dom sin is set

cos " {0} is set

(dom cos) \ (cos " {0}) is Element of K6((dom cos))

K6((dom cos)) is set

(dom sin) /\ ((dom cos) \ (cos " {0})) is Element of K6((dom cos))

cos . t is complex real V30() set

cos . (t + PI) is complex real V30() Element of REAL

- (cos . t) is complex real V30() set

cos . (t - PI) is complex real V30() Element of REAL

(t - PI) + (2 * PI) is complex real V30() Element of REAL

cos . ((t - PI) + (2 * PI)) is complex real V30() Element of REAL

sin . (t + PI) is complex real V30() Element of REAL

(sin . (t + PI)) / (cos . (t + PI)) is complex real V30() Element of REAL

(cos . (t + PI)) " is complex real V30() set

(sin . (t + PI)) * ((cos . (t + PI)) ") is complex real V30() set

sin . t is complex real V30() set

- (sin . t) is complex real V30() set

(- (sin . t)) / (cos . (t + PI)) is complex real V30() Element of REAL

(- (sin . t)) * ((cos . (t + PI)) ") is complex real V30() set

(- (sin . t)) / (- (cos . t)) is complex real V30() set

(- (cos . t)) " is complex real V30() set

(- (sin . t)) * ((- (cos . t)) ") is complex real V30() set

(sin . t) / (cos . t) is complex real V30() set

(cos . t) " is complex real V30() set

(sin . t) * ((cos . t) ") is complex real V30() set

cot is Relation-like Function-like complex-valued ext-real-valued real-valued Element of K6(K7(REAL,REAL))

K372(REAL,REAL,cos,sin) is Relation-like Function-like complex-valued ext-real-valued real-valued Element of K6(K7(REAL,REAL))

dom cot is set

t is complex real V30() set

t + PI is complex real V30() Element of REAL

t - PI is complex real V30() Element of REAL

- PI is non empty complex real V30() V31() V32() set

t + (- PI) is complex real V30() set

cot . t is complex real V30() set

cot . (t + PI) is complex real V30() set

dom sin is set

dom cos is set

sin " {0} is set

(dom sin) \ (sin " {0}) is Element of K6((dom sin))

K6((dom sin)) is set

(dom cos) /\ ((dom sin) \ (sin " {0})) is Element of K6((dom sin))

sin . t is complex real V30() set

sin . (t + PI) is complex real V30() Element of REAL

- (sin . t) is complex real V30() set

sin . (t - PI) is complex real V30() Element of REAL

(t - PI) + (2 * PI) is complex real V30() Element of REAL

sin . ((t - PI) + (2 * PI)) is complex real V30() Element of REAL

cos . (t + PI) is complex real V30() Element of REAL

(cos . (t + PI)) / (sin . (t + PI)) is complex real V30() Element of REAL

(sin . (t + PI)) " is complex real V30() set

(cos . (t + PI)) * ((sin . (t + PI)) ") is complex real V30() set

cos . t is complex real V30() set

- (cos . t) is complex real V30() set

(- (cos . t)) / (sin . (t + PI)) is complex real V30() Element of REAL

(- (cos . t)) * ((sin . (t + PI)) ") is complex real V30() set

(- (cos . t)) / (- (sin . t)) is complex real V30() set

(- (sin . t)) " is complex real V30() set

(- (cos . t)) * ((- (sin . t)) ") is complex real V30() set

(cos . t) / (sin . t) is complex real V30() set

(sin . t) " is complex real V30() set

(cos . t) * ((sin . t) ") is complex real V30() set

t is ordinal natural complex real V30() V32() integer set

t + 1 is non empty ordinal natural complex real V30() V31() V32() integer Element of REAL

PI * (t + 1) is non empty complex real V30() V31() V32() Element of REAL

0 + 1 is non empty ordinal natural complex real V30() V31() V32() integer Element of REAL

PI * (0 + 1) is non empty complex real V30() V31() V32() Element of REAL

c

c

PI * (c

(c

PI * ((c

(c

PI * ((c

dom tan is set

i is complex real V30() set

i + (PI * ((c

i - (PI * ((c

- (PI * ((c

i + (- (PI * ((c

tan . i is complex real V30() set

tan . (i + (PI * ((c

i + (PI * (c

i - (PI * (c

- (PI * (c

i + (- (PI * (c

tan . (i + (PI * (c

dom cos is set

dom sin is set

cos " {0} is set

(dom cos) \ (cos " {0}) is Element of K6((dom cos))

K6((dom cos)) is set

(dom sin) /\ ((dom cos) \ (cos " {0})) is Element of K6((dom cos))

cos . (i + (PI * (c

cos . (i - (PI * (c

(i + (PI * (c

cos . ((i + (PI * (c

- (cos . (i + (PI * (c

(i - (PI * ((c

cos . ((i - (PI * ((c

cos . (i - (PI * ((c

- (cos . (i - (PI * ((c

- (cos . (i - (PI * (c

sin . ((i + (PI * (c

(sin . ((i + (PI * (c

(cos . ((i + (PI * (c

(sin . ((i + (PI * (c

sin . (i + (PI * (c

- (sin . (i + (PI * (c

(- (sin . (i + (PI * (c

(- (sin . (i + (PI * (c

(- (sin . (i + (PI * (c

(- (cos . (i + (PI * (c

(- (sin . (i + (PI * (c

(sin . (i + (PI * (c

(cos . (i + (PI * (c

(sin . (i + (PI * (c

t is non empty complex real V30() integer set

PI * t is non empty complex real V30() Element of REAL

c

- c

i is ordinal natural complex real V30() V32() integer set

i + 1 is non empty ordinal natural complex real V30() V31() V32() integer Element of REAL

- t is non empty complex real V30() integer set

i is ordinal natural complex real V30() V32() integer set

i + 1 is non empty ordinal natural complex real V30() V31() V32() integer Element of REAL

PI * (i + 1) is non empty complex real V30() V31() V32() Element of REAL

- (PI * (i + 1)) is non empty complex real V30() V31() V32() Element of REAL

t is ordinal natural complex real V30() V32() integer set

t + 1 is non empty ordinal natural complex real V30() V31() V32() integer Element of REAL

PI * (t + 1) is non empty complex real V30() V31() V32() Element of REAL

0 + 1 is non empty ordinal natural complex real V30() V31() V32() integer Element of REAL

PI * (0 + 1) is non empty complex real V30() V31() V32() Element of REAL

c

c

PI * (c

(c

PI * ((c

(c

PI * ((c

dom cot is set

i is complex real V30() set

i + (PI * ((c

i - (PI * ((c

- (PI * ((c

i + (- (PI * ((c

cot . i is complex real V30() set

cot . (i + (PI * ((c

i + (PI * (c

i - (PI * (c

- (PI * (c

i + (- (PI * (c

cot . (i + (PI * (c

dom sin is set

dom cos is set

sin " {0} is set

(dom sin) \ (sin " {0}) is Element of K6((dom sin))

K6((dom sin)) is set

(dom cos) /\ ((dom sin) \ (sin " {0})) is Element of K6((dom sin))

sin . (i + (PI * (c

sin . (i - (PI * (c

(i + (PI