let B be symmetrical Subset of REAL; :: thesis: ( B c= dom cosec implies cosec is_odd_on B )

assume A1: B c= dom cosec ; :: thesis: cosec is_odd_on B

then A2: dom (cosec | B) = B by RELAT_1:62;

A3: for x being Real st x in B holds

cosec . (- x) = - (cosec . x)

(cosec | B) . (- x) = - ((cosec | B) . x)

hence cosec is_odd_on B by A1; :: thesis: verum

assume A1: B c= dom cosec ; :: thesis: cosec is_odd_on B

then A2: dom (cosec | B) = B by RELAT_1:62;

A3: for x being Real st x in B holds

cosec . (- x) = - (cosec . x)

proof

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

assume A4: x in B ; :: thesis: cosec . (- x) = - (cosec . x)

then - x in B by Def1;

then cosec . (- x) = (sin . (- x)) " by A1, RFUNCT_1:def 2

.= (- (sin . x)) " by SIN_COS:30

.= - ((sin . x) ") by XCMPLX_1:222

.= - (cosec . x) by A1, A4, RFUNCT_1:def 2 ;

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

end;assume A4: x in B ; :: thesis: cosec . (- x) = - (cosec . x)

then - x in B by Def1;

then cosec . (- x) = (sin . (- x)) " by A1, RFUNCT_1:def 2

.= (- (sin . x)) " by SIN_COS:30

.= - ((sin . x) ") by XCMPLX_1:222

.= - (cosec . x) by A1, A4, RFUNCT_1:def 2 ;

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

(cosec | B) . (- x) = - ((cosec | B) . x)

proof

then
( cosec | B is with_symmetrical_domain & cosec | B is quasi_odd )
by A2;
let x be Real; :: thesis: ( x in dom (cosec | B) & - x in dom (cosec | B) implies (cosec | B) . (- x) = - ((cosec | B) . x) )

assume that

A5: x in dom (cosec | B) and

A6: - x in dom (cosec | B) ; :: thesis: (cosec | B) . (- x) = - ((cosec | B) . x)

(cosec | B) . (- x) = (cosec | B) /. (- x) by A6, PARTFUN1:def 6

.= cosec /. (- x) by A1, A2, A6, PARTFUN2:17

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

.= - (cosec . x) by A3, A5

.= - (cosec /. x) by A1, A5, PARTFUN1:def 6

.= - ((cosec | B) /. x) by A1, A2, A5, PARTFUN2:17

.= - ((cosec | B) . x) by A5, PARTFUN1:def 6 ;

hence (cosec | B) . (- x) = - ((cosec | B) . x) ; :: thesis: verum

end;assume that

A5: x in dom (cosec | B) and

A6: - x in dom (cosec | B) ; :: thesis: (cosec | B) . (- x) = - ((cosec | B) . x)

(cosec | B) . (- x) = (cosec | B) /. (- x) by A6, PARTFUN1:def 6

.= cosec /. (- x) by A1, A2, A6, PARTFUN2:17

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

.= - (cosec . x) by A3, A5

.= - (cosec /. x) by A1, A5, PARTFUN1:def 6

.= - ((cosec | B) /. x) by A1, A2, A5, PARTFUN2:17

.= - ((cosec | B) . x) by A5, PARTFUN1:def 6 ;

hence (cosec | B) . (- x) = - ((cosec | B) . x) ; :: thesis: verum

hence cosec is_odd_on B by A1; :: thesis: verum