let A be symmetrical Subset of REAL ; :: thesis: cos is_even_on A
A2: 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 A3: ( x in dom (cos | A) & - x in dom (cos | A) ) ; :: thesis: (cos | A) . (- x) = (cos | A) . x
(cos | A) . (- x) = (cos | A) /. (- x) by PARTFUN1:def 8, A3
.= cos /. (- x) by PARTFUN2:35, A2, A3, SIN_COS:27
.= cos /. x by SIN_COS:33
.= (cos | A) /. x by PARTFUN2:35, A2, A3, SIN_COS:27
.= (cos | A) . x by PARTFUN1:def 8, A3 ;
hence (cos | A) . (- x) = (cos | A) . x ; :: thesis: verum

end;

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