let ff be PartFunc of REAL ,REAL ; :: thesis: ( ff = compreal implies cosh = (1 / 2) (#) (exp_R + (exp_R * ff)) )
assume A1: ff = compreal ; :: thesis: cosh = (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:def 1;
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 cosh & 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
cosh . p = ((1 / 2) (#) (exp_R + (exp_R * ff))) . p by A1, Lm21;
hence cosh = (1 / 2) (#) (exp_R + (exp_R * ff)) by A3, PARTFUN1:34; :: thesis: verum