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

proof

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;

hence sec is_even_on B by Th81; :: thesis: verum