let A be symmetrical Subset of COMPLEX ; :: thesis: ( A c= ].(- (PI / 2)),(PI / 2).[ implies tan is_odd_on A )
assume A0: A c= ].(- (PI / 2)),(PI / 2).[ ; :: thesis: tan is_odd_on A
A1: A c= dom tan by XBOOLE_1:1, A0, SIN_COS9:1;
B1: 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)
- x in A by A4, Def1;
then tan . (- x) = tan (- x) by A0, SIN_COS9:13
.= - (tan x) by SIN_COS4:2
.= - (tan . x) by SIN_COS9:13, A0, A4 ;
hence tan . (- x) = - (tan . x) ; :: thesis: verum

end;

A2: dom (tan | A) = A by RELAT_1:91, XBOOLE_1:1, A0, SIN_COS9:1;
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 A3: ( x in dom (tan | A) & - x in dom (tan | A) ) ; :: thesis: (tan | A) . (- x) = - ((tan | A) . x)
(tan | A) . (- x) = (tan | A) /. (- x) by PARTFUN1:def 8, A3
.= tan /. (- x) by PARTFUN2:35, A2, A3, A1
.= tan . (- x) by PARTFUN1:def 8, A1, A2, A3
.= - (tan . x) by B1, A2, A3
.= - (tan /. x) by PARTFUN1:def 8, A1, A2, A3
.= - ((tan | A) /. x) by PARTFUN2:35, A2, A3, A1
.= - ((tan | A) . x) by PARTFUN1:def 8, A3 ;
hence (tan | A) . (- x) = - ((tan | A) . x) ; :: thesis: verum

end;

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