let z1, z2 be Element of COMPLEX ; sinh_C /. (z1 + z2) = ((sinh_C /. z1) * (cosh_C /. z2)) + ((cosh_C /. z1) * (sinh_C /. z2))
set e1 = exp z1;
set e2 = exp (- z1);
set e3 = exp z2;
set e4 = exp (- z2);
((sinh_C /. z1) * (cosh_C /. z2)) + ((cosh_C /. z1) * (sinh_C /. z2)) =
((((exp z1) - (exp (- z1))) / 2) * (cosh_C /. z2)) + ((cosh_C /. z1) * (sinh_C /. z2))
by Def3
.=
((((exp z1) - (exp (- z1))) / 2) * (cosh_C /. z2)) + ((cosh_C /. z1) * (((exp z2) - (exp (- z2))) / 2))
by Def3
.=
((((exp z1) - (exp (- z1))) / 2) * (cosh_C /. z2)) + ((((exp z1) + (exp (- z1))) / 2) * (((exp z2) - (exp (- z2))) / 2))
by Def4
.=
((((exp z1) - (exp (- z1))) / 2) * (((exp z2) + (exp (- z2))) / 2)) + ((((exp z1) + (exp (- z1))) / 2) * (((exp z2) - (exp (- z2))) / 2))
by Def4
.=
((((exp z1) * (exp z2)) + ((exp z1) * (exp z2))) - (((exp (- z1)) * (exp (- z2))) + ((exp (- z1)) * (exp (- z2))))) / 4
.=
((((Re ((exp z1) * (exp z2))) + (Re ((exp z1) * (exp z2)))) + (((Im ((exp z1) * (exp z2))) + (Im ((exp z1) * (exp z2)))) * <i>)) - (((exp (- z1)) * (exp (- z2))) + ((exp (- z1)) * (exp (- z2))))) / 4
by COMPLEX1:def 5
.=
(((2 * (Re ((exp z1) * (exp z2)))) + ((2 * (Im ((exp z1) * (exp z2)))) * <i>)) - (((exp (- z1)) * (exp (- z2))) + ((exp (- z1)) * (exp (- z2))))) / 4
.=
(((Re (2 * ((exp z1) * (exp z2)))) + ((2 * (Im ((exp z1) * (exp z2)))) * <i>)) - (((exp (- z1)) * (exp (- z2))) + ((exp (- z1)) * (exp (- z2))))) / 4
by COMSEQ_3:17
.=
(((Re (2 * ((exp z1) * (exp z2)))) + ((Im (2 * ((exp z1) * (exp z2)))) * <i>)) - (((exp (- z1)) * (exp (- z2))) + ((exp (- z1)) * (exp (- z2))))) / 4
by COMSEQ_3:17
.=
((2 * ((exp z1) * (exp z2))) - (((exp (- z1)) * (exp (- z2))) + ((exp (- z1)) * (exp (- z2))))) / 4
by COMPLEX1:13
.=
((2 * ((exp z1) * (exp z2))) - (((Re ((exp (- z1)) * (exp (- z2)))) + (Re ((exp (- z1)) * (exp (- z2))))) + (((Im ((exp (- z1)) * (exp (- z2)))) + (Im ((exp (- z1)) * (exp (- z2))))) * <i>))) / 4
by COMPLEX1:def 5
.=
((2 * ((exp z1) * (exp z2))) - ((2 * (Re ((exp (- z1)) * (exp (- z2))))) + ((2 * (Im ((exp (- z1)) * (exp (- z2))))) * <i>))) / 4
.=
((2 * ((exp z1) * (exp z2))) - ((Re (2 * ((exp (- z1)) * (exp (- z2))))) + ((2 * (Im ((exp (- z1)) * (exp (- z2))))) * <i>))) / 4
by COMSEQ_3:17
.=
((2 * ((exp z1) * (exp z2))) - ((Re (2 * ((exp (- z1)) * (exp (- z2))))) + ((Im (2 * ((exp (- z1)) * (exp (- z2))))) * <i>))) / 4
by COMSEQ_3:17
.=
((2 * ((exp z1) * (exp z2))) - (2 * ((exp (- z1)) * (exp (- z2))))) / 4
by COMPLEX1:13
.=
(((exp z1) * (exp z2)) / 2) - ((2 * ((exp (- z1)) * (exp (- z2)))) / (2 * 2))
.=
((exp (z1 + z2)) / 2) - (((exp (- z1)) * (exp (- z2))) / 2)
by SIN_COS:23
.=
((exp (z1 + z2)) / 2) - ((exp ((- z1) + (- z2))) / 2)
by SIN_COS:23
.=
((exp (z1 + z2)) - (exp (- (z1 + z2)))) / 2
;
hence
sinh_C /. (z1 + z2) = ((sinh_C /. z1) * (cosh_C /. z2)) + ((cosh_C /. z1) * (sinh_C /. z2))
by Def3; verum