theorem :: SIN_COS8:13

for y, z being Real holds
( (((sinh y) - (sinh z)) ^2) - (((cosh y) - (cosh z)) ^2) = 4 * ((sinh ((y - z) / 2)) ^2) & (((cosh y) + (cosh z)) ^2) - (((sinh y) + (sinh z)) ^2) = 4 * ((cosh ((y - z) / 2)) ^2) )