let p be real number ; :: thesis: for ff being PartFunc of REAL,REAL st ff = compreal holds
sinh . p = ((1 / 2) (#) (exp_R - (exp_R * ff))) . p
A1: p is Real by XREAL_0:def 1;
let ff be PartFunc of REAL,REAL; :: thesis: ( ff = compreal implies sinh . p = ((1 / 2) (#) (exp_R - (exp_R * ff))) . p )
assume A2: ff = compreal ; :: thesis: sinh . p = ((1 / 2) (#) (exp_R - (exp_R * ff))) . p
A3: ( dom (exp_R - (exp_R * ff)) = (dom exp_R) /\ (dom (exp_R * ff)) & dom (exp_R * ff) = REAL ) by A2, FUNCT_2:def 1, VALUED_1:12;
A4: dom ((1 / 2) (#) (exp_R - (exp_R * ff))) = REAL by A2, FUNCT_2:def 1;
sinh . p = ((exp_R . p) - (exp_R . (- p))) / 2 by Def1
.= (1 / 2) * ((exp_R . p) - (exp_R . ((- 1) * p)))
.= (1 / 2) * ((exp_R . p) - ((exp_R * ff) . p)) by A2, Lm14
.= (1 / 2) * ((exp_R - (exp_R * ff)) . p) by A1, A3, SIN_COS:47, VALUED_1:13
.= ((1 / 2) (#) (exp_R - (exp_R * ff))) . p by A1, A4, VALUED_1:def 5 ;
hence sinh . p = ((1 / 2) (#) (exp_R - (exp_R * ff))) . p ; :: thesis: verum