let B be symmetrical Subset of REAL; :: thesis: ( ( for x being Real st x in B holds

sin . x <> 0 ) implies cosec is_odd_on B )

assume A1: for x being Real st x in B holds

sin . x <> 0 ; :: thesis: cosec is_odd_on B

B c= dom cosec

sin . x <> 0 ) implies cosec is_odd_on B )

assume A1: for x being Real st x in B holds

sin . x <> 0 ; :: thesis: cosec is_odd_on B

B c= dom cosec

proof

hence
cosec is_odd_on B
by Th83; :: thesis: verum
let x be Real; :: according to MEMBERED:def 9 :: thesis: ( not x in B or x in dom cosec )

assume A2: x in B ; :: thesis: x in dom cosec

then sin . x <> 0 by A1;

then not sin . x in {0} by TARSKI:def 1;

then not x in sin " {0} by FUNCT_1:def 7;

then x in (dom sin) \ (sin " {0}) by A2, SIN_COS:24, XBOOLE_0:def 5;

hence x in dom cosec by RFUNCT_1:def 2; :: thesis: verum

end;assume A2: x in B ; :: thesis: x in dom cosec

then sin . x <> 0 by A1;

then not sin . x in {0} by TARSKI:def 1;

then not x in sin " {0} by FUNCT_1:def 7;

then x in (dom sin) \ (sin " {0}) by A2, SIN_COS:24, XBOOLE_0:def 5;

hence x in dom cosec by RFUNCT_1:def 2; :: thesis: verum