let A be symmetrical Subset of COMPLEX; :: thesis: ( A c= dom tan implies tan is_odd_on A )
assume A1: A c= dom tan ; :: thesis: tan is_odd_on A
A2: dom (tan | A) = A by A1, RELAT_1:62;
A3: for x being Real st x in A holds
tan . (- x) = - (tan . x)

proof

let x be Real; :: thesis: ( x in A implies tan . (- x) = - (tan . x) )
assume A4: x in A ; :: thesis: tan . (- x) = - (tan . x)
then A5: cos . x <> 0 by A1, FDIFF_8:1;
- x in A by Def1, A4;
then tan . (- x) = tan (- x) by A1, FDIFF_8:1, SIN_COS9:15
.= - (tan x) by SIN_COS4:1
.= - (tan . x) by A5, SIN_COS9:15 ;
hence tan . (- x) = - (tan . x) ; :: thesis: verum

end;

for x being Real st x in dom (tan | A) & - x in dom (tan | A) holds
(tan | A) . (- x) = - ((tan | A) . x)

proof

let x be Real; :: thesis: ( x in dom (tan | A) & - x in dom (tan | A) implies (tan | A) . (- x) = - ((tan | A) . x) )
assume that
A6: x in dom (tan | A) and
A7: - x in dom (tan | A) ; :: thesis: (tan | A) . (- x) = - ((tan | A) . x)
reconsider x = x as Element of REAL by XREAL_0:def 1;
(tan | A) . (- x) = (tan | A) /. (- x) by A7, PARTFUN1:def 6
.= tan /. (- x) by A1, A2, A7, PARTFUN2:17
.= tan . (- x) by A1, A7, PARTFUN1:def 6
.= - (tan . x) by A3, A6
.= - (tan /. x) by A1, A6, PARTFUN1:def 6
.= - ((tan | A) /. x) by A1, A2, A6, PARTFUN2:17
.= - ((tan | A) . x) by A6, PARTFUN1:def 6 ;
hence (tan | A) . (- x) = - ((tan | A) . x) ; :: thesis: verum

end;

then ( tan | A is with_symmetrical_domain & tan | A is quasi_odd ) by A2;
hence tan is_odd_on A by A1; :: thesis: verum