let z1, z2 be Complex; :: thesis: ( (sinh_C /. (2 * z1)) + (sinh_C /. (2 * z2)) = (2 * (sinh_C /. (z1 + z2))) * (cosh_C /. (z1 - z2)) & (sinh_C /. (2 * z1)) - (sinh_C /. (2 * z2)) = (2 * (sinh_C /. (z1 - z2))) * (cosh_C /. (z1 + z2)) )
set c1 = cosh_C /. z1;
set c2 = cosh_C /. z2;
set s1 = sinh_C /. z1;
set s2 = sinh_C /. z2;
A1: (2 * (sinh_C /. (z1 - z2))) * (cosh_C /. (z1 + z2)) = (2 * (((sinh_C /. z1) * (cosh_C /. z2)) - ((cosh_C /. z1) * (sinh_C /. z2)))) * (cosh_C /. (z1 + z2)) by Th12
.= (2 * (((sinh_C /. z1) * (cosh_C /. z2)) - ((cosh_C /. z1) * (sinh_C /. z2)))) * (((cosh_C /. z1) * (cosh_C /. z2)) + ((sinh_C /. z1) * (sinh_C /. z2))) by Th14
.= 2 * ((((sinh_C /. z1) * (cosh_C /. z1)) * (((cosh_C /. z2) * (cosh_C /. z2)) - ((sinh_C /. z2) * (sinh_C /. z2)))) - ((((sinh_C /. z2) * (cosh_C /. z2)) * ((cosh_C /. z1) * (cosh_C /. z1))) - (((sinh_C /. z2) * (cosh_C /. z2)) * ((sinh_C /. z1) * (sinh_C /. z1)))))
.= 2 * ((((sinh_C /. z1) * (cosh_C /. z1)) * 1) - (((sinh_C /. z2) * (cosh_C /. z2)) * (((cosh_C /. z1) * (cosh_C /. z1)) - ((sinh_C /. z1) * (sinh_C /. z1))))) by Th8
.= 2 * ((((sinh_C /. z1) * (cosh_C /. z1)) * 1) - (((sinh_C /. z2) * (cosh_C /. z2)) * 1)) by Th8
.= ((2 * (sinh_C /. z1)) * (cosh_C /. z1)) - (2 * ((sinh_C /. z2) * (cosh_C /. z2)))
.= (sinh_C /. (2 * z1)) - ((2 * (sinh_C /. z2)) * (cosh_C /. z2)) by Th58 ;
(2 * (sinh_C /. (z1 + z2))) * (cosh_C /. (z1 - z2)) = (2 * (((sinh_C /. z1) * (cosh_C /. z2)) + ((cosh_C /. z1) * (sinh_C /. z2)))) * (cosh_C /. (z1 - z2)) by Th11
.= (2 * (((sinh_C /. z1) * (cosh_C /. z2)) + ((cosh_C /. z1) * (sinh_C /. z2)))) * (((cosh_C /. z1) * (cosh_C /. z2)) - ((sinh_C /. z1) * (sinh_C /. z2))) by Th13
.= 2 * (((((cosh_C /. z2) * (cosh_C /. z2)) - ((sinh_C /. z2) * (sinh_C /. z2))) * ((cosh_C /. z1) * (sinh_C /. z1))) + ((((cosh_C /. z1) * (cosh_C /. z1)) * ((sinh_C /. z2) * (cosh_C /. z2))) - (((sinh_C /. z1) * (sinh_C /. z1)) * ((cosh_C /. z2) * (sinh_C /. z2)))))
.= 2 * ((1 * ((cosh_C /. z1) * (sinh_C /. z1))) + ((((cosh_C /. z1) * (cosh_C /. z1)) - ((sinh_C /. z1) * (sinh_C /. z1))) * ((cosh_C /. z2) * (sinh_C /. z2)))) by Th8
.= 2 * ((1 * ((cosh_C /. z1) * (sinh_C /. z1))) + (1 * ((cosh_C /. z2) * (sinh_C /. z2)))) by Th8
.= ((2 * (sinh_C /. z1)) * (cosh_C /. z1)) + (2 * ((cosh_C /. z2) * (sinh_C /. z2)))
.= (sinh_C /. (2 * z1)) + ((2 * (sinh_C /. z2)) * (cosh_C /. z2)) by Th58
.= (sinh_C /. (2 * z1)) + (sinh_C /. (2 * z2)) by Th58 ;
hence ( (sinh_C /. (2 * z1)) + (sinh_C /. (2 * z2)) = (2 * (sinh_C /. (z1 + z2))) * (cosh_C /. (z1 - z2)) & (sinh_C /. (2 * z1)) - (sinh_C /. (2 * z2)) = (2 * (sinh_C /. (z1 - z2))) * (cosh_C /. (z1 + z2)) ) by A1, Th58; :: thesis: verum