A1: ( dom (sinh / cosh ) = (dom sinh ) /\ ((dom cosh ) \ (cosh " {0 })) & ( for p being Real st p in dom (sinh / cosh ) holds
(sinh / cosh ) . p = (sinh . p) * ((cosh . p) " ) ) ) by RFUNCT_1:def 4;
not 0 in rng cosh

proof

assume 0 in rng cosh ; :: thesis: contradiction
then ex p being Real st
( p in dom cosh & 0 = cosh . p ) by PARTFUN1:26;
hence contradiction by Th15; :: thesis: verum

end;

then A2: cosh " {0 } = {} by FUNCT_1:142;
for p being Element of REAL st p in REAL holds
tanh . p = (sinh / cosh ) . p

proof

let p be real number ; :: thesis: ( p is Element of REAL & p in REAL implies tanh . p = (sinh / cosh ) . p )
p is Real by XREAL_0:def 1;
then (sinh / cosh ) . p = (sinh . p) * ((cosh . p) " ) by A1, A2, Th30
.= (sinh . p) / (cosh . p) by XCMPLX_0:def 9
.= tanh . p by Th17 ;
hence ( p is Element of REAL & p in REAL implies tanh . p = (sinh / cosh ) . p ) ; :: thesis: verum

end;

hence tanh = sinh / cosh by A1, A2, Th30, PARTFUN1:34; :: thesis: verum