let z1, z2 be Complex; :: thesis: ( ((sinh_C /. z1) * (sinh_C /. z1)) - ((sinh_C /. z2) * (sinh_C /. z2)) = (sinh_C /. (z1 + z2)) * (sinh_C /. (z1 - z2)) & ((cosh_C /. z1) * (cosh_C /. z1)) - ((cosh_C /. z2) * (cosh_C /. z2)) = (sinh_C /. (z1 + z2)) * (sinh_C /. (z1 - z2)) & ((sinh_C /. z1) * (sinh_C /. z1)) - ((sinh_C /. z2) * (sinh_C /. z2)) = ((cosh_C /. z1) * (cosh_C /. z1)) - ((cosh_C /. z2) * (cosh_C /. z2)) )
set s1 = sinh_C /. z1;
set s2 = sinh_C /. z2;
set c1 = cosh_C /. z1;
set c2 = cosh_C /. z2;
A1: (sinh_C /. (z1 + z2)) * (sinh_C /. (z1 - z2)) = (((sinh_C /. z1) * (cosh_C /. z2)) + ((cosh_C /. z1) * (sinh_C /. z2))) * (sinh_C /. (z1 - z2)) by Th11
.= (((sinh_C /. z1) * (cosh_C /. z2)) + ((cosh_C /. z1) * (sinh_C /. z2))) * (((sinh_C /. z1) * (cosh_C /. z2)) - ((cosh_C /. z1) * (sinh_C /. z2))) by Th12
.= (((sinh_C /. z1) * (sinh_C /. z1)) * ((cosh_C /. z2) * (cosh_C /. z2))) - (((sinh_C /. z2) * ((cosh_C /. z1) * (cosh_C /. z1))) * (sinh_C /. z2)) ;
then A2: (sinh_C /. (z1 + z2)) * (sinh_C /. (z1 - z2)) = (((- (((cosh_C /. z1) * (cosh_C /. z1)) - ((sinh_C /. z1) * (sinh_C /. z1)))) * ((cosh_C /. z2) * (cosh_C /. 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)))
.= (((- 1) * ((cosh_C /. z2) * (cosh_C /. 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))) by Th8
.= ((- 1) * ((cosh_C /. z2) * (cosh_C /. z2))) + (((cosh_C /. z1) * (cosh_C /. z1)) * (((cosh_C /. z2) * (cosh_C /. z2)) - ((sinh_C /. z2) * (sinh_C /. z2))))
.= ((- 1) * ((cosh_C /. z2) * (cosh_C /. z2))) + (((cosh_C /. z1) * (cosh_C /. z1)) * 1) by Th8
.= (- ((cosh_C /. z2) * (cosh_C /. z2))) + ((cosh_C /. z1) * (cosh_C /. z1)) ;
(sinh_C /. (z1 + z2)) * (sinh_C /. (z1 - z2)) = ((((sinh_C /. z1) * (sinh_C /. z1)) * (((cosh_C /. z2) * (cosh_C /. z2)) - ((sinh_C /. z2) * (sinh_C /. z2)))) + (((sinh_C /. z1) * (sinh_C /. z1)) * ((sinh_C /. z2) * (sinh_C /. z2)))) - (((sinh_C /. z2) * (sinh_C /. z2)) * ((cosh_C /. z1) * (cosh_C /. z1))) by A1
.= ((((sinh_C /. z1) * (sinh_C /. z1)) * 1) + (((sinh_C /. z1) * (sinh_C /. z1)) * ((sinh_C /. z2) * (sinh_C /. z2)))) - (((sinh_C /. z2) * (sinh_C /. z2)) * ((cosh_C /. z1) * (cosh_C /. z1))) by Th8
.= (((sinh_C /. z1) * (sinh_C /. z1)) * 1) + (((sinh_C /. z2) * (sinh_C /. z2)) * (- (((cosh_C /. z1) * (cosh_C /. z1)) - ((sinh_C /. z1) * (sinh_C /. z1)))))
.= (((sinh_C /. z1) * (sinh_C /. z1)) * 1) + (((sinh_C /. z2) * (sinh_C /. z2)) * (- 1)) by Th8
.= (((sinh_C /. z1) * (sinh_C /. z1)) * 1) - ((sinh_C /. z2) * (sinh_C /. z2)) ;
hence ( ((sinh_C /. z1) * (sinh_C /. z1)) - ((sinh_C /. z2) * (sinh_C /. z2)) = (sinh_C /. (z1 + z2)) * (sinh_C /. (z1 - z2)) & ((cosh_C /. z1) * (cosh_C /. z1)) - ((cosh_C /. z2) * (cosh_C /. z2)) = (sinh_C /. (z1 + z2)) * (sinh_C /. (z1 - z2)) & ((sinh_C /. z1) * (sinh_C /. z1)) - ((sinh_C /. z2) * (sinh_C /. z2)) = ((cosh_C /. z1) * (cosh_C /. z1)) - ((cosh_C /. z2) * (cosh_C /. z2)) ) by A2; :: thesis: verum