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
proof
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;
hence cosec is_odd_on B by Th83; :: thesis: verum