let B be symmetrical Subset of REAL; ( B c= dom cosec implies cosec is_odd_on B )
assume A1:
B c= dom cosec
; 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)
for x being Real st x in dom (cosec | B) & - x in dom (cosec | B) holds
(cosec | B) . (- x) = - ((cosec | B) . x)
proof
let x be
Real;
( 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)
;
(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)
;
verum
end;
then
( cosec | B is with_symmetrical_domain & cosec | B is quasi_odd )
by A2;
hence
cosec is_odd_on B
by A1; verum