:: FUNCT_9 semantic presentation

begin

definition
let t be ( ( real ) ( complex real V30() ) number ) ;
let F be ( ( Relation-like Function-like ) ( Relation-like Function-like ) Function) ;
attr F is t -periodic means :: FUNCT_9:def 1
( t : ( ( ) ( complex real V30() ) Element of REAL : ( ( ) ( non empty V45() V134() V135() V136() V140() ) set ) ) <> 0 : ( ( ) ( ordinal natural complex real V30() V32() integer V44() V134() V135() V136() V137() V138() V139() ) Element of NAT : ( ( ) ( V134() V135() V136() V137() V138() V139() V140() ) Element of K6(REAL : ( ( ) ( non empty V45() V134() V135() V136() V140() ) set ) ) : ( ( ) ( ) set ) ) ) & ( for x being ( ( real ) ( complex real V30() ) number ) holds
( ( x : ( ( real ) ( complex real V30() ) number ) in dom F : ( ( integer ) ( complex real V30() integer ) set ) : ( ( ) ( ) set ) implies x : ( ( real ) ( complex real V30() ) number ) + t : ( ( ) ( complex real V30() ) Element of REAL : ( ( ) ( non empty V45() V134() V135() V136() V140() ) set ) ) : ( ( ) ( complex real V30() ) set ) in dom F : ( ( integer ) ( complex real V30() integer ) set ) : ( ( ) ( ) set ) ) & ( x : ( ( real ) ( complex real V30() ) number ) + t : ( ( ) ( complex real V30() ) Element of REAL : ( ( ) ( non empty V45() V134() V135() V136() V140() ) set ) ) : ( ( ) ( complex real V30() ) set ) in dom F : ( ( integer ) ( complex real V30() integer ) set ) : ( ( ) ( ) set ) implies x : ( ( real ) ( complex real V30() ) number ) in dom F : ( ( integer ) ( complex real V30() integer ) set ) : ( ( ) ( ) set ) ) & ( x : ( ( real ) ( complex real V30() ) number ) in dom F : ( ( integer ) ( complex real V30() integer ) set ) : ( ( ) ( ) set ) implies F : ( ( integer ) ( complex real V30() integer ) set ) . x : ( ( real ) ( complex real V30() ) number ) : ( ( ) ( ) set ) = F : ( ( integer ) ( complex real V30() integer ) set ) . (x : ( ( real ) ( complex real V30() ) number ) + t : ( ( ) ( complex real V30() ) Element of REAL : ( ( ) ( non empty V45() V134() V135() V136() V140() ) set ) ) ) : ( ( ) ( complex real V30() ) set ) : ( ( ) ( ) set ) ) ) ) );
end;

definition
let F be ( ( Relation-like Function-like ) ( Relation-like Function-like ) Function) ;
attr F is periodic means :: FUNCT_9:def 2
 ex t being ( ( real ) ( complex real V30() ) number ) st F : ( ( ) ( complex real V30() ) Element of REAL : ( ( ) ( non empty V45() V134() V135() V136() V140() ) set ) ) is t : ( ( real ) ( complex real V30() ) number ) -periodic ;
end;

theorem :: FUNCT_9:1
for t being ( ( real ) ( complex real V30() ) number )
for F being ( ( Relation-like Function-like real-valued ) ( Relation-like Function-like complex-valued ext-real-valued real-valued ) Function) holds
( F : ( ( Relation-like Function-like real-valued ) ( Relation-like Function-like complex-valued ext-real-valued real-valued ) Function) is t : ( ( real ) ( complex real V30() ) number ) -periodic iff ( t : ( ( real ) ( complex real V30() ) number ) <> 0 : ( ( ) ( ordinal natural complex real V30() V32() integer V44() V134() V135() V136() V137() V138() V139() ) Element of NAT : ( ( ) ( V134() V135() V136() V137() V138() V139() V140() ) Element of K6(REAL : ( ( ) ( non empty V45() V134() V135() V136() V140() ) set ) ) : ( ( ) ( ) set ) ) ) & ( for x being ( ( real ) ( complex real V30() ) number ) st x : ( ( real ) ( complex real V30() ) number ) in dom F : ( ( Relation-like Function-like real-valued ) ( Relation-like Function-like complex-valued ext-real-valued real-valued ) Function) : ( ( ) ( ) set ) holds
( x : ( ( real ) ( complex real V30() ) number ) + t : ( ( real ) ( complex real V30() ) number ) : ( ( ) ( complex real V30() ) set ) in dom F : ( ( Relation-like Function-like real-valued ) ( Relation-like Function-like complex-valued ext-real-valued real-valued ) Function) : ( ( ) ( ) set ) & x : ( ( real ) ( complex real V30() ) number ) - t : ( ( real ) ( complex real V30() ) number ) : ( ( ) ( complex real V30() ) set ) in dom F : ( ( Relation-like Function-like real-valued ) ( Relation-like Function-like complex-valued ext-real-valued real-valued ) Function) : ( ( ) ( ) set ) & F : ( ( Relation-like Function-like real-valued ) ( Relation-like Function-like complex-valued ext-real-valued real-valued ) Function) . x : ( ( real ) ( complex real V30() ) number ) : ( ( ) ( complex real V30() ) set ) = F : ( ( Relation-like Function-like real-valued ) ( Relation-like Function-like complex-valued ext-real-valued real-valued ) Function) . (x : ( ( real ) ( complex real V30() ) number ) + t : ( ( real ) ( complex real V30() ) number ) ) : ( ( ) ( complex real V30() ) set ) : ( ( ) ( complex real V30() ) set ) ) ) ) ) ;

theorem :: FUNCT_9:2
for t being ( ( real ) ( complex real V30() ) number )
for F, G being ( ( Relation-like Function-like real-valued ) ( Relation-like Function-like complex-valued ext-real-valued real-valued ) Function) st F : ( ( Relation-like Function-like real-valued ) ( Relation-like Function-like complex-valued ext-real-valued real-valued ) Function) is t : ( ( real ) ( complex real V30() ) number ) -periodic & G : ( ( Relation-like Function-like real-valued ) ( Relation-like Function-like complex-valued ext-real-valued real-valued ) Function) is t : ( ( real ) ( complex real V30() ) number ) -periodic holds
F : ( ( Relation-like Function-like real-valued ) ( Relation-like Function-like complex-valued ext-real-valued real-valued ) Function) + G : ( ( Relation-like Function-like real-valued ) ( Relation-like Function-like complex-valued ext-real-valued real-valued ) Function) : ( ( Relation-like Function-like ) ( Relation-like Function-like complex-valued ext-real-valued real-valued ) set ) is t : ( ( real ) ( complex real V30() ) number ) -periodic ;

theorem :: FUNCT_9:3
for t being ( ( real ) ( complex real V30() ) number )
for F, G being ( ( Relation-like Function-like real-valued ) ( Relation-like Function-like complex-valued ext-real-valued real-valued ) Function) st F : ( ( Relation-like Function-like real-valued ) ( Relation-like Function-like complex-valued ext-real-valued real-valued ) Function) is t : ( ( real ) ( complex real V30() ) number ) -periodic & G : ( ( Relation-like Function-like real-valued ) ( Relation-like Function-like complex-valued ext-real-valued real-valued ) Function) is t : ( ( real ) ( complex real V30() ) number ) -periodic holds
F : ( ( Relation-like Function-like real-valued ) ( Relation-like Function-like complex-valued ext-real-valued real-valued ) Function) - G : ( ( Relation-like Function-like real-valued ) ( Relation-like Function-like complex-valued ext-real-valued real-valued ) Function) : ( ( Relation-like Function-like ) ( Relation-like Function-like complex-valued ext-real-valued real-valued ) set ) is t : ( ( real ) ( complex real V30() ) number ) -periodic ;

