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

then A2: dom (sec | B) = B by RELAT_1:62;

A3: for x being Real st x in B holds

sec . (- x) = sec . x

(sec | B) . (- x) = (sec | B) . x

hence sec is_even_on B by A1; :: thesis: verum

assume A1: B c= dom sec ; :: thesis: sec is_even_on B

then A2: dom (sec | B) = B by RELAT_1:62;

A3: for x being Real st x in B holds

sec . (- x) = sec . x

proof

for x being Real st x in dom (sec | B) & - x in dom (sec | B) holds
let x be Real; :: thesis: ( x in B implies sec . (- x) = sec . x )

assume A4: x in B ; :: thesis: sec . (- x) = sec . x

then - x in B by Def1;

then sec . (- x) = (cos . (- x)) " by A1, RFUNCT_1:def 2

.= (cos . x) " by SIN_COS:30

.= sec . x by A1, A4, RFUNCT_1:def 2 ;

hence sec . (- x) = sec . x ; :: thesis: verum

end;assume A4: x in B ; :: thesis: sec . (- x) = sec . x

then - x in B by Def1;

then sec . (- x) = (cos . (- x)) " by A1, RFUNCT_1:def 2

.= (cos . x) " by SIN_COS:30

.= sec . x by A1, A4, RFUNCT_1:def 2 ;

hence sec . (- x) = sec . x ; :: thesis: verum

(sec | B) . (- x) = (sec | B) . x

proof

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

assume that

A5: x in dom (sec | B) and

A6: - x in dom (sec | B) ; :: thesis: (sec | B) . (- x) = (sec | B) . x

(sec | B) . (- x) = (sec | B) /. (- x) by A6, PARTFUN1:def 6

.= sec /. (- x) by A1, A2, A6, PARTFUN2:17

.= sec . (- x) by A1, A6, PARTFUN1:def 6

.= sec . x by A3, A5

.= sec /. x by A1, A5, PARTFUN1:def 6

.= (sec | B) /. x by A1, A2, A5, PARTFUN2:17

.= (sec | B) . x by A5, PARTFUN1:def 6 ;

hence (sec | B) . (- x) = (sec | B) . x ; :: thesis: verum

end;assume that

A5: x in dom (sec | B) and

A6: - x in dom (sec | B) ; :: thesis: (sec | B) . (- x) = (sec | B) . x

(sec | B) . (- x) = (sec | B) /. (- x) by A6, PARTFUN1:def 6

.= sec /. (- x) by A1, A2, A6, PARTFUN2:17

.= sec . (- x) by A1, A6, PARTFUN1:def 6

.= sec . x by A3, A5

.= sec /. x by A1, A5, PARTFUN1:def 6

.= (sec | B) /. x by A1, A2, A5, PARTFUN2:17

.= (sec | B) . x by A5, PARTFUN1:def 6 ;

hence (sec | B) . (- x) = (sec | B) . x ; :: thesis: verum

hence sec is_even_on B by A1; :: thesis: verum