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

proof

let x be real number ; :: thesis: ( x in dom tan implies ( x + PI in dom tan & x - PI in dom tan & tan . x = tan . (x + PI ) ) )
assume A1: x in dom tan ; :: thesis: ( x + PI in dom tan & x - PI in dom tan & tan . x = tan . (x + PI ) )
then x in (dom sin ) /\ ((dom cos ) \ (cos " {0 })) by RFUNCT_1:def 4;
then ( x in dom sin & x in (dom cos ) \ (cos " {0 }) ) by XBOOLE_0:def 4;
then ( x in dom sin & x in dom cos & not x in cos " {0 } ) by XBOOLE_0:def 5;
then not cos . x in {0 } by FUNCT_1:def 13;
then B1: cos . x <> 0 by TARSKI:def 1;
B2: cos . (x + PI ) = - (cos . x) by SIN_COS:83;
then not cos . (x + PI ) in {0 } by TARSKI:def 1, B1;
then ( x + PI in dom sin & x + PI in dom cos & not x + PI in cos " {0 } ) by FUNCT_1:def 13, SIN_COS:27;
then ( x + PI in dom sin & x + PI in (dom cos ) \ (cos " {0 }) ) by XBOOLE_0:def 5;
then A3: x + PI in (dom sin ) /\ ((dom cos ) \ (cos " {0 })) by XBOOLE_0:def 4;
cos . (x - PI ) = cos . ((x - PI ) + (2 * PI )) by SIN_COS:83
.= cos . (x + PI ) ;
then not cos . (x - PI ) in {0 } by B1, B2, TARSKI:def 1;
then ( x - PI in dom sin & x - PI in dom cos & not x - PI in cos " {0 } ) by FUNCT_1:def 13, SIN_COS:27;
then ( x - PI in dom sin & x - PI in (dom cos ) \ (cos " {0 }) ) by XBOOLE_0:def 5;
then A4: x - PI in (dom sin ) /\ ((dom cos ) \ (cos " {0 })) by XBOOLE_0:def 4;
then A5: ( x + PI in dom tan & x - PI in dom tan ) by A3, RFUNCT_1:def 4;
tan . (x + PI ) = (sin . (x + PI )) / (cos . (x + PI )) by A5, RFUNCT_1:def 4
.= (- (sin . x)) / (cos . (x + PI )) by SIN_COS:83
.= (- (sin . x)) / (- (cos . x)) by SIN_COS:83
.= (sin . x) / (cos . x) by XCMPLX_1:192
.= tan . x by A1, RFUNCT_1:def 4 ;
hence ( x + PI in dom tan & x - PI in dom tan & tan . x = tan . (x + PI ) ) by A3, A4, RFUNCT_1:def 4; :: thesis: verum

end;

hence tan is PI -periodic by Th1; :: thesis: verum