not 0 in rng cosh
proof
assume 0 in rng cosh ; :: thesis: contradiction
then ex p being Element of REAL st
( p in dom cosh & 0 = cosh . p ) by PARTFUN1:3;
hence contradiction by Th15; :: thesis: verum
end;
then A1: ( dom (sinh / cosh) = (dom sinh) /\ ((dom cosh) \ (cosh " {0})) & cosh " {0} = {} ) by FUNCT_1:72, RFUNCT_1:def 1;
for p being Element of REAL st p in REAL holds
tanh . p = (sinh / cosh) . p
proof
let p be Real; :: thesis: ( p is set & p is Element of REAL & p in REAL implies tanh . p = (sinh / cosh) . p )
p in REAL by XREAL_0:def 1;
then (sinh / cosh) . p = (sinh . p) * ((cosh . p) ") by A1, Th30, RFUNCT_1:def 1
.= (sinh . p) / (cosh . p) by XCMPLX_0:def 9
.= tanh . p by Th17 ;
hence ( p is set & p is Element of REAL & p in REAL implies tanh . p = (sinh / cosh) . p ) ; :: thesis: verum
end;
hence tanh = sinh / cosh by A1, Th30, PARTFUN1:5; :: thesis: verum