let x be Real; ( x >= 1 implies cosh1" x = 2 * (sinh" (sqrt ((x - 1) / 2))) )
assume A1:
x >= 1
; cosh1" x = 2 * (sinh" (sqrt ((x - 1) / 2)))
then A2:
(sqrt ((x + 1) / 2)) + (sqrt ((x - 1) / 2)) > 0
by Th10;
A3:
((x ^2) - 1) / 4 >= 0
by A1, Th9;
A4:
(x - 1) / 2 >= 0
by A1, Th7;
then 2 * (sinh" (sqrt ((x - 1) / 2))) =
2 * (log (number_e,((sqrt ((x - 1) / 2)) + (sqrt (((x - 1) / 2) + 1)))))
by SQUARE_1:def 2
.=
log (number_e,(((sqrt ((x - 1) / 2)) + (sqrt ((x + 1) / 2))) to_power 2))
by A2, Lm1, POWER:55, TAYLOR_1:11
.=
log (number_e,(((sqrt ((x - 1) / 2)) + (sqrt ((x + 1) / 2))) ^2))
by POWER:46
.=
log (number_e,((((sqrt ((x - 1) / 2)) ^2) + ((2 * (sqrt ((x - 1) / 2))) * (sqrt ((x + 1) / 2)))) + ((sqrt ((x + 1) / 2)) ^2)))
.=
log (number_e,((((x - 1) / 2) + ((2 * (sqrt ((x - 1) / 2))) * (sqrt ((x + 1) / 2)))) + ((sqrt ((x + 1) / 2)) ^2)))
by A4, SQUARE_1:def 2
.=
log (number_e,((((x - 1) / 2) + ((2 * (sqrt ((x - 1) / 2))) * (sqrt ((x + 1) / 2)))) + ((x + 1) / 2)))
by A1, SQUARE_1:def 2
.=
log (number_e,(x + (2 * ((sqrt ((x - 1) / 2)) * (sqrt ((x + 1) / 2))))))
.=
log (number_e,(x + (2 * (sqrt (((x - 1) / 2) * ((x + 1) / 2))))))
by A1, A4, SQUARE_1:29
.=
log (number_e,(x + ((sqrt (2 ^2)) * (sqrt (((x ^2) - 1) / 4)))))
by SQUARE_1:22
.=
log (number_e,(x + (sqrt (4 * (((x ^2) - 1) / 4)))))
by A3, SQUARE_1:29
.=
log (number_e,(x + (sqrt ((x ^2) - 1))))
;
hence
cosh1" x = 2 * (sinh" (sqrt ((x - 1) / 2)))
; verum