let A be symmetrical Subset of COMPLEX; :: thesis: ( A c= dom cot implies cot is_odd_on A )

assume A1: A c= dom cot ; :: thesis: cot is_odd_on A

A2: dom (cot | A) = A by A1, RELAT_1:62;

A3: for x being Real st x in A holds

cot . (- x) = - (cot . x)

(cot | A) . (- x) = - ((cot | A) . x)

hence cot is_odd_on A by A1; :: thesis: verum

assume A1: A c= dom cot ; :: thesis: cot is_odd_on A

A2: dom (cot | A) = A by A1, RELAT_1:62;

A3: for x being Real st x in A holds

cot . (- x) = - (cot . x)

proof

for x being Real st x in dom (cot | A) & - x in dom (cot | A) holds
let x be Real; :: thesis: ( x in A implies cot . (- x) = - (cot . x) )

assume A4: x in A ; :: thesis: cot . (- x) = - (cot . x)

then A5: sin . x <> 0 by A1, FDIFF_8:2;

- x in A by A4, Def1;

then cot . (- x) = cot (- x) by A1, FDIFF_8:2, SIN_COS9:16

.= - (cot x) by SIN_COS4:3

.= - (cot . x) by A5, SIN_COS9:16 ;

hence cot . (- x) = - (cot . x) ; :: thesis: verum

end;assume A4: x in A ; :: thesis: cot . (- x) = - (cot . x)

then A5: sin . x <> 0 by A1, FDIFF_8:2;

- x in A by A4, Def1;

then cot . (- x) = cot (- x) by A1, FDIFF_8:2, SIN_COS9:16

.= - (cot x) by SIN_COS4:3

.= - (cot . x) by A5, SIN_COS9:16 ;

hence cot . (- x) = - (cot . x) ; :: thesis: verum

(cot | A) . (- x) = - ((cot | A) . x)

proof

then
( cot | A is with_symmetrical_domain & cot | A is quasi_odd )
by A2;
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)

reconsider x = x as Element of REAL by XREAL_0:def 1;

(cot | A) . (- x) = (cot | A) /. (- x) by A7, PARTFUN1:def 6

.= cot /. (- x) by A1, A2, A7, PARTFUN2:17

.= cot . (- x) by A1, A7, PARTFUN1:def 6

.= - (cot . x) by A3, A6

.= - (cot /. x) by A1, A6, PARTFUN1:def 6

.= - ((cot | A) /. x) by A1, A2, A6, PARTFUN2:17

.= - ((cot | A) . x) by A6, PARTFUN1:def 6 ;

hence (cot | A) . (- x) = - ((cot | A) . x) ; :: thesis: verum

end;assume that

A6: x in dom (cot | A) and

A7: - x in dom (cot | A) ; :: thesis: (cot | A) . (- x) = - ((cot | A) . x)

reconsider x = x as Element of REAL by XREAL_0:def 1;

(cot | A) . (- x) = (cot | A) /. (- x) by A7, PARTFUN1:def 6

.= cot /. (- x) by A1, A2, A7, PARTFUN2:17

.= cot . (- x) by A1, A7, PARTFUN1:def 6

.= - (cot . x) by A3, A6

.= - (cot /. x) by A1, A6, PARTFUN1:def 6

.= - ((cot | A) /. x) by A1, A2, A6, PARTFUN2:17

.= - ((cot | A) . x) by A6, PARTFUN1:def 6 ;

hence (cot | A) . (- x) = - ((cot | A) . x) ; :: thesis: verum

hence cot is_odd_on A by A1; :: thesis: verum