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 A1: ( dom (sinh / cosh ) = (dom sinh ) /\ ((dom cosh ) \ (cosh " {0 })) & cosh " {0 } = {} ) by FUNCT_1:142, RFUNCT_1:def 4;
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, Th30, RFUNCT_1:def 4
.= (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, Th30, PARTFUN1:34; :: thesis: verum