let x, y be Real; ( (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
; (sinh" x) + (sinh" y) = sinh" ((x * (sqrt (1 + (y ^2)))) + (y * (sqrt (1 + (x ^2)))))
( (sqrt ((x ^2) + 1)) + x > 0 & (sqrt ((y ^2) + 1)) + y > 0 )
by Th5;
then A2: (sinh" x) + (sinh" y) =
log (number_e,((x + (sqrt ((x ^2) + 1))) * (y + (sqrt ((y ^2) + 1)))))
by Lm1, POWER:53, TAYLOR_1:11
.=
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:22
;
A3:
(y ^2) + 1 >= 0
by Lm6;
set p = sqrt ((((x * (sqrt (1 + (y ^2)))) + (y * (sqrt (1 + (x ^2))))) ^2) + 1);
set t = sqrt (((x * y) + ((sqrt ((x ^2) + 1)) * (sqrt ((y ^2) + 1)))) ^2);
A4:
(x ^2) + 1 >= 0
by Lm6;
A5: 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 2
.=
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 A4, SQUARE_1:def 2
.=
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 A4, A3, SQUARE_1:29
;
sqrt (((x * y) + ((sqrt ((x ^2) + 1)) * (sqrt ((y ^2) + 1)))) ^2) =
sqrt (((x * y) + (sqrt (((x ^2) + 1) * ((y ^2) + 1)))) ^2)
by A4, A3, SQUARE_1:29
.=
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, A3, SQUARE_1:def 2
.=
sqrt (((((2 * ((x * y) ^2)) + (x ^2)) + (y ^2)) + 1) + ((2 * (x * y)) * (sqrt (((x ^2) + 1) * ((y ^2) + 1)))))
;
hence
(sinh" x) + (sinh" y) = sinh" ((x * (sqrt (1 + (y ^2)))) + (y * (sqrt (1 + (x ^2)))))
by A2, A5; verum