let p be Real; :: thesis: for ff being PartFunc of REAL,REAL st ff = compreal holds
cosh . 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; :: thesis: ( ff = compreal implies cosh . p = ((1 / 2) (#) (exp_R + (exp_R * ff))) . p )
assume A2: ff = compreal ; :: thesis: cosh . 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:def 1;
A4: dom ((1 / 2) (#) (exp_R + (exp_R * ff))) = REAL by A2, FUNCT_2:def 1;
cosh . p = ((exp_R . p) + (exp_R . (- p))) / 2 by Def3
.= (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:def 1
.= ((1 / 2) (#) (exp_R + (exp_R * ff))) . p by A1, A4, VALUED_1:def 5 ;
hence cosh . p = ((1 / 2) (#) (exp_R + (exp_R * ff))) . p ; :: thesis: verum