let x, y be Real; ( 1 <= x & 1 <= y implies (cosh1" x) + (cosh1" y) = cosh1" ((x * y) + (sqrt (((x ^2) - 1) * ((y ^2) - 1)))) )
assume that
A1:
1 <= x
and
A2:
1 <= y
; (cosh1" x) + (cosh1" y) = cosh1" ((x * y) + (sqrt (((x ^2) - 1) * ((y ^2) - 1))))
A3:
(y ^2) - 1 >= 0
by A2, Lm3;
set t = (x * (sqrt ((y ^2) - 1))) + (y * (sqrt ((x ^2) - 1)));
A4:
(x ^2) - 1 >= 0
by A1, Lm3;
(x * (sqrt ((y ^2) - 1))) + (y * (sqrt ((x ^2) - 1))) =
sqrt (((x * (sqrt ((y ^2) - 1))) + (y * (sqrt ((x ^2) - 1)))) ^2)
by A1, A2, Th24, SQUARE_1:22
.=
sqrt ((((x ^2) * ((sqrt ((y ^2) - 1)) ^2)) + ((2 * (x * (sqrt ((y ^2) - 1)))) * (y * (sqrt ((x ^2) - 1))))) + ((y * (sqrt ((x ^2) - 1))) ^2))
.=
sqrt ((((x ^2) * ((y ^2) - 1)) + ((2 * (x * (sqrt ((y ^2) - 1)))) * (y * (sqrt ((x ^2) - 1))))) + ((y * (sqrt ((x ^2) - 1))) ^2))
by A3, SQUARE_1:def 2
.=
sqrt (((((x ^2) * (y ^2)) - (x ^2)) + ((2 * (x * (sqrt ((y ^2) - 1)))) * (y * (sqrt ((x ^2) - 1))))) + ((y ^2) * ((sqrt ((x ^2) - 1)) ^2)))
.=
sqrt (((((x ^2) * (y ^2)) - (x ^2)) + ((2 * (x * (sqrt ((y ^2) - 1)))) * (y * (sqrt ((x ^2) - 1))))) + ((y ^2) * ((x ^2) - 1)))
by A4, SQUARE_1:def 2
.=
sqrt ((((2 * ((x * y) ^2)) - (x ^2)) - (y ^2)) + ((2 * (x * (sqrt ((y ^2) - 1)))) * (y * (sqrt ((x ^2) - 1)))))
;
then A5: log (number_e,((((x * (sqrt ((y ^2) - 1))) + (y * (sqrt ((x ^2) - 1)))) + (sqrt (((x ^2) - 1) * ((y ^2) - 1)))) + (x * y))) =
log (number_e,(((sqrt ((((2 * ((x * y) ^2)) - (x ^2)) - (y ^2)) + (((2 * x) * y) * ((sqrt ((y ^2) - 1)) * (sqrt ((x ^2) - 1)))))) + (sqrt (((x ^2) - 1) * ((y ^2) - 1)))) + (x * y)))
.=
log (number_e,(((sqrt ((((2 * ((x * y) ^2)) - (x ^2)) - (y ^2)) + (((2 * x) * y) * (sqrt (((y ^2) - 1) * ((x ^2) - 1)))))) + (sqrt (((x ^2) - 1) * ((y ^2) - 1)))) + (x * y)))
by A4, A3, SQUARE_1:29
;
A6: cosh1" ((x * y) + (sqrt (((x ^2) - 1) * ((y ^2) - 1)))) =
log (number_e,(((x * y) + (sqrt (((x ^2) - 1) * ((y ^2) - 1)))) + (sqrt (((((x * y) ^2) + ((2 * (x * y)) * (sqrt (((x ^2) - 1) * ((y ^2) - 1))))) + ((sqrt (((x ^2) - 1) * ((y ^2) - 1))) ^2)) - 1))))
.=
log (number_e,(((x * y) + (sqrt (((x ^2) - 1) * ((y ^2) - 1)))) + (sqrt (((((x * y) ^2) + ((2 * (x * y)) * (sqrt (((x ^2) - 1) * ((y ^2) - 1))))) + (((x ^2) - 1) * ((y ^2) - 1))) - 1))))
by A4, A3, SQUARE_1:def 2
.=
log (number_e,((sqrt ((((2 * ((x * y) ^2)) - (x ^2)) - (y ^2)) + (((2 * x) * y) * (sqrt (((y ^2) - 1) * ((x ^2) - 1)))))) + ((sqrt (((x ^2) - 1) * ((y ^2) - 1))) + (x * y))))
;
( 0 < x + (sqrt ((x ^2) - 1)) & 0 < y + (sqrt ((y ^2) - 1)) )
by A1, A2, Th23;
then (cosh1" x) + (cosh1" 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))) + (y * (sqrt ((x ^2) - 1)))) + ((sqrt ((x ^2) - 1)) * (sqrt ((y ^2) - 1)))) + (x * y)))
.=
log (number_e,((((x * (sqrt ((y ^2) - 1))) + (y * (sqrt ((x ^2) - 1)))) + (sqrt (((x ^2) - 1) * ((y ^2) - 1)))) + (x * y)))
by A4, A3, SQUARE_1:29
;
hence
(cosh1" x) + (cosh1" y) = cosh1" ((x * y) + (sqrt (((x ^2) - 1) * ((y ^2) - 1))))
by A5, A6; verum