let ff be PartFunc of REAL ,REAL ; :: thesis: ( ff = compreal implies sinh = (1 / 2) (#) (exp_R - (exp_R * ff)) )
assume A1: ff = compreal ; :: thesis: sinh = (1 / 2) (#) (exp_R - (exp_R * ff))
A2: ( dom (exp_R - (exp_R * ff)) = (dom exp_R ) /\ (dom (exp_R * ff)) & ( for p being Real st p in dom (exp_R - (exp_R * ff)) holds
(exp_R . p) - ((exp_R * ff) . p) = (exp_R - (exp_R * ff)) . p ) ) by VALUED_1:12, VALUED_1:13;
dom (exp_R - (exp_R * ff)) = REAL

proof

dom (exp_R * ff) = REAL by A1, Lm12, RELAT_1:46, SIN_COS:51;
hence dom (exp_R - (exp_R * ff)) = REAL by A2, SIN_COS:51; :: thesis: verum

end;

then A3: ( REAL = dom sinh & REAL = dom ((1 / 2) (#) (exp_R - (exp_R * ff))) ) by FUNCT_2:def 1, VALUED_1:def 5;
for p being Element of REAL st p in REAL holds
sinh . p = ((1 / 2) (#) (exp_R - (exp_R * ff))) . p by A1, Lm18;
hence sinh = (1 / 2) (#) (exp_R - (exp_R * ff)) by A3, PARTFUN1:34; :: thesis: verum
thus verum ; :: thesis: verum