let A be symmetrical Subset of COMPLEX; :: thesis: ( A c= [.(- 1),1.] implies arctan is_odd_on A )
assume A1: A c= [.(- 1),1.] ; :: thesis: arctan is_odd_on A
then A2: A c= dom arctan by SIN_COS9:23;
A3: dom (arctan | A) = A by A1, RELAT_1:62, SIN_COS9:23, XBOOLE_1:1;
A4: 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 A1, XXREAL_1:1;
then arctan x = - (arctan (- x)) by SIN_COS9:67;
hence arctan . (- x) = - (arctan . x) ; :: thesis: verum

end;

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 that
A5: x in dom (arctan | A) and
A6: - x in dom (arctan | A) ; :: thesis: (arctan | A) . (- x) = - ((arctan | A) . x)
reconsider x = x as Element of REAL by XREAL_0:def 1;
(arctan | A) . (- x) = (arctan | A) /. (- x) by A6, PARTFUN1:def 6
.= arctan /. (- x) by A2, A3, A6, PARTFUN2:17
.= arctan . (- x) by A2, A6, PARTFUN1:def 6
.= - (arctan . x) by A4, A5
.= - (arctan /. x) by A2, A5, PARTFUN1:def 6
.= - ((arctan | A) /. x) by A2, A3, A5, PARTFUN2:17
.= - ((arctan | A) . x) by A5, PARTFUN1:def 6 ;
hence (arctan | A) . (- x) = - ((arctan | A) . x) ; :: thesis: verum

end;

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