let A be symmetrical Subset of REAL; :: thesis: cosh is_even_on A

A1: dom cosh = REAL by FUNCT_2:def 1;

then A2: dom (cosh | A) = A by RELAT_1:62;

for x being Real st x in dom (cosh | A) & - x in dom (cosh | A) holds

(cosh | A) . (- x) = (cosh | A) . x

hence cosh is_even_on A by A1; :: thesis: verum

A1: dom cosh = REAL by FUNCT_2:def 1;

then A2: dom (cosh | A) = A by RELAT_1:62;

for x being Real st x in dom (cosh | A) & - x in dom (cosh | A) holds

(cosh | A) . (- x) = (cosh | A) . x

proof

then
( cosh | A is with_symmetrical_domain & cosh | A is quasi_even )
by A2;
let x be Real; :: thesis: ( x in dom (cosh | A) & - x in dom (cosh | A) implies (cosh | A) . (- x) = (cosh | A) . x )

assume that

A3: x in dom (cosh | A) and

A4: - x in dom (cosh | A) ; :: thesis: (cosh | A) . (- x) = (cosh | A) . x

reconsider x = x as Element of REAL by XREAL_0:def 1;

(cosh | A) . (- x) = (cosh | A) /. (- x) by A4, PARTFUN1:def 6

.= cosh /. (- x) by A1, A4, PARTFUN2:17

.= cosh /. x by SIN_COS2:19

.= (cosh | A) /. x by A1, A3, PARTFUN2:17

.= (cosh | A) . x by A3, PARTFUN1:def 6 ;

hence (cosh | A) . (- x) = (cosh | A) . x ; :: thesis: verum

end;assume that

A3: x in dom (cosh | A) and

A4: - x in dom (cosh | A) ; :: thesis: (cosh | A) . (- x) = (cosh | A) . x

reconsider x = x as Element of REAL by XREAL_0:def 1;

(cosh | A) . (- x) = (cosh | A) /. (- x) by A4, PARTFUN1:def 6

.= cosh /. (- x) by A1, A4, PARTFUN2:17

.= cosh /. x by SIN_COS2:19

.= (cosh | A) /. x by A1, A3, PARTFUN2:17

.= (cosh | A) . x by A3, PARTFUN1:def 6 ;

hence (cosh | A) . (- x) = (cosh | A) . x ; :: thesis: verum

hence cosh is_even_on A by A1; :: thesis: verum