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; :: thesis: ( 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 ; :: thesis: ( 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; :: thesis: verum

end;

hence sec is 2 * PI -periodic by Th1; :: thesis: verum