let y, z be Real; :: thesis: ( y + z <> 0 implies sinh ((y / 2) + (z / 2)) <> 0 )
assume y + z <> 0 ; :: thesis: sinh ((y / 2) + (z / 2)) <> 0
then (y + z) / 2 <> 0 ;
hence sinh ((y / 2) + (z / 2)) <> 0 by Lm4; :: thesis: verum