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

cos . x <> 0 ) implies sec is_even_on B )

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

cos . x <> 0 ; :: thesis: sec is_even_on B

B c= dom sec

cos . x <> 0 ) implies sec is_even_on B )

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

cos . x <> 0 ; :: thesis: sec is_even_on B

B c= dom sec

proof

hence
sec is_even_on B
by Th81; :: thesis: verum
let x be Real; :: according to MEMBERED:def 9 :: thesis: ( not x in B or x in dom sec )

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

then cos . x <> 0 by A1;

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

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

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

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

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

then cos . x <> 0 by A1;

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

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

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

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