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

A1: dom (cos | A) = A by RELAT_1:62, SIN_COS:24;

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

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

hence cos is_even_on A by SIN_COS:24; :: thesis: verum

A1: dom (cos | A) = A by RELAT_1:62, SIN_COS:24;

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

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

proof

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

assume that

A2: x in dom (cos | A) and

A3: - x in dom (cos | A) ; :: thesis: (cos | A) . (- x) = (cos | A) . x

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

(cos | A) . (- x) = (cos | A) /. (- x) by A3, PARTFUN1:def 6

.= cos /. (- x) by A3, PARTFUN2:17, SIN_COS:24

.= cos /. x by SIN_COS:30

.= (cos | A) /. x by A2, PARTFUN2:17, SIN_COS:24

.= (cos | A) . x by A2, PARTFUN1:def 6 ;

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

end;assume that

A2: x in dom (cos | A) and

A3: - x in dom (cos | A) ; :: thesis: (cos | A) . (- x) = (cos | A) . x

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

(cos | A) . (- x) = (cos | A) /. (- x) by A3, PARTFUN1:def 6

.= cos /. (- x) by A3, PARTFUN2:17, SIN_COS:24

.= cos /. x by SIN_COS:30

.= (cos | A) /. x by A2, PARTFUN2:17, SIN_COS:24

.= (cos | A) . x by A2, PARTFUN1:def 6 ;

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

hence cos is_even_on A by SIN_COS:24; :: thesis: verum