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