for x being real number st x in dom cosec holds
( x + (2 * PI ) in dom cosec & x - (2 * PI ) in dom cosec & cosec . x = cosec . (x + (2 * PI )) )

proof

let x be real number ; :: thesis: ( x in dom cosec implies ( x + (2 * PI ) in dom cosec & x - (2 * PI ) in dom cosec & cosec . x = cosec . (x + (2 * PI )) ) )
assume A1: x in dom cosec ; :: thesis: ( x + (2 * PI ) in dom cosec & x - (2 * PI ) in dom cosec & cosec . x = cosec . (x + (2 * PI )) )
then x in (dom sin ) \ (sin " {0 }) by RFUNCT_1:def 8;
then ( x in dom sin & not x in sin " {0 } ) by XBOOLE_0:def 5;
then A2: not sin . x in {0 } by FUNCT_1:def 13;
then sin . x <> 0 by TARSKI:def 1;
then sin . (x + (2 * PI )) <> 0 by SIN_COS:83;
then not sin . (x + (2 * PI )) in {0 } by TARSKI:def 1;
then ( x + (2 * PI ) in dom sin & not x + (2 * PI ) in sin " {0 } ) by FUNCT_1:def 13, SIN_COS:27;
then A3: x + (2 * PI ) in (dom sin ) \ (sin " {0 }) by XBOOLE_0:def 5;
sin . (x - (2 * PI )) = sin . ((x - (2 * PI )) + (2 * PI )) by L1, Th1, SIN_COS:27;
then ( x - (2 * PI ) in dom sin & not x - (2 * PI ) in sin " {0 } ) by A2, FUNCT_1:def 13, SIN_COS:27;
then A4: x - (2 * PI ) in (dom sin ) \ (sin " {0 }) by XBOOLE_0:def 5;
then A5: ( x + (2 * PI ) in dom cosec & x - (2 * PI ) in dom cosec ) by A3, RFUNCT_1:def 8;
cosec . (x + (2 * PI )) = (sin . (x + (2 * PI ))) " by A5, RFUNCT_1:def 8
.= (sin . x) " by SIN_COS:83
.= cosec . x by A1, RFUNCT_1:def 8 ;
hence ( x + (2 * PI ) in dom cosec & x - (2 * PI ) in dom cosec & cosec . x = cosec . (x + (2 * PI )) ) by A3, A4, RFUNCT_1:def 8; :: thesis: verum

end;

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