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)) )
proof
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 () \ () by RFUNCT_1:def 2;
then ( x in dom sin & not x in sin " ) by XBOOLE_0:def 5;
then A2: not sin . x in 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 by TARSKI:def 1;
then ( x + (2 * PI) in dom sin & not x + (2 * PI) in sin " ) by ;
then A3: x + (2 * PI) in () \ () by XBOOLE_0:def 5;
x - (2 * PI) in dom sin by ;
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 " ) by ;
then A4: x - (2 * PI) in () \ () by XBOOLE_0:def 5;
then ( x + (2 * PI) in dom cosec & x - (2 * PI) in dom cosec ) by ;
then cosec . (x + (2 * PI)) = (sin . (x + (2 * PI))) " by RFUNCT_1:def 2
.= (sin . x) " by SIN_COS:78
.= cosec . x by ;
hence ( x + (2 * PI) in dom cosec & x - (2 * PI) in dom cosec & cosec . x = cosec . (x + (2 * PI)) ) by ; :: thesis: verum
end;
hence cosec is 2 * PI -periodic by Th1; :: thesis: verum