SIN_COS3

:: SIN_COS3 semantic presentation

begin

definition

func sin_C -> ( ( V6() V18( COMPLEX : ( ( ) ( non zero V46() V57() V63() ) set ) , COMPLEX : ( ( ) ( non zero V46() V57() V63() ) set ) ) ) ( V1() V4( COMPLEX : ( ( ) ( non zero V46() V57() V63() ) set ) ) V5( COMPLEX : ( ( ) ( non zero V46() V57() V63() ) set ) ) V6() non zero total V18( COMPLEX : ( ( ) ( non zero V46() V57() V63() ) set ) , COMPLEX : ( ( ) ( non zero V46() V57() V63() ) set ) ) ) Function of COMPLEX : ( ( ) ( non zero V46() V57() V63() ) set ) , COMPLEX : ( ( ) ( non zero V46() V57() V63() ) set ) ) means :: SIN_COS3:def 1
for z being ( ( ) ( complex ) Element of COMPLEX : ( ( ) ( non zero V46() V57() V63() ) set ) ) holds it : ( ( ) ( ) set ) . z : ( ( ) ( complex ) Element of COMPLEX : ( ( ) ( non zero V46() V57() V63() ) set ) ) : ( ( ) ( complex ) Element of COMPLEX : ( ( ) ( non zero V46() V57() V63() ) set ) ) = ((exp ( : ( ( ) ( complex ) Element of COMPLEX : ( ( ) ( non zero V46() V57() V63() ) set ) ) * z : ( ( ) ( complex ) Element of COMPLEX : ( ( ) ( non zero V46() V57() V63() ) set ) ) ) : ( ( ) ( complex ) Element of COMPLEX : ( ( ) ( non zero V46() V57() V63() ) set ) ) ) : ( ( ) ( complex ) Element of COMPLEX : ( ( ) ( non zero V46() V57() V63() ) set ) ) - (exp (- ( : ( ( ) ( complex ) Element of COMPLEX : ( ( ) ( non zero V46() V57() V63() ) set ) ) * z : ( ( ) ( complex ) Element of COMPLEX : ( ( ) ( non zero V46() V57() V63() ) set ) ) ) : ( ( ) ( complex ) Element of COMPLEX : ( ( ) ( non zero V46() V57() V63() ) set ) ) ) : ( ( ) ( complex ) Element of COMPLEX : ( ( ) ( non zero V46() V57() V63() ) set ) ) ) : ( ( ) ( complex ) Element of COMPLEX : ( ( ) ( non zero V46() V57() V63() ) set ) ) ) : ( ( ) ( complex ) Element of COMPLEX : ( ( ) ( non zero V46() V57() V63() ) set ) ) / (2 : ( ( ) ( non zero natural complex V29() V30() V33() V34() V57() V58() V59() V60() V61() V62() ) Element of NAT : ( ( ) ( V57() V58() V59() V60() V61() V62() V63() ) Element of K19(REAL : ( ( ) ( non zero V46() V57() V58() V59() V63() ) set ) ) : ( ( ) ( ) set ) ) ) * : ( ( ) ( complex ) Element of COMPLEX : ( ( ) ( non zero V46() V57() V63() ) set ) ) ) : ( ( ) ( complex ) Element of COMPLEX : ( ( ) ( non zero V46() V57() V63() ) set ) ) : ( ( ) ( complex ) Element of COMPLEX : ( ( ) ( non zero V46() V57() V63() ) set ) ) ;

end;

definition

func cos_C -> ( ( V6() V18( COMPLEX : ( ( ) ( non zero V46() V57() V63() ) set ) , COMPLEX : ( ( ) ( non zero V46() V57() V63() ) set ) ) ) ( V1() V4( COMPLEX : ( ( ) ( non zero V46() V57() V63() ) set ) ) V5( COMPLEX : ( ( ) ( non zero V46() V57() V63() ) set ) ) V6() non zero total V18( COMPLEX : ( ( ) ( non zero V46() V57() V63() ) set ) , COMPLEX : ( ( ) ( non zero V46() V57() V63() ) set ) ) ) Function of COMPLEX : ( ( ) ( non zero V46() V57() V63() ) set ) , COMPLEX : ( ( ) ( non zero V46() V57() V63() ) set ) ) means :: SIN_COS3:def 2
for z being ( ( ) ( complex ) Element of COMPLEX : ( ( ) ( non zero V46() V57() V63() ) set ) ) holds it : ( ( ) ( ) set ) . z : ( ( ) ( complex ) Element of COMPLEX : ( ( ) ( non zero V46() V57() V63() ) set ) ) : ( ( ) ( complex ) Element of COMPLEX : ( ( ) ( non zero V46() V57() V63() ) set ) ) = ((exp ( : ( ( ) ( complex ) Element of COMPLEX : ( ( ) ( non zero V46() V57() V63() ) set ) ) * z : ( ( ) ( complex ) Element of COMPLEX : ( ( ) ( non zero V46() V57() V63() ) set ) ) ) : ( ( ) ( complex ) Element of COMPLEX : ( ( ) ( non zero V46() V57() V63() ) set ) ) ) : ( ( ) ( complex ) Element of COMPLEX : ( ( ) ( non zero V46() V57() V63() ) set ) ) + (exp (- ( : ( ( ) ( complex ) Element of COMPLEX : ( ( ) ( non zero V46() V57() V63() ) set ) ) * z : ( ( ) ( complex ) Element of COMPLEX : ( ( ) ( non zero V46() V57() V63() ) set ) ) ) : ( ( ) ( complex ) Element of COMPLEX : ( ( ) ( non zero V46() V57() V63() ) set ) ) ) : ( ( ) ( complex ) Element of COMPLEX : ( ( ) ( non zero V46() V57() V63() ) set ) ) ) : ( ( ) ( complex ) Element of COMPLEX : ( ( ) ( non zero V46() V57() V63() ) set ) ) ) : ( ( ) ( complex ) Element of COMPLEX : ( ( ) ( non zero V46() V57() V63() ) set ) ) / 2 : ( ( ) ( non zero natural complex V29() V30() V33() V34() V57() V58() V59() V60() V61() V62() ) Element of NAT : ( ( ) ( V57() V58() V59() V60() V61() V62() V63() ) Element of K19(REAL : ( ( ) ( non zero V46() V57() V58() V59() V63() ) set ) ) : ( ( ) ( ) set ) ) ) : ( ( ) ( complex ) Element of COMPLEX : ( ( ) ( non zero V46() V57() V63() ) set ) ) ;

end;

definition

func sinh_C -> ( ( V6() V18( COMPLEX : ( ( ) ( non zero V46() V57() V63() ) set ) , COMPLEX : ( ( ) ( non zero V46() V57() V63() ) set ) ) ) ( V1() V4( COMPLEX : ( ( ) ( non zero V46() V57() V63() ) set ) ) V5( COMPLEX : ( ( ) ( non zero V46() V57() V63() ) set ) ) V6() non zero total V18( COMPLEX : ( ( ) ( non zero V46() V57() V63() ) set ) , COMPLEX : ( ( ) ( non zero V46() V57() V63() ) set ) ) ) Function of COMPLEX : ( ( ) ( non zero V46() V57() V63() ) set ) , COMPLEX : ( ( ) ( non zero V46() V57() V63() ) set ) ) means :: SIN_COS3:def 3
for z being ( ( ) ( complex ) Element of COMPLEX : ( ( ) ( non zero V46() V57() V63() ) set ) ) holds it : ( ( ) ( ) set ) . z : ( ( ) ( complex ) Element of COMPLEX : ( ( ) ( non zero V46() V57() V63() ) set ) ) : ( ( ) ( complex ) Element of COMPLEX : ( ( ) ( non zero V46() V57() V63() ) set ) ) = ((exp z : ( ( ) ( complex ) Element of COMPLEX : ( ( ) ( non zero V46() V57() V63() ) set ) ) ) : ( ( ) ( complex ) Element of COMPLEX : ( ( ) ( non zero V46() V57() V63() ) set ) ) - (exp (- z : ( ( ) ( complex ) Element of COMPLEX : ( ( ) ( non zero V46() V57() V63() ) set ) ) ) : ( ( ) ( complex ) Element of COMPLEX : ( ( ) ( non zero V46() V57() V63() ) set ) ) ) : ( ( ) ( complex ) Element of COMPLEX : ( ( ) ( non zero V46() V57() V63() ) set ) ) ) : ( ( ) ( complex ) Element of COMPLEX : ( ( ) ( non zero V46() V57() V63() ) set ) ) / 2 : ( ( ) ( non zero natural complex V29() V30() V33() V34() V57() V58() V59() V60() V61() V62() ) Element of NAT : ( ( ) ( V57() V58() V59() V60() V61() V62() V63() ) Element of K19(REAL : ( ( ) ( non zero V46() V57() V58() V59() V63() ) set ) ) : ( ( ) ( ) set ) ) ) : ( ( ) ( complex ) Element of COMPLEX : ( ( ) ( non zero V46() V57() V63() ) set ) ) ;

end;

definition

func cosh_C -> ( ( V6() V18( COMPLEX : ( ( ) ( non zero V46() V57() V63() ) set ) , COMPLEX : ( ( ) ( non zero V46() V57() V63() ) set ) ) ) ( V1() V4( COMPLEX : ( ( ) ( non zero V46() V57() V63() ) set ) ) V5( COMPLEX : ( ( ) ( non zero V46() V57() V63() ) set ) ) V6() non zero total V18( COMPLEX : ( ( ) ( non zero V46() V57() V63() ) set ) , COMPLEX : ( ( ) ( non zero V46() V57() V63() ) set ) ) ) Function of COMPLEX : ( ( ) ( non zero V46() V57() V63() ) set ) , COMPLEX : ( ( ) ( non zero V46() V57() V63() ) set ) ) means :: SIN_COS3:def 4
for z being ( ( ) ( complex ) Element of COMPLEX : ( ( ) ( non zero V46() V57() V63() ) set ) ) holds it : ( ( ) ( ) set ) . z : ( ( ) ( complex ) Element of COMPLEX : ( ( ) ( non zero V46() V57() V63() ) set ) ) : ( ( ) ( complex ) Element of COMPLEX : ( ( ) ( non zero V46() V57() V63() ) set ) ) = ((exp z : ( ( ) ( complex ) Element of COMPLEX : ( ( ) ( non zero V46() V57() V63() ) set ) ) ) : ( ( ) ( complex ) Element of COMPLEX : ( ( ) ( non zero V46() V57() V63() ) set ) ) + (exp (- z : ( ( ) ( complex ) Element of COMPLEX : ( ( ) ( non zero V46() V57() V63() ) set ) ) ) : ( ( ) ( complex ) Element of COMPLEX : ( ( ) ( non zero V46() V57() V63() ) set ) ) ) : ( ( ) ( complex ) Element of COMPLEX : ( ( ) ( non zero V46() V57() V63() ) set ) ) ) : ( ( ) ( complex ) Element of COMPLEX : ( ( ) ( non zero V46() V57() V63() ) set ) ) / 2 : ( ( ) ( non zero natural complex V29() V30() V33() V34() V57() V58() V59() V60() V61() V62() ) Element of NAT : ( ( ) ( V57() V58() V59() V60() V61() V62() V63() ) Element of K19(REAL : ( ( ) ( non zero V46() V57() V58() V59() V63() ) set ) ) : ( ( ) ( ) set ) ) ) : ( ( ) ( complex ) Element of COMPLEX : ( ( ) ( non zero V46() V57() V63() ) set ) ) ;

end;

begin

theorem :: SIN_COS3:1

for z being ( ( ) ( complex ) Element of COMPLEX : ( ( ) ( non zero V46() V57() V63() ) set ) ) holds ((sin_C : ( ( V6() V18( COMPLEX : ( ( ) ( non zero V46() V57() V63() ) set ) , COMPLEX : ( ( ) ( non zero V46() V57() V63() ) set ) ) ) ( V1() V4( COMPLEX : ( ( ) ( non zero V46() V57() V63() ) set ) ) V5( COMPLEX : ( ( ) ( non zero V46() V57() V63() ) set ) ) V6() non zero total V18( COMPLEX : ( ( ) ( non zero V46() V57() V63() ) set ) , COMPLEX : ( ( ) ( non zero V46() V57() V63() ) set ) ) ) Function of COMPLEX : ( ( ) ( non zero V46() V57() V63() ) set ) , COMPLEX : ( ( ) ( non zero V46() V57() V63() ) set ) ) /. z : ( ( ) ( complex ) Element of COMPLEX : ( ( ) ( non zero V46() V57() V63() ) set ) ) ) : ( ( ) ( complex ) Element of COMPLEX : ( ( ) ( non zero V46() V57() V63() ) set ) ) * (sin_C : ( ( V6() V18( COMPLEX : ( ( ) ( non zero V46() V57() V63() ) set ) , COMPLEX : ( ( ) ( non zero V46() V57() V63() ) set ) ) ) ( V1() V4( COMPLEX : ( ( ) ( non zero V46() V57() V63() ) set ) ) V5( COMPLEX : ( ( ) ( non zero V46() V57() V63() ) set ) ) V6() non zero total V18( COMPLEX : ( ( ) ( non zero V46() V57() V63() ) set ) , COMPLEX : ( ( ) ( non zero V46() V57() V63() ) set ) ) ) Function of COMPLEX : ( ( ) ( non zero V46() V57() V63() ) set ) , COMPLEX : ( ( ) ( non zero V46() V57() V63() ) set ) ) /. z : ( ( ) ( complex ) Element of COMPLEX : ( ( ) ( non zero V46() V57() V63() ) set ) ) ) : ( ( ) ( complex ) Element of COMPLEX : ( ( ) ( non zero V46() V57() V63() ) set ) ) ) : ( ( ) ( complex ) Element of COMPLEX : ( ( ) ( non zero V46() V57() V63() ) set ) ) + ((cos_C : ( ( V6() V18( COMPLEX : ( ( ) ( non zero V46() V57() V63() ) set ) , COMPLEX : ( ( ) ( non zero V46() V57() V63() ) set ) ) ) ( V1() V4( COMPLEX : ( ( ) ( non zero V46() V57() V63() ) set ) ) V5( COMPLEX : ( ( ) ( non zero V46() V57() V63() ) set ) ) V6() non zero total V18( COMPLEX : ( ( ) ( non zero V46() V57() V63() ) set ) , COMPLEX : ( ( ) ( non zero V46() V57() V63() ) set ) ) ) Function of COMPLEX : ( ( ) ( non zero V46() V57() V63() ) set ) , COMPLEX : ( ( ) ( non zero V46() V57() V63() ) set ) ) /. z : ( ( ) ( complex ) Element of COMPLEX : ( ( ) ( non zero V46() V57() V63() ) set ) ) ) : ( ( ) ( complex ) Element of COMPLEX : ( ( ) ( non zero V46() V57() V63() ) set ) ) * (cos_C : ( ( V6() V18( COMPLEX : ( ( ) ( non zero V46() V57() V63() ) set ) , COMPLEX : ( ( ) ( non zero V46() V57() V63() ) set ) ) ) ( V1() V4( COMPLEX : ( ( ) ( non zero V46() V57() V63() ) set ) ) V5( COMPLEX : ( ( ) ( non zero V46() V57() V63() ) set ) ) V6() non zero total V18( COMPLEX : ( ( ) ( non zero V46() V57() V63() ) set ) , COMPLEX : ( ( ) ( non zero V46() V57() V63() ) set ) ) ) Function of COMPLEX : ( ( ) ( non zero V46() V57() V63() ) set ) , COMPLEX : ( ( ) ( non zero V46() V57() V63() ) set ) ) /. z : ( ( ) ( complex ) Element of COMPLEX : ( ( ) ( non zero V46() V57() V63() ) set ) ) ) : ( ( ) ( complex ) Element of COMPLEX : ( ( ) ( non zero V46() V57() V63() ) set ) ) ) : ( ( ) ( complex ) Element of COMPLEX : ( ( ) ( non zero V46() V57() V63() ) set ) ) : ( ( ) ( complex ) Element of COMPLEX : ( ( ) ( non zero V46() V57() V63() ) set ) ) = 1 : ( ( ) ( non zero natural complex V29() V30() V33() V34() V57() V58() V59() V60() V61() V62() ) Element of NAT : ( ( ) ( V57() V58() V59() V60() V61() V62() V63() ) Element of K19(REAL : ( ( ) ( non zero V46() V57() V58() V59() V63() ) set ) ) : ( ( ) ( ) set ) ) ) ;

theorem :: SIN_COS3:2

for z being ( ( complex ) ( complex ) number ) holds - (sin_C : ( ( V6() V18( COMPLEX : ( ( ) ( non zero V46() V57() V63() ) set ) , COMPLEX : ( ( ) ( non zero V46() V57() V63() ) set ) ) ) ( V1() V4( COMPLEX : ( ( ) ( non zero V46() V57() V63() ) set ) ) V5( COMPLEX : ( ( ) ( non zero V46() V57() V63() ) set ) ) V6() non zero total V18( COMPLEX : ( ( ) ( non zero V46() V57() V63() ) set ) , COMPLEX : ( ( ) ( non zero V46() V57() V63() ) set ) ) ) Function of COMPLEX : ( ( ) ( non zero V46() V57() V63() ) set ) , COMPLEX : ( ( ) ( non zero V46() V57() V63() ) set ) ) /. z : ( ( complex ) ( complex ) number ) ) : ( ( ) ( complex ) Element of COMPLEX : ( ( ) ( non zero V46() V57() V63() ) set ) ) : ( ( ) ( complex ) Element of COMPLEX : ( ( ) ( non zero V46() V57() V63() ) set ) ) = sin_C : ( ( V6() V18( COMPLEX : ( ( ) ( non zero V46() V57() V63() ) set ) , COMPLEX : ( ( ) ( non zero V46() V57() V63() ) set ) ) ) ( V1() V4( COMPLEX : ( ( ) ( non zero V46() V57() V63() ) set ) ) V5( COMPLEX : ( ( ) ( non zero V46() V57() V63() ) set ) ) V6() non zero total V18( COMPLEX : ( ( ) ( non zero V46() V57() V63() ) set ) , COMPLEX : ( ( ) ( non zero V46() V57() V63() ) set ) ) ) Function of COMPLEX : ( ( ) ( non zero V46() V57() V63() ) set ) , COMPLEX : ( ( ) ( non zero V46() V57() V63() ) set ) ) /. (- z : ( ( complex ) ( complex ) number ) ) : ( ( ) ( complex ) Element of COMPLEX : ( ( ) ( non zero V46() V57() V63() ) set ) ) : ( ( ) ( complex ) Element of COMPLEX : ( ( ) ( non zero V46() V57() V63() ) set ) ) ;

theorem :: SIN_COS3:3

for z being ( ( complex ) ( complex ) number ) holds cos_C : ( ( V6() V18( COMPLEX : ( ( ) ( non zero V46() V57() V63() ) set ) , COMPLEX : ( ( ) ( non zero V46() V57() V63() ) set ) ) ) ( V1() V4( COMPLEX : ( ( ) ( non zero V46() V57() V63() ) set ) ) V5( COMPLEX : ( ( ) ( non zero V46() V57() V63() ) set ) ) V6() non zero total V18( COMPLEX : ( ( ) ( non zero V46() V57() V63() ) set ) , COMPLEX : ( ( ) ( non zero V46() V57() V63() ) set ) ) ) Function of COMPLEX : ( ( ) ( non zero V46() V57() V63() ) set ) , COMPLEX : ( ( ) ( non zero V46() V57() V63() ) set ) ) /. z : ( ( complex ) ( complex ) number ) : ( ( ) ( complex ) Element of COMPLEX : ( ( ) ( non zero V46() V57() V63() ) set ) ) = cos_C : ( ( V6() V18( COMPLEX : ( ( ) ( non zero V46() V57() V63() ) set ) , COMPLEX : ( ( ) ( non zero V46() V57() V63() ) set ) ) ) ( V1() V4( COMPLEX : ( ( ) ( non zero V46() V57() V63() ) set ) ) V5( COMPLEX : ( ( ) ( non zero V46() V57() V63() ) set ) ) V6() non zero total V18( COMPLEX : ( ( ) ( non zero V46() V57() V63() ) set ) , COMPLEX : ( ( ) ( non zero V46() V57() V63() ) set ) ) ) Function of COMPLEX : ( ( ) ( non zero V46() V57() V63() ) set ) , COMPLEX : ( ( ) ( non zero V46() V57() V63() ) set ) ) /. (- z : ( ( complex ) ( complex ) number ) ) : ( ( ) ( complex ) Element of COMPLEX : ( ( ) ( non zero V46() V57() V63() ) set ) ) : ( ( ) ( complex ) Element of COMPLEX : ( ( ) ( non zero V46() V57() V63() ) set ) ) ;

theorem :: SIN_COS3:4

for z1, z2 being ( ( complex ) ( complex ) number ) holds sin_C : ( ( V6() V18( COMPLEX : ( ( ) ( non zero V46() V57() V63() ) set ) , COMPLEX : ( ( ) ( non zero V46() V57() V63() ) set ) ) ) ( V1() V4( COMPLEX : ( ( ) ( non zero V46() V57() V63() ) set ) ) V5( COMPLEX : ( ( ) ( non zero V46() V57() V63() ) set ) ) V6() non zero total V18( COMPLEX : ( ( ) ( non zero V46() V57() V63() ) set ) , COMPLEX : ( ( ) ( non zero V46() V57() V63() ) set ) ) ) Function of COMPLEX : ( ( ) ( non zero V46() V57() V63() ) set ) , COMPLEX : ( ( ) ( non zero V46() V57() V63() ) set ) ) /. (z1 : ( ( complex ) ( complex ) number ) + z2 : ( ( complex ) ( complex ) number ) ) : ( ( ) ( complex ) Element of COMPLEX : ( ( ) ( non zero V46() V57() V63() ) set ) ) : ( ( ) ( complex ) Element of COMPLEX : ( ( ) ( non zero V46() V57() V63() ) set ) ) = ((sin_C : ( ( V6() V18( COMPLEX : ( ( ) ( non zero V46() V57() V63() ) set ) , COMPLEX : ( ( ) ( non zero V46() V57() V63() ) set ) ) ) ( V1() V4( COMPLEX : ( ( ) ( non zero V46() V57() V63() ) set ) ) V5( COMPLEX : ( ( ) ( non zero V46() V57() V63() ) set ) ) V6() non zero total V18( COMPLEX : ( ( ) ( non zero V46() V57() V63() ) set ) , COMPLEX : ( ( ) ( non zero V46() V57() V63() ) set ) ) ) Function of COMPLEX : ( ( ) ( non zero V46() V57() V63() ) set ) , COMPLEX : ( ( ) ( non zero V46() V57() V63() ) set ) ) /. z1 : ( ( complex ) ( complex ) number ) ) : ( ( ) ( complex ) Element of COMPLEX : ( ( ) ( non zero V46() V57() V63() ) set ) ) * (cos_C : ( ( V6() V18( COMPLEX : ( ( ) ( non zero V46() V57() V63() ) set ) , COMPLEX : ( ( ) ( non zero V46() V57() V63() ) set ) ) ) ( V1() V4( COMPLEX : ( ( ) ( non zero V46() V57() V63() ) set ) ) V5( COMPLEX : ( ( ) ( non zero V46() V57() V63() ) set ) ) V6() non zero total V18( COMPLEX : ( ( ) ( non zero V46() V57() V63() ) set ) , COMPLEX : ( ( ) ( non zero V46() V57() V63() ) set ) ) ) Function of COMPLEX : ( ( ) ( non zero V46() V57() V63() ) set ) , COMPLEX : ( ( ) ( non zero V46() V57() V63() ) set ) ) /. z2 : ( ( complex ) ( complex ) number ) ) : ( ( ) ( complex ) Element of COMPLEX : ( ( ) ( non zero V46() V57() V63() ) set ) ) ) : ( ( ) ( complex ) Element of COMPLEX : ( ( ) ( non zero V46() V57() V63() ) set ) ) + ((cos_C : ( ( V6() V18( COMPLEX : ( ( ) ( non zero V46() V57() V63() ) set ) , COMPLEX : ( ( ) ( non zero V46() V57() V63() ) set ) ) ) ( V1() V4( COMPLEX : ( ( ) ( non zero V46() V57() V63() ) set ) ) V5( COMPLEX : ( ( ) ( non zero V46() V57() V63() ) set ) ) V6() non zero total V18( COMPLEX : ( ( ) ( non zero V46() V57() V63() ) set ) , COMPLEX : ( ( ) ( non zero V46() V57() V63() ) set ) ) ) Function of COMPLEX : ( ( ) ( non zero V46() V57() V63() ) set ) , COMPLEX : ( ( ) ( non zero V46() V57() V63() ) set ) ) /. z1 : ( ( complex ) ( complex ) number ) ) : ( ( ) ( complex ) Element of COMPLEX : ( ( ) ( non zero V46() V57() V63() ) set ) ) * (sin_C : ( ( V6() V18( COMPLEX : ( ( ) ( non zero V46() V57() V63() ) set ) , COMPLEX : ( ( ) ( non zero V46() V57() V63() ) set ) ) ) ( V1() V4( COMPLEX : ( ( ) ( non zero V46() V57() V63() ) set ) ) V5( COMPLEX : ( ( ) ( non zero V46() V57() V63() ) set ) ) V6() non zero total V18( COMPLEX : ( ( ) ( non zero V46() V57() V63() ) set ) , COMPLEX : ( ( ) ( non zero V46() V57() V63() ) set ) ) ) Function of COMPLEX : ( ( ) ( non zero V46() V57() V63() ) set ) , COMPLEX : ( ( ) ( non zero V46() V57() V63() ) set ) ) /. z2 : ( ( complex ) ( complex ) number ) ) : ( ( ) ( complex ) Element of COMPLEX : ( ( ) ( non zero V46() V57() V63() ) set ) ) ) : ( ( ) ( complex ) Element of COMPLEX : ( ( ) ( non zero V46() V57() V63() ) set ) ) : ( ( ) ( complex ) Element of COMPLEX : ( ( ) ( non zero V46() V57() V63() ) set ) ) ;

theorem :: SIN_COS3:5

for z1, z2 being ( ( ) ( complex ) Element of COMPLEX : ( ( ) ( non zero V46() V57() V63() ) set ) ) holds sin_C : ( ( V6() V18( COMPLEX : ( ( ) ( non zero V46() V57() V63() ) set ) , COMPLEX : ( ( ) ( non zero V46() V57() V63() ) set ) ) ) ( V1() V4( COMPLEX : ( ( ) ( non zero V46() V57() V63() ) set ) ) V5( COMPLEX : ( ( ) ( non zero V46() V57() V63() ) set ) ) V6() non zero total V18( COMPLEX : ( ( ) ( non zero V46() V57() V63() ) set ) , COMPLEX : ( ( ) ( non zero V46() V57() V63() ) set ) ) ) Function of COMPLEX : ( ( ) ( non zero V46() V57() V63() ) set ) , COMPLEX : ( ( ) ( non zero V46() V57() V63() ) set ) ) /. (z1 : ( ( ) ( complex ) Element of COMPLEX : ( ( ) ( non zero V46() V57() V63() ) set ) ) - z2 : ( ( ) ( complex ) Element of COMPLEX : ( ( ) ( non zero V46() V57() V63() ) set ) ) ) : ( ( ) ( complex ) Element of COMPLEX : ( ( ) ( non zero V46() V57() V63() ) set ) ) : ( ( ) ( complex ) Element of COMPLEX : ( ( ) ( non zero V46() V57() V63() ) set ) ) = ((sin_C : ( ( V6() V18( COMPLEX : ( ( ) ( non zero V46() V57() V63() ) set ) , COMPLEX : ( ( ) ( non zero V46() V57() V63() ) set ) ) ) ( V1() V4( COMPLEX : ( ( ) ( non zero V46() V57() V63() ) set ) ) V5( COMPLEX : ( ( ) ( non zero V46() V57() V63() ) set ) ) V6() non zero total V18( COMPLEX : ( ( ) ( non zero V46() V57() V63() ) set ) , COMPLEX : ( ( ) ( non zero V46() V57() V63() ) set ) ) ) Function of COMPLEX : ( ( ) ( non zero V46() V57() V63() ) set ) , COMPLEX : ( ( ) ( non zero V46() V57() V63() ) set ) ) /. z1 : ( ( ) ( complex ) Element of COMPLEX : ( ( ) ( non zero V46() V57() V63() ) set ) ) ) : ( ( ) ( complex ) Element of COMPLEX : ( ( ) ( non zero V46() V57() V63() ) set ) ) * (cos_C : ( ( V6() V18( COMPLEX : ( ( ) ( non zero V46() V57() V63() ) set ) , COMPLEX : ( ( ) ( non zero V46() V57() V63() ) set ) ) ) ( V1() V4( COMPLEX : ( ( ) ( non zero V46() V57() V63() ) set ) ) V5( COMPLEX : ( ( ) ( non zero V46() V57() V63() ) set ) ) V6() non zero total V18( COMPLEX : ( ( ) ( non zero V46() V57() V63() ) set ) , COMPLEX : ( ( ) ( non zero V46() V57() V63() ) set ) ) ) Function of COMPLEX : ( ( ) ( non zero V46() V57() V63() ) set ) , COMPLEX : ( ( ) ( non zero V46() V57() V63() ) set ) ) /. z2 : ( ( ) ( complex ) Element of COMPLEX : ( ( ) ( non zero V46() V57() V63() ) set ) ) ) : ( ( ) ( complex ) Element of COMPLEX : ( ( ) ( non zero V46() V57() V63() ) set ) ) ) : ( ( ) ( complex ) Element of COMPLEX : ( ( ) ( non zero V46() V57() V63() ) set ) ) - ((cos_C : ( ( V6() V18( COMPLEX : ( ( ) ( non zero V46() V57() V63() ) set ) , COMPLEX : ( ( ) ( non zero V46() V57() V63() ) set ) ) ) ( V1() V4( COMPLEX : ( ( ) ( non zero V46() V57() V63() ) set ) ) V5( COMPLEX : ( ( ) ( non zero V46() V57() V63() ) set ) ) V6() non zero total V18( COMPLEX : ( ( ) ( non zero V46() V57() V63() ) set ) , COMPLEX : ( ( ) ( non zero V46() V57() V63() ) set ) ) ) Function of COMPLEX : ( ( ) ( non zero V46() V57() V63() ) set ) , COMPLEX : ( ( ) ( non zero V46() V57() V63() ) set ) ) /. z1 : ( ( ) ( complex ) Element of COMPLEX : ( ( ) ( non zero V46() V57() V63() ) set ) ) ) : ( ( ) ( complex ) Element of COMPLEX : ( ( ) ( non zero V46() V57() V63() ) set ) ) * (sin_C : ( ( V6() V18( COMPLEX : ( ( ) ( non zero V46() V57() V63() ) set ) , COMPLEX : ( ( ) ( non zero V46() V57() V63() ) set ) ) ) ( V1() V4( COMPLEX : ( ( ) ( non zero V46() V57() V63() ) set ) ) V5( COMPLEX : ( ( ) ( non zero V46() V57() V63() ) set ) ) V6() non zero total V18( COMPLEX : ( ( ) ( non zero V46() V57() V63() ) set ) , COMPLEX : ( ( ) ( non zero V46() V57() V63() ) set ) ) ) Function of COMPLEX : ( ( ) ( non zero V46() V57() V63() ) set ) , COMPLEX : ( ( ) ( non zero V46() V57() V63() ) set ) ) /. z2 : ( ( ) ( complex ) Element of COMPLEX : ( ( ) ( non zero V46() V57() V63() ) set ) ) ) : ( ( ) ( complex ) Element of COMPLEX : ( ( ) ( non zero V46() V57() V63() ) set ) ) ) : ( ( ) ( complex ) Element of COMPLEX : ( ( ) ( non zero V46() V57() V63() ) set ) ) : ( ( ) ( complex ) Element of COMPLEX : ( ( ) ( non zero V46() V57() V63() ) set ) ) ;

theorem :: SIN_COS3:6

for z1, z2 being ( ( complex ) ( complex ) number ) holds cos_C : ( ( V6() V18( COMPLEX : ( ( ) ( non zero V46() V57() V63() ) set ) , COMPLEX : ( ( ) ( non zero V46() V57() V63() ) set ) ) ) ( V1() V4( COMPLEX : ( ( ) ( non zero V46() V57() V63() ) set ) ) V5( COMPLEX : ( ( ) ( non zero V46() V57() V63() ) set ) ) V6() non zero total V18( COMPLEX : ( ( ) ( non zero V46() V57() V63() ) set ) , COMPLEX : ( ( ) ( non zero V46() V57() V63() ) set ) ) ) Function of COMPLEX : ( ( ) ( non zero V46() V57() V63() ) set ) , COMPLEX : ( ( ) ( non zero V46() V57() V63() ) set ) ) /. (z1 : ( ( complex ) ( complex ) number ) + z2 : ( ( complex ) ( complex ) number ) ) : ( ( ) ( complex ) Element of COMPLEX : ( ( ) ( non zero V46() V57() V63() ) set ) ) : ( ( ) ( complex ) Element of COMPLEX : ( ( ) ( non zero V46() V57() V63() ) set ) ) = ((cos_C : ( ( V6() V18( COMPLEX : ( ( ) ( non zero V46() V57() V63() ) set ) , COMPLEX : ( ( ) ( non zero V46() V57() V63() ) set ) ) ) ( V1() V4( COMPLEX : ( ( ) ( non zero V46() V57() V63() ) set ) ) V5( COMPLEX : ( ( ) ( non zero V46() V57() V63() ) set ) ) V6() non zero total V18( COMPLEX : ( ( ) ( non zero V46() V57() V63() ) set ) , COMPLEX : ( ( ) ( non zero V46() V57() V63() ) set ) ) ) Function of COMPLEX : ( ( ) ( non zero V46() V57() V63() ) set ) , COMPLEX : ( ( ) ( non zero V46() V57() V63() ) set ) ) /. z1 : ( ( complex ) ( complex ) number ) ) : ( ( ) ( complex ) Element of COMPLEX : ( ( ) ( non zero V46() V57() V63() ) set ) ) * (cos_C : ( ( V6() V18( COMPLEX : ( ( ) ( non zero V46() V57() V63() ) set ) , COMPLEX : ( ( ) ( non zero V46() V57() V63() ) set ) ) ) ( V1() V4( COMPLEX : ( ( ) ( non zero V46() V57() V63() ) set ) ) V5( COMPLEX : ( ( ) ( non zero V46() V57() V63() ) set ) ) V6() non zero total V18( COMPLEX : ( ( ) ( non zero V46() V57() V63() ) set ) , COMPLEX : ( ( ) ( non zero V46() V57() V63() ) set ) ) ) Function of COMPLEX : ( ( ) ( non zero V46() V57() V63() ) set ) , COMPLEX : ( ( ) ( non zero V46() V57() V63() ) set ) ) /. z2 : ( ( complex ) ( complex ) number ) ) : ( ( ) ( complex ) Element of COMPLEX : ( ( ) ( non zero V46() V57() V63() ) set ) ) ) : ( ( ) ( complex ) Element of COMPLEX : ( ( ) ( non zero V46() V57() V63() ) set ) ) - ((sin_C : ( ( V6() V18( COMPLEX : ( ( ) ( non zero V46() V57() V63() ) set ) , COMPLEX : ( ( ) ( non zero V46() V57() V63() ) set ) ) ) ( V1() V4( COMPLEX : ( ( ) ( non zero V46() V57() V63() ) set ) ) V5( COMPLEX : ( ( ) ( non zero V46() V57() V63() ) set ) ) V6() non zero total V18( COMPLEX : ( ( ) ( non zero V46() V57() V63() ) set ) , COMPLEX : ( ( ) ( non zero V46() V57() V63() ) set ) ) ) Function of COMPLEX : ( ( ) ( non zero V46() V57() V63() ) set ) , COMPLEX : ( ( ) ( non zero V46() V57() V63() ) set ) ) /. z1 : ( ( complex ) ( complex ) number ) ) : ( ( ) ( complex ) Element of COMPLEX : ( ( ) ( non zero V46() V57() V63() ) set ) ) * (sin_C : ( ( V6() V18( COMPLEX : ( ( ) ( non zero V46() V57() V63() ) set ) , COMPLEX : ( ( ) ( non zero V46() V57() V63() ) set ) ) ) ( V1() V4( COMPLEX : ( ( ) ( non zero V46() V57() V63() ) set ) ) V5( COMPLEX : ( ( ) ( non zero V46() V57() V63() ) set ) ) V6() non zero total V18( COMPLEX : ( ( ) ( non zero V46() V57() V63() ) set ) , COMPLEX : ( ( ) ( non zero V46() V57() V63() ) set ) ) ) Function of COMPLEX : ( ( ) ( non zero V46() V57() V63() ) set ) , COMPLEX : ( ( ) ( non zero V46() V57() V63() ) set ) ) /. z2 : ( ( complex ) ( complex ) number ) ) : ( ( ) ( complex ) Element of COMPLEX : ( ( ) ( non zero V46() V57() V63() ) set ) ) ) : ( ( ) ( complex ) Element of COMPLEX : ( ( ) ( non zero V46() V57() V63() ) set ) ) : ( ( ) ( complex ) Element of COMPLEX : ( ( ) ( non zero V46() V57() V63() ) set ) ) ;

theorem :: SIN_COS3:7

for z1, z2 being ( ( ) ( complex ) Element of COMPLEX : ( ( ) ( non zero V46() V57() V63() ) set ) ) holds cos_C : ( ( V6() V18( COMPLEX : ( ( ) ( non zero V46() V57() V63() ) set ) , COMPLEX : ( ( ) ( non zero V46() V57() V63() ) set ) ) ) ( V1() V4( COMPLEX : ( ( ) ( non zero V46() V57() V63() ) set ) ) V5( COMPLEX : ( ( ) ( non zero V46() V57() V63() ) set ) ) V6() non zero total V18( COMPLEX : ( ( ) ( non zero V46() V57() V63() ) set ) , COMPLEX : ( ( ) ( non zero V46() V57() V63() ) set ) ) ) Function of COMPLEX : ( ( ) ( non zero V46() V57() V63() ) set ) , COMPLEX : ( ( ) ( non zero V46() V57() V63() ) set ) ) /. (z1 : ( ( ) ( complex ) Element of COMPLEX : ( ( ) ( non zero V46() V57() V63() ) set ) ) - z2 : ( ( ) ( complex ) Element of COMPLEX : ( ( ) ( non zero V46() V57() V63() ) set ) ) ) : ( ( ) ( complex ) Element of COMPLEX : ( ( ) ( non zero V46() V57() V63() ) set ) ) : ( ( ) ( complex ) Element of COMPLEX : ( ( ) ( non zero V46() V57() V63() ) set ) ) = ((cos_C : ( ( V6() V18( COMPLEX : ( ( ) ( non zero V46() V57() V63() ) set ) , COMPLEX : ( ( ) ( non zero V46() V57() V63() ) set ) ) ) ( V1() V4( COMPLEX : ( ( ) ( non zero V46() V57() V63() ) set ) ) V5( COMPLEX : ( ( ) ( non zero V46() V57() V63() ) set ) ) V6() non zero total V18( COMPLEX : ( ( ) ( non zero V46() V57() V63() ) set ) , COMPLEX : ( ( ) ( non zero V46() V57() V63() ) set ) ) ) Function of COMPLEX : ( ( ) ( non zero V46() V57() V63() ) set ) , COMPLEX : ( ( ) ( non zero V46() V57() V63() ) set ) ) /. z1 : ( ( ) ( complex ) Element of COMPLEX : ( ( ) ( non zero V46() V57() V63() ) set ) ) ) : ( ( ) ( complex ) Element of COMPLEX : ( ( ) ( non zero V46() V57() V63() ) set ) ) * (cos_C : ( ( V6() V18( COMPLEX : ( ( ) ( non zero V46() V57() V63() ) set ) , COMPLEX : ( ( ) ( non zero V46() V57() V63() ) set ) ) ) ( V1() V4( COMPLEX : ( ( ) ( non zero V46() V57() V63() ) set ) ) V5( COMPLEX : ( ( ) ( non zero V46() V57() V63() ) set ) ) V6() non zero total V18( COMPLEX : ( ( ) ( non zero V46() V57() V63() ) set ) , COMPLEX : ( ( ) ( non zero V46() V57() V63() ) set ) ) ) Function of COMPLEX : ( ( ) ( non zero V46() V57() V63() ) set ) , COMPLEX : ( ( ) ( non zero V46() V57() V63() ) set ) ) /. z2 : ( ( ) ( complex ) Element of COMPLEX : ( ( ) ( non zero V46() V57() V63() ) set ) ) ) : ( ( ) ( complex ) Element of COMPLEX : ( ( ) ( non zero V46() V57() V63() ) set ) ) ) : ( ( ) ( complex ) Element of COMPLEX : ( ( ) ( non zero V46() V57() V63() ) set ) ) + ((sin_C : ( ( V6() V18( COMPLEX : ( ( ) ( non zero V46() V57() V63() ) set ) , COMPLEX : ( ( ) ( non zero V46() V57() V63() ) set ) ) ) ( V1() V4( COMPLEX : ( ( ) ( non zero V46() V57() V63() ) set ) ) V5( COMPLEX : ( ( ) ( non zero V46() V57() V63() ) set ) ) V6() non zero total V18( COMPLEX : ( ( ) ( non zero V46() V57() V63() ) set ) , COMPLEX : ( ( ) ( non zero V46() V57() V63() ) set ) ) ) Function of COMPLEX : ( ( ) ( non zero V46() V57() V63() ) set ) , COMPLEX : ( ( ) ( non zero V46() V57() V63() ) set ) ) /. z1 : ( ( ) ( complex ) Element of COMPLEX : ( ( ) ( non zero V46() V57() V63() ) set ) ) ) : ( ( ) ( complex ) Element of COMPLEX : ( ( ) ( non zero V46() V57() V63() ) set ) ) * (sin_C : ( ( V6() V18( COMPLEX : ( ( ) ( non zero V46() V57() V63() ) set ) , COMPLEX : ( ( ) ( non zero V46() V57() V63() ) set ) ) ) ( V1() V4( COMPLEX : ( ( ) ( non zero V46() V57() V63() ) set ) ) V5( COMPLEX : ( ( ) ( non zero V46() V57() V63() ) set ) ) V6() non zero total V18( COMPLEX : ( ( ) ( non zero V46() V57() V63() ) set ) , COMPLEX : ( ( ) ( non zero V46() V57() V63() ) set ) ) ) Function of COMPLEX : ( ( ) ( non zero V46() V57() V63() ) set ) , COMPLEX : ( ( ) ( non zero V46() V57() V63() ) set ) ) /. z2 : ( ( ) ( complex ) Element of COMPLEX : ( ( ) ( non zero V46() V57() V63() ) set ) ) ) : ( ( ) ( complex ) Element of COMPLEX : ( ( ) ( non zero V46() V57() V63() ) set ) ) ) : ( ( ) ( complex ) Element of COMPLEX : ( ( ) ( non zero V46() V57() V63() ) set ) ) : ( ( ) ( complex ) Element of COMPLEX : ( ( ) ( non zero V46() V57() V63() ) set ) ) ;

theorem :: SIN_COS3:8

for z being ( ( ) ( complex ) Element of COMPLEX : ( ( ) ( non zero V46() V57() V63() ) set ) ) holds ((cosh_C : ( ( V6() V18( COMPLEX : ( ( ) ( non zero V46() V57() V63() ) set ) , COMPLEX : ( ( ) ( non zero V46() V57() V63() ) set ) ) ) ( V1() V4( COMPLEX : ( ( ) ( non zero V46() V57() V63() ) set ) ) V5( COMPLEX : ( ( ) ( non zero V46() V57() V63() ) set ) ) V6() non zero total V18( COMPLEX : ( ( ) ( non zero V46() V57() V63() ) set ) , COMPLEX : ( ( ) ( non zero V46() V57() V63() ) set ) ) ) Function of COMPLEX : ( ( ) ( non zero V46() V57() V63() ) set ) , COMPLEX : ( ( ) ( non zero V46() V57() V63() ) set ) ) /. z : ( ( ) ( complex ) Element of COMPLEX : ( ( ) ( non zero V46() V57() V63() ) set ) ) ) : ( ( ) ( complex ) Element of COMPLEX : ( ( ) ( non zero V46() V57() V63() ) set ) ) * (cosh_C : ( ( V6() V18( COMPLEX : ( ( ) ( non zero V46() V57() V63() ) set ) , COMPLEX : ( ( ) ( non zero V46() V57() V63() ) set ) ) ) ( V1() V4( COMPLEX : ( ( ) ( non zero V46() V57() V63() ) set ) ) V5( COMPLEX : ( ( ) ( non zero V46() V57() V63() ) set ) ) V6() non zero total V18( COMPLEX : ( ( ) ( non zero V46() V57() V63() ) set ) , COMPLEX : ( ( ) ( non zero V46() V57() V63() ) set ) ) ) Function of COMPLEX : ( ( ) ( non zero V46() V57() V63() ) set ) , COMPLEX : ( ( ) ( non zero V46() V57() V63() ) set ) ) /. z : ( ( ) ( complex ) Element of COMPLEX : ( ( ) ( non zero V46() V57() V63() ) set ) ) ) : ( ( ) ( complex ) Element of COMPLEX : ( ( ) ( non zero V46() V57() V63() ) set ) ) ) : ( ( ) ( complex ) Element of COMPLEX : ( ( ) ( non zero V46() V57() V63() ) set ) ) - ((sinh_C : ( ( V6() V18( COMPLEX : ( ( ) ( non zero V46() V57() V63() ) set ) , COMPLEX : ( ( ) ( non zero V46() V57() V63() ) set ) ) ) ( V1() V4( COMPLEX : ( ( ) ( non zero V46() V57() V63() ) set ) ) V5( COMPLEX : ( ( ) ( non zero V46() V57() V63() ) set ) ) V6() non zero total V18( COMPLEX : ( ( ) ( non zero V46() V57() V63() ) set ) , COMPLEX : ( ( ) ( non zero V46() V57() V63() ) set ) ) ) Function of COMPLEX : ( ( ) ( non zero V46() V57() V63() ) set ) , COMPLEX : ( ( ) ( non zero V46() V57() V63() ) set ) ) /. z : ( ( ) ( complex ) Element of COMPLEX : ( ( ) ( non zero V46() V57() V63() ) set ) ) ) : ( ( ) ( complex ) Element of COMPLEX : ( ( ) ( non zero V46() V57() V63() ) set ) ) * (sinh_C : ( ( V6() V18( COMPLEX : ( ( ) ( non zero V46() V57() V63() ) set ) , COMPLEX : ( ( ) ( non zero V46() V57() V63() ) set ) ) ) ( V1() V4( COMPLEX : ( ( ) ( non zero V46() V57() V63() ) set ) ) V5( COMPLEX : ( ( ) ( non zero V46() V57() V63() ) set ) ) V6() non zero total V18( COMPLEX : ( ( ) ( non zero V46() V57() V63() ) set ) , COMPLEX : ( ( ) ( non zero V46() V57() V63() ) set ) ) ) Function of COMPLEX : ( ( ) ( non zero V46() V57() V63() ) set ) , COMPLEX : ( ( ) ( non zero V46() V57() V63() ) set ) ) /. z : ( ( ) ( complex ) Element of COMPLEX : ( ( ) ( non zero V46() V57() V63() ) set ) ) ) : ( ( ) ( complex ) Element of COMPLEX : ( ( ) ( non zero V46() V57() V63() ) set ) ) ) : ( ( ) ( complex ) Element of COMPLEX : ( ( ) ( non zero V46() V57() V63() ) set ) ) : ( ( ) ( complex ) Element of COMPLEX : ( ( ) ( non zero V46() V57() V63() ) set ) ) = 1 : ( ( ) ( non zero natural complex V29() V30() V33() V34() V57() V58() V59() V60() V61() V62() ) Element of NAT : ( ( ) ( V57() V58() V59() V60() V61() V62() V63() ) Element of K19(REAL : ( ( ) ( non zero V46() V57() V58() V59() V63() ) set ) ) : ( ( ) ( ) set ) ) ) ;

theorem :: SIN_COS3:9

for z being ( ( ) ( complex ) Element of COMPLEX : ( ( ) ( non zero V46() V57() V63() ) set ) ) holds - (sinh_C : ( ( V6() V18( COMPLEX : ( ( ) ( non zero V46() V57() V63() ) set ) , COMPLEX : ( ( ) ( non zero V46() V57() V63() ) set ) ) ) ( V1() V4( COMPLEX : ( ( ) ( non zero V46() V57() V63() ) set ) ) V5( COMPLEX : ( ( ) ( non zero V46() V57() V63() ) set ) ) V6() non zero total V18( COMPLEX : ( ( ) ( non zero V46() V57() V63() ) set ) , COMPLEX : ( ( ) ( non zero V46() V57() V63() ) set ) ) ) Function of COMPLEX : ( ( ) ( non zero V46() V57() V63() ) set ) , COMPLEX : ( ( ) ( non zero V46() V57() V63() ) set ) ) /. z : ( ( ) ( complex ) Element of COMPLEX : ( ( ) ( non zero V46() V57() V63() ) set ) ) ) : ( ( ) ( complex ) Element of COMPLEX : ( ( ) ( non zero V46() V57() V63() ) set ) ) : ( ( ) ( complex ) Element of COMPLEX : ( ( ) ( non zero V46() V57() V63() ) set ) ) = sinh_C : ( ( V6() V18( COMPLEX : ( ( ) ( non zero V46() V57() V63() ) set ) , COMPLEX : ( ( ) ( non zero V46() V57() V63() ) set ) ) ) ( V1() V4( COMPLEX : ( ( ) ( non zero V46() V57() V63() ) set ) ) V5( COMPLEX : ( ( ) ( non zero V46() V57() V63() ) set ) ) V6() non zero total V18( COMPLEX : ( ( ) ( non zero V46() V57() V63() ) set ) , COMPLEX : ( ( ) ( non zero V46() V57() V63() ) set ) ) ) Function of COMPLEX : ( ( ) ( non zero V46() V57() V63() ) set ) , COMPLEX : ( ( ) ( non zero V46() V57() V63() ) set ) ) /. (- z : ( ( ) ( complex ) Element of COMPLEX : ( ( ) ( non zero V46() V57() V63() ) set ) ) ) : ( ( ) ( complex ) Element of COMPLEX : ( ( ) ( non zero V46() V57() V63() ) set ) ) : ( ( ) ( complex ) Element of COMPLEX : ( ( ) ( non zero V46() V57() V63() ) set ) ) ;

theorem :: SIN_COS3:10

for z being ( ( ) ( complex ) Element of COMPLEX : ( ( ) ( non zero V46() V57() V63() ) set ) ) holds cosh_C : ( ( V6() V18( COMPLEX : ( ( ) ( non zero V46() V57() V63() ) set ) , COMPLEX : ( ( ) ( non zero V46() V57() V63() ) set ) ) ) ( V1() V4( COMPLEX : ( ( ) ( non zero V46() V57() V63() ) set ) ) V5( COMPLEX : ( ( ) ( non zero V46() V57() V63() ) set ) ) V6() non zero total V18( COMPLEX : ( ( ) ( non zero V46() V57() V63() ) set ) , COMPLEX : ( ( ) ( non zero V46() V57() V63() ) set ) ) ) Function of COMPLEX : ( ( ) ( non zero V46() V57() V63() ) set ) , COMPLEX : ( ( ) ( non zero V46() V57() V63() ) set ) ) /. z : ( ( ) ( complex ) Element of COMPLEX : ( ( ) ( non zero V46() V57() V63() ) set ) ) : ( ( ) ( complex ) Element of COMPLEX : ( ( ) ( non zero V46() V57() V63() ) set ) ) = cosh_C : ( ( V6() V18( COMPLEX : ( ( ) ( non zero V46() V57() V63() ) set ) , COMPLEX : ( ( ) ( non zero V46() V57() V63() ) set ) ) ) ( V1() V4( COMPLEX : ( ( ) ( non zero V46() V57() V63() ) set ) ) V5( COMPLEX : ( ( ) ( non zero V46() V57() V63() ) set ) ) V6() non zero total V18( COMPLEX : ( ( ) ( non zero V46() V57() V63() ) set ) , COMPLEX : ( ( ) ( non zero V46() V57() V63() ) set ) ) ) Function of COMPLEX : ( ( ) ( non zero V46() V57() V63() ) set ) , COMPLEX : ( ( ) ( non zero V46() V57() V63() ) set ) ) /. (- z : ( ( ) ( complex ) Element of COMPLEX : ( ( ) ( non zero V46() V57() V63() ) set ) ) ) : ( ( ) ( complex ) Element of COMPLEX : ( ( ) ( non zero V46() V57() V63() ) set ) ) : ( ( ) ( complex ) Element of COMPLEX : ( ( ) ( non zero V46() V57() V63() ) set ) ) ;

theorem :: SIN_COS3:11

for z1, z2 being ( ( ) ( complex ) Element of COMPLEX : ( ( ) ( non zero V46() V57() V63() ) set ) ) holds sinh_C : ( ( V6() V18( COMPLEX : ( ( ) ( non zero V46() V57() V63() ) set ) , COMPLEX : ( ( ) ( non zero V46() V57() V63() ) set ) ) ) ( V1() V4( COMPLEX : ( ( ) ( non zero V46() V57() V63() ) set ) ) V5( COMPLEX : ( ( ) ( non zero V46() V57() V63() ) set ) ) V6() non zero total V18( COMPLEX : ( ( ) ( non zero V46() V57() V63() ) set ) , COMPLEX : ( ( ) ( non zero V46() V57() V63() ) set ) ) ) Function of COMPLEX : ( ( ) ( non zero V46() V57() V63() ) set ) , COMPLEX : ( ( ) ( non zero V46() V57() V63() ) set ) ) /. (z1 : ( ( ) ( complex ) Element of COMPLEX : ( ( ) ( non zero V46() V57() V63() ) set ) ) + z2 : ( ( ) ( complex ) Element of COMPLEX : ( ( ) ( non zero V46() V57() V63() ) set ) ) ) : ( ( ) ( complex ) Element of COMPLEX : ( ( ) ( non zero V46() V57() V63() ) set ) ) : ( ( ) ( complex ) Element of COMPLEX : ( ( ) ( non zero V46() V57() V63() ) set ) ) = ((sinh_C : ( ( V6() V18( COMPLEX : ( ( ) ( non zero V46() V57() V63() ) set ) , COMPLEX : ( ( ) ( non zero V46() V57() V63() ) set ) ) ) ( V1() V4( COMPLEX : ( ( ) ( non zero V46() V57() V63() ) set ) ) V5( COMPLEX : ( ( ) ( non zero V46() V57() V63() ) set ) ) V6() non zero total V18( COMPLEX : ( ( ) ( non zero V46() V57() V63() ) set ) , COMPLEX : ( ( ) ( non zero V46() V57() V63() ) set ) ) ) Function of COMPLEX : ( ( ) ( non zero V46() V57() V63() ) set ) , COMPLEX : ( ( ) ( non zero V46() V57() V63() ) set ) ) /. z1 : ( ( ) ( complex ) Element of COMPLEX : ( ( ) ( non zero V46() V57() V63() ) set ) ) ) : ( ( ) ( complex ) Element of COMPLEX : ( ( ) ( non zero V46() V57() V63() ) set ) ) * (cosh_C : ( ( V6() V18( COMPLEX : ( ( ) ( non zero V46() V57() V63() ) set ) , COMPLEX : ( ( ) ( non zero V46() V57() V63() ) set ) ) ) ( V1() V4( COMPLEX : ( ( ) ( non zero V46() V57() V63() ) set ) ) V5( COMPLEX : ( ( ) ( non zero V46() V57() V63() ) set ) ) V6() non zero total V18( COMPLEX : ( ( ) ( non zero V46() V57() V63() ) set ) , COMPLEX : ( ( ) ( non zero V46() V57() V63() ) set ) ) ) Function of COMPLEX : ( ( ) ( non zero V46() V57() V63() ) set ) , COMPLEX : ( ( ) ( non zero V46() V57() V63() ) set ) ) /. z2 : ( ( ) ( complex ) Element of COMPLEX : ( ( ) ( non zero V46() V57() V63() ) set ) ) ) : ( ( ) ( complex ) Element of COMPLEX : ( ( ) ( non zero V46() V57() V63() ) set ) ) ) : ( ( ) ( complex ) Element of COMPLEX : ( ( ) ( non zero V46() V57() V63() ) set ) ) + ((cosh_C : ( ( V6() V18( COMPLEX : ( ( ) ( non zero V46() V57() V63() ) set ) , COMPLEX : ( ( ) ( non zero V46() V57() V63() ) set ) ) ) ( V1() V4( COMPLEX : ( ( ) ( non zero V46() V57() V63() ) set ) ) V5( COMPLEX : ( ( ) ( non zero V46() V57() V63() ) set ) ) V6() non zero total V18( COMPLEX : ( ( ) ( non zero V46() V57() V63() ) set ) , COMPLEX : ( ( ) ( non zero V46() V57() V63() ) set ) ) ) Function of COMPLEX : ( ( ) ( non zero V46() V57() V63() ) set ) , COMPLEX : ( ( ) ( non zero V46() V57() V63() ) set ) ) /. z1 : ( ( ) ( complex ) Element of COMPLEX : ( ( ) ( non zero V46() V57() V63() ) set ) ) ) : ( ( ) ( complex ) Element of COMPLEX : ( ( ) ( non zero V46() V57() V63() ) set ) ) * (sinh_C : ( ( V6() V18( COMPLEX : ( ( ) ( non zero V46() V57() V63() ) set ) , COMPLEX : ( ( ) ( non zero V46() V57() V63() ) set ) ) ) ( V1() V4( COMPLEX : ( ( ) ( non zero V46() V57() V63() ) set ) ) V5( COMPLEX : ( ( ) ( non zero V46() V57() V63() ) set ) ) V6() non zero total V18( COMPLEX : ( ( ) ( non zero V46() V57() V63() ) set ) , COMPLEX : ( ( ) ( non zero V46() V57() V63() ) set ) ) ) Function of COMPLEX : ( ( ) ( non zero V46() V57() V63() ) set ) , COMPLEX : ( ( ) ( non zero V46() V57() V63() ) set ) ) /. z2 : ( ( ) ( complex ) Element of COMPLEX : ( ( ) ( non zero V46() V57() V63() ) set ) ) ) : ( ( ) ( complex ) Element of COMPLEX : ( ( ) ( non zero V46() V57() V63() ) set ) ) ) : ( ( ) ( complex ) Element of COMPLEX : ( ( ) ( non zero V46() V57() V63() ) set ) ) : ( ( ) ( complex ) Element of COMPLEX : ( ( ) ( non zero V46() V57() V63() ) set ) ) ;

theorem :: SIN_COS3:12

for z1, z2 being ( ( ) ( complex ) Element of COMPLEX : ( ( ) ( non zero V46() V57() V63() ) set ) ) holds sinh_C : ( ( V6() V18( COMPLEX : ( ( ) ( non zero V46() V57() V63() ) set ) , COMPLEX : ( ( ) ( non zero V46() V57() V63() ) set ) ) ) ( V1() V4( COMPLEX : ( ( ) ( non zero V46() V57() V63() ) set ) ) V5( COMPLEX : ( ( ) ( non zero V46() V57() V63() ) set ) ) V6() non zero total V18( COMPLEX : ( ( ) ( non zero V46() V57() V63() ) set ) , COMPLEX : ( ( ) ( non zero V46() V57() V63() ) set ) ) ) Function of COMPLEX : ( ( ) ( non zero V46() V57() V63() ) set ) , COMPLEX : ( ( ) ( non zero V46() V57() V63() ) set ) ) /. (z1 : ( ( ) ( complex ) Element of COMPLEX : ( ( ) ( non zero V46() V57() V63() ) set ) ) - z2 : ( ( ) ( complex ) Element of COMPLEX : ( ( ) ( non zero V46() V57() V63() ) set ) ) ) : ( ( ) ( complex ) Element of COMPLEX : ( ( ) ( non zero V46() V57() V63() ) set ) ) : ( ( ) ( complex ) Element of COMPLEX : ( ( ) ( non zero V46() V57() V63() ) set ) ) = ((sinh_C : ( ( V6() V18( COMPLEX : ( ( ) ( non zero V46() V57() V63() ) set ) , COMPLEX : ( ( ) ( non zero V46() V57() V63() ) set ) ) ) ( V1() V4( COMPLEX : ( ( ) ( non zero V46() V57() V63() ) set ) ) V5( COMPLEX : ( ( ) ( non zero V46() V57() V63() ) set ) ) V6() non zero total V18( COMPLEX : ( ( ) ( non zero V46() V57() V63() ) set ) , COMPLEX : ( ( ) ( non zero V46() V57() V63() ) set ) ) ) Function of COMPLEX : ( ( ) ( non zero V46() V57() V63() ) set ) , COMPLEX : ( ( ) ( non zero V46() V57() V63() ) set ) ) /. z1 : ( ( ) ( complex ) Element of COMPLEX : ( ( ) ( non zero V46() V57() V63() ) set ) ) ) : ( ( ) ( complex ) Element of COMPLEX : ( ( ) ( non zero V46() V57() V63() ) set ) ) * (cosh_C : ( ( V6() V18( COMPLEX : ( ( ) ( non zero V46() V57() V63() ) set ) , COMPLEX : ( ( ) ( non zero V46() V57() V63() ) set ) ) ) ( V1() V4( COMPLEX : ( ( ) ( non zero V46() V57() V63() ) set ) ) V5( COMPLEX : ( ( ) ( non zero V46() V57() V63() ) set ) ) V6() non zero total V18( COMPLEX : ( ( ) ( non zero V46() V57() V63() ) set ) , COMPLEX : ( ( ) ( non zero V46() V57() V63() ) set ) ) ) Function of COMPLEX : ( ( ) ( non zero V46() V57() V63() ) set ) , COMPLEX : ( ( ) ( non zero V46() V57() V63() ) set ) ) /. z2 : ( ( ) ( complex ) Element of COMPLEX : ( ( ) ( non zero V46() V57() V63() ) set ) ) ) : ( ( ) ( complex ) Element of COMPLEX : ( ( ) ( non zero V46() V57() V63() ) set ) ) ) : ( ( ) ( complex ) Element of COMPLEX : ( ( ) ( non zero V46() V57() V63() ) set ) ) - ((cosh_C : ( ( V6() V18( COMPLEX : ( ( ) ( non zero V46() V57() V63() ) set ) , COMPLEX : ( ( ) ( non zero V46() V57() V63() ) set ) ) ) ( V1() V4( COMPLEX : ( ( ) ( non zero V46() V57() V63() ) set ) ) V5( COMPLEX : ( ( ) ( non zero V46() V57() V63() ) set ) ) V6() non zero total V18( COMPLEX : ( ( ) ( non zero V46() V57() V63() ) set ) , COMPLEX : ( ( ) ( non zero V46() V57() V63() ) set ) ) ) Function of COMPLEX : ( ( ) ( non zero V46() V57() V63() ) set ) , COMPLEX : ( ( ) ( non zero V46() V57() V63() ) set ) ) /. z1 : ( ( ) ( complex ) Element of COMPLEX : ( ( ) ( non zero V46() V57() V63() ) set ) ) ) : ( ( ) ( complex ) Element of COMPLEX : ( ( ) ( non zero V46() V57() V63() ) set ) ) * (sinh_C : ( ( V6() V18( COMPLEX : ( ( ) ( non zero V46() V57() V63() ) set ) , COMPLEX : ( ( ) ( non zero V46() V57() V63() ) set ) ) ) ( V1() V4( COMPLEX : ( ( ) ( non zero V46() V57() V63() ) set ) ) V5( COMPLEX : ( ( ) ( non zero V46() V57() V63() ) set ) ) V6() non zero total V18( COMPLEX : ( ( ) ( non zero V46() V57() V63() ) set ) , COMPLEX : ( ( ) ( non zero V46() V57() V63() ) set ) ) ) Function of COMPLEX : ( ( ) ( non zero V46() V57() V63() ) set ) , COMPLEX : ( ( ) ( non zero V46() V57() V63() ) set ) ) /. z2 : ( ( ) ( complex ) Element of COMPLEX : ( ( ) ( non zero V46() V57() V63() ) set ) ) ) : ( ( ) ( complex ) Element of COMPLEX : ( ( ) ( non zero V46() V57() V63() ) set ) ) ) : ( ( ) ( complex ) Element of COMPLEX : ( ( ) ( non zero V46() V57() V63() ) set ) ) : ( ( ) ( complex ) Element of COMPLEX : ( ( ) ( non zero V46() V57() V63() ) set ) ) ;

theorem :: SIN_COS3:13

for z1, z2 being ( ( ) ( complex ) Element of COMPLEX : ( ( ) ( non zero V46() V57() V63() ) set ) ) holds cosh_C : ( ( V6() V18( COMPLEX : ( ( ) ( non zero V46() V57() V63() ) set ) , COMPLEX : ( ( ) ( non zero V46() V57() V63() ) set ) ) ) ( V1() V4( COMPLEX : ( ( ) ( non zero V46() V57() V63() ) set ) ) V5( COMPLEX : ( ( ) ( non zero V46() V57() V63() ) set ) ) V6() non zero total V18( COMPLEX : ( ( ) ( non zero V46() V57() V63() ) set ) , COMPLEX : ( ( ) ( non zero V46() V57() V63() ) set ) ) ) Function of COMPLEX : ( ( ) ( non zero V46() V57() V63() ) set ) , COMPLEX : ( ( ) ( non zero V46() V57() V63() ) set ) ) /. (z1 : ( ( ) ( complex ) Element of COMPLEX : ( ( ) ( non zero V46() V57() V63() ) set ) ) - z2 : ( ( ) ( complex ) Element of COMPLEX : ( ( ) ( non zero V46() V57() V63() ) set ) ) ) : ( ( ) ( complex ) Element of COMPLEX : ( ( ) ( non zero V46() V57() V63() ) set ) ) : ( ( ) ( complex ) Element of COMPLEX : ( ( ) ( non zero V46() V57() V63() ) set ) ) = ((cosh_C : ( ( V6() V18( COMPLEX : ( ( ) ( non zero V46() V57() V63() ) set ) , COMPLEX : ( ( ) ( non zero V46() V57() V63() ) set ) ) ) ( V1() V4( COMPLEX : ( ( ) ( non zero V46() V57() V63() ) set ) ) V5( COMPLEX : ( ( ) ( non zero V46() V57() V63() ) set ) ) V6() non zero total V18( COMPLEX : ( ( ) ( non zero V46() V57() V63() ) set ) , COMPLEX : ( ( ) ( non zero V46() V57() V63() ) set ) ) ) Function of COMPLEX : ( ( ) ( non zero V46() V57() V63() ) set ) , COMPLEX : ( ( ) ( non zero V46() V57() V63() ) set ) ) /. z1 : ( ( ) ( complex ) Element of COMPLEX : ( ( ) ( non zero V46() V57() V63() ) set ) ) ) : ( ( ) ( complex ) Element of COMPLEX : ( ( ) ( non zero V46() V57() V63() ) set ) ) * (cosh_C : ( ( V6() V18( COMPLEX : ( ( ) ( non zero V46() V57() V63() ) set ) , COMPLEX : ( ( ) ( non zero V46() V57() V63() ) set ) ) ) ( V1() V4( COMPLEX : ( ( ) ( non zero V46() V57() V63() ) set ) ) V5( COMPLEX : ( ( ) ( non zero V46() V57() V63() ) set ) ) V6() non zero total V18( COMPLEX : ( ( ) ( non zero V46() V57() V63() ) set ) , COMPLEX : ( ( ) ( non zero V46() V57() V63() ) set ) ) ) Function of COMPLEX : ( ( ) ( non zero V46() V57() V63() ) set ) , COMPLEX : ( ( ) ( non zero V46() V57() V63() ) set ) ) /. z2 : ( ( ) ( complex ) Element of COMPLEX : ( ( ) ( non zero V46() V57() V63() ) set ) ) ) : ( ( ) ( complex ) Element of COMPLEX : ( ( ) ( non zero V46() V57() V63() ) set ) ) ) : ( ( ) ( complex ) Element of COMPLEX : ( ( ) ( non zero V46() V57() V63() ) set ) ) - ((sinh_C : ( ( V6() V18( COMPLEX : ( ( ) ( non zero V46() V57() V63() ) set ) , COMPLEX : ( ( ) ( non zero V46() V57() V63() ) set ) ) ) ( V1() V4( COMPLEX : ( ( ) ( non zero V46() V57() V63() ) set ) ) V5( COMPLEX : ( ( ) ( non zero V46() V57() V63() ) set ) ) V6() non zero total V18( COMPLEX : ( ( ) ( non zero V46() V57() V63() ) set ) , COMPLEX : ( ( ) ( non zero V46() V57() V63() ) set ) ) ) Function of COMPLEX : ( ( ) ( non zero V46() V57() V63() ) set ) , COMPLEX : ( ( ) ( non zero V46() V57() V63() ) set ) ) /. z1 : ( ( ) ( complex ) Element of COMPLEX : ( ( ) ( non zero V46() V57() V63() ) set ) ) ) : ( ( ) ( complex ) Element of COMPLEX : ( ( ) ( non zero V46() V57() V63() ) set ) ) * (sinh_C : ( ( V6() V18( COMPLEX : ( ( ) ( non zero V46() V57() V63() ) set ) , COMPLEX : ( ( ) ( non zero V46() V57() V63() ) set ) ) ) ( V1() V4( COMPLEX : ( ( ) ( non zero V46() V57() V63() ) set ) ) V5( COMPLEX : ( ( ) ( non zero V46() V57() V63() ) set ) ) V6() non zero total V18( COMPLEX : ( ( ) ( non zero V46() V57() V63() ) set ) , COMPLEX : ( ( ) ( non zero V46() V57() V63() ) set ) ) ) Function of COMPLEX : ( ( ) ( non zero V46() V57() V63() ) set ) , COMPLEX : ( ( ) ( non zero V46() V57() V63() ) set ) ) /. z2 : ( ( ) ( complex ) Element of COMPLEX : ( ( ) ( non zero V46() V57() V63() ) set ) ) ) : ( ( ) ( complex ) Element of COMPLEX : ( ( ) ( non zero V46() V57() V63() ) set ) ) ) : ( ( ) ( complex ) Element of COMPLEX : ( ( ) ( non zero V46() V57() V63() ) set ) ) : ( ( ) ( complex ) Element of COMPLEX : ( ( ) ( non zero V46() V57() V63() ) set ) ) ;

theorem :: SIN_COS3:14

for z1, z2 being ( ( ) ( complex ) Element of COMPLEX : ( ( ) ( non zero V46() V57() V63() ) set ) ) holds cosh_C : ( ( V6() V18( COMPLEX : ( ( ) ( non zero V46() V57() V63() ) set ) , COMPLEX : ( ( ) ( non zero V46() V57() V63() ) set ) ) ) ( V1() V4( COMPLEX : ( ( ) ( non zero V46() V57() V63() ) set ) ) V5( COMPLEX : ( ( ) ( non zero V46() V57() V63() ) set ) ) V6() non zero total V18( COMPLEX : ( ( ) ( non zero V46() V57() V63() ) set ) , COMPLEX : ( ( ) ( non zero V46() V57() V63() ) set ) ) ) Function of COMPLEX : ( ( ) ( non zero V46() V57() V63() ) set ) , COMPLEX : ( ( ) ( non zero V46() V57() V63() ) set ) ) /. (z1 : ( ( ) ( complex ) Element of COMPLEX : ( ( ) ( non zero V46() V57() V63() ) set ) ) + z2 : ( ( ) ( complex ) Element of COMPLEX : ( ( ) ( non zero V46() V57() V63() ) set ) ) ) : ( ( ) ( complex ) Element of COMPLEX : ( ( ) ( non zero V46() V57() V63() ) set ) ) : ( ( ) ( complex ) Element of COMPLEX : ( ( ) ( non zero V46() V57() V63() ) set ) ) = ((cosh_C : ( ( V6() V18( COMPLEX : ( ( ) ( non zero V46() V57() V63() ) set ) , COMPLEX : ( ( ) ( non zero V46() V57() V63() ) set ) ) ) ( V1() V4( COMPLEX : ( ( ) ( non zero V46() V57() V63() ) set ) ) V5( COMPLEX : ( ( ) ( non zero V46() V57() V63() ) set ) ) V6() non zero total V18( COMPLEX : ( ( ) ( non zero V46() V57() V63() ) set ) , COMPLEX : ( ( ) ( non zero V46() V57() V63() ) set ) ) ) Function of COMPLEX : ( ( ) ( non zero V46() V57() V63() ) set ) , COMPLEX : ( ( ) ( non zero V46() V57() V63() ) set ) ) /. z1 : ( ( ) ( complex ) Element of COMPLEX : ( ( ) ( non zero V46() V57() V63() ) set ) ) ) : ( ( ) ( complex ) Element of COMPLEX : ( ( ) ( non zero V46() V57() V63() ) set ) ) * (cosh_C : ( ( V6() V18( COMPLEX : ( ( ) ( non zero V46() V57() V63() ) set ) , COMPLEX : ( ( ) ( non zero V46() V57() V63() ) set ) ) ) ( V1() V4( COMPLEX : ( ( ) ( non zero V46() V57() V63() ) set ) ) V5( COMPLEX : ( ( ) ( non zero V46() V57() V63() ) set ) ) V6() non zero total V18( COMPLEX : ( ( ) ( non zero V46() V57() V63() ) set ) , COMPLEX : ( ( ) ( non zero V46() V57() V63() ) set ) ) ) Function of COMPLEX : ( ( ) ( non zero V46() V57() V63() ) set ) , COMPLEX : ( ( ) ( non zero V46() V57() V63() ) set ) ) /. z2 : ( ( ) ( complex ) Element of COMPLEX : ( ( ) ( non zero V46() V57() V63() ) set ) ) ) : ( ( ) ( complex ) Element of COMPLEX : ( ( ) ( non zero V46() V57() V63() ) set ) ) ) : ( ( ) ( complex ) Element of COMPLEX : ( ( ) ( non zero V46() V57() V63() ) set ) ) + ((sinh_C : ( ( V6() V18( COMPLEX : ( ( ) ( non zero V46() V57() V63() ) set ) , COMPLEX : ( ( ) ( non zero V46() V57() V63() ) set ) ) ) ( V1() V4( COMPLEX : ( ( ) ( non zero V46() V57() V63() ) set ) ) V5( COMPLEX : ( ( ) ( non zero V46() V57() V63() ) set ) ) V6() non zero total V18( COMPLEX : ( ( ) ( non zero V46() V57() V63() ) set ) , COMPLEX : ( ( ) ( non zero V46() V57() V63() ) set ) ) ) Function of COMPLEX : ( ( ) ( non zero V46() V57() V63() ) set ) , COMPLEX : ( ( ) ( non zero V46() V57() V63() ) set ) ) /. z1 : ( ( ) ( complex ) Element of COMPLEX : ( ( ) ( non zero V46() V57() V63() ) set ) ) ) : ( ( ) ( complex ) Element of COMPLEX : ( ( ) ( non zero V46() V57() V63() ) set ) ) * (sinh_C : ( ( V6() V18( COMPLEX : ( ( ) ( non zero V46() V57() V63() ) set ) , COMPLEX : ( ( ) ( non zero V46() V57() V63() ) set ) ) ) ( V1() V4( COMPLEX : ( ( ) ( non zero V46() V57() V63() ) set ) ) V5( COMPLEX : ( ( ) ( non zero V46() V57() V63() ) set ) ) V6() non zero total V18( COMPLEX : ( ( ) ( non zero V46() V57() V63() ) set ) , COMPLEX : ( ( ) ( non zero V46() V57() V63() ) set ) ) ) Function of COMPLEX : ( ( ) ( non zero V46() V57() V63() ) set ) , COMPLEX : ( ( ) ( non zero V46() V57() V63() ) set ) ) /. z2 : ( ( ) ( complex ) Element of COMPLEX : ( ( ) ( non zero V46() V57() V63() ) set ) ) ) : ( ( ) ( complex ) Element of COMPLEX : ( ( ) ( non zero V46() V57() V63() ) set ) ) ) : ( ( ) ( complex ) Element of COMPLEX : ( ( ) ( non zero V46() V57() V63() ) set ) ) : ( ( ) ( complex ) Element of COMPLEX : ( ( ) ( non zero V46() V57() V63() ) set ) ) ;

theorem :: SIN_COS3:15

for z being ( ( complex ) ( complex ) number ) holds sin_C : ( ( V6() V18( COMPLEX : ( ( ) ( non zero V46() V57() V63() ) set ) , COMPLEX : ( ( ) ( non zero V46() V57() V63() ) set ) ) ) ( V1() V4( COMPLEX : ( ( ) ( non zero V46() V57() V63() ) set ) ) V5( COMPLEX : ( ( ) ( non zero V46() V57() V63() ) set ) ) V6() non zero total V18( COMPLEX : ( ( ) ( non zero V46() V57() V63() ) set ) , COMPLEX : ( ( ) ( non zero V46() V57() V63() ) set ) ) ) Function of COMPLEX : ( ( ) ( non zero V46() V57() V63() ) set ) , COMPLEX : ( ( ) ( non zero V46() V57() V63() ) set ) ) /. ( : ( ( ) ( complex ) Element of COMPLEX : ( ( ) ( non zero V46() V57() V63() ) set ) ) * z : ( ( complex ) ( complex ) number ) ) : ( ( ) ( complex ) Element of COMPLEX : ( ( ) ( non zero V46() V57() V63() ) set ) ) : ( ( ) ( complex ) Element of COMPLEX : ( ( ) ( non zero V46() V57() V63() ) set ) ) = : ( ( ) ( complex ) Element of COMPLEX : ( ( ) ( non zero V46() V57() V63() ) set ) ) * (sinh_C : ( ( V6() V18( COMPLEX : ( ( ) ( non zero V46() V57() V63() ) set ) , COMPLEX : ( ( ) ( non zero V46() V57() V63() ) set ) ) ) ( V1() V4( COMPLEX : ( ( ) ( non zero V46() V57() V63() ) set ) ) V5( COMPLEX : ( ( ) ( non zero V46() V57() V63() ) set ) ) V6() non zero total V18( COMPLEX : ( ( ) ( non zero V46() V57() V63() ) set ) , COMPLEX : ( ( ) ( non zero V46() V57() V63() ) set ) ) ) Function of COMPLEX : ( ( ) ( non zero V46() V57() V63() ) set ) , COMPLEX : ( ( ) ( non zero V46() V57() V63() ) set ) ) /. z : ( ( complex ) ( complex ) number ) ) : ( ( ) ( complex ) Element of COMPLEX : ( ( ) ( non zero V46() V57() V63() ) set ) ) : ( ( ) ( complex ) Element of COMPLEX : ( ( ) ( non zero V46() V57() V63() ) set ) ) ;

theorem :: SIN_COS3:16

for z being ( ( complex ) ( complex ) number ) holds cos_C : ( ( V6() V18( COMPLEX : ( ( ) ( non zero V46() V57() V63() ) set ) , COMPLEX : ( ( ) ( non zero V46() V57() V63() ) set ) ) ) ( V1() V4( COMPLEX : ( ( ) ( non zero V46() V57() V63() ) set ) ) V5( COMPLEX : ( ( ) ( non zero V46() V57() V63() ) set ) ) V6() non zero total V18( COMPLEX : ( ( ) ( non zero V46() V57() V63() ) set ) , COMPLEX : ( ( ) ( non zero V46() V57() V63() ) set ) ) ) Function of COMPLEX : ( ( ) ( non zero V46() V57() V63() ) set ) , COMPLEX : ( ( ) ( non zero V46() V57() V63() ) set ) ) /. ( : ( ( ) ( complex ) Element of COMPLEX : ( ( ) ( non zero V46() V57() V63() ) set ) ) * z : ( ( complex ) ( complex ) number ) ) : ( ( ) ( complex ) Element of COMPLEX : ( ( ) ( non zero V46() V57() V63() ) set ) ) : ( ( ) ( complex ) Element of COMPLEX : ( ( ) ( non zero V46() V57() V63() ) set ) ) = cosh_C : ( ( V6() V18( COMPLEX : ( ( ) ( non zero V46() V57() V63() ) set ) , COMPLEX : ( ( ) ( non zero V46() V57() V63() ) set ) ) ) ( V1() V4( COMPLEX : ( ( ) ( non zero V46() V57() V63() ) set ) ) V5( COMPLEX : ( ( ) ( non zero V46() V57() V63() ) set ) ) V6() non zero total V18( COMPLEX : ( ( ) ( non zero V46() V57() V63() ) set ) , COMPLEX : ( ( ) ( non zero V46() V57() V63() ) set ) ) ) Function of COMPLEX : ( ( ) ( non zero V46() V57() V63() ) set ) , COMPLEX : ( ( ) ( non zero V46() V57() V63() ) set ) ) /. z : ( ( complex ) ( complex ) number ) : ( ( ) ( complex ) Element of COMPLEX : ( ( ) ( non zero V46() V57() V63() ) set ) ) ;

theorem :: SIN_COS3:17

for z being ( ( complex ) ( complex ) number ) holds sinh_C : ( ( V6() V18( COMPLEX : ( ( ) ( non zero V46() V57() V63() ) set ) , COMPLEX : ( ( ) ( non zero V46() V57() V63() ) set ) ) ) ( V1() V4( COMPLEX : ( ( ) ( non zero V46() V57() V63() ) set ) ) V5( COMPLEX : ( ( ) ( non zero V46() V57() V63() ) set ) ) V6() non zero total V18( COMPLEX : ( ( ) ( non zero V46() V57() V63() ) set ) , COMPLEX : ( ( ) ( non zero V46() V57() V63() ) set ) ) ) Function of COMPLEX : ( ( ) ( non zero V46() V57() V63() ) set ) , COMPLEX : ( ( ) ( non zero V46() V57() V63() ) set ) ) /. ( : ( ( ) ( complex ) Element of COMPLEX : ( ( ) ( non zero V46() V57() V63() ) set ) ) * z : ( ( complex ) ( complex ) number ) ) : ( ( ) ( complex ) Element of COMPLEX : ( ( ) ( non zero V46() V57() V63() ) set ) ) : ( ( ) ( complex ) Element of COMPLEX : ( ( ) ( non zero V46() V57() V63() ) set ) ) = : ( ( ) ( complex ) Element of COMPLEX : ( ( ) ( non zero V46() V57() V63() ) set ) ) * (sin_C : ( ( V6() V18( COMPLEX : ( ( ) ( non zero V46() V57() V63() ) set ) , COMPLEX : ( ( ) ( non zero V46() V57() V63() ) set ) ) ) ( V1() V4( COMPLEX : ( ( ) ( non zero V46() V57() V63() ) set ) ) V5( COMPLEX : ( ( ) ( non zero V46() V57() V63() ) set ) ) V6() non zero total V18( COMPLEX : ( ( ) ( non zero V46() V57() V63() ) set ) , COMPLEX : ( ( ) ( non zero V46() V57() V63() ) set ) ) ) Function of COMPLEX : ( ( ) ( non zero V46() V57() V63() ) set ) , COMPLEX : ( ( ) ( non zero V46() V57() V63() ) set ) ) /. z : ( ( complex ) ( complex ) number ) ) : ( ( ) ( complex ) Element of COMPLEX : ( ( ) ( non zero V46() V57() V63() ) set ) ) : ( ( ) ( complex ) Element of COMPLEX : ( ( ) ( non zero V46() V57() V63() ) set ) ) ;

theorem :: SIN_COS3:18

for z being ( ( complex ) ( complex ) number ) holds cosh_C : ( ( V6() V18( COMPLEX : ( ( ) ( non zero V46() V57() V63() ) set ) , COMPLEX : ( ( ) ( non zero V46() V57() V63() ) set ) ) ) ( V1() V4( COMPLEX : ( ( ) ( non zero V46() V57() V63() ) set ) ) V5( COMPLEX : ( ( ) ( non zero V46() V57() V63() ) set ) ) V6() non zero total V18( COMPLEX : ( ( ) ( non zero V46() V57() V63() ) set ) , COMPLEX : ( ( ) ( non zero V46() V57() V63() ) set ) ) ) Function of COMPLEX : ( ( ) ( non zero V46() V57() V63() ) set ) , COMPLEX : ( ( ) ( non zero V46() V57() V63() ) set ) ) /. ( : ( ( ) ( complex ) Element of COMPLEX : ( ( ) ( non zero V46() V57() V63() ) set ) ) * z : ( ( complex ) ( complex ) number ) ) : ( ( ) ( complex ) Element of COMPLEX : ( ( ) ( non zero V46() V57() V63() ) set ) ) : ( ( ) ( complex ) Element of COMPLEX : ( ( ) ( non zero V46() V57() V63() ) set ) ) = cos_C : ( ( V6() V18( COMPLEX : ( ( ) ( non zero V46() V57() V63() ) set ) , COMPLEX : ( ( ) ( non zero V46() V57() V63() ) set ) ) ) ( V1() V4( COMPLEX : ( ( ) ( non zero V46() V57() V63() ) set ) ) V5( COMPLEX : ( ( ) ( non zero V46() V57() V63() ) set ) ) V6() non zero total V18( COMPLEX : ( ( ) ( non zero V46() V57() V63() ) set ) , COMPLEX : ( ( ) ( non zero V46() V57() V63() ) set ) ) ) Function of COMPLEX : ( ( ) ( non zero V46() V57() V63() ) set ) , COMPLEX : ( ( ) ( non zero V46() V57() V63() ) set ) ) /. z : ( ( complex ) ( complex ) number ) : ( ( ) ( complex ) Element of COMPLEX : ( ( ) ( non zero V46() V57() V63() ) set ) ) ;

theorem :: SIN_COS3:19

for x, y being ( ( ) ( complex V29() V30() ) Element of REAL : ( ( ) ( non zero V46() V57() V58() V59() V63() ) set ) ) holds exp (x : ( ( ) ( complex V29() V30() ) Element of REAL : ( ( ) ( non zero V46() V57() V58() V59() V63() ) set ) ) + (y : ( ( ) ( complex V29() V30() ) Element of REAL : ( ( ) ( non zero V46() V57() V58() V59() V63() ) set ) ) * : ( ( ) ( complex ) Element of COMPLEX : ( ( ) ( non zero V46() V57() V63() ) set ) ) ) : ( ( ) ( complex ) Element of COMPLEX : ( ( ) ( non zero V46() V57() V63() ) set ) ) ) : ( ( ) ( complex ) Element of COMPLEX : ( ( ) ( non zero V46() V57() V63() ) set ) ) : ( ( ) ( complex ) Element of COMPLEX : ( ( ) ( non zero V46() V57() V63() ) set ) ) = ((exp_R : ( ( V6() V18( REAL : ( ( ) ( non zero V46() V57() V58() V59() V63() ) set ) , REAL : ( ( ) ( non zero V46() V57() V58() V59() V63() ) set ) ) ) ( V1() V4( REAL : ( ( ) ( non zero V46() V57() V58() V59() V63() ) set ) ) V5( REAL : ( ( ) ( non zero V46() V57() V58() V59() V63() ) set ) ) V6() non zero total V18( REAL : ( ( ) ( non zero V46() V57() V58() V59() V63() ) set ) , REAL : ( ( ) ( non zero V46() V57() V58() V59() V63() ) set ) ) ) Element of K19(K20(REAL : ( ( ) ( non zero V46() V57() V58() V59() V63() ) set ) ,REAL : ( ( ) ( non zero V46() V57() V58() V59() V63() ) set ) ) : ( ( ) ( ) set ) ) : ( ( ) ( ) set ) ) . x : ( ( ) ( complex V29() V30() ) Element of REAL : ( ( ) ( non zero V46() V57() V58() V59() V63() ) set ) ) ) : ( ( ) ( complex V29() V30() ) Element of REAL : ( ( ) ( non zero V46() V57() V58() V59() V63() ) set ) ) * (cos : ( ( V6() V18( REAL : ( ( ) ( non zero V46() V57() V58() V59() V63() ) set ) , REAL : ( ( ) ( non zero V46() V57() V58() V59() V63() ) set ) ) ) ( V1() V4( REAL : ( ( ) ( non zero V46() V57() V58() V59() V63() ) set ) ) V5( REAL : ( ( ) ( non zero V46() V57() V58() V59() V63() ) set ) ) V6() non zero total V18( REAL : ( ( ) ( non zero V46() V57() V58() V59() V63() ) set ) , REAL : ( ( ) ( non zero V46() V57() V58() V59() V63() ) set ) ) ) Element of K19(K20(REAL : ( ( ) ( non zero V46() V57() V58() V59() V63() ) set ) ,REAL : ( ( ) ( non zero V46() V57() V58() V59() V63() ) set ) ) : ( ( ) ( ) set ) ) : ( ( ) ( ) set ) ) . y : ( ( ) ( complex V29() V30() ) Element of REAL : ( ( ) ( non zero V46() V57() V58() V59() V63() ) set ) ) ) : ( ( ) ( complex V29() V30() ) Element of REAL : ( ( ) ( non zero V46() V57() V58() V59() V63() ) set ) ) ) : ( ( ) ( complex V29() V30() ) Element of REAL : ( ( ) ( non zero V46() V57() V58() V59() V63() ) set ) ) + (((exp_R : ( ( V6() V18( REAL : ( ( ) ( non zero V46() V57() V58() V59() V63() ) set ) , REAL : ( ( ) ( non zero V46() V57() V58() V59() V63() ) set ) ) ) ( V1() V4( REAL : ( ( ) ( non zero V46() V57() V58() V59() V63() ) set ) ) V5( REAL : ( ( ) ( non zero V46() V57() V58() V59() V63() ) set ) ) V6() non zero total V18( REAL : ( ( ) ( non zero V46() V57() V58() V59() V63() ) set ) , REAL : ( ( ) ( non zero V46() V57() V58() V59() V63() ) set ) ) ) Element of K19(K20(REAL : ( ( ) ( non zero V46() V57() V58() V59() V63() ) set ) ,REAL : ( ( ) ( non zero V46() V57() V58() V59() V63() ) set ) ) : ( ( ) ( ) set ) ) : ( ( ) ( ) set ) ) . x : ( ( ) ( complex V29() V30() ) Element of REAL : ( ( ) ( non zero V46() V57() V58() V59() V63() ) set ) ) ) : ( ( ) ( complex V29() V30() ) Element of REAL : ( ( ) ( non zero V46() V57() V58() V59() V63() ) set ) ) * (sin : ( ( V6() V18( REAL : ( ( ) ( non zero V46() V57() V58() V59() V63() ) set ) , REAL : ( ( ) ( non zero V46() V57() V58() V59() V63() ) set ) ) ) ( V1() V4( REAL : ( ( ) ( non zero V46() V57() V58() V59() V63() ) set ) ) V5( REAL : ( ( ) ( non zero V46() V57() V58() V59() V63() ) set ) ) V6() non zero total V18( REAL : ( ( ) ( non zero V46() V57() V58() V59() V63() ) set ) , REAL : ( ( ) ( non zero V46() V57() V58() V59() V63() ) set ) ) ) Element of K19(K20(REAL : ( ( ) ( non zero V46() V57() V58() V59() V63() ) set ) ,REAL : ( ( ) ( non zero V46() V57() V58() V59() V63() ) set ) ) : ( ( ) ( ) set ) ) : ( ( ) ( ) set ) ) . y : ( ( ) ( complex V29() V30() ) Element of REAL : ( ( ) ( non zero V46() V57() V58() V59() V63() ) set ) ) ) : ( ( ) ( complex V29() V30() ) Element of REAL : ( ( ) ( non zero V46() V57() V58() V59() V63() ) set ) ) ) : ( ( ) ( complex V29() V30() ) Element of REAL : ( ( ) ( non zero V46() V57() V58() V59() V63() ) set ) ) * : ( ( ) ( complex ) Element of COMPLEX : ( ( ) ( non zero V46() V57() V63() ) set ) ) ) : ( ( ) ( complex ) Element of COMPLEX : ( ( ) ( non zero V46() V57() V63() ) set ) ) : ( ( ) ( complex ) Element of COMPLEX : ( ( ) ( non zero V46() V57() V63() ) set ) ) ;

theorem :: SIN_COS3:20

exp 0c : ( ( ) ( complex ) Element of COMPLEX : ( ( ) ( non zero V46() V57() V63() ) set ) ) : ( ( ) ( complex ) Element of COMPLEX : ( ( ) ( non zero V46() V57() V63() ) set ) ) = 1 : ( ( ) ( non zero natural complex V29() V30() V33() V34() V57() V58() V59() V60() V61() V62() ) Element of NAT : ( ( ) ( V57() V58() V59() V60() V61() V62() V63() ) Element of K19(REAL : ( ( ) ( non zero V46() V57() V58() V59() V63() ) set ) ) : ( ( ) ( ) set ) ) ) ;

theorem :: SIN_COS3:21

sin_C : ( ( V6() V18( COMPLEX : ( ( ) ( non zero V46() V57() V63() ) set ) , COMPLEX : ( ( ) ( non zero V46() V57() V63() ) set ) ) ) ( V1() V4( COMPLEX : ( ( ) ( non zero V46() V57() V63() ) set ) ) V5( COMPLEX : ( ( ) ( non zero V46() V57() V63() ) set ) ) V6() non zero total V18( COMPLEX : ( ( ) ( non zero V46() V57() V63() ) set ) , COMPLEX : ( ( ) ( non zero V46() V57() V63() ) set ) ) ) Function of COMPLEX : ( ( ) ( non zero V46() V57() V63() ) set ) , COMPLEX : ( ( ) ( non zero V46() V57() V63() ) set ) ) /. 0c : ( ( ) ( complex ) Element of COMPLEX : ( ( ) ( non zero V46() V57() V63() ) set ) ) : ( ( ) ( complex ) Element of COMPLEX : ( ( ) ( non zero V46() V57() V63() ) set ) ) = 0 : ( ( ) ( natural complex V29() V30() V33() V34() V57() V58() V59() V60() V61() V62() ) Element of NAT : ( ( ) ( V57() V58() V59() V60() V61() V62() V63() ) Element of K19(REAL : ( ( ) ( non zero V46() V57() V58() V59() V63() ) set ) ) : ( ( ) ( ) set ) ) ) ;

theorem :: SIN_COS3:22

sinh_C : ( ( V6() V18( COMPLEX : ( ( ) ( non zero V46() V57() V63() ) set ) , COMPLEX : ( ( ) ( non zero V46() V57() V63() ) set ) ) ) ( V1() V4( COMPLEX : ( ( ) ( non zero V46() V57() V63() ) set ) ) V5( COMPLEX : ( ( ) ( non zero V46() V57() V63() ) set ) ) V6() non zero total V18( COMPLEX : ( ( ) ( non zero V46() V57() V63() ) set ) , COMPLEX : ( ( ) ( non zero V46() V57() V63() ) set ) ) ) Function of COMPLEX : ( ( ) ( non zero V46() V57() V63() ) set ) , COMPLEX : ( ( ) ( non zero V46() V57() V63() ) set ) ) /. 0c : ( ( ) ( complex ) Element of COMPLEX : ( ( ) ( non zero V46() V57() V63() ) set ) ) : ( ( ) ( complex ) Element of COMPLEX : ( ( ) ( non zero V46() V57() V63() ) set ) ) = 0 : ( ( ) ( natural complex V29() V30() V33() V34() V57() V58() V59() V60() V61() V62() ) Element of NAT : ( ( ) ( V57() V58() V59() V60() V61() V62() V63() ) Element of K19(REAL : ( ( ) ( non zero V46() V57() V58() V59() V63() ) set ) ) : ( ( ) ( ) set ) ) ) ;

theorem :: SIN_COS3:23

cos_C : ( ( V6() V18( COMPLEX : ( ( ) ( non zero V46() V57() V63() ) set ) , COMPLEX : ( ( ) ( non zero V46() V57() V63() ) set ) ) ) ( V1() V4( COMPLEX : ( ( ) ( non zero V46() V57() V63() ) set ) ) V5( COMPLEX : ( ( ) ( non zero V46() V57() V63() ) set ) ) V6() non zero total V18( COMPLEX : ( ( ) ( non zero V46() V57() V63() ) set ) , COMPLEX : ( ( ) ( non zero V46() V57() V63() ) set ) ) ) Function of COMPLEX : ( ( ) ( non zero V46() V57() V63() ) set ) , COMPLEX : ( ( ) ( non zero V46() V57() V63() ) set ) ) /. 0c : ( ( ) ( complex ) Element of COMPLEX : ( ( ) ( non zero V46() V57() V63() ) set ) ) : ( ( ) ( complex ) Element of COMPLEX : ( ( ) ( non zero V46() V57() V63() ) set ) ) = 1 : ( ( ) ( non zero natural complex V29() V30() V33() V34() V57() V58() V59() V60() V61() V62() ) Element of NAT : ( ( ) ( V57() V58() V59() V60() V61() V62() V63() ) Element of K19(REAL : ( ( ) ( non zero V46() V57() V58() V59() V63() ) set ) ) : ( ( ) ( ) set ) ) ) ;

theorem :: SIN_COS3:24

cosh_C : ( ( V6() V18( COMPLEX : ( ( ) ( non zero V46() V57() V63() ) set ) , COMPLEX : ( ( ) ( non zero V46() V57() V63() ) set ) ) ) ( V1() V4( COMPLEX : ( ( ) ( non zero V46() V57() V63() ) set ) ) V5( COMPLEX : ( ( ) ( non zero V46() V57() V63() ) set ) ) V6() non zero total V18( COMPLEX : ( ( ) ( non zero V46() V57() V63() ) set ) , COMPLEX : ( ( ) ( non zero V46() V57() V63() ) set ) ) ) Function of COMPLEX : ( ( ) ( non zero V46() V57() V63() ) set ) , COMPLEX : ( ( ) ( non zero V46() V57() V63() ) set ) ) /. 0c : ( ( ) ( complex ) Element of COMPLEX : ( ( ) ( non zero V46() V57() V63() ) set ) ) : ( ( ) ( complex ) Element of COMPLEX : ( ( ) ( non zero V46() V57() V63() ) set ) ) = 1 : ( ( ) ( non zero natural complex V29() V30() V33() V34() V57() V58() V59() V60() V61() V62() ) Element of NAT : ( ( ) ( V57() V58() V59() V60() V61() V62() V63() ) Element of K19(REAL : ( ( ) ( non zero V46() V57() V58() V59() V63() ) set ) ) : ( ( ) ( ) set ) ) ) ;

theorem :: SIN_COS3:25

for z being ( ( ) ( complex ) Element of COMPLEX : ( ( ) ( non zero V46() V57() V63() ) set ) ) holds exp z : ( ( ) ( complex ) Element of COMPLEX : ( ( ) ( non zero V46() V57() V63() ) set ) ) : ( ( ) ( complex ) Element of COMPLEX : ( ( ) ( non zero V46() V57() V63() ) set ) ) = (cosh_C : ( ( V6() V18( COMPLEX : ( ( ) ( non zero V46() V57() V63() ) set ) , COMPLEX : ( ( ) ( non zero V46() V57() V63() ) set ) ) ) ( V1() V4( COMPLEX : ( ( ) ( non zero V46() V57() V63() ) set ) ) V5( COMPLEX : ( ( ) ( non zero V46() V57() V63() ) set ) ) V6() non zero total V18( COMPLEX : ( ( ) ( non zero V46() V57() V63() ) set ) , COMPLEX : ( ( ) ( non zero V46() V57() V63() ) set ) ) ) Function of COMPLEX : ( ( ) ( non zero V46() V57() V63() ) set ) , COMPLEX : ( ( ) ( non zero V46() V57() V63() ) set ) ) /. z : ( ( ) ( complex ) Element of COMPLEX : ( ( ) ( non zero V46() V57() V63() ) set ) ) ) : ( ( ) ( complex ) Element of COMPLEX : ( ( ) ( non zero V46() V57() V63() ) set ) ) + (sinh_C : ( ( V6() V18( COMPLEX : ( ( ) ( non zero V46() V57() V63() ) set ) , COMPLEX : ( ( ) ( non zero V46() V57() V63() ) set ) ) ) ( V1() V4( COMPLEX : ( ( ) ( non zero V46() V57() V63() ) set ) ) V5( COMPLEX : ( ( ) ( non zero V46() V57() V63() ) set ) ) V6() non zero total V18( COMPLEX : ( ( ) ( non zero V46() V57() V63() ) set ) , COMPLEX : ( ( ) ( non zero V46() V57() V63() ) set ) ) ) Function of COMPLEX : ( ( ) ( non zero V46() V57() V63() ) set ) , COMPLEX : ( ( ) ( non zero V46() V57() V63() ) set ) ) /. z : ( ( ) ( complex ) Element of COMPLEX : ( ( ) ( non zero V46() V57() V63() ) set ) ) ) : ( ( ) ( complex ) Element of COMPLEX : ( ( ) ( non zero V46() V57() V63() ) set ) ) : ( ( ) ( complex ) Element of COMPLEX : ( ( ) ( non zero V46() V57() V63() ) set ) ) ;

theorem :: SIN_COS3:26

for z being ( ( ) ( complex ) Element of COMPLEX : ( ( ) ( non zero V46() V57() V63() ) set ) ) holds exp (- z : ( ( ) ( complex ) Element of COMPLEX : ( ( ) ( non zero V46() V57() V63() ) set ) ) ) : ( ( ) ( complex ) Element of COMPLEX : ( ( ) ( non zero V46() V57() V63() ) set ) ) : ( ( ) ( complex ) Element of COMPLEX : ( ( ) ( non zero V46() V57() V63() ) set ) ) = (cosh_C : ( ( V6() V18( COMPLEX : ( ( ) ( non zero V46() V57() V63() ) set ) , COMPLEX : ( ( ) ( non zero V46() V57() V63() ) set ) ) ) ( V1() V4( COMPLEX : ( ( ) ( non zero V46() V57() V63() ) set ) ) V5( COMPLEX : ( ( ) ( non zero V46() V57() V63() ) set ) ) V6() non zero total V18( COMPLEX : ( ( ) ( non zero V46() V57() V63() ) set ) , COMPLEX : ( ( ) ( non zero V46() V57() V63() ) set ) ) ) Function of COMPLEX : ( ( ) ( non zero V46() V57() V63() ) set ) , COMPLEX : ( ( ) ( non zero V46() V57() V63() ) set ) ) /. z : ( ( ) ( complex ) Element of COMPLEX : ( ( ) ( non zero V46() V57() V63() ) set ) ) ) : ( ( ) ( complex ) Element of COMPLEX : ( ( ) ( non zero V46() V57() V63() ) set ) ) - (sinh_C : ( ( V6() V18( COMPLEX : ( ( ) ( non zero V46() V57() V63() ) set ) , COMPLEX : ( ( ) ( non zero V46() V57() V63() ) set ) ) ) ( V1() V4( COMPLEX : ( ( ) ( non zero V46() V57() V63() ) set ) ) V5( COMPLEX : ( ( ) ( non zero V46() V57() V63() ) set ) ) V6() non zero total V18( COMPLEX : ( ( ) ( non zero V46() V57() V63() ) set ) , COMPLEX : ( ( ) ( non zero V46() V57() V63() ) set ) ) ) Function of COMPLEX : ( ( ) ( non zero V46() V57() V63() ) set ) , COMPLEX : ( ( ) ( non zero V46() V57() V63() ) set ) ) /. z : ( ( ) ( complex ) Element of COMPLEX : ( ( ) ( non zero V46() V57() V63() ) set ) ) ) : ( ( ) ( complex ) Element of COMPLEX : ( ( ) ( non zero V46() V57() V63() ) set ) ) : ( ( ) ( complex ) Element of COMPLEX : ( ( ) ( non zero V46() V57() V63() ) set ) ) ;

theorem :: SIN_COS3:27

for z being ( ( ) ( complex ) Element of COMPLEX : ( ( ) ( non zero V46() V57() V63() ) set ) ) holds exp (z : ( ( ) ( complex ) Element of COMPLEX : ( ( ) ( non zero V46() V57() V63() ) set ) ) + ((2 : ( ( ) ( non zero natural complex V29() V30() V33() V34() V57() V58() V59() V60() V61() V62() ) Element of NAT : ( ( ) ( V57() V58() V59() V60() V61() V62() V63() ) Element of K19(REAL : ( ( ) ( non zero V46() V57() V58() V59() V63() ) set ) ) : ( ( ) ( ) set ) ) ) * PI : ( ( ) ( complex V29() V30() ) Element of REAL : ( ( ) ( non zero V46() V57() V58() V59() V63() ) set ) ) ) : ( ( ) ( complex V29() V30() ) Element of REAL : ( ( ) ( non zero V46() V57() V58() V59() V63() ) set ) ) * : ( ( ) ( complex ) Element of COMPLEX : ( ( ) ( non zero V46() V57() V63() ) set ) ) ) : ( ( ) ( complex ) Element of COMPLEX : ( ( ) ( non zero V46() V57() V63() ) set ) ) ) : ( ( ) ( complex ) Element of COMPLEX : ( ( ) ( non zero V46() V57() V63() ) set ) ) : ( ( ) ( complex ) Element of COMPLEX : ( ( ) ( non zero V46() V57() V63() ) set ) ) = exp z : ( ( ) ( complex ) Element of COMPLEX : ( ( ) ( non zero V46() V57() V63() ) set ) ) : ( ( ) ( complex ) Element of COMPLEX : ( ( ) ( non zero V46() V57() V63() ) set ) ) ;

theorem :: SIN_COS3:28

for n being ( ( ) ( natural complex V29() V30() V33() V34() V57() V58() V59() V60() V61() V62() ) Element of NAT : ( ( ) ( V57() V58() V59() V60() V61() V62() V63() ) Element of K19(REAL : ( ( ) ( non zero V46() V57() V58() V59() V63() ) set ) ) : ( ( ) ( ) set ) ) ) holds exp (((2 : ( ( ) ( non zero natural complex V29() V30() V33() V34() V57() V58() V59() V60() V61() V62() ) Element of NAT : ( ( ) ( V57() V58() V59() V60() V61() V62() V63() ) Element of K19(REAL : ( ( ) ( non zero V46() V57() V58() V59() V63() ) set ) ) : ( ( ) ( ) set ) ) ) * PI : ( ( ) ( complex V29() V30() ) Element of REAL : ( ( ) ( non zero V46() V57() V58() V59() V63() ) set ) ) ) : ( ( ) ( complex V29() V30() ) Element of REAL : ( ( ) ( non zero V46() V57() V58() V59() V63() ) set ) ) * n : ( ( ) ( natural complex V29() V30() V33() V34() V57() V58() V59() V60() V61() V62() ) Element of NAT : ( ( ) ( V57() V58() V59() V60() V61() V62() V63() ) Element of K19(REAL : ( ( ) ( non zero V46() V57() V58() V59() V63() ) set ) ) : ( ( ) ( ) set ) ) ) ) : ( ( ) ( complex V29() V30() ) Element of REAL : ( ( ) ( non zero V46() V57() V58() V59() V63() ) set ) ) * : ( ( ) ( complex ) Element of COMPLEX : ( ( ) ( non zero V46() V57() V63() ) set ) ) ) : ( ( ) ( complex ) Element of COMPLEX : ( ( ) ( non zero V46() V57() V63() ) set ) ) : ( ( ) ( complex ) Element of COMPLEX : ( ( ) ( non zero V46() V57() V63() ) set ) ) = 1 : ( ( ) ( non zero natural complex V29() V30() V33() V34() V57() V58() V59() V60() V61() V62() ) Element of NAT : ( ( ) ( V57() V58() V59() V60() V61() V62() V63() ) Element of K19(REAL : ( ( ) ( non zero V46() V57() V58() V59() V63() ) set ) ) : ( ( ) ( ) set ) ) ) ;

theorem :: SIN_COS3:29

for n being ( ( ) ( natural complex V29() V30() V33() V34() V57() V58() V59() V60() V61() V62() ) Element of NAT : ( ( ) ( V57() V58() V59() V60() V61() V62() V63() ) Element of K19(REAL : ( ( ) ( non zero V46() V57() V58() V59() V63() ) set ) ) : ( ( ) ( ) set ) ) ) holds exp ((- ((2 : ( ( ) ( non zero natural complex V29() V30() V33() V34() V57() V58() V59() V60() V61() V62() ) Element of NAT : ( ( ) ( V57() V58() V59() V60() V61() V62() V63() ) Element of K19(REAL : ( ( ) ( non zero V46() V57() V58() V59() V63() ) set ) ) : ( ( ) ( ) set ) ) ) * PI : ( ( ) ( complex V29() V30() ) Element of REAL : ( ( ) ( non zero V46() V57() V58() V59() V63() ) set ) ) ) : ( ( ) ( complex V29() V30() ) Element of REAL : ( ( ) ( non zero V46() V57() V58() V59() V63() ) set ) ) * n : ( ( ) ( natural complex V29() V30() V33() V34() V57() V58() V59() V60() V61() V62() ) Element of NAT : ( ( ) ( V57() V58() V59() V60() V61() V62() V63() ) Element of K19(REAL : ( ( ) ( non zero V46() V57() V58() V59() V63() ) set ) ) : ( ( ) ( ) set ) ) ) ) : ( ( ) ( complex V29() V30() ) Element of REAL : ( ( ) ( non zero V46() V57() V58() V59() V63() ) set ) ) ) : ( ( ) ( complex V29() V30() ) Element of REAL : ( ( ) ( non zero V46() V57() V58() V59() V63() ) set ) ) * : ( ( ) ( complex ) Element of COMPLEX : ( ( ) ( non zero V46() V57() V63() ) set ) ) ) : ( ( ) ( complex ) Element of COMPLEX : ( ( ) ( non zero V46() V57() V63() ) set ) ) : ( ( ) ( complex ) Element of COMPLEX : ( ( ) ( non zero V46() V57() V63() ) set ) ) = 1 : ( ( ) ( non zero natural complex V29() V30() V33() V34() V57() V58() V59() V60() V61() V62() ) Element of NAT : ( ( ) ( V57() V58() V59() V60() V61() V62() V63() ) Element of K19(REAL : ( ( ) ( non zero V46() V57() V58() V59() V63() ) set ) ) : ( ( ) ( ) set ) ) ) ;

theorem :: SIN_COS3:30

for n being ( ( ) ( natural complex V29() V30() V33() V34() V57() V58() V59() V60() V61() V62() ) Element of NAT : ( ( ) ( V57() V58() V59() V60() V61() V62() V63() ) Element of K19(REAL : ( ( ) ( non zero V46() V57() V58() V59() V63() ) set ) ) : ( ( ) ( ) set ) ) ) holds exp ((((2 : ( ( ) ( non zero natural complex V29() V30() V33() V34() V57() V58() V59() V60() V61() V62() ) Element of NAT : ( ( ) ( V57() V58() V59() V60() V61() V62() V63() ) Element of K19(REAL : ( ( ) ( non zero V46() V57() V58() V59() V63() ) set ) ) : ( ( ) ( ) set ) ) ) * n : ( ( ) ( natural complex V29() V30() V33() V34() V57() V58() V59() V60() V61() V62() ) Element of NAT : ( ( ) ( V57() V58() V59() V60() V61() V62() V63() ) Element of K19(REAL : ( ( ) ( non zero V46() V57() V58() V59() V63() ) set ) ) : ( ( ) ( ) set ) ) ) ) : ( ( ) ( natural complex V29() V30() V33() V34() V57() V58() V59() V60() V61() V62() ) Element of NAT : ( ( ) ( V57() V58() V59() V60() V61() V62() V63() ) Element of K19(REAL : ( ( ) ( non zero V46() V57() V58() V59() V63() ) set ) ) : ( ( ) ( ) set ) ) ) + 1 : ( ( ) ( non zero natural complex V29() V30() V33() V34() V57() V58() V59() V60() V61() V62() ) Element of NAT : ( ( ) ( V57() V58() V59() V60() V61() V62() V63() ) Element of K19(REAL : ( ( ) ( non zero V46() V57() V58() V59() V63() ) set ) ) : ( ( ) ( ) set ) ) ) ) : ( ( ) ( natural complex V29() V30() V33() V34() V57() V58() V59() V60() V61() V62() ) Element of NAT : ( ( ) ( V57() V58() V59() V60() V61() V62() V63() ) Element of K19(REAL : ( ( ) ( non zero V46() V57() V58() V59() V63() ) set ) ) : ( ( ) ( ) set ) ) ) * PI : ( ( ) ( complex V29() V30() ) Element of REAL : ( ( ) ( non zero V46() V57() V58() V59() V63() ) set ) ) ) : ( ( ) ( complex V29() V30() ) Element of REAL : ( ( ) ( non zero V46() V57() V58() V59() V63() ) set ) ) * : ( ( ) ( complex ) Element of COMPLEX : ( ( ) ( non zero V46() V57() V63() ) set ) ) ) : ( ( ) ( complex ) Element of COMPLEX : ( ( ) ( non zero V46() V57() V63() ) set ) ) : ( ( ) ( complex ) Element of COMPLEX : ( ( ) ( non zero V46() V57() V63() ) set ) ) = - 1 : ( ( ) ( non zero natural complex V29() V30() V33() V34() V57() V58() V59() V60() V61() V62() ) Element of NAT : ( ( ) ( V57() V58() V59() V60() V61() V62() V63() ) Element of K19(REAL : ( ( ) ( non zero V46() V57() V58() V59() V63() ) set ) ) : ( ( ) ( ) set ) ) ) : ( ( ) ( non zero complex V29() V30() V33() V34() ) Element of INT : ( ( ) ( non zero V46() V57() V58() V59() V60() V61() V63() ) set ) ) ;

theorem :: SIN_COS3:31

for n being ( ( ) ( natural complex V29() V30() V33() V34() V57() V58() V59() V60() V61() V62() ) Element of NAT : ( ( ) ( V57() V58() V59() V60() V61() V62() V63() ) Element of K19(REAL : ( ( ) ( non zero V46() V57() V58() V59() V63() ) set ) ) : ( ( ) ( ) set ) ) ) holds exp ((- (((2 : ( ( ) ( non zero natural complex V29() V30() V33() V34() V57() V58() V59() V60() V61() V62() ) Element of NAT : ( ( ) ( V57() V58() V59() V60() V61() V62() V63() ) Element of K19(REAL : ( ( ) ( non zero V46() V57() V58() V59() V63() ) set ) ) : ( ( ) ( ) set ) ) ) * n : ( ( ) ( natural complex V29() V30() V33() V34() V57() V58() V59() V60() V61() V62() ) Element of NAT : ( ( ) ( V57() V58() V59() V60() V61() V62() V63() ) Element of K19(REAL : ( ( ) ( non zero V46() V57() V58() V59() V63() ) set ) ) : ( ( ) ( ) set ) ) ) ) : ( ( ) ( natural complex V29() V30() V33() V34() V57() V58() V59() V60() V61() V62() ) Element of NAT : ( ( ) ( V57() V58() V59() V60() V61() V62() V63() ) Element of K19(REAL : ( ( ) ( non zero V46() V57() V58() V59() V63() ) set ) ) : ( ( ) ( ) set ) ) ) + 1 : ( ( ) ( non zero natural complex V29() V30() V33() V34() V57() V58() V59() V60() V61() V62() ) Element of NAT : ( ( ) ( V57() V58() V59() V60() V61() V62() V63() ) Element of K19(REAL : ( ( ) ( non zero V46() V57() V58() V59() V63() ) set ) ) : ( ( ) ( ) set ) ) ) ) : ( ( ) ( natural complex V29() V30() V33() V34() V57() V58() V59() V60() V61() V62() ) Element of NAT : ( ( ) ( V57() V58() V59() V60() V61() V62() V63() ) Element of K19(REAL : ( ( ) ( non zero V46() V57() V58() V59() V63() ) set ) ) : ( ( ) ( ) set ) ) ) * PI : ( ( ) ( complex V29() V30() ) Element of REAL : ( ( ) ( non zero V46() V57() V58() V59() V63() ) set ) ) ) : ( ( ) ( complex V29() V30() ) Element of REAL : ( ( ) ( non zero V46() V57() V58() V59() V63() ) set ) ) ) : ( ( ) ( complex V29() V30() ) Element of REAL : ( ( ) ( non zero V46() V57() V58() V59() V63() ) set ) ) * : ( ( ) ( complex ) Element of COMPLEX : ( ( ) ( non zero V46() V57() V63() ) set ) ) ) : ( ( ) ( complex ) Element of COMPLEX : ( ( ) ( non zero V46() V57() V63() ) set ) ) : ( ( ) ( complex ) Element of COMPLEX : ( ( ) ( non zero V46() V57() V63() ) set ) ) = - 1 : ( ( ) ( non zero natural complex V29() V30() V33() V34() V57() V58() V59() V60() V61() V62() ) Element of NAT : ( ( ) ( V57() V58() V59() V60() V61() V62() V63() ) Element of K19(REAL : ( ( ) ( non zero V46() V57() V58() V59() V63() ) set ) ) : ( ( ) ( ) set ) ) ) : ( ( ) ( non zero complex V29() V30() V33() V34() ) Element of INT : ( ( ) ( non zero V46() V57() V58() V59() V60() V61() V63() ) set ) ) ;

theorem :: SIN_COS3:32

for n being ( ( ) ( natural complex V29() V30() V33() V34() V57() V58() V59() V60() V61() V62() ) Element of NAT : ( ( ) ( V57() V58() V59() V60() V61() V62() V63() ) Element of K19(REAL : ( ( ) ( non zero V46() V57() V58() V59() V63() ) set ) ) : ( ( ) ( ) set ) ) ) holds exp ((((2 : ( ( ) ( non zero natural complex V29() V30() V33() V34() V57() V58() V59() V60() V61() V62() ) Element of NAT : ( ( ) ( V57() V58() V59() V60() V61() V62() V63() ) Element of K19(REAL : ( ( ) ( non zero V46() V57() V58() V59() V63() ) set ) ) : ( ( ) ( ) set ) ) ) * n : ( ( ) ( natural complex V29() V30() V33() V34() V57() V58() V59() V60() V61() V62() ) Element of NAT : ( ( ) ( V57() V58() V59() V60() V61() V62() V63() ) Element of K19(REAL : ( ( ) ( non zero V46() V57() V58() V59() V63() ) set ) ) : ( ( ) ( ) set ) ) ) ) : ( ( ) ( natural complex V29() V30() V33() V34() V57() V58() V59() V60() V61() V62() ) Element of NAT : ( ( ) ( V57() V58() V59() V60() V61() V62() V63() ) Element of K19(REAL : ( ( ) ( non zero V46() V57() V58() V59() V63() ) set ) ) : ( ( ) ( ) set ) ) ) + (1 : ( ( ) ( non zero natural complex V29() V30() V33() V34() V57() V58() V59() V60() V61() V62() ) Element of NAT : ( ( ) ( V57() V58() V59() V60() V61() V62() V63() ) Element of K19(REAL : ( ( ) ( non zero V46() V57() V58() V59() V63() ) set ) ) : ( ( ) ( ) set ) ) ) / 2 : ( ( ) ( non zero natural complex V29() V30() V33() V34() V57() V58() V59() V60() V61() V62() ) Element of NAT : ( ( ) ( V57() V58() V59() V60() V61() V62() V63() ) Element of K19(REAL : ( ( ) ( non zero V46() V57() V58() V59() V63() ) set ) ) : ( ( ) ( ) set ) ) ) ) : ( ( ) ( non zero complex V29() V30() V34() ) Element of RAT : ( ( ) ( non zero V46() V57() V58() V59() V60() V63() ) set ) ) ) : ( ( ) ( complex V29() V30() V34() ) Element of RAT : ( ( ) ( non zero V46() V57() V58() V59() V60() V63() ) set ) ) * PI : ( ( ) ( complex V29() V30() ) Element of REAL : ( ( ) ( non zero V46() V57() V58() V59() V63() ) set ) ) ) : ( ( ) ( complex V29() V30() ) Element of REAL : ( ( ) ( non zero V46() V57() V58() V59() V63() ) set ) ) * : ( ( ) ( complex ) Element of COMPLEX : ( ( ) ( non zero V46() V57() V63() ) set ) ) ) : ( ( ) ( complex ) Element of COMPLEX : ( ( ) ( non zero V46() V57() V63() ) set ) ) : ( ( ) ( complex ) Element of COMPLEX : ( ( ) ( non zero V46() V57() V63() ) set ) ) = : ( ( ) ( complex ) Element of COMPLEX : ( ( ) ( non zero V46() V57() V63() ) set ) ) ;

theorem :: SIN_COS3:33

for n being ( ( ) ( natural complex V29() V30() V33() V34() V57() V58() V59() V60() V61() V62() ) Element of NAT : ( ( ) ( V57() V58() V59() V60() V61() V62() V63() ) Element of K19(REAL : ( ( ) ( non zero V46() V57() V58() V59() V63() ) set ) ) : ( ( ) ( ) set ) ) ) holds exp ((- (((2 : ( ( ) ( non zero natural complex V29() V30() V33() V34() V57() V58() V59() V60() V61() V62() ) Element of NAT : ( ( ) ( V57() V58() V59() V60() V61() V62() V63() ) Element of K19(REAL : ( ( ) ( non zero V46() V57() V58() V59() V63() ) set ) ) : ( ( ) ( ) set ) ) ) * n : ( ( ) ( natural complex V29() V30() V33() V34() V57() V58() V59() V60() V61() V62() ) Element of NAT : ( ( ) ( V57() V58() V59() V60() V61() V62() V63() ) Element of K19(REAL : ( ( ) ( non zero V46() V57() V58() V59() V63() ) set ) ) : ( ( ) ( ) set ) ) ) ) : ( ( ) ( natural complex V29() V30() V33() V34() V57() V58() V59() V60() V61() V62() ) Element of NAT : ( ( ) ( V57() V58() V59() V60() V61() V62() V63() ) Element of K19(REAL : ( ( ) ( non zero V46() V57() V58() V59() V63() ) set ) ) : ( ( ) ( ) set ) ) ) + (1 : ( ( ) ( non zero natural complex V29() V30() V33() V34() V57() V58() V59() V60() V61() V62() ) Element of NAT : ( ( ) ( V57() V58() V59() V60() V61() V62() V63() ) Element of K19(REAL : ( ( ) ( non zero V46() V57() V58() V59() V63() ) set ) ) : ( ( ) ( ) set ) ) ) / 2 : ( ( ) ( non zero natural complex V29() V30() V33() V34() V57() V58() V59() V60() V61() V62() ) Element of NAT : ( ( ) ( V57() V58() V59() V60() V61() V62() V63() ) Element of K19(REAL : ( ( ) ( non zero V46() V57() V58() V59() V63() ) set ) ) : ( ( ) ( ) set ) ) ) ) : ( ( ) ( non zero complex V29() V30() V34() ) Element of RAT : ( ( ) ( non zero V46() V57() V58() V59() V60() V63() ) set ) ) ) : ( ( ) ( complex V29() V30() V34() ) Element of RAT : ( ( ) ( non zero V46() V57() V58() V59() V60() V63() ) set ) ) * PI : ( ( ) ( complex V29() V30() ) Element of REAL : ( ( ) ( non zero V46() V57() V58() V59() V63() ) set ) ) ) : ( ( ) ( complex V29() V30() ) Element of REAL : ( ( ) ( non zero V46() V57() V58() V59() V63() ) set ) ) ) : ( ( ) ( complex V29() V30() ) Element of REAL : ( ( ) ( non zero V46() V57() V58() V59() V63() ) set ) ) * : ( ( ) ( complex ) Element of COMPLEX : ( ( ) ( non zero V46() V57() V63() ) set ) ) ) : ( ( ) ( complex ) Element of COMPLEX : ( ( ) ( non zero V46() V57() V63() ) set ) ) : ( ( ) ( complex ) Element of COMPLEX : ( ( ) ( non zero V46() V57() V63() ) set ) ) = - (1 : ( ( ) ( non zero natural complex V29() V30() V33() V34() V57() V58() V59() V60() V61() V62() ) Element of NAT : ( ( ) ( V57() V58() V59() V60() V61() V62() V63() ) Element of K19(REAL : ( ( ) ( non zero V46() V57() V58() V59() V63() ) set ) ) : ( ( ) ( ) set ) ) ) * : ( ( ) ( complex ) Element of COMPLEX : ( ( ) ( non zero V46() V57() V63() ) set ) ) ) : ( ( ) ( complex ) Element of COMPLEX : ( ( ) ( non zero V46() V57() V63() ) set ) ) : ( ( ) ( complex ) Element of COMPLEX : ( ( ) ( non zero V46() V57() V63() ) set ) ) ;

theorem :: SIN_COS3:34

for z being ( ( ) ( complex ) Element of COMPLEX : ( ( ) ( non zero V46() V57() V63() ) set ) )
for n being ( ( ) ( natural complex V29() V30() V33() V34() V57() V58() V59() V60() V61() V62() ) Element of NAT : ( ( ) ( V57() V58() V59() V60() V61() V62() V63() ) Element of K19(REAL : ( ( ) ( non zero V46() V57() V58() V59() V63() ) set ) ) : ( ( ) ( ) set ) ) ) holds sin_C : ( ( V6() V18( COMPLEX : ( ( ) ( non zero V46() V57() V63() ) set ) , COMPLEX : ( ( ) ( non zero V46() V57() V63() ) set ) ) ) ( V1() V4( COMPLEX : ( ( ) ( non zero V46() V57() V63() ) set ) ) V5( COMPLEX : ( ( ) ( non zero V46() V57() V63() ) set ) ) V6() non zero total V18( COMPLEX : ( ( ) ( non zero V46() V57() V63() ) set ) , COMPLEX : ( ( ) ( non zero V46() V57() V63() ) set ) ) ) Function of COMPLEX : ( ( ) ( non zero V46() V57() V63() ) set ) , COMPLEX : ( ( ) ( non zero V46() V57() V63() ) set ) ) /. (z : ( ( ) ( complex ) Element of COMPLEX : ( ( ) ( non zero V46() V57() V63() ) set ) ) + ((2 : ( ( ) ( non zero natural complex V29() V30() V33() V34() V57() V58() V59() V60() V61() V62() ) Element of NAT : ( ( ) ( V57() V58() V59() V60() V61() V62() V63() ) Element of K19(REAL : ( ( ) ( non zero V46() V57() V58() V59() V63() ) set ) ) : ( ( ) ( ) set ) ) ) * n : ( ( ) ( natural complex V29() V30() V33() V34() V57() V58() V59() V60() V61() V62() ) Element of NAT : ( ( ) ( V57() V58() V59() V60() V61() V62() V63() ) Element of K19(REAL : ( ( ) ( non zero V46() V57() V58() V59() V63() ) set ) ) : ( ( ) ( ) set ) ) ) ) : ( ( ) ( natural complex V29() V30() V33() V34() V57() V58() V59() V60() V61() V62() ) Element of NAT : ( ( ) ( V57() V58() V59() V60() V61() V62() V63() ) Element of K19(REAL : ( ( ) ( non zero V46() V57() V58() V59() V63() ) set ) ) : ( ( ) ( ) set ) ) ) * PI : ( ( ) ( complex V29() V30() ) Element of REAL : ( ( ) ( non zero V46() V57() V58() V59() V63() ) set ) ) ) : ( ( ) ( complex V29() V30() ) Element of REAL : ( ( ) ( non zero V46() V57() V58() V59() V63() ) set ) ) ) : ( ( ) ( complex ) Element of COMPLEX : ( ( ) ( non zero V46() V57() V63() ) set ) ) : ( ( ) ( complex ) Element of COMPLEX : ( ( ) ( non zero V46() V57() V63() ) set ) ) = sin_C : ( ( V6() V18( COMPLEX : ( ( ) ( non zero V46() V57() V63() ) set ) , COMPLEX : ( ( ) ( non zero V46() V57() V63() ) set ) ) ) ( V1() V4( COMPLEX : ( ( ) ( non zero V46() V57() V63() ) set ) ) V5( COMPLEX : ( ( ) ( non zero V46() V57() V63() ) set ) ) V6() non zero total V18( COMPLEX : ( ( ) ( non zero V46() V57() V63() ) set ) , COMPLEX : ( ( ) ( non zero V46() V57() V63() ) set ) ) ) Function of COMPLEX : ( ( ) ( non zero V46() V57() V63() ) set ) , COMPLEX : ( ( ) ( non zero V46() V57() V63() ) set ) ) /. z : ( ( ) ( complex ) Element of COMPLEX : ( ( ) ( non zero V46() V57() V63() ) set ) ) : ( ( ) ( complex ) Element of COMPLEX : ( ( ) ( non zero V46() V57() V63() ) set ) ) ;

theorem :: SIN_COS3:35

for z being ( ( ) ( complex ) Element of COMPLEX : ( ( ) ( non zero V46() V57() V63() ) set ) )
for n being ( ( ) ( natural complex V29() V30() V33() V34() V57() V58() V59() V60() V61() V62() ) Element of NAT : ( ( ) ( V57() V58() V59() V60() V61() V62() V63() ) Element of K19(REAL : ( ( ) ( non zero V46() V57() V58() V59() V63() ) set ) ) : ( ( ) ( ) set ) ) ) holds cos_C : ( ( V6() V18( COMPLEX : ( ( ) ( non zero V46() V57() V63() ) set ) , COMPLEX : ( ( ) ( non zero V46() V57() V63() ) set ) ) ) ( V1() V4( COMPLEX : ( ( ) ( non zero V46() V57() V63() ) set ) ) V5( COMPLEX : ( ( ) ( non zero V46() V57() V63() ) set ) ) V6() non zero total V18( COMPLEX : ( ( ) ( non zero V46() V57() V63() ) set ) , COMPLEX : ( ( ) ( non zero V46() V57() V63() ) set ) ) ) Function of COMPLEX : ( ( ) ( non zero V46() V57() V63() ) set ) , COMPLEX : ( ( ) ( non zero V46() V57() V63() ) set ) ) /. (z : ( ( ) ( complex ) Element of COMPLEX : ( ( ) ( non zero V46() V57() V63() ) set ) ) + ((2 : ( ( ) ( non zero natural complex V29() V30() V33() V34() V57() V58() V59() V60() V61() V62() ) Element of NAT : ( ( ) ( V57() V58() V59() V60() V61() V62() V63() ) Element of K19(REAL : ( ( ) ( non zero V46() V57() V58() V59() V63() ) set ) ) : ( ( ) ( ) set ) ) ) * n : ( ( ) ( natural complex V29() V30() V33() V34() V57() V58() V59() V60() V61() V62() ) Element of NAT : ( ( ) ( V57() V58() V59() V60() V61() V62() V63() ) Element of K19(REAL : ( ( ) ( non zero V46() V57() V58() V59() V63() ) set ) ) : ( ( ) ( ) set ) ) ) ) : ( ( ) ( natural complex V29() V30() V33() V34() V57() V58() V59() V60() V61() V62() ) Element of NAT : ( ( ) ( V57() V58() V59() V60() V61() V62() V63() ) Element of K19(REAL : ( ( ) ( non zero V46() V57() V58() V59() V63() ) set ) ) : ( ( ) ( ) set ) ) ) * PI : ( ( ) ( complex V29() V30() ) Element of REAL : ( ( ) ( non zero V46() V57() V58() V59() V63() ) set ) ) ) : ( ( ) ( complex V29() V30() ) Element of REAL : ( ( ) ( non zero V46() V57() V58() V59() V63() ) set ) ) ) : ( ( ) ( complex ) Element of COMPLEX : ( ( ) ( non zero V46() V57() V63() ) set ) ) : ( ( ) ( complex ) Element of COMPLEX : ( ( ) ( non zero V46() V57() V63() ) set ) ) = cos_C : ( ( V6() V18( COMPLEX : ( ( ) ( non zero V46() V57() V63() ) set ) , COMPLEX : ( ( ) ( non zero V46() V57() V63() ) set ) ) ) ( V1() V4( COMPLEX : ( ( ) ( non zero V46() V57() V63() ) set ) ) V5( COMPLEX : ( ( ) ( non zero V46() V57() V63() ) set ) ) V6() non zero total V18( COMPLEX : ( ( ) ( non zero V46() V57() V63() ) set ) , COMPLEX : ( ( ) ( non zero V46() V57() V63() ) set ) ) ) Function of COMPLEX : ( ( ) ( non zero V46() V57() V63() ) set ) , COMPLEX : ( ( ) ( non zero V46() V57() V63() ) set ) ) /. z : ( ( ) ( complex ) Element of COMPLEX : ( ( ) ( non zero V46() V57() V63() ) set ) ) : ( ( ) ( complex ) Element of COMPLEX : ( ( ) ( non zero V46() V57() V63() ) set ) ) ;

theorem :: SIN_COS3:36

for z being ( ( complex ) ( complex ) number ) holds exp ( : ( ( ) ( complex ) Element of COMPLEX : ( ( ) ( non zero V46() V57() V63() ) set ) ) * z : ( ( complex ) ( complex ) number ) ) : ( ( ) ( complex ) Element of COMPLEX : ( ( ) ( non zero V46() V57() V63() ) set ) ) : ( ( ) ( complex ) Element of COMPLEX : ( ( ) ( non zero V46() V57() V63() ) set ) ) = (cos_C : ( ( V6() V18( COMPLEX : ( ( ) ( non zero V46() V57() V63() ) set ) , COMPLEX : ( ( ) ( non zero V46() V57() V63() ) set ) ) ) ( V1() V4( COMPLEX : ( ( ) ( non zero V46() V57() V63() ) set ) ) V5( COMPLEX : ( ( ) ( non zero V46() V57() V63() ) set ) ) V6() non zero total V18( COMPLEX : ( ( ) ( non zero V46() V57() V63() ) set ) , COMPLEX : ( ( ) ( non zero V46() V57() V63() ) set ) ) ) Function of COMPLEX : ( ( ) ( non zero V46() V57() V63() ) set ) , COMPLEX : ( ( ) ( non zero V46() V57() V63() ) set ) ) /. z : ( ( complex ) ( complex ) number ) ) : ( ( ) ( complex ) Element of COMPLEX : ( ( ) ( non zero V46() V57() V63() ) set ) ) + ( : ( ( ) ( complex ) Element of COMPLEX : ( ( ) ( non zero V46() V57() V63() ) set ) ) * (sin_C : ( ( V6() V18( COMPLEX : ( ( ) ( non zero V46() V57() V63() ) set ) , COMPLEX : ( ( ) ( non zero V46() V57() V63() ) set ) ) ) ( V1() V4( COMPLEX : ( ( ) ( non zero V46() V57() V63() ) set ) ) V5( COMPLEX : ( ( ) ( non zero V46() V57() V63() ) set ) ) V6() non zero total V18( COMPLEX : ( ( ) ( non zero V46() V57() V63() ) set ) , COMPLEX : ( ( ) ( non zero V46() V57() V63() ) set ) ) ) Function of COMPLEX : ( ( ) ( non zero V46() V57() V63() ) set ) , COMPLEX : ( ( ) ( non zero V46() V57() V63() ) set ) ) /. z : ( ( complex ) ( complex ) number ) ) : ( ( ) ( complex ) Element of COMPLEX : ( ( ) ( non zero V46() V57() V63() ) set ) ) ) : ( ( ) ( complex ) Element of COMPLEX : ( ( ) ( non zero V46() V57() V63() ) set ) ) : ( ( ) ( complex ) Element of COMPLEX : ( ( ) ( non zero V46() V57() V63() ) set ) ) ;

theorem :: SIN_COS3:37

for z being ( ( complex ) ( complex ) number ) holds exp (- ( : ( ( ) ( complex ) Element of COMPLEX : ( ( ) ( non zero V46() V57() V63() ) set ) ) * z : ( ( complex ) ( complex ) number ) ) : ( ( ) ( complex ) Element of COMPLEX : ( ( ) ( non zero V46() V57() V63() ) set ) ) ) : ( ( ) ( complex ) Element of COMPLEX : ( ( ) ( non zero V46() V57() V63() ) set ) ) : ( ( ) ( complex ) Element of COMPLEX : ( ( ) ( non zero V46() V57() V63() ) set ) ) = (cos_C : ( ( V6() V18( COMPLEX : ( ( ) ( non zero V46() V57() V63() ) set ) , COMPLEX : ( ( ) ( non zero V46() V57() V63() ) set ) ) ) ( V1() V4( COMPLEX : ( ( ) ( non zero V46() V57() V63() ) set ) ) V5( COMPLEX : ( ( ) ( non zero V46() V57() V63() ) set ) ) V6() non zero total V18( COMPLEX : ( ( ) ( non zero V46() V57() V63() ) set ) , COMPLEX : ( ( ) ( non zero V46() V57() V63() ) set ) ) ) Function of COMPLEX : ( ( ) ( non zero V46() V57() V63() ) set ) , COMPLEX : ( ( ) ( non zero V46() V57() V63() ) set ) ) /. z : ( ( complex ) ( complex ) number ) ) : ( ( ) ( complex ) Element of COMPLEX : ( ( ) ( non zero V46() V57() V63() ) set ) ) - ( : ( ( ) ( complex ) Element of COMPLEX : ( ( ) ( non zero V46() V57() V63() ) set ) ) * (sin_C : ( ( V6() V18( COMPLEX : ( ( ) ( non zero V46() V57() V63() ) set ) , COMPLEX : ( ( ) ( non zero V46() V57() V63() ) set ) ) ) ( V1() V4( COMPLEX : ( ( ) ( non zero V46() V57() V63() ) set ) ) V5( COMPLEX : ( ( ) ( non zero V46() V57() V63() ) set ) ) V6() non zero total V18( COMPLEX : ( ( ) ( non zero V46() V57() V63() ) set ) , COMPLEX : ( ( ) ( non zero V46() V57() V63() ) set ) ) ) Function of COMPLEX : ( ( ) ( non zero V46() V57() V63() ) set ) , COMPLEX : ( ( ) ( non zero V46() V57() V63() ) set ) ) /. z : ( ( complex ) ( complex ) number ) ) : ( ( ) ( complex ) Element of COMPLEX : ( ( ) ( non zero V46() V57() V63() ) set ) ) ) : ( ( ) ( complex ) Element of COMPLEX : ( ( ) ( non zero V46() V57() V63() ) set ) ) : ( ( ) ( complex ) Element of COMPLEX : ( ( ) ( non zero V46() V57() V63() ) set ) ) ;

theorem :: SIN_COS3:38

for x being ( ( ) ( complex V29() V30() ) Element of REAL : ( ( ) ( non zero V46() V57() V58() V59() V63() ) set ) ) holds sin_C : ( ( V6() V18( COMPLEX : ( ( ) ( non zero V46() V57() V63() ) set ) , COMPLEX : ( ( ) ( non zero V46() V57() V63() ) set ) ) ) ( V1() V4( COMPLEX : ( ( ) ( non zero V46() V57() V63() ) set ) ) V5( COMPLEX : ( ( ) ( non zero V46() V57() V63() ) set ) ) V6() non zero total V18( COMPLEX : ( ( ) ( non zero V46() V57() V63() ) set ) , COMPLEX : ( ( ) ( non zero V46() V57() V63() ) set ) ) ) Function of COMPLEX : ( ( ) ( non zero V46() V57() V63() ) set ) , COMPLEX : ( ( ) ( non zero V46() V57() V63() ) set ) ) /. x : ( ( ) ( complex V29() V30() ) Element of REAL : ( ( ) ( non zero V46() V57() V58() V59() V63() ) set ) ) : ( ( ) ( complex ) Element of COMPLEX : ( ( ) ( non zero V46() V57() V63() ) set ) ) = sin : ( ( V6() V18( REAL : ( ( ) ( non zero V46() V57() V58() V59() V63() ) set ) , REAL : ( ( ) ( non zero V46() V57() V58() V59() V63() ) set ) ) ) ( V1() V4( REAL : ( ( ) ( non zero V46() V57() V58() V59() V63() ) set ) ) V5( REAL : ( ( ) ( non zero V46() V57() V58() V59() V63() ) set ) ) V6() non zero total V18( REAL : ( ( ) ( non zero V46() V57() V58() V59() V63() ) set ) , REAL : ( ( ) ( non zero V46() V57() V58() V59() V63() ) set ) ) ) Element of K19(K20(REAL : ( ( ) ( non zero V46() V57() V58() V59() V63() ) set ) ,REAL : ( ( ) ( non zero V46() V57() V58() V59() V63() ) set ) ) : ( ( ) ( ) set ) ) : ( ( ) ( ) set ) ) . x : ( ( ) ( complex V29() V30() ) Element of REAL : ( ( ) ( non zero V46() V57() V58() V59() V63() ) set ) ) : ( ( ) ( complex V29() V30() ) Element of REAL : ( ( ) ( non zero V46() V57() V58() V59() V63() ) set ) ) ;

theorem :: SIN_COS3:39

for x being ( ( ) ( complex V29() V30() ) Element of REAL : ( ( ) ( non zero V46() V57() V58() V59() V63() ) set ) ) holds cos_C : ( ( V6() V18( COMPLEX : ( ( ) ( non zero V46() V57() V63() ) set ) , COMPLEX : ( ( ) ( non zero V46() V57() V63() ) set ) ) ) ( V1() V4( COMPLEX : ( ( ) ( non zero V46() V57() V63() ) set ) ) V5( COMPLEX : ( ( ) ( non zero V46() V57() V63() ) set ) ) V6() non zero total V18( COMPLEX : ( ( ) ( non zero V46() V57() V63() ) set ) , COMPLEX : ( ( ) ( non zero V46() V57() V63() ) set ) ) ) Function of COMPLEX : ( ( ) ( non zero V46() V57() V63() ) set ) , COMPLEX : ( ( ) ( non zero V46() V57() V63() ) set ) ) /. x : ( ( ) ( complex V29() V30() ) Element of REAL : ( ( ) ( non zero V46() V57() V58() V59() V63() ) set ) ) : ( ( ) ( complex ) Element of COMPLEX : ( ( ) ( non zero V46() V57() V63() ) set ) ) = cos : ( ( V6() V18( REAL : ( ( ) ( non zero V46() V57() V58() V59() V63() ) set ) , REAL : ( ( ) ( non zero V46() V57() V58() V59() V63() ) set ) ) ) ( V1() V4( REAL : ( ( ) ( non zero V46() V57() V58() V59() V63() ) set ) ) V5( REAL : ( ( ) ( non zero V46() V57() V58() V59() V63() ) set ) ) V6() non zero total V18( REAL : ( ( ) ( non zero V46() V57() V58() V59() V63() ) set ) , REAL : ( ( ) ( non zero V46() V57() V58() V59() V63() ) set ) ) ) Element of K19(K20(REAL : ( ( ) ( non zero V46() V57() V58() V59() V63() ) set ) ,REAL : ( ( ) ( non zero V46() V57() V58() V59() V63() ) set ) ) : ( ( ) ( ) set ) ) : ( ( ) ( ) set ) ) . x : ( ( ) ( complex V29() V30() ) Element of REAL : ( ( ) ( non zero V46() V57() V58() V59() V63() ) set ) ) : ( ( ) ( complex V29() V30() ) Element of REAL : ( ( ) ( non zero V46() V57() V58() V59() V63() ) set ) ) ;

theorem :: SIN_COS3:40

for x being ( ( ) ( complex V29() V30() ) Element of REAL : ( ( ) ( non zero V46() V57() V58() V59() V63() ) set ) ) holds sinh_C : ( ( V6() V18( COMPLEX : ( ( ) ( non zero V46() V57() V63() ) set ) , COMPLEX : ( ( ) ( non zero V46() V57() V63() ) set ) ) ) ( V1() V4( COMPLEX : ( ( ) ( non zero V46() V57() V63() ) set ) ) V5( COMPLEX : ( ( ) ( non zero V46() V57() V63() ) set ) ) V6() non zero total V18( COMPLEX : ( ( ) ( non zero V46() V57() V63() ) set ) , COMPLEX : ( ( ) ( non zero V46() V57() V63() ) set ) ) ) Function of COMPLEX : ( ( ) ( non zero V46() V57() V63() ) set ) , COMPLEX : ( ( ) ( non zero V46() V57() V63() ) set ) ) /. x : ( ( ) ( complex V29() V30() ) Element of REAL : ( ( ) ( non zero V46() V57() V58() V59() V63() ) set ) ) : ( ( ) ( complex ) Element of COMPLEX : ( ( ) ( non zero V46() V57() V63() ) set ) ) = sinh : ( ( V6() V18( REAL : ( ( ) ( non zero V46() V57() V58() V59() V63() ) set ) , REAL : ( ( ) ( non zero V46() V57() V58() V59() V63() ) set ) ) ) ( V1() V4( REAL : ( ( ) ( non zero V46() V57() V58() V59() V63() ) set ) ) V5( REAL : ( ( ) ( non zero V46() V57() V58() V59() V63() ) set ) ) V6() non zero total V18( REAL : ( ( ) ( non zero V46() V57() V58() V59() V63() ) set ) , REAL : ( ( ) ( non zero V46() V57() V58() V59() V63() ) set ) ) ) Element of K19(K20(REAL : ( ( ) ( non zero V46() V57() V58() V59() V63() ) set ) ,REAL : ( ( ) ( non zero V46() V57() V58() V59() V63() ) set ) ) : ( ( ) ( ) set ) ) : ( ( ) ( ) set ) ) . x : ( ( ) ( complex V29() V30() ) Element of REAL : ( ( ) ( non zero V46() V57() V58() V59() V63() ) set ) ) : ( ( ) ( complex V29() V30() ) Element of REAL : ( ( ) ( non zero V46() V57() V58() V59() V63() ) set ) ) ;

theorem :: SIN_COS3:41

for x being ( ( ) ( complex V29() V30() ) Element of REAL : ( ( ) ( non zero V46() V57() V58() V59() V63() ) set ) ) holds cosh_C : ( ( V6() V18( COMPLEX : ( ( ) ( non zero V46() V57() V63() ) set ) , COMPLEX : ( ( ) ( non zero V46() V57() V63() ) set ) ) ) ( V1() V4( COMPLEX : ( ( ) ( non zero V46() V57() V63() ) set ) ) V5( COMPLEX : ( ( ) ( non zero V46() V57() V63() ) set ) ) V6() non zero total V18( COMPLEX : ( ( ) ( non zero V46() V57() V63() ) set ) , COMPLEX : ( ( ) ( non zero V46() V57() V63() ) set ) ) ) Function of COMPLEX : ( ( ) ( non zero V46() V57() V63() ) set ) , COMPLEX : ( ( ) ( non zero V46() V57() V63() ) set ) ) /. x : ( ( ) ( complex V29() V30() ) Element of REAL : ( ( ) ( non zero V46() V57() V58() V59() V63() ) set ) ) : ( ( ) ( complex ) Element of COMPLEX : ( ( ) ( non zero V46() V57() V63() ) set ) ) = cosh : ( ( V6() V18( REAL : ( ( ) ( non zero V46() V57() V58() V59() V63() ) set ) , REAL : ( ( ) ( non zero V46() V57() V58() V59() V63() ) set ) ) ) ( V1() V4( REAL : ( ( ) ( non zero V46() V57() V58() V59() V63() ) set ) ) V5( REAL : ( ( ) ( non zero V46() V57() V58() V59() V63() ) set ) ) V6() non zero total V18( REAL : ( ( ) ( non zero V46() V57() V58() V59() V63() ) set ) , REAL : ( ( ) ( non zero V46() V57() V58() V59() V63() ) set ) ) ) Element of K19(K20(REAL : ( ( ) ( non zero V46() V57() V58() V59() V63() ) set ) ,REAL : ( ( ) ( non zero V46() V57() V58() V59() V63() ) set ) ) : ( ( ) ( ) set ) ) : ( ( ) ( ) set ) ) . x : ( ( ) ( complex V29() V30() ) Element of REAL : ( ( ) ( non zero V46() V57() V58() V59() V63() ) set ) ) : ( ( ) ( complex V29() V30() ) Element of REAL : ( ( ) ( non zero V46() V57() V58() V59() V63() ) set ) ) ;

theorem :: SIN_COS3:42

for x, y being ( ( ) ( complex V29() V30() ) Element of REAL : ( ( ) ( non zero V46() V57() V58() V59() V63() ) set ) ) holds sin_C : ( ( V6() V18( COMPLEX : ( ( ) ( non zero V46() V57() V63() ) set ) , COMPLEX : ( ( ) ( non zero V46() V57() V63() ) set ) ) ) ( V1() V4( COMPLEX : ( ( ) ( non zero V46() V57() V63() ) set ) ) V5( COMPLEX : ( ( ) ( non zero V46() V57() V63() ) set ) ) V6() non zero total V18( COMPLEX : ( ( ) ( non zero V46() V57() V63() ) set ) , COMPLEX : ( ( ) ( non zero V46() V57() V63() ) set ) ) ) Function of COMPLEX : ( ( ) ( non zero V46() V57() V63() ) set ) , COMPLEX : ( ( ) ( non zero V46() V57() V63() ) set ) ) /. (x : ( ( ) ( complex V29() V30() ) Element of REAL : ( ( ) ( non zero V46() V57() V58() V59() V63() ) set ) ) + (y : ( ( ) ( complex V29() V30() ) Element of REAL : ( ( ) ( non zero V46() V57() V58() V59() V63() ) set ) ) * : ( ( ) ( complex ) Element of COMPLEX : ( ( ) ( non zero V46() V57() V63() ) set ) ) ) : ( ( ) ( complex ) Element of COMPLEX : ( ( ) ( non zero V46() V57() V63() ) set ) ) ) : ( ( ) ( complex ) Element of COMPLEX : ( ( ) ( non zero V46() V57() V63() ) set ) ) : ( ( ) ( complex ) Element of COMPLEX : ( ( ) ( non zero V46() V57() V63() ) set ) ) = ((sin : ( ( V6() V18( REAL : ( ( ) ( non zero V46() V57() V58() V59() V63() ) set ) , REAL : ( ( ) ( non zero V46() V57() V58() V59() V63() ) set ) ) ) ( V1() V4( REAL : ( ( ) ( non zero V46() V57() V58() V59() V63() ) set ) ) V5( REAL : ( ( ) ( non zero V46() V57() V58() V59() V63() ) set ) ) V6() non zero total V18( REAL : ( ( ) ( non zero V46() V57() V58() V59() V63() ) set ) , REAL : ( ( ) ( non zero V46() V57() V58() V59() V63() ) set ) ) ) Element of K19(K20(REAL : ( ( ) ( non zero V46() V57() V58() V59() V63() ) set ) ,REAL : ( ( ) ( non zero V46() V57() V58() V59() V63() ) set ) ) : ( ( ) ( ) set ) ) : ( ( ) ( ) set ) ) . x : ( ( ) ( complex V29() V30() ) Element of REAL : ( ( ) ( non zero V46() V57() V58() V59() V63() ) set ) ) ) : ( ( ) ( complex V29() V30() ) Element of REAL : ( ( ) ( non zero V46() V57() V58() V59() V63() ) set ) ) * (cosh : ( ( V6() V18( REAL : ( ( ) ( non zero V46() V57() V58() V59() V63() ) set ) , REAL : ( ( ) ( non zero V46() V57() V58() V59() V63() ) set ) ) ) ( V1() V4( REAL : ( ( ) ( non zero V46() V57() V58() V59() V63() ) set ) ) V5( REAL : ( ( ) ( non zero V46() V57() V58() V59() V63() ) set ) ) V6() non zero total V18( REAL : ( ( ) ( non zero V46() V57() V58() V59() V63() ) set ) , REAL : ( ( ) ( non zero V46() V57() V58() V59() V63() ) set ) ) ) Element of K19(K20(REAL : ( ( ) ( non zero V46() V57() V58() V59() V63() ) set ) ,REAL : ( ( ) ( non zero V46() V57() V58() V59() V63() ) set ) ) : ( ( ) ( ) set ) ) : ( ( ) ( ) set ) ) . y : ( ( ) ( complex V29() V30() ) Element of REAL : ( ( ) ( non zero V46() V57() V58() V59() V63() ) set ) ) ) : ( ( ) ( complex V29() V30() ) Element of REAL : ( ( ) ( non zero V46() V57() V58() V59() V63() ) set ) ) ) : ( ( ) ( complex V29() V30() ) Element of REAL : ( ( ) ( non zero V46() V57() V58() V59() V63() ) set ) ) + (((cos : ( ( V6() V18( REAL : ( ( ) ( non zero V46() V57() V58() V59() V63() ) set ) , REAL : ( ( ) ( non zero V46() V57() V58() V59() V63() ) set ) ) ) ( V1() V4( REAL : ( ( ) ( non zero V46() V57() V58() V59() V63() ) set ) ) V5( REAL : ( ( ) ( non zero V46() V57() V58() V59() V63() ) set ) ) V6() non zero total V18( REAL : ( ( ) ( non zero V46() V57() V58() V59() V63() ) set ) , REAL : ( ( ) ( non zero V46() V57() V58() V59() V63() ) set ) ) ) Element of K19(K20(REAL : ( ( ) ( non zero V46() V57() V58() V59() V63() ) set ) ,REAL : ( ( ) ( non zero V46() V57() V58() V59() V63() ) set ) ) : ( ( ) ( ) set ) ) : ( ( ) ( ) set ) ) . x : ( ( ) ( complex V29() V30() ) Element of REAL : ( ( ) ( non zero V46() V57() V58() V59() V63() ) set ) ) ) : ( ( ) ( complex V29() V30() ) Element of REAL : ( ( ) ( non zero V46() V57() V58() V59() V63() ) set ) ) * (sinh : ( ( V6() V18( REAL : ( ( ) ( non zero V46() V57() V58() V59() V63() ) set ) , REAL : ( ( ) ( non zero V46() V57() V58() V59() V63() ) set ) ) ) ( V1() V4( REAL : ( ( ) ( non zero V46() V57() V58() V59() V63() ) set ) ) V5( REAL : ( ( ) ( non zero V46() V57() V58() V59() V63() ) set ) ) V6() non zero total V18( REAL : ( ( ) ( non zero V46() V57() V58() V59() V63() ) set ) , REAL : ( ( ) ( non zero V46() V57() V58() V59() V63() ) set ) ) ) Element of K19(K20(REAL : ( ( ) ( non zero V46() V57() V58() V59() V63() ) set ) ,REAL : ( ( ) ( non zero V46() V57() V58() V59() V63() ) set ) ) : ( ( ) ( ) set ) ) : ( ( ) ( ) set ) ) . y : ( ( ) ( complex V29() V30() ) Element of REAL : ( ( ) ( non zero V46() V57() V58() V59() V63() ) set ) ) ) : ( ( ) ( complex V29() V30() ) Element of REAL : ( ( ) ( non zero V46() V57() V58() V59() V63() ) set ) ) ) : ( ( ) ( complex V29() V30() ) Element of REAL : ( ( ) ( non zero V46() V57() V58() V59() V63() ) set ) ) * : ( ( ) ( complex ) Element of COMPLEX : ( ( ) ( non zero V46() V57() V63() ) set ) ) ) : ( ( ) ( complex ) Element of COMPLEX : ( ( ) ( non zero V46() V57() V63() ) set ) ) : ( ( ) ( complex ) Element of COMPLEX : ( ( ) ( non zero V46() V57() V63() ) set ) ) ;

theorem :: SIN_COS3:43

for x, y being ( ( ) ( complex V29() V30() ) Element of REAL : ( ( ) ( non zero V46() V57() V58() V59() V63() ) set ) ) holds sin_C : ( ( V6() V18( COMPLEX : ( ( ) ( non zero V46() V57() V63() ) set ) , COMPLEX : ( ( ) ( non zero V46() V57() V63() ) set ) ) ) ( V1() V4( COMPLEX : ( ( ) ( non zero V46() V57() V63() ) set ) ) V5( COMPLEX : ( ( ) ( non zero V46() V57() V63() ) set ) ) V6() non zero total V18( COMPLEX : ( ( ) ( non zero V46() V57() V63() ) set ) , COMPLEX : ( ( ) ( non zero V46() V57() V63() ) set ) ) ) Function of COMPLEX : ( ( ) ( non zero V46() V57() V63() ) set ) , COMPLEX : ( ( ) ( non zero V46() V57() V63() ) set ) ) /. (x : ( ( ) ( complex V29() V30() ) Element of REAL : ( ( ) ( non zero V46() V57() V58() V59() V63() ) set ) ) + ((- y : ( ( ) ( complex V29() V30() ) Element of REAL : ( ( ) ( non zero V46() V57() V58() V59() V63() ) set ) ) ) : ( ( ) ( complex V29() V30() ) Element of REAL : ( ( ) ( non zero V46() V57() V58() V59() V63() ) set ) ) * : ( ( ) ( complex ) Element of COMPLEX : ( ( ) ( non zero V46() V57() V63() ) set ) ) ) : ( ( ) ( complex ) Element of COMPLEX : ( ( ) ( non zero V46() V57() V63() ) set ) ) ) : ( ( ) ( complex ) Element of COMPLEX : ( ( ) ( non zero V46() V57() V63() ) set ) ) : ( ( ) ( complex ) Element of COMPLEX : ( ( ) ( non zero V46() V57() V63() ) set ) ) = ((sin : ( ( V6() V18( REAL : ( ( ) ( non zero V46() V57() V58() V59() V63() ) set ) , REAL : ( ( ) ( non zero V46() V57() V58() V59() V63() ) set ) ) ) ( V1() V4( REAL : ( ( ) ( non zero V46() V57() V58() V59() V63() ) set ) ) V5( REAL : ( ( ) ( non zero V46() V57() V58() V59() V63() ) set ) ) V6() non zero total V18( REAL : ( ( ) ( non zero V46() V57() V58() V59() V63() ) set ) , REAL : ( ( ) ( non zero V46() V57() V58() V59() V63() ) set ) ) ) Element of K19(K20(REAL : ( ( ) ( non zero V46() V57() V58() V59() V63() ) set ) ,REAL : ( ( ) ( non zero V46() V57() V58() V59() V63() ) set ) ) : ( ( ) ( ) set ) ) : ( ( ) ( ) set ) ) . x : ( ( ) ( complex V29() V30() ) Element of REAL : ( ( ) ( non zero V46() V57() V58() V59() V63() ) set ) ) ) : ( ( ) ( complex V29() V30() ) Element of REAL : ( ( ) ( non zero V46() V57() V58() V59() V63() ) set ) ) * (cosh : ( ( V6() V18( REAL : ( ( ) ( non zero V46() V57() V58() V59() V63() ) set ) , REAL : ( ( ) ( non zero V46() V57() V58() V59() V63() ) set ) ) ) ( V1() V4( REAL : ( ( ) ( non zero V46() V57() V58() V59() V63() ) set ) ) V5( REAL : ( ( ) ( non zero V46() V57() V58() V59() V63() ) set ) ) V6() non zero total V18( REAL : ( ( ) ( non zero V46() V57() V58() V59() V63() ) set ) , REAL : ( ( ) ( non zero V46() V57() V58() V59() V63() ) set ) ) ) Element of K19(K20(REAL : ( ( ) ( non zero V46() V57() V58() V59() V63() ) set ) ,REAL : ( ( ) ( non zero V46() V57() V58() V59() V63() ) set ) ) : ( ( ) ( ) set ) ) : ( ( ) ( ) set ) ) . y : ( ( ) ( complex V29() V30() ) Element of REAL : ( ( ) ( non zero V46() V57() V58() V59() V63() ) set ) ) ) : ( ( ) ( complex V29() V30() ) Element of REAL : ( ( ) ( non zero V46() V57() V58() V59() V63() ) set ) ) ) : ( ( ) ( complex V29() V30() ) Element of REAL : ( ( ) ( non zero V46() V57() V58() V59() V63() ) set ) ) + ((- ((cos : ( ( V6() V18( REAL : ( ( ) ( non zero V46() V57() V58() V59() V63() ) set ) , REAL : ( ( ) ( non zero V46() V57() V58() V59() V63() ) set ) ) ) ( V1() V4( REAL : ( ( ) ( non zero V46() V57() V58() V59() V63() ) set ) ) V5( REAL : ( ( ) ( non zero V46() V57() V58() V59() V63() ) set ) ) V6() non zero total V18( REAL : ( ( ) ( non zero V46() V57() V58() V59() V63() ) set ) , REAL : ( ( ) ( non zero V46() V57() V58() V59() V63() ) set ) ) ) Element of K19(K20(REAL : ( ( ) ( non zero V46() V57() V58() V59() V63() ) set ) ,REAL : ( ( ) ( non zero V46() V57() V58() V59() V63() ) set ) ) : ( ( ) ( ) set ) ) : ( ( ) ( ) set ) ) . x : ( ( ) ( complex V29() V30() ) Element of REAL : ( ( ) ( non zero V46() V57() V58() V59() V63() ) set ) ) ) : ( ( ) ( complex V29() V30() ) Element of REAL : ( ( ) ( non zero V46() V57() V58() V59() V63() ) set ) ) * (sinh : ( ( V6() V18( REAL : ( ( ) ( non zero V46() V57() V58() V59() V63() ) set ) , REAL : ( ( ) ( non zero V46() V57() V58() V59() V63() ) set ) ) ) ( V1() V4( REAL : ( ( ) ( non zero V46() V57() V58() V59() V63() ) set ) ) V5( REAL : ( ( ) ( non zero V46() V57() V58() V59() V63() ) set ) ) V6() non zero total V18( REAL : ( ( ) ( non zero V46() V57() V58() V59() V63() ) set ) , REAL : ( ( ) ( non zero V46() V57() V58() V59() V63() ) set ) ) ) Element of K19(K20(REAL : ( ( ) ( non zero V46() V57() V58() V59() V63() ) set ) ,REAL : ( ( ) ( non zero V46() V57() V58() V59() V63() ) set ) ) : ( ( ) ( ) set ) ) : ( ( ) ( ) set ) ) . y : ( ( ) ( complex V29() V30() ) Element of REAL : ( ( ) ( non zero V46() V57() V58() V59() V63() ) set ) ) ) : ( ( ) ( complex V29() V30() ) Element of REAL : ( ( ) ( non zero V46() V57() V58() V59() V63() ) set ) ) ) : ( ( ) ( complex V29() V30() ) Element of REAL : ( ( ) ( non zero V46() V57() V58() V59() V63() ) set ) ) ) : ( ( ) ( complex V29() V30() ) Element of REAL : ( ( ) ( non zero V46() V57() V58() V59() V63() ) set ) ) * : ( ( ) ( complex ) Element of COMPLEX : ( ( ) ( non zero V46() V57() V63() ) set ) ) ) : ( ( ) ( complex ) Element of COMPLEX : ( ( ) ( non zero V46() V57() V63() ) set ) ) : ( ( ) ( complex ) Element of COMPLEX : ( ( ) ( non zero V46() V57() V63() ) set ) ) ;

theorem :: SIN_COS3:44

for x, y being ( ( ) ( complex V29() V30() ) Element of REAL : ( ( ) ( non zero V46() V57() V58() V59() V63() ) set ) ) holds cos_C : ( ( V6() V18( COMPLEX : ( ( ) ( non zero V46() V57() V63() ) set ) , COMPLEX : ( ( ) ( non zero V46() V57() V63() ) set ) ) ) ( V1() V4( COMPLEX : ( ( ) ( non zero V46() V57() V63() ) set ) ) V5( COMPLEX : ( ( ) ( non zero V46() V57() V63() ) set ) ) V6() non zero total V18( COMPLEX : ( ( ) ( non zero V46() V57() V63() ) set ) , COMPLEX : ( ( ) ( non zero V46() V57() V63() ) set ) ) ) Function of COMPLEX : ( ( ) ( non zero V46() V57() V63() ) set ) , COMPLEX : ( ( ) ( non zero V46() V57() V63() ) set ) ) /. (x : ( ( ) ( complex V29() V30() ) Element of REAL : ( ( ) ( non zero V46() V57() V58() V59() V63() ) set ) ) + (y : ( ( ) ( complex V29() V30() ) Element of REAL : ( ( ) ( non zero V46() V57() V58() V59() V63() ) set ) ) * : ( ( ) ( complex ) Element of COMPLEX : ( ( ) ( non zero V46() V57() V63() ) set ) ) ) : ( ( ) ( complex ) Element of COMPLEX : ( ( ) ( non zero V46() V57() V63() ) set ) ) ) : ( ( ) ( complex ) Element of COMPLEX : ( ( ) ( non zero V46() V57() V63() ) set ) ) : ( ( ) ( complex ) Element of COMPLEX : ( ( ) ( non zero V46() V57() V63() ) set ) ) = ((cos : ( ( V6() V18( REAL : ( ( ) ( non zero V46() V57() V58() V59() V63() ) set ) , REAL : ( ( ) ( non zero V46() V57() V58() V59() V63() ) set ) ) ) ( V1() V4( REAL : ( ( ) ( non zero V46() V57() V58() V59() V63() ) set ) ) V5( REAL : ( ( ) ( non zero V46() V57() V58() V59() V63() ) set ) ) V6() non zero total V18( REAL : ( ( ) ( non zero V46() V57() V58() V59() V63() ) set ) , REAL : ( ( ) ( non zero V46() V57() V58() V59() V63() ) set ) ) ) Element of K19(K20(REAL : ( ( ) ( non zero V46() V57() V58() V59() V63() ) set ) ,REAL : ( ( ) ( non zero V46() V57() V58() V59() V63() ) set ) ) : ( ( ) ( ) set ) ) : ( ( ) ( ) set ) ) . x : ( ( ) ( complex V29() V30() ) Element of REAL : ( ( ) ( non zero V46() V57() V58() V59() V63() ) set ) ) ) : ( ( ) ( complex V29() V30() ) Element of REAL : ( ( ) ( non zero V46() V57() V58() V59() V63() ) set ) ) * (cosh : ( ( V6() V18( REAL : ( ( ) ( non zero V46() V57() V58() V59() V63() ) set ) , REAL : ( ( ) ( non zero V46() V57() V58() V59() V63() ) set ) ) ) ( V1() V4( REAL : ( ( ) ( non zero V46() V57() V58() V59() V63() ) set ) ) V5( REAL : ( ( ) ( non zero V46() V57() V58() V59() V63() ) set ) ) V6() non zero total V18( REAL : ( ( ) ( non zero V46() V57() V58() V59() V63() ) set ) , REAL : ( ( ) ( non zero V46() V57() V58() V59() V63() ) set ) ) ) Element of K19(K20(REAL : ( ( ) ( non zero V46() V57() V58() V59() V63() ) set ) ,REAL : ( ( ) ( non zero V46() V57() V58() V59() V63() ) set ) ) : ( ( ) ( ) set ) ) : ( ( ) ( ) set ) ) . y : ( ( ) ( complex V29() V30() ) Element of REAL : ( ( ) ( non zero V46() V57() V58() V59() V63() ) set ) ) ) : ( ( ) ( complex V29() V30() ) Element of REAL : ( ( ) ( non zero V46() V57() V58() V59() V63() ) set ) ) ) : ( ( ) ( complex V29() V30() ) Element of REAL : ( ( ) ( non zero V46() V57() V58() V59() V63() ) set ) ) + ((- ((sin : ( ( V6() V18( REAL : ( ( ) ( non zero V46() V57() V58() V59() V63() ) set ) , REAL : ( ( ) ( non zero V46() V57() V58() V59() V63() ) set ) ) ) ( V1() V4( REAL : ( ( ) ( non zero V46() V57() V58() V59() V63() ) set ) ) V5( REAL : ( ( ) ( non zero V46() V57() V58() V59() V63() ) set ) ) V6() non zero total V18( REAL : ( ( ) ( non zero V46() V57() V58() V59() V63() ) set ) , REAL : ( ( ) ( non zero V46() V57() V58() V59() V63() ) set ) ) ) Element of K19(K20(REAL : ( ( ) ( non zero V46() V57() V58() V59() V63() ) set ) ,REAL : ( ( ) ( non zero V46() V57() V58() V59() V63() ) set ) ) : ( ( ) ( ) set ) ) : ( ( ) ( ) set ) ) . x : ( ( ) ( complex V29() V30() ) Element of REAL : ( ( ) ( non zero V46() V57() V58() V59() V63() ) set ) ) ) : ( ( ) ( complex V29() V30() ) Element of REAL : ( ( ) ( non zero V46() V57() V58() V59() V63() ) set ) ) * (sinh : ( ( V6() V18( REAL : ( ( ) ( non zero V46() V57() V58() V59() V63() ) set ) , REAL : ( ( ) ( non zero V46() V57() V58() V59() V63() ) set ) ) ) ( V1() V4( REAL : ( ( ) ( non zero V46() V57() V58() V59() V63() ) set ) ) V5( REAL : ( ( ) ( non zero V46() V57() V58() V59() V63() ) set ) ) V6() non zero total V18( REAL : ( ( ) ( non zero V46() V57() V58() V59() V63() ) set ) , REAL : ( ( ) ( non zero V46() V57() V58() V59() V63() ) set ) ) ) Element of K19(K20(REAL : ( ( ) ( non zero V46() V57() V58() V59() V63() ) set ) ,REAL : ( ( ) ( non zero V46() V57() V58() V59() V63() ) set ) ) : ( ( ) ( ) set ) ) : ( ( ) ( ) set ) ) . y : ( ( ) ( complex V29() V30() ) Element of REAL : ( ( ) ( non zero V46() V57() V58() V59() V63() ) set ) ) ) : ( ( ) ( complex V29() V30() ) Element of REAL : ( ( ) ( non zero V46() V57() V58() V59() V63() ) set ) ) ) : ( ( ) ( complex V29() V30() ) Element of REAL : ( ( ) ( non zero V46() V57() V58() V59() V63() ) set ) ) ) : ( ( ) ( complex V29() V30() ) Element of REAL : ( ( ) ( non zero V46() V57() V58() V59() V63() ) set ) ) * : ( ( ) ( complex ) Element of COMPLEX : ( ( ) ( non zero V46() V57() V63() ) set ) ) ) : ( ( ) ( complex ) Element of COMPLEX : ( ( ) ( non zero V46() V57() V63() ) set ) ) : ( ( ) ( complex ) Element of COMPLEX : ( ( ) ( non zero V46() V57() V63() ) set ) ) ;

theorem :: SIN_COS3:45

for x, y being ( ( ) ( complex V29() V30() ) Element of REAL : ( ( ) ( non zero V46() V57() V58() V59() V63() ) set ) ) holds cos_C : ( ( V6() V18( COMPLEX : ( ( ) ( non zero V46() V57() V63() ) set ) , COMPLEX : ( ( ) ( non zero V46() V57() V63() ) set ) ) ) ( V1() V4( COMPLEX : ( ( ) ( non zero V46() V57() V63() ) set ) ) V5( COMPLEX : ( ( ) ( non zero V46() V57() V63() ) set ) ) V6() non zero total V18( COMPLEX : ( ( ) ( non zero V46() V57() V63() ) set ) , COMPLEX : ( ( ) ( non zero V46() V57() V63() ) set ) ) ) Function of COMPLEX : ( ( ) ( non zero V46() V57() V63() ) set ) , COMPLEX : ( ( ) ( non zero V46() V57() V63() ) set ) ) /. (x : ( ( ) ( complex V29() V30() ) Element of REAL : ( ( ) ( non zero V46() V57() V58() V59() V63() ) set ) ) + ((- y : ( ( ) ( complex V29() V30() ) Element of REAL : ( ( ) ( non zero V46() V57() V58() V59() V63() ) set ) ) ) : ( ( ) ( complex V29() V30() ) Element of REAL : ( ( ) ( non zero V46() V57() V58() V59() V63() ) set ) ) * : ( ( ) ( complex ) Element of COMPLEX : ( ( ) ( non zero V46() V57() V63() ) set ) ) ) : ( ( ) ( complex ) Element of COMPLEX : ( ( ) ( non zero V46() V57() V63() ) set ) ) ) : ( ( ) ( complex ) Element of COMPLEX : ( ( ) ( non zero V46() V57() V63() ) set ) ) : ( ( ) ( complex ) Element of COMPLEX : ( ( ) ( non zero V46() V57() V63() ) set ) ) = ((cos : ( ( V6() V18( REAL : ( ( ) ( non zero V46() V57() V58() V59() V63() ) set ) , REAL : ( ( ) ( non zero V46() V57() V58() V59() V63() ) set ) ) ) ( V1() V4( REAL : ( ( ) ( non zero V46() V57() V58() V59() V63() ) set ) ) V5( REAL : ( ( ) ( non zero V46() V57() V58() V59() V63() ) set ) ) V6() non zero total V18( REAL : ( ( ) ( non zero V46() V57() V58() V59() V63() ) set ) , REAL : ( ( ) ( non zero V46() V57() V58() V59() V63() ) set ) ) ) Element of K19(K20(REAL : ( ( ) ( non zero V46() V57() V58() V59() V63() ) set ) ,REAL : ( ( ) ( non zero V46() V57() V58() V59() V63() ) set ) ) : ( ( ) ( ) set ) ) : ( ( ) ( ) set ) ) . x : ( ( ) ( complex V29() V30() ) Element of REAL : ( ( ) ( non zero V46() V57() V58() V59() V63() ) set ) ) ) : ( ( ) ( complex V29() V30() ) Element of REAL : ( ( ) ( non zero V46() V57() V58() V59() V63() ) set ) ) * (cosh : ( ( V6() V18( REAL : ( ( ) ( non zero V46() V57() V58() V59() V63() ) set ) , REAL : ( ( ) ( non zero V46() V57() V58() V59() V63() ) set ) ) ) ( V1() V4( REAL : ( ( ) ( non zero V46() V57() V58() V59() V63() ) set ) ) V5( REAL : ( ( ) ( non zero V46() V57() V58() V59() V63() ) set ) ) V6() non zero total V18( REAL : ( ( ) ( non zero V46() V57() V58() V59() V63() ) set ) , REAL : ( ( ) ( non zero V46() V57() V58() V59() V63() ) set ) ) ) Element of K19(K20(REAL : ( ( ) ( non zero V46() V57() V58() V59() V63() ) set ) ,REAL : ( ( ) ( non zero V46() V57() V58() V59() V63() ) set ) ) : ( ( ) ( ) set ) ) : ( ( ) ( ) set ) ) . y : ( ( ) ( complex V29() V30() ) Element of REAL : ( ( ) ( non zero V46() V57() V58() V59() V63() ) set ) ) ) : ( ( ) ( complex V29() V30() ) Element of REAL : ( ( ) ( non zero V46() V57() V58() V59() V63() ) set ) ) ) : ( ( ) ( complex V29() V30() ) Element of REAL : ( ( ) ( non zero V46() V57() V58() V59() V63() ) set ) ) + (((sin : ( ( V6() V18( REAL : ( ( ) ( non zero V46() V57() V58() V59() V63() ) set ) , REAL : ( ( ) ( non zero V46() V57() V58() V59() V63() ) set ) ) ) ( V1() V4( REAL : ( ( ) ( non zero V46() V57() V58() V59() V63() ) set ) ) V5( REAL : ( ( ) ( non zero V46() V57() V58() V59() V63() ) set ) ) V6() non zero total V18( REAL : ( ( ) ( non zero V46() V57() V58() V59() V63() ) set ) , REAL : ( ( ) ( non zero V46() V57() V58() V59() V63() ) set ) ) ) Element of K19(K20(REAL : ( ( ) ( non zero V46() V57() V58() V59() V63() ) set ) ,REAL : ( ( ) ( non zero V46() V57() V58() V59() V63() ) set ) ) : ( ( ) ( ) set ) ) : ( ( ) ( ) set ) ) . x : ( ( ) ( complex V29() V30() ) Element of REAL : ( ( ) ( non zero V46() V57() V58() V59() V63() ) set ) ) ) : ( ( ) ( complex V29() V30() ) Element of REAL : ( ( ) ( non zero V46() V57() V58() V59() V63() ) set ) ) * (sinh : ( ( V6() V18( REAL : ( ( ) ( non zero V46() V57() V58() V59() V63() ) set ) , REAL : ( ( ) ( non zero V46() V57() V58() V59() V63() ) set ) ) ) ( V1() V4( REAL : ( ( ) ( non zero V46() V57() V58() V59() V63() ) set ) ) V5( REAL : ( ( ) ( non zero V46() V57() V58() V59() V63() ) set ) ) V6() non zero total V18( REAL : ( ( ) ( non zero V46() V57() V58() V59() V63() ) set ) , REAL : ( ( ) ( non zero V46() V57() V58() V59() V63() ) set ) ) ) Element of K19(K20(REAL : ( ( ) ( non zero V46() V57() V58() V59() V63() ) set ) ,REAL : ( ( ) ( non zero V46() V57() V58() V59() V63() ) set ) ) : ( ( ) ( ) set ) ) : ( ( ) ( ) set ) ) . y : ( ( ) ( complex V29() V30() ) Element of REAL : ( ( ) ( non zero V46() V57() V58() V59() V63() ) set ) ) ) : ( ( ) ( complex V29() V30() ) Element of REAL : ( ( ) ( non zero V46() V57() V58() V59() V63() ) set ) ) ) : ( ( ) ( complex V29() V30() ) Element of REAL : ( ( ) ( non zero V46() V57() V58() V59() V63() ) set ) ) * : ( ( ) ( complex ) Element of COMPLEX : ( ( ) ( non zero V46() V57() V63() ) set ) ) ) : ( ( ) ( complex ) Element of COMPLEX : ( ( ) ( non zero V46() V57() V63() ) set ) ) : ( ( ) ( complex ) Element of COMPLEX : ( ( ) ( non zero V46() V57() V63() ) set ) ) ;

theorem :: SIN_COS3:46

for x, y being ( ( ) ( complex V29() V30() ) Element of REAL : ( ( ) ( non zero V46() V57() V58() V59() V63() ) set ) ) holds sinh_C : ( ( V6() V18( COMPLEX : ( ( ) ( non zero V46() V57() V63() ) set ) , COMPLEX : ( ( ) ( non zero V46() V57() V63() ) set ) ) ) ( V1() V4( COMPLEX : ( ( ) ( non zero V46() V57() V63() ) set ) ) V5( COMPLEX : ( ( ) ( non zero V46() V57() V63() ) set ) ) V6() non zero total V18( COMPLEX : ( ( ) ( non zero V46() V57() V63() ) set ) , COMPLEX : ( ( ) ( non zero V46() V57() V63() ) set ) ) ) Function of COMPLEX : ( ( ) ( non zero V46() V57() V63() ) set ) , COMPLEX : ( ( ) ( non zero V46() V57() V63() ) set ) ) /. (x : ( ( ) ( complex V29() V30() ) Element of REAL : ( ( ) ( non zero V46() V57() V58() V59() V63() ) set ) ) + (y : ( ( ) ( complex V29() V30() ) Element of REAL : ( ( ) ( non zero V46() V57() V58() V59() V63() ) set ) ) * : ( ( ) ( complex ) Element of COMPLEX : ( ( ) ( non zero V46() V57() V63() ) set ) ) ) : ( ( ) ( complex ) Element of COMPLEX : ( ( ) ( non zero V46() V57() V63() ) set ) ) ) : ( ( ) ( complex ) Element of COMPLEX : ( ( ) ( non zero V46() V57() V63() ) set ) ) : ( ( ) ( complex ) Element of COMPLEX : ( ( ) ( non zero V46() V57() V63() ) set ) ) = ((sinh : ( ( V6() V18( REAL : ( ( ) ( non zero V46() V57() V58() V59() V63() ) set ) , REAL : ( ( ) ( non zero V46() V57() V58() V59() V63() ) set ) ) ) ( V1() V4( REAL : ( ( ) ( non zero V46() V57() V58() V59() V63() ) set ) ) V5( REAL : ( ( ) ( non zero V46() V57() V58() V59() V63() ) set ) ) V6() non zero total V18( REAL : ( ( ) ( non zero V46() V57() V58() V59() V63() ) set ) , REAL : ( ( ) ( non zero V46() V57() V58() V59() V63() ) set ) ) ) Element of K19(K20(REAL : ( ( ) ( non zero V46() V57() V58() V59() V63() ) set ) ,REAL : ( ( ) ( non zero V46() V57() V58() V59() V63() ) set ) ) : ( ( ) ( ) set ) ) : ( ( ) ( ) set ) ) . x : ( ( ) ( complex V29() V30() ) Element of REAL : ( ( ) ( non zero V46() V57() V58() V59() V63() ) set ) ) ) : ( ( ) ( complex V29() V30() ) Element of REAL : ( ( ) ( non zero V46() V57() V58() V59() V63() ) set ) ) * (cos : ( ( V6() V18( REAL : ( ( ) ( non zero V46() V57() V58() V59() V63() ) set ) , REAL : ( ( ) ( non zero V46() V57() V58() V59() V63() ) set ) ) ) ( V1() V4( REAL : ( ( ) ( non zero V46() V57() V58() V59() V63() ) set ) ) V5( REAL : ( ( ) ( non zero V46() V57() V58() V59() V63() ) set ) ) V6() non zero total V18( REAL : ( ( ) ( non zero V46() V57() V58() V59() V63() ) set ) , REAL : ( ( ) ( non zero V46() V57() V58() V59() V63() ) set ) ) ) Element of K19(K20(REAL : ( ( ) ( non zero V46() V57() V58() V59() V63() ) set ) ,REAL : ( ( ) ( non zero V46() V57() V58() V59() V63() ) set ) ) : ( ( ) ( ) set ) ) : ( ( ) ( ) set ) ) . y : ( ( ) ( complex V29() V30() ) Element of REAL : ( ( ) ( non zero V46() V57() V58() V59() V63() ) set ) ) ) : ( ( ) ( complex V29() V30() ) Element of REAL : ( ( ) ( non zero V46() V57() V58() V59() V63() ) set ) ) ) : ( ( ) ( complex V29() V30() ) Element of REAL : ( ( ) ( non zero V46() V57() V58() V59() V63() ) set ) ) + (((cosh : ( ( V6() V18( REAL : ( ( ) ( non zero V46() V57() V58() V59() V63() ) set ) , REAL : ( ( ) ( non zero V46() V57() V58() V59() V63() ) set ) ) ) ( V1() V4( REAL : ( ( ) ( non zero V46() V57() V58() V59() V63() ) set ) ) V5( REAL : ( ( ) ( non zero V46() V57() V58() V59() V63() ) set ) ) V6() non zero total V18( REAL : ( ( ) ( non zero V46() V57() V58() V59() V63() ) set ) , REAL : ( ( ) ( non zero V46() V57() V58() V59() V63() ) set ) ) ) Element of K19(K20(REAL : ( ( ) ( non zero V46() V57() V58() V59() V63() ) set ) ,REAL : ( ( ) ( non zero V46() V57() V58() V59() V63() ) set ) ) : ( ( ) ( ) set ) ) : ( ( ) ( ) set ) ) . x : ( ( ) ( complex V29() V30() ) Element of REAL : ( ( ) ( non zero V46() V57() V58() V59() V63() ) set ) ) ) : ( ( ) ( complex V29() V30() ) Element of REAL : ( ( ) ( non zero V46() V57() V58() V59() V63() ) set ) ) * (sin : ( ( V6() V18( REAL : ( ( ) ( non zero V46() V57() V58() V59() V63() ) set ) , REAL : ( ( ) ( non zero V46() V57() V58() V59() V63() ) set ) ) ) ( V1() V4( REAL : ( ( ) ( non zero V46() V57() V58() V59() V63() ) set ) ) V5( REAL : ( ( ) ( non zero V46() V57() V58() V59() V63() ) set ) ) V6() non zero total V18( REAL : ( ( ) ( non zero V46() V57() V58() V59() V63() ) set ) , REAL : ( ( ) ( non zero V46() V57() V58() V59() V63() ) set ) ) ) Element of K19(K20(REAL : ( ( ) ( non zero V46() V57() V58() V59() V63() ) set ) ,REAL : ( ( ) ( non zero V46() V57() V58() V59() V63() ) set ) ) : ( ( ) ( ) set ) ) : ( ( ) ( ) set ) ) . y : ( ( ) ( complex V29() V30() ) Element of REAL : ( ( ) ( non zero V46() V57() V58() V59() V63() ) set ) ) ) : ( ( ) ( complex V29() V30() ) Element of REAL : ( ( ) ( non zero V46() V57() V58() V59() V63() ) set ) ) ) : ( ( ) ( complex V29() V30() ) Element of REAL : ( ( ) ( non zero V46() V57() V58() V59() V63() ) set ) ) * : ( ( ) ( complex ) Element of COMPLEX : ( ( ) ( non zero V46() V57() V63() ) set ) ) ) : ( ( ) ( complex ) Element of COMPLEX : ( ( ) ( non zero V46() V57() V63() ) set ) ) : ( ( ) ( complex ) Element of COMPLEX : ( ( ) ( non zero V46() V57() V63() ) set ) ) ;

theorem :: SIN_COS3:47

for x, y being ( ( ) ( complex V29() V30() ) Element of REAL : ( ( ) ( non zero V46() V57() V58() V59() V63() ) set ) ) holds sinh_C : ( ( V6() V18( COMPLEX : ( ( ) ( non zero V46() V57() V63() ) set ) , COMPLEX : ( ( ) ( non zero V46() V57() V63() ) set ) ) ) ( V1() V4( COMPLEX : ( ( ) ( non zero V46() V57() V63() ) set ) ) V5( COMPLEX : ( ( ) ( non zero V46() V57() V63() ) set ) ) V6() non zero total V18( COMPLEX : ( ( ) ( non zero V46() V57() V63() ) set ) , COMPLEX : ( ( ) ( non zero V46() V57() V63() ) set ) ) ) Function of COMPLEX : ( ( ) ( non zero V46() V57() V63() ) set ) , COMPLEX : ( ( ) ( non zero V46() V57() V63() ) set ) ) /. (x : ( ( ) ( complex V29() V30() ) Element of REAL : ( ( ) ( non zero V46() V57() V58() V59() V63() ) set ) ) + ((- y : ( ( ) ( complex V29() V30() ) Element of REAL : ( ( ) ( non zero V46() V57() V58() V59() V63() ) set ) ) ) : ( ( ) ( complex V29() V30() ) Element of REAL : ( ( ) ( non zero V46() V57() V58() V59() V63() ) set ) ) * : ( ( ) ( complex ) Element of COMPLEX : ( ( ) ( non zero V46() V57() V63() ) set ) ) ) : ( ( ) ( complex ) Element of COMPLEX : ( ( ) ( non zero V46() V57() V63() ) set ) ) ) : ( ( ) ( complex ) Element of COMPLEX : ( ( ) ( non zero V46() V57() V63() ) set ) ) : ( ( ) ( complex ) Element of COMPLEX : ( ( ) ( non zero V46() V57() V63() ) set ) ) = ((sinh : ( ( V6() V18( REAL : ( ( ) ( non zero V46() V57() V58() V59() V63() ) set ) , REAL : ( ( ) ( non zero V46() V57() V58() V59() V63() ) set ) ) ) ( V1() V4( REAL : ( ( ) ( non zero V46() V57() V58() V59() V63() ) set ) ) V5( REAL : ( ( ) ( non zero V46() V57() V58() V59() V63() ) set ) ) V6() non zero total V18( REAL : ( ( ) ( non zero V46() V57() V58() V59() V63() ) set ) , REAL : ( ( ) ( non zero V46() V57() V58() V59() V63() ) set ) ) ) Element of K19(K20(REAL : ( ( ) ( non zero V46() V57() V58() V59() V63() ) set ) ,REAL : ( ( ) ( non zero V46() V57() V58() V59() V63() ) set ) ) : ( ( ) ( ) set ) ) : ( ( ) ( ) set ) ) . x : ( ( ) ( complex V29() V30() ) Element of REAL : ( ( ) ( non zero V46() V57() V58() V59() V63() ) set ) ) ) : ( ( ) ( complex V29() V30() ) Element of REAL : ( ( ) ( non zero V46() V57() V58() V59() V63() ) set ) ) * (cos : ( ( V6() V18( REAL : ( ( ) ( non zero V46() V57() V58() V59() V63() ) set ) , REAL : ( ( ) ( non zero V46() V57() V58() V59() V63() ) set ) ) ) ( V1() V4( REAL : ( ( ) ( non zero V46() V57() V58() V59() V63() ) set ) ) V5( REAL : ( ( ) ( non zero V46() V57() V58() V59() V63() ) set ) ) V6() non zero total V18( REAL : ( ( ) ( non zero V46() V57() V58() V59() V63() ) set ) , REAL : ( ( ) ( non zero V46() V57() V58() V59() V63() ) set ) ) ) Element of K19(K20(REAL : ( ( ) ( non zero V46() V57() V58() V59() V63() ) set ) ,REAL : ( ( ) ( non zero V46() V57() V58() V59() V63() ) set ) ) : ( ( ) ( ) set ) ) : ( ( ) ( ) set ) ) . y : ( ( ) ( complex V29() V30() ) Element of REAL : ( ( ) ( non zero V46() V57() V58() V59() V63() ) set ) ) ) : ( ( ) ( complex V29() V30() ) Element of REAL : ( ( ) ( non zero V46() V57() V58() V59() V63() ) set ) ) ) : ( ( ) ( complex V29() V30() ) Element of REAL : ( ( ) ( non zero V46() V57() V58() V59() V63() ) set ) ) + ((- ((cosh : ( ( V6() V18( REAL : ( ( ) ( non zero V46() V57() V58() V59() V63() ) set ) , REAL : ( ( ) ( non zero V46() V57() V58() V59() V63() ) set ) ) ) ( V1() V4( REAL : ( ( ) ( non zero V46() V57() V58() V59() V63() ) set ) ) V5( REAL : ( ( ) ( non zero V46() V57() V58() V59() V63() ) set ) ) V6() non zero total V18( REAL : ( ( ) ( non zero V46() V57() V58() V59() V63() ) set ) , REAL : ( ( ) ( non zero V46() V57() V58() V59() V63() ) set ) ) ) Element of K19(K20(REAL : ( ( ) ( non zero V46() V57() V58() V59() V63() ) set ) ,REAL : ( ( ) ( non zero V46() V57() V58() V59() V63() ) set ) ) : ( ( ) ( ) set ) ) : ( ( ) ( ) set ) ) . x : ( ( ) ( complex V29() V30() ) Element of REAL : ( ( ) ( non zero V46() V57() V58() V59() V63() ) set ) ) ) : ( ( ) ( complex V29() V30() ) Element of REAL : ( ( ) ( non zero V46() V57() V58() V59() V63() ) set ) ) * (sin : ( ( V6() V18( REAL : ( ( ) ( non zero V46() V57() V58() V59() V63() ) set ) , REAL : ( ( ) ( non zero V46() V57() V58() V59() V63() ) set ) ) ) ( V1() V4( REAL : ( ( ) ( non zero V46() V57() V58() V59() V63() ) set ) ) V5( REAL : ( ( ) ( non zero V46() V57() V58() V59() V63() ) set ) ) V6() non zero total V18( REAL : ( ( ) ( non zero V46() V57() V58() V59() V63() ) set ) , REAL : ( ( ) ( non zero V46() V57() V58() V59() V63() ) set ) ) ) Element of K19(K20(REAL : ( ( ) ( non zero V46() V57() V58() V59() V63() ) set ) ,REAL : ( ( ) ( non zero V46() V57() V58() V59() V63() ) set ) ) : ( ( ) ( ) set ) ) : ( ( ) ( ) set ) ) . y : ( ( ) ( complex V29() V30() ) Element of REAL : ( ( ) ( non zero V46() V57() V58() V59() V63() ) set ) ) ) : ( ( ) ( complex V29() V30() ) Element of REAL : ( ( ) ( non zero V46() V57() V58() V59() V63() ) set ) ) ) : ( ( ) ( complex V29() V30() ) Element of REAL : ( ( ) ( non zero V46() V57() V58() V59() V63() ) set ) ) ) : ( ( ) ( complex V29() V30() ) Element of REAL : ( ( ) ( non zero V46() V57() V58() V59() V63() ) set ) ) * : ( ( ) ( complex ) Element of COMPLEX : ( ( ) ( non zero V46() V57() V63() ) set ) ) ) : ( ( ) ( complex ) Element of COMPLEX : ( ( ) ( non zero V46() V57() V63() ) set ) ) : ( ( ) ( complex ) Element of COMPLEX : ( ( ) ( non zero V46() V57() V63() ) set ) ) ;

theorem :: SIN_COS3:48

for x, y being ( ( ) ( complex V29() V30() ) Element of REAL : ( ( ) ( non zero V46() V57() V58() V59() V63() ) set ) ) holds cosh_C : ( ( V6() V18( COMPLEX : ( ( ) ( non zero V46() V57() V63() ) set ) , COMPLEX : ( ( ) ( non zero V46() V57() V63() ) set ) ) ) ( V1() V4( COMPLEX : ( ( ) ( non zero V46() V57() V63() ) set ) ) V5( COMPLEX : ( ( ) ( non zero V46() V57() V63() ) set ) ) V6() non zero total V18( COMPLEX : ( ( ) ( non zero V46() V57() V63() ) set ) , COMPLEX : ( ( ) ( non zero V46() V57() V63() ) set ) ) ) Function of COMPLEX : ( ( ) ( non zero V46() V57() V63() ) set ) , COMPLEX : ( ( ) ( non zero V46() V57() V63() ) set ) ) /. (x : ( ( ) ( complex V29() V30() ) Element of REAL : ( ( ) ( non zero V46() V57() V58() V59() V63() ) set ) ) + (y : ( ( ) ( complex V29() V30() ) Element of REAL : ( ( ) ( non zero V46() V57() V58() V59() V63() ) set ) ) * : ( ( ) ( complex ) Element of COMPLEX : ( ( ) ( non zero V46() V57() V63() ) set ) ) ) : ( ( ) ( complex ) Element of COMPLEX : ( ( ) ( non zero V46() V57() V63() ) set ) ) ) : ( ( ) ( complex ) Element of COMPLEX : ( ( ) ( non zero V46() V57() V63() ) set ) ) : ( ( ) ( complex ) Element of COMPLEX : ( ( ) ( non zero V46() V57() V63() ) set ) ) = ((cosh : ( ( V6() V18( REAL : ( ( ) ( non zero V46() V57() V58() V59() V63() ) set ) , REAL : ( ( ) ( non zero V46() V57() V58() V59() V63() ) set ) ) ) ( V1() V4( REAL : ( ( ) ( non zero V46() V57() V58() V59() V63() ) set ) ) V5( REAL : ( ( ) ( non zero V46() V57() V58() V59() V63() ) set ) ) V6() non zero total V18( REAL : ( ( ) ( non zero V46() V57() V58() V59() V63() ) set ) , REAL : ( ( ) ( non zero V46() V57() V58() V59() V63() ) set ) ) ) Element of K19(K20(REAL : ( ( ) ( non zero V46() V57() V58() V59() V63() ) set ) ,REAL : ( ( ) ( non zero V46() V57() V58() V59() V63() ) set ) ) : ( ( ) ( ) set ) ) : ( ( ) ( ) set ) ) . x : ( ( ) ( complex V29() V30() ) Element of REAL : ( ( ) ( non zero V46() V57() V58() V59() V63() ) set ) ) ) : ( ( ) ( complex V29() V30() ) Element of REAL : ( ( ) ( non zero V46() V57() V58() V59() V63() ) set ) ) * (cos : ( ( V6() V18( REAL : ( ( ) ( non zero V46() V57() V58() V59() V63() ) set ) , REAL : ( ( ) ( non zero V46() V57() V58() V59() V63() ) set ) ) ) ( V1() V4( REAL : ( ( ) ( non zero V46() V57() V58() V59() V63() ) set ) ) V5( REAL : ( ( ) ( non zero V46() V57() V58() V59() V63() ) set ) ) V6() non zero total V18( REAL : ( ( ) ( non zero V46() V57() V58() V59() V63() ) set ) , REAL : ( ( ) ( non zero V46() V57() V58() V59() V63() ) set ) ) ) Element of K19(K20(REAL : ( ( ) ( non zero V46() V57() V58() V59() V63() ) set ) ,REAL : ( ( ) ( non zero V46() V57() V58() V59() V63() ) set ) ) : ( ( ) ( ) set ) ) : ( ( ) ( ) set ) ) . y : ( ( ) ( complex V29() V30() ) Element of REAL : ( ( ) ( non zero V46() V57() V58() V59() V63() ) set ) ) ) : ( ( ) ( complex V29() V30() ) Element of REAL : ( ( ) ( non zero V46() V57() V58() V59() V63() ) set ) ) ) : ( ( ) ( complex V29() V30() ) Element of REAL : ( ( ) ( non zero V46() V57() V58() V59() V63() ) set ) ) + (((sinh : ( ( V6() V18( REAL : ( ( ) ( non zero V46() V57() V58() V59() V63() ) set ) , REAL : ( ( ) ( non zero V46() V57() V58() V59() V63() ) set ) ) ) ( V1() V4( REAL : ( ( ) ( non zero V46() V57() V58() V59() V63() ) set ) ) V5( REAL : ( ( ) ( non zero V46() V57() V58() V59() V63() ) set ) ) V6() non zero total V18( REAL : ( ( ) ( non zero V46() V57() V58() V59() V63() ) set ) , REAL : ( ( ) ( non zero V46() V57() V58() V59() V63() ) set ) ) ) Element of K19(K20(REAL : ( ( ) ( non zero V46() V57() V58() V59() V63() ) set ) ,REAL : ( ( ) ( non zero V46() V57() V58() V59() V63() ) set ) ) : ( ( ) ( ) set ) ) : ( ( ) ( ) set ) ) . x : ( ( ) ( complex V29() V30() ) Element of REAL : ( ( ) ( non zero V46() V57() V58() V59() V63() ) set ) ) ) : ( ( ) ( complex V29() V30() ) Element of REAL : ( ( ) ( non zero V46() V57() V58() V59() V63() ) set ) ) * (sin : ( ( V6() V18( REAL : ( ( ) ( non zero V46() V57() V58() V59() V63() ) set ) , REAL : ( ( ) ( non zero V46() V57() V58() V59() V63() ) set ) ) ) ( V1() V4( REAL : ( ( ) ( non zero V46() V57() V58() V59() V63() ) set ) ) V5( REAL : ( ( ) ( non zero V46() V57() V58() V59() V63() ) set ) ) V6() non zero total V18( REAL : ( ( ) ( non zero V46() V57() V58() V59() V63() ) set ) , REAL : ( ( ) ( non zero V46() V57() V58() V59() V63() ) set ) ) ) Element of K19(K20(REAL : ( ( ) ( non zero V46() V57() V58() V59() V63() ) set ) ,REAL : ( ( ) ( non zero V46() V57() V58() V59() V63() ) set ) ) : ( ( ) ( ) set ) ) : ( ( ) ( ) set ) ) . y : ( ( ) ( complex V29() V30() ) Element of REAL : ( ( ) ( non zero V46() V57() V58() V59() V63() ) set ) ) ) : ( ( ) ( complex V29() V30() ) Element of REAL : ( ( ) ( non zero V46() V57() V58() V59() V63() ) set ) ) ) : ( ( ) ( complex V29() V30() ) Element of REAL : ( ( ) ( non zero V46() V57() V58() V59() V63() ) set ) ) * : ( ( ) ( complex ) Element of COMPLEX : ( ( ) ( non zero V46() V57() V63() ) set ) ) ) : ( ( ) ( complex ) Element of COMPLEX : ( ( ) ( non zero V46() V57() V63() ) set ) ) : ( ( ) ( complex ) Element of COMPLEX : ( ( ) ( non zero V46() V57() V63() ) set ) ) ;

theorem :: SIN_COS3:49

for x, y being ( ( ) ( complex V29() V30() ) Element of REAL : ( ( ) ( non zero V46() V57() V58() V59() V63() ) set ) ) holds cosh_C : ( ( V6() V18( COMPLEX : ( ( ) ( non zero V46() V57() V63() ) set ) , COMPLEX : ( ( ) ( non zero V46() V57() V63() ) set ) ) ) ( V1() V4( COMPLEX : ( ( ) ( non zero V46() V57() V63() ) set ) ) V5( COMPLEX : ( ( ) ( non zero V46() V57() V63() ) set ) ) V6() non zero total V18( COMPLEX : ( ( ) ( non zero V46() V57() V63() ) set ) , COMPLEX : ( ( ) ( non zero V46() V57() V63() ) set ) ) ) Function of COMPLEX : ( ( ) ( non zero V46() V57() V63() ) set ) , COMPLEX : ( ( ) ( non zero V46() V57() V63() ) set ) ) /. (x : ( ( ) ( complex V29() V30() ) Element of REAL : ( ( ) ( non zero V46() V57() V58() V59() V63() ) set ) ) + ((- y : ( ( ) ( complex V29() V30() ) Element of REAL : ( ( ) ( non zero V46() V57() V58() V59() V63() ) set ) ) ) : ( ( ) ( complex V29() V30() ) Element of REAL : ( ( ) ( non zero V46() V57() V58() V59() V63() ) set ) ) * : ( ( ) ( complex ) Element of COMPLEX : ( ( ) ( non zero V46() V57() V63() ) set ) ) ) : ( ( ) ( complex ) Element of COMPLEX : ( ( ) ( non zero V46() V57() V63() ) set ) ) ) : ( ( ) ( complex ) Element of COMPLEX : ( ( ) ( non zero V46() V57() V63() ) set ) ) : ( ( ) ( complex ) Element of COMPLEX : ( ( ) ( non zero V46() V57() V63() ) set ) ) = ((cosh : ( ( V6() V18( REAL : ( ( ) ( non zero V46() V57() V58() V59() V63() ) set ) , REAL : ( ( ) ( non zero V46() V57() V58() V59() V63() ) set ) ) ) ( V1() V4( REAL : ( ( ) ( non zero V46() V57() V58() V59() V63() ) set ) ) V5( REAL : ( ( ) ( non zero V46() V57() V58() V59() V63() ) set ) ) V6() non zero total V18( REAL : ( ( ) ( non zero V46() V57() V58() V59() V63() ) set ) , REAL : ( ( ) ( non zero V46() V57() V58() V59() V63() ) set ) ) ) Element of K19(K20(REAL : ( ( ) ( non zero V46() V57() V58() V59() V63() ) set ) ,REAL : ( ( ) ( non zero V46() V57() V58() V59() V63() ) set ) ) : ( ( ) ( ) set ) ) : ( ( ) ( ) set ) ) . x : ( ( ) ( complex V29() V30() ) Element of REAL : ( ( ) ( non zero V46() V57() V58() V59() V63() ) set ) ) ) : ( ( ) ( complex V29() V30() ) Element of REAL : ( ( ) ( non zero V46() V57() V58() V59() V63() ) set ) ) * (cos : ( ( V6() V18( REAL : ( ( ) ( non zero V46() V57() V58() V59() V63() ) set ) , REAL : ( ( ) ( non zero V46() V57() V58() V59() V63() ) set ) ) ) ( V1() V4( REAL : ( ( ) ( non zero V46() V57() V58() V59() V63() ) set ) ) V5( REAL : ( ( ) ( non zero V46() V57() V58() V59() V63() ) set ) ) V6() non zero total V18( REAL : ( ( ) ( non zero V46() V57() V58() V59() V63() ) set ) , REAL : ( ( ) ( non zero V46() V57() V58() V59() V63() ) set ) ) ) Element of K19(K20(REAL : ( ( ) ( non zero V46() V57() V58() V59() V63() ) set ) ,REAL : ( ( ) ( non zero V46() V57() V58() V59() V63() ) set ) ) : ( ( ) ( ) set ) ) : ( ( ) ( ) set ) ) . y : ( ( ) ( complex V29() V30() ) Element of REAL : ( ( ) ( non zero V46() V57() V58() V59() V63() ) set ) ) ) : ( ( ) ( complex V29() V30() ) Element of REAL : ( ( ) ( non zero V46() V57() V58() V59() V63() ) set ) ) ) : ( ( ) ( complex V29() V30() ) Element of REAL : ( ( ) ( non zero V46() V57() V58() V59() V63() ) set ) ) + ((- ((sinh : ( ( V6() V18( REAL : ( ( ) ( non zero V46() V57() V58() V59() V63() ) set ) , REAL : ( ( ) ( non zero V46() V57() V58() V59() V63() ) set ) ) ) ( V1() V4( REAL : ( ( ) ( non zero V46() V57() V58() V59() V63() ) set ) ) V5( REAL : ( ( ) ( non zero V46() V57() V58() V59() V63() ) set ) ) V6() non zero total V18( REAL : ( ( ) ( non zero V46() V57() V58() V59() V63() ) set ) , REAL : ( ( ) ( non zero V46() V57() V58() V59() V63() ) set ) ) ) Element of K19(K20(REAL : ( ( ) ( non zero V46() V57() V58() V59() V63() ) set ) ,REAL : ( ( ) ( non zero V46() V57() V58() V59() V63() ) set ) ) : ( ( ) ( ) set ) ) : ( ( ) ( ) set ) ) . x : ( ( ) ( complex V29() V30() ) Element of REAL : ( ( ) ( non zero V46() V57() V58() V59() V63() ) set ) ) ) : ( ( ) ( complex V29() V30() ) Element of REAL : ( ( ) ( non zero V46() V57() V58() V59() V63() ) set ) ) * (sin : ( ( V6() V18( REAL : ( ( ) ( non zero V46() V57() V58() V59() V63() ) set ) , REAL : ( ( ) ( non zero V46() V57() V58() V59() V63() ) set ) ) ) ( V1() V4( REAL : ( ( ) ( non zero V46() V57() V58() V59() V63() ) set ) ) V5( REAL : ( ( ) ( non zero V46() V57() V58() V59() V63() ) set ) ) V6() non zero total V18( REAL : ( ( ) ( non zero V46() V57() V58() V59() V63() ) set ) , REAL : ( ( ) ( non zero V46() V57() V58() V59() V63() ) set ) ) ) Element of K19(K20(REAL : ( ( ) ( non zero V46() V57() V58() V59() V63() ) set ) ,REAL : ( ( ) ( non zero V46() V57() V58() V59() V63() ) set ) ) : ( ( ) ( ) set ) ) : ( ( ) ( ) set ) ) . y : ( ( ) ( complex V29() V30() ) Element of REAL : ( ( ) ( non zero V46() V57() V58() V59() V63() ) set ) ) ) : ( ( ) ( complex V29() V30() ) Element of REAL : ( ( ) ( non zero V46() V57() V58() V59() V63() ) set ) ) ) : ( ( ) ( complex V29() V30() ) Element of REAL : ( ( ) ( non zero V46() V57() V58() V59() V63() ) set ) ) ) : ( ( ) ( complex V29() V30() ) Element of REAL : ( ( ) ( non zero V46() V57() V58() V59() V63() ) set ) ) * : ( ( ) ( complex ) Element of COMPLEX : ( ( ) ( non zero V46() V57() V63() ) set ) ) ) : ( ( ) ( complex ) Element of COMPLEX : ( ( ) ( non zero V46() V57() V63() ) set ) ) : ( ( ) ( complex ) Element of COMPLEX : ( ( ) ( non zero V46() V57() V63() ) set ) ) ;

theorem :: SIN_COS3:50

for n being ( ( ) ( natural complex V29() V30() V33() V34() V57() V58() V59() V60() V61() V62() ) Element of NAT : ( ( ) ( V57() V58() V59() V60() V61() V62() V63() ) Element of K19(REAL : ( ( ) ( non zero V46() V57() V58() V59() V63() ) set ) ) : ( ( ) ( ) set ) ) )
for z being ( ( ) ( complex ) Element of COMPLEX : ( ( ) ( non zero V46() V57() V63() ) set ) ) holds ((cos_C : ( ( V6() V18( COMPLEX : ( ( ) ( non zero V46() V57() V63() ) set ) , COMPLEX : ( ( ) ( non zero V46() V57() V63() ) set ) ) ) ( V1() V4( COMPLEX : ( ( ) ( non zero V46() V57() V63() ) set ) ) V5( COMPLEX : ( ( ) ( non zero V46() V57() V63() ) set ) ) V6() non zero total V18( COMPLEX : ( ( ) ( non zero V46() V57() V63() ) set ) , COMPLEX : ( ( ) ( non zero V46() V57() V63() ) set ) ) ) Function of COMPLEX : ( ( ) ( non zero V46() V57() V63() ) set ) , COMPLEX : ( ( ) ( non zero V46() V57() V63() ) set ) ) /. z : ( ( ) ( complex ) Element of COMPLEX : ( ( ) ( non zero V46() V57() V63() ) set ) ) ) : ( ( ) ( complex ) Element of COMPLEX : ( ( ) ( non zero V46() V57() V63() ) set ) ) + ( : ( ( ) ( complex ) Element of COMPLEX : ( ( ) ( non zero V46() V57() V63() ) set ) ) * (sin_C : ( ( V6() V18( COMPLEX : ( ( ) ( non zero V46() V57() V63() ) set ) , COMPLEX : ( ( ) ( non zero V46() V57() V63() ) set ) ) ) ( V1() V4( COMPLEX : ( ( ) ( non zero V46() V57() V63() ) set ) ) V5( COMPLEX : ( ( ) ( non zero V46() V57() V63() ) set ) ) V6() non zero total V18( COMPLEX : ( ( ) ( non zero V46() V57() V63() ) set ) , COMPLEX : ( ( ) ( non zero V46() V57() V63() ) set ) ) ) Function of COMPLEX : ( ( ) ( non zero V46() V57() V63() ) set ) , COMPLEX : ( ( ) ( non zero V46() V57() V63() ) set ) ) /. z : ( ( ) ( complex ) Element of COMPLEX : ( ( ) ( non zero V46() V57() V63() ) set ) ) ) : ( ( ) ( complex ) Element of COMPLEX : ( ( ) ( non zero V46() V57() V63() ) set ) ) ) : ( ( ) ( complex ) Element of COMPLEX : ( ( ) ( non zero V46() V57() V63() ) set ) ) ) : ( ( ) ( complex ) Element of COMPLEX : ( ( ) ( non zero V46() V57() V63() ) set ) ) #N n : ( ( ) ( natural complex V29() V30() V33() V34() V57() V58() V59() V60() V61() V62() ) Element of NAT : ( ( ) ( V57() V58() V59() V60() V61() V62() V63() ) Element of K19(REAL : ( ( ) ( non zero V46() V57() V58() V59() V63() ) set ) ) : ( ( ) ( ) set ) ) ) : ( ( ) ( complex ) Element of COMPLEX : ( ( ) ( non zero V46() V57() V63() ) set ) ) = (cos_C : ( ( V6() V18( COMPLEX : ( ( ) ( non zero V46() V57() V63() ) set ) , COMPLEX : ( ( ) ( non zero V46() V57() V63() ) set ) ) ) ( V1() V4( COMPLEX : ( ( ) ( non zero V46() V57() V63() ) set ) ) V5( COMPLEX : ( ( ) ( non zero V46() V57() V63() ) set ) ) V6() non zero total V18( COMPLEX : ( ( ) ( non zero V46() V57() V63() ) set ) , COMPLEX : ( ( ) ( non zero V46() V57() V63() ) set ) ) ) Function of COMPLEX : ( ( ) ( non zero V46() V57() V63() ) set ) , COMPLEX : ( ( ) ( non zero V46() V57() V63() ) set ) ) /. (n : ( ( ) ( natural complex V29() V30() V33() V34() V57() V58() V59() V60() V61() V62() ) Element of NAT : ( ( ) ( V57() V58() V59() V60() V61() V62() V63() ) Element of K19(REAL : ( ( ) ( non zero V46() V57() V58() V59() V63() ) set ) ) : ( ( ) ( ) set ) ) ) * z : ( ( ) ( complex ) Element of COMPLEX : ( ( ) ( non zero V46() V57() V63() ) set ) ) ) : ( ( ) ( complex ) Element of COMPLEX : ( ( ) ( non zero V46() V57() V63() ) set ) ) ) : ( ( ) ( complex ) Element of COMPLEX : ( ( ) ( non zero V46() V57() V63() ) set ) ) + ( : ( ( ) ( complex ) Element of COMPLEX : ( ( ) ( non zero V46() V57() V63() ) set ) ) * (sin_C : ( ( V6() V18( COMPLEX : ( ( ) ( non zero V46() V57() V63() ) set ) , COMPLEX : ( ( ) ( non zero V46() V57() V63() ) set ) ) ) ( V1() V4( COMPLEX : ( ( ) ( non zero V46() V57() V63() ) set ) ) V5( COMPLEX : ( ( ) ( non zero V46() V57() V63() ) set ) ) V6() non zero total V18( COMPLEX : ( ( ) ( non zero V46() V57() V63() ) set ) , COMPLEX : ( ( ) ( non zero V46() V57() V63() ) set ) ) ) Function of COMPLEX : ( ( ) ( non zero V46() V57() V63() ) set ) , COMPLEX : ( ( ) ( non zero V46() V57() V63() ) set ) ) /. (n : ( ( ) ( natural complex V29() V30() V33() V34() V57() V58() V59() V60() V61() V62() ) Element of NAT : ( ( ) ( V57() V58() V59() V60() V61() V62() V63() ) Element of K19(REAL : ( ( ) ( non zero V46() V57() V58() V59() V63() ) set ) ) : ( ( ) ( ) set ) ) ) * z : ( ( ) ( complex ) Element of COMPLEX : ( ( ) ( non zero V46() V57() V63() ) set ) ) ) : ( ( ) ( complex ) Element of COMPLEX : ( ( ) ( non zero V46() V57() V63() ) set ) ) ) : ( ( ) ( complex ) Element of COMPLEX : ( ( ) ( non zero V46() V57() V63() ) set ) ) ) : ( ( ) ( complex ) Element of COMPLEX : ( ( ) ( non zero V46() V57() V63() ) set ) ) : ( ( ) ( complex ) Element of COMPLEX : ( ( ) ( non zero V46() V57() V63() ) set ) ) ;

theorem :: SIN_COS3:51

for n being ( ( ) ( natural complex V29() V30() V33() V34() V57() V58() V59() V60() V61() V62() ) Element of NAT : ( ( ) ( V57() V58() V59() V60() V61() V62() V63() ) Element of K19(REAL : ( ( ) ( non zero V46() V57() V58() V59() V63() ) set ) ) : ( ( ) ( ) set ) ) )
for z being ( ( ) ( complex ) Element of COMPLEX : ( ( ) ( non zero V46() V57() V63() ) set ) ) holds ((cos_C : ( ( V6() V18( COMPLEX : ( ( ) ( non zero V46() V57() V63() ) set ) , COMPLEX : ( ( ) ( non zero V46() V57() V63() ) set ) ) ) ( V1() V4( COMPLEX : ( ( ) ( non zero V46() V57() V63() ) set ) ) V5( COMPLEX : ( ( ) ( non zero V46() V57() V63() ) set ) ) V6() non zero total V18( COMPLEX : ( ( ) ( non zero V46() V57() V63() ) set ) , COMPLEX : ( ( ) ( non zero V46() V57() V63() ) set ) ) ) Function of COMPLEX : ( ( ) ( non zero V46() V57() V63() ) set ) , COMPLEX : ( ( ) ( non zero V46() V57() V63() ) set ) ) /. z : ( ( ) ( complex ) Element of COMPLEX : ( ( ) ( non zero V46() V57() V63() ) set ) ) ) : ( ( ) ( complex ) Element of COMPLEX : ( ( ) ( non zero V46() V57() V63() ) set ) ) - ( : ( ( ) ( complex ) Element of COMPLEX : ( ( ) ( non zero V46() V57() V63() ) set ) ) * (sin_C : ( ( V6() V18( COMPLEX : ( ( ) ( non zero V46() V57() V63() ) set ) , COMPLEX : ( ( ) ( non zero V46() V57() V63() ) set ) ) ) ( V1() V4( COMPLEX : ( ( ) ( non zero V46() V57() V63() ) set ) ) V5( COMPLEX : ( ( ) ( non zero V46() V57() V63() ) set ) ) V6() non zero total V18( COMPLEX : ( ( ) ( non zero V46() V57() V63() ) set ) , COMPLEX : ( ( ) ( non zero V46() V57() V63() ) set ) ) ) Function of COMPLEX : ( ( ) ( non zero V46() V57() V63() ) set ) , COMPLEX : ( ( ) ( non zero V46() V57() V63() ) set ) ) /. z : ( ( ) ( complex ) Element of COMPLEX : ( ( ) ( non zero V46() V57() V63() ) set ) ) ) : ( ( ) ( complex ) Element of COMPLEX : ( ( ) ( non zero V46() V57() V63() ) set ) ) ) : ( ( ) ( complex ) Element of COMPLEX : ( ( ) ( non zero V46() V57() V63() ) set ) ) ) : ( ( ) ( complex ) Element of COMPLEX : ( ( ) ( non zero V46() V57() V63() ) set ) ) #N n : ( ( ) ( natural complex V29() V30() V33() V34() V57() V58() V59() V60() V61() V62() ) Element of NAT : ( ( ) ( V57() V58() V59() V60() V61() V62() V63() ) Element of K19(REAL : ( ( ) ( non zero V46() V57() V58() V59() V63() ) set ) ) : ( ( ) ( ) set ) ) ) : ( ( ) ( complex ) Element of COMPLEX : ( ( ) ( non zero V46() V57() V63() ) set ) ) = (cos_C : ( ( V6() V18( COMPLEX : ( ( ) ( non zero V46() V57() V63() ) set ) , COMPLEX : ( ( ) ( non zero V46() V57() V63() ) set ) ) ) ( V1() V4( COMPLEX : ( ( ) ( non zero V46() V57() V63() ) set ) ) V5( COMPLEX : ( ( ) ( non zero V46() V57() V63() ) set ) ) V6() non zero total V18( COMPLEX : ( ( ) ( non zero V46() V57() V63() ) set ) , COMPLEX : ( ( ) ( non zero V46() V57() V63() ) set ) ) ) Function of COMPLEX : ( ( ) ( non zero V46() V57() V63() ) set ) , COMPLEX : ( ( ) ( non zero V46() V57() V63() ) set ) ) /. (n : ( ( ) ( natural complex V29() V30() V33() V34() V57() V58() V59() V60() V61() V62() ) Element of NAT : ( ( ) ( V57() V58() V59() V60() V61() V62() V63() ) Element of K19(REAL : ( ( ) ( non zero V46() V57() V58() V59() V63() ) set ) ) : ( ( ) ( ) set ) ) ) * z : ( ( ) ( complex ) Element of COMPLEX : ( ( ) ( non zero V46() V57() V63() ) set ) ) ) : ( ( ) ( complex ) Element of COMPLEX : ( ( ) ( non zero V46() V57() V63() ) set ) ) ) : ( ( ) ( complex ) Element of COMPLEX : ( ( ) ( non zero V46() V57() V63() ) set ) ) - ( : ( ( ) ( complex ) Element of COMPLEX : ( ( ) ( non zero V46() V57() V63() ) set ) ) * (sin_C : ( ( V6() V18( COMPLEX : ( ( ) ( non zero V46() V57() V63() ) set ) , COMPLEX : ( ( ) ( non zero V46() V57() V63() ) set ) ) ) ( V1() V4( COMPLEX : ( ( ) ( non zero V46() V57() V63() ) set ) ) V5( COMPLEX : ( ( ) ( non zero V46() V57() V63() ) set ) ) V6() non zero total V18( COMPLEX : ( ( ) ( non zero V46() V57() V63() ) set ) , COMPLEX : ( ( ) ( non zero V46() V57() V63() ) set ) ) ) Function of COMPLEX : ( ( ) ( non zero V46() V57() V63() ) set ) , COMPLEX : ( ( ) ( non zero V46() V57() V63() ) set ) ) /. (n : ( ( ) ( natural complex V29() V30() V33() V34() V57() V58() V59() V60() V61() V62() ) Element of NAT : ( ( ) ( V57() V58() V59() V60() V61() V62() V63() ) Element of K19(REAL : ( ( ) ( non zero V46() V57() V58() V59() V63() ) set ) ) : ( ( ) ( ) set ) ) ) * z : ( ( ) ( complex ) Element of COMPLEX : ( ( ) ( non zero V46() V57() V63() ) set ) ) ) : ( ( ) ( complex ) Element of COMPLEX : ( ( ) ( non zero V46() V57() V63() ) set ) ) ) : ( ( ) ( complex ) Element of COMPLEX : ( ( ) ( non zero V46() V57() V63() ) set ) ) ) : ( ( ) ( complex ) Element of COMPLEX : ( ( ) ( non zero V46() V57() V63() ) set ) ) : ( ( ) ( complex ) Element of COMPLEX : ( ( ) ( non zero V46() V57() V63() ) set ) ) ;

theorem :: SIN_COS3:52

theorem :: SIN_COS3:53

theorem :: SIN_COS3:54

for x, y being ( ( ) ( complex V29() V30() ) Element of REAL : ( ( ) ( non zero V46() V57() V58() V59() V63() ) set ) ) holds (((1 : ( ( ) ( non zero natural complex V29() V30() V33() V34() V57() V58() V59() V60() V61() V62() ) Element of NAT : ( ( ) ( V57() V58() V59() V60() V61() V62() V63() ) Element of K19(REAL : ( ( ) ( non zero V46() V57() V58() V59() V63() ) set ) ) : ( ( ) ( ) set ) ) ) + ((- 1 : ( ( ) ( non zero natural complex V29() V30() V33() V34() V57() V58() V59() V60() V61() V62() ) Element of NAT : ( ( ) ( V57() V58() V59() V60() V61() V62() V63() ) Element of K19(REAL : ( ( ) ( non zero V46() V57() V58() V59() V63() ) set ) ) : ( ( ) ( ) set ) ) ) ) : ( ( ) ( non zero complex V29() V30() V33() V34() ) Element of INT : ( ( ) ( non zero V46() V57() V58() V59() V60() V61() V63() ) set ) ) * : ( ( ) ( complex ) Element of COMPLEX : ( ( ) ( non zero V46() V57() V63() ) set ) ) ) : ( ( ) ( complex ) Element of COMPLEX : ( ( ) ( non zero V46() V57() V63() ) set ) ) ) : ( ( ) ( complex ) Element of COMPLEX : ( ( ) ( non zero V46() V57() V63() ) set ) ) / 2 : ( ( ) ( non zero natural complex V29() V30() V33() V34() V57() V58() V59() V60() V61() V62() ) Element of NAT : ( ( ) ( V57() V58() V59() V60() V61() V62() V63() ) Element of K19(REAL : ( ( ) ( non zero V46() V57() V58() V59() V63() ) set ) ) : ( ( ) ( ) set ) ) ) ) : ( ( ) ( complex ) Element of COMPLEX : ( ( ) ( non zero V46() V57() V63() ) set ) ) * (sinh_C : ( ( V6() V18( COMPLEX : ( ( ) ( non zero V46() V57() V63() ) set ) , COMPLEX : ( ( ) ( non zero V46() V57() V63() ) set ) ) ) ( V1() V4( COMPLEX : ( ( ) ( non zero V46() V57() V63() ) set ) ) V5( COMPLEX : ( ( ) ( non zero V46() V57() V63() ) set ) ) V6() non zero total V18( COMPLEX : ( ( ) ( non zero V46() V57() V63() ) set ) , COMPLEX : ( ( ) ( non zero V46() V57() V63() ) set ) ) ) Function of COMPLEX : ( ( ) ( non zero V46() V57() V63() ) set ) , COMPLEX : ( ( ) ( non zero V46() V57() V63() ) set ) ) /. (x : ( ( ) ( complex V29() V30() ) Element of REAL : ( ( ) ( non zero V46() V57() V58() V59() V63() ) set ) ) + (y : ( ( ) ( complex V29() V30() ) Element of REAL : ( ( ) ( non zero V46() V57() V58() V59() V63() ) set ) ) * : ( ( ) ( complex ) Element of COMPLEX : ( ( ) ( non zero V46() V57() V63() ) set ) ) ) : ( ( ) ( complex ) Element of COMPLEX : ( ( ) ( non zero V46() V57() V63() ) set ) ) ) : ( ( ) ( complex ) Element of COMPLEX : ( ( ) ( non zero V46() V57() V63() ) set ) ) ) : ( ( ) ( complex ) Element of COMPLEX : ( ( ) ( non zero V46() V57() V63() ) set ) ) ) : ( ( ) ( complex ) Element of COMPLEX : ( ( ) ( non zero V46() V57() V63() ) set ) ) + (((1 : ( ( ) ( non zero natural complex V29() V30() V33() V34() V57() V58() V59() V60() V61() V62() ) Element of NAT : ( ( ) ( V57() V58() V59() V60() V61() V62() V63() ) Element of K19(REAL : ( ( ) ( non zero V46() V57() V58() V59() V63() ) set ) ) : ( ( ) ( ) set ) ) ) + : ( ( ) ( complex ) Element of COMPLEX : ( ( ) ( non zero V46() V57() V63() ) set ) ) ) : ( ( ) ( complex ) Element of COMPLEX : ( ( ) ( non zero V46() V57() V63() ) set ) ) / 2 : ( ( ) ( non zero natural complex V29() V30() V33() V34() V57() V58() V59() V60() V61() V62() ) Element of NAT : ( ( ) ( V57() V58() V59() V60() V61() V62() V63() ) Element of K19(REAL : ( ( ) ( non zero V46() V57() V58() V59() V63() ) set ) ) : ( ( ) ( ) set ) ) ) ) : ( ( ) ( complex ) Element of COMPLEX : ( ( ) ( non zero V46() V57() V63() ) set ) ) * (sinh_C : ( ( V6() V18( COMPLEX : ( ( ) ( non zero V46() V57() V63() ) set ) , COMPLEX : ( ( ) ( non zero V46() V57() V63() ) set ) ) ) ( V1() V4( COMPLEX : ( ( ) ( non zero V46() V57() V63() ) set ) ) V5( COMPLEX : ( ( ) ( non zero V46() V57() V63() ) set ) ) V6() non zero total V18( COMPLEX : ( ( ) ( non zero V46() V57() V63() ) set ) , COMPLEX : ( ( ) ( non zero V46() V57() V63() ) set ) ) ) Function of COMPLEX : ( ( ) ( non zero V46() V57() V63() ) set ) , COMPLEX : ( ( ) ( non zero V46() V57() V63() ) set ) ) /. (x : ( ( ) ( complex V29() V30() ) Element of REAL : ( ( ) ( non zero V46() V57() V58() V59() V63() ) set ) ) + ((- y : ( ( ) ( complex V29() V30() ) Element of REAL : ( ( ) ( non zero V46() V57() V58() V59() V63() ) set ) ) ) : ( ( ) ( complex V29() V30() ) Element of REAL : ( ( ) ( non zero V46() V57() V58() V59() V63() ) set ) ) * : ( ( ) ( complex ) Element of COMPLEX : ( ( ) ( non zero V46() V57() V63() ) set ) ) ) : ( ( ) ( complex ) Element of COMPLEX : ( ( ) ( non zero V46() V57() V63() ) set ) ) ) : ( ( ) ( complex ) Element of COMPLEX : ( ( ) ( non zero V46() V57() V63() ) set ) ) ) : ( ( ) ( complex ) Element of COMPLEX : ( ( ) ( non zero V46() V57() V63() ) set ) ) ) : ( ( ) ( complex ) Element of COMPLEX : ( ( ) ( non zero V46() V57() V63() ) set ) ) : ( ( ) ( complex ) Element of COMPLEX : ( ( ) ( non zero V46() V57() V63() ) set ) ) = ((sinh : ( ( V6() V18( REAL : ( ( ) ( non zero V46() V57() V58() V59() V63() ) set ) , REAL : ( ( ) ( non zero V46() V57() V58() V59() V63() ) set ) ) ) ( V1() V4( REAL : ( ( ) ( non zero V46() V57() V58() V59() V63() ) set ) ) V5( REAL : ( ( ) ( non zero V46() V57() V58() V59() V63() ) set ) ) V6() non zero total V18( REAL : ( ( ) ( non zero V46() V57() V58() V59() V63() ) set ) , REAL : ( ( ) ( non zero V46() V57() V58() V59() V63() ) set ) ) ) Element of K19(K20(REAL : ( ( ) ( non zero V46() V57() V58() V59() V63() ) set ) ,REAL : ( ( ) ( non zero V46() V57() V58() V59() V63() ) set ) ) : ( ( ) ( ) set ) ) : ( ( ) ( ) set ) ) . x : ( ( ) ( complex V29() V30() ) Element of REAL : ( ( ) ( non zero V46() V57() V58() V59() V63() ) set ) ) ) : ( ( ) ( complex V29() V30() ) Element of REAL : ( ( ) ( non zero V46() V57() V58() V59() V63() ) set ) ) * (cos : ( ( V6() V18( REAL : ( ( ) ( non zero V46() V57() V58() V59() V63() ) set ) , REAL : ( ( ) ( non zero V46() V57() V58() V59() V63() ) set ) ) ) ( V1() V4( REAL : ( ( ) ( non zero V46() V57() V58() V59() V63() ) set ) ) V5( REAL : ( ( ) ( non zero V46() V57() V58() V59() V63() ) set ) ) V6() non zero total V18( REAL : ( ( ) ( non zero V46() V57() V58() V59() V63() ) set ) , REAL : ( ( ) ( non zero V46() V57() V58() V59() V63() ) set ) ) ) Element of K19(K20(REAL : ( ( ) ( non zero V46() V57() V58() V59() V63() ) set ) ,REAL : ( ( ) ( non zero V46() V57() V58() V59() V63() ) set ) ) : ( ( ) ( ) set ) ) : ( ( ) ( ) set ) ) . y : ( ( ) ( complex V29() V30() ) Element of REAL : ( ( ) ( non zero V46() V57() V58() V59() V63() ) set ) ) ) : ( ( ) ( complex V29() V30() ) Element of REAL : ( ( ) ( non zero V46() V57() V58() V59() V63() ) set ) ) ) : ( ( ) ( complex V29() V30() ) Element of REAL : ( ( ) ( non zero V46() V57() V58() V59() V63() ) set ) ) + ((cosh : ( ( V6() V18( REAL : ( ( ) ( non zero V46() V57() V58() V59() V63() ) set ) , REAL : ( ( ) ( non zero V46() V57() V58() V59() V63() ) set ) ) ) ( V1() V4( REAL : ( ( ) ( non zero V46() V57() V58() V59() V63() ) set ) ) V5( REAL : ( ( ) ( non zero V46() V57() V58() V59() V63() ) set ) ) V6() non zero total V18( REAL : ( ( ) ( non zero V46() V57() V58() V59() V63() ) set ) , REAL : ( ( ) ( non zero V46() V57() V58() V59() V63() ) set ) ) ) Element of K19(K20(REAL : ( ( ) ( non zero V46() V57() V58() V59() V63() ) set ) ,REAL : ( ( ) ( non zero V46() V57() V58() V59() V63() ) set ) ) : ( ( ) ( ) set ) ) : ( ( ) ( ) set ) ) . x : ( ( ) ( complex V29() V30() ) Element of REAL : ( ( ) ( non zero V46() V57() V58() V59() V63() ) set ) ) ) : ( ( ) ( complex V29() V30() ) Element of REAL : ( ( ) ( non zero V46() V57() V58() V59() V63() ) set ) ) * (sin : ( ( V6() V18( REAL : ( ( ) ( non zero V46() V57() V58() V59() V63() ) set ) , REAL : ( ( ) ( non zero V46() V57() V58() V59() V63() ) set ) ) ) ( V1() V4( REAL : ( ( ) ( non zero V46() V57() V58() V59() V63() ) set ) ) V5( REAL : ( ( ) ( non zero V46() V57() V58() V59() V63() ) set ) ) V6() non zero total V18( REAL : ( ( ) ( non zero V46() V57() V58() V59() V63() ) set ) , REAL : ( ( ) ( non zero V46() V57() V58() V59() V63() ) set ) ) ) Element of K19(K20(REAL : ( ( ) ( non zero V46() V57() V58() V59() V63() ) set ) ,REAL : ( ( ) ( non zero V46() V57() V58() V59() V63() ) set ) ) : ( ( ) ( ) set ) ) : ( ( ) ( ) set ) ) . y : ( ( ) ( complex V29() V30() ) Element of REAL : ( ( ) ( non zero V46() V57() V58() V59() V63() ) set ) ) ) : ( ( ) ( complex V29() V30() ) Element of REAL : ( ( ) ( non zero V46() V57() V58() V59() V63() ) set ) ) ) : ( ( ) ( complex V29() V30() ) Element of REAL : ( ( ) ( non zero V46() V57() V58() V59() V63() ) set ) ) : ( ( ) ( complex V29() V30() ) Element of REAL : ( ( ) ( non zero V46() V57() V58() V59() V63() ) set ) ) ;

theorem :: SIN_COS3:55

for x, y being ( ( ) ( complex V29() V30() ) Element of REAL : ( ( ) ( non zero V46() V57() V58() V59() V63() ) set ) ) holds (((1 : ( ( ) ( non zero natural complex V29() V30() V33() V34() V57() V58() V59() V60() V61() V62() ) Element of NAT : ( ( ) ( V57() V58() V59() V60() V61() V62() V63() ) Element of K19(REAL : ( ( ) ( non zero V46() V57() V58() V59() V63() ) set ) ) : ( ( ) ( ) set ) ) ) + ((- 1 : ( ( ) ( non zero natural complex V29() V30() V33() V34() V57() V58() V59() V60() V61() V62() ) Element of NAT : ( ( ) ( V57() V58() V59() V60() V61() V62() V63() ) Element of K19(REAL : ( ( ) ( non zero V46() V57() V58() V59() V63() ) set ) ) : ( ( ) ( ) set ) ) ) ) : ( ( ) ( non zero complex V29() V30() V33() V34() ) Element of INT : ( ( ) ( non zero V46() V57() V58() V59() V60() V61() V63() ) set ) ) * : ( ( ) ( complex ) Element of COMPLEX : ( ( ) ( non zero V46() V57() V63() ) set ) ) ) : ( ( ) ( complex ) Element of COMPLEX : ( ( ) ( non zero V46() V57() V63() ) set ) ) ) : ( ( ) ( complex ) Element of COMPLEX : ( ( ) ( non zero V46() V57() V63() ) set ) ) / 2 : ( ( ) ( non zero natural complex V29() V30() V33() V34() V57() V58() V59() V60() V61() V62() ) Element of NAT : ( ( ) ( V57() V58() V59() V60() V61() V62() V63() ) Element of K19(REAL : ( ( ) ( non zero V46() V57() V58() V59() V63() ) set ) ) : ( ( ) ( ) set ) ) ) ) : ( ( ) ( complex ) Element of COMPLEX : ( ( ) ( non zero V46() V57() V63() ) set ) ) * (cosh_C : ( ( V6() V18( COMPLEX : ( ( ) ( non zero V46() V57() V63() ) set ) , COMPLEX : ( ( ) ( non zero V46() V57() V63() ) set ) ) ) ( V1() V4( COMPLEX : ( ( ) ( non zero V46() V57() V63() ) set ) ) V5( COMPLEX : ( ( ) ( non zero V46() V57() V63() ) set ) ) V6() non zero total V18( COMPLEX : ( ( ) ( non zero V46() V57() V63() ) set ) , COMPLEX : ( ( ) ( non zero V46() V57() V63() ) set ) ) ) Function of COMPLEX : ( ( ) ( non zero V46() V57() V63() ) set ) , COMPLEX : ( ( ) ( non zero V46() V57() V63() ) set ) ) /. (x : ( ( ) ( complex V29() V30() ) Element of REAL : ( ( ) ( non zero V46() V57() V58() V59() V63() ) set ) ) + (y : ( ( ) ( complex V29() V30() ) Element of REAL : ( ( ) ( non zero V46() V57() V58() V59() V63() ) set ) ) * : ( ( ) ( complex ) Element of COMPLEX : ( ( ) ( non zero V46() V57() V63() ) set ) ) ) : ( ( ) ( complex ) Element of COMPLEX : ( ( ) ( non zero V46() V57() V63() ) set ) ) ) : ( ( ) ( complex ) Element of COMPLEX : ( ( ) ( non zero V46() V57() V63() ) set ) ) ) : ( ( ) ( complex ) Element of COMPLEX : ( ( ) ( non zero V46() V57() V63() ) set ) ) ) : ( ( ) ( complex ) Element of COMPLEX : ( ( ) ( non zero V46() V57() V63() ) set ) ) + (((1 : ( ( ) ( non zero natural complex V29() V30() V33() V34() V57() V58() V59() V60() V61() V62() ) Element of NAT : ( ( ) ( V57() V58() V59() V60() V61() V62() V63() ) Element of K19(REAL : ( ( ) ( non zero V46() V57() V58() V59() V63() ) set ) ) : ( ( ) ( ) set ) ) ) + : ( ( ) ( complex ) Element of COMPLEX : ( ( ) ( non zero V46() V57() V63() ) set ) ) ) : ( ( ) ( complex ) Element of COMPLEX : ( ( ) ( non zero V46() V57() V63() ) set ) ) / 2 : ( ( ) ( non zero natural complex V29() V30() V33() V34() V57() V58() V59() V60() V61() V62() ) Element of NAT : ( ( ) ( V57() V58() V59() V60() V61() V62() V63() ) Element of K19(REAL : ( ( ) ( non zero V46() V57() V58() V59() V63() ) set ) ) : ( ( ) ( ) set ) ) ) ) : ( ( ) ( complex ) Element of COMPLEX : ( ( ) ( non zero V46() V57() V63() ) set ) ) * (cosh_C : ( ( V6() V18( COMPLEX : ( ( ) ( non zero V46() V57() V63() ) set ) , COMPLEX : ( ( ) ( non zero V46() V57() V63() ) set ) ) ) ( V1() V4( COMPLEX : ( ( ) ( non zero V46() V57() V63() ) set ) ) V5( COMPLEX : ( ( ) ( non zero V46() V57() V63() ) set ) ) V6() non zero total V18( COMPLEX : ( ( ) ( non zero V46() V57() V63() ) set ) , COMPLEX : ( ( ) ( non zero V46() V57() V63() ) set ) ) ) Function of COMPLEX : ( ( ) ( non zero V46() V57() V63() ) set ) , COMPLEX : ( ( ) ( non zero V46() V57() V63() ) set ) ) /. (x : ( ( ) ( complex V29() V30() ) Element of REAL : ( ( ) ( non zero V46() V57() V58() V59() V63() ) set ) ) + ((- y : ( ( ) ( complex V29() V30() ) Element of REAL : ( ( ) ( non zero V46() V57() V58() V59() V63() ) set ) ) ) : ( ( ) ( complex V29() V30() ) Element of REAL : ( ( ) ( non zero V46() V57() V58() V59() V63() ) set ) ) * : ( ( ) ( complex ) Element of COMPLEX : ( ( ) ( non zero V46() V57() V63() ) set ) ) ) : ( ( ) ( complex ) Element of COMPLEX : ( ( ) ( non zero V46() V57() V63() ) set ) ) ) : ( ( ) ( complex ) Element of COMPLEX : ( ( ) ( non zero V46() V57() V63() ) set ) ) ) : ( ( ) ( complex ) Element of COMPLEX : ( ( ) ( non zero V46() V57() V63() ) set ) ) ) : ( ( ) ( complex ) Element of COMPLEX : ( ( ) ( non zero V46() V57() V63() ) set ) ) : ( ( ) ( complex ) Element of COMPLEX : ( ( ) ( non zero V46() V57() V63() ) set ) ) = ((sinh : ( ( V6() V18( REAL : ( ( ) ( non zero V46() V57() V58() V59() V63() ) set ) , REAL : ( ( ) ( non zero V46() V57() V58() V59() V63() ) set ) ) ) ( V1() V4( REAL : ( ( ) ( non zero V46() V57() V58() V59() V63() ) set ) ) V5( REAL : ( ( ) ( non zero V46() V57() V58() V59() V63() ) set ) ) V6() non zero total V18( REAL : ( ( ) ( non zero V46() V57() V58() V59() V63() ) set ) , REAL : ( ( ) ( non zero V46() V57() V58() V59() V63() ) set ) ) ) Element of K19(K20(REAL : ( ( ) ( non zero V46() V57() V58() V59() V63() ) set ) ,REAL : ( ( ) ( non zero V46() V57() V58() V59() V63() ) set ) ) : ( ( ) ( ) set ) ) : ( ( ) ( ) set ) ) . x : ( ( ) ( complex V29() V30() ) Element of REAL : ( ( ) ( non zero V46() V57() V58() V59() V63() ) set ) ) ) : ( ( ) ( complex V29() V30() ) Element of REAL : ( ( ) ( non zero V46() V57() V58() V59() V63() ) set ) ) * (sin : ( ( V6() V18( REAL : ( ( ) ( non zero V46() V57() V58() V59() V63() ) set ) , REAL : ( ( ) ( non zero V46() V57() V58() V59() V63() ) set ) ) ) ( V1() V4( REAL : ( ( ) ( non zero V46() V57() V58() V59() V63() ) set ) ) V5( REAL : ( ( ) ( non zero V46() V57() V58() V59() V63() ) set ) ) V6() non zero total V18( REAL : ( ( ) ( non zero V46() V57() V58() V59() V63() ) set ) , REAL : ( ( ) ( non zero V46() V57() V58() V59() V63() ) set ) ) ) Element of K19(K20(REAL : ( ( ) ( non zero V46() V57() V58() V59() V63() ) set ) ,REAL : ( ( ) ( non zero V46() V57() V58() V59() V63() ) set ) ) : ( ( ) ( ) set ) ) : ( ( ) ( ) set ) ) . y : ( ( ) ( complex V29() V30() ) Element of REAL : ( ( ) ( non zero V46() V57() V58() V59() V63() ) set ) ) ) : ( ( ) ( complex V29() V30() ) Element of REAL : ( ( ) ( non zero V46() V57() V58() V59() V63() ) set ) ) ) : ( ( ) ( complex V29() V30() ) Element of REAL : ( ( ) ( non zero V46() V57() V58() V59() V63() ) set ) ) + ((cosh : ( ( V6() V18( REAL : ( ( ) ( non zero V46() V57() V58() V59() V63() ) set ) , REAL : ( ( ) ( non zero V46() V57() V58() V59() V63() ) set ) ) ) ( V1() V4( REAL : ( ( ) ( non zero V46() V57() V58() V59() V63() ) set ) ) V5( REAL : ( ( ) ( non zero V46() V57() V58() V59() V63() ) set ) ) V6() non zero total V18( REAL : ( ( ) ( non zero V46() V57() V58() V59() V63() ) set ) , REAL : ( ( ) ( non zero V46() V57() V58() V59() V63() ) set ) ) ) Element of K19(K20(REAL : ( ( ) ( non zero V46() V57() V58() V59() V63() ) set ) ,REAL : ( ( ) ( non zero V46() V57() V58() V59() V63() ) set ) ) : ( ( ) ( ) set ) ) : ( ( ) ( ) set ) ) . x : ( ( ) ( complex V29() V30() ) Element of REAL : ( ( ) ( non zero V46() V57() V58() V59() V63() ) set ) ) ) : ( ( ) ( complex V29() V30() ) Element of REAL : ( ( ) ( non zero V46() V57() V58() V59() V63() ) set ) ) * (cos : ( ( V6() V18( REAL : ( ( ) ( non zero V46() V57() V58() V59() V63() ) set ) , REAL : ( ( ) ( non zero V46() V57() V58() V59() V63() ) set ) ) ) ( V1() V4( REAL : ( ( ) ( non zero V46() V57() V58() V59() V63() ) set ) ) V5( REAL : ( ( ) ( non zero V46() V57() V58() V59() V63() ) set ) ) V6() non zero total V18( REAL : ( ( ) ( non zero V46() V57() V58() V59() V63() ) set ) , REAL : ( ( ) ( non zero V46() V57() V58() V59() V63() ) set ) ) ) Element of K19(K20(REAL : ( ( ) ( non zero V46() V57() V58() V59() V63() ) set ) ,REAL : ( ( ) ( non zero V46() V57() V58() V59() V63() ) set ) ) : ( ( ) ( ) set ) ) : ( ( ) ( ) set ) ) . y : ( ( ) ( complex V29() V30() ) Element of REAL : ( ( ) ( non zero V46() V57() V58() V59() V63() ) set ) ) ) : ( ( ) ( complex V29() V30() ) Element of REAL : ( ( ) ( non zero V46() V57() V58() V59() V63() ) set ) ) ) : ( ( ) ( complex V29() V30() ) Element of REAL : ( ( ) ( non zero V46() V57() V58() V59() V63() ) set ) ) : ( ( ) ( complex V29() V30() ) Element of REAL : ( ( ) ( non zero V46() V57() V58() V59() V63() ) set ) ) ;

theorem :: SIN_COS3:56

theorem :: SIN_COS3:57

for z being ( ( ) ( complex ) Element of COMPLEX : ( ( ) ( non zero V46() V57() V63() ) set ) ) holds (cosh_C : ( ( V6() V18( COMPLEX : ( ( ) ( non zero V46() V57() V63() ) set ) , COMPLEX : ( ( ) ( non zero V46() V57() V63() ) set ) ) ) ( V1() V4( COMPLEX : ( ( ) ( non zero V46() V57() V63() ) set ) ) V5( COMPLEX : ( ( ) ( non zero V46() V57() V63() ) set ) ) V6() non zero total V18( COMPLEX : ( ( ) ( non zero V46() V57() V63() ) set ) , COMPLEX : ( ( ) ( non zero V46() V57() V63() ) set ) ) ) Function of COMPLEX : ( ( ) ( non zero V46() V57() V63() ) set ) , COMPLEX : ( ( ) ( non zero V46() V57() V63() ) set ) ) /. z : ( ( ) ( complex ) Element of COMPLEX : ( ( ) ( non zero V46() V57() V63() ) set ) ) ) : ( ( ) ( complex ) Element of COMPLEX : ( ( ) ( non zero V46() V57() V63() ) set ) ) * (cosh_C : ( ( V6() V18( COMPLEX : ( ( ) ( non zero V46() V57() V63() ) set ) , COMPLEX : ( ( ) ( non zero V46() V57() V63() ) set ) ) ) ( V1() V4( COMPLEX : ( ( ) ( non zero V46() V57() V63() ) set ) ) V5( COMPLEX : ( ( ) ( non zero V46() V57() V63() ) set ) ) V6() non zero total V18( COMPLEX : ( ( ) ( non zero V46() V57() V63() ) set ) , COMPLEX : ( ( ) ( non zero V46() V57() V63() ) set ) ) ) Function of COMPLEX : ( ( ) ( non zero V46() V57() V63() ) set ) , COMPLEX : ( ( ) ( non zero V46() V57() V63() ) set ) ) /. z : ( ( ) ( complex ) Element of COMPLEX : ( ( ) ( non zero V46() V57() V63() ) set ) ) ) : ( ( ) ( complex ) Element of COMPLEX : ( ( ) ( non zero V46() V57() V63() ) set ) ) : ( ( ) ( complex ) Element of COMPLEX : ( ( ) ( non zero V46() V57() V63() ) set ) ) = ((cosh_C : ( ( V6() V18( COMPLEX : ( ( ) ( non zero V46() V57() V63() ) set ) , COMPLEX : ( ( ) ( non zero V46() V57() V63() ) set ) ) ) ( V1() V4( COMPLEX : ( ( ) ( non zero V46() V57() V63() ) set ) ) V5( COMPLEX : ( ( ) ( non zero V46() V57() V63() ) set ) ) V6() non zero total V18( COMPLEX : ( ( ) ( non zero V46() V57() V63() ) set ) , COMPLEX : ( ( ) ( non zero V46() V57() V63() ) set ) ) ) Function of COMPLEX : ( ( ) ( non zero V46() V57() V63() ) set ) , COMPLEX : ( ( ) ( non zero V46() V57() V63() ) set ) ) /. (2 : ( ( ) ( non zero natural complex V29() V30() V33() V34() V57() V58() V59() V60() V61() V62() ) Element of NAT : ( ( ) ( V57() V58() V59() V60() V61() V62() V63() ) Element of K19(REAL : ( ( ) ( non zero V46() V57() V58() V59() V63() ) set ) ) : ( ( ) ( ) set ) ) ) * z : ( ( ) ( complex ) Element of COMPLEX : ( ( ) ( non zero V46() V57() V63() ) set ) ) ) : ( ( ) ( complex ) Element of COMPLEX : ( ( ) ( non zero V46() V57() V63() ) set ) ) ) : ( ( ) ( complex ) Element of COMPLEX : ( ( ) ( non zero V46() V57() V63() ) set ) ) + 1 : ( ( ) ( non zero natural complex V29() V30() V33() V34() V57() V58() V59() V60() V61() V62() ) Element of NAT : ( ( ) ( V57() V58() V59() V60() V61() V62() V63() ) Element of K19(REAL : ( ( ) ( non zero V46() V57() V58() V59() V63() ) set ) ) : ( ( ) ( ) set ) ) ) ) : ( ( ) ( complex ) Element of COMPLEX : ( ( ) ( non zero V46() V57() V63() ) set ) ) / 2 : ( ( ) ( non zero natural complex V29() V30() V33() V34() V57() V58() V59() V60() V61() V62() ) Element of NAT : ( ( ) ( V57() V58() V59() V60() V61() V62() V63() ) Element of K19(REAL : ( ( ) ( non zero V46() V57() V58() V59() V63() ) set ) ) : ( ( ) ( ) set ) ) ) : ( ( ) ( complex ) Element of COMPLEX : ( ( ) ( non zero V46() V57() V63() ) set ) ) ;

theorem :: SIN_COS3:58

for z being ( ( ) ( complex ) Element of COMPLEX : ( ( ) ( non zero V46() V57() V63() ) set ) ) holds
( sinh_C : ( ( V6() V18( COMPLEX : ( ( ) ( non zero V46() V57() V63() ) set ) , COMPLEX : ( ( ) ( non zero V46() V57() V63() ) set ) ) ) ( V1() V4( COMPLEX : ( ( ) ( non zero V46() V57() V63() ) set ) ) V5( COMPLEX : ( ( ) ( non zero V46() V57() V63() ) set ) ) V6() non zero total V18( COMPLEX : ( ( ) ( non zero V46() V57() V63() ) set ) , COMPLEX : ( ( ) ( non zero V46() V57() V63() ) set ) ) ) Function of COMPLEX : ( ( ) ( non zero V46() V57() V63() ) set ) , COMPLEX : ( ( ) ( non zero V46() V57() V63() ) set ) ) /. (2 : ( ( ) ( non zero natural complex V29() V30() V33() V34() V57() V58() V59() V60() V61() V62() ) Element of NAT : ( ( ) ( V57() V58() V59() V60() V61() V62() V63() ) Element of K19(REAL : ( ( ) ( non zero V46() V57() V58() V59() V63() ) set ) ) : ( ( ) ( ) set ) ) ) * z : ( ( ) ( complex ) Element of COMPLEX : ( ( ) ( non zero V46() V57() V63() ) set ) ) ) : ( ( ) ( complex ) Element of COMPLEX : ( ( ) ( non zero V46() V57() V63() ) set ) ) : ( ( ) ( complex ) Element of COMPLEX : ( ( ) ( non zero V46() V57() V63() ) set ) ) = (2 : ( ( ) ( non zero natural complex V29() V30() V33() V34() V57() V58() V59() V60() V61() V62() ) Element of NAT : ( ( ) ( V57() V58() V59() V60() V61() V62() V63() ) Element of K19(REAL : ( ( ) ( non zero V46() V57() V58() V59() V63() ) set ) ) : ( ( ) ( ) set ) ) ) * (sinh_C : ( ( V6() V18( COMPLEX : ( ( ) ( non zero V46() V57() V63() ) set ) , COMPLEX : ( ( ) ( non zero V46() V57() V63() ) set ) ) ) ( V1() V4( COMPLEX : ( ( ) ( non zero V46() V57() V63() ) set ) ) V5( COMPLEX : ( ( ) ( non zero V46() V57() V63() ) set ) ) V6() non zero total V18( COMPLEX : ( ( ) ( non zero V46() V57() V63() ) set ) , COMPLEX : ( ( ) ( non zero V46() V57() V63() ) set ) ) ) Function of COMPLEX : ( ( ) ( non zero V46() V57() V63() ) set ) , COMPLEX : ( ( ) ( non zero V46() V57() V63() ) set ) ) /. z : ( ( ) ( complex ) Element of COMPLEX : ( ( ) ( non zero V46() V57() V63() ) set ) ) ) : ( ( ) ( complex ) Element of COMPLEX : ( ( ) ( non zero V46() V57() V63() ) set ) ) ) : ( ( ) ( complex ) Element of COMPLEX : ( ( ) ( non zero V46() V57() V63() ) set ) ) * (cosh_C : ( ( V6() V18( COMPLEX : ( ( ) ( non zero V46() V57() V63() ) set ) , COMPLEX : ( ( ) ( non zero V46() V57() V63() ) set ) ) ) ( V1() V4( COMPLEX : ( ( ) ( non zero V46() V57() V63() ) set ) ) V5( COMPLEX : ( ( ) ( non zero V46() V57() V63() ) set ) ) V6() non zero total V18( COMPLEX : ( ( ) ( non zero V46() V57() V63() ) set ) , COMPLEX : ( ( ) ( non zero V46() V57() V63() ) set ) ) ) Function of COMPLEX : ( ( ) ( non zero V46() V57() V63() ) set ) , COMPLEX : ( ( ) ( non zero V46() V57() V63() ) set ) ) /. z : ( ( ) ( complex ) Element of COMPLEX : ( ( ) ( non zero V46() V57() V63() ) set ) ) ) : ( ( ) ( complex ) Element of COMPLEX : ( ( ) ( non zero V46() V57() V63() ) set ) ) : ( ( ) ( complex ) Element of COMPLEX : ( ( ) ( non zero V46() V57() V63() ) set ) ) & cosh_C : ( ( V6() V18( COMPLEX : ( ( ) ( non zero V46() V57() V63() ) set ) , COMPLEX : ( ( ) ( non zero V46() V57() V63() ) set ) ) ) ( V1() V4( COMPLEX : ( ( ) ( non zero V46() V57() V63() ) set ) ) V5( COMPLEX : ( ( ) ( non zero V46() V57() V63() ) set ) ) V6() non zero total V18( COMPLEX : ( ( ) ( non zero V46() V57() V63() ) set ) , COMPLEX : ( ( ) ( non zero V46() V57() V63() ) set ) ) ) Function of COMPLEX : ( ( ) ( non zero V46() V57() V63() ) set ) , COMPLEX : ( ( ) ( non zero V46() V57() V63() ) set ) ) /. (2 : ( ( ) ( non zero natural complex V29() V30() V33() V34() V57() V58() V59() V60() V61() V62() ) Element of NAT : ( ( ) ( V57() V58() V59() V60() V61() V62() V63() ) Element of K19(REAL : ( ( ) ( non zero V46() V57() V58() V59() V63() ) set ) ) : ( ( ) ( ) set ) ) ) * z : ( ( ) ( complex ) Element of COMPLEX : ( ( ) ( non zero V46() V57() V63() ) set ) ) ) : ( ( ) ( complex ) Element of COMPLEX : ( ( ) ( non zero V46() V57() V63() ) set ) ) : ( ( ) ( complex ) Element of COMPLEX : ( ( ) ( non zero V46() V57() V63() ) set ) ) = ((2 : ( ( ) ( non zero natural complex V29() V30() V33() V34() V57() V58() V59() V60() V61() V62() ) Element of NAT : ( ( ) ( V57() V58() V59() V60() V61() V62() V63() ) Element of K19(REAL : ( ( ) ( non zero V46() V57() V58() V59() V63() ) set ) ) : ( ( ) ( ) set ) ) ) * (cosh_C : ( ( V6() V18( COMPLEX : ( ( ) ( non zero V46() V57() V63() ) set ) , COMPLEX : ( ( ) ( non zero V46() V57() V63() ) set ) ) ) ( V1() V4( COMPLEX : ( ( ) ( non zero V46() V57() V63() ) set ) ) V5( COMPLEX : ( ( ) ( non zero V46() V57() V63() ) set ) ) V6() non zero total V18( COMPLEX : ( ( ) ( non zero V46() V57() V63() ) set ) , COMPLEX : ( ( ) ( non zero V46() V57() V63() ) set ) ) ) Function of COMPLEX : ( ( ) ( non zero V46() V57() V63() ) set ) , COMPLEX : ( ( ) ( non zero V46() V57() V63() ) set ) ) /. z : ( ( ) ( complex ) Element of COMPLEX : ( ( ) ( non zero V46() V57() V63() ) set ) ) ) : ( ( ) ( complex ) Element of COMPLEX : ( ( ) ( non zero V46() V57() V63() ) set ) ) ) : ( ( ) ( complex ) Element of COMPLEX : ( ( ) ( non zero V46() V57() V63() ) set ) ) * (cosh_C : ( ( V6() V18( COMPLEX : ( ( ) ( non zero V46() V57() V63() ) set ) , COMPLEX : ( ( ) ( non zero V46() V57() V63() ) set ) ) ) ( V1() V4( COMPLEX : ( ( ) ( non zero V46() V57() V63() ) set ) ) V5( COMPLEX : ( ( ) ( non zero V46() V57() V63() ) set ) ) V6() non zero total V18( COMPLEX : ( ( ) ( non zero V46() V57() V63() ) set ) , COMPLEX : ( ( ) ( non zero V46() V57() V63() ) set ) ) ) Function of COMPLEX : ( ( ) ( non zero V46() V57() V63() ) set ) , COMPLEX : ( ( ) ( non zero V46() V57() V63() ) set ) ) /. z : ( ( ) ( complex ) Element of COMPLEX : ( ( ) ( non zero V46() V57() V63() ) set ) ) ) : ( ( ) ( complex ) Element of COMPLEX : ( ( ) ( non zero V46() V57() V63() ) set ) ) ) : ( ( ) ( complex ) Element of COMPLEX : ( ( ) ( non zero V46() V57() V63() ) set ) ) - 1 : ( ( ) ( non zero natural complex V29() V30() V33() V34() V57() V58() V59() V60() V61() V62() ) Element of NAT : ( ( ) ( V57() V58() V59() V60() V61() V62() V63() ) Element of K19(REAL : ( ( ) ( non zero V46() V57() V58() V59() V63() ) set ) ) : ( ( ) ( ) set ) ) ) : ( ( ) ( complex ) Element of COMPLEX : ( ( ) ( non zero V46() V57() V63() ) set ) ) ) ;

theorem :: SIN_COS3:59

for z1, z2 being ( ( ) ( complex ) Element of COMPLEX : ( ( ) ( non zero V46() V57() V63() ) set ) ) holds
( ((sinh_C : ( ( V6() V18( COMPLEX : ( ( ) ( non zero V46() V57() V63() ) set ) , COMPLEX : ( ( ) ( non zero V46() V57() V63() ) set ) ) ) ( V1() V4( COMPLEX : ( ( ) ( non zero V46() V57() V63() ) set ) ) V5( COMPLEX : ( ( ) ( non zero V46() V57() V63() ) set ) ) V6() non zero total V18( COMPLEX : ( ( ) ( non zero V46() V57() V63() ) set ) , COMPLEX : ( ( ) ( non zero V46() V57() V63() ) set ) ) ) Function of COMPLEX : ( ( ) ( non zero V46() V57() V63() ) set ) , COMPLEX : ( ( ) ( non zero V46() V57() V63() ) set ) ) /. z1 : ( ( ) ( complex ) Element of COMPLEX : ( ( ) ( non zero V46() V57() V63() ) set ) ) ) : ( ( ) ( complex ) Element of COMPLEX : ( ( ) ( non zero V46() V57() V63() ) set ) ) * (sinh_C : ( ( V6() V18( COMPLEX : ( ( ) ( non zero V46() V57() V63() ) set ) , COMPLEX : ( ( ) ( non zero V46() V57() V63() ) set ) ) ) ( V1() V4( COMPLEX : ( ( ) ( non zero V46() V57() V63() ) set ) ) V5( COMPLEX : ( ( ) ( non zero V46() V57() V63() ) set ) ) V6() non zero total V18( COMPLEX : ( ( ) ( non zero V46() V57() V63() ) set ) , COMPLEX : ( ( ) ( non zero V46() V57() V63() ) set ) ) ) Function of COMPLEX : ( ( ) ( non zero V46() V57() V63() ) set ) , COMPLEX : ( ( ) ( non zero V46() V57() V63() ) set ) ) /. z1 : ( ( ) ( complex ) Element of COMPLEX : ( ( ) ( non zero V46() V57() V63() ) set ) ) ) : ( ( ) ( complex ) Element of COMPLEX : ( ( ) ( non zero V46() V57() V63() ) set ) ) ) : ( ( ) ( complex ) Element of COMPLEX : ( ( ) ( non zero V46() V57() V63() ) set ) ) - ((sinh_C : ( ( V6() V18( COMPLEX : ( ( ) ( non zero V46() V57() V63() ) set ) , COMPLEX : ( ( ) ( non zero V46() V57() V63() ) set ) ) ) ( V1() V4( COMPLEX : ( ( ) ( non zero V46() V57() V63() ) set ) ) V5( COMPLEX : ( ( ) ( non zero V46() V57() V63() ) set ) ) V6() non zero total V18( COMPLEX : ( ( ) ( non zero V46() V57() V63() ) set ) , COMPLEX : ( ( ) ( non zero V46() V57() V63() ) set ) ) ) Function of COMPLEX : ( ( ) ( non zero V46() V57() V63() ) set ) , COMPLEX : ( ( ) ( non zero V46() V57() V63() ) set ) ) /. z2 : ( ( ) ( complex ) Element of COMPLEX : ( ( ) ( non zero V46() V57() V63() ) set ) ) ) : ( ( ) ( complex ) Element of COMPLEX : ( ( ) ( non zero V46() V57() V63() ) set ) ) * (sinh_C : ( ( V6() V18( COMPLEX : ( ( ) ( non zero V46() V57() V63() ) set ) , COMPLEX : ( ( ) ( non zero V46() V57() V63() ) set ) ) ) ( V1() V4( COMPLEX : ( ( ) ( non zero V46() V57() V63() ) set ) ) V5( COMPLEX : ( ( ) ( non zero V46() V57() V63() ) set ) ) V6() non zero total V18( COMPLEX : ( ( ) ( non zero V46() V57() V63() ) set ) , COMPLEX : ( ( ) ( non zero V46() V57() V63() ) set ) ) ) Function of COMPLEX : ( ( ) ( non zero V46() V57() V63() ) set ) , COMPLEX : ( ( ) ( non zero V46() V57() V63() ) set ) ) /. z2 : ( ( ) ( complex ) Element of COMPLEX : ( ( ) ( non zero V46() V57() V63() ) set ) ) ) : ( ( ) ( complex ) Element of COMPLEX : ( ( ) ( non zero V46() V57() V63() ) set ) ) ) : ( ( ) ( complex ) Element of COMPLEX : ( ( ) ( non zero V46() V57() V63() ) set ) ) : ( ( ) ( complex ) Element of COMPLEX : ( ( ) ( non zero V46() V57() V63() ) set ) ) = (sinh_C : ( ( V6() V18( COMPLEX : ( ( ) ( non zero V46() V57() V63() ) set ) , COMPLEX : ( ( ) ( non zero V46() V57() V63() ) set ) ) ) ( V1() V4( COMPLEX : ( ( ) ( non zero V46() V57() V63() ) set ) ) V5( COMPLEX : ( ( ) ( non zero V46() V57() V63() ) set ) ) V6() non zero total V18( COMPLEX : ( ( ) ( non zero V46() V57() V63() ) set ) , COMPLEX : ( ( ) ( non zero V46() V57() V63() ) set ) ) ) Function of COMPLEX : ( ( ) ( non zero V46() V57() V63() ) set ) , COMPLEX : ( ( ) ( non zero V46() V57() V63() ) set ) ) /. (z1 : ( ( ) ( complex ) Element of COMPLEX : ( ( ) ( non zero V46() V57() V63() ) set ) ) + z2 : ( ( ) ( complex ) Element of COMPLEX : ( ( ) ( non zero V46() V57() V63() ) set ) ) ) : ( ( ) ( complex ) Element of COMPLEX : ( ( ) ( non zero V46() V57() V63() ) set ) ) ) : ( ( ) ( complex ) Element of COMPLEX : ( ( ) ( non zero V46() V57() V63() ) set ) ) * (sinh_C : ( ( V6() V18( COMPLEX : ( ( ) ( non zero V46() V57() V63() ) set ) , COMPLEX : ( ( ) ( non zero V46() V57() V63() ) set ) ) ) ( V1() V4( COMPLEX : ( ( ) ( non zero V46() V57() V63() ) set ) ) V5( COMPLEX : ( ( ) ( non zero V46() V57() V63() ) set ) ) V6() non zero total V18( COMPLEX : ( ( ) ( non zero V46() V57() V63() ) set ) , COMPLEX : ( ( ) ( non zero V46() V57() V63() ) set ) ) ) Function of COMPLEX : ( ( ) ( non zero V46() V57() V63() ) set ) , COMPLEX : ( ( ) ( non zero V46() V57() V63() ) set ) ) /. (z1 : ( ( ) ( complex ) Element of COMPLEX : ( ( ) ( non zero V46() V57() V63() ) set ) ) - z2 : ( ( ) ( complex ) Element of COMPLEX : ( ( ) ( non zero V46() V57() V63() ) set ) ) ) : ( ( ) ( complex ) Element of COMPLEX : ( ( ) ( non zero V46() V57() V63() ) set ) ) ) : ( ( ) ( complex ) Element of COMPLEX : ( ( ) ( non zero V46() V57() V63() ) set ) ) : ( ( ) ( complex ) Element of COMPLEX : ( ( ) ( non zero V46() V57() V63() ) set ) ) & ((cosh_C : ( ( V6() V18( COMPLEX : ( ( ) ( non zero V46() V57() V63() ) set ) , COMPLEX : ( ( ) ( non zero V46() V57() V63() ) set ) ) ) ( V1() V4( COMPLEX : ( ( ) ( non zero V46() V57() V63() ) set ) ) V5( COMPLEX : ( ( ) ( non zero V46() V57() V63() ) set ) ) V6() non zero total V18( COMPLEX : ( ( ) ( non zero V46() V57() V63() ) set ) , COMPLEX : ( ( ) ( non zero V46() V57() V63() ) set ) ) ) Function of COMPLEX : ( ( ) ( non zero V46() V57() V63() ) set ) , COMPLEX : ( ( ) ( non zero V46() V57() V63() ) set ) ) /. z1 : ( ( ) ( complex ) Element of COMPLEX : ( ( ) ( non zero V46() V57() V63() ) set ) ) ) : ( ( ) ( complex ) Element of COMPLEX : ( ( ) ( non zero V46() V57() V63() ) set ) ) * (cosh_C : ( ( V6() V18( COMPLEX : ( ( ) ( non zero V46() V57() V63() ) set ) , COMPLEX : ( ( ) ( non zero V46() V57() V63() ) set ) ) ) ( V1() V4( COMPLEX : ( ( ) ( non zero V46() V57() V63() ) set ) ) V5( COMPLEX : ( ( ) ( non zero V46() V57() V63() ) set ) ) V6() non zero total V18( COMPLEX : ( ( ) ( non zero V46() V57() V63() ) set ) , COMPLEX : ( ( ) ( non zero V46() V57() V63() ) set ) ) ) Function of COMPLEX : ( ( ) ( non zero V46() V57() V63() ) set ) , COMPLEX : ( ( ) ( non zero V46() V57() V63() ) set ) ) /. z1 : ( ( ) ( complex ) Element of COMPLEX : ( ( ) ( non zero V46() V57() V63() ) set ) ) ) : ( ( ) ( complex ) Element of COMPLEX : ( ( ) ( non zero V46() V57() V63() ) set ) ) ) : ( ( ) ( complex ) Element of COMPLEX : ( ( ) ( non zero V46() V57() V63() ) set ) ) - ((cosh_C : ( ( V6() V18( COMPLEX : ( ( ) ( non zero V46() V57() V63() ) set ) , COMPLEX : ( ( ) ( non zero V46() V57() V63() ) set ) ) ) ( V1() V4( COMPLEX : ( ( ) ( non zero V46() V57() V63() ) set ) ) V5( COMPLEX : ( ( ) ( non zero V46() V57() V63() ) set ) ) V6() non zero total V18( COMPLEX : ( ( ) ( non zero V46() V57() V63() ) set ) , COMPLEX : ( ( ) ( non zero V46() V57() V63() ) set ) ) ) Function of COMPLEX : ( ( ) ( non zero V46() V57() V63() ) set ) , COMPLEX : ( ( ) ( non zero V46() V57() V63() ) set ) ) /. z2 : ( ( ) ( complex ) Element of COMPLEX : ( ( ) ( non zero V46() V57() V63() ) set ) ) ) : ( ( ) ( complex ) Element of COMPLEX : ( ( ) ( non zero V46() V57() V63() ) set ) ) * (cosh_C : ( ( V6() V18( COMPLEX : ( ( ) ( non zero V46() V57() V63() ) set ) , COMPLEX : ( ( ) ( non zero V46() V57() V63() ) set ) ) ) ( V1() V4( COMPLEX : ( ( ) ( non zero V46() V57() V63() ) set ) ) V5( COMPLEX : ( ( ) ( non zero V46() V57() V63() ) set ) ) V6() non zero total V18( COMPLEX : ( ( ) ( non zero V46() V57() V63() ) set ) , COMPLEX : ( ( ) ( non zero V46() V57() V63() ) set ) ) ) Function of COMPLEX : ( ( ) ( non zero V46() V57() V63() ) set ) , COMPLEX : ( ( ) ( non zero V46() V57() V63() ) set ) ) /. z2 : ( ( ) ( complex ) Element of COMPLEX : ( ( ) ( non zero V46() V57() V63() ) set ) ) ) : ( ( ) ( complex ) Element of COMPLEX : ( ( ) ( non zero V46() V57() V63() ) set ) ) ) : ( ( ) ( complex ) Element of COMPLEX : ( ( ) ( non zero V46() V57() V63() ) set ) ) : ( ( ) ( complex ) Element of COMPLEX : ( ( ) ( non zero V46() V57() V63() ) set ) ) = (sinh_C : ( ( V6() V18( COMPLEX : ( ( ) ( non zero V46() V57() V63() ) set ) , COMPLEX : ( ( ) ( non zero V46() V57() V63() ) set ) ) ) ( V1() V4( COMPLEX : ( ( ) ( non zero V46() V57() V63() ) set ) ) V5( COMPLEX : ( ( ) ( non zero V46() V57() V63() ) set ) ) V6() non zero total V18( COMPLEX : ( ( ) ( non zero V46() V57() V63() ) set ) , COMPLEX : ( ( ) ( non zero V46() V57() V63() ) set ) ) ) Function of COMPLEX : ( ( ) ( non zero V46() V57() V63() ) set ) , COMPLEX : ( ( ) ( non zero V46() V57() V63() ) set ) ) /. (z1 : ( ( ) ( complex ) Element of COMPLEX : ( ( ) ( non zero V46() V57() V63() ) set ) ) + z2 : ( ( ) ( complex ) Element of COMPLEX : ( ( ) ( non zero V46() V57() V63() ) set ) ) ) : ( ( ) ( complex ) Element of COMPLEX : ( ( ) ( non zero V46() V57() V63() ) set ) ) ) : ( ( ) ( complex ) Element of COMPLEX : ( ( ) ( non zero V46() V57() V63() ) set ) ) * (sinh_C : ( ( V6() V18( COMPLEX : ( ( ) ( non zero V46() V57() V63() ) set ) , COMPLEX : ( ( ) ( non zero V46() V57() V63() ) set ) ) ) ( V1() V4( COMPLEX : ( ( ) ( non zero V46() V57() V63() ) set ) ) V5( COMPLEX : ( ( ) ( non zero V46() V57() V63() ) set ) ) V6() non zero total V18( COMPLEX : ( ( ) ( non zero V46() V57() V63() ) set ) , COMPLEX : ( ( ) ( non zero V46() V57() V63() ) set ) ) ) Function of COMPLEX : ( ( ) ( non zero V46() V57() V63() ) set ) , COMPLEX : ( ( ) ( non zero V46() V57() V63() ) set ) ) /. (z1 : ( ( ) ( complex ) Element of COMPLEX : ( ( ) ( non zero V46() V57() V63() ) set ) ) - z2 : ( ( ) ( complex ) Element of COMPLEX : ( ( ) ( non zero V46() V57() V63() ) set ) ) ) : ( ( ) ( complex ) Element of COMPLEX : ( ( ) ( non zero V46() V57() V63() ) set ) ) ) : ( ( ) ( complex ) Element of COMPLEX : ( ( ) ( non zero V46() V57() V63() ) set ) ) : ( ( ) ( complex ) Element of COMPLEX : ( ( ) ( non zero V46() V57() V63() ) set ) ) & ((sinh_C : ( ( V6() V18( COMPLEX : ( ( ) ( non zero V46() V57() V63() ) set ) , COMPLEX : ( ( ) ( non zero V46() V57() V63() ) set ) ) ) ( V1() V4( COMPLEX : ( ( ) ( non zero V46() V57() V63() ) set ) ) V5( COMPLEX : ( ( ) ( non zero V46() V57() V63() ) set ) ) V6() non zero total V18( COMPLEX : ( ( ) ( non zero V46() V57() V63() ) set ) , COMPLEX : ( ( ) ( non zero V46() V57() V63() ) set ) ) ) Function of COMPLEX : ( ( ) ( non zero V46() V57() V63() ) set ) , COMPLEX : ( ( ) ( non zero V46() V57() V63() ) set ) ) /. z1 : ( ( ) ( complex ) Element of COMPLEX : ( ( ) ( non zero V46() V57() V63() ) set ) ) ) : ( ( ) ( complex ) Element of COMPLEX : ( ( ) ( non zero V46() V57() V63() ) set ) ) * (sinh_C : ( ( V6() V18( COMPLEX : ( ( ) ( non zero V46() V57() V63() ) set ) , COMPLEX : ( ( ) ( non zero V46() V57() V63() ) set ) ) ) ( V1() V4( COMPLEX : ( ( ) ( non zero V46() V57() V63() ) set ) ) V5( COMPLEX : ( ( ) ( non zero V46() V57() V63() ) set ) ) V6() non zero total V18( COMPLEX : ( ( ) ( non zero V46() V57() V63() ) set ) , COMPLEX : ( ( ) ( non zero V46() V57() V63() ) set ) ) ) Function of COMPLEX : ( ( ) ( non zero V46() V57() V63() ) set ) , COMPLEX : ( ( ) ( non zero V46() V57() V63() ) set ) ) /. z1 : ( ( ) ( complex ) Element of COMPLEX : ( ( ) ( non zero V46() V57() V63() ) set ) ) ) : ( ( ) ( complex ) Element of COMPLEX : ( ( ) ( non zero V46() V57() V63() ) set ) ) ) : ( ( ) ( complex ) Element of COMPLEX : ( ( ) ( non zero V46() V57() V63() ) set ) ) - ((sinh_C : ( ( V6() V18( COMPLEX : ( ( ) ( non zero V46() V57() V63() ) set ) , COMPLEX : ( ( ) ( non zero V46() V57() V63() ) set ) ) ) ( V1() V4( COMPLEX : ( ( ) ( non zero V46() V57() V63() ) set ) ) V5( COMPLEX : ( ( ) ( non zero V46() V57() V63() ) set ) ) V6() non zero total V18( COMPLEX : ( ( ) ( non zero V46() V57() V63() ) set ) , COMPLEX : ( ( ) ( non zero V46() V57() V63() ) set ) ) ) Function of COMPLEX : ( ( ) ( non zero V46() V57() V63() ) set ) , COMPLEX : ( ( ) ( non zero V46() V57() V63() ) set ) ) /. z2 : ( ( ) ( complex ) Element of COMPLEX : ( ( ) ( non zero V46() V57() V63() ) set ) ) ) : ( ( ) ( complex ) Element of COMPLEX : ( ( ) ( non zero V46() V57() V63() ) set ) ) * (sinh_C : ( ( V6() V18( COMPLEX : ( ( ) ( non zero V46() V57() V63() ) set ) , COMPLEX : ( ( ) ( non zero V46() V57() V63() ) set ) ) ) ( V1() V4( COMPLEX : ( ( ) ( non zero V46() V57() V63() ) set ) ) V5( COMPLEX : ( ( ) ( non zero V46() V57() V63() ) set ) ) V6() non zero total V18( COMPLEX : ( ( ) ( non zero V46() V57() V63() ) set ) , COMPLEX : ( ( ) ( non zero V46() V57() V63() ) set ) ) ) Function of COMPLEX : ( ( ) ( non zero V46() V57() V63() ) set ) , COMPLEX : ( ( ) ( non zero V46() V57() V63() ) set ) ) /. z2 : ( ( ) ( complex ) Element of COMPLEX : ( ( ) ( non zero V46() V57() V63() ) set ) ) ) : ( ( ) ( complex ) Element of COMPLEX : ( ( ) ( non zero V46() V57() V63() ) set ) ) ) : ( ( ) ( complex ) Element of COMPLEX : ( ( ) ( non zero V46() V57() V63() ) set ) ) : ( ( ) ( complex ) Element of COMPLEX : ( ( ) ( non zero V46() V57() V63() ) set ) ) = ((cosh_C : ( ( V6() V18( COMPLEX : ( ( ) ( non zero V46() V57() V63() ) set ) , COMPLEX : ( ( ) ( non zero V46() V57() V63() ) set ) ) ) ( V1() V4( COMPLEX : ( ( ) ( non zero V46() V57() V63() ) set ) ) V5( COMPLEX : ( ( ) ( non zero V46() V57() V63() ) set ) ) V6() non zero total V18( COMPLEX : ( ( ) ( non zero V46() V57() V63() ) set ) , COMPLEX : ( ( ) ( non zero V46() V57() V63() ) set ) ) ) Function of COMPLEX : ( ( ) ( non zero V46() V57() V63() ) set ) , COMPLEX : ( ( ) ( non zero V46() V57() V63() ) set ) ) /. z1 : ( ( ) ( complex ) Element of COMPLEX : ( ( ) ( non zero V46() V57() V63() ) set ) ) ) : ( ( ) ( complex ) Element of COMPLEX : ( ( ) ( non zero V46() V57() V63() ) set ) ) * (cosh_C : ( ( V6() V18( COMPLEX : ( ( ) ( non zero V46() V57() V63() ) set ) , COMPLEX : ( ( ) ( non zero V46() V57() V63() ) set ) ) ) ( V1() V4( COMPLEX : ( ( ) ( non zero V46() V57() V63() ) set ) ) V5( COMPLEX : ( ( ) ( non zero V46() V57() V63() ) set ) ) V6() non zero total V18( COMPLEX : ( ( ) ( non zero V46() V57() V63() ) set ) , COMPLEX : ( ( ) ( non zero V46() V57() V63() ) set ) ) ) Function of COMPLEX : ( ( ) ( non zero V46() V57() V63() ) set ) , COMPLEX : ( ( ) ( non zero V46() V57() V63() ) set ) ) /. z1 : ( ( ) ( complex ) Element of COMPLEX : ( ( ) ( non zero V46() V57() V63() ) set ) ) ) : ( ( ) ( complex ) Element of COMPLEX : ( ( ) ( non zero V46() V57() V63() ) set ) ) ) : ( ( ) ( complex ) Element of COMPLEX : ( ( ) ( non zero V46() V57() V63() ) set ) ) - ((cosh_C : ( ( V6() V18( COMPLEX : ( ( ) ( non zero V46() V57() V63() ) set ) , COMPLEX : ( ( ) ( non zero V46() V57() V63() ) set ) ) ) ( V1() V4( COMPLEX : ( ( ) ( non zero V46() V57() V63() ) set ) ) V5( COMPLEX : ( ( ) ( non zero V46() V57() V63() ) set ) ) V6() non zero total V18( COMPLEX : ( ( ) ( non zero V46() V57() V63() ) set ) , COMPLEX : ( ( ) ( non zero V46() V57() V63() ) set ) ) ) Function of COMPLEX : ( ( ) ( non zero V46() V57() V63() ) set ) , COMPLEX : ( ( ) ( non zero V46() V57() V63() ) set ) ) /. z2 : ( ( ) ( complex ) Element of COMPLEX : ( ( ) ( non zero V46() V57() V63() ) set ) ) ) : ( ( ) ( complex ) Element of COMPLEX : ( ( ) ( non zero V46() V57() V63() ) set ) ) * (cosh_C : ( ( V6() V18( COMPLEX : ( ( ) ( non zero V46() V57() V63() ) set ) , COMPLEX : ( ( ) ( non zero V46() V57() V63() ) set ) ) ) ( V1() V4( COMPLEX : ( ( ) ( non zero V46() V57() V63() ) set ) ) V5( COMPLEX : ( ( ) ( non zero V46() V57() V63() ) set ) ) V6() non zero total V18( COMPLEX : ( ( ) ( non zero V46() V57() V63() ) set ) , COMPLEX : ( ( ) ( non zero V46() V57() V63() ) set ) ) ) Function of COMPLEX : ( ( ) ( non zero V46() V57() V63() ) set ) , COMPLEX : ( ( ) ( non zero V46() V57() V63() ) set ) ) /. z2 : ( ( ) ( complex ) Element of COMPLEX : ( ( ) ( non zero V46() V57() V63() ) set ) ) ) : ( ( ) ( complex ) Element of COMPLEX : ( ( ) ( non zero V46() V57() V63() ) set ) ) ) : ( ( ) ( complex ) Element of COMPLEX : ( ( ) ( non zero V46() V57() V63() ) set ) ) : ( ( ) ( complex ) Element of COMPLEX : ( ( ) ( non zero V46() V57() V63() ) set ) ) ) ;

theorem :: SIN_COS3:60

for z1, z2 being ( ( ) ( complex ) Element of COMPLEX : ( ( ) ( non zero V46() V57() V63() ) set ) ) holds
( (cosh_C : ( ( V6() V18( COMPLEX : ( ( ) ( non zero V46() V57() V63() ) set ) , COMPLEX : ( ( ) ( non zero V46() V57() V63() ) set ) ) ) ( V1() V4( COMPLEX : ( ( ) ( non zero V46() V57() V63() ) set ) ) V5( COMPLEX : ( ( ) ( non zero V46() V57() V63() ) set ) ) V6() non zero total V18( COMPLEX : ( ( ) ( non zero V46() V57() V63() ) set ) , COMPLEX : ( ( ) ( non zero V46() V57() V63() ) set ) ) ) Function of COMPLEX : ( ( ) ( non zero V46() V57() V63() ) set ) , COMPLEX : ( ( ) ( non zero V46() V57() V63() ) set ) ) /. (z1 : ( ( ) ( complex ) Element of COMPLEX : ( ( ) ( non zero V46() V57() V63() ) set ) ) + z2 : ( ( ) ( complex ) Element of COMPLEX : ( ( ) ( non zero V46() V57() V63() ) set ) ) ) : ( ( ) ( complex ) Element of COMPLEX : ( ( ) ( non zero V46() V57() V63() ) set ) ) ) : ( ( ) ( complex ) Element of COMPLEX : ( ( ) ( non zero V46() V57() V63() ) set ) ) * (cosh_C : ( ( V6() V18( COMPLEX : ( ( ) ( non zero V46() V57() V63() ) set ) , COMPLEX : ( ( ) ( non zero V46() V57() V63() ) set ) ) ) ( V1() V4( COMPLEX : ( ( ) ( non zero V46() V57() V63() ) set ) ) V5( COMPLEX : ( ( ) ( non zero V46() V57() V63() ) set ) ) V6() non zero total V18( COMPLEX : ( ( ) ( non zero V46() V57() V63() ) set ) , COMPLEX : ( ( ) ( non zero V46() V57() V63() ) set ) ) ) Function of COMPLEX : ( ( ) ( non zero V46() V57() V63() ) set ) , COMPLEX : ( ( ) ( non zero V46() V57() V63() ) set ) ) /. (z1 : ( ( ) ( complex ) Element of COMPLEX : ( ( ) ( non zero V46() V57() V63() ) set ) ) - z2 : ( ( ) ( complex ) Element of COMPLEX : ( ( ) ( non zero V46() V57() V63() ) set ) ) ) : ( ( ) ( complex ) Element of COMPLEX : ( ( ) ( non zero V46() V57() V63() ) set ) ) ) : ( ( ) ( complex ) Element of COMPLEX : ( ( ) ( non zero V46() V57() V63() ) set ) ) : ( ( ) ( complex ) Element of COMPLEX : ( ( ) ( non zero V46() V57() V63() ) set ) ) = ((sinh_C : ( ( V6() V18( COMPLEX : ( ( ) ( non zero V46() V57() V63() ) set ) , COMPLEX : ( ( ) ( non zero V46() V57() V63() ) set ) ) ) ( V1() V4( COMPLEX : ( ( ) ( non zero V46() V57() V63() ) set ) ) V5( COMPLEX : ( ( ) ( non zero V46() V57() V63() ) set ) ) V6() non zero total V18( COMPLEX : ( ( ) ( non zero V46() V57() V63() ) set ) , COMPLEX : ( ( ) ( non zero V46() V57() V63() ) set ) ) ) Function of COMPLEX : ( ( ) ( non zero V46() V57() V63() ) set ) , COMPLEX : ( ( ) ( non zero V46() V57() V63() ) set ) ) /. z1 : ( ( ) ( complex ) Element of COMPLEX : ( ( ) ( non zero V46() V57() V63() ) set ) ) ) : ( ( ) ( complex ) Element of COMPLEX : ( ( ) ( non zero V46() V57() V63() ) set ) ) * (sinh_C : ( ( V6() V18( COMPLEX : ( ( ) ( non zero V46() V57() V63() ) set ) , COMPLEX : ( ( ) ( non zero V46() V57() V63() ) set ) ) ) ( V1() V4( COMPLEX : ( ( ) ( non zero V46() V57() V63() ) set ) ) V5( COMPLEX : ( ( ) ( non zero V46() V57() V63() ) set ) ) V6() non zero total V18( COMPLEX : ( ( ) ( non zero V46() V57() V63() ) set ) , COMPLEX : ( ( ) ( non zero V46() V57() V63() ) set ) ) ) Function of COMPLEX : ( ( ) ( non zero V46() V57() V63() ) set ) , COMPLEX : ( ( ) ( non zero V46() V57() V63() ) set ) ) /. z1 : ( ( ) ( complex ) Element of COMPLEX : ( ( ) ( non zero V46() V57() V63() ) set ) ) ) : ( ( ) ( complex ) Element of COMPLEX : ( ( ) ( non zero V46() V57() V63() ) set ) ) ) : ( ( ) ( complex ) Element of COMPLEX : ( ( ) ( non zero V46() V57() V63() ) set ) ) + ((cosh_C : ( ( V6() V18( COMPLEX : ( ( ) ( non zero V46() V57() V63() ) set ) , COMPLEX : ( ( ) ( non zero V46() V57() V63() ) set ) ) ) ( V1() V4( COMPLEX : ( ( ) ( non zero V46() V57() V63() ) set ) ) V5( COMPLEX : ( ( ) ( non zero V46() V57() V63() ) set ) ) V6() non zero total V18( COMPLEX : ( ( ) ( non zero V46() V57() V63() ) set ) , COMPLEX : ( ( ) ( non zero V46() V57() V63() ) set ) ) ) Function of COMPLEX : ( ( ) ( non zero V46() V57() V63() ) set ) , COMPLEX : ( ( ) ( non zero V46() V57() V63() ) set ) ) /. z2 : ( ( ) ( complex ) Element of COMPLEX : ( ( ) ( non zero V46() V57() V63() ) set ) ) ) : ( ( ) ( complex ) Element of COMPLEX : ( ( ) ( non zero V46() V57() V63() ) set ) ) * (cosh_C : ( ( V6() V18( COMPLEX : ( ( ) ( non zero V46() V57() V63() ) set ) , COMPLEX : ( ( ) ( non zero V46() V57() V63() ) set ) ) ) ( V1() V4( COMPLEX : ( ( ) ( non zero V46() V57() V63() ) set ) ) V5( COMPLEX : ( ( ) ( non zero V46() V57() V63() ) set ) ) V6() non zero total V18( COMPLEX : ( ( ) ( non zero V46() V57() V63() ) set ) , COMPLEX : ( ( ) ( non zero V46() V57() V63() ) set ) ) ) Function of COMPLEX : ( ( ) ( non zero V46() V57() V63() ) set ) , COMPLEX : ( ( ) ( non zero V46() V57() V63() ) set ) ) /. z2 : ( ( ) ( complex ) Element of COMPLEX : ( ( ) ( non zero V46() V57() V63() ) set ) ) ) : ( ( ) ( complex ) Element of COMPLEX : ( ( ) ( non zero V46() V57() V63() ) set ) ) ) : ( ( ) ( complex ) Element of COMPLEX : ( ( ) ( non zero V46() V57() V63() ) set ) ) : ( ( ) ( complex ) Element of COMPLEX : ( ( ) ( non zero V46() V57() V63() ) set ) ) & (cosh_C : ( ( V6() V18( COMPLEX : ( ( ) ( non zero V46() V57() V63() ) set ) , COMPLEX : ( ( ) ( non zero V46() V57() V63() ) set ) ) ) ( V1() V4( COMPLEX : ( ( ) ( non zero V46() V57() V63() ) set ) ) V5( COMPLEX : ( ( ) ( non zero V46() V57() V63() ) set ) ) V6() non zero total V18( COMPLEX : ( ( ) ( non zero V46() V57() V63() ) set ) , COMPLEX : ( ( ) ( non zero V46() V57() V63() ) set ) ) ) Function of COMPLEX : ( ( ) ( non zero V46() V57() V63() ) set ) , COMPLEX : ( ( ) ( non zero V46() V57() V63() ) set ) ) /. (z1 : ( ( ) ( complex ) Element of COMPLEX : ( ( ) ( non zero V46() V57() V63() ) set ) ) + z2 : ( ( ) ( complex ) Element of COMPLEX : ( ( ) ( non zero V46() V57() V63() ) set ) ) ) : ( ( ) ( complex ) Element of COMPLEX : ( ( ) ( non zero V46() V57() V63() ) set ) ) ) : ( ( ) ( complex ) Element of COMPLEX : ( ( ) ( non zero V46() V57() V63() ) set ) ) * (cosh_C : ( ( V6() V18( COMPLEX : ( ( ) ( non zero V46() V57() V63() ) set ) , COMPLEX : ( ( ) ( non zero V46() V57() V63() ) set ) ) ) ( V1() V4( COMPLEX : ( ( ) ( non zero V46() V57() V63() ) set ) ) V5( COMPLEX : ( ( ) ( non zero V46() V57() V63() ) set ) ) V6() non zero total V18( COMPLEX : ( ( ) ( non zero V46() V57() V63() ) set ) , COMPLEX : ( ( ) ( non zero V46() V57() V63() ) set ) ) ) Function of COMPLEX : ( ( ) ( non zero V46() V57() V63() ) set ) , COMPLEX : ( ( ) ( non zero V46() V57() V63() ) set ) ) /. (z1 : ( ( ) ( complex ) Element of COMPLEX : ( ( ) ( non zero V46() V57() V63() ) set ) ) - z2 : ( ( ) ( complex ) Element of COMPLEX : ( ( ) ( non zero V46() V57() V63() ) set ) ) ) : ( ( ) ( complex ) Element of COMPLEX : ( ( ) ( non zero V46() V57() V63() ) set ) ) ) : ( ( ) ( complex ) Element of COMPLEX : ( ( ) ( non zero V46() V57() V63() ) set ) ) : ( ( ) ( complex ) Element of COMPLEX : ( ( ) ( non zero V46() V57() V63() ) set ) ) = ((cosh_C : ( ( V6() V18( COMPLEX : ( ( ) ( non zero V46() V57() V63() ) set ) , COMPLEX : ( ( ) ( non zero V46() V57() V63() ) set ) ) ) ( V1() V4( COMPLEX : ( ( ) ( non zero V46() V57() V63() ) set ) ) V5( COMPLEX : ( ( ) ( non zero V46() V57() V63() ) set ) ) V6() non zero total V18( COMPLEX : ( ( ) ( non zero V46() V57() V63() ) set ) , COMPLEX : ( ( ) ( non zero V46() V57() V63() ) set ) ) ) Function of COMPLEX : ( ( ) ( non zero V46() V57() V63() ) set ) , COMPLEX : ( ( ) ( non zero V46() V57() V63() ) set ) ) /. z1 : ( ( ) ( complex ) Element of COMPLEX : ( ( ) ( non zero V46() V57() V63() ) set ) ) ) : ( ( ) ( complex ) Element of COMPLEX : ( ( ) ( non zero V46() V57() V63() ) set ) ) * (cosh_C : ( ( V6() V18( COMPLEX : ( ( ) ( non zero V46() V57() V63() ) set ) , COMPLEX : ( ( ) ( non zero V46() V57() V63() ) set ) ) ) ( V1() V4( COMPLEX : ( ( ) ( non zero V46() V57() V63() ) set ) ) V5( COMPLEX : ( ( ) ( non zero V46() V57() V63() ) set ) ) V6() non zero total V18( COMPLEX : ( ( ) ( non zero V46() V57() V63() ) set ) , COMPLEX : ( ( ) ( non zero V46() V57() V63() ) set ) ) ) Function of COMPLEX : ( ( ) ( non zero V46() V57() V63() ) set ) , COMPLEX : ( ( ) ( non zero V46() V57() V63() ) set ) ) /. z1 : ( ( ) ( complex ) Element of COMPLEX : ( ( ) ( non zero V46() V57() V63() ) set ) ) ) : ( ( ) ( complex ) Element of COMPLEX : ( ( ) ( non zero V46() V57() V63() ) set ) ) ) : ( ( ) ( complex ) Element of COMPLEX : ( ( ) ( non zero V46() V57() V63() ) set ) ) + ((sinh_C : ( ( V6() V18( COMPLEX : ( ( ) ( non zero V46() V57() V63() ) set ) , COMPLEX : ( ( ) ( non zero V46() V57() V63() ) set ) ) ) ( V1() V4( COMPLEX : ( ( ) ( non zero V46() V57() V63() ) set ) ) V5( COMPLEX : ( ( ) ( non zero V46() V57() V63() ) set ) ) V6() non zero total V18( COMPLEX : ( ( ) ( non zero V46() V57() V63() ) set ) , COMPLEX : ( ( ) ( non zero V46() V57() V63() ) set ) ) ) Function of COMPLEX : ( ( ) ( non zero V46() V57() V63() ) set ) , COMPLEX : ( ( ) ( non zero V46() V57() V63() ) set ) ) /. z2 : ( ( ) ( complex ) Element of COMPLEX : ( ( ) ( non zero V46() V57() V63() ) set ) ) ) : ( ( ) ( complex ) Element of COMPLEX : ( ( ) ( non zero V46() V57() V63() ) set ) ) * (sinh_C : ( ( V6() V18( COMPLEX : ( ( ) ( non zero V46() V57() V63() ) set ) , COMPLEX : ( ( ) ( non zero V46() V57() V63() ) set ) ) ) ( V1() V4( COMPLEX : ( ( ) ( non zero V46() V57() V63() ) set ) ) V5( COMPLEX : ( ( ) ( non zero V46() V57() V63() ) set ) ) V6() non zero total V18( COMPLEX : ( ( ) ( non zero V46() V57() V63() ) set ) , COMPLEX : ( ( ) ( non zero V46() V57() V63() ) set ) ) ) Function of COMPLEX : ( ( ) ( non zero V46() V57() V63() ) set ) , COMPLEX : ( ( ) ( non zero V46() V57() V63() ) set ) ) /. z2 : ( ( ) ( complex ) Element of COMPLEX : ( ( ) ( non zero V46() V57() V63() ) set ) ) ) : ( ( ) ( complex ) Element of COMPLEX : ( ( ) ( non zero V46() V57() V63() ) set ) ) ) : ( ( ) ( complex ) Element of COMPLEX : ( ( ) ( non zero V46() V57() V63() ) set ) ) : ( ( ) ( complex ) Element of COMPLEX : ( ( ) ( non zero V46() V57() V63() ) set ) ) & ((sinh_C : ( ( V6() V18( COMPLEX : ( ( ) ( non zero V46() V57() V63() ) set ) , COMPLEX : ( ( ) ( non zero V46() V57() V63() ) set ) ) ) ( V1() V4( COMPLEX : ( ( ) ( non zero V46() V57() V63() ) set ) ) V5( COMPLEX : ( ( ) ( non zero V46() V57() V63() ) set ) ) V6() non zero total V18( COMPLEX : ( ( ) ( non zero V46() V57() V63() ) set ) , COMPLEX : ( ( ) ( non zero V46() V57() V63() ) set ) ) ) Function of COMPLEX : ( ( ) ( non zero V46() V57() V63() ) set ) , COMPLEX : ( ( ) ( non zero V46() V57() V63() ) set ) ) /. z1 : ( ( ) ( complex ) Element of COMPLEX : ( ( ) ( non zero V46() V57() V63() ) set ) ) ) : ( ( ) ( complex ) Element of COMPLEX : ( ( ) ( non zero V46() V57() V63() ) set ) ) * (sinh_C : ( ( V6() V18( COMPLEX : ( ( ) ( non zero V46() V57() V63() ) set ) , COMPLEX : ( ( ) ( non zero V46() V57() V63() ) set ) ) ) ( V1() V4( COMPLEX : ( ( ) ( non zero V46() V57() V63() ) set ) ) V5( COMPLEX : ( ( ) ( non zero V46() V57() V63() ) set ) ) V6() non zero total V18( COMPLEX : ( ( ) ( non zero V46() V57() V63() ) set ) , COMPLEX : ( ( ) ( non zero V46() V57() V63() ) set ) ) ) Function of COMPLEX : ( ( ) ( non zero V46() V57() V63() ) set ) , COMPLEX : ( ( ) ( non zero V46() V57() V63() ) set ) ) /. z1 : ( ( ) ( complex ) Element of COMPLEX : ( ( ) ( non zero V46() V57() V63() ) set ) ) ) : ( ( ) ( complex ) Element of COMPLEX : ( ( ) ( non zero V46() V57() V63() ) set ) ) ) : ( ( ) ( complex ) Element of COMPLEX : ( ( ) ( non zero V46() V57() V63() ) set ) ) + ((cosh_C : ( ( V6() V18( COMPLEX : ( ( ) ( non zero V46() V57() V63() ) set ) , COMPLEX : ( ( ) ( non zero V46() V57() V63() ) set ) ) ) ( V1() V4( COMPLEX : ( ( ) ( non zero V46() V57() V63() ) set ) ) V5( COMPLEX : ( ( ) ( non zero V46() V57() V63() ) set ) ) V6() non zero total V18( COMPLEX : ( ( ) ( non zero V46() V57() V63() ) set ) , COMPLEX : ( ( ) ( non zero V46() V57() V63() ) set ) ) ) Function of COMPLEX : ( ( ) ( non zero V46() V57() V63() ) set ) , COMPLEX : ( ( ) ( non zero V46() V57() V63() ) set ) ) /. z2 : ( ( ) ( complex ) Element of COMPLEX : ( ( ) ( non zero V46() V57() V63() ) set ) ) ) : ( ( ) ( complex ) Element of COMPLEX : ( ( ) ( non zero V46() V57() V63() ) set ) ) * (cosh_C : ( ( V6() V18( COMPLEX : ( ( ) ( non zero V46() V57() V63() ) set ) , COMPLEX : ( ( ) ( non zero V46() V57() V63() ) set ) ) ) ( V1() V4( COMPLEX : ( ( ) ( non zero V46() V57() V63() ) set ) ) V5( COMPLEX : ( ( ) ( non zero V46() V57() V63() ) set ) ) V6() non zero total V18( COMPLEX : ( ( ) ( non zero V46() V57() V63() ) set ) , COMPLEX : ( ( ) ( non zero V46() V57() V63() ) set ) ) ) Function of COMPLEX : ( ( ) ( non zero V46() V57() V63() ) set ) , COMPLEX : ( ( ) ( non zero V46() V57() V63() ) set ) ) /. z2 : ( ( ) ( complex ) Element of COMPLEX : ( ( ) ( non zero V46() V57() V63() ) set ) ) ) : ( ( ) ( complex ) Element of COMPLEX : ( ( ) ( non zero V46() V57() V63() ) set ) ) ) : ( ( ) ( complex ) Element of COMPLEX : ( ( ) ( non zero V46() V57() V63() ) set ) ) : ( ( ) ( complex ) Element of COMPLEX : ( ( ) ( non zero V46() V57() V63() ) set ) ) = ((cosh_C : ( ( V6() V18( COMPLEX : ( ( ) ( non zero V46() V57() V63() ) set ) , COMPLEX : ( ( ) ( non zero V46() V57() V63() ) set ) ) ) ( V1() V4( COMPLEX : ( ( ) ( non zero V46() V57() V63() ) set ) ) V5( COMPLEX : ( ( ) ( non zero V46() V57() V63() ) set ) ) V6() non zero total V18( COMPLEX : ( ( ) ( non zero V46() V57() V63() ) set ) , COMPLEX : ( ( ) ( non zero V46() V57() V63() ) set ) ) ) Function of COMPLEX : ( ( ) ( non zero V46() V57() V63() ) set ) , COMPLEX : ( ( ) ( non zero V46() V57() V63() ) set ) ) /. z1 : ( ( ) ( complex ) Element of COMPLEX : ( ( ) ( non zero V46() V57() V63() ) set ) ) ) : ( ( ) ( complex ) Element of COMPLEX : ( ( ) ( non zero V46() V57() V63() ) set ) ) * (cosh_C : ( ( V6() V18( COMPLEX : ( ( ) ( non zero V46() V57() V63() ) set ) , COMPLEX : ( ( ) ( non zero V46() V57() V63() ) set ) ) ) ( V1() V4( COMPLEX : ( ( ) ( non zero V46() V57() V63() ) set ) ) V5( COMPLEX : ( ( ) ( non zero V46() V57() V63() ) set ) ) V6() non zero total V18( COMPLEX : ( ( ) ( non zero V46() V57() V63() ) set ) , COMPLEX : ( ( ) ( non zero V46() V57() V63() ) set ) ) ) Function of COMPLEX : ( ( ) ( non zero V46() V57() V63() ) set ) , COMPLEX : ( ( ) ( non zero V46() V57() V63() ) set ) ) /. z1 : ( ( ) ( complex ) Element of COMPLEX : ( ( ) ( non zero V46() V57() V63() ) set ) ) ) : ( ( ) ( complex ) Element of COMPLEX : ( ( ) ( non zero V46() V57() V63() ) set ) ) ) : ( ( ) ( complex ) Element of COMPLEX : ( ( ) ( non zero V46() V57() V63() ) set ) ) + ((sinh_C : ( ( V6() V18( COMPLEX : ( ( ) ( non zero V46() V57() V63() ) set ) , COMPLEX : ( ( ) ( non zero V46() V57() V63() ) set ) ) ) ( V1() V4( COMPLEX : ( ( ) ( non zero V46() V57() V63() ) set ) ) V5( COMPLEX : ( ( ) ( non zero V46() V57() V63() ) set ) ) V6() non zero total V18( COMPLEX : ( ( ) ( non zero V46() V57() V63() ) set ) , COMPLEX : ( ( ) ( non zero V46() V57() V63() ) set ) ) ) Function of COMPLEX : ( ( ) ( non zero V46() V57() V63() ) set ) , COMPLEX : ( ( ) ( non zero V46() V57() V63() ) set ) ) /. z2 : ( ( ) ( complex ) Element of COMPLEX : ( ( ) ( non zero V46() V57() V63() ) set ) ) ) : ( ( ) ( complex ) Element of COMPLEX : ( ( ) ( non zero V46() V57() V63() ) set ) ) * (sinh_C : ( ( V6() V18( COMPLEX : ( ( ) ( non zero V46() V57() V63() ) set ) , COMPLEX : ( ( ) ( non zero V46() V57() V63() ) set ) ) ) ( V1() V4( COMPLEX : ( ( ) ( non zero V46() V57() V63() ) set ) ) V5( COMPLEX : ( ( ) ( non zero V46() V57() V63() ) set ) ) V6() non zero total V18( COMPLEX : ( ( ) ( non zero V46() V57() V63() ) set ) , COMPLEX : ( ( ) ( non zero V46() V57() V63() ) set ) ) ) Function of COMPLEX : ( ( ) ( non zero V46() V57() V63() ) set ) , COMPLEX : ( ( ) ( non zero V46() V57() V63() ) set ) ) /. z2 : ( ( ) ( complex ) Element of COMPLEX : ( ( ) ( non zero V46() V57() V63() ) set ) ) ) : ( ( ) ( complex ) Element of COMPLEX : ( ( ) ( non zero V46() V57() V63() ) set ) ) ) : ( ( ) ( complex ) Element of COMPLEX : ( ( ) ( non zero V46() V57() V63() ) set ) ) : ( ( ) ( complex ) Element of COMPLEX : ( ( ) ( non zero V46() V57() V63() ) set ) ) ) ;

theorem :: SIN_COS3:61

for z1, z2 being ( ( ) ( complex ) Element of COMPLEX : ( ( ) ( non zero V46() V57() V63() ) set ) ) holds
( (sinh_C : ( ( V6() V18( COMPLEX : ( ( ) ( non zero V46() V57() V63() ) set ) , COMPLEX : ( ( ) ( non zero V46() V57() V63() ) set ) ) ) ( V1() V4( COMPLEX : ( ( ) ( non zero V46() V57() V63() ) set ) ) V5( COMPLEX : ( ( ) ( non zero V46() V57() V63() ) set ) ) V6() non zero total V18( COMPLEX : ( ( ) ( non zero V46() V57() V63() ) set ) , COMPLEX : ( ( ) ( non zero V46() V57() V63() ) set ) ) ) Function of COMPLEX : ( ( ) ( non zero V46() V57() V63() ) set ) , COMPLEX : ( ( ) ( non zero V46() V57() V63() ) set ) ) /. (2 : ( ( ) ( non zero natural complex V29() V30() V33() V34() V57() V58() V59() V60() V61() V62() ) Element of NAT : ( ( ) ( V57() V58() V59() V60() V61() V62() V63() ) Element of K19(REAL : ( ( ) ( non zero V46() V57() V58() V59() V63() ) set ) ) : ( ( ) ( ) set ) ) ) * z1 : ( ( ) ( complex ) Element of COMPLEX : ( ( ) ( non zero V46() V57() V63() ) set ) ) ) : ( ( ) ( complex ) Element of COMPLEX : ( ( ) ( non zero V46() V57() V63() ) set ) ) ) : ( ( ) ( complex ) Element of COMPLEX : ( ( ) ( non zero V46() V57() V63() ) set ) ) + (sinh_C : ( ( V6() V18( COMPLEX : ( ( ) ( non zero V46() V57() V63() ) set ) , COMPLEX : ( ( ) ( non zero V46() V57() V63() ) set ) ) ) ( V1() V4( COMPLEX : ( ( ) ( non zero V46() V57() V63() ) set ) ) V5( COMPLEX : ( ( ) ( non zero V46() V57() V63() ) set ) ) V6() non zero total V18( COMPLEX : ( ( ) ( non zero V46() V57() V63() ) set ) , COMPLEX : ( ( ) ( non zero V46() V57() V63() ) set ) ) ) Function of COMPLEX : ( ( ) ( non zero V46() V57() V63() ) set ) , COMPLEX : ( ( ) ( non zero V46() V57() V63() ) set ) ) /. (2 : ( ( ) ( non zero natural complex V29() V30() V33() V34() V57() V58() V59() V60() V61() V62() ) Element of NAT : ( ( ) ( V57() V58() V59() V60() V61() V62() V63() ) Element of K19(REAL : ( ( ) ( non zero V46() V57() V58() V59() V63() ) set ) ) : ( ( ) ( ) set ) ) ) * z2 : ( ( ) ( complex ) Element of COMPLEX : ( ( ) ( non zero V46() V57() V63() ) set ) ) ) : ( ( ) ( complex ) Element of COMPLEX : ( ( ) ( non zero V46() V57() V63() ) set ) ) ) : ( ( ) ( complex ) Element of COMPLEX : ( ( ) ( non zero V46() V57() V63() ) set ) ) : ( ( ) ( complex ) Element of COMPLEX : ( ( ) ( non zero V46() V57() V63() ) set ) ) = (2 : ( ( ) ( non zero natural complex V29() V30() V33() V34() V57() V58() V59() V60() V61() V62() ) Element of NAT : ( ( ) ( V57() V58() V59() V60() V61() V62() V63() ) Element of K19(REAL : ( ( ) ( non zero V46() V57() V58() V59() V63() ) set ) ) : ( ( ) ( ) set ) ) ) * (sinh_C : ( ( V6() V18( COMPLEX : ( ( ) ( non zero V46() V57() V63() ) set ) , COMPLEX : ( ( ) ( non zero V46() V57() V63() ) set ) ) ) ( V1() V4( COMPLEX : ( ( ) ( non zero V46() V57() V63() ) set ) ) V5( COMPLEX : ( ( ) ( non zero V46() V57() V63() ) set ) ) V6() non zero total V18( COMPLEX : ( ( ) ( non zero V46() V57() V63() ) set ) , COMPLEX : ( ( ) ( non zero V46() V57() V63() ) set ) ) ) Function of COMPLEX : ( ( ) ( non zero V46() V57() V63() ) set ) , COMPLEX : ( ( ) ( non zero V46() V57() V63() ) set ) ) /. (z1 : ( ( ) ( complex ) Element of COMPLEX : ( ( ) ( non zero V46() V57() V63() ) set ) ) + z2 : ( ( ) ( complex ) Element of COMPLEX : ( ( ) ( non zero V46() V57() V63() ) set ) ) ) : ( ( ) ( complex ) Element of COMPLEX : ( ( ) ( non zero V46() V57() V63() ) set ) ) ) : ( ( ) ( complex ) Element of COMPLEX : ( ( ) ( non zero V46() V57() V63() ) set ) ) ) : ( ( ) ( complex ) Element of COMPLEX : ( ( ) ( non zero V46() V57() V63() ) set ) ) * (cosh_C : ( ( V6() V18( COMPLEX : ( ( ) ( non zero V46() V57() V63() ) set ) , COMPLEX : ( ( ) ( non zero V46() V57() V63() ) set ) ) ) ( V1() V4( COMPLEX : ( ( ) ( non zero V46() V57() V63() ) set ) ) V5( COMPLEX : ( ( ) ( non zero V46() V57() V63() ) set ) ) V6() non zero total V18( COMPLEX : ( ( ) ( non zero V46() V57() V63() ) set ) , COMPLEX : ( ( ) ( non zero V46() V57() V63() ) set ) ) ) Function of COMPLEX : ( ( ) ( non zero V46() V57() V63() ) set ) , COMPLEX : ( ( ) ( non zero V46() V57() V63() ) set ) ) /. (z1 : ( ( ) ( complex ) Element of COMPLEX : ( ( ) ( non zero V46() V57() V63() ) set ) ) - z2 : ( ( ) ( complex ) Element of COMPLEX : ( ( ) ( non zero V46() V57() V63() ) set ) ) ) : ( ( ) ( complex ) Element of COMPLEX : ( ( ) ( non zero V46() V57() V63() ) set ) ) ) : ( ( ) ( complex ) Element of COMPLEX : ( ( ) ( non zero V46() V57() V63() ) set ) ) : ( ( ) ( complex ) Element of COMPLEX : ( ( ) ( non zero V46() V57() V63() ) set ) ) & (sinh_C : ( ( V6() V18( COMPLEX : ( ( ) ( non zero V46() V57() V63() ) set ) , COMPLEX : ( ( ) ( non zero V46() V57() V63() ) set ) ) ) ( V1() V4( COMPLEX : ( ( ) ( non zero V46() V57() V63() ) set ) ) V5( COMPLEX : ( ( ) ( non zero V46() V57() V63() ) set ) ) V6() non zero total V18( COMPLEX : ( ( ) ( non zero V46() V57() V63() ) set ) , COMPLEX : ( ( ) ( non zero V46() V57() V63() ) set ) ) ) Function of COMPLEX : ( ( ) ( non zero V46() V57() V63() ) set ) , COMPLEX : ( ( ) ( non zero V46() V57() V63() ) set ) ) /. (2 : ( ( ) ( non zero natural complex V29() V30() V33() V34() V57() V58() V59() V60() V61() V62() ) Element of NAT : ( ( ) ( V57() V58() V59() V60() V61() V62() V63() ) Element of K19(REAL : ( ( ) ( non zero V46() V57() V58() V59() V63() ) set ) ) : ( ( ) ( ) set ) ) ) * z1 : ( ( ) ( complex ) Element of COMPLEX : ( ( ) ( non zero V46() V57() V63() ) set ) ) ) : ( ( ) ( complex ) Element of COMPLEX : ( ( ) ( non zero V46() V57() V63() ) set ) ) ) : ( ( ) ( complex ) Element of COMPLEX : ( ( ) ( non zero V46() V57() V63() ) set ) ) - (sinh_C : ( ( V6() V18( COMPLEX : ( ( ) ( non zero V46() V57() V63() ) set ) , COMPLEX : ( ( ) ( non zero V46() V57() V63() ) set ) ) ) ( V1() V4( COMPLEX : ( ( ) ( non zero V46() V57() V63() ) set ) ) V5( COMPLEX : ( ( ) ( non zero V46() V57() V63() ) set ) ) V6() non zero total V18( COMPLEX : ( ( ) ( non zero V46() V57() V63() ) set ) , COMPLEX : ( ( ) ( non zero V46() V57() V63() ) set ) ) ) Function of COMPLEX : ( ( ) ( non zero V46() V57() V63() ) set ) , COMPLEX : ( ( ) ( non zero V46() V57() V63() ) set ) ) /. (2 : ( ( ) ( non zero natural complex V29() V30() V33() V34() V57() V58() V59() V60() V61() V62() ) Element of NAT : ( ( ) ( V57() V58() V59() V60() V61() V62() V63() ) Element of K19(REAL : ( ( ) ( non zero V46() V57() V58() V59() V63() ) set ) ) : ( ( ) ( ) set ) ) ) * z2 : ( ( ) ( complex ) Element of COMPLEX : ( ( ) ( non zero V46() V57() V63() ) set ) ) ) : ( ( ) ( complex ) Element of COMPLEX : ( ( ) ( non zero V46() V57() V63() ) set ) ) ) : ( ( ) ( complex ) Element of COMPLEX : ( ( ) ( non zero V46() V57() V63() ) set ) ) : ( ( ) ( complex ) Element of COMPLEX : ( ( ) ( non zero V46() V57() V63() ) set ) ) = (2 : ( ( ) ( non zero natural complex V29() V30() V33() V34() V57() V58() V59() V60() V61() V62() ) Element of NAT : ( ( ) ( V57() V58() V59() V60() V61() V62() V63() ) Element of K19(REAL : ( ( ) ( non zero V46() V57() V58() V59() V63() ) set ) ) : ( ( ) ( ) set ) ) ) * (sinh_C : ( ( V6() V18( COMPLEX : ( ( ) ( non zero V46() V57() V63() ) set ) , COMPLEX : ( ( ) ( non zero V46() V57() V63() ) set ) ) ) ( V1() V4( COMPLEX : ( ( ) ( non zero V46() V57() V63() ) set ) ) V5( COMPLEX : ( ( ) ( non zero V46() V57() V63() ) set ) ) V6() non zero total V18( COMPLEX : ( ( ) ( non zero V46() V57() V63() ) set ) , COMPLEX : ( ( ) ( non zero V46() V57() V63() ) set ) ) ) Function of COMPLEX : ( ( ) ( non zero V46() V57() V63() ) set ) , COMPLEX : ( ( ) ( non zero V46() V57() V63() ) set ) ) /. (z1 : ( ( ) ( complex ) Element of COMPLEX : ( ( ) ( non zero V46() V57() V63() ) set ) ) - z2 : ( ( ) ( complex ) Element of COMPLEX : ( ( ) ( non zero V46() V57() V63() ) set ) ) ) : ( ( ) ( complex ) Element of COMPLEX : ( ( ) ( non zero V46() V57() V63() ) set ) ) ) : ( ( ) ( complex ) Element of COMPLEX : ( ( ) ( non zero V46() V57() V63() ) set ) ) ) : ( ( ) ( complex ) Element of COMPLEX : ( ( ) ( non zero V46() V57() V63() ) set ) ) * (cosh_C : ( ( V6() V18( COMPLEX : ( ( ) ( non zero V46() V57() V63() ) set ) , COMPLEX : ( ( ) ( non zero V46() V57() V63() ) set ) ) ) ( V1() V4( COMPLEX : ( ( ) ( non zero V46() V57() V63() ) set ) ) V5( COMPLEX : ( ( ) ( non zero V46() V57() V63() ) set ) ) V6() non zero total V18( COMPLEX : ( ( ) ( non zero V46() V57() V63() ) set ) , COMPLEX : ( ( ) ( non zero V46() V57() V63() ) set ) ) ) Function of COMPLEX : ( ( ) ( non zero V46() V57() V63() ) set ) , COMPLEX : ( ( ) ( non zero V46() V57() V63() ) set ) ) /. (z1 : ( ( ) ( complex ) Element of COMPLEX : ( ( ) ( non zero V46() V57() V63() ) set ) ) + z2 : ( ( ) ( complex ) Element of COMPLEX : ( ( ) ( non zero V46() V57() V63() ) set ) ) ) : ( ( ) ( complex ) Element of COMPLEX : ( ( ) ( non zero V46() V57() V63() ) set ) ) ) : ( ( ) ( complex ) Element of COMPLEX : ( ( ) ( non zero V46() V57() V63() ) set ) ) : ( ( ) ( complex ) Element of COMPLEX : ( ( ) ( non zero V46() V57() V63() ) set ) ) ) ;

theorem :: SIN_COS3:62