let ff be PartFunc of REAL,REAL; :: thesis: ( ff = compreal implies sinh = (1 / 2) (#) (exp_R - (exp_R * ff)) )
assume ff = compreal ; :: thesis: sinh = (1 / 2) (#) (exp_R - (exp_R * ff))
then A1: ( REAL = dom ((1 / 2) (#) (exp_R - (exp_R * ff))) & ( for p being Element of REAL st p in REAL holds
sinh . p = ((1 / 2) (#) (exp_R - (exp_R * ff))) . p ) ) by Lm17, FUNCT_2:def 1;
REAL = dom sinh by FUNCT_2:def 1;
hence sinh = (1 / 2) (#) (exp_R - (exp_R * ff)) by A1, PARTFUN1:5; :: thesis: verum