let x, y be real number ; :: thesis: ( (x * y) + ((sqrt ((x ^2 ) + 1)) * (sqrt ((y ^2 ) + 1))) >= 0 implies (sinh" x) + (sinh" y) = sinh" ((x * (sqrt (1 + (y ^2 )))) + (y * (sqrt (1 + (x ^2 ))))) )
assume A1: (x * y) + ((sqrt ((x ^2 ) + 1)) * (sqrt ((y ^2 ) + 1))) >= 0 ; :: thesis: (sinh" x) + (sinh" y) = sinh" ((x * (sqrt (1 + (y ^2 )))) + (y * (sqrt (1 + (x ^2 )))))
A2: ( (sqrt ((x ^2 ) + 1)) + x > 0 & (sqrt ((y ^2 ) + 1)) + y > 0 ) by Th5;
A3: ( (x ^2 ) + 1 >= 0 & (y ^2 ) + 1 >= 0 ) by Lm8;
then A4: ((x ^2 ) + 1) * ((y ^2 ) + 1) >= 0 ;
A5: (sinh" x) + (sinh" y) = log number_e ,((x + (sqrt ((x ^2 ) + 1))) * (y + (sqrt ((y ^2 ) + 1)))) by A2, Lm2, POWER:61
.= log number_e ,(((x * (sqrt ((y ^2 ) + 1))) + ((sqrt ((x ^2 ) + 1)) * y)) + ((x * y) + ((sqrt ((x ^2 ) + 1)) * (sqrt ((y ^2 ) + 1)))))
.= log number_e ,(((x * (sqrt ((y ^2 ) + 1))) + ((sqrt ((x ^2 ) + 1)) * y)) + (sqrt (((x * y) + ((sqrt ((x ^2 ) + 1)) * (sqrt ((y ^2 ) + 1)))) ^2 ))) by A1, SQUARE_1:89 ;
set t = sqrt (((x * y) + ((sqrt ((x ^2 ) + 1)) * (sqrt ((y ^2 ) + 1)))) ^2 );
A6: sqrt (((x * y) + ((sqrt ((x ^2 ) + 1)) * (sqrt ((y ^2 ) + 1)))) ^2 ) = sqrt (((x * y) + (sqrt (((x ^2 ) + 1) * ((y ^2 ) + 1)))) ^2 ) by A3, SQUARE_1:97
.= sqrt ((((x * y) ^2 ) + ((2 * (x * y)) * (sqrt (((x ^2 ) + 1) * ((y ^2 ) + 1))))) + ((sqrt (((x ^2 ) + 1) * ((y ^2 ) + 1))) ^2 ))
.= sqrt ((((x * y) ^2 ) + ((2 * (x * y)) * (sqrt (((x ^2 ) + 1) * ((y ^2 ) + 1))))) + (((((x * y) ^2 ) + (x ^2 )) + (y ^2 )) + 1)) by A4, SQUARE_1:def 4
.= sqrt (((((2 * ((x * y) ^2 )) + (x ^2 )) + (y ^2 )) + 1) + ((2 * (x * y)) * (sqrt (((x ^2 ) + 1) * ((y ^2 ) + 1))))) ;
set p = sqrt ((((x * (sqrt (1 + (y ^2 )))) + (y * (sqrt (1 + (x ^2 ))))) ^2 ) + 1);
sqrt ((((x * (sqrt (1 + (y ^2 )))) + (y * (sqrt (1 + (x ^2 ))))) ^2 ) + 1) = sqrt (((((x ^2 ) * ((sqrt (1 + (y ^2 ))) ^2 )) + ((2 * (x * (sqrt (1 + (y ^2 ))))) * (y * (sqrt (1 + (x ^2 )))))) + ((y * (sqrt (1 + (x ^2 )))) ^2 )) + 1)
.= sqrt (((((x ^2 ) * (1 + (y ^2 ))) + ((2 * (x * (sqrt (1 + (y ^2 ))))) * (y * (sqrt (1 + (x ^2 )))))) + ((y * (sqrt (1 + (x ^2 )))) ^2 )) + 1) by A3, SQUARE_1:def 4
.= sqrt (((((x ^2 ) + ((x * y) ^2 )) + ((2 * (x * (sqrt (1 + (y ^2 ))))) * (y * (sqrt (1 + (x ^2 )))))) + ((y ^2 ) * ((sqrt (1 + (x ^2 ))) ^2 ))) + 1)
.= sqrt (((((x ^2 ) + ((x * y) ^2 )) + ((2 * (x * (sqrt (1 + (y ^2 ))))) * (y * (sqrt (1 + (x ^2 )))))) + ((y ^2 ) * (1 + (x ^2 )))) + 1) by A3, SQUARE_1:def 4
.= sqrt (((((x ^2 ) + (2 * ((x * y) ^2 ))) + (y ^2 )) + 1) + (((2 * x) * y) * ((sqrt (1 + (y ^2 ))) * (sqrt (1 + (x ^2 ))))))
.= sqrt (((((x ^2 ) + (2 * ((x * y) ^2 ))) + (y ^2 )) + 1) + (((2 * x) * y) * (sqrt ((1 + (y ^2 )) * (1 + (x ^2 )))))) by A3, SQUARE_1:97 ;
hence (sinh" x) + (sinh" y) = sinh" ((x * (sqrt (1 + (y ^2 )))) + (y * (sqrt (1 + (x ^2 ))))) by A5, A6; :: thesis: verum