let A be symmetrical Subset of COMPLEX ; :: thesis: ( A c= dom cot & ( for x being Real st x in A holds
sin . x <> 0 ) implies cot is_odd_on A )
assume that
A1: A c= dom cot and
A2: for x being Real st x in A holds
sin . x <> 0 ; :: thesis: cot is_odd_on A
A3: dom (cot | A) = A by A1, RELAT_1:91;
A4: for x being Real st x in A holds
cot . (- x) = - (cot . x)

proof

let x be Real; :: thesis: ( x in A implies cot . (- x) = - (cot . x) )
assume A5: x in A ; :: thesis: cot . (- x) = - (cot . x)
then - x in A by Def1;
then cot . (- x) = cot (- x) by A2, SIN_COS9:16
.= - (cot x) by SIN_COS4:4
.= - (cot . x) by A2, A5, SIN_COS9:16 ;
hence cot . (- x) = - (cot . x) ; :: thesis: verum

end;

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

proof

let x be Real; :: thesis: ( x in dom (cot | A) & - x in dom (cot | A) implies (cot | A) . (- x) = - ((cot | A) . x) )
assume that
A6: x in dom (cot | A) and
A7: - x in dom (cot | A) ; :: thesis: (cot | A) . (- x) = - ((cot | A) . x)
(cot | A) . (- x) = (cot | A) /. (- x) by A7, PARTFUN1:def 8
.= cot /. (- x) by A1, A3, A7, PARTFUN2:35
.= cot . (- x) by A1, A3, A7, PARTFUN1:def 8
.= - (cot . x) by A4, A3, A6
.= - (cot /. x) by A1, A3, A6, PARTFUN1:def 8
.= - ((cot | A) /. x) by A1, A3, A6, PARTFUN2:35
.= - ((cot | A) . x) by A6, PARTFUN1:def 8 ;
hence (cot | A) . (- x) = - ((cot | A) . x) ; :: thesis: verum

end;

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