for x being Real st x in dom cosec holds

( x + (2 * PI) in dom cosec & x - (2 * PI) in dom cosec & cosec . x = cosec . (x + (2 * PI)) )

( x + (2 * PI) in dom cosec & x - (2 * PI) in dom cosec & cosec . x = cosec . (x + (2 * PI)) )

proof

hence
cosec is 2 * PI -periodic
by Th1; :: thesis: verum
let x be Real; :: 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 2;

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 7;

then sin . x <> 0 by TARSKI:def 1;

then sin . (x + (2 * PI)) <> 0 by SIN_COS:78;

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 7, SIN_COS:24, XREAL_0:def 1;

then A3: x + (2 * PI) in (dom sin) \ (sin " {0}) by XBOOLE_0:def 5;

x - (2 * PI) in dom sin by SIN_COS:24, XREAL_0:def 1;

then sin . (x - (2 * PI)) = sin . ((x - (2 * PI)) + (2 * PI)) by Lm2;

then ( x - (2 * PI) in dom sin & not x - (2 * PI) in sin " {0} ) by A2, FUNCT_1:def 7, SIN_COS:24, XREAL_0:def 1;

then A4: x - (2 * PI) in (dom sin) \ (sin " {0}) by XBOOLE_0:def 5;

then ( x + (2 * PI) in dom cosec & x - (2 * PI) in dom cosec ) by A3, RFUNCT_1:def 2;

then cosec . (x + (2 * PI)) = (sin . (x + (2 * PI))) " by RFUNCT_1:def 2

.= (sin . x) " by SIN_COS:78

.= cosec . x by A1, RFUNCT_1:def 2 ;

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

end;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 2;

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 7;

then sin . x <> 0 by TARSKI:def 1;

then sin . (x + (2 * PI)) <> 0 by SIN_COS:78;

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 7, SIN_COS:24, XREAL_0:def 1;

then A3: x + (2 * PI) in (dom sin) \ (sin " {0}) by XBOOLE_0:def 5;

x - (2 * PI) in dom sin by SIN_COS:24, XREAL_0:def 1;

then sin . (x - (2 * PI)) = sin . ((x - (2 * PI)) + (2 * PI)) by Lm2;

then ( x - (2 * PI) in dom sin & not x - (2 * PI) in sin " {0} ) by A2, FUNCT_1:def 7, SIN_COS:24, XREAL_0:def 1;

then A4: x - (2 * PI) in (dom sin) \ (sin " {0}) by XBOOLE_0:def 5;

then ( x + (2 * PI) in dom cosec & x - (2 * PI) in dom cosec ) by A3, RFUNCT_1:def 2;

then cosec . (x + (2 * PI)) = (sin . (x + (2 * PI))) " by RFUNCT_1:def 2

.= (sin . x) " by SIN_COS:78

.= cosec . x by A1, RFUNCT_1:def 2 ;

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