for x being Real st x in dom sec holds
( x + (2 * PI) in dom sec & x - (2 * PI) in dom sec & sec . x = sec . (x + (2 * PI)) )
proof
let x be
Real;
( x in dom sec implies ( x + (2 * PI) in dom sec & x - (2 * PI) in dom sec & sec . x = sec . (x + (2 * PI)) ) )
assume A1:
x in dom sec
;
( x + (2 * PI) in dom sec & x - (2 * PI) in dom sec & sec . x = sec . (x + (2 * PI)) )
then
x in (dom cos) \ (cos " {0})
by RFUNCT_1:def 2;
then
(
x in dom cos & not
x in cos " {0} )
by XBOOLE_0:def 5;
then A2:
not
cos . x in {0}
by FUNCT_1:def 7;
then
cos . x <> 0
by TARSKI:def 1;
then
cos . (x + (2 * PI)) <> 0
by SIN_COS:78;
then
not
cos . (x + (2 * PI)) in {0}
by TARSKI:def 1;
then
(
x + (2 * PI) in dom cos & not
x + (2 * PI) in cos " {0} )
by FUNCT_1:def 7, SIN_COS:24, XREAL_0:def 1;
then A3:
x + (2 * PI) in (dom cos) \ (cos " {0})
by XBOOLE_0:def 5;
x - (2 * PI) in dom cos
by SIN_COS:24, XREAL_0:def 1;
then
cos . (x - (2 * PI)) = cos . ((x - (2 * PI)) + (2 * PI))
by Lm3;
then
(
x - (2 * PI) in dom cos & not
x - (2 * PI) in cos " {0} )
by A2, FUNCT_1:def 7, SIN_COS:24, XREAL_0:def 1;
then A4:
x - (2 * PI) in (dom cos) \ (cos " {0})
by XBOOLE_0:def 5;
then
(
x + (2 * PI) in dom sec &
x - (2 * PI) in dom sec )
by A3, RFUNCT_1:def 2;
then sec . (x + (2 * PI)) =
(cos . (x + (2 * PI))) "
by RFUNCT_1:def 2
.=
(cos . x) "
by SIN_COS:78
.=
sec . x
by A1, RFUNCT_1:def 2
;
hence
(
x + (2 * PI) in dom sec &
x - (2 * PI) in dom sec &
sec . x = sec . (x + (2 * PI)) )
by A3, A4, RFUNCT_1:def 2;
verum
end;
hence
sec is 2 * PI -periodic
by Th1; verum