theorem :: FUNCT_9:4
for t being ( ( real ) ( complex real V30() ) number )
for F, G being ( ( Relation-like Function-like real-valued ) ( Relation-like Function-like complex-valued ext-real-valued real-valued ) Function) st F : ( ( Relation-like Function-like real-valued ) ( Relation-like Function-like complex-valued ext-real-valued real-valued ) Function) is t : ( ( real ) ( complex real V30() ) number ) -periodic & G : ( ( Relation-like Function-like real-valued ) ( Relation-like Function-like complex-valued ext-real-valued real-valued ) Function) is t : ( ( real ) ( complex real V30() ) number ) -periodic holds
F : ( ( Relation-like Function-like real-valued ) ( Relation-like Function-like complex-valued ext-real-valued real-valued ) Function) (#) G : ( ( Relation-like Function-like real-valued ) ( Relation-like Function-like complex-valued ext-real-valued real-valued ) Function) : ( ( Relation-like Function-like ) ( Relation-like Function-like complex-valued ext-real-valued real-valued ) set ) is t : ( ( real ) ( complex real V30() ) number ) -periodic ;

theorem :: FUNCT_9:5
for t being ( ( real ) ( complex real V30() ) number )
for F, G being ( ( Relation-like Function-like real-valued ) ( Relation-like Function-like complex-valued ext-real-valued real-valued ) Function) st F : ( ( Relation-like Function-like real-valued ) ( Relation-like Function-like complex-valued ext-real-valued real-valued ) Function) is t : ( ( real ) ( complex real V30() ) number ) -periodic & G : ( ( Relation-like Function-like real-valued ) ( Relation-like Function-like complex-valued ext-real-valued real-valued ) Function) is t : ( ( real ) ( complex real V30() ) number ) -periodic holds
F : ( ( Relation-like Function-like real-valued ) ( Relation-like Function-like complex-valued ext-real-valued real-valued ) Function) /" G : ( ( Relation-like Function-like real-valued ) ( Relation-like Function-like complex-valued ext-real-valued real-valued ) Function) : ( ( Relation-like Function-like ) ( Relation-like Function-like complex-valued ext-real-valued real-valued ) set ) is t : ( ( real ) ( complex real V30() ) number ) -periodic ;

theorem :: FUNCT_9:6
for t being ( ( real ) ( complex real V30() ) number )
for F being ( ( Relation-like Function-like real-valued ) ( Relation-like Function-like complex-valued ext-real-valued real-valued ) Function) st F : ( ( Relation-like Function-like real-valued ) ( Relation-like Function-like complex-valued ext-real-valued real-valued ) Function) is t : ( ( real ) ( complex real V30() ) number ) -periodic holds
- F : ( ( Relation-like Function-like real-valued ) ( Relation-like Function-like complex-valued ext-real-valued real-valued ) Function) : ( ( Relation-like Function-like complex-valued ) ( Relation-like Function-like complex-valued ext-real-valued real-valued ) set ) is t : ( ( real ) ( complex real V30() ) number ) -periodic ;

theorem :: FUNCT_9:7
for t, r being ( ( real ) ( complex real V30() ) number )
for F being ( ( Relation-like Function-like real-valued ) ( Relation-like Function-like complex-valued ext-real-valued real-valued ) Function) st F : ( ( Relation-like Function-like real-valued ) ( Relation-like Function-like complex-valued ext-real-valued real-valued ) Function) is t : ( ( real ) ( complex real V30() ) number ) -periodic holds
r : ( ( real ) ( complex real V30() ) number ) (#) F : ( ( Relation-like Function-like real-valued ) ( Relation-like Function-like complex-valued ext-real-valued real-valued ) Function) : ( ( Relation-like Function-like ) ( Relation-like Function-like complex-valued ext-real-valued real-valued ) set ) is t : ( ( real ) ( complex real V30() ) number ) -periodic ;

theorem :: FUNCT_9:8
for t, r being ( ( real ) ( complex real V30() ) number )
for F being ( ( Relation-like Function-like real-valued ) ( Relation-like Function-like complex-valued ext-real-valued real-valued ) Function) st F : ( ( Relation-like Function-like real-valued ) ( Relation-like Function-like complex-valued ext-real-valued real-valued ) Function) is t : ( ( real ) ( complex real V30() ) number ) -periodic holds
r : ( ( real ) ( complex real V30() ) number ) + F : ( ( Relation-like Function-like real-valued ) ( Relation-like Function-like complex-valued ext-real-valued real-valued ) Function) : ( ( Relation-like Function-like ) ( Relation-like Function-like complex-valued ext-real-valued real-valued ) set ) is t : ( ( real ) ( complex real V30() ) number ) -periodic ;

theorem :: FUNCT_9:9
for t, r being ( ( real ) ( complex real V30() ) number )
for F being ( ( Relation-like Function-like real-valued ) ( Relation-like Function-like complex-valued ext-real-valued real-valued ) Function) st F : ( ( Relation-like Function-like real-valued ) ( Relation-like Function-like complex-valued ext-real-valued real-valued ) Function) is t : ( ( real ) ( complex real V30() ) number ) -periodic holds
F : ( ( Relation-like Function-like real-valued ) ( Relation-like Function-like complex-valued ext-real-valued real-valued ) Function) - r : ( ( real ) ( complex real V30() ) number ) : ( ( Relation-like Function-like ) ( Relation-like Function-like complex-valued ext-real-valued real-valued ) set ) is t : ( ( real ) ( complex real V30() ) number ) -periodic ;

theorem :: FUNCT_9:10
for t being ( ( real ) ( complex real V30() ) number )
for F being ( ( Relation-like Function-like real-valued ) ( Relation-like Function-like complex-valued ext-real-valued real-valued ) Function) st F : ( ( Relation-like Function-like real-valued ) ( Relation-like Function-like complex-valued ext-real-valued real-valued ) Function) is t : ( ( real ) ( complex real V30() ) number ) -periodic holds
|.F : ( ( Relation-like Function-like real-valued ) ( Relation-like Function-like complex-valued ext-real-valued real-valued ) Function) .| : ( ( Relation-like Function-like real-valued ) ( Relation-like Function-like complex-valued ext-real-valued real-valued ) set ) is t : ( ( real ) ( complex real V30() ) number ) -periodic ;

theorem :: FUNCT_9:11
for t being ( ( real ) ( complex real V30() ) number )
for F being ( ( Relation-like Function-like real-valued ) ( Relation-like Function-like complex-valued ext-real-valued real-valued ) Function) st F : ( ( Relation-like Function-like real-valued ) ( Relation-like Function-like complex-valued ext-real-valued real-valued ) Function) is t : ( ( real ) ( complex real V30() ) number ) -periodic holds
F : ( ( Relation-like Function-like real-valued ) ( Relation-like Function-like complex-valued ext-real-valued real-valued ) Function) " : ( ( Relation-like Function-like complex-valued ) ( Relation-like Function-like complex-valued ext-real-valued real-valued ) set ) is t : ( ( real ) ( complex real V30() ) number ) -periodic ;

theorem :: FUNCT_9:12
for t being ( ( real ) ( complex real V30() ) number )
for F being ( ( Relation-like Function-like real-valued ) ( Relation-like Function-like complex-valued ext-real-valued real-valued ) Function) st F : ( ( Relation-like Function-like real-valued ) ( Relation-like Function-like complex-valued ext-real-valued real-valued ) Function) is t : ( ( real ) ( complex real V30() ) number ) -periodic holds
F : ( ( Relation-like Function-like real-valued ) ( Relation-like Function-like complex-valued ext-real-valued real-valued ) Function) ^2 : ( ( Relation-like Function-like ) ( Relation-like Function-like complex-valued ext-real-valued real-valued ) set ) is t : ( ( real ) ( complex real V30() ) number ) -periodic ;

theorem :: FUNCT_9:13
for t being ( ( real ) ( complex real V30() ) number )
for F being ( ( Relation-like Function-like real-valued ) ( Relation-like Function-like complex-valued ext-real-valued real-valued ) Function) st F : ( ( Relation-like Function-like real-valued ) ( Relation-like Function-like complex-valued ext-real-valued real-valued ) Function) is t : ( ( real ) ( complex real V30() ) number ) -periodic holds
for x being ( ( real ) ( complex real V30() ) number ) st x : ( ( real ) ( complex real V30() ) number ) in dom F : ( ( Relation-like Function-like real-valued ) ( Relation-like Function-like complex-valued ext-real-valued real-valued ) Function) : ( ( ) ( ) set ) holds
F : ( ( Relation-like Function-like real-valued ) ( Relation-like Function-like complex-valued ext-real-valued real-valued ) Function) . x : ( ( real ) ( complex real V30() ) number ) : ( ( ) ( complex real V30() ) set ) = F : ( ( Relation-like Function-like real-valued ) ( Relation-like Function-like complex-valued ext-real-valued real-valued ) Function) . (x : ( ( real ) ( complex real V30() ) number ) - t : ( ( real ) ( complex real V30() ) number ) ) : ( ( ) ( complex real V30() ) set ) : ( ( ) ( complex real V30() ) set ) ;

theorem :: FUNCT_9:14
for t being ( ( real ) ( complex real V30() ) number )
for F being ( ( Relation-like Function-like real-valued ) ( Relation-like Function-like complex-valued ext-real-valued real-valued ) Function) st F : ( ( Relation-like Function-like real-valued ) ( Relation-like Function-like complex-valued ext-real-valued real-valued ) Function) is t : ( ( real ) ( complex real V30() ) number ) -periodic holds
F : ( ( Relation-like Function-like real-valued ) ( Relation-like Function-like complex-valued ext-real-valued real-valued ) Function) is - t : ( ( real ) ( complex real V30() ) number ) : ( ( complex ) ( complex real V30() ) set ) -periodic ;

theorem :: FUNCT_9:15
for t1, t2 being ( ( real ) ( complex real V30() ) number )
for F being ( ( Relation-like Function-like real-valued ) ( Relation-like Function-like complex-valued ext-real-valued real-valued ) Function) st F : ( ( Relation-like Function-like real-valued ) ( Relation-like Function-like complex-valued ext-real-valued real-valued ) Function) is t1 : ( ( real ) ( complex real V30() ) number ) -periodic & F : ( ( Relation-like Function-like real-valued ) ( Relation-like Function-like complex-valued ext-real-valued real-valued ) Function) is t2 : ( ( real ) ( complex real V30() ) number ) -periodic & t1 : ( ( real ) ( complex real V30() ) number ) + t2 : ( ( real ) ( complex real V30() ) number ) : ( ( ) ( complex real V30() ) set ) <> 0 : ( ( ) ( ordinal natural complex real V30() V32() integer V44() V134() V135() V136() V137() V138() V139() ) Element of NAT : ( ( ) ( V134() V135() V136() V137() V138() V139() V140() ) Element of K6(REAL : ( ( ) ( non empty V45() V134() V135() V136() V140() ) set ) ) : ( ( ) ( ) set ) ) ) holds
F : ( ( Relation-like Function-like real-valued ) ( Relation-like Function-like complex-valued ext-real-valued real-valued ) Function) is t1 : ( ( real ) ( complex real V30() ) number ) + t2 : ( ( real ) ( complex real V30() ) number ) : ( ( ) ( complex real V30() ) set ) -periodic ;

theorem :: FUNCT_9:16
for t1, t2 being ( ( real ) ( complex real V30() ) number )
for F being ( ( Relation-like Function-like real-valued ) ( Relation-like Function-like complex-valued ext-real-valued real-valued ) Function) st F : ( ( Relation-like Function-like real-valued ) ( Relation-like Function-like complex-valued ext-real-valued real-valued ) Function) is t1 : ( ( real ) ( complex real V30() ) number ) -periodic & F : ( ( Relation-like Function-like real-valued ) ( Relation-like Function-like complex-valued ext-real-valued real-valued ) Function) is t2 : ( ( real ) ( complex real V30() ) number ) -periodic & t1 : ( ( real ) ( complex real V30() ) number ) - t2 : ( ( real ) ( complex real V30() ) number ) : ( ( ) ( complex real V30() ) set ) <> 0 : ( ( ) ( ordinal natural complex real V30() V32() integer V44() V134() V135() V136() V137() V138() V139() ) Element of NAT : ( ( ) ( V134() V135() V136() V137() V138() V139() V140() ) Element of K6(REAL : ( ( ) ( non empty V45() V134() V135() V136() V140() ) set ) ) : ( ( ) ( ) set ) ) ) holds
F : ( ( Relation-like Function-like real-valued ) ( Relation-like Function-like complex-valued ext-real-valued real-valued ) Function) is t1 : ( ( real ) ( complex real V30() ) number ) - t2 : ( ( real ) ( complex real V30() ) number ) : ( ( ) ( complex real V30() ) set ) -periodic ;

theorem :: FUNCT_9:17
for t being ( ( real ) ( complex real V30() ) number )
for F being ( ( Relation-like Function-like real-valued ) ( Relation-like Function-like complex-valued ext-real-valued real-valued ) Function) st t : ( ( real ) ( complex real V30() ) number ) <> 0 : ( ( ) ( ordinal natural complex real V30() V32() integer V44() V134() V135() V136() V137() V138() V139() ) Element of NAT : ( ( ) ( V134() V135() V136() V137() V138() V139() V140() ) Element of K6(REAL : ( ( ) ( non empty V45() V134() V135() V136() V140() ) set ) ) : ( ( ) ( ) set ) ) ) & ( for x being ( ( real ) ( complex real V30() ) number ) st x : ( ( real ) ( complex real V30() ) number ) in dom F : ( ( Relation-like Function-like real-valued ) ( Relation-like Function-like complex-valued ext-real-valued real-valued ) Function) : ( ( ) ( ) set ) holds
( x : ( ( real ) ( complex real V30() ) number ) + t : ( ( real ) ( complex real V30() ) number ) : ( ( ) ( complex real V30() ) set ) in dom F : ( ( Relation-like Function-like real-valued ) ( Relation-like Function-like complex-valued ext-real-valued real-valued ) Function) : ( ( ) ( ) set ) & x : ( ( real ) ( complex real V30() ) number ) - t : ( ( real ) ( complex real V30() ) number ) : ( ( ) ( complex real V30() ) set ) in dom F : ( ( Relation-like Function-like real-valued ) ( Relation-like Function-like complex-valued ext-real-valued real-valued ) Function) : ( ( ) ( ) set ) & F : ( ( Relation-like Function-like real-valued ) ( Relation-like Function-like complex-valued ext-real-valued real-valued ) Function) . (x : ( ( real ) ( complex real V30() ) number ) + t : ( ( real ) ( complex real V30() ) number ) ) : ( ( ) ( complex real V30() ) set ) : ( ( ) ( complex real V30() ) set ) = F : ( ( Relation-like Function-like real-valued ) ( Relation-like Function-like complex-valued ext-real-valued real-valued ) Function) . (x : ( ( real ) ( complex real V30() ) number ) - t : ( ( real ) ( complex real V30() ) number ) ) : ( ( ) ( complex real V30() ) set ) : ( ( ) ( complex real V30() ) set ) ) ) holds
( F : ( ( Relation-like Function-like real-valued ) ( Relation-like Function-like complex-valued ext-real-valued real-valued ) Function) is 2 : ( ( ) ( non empty ordinal natural complex real V30() V31() V32() integer V44() V134() V135() V136() V137() V138() V139() ) Element of NAT : ( ( ) ( V134() V135() V136() V137() V138() V139() V140() ) Element of K6(REAL : ( ( ) ( non empty V45() V134() V135() V136() V140() ) set ) ) : ( ( ) ( ) set ) ) ) * t : ( ( real ) ( complex real V30() ) number ) : ( ( ) ( complex real V30() ) Element of REAL : ( ( ) ( non empty V45() V134() V135() V136() V140() ) set ) ) -periodic & F : ( ( Relation-like Function-like real-valued ) ( Relation-like Function-like complex-valued ext-real-valued real-valued ) Function) is periodic ) ;

theorem :: FUNCT_9:18
for t1, t2 being ( ( real ) ( complex real V30() ) number )
for F being ( ( Relation-like Function-like real-valued ) ( Relation-like Function-like complex-valued ext-real-valued real-valued ) Function) st t1 : ( ( real ) ( complex real V30() ) number ) + t2 : ( ( real ) ( complex real V30() ) number ) : ( ( ) ( complex real V30() ) set ) <> 0 : ( ( ) ( ordinal natural complex real V30() V32() integer V44() V134() V135() V136() V137() V138() V139() ) Element of NAT : ( ( ) ( V134() V135() V136() V137() V138() V139() V140() ) Element of K6(REAL : ( ( ) ( non empty V45() V134() V135() V136() V140() ) set ) ) : ( ( ) ( ) set ) ) ) & ( for x being ( ( real ) ( complex real V30() ) number ) st x : ( ( real ) ( complex real V30() ) number ) in dom F : ( ( Relation-like Function-like real-valued ) ( Relation-like Function-like complex-valued ext-real-valued real-valued ) Function) : ( ( ) ( ) set ) holds
( x : ( ( real ) ( complex real V30() ) number ) + t1 : ( ( real ) ( complex real V30() ) number ) : ( ( ) ( complex real V30() ) set ) in dom F : ( ( Relation-like Function-like real-valued ) ( Relation-like Function-like complex-valued ext-real-valued real-valued ) Function) : ( ( ) ( ) set ) & x : ( ( real ) ( complex real V30() ) number ) - t1 : ( ( real ) ( complex real V30() ) number ) : ( ( ) ( complex real V30() ) set ) in dom F : ( ( Relation-like Function-like real-valued ) ( Relation-like Function-like complex-valued ext-real-valued real-valued ) Function) : ( ( ) ( ) set ) & x : ( ( real ) ( complex real V30() ) number ) + t2 : ( ( real ) ( complex real V30() ) number ) : ( ( ) ( complex real V30() ) set ) in dom F : ( ( Relation-like Function-like real-valued ) ( Relation-like Function-like complex-valued ext-real-valued real-valued ) Function) : ( ( ) ( ) set ) & x : ( ( real ) ( complex real V30() ) number ) - t2 : ( ( real ) ( complex real V30() ) number ) : ( ( ) ( complex real V30() ) set ) in dom F : ( ( Relation-like Function-like real-valued ) ( Relation-like Function-like complex-valued ext-real-valued real-valued ) Function) : ( ( ) ( ) set ) & F : ( ( Relation-like Function-like real-valued ) ( Relation-like Function-like complex-valued ext-real-valued real-valued ) Function) . (x : ( ( real ) ( complex real V30() ) number ) + t1 : ( ( real ) ( complex real V30() ) number ) ) : ( ( ) ( complex real V30() ) set ) : ( ( ) ( complex real V30() ) set ) = F : ( ( Relation-like Function-like real-valued ) ( Relation-like Function-like complex-valued ext-real-valued real-valued ) Function) . (x : ( ( real ) ( complex real V30() ) number ) - t2 : ( ( real ) ( complex real V30() ) number ) ) : ( ( ) ( complex real V30() ) set ) : ( ( ) ( complex real V30() ) set ) ) ) holds
( F : ( ( Relation-like Function-like real-valued ) ( Relation-like Function-like complex-valued ext-real-valued real-valued ) Function) is t1 : ( ( real ) ( complex real V30() ) number ) + t2 : ( ( real ) ( complex real V30() ) number ) : ( ( ) ( complex real V30() ) set ) -periodic & F : ( ( Relation-like Function-like real-valued ) ( Relation-like Function-like complex-valued ext-real-valued real-valued ) Function) is periodic ) ;

theorem :: FUNCT_9:19
for t1, t2 being ( ( real ) ( complex real V30() ) number )
for F being ( ( Relation-like Function-like real-valued ) ( Relation-like Function-like complex-valued ext-real-valued real-valued ) Function) st t1 : ( ( real ) ( complex real V30() ) number ) - t2 : ( ( real ) ( complex real V30() ) number ) : ( ( ) ( complex real V30() ) set ) <> 0 : ( ( ) ( ordinal natural complex real V30() V32() integer V44() V134() V135() V136() V137() V138() V139() ) Element of NAT : ( ( ) ( V134() V135() V136() V137() V138() V139() V140() ) Element of K6(REAL : ( ( ) ( non empty V45() V134() V135() V136() V140() ) set ) ) : ( ( ) ( ) set ) ) ) & ( for x being ( ( real ) ( complex real V30() ) number ) st x : ( ( real ) ( complex real V30() ) number ) in dom F : ( ( Relation-like Function-like real-valued ) ( Relation-like Function-like complex-valued ext-real-valued real-valued ) Function) : ( ( ) ( ) set ) holds
( x : ( ( real ) ( complex real V30() ) number ) + t1 : ( ( real ) ( complex real V30() ) number ) : ( ( ) ( complex real V30() ) set ) in dom F : ( ( Relation-like Function-like real-valued ) ( Relation-like Function-like complex-valued ext-real-valued real-valued ) Function) : ( ( ) ( ) set ) & x : ( ( real ) ( complex real V30() ) number ) - t1 : ( ( real ) ( complex real V30() ) number ) : ( ( ) ( complex real V30() ) set ) in dom F : ( ( Relation-like Function-like real-valued ) ( Relation-like Function-like complex-valued ext-real-valued real-valued ) Function) : ( ( ) ( ) set ) & x : ( ( real ) ( complex real V30() ) number ) + t2 : ( ( real ) ( complex real V30() ) number ) : ( ( ) ( complex real V30() ) set ) in dom F : ( ( Relation-like Function-like real-valued ) ( Relation-like Function-like complex-valued ext-real-valued real-valued ) Function) : ( ( ) ( ) set ) & x : ( ( real ) ( complex real V30() ) number ) - t2 : ( ( real ) ( complex real V30() ) number ) : ( ( ) ( complex real V30() ) set ) in dom F : ( ( Relation-like Function-like real-valued ) ( Relation-like Function-like complex-valued ext-real-valued real-valued ) Function) : ( ( ) ( ) set ) & F : ( ( Relation-like Function-like real-valued ) ( Relation-like Function-like complex-valued ext-real-valued real-valued ) Function) . (x : ( ( real ) ( complex real V30() ) number ) + t1 : ( ( real ) ( complex real V30() ) number ) ) : ( ( ) ( complex real V30() ) set ) : ( ( ) ( complex real V30() ) set ) = F : ( ( Relation-like Function-like real-valued ) ( Relation-like Function-like complex-valued ext-real-valued real-valued ) Function) . (x : ( ( real ) ( complex real V30() ) number ) + t2 : ( ( real ) ( complex real V30() ) number ) ) : ( ( ) ( complex real V30() ) set ) : ( ( ) ( complex real V30() ) set ) ) ) holds
( F : ( ( Relation-like Function-like real-valued ) ( Relation-like Function-like complex-valued ext-real-valued real-valued ) Function) is t1 : ( ( real ) ( complex real V30() ) number ) - t2 : ( ( real ) ( complex real V30() ) number ) : ( ( ) ( complex real V30() ) set ) -periodic & F : ( ( Relation-like Function-like real-valued ) ( Relation-like Function-like complex-valued ext-real-valued real-valued ) Function) is periodic ) ;

theorem :: FUNCT_9:20
for t being ( ( real ) ( complex real V30() ) number )
for F being ( ( Relation-like Function-like real-valued ) ( Relation-like Function-like complex-valued ext-real-valued real-valued ) Function) st t : ( ( real ) ( complex real V30() ) number ) <> 0 : ( ( ) ( ordinal natural complex real V30() V32() integer V44() V134() V135() V136() V137() V138() V139() ) Element of NAT : ( ( ) ( V134() V135() V136() V137() V138() V139() V140() ) Element of K6(REAL : ( ( ) ( non empty V45() V134() V135() V136() V140() ) set ) ) : ( ( ) ( ) set ) ) ) & ( for x being ( ( real ) ( complex real V30() ) number ) st x : ( ( real ) ( complex real V30() ) number ) in dom F : ( ( Relation-like Function-like real-valued ) ( Relation-like Function-like complex-valued ext-real-valued real-valued ) Function) : ( ( ) ( ) set ) holds
( x : ( ( real ) ( complex real V30() ) number ) + t : ( ( real ) ( complex real V30() ) number ) : ( ( ) ( complex real V30() ) set ) in dom F : ( ( Relation-like Function-like real-valued ) ( Relation-like Function-like complex-valued ext-real-valued real-valued ) Function) : ( ( ) ( ) set ) & x : ( ( real ) ( complex real V30() ) number ) - t : ( ( real ) ( complex real V30() ) number ) : ( ( ) ( complex real V30() ) set ) in dom F : ( ( Relation-like Function-like real-valued ) ( Relation-like Function-like complex-valued ext-real-valued real-valued ) Function) : ( ( ) ( ) set ) & F : ( ( Relation-like Function-like real-valued ) ( Relation-like Function-like complex-valued ext-real-valued real-valued ) Function) . (x : ( ( real ) ( complex real V30() ) number ) + t : ( ( real ) ( complex real V30() ) number ) ) : ( ( ) ( complex real V30() ) set ) : ( ( ) ( complex real V30() ) set ) = (F : ( ( Relation-like Function-like real-valued ) ( Relation-like Function-like complex-valued ext-real-valued real-valued ) Function) . x : ( ( real ) ( complex real V30() ) number ) ) : ( ( ) ( complex real V30() ) set ) " : ( ( complex ) ( complex real V30() ) set ) ) ) holds
( F : ( ( Relation-like Function-like real-valued ) ( Relation-like Function-like complex-valued ext-real-valued real-valued ) Function) is 2 : ( ( ) ( non empty ordinal natural complex real V30() V31() V32() integer V44() V134() V135() V136() V137() V138() V139() ) Element of NAT : ( ( ) ( V134() V135() V136() V137() V138() V139() V140() ) Element of K6(REAL : ( ( ) ( non empty V45() V134() V135() V136() V140() ) set ) ) : ( ( ) ( ) set ) ) ) * t : ( ( real ) ( complex real V30() ) number ) : ( ( ) ( complex real V30() ) Element of REAL : ( ( ) ( non empty V45() V134() V135() V136() V140() ) set ) ) -periodic & F : ( ( Relation-like Function-like real-valued ) ( Relation-like Function-like complex-valued ext-real-valued real-valued ) Function) is periodic ) ;

registration
cluster Relation-like Function-like real-valued periodic for ( ( ) ( ) set ) ;
cluster Relation-like Function-like complex-valued ext-real-valued real-valued periodic for ( ( ) ( ) Element of K6(K7(REAL : ( ( ) ( non empty V45() V134() V135() V136() V140() ) set ) ,REAL : ( ( ) ( non empty V45() V134() V135() V136() V140() ) set ) ) : ( ( ) ( Relation-like complex-valued ext-real-valued real-valued ) set ) ) : ( ( ) ( ) set ) ) ;
end;

registration
let t be ( ( non zero real ) ( non zero complex real V30() ) number ) ;
cluster REAL : ( ( ) ( non empty V45() V134() V135() V136() V140() ) set ) --> t : ( ( non zero real ) ( non zero complex real V30() ) set ) : ( ( ) ( non empty Relation-like non-empty REAL : ( ( ) ( non empty V45() V134() V135() V136() V140() ) set ) -defined Function-like constant total complex-valued ext-real-valued real-valued ) set ) -> t : ( ( non zero real ) ( non zero complex real V30() ) set ) -periodic ;
cluster Relation-like Function-like real-valued t : ( ( non zero real ) ( non zero complex real V30() ) set ) -periodic for ( ( ) ( ) set ) ;
end;

registration
let t be ( ( non zero real ) ( non zero complex real V30() ) number ) ;
let F, G be ( ( Relation-like Function-like real-valued t : ( ( non zero real ) ( non zero complex real V30() ) number ) -periodic ) ( Relation-like Function-like complex-valued ext-real-valued real-valued t : ( ( non zero real ) ( non zero complex real V30() ) number ) -periodic ) Function) ;
cluster F : ( ( Relation-like Function-like real-valued t : ( ( non zero real ) ( non zero complex real V30() ) set ) -periodic ) ( Relation-like Function-like complex-valued ext-real-valued real-valued t : ( ( non zero real ) ( non zero complex real V30() ) set ) -periodic ) set ) + G : ( ( Relation-like Function-like real-valued t : ( ( non zero real ) ( non zero complex real V30() ) set ) -periodic ) ( Relation-like Function-like complex-valued ext-real-valued real-valued t : ( ( non zero real ) ( non zero complex real V30() ) set ) -periodic ) set ) : ( ( Relation-like Function-like ) ( Relation-like Function-like complex-valued ext-real-valued real-valued ) set ) -> Relation-like Function-like t : ( ( non zero real ) ( non zero complex real V30() ) set ) -periodic ;
cluster F : ( ( Relation-like Function-like real-valued t : ( ( non zero real ) ( non zero complex real V30() ) set ) -periodic ) ( Relation-like Function-like complex-valued ext-real-valued real-valued t : ( ( non zero real ) ( non zero complex real V30() ) set ) -periodic ) set ) - G : ( ( Relation-like Function-like real-valued t : ( ( non zero real ) ( non zero complex real V30() ) set ) -periodic ) ( Relation-like Function-like complex-valued ext-real-valued real-valued t : ( ( non zero real ) ( non zero complex real V30() ) set ) -periodic ) set ) : ( ( Relation-like Function-like ) ( Relation-like Function-like complex-valued ext-real-valued real-valued ) set ) -> Relation-like Function-like t : ( ( non zero real ) ( non zero complex real V30() ) set ) -periodic ;
cluster F : ( ( Relation-like Function-like real-valued t : ( ( non zero real ) ( non zero complex real V30() ) set ) -periodic ) ( Relation-like Function-like complex-valued ext-real-valued real-valued t : ( ( non zero real ) ( non zero complex real V30() ) set ) -periodic ) set ) (#) G : ( ( Relation-like Function-like real-valued t : ( ( non zero real ) ( non zero complex real V30() ) set ) -periodic ) ( Relation-like Function-like complex-valued ext-real-valued real-valued t : ( ( non zero real ) ( non zero complex real V30() ) set ) -periodic ) set ) : ( ( Relation-like Function-like ) ( Relation-like Function-like complex-valued ext-real-valued real-valued ) set ) -> Relation-like Function-like t : ( ( non zero real ) ( non zero complex real V30() ) set ) -periodic ;
cluster F : ( ( Relation-like Function-like real-valued t : ( ( non zero real ) ( non zero complex real V30() ) set ) -periodic ) ( Relation-like Function-like complex-valued ext-real-valued real-valued t : ( ( non zero real ) ( non zero complex real V30() ) set ) -periodic ) set ) /" G : ( ( Relation-like Function-like real-valued t : ( ( non zero real ) ( non zero complex real V30() ) set ) -periodic ) ( Relation-like Function-like complex-valued ext-real-valued real-valued t : ( ( non zero real ) ( non zero complex real V30() ) set ) -periodic ) set ) : ( ( Relation-like Function-like ) ( Relation-like Function-like complex-valued ext-real-valued real-valued ) set ) -> Relation-like Function-like t : ( ( non zero real ) ( non zero complex real V30() ) set ) -periodic ;
end;

registration
let F be ( ( Relation-like Function-like real-valued periodic ) ( Relation-like Function-like complex-valued ext-real-valued real-valued periodic ) Function) ;
cluster - F : ( ( Relation-like Function-like real-valued periodic ) ( Relation-like Function-like complex-valued ext-real-valued real-valued periodic ) set ) : ( ( Relation-like Function-like complex-valued ) ( Relation-like Function-like complex-valued ext-real-valued real-valued ) set ) -> Relation-like Function-like complex-valued periodic ;
end;

registration
let F be ( ( Relation-like Function-like real-valued periodic ) ( Relation-like Function-like complex-valued ext-real-valued real-valued periodic ) Function) ;
let r be ( ( real ) ( complex real V30() ) number ) ;
cluster r : ( ( real ) ( complex real V30() ) set ) (#) F : ( ( Relation-like Function-like real-valued periodic ) ( Relation-like Function-like complex-valued ext-real-valued real-valued periodic ) set ) : ( ( Relation-like Function-like ) ( Relation-like Function-like complex-valued ext-real-valued real-valued ) set ) -> Relation-like Function-like periodic ;
cluster r : ( ( real ) ( complex real V30() ) set ) + F : ( ( Relation-like Function-like real-valued periodic ) ( Relation-like Function-like complex-valued ext-real-valued real-valued periodic ) set ) : ( ( Relation-like Function-like ) ( Relation-like Function-like complex-valued ext-real-valued real-valued ) set ) -> Relation-like Function-like periodic ;
cluster F : ( ( Relation-like Function-like real-valued periodic ) ( Relation-like Function-like complex-valued ext-real-valued real-valued periodic ) set ) - r : ( ( real ) ( complex real V30() ) set ) : ( ( Relation-like Function-like ) ( Relation-like Function-like complex-valued ext-real-valued real-valued ) set ) -> Relation-like Function-like periodic ;
end;

registration
let F be ( ( Relation-like Function-like real-valued periodic ) ( Relation-like Function-like complex-valued ext-real-valued real-valued periodic ) Function) ;
cluster |.F : ( ( Relation-like Function-like real-valued periodic ) ( Relation-like Function-like complex-valued ext-real-valued real-valued periodic ) set ) .| : ( ( Relation-like Function-like real-valued ) ( Relation-like Function-like complex-valued ext-real-valued real-valued ) set ) -> Relation-like Function-like real-valued periodic ;
cluster F : ( ( Relation-like Function-like real-valued periodic ) ( Relation-like Function-like complex-valued ext-real-valued real-valued periodic ) set ) " : ( ( Relation-like Function-like complex-valued ) ( Relation-like Function-like complex-valued ext-real-valued real-valued ) set ) -> Relation-like Function-like complex-valued periodic ;
cluster F : ( ( Relation-like Function-like real-valued periodic ) ( Relation-like Function-like complex-valued ext-real-valued real-valued periodic ) set ) ^2 : ( ( Relation-like Function-like ) ( Relation-like Function-like complex-valued ext-real-valued real-valued ) set ) -> Relation-like Function-like periodic ;
end;

begin

registration
cluster sin : ( ( Function-like V27( REAL : ( ( ) ( non empty V45() V134() V135() V136() V140() ) set ) , REAL : ( ( ) ( non empty V45() V134() V135() V136() V140() ) set ) ) ) ( Relation-like Function-like V27( REAL : ( ( ) ( non empty V45() V134() V135() V136() V140() ) set ) , REAL : ( ( ) ( non empty V45() V134() V135() V136() V140() ) set ) ) complex-valued ext-real-valued real-valued ) Element of K6(K7(REAL : ( ( ) ( non empty V45() V134() V135() V136() V140() ) set ) ,REAL : ( ( ) ( non empty V45() V134() V135() V136() V140() ) set ) ) : ( ( ) ( Relation-like complex-valued ext-real-valued real-valued ) set ) ) : ( ( ) ( ) set ) ) -> Function-like V27( REAL : ( ( ) ( non empty V45() V134() V135() V136() V140() ) set ) , REAL : ( ( ) ( non empty V45() V134() V135() V136() V140() ) set ) ) periodic ;
cluster cos : ( ( Function-like V27( REAL : ( ( ) ( non empty V45() V134() V135() V136() V140() ) set ) , REAL : ( ( ) ( non empty V45() V134() V135() V136() V140() ) set ) ) ) ( Relation-like Function-like V27( REAL : ( ( ) ( non empty V45() V134() V135() V136() V140() ) set ) , REAL : ( ( ) ( non empty V45() V134() V135() V136() V140() ) set ) ) complex-valued ext-real-valued real-valued ) Element of K6(K7(REAL : ( ( ) ( non empty V45() V134() V135() V136() V140() ) set ) ,REAL : ( ( ) ( non empty V45() V134() V135() V136() V140() ) set ) ) : ( ( ) ( Relation-like complex-valued ext-real-valued real-valued ) set ) ) : ( ( ) ( ) set ) ) -> Function-like V27( REAL : ( ( ) ( non empty V45() V134() V135() V136() V140() ) set ) , REAL : ( ( ) ( non empty V45() V134() V135() V136() V140() ) set ) ) periodic ;
end;

theorem :: FUNCT_9:21
for i being ( ( non zero integer ) ( non zero complex real V30() integer ) Integer) holds sin : ( ( Function-like V27( REAL : ( ( ) ( non empty V45() V134() V135() V136() V140() ) set ) , REAL : ( ( ) ( non empty V45() V134() V135() V136() V140() ) set ) ) ) ( Relation-like Function-like V27( REAL : ( ( ) ( non empty V45() V134() V135() V136() V140() ) set ) , REAL : ( ( ) ( non empty V45() V134() V135() V136() V140() ) set ) ) complex-valued ext-real-valued real-valued periodic ) Element of K6(K7(REAL : ( ( ) ( non empty V45() V134() V135() V136() V140() ) set ) ,REAL : ( ( ) ( non empty V45() V134() V135() V136() V140() ) set ) ) : ( ( ) ( Relation-like complex-valued ext-real-valued real-valued ) set ) ) : ( ( ) ( ) set ) ) is (2 : ( ( ) ( non empty ordinal natural complex real V30() V31() V32() integer V44() V134() V135() V136() V137() V138() V139() ) Element of NAT : ( ( ) ( V134() V135() V136() V137() V138() V139() V140() ) Element of K6(REAL : ( ( ) ( non empty V45() V134() V135() V136() V140() ) set ) ) : ( ( ) ( ) set ) ) ) * PI : ( ( ) ( non empty complex real V30() V31() V32() ) Element of REAL : ( ( ) ( non empty V45() V134() V135() V136() V140() ) set ) ) ) : ( ( ) ( non empty complex real V30() V31() V32() ) Element of REAL : ( ( ) ( non empty V45() V134() V135() V136() V140() ) set ) ) * i : ( ( non zero integer ) ( non zero complex real V30() integer ) Integer) : ( ( ) ( non empty complex real V30() ) Element of REAL : ( ( ) ( non empty V45() V134() V135() V136() V140() ) set ) ) -periodic ;

theorem :: FUNCT_9:22
for i being ( ( non zero integer ) ( non zero complex real V30() integer ) Integer) holds cos : ( ( Function-like V27( REAL : ( ( ) ( non empty V45() V134() V135() V136() V140() ) set ) , REAL : ( ( ) ( non empty V45() V134() V135() V136() V140() ) set ) ) ) ( Relation-like Function-like V27( REAL : ( ( ) ( non empty V45() V134() V135() V136() V140() ) set ) , REAL : ( ( ) ( non empty V45() V134() V135() V136() V140() ) set ) ) complex-valued ext-real-valued real-valued periodic ) Element of K6(K7(REAL : ( ( ) ( non empty V45() V134() V135() V136() V140() ) set ) ,REAL : ( ( ) ( non empty V45() V134() V135() V136() V140() ) set ) ) : ( ( ) ( Relation-like complex-valued ext-real-valued real-valued ) set ) ) : ( ( ) ( ) set ) ) is (2 : ( ( ) ( non empty ordinal natural complex real V30() V31() V32() integer V44() V134() V135() V136() V137() V138() V139() ) Element of NAT : ( ( ) ( V134() V135() V136() V137() V138() V139() V140() ) Element of K6(REAL : ( ( ) ( non empty V45() V134() V135() V136() V140() ) set ) ) : ( ( ) ( ) set ) ) ) * PI : ( ( ) ( non empty complex real V30() V31() V32() ) Element of REAL : ( ( ) ( non empty V45() V134() V135() V136() V140() ) set ) ) ) : ( ( ) ( non empty complex real V30() V31() V32() ) Element of REAL : ( ( ) ( non empty V45() V134() V135() V136() V140() ) set ) ) * i : ( ( non zero integer ) ( non zero complex real V30() integer ) Integer) : ( ( ) ( non empty complex real V30() ) Element of REAL : ( ( ) ( non empty V45() V134() V135() V136() V140() ) set ) ) -periodic ;

registration
cluster cosec : ( ( Function-like ) ( Relation-like Function-like complex-valued ext-real-valued real-valued ) Element of K6(K7(REAL : ( ( ) ( non empty V45() V134() V135() V136() V140() ) set ) ,REAL : ( ( ) ( non empty V45() V134() V135() V136() V140() ) set ) ) : ( ( ) ( Relation-like complex-valued ext-real-valued real-valued ) set ) ) : ( ( ) ( ) set ) ) -> Function-like periodic ;
cluster sec : ( ( Function-like ) ( Relation-like Function-like complex-valued ext-real-valued real-valued ) Element of K6(K7(REAL : ( ( ) ( non empty V45() V134() V135() V136() V140() ) set ) ,REAL : ( ( ) ( non empty V45() V134() V135() V136() V140() ) set ) ) : ( ( ) ( Relation-like complex-valued ext-real-valued real-valued ) set ) ) : ( ( ) ( ) set ) ) -> Function-like periodic ;
end;

theorem :: FUNCT_9:23
for i being ( ( non zero integer ) ( non zero complex real V30() integer ) Integer) holds sec : ( ( Function-like ) ( Relation-like Function-like complex-valued ext-real-valued real-valued periodic ) Element of K6(K7(REAL : ( ( ) ( non empty V45() V134() V135() V136() V140() ) set ) ,REAL : ( ( ) ( non empty V45() V134() V135() V136() V140() ) set ) ) : ( ( ) ( Relation-like complex-valued ext-real-valued real-valued ) set ) ) : ( ( ) ( ) set ) ) is (2 : ( ( ) ( non empty ordinal natural complex real V30() V31() V32() integer V44() V134() V135() V136() V137() V138() V139() ) Element of NAT : ( ( ) ( V134() V135() V136() V137() V138() V139() V140() ) Element of K6(REAL : ( ( ) ( non empty V45() V134() V135() V136() V140() ) set ) ) : ( ( ) ( ) set ) ) ) * PI : ( ( ) ( non empty complex real V30() V31() V32() ) Element of REAL : ( ( ) ( non empty V45() V134() V135() V136() V140() ) set ) ) ) : ( ( ) ( non empty complex real V30() V31() V32() ) Element of REAL : ( ( ) ( non empty V45() V134() V135() V136() V140() ) set ) ) * i : ( ( non zero integer ) ( non zero complex real V30() integer ) Integer) : ( ( ) ( non empty complex real V30() ) Element of REAL : ( ( ) ( non empty V45() V134() V135() V136() V140() ) set ) ) -periodic ;

theorem :: FUNCT_9:24
for i being ( ( non zero integer ) ( non zero complex real V30() integer ) Integer) holds cosec : ( ( Function-like ) ( Relation-like Function-like complex-valued ext-real-valued real-valued periodic ) Element of K6(K7(REAL : ( ( ) ( non empty V45() V134() V135() V136() V140() ) set ) ,REAL : ( ( ) ( non empty V45() V134() V135() V136() V140() ) set ) ) : ( ( ) ( Relation-like complex-valued ext-real-valued real-valued ) set ) ) : ( ( ) ( ) set ) ) is (2 : ( ( ) ( non empty ordinal natural complex real V30() V31() V32() integer V44() V134() V135() V136() V137() V138() V139() ) Element of NAT : ( ( ) ( V134() V135() V136() V137() V138() V139() V140() ) Element of K6(REAL : ( ( ) ( non empty V45() V134() V135() V136() V140() ) set ) ) : ( ( ) ( ) set ) ) ) * PI : ( ( ) ( non empty complex real V30() V31() V32() ) Element of REAL : ( ( ) ( non empty V45() V134() V135() V136() V140() ) set ) ) ) : ( ( ) ( non empty complex real V30() V31() V32() ) Element of REAL : ( ( ) ( non empty V45() V134() V135() V136() V140() ) set ) ) * i : ( ( non zero integer ) ( non zero complex real V30() integer ) Integer) : ( ( ) ( non empty complex real V30() ) Element of REAL : ( ( ) ( non empty V45() V134() V135() V136() V140() ) set ) ) -periodic ;

registration
cluster tan : ( ( Function-like ) ( Relation-like Function-like complex-valued ext-real-valued real-valued ) Element of K6(K7(REAL : ( ( ) ( non empty V45() V134() V135() V136() V140() ) set ) ,REAL : ( ( ) ( non empty V45() V134() V135() V136() V140() ) set ) ) : ( ( ) ( Relation-like complex-valued ext-real-valued real-valued ) set ) ) : ( ( ) ( ) set ) ) -> Function-like periodic ;
cluster cot : ( ( Function-like ) ( Relation-like Function-like complex-valued ext-real-valued real-valued ) Element of K6(K7(REAL : ( ( ) ( non empty V45() V134() V135() V136() V140() ) set ) ,REAL : ( ( ) ( non empty V45() V134() V135() V136() V140() ) set ) ) : ( ( ) ( Relation-like complex-valued ext-real-valued real-valued ) set ) ) : ( ( ) ( ) set ) ) -> Function-like periodic ;
end;

theorem :: FUNCT_9:25
for i being ( ( non zero integer ) ( non zero complex real V30() integer ) Integer) holds tan : ( ( Function-like ) ( Relation-like Function-like complex-valued ext-real-valued real-valued periodic ) Element of K6(K7(REAL : ( ( ) ( non empty V45() V134() V135() V136() V140() ) set ) ,REAL : ( ( ) ( non empty V45() V134() V135() V136() V140() ) set ) ) : ( ( ) ( Relation-like complex-valued ext-real-valued real-valued ) set ) ) : ( ( ) ( ) set ) ) is PI : ( ( ) ( non empty complex real V30() V31() V32() ) Element of REAL : ( ( ) ( non empty V45() V134() V135() V136() V140() ) set ) ) * i : ( ( non zero integer ) ( non zero complex real V30() integer ) Integer) : ( ( ) ( non empty complex real V30() ) Element of REAL : ( ( ) ( non empty V45() V134() V135() V136() V140() ) set ) ) -periodic ;

theorem :: FUNCT_9:26
for i being ( ( non zero integer ) ( non zero complex real V30() integer ) Integer) holds cot : ( ( Function-like ) ( Relation-like Function-like complex-valued ext-real-valued real-valued periodic ) Element of K6(K7(REAL : ( ( ) ( non empty V45() V134() V135() V136() V140() ) set ) ,REAL : ( ( ) ( non empty V45() V134() V135() V136() V140() ) set ) ) : ( ( ) ( Relation-like complex-valued ext-real-valued real-valued ) set ) ) : ( ( ) ( ) set ) ) is PI : ( ( ) ( non empty complex real V30() V31() V32() ) Element of REAL : ( ( ) ( non empty V45() V134() V135() V136() V140() ) set ) ) * i : ( ( non zero integer ) ( non zero complex real V30() integer ) Integer) : ( ( ) ( non empty complex real V30() ) Element of REAL : ( ( ) ( non empty V45() V134() V135() V136() V140() ) set ) ) -periodic ;

theorem :: FUNCT_9:27
for i being ( ( non zero integer ) ( non zero complex real V30() integer ) Integer) holds |.sin : ( ( Function-like V27( REAL : ( ( ) ( non empty V45() V134() V135() V136() V140() ) set ) , REAL : ( ( ) ( non empty V45() V134() V135() V136() V140() ) set ) ) ) ( Relation-like Function-like V27( REAL : ( ( ) ( non empty V45() V134() V135() V136() V140() ) set ) , REAL : ( ( ) ( non empty V45() V134() V135() V136() V140() ) set ) ) complex-valued ext-real-valued real-valued periodic ) Element of K6(K7(REAL : ( ( ) ( non empty V45() V134() V135() V136() V140() ) set ) ,REAL : ( ( ) ( non empty V45() V134() V135() V136() V140() ) set ) ) : ( ( ) ( Relation-like complex-valued ext-real-valued real-valued ) set ) ) : ( ( ) ( ) set ) ) .| : ( ( Function-like ) ( Relation-like Function-like total complex-valued ext-real-valued real-valued periodic ) Element of K6(K7(REAL : ( ( ) ( non empty V45() V134() V135() V136() V140() ) set ) ,REAL : ( ( ) ( non empty V45() V134() V135() V136() V140() ) set ) ) : ( ( ) ( Relation-like complex-valued ext-real-valued real-valued ) set ) ) : ( ( ) ( ) set ) ) is PI : ( ( ) ( non empty complex real V30() V31() V32() ) Element of REAL : ( ( ) ( non empty V45() V134() V135() V136() V140() ) set ) ) * i : ( ( non zero integer ) ( non zero complex real V30() integer ) Integer) : ( ( ) ( non empty complex real V30() ) Element of REAL : ( ( ) ( non empty V45() V134() V135() V136() V140() ) set ) ) -periodic ;

theorem :: FUNCT_9:28
for i being ( ( non zero integer ) ( non zero complex real V30() integer ) Integer) holds |.cos : ( ( Function-like V27( REAL : ( ( ) ( non empty V45() V134() V135() V136() V140() ) set ) , REAL : ( ( ) ( non empty V45() V134() V135() V136() V140() ) set ) ) ) ( Relation-like Function-like V27( REAL : ( ( ) ( non empty V45() V134() V135() V136() V140() ) set ) , REAL : ( ( ) ( non empty V45() V134() V135() V136() V140() ) set ) ) complex-valued ext-real-valued real-valued periodic ) Element of K6(K7(REAL : ( ( ) ( non empty V45() V134() V135() V136() V140() ) set ) ,REAL : ( ( ) ( non empty V45() V134() V135() V136() V140() ) set ) ) : ( ( ) ( Relation-like complex-valued ext-real-valued real-valued ) set ) ) : ( ( ) ( ) set ) ) .| : ( ( Function-like ) ( Relation-like Function-like total complex-valued ext-real-valued real-valued periodic ) Element of K6(K7(REAL : ( ( ) ( non empty V45() V134() V135() V136() V140() ) set ) ,REAL : ( ( ) ( non empty V45() V134() V135() V136() V140() ) set ) ) : ( ( ) ( Relation-like complex-valued ext-real-valued real-valued ) set ) ) : ( ( ) ( ) set ) ) is PI : ( ( ) ( non empty complex real V30() V31() V32() ) Element of REAL : ( ( ) ( non empty V45() V134() V135() V136() V140() ) set ) ) * i : ( ( non zero integer ) ( non zero complex real V30() integer ) Integer) : ( ( ) ( non empty complex real V30() ) Element of REAL : ( ( ) ( non empty V45() V134() V135() V136() V140() ) set ) ) -periodic ;

theorem :: FUNCT_9:29
for i being ( ( non zero integer ) ( non zero complex real V30() integer ) Integer) holds |.sin : ( ( Function-like V27( REAL : ( ( ) ( non empty V45() V134() V135() V136() V140() ) set ) , REAL : ( ( ) ( non empty V45() V134() V135() V136() V140() ) set ) ) ) ( Relation-like Function-like V27( REAL : ( ( ) ( non empty V45() V134() V135() V136() V140() ) set ) , REAL : ( ( ) ( non empty V45() V134() V135() V136() V140() ) set ) ) complex-valued ext-real-valued real-valued periodic ) Element of K6(K7(REAL : ( ( ) ( non empty V45() V134() V135() V136() V140() ) set ) ,REAL : ( ( ) ( non empty V45() V134() V135() V136() V140() ) set ) ) : ( ( ) ( Relation-like complex-valued ext-real-valued real-valued ) set ) ) : ( ( ) ( ) set ) ) .| : ( ( Function-like ) ( Relation-like Function-like total complex-valued ext-real-valued real-valued periodic ) Element of K6(K7(REAL : ( ( ) ( non empty V45() V134() V135() V136() V140() ) set ) ,REAL : ( ( ) ( non empty V45() V134() V135() V136() V140() ) set ) ) : ( ( ) ( Relation-like complex-valued ext-real-valued real-valued ) set ) ) : ( ( ) ( ) set ) ) + |.cos : ( ( Function-like V27( REAL : ( ( ) ( non empty V45() V134() V135() V136() V140() ) set ) , REAL : ( ( ) ( non empty V45() V134() V135() V136() V140() ) set ) ) ) ( Relation-like Function-like V27( REAL : ( ( ) ( non empty V45() V134() V135() V136() V140() ) set ) , REAL : ( ( ) ( non empty V45() V134() V135() V136() V140() ) set ) ) complex-valued ext-real-valued real-valued periodic ) Element of K6(K7(REAL : ( ( ) ( non empty V45() V134() V135() V136() V140() ) set ) ,REAL : ( ( ) ( non empty V45() V134() V135() V136() V140() ) set ) ) : ( ( ) ( Relation-like complex-valued ext-real-valued real-valued ) set ) ) : ( ( ) ( ) set ) ) .| : ( ( Function-like ) ( Relation-like Function-like total complex-valued ext-real-valued real-valued periodic ) Element of K6(K7(REAL : ( ( ) ( non empty V45() V134() V135() V136() V140() ) set ) ,REAL : ( ( ) ( non empty V45() V134() V135() V136() V140() ) set ) ) : ( ( ) ( Relation-like complex-valued ext-real-valued real-valued ) set ) ) : ( ( ) ( ) set ) ) : ( ( Function-like ) ( Relation-like Function-like complex-valued ext-real-valued real-valued ) Element of K6(K7(REAL : ( ( ) ( non empty V45() V134() V135() V136() V140() ) set ) ,REAL : ( ( ) ( non empty V45() V134() V135() V136() V140() ) set ) ) : ( ( ) ( Relation-like complex-valued ext-real-valued real-valued ) set ) ) : ( ( ) ( ) set ) ) is (PI : ( ( ) ( non empty complex real V30() V31() V32() ) Element of REAL : ( ( ) ( non empty V45() V134() V135() V136() V140() ) set ) ) / 2 : ( ( ) ( non empty ordinal natural complex real V30() V31() V32() integer V44() V134() V135() V136() V137() V138() V139() ) Element of NAT : ( ( ) ( V134() V135() V136() V137() V138() V139() V140() ) Element of K6(REAL : ( ( ) ( non empty V45() V134() V135() V136() V140() ) set ) ) : ( ( ) ( ) set ) ) ) ) : ( ( ) ( non empty complex real V30() V31() V32() ) Element of REAL : ( ( ) ( non empty V45() V134() V135() V136() V140() ) set ) ) * i : ( ( non zero integer ) ( non zero complex real V30() integer ) Integer) : ( ( ) ( non empty complex real V30() ) Element of REAL : ( ( ) ( non empty V45() V134() V135() V136() V140() ) set ) ) -periodic ;

theorem :: FUNCT_9:30
for i being ( ( non zero integer ) ( non zero complex real V30() integer ) Integer) holds sin : ( ( Function-like V27( REAL : ( ( ) ( non empty V45() V134() V135() V136() V140() ) set ) , REAL : ( ( ) ( non empty V45() V134() V135() V136() V140() ) set ) ) ) ( Relation-like Function-like V27( REAL : ( ( ) ( non empty V45() V134() V135() V136() V140() ) set ) , REAL : ( ( ) ( non empty V45() V134() V135() V136() V140() ) set ) ) complex-valued ext-real-valued real-valued periodic ) Element of K6(K7(REAL : ( ( ) ( non empty V45() V134() V135() V136() V140() ) set ) ,REAL : ( ( ) ( non empty V45() V134() V135() V136() V140() ) set ) ) : ( ( ) ( Relation-like complex-valued ext-real-valued real-valued ) set ) ) : ( ( ) ( ) set ) ) ^2 : ( ( Function-like ) ( Relation-like Function-like total complex-valued ext-real-valued real-valued periodic ) Element of K6(K7(REAL : ( ( ) ( non empty V45() V134() V135() V136() V140() ) set ) ,REAL : ( ( ) ( non empty V45() V134() V135() V136() V140() ) set ) ) : ( ( ) ( Relation-like complex-valued ext-real-valued real-valued ) set ) ) : ( ( ) ( ) set ) ) is PI : ( ( ) ( non empty complex real V30() V31() V32() ) Element of REAL : ( ( ) ( non empty V45() V134() V135() V136() V140() ) set ) ) * i : ( ( non zero integer ) ( non zero complex real V30() integer ) Integer) : ( ( ) ( non empty complex real V30() ) Element of REAL : ( ( ) ( non empty V45() V134() V135() V136() V140() ) set ) ) -periodic ;

theorem :: FUNCT_9:31
for i being ( ( non zero integer ) ( non zero complex real V30() integer ) Integer) holds cos : ( ( Function-like V27( REAL : ( ( ) ( non empty V45() V134() V135() V136() V140() ) set ) , REAL : ( ( ) ( non empty V45() V134() V135() V136() V140() ) set ) ) ) ( Relation-like Function-like V27( REAL : ( ( ) ( non empty V45() V134() V135() V136() V140() ) set ) , REAL : ( ( ) ( non empty V45() V134() V135() V136() V140() ) set ) ) complex-valued ext-real-valued real-valued periodic ) Element of K6(K7(REAL : ( ( ) ( non empty V45() V134() V135() V136() V140() ) set ) ,REAL : ( ( ) ( non empty V45() V134() V135() V136() V140() ) set ) ) : ( ( ) ( Relation-like complex-valued ext-real-valued real-valued ) set ) ) : ( ( ) ( ) set ) ) ^2 : ( ( Function-like ) ( Relation-like Function-like total complex-valued ext-real-valued real-valued periodic ) Element of K6(K7(REAL : ( ( ) ( non empty V45() V134() V135() V136() V140() ) set ) ,REAL : ( ( ) ( non empty V45() V134() V135() V136() V140() ) set ) ) : ( ( ) ( Relation-like complex-valued ext-real-valued real-valued ) set ) ) : ( ( ) ( ) set ) ) is PI : ( ( ) ( non empty complex real V30() V31() V32() ) Element of REAL : ( ( ) ( non empty V45() V134() V135() V136() V140() ) set ) ) * i : ( ( non zero integer ) ( non zero complex real V30() integer ) Integer) : ( ( ) ( non empty complex real V30() ) Element of REAL : ( ( ) ( non empty V45() V134() V135() V136() V140() ) set ) ) -periodic ;

theorem :: FUNCT_9:32
for i being ( ( non zero integer ) ( non zero complex real V30() integer ) Integer) holds sin : ( ( Function-like V27( REAL : ( ( ) ( non empty V45() V134() V135() V136() V140() ) set ) , REAL : ( ( ) ( non empty V45() V134() V135() V136() V140() ) set ) ) ) ( Relation-like Function-like V27( REAL : ( ( ) ( non empty V45() V134() V135() V136() V140() ) set ) , REAL : ( ( ) ( non empty V45() V134() V135() V136() V140() ) set ) ) complex-valued ext-real-valued real-valued periodic ) Element of K6(K7(REAL : ( ( ) ( non empty V45() V134() V135() V136() V140() ) set ) ,REAL : ( ( ) ( non empty V45() V134() V135() V136() V140() ) set ) ) : ( ( ) ( Relation-like complex-valued ext-real-valued real-valued ) set ) ) : ( ( ) ( ) set ) ) (#) cos : ( ( Function-like V27( REAL : ( ( ) ( non empty V45() V134() V135() V136() V140() ) set ) , REAL : ( ( ) ( non empty V45() V134() V135() V136() V140() ) set ) ) ) ( Relation-like Function-like V27( REAL : ( ( ) ( non empty V45() V134() V135() V136() V140() ) set ) , REAL : ( ( ) ( non empty V45() V134() V135() V136() V140() ) set ) ) complex-valued ext-real-valued real-valued periodic ) Element of K6(K7(REAL : ( ( ) ( non empty V45() V134() V135() V136() V140() ) set ) ,REAL : ( ( ) ( non empty V45() V134() V135() V136() V140() ) set ) ) : ( ( ) ( Relation-like complex-valued ext-real-valued real-valued ) set ) ) : ( ( ) ( ) set ) ) : ( ( Function-like ) ( Relation-like Function-like total complex-valued ext-real-valued real-valued ) Element of K6(K7(REAL : ( ( ) ( non empty V45() V134() V135() V136() V140() ) set ) ,REAL : ( ( ) ( non empty V45() V134() V135() V136() V140() ) set ) ) : ( ( ) ( Relation-like complex-valued ext-real-valued real-valued ) set ) ) : ( ( ) ( ) set ) ) is PI : ( ( ) ( non empty complex real V30() V31() V32() ) Element of REAL : ( ( ) ( non empty V45() V134() V135() V136() V140() ) set ) ) * i : ( ( non zero integer ) ( non zero complex real V30() integer ) Integer) : ( ( ) ( non empty complex real V30() ) Element of REAL : ( ( ) ( non empty V45() V134() V135() V136() V140() ) set ) ) -periodic ;

theorem :: FUNCT_9:33
for b, a being ( ( real ) ( complex real V30() ) number )
for i being ( ( non zero integer ) ( non zero complex real V30() integer ) Integer) holds b : ( ( real ) ( complex real V30() ) number ) + (a : ( ( real ) ( complex real V30() ) number ) (#) sin : ( ( Function-like V27( REAL : ( ( ) ( non empty V45() V134() V135() V136() V140() ) set ) , REAL : ( ( ) ( non empty V45() V134() V135() V136() V140() ) set ) ) ) ( Relation-like Function-like V27( REAL : ( ( ) ( non empty V45() V134() V135() V136() V140() ) set ) , REAL : ( ( ) ( non empty V45() V134() V135() V136() V140() ) set ) ) complex-valued ext-real-valued real-valued periodic ) Element of K6(K7(REAL : ( ( ) ( non empty V45() V134() V135() V136() V140() ) set ) ,REAL : ( ( ) ( non empty V45() V134() V135() V136() V140() ) set ) ) : ( ( ) ( Relation-like complex-valued ext-real-valued real-valued ) set ) ) : ( ( ) ( ) set ) ) ) : ( ( Function-like ) ( Relation-like Function-like total complex-valued ext-real-valued real-valued periodic ) Element of K6(K7(REAL : ( ( ) ( non empty V45() V134() V135() V136() V140() ) set ) ,REAL : ( ( ) ( non empty V45() V134() V135() V136() V140() ) set ) ) : ( ( ) ( Relation-like complex-valued ext-real-valued real-valued ) set ) ) : ( ( ) ( ) set ) ) : ( ( Function-like ) ( Relation-like Function-like complex-valued ext-real-valued real-valued periodic ) Element of K6(K7(REAL : ( ( ) ( non empty V45() V134() V135() V136() V140() ) set ) ,REAL : ( ( ) ( non empty V45() V134() V135() V136() V140() ) set ) ) : ( ( ) ( Relation-like complex-valued ext-real-valued real-valued ) set ) ) : ( ( ) ( ) set ) ) is (2 : ( ( ) ( non empty ordinal natural complex real V30() V31() V32() integer V44() V134() V135() V136() V137() V138() V139() ) Element of NAT : ( ( ) ( V134() V135() V136() V137() V138() V139() V140() ) Element of K6(REAL : ( ( ) ( non empty V45() V134() V135() V136() V140() ) set ) ) : ( ( ) ( ) set ) ) ) * PI : ( ( ) ( non empty complex real V30() V31() V32() ) Element of REAL : ( ( ) ( non empty V45() V134() V135() V136() V140() ) set ) ) ) : ( ( ) ( non empty complex real V30() V31() V32() ) Element of REAL : ( ( ) ( non empty V45() V134() V135() V136() V140() ) set ) ) * i : ( ( non zero integer ) ( non zero complex real V30() integer ) Integer) : ( ( ) ( non empty complex real V30() ) Element of REAL : ( ( ) ( non empty V45() V134() V135() V136() V140() ) set ) ) -periodic ;

theorem :: FUNCT_9:34
for a, b being ( ( real ) ( complex real V30() ) number )
for i being ( ( non zero integer ) ( non zero complex real V30() integer ) Integer) holds (a : ( ( real ) ( complex real V30() ) number ) (#) sin : ( ( Function-like V27( REAL : ( ( ) ( non empty V45() V134() V135() V136() V140() ) set ) , REAL : ( ( ) ( non empty V45() V134() V135() V136() V140() ) set ) ) ) ( Relation-like Function-like V27( REAL : ( ( ) ( non empty V45() V134() V135() V136() V140() ) set ) , REAL : ( ( ) ( non empty V45() V134() V135() V136() V140() ) set ) ) complex-valued ext-real-valued real-valued periodic ) Element of K6(K7(REAL : ( ( ) ( non empty V45() V134() V135() V136() V140() ) set ) ,REAL : ( ( ) ( non empty V45() V134() V135() V136() V140() ) set ) ) : ( ( ) ( Relation-like complex-valued ext-real-valued real-valued ) set ) ) : ( ( ) ( ) set ) ) ) : ( ( Function-like ) ( Relation-like Function-like total complex-valued ext-real-valued real-valued periodic ) Element of K6(K7(REAL : ( ( ) ( non empty V45() V134() V135() V136() V140() ) set ) ,REAL : ( ( ) ( non empty V45() V134() V135() V136() V140() ) set ) ) : ( ( ) ( Relation-like complex-valued ext-real-valued real-valued ) set ) ) : ( ( ) ( ) set ) ) - b : ( ( real ) ( complex real V30() ) number ) : ( ( Function-like ) ( Relation-like Function-like complex-valued ext-real-valued real-valued periodic ) Element of K6(K7(REAL : ( ( ) ( non empty V45() V134() V135() V136() V140() ) set ) ,REAL : ( ( ) ( non empty V45() V134() V135() V136() V140() ) set ) ) : ( ( ) ( Relation-like complex-valued ext-real-valued real-valued ) set ) ) : ( ( ) ( ) set ) ) is (2 : ( ( ) ( non empty ordinal natural complex real V30() V31() V32() integer V44() V134() V135() V136() V137() V138() V139() ) Element of NAT : ( ( ) ( V134() V135() V136() V137() V138() V139() V140() ) Element of K6(REAL : ( ( ) ( non empty V45() V134() V135() V136() V140() ) set ) ) : ( ( ) ( ) set ) ) ) * PI : ( ( ) ( non empty complex real V30() V31() V32() ) Element of REAL : ( ( ) ( non empty V45() V134() V135() V136() V140() ) set ) ) ) : ( ( ) ( non empty complex real V30() V31() V32() ) Element of REAL : ( ( ) ( non empty V45() V134() V135() V136() V140() ) set ) ) * i : ( ( non zero integer ) ( non zero complex real V30() integer ) Integer) : ( ( ) ( non empty complex real V30() ) Element of REAL : ( ( ) ( non empty V45() V134() V135() V136() V140() ) set ) ) -periodic ;

theorem :: FUNCT_9:35
for b, a being ( ( real ) ( complex real V30() ) number )
for i being ( ( non zero integer ) ( non zero complex real V30() integer ) Integer) holds b : ( ( real ) ( complex real V30() ) number ) + (a : ( ( real ) ( complex real V30() ) number ) (#) cos : ( ( Function-like V27( REAL : ( ( ) ( non empty V45() V134() V135() V136() V140() ) set ) , REAL : ( ( ) ( non empty V45() V134() V135() V136() V140() ) set ) ) ) ( Relation-like Function-like V27( REAL : ( ( ) ( non empty V45() V134() V135() V136() V140() ) set ) , REAL : ( ( ) ( non empty V45() V134() V135() V136() V140() ) set ) ) complex-valued ext-real-valued real-valued periodic ) Element of K6(K7(REAL : ( ( ) ( non empty V45() V134() V135() V136() V140() ) set ) ,REAL : ( ( ) ( non empty V45() V134() V135() V136() V140() ) set ) ) : ( ( ) ( Relation-like complex-valued ext-real-valued real-valued ) set ) ) : ( ( ) ( ) set ) ) ) : ( ( Function-like ) ( Relation-like Function-like total complex-valued ext-real-valued real-valued periodic ) Element of K6(K7(REAL : ( ( ) ( non empty V45() V134() V135() V136() V140() ) set ) ,REAL : ( ( ) ( non empty V45() V134() V135() V136() V140() ) set ) ) : ( ( ) ( Relation-like complex-valued ext-real-valued real-valued ) set ) ) : ( ( ) ( ) set ) ) : ( ( Function-like ) ( Relation-like Function-like complex-valued ext-real-valued real-valued periodic ) Element of K6(K7(REAL : ( ( ) ( non empty V45() V134() V135() V136() V140() ) set ) ,REAL : ( ( ) ( non empty V45() V134() V135() V136() V140() ) set ) ) : ( ( ) ( Relation-like complex-valued ext-real-valued real-valued ) set ) ) : ( ( ) ( ) set ) ) is (2 : ( ( ) ( non empty ordinal natural complex real V30() V31() V32() integer V44() V134() V135() V136() V137() V138() V139() ) Element of NAT : ( ( ) ( V134() V135() V136() V137() V138() V139() V140() ) Element of K6(REAL : ( ( ) ( non empty V45() V134() V135() V136() V140() ) set ) ) : ( ( ) ( ) set ) ) ) * PI : ( ( ) ( non empty complex real V30() V31() V32() ) Element of REAL : ( ( ) ( non empty V45() V134() V135() V136() V140() ) set ) ) ) : ( ( ) ( non empty complex real V30() V31() V32() ) Element of REAL : ( ( ) ( non empty V45() V134() V135() V136() V140() ) set ) ) * i : ( ( non zero integer ) ( non zero complex real V30() integer ) Integer) : ( ( ) ( non empty complex real V30() ) Element of REAL : ( ( ) ( non empty V45() V134() V135() V136() V140() ) set ) ) -periodic ;

theorem :: FUNCT_9:36
for a, b being ( ( real ) ( complex real V30() ) number )
for i being ( ( non zero integer ) ( non zero complex real V30() integer ) Integer) holds (a : ( ( real ) ( complex real V30() ) number ) (#) cos : ( ( Function-like V27( REAL : ( ( ) ( non empty V45() V134() V135() V136() V140() ) set ) , REAL : ( ( ) ( non empty V45() V134() V135() V136() V140() ) set ) ) ) ( Relation-like Function-like V27( REAL : ( ( ) ( non empty V45() V134() V135() V136() V140() ) set ) , REAL : ( ( ) ( non empty V45() V134() V135() V136() V140() ) set ) ) complex-valued ext-real-valued real-valued periodic ) Element of K6(K7(REAL : ( ( ) ( non empty V45() V134() V135() V136() V140() ) set ) ,REAL : ( ( ) ( non empty V45() V134() V135() V136() V140() ) set ) ) : ( ( ) ( Relation-like complex-valued ext-real-valued real-valued ) set ) ) : ( ( ) ( ) set ) ) ) : ( ( Function-like ) ( Relation-like Function-like total complex-valued ext-real-valued real-valued periodic ) Element of K6(K7(REAL : ( ( ) ( non empty V45() V134() V135() V136() V140() ) set ) ,REAL : ( ( ) ( non empty V45() V134() V135() V136() V140() ) set ) ) : ( ( ) ( Relation-like complex-valued ext-real-valued real-valued ) set ) ) : ( ( ) ( ) set ) ) - b : ( ( real ) ( complex real V30() ) number ) : ( ( Function-like ) ( Relation-like Function-like complex-valued ext-real-valued real-valued periodic ) Element of K6(K7(REAL : ( ( ) ( non empty V45() V134() V135() V136() V140() ) set ) ,REAL : ( ( ) ( non empty V45() V134() V135() V136() V140() ) set ) ) : ( ( ) ( Relation-like complex-valued ext-real-valued real-valued ) set ) ) : ( ( ) ( ) set ) ) is (2 : ( ( ) ( non empty ordinal natural complex real V30() V31() V32() integer V44() V134() V135() V136() V137() V138() V139() ) Element of NAT : ( ( ) ( V134() V135() V136() V137() V138() V139() V140() ) Element of K6(REAL : ( ( ) ( non empty V45() V134() V135() V136() V140() ) set ) ) : ( ( ) ( ) set ) ) ) * PI : ( ( ) ( non empty complex real V30() V31() V32() ) Element of REAL : ( ( ) ( non empty V45() V134() V135() V136() V140() ) set ) ) ) : ( ( ) ( non empty complex real V30() V31() V32() ) Element of REAL : ( ( ) ( non empty V45() V134() V135() V136() V140() ) set ) ) * i : ( ( non zero integer ) ( non zero complex real V30() integer ) Integer) : ( ( ) ( non empty complex real V30() ) Element of REAL : ( ( ) ( non empty V45() V134() V135() V136() V140() ) set ) ) -periodic ;

theorem :: FUNCT_9:37
for t, a being ( ( real ) ( complex real V30() ) number ) st t : ( ( real ) ( complex real V30() ) number ) <> 0 : ( ( ) ( ordinal natural complex real V30() V32() integer V44() V134() V135() V136() V137() V138() V139() ) Element of NAT : ( ( ) ( V134() V135() V136() V137() V138() V139() V140() ) Element of K6(REAL : ( ( ) ( non empty V45() V134() V135() V136() V140() ) set ) ) : ( ( ) ( ) set ) ) ) holds
REAL : ( ( ) ( non empty V45() V134() V135() V136() V140() ) set ) --> a : ( ( real ) ( complex real V30() ) number ) : ( ( Function-like V27( REAL : ( ( ) ( non empty V45() V134() V135() V136() V140() ) set ) ,{b2 : ( ( real ) ( complex real V30() ) number ) } : ( ( ) ( V134() V135() V136() ) set ) ) ) ( non empty Relation-like REAL : ( ( ) ( non empty V45() V134() V135() V136() V140() ) set ) -defined Function-like constant total V27( REAL : ( ( ) ( non empty V45() V134() V135() V136() V140() ) set ) ,{b2 : ( ( real ) ( complex real V30() ) number ) } : ( ( ) ( V134() V135() V136() ) set ) ) complex-valued ext-real-valued real-valued ) Element of K6(K7(REAL : ( ( ) ( non empty V45() V134() V135() V136() V140() ) set ) ,{b2 : ( ( real ) ( complex real V30() ) number ) } : ( ( ) ( V134() V135() V136() ) set ) ) : ( ( ) ( Relation-like complex-valued ext-real-valued real-valued ) set ) ) : ( ( ) ( ) set ) ) is t : ( ( real ) ( complex real V30() ) number ) -periodic ;

registration
let a be ( ( real ) ( complex real V30() ) number ) ;
cluster REAL : ( ( ) ( non empty V45() V134() V135() V136() V140() ) set ) --> a : ( ( real ) ( complex real V30() ) set ) : ( ( ) ( non empty Relation-like REAL : ( ( ) ( non empty V45() V134() V135() V136() V140() ) set ) -defined Function-like constant total complex-valued ext-real-valued real-valued ) set ) -> periodic ;
end;

registration
let t be ( ( non zero real ) ( non zero complex real V30() ) number ) ;
cluster Relation-like Function-like V27( REAL : ( ( ) ( non empty V45() V134() V135() V136() V140() ) set ) , REAL : ( ( ) ( non empty V45() V134() V135() V136() V140() ) set ) ) complex-valued ext-real-valued real-valued t : ( ( non zero real ) ( non zero complex real V30() ) set ) -periodic for ( ( ) ( ) Element of K6(K7(REAL : ( ( ) ( non empty V45() V134() V135() V136() V140() ) set ) ,REAL : ( ( ) ( non empty V45() V134() V135() V136() V140() ) set ) ) : ( ( ) ( Relation-like complex-valued ext-real-valued real-valued ) set ) ) : ( ( ) ( ) set ) ) ;
end;