let B be symmetrical Subset of REAL ; :: thesis: ( B c= dom sec implies sec is_even_on B )
assume A1: B c= dom sec ; :: thesis: sec is_even_on B
B1: for x being Real st x in B holds
sec . (- x) = sec . x

proof

let x be Real; :: thesis: ( x in B implies sec . (- x) = sec . x )
assume A2: x in B ; :: thesis: sec . (- x) = sec . x
then A3: - x in B by Def1;
sec . (- x) = (cos . (- x)) " by A1, A3, RFUNCT_1:def 8
.= (cos . x) " by SIN_COS:33
.= sec . x by A1, A2, RFUNCT_1:def 8 ;
hence sec . (- x) = sec . x ; :: thesis: verum

end;

B2: dom (sec | B) = B by RELAT_1:91, A1;
for x being Real st x in dom (sec | B) & - x in dom (sec | B) holds
(sec | B) . (- x) = (sec | B) . x

proof

let x be Real; :: thesis: ( x in dom (sec | B) & - x in dom (sec | B) implies (sec | B) . (- x) = (sec | B) . x )
assume A4: ( x in dom (sec | B) & - x in dom (sec | B) ) ; :: thesis: (sec | B) . (- x) = (sec | B) . x
(sec | B) . (- x) = (sec | B) /. (- x) by PARTFUN1:def 8, A4
.= sec /. (- x) by PARTFUN2:35, B2, A4, A1
.= sec . (- x) by PARTFUN1:def 8, A1, B2, A4
.= sec . x by B1, B2, A4
.= sec /. x by PARTFUN1:def 8, A1, B2, A4
.= (sec | B) /. x by PARTFUN2:35, B2, A4, A1
.= (sec | B) . x by PARTFUN1:def 8, A4 ;
hence (sec | B) . (- x) = (sec | B) . x ; :: thesis: verum

end;

then ( sec | B is with_symmetrical_domain & sec | B is quasi_even ) by Def3, B2, Def2;
hence sec is_even_on B by A1, Def5; :: thesis: verum