let p be Real; for ff being PartFunc of REAL,REAL st ff = compreal holds
sinh . p = ((1 / 2) (#) (exp_R - (exp_R * ff))) . p
A1:
p in REAL
by XREAL_0:def 1;
let ff be PartFunc of REAL,REAL; ( ff = compreal implies sinh . p = ((1 / 2) (#) (exp_R - (exp_R * ff))) . p )
assume A2:
ff = compreal
; 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
; verum