let z1, z2 be Element of COMPLEX ; :: thesis: cosh_C /. (z1 + z2) = ((cosh_C /. z1) * (cosh_C /. z2)) + ((sinh_C /. z1) * (sinh_C /. z2))
cosh_C /. (z1 + z2) = cosh_C /. (z1 - (- z2))
.= ((cosh_C /. z1) * (cosh_C /. (- z2))) - ((sinh_C /. z1) * (sinh_C /. (- z2))) by Th13
.= ((cosh_C /. z1) * (cosh_C /. z2)) - ((sinh_C /. z1) * (sinh_C /. (- z2))) by Th10
.= ((cosh_C /. z1) * (cosh_C /. z2)) - ((sinh_C /. z1) * (- (sinh_C /. z2))) by Th9
.= ((cosh_C /. z1) * (cosh_C /. z2)) - (- ((sinh_C /. z1) * (sinh_C /. z2))) ;
hence cosh_C /. (z1 + z2) = ((cosh_C /. z1) * (cosh_C /. z2)) + ((sinh_C /. z1) * (sinh_C /. z2)) ; :: thesis: verum