let A be symmetrical Subset of REAL; :: thesis: cos is_even_on A
A1: dom (cos | A) = A by RELAT_1:91, SIN_COS:27;
for x being Real st x in dom (cos | A) & - x in dom (cos | A) holds
(cos | A) . (- x) = (cos | A) . x

proof

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
(cos | A) . (- x) = (cos | A) /. (- x) by A3, PARTFUN1:def 8
.= cos /. (- x) by A1, A3, PARTFUN2:35, SIN_COS:27
.= cos /. x by SIN_COS:33
.= (cos | A) /. x by A1, A2, PARTFUN2:35, SIN_COS:27
.= (cos | A) . x by A2, PARTFUN1:def 8 ;
hence (cos | A) . (- x) = (cos | A) . x ; :: thesis: verum

end;

then ( cos | A is with_symmetrical_domain & cos | A is quasi_even ) by A1, Def2, Def3;
hence cos is_even_on A by Def5, SIN_COS:27; :: thesis: verum