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