let x, y be Real; (sinh" x) - (sinh" y) = sinh" ((x * (sqrt (1 + (y ^2)))) - (y * (sqrt (1 + (x ^2)))))
set t = ((sqrt ((x ^2) + 1)) * (sqrt ((y ^2) + 1))) - (x * y);
set q = sqrt ((((x * (sqrt (1 + (y ^2)))) - (y * (sqrt (1 + (x ^2))))) ^2) + 1);
A1:
(x ^2) + 1 >= 0
by Lm6;
y + 0 < sqrt ((y ^2) + 1)
by Lm8;
then A2:
(sqrt ((y ^2) + 1)) - y > 0
by XREAL_1:20;
A3:
(y ^2) + 1 >= 0
by Lm6;
((sqrt ((x ^2) + 1)) * (sqrt ((y ^2) + 1))) - (x * y) >= 0
by Lm9;
then A4: ((sqrt ((x ^2) + 1)) * (sqrt ((y ^2) + 1))) - (x * y) =
sqrt ((((sqrt ((x ^2) + 1)) * (sqrt ((y ^2) + 1))) - (x * y)) ^2)
by SQUARE_1:22
.=
sqrt (((((sqrt ((x ^2) + 1)) ^2) * ((sqrt ((y ^2) + 1)) ^2)) - ((2 * ((sqrt ((x ^2) + 1)) * (sqrt ((y ^2) + 1)))) * (x * y))) + ((x * y) ^2))
.=
sqrt (((((x ^2) + 1) * ((sqrt ((y ^2) + 1)) ^2)) - ((2 * ((sqrt ((x ^2) + 1)) * (sqrt ((y ^2) + 1)))) * (x * y))) + ((x * y) ^2))
by A1, SQUARE_1:def 2
.=
sqrt (((((x ^2) + 1) * ((y ^2) + 1)) - ((2 * ((sqrt ((x ^2) + 1)) * (sqrt ((y ^2) + 1)))) * (x * y))) + ((x * y) ^2))
by A3, SQUARE_1:def 2
.=
sqrt (((((2 * ((x * y) ^2)) + (x ^2)) + (y ^2)) + 1) - ((2 * (x * y)) * ((sqrt ((x ^2) + 1)) * (sqrt ((y ^2) + 1)))))
;
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 ^2) * (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 ^2) * (y ^2))) - ((2 * (x * (sqrt (1 + (y ^2))))) * (y * (sqrt (1 + (x ^2)))))) + ((y ^2) * (1 + (x ^2)))) + 1)
by A1, SQUARE_1:def 2
.=
sqrt (((((x ^2) + (y ^2)) + (2 * ((x * y) ^2))) + 1) - ((((2 * x) * y) * (sqrt (1 + (y ^2)))) * (sqrt (1 + (x ^2)))))
;
( (sqrt ((x ^2) + 1)) + x > 0 & (sqrt ((y ^2) + 1)) + y > 0 )
by Th5;
then (sinh" x) - (sinh" y) =
log (number_e,((x + (sqrt ((x ^2) + 1))) / (y + (sqrt ((y ^2) + 1)))))
by Lm1, POWER:54, TAYLOR_1:11
.=
log (number_e,(((x + (sqrt ((x ^2) + 1))) * ((sqrt ((y ^2) + 1)) - y)) / ((y + (sqrt ((y ^2) + 1))) * ((sqrt ((y ^2) + 1)) - y))))
by A2, XCMPLX_1:91
.=
log (number_e,(((x + (sqrt ((x ^2) + 1))) * ((sqrt ((y ^2) + 1)) - y)) / (((sqrt ((y ^2) + 1)) ^2) - (y ^2))))
.=
log (number_e,(((x + (sqrt ((x ^2) + 1))) * ((sqrt ((y ^2) + 1)) - y)) / (((y ^2) + 1) - (y ^2))))
by A3, SQUARE_1:def 2
.=
log (number_e,((((x * (sqrt ((y ^2) + 1))) - (y * (sqrt ((x ^2) + 1)))) + ((sqrt ((x ^2) + 1)) * (sqrt ((y ^2) + 1)))) - (x * y)))
;
hence
(sinh" x) - (sinh" y) = sinh" ((x * (sqrt (1 + (y ^2)))) - (y * (sqrt (1 + (x ^2)))))
by A4, A5; verum