let A be symmetrical Subset of COMPLEX ; :: thesis: ( A c= [.(- 1),1.] implies arctan is_odd_on A )
assume A0: A c= [.(- 1),1.] ; :: thesis: arctan is_odd_on A
then A1: A c= dom arctan by SIN_COS9:23, XBOOLE_1:1;
B1: for x being Real st x in A holds
arctan . (- x) = - (arctan . x)

proof

let x be Real; :: thesis: ( x in A implies arctan . (- x) = - (arctan . x) )
assume x in A ; :: thesis: arctan . (- x) = - (arctan . x)
then ( - 1 <= x & x <= 1 ) by XXREAL_1:1, A0;
then arctan x = - (arctan (- x)) by SIN_COS9:67;
hence arctan . (- x) = - (arctan . x) ; :: thesis: verum

end;

A2: dom (arctan | A) = A by RELAT_1:91, A0, SIN_COS9:23, XBOOLE_1:1;
for x being Real st x in dom (arctan | A) & - x in dom (arctan | A) holds
(arctan | A) . (- x) = - ((arctan | A) . x)

proof

let x be Real; :: thesis: ( x in dom (arctan | A) & - x in dom (arctan | A) implies (arctan | A) . (- x) = - ((arctan | A) . x) )
assume A3: ( x in dom (arctan | A) & - x in dom (arctan | A) ) ; :: thesis: (arctan | A) . (- x) = - ((arctan | A) . x)
(arctan | A) . (- x) = (arctan | A) /. (- x) by PARTFUN1:def 8, A3
.= arctan /. (- x) by PARTFUN2:35, A2, A3, A1
.= arctan . (- x) by PARTFUN1:def 8, A1, A2, A3
.= - (arctan . x) by B1, A2, A3
.= - (arctan /. x) by PARTFUN1:def 8, A1, A2, A3
.= - ((arctan | A) /. x) by PARTFUN2:35, A2, A3, A1
.= - ((arctan | A) . x) by PARTFUN1:def 8, A3 ;
hence (arctan | A) . (- x) = - ((arctan | A) . x) ; :: thesis: verum

end;

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