let p be real number ; :: thesis: ( tanh . p < 1 & tanh . p > - 1 )
thus tanh . p < 1 :: thesis: tanh . p > - 1

proof

assume tanh . p >= 1 ; :: thesis: contradiction
then A1: ((exp_R . p) - (exp_R . (- p))) / ((exp_R . p) + (exp_R . (- p))) >= 1 by Def5;
(exp_R . p) + (exp_R . (- p)) >= 2 by Lm25;
then A2: (((exp_R . p) - (exp_R . (- p))) / ((exp_R . p) + (exp_R . (- p)))) * ((exp_R . p) + (exp_R . (- p))) >= 1 * ((exp_R . p) + (exp_R . (- p))) by A1, XREAL_1:66;
( exp_R . p > 0 & exp_R . (- p) > 0 ) by SIN_COS:59;
then (exp_R . p) + (exp_R . (- p)) > 0 + 0 ;
then (((exp_R . p) - (exp_R . (- p))) / ((exp_R . p) + (exp_R . (- p)))) * ((exp_R . p) + (exp_R . (- p))) = (exp_R . p) - (exp_R . (- p)) by XCMPLX_1:88;
then ((exp_R . p) - (exp_R . (- p))) - (exp_R . p) >= ((exp_R . p) + (exp_R . (- p))) - (exp_R . p) by A2, XREAL_1:11;
then A3: (- (exp_R . (- p))) + (exp_R . (- p)) >= (exp_R . (- p)) + (exp_R . (- p)) by XREAL_1:8;
( exp_R . (- p) > 0 & exp_R . (- p) > 0 ) by SIN_COS:59;
then (exp_R . (- p)) + (exp_R . (- p)) > 0 + 0 ;
hence contradiction by A3; :: thesis: verum

end;

assume tanh . p <= - 1 ; :: thesis: contradiction
then A4: ((exp_R . p) - (exp_R . (- p))) / ((exp_R . p) + (exp_R . (- p))) <= - 1 by Def5;
(exp_R . p) + (exp_R . (- p)) >= 2 by Lm25;
then A5: (((exp_R . p) - (exp_R . (- p))) / ((exp_R . p) + (exp_R . (- p)))) * ((exp_R . p) + (exp_R . (- p))) <= (- 1) * ((exp_R . p) + (exp_R . (- p))) by A4, XREAL_1:66;
( exp_R . p > 0 & exp_R . (- p) > 0 ) by SIN_COS:59;
then (exp_R . p) + (exp_R . (- p)) > 0 + 0 ;
then (exp_R . p) - (exp_R . (- p)) <= - ((exp_R . p) + (exp_R . (- p))) by A5, XCMPLX_1:88;
then ((exp_R . p) - (exp_R . (- p))) + (exp_R . (- p)) <= ((- (exp_R . p)) + (- (exp_R . (- p)))) + (exp_R . (- p)) by XREAL_1:8;
then A6: (exp_R . p) + (exp_R . p) <= (- (exp_R . p)) + (exp_R . p) by XREAL_1:8;
( exp_R . p > 0 & exp_R . p > 0 ) by SIN_COS:59;
then (exp_R . p) + (exp_R . p) > 0 + 0 ;
hence contradiction by A6; :: thesis: verum