:: SIN_COS2 semantic presentation

begin

theorem :: SIN_COS2:1
for p, r being ( ( real ) ( V30() real ext-real ) number ) st p : ( ( real ) ( V30() real ext-real ) number ) >= 0 : ( ( ) ( empty ordinal natural V30() real ext-real non positive non negative V35() V36() V52() V53() V54() V55() V56() V57() V58() ) Element of NAT : ( ( ) ( V52() V53() V54() V55() V56() V57() V58() ) Element of K19(REAL : ( ( ) ( non empty V52() V53() V54() V58() V66() ) set ) ) : ( ( ) ( ) set ) ) ) & r : ( ( real ) ( V30() real ext-real ) number ) >= 0 : ( ( ) ( empty ordinal natural V30() real ext-real non positive non negative V35() V36() V52() V53() V54() V55() V56() V57() V58() ) Element of NAT : ( ( ) ( V52() V53() V54() V55() V56() V57() V58() ) Element of K19(REAL : ( ( ) ( non empty V52() V53() V54() V58() V66() ) set ) ) : ( ( ) ( ) set ) ) ) holds
p : ( ( real ) ( V30() real ext-real ) number ) + r : ( ( real ) ( V30() real ext-real ) number ) : ( ( ) ( V30() real ext-real ) Element of REAL : ( ( ) ( non empty V52() V53() V54() V58() V66() ) set ) ) >= 2 : ( ( ) ( non empty ordinal natural V30() real ext-real positive non negative V35() V36() V52() V53() V54() V55() V56() V57() ) Element of NAT : ( ( ) ( V52() V53() V54() V55() V56() V57() V58() ) Element of K19(REAL : ( ( ) ( non empty V52() V53() V54() V58() V66() ) set ) ) : ( ( ) ( ) set ) ) ) * (sqrt (p : ( ( real ) ( V30() real ext-real ) number ) * r : ( ( real ) ( V30() real ext-real ) number ) ) : ( ( ) ( V30() real ext-real ) Element of REAL : ( ( ) ( non empty V52() V53() V54() V58() V66() ) set ) ) ) : ( ( ) ( V30() real ext-real ) Element of REAL : ( ( ) ( non empty V52() V53() V54() V58() V66() ) set ) ) : ( ( ) ( V30() real ext-real ) Element of REAL : ( ( ) ( non empty V52() V53() V54() V58() V66() ) set ) ) ;

