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