theorem :: SIN_COS2:2
sin : ( ( V6() quasi_total ) ( V1() V4( REAL : ( ( ) ( non empty V52() V53() V54() V58() V66() ) set ) ) V5( REAL : ( ( ) ( non empty V52() V53() V54() V58() V66() ) set ) ) V6() non empty total quasi_total complex-valued ext-real-valued real-valued continuous ) Element of K19(K20(REAL : ( ( ) ( non empty V52() V53() V54() V58() V66() ) set ) ,REAL : ( ( ) ( non empty V52() V53() V54() V58() V66() ) set ) ) : ( ( ) ( complex-valued ext-real-valued real-valued ) set ) ) : ( ( ) ( ) set ) ) | ].0 : ( ( ) ( empty ordinal natural V30() real ext-real non positive non negative V35() V36() V52() V53() V54() V55() V56() V57() V58() ) Element of NAT : ( ( ) ( V52() V53() V54() V55() V56() V57() V58() ) Element of K19(REAL : ( ( ) ( non empty V52() V53() V54() V58() V66() ) set ) ) : ( ( ) ( ) set ) ) ) ,(PI : ( ( ) ( V30() real ext-real ) Element of REAL : ( ( ) ( non empty V52() V53() V54() V58() V66() ) set ) ) / 2 : ( ( ) ( non empty ordinal natural V30() real ext-real positive non negative V35() V36() V52() V53() V54() V55() V56() V57() ) Element of NAT : ( ( ) ( V52() V53() V54() V55() V56() V57() V58() ) Element of K19(REAL : ( ( ) ( non empty V52() V53() V54() V58() V66() ) set ) ) : ( ( ) ( ) set ) ) ) ) : ( ( ) ( V30() real ext-real ) Element of REAL : ( ( ) ( non empty V52() V53() V54() V58() V66() ) set ) ) .[ : ( ( ) ( open V52() V53() V54() ) Element of K19(REAL : ( ( ) ( non empty V52() V53() V54() V58() V66() ) set ) ) : ( ( ) ( ) set ) ) : ( ( V6() ) ( V1() V4( REAL : ( ( ) ( non empty V52() V53() V54() V58() V66() ) set ) ) V5( REAL : ( ( ) ( non empty V52() V53() V54() V58() V66() ) set ) ) V6() complex-valued ext-real-valued real-valued ) Element of K19(K20(REAL : ( ( ) ( non empty V52() V53() V54() V58() V66() ) set ) ,REAL : ( ( ) ( non empty V52() V53() V54() V58() V66() ) set ) ) : ( ( ) ( complex-valued ext-real-valued real-valued ) set ) ) : ( ( ) ( ) set ) ) is increasing ;

theorem :: SIN_COS2:3
sin : ( ( V6() quasi_total ) ( V1() V4( REAL : ( ( ) ( non empty V52() V53() V54() V58() V66() ) set ) ) V5( REAL : ( ( ) ( non empty V52() V53() V54() V58() V66() ) set ) ) V6() non empty total quasi_total complex-valued ext-real-valued real-valued continuous ) Element of K19(K20(REAL : ( ( ) ( non empty V52() V53() V54() V58() V66() ) set ) ,REAL : ( ( ) ( non empty V52() V53() V54() V58() V66() ) set ) ) : ( ( ) ( complex-valued ext-real-valued real-valued ) set ) ) : ( ( ) ( ) set ) ) | ].(PI : ( ( ) ( V30() real ext-real ) Element of REAL : ( ( ) ( non empty V52() V53() V54() V58() V66() ) set ) ) / 2 : ( ( ) ( non empty ordinal natural V30() real ext-real positive non negative V35() V36() V52() V53() V54() V55() V56() V57() ) Element of NAT : ( ( ) ( V52() V53() V54() V55() V56() V57() V58() ) Element of K19(REAL : ( ( ) ( non empty V52() V53() V54() V58() V66() ) set ) ) : ( ( ) ( ) set ) ) ) ) : ( ( ) ( V30() real ext-real ) Element of REAL : ( ( ) ( non empty V52() V53() V54() V58() V66() ) set ) ) ,PI : ( ( ) ( V30() real ext-real ) Element of REAL : ( ( ) ( non empty V52() V53() V54() V58() V66() ) set ) ) .[ : ( ( ) ( open V52() V53() V54() ) Element of K19(REAL : ( ( ) ( non empty V52() V53() V54() V58() V66() ) set ) ) : ( ( ) ( ) set ) ) : ( ( V6() ) ( V1() V4( REAL : ( ( ) ( non empty V52() V53() V54() V58() V66() ) set ) ) V5( REAL : ( ( ) ( non empty V52() V53() V54() V58() V66() ) set ) ) V6() complex-valued ext-real-valued real-valued ) Element of K19(K20(REAL : ( ( ) ( non empty V52() V53() V54() V58() V66() ) set ) ,REAL : ( ( ) ( non empty V52() V53() V54() V58() V66() ) set ) ) : ( ( ) ( complex-valued ext-real-valued real-valued ) set ) ) : ( ( ) ( ) set ) ) is decreasing ;

theorem :: SIN_COS2:4
cos : ( ( V6() quasi_total ) ( V1() V4( REAL : ( ( ) ( non empty V52() V53() V54() V58() V66() ) set ) ) V5( REAL : ( ( ) ( non empty V52() V53() V54() V58() V66() ) set ) ) V6() non empty total quasi_total complex-valued ext-real-valued real-valued continuous ) Element of K19(K20(REAL : ( ( ) ( non empty V52() V53() V54() V58() V66() ) set ) ,REAL : ( ( ) ( non empty V52() V53() V54() V58() V66() ) set ) ) : ( ( ) ( complex-valued ext-real-valued real-valued ) set ) ) : ( ( ) ( ) set ) ) | ].0 : ( ( ) ( empty ordinal natural V30() real ext-real non positive non negative V35() V36() V52() V53() V54() V55() V56() V57() V58() ) Element of NAT : ( ( ) ( V52() V53() V54() V55() V56() V57() V58() ) Element of K19(REAL : ( ( ) ( non empty V52() V53() V54() V58() V66() ) set ) ) : ( ( ) ( ) set ) ) ) ,(PI : ( ( ) ( V30() real ext-real ) Element of REAL : ( ( ) ( non empty V52() V53() V54() V58() V66() ) set ) ) / 2 : ( ( ) ( non empty ordinal natural V30() real ext-real positive non negative V35() V36() V52() V53() V54() V55() V56() V57() ) Element of NAT : ( ( ) ( V52() V53() V54() V55() V56() V57() V58() ) Element of K19(REAL : ( ( ) ( non empty V52() V53() V54() V58() V66() ) set ) ) : ( ( ) ( ) set ) ) ) ) : ( ( ) ( V30() real ext-real ) Element of REAL : ( ( ) ( non empty V52() V53() V54() V58() V66() ) set ) ) .[ : ( ( ) ( open V52() V53() V54() ) Element of K19(REAL : ( ( ) ( non empty V52() V53() V54() V58() V66() ) set ) ) : ( ( ) ( ) set ) ) : ( ( V6() ) ( V1() V4( REAL : ( ( ) ( non empty V52() V53() V54() V58() V66() ) set ) ) V5( REAL : ( ( ) ( non empty V52() V53() V54() V58() V66() ) set ) ) V6() complex-valued ext-real-valued real-valued ) Element of K19(K20(REAL : ( ( ) ( non empty V52() V53() V54() V58() V66() ) set ) ,REAL : ( ( ) ( non empty V52() V53() V54() V58() V66() ) set ) ) : ( ( ) ( complex-valued ext-real-valued real-valued ) set ) ) : ( ( ) ( ) set ) ) is decreasing ;

theorem :: SIN_COS2:5
cos : ( ( V6() quasi_total ) ( V1() V4( REAL : ( ( ) ( non empty V52() V53() V54() V58() V66() ) set ) ) V5( REAL : ( ( ) ( non empty V52() V53() V54() V58() V66() ) set ) ) V6() non empty total quasi_total complex-valued ext-real-valued real-valued continuous ) Element of K19(K20(REAL : ( ( ) ( non empty V52() V53() V54() V58() V66() ) set ) ,REAL : ( ( ) ( non empty V52() V53() V54() V58() V66() ) set ) ) : ( ( ) ( complex-valued ext-real-valued real-valued ) set ) ) : ( ( ) ( ) set ) ) | ].(PI : ( ( ) ( V30() real ext-real ) Element of REAL : ( ( ) ( non empty V52() V53() V54() V58() V66() ) set ) ) / 2 : ( ( ) ( non empty ordinal natural V30() real ext-real positive non negative V35() V36() V52() V53() V54() V55() V56() V57() ) Element of NAT : ( ( ) ( V52() V53() V54() V55() V56() V57() V58() ) Element of K19(REAL : ( ( ) ( non empty V52() V53() V54() V58() V66() ) set ) ) : ( ( ) ( ) set ) ) ) ) : ( ( ) ( V30() real ext-real ) Element of REAL : ( ( ) ( non empty V52() V53() V54() V58() V66() ) set ) ) ,PI : ( ( ) ( V30() real ext-real ) Element of REAL : ( ( ) ( non empty V52() V53() V54() V58() V66() ) set ) ) .[ : ( ( ) ( open V52() V53() V54() ) Element of K19(REAL : ( ( ) ( non empty V52() V53() V54() V58() V66() ) set ) ) : ( ( ) ( ) set ) ) : ( ( V6() ) ( V1() V4( REAL : ( ( ) ( non empty V52() V53() V54() V58() V66() ) set ) ) V5( REAL : ( ( ) ( non empty V52() V53() V54() V58() V66() ) set ) ) V6() complex-valued ext-real-valued real-valued ) Element of K19(K20(REAL : ( ( ) ( non empty V52() V53() V54() V58() V66() ) set ) ,REAL : ( ( ) ( non empty V52() V53() V54() V58() V66() ) set ) ) : ( ( ) ( complex-valued ext-real-valued real-valued ) set ) ) : ( ( ) ( ) set ) ) is decreasing ;

theorem :: SIN_COS2:6
sin : ( ( V6() quasi_total ) ( V1() V4( REAL : ( ( ) ( non empty V52() V53() V54() V58() V66() ) set ) ) V5( REAL : ( ( ) ( non empty V52() V53() V54() V58() V66() ) set ) ) V6() non empty total quasi_total complex-valued ext-real-valued real-valued continuous ) Element of K19(K20(REAL : ( ( ) ( non empty V52() V53() V54() V58() V66() ) set ) ,REAL : ( ( ) ( non empty V52() V53() V54() V58() V66() ) set ) ) : ( ( ) ( complex-valued ext-real-valued real-valued ) set ) ) : ( ( ) ( ) set ) ) | ].PI : ( ( ) ( V30() real ext-real ) Element of REAL : ( ( ) ( non empty V52() V53() V54() V58() V66() ) set ) ) ,((3 : ( ( ) ( non empty ordinal natural V30() real ext-real positive non negative V35() V36() V52() V53() V54() V55() V56() V57() ) Element of NAT : ( ( ) ( V52() V53() V54() V55() V56() V57() V58() ) Element of K19(REAL : ( ( ) ( non empty V52() V53() V54() V58() V66() ) set ) ) : ( ( ) ( ) set ) ) ) / 2 : ( ( ) ( non empty ordinal natural V30() real ext-real positive non negative V35() V36() V52() V53() V54() V55() V56() V57() ) Element of NAT : ( ( ) ( V52() V53() V54() V55() V56() V57() V58() ) Element of K19(REAL : ( ( ) ( non empty V52() V53() V54() V58() V66() ) set ) ) : ( ( ) ( ) set ) ) ) ) : ( ( ) ( V30() real ext-real non negative ) Element of REAL : ( ( ) ( non empty V52() V53() V54() V58() V66() ) set ) ) * PI : ( ( ) ( V30() real ext-real ) Element of REAL : ( ( ) ( non empty V52() V53() V54() V58() V66() ) set ) ) ) : ( ( ) ( V30() real ext-real ) Element of REAL : ( ( ) ( non empty V52() V53() V54() V58() V66() ) set ) ) .[ : ( ( ) ( open V52() V53() V54() ) Element of K19(REAL : ( ( ) ( non empty V52() V53() V54() V58() V66() ) set ) ) : ( ( ) ( ) set ) ) : ( ( V6() ) ( V1() V4( REAL : ( ( ) ( non empty V52() V53() V54() V58() V66() ) set ) ) V5( REAL : ( ( ) ( non empty V52() V53() V54() V58() V66() ) set ) ) V6() complex-valued ext-real-valued real-valued ) Element of K19(K20(REAL : ( ( ) ( non empty V52() V53() V54() V58() V66() ) set ) ,REAL : ( ( ) ( non empty V52() V53() V54() V58() V66() ) set ) ) : ( ( ) ( complex-valued ext-real-valued real-valued ) set ) ) : ( ( ) ( ) set ) ) is decreasing ;

theorem :: SIN_COS2:7
sin : ( ( V6() quasi_total ) ( V1() V4( REAL : ( ( ) ( non empty V52() V53() V54() V58() V66() ) set ) ) V5( REAL : ( ( ) ( non empty V52() V53() V54() V58() V66() ) set ) ) V6() non empty total quasi_total complex-valued ext-real-valued real-valued continuous ) Element of K19(K20(REAL : ( ( ) ( non empty V52() V53() V54() V58() V66() ) set ) ,REAL : ( ( ) ( non empty V52() V53() V54() V58() V66() ) set ) ) : ( ( ) ( complex-valued ext-real-valued real-valued ) set ) ) : ( ( ) ( ) set ) ) | ].((3 : ( ( ) ( non empty ordinal natural V30() real ext-real positive non negative V35() V36() V52() V53() V54() V55() V56() V57() ) Element of NAT : ( ( ) ( V52() V53() V54() V55() V56() V57() V58() ) Element of K19(REAL : ( ( ) ( non empty V52() V53() V54() V58() V66() ) set ) ) : ( ( ) ( ) set ) ) ) / 2 : ( ( ) ( non empty ordinal natural V30() real ext-real positive non negative V35() V36() V52() V53() V54() V55() V56() V57() ) Element of NAT : ( ( ) ( V52() V53() V54() V55() V56() V57() V58() ) Element of K19(REAL : ( ( ) ( non empty V52() V53() V54() V58() V66() ) set ) ) : ( ( ) ( ) set ) ) ) ) : ( ( ) ( V30() real ext-real non negative ) Element of REAL : ( ( ) ( non empty V52() V53() V54() V58() V66() ) set ) ) * PI : ( ( ) ( V30() real ext-real ) Element of REAL : ( ( ) ( non empty V52() V53() V54() V58() V66() ) set ) ) ) : ( ( ) ( V30() real ext-real ) Element of REAL : ( ( ) ( non empty V52() V53() V54() V58() V66() ) set ) ) ,(2 : ( ( ) ( non empty ordinal natural V30() real ext-real positive non negative V35() V36() V52() V53() V54() V55() V56() V57() ) Element of NAT : ( ( ) ( V52() V53() V54() V55() V56() V57() V58() ) Element of K19(REAL : ( ( ) ( non empty V52() V53() V54() V58() V66() ) set ) ) : ( ( ) ( ) set ) ) ) * PI : ( ( ) ( V30() real ext-real ) Element of REAL : ( ( ) ( non empty V52() V53() V54() V58() V66() ) set ) ) ) : ( ( ) ( V30() real ext-real ) Element of REAL : ( ( ) ( non empty V52() V53() V54() V58() V66() ) set ) ) .[ : ( ( ) ( open V52() V53() V54() ) Element of K19(REAL : ( ( ) ( non empty V52() V53() V54() V58() V66() ) set ) ) : ( ( ) ( ) set ) ) : ( ( V6() ) ( V1() V4( REAL : ( ( ) ( non empty V52() V53() V54() V58() V66() ) set ) ) V5( REAL : ( ( ) ( non empty V52() V53() V54() V58() V66() ) set ) ) V6() complex-valued ext-real-valued real-valued ) Element of K19(K20(REAL : ( ( ) ( non empty V52() V53() V54() V58() V66() ) set ) ,REAL : ( ( ) ( non empty V52() V53() V54() V58() V66() ) set ) ) : ( ( ) ( complex-valued ext-real-valued real-valued ) set ) ) : ( ( ) ( ) set ) ) is increasing ;

theorem :: SIN_COS2:8
cos : ( ( V6() quasi_total ) ( V1() V4( REAL : ( ( ) ( non empty V52() V53() V54() V58() V66() ) set ) ) V5( REAL : ( ( ) ( non empty V52() V53() V54() V58() V66() ) set ) ) V6() non empty total quasi_total complex-valued ext-real-valued real-valued continuous ) Element of K19(K20(REAL : ( ( ) ( non empty V52() V53() V54() V58() V66() ) set ) ,REAL : ( ( ) ( non empty V52() V53() V54() V58() V66() ) set ) ) : ( ( ) ( complex-valued ext-real-valued real-valued ) set ) ) : ( ( ) ( ) set ) ) | ].PI : ( ( ) ( V30() real ext-real ) Element of REAL : ( ( ) ( non empty V52() V53() V54() V58() V66() ) set ) ) ,((3 : ( ( ) ( non empty ordinal natural V30() real ext-real positive non negative V35() V36() V52() V53() V54() V55() V56() V57() ) Element of NAT : ( ( ) ( V52() V53() V54() V55() V56() V57() V58() ) Element of K19(REAL : ( ( ) ( non empty V52() V53() V54() V58() V66() ) set ) ) : ( ( ) ( ) set ) ) ) / 2 : ( ( ) ( non empty ordinal natural V30() real ext-real positive non negative V35() V36() V52() V53() V54() V55() V56() V57() ) Element of NAT : ( ( ) ( V52() V53() V54() V55() V56() V57() V58() ) Element of K19(REAL : ( ( ) ( non empty V52() V53() V54() V58() V66() ) set ) ) : ( ( ) ( ) set ) ) ) ) : ( ( ) ( V30() real ext-real non negative ) Element of REAL : ( ( ) ( non empty V52() V53() V54() V58() V66() ) set ) ) * PI : ( ( ) ( V30() real ext-real ) Element of REAL : ( ( ) ( non empty V52() V53() V54() V58() V66() ) set ) ) ) : ( ( ) ( V30() real ext-real ) Element of REAL : ( ( ) ( non empty V52() V53() V54() V58() V66() ) set ) ) .[ : ( ( ) ( open V52() V53() V54() ) Element of K19(REAL : ( ( ) ( non empty V52() V53() V54() V58() V66() ) set ) ) : ( ( ) ( ) set ) ) : ( ( V6() ) ( V1() V4( REAL : ( ( ) ( non empty V52() V53() V54() V58() V66() ) set ) ) V5( REAL : ( ( ) ( non empty V52() V53() V54() V58() V66() ) set ) ) V6() complex-valued ext-real-valued real-valued ) Element of K19(K20(REAL : ( ( ) ( non empty V52() V53() V54() V58() V66() ) set ) ,REAL : ( ( ) ( non empty V52() V53() V54() V58() V66() ) set ) ) : ( ( ) ( complex-valued ext-real-valued real-valued ) set ) ) : ( ( ) ( ) set ) ) is increasing ;

theorem :: SIN_COS2:9
cos : ( ( V6() quasi_total ) ( V1() V4( REAL : ( ( ) ( non empty V52() V53() V54() V58() V66() ) set ) ) V5( REAL : ( ( ) ( non empty V52() V53() V54() V58() V66() ) set ) ) V6() non empty total quasi_total complex-valued ext-real-valued real-valued continuous ) Element of K19(K20(REAL : ( ( ) ( non empty V52() V53() V54() V58() V66() ) set ) ,REAL : ( ( ) ( non empty V52() V53() V54() V58() V66() ) set ) ) : ( ( ) ( complex-valued ext-real-valued real-valued ) set ) ) : ( ( ) ( ) set ) ) | ].((3 : ( ( ) ( non empty ordinal natural V30() real ext-real positive non negative V35() V36() V52() V53() V54() V55() V56() V57() ) Element of NAT : ( ( ) ( V52() V53() V54() V55() V56() V57() V58() ) Element of K19(REAL : ( ( ) ( non empty V52() V53() V54() V58() V66() ) set ) ) : ( ( ) ( ) set ) ) ) / 2 : ( ( ) ( non empty ordinal natural V30() real ext-real positive non negative V35() V36() V52() V53() V54() V55() V56() V57() ) Element of NAT : ( ( ) ( V52() V53() V54() V55() V56() V57() V58() ) Element of K19(REAL : ( ( ) ( non empty V52() V53() V54() V58() V66() ) set ) ) : ( ( ) ( ) set ) ) ) ) : ( ( ) ( V30() real ext-real non negative ) Element of REAL : ( ( ) ( non empty V52() V53() V54() V58() V66() ) set ) ) * PI : ( ( ) ( V30() real ext-real ) Element of REAL : ( ( ) ( non empty V52() V53() V54() V58() V66() ) set ) ) ) : ( ( ) ( V30() real ext-real ) Element of REAL : ( ( ) ( non empty V52() V53() V54() V58() V66() ) set ) ) ,(2 : ( ( ) ( non empty ordinal natural V30() real ext-real positive non negative V35() V36() V52() V53() V54() V55() V56() V57() ) Element of NAT : ( ( ) ( V52() V53() V54() V55() V56() V57() V58() ) Element of K19(REAL : ( ( ) ( non empty V52() V53() V54() V58() V66() ) set ) ) : ( ( ) ( ) set ) ) ) * PI : ( ( ) ( V30() real ext-real ) Element of REAL : ( ( ) ( non empty V52() V53() V54() V58() V66() ) set ) ) ) : ( ( ) ( V30() real ext-real ) Element of REAL : ( ( ) ( non empty V52() V53() V54() V58() V66() ) set ) ) .[ : ( ( ) ( open V52() V53() V54() ) Element of K19(REAL : ( ( ) ( non empty V52() V53() V54() V58() V66() ) set ) ) : ( ( ) ( ) set ) ) : ( ( V6() ) ( V1() V4( REAL : ( ( ) ( non empty V52() V53() V54() V58() V66() ) set ) ) V5( REAL : ( ( ) ( non empty V52() V53() V54() V58() V66() ) set ) ) V6() complex-valued ext-real-valued real-valued ) Element of K19(K20(REAL : ( ( ) ( non empty V52() V53() V54() V58() V66() ) set ) ,REAL : ( ( ) ( non empty V52() V53() V54() V58() V66() ) set ) ) : ( ( ) ( complex-valued ext-real-valued real-valued ) set ) ) : ( ( ) ( ) set ) ) is increasing ;

theorem :: SIN_COS2:10
for th being ( ( real ) ( V30() real ext-real ) number )
for n being ( ( natural ) ( ordinal natural V30() real ext-real non negative ) Nat) holds sin : ( ( V6() quasi_total ) ( V1() V4( REAL : ( ( ) ( non empty V52() V53() V54() V58() V66() ) set ) ) V5( REAL : ( ( ) ( non empty V52() V53() V54() V58() V66() ) set ) ) V6() non empty total quasi_total complex-valued ext-real-valued real-valued continuous ) Element of K19(K20(REAL : ( ( ) ( non empty V52() V53() V54() V58() V66() ) set ) ,REAL : ( ( ) ( non empty V52() V53() V54() V58() V66() ) set ) ) : ( ( ) ( complex-valued ext-real-valued real-valued ) set ) ) : ( ( ) ( ) set ) ) . th : ( ( real ) ( V30() real ext-real ) number ) : ( ( ) ( V30() real ext-real ) Element of REAL : ( ( ) ( non empty V52() V53() V54() V58() V66() ) set ) ) = sin : ( ( V6() quasi_total ) ( V1() V4( REAL : ( ( ) ( non empty V52() V53() V54() V58() V66() ) set ) ) V5( REAL : ( ( ) ( non empty V52() V53() V54() V58() V66() ) set ) ) V6() non empty total quasi_total complex-valued ext-real-valued real-valued continuous ) Element of K19(K20(REAL : ( ( ) ( non empty V52() V53() V54() V58() V66() ) set ) ,REAL : ( ( ) ( non empty V52() V53() V54() V58() V66() ) set ) ) : ( ( ) ( complex-valued ext-real-valued real-valued ) set ) ) : ( ( ) ( ) set ) ) . (((2 : ( ( ) ( non empty ordinal natural V30() real ext-real positive non negative V35() V36() V52() V53() V54() V55() V56() V57() ) Element of NAT : ( ( ) ( V52() V53() V54() V55() V56() V57() V58() ) Element of K19(REAL : ( ( ) ( non empty V52() V53() V54() V58() V66() ) set ) ) : ( ( ) ( ) set ) ) ) * PI : ( ( ) ( V30() real ext-real ) Element of REAL : ( ( ) ( non empty V52() V53() V54() V58() V66() ) set ) ) ) : ( ( ) ( V30() real ext-real ) Element of REAL : ( ( ) ( non empty V52() V53() V54() V58() V66() ) set ) ) * n : ( ( natural ) ( ordinal natural V30() real ext-real non negative ) Nat) ) : ( ( ) ( V30() real ext-real ) Element of REAL : ( ( ) ( non empty V52() V53() V54() V58() V66() ) set ) ) + th : ( ( real ) ( V30() real ext-real ) number ) ) : ( ( ) ( V30() real ext-real ) Element of REAL : ( ( ) ( non empty V52() V53() V54() V58() V66() ) set ) ) : ( ( ) ( V30() real ext-real ) Element of REAL : ( ( ) ( non empty V52() V53() V54() V58() V66() ) set ) ) ;

theorem :: SIN_COS2:11
for th being ( ( real ) ( V30() real ext-real ) number )
for n being ( ( natural ) ( ordinal natural V30() real ext-real non negative ) Nat) holds cos : ( ( V6() quasi_total ) ( V1() V4( REAL : ( ( ) ( non empty V52() V53() V54() V58() V66() ) set ) ) V5( REAL : ( ( ) ( non empty V52() V53() V54() V58() V66() ) set ) ) V6() non empty total quasi_total complex-valued ext-real-valued real-valued continuous ) Element of K19(K20(REAL : ( ( ) ( non empty V52() V53() V54() V58() V66() ) set ) ,REAL : ( ( ) ( non empty V52() V53() V54() V58() V66() ) set ) ) : ( ( ) ( complex-valued ext-real-valued real-valued ) set ) ) : ( ( ) ( ) set ) ) . th : ( ( real ) ( V30() real ext-real ) number ) : ( ( ) ( V30() real ext-real ) Element of REAL : ( ( ) ( non empty V52() V53() V54() V58() V66() ) set ) ) = cos : ( ( V6() quasi_total ) ( V1() V4( REAL : ( ( ) ( non empty V52() V53() V54() V58() V66() ) set ) ) V5( REAL : ( ( ) ( non empty V52() V53() V54() V58() V66() ) set ) ) V6() non empty total quasi_total complex-valued ext-real-valued real-valued continuous ) Element of K19(K20(REAL : ( ( ) ( non empty V52() V53() V54() V58() V66() ) set ) ,REAL : ( ( ) ( non empty V52() V53() V54() V58() V66() ) set ) ) : ( ( ) ( complex-valued ext-real-valued real-valued ) set ) ) : ( ( ) ( ) set ) ) . (((2 : ( ( ) ( non empty ordinal natural V30() real ext-real positive non negative V35() V36() V52() V53() V54() V55() V56() V57() ) Element of NAT : ( ( ) ( V52() V53() V54() V55() V56() V57() V58() ) Element of K19(REAL : ( ( ) ( non empty V52() V53() V54() V58() V66() ) set ) ) : ( ( ) ( ) set ) ) ) * PI : ( ( ) ( V30() real ext-real ) Element of REAL : ( ( ) ( non empty V52() V53() V54() V58() V66() ) set ) ) ) : ( ( ) ( V30() real ext-real ) Element of REAL : ( ( ) ( non empty V52() V53() V54() V58() V66() ) set ) ) * n : ( ( natural ) ( ordinal natural V30() real ext-real non negative ) Nat) ) : ( ( ) ( V30() real ext-real ) Element of REAL : ( ( ) ( non empty V52() V53() V54() V58() V66() ) set ) ) + th : ( ( real ) ( V30() real ext-real ) number ) ) : ( ( ) ( V30() real ext-real ) Element of REAL : ( ( ) ( non empty V52() V53() V54() V58() V66() ) set ) ) : ( ( ) ( V30() real ext-real ) Element of REAL : ( ( ) ( non empty V52() V53() V54() V58() V66() ) set ) ) ;

begin

definition
func sinh -> ( ( V6() quasi_total ) ( V1() V4( REAL : ( ( ) ( non empty V52() V53() V54() V58() V66() ) set ) ) V5( REAL : ( ( ) ( non empty V52() V53() V54() V58() V66() ) set ) ) V6() non empty total quasi_total complex-valued ext-real-valued real-valued ) Function of REAL : ( ( ) ( non empty V52() V53() V54() V58() V66() ) set ) , REAL : ( ( ) ( non empty V52() V53() V54() V58() V66() ) set ) ) means :: SIN_COS2:def 1
 for d being ( ( real ) ( V30() real ext-real ) number ) holds it : ( ( ) ( V30() real ext-real ) Element of REAL : ( ( ) ( non empty V52() V53() V54() V58() V66() ) set ) ) . d : ( ( real ) ( V30() real ext-real ) number ) : ( ( ) ( V30() real ext-real ) Element of REAL : ( ( ) ( non empty V52() V53() V54() V58() V66() ) set ) ) = ((exp_R : ( ( V6() quasi_total ) ( V1() V4( REAL : ( ( ) ( non empty V52() V53() V54() V58() V66() ) set ) ) V5( REAL : ( ( ) ( non empty V52() V53() V54() V58() V66() ) set ) ) V6() non empty total quasi_total complex-valued ext-real-valued real-valued continuous ) Element of K19(K20(REAL : ( ( ) ( non empty V52() V53() V54() V58() V66() ) set ) ,REAL : ( ( ) ( non empty V52() V53() V54() V58() V66() ) set ) ) : ( ( ) ( complex-valued ext-real-valued real-valued ) set ) ) : ( ( ) ( ) set ) ) . d : ( ( real ) ( V30() real ext-real ) number ) ) : ( ( ) ( V30() real ext-real ) Element of REAL : ( ( ) ( non empty V52() V53() V54() V58() V66() ) set ) ) - (exp_R : ( ( V6() quasi_total ) ( V1() V4( REAL : ( ( ) ( non empty V52() V53() V54() V58() V66() ) set ) ) V5( REAL : ( ( ) ( non empty V52() V53() V54() V58() V66() ) set ) ) V6() non empty total quasi_total complex-valued ext-real-valued real-valued continuous ) Element of K19(K20(REAL : ( ( ) ( non empty V52() V53() V54() V58() V66() ) set ) ,REAL : ( ( ) ( non empty V52() V53() V54() V58() V66() ) set ) ) : ( ( ) ( complex-valued ext-real-valued real-valued ) set ) ) : ( ( ) ( ) set ) ) . (- d : ( ( real ) ( V30() real ext-real ) number ) ) : ( ( ) ( V30() real ext-real ) Element of REAL : ( ( ) ( non empty V52() V53() V54() V58() V66() ) set ) ) ) : ( ( ) ( V30() real ext-real ) Element of REAL : ( ( ) ( non empty V52() V53() V54() V58() V66() ) set ) ) ) : ( ( ) ( V30() real ext-real ) Element of REAL : ( ( ) ( non empty V52() V53() V54() V58() V66() ) set ) ) / 2 : ( ( ) ( non empty ordinal natural V30() real ext-real positive non negative V35() V36() V52() V53() V54() V55() V56() V57() ) Element of NAT : ( ( ) ( V52() V53() V54() V55() V56() V57() V58() ) Element of K19(REAL : ( ( ) ( non empty V52() V53() V54() V58() V66() ) set ) ) : ( ( ) ( ) set ) ) ) : ( ( ) ( V30() real ext-real ) Element of REAL : ( ( ) ( non empty V52() V53() V54() V58() V66() ) set ) ) ;
end;

definition
let d be ( ( ) ( ) number ) ;
func sinh d -> ( ( ) ( ) set ) equals :: SIN_COS2:def 2
sinh : ( ( V6() quasi_total ) ( V1() V4( REAL : ( ( ) ( non empty V52() V53() V54() V58() V66() ) set ) ) V5( REAL : ( ( ) ( non empty V52() V53() V54() V58() V66() ) set ) ) V6() non empty total quasi_total complex-valued ext-real-valued real-valued ) Function of REAL : ( ( ) ( non empty V52() V53() V54() V58() V66() ) set ) , REAL : ( ( ) ( non empty V52() V53() V54() V58() V66() ) set ) ) . d : ( ( ) ( V30() real ext-real ) Element of REAL : ( ( ) ( non empty V52() V53() V54() V58() V66() ) set ) ) : ( ( ) ( V30() real ext-real ) Element of REAL : ( ( ) ( non empty V52() V53() V54() V58() V66() ) set ) ) ;
end;

registration
let d be ( ( ) ( ) number ) ;
cluster sinh d : ( ( ) ( ) set ) : ( ( ) ( ) set ) -> real ;
end;

definition
let d be ( ( ) ( ) number ) ;
:: original: sinh
redefine func sinh d -> ( ( ) ( V30() real ext-real ) Real) ;
end;

definition
func cosh -> ( ( V6() quasi_total ) ( V1() V4( REAL : ( ( ) ( non empty V52() V53() V54() V58() V66() ) set ) ) V5( REAL : ( ( ) ( non empty V52() V53() V54() V58() V66() ) set ) ) V6() non empty total quasi_total complex-valued ext-real-valued real-valued ) Function of REAL : ( ( ) ( non empty V52() V53() V54() V58() V66() ) set ) , REAL : ( ( ) ( non empty V52() V53() V54() V58() V66() ) set ) ) means :: SIN_COS2:def 3
 for d being ( ( real ) ( V30() real ext-real ) number ) holds it : ( ( ) ( ) set ) . d : ( ( real ) ( V30() real ext-real ) number ) : ( ( ) ( V30() real ext-real ) Element of REAL : ( ( ) ( non empty V52() V53() V54() V58() V66() ) set ) ) = ((exp_R : ( ( V6() quasi_total ) ( V1() V4( REAL : ( ( ) ( non empty V52() V53() V54() V58() V66() ) set ) ) V5( REAL : ( ( ) ( non empty V52() V53() V54() V58() V66() ) set ) ) V6() non empty total quasi_total complex-valued ext-real-valued real-valued continuous ) Element of K19(K20(REAL : ( ( ) ( non empty V52() V53() V54() V58() V66() ) set ) ,REAL : ( ( ) ( non empty V52() V53() V54() V58() V66() ) set ) ) : ( ( ) ( complex-valued ext-real-valued real-valued ) set ) ) : ( ( ) ( ) set ) ) . d : ( ( real ) ( V30() real ext-real ) number ) ) : ( ( ) ( V30() real ext-real ) Element of REAL : ( ( ) ( non empty V52() V53() V54() V58() V66() ) set ) ) + (exp_R : ( ( V6() quasi_total ) ( V1() V4( REAL : ( ( ) ( non empty V52() V53() V54() V58() V66() ) set ) ) V5( REAL : ( ( ) ( non empty V52() V53() V54() V58() V66() ) set ) ) V6() non empty total quasi_total complex-valued ext-real-valued real-valued continuous ) Element of K19(K20(REAL : ( ( ) ( non empty V52() V53() V54() V58() V66() ) set ) ,REAL : ( ( ) ( non empty V52() V53() V54() V58() V66() ) set ) ) : ( ( ) ( complex-valued ext-real-valued real-valued ) set ) ) : ( ( ) ( ) set ) ) . (- d : ( ( real ) ( V30() real ext-real ) number ) ) : ( ( ) ( V30() real ext-real ) Element of REAL : ( ( ) ( non empty V52() V53() V54() V58() V66() ) set ) ) ) : ( ( ) ( V30() real ext-real ) Element of REAL : ( ( ) ( non empty V52() V53() V54() V58() V66() ) set ) ) ) : ( ( ) ( V30() real ext-real ) Element of REAL : ( ( ) ( non empty V52() V53() V54() V58() V66() ) set ) ) / 2 : ( ( ) ( non empty ordinal natural V30() real ext-real positive non negative V35() V36() V52() V53() V54() V55() V56() V57() ) Element of NAT : ( ( ) ( V52() V53() V54() V55() V56() V57() V58() ) Element of K19(REAL : ( ( ) ( non empty V52() V53() V54() V58() V66() ) set ) ) : ( ( ) ( ) set ) ) ) : ( ( ) ( V30() real ext-real ) Element of REAL : ( ( ) ( non empty V52() V53() V54() V58() V66() ) set ) ) ;
end;

definition
let d be ( ( ) ( ) number ) ;
func cosh d -> ( ( ) ( ) set ) equals :: SIN_COS2:def 4
cosh : ( ( V6() quasi_total ) ( V1() V4( REAL : ( ( ) ( non empty V52() V53() V54() V58() V66() ) set ) ) V5( REAL : ( ( ) ( non empty V52() V53() V54() V58() V66() ) set ) ) V6() non empty total quasi_total complex-valued ext-real-valued real-valued ) Function of REAL : ( ( ) ( non empty V52() V53() V54() V58() V66() ) set ) , REAL : ( ( ) ( non empty V52() V53() V54() V58() V66() ) set ) ) . d : ( ( ) ( ) set ) : ( ( ) ( V30() real ext-real ) Element of REAL : ( ( ) ( non empty V52() V53() V54() V58() V66() ) set ) ) ;
end;

registration
let d be ( ( ) ( ) number ) ;
cluster cosh d : ( ( ) ( ) set ) : ( ( ) ( ) set ) -> real ;
end;

definition
let d be ( ( ) ( ) number ) ;
:: original: cosh
redefine func cosh d -> ( ( ) ( V30() real ext-real ) Real) ;
end;

definition
func tanh -> ( ( V6() quasi_total ) ( V1() V4( REAL : ( ( ) ( non empty V52() V53() V54() V58() V66() ) set ) ) V5( REAL : ( ( ) ( non empty V52() V53() V54() V58() V66() ) set ) ) V6() non empty total quasi_total complex-valued ext-real-valued real-valued ) Function of REAL : ( ( ) ( non empty V52() V53() V54() V58() V66() ) set ) , REAL : ( ( ) ( non empty V52() V53() V54() V58() V66() ) set ) ) means :: SIN_COS2:def 5
 for d being ( ( real ) ( V30() real ext-real ) number ) holds it : ( ( ) ( ) set ) . d : ( ( real ) ( V30() real ext-real ) number ) : ( ( ) ( V30() real ext-real ) Element of REAL : ( ( ) ( non empty V52() V53() V54() V58() V66() ) set ) ) = ((exp_R : ( ( V6() quasi_total ) ( V1() V4( REAL : ( ( ) ( non empty V52() V53() V54() V58() V66() ) set ) ) V5( REAL : ( ( ) ( non empty V52() V53() V54() V58() V66() ) set ) ) V6() non empty total quasi_total complex-valued ext-real-valued real-valued continuous ) Element of K19(K20(REAL : ( ( ) ( non empty V52() V53() V54() V58() V66() ) set ) ,REAL : ( ( ) ( non empty V52() V53() V54() V58() V66() ) set ) ) : ( ( ) ( complex-valued ext-real-valued real-valued ) set ) ) : ( ( ) ( ) set ) ) . d : ( ( real ) ( V30() real ext-real ) number ) ) : ( ( ) ( V30() real ext-real ) Element of REAL : ( ( ) ( non empty V52() V53() V54() V58() V66() ) set ) ) - (exp_R : ( ( V6() quasi_total ) ( V1() V4( REAL : ( ( ) ( non empty V52() V53() V54() V58() V66() ) set ) ) V5( REAL : ( ( ) ( non empty V52() V53() V54() V58() V66() ) set ) ) V6() non empty total quasi_total complex-valued ext-real-valued real-valued continuous ) Element of K19(K20(REAL : ( ( ) ( non empty V52() V53() V54() V58() V66() ) set ) ,REAL : ( ( ) ( non empty V52() V53() V54() V58() V66() ) set ) ) : ( ( ) ( complex-valued ext-real-valued real-valued ) set ) ) : ( ( ) ( ) set ) ) . (- d : ( ( real ) ( V30() real ext-real ) number ) ) : ( ( ) ( V30() real ext-real ) Element of REAL : ( ( ) ( non empty V52() V53() V54() V58() V66() ) set ) ) ) : ( ( ) ( V30() real ext-real ) Element of REAL : ( ( ) ( non empty V52() V53() V54() V58() V66() ) set ) ) ) : ( ( ) ( V30() real ext-real ) Element of REAL : ( ( ) ( non empty V52() V53() V54() V58() V66() ) set ) ) / ((exp_R : ( ( V6() quasi_total ) ( V1() V4( REAL : ( ( ) ( non empty V52() V53() V54() V58() V66() ) set ) ) V5( REAL : ( ( ) ( non empty V52() V53() V54() V58() V66() ) set ) ) V6() non empty total quasi_total complex-valued ext-real-valued real-valued continuous ) Element of K19(K20(REAL : ( ( ) ( non empty V52() V53() V54() V58() V66() ) set ) ,REAL : ( ( ) ( non empty V52() V53() V54() V58() V66() ) set ) ) : ( ( ) ( complex-valued ext-real-valued real-valued ) set ) ) : ( ( ) ( ) set ) ) . d : ( ( real ) ( V30() real ext-real ) number ) ) : ( ( ) ( V30() real ext-real ) Element of REAL : ( ( ) ( non empty V52() V53() V54() V58() V66() ) set ) ) + (exp_R : ( ( V6() quasi_total ) ( V1() V4( REAL : ( ( ) ( non empty V52() V53() V54() V58() V66() ) set ) ) V5( REAL : ( ( ) ( non empty V52() V53() V54() V58() V66() ) set ) ) V6() non empty total quasi_total complex-valued ext-real-valued real-valued continuous ) Element of K19(K20(REAL : ( ( ) ( non empty V52() V53() V54() V58() V66() ) set ) ,REAL : ( ( ) ( non empty V52() V53() V54() V58() V66() ) set ) ) : ( ( ) ( complex-valued ext-real-valued real-valued ) set ) ) : ( ( ) ( ) set ) ) . (- d : ( ( real ) ( V30() real ext-real ) number ) ) : ( ( ) ( V30() real ext-real ) Element of REAL : ( ( ) ( non empty V52() V53() V54() V58() V66() ) set ) ) ) : ( ( ) ( V30() real ext-real ) Element of REAL : ( ( ) ( non empty V52() V53() V54() V58() V66() ) set ) ) ) : ( ( ) ( V30() real ext-real ) Element of REAL : ( ( ) ( non empty V52() V53() V54() V58() V66() ) set ) ) : ( ( ) ( V30() real ext-real ) Element of REAL : ( ( ) ( non empty V52() V53() V54() V58() V66() ) set ) ) ;
end;

definition
let d be ( ( ) ( ) number ) ;
func tanh d -> ( ( ) ( ) set ) equals :: SIN_COS2:def 6
tanh : ( ( V6() quasi_total ) ( V1() V4( REAL : ( ( ) ( non empty V52() V53() V54() V58() V66() ) set ) ) V5( REAL : ( ( ) ( non empty V52() V53() V54() V58() V66() ) set ) ) V6() non empty total quasi_total complex-valued ext-real-valued real-valued ) Function of REAL : ( ( ) ( non empty V52() V53() V54() V58() V66() ) set ) , REAL : ( ( ) ( non empty V52() V53() V54() V58() V66() ) set ) ) . d : ( ( ) ( ) set ) : ( ( ) ( V30() real ext-real ) Element of REAL : ( ( ) ( non empty V52() V53() V54() V58() V66() ) set ) ) ;
end;

registration
let d be ( ( ) ( ) number ) ;
cluster tanh d : ( ( ) ( ) set ) : ( ( ) ( ) set ) -> real ;
end;

definition
let d be ( ( ) ( ) number ) ;
:: original: tanh
redefine func tanh d -> ( ( ) ( V30() real ext-real ) Real) ;
end;

theorem :: SIN_COS2:12
for p, q being ( ( real ) ( V30() real ext-real ) number ) holds exp_R : ( ( V6() quasi_total ) ( V1() V4( REAL : ( ( ) ( non empty V52() V53() V54() V58() V66() ) set ) ) V5( REAL : ( ( ) ( non empty V52() V53() V54() V58() V66() ) set ) ) V6() non empty total quasi_total complex-valued ext-real-valued real-valued continuous ) Element of K19(K20(REAL : ( ( ) ( non empty V52() V53() V54() V58() V66() ) set ) ,REAL : ( ( ) ( non empty V52() V53() V54() V58() V66() ) set ) ) : ( ( ) ( complex-valued ext-real-valued real-valued ) set ) ) : ( ( ) ( ) set ) ) . (p : ( ( real ) ( V30() real ext-real ) number ) + q : ( ( real ) ( V30() real ext-real ) number ) ) : ( ( ) ( V30() real ext-real ) Element of REAL : ( ( ) ( non empty V52() V53() V54() V58() V66() ) set ) ) : ( ( ) ( V30() real ext-real ) Element of REAL : ( ( ) ( non empty V52() V53() V54() V58() V66() ) set ) ) = (exp_R : ( ( V6() quasi_total ) ( V1() V4( REAL : ( ( ) ( non empty V52() V53() V54() V58() V66() ) set ) ) V5( REAL : ( ( ) ( non empty V52() V53() V54() V58() V66() ) set ) ) V6() non empty total quasi_total complex-valued ext-real-valued real-valued continuous ) Element of K19(K20(REAL : ( ( ) ( non empty V52() V53() V54() V58() V66() ) set ) ,REAL : ( ( ) ( non empty V52() V53() V54() V58() V66() ) set ) ) : ( ( ) ( complex-valued ext-real-valued real-valued ) set ) ) : ( ( ) ( ) set ) ) . p : ( ( real ) ( V30() real ext-real ) number ) ) : ( ( ) ( V30() real ext-real ) Element of REAL : ( ( ) ( non empty V52() V53() V54() V58() V66() ) set ) ) * (exp_R : ( ( V6() quasi_total ) ( V1() V4( REAL : ( ( ) ( non empty V52() V53() V54() V58() V66() ) set ) ) V5( REAL : ( ( ) ( non empty V52() V53() V54() V58() V66() ) set ) ) V6() non empty total quasi_total complex-valued ext-real-valued real-valued continuous ) Element of K19(K20(REAL : ( ( ) ( non empty V52() V53() V54() V58() V66() ) set ) ,REAL : ( ( ) ( non empty V52() V53() V54() V58() V66() ) set ) ) : ( ( ) ( complex-valued ext-real-valued real-valued ) set ) ) : ( ( ) ( ) set ) ) . q : ( ( real ) ( V30() real ext-real ) number ) ) : ( ( ) ( V30() real ext-real ) Element of REAL : ( ( ) ( non empty V52() V53() V54() V58() V66() ) set ) ) : ( ( ) ( V30() real ext-real ) Element of REAL : ( ( ) ( non empty V52() V53() V54() V58() V66() ) set ) ) ;

theorem :: SIN_COS2:13
exp_R : ( ( V6() quasi_total ) ( V1() V4( REAL : ( ( ) ( non empty V52() V53() V54() V58() V66() ) set ) ) V5( REAL : ( ( ) ( non empty V52() V53() V54() V58() V66() ) set ) ) V6() non empty total quasi_total complex-valued ext-real-valued real-valued continuous ) Element of K19(K20(REAL : ( ( ) ( non empty V52() V53() V54() V58() V66() ) set ) ,REAL : ( ( ) ( non empty V52() V53() V54() V58() V66() ) set ) ) : ( ( ) ( complex-valued ext-real-valued real-valued ) set ) ) : ( ( ) ( ) set ) ) . 0 : ( ( ) ( empty ordinal natural V30() real ext-real non positive non negative V35() V36() V52() V53() V54() V55() V56() V57() V58() ) Element of NAT : ( ( ) ( V52() V53() V54() V55() V56() V57() V58() ) Element of K19(REAL : ( ( ) ( non empty V52() V53() V54() V58() V66() ) set ) ) : ( ( ) ( ) set ) ) ) : ( ( ) ( V30() real ext-real ) Element of REAL : ( ( ) ( non empty V52() V53() V54() V58() V66() ) set ) ) = 1 : ( ( ) ( non empty ordinal natural V30() real ext-real positive non negative V35() V36() V52() V53() V54() V55() V56() V57() ) Element of NAT : ( ( ) ( V52() V53() V54() V55() V56() V57() V58() ) Element of K19(REAL : ( ( ) ( non empty V52() V53() V54() V58() V66() ) set ) ) : ( ( ) ( ) set ) ) ) ;

theorem :: SIN_COS2:14
for p being ( ( real ) ( V30() real ext-real ) number ) holds
( ((cosh : ( ( V6() quasi_total ) ( V1() V4( REAL : ( ( ) ( non empty V52() V53() V54() V58() V66() ) set ) ) V5( REAL : ( ( ) ( non empty V52() V53() V54() V58() V66() ) set ) ) V6() non empty total quasi_total complex-valued ext-real-valued real-valued ) Function of REAL : ( ( ) ( non empty V52() V53() V54() V58() V66() ) set ) , REAL : ( ( ) ( non empty V52() V53() V54() V58() V66() ) set ) ) . p : ( ( real ) ( V30() real ext-real ) number ) ) : ( ( ) ( V30() real ext-real ) Element of REAL : ( ( ) ( non empty V52() V53() V54() V58() V66() ) set ) ) ^2) : ( ( ) ( V30() real ext-real ) Element of REAL : ( ( ) ( non empty V52() V53() V54() V58() V66() ) set ) ) - ((sinh : ( ( V6() quasi_total ) ( V1() V4( REAL : ( ( ) ( non empty V52() V53() V54() V58() V66() ) set ) ) V5( REAL : ( ( ) ( non empty V52() V53() V54() V58() V66() ) set ) ) V6() non empty total quasi_total complex-valued ext-real-valued real-valued ) Function of REAL : ( ( ) ( non empty V52() V53() V54() V58() V66() ) set ) , REAL : ( ( ) ( non empty V52() V53() V54() V58() V66() ) set ) ) . p : ( ( real ) ( V30() real ext-real ) number ) ) : ( ( ) ( V30() real ext-real ) Element of REAL : ( ( ) ( non empty V52() V53() V54() V58() V66() ) set ) ) ^2) : ( ( ) ( V30() real ext-real ) Element of REAL : ( ( ) ( non empty V52() V53() V54() V58() V66() ) set ) ) : ( ( ) ( V30() real ext-real ) Element of REAL : ( ( ) ( non empty V52() V53() V54() V58() V66() ) set ) ) = 1 : ( ( ) ( non empty ordinal natural V30() real ext-real positive non negative V35() V36() V52() V53() V54() V55() V56() V57() ) Element of NAT : ( ( ) ( V52() V53() V54() V55() V56() V57() V58() ) Element of K19(REAL : ( ( ) ( non empty V52() V53() V54() V58() V66() ) set ) ) : ( ( ) ( ) set ) ) ) & ((cosh : ( ( V6() quasi_total ) ( V1() V4( REAL : ( ( ) ( non empty V52() V53() V54() V58() V66() ) set ) ) V5( REAL : ( ( ) ( non empty V52() V53() V54() V58() V66() ) set ) ) V6() non empty total quasi_total complex-valued ext-real-valued real-valued ) Function of REAL : ( ( ) ( non empty V52() V53() V54() V58() V66() ) set ) , REAL : ( ( ) ( non empty V52() V53() V54() V58() V66() ) set ) ) . p : ( ( real ) ( V30() real ext-real ) number ) ) : ( ( ) ( V30() real ext-real ) Element of REAL : ( ( ) ( non empty V52() V53() V54() V58() V66() ) set ) ) * (cosh : ( ( V6() quasi_total ) ( V1() V4( REAL : ( ( ) ( non empty V52() V53() V54() V58() V66() ) set ) ) V5( REAL : ( ( ) ( non empty V52() V53() V54() V58() V66() ) set ) ) V6() non empty total quasi_total complex-valued ext-real-valued real-valued ) Function of REAL : ( ( ) ( non empty V52() V53() V54() V58() V66() ) set ) , REAL : ( ( ) ( non empty V52() V53() V54() V58() V66() ) set ) ) . p : ( ( real ) ( V30() real ext-real ) number ) ) : ( ( ) ( V30() real ext-real ) Element of REAL : ( ( ) ( non empty V52() V53() V54() V58() V66() ) set ) ) ) : ( ( ) ( V30() real ext-real ) Element of REAL : ( ( ) ( non empty V52() V53() V54() V58() V66() ) set ) ) - ((sinh : ( ( V6() quasi_total ) ( V1() V4( REAL : ( ( ) ( non empty V52() V53() V54() V58() V66() ) set ) ) V5( REAL : ( ( ) ( non empty V52() V53() V54() V58() V66() ) set ) ) V6() non empty total quasi_total complex-valued ext-real-valued real-valued ) Function of REAL : ( ( ) ( non empty V52() V53() V54() V58() V66() ) set ) , REAL : ( ( ) ( non empty V52() V53() V54() V58() V66() ) set ) ) . p : ( ( real ) ( V30() real ext-real ) number ) ) : ( ( ) ( V30() real ext-real ) Element of REAL : ( ( ) ( non empty V52() V53() V54() V58() V66() ) set ) ) * (sinh : ( ( V6() quasi_total ) ( V1() V4( REAL : ( ( ) ( non empty V52() V53() V54() V58() V66() ) set ) ) V5( REAL : ( ( ) ( non empty V52() V53() V54() V58() V66() ) set ) ) V6() non empty total quasi_total complex-valued ext-real-valued real-valued ) Function of REAL : ( ( ) ( non empty V52() V53() V54() V58() V66() ) set ) , REAL : ( ( ) ( non empty V52() V53() V54() V58() V66() ) set ) ) . p : ( ( real ) ( V30() real ext-real ) number ) ) : ( ( ) ( V30() real ext-real ) Element of REAL : ( ( ) ( non empty V52() V53() V54() V58() V66() ) set ) ) ) : ( ( ) ( V30() real ext-real ) Element of REAL : ( ( ) ( non empty V52() V53() V54() V58() V66() ) set ) ) : ( ( ) ( V30() real ext-real ) Element of REAL : ( ( ) ( non empty V52() V53() V54() V58() V66() ) set ) ) = 1 : ( ( ) ( non empty ordinal natural V30() real ext-real positive non negative V35() V36() V52() V53() V54() V55() V56() V57() ) Element of NAT : ( ( ) ( V52() V53() V54() V55() V56() V57() V58() ) Element of K19(REAL : ( ( ) ( non empty V52() V53() V54() V58() V66() ) set ) ) : ( ( ) ( ) set ) ) ) ) ;

theorem :: SIN_COS2:15
for p being ( ( real ) ( V30() real ext-real ) number ) holds
( cosh : ( ( V6() quasi_total ) ( V1() V4( REAL : ( ( ) ( non empty V52() V53() V54() V58() V66() ) set ) ) V5( REAL : ( ( ) ( non empty V52() V53() V54() V58() V66() ) set ) ) V6() non empty total quasi_total complex-valued ext-real-valued real-valued ) Function of REAL : ( ( ) ( non empty V52() V53() V54() V58() V66() ) set ) , REAL : ( ( ) ( non empty V52() V53() V54() V58() V66() ) set ) ) . p : ( ( real ) ( V30() real ext-real ) number ) : ( ( ) ( V30() real ext-real ) Element of REAL : ( ( ) ( non empty V52() V53() V54() V58() V66() ) set ) ) <> 0 : ( ( ) ( empty ordinal natural V30() real ext-real non positive non negative V35() V36() V52() V53() V54() V55() V56() V57() V58() ) Element of NAT : ( ( ) ( V52() V53() V54() V55() V56() V57() V58() ) Element of K19(REAL : ( ( ) ( non empty V52() V53() V54() V58() V66() ) set ) ) : ( ( ) ( ) set ) ) ) & cosh : ( ( V6() quasi_total ) ( V1() V4( REAL : ( ( ) ( non empty V52() V53() V54() V58() V66() ) set ) ) V5( REAL : ( ( ) ( non empty V52() V53() V54() V58() V66() ) set ) ) V6() non empty total quasi_total complex-valued ext-real-valued real-valued ) Function of REAL : ( ( ) ( non empty V52() V53() V54() V58() V66() ) set ) , REAL : ( ( ) ( non empty V52() V53() V54() V58() V66() ) set ) ) . p : ( ( real ) ( V30() real ext-real ) number ) : ( ( ) ( V30() real ext-real ) Element of REAL : ( ( ) ( non empty V52() V53() V54() V58() V66() ) set ) ) > 0 : ( ( ) ( empty ordinal natural V30() real ext-real non positive non negative V35() V36() V52() V53() V54() V55() V56() V57() V58() ) Element of NAT : ( ( ) ( V52() V53() V54() V55() V56() V57() V58() ) Element of K19(REAL : ( ( ) ( non empty V52() V53() V54() V58() V66() ) set ) ) : ( ( ) ( ) set ) ) ) & cosh : ( ( V6() quasi_total ) ( V1() V4( REAL : ( ( ) ( non empty V52() V53() V54() V58() V66() ) set ) ) V5( REAL : ( ( ) ( non empty V52() V53() V54() V58() V66() ) set ) ) V6() non empty total quasi_total complex-valued ext-real-valued real-valued ) Function of REAL : ( ( ) ( non empty V52() V53() V54() V58() V66() ) set ) , REAL : ( ( ) ( non empty V52() V53() V54() V58() V66() ) set ) ) . 0 : ( ( ) ( empty ordinal natural V30() real ext-real non positive non negative V35() V36() V52() V53() V54() V55() V56() V57() V58() ) Element of NAT : ( ( ) ( V52() V53() V54() V55() V56() V57() V58() ) Element of K19(REAL : ( ( ) ( non empty V52() V53() V54() V58() V66() ) set ) ) : ( ( ) ( ) set ) ) ) : ( ( ) ( V30() real ext-real ) Element of REAL : ( ( ) ( non empty V52() V53() V54() V58() V66() ) set ) ) = 1 : ( ( ) ( non empty ordinal natural V30() real ext-real positive non negative V35() V36() V52() V53() V54() V55() V56() V57() ) Element of NAT : ( ( ) ( V52() V53() V54() V55() V56() V57() V58() ) Element of K19(REAL : ( ( ) ( non empty V52() V53() V54() V58() V66() ) set ) ) : ( ( ) ( ) set ) ) ) ) ;

theorem :: SIN_COS2:16
sinh : ( ( V6() quasi_total ) ( V1() V4( REAL : ( ( ) ( non empty V52() V53() V54() V58() V66() ) set ) ) V5( REAL : ( ( ) ( non empty V52() V53() V54() V58() V66() ) set ) ) V6() non empty total quasi_total complex-valued ext-real-valued real-valued ) Function of REAL : ( ( ) ( non empty V52() V53() V54() V58() V66() ) set ) , REAL : ( ( ) ( non empty V52() V53() V54() V58() V66() ) set ) ) . 0 : ( ( ) ( empty ordinal natural V30() real ext-real non positive non negative V35() V36() V52() V53() V54() V55() V56() V57() V58() ) Element of NAT : ( ( ) ( V52() V53() V54() V55() V56() V57() V58() ) Element of K19(REAL : ( ( ) ( non empty V52() V53() V54() V58() V66() ) set ) ) : ( ( ) ( ) set ) ) ) : ( ( ) ( V30() real ext-real ) Element of REAL : ( ( ) ( non empty V52() V53() V54() V58() V66() ) set ) ) = 0 : ( ( ) ( empty ordinal natural V30() real ext-real non positive non negative V35() V36() V52() V53() V54() V55() V56() V57() V58() ) Element of NAT : ( ( ) ( V52() V53() V54() V55() V56() V57() V58() ) Element of K19(REAL : ( ( ) ( non empty V52() V53() V54() V58() V66() ) set ) ) : ( ( ) ( ) set ) ) ) ;

theorem :: SIN_COS2:17
for p being ( ( real ) ( V30() real ext-real ) number ) holds tanh : ( ( V6() quasi_total ) ( V1() V4( REAL : ( ( ) ( non empty V52() V53() V54() V58() V66() ) set ) ) V5( REAL : ( ( ) ( non empty V52() V53() V54() V58() V66() ) set ) ) V6() non empty total quasi_total complex-valued ext-real-valued real-valued ) Function of REAL : ( ( ) ( non empty V52() V53() V54() V58() V66() ) set ) , REAL : ( ( ) ( non empty V52() V53() V54() V58() V66() ) set ) ) . p : ( ( real ) ( V30() real ext-real ) number ) : ( ( ) ( V30() real ext-real ) Element of REAL : ( ( ) ( non empty V52() V53() V54() V58() V66() ) set ) ) = (sinh : ( ( V6() quasi_total ) ( V1() V4( REAL : ( ( ) ( non empty V52() V53() V54() V58() V66() ) set ) ) V5( REAL : ( ( ) ( non empty V52() V53() V54() V58() V66() ) set ) ) V6() non empty total quasi_total complex-valued ext-real-valued real-valued ) Function of REAL : ( ( ) ( non empty V52() V53() V54() V58() V66() ) set ) , REAL : ( ( ) ( non empty V52() V53() V54() V58() V66() ) set ) ) . p : ( ( real ) ( V30() real ext-real ) number ) ) : ( ( ) ( V30() real ext-real ) Element of REAL : ( ( ) ( non empty V52() V53() V54() V58() V66() ) set ) ) / (cosh : ( ( V6() quasi_total ) ( V1() V4( REAL : ( ( ) ( non empty V52() V53() V54() V58() V66() ) set ) ) V5( REAL : ( ( ) ( non empty V52() V53() V54() V58() V66() ) set ) ) V6() non empty total quasi_total complex-valued ext-real-valued real-valued ) Function of REAL : ( ( ) ( non empty V52() V53() V54() V58() V66() ) set ) , REAL : ( ( ) ( non empty V52() V53() V54() V58() V66() ) set ) ) . p : ( ( real ) ( V30() real ext-real ) number ) ) : ( ( ) ( V30() real ext-real ) Element of REAL : ( ( ) ( non empty V52() V53() V54() V58() V66() ) set ) ) : ( ( ) ( V30() real ext-real ) Element of REAL : ( ( ) ( non empty V52() V53() V54() V58() V66() ) set ) ) ;

theorem :: SIN_COS2:18
for p being ( ( real ) ( V30() real ext-real ) number ) holds
( (sinh : ( ( V6() quasi_total ) ( V1() V4( REAL : ( ( ) ( non empty V52() V53() V54() V58() V66() ) set ) ) V5( REAL : ( ( ) ( non empty V52() V53() V54() V58() V66() ) set ) ) V6() non empty total quasi_total complex-valued ext-real-valued real-valued ) Function of REAL : ( ( ) ( non empty V52() V53() V54() V58() V66() ) set ) , REAL : ( ( ) ( non empty V52() V53() V54() V58() V66() ) set ) ) . p : ( ( real ) ( V30() real ext-real ) number ) ) : ( ( ) ( V30() real ext-real ) Element of REAL : ( ( ) ( non empty V52() V53() V54() V58() V66() ) set ) ) ^2 : ( ( ) ( V30() real ext-real ) Element of REAL : ( ( ) ( non empty V52() V53() V54() V58() V66() ) set ) ) = (1 : ( ( ) ( non empty ordinal natural V30() real ext-real positive non negative V35() V36() V52() V53() V54() V55() V56() V57() ) Element of NAT : ( ( ) ( V52() V53() V54() V55() V56() V57() V58() ) Element of K19(REAL : ( ( ) ( non empty V52() V53() V54() V58() V66() ) set ) ) : ( ( ) ( ) set ) ) ) / 2 : ( ( ) ( non empty ordinal natural V30() real ext-real positive non negative V35() V36() V52() V53() V54() V55() V56() V57() ) Element of NAT : ( ( ) ( V52() V53() V54() V55() V56() V57() V58() ) Element of K19(REAL : ( ( ) ( non empty V52() V53() V54() V58() V66() ) set ) ) : ( ( ) ( ) set ) ) ) ) : ( ( ) ( V30() real ext-real non negative ) Element of REAL : ( ( ) ( non empty V52() V53() V54() V58() V66() ) set ) ) * ((cosh : ( ( V6() quasi_total ) ( V1() V4( REAL : ( ( ) ( non empty V52() V53() V54() V58() V66() ) set ) ) V5( REAL : ( ( ) ( non empty V52() V53() V54() V58() V66() ) set ) ) V6() non empty total quasi_total complex-valued ext-real-valued real-valued ) Function of REAL : ( ( ) ( non empty V52() V53() V54() V58() V66() ) set ) , REAL : ( ( ) ( non empty V52() V53() V54() V58() V66() ) set ) ) . (2 : ( ( ) ( non empty ordinal natural V30() real ext-real positive non negative V35() V36() V52() V53() V54() V55() V56() V57() ) Element of NAT : ( ( ) ( V52() V53() V54() V55() V56() V57() V58() ) Element of K19(REAL : ( ( ) ( non empty V52() V53() V54() V58() V66() ) set ) ) : ( ( ) ( ) set ) ) ) * p : ( ( real ) ( V30() real ext-real ) number ) ) : ( ( ) ( V30() real ext-real ) Element of REAL : ( ( ) ( non empty V52() V53() V54() V58() V66() ) set ) ) ) : ( ( ) ( V30() real ext-real ) Element of REAL : ( ( ) ( non empty V52() V53() V54() V58() V66() ) set ) ) - 1 : ( ( ) ( non empty ordinal natural V30() real ext-real positive non negative V35() V36() V52() V53() V54() V55() V56() V57() ) Element of NAT : ( ( ) ( V52() V53() V54() V55() V56() V57() V58() ) Element of K19(REAL : ( ( ) ( non empty V52() V53() V54() V58() V66() ) set ) ) : ( ( ) ( ) set ) ) ) ) : ( ( ) ( V30() real ext-real ) Element of REAL : ( ( ) ( non empty V52() V53() V54() V58() V66() ) set ) ) : ( ( ) ( V30() real ext-real ) Element of REAL : ( ( ) ( non empty V52() V53() V54() V58() V66() ) set ) ) & (cosh : ( ( V6() quasi_total ) ( V1() V4( REAL : ( ( ) ( non empty V52() V53() V54() V58() V66() ) set ) ) V5( REAL : ( ( ) ( non empty V52() V53() V54() V58() V66() ) set ) ) V6() non empty total quasi_total complex-valued ext-real-valued real-valued ) Function of REAL : ( ( ) ( non empty V52() V53() V54() V58() V66() ) set ) , REAL : ( ( ) ( non empty V52() V53() V54() V58() V66() ) set ) ) . p : ( ( real ) ( V30() real ext-real ) number ) ) : ( ( ) ( V30() real ext-real ) Element of REAL : ( ( ) ( non empty V52() V53() V54() V58() V66() ) set ) ) ^2 : ( ( ) ( V30() real ext-real ) Element of REAL : ( ( ) ( non empty V52() V53() V54() V58() V66() ) set ) ) = (1 : ( ( ) ( non empty ordinal natural V30() real ext-real positive non negative V35() V36() V52() V53() V54() V55() V56() V57() ) Element of NAT : ( ( ) ( V52() V53() V54() V55() V56() V57() V58() ) Element of K19(REAL : ( ( ) ( non empty V52() V53() V54() V58() V66() ) set ) ) : ( ( ) ( ) set ) ) ) / 2 : ( ( ) ( non empty ordinal natural V30() real ext-real positive non negative V35() V36() V52() V53() V54() V55() V56() V57() ) Element of NAT : ( ( ) ( V52() V53() V54() V55() V56() V57() V58() ) Element of K19(REAL : ( ( ) ( non empty V52() V53() V54() V58() V66() ) set ) ) : ( ( ) ( ) set ) ) ) ) : ( ( ) ( V30() real ext-real non negative ) Element of REAL : ( ( ) ( non empty V52() V53() V54() V58() V66() ) set ) ) * ((cosh : ( ( V6() quasi_total ) ( V1() V4( REAL : ( ( ) ( non empty V52() V53() V54() V58() V66() ) set ) ) V5( REAL : ( ( ) ( non empty V52() V53() V54() V58() V66() ) set ) ) V6() non empty total quasi_total complex-valued ext-real-valued real-valued ) Function of REAL : ( ( ) ( non empty V52() V53() V54() V58() V66() ) set ) , REAL : ( ( ) ( non empty V52() V53() V54() V58() V66() ) set ) ) . (2 : ( ( ) ( non empty ordinal natural V30() real ext-real positive non negative V35() V36() V52() V53() V54() V55() V56() V57() ) Element of NAT : ( ( ) ( V52() V53() V54() V55() V56() V57() V58() ) Element of K19(REAL : ( ( ) ( non empty V52() V53() V54() V58() V66() ) set ) ) : ( ( ) ( ) set ) ) ) * p : ( ( real ) ( V30() real ext-real ) number ) ) : ( ( ) ( V30() real ext-real ) Element of REAL : ( ( ) ( non empty V52() V53() V54() V58() V66() ) set ) ) ) : ( ( ) ( V30() real ext-real ) Element of REAL : ( ( ) ( non empty V52() V53() V54() V58() V66() ) set ) ) + 1 : ( ( ) ( non empty ordinal natural V30() real ext-real positive non negative V35() V36() V52() V53() V54() V55() V56() V57() ) Element of NAT : ( ( ) ( V52() V53() V54() V55() V56() V57() V58() ) Element of K19(REAL : ( ( ) ( non empty V52() V53() V54() V58() V66() ) set ) ) : ( ( ) ( ) set ) ) ) ) : ( ( ) ( V30() real ext-real ) Element of REAL : ( ( ) ( non empty V52() V53() V54() V58() V66() ) set ) ) : ( ( ) ( V30() real ext-real ) Element of REAL : ( ( ) ( non empty V52() V53() V54() V58() V66() ) set ) ) ) ;

theorem :: SIN_COS2:19
for p being ( ( real ) ( V30() real ext-real ) number ) holds
( cosh : ( ( V6() quasi_total ) ( V1() V4( REAL : ( ( ) ( non empty V52() V53() V54() V58() V66() ) set ) ) V5( REAL : ( ( ) ( non empty V52() V53() V54() V58() V66() ) set ) ) V6() non empty total quasi_total complex-valued ext-real-valued real-valued ) Function of REAL : ( ( ) ( non empty V52() V53() V54() V58() V66() ) set ) , REAL : ( ( ) ( non empty V52() V53() V54() V58() V66() ) set ) ) . (- p : ( ( real ) ( V30() real ext-real ) number ) ) : ( ( ) ( V30() real ext-real ) Element of REAL : ( ( ) ( non empty V52() V53() V54() V58() V66() ) set ) ) : ( ( ) ( V30() real ext-real ) Element of REAL : ( ( ) ( non empty V52() V53() V54() V58() V66() ) set ) ) = cosh : ( ( V6() quasi_total ) ( V1() V4( REAL : ( ( ) ( non empty V52() V53() V54() V58() V66() ) set ) ) V5( REAL : ( ( ) ( non empty V52() V53() V54() V58() V66() ) set ) ) V6() non empty total quasi_total complex-valued ext-real-valued real-valued ) Function of REAL : ( ( ) ( non empty V52() V53() V54() V58() V66() ) set ) , REAL : ( ( ) ( non empty V52() V53() V54() V58() V66() ) set ) ) . p : ( ( real ) ( V30() real ext-real ) number ) : ( ( ) ( V30() real ext-real ) Element of REAL : ( ( ) ( non empty V52() V53() V54() V58() V66() ) set ) ) & sinh : ( ( V6() quasi_total ) ( V1() V4( REAL : ( ( ) ( non empty V52() V53() V54() V58() V66() ) set ) ) V5( REAL : ( ( ) ( non empty V52() V53() V54() V58() V66() ) set ) ) V6() non empty total quasi_total complex-valued ext-real-valued real-valued ) Function of REAL : ( ( ) ( non empty V52() V53() V54() V58() V66() ) set ) , REAL : ( ( ) ( non empty V52() V53() V54() V58() V66() ) set ) ) . (- p : ( ( real ) ( V30() real ext-real ) number ) ) : ( ( ) ( V30() real ext-real ) Element of REAL : ( ( ) ( non empty V52() V53() V54() V58() V66() ) set ) ) : ( ( ) ( V30() real ext-real ) Element of REAL : ( ( ) ( non empty V52() V53() V54() V58() V66() ) set ) ) = - (sinh : ( ( V6() quasi_total ) ( V1() V4( REAL : ( ( ) ( non empty V52() V53() V54() V58() V66() ) set ) ) V5( REAL : ( ( ) ( non empty V52() V53() V54() V58() V66() ) set ) ) V6() non empty total quasi_total complex-valued ext-real-valued real-valued ) Function of REAL : ( ( ) ( non empty V52() V53() V54() V58() V66() ) set ) , REAL : ( ( ) ( non empty V52() V53() V54() V58() V66() ) set ) ) . p : ( ( real ) ( V30() real ext-real ) number ) ) : ( ( ) ( V30() real ext-real ) Element of REAL : ( ( ) ( non empty V52() V53() V54() V58() V66() ) set ) ) : ( ( ) ( V30() real ext-real ) Element of REAL : ( ( ) ( non empty V52() V53() V54() V58() V66() ) set ) ) & tanh : ( ( V6() quasi_total ) ( V1() V4( REAL : ( ( ) ( non empty V52() V53() V54() V58() V66() ) set ) ) V5( REAL : ( ( ) ( non empty V52() V53() V54() V58() V66() ) set ) ) V6() non empty total quasi_total complex-valued ext-real-valued real-valued ) Function of REAL : ( ( ) ( non empty V52() V53() V54() V58() V66() ) set ) , REAL : ( ( ) ( non empty V52() V53() V54() V58() V66() ) set ) ) . (- p : ( ( real ) ( V30() real ext-real ) number ) ) : ( ( ) ( V30() real ext-real ) Element of REAL : ( ( ) ( non empty V52() V53() V54() V58() V66() ) set ) ) : ( ( ) ( V30() real ext-real ) Element of REAL : ( ( ) ( non empty V52() V53() V54() V58() V66() ) set ) ) = - (tanh : ( ( V6() quasi_total ) ( V1() V4( REAL : ( ( ) ( non empty V52() V53() V54() V58() V66() ) set ) ) V5( REAL : ( ( ) ( non empty V52() V53() V54() V58() V66() ) set ) ) V6() non empty total quasi_total complex-valued ext-real-valued real-valued ) Function of REAL : ( ( ) ( non empty V52() V53() V54() V58() V66() ) set ) , REAL : ( ( ) ( non empty V52() V53() V54() V58() V66() ) set ) ) . p : ( ( real ) ( V30() real ext-real ) number ) ) : ( ( ) ( V30() real ext-real ) Element of REAL : ( ( ) ( non empty V52() V53() V54() V58() V66() ) set ) ) : ( ( ) ( V30() real ext-real ) Element of REAL : ( ( ) ( non empty V52() V53() V54() V58() V66() ) set ) ) ) ;

theorem :: SIN_COS2:20
for p, r being ( ( real ) ( V30() real ext-real ) number ) holds
( cosh : ( ( V6() quasi_total ) ( V1() V4( REAL : ( ( ) ( non empty V52() V53() V54() V58() V66() ) set ) ) V5( REAL : ( ( ) ( non empty V52() V53() V54() V58() V66() ) set ) ) V6() non empty total quasi_total complex-valued ext-real-valued real-valued ) Function of REAL : ( ( ) ( non empty V52() V53() V54() V58() V66() ) set ) , REAL : ( ( ) ( non empty V52() V53() V54() V58() V66() ) set ) ) . (p : ( ( real ) ( V30() real ext-real ) number ) + r : ( ( real ) ( V30() real ext-real ) number ) ) : ( ( ) ( V30() real ext-real ) Element of REAL : ( ( ) ( non empty V52() V53() V54() V58() V66() ) set ) ) : ( ( ) ( V30() real ext-real ) Element of REAL : ( ( ) ( non empty V52() V53() V54() V58() V66() ) set ) ) = ((cosh : ( ( V6() quasi_total ) ( V1() V4( REAL : ( ( ) ( non empty V52() V53() V54() V58() V66() ) set ) ) V5( REAL : ( ( ) ( non empty V52() V53() V54() V58() V66() ) set ) ) V6() non empty total quasi_total complex-valued ext-real-valued real-valued ) Function of REAL : ( ( ) ( non empty V52() V53() V54() V58() V66() ) set ) , REAL : ( ( ) ( non empty V52() V53() V54() V58() V66() ) set ) ) . p : ( ( real ) ( V30() real ext-real ) number ) ) : ( ( ) ( V30() real ext-real ) Element of REAL : ( ( ) ( non empty V52() V53() V54() V58() V66() ) set ) ) * (cosh : ( ( V6() quasi_total ) ( V1() V4( REAL : ( ( ) ( non empty V52() V53() V54() V58() V66() ) set ) ) V5( REAL : ( ( ) ( non empty V52() V53() V54() V58() V66() ) set ) ) V6() non empty total quasi_total complex-valued ext-real-valued real-valued ) Function of REAL : ( ( ) ( non empty V52() V53() V54() V58() V66() ) set ) , REAL : ( ( ) ( non empty V52() V53() V54() V58() V66() ) set ) ) . r : ( ( real ) ( V30() real ext-real ) number ) ) : ( ( ) ( V30() real ext-real ) Element of REAL : ( ( ) ( non empty V52() V53() V54() V58() V66() ) set ) ) ) : ( ( ) ( V30() real ext-real ) Element of REAL : ( ( ) ( non empty V52() V53() V54() V58() V66() ) set ) ) + ((sinh : ( ( V6() quasi_total ) ( V1() V4( REAL : ( ( ) ( non empty V52() V53() V54() V58() V66() ) set ) ) V5( REAL : ( ( ) ( non empty V52() V53() V54() V58() V66() ) set ) ) V6() non empty total quasi_total complex-valued ext-real-valued real-valued ) Function of REAL : ( ( ) ( non empty V52() V53() V54() V58() V66() ) set ) , REAL : ( ( ) ( non empty V52() V53() V54() V58() V66() ) set ) ) . p : ( ( real ) ( V30() real ext-real ) number ) ) : ( ( ) ( V30() real ext-real ) Element of REAL : ( ( ) ( non empty V52() V53() V54() V58() V66() ) set ) ) * (sinh : ( ( V6() quasi_total ) ( V1() V4( REAL : ( ( ) ( non empty V52() V53() V54() V58() V66() ) set ) ) V5( REAL : ( ( ) ( non empty V52() V53() V54() V58() V66() ) set ) ) V6() non empty total quasi_total complex-valued ext-real-valued real-valued ) Function of REAL : ( ( ) ( non empty V52() V53() V54() V58() V66() ) set ) , REAL : ( ( ) ( non empty V52() V53() V54() V58() V66() ) set ) ) . r : ( ( real ) ( V30() real ext-real ) number ) ) : ( ( ) ( V30() real ext-real ) Element of REAL : ( ( ) ( non empty V52() V53() V54() V58() V66() ) set ) ) ) : ( ( ) ( V30() real ext-real ) Element of REAL : ( ( ) ( non empty V52() V53() V54() V58() V66() ) set ) ) : ( ( ) ( V30() real ext-real ) Element of REAL : ( ( ) ( non empty V52() V53() V54() V58() V66() ) set ) ) & cosh : ( ( V6() quasi_total ) ( V1() V4( REAL : ( ( ) ( non empty V52() V53() V54() V58() V66() ) set ) ) V5( REAL : ( ( ) ( non empty V52() V53() V54() V58() V66() ) set ) ) V6() non empty total quasi_total complex-valued ext-real-valued real-valued ) Function of REAL : ( ( ) ( non empty V52() V53() V54() V58() V66() ) set ) , REAL : ( ( ) ( non empty V52() V53() V54() V58() V66() ) set ) ) . (p : ( ( real ) ( V30() real ext-real ) number ) - r : ( ( real ) ( V30() real ext-real ) number ) ) : ( ( ) ( V30() real ext-real ) Element of REAL : ( ( ) ( non empty V52() V53() V54() V58() V66() ) set ) ) : ( ( ) ( V30() real ext-real ) Element of REAL : ( ( ) ( non empty V52() V53() V54() V58() V66() ) set ) ) = ((cosh : ( ( V6() quasi_total ) ( V1() V4( REAL : ( ( ) ( non empty V52() V53() V54() V58() V66() ) set ) ) V5( REAL : ( ( ) ( non empty V52() V53() V54() V58() V66() ) set ) ) V6() non empty total quasi_total complex-valued ext-real-valued real-valued ) Function of REAL : ( ( ) ( non empty V52() V53() V54() V58() V66() ) set ) , REAL : ( ( ) ( non empty V52() V53() V54() V58() V66() ) set ) ) . p : ( ( real ) ( V30() real ext-real ) number ) ) : ( ( ) ( V30() real ext-real ) Element of REAL : ( ( ) ( non empty V52() V53() V54() V58() V66() ) set ) ) * (cosh : ( ( V6() quasi_total ) ( V1() V4( REAL : ( ( ) ( non empty V52() V53() V54() V58() V66() ) set ) ) V5( REAL : ( ( ) ( non empty V52() V53() V54() V58() V66() ) set ) ) V6() non empty total quasi_total complex-valued ext-real-valued real-valued ) Function of REAL : ( ( ) ( non empty V52() V53() V54() V58() V66() ) set ) , REAL : ( ( ) ( non empty V52() V53() V54() V58() V66() ) set ) ) . r : ( ( real ) ( V30() real ext-real ) number ) ) : ( ( ) ( V30() real ext-real ) Element of REAL : ( ( ) ( non empty V52() V53() V54() V58() V66() ) set ) ) ) : ( ( ) ( V30() real ext-real ) Element of REAL : ( ( ) ( non empty V52() V53() V54() V58() V66() ) set ) ) - ((sinh : ( ( V6() quasi_total ) ( V1() V4( REAL : ( ( ) ( non empty V52() V53() V54() V58() V66() ) set ) ) V5( REAL : ( ( ) ( non empty V52() V53() V54() V58() V66() ) set ) ) V6() non empty total quasi_total complex-valued ext-real-valued real-valued ) Function of REAL : ( ( ) ( non empty V52() V53() V54() V58() V66() ) set ) , REAL : ( ( ) ( non empty V52() V53() V54() V58() V66() ) set ) ) . p : ( ( real ) ( V30() real ext-real ) number ) ) : ( ( ) ( V30() real ext-real ) Element of REAL : ( ( ) ( non empty V52() V53() V54() V58() V66() ) set ) ) * (sinh : ( ( V6() quasi_total ) ( V1() V4( REAL : ( ( ) ( non empty V52() V53() V54() V58() V66() ) set ) ) V5( REAL : ( ( ) ( non empty V52() V53() V54() V58() V66() ) set ) ) V6() non empty total quasi_total complex-valued ext-real-valued real-valued ) Function of REAL : ( ( ) ( non empty V52() V53() V54() V58() V66() ) set ) , REAL : ( ( ) ( non empty V52() V53() V54() V58() V66() ) set ) ) . r : ( ( real ) ( V30() real ext-real ) number ) ) : ( ( ) ( V30() real ext-real ) Element of REAL : ( ( ) ( non empty V52() V53() V54() V58() V66() ) set ) ) ) : ( ( ) ( V30() real ext-real ) Element of REAL : ( ( ) ( non empty V52() V53() V54() V58() V66() ) set ) ) : ( ( ) ( V30() real ext-real ) Element of REAL : ( ( ) ( non empty V52() V53() V54() V58() V66() ) set ) ) ) ;

theorem :: SIN_COS2:21
for p, r being ( ( real ) ( V30() real ext-real ) number ) holds
( sinh : ( ( V6() quasi_total ) ( V1() V4( REAL : ( ( ) ( non empty V52() V53() V54() V58() V66() ) set ) ) V5( REAL : ( ( ) ( non empty V52() V53() V54() V58() V66() ) set ) ) V6() non empty total quasi_total complex-valued ext-real-valued real-valued ) Function of REAL : ( ( ) ( non empty V52() V53() V54() V58() V66() ) set ) , REAL : ( ( ) ( non empty V52() V53() V54() V58() V66() ) set ) ) . (p : ( ( real ) ( V30() real ext-real ) number ) + r : ( ( real ) ( V30() real ext-real ) number ) ) : ( ( ) ( V30() real ext-real ) Element of REAL : ( ( ) ( non empty V52() V53() V54() V58() V66() ) set ) ) : ( ( ) ( V30() real ext-real ) Element of REAL : ( ( ) ( non empty V52() V53() V54() V58() V66() ) set ) ) = ((sinh : ( ( V6() quasi_total ) ( V1() V4( REAL : ( ( ) ( non empty V52() V53() V54() V58() V66() ) set ) ) V5( REAL : ( ( ) ( non empty V52() V53() V54() V58() V66() ) set ) ) V6() non empty total quasi_total complex-valued ext-real-valued real-valued ) Function of REAL : ( ( ) ( non empty V52() V53() V54() V58() V66() ) set ) , REAL : ( ( ) ( non empty V52() V53() V54() V58() V66() ) set ) ) . p : ( ( real ) ( V30() real ext-real ) number ) ) : ( ( ) ( V30() real ext-real ) Element of REAL : ( ( ) ( non empty V52() V53() V54() V58() V66() ) set ) ) * (cosh : ( ( V6() quasi_total ) ( V1() V4( REAL : ( ( ) ( non empty V52() V53() V54() V58() V66() ) set ) ) V5( REAL : ( ( ) ( non empty V52() V53() V54() V58() V66() ) set ) ) V6() non empty total quasi_total complex-valued ext-real-valued real-valued ) Function of REAL : ( ( ) ( non empty V52() V53() V54() V58() V66() ) set ) , REAL : ( ( ) ( non empty V52() V53() V54() V58() V66() ) set ) ) . r : ( ( real ) ( V30() real ext-real ) number ) ) : ( ( ) ( V30() real ext-real ) Element of REAL : ( ( ) ( non empty V52() V53() V54() V58() V66() ) set ) ) ) : ( ( ) ( V30() real ext-real ) Element of REAL : ( ( ) ( non empty V52() V53() V54() V58() V66() ) set ) ) + ((cosh : ( ( V6() quasi_total ) ( V1() V4( REAL : ( ( ) ( non empty V52() V53() V54() V58() V66() ) set ) ) V5( REAL : ( ( ) ( non empty V52() V53() V54() V58() V66() ) set ) ) V6() non empty total quasi_total complex-valued ext-real-valued real-valued ) Function of REAL : ( ( ) ( non empty V52() V53() V54() V58() V66() ) set ) , REAL : ( ( ) ( non empty V52() V53() V54() V58() V66() ) set ) ) . p : ( ( real ) ( V30() real ext-real ) number ) ) : ( ( ) ( V30() real ext-real ) Element of REAL : ( ( ) ( non empty V52() V53() V54() V58() V66() ) set ) ) * (sinh : ( ( V6() quasi_total ) ( V1() V4( REAL : ( ( ) ( non empty V52() V53() V54() V58() V66() ) set ) ) V5( REAL : ( ( ) ( non empty V52() V53() V54() V58() V66() ) set ) ) V6() non empty total quasi_total complex-valued ext-real-valued real-valued ) Function of REAL : ( ( ) ( non empty V52() V53() V54() V58() V66() ) set ) , REAL : ( ( ) ( non empty V52() V53() V54() V58() V66() ) set ) ) . r : ( ( real ) ( V30() real ext-real ) number ) ) : ( ( ) ( V30() real ext-real ) Element of REAL : ( ( ) ( non empty V52() V53() V54() V58() V66() ) set ) ) ) : ( ( ) ( V30() real ext-real ) Element of REAL : ( ( ) ( non empty V52() V53() V54() V58() V66() ) set ) ) : ( ( ) ( V30() real ext-real ) Element of REAL : ( ( ) ( non empty V52() V53() V54() V58() V66() ) set ) ) & sinh : ( ( V6() quasi_total ) ( V1() V4( REAL : ( ( ) ( non empty V52() V53() V54() V58() V66() ) set ) ) V5( REAL : ( ( ) ( non empty V52() V53() V54() V58() V66() ) set ) ) V6() non empty total quasi_total complex-valued ext-real-valued real-valued ) Function of REAL : ( ( ) ( non empty V52() V53() V54() V58() V66() ) set ) , REAL : ( ( ) ( non empty V52() V53() V54() V58() V66() ) set ) ) . (p : ( ( real ) ( V30() real ext-real ) number ) - r : ( ( real ) ( V30() real ext-real ) number ) ) : ( ( ) ( V30() real ext-real ) Element of REAL : ( ( ) ( non empty V52() V53() V54() V58() V66() ) set ) ) : ( ( ) ( V30() real ext-real ) Element of REAL : ( ( ) ( non empty V52() V53() V54() V58() V66() ) set ) ) = ((sinh : ( ( V6() quasi_total ) ( V1() V4( REAL : ( ( ) ( non empty V52() V53() V54() V58() V66() ) set ) ) V5( REAL : ( ( ) ( non empty V52() V53() V54() V58() V66() ) set ) ) V6() non empty total quasi_total complex-valued ext-real-valued real-valued ) Function of REAL : ( ( ) ( non empty V52() V53() V54() V58() V66() ) set ) , REAL : ( ( ) ( non empty V52() V53() V54() V58() V66() ) set ) ) . p : ( ( real ) ( V30() real ext-real ) number ) ) : ( ( ) ( V30() real ext-real ) Element of REAL : ( ( ) ( non empty V52() V53() V54() V58() V66() ) set ) ) * (cosh : ( ( V6() quasi_total ) ( V1() V4( REAL : ( ( ) ( non empty V52() V53() V54() V58() V66() ) set ) ) V5( REAL : ( ( ) ( non empty V52() V53() V54() V58() V66() ) set ) ) V6() non empty total quasi_total complex-valued ext-real-valued real-valued ) Function of REAL : ( ( ) ( non empty V52() V53() V54() V58() V66() ) set ) , REAL : ( ( ) ( non empty V52() V53() V54() V58() V66() ) set ) ) . r : ( ( real ) ( V30() real ext-real ) number ) ) : ( ( ) ( V30() real ext-real ) Element of REAL : ( ( ) ( non empty V52() V53() V54() V58() V66() ) set ) ) ) : ( ( ) ( V30() real ext-real ) Element of REAL : ( ( ) ( non empty V52() V53() V54() V58() V66() ) set ) ) - ((cosh : ( ( V6() quasi_total ) ( V1() V4( REAL : ( ( ) ( non empty V52() V53() V54() V58() V66() ) set ) ) V5( REAL : ( ( ) ( non empty V52() V53() V54() V58() V66() ) set ) ) V6() non empty total quasi_total complex-valued ext-real-valued real-valued ) Function of REAL : ( ( ) ( non empty V52() V53() V54() V58() V66() ) set ) , REAL : ( ( ) ( non empty V52() V53() V54() V58() V66() ) set ) ) . p : ( ( real ) ( V30() real ext-real ) number ) ) : ( ( ) ( V30() real ext-real ) Element of REAL : ( ( ) ( non empty V52() V53() V54() V58() V66() ) set ) ) * (sinh : ( ( V6() quasi_total ) ( V1() V4( REAL : ( ( ) ( non empty V52() V53() V54() V58() V66() ) set ) ) V5( REAL : ( ( ) ( non empty V52() V53() V54() V58() V66() ) set ) ) V6() non empty total quasi_total complex-valued ext-real-valued real-valued ) Function of REAL : ( ( ) ( non empty V52() V53() V54() V58() V66() ) set ) , REAL : ( ( ) ( non empty V52() V53() V54() V58() V66() ) set ) ) . r : ( ( real ) ( V30() real ext-real ) number ) ) : ( ( ) ( V30() real ext-real ) Element of REAL : ( ( ) ( non empty V52() V53() V54() V58() V66() ) set ) ) ) : ( ( ) ( V30() real ext-real ) Element of REAL : ( ( ) ( non empty V52() V53() V54() V58() V66() ) set ) ) : ( ( ) ( V30() real ext-real ) Element of REAL : ( ( ) ( non empty V52() V53() V54() V58() V66() ) set ) ) ) ;

theorem :: SIN_COS2:22
for p, r being ( ( real ) ( V30() real ext-real ) number ) holds
( tanh : ( ( V6() quasi_total ) ( V1() V4( REAL : ( ( ) ( non empty V52() V53() V54() V58() V66() ) set ) ) V5( REAL : ( ( ) ( non empty V52() V53() V54() V58() V66() ) set ) ) V6() non empty total quasi_total complex-valued ext-real-valued real-valued ) Function of REAL : ( ( ) ( non empty V52() V53() V54() V58() V66() ) set ) , REAL : ( ( ) ( non empty V52() V53() V54() V58() V66() ) set ) ) . (p : ( ( real ) ( V30() real ext-real ) number ) + r : ( ( real ) ( V30() real ext-real ) number ) ) : ( ( ) ( V30() real ext-real ) Element of REAL : ( ( ) ( non empty V52() V53() V54() V58() V66() ) set ) ) : ( ( ) ( V30() real ext-real ) Element of REAL : ( ( ) ( non empty V52() V53() V54() V58() V66() ) set ) ) = ((tanh : ( ( V6() quasi_total ) ( V1() V4( REAL : ( ( ) ( non empty V52() V53() V54() V58() V66() ) set ) ) V5( REAL : ( ( ) ( non empty V52() V53() V54() V58() V66() ) set ) ) V6() non empty total quasi_total complex-valued ext-real-valued real-valued ) Function of REAL : ( ( ) ( non empty V52() V53() V54() V58() V66() ) set ) , REAL : ( ( ) ( non empty V52() V53() V54() V58() V66() ) set ) ) . p : ( ( real ) ( V30() real ext-real ) number ) ) : ( ( ) ( V30() real ext-real ) Element of REAL : ( ( ) ( non empty V52() V53() V54() V58() V66() ) set ) ) + (tanh : ( ( V6() quasi_total ) ( V1() V4( REAL : ( ( ) ( non empty V52() V53() V54() V58() V66() ) set ) ) V5( REAL : ( ( ) ( non empty V52() V53() V54() V58() V66() ) set ) ) V6() non empty total quasi_total complex-valued ext-real-valued real-valued ) Function of REAL : ( ( ) ( non empty V52() V53() V54() V58() V66() ) set ) , REAL : ( ( ) ( non empty V52() V53() V54() V58() V66() ) set ) ) . r : ( ( real ) ( V30() real ext-real ) number ) ) : ( ( ) ( V30() real ext-real ) Element of REAL : ( ( ) ( non empty V52() V53() V54() V58() V66() ) set ) ) ) : ( ( ) ( V30() real ext-real ) Element of REAL : ( ( ) ( non empty V52() V53() V54() V58() V66() ) set ) ) / (1 : ( ( ) ( non empty ordinal natural V30() real ext-real positive non negative V35() V36() V52() V53() V54() V55() V56() V57() ) Element of NAT : ( ( ) ( V52() V53() V54() V55() V56() V57() V58() ) Element of K19(REAL : ( ( ) ( non empty V52() V53() V54() V58() V66() ) set ) ) : ( ( ) ( ) set ) ) ) + ((tanh : ( ( V6() quasi_total ) ( V1() V4( REAL : ( ( ) ( non empty V52() V53() V54() V58() V66() ) set ) ) V5( REAL : ( ( ) ( non empty V52() V53() V54() V58() V66() ) set ) ) V6() non empty total quasi_total complex-valued ext-real-valued real-valued ) Function of REAL : ( ( ) ( non empty V52() V53() V54() V58() V66() ) set ) , REAL : ( ( ) ( non empty V52() V53() V54() V58() V66() ) set ) ) . p : ( ( real ) ( V30() real ext-real ) number ) ) : ( ( ) ( V30() real ext-real ) Element of REAL : ( ( ) ( non empty V52() V53() V54() V58() V66() ) set ) ) * (tanh : ( ( V6() quasi_total ) ( V1() V4( REAL : ( ( ) ( non empty V52() V53() V54() V58() V66() ) set ) ) V5( REAL : ( ( ) ( non empty V52() V53() V54() V58() V66() ) set ) ) V6() non empty total quasi_total complex-valued ext-real-valued real-valued ) Function of REAL : ( ( ) ( non empty V52() V53() V54() V58() V66() ) set ) , REAL : ( ( ) ( non empty V52() V53() V54() V58() V66() ) set ) ) . r : ( ( real ) ( V30() real ext-real ) number ) ) : ( ( ) ( V30() real ext-real ) Element of REAL : ( ( ) ( non empty V52() V53() V54() V58() V66() ) set ) ) ) : ( ( ) ( V30() real ext-real ) Element of REAL : ( ( ) ( non empty V52() V53() V54() V58() V66() ) set ) ) ) : ( ( ) ( V30() real ext-real ) Element of REAL : ( ( ) ( non empty V52() V53() V54() V58() V66() ) set ) ) : ( ( ) ( V30() real ext-real ) Element of REAL : ( ( ) ( non empty V52() V53() V54() V58() V66() ) set ) ) & tanh : ( ( V6() quasi_total ) ( V1() V4( REAL : ( ( ) ( non empty V52() V53() V54() V58() V66() ) set ) ) V5( REAL : ( ( ) ( non empty V52() V53() V54() V58() V66() ) set ) ) V6() non empty total quasi_total complex-valued ext-real-valued real-valued ) Function of REAL : ( ( ) ( non empty V52() V53() V54() V58() V66() ) set ) , REAL : ( ( ) ( non empty V52() V53() V54() V58() V66() ) set ) ) . (p : ( ( real ) ( V30() real ext-real ) number ) - r : ( ( real ) ( V30() real ext-real ) number ) ) : ( ( ) ( V30() real ext-real ) Element of REAL : ( ( ) ( non empty V52() V53() V54() V58() V66() ) set ) ) : ( ( ) ( V30() real ext-real ) Element of REAL : ( ( ) ( non empty V52() V53() V54() V58() V66() ) set ) ) = ((tanh : ( ( V6() quasi_total ) ( V1() V4( REAL : ( ( ) ( non empty V52() V53() V54() V58() V66() ) set ) ) V5( REAL : ( ( ) ( non empty V52() V53() V54() V58() V66() ) set ) ) V6() non empty total quasi_total complex-valued ext-real-valued real-valued ) Function of REAL : ( ( ) ( non empty V52() V53() V54() V58() V66() ) set ) , REAL : ( ( ) ( non empty V52() V53() V54() V58() V66() ) set ) ) . p : ( ( real ) ( V30() real ext-real ) number ) ) : ( ( ) ( V30() real ext-real ) Element of REAL : ( ( ) ( non empty V52() V53() V54() V58() V66() ) set ) ) - (tanh : ( ( V6() quasi_total ) ( V1() V4( REAL : ( ( ) ( non empty V52() V53() V54() V58() V66() ) set ) ) V5( REAL : ( ( ) ( non empty V52() V53() V54() V58() V66() ) set ) ) V6() non empty total quasi_total complex-valued ext-real-valued real-valued ) Function of REAL : ( ( ) ( non empty V52() V53() V54() V58() V66() ) set ) , REAL : ( ( ) ( non empty V52() V53() V54() V58() V66() ) set ) ) . r : ( ( real ) ( V30() real ext-real ) number ) ) : ( ( ) ( V30() real ext-real ) Element of REAL : ( ( ) ( non empty V52() V53() V54() V58() V66() ) set ) ) ) : ( ( ) ( V30() real ext-real ) Element of REAL : ( ( ) ( non empty V52() V53() V54() V58() V66() ) set ) ) / (1 : ( ( ) ( non empty ordinal natural V30() real ext-real positive non negative V35() V36() V52() V53() V54() V55() V56() V57() ) Element of NAT : ( ( ) ( V52() V53() V54() V55() V56() V57() V58() ) Element of K19(REAL : ( ( ) ( non empty V52() V53() V54() V58() V66() ) set ) ) : ( ( ) ( ) set ) ) ) - ((tanh : ( ( V6() quasi_total ) ( V1() V4( REAL : ( ( ) ( non empty V52() V53() V54() V58() V66() ) set ) ) V5( REAL : ( ( ) ( non empty V52() V53() V54() V58() V66() ) set ) ) V6() non empty total quasi_total complex-valued ext-real-valued real-valued ) Function of REAL : ( ( ) ( non empty V52() V53() V54() V58() V66() ) set ) , REAL : ( ( ) ( non empty V52() V53() V54() V58() V66() ) set ) ) . p : ( ( real ) ( V30() real ext-real ) number ) ) : ( ( ) ( V30() real ext-real ) Element of REAL : ( ( ) ( non empty V52() V53() V54() V58() V66() ) set ) ) * (tanh : ( ( V6() quasi_total ) ( V1() V4( REAL : ( ( ) ( non empty V52() V53() V54() V58() V66() ) set ) ) V5( REAL : ( ( ) ( non empty V52() V53() V54() V58() V66() ) set ) ) V6() non empty total quasi_total complex-valued ext-real-valued real-valued ) Function of REAL : ( ( ) ( non empty V52() V53() V54() V58() V66() ) set ) , REAL : ( ( ) ( non empty V52() V53() V54() V58() V66() ) set ) ) . r : ( ( real ) ( V30() real ext-real ) number ) ) : ( ( ) ( V30() real ext-real ) Element of REAL : ( ( ) ( non empty V52() V53() V54() V58() V66() ) set ) ) ) : ( ( ) ( V30() real ext-real ) Element of REAL : ( ( ) ( non empty V52() V53() V54() V58() V66() ) set ) ) ) : ( ( ) ( V30() real ext-real ) Element of REAL : ( ( ) ( non empty V52() V53() V54() V58() V66() ) set ) ) : ( ( ) ( V30() real ext-real ) Element of REAL : ( ( ) ( non empty V52() V53() V54() V58() V66() ) set ) ) ) ;

theorem :: SIN_COS2:23
for p being ( ( real ) ( V30() real ext-real ) number ) holds
( sinh : ( ( V6() quasi_total ) ( V1() V4( REAL : ( ( ) ( non empty V52() V53() V54() V58() V66() ) set ) ) V5( REAL : ( ( ) ( non empty V52() V53() V54() V58() V66() ) set ) ) V6() non empty total quasi_total complex-valued ext-real-valued real-valued ) Function of REAL : ( ( ) ( non empty V52() V53() V54() V58() V66() ) set ) , REAL : ( ( ) ( non empty V52() V53() V54() V58() V66() ) set ) ) . (2 : ( ( ) ( non empty ordinal natural V30() real ext-real positive non negative V35() V36() V52() V53() V54() V55() V56() V57() ) Element of NAT : ( ( ) ( V52() V53() V54() V55() V56() V57() V58() ) Element of K19(REAL : ( ( ) ( non empty V52() V53() V54() V58() V66() ) set ) ) : ( ( ) ( ) set ) ) ) * p : ( ( real ) ( V30() real ext-real ) number ) ) : ( ( ) ( V30() real ext-real ) Element of REAL : ( ( ) ( non empty V52() V53() V54() V58() V66() ) set ) ) : ( ( ) ( V30() real ext-real ) Element of REAL : ( ( ) ( non empty V52() V53() V54() V58() V66() ) set ) ) = (2 : ( ( ) ( non empty ordinal natural V30() real ext-real positive non negative V35() V36() V52() V53() V54() V55() V56() V57() ) Element of NAT : ( ( ) ( V52() V53() V54() V55() V56() V57() V58() ) Element of K19(REAL : ( ( ) ( non empty V52() V53() V54() V58() V66() ) set ) ) : ( ( ) ( ) set ) ) ) * (sinh : ( ( V6() quasi_total ) ( V1() V4( REAL : ( ( ) ( non empty V52() V53() V54() V58() V66() ) set ) ) V5( REAL : ( ( ) ( non empty V52() V53() V54() V58() V66() ) set ) ) V6() non empty total quasi_total complex-valued ext-real-valued real-valued ) Function of REAL : ( ( ) ( non empty V52() V53() V54() V58() V66() ) set ) , REAL : ( ( ) ( non empty V52() V53() V54() V58() V66() ) set ) ) . p : ( ( real ) ( V30() real ext-real ) number ) ) : ( ( ) ( V30() real ext-real ) Element of REAL : ( ( ) ( non empty V52() V53() V54() V58() V66() ) set ) ) ) : ( ( ) ( V30() real ext-real ) Element of REAL : ( ( ) ( non empty V52() V53() V54() V58() V66() ) set ) ) * (cosh : ( ( V6() quasi_total ) ( V1() V4( REAL : ( ( ) ( non empty V52() V53() V54() V58() V66() ) set ) ) V5( REAL : ( ( ) ( non empty V52() V53() V54() V58() V66() ) set ) ) V6() non empty total quasi_total complex-valued ext-real-valued real-valued ) Function of REAL : ( ( ) ( non empty V52() V53() V54() V58() V66() ) set ) , REAL : ( ( ) ( non empty V52() V53() V54() V58() V66() ) set ) ) . p : ( ( real ) ( V30() real ext-real ) number ) ) : ( ( ) ( V30() real ext-real ) Element of REAL : ( ( ) ( non empty V52() V53() V54() V58() V66() ) set ) ) : ( ( ) ( V30() real ext-real ) Element of REAL : ( ( ) ( non empty V52() V53() V54() V58() V66() ) set ) ) & cosh : ( ( V6() quasi_total ) ( V1() V4( REAL : ( ( ) ( non empty V52() V53() V54() V58() V66() ) set ) ) V5( REAL : ( ( ) ( non empty V52() V53() V54() V58() V66() ) set ) ) V6() non empty total quasi_total complex-valued ext-real-valued real-valued ) Function of REAL : ( ( ) ( non empty V52() V53() V54() V58() V66() ) set ) , REAL : ( ( ) ( non empty V52() V53() V54() V58() V66() ) set ) ) . (2 : ( ( ) ( non empty ordinal natural V30() real ext-real positive non negative V35() V36() V52() V53() V54() V55() V56() V57() ) Element of NAT : ( ( ) ( V52() V53() V54() V55() V56() V57() V58() ) Element of K19(REAL : ( ( ) ( non empty V52() V53() V54() V58() V66() ) set ) ) : ( ( ) ( ) set ) ) ) * p : ( ( real ) ( V30() real ext-real ) number ) ) : ( ( ) ( V30() real ext-real ) Element of REAL : ( ( ) ( non empty V52() V53() V54() V58() V66() ) set ) ) : ( ( ) ( V30() real ext-real ) Element of REAL : ( ( ) ( non empty V52() V53() V54() V58() V66() ) set ) ) = (2 : ( ( ) ( non empty ordinal natural V30() real ext-real positive non negative V35() V36() V52() V53() V54() V55() V56() V57() ) Element of NAT : ( ( ) ( V52() V53() V54() V55() V56() V57() V58() ) Element of K19(REAL : ( ( ) ( non empty V52() V53() V54() V58() V66() ) set ) ) : ( ( ) ( ) set ) ) ) * ((cosh : ( ( V6() quasi_total ) ( V1() V4( REAL : ( ( ) ( non empty V52() V53() V54() V58() V66() ) set ) ) V5( REAL : ( ( ) ( non empty V52() V53() V54() V58() V66() ) set ) ) V6() non empty total quasi_total complex-valued ext-real-valued real-valued ) Function of REAL : ( ( ) ( non empty V52() V53() V54() V58() V66() ) set ) , REAL : ( ( ) ( non empty V52() V53() V54() V58() V66() ) set ) ) . p : ( ( real ) ( V30() real ext-real ) number ) ) : ( ( ) ( V30() real ext-real ) Element of REAL : ( ( ) ( non empty V52() V53() V54() V58() V66() ) set ) ) ^2) : ( ( ) ( V30() real ext-real ) Element of REAL : ( ( ) ( non empty V52() V53() V54() V58() V66() ) set ) ) ) : ( ( ) ( V30() real ext-real ) Element of REAL : ( ( ) ( non empty V52() V53() V54() V58() V66() ) set ) ) - 1 : ( ( ) ( non empty ordinal natural V30() real ext-real positive non negative V35() V36() V52() V53() V54() V55() V56() V57() ) Element of NAT : ( ( ) ( V52() V53() V54() V55() V56() V57() V58() ) Element of K19(REAL : ( ( ) ( non empty V52() V53() V54() V58() V66() ) set ) ) : ( ( ) ( ) set ) ) ) : ( ( ) ( V30() real ext-real ) Element of REAL : ( ( ) ( non empty V52() V53() V54() V58() V66() ) set ) ) & tanh : ( ( V6() quasi_total ) ( V1() V4( REAL : ( ( ) ( non empty V52() V53() V54() V58() V66() ) set ) ) V5( REAL : ( ( ) ( non empty V52() V53() V54() V58() V66() ) set ) ) V6() non empty total quasi_total complex-valued ext-real-valued real-valued ) Function of REAL : ( ( ) ( non empty V52() V53() V54() V58() V66() ) set ) , REAL : ( ( ) ( non empty V52() V53() V54() V58() V66() ) set ) ) . (2 : ( ( ) ( non empty ordinal natural V30() real ext-real positive non negative V35() V36() V52() V53() V54() V55() V56() V57() ) Element of NAT : ( ( ) ( V52() V53() V54() V55() V56() V57() V58() ) Element of K19(REAL : ( ( ) ( non empty V52() V53() V54() V58() V66() ) set ) ) : ( ( ) ( ) set ) ) ) * p : ( ( real ) ( V30() real ext-real ) number ) ) : ( ( ) ( V30() real ext-real ) Element of REAL : ( ( ) ( non empty V52() V53() V54() V58() V66() ) set ) ) : ( ( ) ( V30() real ext-real ) Element of REAL : ( ( ) ( non empty V52() V53() V54() V58() V66() ) set ) ) = (2 : ( ( ) ( non empty ordinal natural V30() real ext-real positive non negative V35() V36() V52() V53() V54() V55() V56() V57() ) Element of NAT : ( ( ) ( V52() V53() V54() V55() V56() V57() V58() ) Element of K19(REAL : ( ( ) ( non empty V52() V53() V54() V58() V66() ) set ) ) : ( ( ) ( ) set ) ) ) * (tanh : ( ( V6() quasi_total ) ( V1() V4( REAL : ( ( ) ( non empty V52() V53() V54() V58() V66() ) set ) ) V5( REAL : ( ( ) ( non empty V52() V53() V54() V58() V66() ) set ) ) V6() non empty total quasi_total complex-valued ext-real-valued real-valued ) Function of REAL : ( ( ) ( non empty V52() V53() V54() V58() V66() ) set ) , REAL : ( ( ) ( non empty V52() V53() V54() V58() V66() ) set ) ) . p : ( ( real ) ( V30() real ext-real ) number ) ) : ( ( ) ( V30() real ext-real ) Element of REAL : ( ( ) ( non empty V52() V53() V54() V58() V66() ) set ) ) ) : ( ( ) ( V30() real ext-real ) Element of REAL : ( ( ) ( non empty V52() V53() V54() V58() V66() ) set ) ) / (1 : ( ( ) ( non empty ordinal natural V30() real ext-real positive non negative V35() V36() V52() V53() V54() V55() V56() V57() ) Element of NAT : ( ( ) ( V52() V53() V54() V55() V56() V57() V58() ) Element of K19(REAL : ( ( ) ( non empty V52() V53() V54() V58() V66() ) set ) ) : ( ( ) ( ) set ) ) ) + ((tanh : ( ( V6() quasi_total ) ( V1() V4( REAL : ( ( ) ( non empty V52() V53() V54() V58() V66() ) set ) ) V5( REAL : ( ( ) ( non empty V52() V53() V54() V58() V66() ) set ) ) V6() non empty total quasi_total complex-valued ext-real-valued real-valued ) Function of REAL : ( ( ) ( non empty V52() V53() V54() V58() V66() ) set ) , REAL : ( ( ) ( non empty V52() V53() V54() V58() V66() ) set ) ) . p : ( ( real ) ( V30() real ext-real ) number ) ) : ( ( ) ( V30() real ext-real ) Element of REAL : ( ( ) ( non empty V52() V53() V54() V58() V66() ) set ) ) ^2) : ( ( ) ( V30() real ext-real ) Element of REAL : ( ( ) ( non empty V52() V53() V54() V58() V66() ) set ) ) ) : ( ( ) ( V30() real ext-real ) Element of REAL : ( ( ) ( non empty V52() V53() V54() V58() V66() ) set ) ) : ( ( ) ( V30() real ext-real ) Element of REAL : ( ( ) ( non empty V52() V53() V54() V58() V66() ) set ) ) ) ;

theorem :: SIN_COS2:24
for p, q being ( ( real ) ( V30() real ext-real ) number ) holds
( ((sinh : ( ( V6() quasi_total ) ( V1() V4( REAL : ( ( ) ( non empty V52() V53() V54() V58() V66() ) set ) ) V5( REAL : ( ( ) ( non empty V52() V53() V54() V58() V66() ) set ) ) V6() non empty total quasi_total complex-valued ext-real-valued real-valued ) Function of REAL : ( ( ) ( non empty V52() V53() V54() V58() V66() ) set ) , REAL : ( ( ) ( non empty V52() V53() V54() V58() V66() ) set ) ) . p : ( ( real ) ( V30() real ext-real ) number ) ) : ( ( ) ( V30() real ext-real ) Element of REAL : ( ( ) ( non empty V52() V53() V54() V58() V66() ) set ) ) ^2) : ( ( ) ( V30() real ext-real ) Element of REAL : ( ( ) ( non empty V52() V53() V54() V58() V66() ) set ) ) - ((sinh : ( ( V6() quasi_total ) ( V1() V4( REAL : ( ( ) ( non empty V52() V53() V54() V58() V66() ) set ) ) V5( REAL : ( ( ) ( non empty V52() V53() V54() V58() V66() ) set ) ) V6() non empty total quasi_total complex-valued ext-real-valued real-valued ) Function of REAL : ( ( ) ( non empty V52() V53() V54() V58() V66() ) set ) , REAL : ( ( ) ( non empty V52() V53() V54() V58() V66() ) set ) ) . q : ( ( real ) ( V30() real ext-real ) number ) ) : ( ( ) ( V30() real ext-real ) Element of REAL : ( ( ) ( non empty V52() V53() V54() V58() V66() ) set ) ) ^2) : ( ( ) ( V30() real ext-real ) Element of REAL : ( ( ) ( non empty V52() V53() V54() V58() V66() ) set ) ) : ( ( ) ( V30() real ext-real ) Element of REAL : ( ( ) ( non empty V52() V53() V54() V58() V66() ) set ) ) = (sinh : ( ( V6() quasi_total ) ( V1() V4( REAL : ( ( ) ( non empty V52() V53() V54() V58() V66() ) set ) ) V5( REAL : ( ( ) ( non empty V52() V53() V54() V58() V66() ) set ) ) V6() non empty total quasi_total complex-valued ext-real-valued real-valued ) Function of REAL : ( ( ) ( non empty V52() V53() V54() V58() V66() ) set ) , REAL : ( ( ) ( non empty V52() V53() V54() V58() V66() ) set ) ) . (p : ( ( real ) ( V30() real ext-real ) number ) + q : ( ( real ) ( V30() real ext-real ) number ) ) : ( ( ) ( V30() real ext-real ) Element of REAL : ( ( ) ( non empty V52() V53() V54() V58() V66() ) set ) ) ) : ( ( ) ( V30() real ext-real ) Element of REAL : ( ( ) ( non empty V52() V53() V54() V58() V66() ) set ) ) * (sinh : ( ( V6() quasi_total ) ( V1() V4( REAL : ( ( ) ( non empty V52() V53() V54() V58() V66() ) set ) ) V5( REAL : ( ( ) ( non empty V52() V53() V54() V58() V66() ) set ) ) V6() non empty total quasi_total complex-valued ext-real-valued real-valued ) Function of REAL : ( ( ) ( non empty V52() V53() V54() V58() V66() ) set ) , REAL : ( ( ) ( non empty V52() V53() V54() V58() V66() ) set ) ) . (p : ( ( real ) ( V30() real ext-real ) number ) - q : ( ( real ) ( V30() real ext-real ) number ) ) : ( ( ) ( V30() real ext-real ) Element of REAL : ( ( ) ( non empty V52() V53() V54() V58() V66() ) set ) ) ) : ( ( ) ( V30() real ext-real ) Element of REAL : ( ( ) ( non empty V52() V53() V54() V58() V66() ) set ) ) : ( ( ) ( V30() real ext-real ) Element of REAL : ( ( ) ( non empty V52() V53() V54() V58() V66() ) set ) ) & (sinh : ( ( V6() quasi_total ) ( V1() V4( REAL : ( ( ) ( non empty V52() V53() V54() V58() V66() ) set ) ) V5( REAL : ( ( ) ( non empty V52() V53() V54() V58() V66() ) set ) ) V6() non empty total quasi_total complex-valued ext-real-valued real-valued ) Function of REAL : ( ( ) ( non empty V52() V53() V54() V58() V66() ) set ) , REAL : ( ( ) ( non empty V52() V53() V54() V58() V66() ) set ) ) . (p : ( ( real ) ( V30() real ext-real ) number ) + q : ( ( real ) ( V30() real ext-real ) number ) ) : ( ( ) ( V30() real ext-real ) Element of REAL : ( ( ) ( non empty V52() V53() V54() V58() V66() ) set ) ) ) : ( ( ) ( V30() real ext-real ) Element of REAL : ( ( ) ( non empty V52() V53() V54() V58() V66() ) set ) ) * (sinh : ( ( V6() quasi_total ) ( V1() V4( REAL : ( ( ) ( non empty V52() V53() V54() V58() V66() ) set ) ) V5( REAL : ( ( ) ( non empty V52() V53() V54() V58() V66() ) set ) ) V6() non empty total quasi_total complex-valued ext-real-valued real-valued ) Function of REAL : ( ( ) ( non empty V52() V53() V54() V58() V66() ) set ) , REAL : ( ( ) ( non empty V52() V53() V54() V58() V66() ) set ) ) . (p : ( ( real ) ( V30() real ext-real ) number ) - q : ( ( real ) ( V30() real ext-real ) number ) ) : ( ( ) ( V30() real ext-real ) Element of REAL : ( ( ) ( non empty V52() V53() V54() V58() V66() ) set ) ) ) : ( ( ) ( V30() real ext-real ) Element of REAL : ( ( ) ( non empty V52() V53() V54() V58() V66() ) set ) ) : ( ( ) ( V30() real ext-real ) Element of REAL : ( ( ) ( non empty V52() V53() V54() V58() V66() ) set ) ) = ((cosh : ( ( V6() quasi_total ) ( V1() V4( REAL : ( ( ) ( non empty V52() V53() V54() V58() V66() ) set ) ) V5( REAL : ( ( ) ( non empty V52() V53() V54() V58() V66() ) set ) ) V6() non empty total quasi_total complex-valued ext-real-valued real-valued ) Function of REAL : ( ( ) ( non empty V52() V53() V54() V58() V66() ) set ) , REAL : ( ( ) ( non empty V52() V53() V54() V58() V66() ) set ) ) . p : ( ( real ) ( V30() real ext-real ) number ) ) : ( ( ) ( V30() real ext-real ) Element of REAL : ( ( ) ( non empty V52() V53() V54() V58() V66() ) set ) ) ^2) : ( ( ) ( V30() real ext-real ) Element of REAL : ( ( ) ( non empty V52() V53() V54() V58() V66() ) set ) ) - ((cosh : ( ( V6() quasi_total ) ( V1() V4( REAL : ( ( ) ( non empty V52() V53() V54() V58() V66() ) set ) ) V5( REAL : ( ( ) ( non empty V52() V53() V54() V58() V66() ) set ) ) V6() non empty total quasi_total complex-valued ext-real-valued real-valued ) Function of REAL : ( ( ) ( non empty V52() V53() V54() V58() V66() ) set ) , REAL : ( ( ) ( non empty V52() V53() V54() V58() V66() ) set ) ) . q : ( ( real ) ( V30() real ext-real ) number ) ) : ( ( ) ( V30() real ext-real ) Element of REAL : ( ( ) ( non empty V52() V53() V54() V58() V66() ) set ) ) ^2) : ( ( ) ( V30() real ext-real ) Element of REAL : ( ( ) ( non empty V52() V53() V54() V58() V66() ) set ) ) : ( ( ) ( V30() real ext-real ) Element of REAL : ( ( ) ( non empty V52() V53() V54() V58() V66() ) set ) ) & ((sinh : ( ( V6() quasi_total ) ( V1() V4( REAL : ( ( ) ( non empty V52() V53() V54() V58() V66() ) set ) ) V5( REAL : ( ( ) ( non empty V52() V53() V54() V58() V66() ) set ) ) V6() non empty total quasi_total complex-valued ext-real-valued real-valued ) Function of REAL : ( ( ) ( non empty V52() V53() V54() V58() V66() ) set ) , REAL : ( ( ) ( non empty V52() V53() V54() V58() V66() ) set ) ) . p : ( ( real ) ( V30() real ext-real ) number ) ) : ( ( ) ( V30() real ext-real ) Element of REAL : ( ( ) ( non empty V52() V53() V54() V58() V66() ) set ) ) ^2) : ( ( ) ( V30() real ext-real ) Element of REAL : ( ( ) ( non empty V52() V53() V54() V58() V66() ) set ) ) - ((sinh : ( ( V6() quasi_total ) ( V1() V4( REAL : ( ( ) ( non empty V52() V53() V54() V58() V66() ) set ) ) V5( REAL : ( ( ) ( non empty V52() V53() V54() V58() V66() ) set ) ) V6() non empty total quasi_total complex-valued ext-real-valued real-valued ) Function of REAL : ( ( ) ( non empty V52() V53() V54() V58() V66() ) set ) , REAL : ( ( ) ( non empty V52() V53() V54() V58() V66() ) set ) ) . q : ( ( real ) ( V30() real ext-real ) number ) ) : ( ( ) ( V30() real ext-real ) Element of REAL : ( ( ) ( non empty V52() V53() V54() V58() V66() ) set ) ) ^2) : ( ( ) ( V30() real ext-real ) Element of REAL : ( ( ) ( non empty V52() V53() V54() V58() V66() ) set ) ) : ( ( ) ( V30() real ext-real ) Element of REAL : ( ( ) ( non empty V52() V53() V54() V58() V66() ) set ) ) = ((cosh : ( ( V6() quasi_total ) ( V1() V4( REAL : ( ( ) ( non empty V52() V53() V54() V58() V66() ) set ) ) V5( REAL : ( ( ) ( non empty V52() V53() V54() V58() V66() ) set ) ) V6() non empty total quasi_total complex-valued ext-real-valued real-valued ) Function of REAL : ( ( ) ( non empty V52() V53() V54() V58() V66() ) set ) , REAL : ( ( ) ( non empty V52() V53() V54() V58() V66() ) set ) ) . p : ( ( real ) ( V30() real ext-real ) number ) ) : ( ( ) ( V30() real ext-real ) Element of REAL : ( ( ) ( non empty V52() V53() V54() V58() V66() ) set ) ) ^2) : ( ( ) ( V30() real ext-real ) Element of REAL : ( ( ) ( non empty V52() V53() V54() V58() V66() ) set ) ) - ((cosh : ( ( V6() quasi_total ) ( V1() V4( REAL : ( ( ) ( non empty V52() V53() V54() V58() V66() ) set ) ) V5( REAL : ( ( ) ( non empty V52() V53() V54() V58() V66() ) set ) ) V6() non empty total quasi_total complex-valued ext-real-valued real-valued ) Function of REAL : ( ( ) ( non empty V52() V53() V54() V58() V66() ) set ) , REAL : ( ( ) ( non empty V52() V53() V54() V58() V66() ) set ) ) . q : ( ( real ) ( V30() real ext-real ) number ) ) : ( ( ) ( V30() real ext-real ) Element of REAL : ( ( ) ( non empty V52() V53() V54() V58() V66() ) set ) ) ^2) : ( ( ) ( V30() real ext-real ) Element of REAL : ( ( ) ( non empty V52() V53() V54() V58() V66() ) set ) ) : ( ( ) ( V30() real ext-real ) Element of REAL : ( ( ) ( non empty V52() V53() V54() V58() V66() ) set ) ) ) ;

theorem :: SIN_COS2:25
for p, q being ( ( real ) ( V30() real ext-real ) number ) holds
( ((sinh : ( ( V6() quasi_total ) ( V1() V4( REAL : ( ( ) ( non empty V52() V53() V54() V58() V66() ) set ) ) V5( REAL : ( ( ) ( non empty V52() V53() V54() V58() V66() ) set ) ) V6() non empty total quasi_total complex-valued ext-real-valued real-valued ) Function of REAL : ( ( ) ( non empty V52() V53() V54() V58() V66() ) set ) , REAL : ( ( ) ( non empty V52() V53() V54() V58() V66() ) set ) ) . p : ( ( real ) ( V30() real ext-real ) number ) ) : ( ( ) ( V30() real ext-real ) Element of REAL : ( ( ) ( non empty V52() V53() V54() V58() V66() ) set ) ) ^2) : ( ( ) ( V30() real ext-real ) Element of REAL : ( ( ) ( non empty V52() V53() V54() V58() V66() ) set ) ) + ((cosh : ( ( V6() quasi_total ) ( V1() V4( REAL : ( ( ) ( non empty V52() V53() V54() V58() V66() ) set ) ) V5( REAL : ( ( ) ( non empty V52() V53() V54() V58() V66() ) set ) ) V6() non empty total quasi_total complex-valued ext-real-valued real-valued ) Function of REAL : ( ( ) ( non empty V52() V53() V54() V58() V66() ) set ) , REAL : ( ( ) ( non empty V52() V53() V54() V58() V66() ) set ) ) . q : ( ( real ) ( V30() real ext-real ) number ) ) : ( ( ) ( V30() real ext-real ) Element of REAL : ( ( ) ( non empty V52() V53() V54() V58() V66() ) set ) ) ^2) : ( ( ) ( V30() real ext-real ) Element of REAL : ( ( ) ( non empty V52() V53() V54() V58() V66() ) set ) ) : ( ( ) ( V30() real ext-real ) Element of REAL : ( ( ) ( non empty V52() V53() V54() V58() V66() ) set ) ) = (cosh : ( ( V6() quasi_total ) ( V1() V4( REAL : ( ( ) ( non empty V52() V53() V54() V58() V66() ) set ) ) V5( REAL : ( ( ) ( non empty V52() V53() V54() V58() V66() ) set ) ) V6() non empty total quasi_total complex-valued ext-real-valued real-valued ) Function of REAL : ( ( ) ( non empty V52() V53() V54() V58() V66() ) set ) , REAL : ( ( ) ( non empty V52() V53() V54() V58() V66() ) set ) ) . (p : ( ( real ) ( V30() real ext-real ) number ) + q : ( ( real ) ( V30() real ext-real ) number ) ) : ( ( ) ( V30() real ext-real ) Element of REAL : ( ( ) ( non empty V52() V53() V54() V58() V66() ) set ) ) ) : ( ( ) ( V30() real ext-real ) Element of REAL : ( ( ) ( non empty V52() V53() V54() V58() V66() ) set ) ) * (cosh : ( ( V6() quasi_total ) ( V1() V4( REAL : ( ( ) ( non empty V52() V53() V54() V58() V66() ) set ) ) V5( REAL : ( ( ) ( non empty V52() V53() V54() V58() V66() ) set ) ) V6() non empty total quasi_total complex-valued ext-real-valued real-valued ) Function of REAL : ( ( ) ( non empty V52() V53() V54() V58() V66() ) set ) , REAL : ( ( ) ( non empty V52() V53() V54() V58() V66() ) set ) ) . (p : ( ( real ) ( V30() real ext-real ) number ) - q : ( ( real ) ( V30() real ext-real ) number ) ) : ( ( ) ( V30() real ext-real ) Element of REAL : ( ( ) ( non empty V52() V53() V54() V58() V66() ) set ) ) ) : ( ( ) ( V30() real ext-real ) Element of REAL : ( ( ) ( non empty V52() V53() V54() V58() V66() ) set ) ) : ( ( ) ( V30() real ext-real ) Element of REAL : ( ( ) ( non empty V52() V53() V54() V58() V66() ) set ) ) & (cosh : ( ( V6() quasi_total ) ( V1() V4( REAL : ( ( ) ( non empty V52() V53() V54() V58() V66() ) set ) ) V5( REAL : ( ( ) ( non empty V52() V53() V54() V58() V66() ) set ) ) V6() non empty total quasi_total complex-valued ext-real-valued real-valued ) Function of REAL : ( ( ) ( non empty V52() V53() V54() V58() V66() ) set ) , REAL : ( ( ) ( non empty V52() V53() V54() V58() V66() ) set ) ) . (p : ( ( real ) ( V30() real ext-real ) number ) + q : ( ( real ) ( V30() real ext-real ) number ) ) : ( ( ) ( V30() real ext-real ) Element of REAL : ( ( ) ( non empty V52() V53() V54() V58() V66() ) set ) ) ) : ( ( ) ( V30() real ext-real ) Element of REAL : ( ( ) ( non empty V52() V53() V54() V58() V66() ) set ) ) * (cosh : ( ( V6() quasi_total ) ( V1() V4( REAL : ( ( ) ( non empty V52() V53() V54() V58() V66() ) set ) ) V5( REAL : ( ( ) ( non empty V52() V53() V54() V58() V66() ) set ) ) V6() non empty total quasi_total complex-valued ext-real-valued real-valued ) Function of REAL : ( ( ) ( non empty V52() V53() V54() V58() V66() ) set ) , REAL : ( ( ) ( non empty V52() V53() V54() V58() V66() ) set ) ) . (p : ( ( real ) ( V30() real ext-real ) number ) - q : ( ( real ) ( V30() real ext-real ) number ) ) : ( ( ) ( V30() real ext-real ) Element of REAL : ( ( ) ( non empty V52() V53() V54() V58() V66() ) set ) ) ) : ( ( ) ( V30() real ext-real ) Element of REAL : ( ( ) ( non empty V52() V53() V54() V58() V66() ) set ) ) : ( ( ) ( V30() real ext-real ) Element of REAL : ( ( ) ( non empty V52() V53() V54() V58() V66() ) set ) ) = ((cosh : ( ( V6() quasi_total ) ( V1() V4( REAL : ( ( ) ( non empty V52() V53() V54() V58() V66() ) set ) ) V5( REAL : ( ( ) ( non empty V52() V53() V54() V58() V66() ) set ) ) V6() non empty total quasi_total complex-valued ext-real-valued real-valued ) Function of REAL : ( ( ) ( non empty V52() V53() V54() V58() V66() ) set ) , REAL : ( ( ) ( non empty V52() V53() V54() V58() V66() ) set ) ) . p : ( ( real ) ( V30() real ext-real ) number ) ) : ( ( ) ( V30() real ext-real ) Element of REAL : ( ( ) ( non empty V52() V53() V54() V58() V66() ) set ) ) ^2) : ( ( ) ( V30() real ext-real ) Element of REAL : ( ( ) ( non empty V52() V53() V54() V58() V66() ) set ) ) + ((sinh : ( ( V6() quasi_total ) ( V1() V4( REAL : ( ( ) ( non empty V52() V53() V54() V58() V66() ) set ) ) V5( REAL : ( ( ) ( non empty V52() V53() V54() V58() V66() ) set ) ) V6() non empty total quasi_total complex-valued ext-real-valued real-valued ) Function of REAL : ( ( ) ( non empty V52() V53() V54() V58() V66() ) set ) , REAL : ( ( ) ( non empty V52() V53() V54() V58() V66() ) set ) ) . q : ( ( real ) ( V30() real ext-real ) number ) ) : ( ( ) ( V30() real ext-real ) Element of REAL : ( ( ) ( non empty V52() V53() V54() V58() V66() ) set ) ) ^2) : ( ( ) ( V30() real ext-real ) Element of REAL : ( ( ) ( non empty V52() V53() V54() V58() V66() ) set ) ) : ( ( ) ( V30() real ext-real ) Element of REAL : ( ( ) ( non empty V52() V53() V54() V58() V66() ) set ) ) & ((sinh : ( ( V6() quasi_total ) ( V1() V4( REAL : ( ( ) ( non empty V52() V53() V54() V58() V66() ) set ) ) V5( REAL : ( ( ) ( non empty V52() V53() V54() V58() V66() ) set ) ) V6() non empty total quasi_total complex-valued ext-real-valued real-valued ) Function of REAL : ( ( ) ( non empty V52() V53() V54() V58() V66() ) set ) , REAL : ( ( ) ( non empty V52() V53() V54() V58() V66() ) set ) ) . p : ( ( real ) ( V30() real ext-real ) number ) ) : ( ( ) ( V30() real ext-real ) Element of REAL : ( ( ) ( non empty V52() V53() V54() V58() V66() ) set ) ) ^2) : ( ( ) ( V30() real ext-real ) Element of REAL : ( ( ) ( non empty V52() V53() V54() V58() V66() ) set ) ) + ((cosh : ( ( V6() quasi_total ) ( V1() V4( REAL : ( ( ) ( non empty V52() V53() V54() V58() V66() ) set ) ) V5( REAL : ( ( ) ( non empty V52() V53() V54() V58() V66() ) set ) ) V6() non empty total quasi_total complex-valued ext-real-valued real-valued ) Function of REAL : ( ( ) ( non empty V52() V53() V54() V58() V66() ) set ) , REAL : ( ( ) ( non empty V52() V53() V54() V58() V66() ) set ) ) . q : ( ( real ) ( V30() real ext-real ) number ) ) : ( ( ) ( V30() real ext-real ) Element of REAL : ( ( ) ( non empty V52() V53() V54() V58() V66() ) set ) ) ^2) : ( ( ) ( V30() real ext-real ) Element of REAL : ( ( ) ( non empty V52() V53() V54() V58() V66() ) set ) ) : ( ( ) ( V30() real ext-real ) Element of REAL : ( ( ) ( non empty V52() V53() V54() V58() V66() ) set ) ) = ((cosh : ( ( V6() quasi_total ) ( V1() V4( REAL : ( ( ) ( non empty V52() V53() V54() V58() V66() ) set ) ) V5( REAL : ( ( ) ( non empty V52() V53() V54() V58() V66() ) set ) ) V6() non empty total quasi_total complex-valued ext-real-valued real-valued ) Function of REAL : ( ( ) ( non empty V52() V53() V54() V58() V66() ) set ) , REAL : ( ( ) ( non empty V52() V53() V54() V58() V66() ) set ) ) . p : ( ( real ) ( V30() real ext-real ) number ) ) : ( ( ) ( V30() real ext-real ) Element of REAL : ( ( ) ( non empty V52() V53() V54() V58() V66() ) set ) ) ^2) : ( ( ) ( V30() real ext-real ) Element of REAL : ( ( ) ( non empty V52() V53() V54() V58() V66() ) set ) ) + ((sinh : ( ( V6() quasi_total ) ( V1() V4( REAL : ( ( ) ( non empty V52() V53() V54() V58() V66() ) set ) ) V5( REAL : ( ( ) ( non empty V52() V53() V54() V58() V66() ) set ) ) V6() non empty total quasi_total complex-valued ext-real-valued real-valued ) Function of REAL : ( ( ) ( non empty V52() V53() V54() V58() V66() ) set ) , REAL : ( ( ) ( non empty V52() V53() V54() V58() V66() ) set ) ) . q : ( ( real ) ( V30() real ext-real ) number ) ) : ( ( ) ( V30() real ext-real ) Element of REAL : ( ( ) ( non empty V52() V53() V54() V58() V66() ) set ) ) ^2) : ( ( ) ( V30() real ext-real ) Element of REAL : ( ( ) ( non empty V52() V53() V54() V58() V66() ) set ) ) : ( ( ) ( V30() real ext-real ) Element of REAL : ( ( ) ( non empty V52() V53() V54() V58() V66() ) set ) ) ) ;

theorem :: SIN_COS2:26
for p, r being ( ( real ) ( V30() real ext-real ) number ) holds
( (sinh : ( ( V6() quasi_total ) ( V1() V4( REAL : ( ( ) ( non empty V52() V53() V54() V58() V66() ) set ) ) V5( REAL : ( ( ) ( non empty V52() V53() V54() V58() V66() ) set ) ) V6() non empty total quasi_total complex-valued ext-real-valued real-valued ) Function of REAL : ( ( ) ( non empty V52() V53() V54() V58() V66() ) set ) , REAL : ( ( ) ( non empty V52() V53() V54() V58() V66() ) set ) ) . p : ( ( real ) ( V30() real ext-real ) number ) ) : ( ( ) ( V30() real ext-real ) Element of REAL : ( ( ) ( non empty V52() V53() V54() V58() V66() ) set ) ) + (sinh : ( ( V6() quasi_total ) ( V1() V4( REAL : ( ( ) ( non empty V52() V53() V54() V58() V66() ) set ) ) V5( REAL : ( ( ) ( non empty V52() V53() V54() V58() V66() ) set ) ) V6() non empty total quasi_total complex-valued ext-real-valued real-valued ) Function of REAL : ( ( ) ( non empty V52() V53() V54() V58() V66() ) set ) , REAL : ( ( ) ( non empty V52() V53() V54() V58() V66() ) set ) ) . r : ( ( real ) ( V30() real ext-real ) number ) ) : ( ( ) ( V30() real ext-real ) Element of REAL : ( ( ) ( non empty V52() V53() V54() V58() V66() ) set ) ) : ( ( ) ( V30() real ext-real ) Element of REAL : ( ( ) ( non empty V52() V53() V54() V58() V66() ) set ) ) = (2 : ( ( ) ( non empty ordinal natural V30() real ext-real positive non negative V35() V36() V52() V53() V54() V55() V56() V57() ) Element of NAT : ( ( ) ( V52() V53() V54() V55() V56() V57() V58() ) Element of K19(REAL : ( ( ) ( non empty V52() V53() V54() V58() V66() ) set ) ) : ( ( ) ( ) set ) ) ) * (sinh : ( ( V6() quasi_total ) ( V1() V4( REAL : ( ( ) ( non empty V52() V53() V54() V58() V66() ) set ) ) V5( REAL : ( ( ) ( non empty V52() V53() V54() V58() V66() ) set ) ) V6() non empty total quasi_total complex-valued ext-real-valued real-valued ) Function of REAL : ( ( ) ( non empty V52() V53() V54() V58() V66() ) set ) , REAL : ( ( ) ( non empty V52() V53() V54() V58() V66() ) set ) ) . ((p : ( ( real ) ( V30() real ext-real ) number ) / 2 : ( ( ) ( non empty ordinal natural V30() real ext-real positive non negative V35() V36() V52() V53() V54() V55() V56() V57() ) Element of NAT : ( ( ) ( V52() V53() V54() V55() V56() V57() V58() ) Element of K19(REAL : ( ( ) ( non empty V52() V53() V54() V58() V66() ) set ) ) : ( ( ) ( ) set ) ) ) ) : ( ( ) ( V30() real ext-real ) Element of REAL : ( ( ) ( non empty V52() V53() V54() V58() V66() ) set ) ) + (r : ( ( real ) ( V30() real ext-real ) number ) / 2 : ( ( ) ( non empty ordinal natural V30() real ext-real positive non negative V35() V36() V52() V53() V54() V55() V56() V57() ) Element of NAT : ( ( ) ( V52() V53() V54() V55() V56() V57() V58() ) Element of K19(REAL : ( ( ) ( non empty V52() V53() V54() V58() V66() ) set ) ) : ( ( ) ( ) set ) ) ) ) : ( ( ) ( V30() real ext-real ) Element of REAL : ( ( ) ( non empty V52() V53() V54() V58() V66() ) set ) ) ) : ( ( ) ( V30() real ext-real ) Element of REAL : ( ( ) ( non empty V52() V53() V54() V58() V66() ) set ) ) ) : ( ( ) ( V30() real ext-real ) Element of REAL : ( ( ) ( non empty V52() V53() V54() V58() V66() ) set ) ) ) : ( ( ) ( V30() real ext-real ) Element of REAL : ( ( ) ( non empty V52() V53() V54() V58() V66() ) set ) ) * (cosh : ( ( V6() quasi_total ) ( V1() V4( REAL : ( ( ) ( non empty V52() V53() V54() V58() V66() ) set ) ) V5( REAL : ( ( ) ( non empty V52() V53() V54() V58() V66() ) set ) ) V6() non empty total quasi_total complex-valued ext-real-valued real-valued ) Function of REAL : ( ( ) ( non empty V52() V53() V54() V58() V66() ) set ) , REAL : ( ( ) ( non empty V52() V53() V54() V58() V66() ) set ) ) . ((p : ( ( real ) ( V30() real ext-real ) number ) / 2 : ( ( ) ( non empty ordinal natural V30() real ext-real positive non negative V35() V36() V52() V53() V54() V55() V56() V57() ) Element of NAT : ( ( ) ( V52() V53() V54() V55() V56() V57() V58() ) Element of K19(REAL : ( ( ) ( non empty V52() V53() V54() V58() V66() ) set ) ) : ( ( ) ( ) set ) ) ) ) : ( ( ) ( V30() real ext-real ) Element of REAL : ( ( ) ( non empty V52() V53() V54() V58() V66() ) set ) ) - (r : ( ( real ) ( V30() real ext-real ) number ) / 2 : ( ( ) ( non empty ordinal natural V30() real ext-real positive non negative V35() V36() V52() V53() V54() V55() V56() V57() ) Element of NAT : ( ( ) ( V52() V53() V54() V55() V56() V57() V58() ) Element of K19(REAL : ( ( ) ( non empty V52() V53() V54() V58() V66() ) set ) ) : ( ( ) ( ) set ) ) ) ) : ( ( ) ( V30() real ext-real ) Element of REAL : ( ( ) ( non empty V52() V53() V54() V58() V66() ) set ) ) ) : ( ( ) ( V30() real ext-real ) Element of REAL : ( ( ) ( non empty V52() V53() V54() V58() V66() ) set ) ) ) : ( ( ) ( V30() real ext-real ) Element of REAL : ( ( ) ( non empty V52() V53() V54() V58() V66() ) set ) ) : ( ( ) ( V30() real ext-real ) Element of REAL : ( ( ) ( non empty V52() V53() V54() V58() V66() ) set ) ) & (sinh : ( ( V6() quasi_total ) ( V1() V4( REAL : ( ( ) ( non empty V52() V53() V54() V58() V66() ) set ) ) V5( REAL : ( ( ) ( non empty V52() V53() V54() V58() V66() ) set ) ) V6() non empty total quasi_total complex-valued ext-real-valued real-valued ) Function of REAL : ( ( ) ( non empty V52() V53() V54() V58() V66() ) set ) , REAL : ( ( ) ( non empty V52() V53() V54() V58() V66() ) set ) ) . p : ( ( real ) ( V30() real ext-real ) number ) ) : ( ( ) ( V30() real ext-real ) Element of REAL : ( ( ) ( non empty V52() V53() V54() V58() V66() ) set ) ) - (sinh : ( ( V6() quasi_total ) ( V1() V4( REAL : ( ( ) ( non empty V52() V53() V54() V58() V66() ) set ) ) V5( REAL : ( ( ) ( non empty V52() V53() V54() V58() V66() ) set ) ) V6() non empty total quasi_total complex-valued ext-real-valued real-valued ) Function of REAL : ( ( ) ( non empty V52() V53() V54() V58() V66() ) set ) , REAL : ( ( ) ( non empty V52() V53() V54() V58() V66() ) set ) ) . r : ( ( real ) ( V30() real ext-real ) number ) ) : ( ( ) ( V30() real ext-real ) Element of REAL : ( ( ) ( non empty V52() V53() V54() V58() V66() ) set ) ) : ( ( ) ( V30() real ext-real ) Element of REAL : ( ( ) ( non empty V52() V53() V54() V58() V66() ) set ) ) = (2 : ( ( ) ( non empty ordinal natural V30() real ext-real positive non negative V35() V36() V52() V53() V54() V55() V56() V57() ) Element of NAT : ( ( ) ( V52() V53() V54() V55() V56() V57() V58() ) Element of K19(REAL : ( ( ) ( non empty V52() V53() V54() V58() V66() ) set ) ) : ( ( ) ( ) set ) ) ) * (sinh : ( ( V6() quasi_total ) ( V1() V4( REAL : ( ( ) ( non empty V52() V53() V54() V58() V66() ) set ) ) V5( REAL : ( ( ) ( non empty V52() V53() V54() V58() V66() ) set ) ) V6() non empty total quasi_total complex-valued ext-real-valued real-valued ) Function of REAL : ( ( ) ( non empty V52() V53() V54() V58() V66() ) set ) , REAL : ( ( ) ( non empty V52() V53() V54() V58() V66() ) set ) ) . ((p : ( ( real ) ( V30() real ext-real ) number ) / 2 : ( ( ) ( non empty ordinal natural V30() real ext-real positive non negative V35() V36() V52() V53() V54() V55() V56() V57() ) Element of NAT : ( ( ) ( V52() V53() V54() V55() V56() V57() V58() ) Element of K19(REAL : ( ( ) ( non empty V52() V53() V54() V58() V66() ) set ) ) : ( ( ) ( ) set ) ) ) ) : ( ( ) ( V30() real ext-real ) Element of REAL : ( ( ) ( non empty V52() V53() V54() V58() V66() ) set ) ) - (r : ( ( real ) ( V30() real ext-real ) number ) / 2 : ( ( ) ( non empty ordinal natural V30() real ext-real positive non negative V35() V36() V52() V53() V54() V55() V56() V57() ) Element of NAT : ( ( ) ( V52() V53() V54() V55() V56() V57() V58() ) Element of K19(REAL : ( ( ) ( non empty V52() V53() V54() V58() V66() ) set ) ) : ( ( ) ( ) set ) ) ) ) : ( ( ) ( V30() real ext-real ) Element of REAL : ( ( ) ( non empty V52() V53() V54() V58() V66() ) set ) ) ) : ( ( ) ( V30() real ext-real ) Element of REAL : ( ( ) ( non empty V52() V53() V54() V58() V66() ) set ) ) ) : ( ( ) ( V30() real ext-real ) Element of REAL : ( ( ) ( non empty V52() V53() V54() V58() V66() ) set ) ) ) : ( ( ) ( V30() real ext-real ) Element of REAL : ( ( ) ( non empty V52() V53() V54() V58() V66() ) set ) ) * (cosh : ( ( V6() quasi_total ) ( V1() V4( REAL : ( ( ) ( non empty V52() V53() V54() V58() V66() ) set ) ) V5( REAL : ( ( ) ( non empty V52() V53() V54() V58() V66() ) set ) ) V6() non empty total quasi_total complex-valued ext-real-valued real-valued ) Function of REAL : ( ( ) ( non empty V52() V53() V54() V58() V66() ) set ) , REAL : ( ( ) ( non empty V52() V53() V54() V58() V66() ) set ) ) . ((p : ( ( real ) ( V30() real ext-real ) number ) / 2 : ( ( ) ( non empty ordinal natural V30() real ext-real positive non negative V35() V36() V52() V53() V54() V55() V56() V57() ) Element of NAT : ( ( ) ( V52() V53() V54() V55() V56() V57() V58() ) Element of K19(REAL : ( ( ) ( non empty V52() V53() V54() V58() V66() ) set ) ) : ( ( ) ( ) set ) ) ) ) : ( ( ) ( V30() real ext-real ) Element of REAL : ( ( ) ( non empty V52() V53() V54() V58() V66() ) set ) ) + (r : ( ( real ) ( V30() real ext-real ) number ) / 2 : ( ( ) ( non empty ordinal natural V30() real ext-real positive non negative V35() V36() V52() V53() V54() V55() V56() V57() ) Element of NAT : ( ( ) ( V52() V53() V54() V55() V56() V57() V58() ) Element of K19(REAL : ( ( ) ( non empty V52() V53() V54() V58() V66() ) set ) ) : ( ( ) ( ) set ) ) ) ) : ( ( ) ( V30() real ext-real ) Element of REAL : ( ( ) ( non empty V52() V53() V54() V58() V66() ) set ) ) ) : ( ( ) ( V30() real ext-real ) Element of REAL : ( ( ) ( non empty V52() V53() V54() V58() V66() ) set ) ) ) : ( ( ) ( V30() real ext-real ) Element of REAL : ( ( ) ( non empty V52() V53() V54() V58() V66() ) set ) ) : ( ( ) ( V30() real ext-real ) Element of REAL : ( ( ) ( non empty V52() V53() V54() V58() V66() ) set ) ) ) ;

theorem :: SIN_COS2:27
for p, r being ( ( real ) ( V30() real ext-real ) number ) holds
( (cosh : ( ( V6() quasi_total ) ( V1() V4( REAL : ( ( ) ( non empty V52() V53() V54() V58() V66() ) set ) ) V5( REAL : ( ( ) ( non empty V52() V53() V54() V58() V66() ) set ) ) V6() non empty total quasi_total complex-valued ext-real-valued real-valued ) Function of REAL : ( ( ) ( non empty V52() V53() V54() V58() V66() ) set ) , REAL : ( ( ) ( non empty V52() V53() V54() V58() V66() ) set ) ) . p : ( ( real ) ( V30() real ext-real ) number ) ) : ( ( ) ( V30() real ext-real ) Element of REAL : ( ( ) ( non empty V52() V53() V54() V58() V66() ) set ) ) + (cosh : ( ( V6() quasi_total ) ( V1() V4( REAL : ( ( ) ( non empty V52() V53() V54() V58() V66() ) set ) ) V5( REAL : ( ( ) ( non empty V52() V53() V54() V58() V66() ) set ) ) V6() non empty total quasi_total complex-valued ext-real-valued real-valued ) Function of REAL : ( ( ) ( non empty V52() V53() V54() V58() V66() ) set ) , REAL : ( ( ) ( non empty V52() V53() V54() V58() V66() ) set ) ) . r : ( ( real ) ( V30() real ext-real ) number ) ) : ( ( ) ( V30() real ext-real ) Element of REAL : ( ( ) ( non empty V52() V53() V54() V58() V66() ) set ) ) : ( ( ) ( V30() real ext-real ) Element of REAL : ( ( ) ( non empty V52() V53() V54() V58() V66() ) set ) ) = (2 : ( ( ) ( non empty ordinal natural V30() real ext-real positive non negative V35() V36() V52() V53() V54() V55() V56() V57() ) Element of NAT : ( ( ) ( V52() V53() V54() V55() V56() V57() V58() ) Element of K19(REAL : ( ( ) ( non empty V52() V53() V54() V58() V66() ) set ) ) : ( ( ) ( ) set ) ) ) * (cosh : ( ( V6() quasi_total ) ( V1() V4( REAL : ( ( ) ( non empty V52() V53() V54() V58() V66() ) set ) ) V5( REAL : ( ( ) ( non empty V52() V53() V54() V58() V66() ) set ) ) V6() non empty total quasi_total complex-valued ext-real-valued real-valued ) Function of REAL : ( ( ) ( non empty V52() V53() V54() V58() V66() ) set ) , REAL : ( ( ) ( non empty V52() V53() V54() V58() V66() ) set ) ) . ((p : ( ( real ) ( V30() real ext-real ) number ) / 2 : ( ( ) ( non empty ordinal natural V30() real ext-real positive non negative V35() V36() V52() V53() V54() V55() V56() V57() ) Element of NAT : ( ( ) ( V52() V53() V54() V55() V56() V57() V58() ) Element of K19(REAL : ( ( ) ( non empty V52() V53() V54() V58() V66() ) set ) ) : ( ( ) ( ) set ) ) ) ) : ( ( ) ( V30() real ext-real ) Element of REAL : ( ( ) ( non empty V52() V53() V54() V58() V66() ) set ) ) + (r : ( ( real ) ( V30() real ext-real ) number ) / 2 : ( ( ) ( non empty ordinal natural V30() real ext-real positive non negative V35() V36() V52() V53() V54() V55() V56() V57() ) Element of NAT : ( ( ) ( V52() V53() V54() V55() V56() V57() V58() ) Element of K19(REAL : ( ( ) ( non empty V52() V53() V54() V58() V66() ) set ) ) : ( ( ) ( ) set ) ) ) ) : ( ( ) ( V30() real ext-real ) Element of REAL : ( ( ) ( non empty V52() V53() V54() V58() V66() ) set ) ) ) : ( ( ) ( V30() real ext-real ) Element of REAL : ( ( ) ( non empty V52() V53() V54() V58() V66() ) set ) ) ) : ( ( ) ( V30() real ext-real ) Element of REAL : ( ( ) ( non empty V52() V53() V54() V58() V66() ) set ) ) ) : ( ( ) ( V30() real ext-real ) Element of REAL : ( ( ) ( non empty V52() V53() V54() V58() V66() ) set ) ) * (cosh : ( ( V6() quasi_total ) ( V1() V4( REAL : ( ( ) ( non empty V52() V53() V54() V58() V66() ) set ) ) V5( REAL : ( ( ) ( non empty V52() V53() V54() V58() V66() ) set ) ) V6() non empty total quasi_total complex-valued ext-real-valued real-valued ) Function of REAL : ( ( ) ( non empty V52() V53() V54() V58() V66() ) set ) , REAL : ( ( ) ( non empty V52() V53() V54() V58() V66() ) set ) ) . ((p : ( ( real ) ( V30() real ext-real ) number ) / 2 : ( ( ) ( non empty ordinal natural V30() real ext-real positive non negative V35() V36() V52() V53() V54() V55() V56() V57() ) Element of NAT : ( ( ) ( V52() V53() V54() V55() V56() V57() V58() ) Element of K19(REAL : ( ( ) ( non empty V52() V53() V54() V58() V66() ) set ) ) : ( ( ) ( ) set ) ) ) ) : ( ( ) ( V30() real ext-real ) Element of REAL : ( ( ) ( non empty V52() V53() V54() V58() V66() ) set ) ) - (r : ( ( real ) ( V30() real ext-real ) number ) / 2 : ( ( ) ( non empty ordinal natural V30() real ext-real positive non negative V35() V36() V52() V53() V54() V55() V56() V57() ) Element of NAT : ( ( ) ( V52() V53() V54() V55() V56() V57() V58() ) Element of K19(REAL : ( ( ) ( non empty V52() V53() V54() V58() V66() ) set ) ) : ( ( ) ( ) set ) ) ) ) : ( ( ) ( V30() real ext-real ) Element of REAL : ( ( ) ( non empty V52() V53() V54() V58() V66() ) set ) ) ) : ( ( ) ( V30() real ext-real ) Element of REAL : ( ( ) ( non empty V52() V53() V54() V58() V66() ) set ) ) ) : ( ( ) ( V30() real ext-real ) Element of REAL : ( ( ) ( non empty V52() V53() V54() V58() V66() ) set ) ) : ( ( ) ( V30() real ext-real ) Element of REAL : ( ( ) ( non empty V52() V53() V54() V58() V66() ) set ) ) & (cosh : ( ( V6() quasi_total ) ( V1() V4( REAL : ( ( ) ( non empty V52() V53() V54() V58() V66() ) set ) ) V5( REAL : ( ( ) ( non empty V52() V53() V54() V58() V66() ) set ) ) V6() non empty total quasi_total complex-valued ext-real-valued real-valued ) Function of REAL : ( ( ) ( non empty V52() V53() V54() V58() V66() ) set ) , REAL : ( ( ) ( non empty V52() V53() V54() V58() V66() ) set ) ) . p : ( ( real ) ( V30() real ext-real ) number ) ) : ( ( ) ( V30() real ext-real ) Element of REAL : ( ( ) ( non empty V52() V53() V54() V58() V66() ) set ) ) - (cosh : ( ( V6() quasi_total ) ( V1() V4( REAL : ( ( ) ( non empty V52() V53() V54() V58() V66() ) set ) ) V5( REAL : ( ( ) ( non empty V52() V53() V54() V58() V66() ) set ) ) V6() non empty total quasi_total complex-valued ext-real-valued real-valued ) Function of REAL : ( ( ) ( non empty V52() V53() V54() V58() V66() ) set ) , REAL : ( ( ) ( non empty V52() V53() V54() V58() V66() ) set ) ) . r : ( ( real ) ( V30() real ext-real ) number ) ) : ( ( ) ( V30() real ext-real ) Element of REAL : ( ( ) ( non empty V52() V53() V54() V58() V66() ) set ) ) : ( ( ) ( V30() real ext-real ) Element of REAL : ( ( ) ( non empty V52() V53() V54() V58() V66() ) set ) ) = (2 : ( ( ) ( non empty ordinal natural V30() real ext-real positive non negative V35() V36() V52() V53() V54() V55() V56() V57() ) Element of NAT : ( ( ) ( V52() V53() V54() V55() V56() V57() V58() ) Element of K19(REAL : ( ( ) ( non empty V52() V53() V54() V58() V66() ) set ) ) : ( ( ) ( ) set ) ) ) * (sinh : ( ( V6() quasi_total ) ( V1() V4( REAL : ( ( ) ( non empty V52() V53() V54() V58() V66() ) set ) ) V5( REAL : ( ( ) ( non empty V52() V53() V54() V58() V66() ) set ) ) V6() non empty total quasi_total complex-valued ext-real-valued real-valued ) Function of REAL : ( ( ) ( non empty V52() V53() V54() V58() V66() ) set ) , REAL : ( ( ) ( non empty V52() V53() V54() V58() V66() ) set ) ) . ((p : ( ( real ) ( V30() real ext-real ) number ) / 2 : ( ( ) ( non empty ordinal natural V30() real ext-real positive non negative V35() V36() V52() V53() V54() V55() V56() V57() ) Element of NAT : ( ( ) ( V52() V53() V54() V55() V56() V57() V58() ) Element of K19(REAL : ( ( ) ( non empty V52() V53() V54() V58() V66() ) set ) ) : ( ( ) ( ) set ) ) ) ) : ( ( ) ( V30() real ext-real ) Element of REAL : ( ( ) ( non empty V52() V53() V54() V58() V66() ) set ) ) - (r : ( ( real ) ( V30() real ext-real ) number ) / 2 : ( ( ) ( non empty ordinal natural V30() real ext-real positive non negative V35() V36() V52() V53() V54() V55() V56() V57() ) Element of NAT : ( ( ) ( V52() V53() V54() V55() V56() V57() V58() ) Element of K19(REAL : ( ( ) ( non empty V52() V53() V54() V58() V66() ) set ) ) : ( ( ) ( ) set ) ) ) ) : ( ( ) ( V30() real ext-real ) Element of REAL : ( ( ) ( non empty V52() V53() V54() V58() V66() ) set ) ) ) : ( ( ) ( V30() real ext-real ) Element of REAL : ( ( ) ( non empty V52() V53() V54() V58() V66() ) set ) ) ) : ( ( ) ( V30() real ext-real ) Element of REAL : ( ( ) ( non empty V52() V53() V54() V58() V66() ) set ) ) ) : ( ( ) ( V30() real ext-real ) Element of REAL : ( ( ) ( non empty V52() V53() V54() V58() V66() ) set ) ) * (sinh : ( ( V6() quasi_total ) ( V1() V4( REAL : ( ( ) ( non empty V52() V53() V54() V58() V66() ) set ) ) V5( REAL : ( ( ) ( non empty V52() V53() V54() V58() V66() ) set ) ) V6() non empty total quasi_total complex-valued ext-real-valued real-valued ) Function of REAL : ( ( ) ( non empty V52() V53() V54() V58() V66() ) set ) , REAL : ( ( ) ( non empty V52() V53() V54() V58() V66() ) set ) ) . ((p : ( ( real ) ( V30() real ext-real ) number ) / 2 : ( ( ) ( non empty ordinal natural V30() real ext-real positive non negative V35() V36() V52() V53() V54() V55() V56() V57() ) Element of NAT : ( ( ) ( V52() V53() V54() V55() V56() V57() V58() ) Element of K19(REAL : ( ( ) ( non empty V52() V53() V54() V58() V66() ) set ) ) : ( ( ) ( ) set ) ) ) ) : ( ( ) ( V30() real ext-real ) Element of REAL : ( ( ) ( non empty V52() V53() V54() V58() V66() ) set ) ) + (r : ( ( real ) ( V30() real ext-real ) number ) / 2 : ( ( ) ( non empty ordinal natural V30() real ext-real positive non negative V35() V36() V52() V53() V54() V55() V56() V57() ) Element of NAT : ( ( ) ( V52() V53() V54() V55() V56() V57() V58() ) Element of K19(REAL : ( ( ) ( non empty V52() V53() V54() V58() V66() ) set ) ) : ( ( ) ( ) set ) ) ) ) : ( ( ) ( V30() real ext-real ) Element of REAL : ( ( ) ( non empty V52() V53() V54() V58() V66() ) set ) ) ) : ( ( ) ( V30() real ext-real ) Element of REAL : ( ( ) ( non empty V52() V53() V54() V58() V66() ) set ) ) ) : ( ( ) ( V30() real ext-real ) Element of REAL : ( ( ) ( non empty V52() V53() V54() V58() V66() ) set ) ) : ( ( ) ( V30() real ext-real ) Element of REAL : ( ( ) ( non empty V52() V53() V54() V58() V66() ) set ) ) ) ;

theorem :: SIN_COS2:28
for p, r being ( ( real ) ( V30() real ext-real ) number ) holds
( (tanh : ( ( V6() quasi_total ) ( V1() V4( REAL : ( ( ) ( non empty V52() V53() V54() V58() V66() ) set ) ) V5( REAL : ( ( ) ( non empty V52() V53() V54() V58() V66() ) set ) ) V6() non empty total quasi_total complex-valued ext-real-valued real-valued ) Function of REAL : ( ( ) ( non empty V52() V53() V54() V58() V66() ) set ) , REAL : ( ( ) ( non empty V52() V53() V54() V58() V66() ) set ) ) . p : ( ( real ) ( V30() real ext-real ) number ) ) : ( ( ) ( V30() real ext-real ) Element of REAL : ( ( ) ( non empty V52() V53() V54() V58() V66() ) set ) ) + (tanh : ( ( V6() quasi_total ) ( V1() V4( REAL : ( ( ) ( non empty V52() V53() V54() V58() V66() ) set ) ) V5( REAL : ( ( ) ( non empty V52() V53() V54() V58() V66() ) set ) ) V6() non empty total quasi_total complex-valued ext-real-valued real-valued ) Function of REAL : ( ( ) ( non empty V52() V53() V54() V58() V66() ) set ) , REAL : ( ( ) ( non empty V52() V53() V54() V58() V66() ) set ) ) . r : ( ( real ) ( V30() real ext-real ) number ) ) : ( ( ) ( V30() real ext-real ) Element of REAL : ( ( ) ( non empty V52() V53() V54() V58() V66() ) set ) ) : ( ( ) ( V30() real ext-real ) Element of REAL : ( ( ) ( non empty V52() V53() V54() V58() V66() ) set ) ) = (sinh : ( ( V6() quasi_total ) ( V1() V4( REAL : ( ( ) ( non empty V52() V53() V54() V58() V66() ) set ) ) V5( REAL : ( ( ) ( non empty V52() V53() V54() V58() V66() ) set ) ) V6() non empty total quasi_total complex-valued ext-real-valued real-valued ) Function of REAL : ( ( ) ( non empty V52() V53() V54() V58() V66() ) set ) , REAL : ( ( ) ( non empty V52() V53() V54() V58() V66() ) set ) ) . (p : ( ( real ) ( V30() real ext-real ) number ) + r : ( ( real ) ( V30() real ext-real ) number ) ) : ( ( ) ( V30() real ext-real ) Element of REAL : ( ( ) ( non empty V52() V53() V54() V58() V66() ) set ) ) ) : ( ( ) ( V30() real ext-real ) Element of REAL : ( ( ) ( non empty V52() V53() V54() V58() V66() ) set ) ) / ((cosh : ( ( V6() quasi_total ) ( V1() V4( REAL : ( ( ) ( non empty V52() V53() V54() V58() V66() ) set ) ) V5( REAL : ( ( ) ( non empty V52() V53() V54() V58() V66() ) set ) ) V6() non empty total quasi_total complex-valued ext-real-valued real-valued ) Function of REAL : ( ( ) ( non empty V52() V53() V54() V58() V66() ) set ) , REAL : ( ( ) ( non empty V52() V53() V54() V58() V66() ) set ) ) . p : ( ( real ) ( V30() real ext-real ) number ) ) : ( ( ) ( V30() real ext-real ) Element of REAL : ( ( ) ( non empty V52() V53() V54() V58() V66() ) set ) ) * (cosh : ( ( V6() quasi_total ) ( V1() V4( REAL : ( ( ) ( non empty V52() V53() V54() V58() V66() ) set ) ) V5( REAL : ( ( ) ( non empty V52() V53() V54() V58() V66() ) set ) ) V6() non empty total quasi_total complex-valued ext-real-valued real-valued ) Function of REAL : ( ( ) ( non empty V52() V53() V54() V58() V66() ) set ) , REAL : ( ( ) ( non empty V52() V53() V54() V58() V66() ) set ) ) . r : ( ( real ) ( V30() real ext-real ) number ) ) : ( ( ) ( V30() real ext-real ) Element of REAL : ( ( ) ( non empty V52() V53() V54() V58() V66() ) set ) ) ) : ( ( ) ( V30() real ext-real ) Element of REAL : ( ( ) ( non empty V52() V53() V54() V58() V66() ) set ) ) : ( ( ) ( V30() real ext-real ) Element of REAL : ( ( ) ( non empty V52() V53() V54() V58() V66() ) set ) ) & (tanh : ( ( V6() quasi_total ) ( V1() V4( REAL : ( ( ) ( non empty V52() V53() V54() V58() V66() ) set ) ) V5( REAL : ( ( ) ( non empty V52() V53() V54() V58() V66() ) set ) ) V6() non empty total quasi_total complex-valued ext-real-valued real-valued ) Function of REAL : ( ( ) ( non empty V52() V53() V54() V58() V66() ) set ) , REAL : ( ( ) ( non empty V52() V53() V54() V58() V66() ) set ) ) . p : ( ( real ) ( V30() real ext-real ) number ) ) : ( ( ) ( V30() real ext-real ) Element of REAL : ( ( ) ( non empty V52() V53() V54() V58() V66() ) set ) ) - (tanh : ( ( V6() quasi_total ) ( V1() V4( REAL : ( ( ) ( non empty V52() V53() V54() V58() V66() ) set ) ) V5( REAL : ( ( ) ( non empty V52() V53() V54() V58() V66() ) set ) ) V6() non empty total quasi_total complex-valued ext-real-valued real-valued ) Function of REAL : ( ( ) ( non empty V52() V53() V54() V58() V66() ) set ) , REAL : ( ( ) ( non empty V52() V53() V54() V58() V66() ) set ) ) . r : ( ( real ) ( V30() real ext-real ) number ) ) : ( ( ) ( V30() real ext-real ) Element of REAL : ( ( ) ( non empty V52() V53() V54() V58() V66() ) set ) ) : ( ( ) ( V30() real ext-real ) Element of REAL : ( ( ) ( non empty V52() V53() V54() V58() V66() ) set ) ) = (sinh : ( ( V6() quasi_total ) ( V1() V4( REAL : ( ( ) ( non empty V52() V53() V54() V58() V66() ) set ) ) V5( REAL : ( ( ) ( non empty V52() V53() V54() V58() V66() ) set ) ) V6() non empty total quasi_total complex-valued ext-real-valued real-valued ) Function of REAL : ( ( ) ( non empty V52() V53() V54() V58() V66() ) set ) , REAL : ( ( ) ( non empty V52() V53() V54() V58() V66() ) set ) ) . (p : ( ( real ) ( V30() real ext-real ) number ) - r : ( ( real ) ( V30() real ext-real ) number ) ) : ( ( ) ( V30() real ext-real ) Element of REAL : ( ( ) ( non empty V52() V53() V54() V58() V66() ) set ) ) ) : ( ( ) ( V30() real ext-real ) Element of REAL : ( ( ) ( non empty V52() V53() V54() V58() V66() ) set ) ) / ((cosh : ( ( V6() quasi_total ) ( V1() V4( REAL : ( ( ) ( non empty V52() V53() V54() V58() V66() ) set ) ) V5( REAL : ( ( ) ( non empty V52() V53() V54() V58() V66() ) set ) ) V6() non empty total quasi_total complex-valued ext-real-valued real-valued ) Function of REAL : ( ( ) ( non empty V52() V53() V54() V58() V66() ) set ) , REAL : ( ( ) ( non empty V52() V53() V54() V58() V66() ) set ) ) . p : ( ( real ) ( V30() real ext-real ) number ) ) : ( ( ) ( V30() real ext-real ) Element of REAL : ( ( ) ( non empty V52() V53() V54() V58() V66() ) set ) ) * (cosh : ( ( V6() quasi_total ) ( V1() V4( REAL : ( ( ) ( non empty V52() V53() V54() V58() V66() ) set ) ) V5( REAL : ( ( ) ( non empty V52() V53() V54() V58() V66() ) set ) ) V6() non empty total quasi_total complex-valued ext-real-valued real-valued ) Function of REAL : ( ( ) ( non empty V52() V53() V54() V58() V66() ) set ) , REAL : ( ( ) ( non empty V52() V53() V54() V58() V66() ) set ) ) . r : ( ( real ) ( V30() real ext-real ) number ) ) : ( ( ) ( V30() real ext-real ) Element of REAL : ( ( ) ( non empty V52() V53() V54() V58() V66() ) set ) ) ) : ( ( ) ( V30() real ext-real ) Element of REAL : ( ( ) ( non empty V52() V53() V54() V58() V66() ) set ) ) : ( ( ) ( V30() real ext-real ) Element of REAL : ( ( ) ( non empty V52() V53() V54() V58() V66() ) set ) ) ) ;

theorem :: SIN_COS2:29
for p being ( ( real ) ( V30() real ext-real ) number )
for n being ( ( ) ( ordinal natural V30() real ext-real non negative V35() V36() V52() V53() V54() V55() V56() V57() ) Element of NAT : ( ( ) ( V52() V53() V54() V55() V56() V57() V58() ) Element of K19(REAL : ( ( ) ( non empty V52() V53() V54() V58() V66() ) set ) ) : ( ( ) ( ) set ) ) ) holds ((cosh : ( ( V6() quasi_total ) ( V1() V4( REAL : ( ( ) ( non empty V52() V53() V54() V58() V66() ) set ) ) V5( REAL : ( ( ) ( non empty V52() V53() V54() V58() V66() ) set ) ) V6() non empty total quasi_total complex-valued ext-real-valued real-valued ) Function of REAL : ( ( ) ( non empty V52() V53() V54() V58() V66() ) set ) , REAL : ( ( ) ( non empty V52() V53() V54() V58() V66() ) set ) ) . p : ( ( real ) ( V30() real ext-real ) number ) ) : ( ( ) ( V30() real ext-real ) Element of REAL : ( ( ) ( non empty V52() V53() V54() V58() V66() ) set ) ) + (sinh : ( ( V6() quasi_total ) ( V1() V4( REAL : ( ( ) ( non empty V52() V53() V54() V58() V66() ) set ) ) V5( REAL : ( ( ) ( non empty V52() V53() V54() V58() V66() ) set ) ) V6() non empty total quasi_total complex-valued ext-real-valued real-valued ) Function of REAL : ( ( ) ( non empty V52() V53() V54() V58() V66() ) set ) , REAL : ( ( ) ( non empty V52() V53() V54() V58() V66() ) set ) ) . p : ( ( real ) ( V30() real ext-real ) number ) ) : ( ( ) ( V30() real ext-real ) Element of REAL : ( ( ) ( non empty V52() V53() V54() V58() V66() ) set ) ) ) : ( ( ) ( V30() real ext-real ) Element of REAL : ( ( ) ( non empty V52() V53() V54() V58() V66() ) set ) ) |^ n : ( ( ) ( ordinal natural V30() real ext-real non negative V35() V36() V52() V53() V54() V55() V56() V57() ) Element of NAT : ( ( ) ( V52() V53() V54() V55() V56() V57() V58() ) Element of K19(REAL : ( ( ) ( non empty V52() V53() V54() V58() V66() ) set ) ) : ( ( ) ( ) set ) ) ) : ( ( ) ( V30() real ext-real ) Element of REAL : ( ( ) ( non empty V52() V53() V54() V58() V66() ) set ) ) = (cosh : ( ( V6() quasi_total ) ( V1() V4( REAL : ( ( ) ( non empty V52() V53() V54() V58() V66() ) set ) ) V5( REAL : ( ( ) ( non empty V52() V53() V54() V58() V66() ) set ) ) V6() non empty total quasi_total complex-valued ext-real-valued real-valued ) Function of REAL : ( ( ) ( non empty V52() V53() V54() V58() V66() ) set ) , REAL : ( ( ) ( non empty V52() V53() V54() V58() V66() ) set ) ) . (n : ( ( ) ( ordinal natural V30() real ext-real non negative V35() V36() V52() V53() V54() V55() V56() V57() ) Element of NAT : ( ( ) ( V52() V53() V54() V55() V56() V57() V58() ) Element of K19(REAL : ( ( ) ( non empty V52() V53() V54() V58() V66() ) set ) ) : ( ( ) ( ) set ) ) ) * p : ( ( real ) ( V30() real ext-real ) number ) ) : ( ( ) ( V30() real ext-real ) Element of REAL : ( ( ) ( non empty V52() V53() V54() V58() V66() ) set ) ) ) : ( ( ) ( V30() real ext-real ) Element of REAL : ( ( ) ( non empty V52() V53() V54() V58() V66() ) set ) ) + (sinh : ( ( V6() quasi_total ) ( V1() V4( REAL : ( ( ) ( non empty V52() V53() V54() V58() V66() ) set ) ) V5( REAL : ( ( ) ( non empty V52() V53() V54() V58() V66() ) set ) ) V6() non empty total quasi_total complex-valued ext-real-valued real-valued ) Function of REAL : ( ( ) ( non empty V52() V53() V54() V58() V66() ) set ) , REAL : ( ( ) ( non empty V52() V53() V54() V58() V66() ) set ) ) . (n : ( ( ) ( ordinal natural V30() real ext-real non negative V35() V36() V52() V53() V54() V55() V56() V57() ) Element of NAT : ( ( ) ( V52() V53() V54() V55() V56() V57() V58() ) Element of K19(REAL : ( ( ) ( non empty V52() V53() V54() V58() V66() ) set ) ) : ( ( ) ( ) set ) ) ) * p : ( ( real ) ( V30() real ext-real ) number ) ) : ( ( ) ( V30() real ext-real ) Element of REAL : ( ( ) ( non empty V52() V53() V54() V58() V66() ) set ) ) ) : ( ( ) ( V30() real ext-real ) Element of REAL : ( ( ) ( non empty V52() V53() V54() V58() V66() ) set ) ) : ( ( ) ( V30() real ext-real ) Element of REAL : ( ( ) ( non empty V52() V53() V54() V58() V66() ) set ) ) ;

theorem :: SIN_COS2:30
( dom sinh : ( ( V6() quasi_total ) ( V1() V4( REAL : ( ( ) ( non empty V52() V53() V54() V58() V66() ) set ) ) V5( REAL : ( ( ) ( non empty V52() V53() V54() V58() V66() ) set ) ) V6() non empty total quasi_total complex-valued ext-real-valued real-valued ) Function of REAL : ( ( ) ( non empty V52() V53() V54() V58() V66() ) set ) , REAL : ( ( ) ( non empty V52() V53() V54() V58() V66() ) set ) ) : ( ( ) ( V52() V53() V54() ) Element of K19(REAL : ( ( ) ( non empty V52() V53() V54() V58() V66() ) set ) ) : ( ( ) ( ) set ) ) = REAL : ( ( ) ( non empty V52() V53() V54() V58() V66() ) set ) & dom cosh : ( ( V6() quasi_total ) ( V1() V4( REAL : ( ( ) ( non empty V52() V53() V54() V58() V66() ) set ) ) V5( REAL : ( ( ) ( non empty V52() V53() V54() V58() V66() ) set ) ) V6() non empty total quasi_total complex-valued ext-real-valued real-valued ) Function of REAL : ( ( ) ( non empty V52() V53() V54() V58() V66() ) set ) , REAL : ( ( ) ( non empty V52() V53() V54() V58() V66() ) set ) ) : ( ( ) ( V52() V53() V54() ) Element of K19(REAL : ( ( ) ( non empty V52() V53() V54() V58() V66() ) set ) ) : ( ( ) ( ) set ) ) = REAL : ( ( ) ( non empty V52() V53() V54() V58() V66() ) set ) & dom tanh : ( ( V6() quasi_total ) ( V1() V4( REAL : ( ( ) ( non empty V52() V53() V54() V58() V66() ) set ) ) V5( REAL : ( ( ) ( non empty V52() V53() V54() V58() V66() ) set ) ) V6() non empty total quasi_total complex-valued ext-real-valued real-valued ) Function of REAL : ( ( ) ( non empty V52() V53() V54() V58() V66() ) set ) , REAL : ( ( ) ( non empty V52() V53() V54() V58() V66() ) set ) ) : ( ( ) ( V52() V53() V54() ) Element of K19(REAL : ( ( ) ( non empty V52() V53() V54() V58() V66() ) set ) ) : ( ( ) ( ) set ) ) = REAL : ( ( ) ( non empty V52() V53() V54() V58() V66() ) set ) ) ;

theorem :: SIN_COS2:31
for p being ( ( real ) ( V30() real ext-real ) number ) holds
( sinh : ( ( V6() quasi_total ) ( V1() V4( REAL : ( ( ) ( non empty V52() V53() V54() V58() V66() ) set ) ) V5( REAL : ( ( ) ( non empty V52() V53() V54() V58() V66() ) set ) ) V6() non empty total quasi_total complex-valued ext-real-valued real-valued ) Function of REAL : ( ( ) ( non empty V52() V53() V54() V58() V66() ) set ) , REAL : ( ( ) ( non empty V52() V53() V54() V58() V66() ) set ) ) is_differentiable_in p : ( ( real ) ( V30() real ext-real ) number ) & diff (sinh : ( ( V6() quasi_total ) ( V1() V4( REAL : ( ( ) ( non empty V52() V53() V54() V58() V66() ) set ) ) V5( REAL : ( ( ) ( non empty V52() V53() V54() V58() V66() ) set ) ) V6() non empty total quasi_total complex-valued ext-real-valued real-valued ) Function of REAL : ( ( ) ( non empty V52() V53() V54() V58() V66() ) set ) , REAL : ( ( ) ( non empty V52() V53() V54() V58() V66() ) set ) ) ,p : ( ( real ) ( V30() real ext-real ) number ) ) : ( ( ) ( V30() real ext-real ) Element of REAL : ( ( ) ( non empty V52() V53() V54() V58() V66() ) set ) ) = cosh : ( ( V6() quasi_total ) ( V1() V4( REAL : ( ( ) ( non empty V52() V53() V54() V58() V66() ) set ) ) V5( REAL : ( ( ) ( non empty V52() V53() V54() V58() V66() ) set ) ) V6() non empty total quasi_total complex-valued ext-real-valued real-valued ) Function of REAL : ( ( ) ( non empty V52() V53() V54() V58() V66() ) set ) , REAL : ( ( ) ( non empty V52() V53() V54() V58() V66() ) set ) ) . p : ( ( real ) ( V30() real ext-real ) number ) : ( ( ) ( V30() real ext-real ) Element of REAL : ( ( ) ( non empty V52() V53() V54() V58() V66() ) set ) ) ) ;

theorem :: SIN_COS2:32
for p being ( ( real ) ( V30() real ext-real ) number ) holds
( cosh : ( ( V6() quasi_total ) ( V1() V4( REAL : ( ( ) ( non empty V52() V53() V54() V58() V66() ) set ) ) V5( REAL : ( ( ) ( non empty V52() V53() V54() V58() V66() ) set ) ) V6() non empty total quasi_total complex-valued ext-real-valued real-valued ) Function of REAL : ( ( ) ( non empty V52() V53() V54() V58() V66() ) set ) , REAL : ( ( ) ( non empty V52() V53() V54() V58() V66() ) set ) ) is_differentiable_in p : ( ( real ) ( V30() real ext-real ) number ) & diff (cosh : ( ( V6() quasi_total ) ( V1() V4( REAL : ( ( ) ( non empty V52() V53() V54() V58() V66() ) set ) ) V5( REAL : ( ( ) ( non empty V52() V53() V54() V58() V66() ) set ) ) V6() non empty total quasi_total complex-valued ext-real-valued real-valued ) Function of REAL : ( ( ) ( non empty V52() V53() V54() V58() V66() ) set ) , REAL : ( ( ) ( non empty V52() V53() V54() V58() V66() ) set ) ) ,p : ( ( real ) ( V30() real ext-real ) number ) ) : ( ( ) ( V30() real ext-real ) Element of REAL : ( ( ) ( non empty V52() V53() V54() V58() V66() ) set ) ) = sinh : ( ( V6() quasi_total ) ( V1() V4( REAL : ( ( ) ( non empty V52() V53() V54() V58() V66() ) set ) ) V5( REAL : ( ( ) ( non empty V52() V53() V54() V58() V66() ) set ) ) V6() non empty total quasi_total complex-valued ext-real-valued real-valued ) Function of REAL : ( ( ) ( non empty V52() V53() V54() V58() V66() ) set ) , REAL : ( ( ) ( non empty V52() V53() V54() V58() V66() ) set ) ) . p : ( ( real ) ( V30() real ext-real ) number ) : ( ( ) ( V30() real ext-real ) Element of REAL : ( ( ) ( non empty V52() V53() V54() V58() V66() ) set ) ) ) ;

theorem :: SIN_COS2:33
for p being ( ( real ) ( V30() real ext-real ) number ) holds
( tanh : ( ( V6() quasi_total ) ( V1() V4( REAL : ( ( ) ( non empty V52() V53() V54() V58() V66() ) set ) ) V5( REAL : ( ( ) ( non empty V52() V53() V54() V58() V66() ) set ) ) V6() non empty total quasi_total complex-valued ext-real-valued real-valued ) Function of REAL : ( ( ) ( non empty V52() V53() V54() V58() V66() ) set ) , REAL : ( ( ) ( non empty V52() V53() V54() V58() V66() ) set ) ) is_differentiable_in p : ( ( real ) ( V30() real ext-real ) number ) & diff (tanh : ( ( V6() quasi_total ) ( V1() V4( REAL : ( ( ) ( non empty V52() V53() V54() V58() V66() ) set ) ) V5( REAL : ( ( ) ( non empty V52() V53() V54() V58() V66() ) set ) ) V6() non empty total quasi_total complex-valued ext-real-valued real-valued ) Function of REAL : ( ( ) ( non empty V52() V53() V54() V58() V66() ) set ) , REAL : ( ( ) ( non empty V52() V53() V54() V58() V66() ) set ) ) ,p : ( ( real ) ( V30() real ext-real ) number ) ) : ( ( ) ( V30() real ext-real ) Element of REAL : ( ( ) ( non empty V52() V53() V54() V58() V66() ) set ) ) = 1 : ( ( ) ( non empty ordinal natural V30() real ext-real positive non negative V35() V36() V52() V53() V54() V55() V56() V57() ) Element of NAT : ( ( ) ( V52() V53() V54() V55() V56() V57() V58() ) Element of K19(REAL : ( ( ) ( non empty V52() V53() V54() V58() V66() ) set ) ) : ( ( ) ( ) set ) ) ) / ((cosh : ( ( V6() quasi_total ) ( V1() V4( REAL : ( ( ) ( non empty V52() V53() V54() V58() V66() ) set ) ) V5( REAL : ( ( ) ( non empty V52() V53() V54() V58() V66() ) set ) ) V6() non empty total quasi_total complex-valued ext-real-valued real-valued ) Function of REAL : ( ( ) ( non empty V52() V53() V54() V58() V66() ) set ) , REAL : ( ( ) ( non empty V52() V53() V54() V58() V66() ) set ) ) . p : ( ( real ) ( V30() real ext-real ) number ) ) : ( ( ) ( V30() real ext-real ) Element of REAL : ( ( ) ( non empty V52() V53() V54() V58() V66() ) set ) ) ^2) : ( ( ) ( V30() real ext-real ) Element of REAL : ( ( ) ( non empty V52() V53() V54() V58() V66() ) set ) ) : ( ( ) ( V30() real ext-real ) Element of REAL : ( ( ) ( non empty V52() V53() V54() V58() V66() ) set ) ) ) ;

theorem :: SIN_COS2:34
for p being ( ( real ) ( V30() real ext-real ) number ) holds
( sinh : ( ( V6() quasi_total ) ( V1() V4( REAL : ( ( ) ( non empty V52() V53() V54() V58() V66() ) set ) ) V5( REAL : ( ( ) ( non empty V52() V53() V54() V58() V66() ) set ) ) V6() non empty total quasi_total complex-valued ext-real-valued real-valued ) Function of REAL : ( ( ) ( non empty V52() V53() V54() V58() V66() ) set ) , REAL : ( ( ) ( non empty V52() V53() V54() V58() V66() ) set ) ) is_differentiable_on REAL : ( ( ) ( non empty V52() V53() V54() V58() V66() ) set ) & diff (sinh : ( ( V6() quasi_total ) ( V1() V4( REAL : ( ( ) ( non empty V52() V53() V54() V58() V66() ) set ) ) V5( REAL : ( ( ) ( non empty V52() V53() V54() V58() V66() ) set ) ) V6() non empty total quasi_total complex-valued ext-real-valued real-valued ) Function of REAL : ( ( ) ( non empty V52() V53() V54() V58() V66() ) set ) , REAL : ( ( ) ( non empty V52() V53() V54() V58() V66() ) set ) ) ,p : ( ( real ) ( V30() real ext-real ) number ) ) : ( ( ) ( V30() real ext-real ) Element of REAL : ( ( ) ( non empty V52() V53() V54() V58() V66() ) set ) ) = cosh : ( ( V6() quasi_total ) ( V1() V4( REAL : ( ( ) ( non empty V52() V53() V54() V58() V66() ) set ) ) V5( REAL : ( ( ) ( non empty V52() V53() V54() V58() V66() ) set ) ) V6() non empty total quasi_total complex-valued ext-real-valued real-valued ) Function of REAL : ( ( ) ( non empty V52() V53() V54() V58() V66() ) set ) , REAL : ( ( ) ( non empty V52() V53() V54() V58() V66() ) set ) ) . p : ( ( real ) ( V30() real ext-real ) number ) : ( ( ) ( V30() real ext-real ) Element of REAL : ( ( ) ( non empty V52() V53() V54() V58() V66() ) set ) ) ) ;

theorem :: SIN_COS2:35
for p being ( ( real ) ( V30() real ext-real ) number ) holds
( cosh : ( ( V6() quasi_total ) ( V1() V4( REAL : ( ( ) ( non empty V52() V53() V54() V58() V66() ) set ) ) V5( REAL : ( ( ) ( non empty V52() V53() V54() V58() V66() ) set ) ) V6() non empty total quasi_total complex-valued ext-real-valued real-valued ) Function of REAL : ( ( ) ( non empty V52() V53() V54() V58() V66() ) set ) , REAL : ( ( ) ( non empty V52() V53() V54() V58() V66() ) set ) ) is_differentiable_on REAL : ( ( ) ( non empty V52() V53() V54() V58() V66() ) set ) & diff (cosh : ( ( V6() quasi_total ) ( V1() V4( REAL : ( ( ) ( non empty V52() V53() V54() V58() V66() ) set ) ) V5( REAL : ( ( ) ( non empty V52() V53() V54() V58() V66() ) set ) ) V6() non empty total quasi_total complex-valued ext-real-valued real-valued ) Function of REAL : ( ( ) ( non empty V52() V53() V54() V58() V66() ) set ) , REAL : ( ( ) ( non empty V52() V53() V54() V58() V66() ) set ) ) ,p : ( ( real ) ( V30() real ext-real ) number ) ) : ( ( ) ( V30() real ext-real ) Element of REAL : ( ( ) ( non empty V52() V53() V54() V58() V66() ) set ) ) = sinh : ( ( V6() quasi_total ) ( V1() V4( REAL : ( ( ) ( non empty V52() V53() V54() V58() V66() ) set ) ) V5( REAL : ( ( ) ( non empty V52() V53() V54() V58() V66() ) set ) ) V6() non empty total quasi_total complex-valued ext-real-valued real-valued ) Function of REAL : ( ( ) ( non empty V52() V53() V54() V58() V66() ) set ) , REAL : ( ( ) ( non empty V52() V53() V54() V58() V66() ) set ) ) . p : ( ( real ) ( V30() real ext-real ) number ) : ( ( ) ( V30() real ext-real ) Element of REAL : ( ( ) ( non empty V52() V53() V54() V58() V66() ) set ) ) ) ;

theorem :: SIN_COS2:36
for p being ( ( real ) ( V30() real ext-real ) number ) holds
( tanh : ( ( V6() quasi_total ) ( V1() V4( REAL : ( ( ) ( non empty V52() V53() V54() V58() V66() ) set ) ) V5( REAL : ( ( ) ( non empty V52() V53() V54() V58() V66() ) set ) ) V6() non empty total quasi_total complex-valued ext-real-valued real-valued ) Function of REAL : ( ( ) ( non empty V52() V53() V54() V58() V66() ) set ) , REAL : ( ( ) ( non empty V52() V53() V54() V58() V66() ) set ) ) is_differentiable_on REAL : ( ( ) ( non empty V52() V53() V54() V58() V66() ) set ) & diff (tanh : ( ( V6() quasi_total ) ( V1() V4( REAL : ( ( ) ( non empty V52() V53() V54() V58() V66() ) set ) ) V5( REAL : ( ( ) ( non empty V52() V53() V54() V58() V66() ) set ) ) V6() non empty total quasi_total complex-valued ext-real-valued real-valued ) Function of REAL : ( ( ) ( non empty V52() V53() V54() V58() V66() ) set ) , REAL : ( ( ) ( non empty V52() V53() V54() V58() V66() ) set ) ) ,p : ( ( real ) ( V30() real ext-real ) number ) ) : ( ( ) ( V30() real ext-real ) Element of REAL : ( ( ) ( non empty V52() V53() V54() V58() V66() ) set ) ) = 1 : ( ( ) ( non empty ordinal natural V30() real ext-real positive non negative V35() V36() V52() V53() V54() V55() V56() V57() ) Element of NAT : ( ( ) ( V52() V53() V54() V55() V56() V57() V58() ) Element of K19(REAL : ( ( ) ( non empty V52() V53() V54() V58() V66() ) set ) ) : ( ( ) ( ) set ) ) ) / ((cosh : ( ( V6() quasi_total ) ( V1() V4( REAL : ( ( ) ( non empty V52() V53() V54() V58() V66() ) set ) ) V5( REAL : ( ( ) ( non empty V52() V53() V54() V58() V66() ) set ) ) V6() non empty total quasi_total complex-valued ext-real-valued real-valued ) Function of REAL : ( ( ) ( non empty V52() V53() V54() V58() V66() ) set ) , REAL : ( ( ) ( non empty V52() V53() V54() V58() V66() ) set ) ) . p : ( ( real ) ( V30() real ext-real ) number ) ) : ( ( ) ( V30() real ext-real ) Element of REAL : ( ( ) ( non empty V52() V53() V54() V58() V66() ) set ) ) ^2) : ( ( ) ( V30() real ext-real ) Element of REAL : ( ( ) ( non empty V52() V53() V54() V58() V66() ) set ) ) : ( ( ) ( V30() real ext-real ) Element of REAL : ( ( ) ( non empty V52() V53() V54() V58() V66() ) set ) ) ) ;

theorem :: SIN_COS2:37
for p being ( ( real ) ( V30() real ext-real ) number ) holds cosh : ( ( V6() quasi_total ) ( V1() V4( REAL : ( ( ) ( non empty V52() V53() V54() V58() V66() ) set ) ) V5( REAL : ( ( ) ( non empty V52() V53() V54() V58() V66() ) set ) ) V6() non empty total quasi_total complex-valued ext-real-valued real-valued ) Function of REAL : ( ( ) ( non empty V52() V53() V54() V58() V66() ) set ) , REAL : ( ( ) ( non empty V52() V53() V54() V58() V66() ) set ) ) . p : ( ( real ) ( V30() real ext-real ) number ) : ( ( ) ( V30() real ext-real ) Element of REAL : ( ( ) ( non empty V52() V53() V54() V58() V66() ) set ) ) >= 1 : ( ( ) ( non empty ordinal natural V30() real ext-real positive non negative V35() V36() V52() V53() V54() V55() V56() V57() ) Element of NAT : ( ( ) ( V52() V53() V54() V55() V56() V57() V58() ) Element of K19(REAL : ( ( ) ( non empty V52() V53() V54() V58() V66() ) set ) ) : ( ( ) ( ) set ) ) ) ;

theorem :: SIN_COS2:38
for p being ( ( real ) ( V30() real ext-real ) number ) holds sinh : ( ( V6() quasi_total ) ( V1() V4( REAL : ( ( ) ( non empty V52() V53() V54() V58() V66() ) set ) ) V5( REAL : ( ( ) ( non empty V52() V53() V54() V58() V66() ) set ) ) V6() non empty total quasi_total complex-valued ext-real-valued real-valued ) Function of REAL : ( ( ) ( non empty V52() V53() V54() V58() V66() ) set ) , REAL : ( ( ) ( non empty V52() V53() V54() V58() V66() ) set ) ) is_continuous_in p : ( ( real ) ( V30() real ext-real ) number ) ;

theorem :: SIN_COS2:39
for p being ( ( real ) ( V30() real ext-real ) number ) holds cosh : ( ( V6() quasi_total ) ( V1() V4( REAL : ( ( ) ( non empty V52() V53() V54() V58() V66() ) set ) ) V5( REAL : ( ( ) ( non empty V52() V53() V54() V58() V66() ) set ) ) V6() non empty total quasi_total complex-valued ext-real-valued real-valued ) Function of REAL : ( ( ) ( non empty V52() V53() V54() V58() V66() ) set ) , REAL : ( ( ) ( non empty V52() V53() V54() V58() V66() ) set ) ) is_continuous_in p : ( ( real ) ( V30() real ext-real ) number ) ;

theorem :: SIN_COS2:40
for p being ( ( real ) ( V30() real ext-real ) number ) holds tanh : ( ( V6() quasi_total ) ( V1() V4( REAL : ( ( ) ( non empty V52() V53() V54() V58() V66() ) set ) ) V5( REAL : ( ( ) ( non empty V52() V53() V54() V58() V66() ) set ) ) V6() non empty total quasi_total complex-valued ext-real-valued real-valued ) Function of REAL : ( ( ) ( non empty V52() V53() V54() V58() V66() ) set ) , REAL : ( ( ) ( non empty V52() V53() V54() V58() V66() ) set ) ) is_continuous_in p : ( ( real ) ( V30() real ext-real ) number ) ;

theorem :: SIN_COS2:41
sinh : ( ( V6() quasi_total ) ( V1() V4( REAL : ( ( ) ( non empty V52() V53() V54() V58() V66() ) set ) ) V5( REAL : ( ( ) ( non empty V52() V53() V54() V58() V66() ) set ) ) V6() non empty total quasi_total complex-valued ext-real-valued real-valued ) Function of REAL : ( ( ) ( non empty V52() V53() V54() V58() V66() ) set ) , REAL : ( ( ) ( non empty V52() V53() V54() V58() V66() ) set ) ) | REAL : ( ( ) ( non empty V52() V53() V54() V58() V66() ) set ) : ( ( V6() ) ( V1() V4( REAL : ( ( ) ( non empty V52() V53() V54() V58() V66() ) set ) ) V5( REAL : ( ( ) ( non empty V52() V53() V54() V58() V66() ) set ) ) V6() complex-valued ext-real-valued real-valued ) Element of K19(K20(REAL : ( ( ) ( non empty V52() V53() V54() V58() V66() ) set ) ,REAL : ( ( ) ( non empty V52() V53() V54() V58() V66() ) set ) ) : ( ( ) ( complex-valued ext-real-valued real-valued ) set ) ) : ( ( ) ( ) set ) ) is continuous ;

theorem :: SIN_COS2:42
cosh : ( ( V6() quasi_total ) ( V1() V4( REAL : ( ( ) ( non empty V52() V53() V54() V58() V66() ) set ) ) V5( REAL : ( ( ) ( non empty V52() V53() V54() V58() V66() ) set ) ) V6() non empty total quasi_total complex-valued ext-real-valued real-valued ) Function of REAL : ( ( ) ( non empty V52() V53() V54() V58() V66() ) set ) , REAL : ( ( ) ( non empty V52() V53() V54() V58() V66() ) set ) ) | REAL : ( ( ) ( non empty V52() V53() V54() V58() V66() ) set ) : ( ( V6() ) ( V1() V4( REAL : ( ( ) ( non empty V52() V53() V54() V58() V66() ) set ) ) V5( REAL : ( ( ) ( non empty V52() V53() V54() V58() V66() ) set ) ) V6() complex-valued ext-real-valued real-valued ) Element of K19(K20(REAL : ( ( ) ( non empty V52() V53() V54() V58() V66() ) set ) ,REAL : ( ( ) ( non empty V52() V53() V54() V58() V66() ) set ) ) : ( ( ) ( complex-valued ext-real-valued real-valued ) set ) ) : ( ( ) ( ) set ) ) is continuous ;

theorem :: SIN_COS2:43
tanh : ( ( V6() quasi_total ) ( V1() V4( REAL : ( ( ) ( non empty V52() V53() V54() V58() V66() ) set ) ) V5( REAL : ( ( ) ( non empty V52() V53() V54() V58() V66() ) set ) ) V6() non empty total quasi_total complex-valued ext-real-valued real-valued ) Function of REAL : ( ( ) ( non empty V52() V53() V54() V58() V66() ) set ) , REAL : ( ( ) ( non empty V52() V53() V54() V58() V66() ) set ) ) | REAL : ( ( ) ( non empty V52() V53() V54() V58() V66() ) set ) : ( ( V6() ) ( V1() V4( REAL : ( ( ) ( non empty V52() V53() V54() V58() V66() ) set ) ) V5( REAL : ( ( ) ( non empty V52() V53() V54() V58() V66() ) set ) ) V6() complex-valued ext-real-valued real-valued ) Element of K19(K20(REAL : ( ( ) ( non empty V52() V53() V54() V58() V66() ) set ) ,REAL : ( ( ) ( non empty V52() V53() V54() V58() V66() ) set ) ) : ( ( ) ( complex-valued ext-real-valued real-valued ) set ) ) : ( ( ) ( ) set ) ) is continuous ;

theorem :: SIN_COS2:44
for p being ( ( real ) ( V30() real ext-real ) number ) holds
( tanh : ( ( V6() quasi_total ) ( V1() V4( REAL : ( ( ) ( non empty V52() V53() V54() V58() V66() ) set ) ) V5( REAL : ( ( ) ( non empty V52() V53() V54() V58() V66() ) set ) ) V6() non empty total quasi_total complex-valued ext-real-valued real-valued ) Function of REAL : ( ( ) ( non empty V52() V53() V54() V58() V66() ) set ) , REAL : ( ( ) ( non empty V52() V53() V54() V58() V66() ) set ) ) . p : ( ( real ) ( V30() real ext-real ) number ) : ( ( ) ( V30() real ext-real ) Element of REAL : ( ( ) ( non empty V52() V53() V54() V58() V66() ) set ) ) < 1 : ( ( ) ( non empty ordinal natural V30() real ext-real positive non negative V35() V36() V52() V53() V54() V55() V56() V57() ) Element of NAT : ( ( ) ( V52() V53() V54() V55() V56() V57() V58() ) Element of K19(REAL : ( ( ) ( non empty V52() V53() V54() V58() V66() ) set ) ) : ( ( ) ( ) set ) ) ) & tanh : ( ( V6() quasi_total ) ( V1() V4( REAL : ( ( ) ( non empty V52() V53() V54() V58() V66() ) set ) ) V5( REAL : ( ( ) ( non empty V52() V53() V54() V58() V66() ) set ) ) V6() non empty total quasi_total complex-valued ext-real-valued real-valued ) Function of REAL : ( ( ) ( non empty V52() V53() V54() V58() V66() ) set ) , REAL : ( ( ) ( non empty V52() V53() V54() V58() V66() ) set ) ) . p : ( ( real ) ( V30() real ext-real ) number ) : ( ( ) ( V30() real ext-real ) Element of REAL : ( ( ) ( non empty V52() V53() V54() V58() V66() ) set ) ) > - 1 : ( ( ) ( non empty ordinal natural V30() real ext-real positive non negative V35() V36() V52() V53() V54() V55() V56() V57() ) Element of NAT : ( ( ) ( V52() V53() V54() V55() V56() V57() V58() ) Element of K19(REAL : ( ( ) ( non empty V52() V53() V54() V58() V66() ) set ) ) : ( ( ) ( ) set ) ) ) : ( ( ) ( V30() real ext-real non positive ) Element of REAL : ( ( ) ( non empty V52() V53() V54() V58() V66() ) set ) ) ) ;