:: FUNCT_9 semantic presentation

begin


definition
let t be real number ;
let F be Function;
attrF is t -periodic  means :Def1: :: FUNCT_9:def 1
( t <> 0 & ( for x being real number holds
( ( x in dom F implies x + t in dom F ) & ( x + t in dom F implies x in dom F ) & ( x in dom F implies F . x = F . (x + t) ) ) ) );
end;

:: deftheorem Def1 defines -periodic FUNCT_9:def_1_:_
 for t being real number
for F being Function holds
( F is t -periodic iff ( t <> 0 & ( for x being real number holds
( ( x in dom F implies x + t in dom F ) & ( x + t in dom F implies x in dom F ) & ( x in dom F implies F . x = F . (x + t) ) ) ) ) );

definition
let F be Function;
attrF is periodic  means :Def2: :: FUNCT_9:def 2
 ex t being real number st F is t -periodic ;
end;

:: deftheorem Def2 defines periodic FUNCT_9:def_2_:_
 for F being Function holds
( F is periodic iff ex t being real number st F is t -periodic );

theorem Th1: :: FUNCT_9:1
for t being real number
for F being real-valued Function holds
( F is t -periodic iff ( t <> 0 & ( for x being real number st x in dom F holds
( x + t in dom F & x - t in dom F & F . x = F . (x + t) ) ) ) )
proof
let t be real number ; ::_thesis: for F being real-valued Function holds
( F is t -periodic iff ( t <> 0 & ( for x being real number st x in dom F holds
( x + t in dom F & x - t in dom F & F . x = F . (x + t) ) ) ) )
let F be real-valued Function; ::_thesis: ( F is t -periodic iff ( t <> 0 & ( for x being real number st x in dom F holds
( x + t in dom F & x - t in dom F & F . x = F . (x + t) ) ) ) )
thus  ( F is t -periodic implies ( t <> 0 & ( for x being real number st x in dom F holds
( x + t in dom F & x - t in dom F & F . x = F . (x + t) ) ) ) ) ::_thesis: ( t <> 0 & ( for x being real number st x in dom F holds
( x + t in dom F & x - t in dom F & F . x = F . (x + t) ) ) implies F is t -periodic )
proof
assume A1: F is t -periodic ; ::_thesis: ( t <> 0 & ( for x being real number st x in dom F holds
( x + t in dom F & x - t in dom F & F . x = F . (x + t) ) ) )
 for x being real number st x in dom F holds
( x + t in dom F & x - t in dom F & F . x = F . (x + t) )
proof
let x be real number ; ::_thesis: ( x in dom F implies ( x + t in dom F & x - t in dom F & F . x = F . (x + t) ) )
assume  x in dom F ; ::_thesis: ( x + t in dom F & x - t in dom F & F . x = F . (x + t) )
then  (x - t) + t in dom F ;
hence  ( x + t in dom F & x - t in dom F & F . x = F . (x + t) ) by A1, Def1; ::_thesis: verum
end;
hence  ( t <> 0 & ( for x being real number st x in dom F holds
( x + t in dom F & x - t in dom F & F . x = F . (x + t) ) ) ) by A1, Def1; ::_thesis: verum
end;
assume A2: ( t <> 0 & ( for x being real number st x in dom F holds
( x + t in dom F & x - t in dom F & F . x = F . (x + t) ) ) ) ; ::_thesis: F is t -periodic
 for x being real number holds
( ( x in dom F implies x + t in dom F ) & ( x + t in dom F implies x in dom F ) & ( x in dom F implies F . x = F . (x + t) ) )
proof
let x be real number ; ::_thesis: ( ( x in dom F implies x + t in dom F ) & ( x + t in dom F implies x in dom F ) & ( x in dom F implies F . x = F . (x + t) ) )
 ( x in dom F iff x + t in dom F )
proof
 ( x + t in dom F implies x in dom F )
proof
assume  x + t in dom F ; ::_thesis: x in dom F
then  (x + t) - t in dom F by A2;
hence  x in dom F ; ::_thesis: verum
end;
hence  ( x in dom F iff x + t in dom F ) by A2; ::_thesis: verum
end;
hence  ( ( x in dom F implies x + t in dom F ) & ( x + t in dom F implies x in dom F ) & ( x in dom F implies F . x = F . (x + t) ) ) by A2; ::_thesis: verum
end;
hence  F is t -periodic by A2, Def1; ::_thesis: verum
end;

theorem Th2: :: FUNCT_9:2
for t being real number
for F, G being real-valued Function st F is t -periodic & G is t -periodic holds
F + G is t -periodic
proof
let t be real number ; ::_thesis: for F, G being real-valued Function st F is t -periodic & G is t -periodic holds
F + G is t -periodic
let F, G be real-valued Function; ::_thesis: ( F is t -periodic & G is t -periodic implies F + G is t -periodic )
assume that
A1: F is t -periodic and
A2: G is t -periodic ; ::_thesis: F + G is t -periodic
A3: ( t <> 0 & ( for x being real number st x in dom F holds
( x + t in dom F & x - t in dom F & F . x = F . (x + t) ) ) ) by A1, Th1;
 for x being real number st x in dom (F + G) holds
( x + t in dom (F + G) & x - t in dom (F + G) & (F + G) . x = (F + G) . (x + t) )
proof
let x be real number ; ::_thesis: ( x in dom (F + G) implies ( x + t in dom (F + G) & x - t in dom (F + G) & (F + G) . x = (F + G) . (x + t) ) )
assume A4: x in dom (F + G) ; ::_thesis: ( x + t in dom (F + G) & x - t in dom (F + G) & (F + G) . x = (F + G) . (x + t) )
then A5: x in (dom F) /\ (dom G) by VALUED_1:def_1;
A6: ( (dom F) /\ (dom G) c= dom F & (dom F) /\ (dom G) c= dom G ) by XBOOLE_1:17;
then A7: ( x + t in dom F & x - t in dom F ) by A1, Th1, A5;
 ( x + t in dom G & x - t in dom G ) by A2, Th1, A5, A6;
then A8: ( x + t in (dom F) /\ (dom G) & x - t in (dom F) /\ (dom G) ) by A7, XBOOLE_0:def_4;
then A9: ( x + t in dom (F + G) & x - t in dom (F + G) ) by VALUED_1:def_1;
(F + G) . x = (F . x) + (G . x) by A4, VALUED_1:def_1
.= (F . (x + t)) + (G . x) by A1, Th1, A5, A6
.= (F . (x + t)) + (G . (x + t)) by A2, Th1, A5, A6
.= (F + G) . (x + t) by A9, VALUED_1:def_1 ;
hence  ( x + t in dom (F + G) & x - t in dom (F + G) & (F + G) . x = (F + G) . (x + t) ) by A8, VALUED_1:def_1; ::_thesis: verum
end;
hence  F + G is t -periodic by A3, Th1; ::_thesis: verum
end;

Lm1:  for t, a being real number st t <> 0 holds
REAL --> a is t -periodic
proof
let t, a be real number ; ::_thesis: ( t <> 0 implies REAL --> a is t -periodic )
set F = REAL --> a;
assume  t <> 0 ; ::_thesis: REAL --> a is t -periodic
hence  t <> 0 ; :: according to FUNCT_9:def_1 ::_thesis: for x being real number holds
( ( x in dom (REAL --> a) implies x + t in dom (REAL --> a) ) & ( x + t in dom (REAL --> a) implies x in dom (REAL --> a) ) & ( x in dom (REAL --> a) implies (REAL --> a) . x = (REAL --> a) . (x + t) ) )
let x be real number ; ::_thesis: ( ( x in dom (REAL --> a) implies x + t in dom (REAL --> a) ) & ( x + t in dom (REAL --> a) implies x in dom (REAL --> a) ) & ( x in dom (REAL --> a) implies (REAL --> a) . x = (REAL --> a) . (x + t) ) )
A1: ( x in REAL & x + t in REAL ) by XREAL_0:def_1;
hence  ( x in dom (REAL --> a) iff x + t in dom (REAL --> a) ) by FUNCOP_1:13; ::_thesis: ( x in dom (REAL --> a) implies (REAL --> a) . x = (REAL --> a) . (x + t) )
assume  x in dom (REAL --> a) ; ::_thesis: (REAL --> a) . x = (REAL --> a) . (x + t)
thus (REAL --> a) . x = a by A1, FUNCOP_1:7
.= (REAL --> a) . (x + t) by A1, FUNCOP_1:7 ; ::_thesis: verum
end;

theorem Th3: :: FUNCT_9:3
for t being real number
for F, G being real-valued Function st F is t -periodic & G is t -periodic holds
F - G is t -periodic
proof
let t be real number ; ::_thesis: for F, G being real-valued Function st F is t -periodic & G is t -periodic holds
F - G is t -periodic
let F, G be real-valued Function; ::_thesis: ( F is t -periodic & G is t -periodic implies F - G is t -periodic )
assume that
A1: F is t -periodic and
A2: G is t -periodic ; ::_thesis: F - G is t -periodic
A3: ( t <> 0 & ( for x being real number st x in dom F holds
( x + t in dom F & x - t in dom F & F . x = F . (x + t) ) ) ) by A1, Th1;
 for x being real number st x in dom (F - G) holds
( x + t in dom (F - G) & x - t in dom (F - G) & (F - G) . x = (F - G) . (x + t) )
proof
let x be real number ; ::_thesis: ( x in dom (F - G) implies ( x + t in dom (F - G) & x - t in dom (F - G) & (F - G) . x = (F - G) . (x + t) ) )
assume A4: x in dom (F - G) ; ::_thesis: ( x + t in dom (F - G) & x - t in dom (F - G) & (F - G) . x = (F - G) . (x + t) )
then A5: x in (dom F) /\ (dom G) by VALUED_1:12;
A6: ( (dom F) /\ (dom G) c= dom F & (dom F) /\ (dom G) c= dom G ) by XBOOLE_1:17;
then A7: ( x + t in dom F & x - t in dom F ) by A1, A5, Th1;
 ( x + t in dom G & x - t in dom G ) by A2, Th1, A5, A6;
then A8: ( x + t in (dom F) /\ (dom G) & x - t in (dom F) /\ (dom G) ) by A7, XBOOLE_0:def_4;
then A9: ( x + t in dom (F - G) & x - t in dom (F - G) ) by VALUED_1:12;
(F - G) . x = (F . x) - (G . x) by A4, VALUED_1:13
.= (F . (x + t)) - (G . x) by A1, Th1, A5, A6
.= (F . (x + t)) - (G . (x + t)) by A2, Th1, A5, A6
.= (F - G) . (x + t) by A9, VALUED_1:13 ;
hence  ( x + t in dom (F - G) & x - t in dom (F - G) & (F - G) . x = (F - G) . (x + t) ) by A8, VALUED_1:12; ::_thesis: verum
end;
hence  F - G is t -periodic by A3, Th1; ::_thesis: verum
end;

theorem Th4: :: FUNCT_9:4
for t being real number
for F, G being real-valued Function st F is t -periodic & G is t -periodic holds
F (#) G is t -periodic
proof
let t be real number ; ::_thesis: for F, G being real-valued Function st F is t -periodic & G is t -periodic holds
F (#) G is t -periodic
let F, G be real-valued Function; ::_thesis: ( F is t -periodic & G is t -periodic implies F (#) G is t -periodic )
assume that
A1: F is t -periodic and
A2: G is t -periodic ; ::_thesis: F (#) G is t -periodic
A3: ( t <> 0 & ( for x being real number st x in dom F holds
( x + t in dom F & x - t in dom F & F . x = F . (x + t) ) ) ) by A1, Th1;
 for x being real number st x in dom (F (#) G) holds
( x + t in dom (F (#) G) & x - t in dom (F (#) G) & (F (#) G) . x = (F (#) G) . (x + t) )
proof
let x be real number ; ::_thesis: ( x in dom (F (#) G) implies ( x + t in dom (F (#) G) & x - t in dom (F (#) G) & (F (#) G) . x = (F (#) G) . (x + t) ) )
assume A4: x in dom (F (#) G) ; ::_thesis: ( x + t in dom (F (#) G) & x - t in dom (F (#) G) & (F (#) G) . x = (F (#) G) . (x + t) )
then A5: x in (dom F) /\ (dom G) by VALUED_1:def_4;
A6: ( (dom F) /\ (dom G) c= dom F & (dom F) /\ (dom G) c= dom G ) by XBOOLE_1:17;
then A7: ( x + t in dom F & x - t in dom F ) by A1, Th1, A5;
 ( x + t in dom G & x - t in dom G ) by A2, Th1, A5, A6;
then A8: ( x + t in (dom F) /\ (dom G) & x - t in (dom F) /\ (dom G) ) by A7, XBOOLE_0:def_4;
then A9: ( x + t in dom (F (#) G) & x - t in dom (F (#) G) ) by VALUED_1:def_4;
(F (#) G) . x = (F . x) * (G . x) by A4, VALUED_1:def_4
.= (F . (x + t)) * (G . x) by A1, Th1, A5, A6
.= (F . (x + t)) * (G . (x + t)) by A2, Th1, A5, A6
.= (F (#) G) . (x + t) by A9, VALUED_1:def_4 ;
hence  ( x + t in dom (F (#) G) & x - t in dom (F (#) G) & (F (#) G) . x = (F (#) G) . (x + t) ) by A8, VALUED_1:def_4; ::_thesis: verum
end;
hence  F (#) G is t -periodic by A3, Th1; ::_thesis: verum
end;

theorem Th5: :: FUNCT_9:5
for t being real number
for F, G being real-valued Function st F is t -periodic & G is t -periodic holds
F /" G is t -periodic
proof
let t be real number ; ::_thesis: for F, G being real-valued Function st F is t -periodic & G is t -periodic holds
F /" G is t -periodic
let F, G be real-valued Function; ::_thesis: ( F is t -periodic & G is t -periodic implies F /" G is t -periodic )
assume that
A1: F is t -periodic and
A2: G is t -periodic ; ::_thesis: F /" G is t -periodic
A3: ( t <> 0 & ( for x being real number st x in dom F holds
( x + t in dom F & x - t in dom F & F . x = F . (x + t) ) ) ) by A1, Th1;
 for x being real number st x in dom (F /" G) holds
( x + t in dom (F /" G) & x - t in dom (F /" G) & (F /" G) . x = (F /" G) . (x + t) )
proof
let x be real number ; ::_thesis: ( x in dom (F /" G) implies ( x + t in dom (F /" G) & x - t in dom (F /" G) & (F /" G) . x = (F /" G) . (x + t) ) )
assume  x in dom (F /" G) ; ::_thesis: ( x + t in dom (F /" G) & x - t in dom (F /" G) & (F /" G) . x = (F /" G) . (x + t) )
then A4: x in (dom F) /\ (dom G) by VALUED_1:16;
A5: ( (dom F) /\ (dom G) c= dom F & (dom F) /\ (dom G) c= dom G ) by XBOOLE_1:17;
then A6: ( x + t in dom F & x - t in dom F ) by A1, Th1, A4;
 ( x + t in dom G & x - t in dom G ) by A2, Th1, A4, A5;
then A7: ( x + t in (dom F) /\ (dom G) & x - t in (dom F) /\ (dom G) ) by A6, XBOOLE_0:def_4;
(F /" G) . x = (F . x) / (G . x) by VALUED_1:17
.= (F . (x + t)) / (G . x) by A1, Th1, A4, A5
.= (F . (x + t)) / (G . (x + t)) by A2, Th1, A4, A5
.= (F /" G) . (x + t) by VALUED_1:17 ;
hence  ( x + t in dom (F /" G) & x - t in dom (F /" G) & (F /" G) . x = (F /" G) . (x + t) ) by A7, VALUED_1:16; ::_thesis: verum
end;
hence  F /" G is t -periodic by A3, Th1; ::_thesis: verum
end;

theorem Th6: :: FUNCT_9:6
for t being real number
for F being real-valued Function st F is t -periodic holds
- F is t -periodic
proof
let t be real number ; ::_thesis: for F being real-valued Function st F is t -periodic holds
- F is t -periodic
let F be real-valued Function; ::_thesis: ( F is t -periodic implies - F is t -periodic )
assume A1: F is t -periodic ; ::_thesis: - F is t -periodic
then A2: ( t <> 0 & ( for x being real number st x in dom F holds
( x + t in dom F & x - t in dom F & F . x = F . (x + t) ) ) ) by Th1;
 for x being real number st x in dom (- F) holds
( x + t in dom (- F) & x - t in dom (- F) & (- F) . x = (- F) . (x + t) )
proof
let x be real number ; ::_thesis: ( x in dom (- F) implies ( x + t in dom (- F) & x - t in dom (- F) & (- F) . x = (- F) . (x + t) ) )
assume  x in dom (- F) ; ::_thesis: ( x + t in dom (- F) & x - t in dom (- F) & (- F) . x = (- F) . (x + t) )
then A3: x in dom F by VALUED_1:8;
then A4: ( x + t in dom F & x - t in dom F ) by A1, Th1;
(- F) . x = - (F . x) by VALUED_1:8
.= - (F . (x + t)) by A1, Th1, A3
.= (- F) . (x + t) by VALUED_1:8 ;
hence  ( x + t in dom (- F) & x - t in dom (- F) & (- F) . x = (- F) . (x + t) ) by A4, VALUED_1:8; ::_thesis: verum
end;
hence  - F is t -periodic by A2, Th1; ::_thesis: verum
end;

theorem Th7: :: FUNCT_9:7
for t, r being real number
for F being real-valued Function st F is t -periodic holds
r (#) F is t -periodic
proof
let t, r be real number ; ::_thesis: for F being real-valued Function st F is t -periodic holds
r (#) F is t -periodic
let F be real-valued Function; ::_thesis: ( F is t -periodic implies r (#) F is t -periodic )
assume A1: F is t -periodic ; ::_thesis: r (#) F is t -periodic
then A2: ( t <> 0 & ( for x being real number st x in dom F holds
( x + t in dom F & x - t in dom F & F . x = F . (x + t) ) ) ) by Th1;
 for x being real number st x in dom (r (#) F) holds
( x + t in dom (r (#) F) & x - t in dom (r (#) F) & (r (#) F) . x = (r (#) F) . (x + t) )
proof
let x be real number ; ::_thesis: ( x in dom (r (#) F) implies ( x + t in dom (r (#) F) & x - t in dom (r (#) F) & (r (#) F) . x = (r (#) F) . (x + t) ) )
assume A3: x in dom (r (#) F) ; ::_thesis: ( x + t in dom (r (#) F) & x - t in dom (r (#) F) & (r (#) F) . x = (r (#) F) . (x + t) )
then A4: x in dom F by VALUED_1:def_5;
then A5: ( x + t in dom F & x - t in dom F ) by A1, Th1;
then A6: ( x + t in dom (r (#) F) & x - t in dom (r (#) F) ) by VALUED_1:def_5;
(r (#) F) . x = r * (F . x) by A3, VALUED_1:def_5
.= r * (F . (x + t)) by A1, Th1, A4
.= (r (#) F) . (x + t) by A6, VALUED_1:def_5 ;
hence  ( x + t in dom (r (#) F) & x - t in dom (r (#) F) & (r (#) F) . x = (r (#) F) . (x + t) ) by A5, VALUED_1:def_5; ::_thesis: verum
end;
hence  r (#) F is t -periodic by A2, Th1; ::_thesis: verum
end;

theorem Th8: :: FUNCT_9:8
for t, r being real number
for F being real-valued Function st F is t -periodic holds
r + F is t -periodic
proof
let t, r be real number ; ::_thesis: for F being real-valued Function st F is t -periodic holds
r + F is t -periodic
let F be real-valued Function; ::_thesis: ( F is t -periodic implies r + F is t -periodic )
assume A1: F is t -periodic ; ::_thesis: r + F is t -periodic
then A2: ( t <> 0 & ( for x being real number st x in dom F holds
( x + t in dom F & x - t in dom F & F . x = F . (x + t) ) ) ) by Th1;
 for x being real number st x in dom (r + F) holds
( x + t in dom (r + F) & x - t in dom (r + F) & (r + F) . x = (r + F) . (x + t) )
proof
let x be real number ; ::_thesis: ( x in dom (r + F) implies ( x + t in dom (r + F) & x - t in dom (r + F) & (r + F) . x = (r + F) . (x + t) ) )
assume A3: x in dom (r + F) ; ::_thesis: ( x + t in dom (r + F) & x - t in dom (r + F) & (r + F) . x = (r + F) . (x + t) )
then A4: x in dom F by VALUED_1:def_2;
then A5: ( x + t in dom F & x - t in dom F ) by A1, Th1;
then A6: ( x + t in dom (r + F) & x - t in dom (r + F) ) by VALUED_1:def_2;
(r + F) . x = r + (F . x) by A3, VALUED_1:def_2
.= r + (F . (x + t)) by A1, Th1, A4
.= (r + F) . (x + t) by A6, VALUED_1:def_2 ;
hence  ( x + t in dom (r + F) & x - t in dom (r + F) & (r + F) . x = (r + F) . (x + t) ) by A5, VALUED_1:def_2; ::_thesis: verum
end;
hence  r + F is t -periodic by A2, Th1; ::_thesis: verum
end;

theorem :: FUNCT_9:9
for t, r being real number
for F being real-valued Function st F is t -periodic holds
F - r is t -periodic by Th8;

theorem Th10: :: FUNCT_9:10
for t being real number
for F being real-valued Function st F is t -periodic holds
|.F.| is t -periodic
proof
let t be real number ; ::_thesis: for F being real-valued Function st F is t -periodic holds
|.F.| is t -periodic
let F be real-valued Function; ::_thesis: ( F is t -periodic implies |.F.| is t -periodic )
assume A1: F is t -periodic ; ::_thesis: |.F.| is t -periodic
then A2: ( t <> 0 & ( for x being real number st x in dom F holds
( x + t in dom F & x - t in dom F & F . x = F . (x + t) ) ) ) by Th1;
 for x being real number st x in dom |.F.| holds
( x + t in dom |.F.| & x - t in dom |.F.| & |.F.| . x = |.F.| . (x + t) )
proof
let x be real number ; ::_thesis: ( x in dom |.F.| implies ( x + t in dom |.F.| & x - t in dom |.F.| & |.F.| . x = |.F.| . (x + t) ) )
assume A3: x in dom |.F.| ; ::_thesis: ( x + t in dom |.F.| & x - t in dom |.F.| & |.F.| . x = |.F.| . (x + t) )
then A4: x in dom F by VALUED_1:def_11;
then A5: ( x + t in dom F & x - t in dom F ) by A1, Th1;
then A6: ( x + t in dom |.F.| & x - t in dom |.F.| ) by VALUED_1:def_11;
|.F.| . x = |.(F . x).| by A3, VALUED_1:def_11
.= |.(F . (x + t)).| by A1, Th1, A4
.= |.F.| . (x + t) by A6, VALUED_1:def_11 ;
hence  ( x + t in dom |.F.| & x - t in dom |.F.| & |.F.| . x = |.F.| . (x + t) ) by A5, VALUED_1:def_11; ::_thesis: verum
end;
hence  |.F.| is t -periodic by A2, Th1; ::_thesis: verum
end;

theorem Th11: :: FUNCT_9:11
for t being real number
for F being real-valued Function st F is t -periodic holds
F " is t -periodic
proof
let t be real number ; ::_thesis: for F being real-valued Function st F is t -periodic holds
F " is t -periodic
let F be real-valued Function; ::_thesis: ( F is t -periodic implies F " is t -periodic )
assume A1: F is t -periodic ; ::_thesis: F " is t -periodic
then A2: ( t <> 0 & ( for x being real number st x in dom F holds
( x + t in dom F & x - t in dom F & F . x = F . (x + t) ) ) ) by Th1;
 for x being real number st x in dom (F ") holds
( x + t in dom (F ") & x - t in dom (F ") & (F ") . x = (F ") . (x + t) )
proof
let x be real number ; ::_thesis: ( x in dom (F ") implies ( x + t in dom (F ") & x - t in dom (F ") & (F ") . x = (F ") . (x + t) ) )
assume A3: x in dom (F ") ; ::_thesis: ( x + t in dom (F ") & x - t in dom (F ") & (F ") . x = (F ") . (x + t) )
then A4: x in dom F by VALUED_1:def_7;
then A5: ( x + t in dom F & x - t in dom F ) by A1, Th1;
then A6: ( x + t in dom (F ") & x - t in dom (F ") ) by VALUED_1:def_7;
(F ") . x = (F . x) " by A3, VALUED_1:def_7
.= (F . (x + t)) " by A1, Th1, A4
.= (F ") . (x + t) by A6, VALUED_1:def_7 ;
hence  ( x + t in dom (F ") & x - t in dom (F ") & (F ") . x = (F ") . (x + t) ) by A5, VALUED_1:def_7; ::_thesis: verum
end;
hence  F " is t -periodic by A2, Th1; ::_thesis: verum
end;

theorem :: FUNCT_9:12
for t being real number
for F being real-valued Function st F is t -periodic holds
F ^2 is t -periodic by Th4;

theorem Th13: :: FUNCT_9:13
for t being real number
for F being real-valued Function st F is t -periodic holds
for x being real number st x in dom F holds
F . x = F . (x - t)
proof
let t be real number ; ::_thesis: for F being real-valued Function st F is t -periodic holds
for x being real number st x in dom F holds
F . x = F . (x - t)
let F be real-valued Function; ::_thesis: ( F is t -periodic implies for x being real number st x in dom F holds
F . x = F . (x - t) )
assume A1: F is t -periodic ; ::_thesis: for x being real number st x in dom F holds
F . x = F . (x - t)
let x be real number ; ::_thesis: ( x in dom F implies F . x = F . (x - t) )
assume  x in dom F ; ::_thesis: F . x = F . (x - t)
then  ( x + t in dom F & x - t in dom F ) by A1, Th1;
then F . (x - t) = F . ((x - t) + t) by A1, Th1
.= F . x ;
hence  F . x = F . (x - t) ; ::_thesis: verum
end;

theorem Th14: :: FUNCT_9:14
for t being real number
for F being real-valued Function st F is t -periodic holds
F is - t -periodic
proof
let t be real number ; ::_thesis: for F being real-valued Function st F is t -periodic holds
F is - t -periodic
let F be real-valued Function; ::_thesis: ( F is t -periodic implies F is - t -periodic )
assume A1: F is t -periodic ; ::_thesis: F is - t -periodic
then A2: - t <> 0 by Th1;
 for x being real number st x in dom F holds
( x + (- t) in dom F & x - (- t) in dom F & F . x = F . (x + (- t)) )
proof
let x be real number ; ::_thesis: ( x in dom F implies ( x + (- t) in dom F & x - (- t) in dom F & F . x = F . (x + (- t)) ) )
assume A3: x in dom F ; ::_thesis: ( x + (- t) in dom F & x - (- t) in dom F & F . x = F . (x + (- t)) )
then  ( x + t in dom F & x - t in dom F ) by A1, Th1;
hence  ( x + (- t) in dom F & x - (- t) in dom F & F . x = F . (x + (- t)) ) by A1, Th13, A3; ::_thesis: verum
end;
hence  F is - t -periodic by A2, Th1; ::_thesis: verum
end;

theorem :: FUNCT_9:15
for t1, t2 being real number
for F being real-valued Function st F is t1 -periodic & F is t2 -periodic & t1 + t2 <> 0 holds
F is t1 + t2 -periodic
proof
let t1, t2 be real number ; ::_thesis: for F being real-valued Function st F is t1 -periodic & F is t2 -periodic & t1 + t2 <> 0 holds
F is t1 + t2 -periodic
let F be real-valued Function; ::_thesis: ( F is t1 -periodic & F is t2 -periodic & t1 + t2 <> 0 implies F is t1 + t2 -periodic )
assume A1: ( F is t1 -periodic & F is t2 -periodic & t1 + t2 <> 0 ) ; ::_thesis: F is t1 + t2 -periodic
 for x being real number st x in dom F holds
( x + (t1 + t2) in dom F & x - (t1 + t2) in dom F & F . x = F . (x + (t1 + t2)) )
proof
let x be real number ; ::_thesis: ( x in dom F implies ( x + (t1 + t2) in dom F & x - (t1 + t2) in dom F & F . x = F . (x + (t1 + t2)) ) )
assume A2: x in dom F ; ::_thesis: ( x + (t1 + t2) in dom F & x - (t1 + t2) in dom F & F . x = F . (x + (t1 + t2)) )
then  ( x + t1 in dom F & x - t1 in dom F ) by A1, Th1;
then  ( (x + t1) + t2 in dom F & (x - t1) - t2 in dom F & F . (x + t1) = F . ((x + t1) + t2) ) by A1, Th1;
hence  ( x + (t1 + t2) in dom F & x - (t1 + t2) in dom F & F . x = F . (x + (t1 + t2)) ) by A1, Th1, A2; ::_thesis: verum
end;
hence  F is t1 + t2 -periodic by A1, Th1; ::_thesis: verum
end;

theorem :: FUNCT_9:16
for t1, t2 being real number
for F being real-valued Function st F is t1 -periodic & F is t2 -periodic & t1 - t2 <> 0 holds
F is t1 - t2 -periodic
proof
let t1, t2 be real number ; ::_thesis: for F being real-valued Function st F is t1 -periodic & F is t2 -periodic & t1 - t2 <> 0 holds
F is t1 - t2 -periodic
let F be real-valued Function; ::_thesis: ( F is t1 -periodic & F is t2 -periodic & t1 - t2 <> 0 implies F is t1 - t2 -periodic )
assume A1: ( F is t1 -periodic & F is t2 -periodic & t1 - t2 <> 0 ) ; ::_thesis: F is t1 - t2 -periodic
 for x being real number st x in dom F holds
( x + (t1 - t2) in dom F & x - (t1 - t2) in dom F & F . x = F . (x + (t1 - t2)) )
proof
let x be real number ; ::_thesis: ( x in dom F implies ( x + (t1 - t2) in dom F & x - (t1 - t2) in dom F & F . x = F . (x + (t1 - t2)) ) )
assume A2: x in dom F ; ::_thesis: ( x + (t1 - t2) in dom F & x - (t1 - t2) in dom F & F . x = F . (x + (t1 - t2)) )
then  ( x + t1 in dom F & x - t1 in dom F ) by A1, Th1;
then A3: ( (x + t1) - t2 in dom F & (x - t1) + t2 in dom F ) by A1, Th1;
A4: x - t2 in dom F by A1, Th1, A2;
then F . ((x - t2) + t1) = F . (x - t2) by A1, Th1
.= F . ((x - t2) + t2) by A1, Th1, A4
.= F . x ;
hence  ( x + (t1 - t2) in dom F & x - (t1 - t2) in dom F & F . x = F . (x + (t1 - t2)) ) by A3; ::_thesis: verum
end;
hence  F is t1 - t2 -periodic by A1, Th1; ::_thesis: verum
end;

theorem :: FUNCT_9:17
for t being real number
for F being real-valued Function st t <> 0 & ( for x being real number st x in dom F holds
( x + t in dom F & x - t in dom F & F . (x + t) = F . (x - t) ) ) holds
( F is 2 * t -periodic & F is periodic )
proof
let t be real number ; ::_thesis: for F being real-valued Function st t <> 0 & ( for x being real number st x in dom F holds
( x + t in dom F & x - t in dom F & F . (x + t) = F . (x - t) ) ) holds
( F is 2 * t -periodic & F is periodic )
let F be real-valued Function; ::_thesis: ( t <> 0 & ( for x being real number st x in dom F holds
( x + t in dom F & x - t in dom F & F . (x + t) = F . (x - t) ) ) implies ( F is 2 * t -periodic & F is periodic ) )
assume that
A1: t <> 0 and
A2: for x being real number st x in dom F holds
( x + t in dom F & x - t in dom F & F . (x + t) = F . (x - t) ) ; ::_thesis: ( F is 2 * t -periodic & F is periodic )
 for x being real number st x in dom F holds
( x + (2 * t) in dom F & x - (2 * t) in dom F & F . x = F . (x + (2 * t)) )
proof
let x be real number ; ::_thesis: ( x in dom F implies ( x + (2 * t) in dom F & x - (2 * t) in dom F & F . x = F . (x + (2 * t)) ) )
assume  x in dom F ; ::_thesis: ( x + (2 * t) in dom F & x - (2 * t) in dom F & F . x = F . (x + (2 * t)) )
then A3: ( x + t in dom F & x - t in dom F ) by A2;
then A4: ( (x + t) + t in dom F & (x - t) - t in dom F ) by A2;
F . (x + (2 * t)) = F . ((x + t) + t)
.= F . ((x + t) - t) by A2, A3
.= F . x ;
hence  ( x + (2 * t) in dom F & x - (2 * t) in dom F & F . x = F . (x + (2 * t)) ) by A4; ::_thesis: verum
end;
then  F is 2 * t -periodic by A1, Th1;
hence  ( F is 2 * t -periodic & F is periodic ) by Def2; ::_thesis: verum
end;

theorem :: FUNCT_9:18
for t1, t2 being real number
for F being real-valued Function st t1 + t2 <> 0 & ( for x being real number st x in dom F holds
( x + t1 in dom F & x - t1 in dom F & x + t2 in dom F & x - t2 in dom F & F . (x + t1) = F . (x - t2) ) ) holds
( F is t1 + t2 -periodic & F is periodic )
proof
let t1, t2 be real number ; ::_thesis: for F being real-valued Function st t1 + t2 <> 0 & ( for x being real number st x in dom F holds
( x + t1 in dom F & x - t1 in dom F & x + t2 in dom F & x - t2 in dom F & F . (x + t1) = F . (x - t2) ) ) holds
( F is t1 + t2 -periodic & F is periodic )
let F be real-valued Function; ::_thesis: ( t1 + t2 <> 0 & ( for x being real number st x in dom F holds
( x + t1 in dom F & x - t1 in dom F & x + t2 in dom F & x - t2 in dom F & F . (x + t1) = F . (x - t2) ) ) implies ( F is t1 + t2 -periodic & F is periodic ) )
assume that
A1: t1 + t2 <> 0 and
A2: for x being real number st x in dom F holds
( x + t1 in dom F & x - t1 in dom F & x + t2 in dom F & x - t2 in dom F & F . (x + t1) = F . (x - t2) ) ; ::_thesis: ( F is t1 + t2 -periodic & F is periodic )
 for x being real number st x in dom F holds
( x + (t1 + t2) in dom F & x - (t1 + t2) in dom F & F . x = F . (x + (t1 + t2)) )
proof
let x be real number ; ::_thesis: ( x in dom F implies ( x + (t1 + t2) in dom F & x - (t1 + t2) in dom F & F . x = F . (x + (t1 + t2)) ) )
assume  x in dom F ; ::_thesis: ( x + (t1 + t2) in dom F & x - (t1 + t2) in dom F & F . x = F . (x + (t1 + t2)) )
then A3: ( x + t1 in dom F & x - t1 in dom F & x + t2 in dom F & x - t2 in dom F ) by A2;
then A4: ( (x + t1) + t2 in dom F & (x - t1) - t2 in dom F ) by A2;
F . (x + (t1 + t2)) = F . ((x + t2) + t1)
.= F . ((x + t2) - t2) by A2, A3
.= F . x ;
hence  ( x + (t1 + t2) in dom F & x - (t1 + t2) in dom F & F . x = F . (x + (t1 + t2)) ) by A4; ::_thesis: verum
end;
then  F is t1 + t2 -periodic by Th1, A1;
hence  ( F is t1 + t2 -periodic & F is periodic ) by Def2; ::_thesis: verum
end;

theorem :: FUNCT_9:19
for t1, t2 being real number
for F being real-valued Function st t1 - t2 <> 0 & ( for x being real number st x in dom F holds
( x + t1 in dom F & x - t1 in dom F & x + t2 in dom F & x - t2 in dom F & F . (x + t1) = F . (x + t2) ) ) holds
( F is t1 - t2 -periodic & F is periodic )
proof
let t1, t2 be real number ; ::_thesis: for F being real-valued Function st t1 - t2 <> 0 & ( for x being real number st x in dom F holds
( x + t1 in dom F & x - t1 in dom F & x + t2 in dom F & x - t2 in dom F & F . (x + t1) = F . (x + t2) ) ) holds
( F is t1 - t2 -periodic & F is periodic )
let F be real-valued Function; ::_thesis: ( t1 - t2 <> 0 & ( for x being real number st x in dom F holds
( x + t1 in dom F & x - t1 in dom F & x + t2 in dom F & x - t2 in dom F & F . (x + t1) = F . (x + t2) ) ) implies ( F is t1 - t2 -periodic & F is periodic ) )
assume that
A1: t1 - t2 <> 0 and
A2: for x being real number st x in dom F holds
( x + t1 in dom F & x - t1 in dom F & x + t2 in dom F & x - t2 in dom F & F . (x + t1) = F . (x + t2) ) ; ::_thesis: ( F is t1 - t2 -periodic & F is periodic )
 for x being real number st x in dom F holds
( x + (t1 - t2) in dom F & x - (t1 - t2) in dom F & F . x = F . (x + (t1 - t2)) )
proof
let x be real number ; ::_thesis: ( x in dom F implies ( x + (t1 - t2) in dom F & x - (t1 - t2) in dom F & F . x = F . (x + (t1 - t2)) ) )
assume  x in dom F ; ::_thesis: ( x + (t1 - t2) in dom F & x - (t1 - t2) in dom F & F . x = F . (x + (t1 - t2)) )
then A3: ( x + t1 in dom F & x - t1 in dom F & x + t2 in dom F & x - t2 in dom F ) by A2;
then A4: ( (x + t1) - t2 in dom F & (x - t1) + t2 in dom F ) by A2;
F . (x + (t1 - t2)) = F . ((x - t2) + t1)
.= F . ((x - t2) + t2) by A2, A3
.= F . x ;
hence  ( x + (t1 - t2) in dom F & x - (t1 - t2) in dom F & F . x = F . (x + (t1 - t2)) ) by A4; ::_thesis: verum
end;
then  F is t1 - t2 -periodic by Th1, A1;
hence  ( F is t1 - t2 -periodic & F is periodic ) by Def2; ::_thesis: verum
end;

theorem :: FUNCT_9:20
for t being real number
for F being real-valued Function st t <> 0 & ( for x being real number st x in dom F holds
( x + t in dom F & x - t in dom F & F . (x + t) = (F . x) " ) ) holds
( F is 2 * t -periodic & F is periodic )
proof
let t be real number ; ::_thesis: for F being real-valued Function st t <> 0 & ( for x being real number st x in dom F holds
( x + t in dom F & x - t in dom F & F . (x + t) = (F . x) " ) ) holds
( F is 2 * t -periodic & F is periodic )
let F be real-valued Function; ::_thesis: ( t <> 0 & ( for x being real number st x in dom F holds
( x + t in dom F & x - t in dom F & F . (x + t) = (F . x) " ) ) implies ( F is 2 * t -periodic & F is periodic ) )
assume that
A1: t <> 0 and
A2: for x being real number st x in dom F holds
( x + t in dom F & x - t in dom F & F . (x + t) = (F . x) " ) ; ::_thesis: ( F is 2 * t -periodic & F is periodic )
 for x being real number st x in dom F holds
( x + (2 * t) in dom F & x - (2 * t) in dom F & F . x = F . (x + (2 * t)) )
proof
let x be real number ; ::_thesis: ( x in dom F implies ( x + (2 * t) in dom F & x - (2 * t) in dom F & F . x = F . (x + (2 * t)) ) )
assume A3: x in dom F ; ::_thesis: ( x + (2 * t) in dom F & x - (2 * t) in dom F & F . x = F . (x + (2 * t)) )
then A4: ( x + t in dom F & x - t in dom F ) by A2;
then A5: ( (x + t) + t in dom F & (x - t) - t in dom F ) by A2;
F . (x + (2 * t)) = F . ((x + t) + t)
.= (F . (x + t)) " by A2, A4
.= ((F . x) ") " by A2, A3
.= F . x ;
hence  ( x + (2 * t) in dom F & x - (2 * t) in dom F & F . x = F . (x + (2 * t)) ) by A5; ::_thesis: verum
end;
then  F is 2 * t -periodic by A1, Th1;
hence  ( F is 2 * t -periodic & F is periodic ) by Def2; ::_thesis: verum
end;

Lm2:  sin is 2 * PI -periodic
proof
 for x being real number st x in dom sin holds
( x + (2 * PI) in dom sin & x - (2 * PI) in dom sin & sin . x = sin . (x + (2 * PI)) ) by SIN_COS:24, SIN_COS:78;
hence  sin is 2 * PI -periodic by Th1; ::_thesis: verum
end;

registration
cluster Relation-like Function-like real-valued periodic for set ;
existence
 ex b1 being Function st
( b1 is periodic & b1 is real-valued )
proof
take  sin ; ::_thesis: ( sin is periodic & sin is real-valued )
thus  ( sin is periodic & sin is real-valued ) by Lm2, Def2; ::_thesis: verum
end;
cluster Relation-like Function-like complex-valued ext-real-valued real-valued periodic for Element of K6(K7(REAL,REAL));
existence
 ex b1 being PartFunc of REAL,REAL st b1 is periodic
proof
take  sin ; ::_thesis: sin is periodic
thus  sin is periodic by Lm2, Def2; ::_thesis: verum
end;
end;

registration
let t be non zero real number ;
clusterREAL --> t -> t -periodic ;
coherence
 REAL --> t is t -periodic by Lm1;
cluster Relation-like Function-like real-valued t -periodic for set ;
existence
 ex b1 being Function st
( b1 is t -periodic & b1 is real-valued )
proof
take  REAL --> t ; ::_thesis: ( REAL --> t is t -periodic & REAL --> t is real-valued )
thus  ( REAL --> t is t -periodic & REAL --> t is real-valued ) ; ::_thesis: verum
end;
end;

registration
let t be non zero real number ;
let F, G be real-valued t -periodic Function;
clusterF + G -> t -periodic ;
coherence
 F + G is t -periodic by Th2;
clusterF - G -> t -periodic ;
coherence
 F - G is t -periodic by Th3;
clusterF (#) G -> t -periodic ;
coherence
 F (#) G is t -periodic by Th4;
clusterF /" G -> t -periodic ;
coherence
 F /" G is t -periodic by Th5;
end;

registration
let F be real-valued periodic Function;
cluster - F ->  periodic ;
coherence
 - F is periodic
proof
consider t being real number  such that
A1: F is t -periodic by Def2;
 - F is t -periodic by A1, Th6;
hence  - F is periodic by Def2; ::_thesis: verum
end;
end;

registration
let F be real-valued periodic Function;
let r be real number ;
clusterr (#) F ->  periodic ;
coherence
 r (#) F is periodic
proof
consider t being real number  such that
A1: F is t -periodic by Def2;
 r (#) F is t -periodic by A1, Th7;
hence  r (#) F is periodic by Def2; ::_thesis: verum
end;
clusterr + F ->  periodic ;
coherence
 r + F is periodic
proof
consider t being real number  such that
A2: F is t -periodic by Def2;
 r + F is t -periodic by A2, Th8;
hence  r + F is periodic by Def2; ::_thesis: verum
end;
clusterF - r ->  periodic ;
coherence
 F - r is periodic ;
end;

registration
let F be real-valued periodic Function;
cluster|.F.| ->  periodic ;
coherence
 |.F.| is periodic
proof
consider t being real number  such that
A1: F is t -periodic by Def2;
 |.F.| is t -periodic by A1, Th10;
hence  |.F.| is periodic by Def2; ::_thesis: verum
end;
clusterF "  ->  periodic ;
coherence
 F " is periodic
proof
consider t being real number  such that
A2: F is t -periodic by Def2;
 F " is t -periodic by A2, Th11;
hence  F " is periodic by Def2; ::_thesis: verum
end;
clusterF ^2  ->  periodic ;
coherence
 F ^2 is periodic
proof
consider t being real number  such that
A3: F is t -periodic by Def2;
 F ^2 is t -periodic by A3, Th4;
hence  F ^2 is periodic by Def2; ::_thesis: verum
end;
end;

begin

Lm3:  cos is 2 * PI -periodic
proof
 for x being real number st x in dom cos holds
( x + (2 * PI) in dom cos & x - (2 * PI) in dom cos & cos . x = cos . (x + (2 * PI)) ) by SIN_COS:24, SIN_COS:78;
hence  cos is 2 * PI -periodic by Th1; ::_thesis: verum
end;

registration
cluster sin  ->  periodic ;
coherence
 sin is periodic by Def2, Lm2;
cluster cos  ->  periodic ;
coherence
 cos is periodic by Def2, Lm3;
end;

Lm4:  for k being Nat holds sin is (2 * PI) * (k + 1) -periodic
proof
let k be Nat; ::_thesis: sin is (2 * PI) * (k + 1) -periodic
defpred S1[ Nat] means  sin is (2 * PI) * ($1 + 1) -periodic ;
A1: S1[ 0 ] by Lm2;
A2: for k being Nat st S1[k] holds
S1[k + 1]
proof
let k be Nat; ::_thesis: ( S1[k] implies S1[k + 1] )
assume A3: sin is (2 * PI) * (k + 1) -periodic ; ::_thesis: S1[k + 1]
 sin is (2 * PI) * ((k + 1) + 1) -periodic
proof
 for x being real number st x in dom sin holds
sin . x = sin . (x + ((2 * PI) * ((k + 1) + 1)))
proof
let x be real number ; ::_thesis: ( x in dom sin implies sin . x = sin . (x + ((2 * PI) * ((k + 1) + 1))) )
assume A4: x in dom sin ; ::_thesis: sin . x = sin . (x + ((2 * PI) * ((k + 1) + 1)))
 sin . (x + ((2 * PI) * (k + 1))) = sin . ((x + ((2 * PI) * (k + 1))) + (2 * PI)) by SIN_COS:78;
hence  sin . x = sin . (x + ((2 * PI) * ((k + 1) + 1))) by A3, Th1, A4; ::_thesis: verum
end;
then  ( (2 * PI) * ((k + 1) + 1) <> 0 & ( for x being real number st x in dom sin holds
( x + ((2 * PI) * ((k + 1) + 1)) in dom sin & x - ((2 * PI) * ((k + 1) + 1)) in dom sin & sin . x = sin . (x + ((2 * PI) * ((k + 1) + 1))) ) ) ) by SIN_COS:24;
hence  sin is (2 * PI) * ((k + 1) + 1) -periodic by Th1; ::_thesis: verum
end;
hence  S1[k + 1] ; ::_thesis: verum
end;
 for n being Nat holds S1[n] from NAT_1:sch_2(A1, A2);
hence  sin is (2 * PI) * (k + 1) -periodic ; ::_thesis: verum
end;

theorem :: FUNCT_9:21
for i being non zero Integer holds sin is (2 * PI) * i -periodic
proof
let i be non zero Integer; ::_thesis: sin is (2 * PI) * i -periodic
 i in INT by INT_1:def_2;
then consider k being Element of NAT  such that
A1: ( i = k or i = - k ) by INT_1:def_1;
percases ( i = k or i = - k ) by A1;
suppose i = k ; ::_thesis: sin is (2 * PI) * i -periodic
then  ex m being Nat st i = m + 1 by NAT_1:6;
hence  sin is (2 * PI) * i -periodic by Lm4; ::_thesis: verum
end;
supposeA2: i = - k ; ::_thesis: sin is (2 * PI) * i -periodic
then consider m being Nat such that
A3: - i = m + 1 by NAT_1:6;
 sin is (2 * PI) * (m + 1) -periodic by Lm4;
then  sin is - ((2 * PI) * (m + 1)) -periodic by Th14;
hence  sin is (2 * PI) * i -periodic by A2, A3; ::_thesis: verum
end;
end;
end;

Lm5:  for k being Nat holds cos is (2 * PI) * (k + 1) -periodic
proof
let k be Nat; ::_thesis: cos is (2 * PI) * (k + 1) -periodic
defpred S1[ Nat] means  cos is (2 * PI) * ($1 + 1) -periodic ;
A1: S1[ 0 ] by Lm3;
A2: for k being Nat st S1[k] holds
S1[k + 1]
proof
let k be Nat; ::_thesis: ( S1[k] implies S1[k + 1] )
assume A3: cos is (2 * PI) * (k + 1) -periodic ; ::_thesis: S1[k + 1]
 cos is (2 * PI) * ((k + 1) + 1) -periodic
proof
 for x being real number st x in dom cos holds
cos . x = cos . (x + ((2 * PI) * ((k + 1) + 1)))
proof
let x be real number ; ::_thesis: ( x in dom cos implies cos . x = cos . (x + ((2 * PI) * ((k + 1) + 1))) )
assume A4: x in dom cos ; ::_thesis: cos . x = cos . (x + ((2 * PI) * ((k + 1) + 1)))
 cos . (x + ((2 * PI) * (k + 1))) = cos . ((x + ((2 * PI) * (k + 1))) + (2 * PI)) by SIN_COS:78;
hence  cos . x = cos . (x + ((2 * PI) * ((k + 1) + 1))) by A3, Th1, A4; ::_thesis: verum
end;
then  ( (2 * PI) * ((k + 1) + 1) <> 0 & ( for x being real number st x in dom cos holds
( x + ((2 * PI) * ((k + 1) + 1)) in dom cos & x - ((2 * PI) * ((k + 1) + 1)) in dom cos & cos . x = cos . (x + ((2 * PI) * ((k + 1) + 1))) ) ) ) by SIN_COS:24;
hence  cos is (2 * PI) * ((k + 1) + 1) -periodic by Th1; ::_thesis: verum
end;
hence  S1[k + 1] ; ::_thesis: verum
end;
 for n being Nat holds S1[n] from NAT_1:sch_2(A1, A2);
hence  cos is (2 * PI) * (k + 1) -periodic ; ::_thesis: verum
end;

theorem :: FUNCT_9:22
for i being non zero Integer holds cos is (2 * PI) * i -periodic
proof
let i be non zero Integer; ::_thesis: cos is (2 * PI) * i -periodic
 i in INT by INT_1:def_2;
then consider k being Element of NAT  such that
A1: ( i = k or i = - k ) by INT_1:def_1;
percases ( i = k or i = - k ) by A1;
suppose i = k ; ::_thesis: cos is (2 * PI) * i -periodic
then  ex m being Nat st i = m + 1 by NAT_1:6;
hence  cos is (2 * PI) * i -periodic by Lm5; ::_thesis: verum
end;
supposeA2: i = - k ; ::_thesis: cos is (2 * PI) * i -periodic
then consider m being Nat such that
A3: - i = m + 1 by NAT_1:6;
 cos is (2 * PI) * (m + 1) -periodic by Lm5;
then  cos is - ((2 * PI) * (m + 1)) -periodic by Th14;
hence  cos is (2 * PI) * i -periodic by A2, A3; ::_thesis: verum
end;
end;
end;

Lm6:  cosec is 2 * PI -periodic
proof
 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_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;
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 Lm2, Th1, SIN_COS:24;
then  ( x - (2 * PI) in dom sin & not x - (2 * PI) in sin " {0} ) by A2, FUNCT_1:def_7, SIN_COS:24;
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;
hence  cosec is 2 * PI -periodic by Th1; ::_thesis: verum
end;

Lm7:  sec is 2 * PI -periodic
proof
 for x being real number 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 number ; ::_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;
then A3: x + (2 * PI) in (dom cos) \ (cos " {0}) by XBOOLE_0:def_5;
 cos . (x - (2 * PI)) = cos . ((x - (2 * PI)) + (2 * PI)) by Lm3, Th1, SIN_COS:24;
then  ( x - (2 * PI) in dom cos & not x - (2 * PI) in cos " {0} ) by A2, FUNCT_1:def_7, SIN_COS:24;
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
end;

registration
cluster cosec  ->  periodic ;
coherence
 cosec is periodic by Def2, Lm6;
cluster sec  ->  periodic ;
coherence
 sec is periodic by Def2, Lm7;
end;

Lm8:  for k being Nat holds sec is (2 * PI) * (k + 1) -periodic
proof
let k be Nat; ::_thesis: sec is (2 * PI) * (k + 1) -periodic
defpred S1[ Nat] means  sec is (2 * PI) * ($1 + 1) -periodic ;
A1: S1[ 0 ] by Lm7;
A2: for k being Nat st S1[k] holds
S1[k + 1]
proof
let k be Nat; ::_thesis: ( S1[k] implies S1[k + 1] )
assume A3: sec is (2 * PI) * (k + 1) -periodic ; ::_thesis: S1[k + 1]
 sec is (2 * PI) * ((k + 1) + 1) -periodic
proof
 for x being real number st x in dom sec holds
( x + ((2 * PI) * ((k + 1) + 1)) in dom sec & x - ((2 * PI) * ((k + 1) + 1)) in dom sec & sec . x = sec . (x + ((2 * PI) * ((k + 1) + 1))) )
proof
let x be real number ; ::_thesis: ( x in dom sec implies ( x + ((2 * PI) * ((k + 1) + 1)) in dom sec & x - ((2 * PI) * ((k + 1) + 1)) in dom sec & sec . x = sec . (x + ((2 * PI) * ((k + 1) + 1))) ) )
assume  x in dom sec ; ::_thesis: ( x + ((2 * PI) * ((k + 1) + 1)) in dom sec & x - ((2 * PI) * ((k + 1) + 1)) in dom sec & sec . x = sec . (x + ((2 * PI) * ((k + 1) + 1))) )
then A4: ( x + ((2 * PI) * (k + 1)) in dom sec & x - ((2 * PI) * (k + 1)) in dom sec & sec . x = sec . (x + ((2 * PI) * (k + 1))) ) by A3, Th1;
then  ( x + ((2 * PI) * (k + 1)) in (dom cos) \ (cos " {0}) & x - ((2 * PI) * (k + 1)) in (dom cos) \ (cos " {0}) ) by RFUNCT_1:def_2;
then  ( x + ((2 * PI) * (k + 1)) in dom cos & not x + ((2 * PI) * (k + 1)) in cos " {0} & x - ((2 * PI) * (k + 1)) in dom cos & not x - ((2 * PI) * (k + 1)) in cos " {0} ) by XBOOLE_0:def_5;
then A5: ( not cos . (x + ((2 * PI) * (k + 1))) in {0} & not cos . (x - ((2 * PI) * (k + 1))) in {0} ) by FUNCT_1:def_7;
then  cos . (x + ((2 * PI) * (k + 1))) <> 0 by TARSKI:def_1;
then  cos . ((x + ((2 * PI) * (k + 1))) + (2 * PI)) <> 0 by SIN_COS:78;
then  not cos . ((x + ((2 * PI) * (k + 1))) + (2 * PI)) in {0} by TARSKI:def_1;
then  ( (x + ((2 * PI) * (k + 1))) + (2 * PI) in dom cos & not (x + ((2 * PI) * (k + 1))) + (2 * PI) in cos " {0} ) by FUNCT_1:def_7, SIN_COS:24;
then A6: x + ((2 * PI) * ((k + 1) + 1)) in (dom cos) \ (cos " {0}) by XBOOLE_0:def_5;
 cos . (x - ((2 * PI) * ((k + 1) + 1))) = cos . ((x - ((2 * PI) * ((k + 1) + 1))) + (2 * PI)) by Lm3, Th1, SIN_COS:24;
then  ( x - ((2 * PI) * ((k + 1) + 1)) in dom cos & not x - ((2 * PI) * ((k + 1) + 1)) in cos " {0} ) by A5, FUNCT_1:def_7, SIN_COS:24;
then A7: x - ((2 * PI) * ((k + 1) + 1)) in (dom cos) \ (cos " {0}) by XBOOLE_0:def_5;
then  ( x + ((2 * PI) * ((k + 1) + 1)) in dom sec & x - ((2 * PI) * ((k + 1) + 1)) in dom sec ) by A6, RFUNCT_1:def_2;
then sec . (x + ((2 * PI) * ((k + 1) + 1))) = (cos . ((x + ((2 * PI) * (k + 1))) + (2 * PI))) " by RFUNCT_1:def_2
.= (cos . (x + ((2 * PI) * (k + 1)))) " by SIN_COS:78
.= sec . x by A4, RFUNCT_1:def_2 ;
hence  ( x + ((2 * PI) * ((k + 1) + 1)) in dom sec & x - ((2 * PI) * ((k + 1) + 1)) in dom sec & sec . x = sec . (x + ((2 * PI) * ((k + 1) + 1))) ) by A6, A7, RFUNCT_1:def_2; ::_thesis: verum
end;
hence  sec is (2 * PI) * ((k + 1) + 1) -periodic by Th1; ::_thesis: verum
end;
hence  S1[k + 1] ; ::_thesis: verum
end;
 for n being Nat holds S1[n] from NAT_1:sch_2(A1, A2);
hence  sec is (2 * PI) * (k + 1) -periodic ; ::_thesis: verum
end;

theorem :: FUNCT_9:23
for i being non zero Integer holds sec is (2 * PI) * i -periodic
proof
let i be non zero Integer; ::_thesis: sec is (2 * PI) * i -periodic
 i in INT by INT_1:def_2;
then consider k being Element of NAT  such that
A1: ( i = k or i = - k ) by INT_1:def_1;
percases ( i = k or i = - k ) by A1;
suppose i = k ; ::_thesis: sec is (2 * PI) * i -periodic
then  ex m being Nat st i = m + 1 by NAT_1:6;
hence  sec is (2 * PI) * i -periodic by Lm8; ::_thesis: verum
end;
supposeA2: i = - k ; ::_thesis: sec is (2 * PI) * i -periodic
then consider m being Nat such that
A3: - i = m + 1 by NAT_1:6;
 sec is (2 * PI) * (m + 1) -periodic by Lm8;
then  sec is - ((2 * PI) * (m + 1)) -periodic by Th14;
hence  sec is (2 * PI) * i -periodic by A2, A3; ::_thesis: verum
end;
end;
end;

Lm9:  for k being Nat holds cosec is (2 * PI) * (k + 1) -periodic
proof
let k be Nat; ::_thesis: cosec is (2 * PI) * (k + 1) -periodic
defpred S1[ Nat] means  cosec is (2 * PI) * ($1 + 1) -periodic ;
A1: S1[ 0 ] by Lm6;
A2: for k being Nat st S1[k] holds
S1[k + 1]
proof
let k be Nat; ::_thesis: ( S1[k] implies S1[k + 1] )
assume A3: cosec is (2 * PI) * (k + 1) -periodic ; ::_thesis: S1[k + 1]
 cosec is (2 * PI) * ((k + 1) + 1) -periodic
proof
 for x being real number st x in dom cosec holds
( x + ((2 * PI) * ((k + 1) + 1)) in dom cosec & x - ((2 * PI) * ((k + 1) + 1)) in dom cosec & cosec . x = cosec . (x + ((2 * PI) * ((k + 1) + 1))) )
proof
let x be real number ; ::_thesis: ( x in dom cosec implies ( x + ((2 * PI) * ((k + 1) + 1)) in dom cosec & x - ((2 * PI) * ((k + 1) + 1)) in dom cosec & cosec . x = cosec . (x + ((2 * PI) * ((k + 1) + 1))) ) )
assume  x in dom cosec ; ::_thesis: ( x + ((2 * PI) * ((k + 1) + 1)) in dom cosec & x - ((2 * PI) * ((k + 1) + 1)) in dom cosec & cosec . x = cosec . (x + ((2 * PI) * ((k + 1) + 1))) )
then A4: ( x + ((2 * PI) * (k + 1)) in dom cosec & x - ((2 * PI) * (k + 1)) in dom cosec & cosec . x = cosec . (x + ((2 * PI) * (k + 1))) ) by A3, Th1;
then  ( x + ((2 * PI) * (k + 1)) in (dom sin) \ (sin " {0}) & x - ((2 * PI) * (k + 1)) in (dom sin) \ (sin " {0}) ) by RFUNCT_1:def_2;
then  ( x + ((2 * PI) * (k + 1)) in dom sin & not x + ((2 * PI) * (k + 1)) in sin " {0} & x - ((2 * PI) * (k + 1)) in dom sin & not x - ((2 * PI) * (k + 1)) in sin " {0} ) by XBOOLE_0:def_5;
then A5: ( not sin . (x + ((2 * PI) * (k + 1))) in {0} & not sin . (x - ((2 * PI) * (k + 1))) in {0} ) by FUNCT_1:def_7;
then  sin . (x + ((2 * PI) * (k + 1))) <> 0 by TARSKI:def_1;
then  sin . ((x + ((2 * PI) * (k + 1))) + (2 * PI)) <> 0 by SIN_COS:78;
then  not sin . ((x + ((2 * PI) * (k + 1))) + (2 * PI)) in {0} by TARSKI:def_1;
then  ( (x + ((2 * PI) * (k + 1))) + (2 * PI) in dom sin & not (x + ((2 * PI) * (k + 1))) + (2 * PI) in sin " {0} ) by FUNCT_1:def_7, SIN_COS:24;
then A6: x + ((2 * PI) * ((k + 1) + 1)) in (dom sin) \ (sin " {0}) by XBOOLE_0:def_5;
 sin . (x - ((2 * PI) * ((k + 1) + 1))) = sin . ((x - ((2 * PI) * ((k + 1) + 1))) + (2 * PI)) by Lm2, Th1, SIN_COS:24;
then  ( x - ((2 * PI) * ((k + 1) + 1)) in dom sin & not x - ((2 * PI) * ((k + 1) + 1)) in sin " {0} ) by A5, FUNCT_1:def_7, SIN_COS:24;
then A7: x - ((2 * PI) * ((k + 1) + 1)) in (dom sin) \ (sin " {0}) by XBOOLE_0:def_5;
then  ( x + ((2 * PI) * ((k + 1) + 1)) in dom cosec & x - ((2 * PI) * ((k + 1) + 1)) in dom cosec ) by A6, RFUNCT_1:def_2;
then cosec . (x + ((2 * PI) * ((k + 1) + 1))) = (sin . ((x + ((2 * PI) * (k + 1))) + (2 * PI))) " by RFUNCT_1:def_2
.= (sin . (x + ((2 * PI) * (k + 1)))) " by SIN_COS:78
.= cosec . x by A4, RFUNCT_1:def_2 ;
hence  ( x + ((2 * PI) * ((k + 1) + 1)) in dom cosec & x - ((2 * PI) * ((k + 1) + 1)) in dom cosec & cosec . x = cosec . (x + ((2 * PI) * ((k + 1) + 1))) ) by A6, A7, RFUNCT_1:def_2; ::_thesis: verum
end;
hence  cosec is (2 * PI) * ((k + 1) + 1) -periodic by Th1; ::_thesis: verum
end;
hence  S1[k + 1] ; ::_thesis: verum
end;
 for n being Nat holds S1[n] from NAT_1:sch_2(A1, A2);
hence  cosec is (2 * PI) * (k + 1) -periodic ; ::_thesis: verum
end;

theorem :: FUNCT_9:24
for i being non zero Integer holds cosec is (2 * PI) * i -periodic
proof
let i be non zero Integer; ::_thesis: cosec is (2 * PI) * i -periodic
 i in INT by INT_1:def_2;
then consider k being Element of NAT  such that
A1: ( i = k or i = - k ) by INT_1:def_1;
percases ( i = k or i = - k ) by A1;
suppose i = k ; ::_thesis: cosec is (2 * PI) * i -periodic
then  ex m being Nat st i = m + 1 by NAT_1:6;
hence  cosec is (2 * PI) * i -periodic by Lm9; ::_thesis: verum
end;
supposeA2: i = - k ; ::_thesis: cosec is (2 * PI) * i -periodic
then consider m being Nat such that
A3: - i = m + 1 by NAT_1:6;
 cosec is (2 * PI) * (m + 1) -periodic by Lm9;
then  cosec is - ((2 * PI) * (m + 1)) -periodic by Th14;
hence  cosec is (2 * PI) * i -periodic by A2, A3; ::_thesis: verum
end;
end;
end;

Lm10:  tan is PI -periodic
proof
 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_1;
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_7;
then A2: cos . x <> 0 by TARSKI:def_1;
A3: cos . (x + PI) = - (cos . x) by SIN_COS:78;
then  not cos . (x + PI) in {0} by A2, TARSKI:def_1;
then  ( x + PI in dom sin & x + PI in dom cos & not x + PI in cos " {0} ) by FUNCT_1:def_7, SIN_COS:24;
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;
cos . (x - PI) = cos . ((x - PI) + (2 * PI)) by SIN_COS:78
.= cos . (x + PI) ;
then  not cos . (x - PI) in {0} by A2, A3, TARSKI:def_1;
then  ( x - PI in dom sin & x - PI in dom cos & not x - PI in cos " {0} ) by FUNCT_1:def_7, SIN_COS:24;
then  ( x - PI in dom sin & x - PI in (dom cos) \ (cos " {0}) ) by XBOOLE_0:def_5;
then A5: x - PI in (dom sin) /\ ((dom cos) \ (cos " {0})) by XBOOLE_0:def_4;
then  ( x + PI in dom tan & x - PI in dom tan ) by A4, RFUNCT_1:def_1;
then tan . (x + PI) = (sin . (x + PI)) / (cos . (x + PI)) by RFUNCT_1:def_1
.= (- (sin . x)) / (cos . (x + PI)) by SIN_COS:78
.= (- (sin . x)) / (- (cos . x)) by SIN_COS:78
.= (sin . x) / (cos . x) by XCMPLX_1:191
.= tan . x by A1, RFUNCT_1:def_1 ;
hence  ( x + PI in dom tan & x - PI in dom tan & tan . x = tan . (x + PI) ) by A4, A5, RFUNCT_1:def_1; ::_thesis: verum
end;
hence  tan is PI -periodic by Th1; ::_thesis: verum
end;

Lm11:  cot is PI -periodic
proof
 for x being real number st x in dom cot holds
( x + PI in dom cot & x - PI in dom cot & cot . x = cot . (x + PI) )
proof
let x be real number ; ::_thesis: ( x in dom cot implies ( x + PI in dom cot & x - PI in dom cot & cot . x = cot . (x + PI) ) )
assume A1: x in dom cot ; ::_thesis: ( x + PI in dom cot & x - PI in dom cot & cot . x = cot . (x + PI) )
then  x in (dom cos) /\ ((dom sin) \ (sin " {0})) by RFUNCT_1:def_1;
then  ( x in dom cos & x in (dom sin) \ (sin " {0}) ) by XBOOLE_0:def_4;
then  ( x in dom cos & x in dom sin & not x in sin " {0} ) by XBOOLE_0:def_5;
then  not sin . x in {0} by FUNCT_1:def_7;
then A2: sin . x <> 0 by TARSKI:def_1;
A3: sin . (x + PI) = - (sin . x) by SIN_COS:78;
then  not sin . (x + PI) in {0} by A2, TARSKI:def_1;
then  ( x + PI in dom cos & x + PI in dom sin & not x + PI in sin " {0} ) by FUNCT_1:def_7, SIN_COS:24;
then  ( x + PI in dom cos & x + PI in (dom sin) \ (sin " {0}) ) by XBOOLE_0:def_5;
then A4: x + PI in (dom cos) /\ ((dom sin) \ (sin " {0})) by XBOOLE_0:def_4;
sin . (x - PI) = sin . ((x - PI) + (2 * PI)) by SIN_COS:78
.= sin . (x + PI) ;
then  not sin . (x - PI) in {0} by A2, A3, TARSKI:def_1;
then  ( x - PI in dom cos & x - PI in dom sin & not x - PI in sin " {0} ) by FUNCT_1:def_7, SIN_COS:24;
then  ( x - PI in dom cos & x - PI in (dom sin) \ (sin " {0}) ) by XBOOLE_0:def_5;
then A5: x - PI in (dom cos) /\ ((dom sin) \ (sin " {0})) by XBOOLE_0:def_4;
then  ( x + PI in dom cot & x - PI in dom cot ) by A4, RFUNCT_1:def_1;
then cot . (x + PI) = (cos . (x + PI)) / (sin . (x + PI)) by RFUNCT_1:def_1
.= (- (cos . x)) / (sin . (x + PI)) by SIN_COS:78
.= (- (cos . x)) / (- (sin . x)) by SIN_COS:78
.= (cos . x) / (sin . x) by XCMPLX_1:191
.= cot . x by A1, RFUNCT_1:def_1 ;
hence  ( x + PI in dom cot & x - PI in dom cot & cot . x = cot . (x + PI) ) by A4, A5, RFUNCT_1:def_1; ::_thesis: verum
end;
hence  cot is PI -periodic by Th1; ::_thesis: verum
end;

registration
cluster tan  ->  periodic ;
coherence
 tan is periodic by Def2, Lm10;
cluster cot  ->  periodic ;
coherence
 cot is periodic by Def2, Lm11;
end;

Lm12:  for k being Nat holds tan is PI * (k + 1) -periodic
proof
let k be Nat; ::_thesis: tan is PI * (k + 1) -periodic
defpred S1[ Nat] means  tan is PI * ($1 + 1) -periodic ;
A1: S1[ 0 ] by Lm10;
A2: for k being Nat st S1[k] holds
S1[k + 1]
proof
let k be Nat; ::_thesis: ( S1[k] implies S1[k + 1] )
assume A3: tan is PI * (k + 1) -periodic ; ::_thesis: S1[k + 1]
 tan is PI * ((k + 1) + 1) -periodic
proof
 for x being real number st x in dom tan holds
( x + (PI * ((k + 1) + 1)) in dom tan & x - (PI * ((k + 1) + 1)) in dom tan & tan . x = tan . (x + (PI * ((k + 1) + 1))) )
proof
let x be real number ; ::_thesis: ( x in dom tan implies ( x + (PI * ((k + 1) + 1)) in dom tan & x - (PI * ((k + 1) + 1)) in dom tan & tan . x = tan . (x + (PI * ((k + 1) + 1))) ) )
assume  x in dom tan ; ::_thesis: ( x + (PI * ((k + 1) + 1)) in dom tan & x - (PI * ((k + 1) + 1)) in dom tan & tan . x = tan . (x + (PI * ((k + 1) + 1))) )
then A4: ( x + (PI * (k + 1)) in dom tan & x - (PI * (k + 1)) in dom tan & tan . x = tan . (x + (PI * (k + 1))) ) by A3, Th1;
then  ( x + (PI * (k + 1)) in (dom sin) /\ ((dom cos) \ (cos " {0})) & x - (PI * (k + 1)) in (dom sin) /\ ((dom cos) \ (cos " {0})) ) by RFUNCT_1:def_1;
then  ( x + (PI * (k + 1)) in dom sin & x + (PI * (k + 1)) in (dom cos) \ (cos " {0}) & x - (PI * (k + 1)) in dom sin & x - (PI * (k + 1)) in (dom cos) \ (cos " {0}) ) by XBOOLE_0:def_4;
then  ( x + (PI * (k + 1)) in dom sin & x + (PI * (k + 1)) in dom cos & not x + (PI * (k + 1)) in cos " {0} & x - (PI * (k + 1)) in dom sin & x - (PI * (k + 1)) in dom cos & not x - (PI * (k + 1)) in cos " {0} ) by XBOOLE_0:def_5;
then  ( not cos . (x + (PI * (k + 1))) in {0} & not cos . (x - (PI * (k + 1))) in {0} ) by FUNCT_1:def_7;
then A5: ( cos . (x + (PI * (k + 1))) <> 0 & cos . (x - (PI * (k + 1))) <> 0 ) by TARSKI:def_1;
 cos . ((x + (PI * (k + 1))) + PI) = - (cos . (x + (PI * (k + 1)))) by SIN_COS:78;
then  not cos . ((x + (PI * (k + 1))) + PI) in {0} by A5, TARSKI:def_1;
then  ( (x + (PI * (k + 1))) + PI in dom sin & (x + (PI * (k + 1))) + PI in dom cos & not (x + (PI * (k + 1))) + PI in cos " {0} ) by FUNCT_1:def_7, SIN_COS:24;
then  ( (x + (PI * (k + 1))) + PI in dom sin & (x + (PI * (k + 1))) + PI in (dom cos) \ (cos " {0}) ) by XBOOLE_0:def_5;
then A6: (x + (PI * (k + 1))) + PI in (dom sin) /\ ((dom cos) \ (cos " {0})) by XBOOLE_0:def_4;
 cos . ((x - (PI * ((k + 1) + 1))) + PI) = - (cos . (x - (PI * ((k + 1) + 1)))) by SIN_COS:78;
then  cos . (x - (PI * ((k + 1) + 1))) = - (cos . (x - (PI * (k + 1)))) ;
then  not cos . (x - (PI * ((k + 1) + 1))) in {0} by A5, TARSKI:def_1;
then  ( x - (PI * ((k + 1) + 1)) in dom sin & x - (PI * ((k + 1) + 1)) in dom cos & not x - (PI * ((k + 1) + 1)) in cos " {0} ) by FUNCT_1:def_7, SIN_COS:24;
then  ( x - (PI * ((k + 1) + 1)) in dom sin & x - (PI * ((k + 1) + 1)) in (dom cos) \ (cos " {0}) ) by XBOOLE_0:def_5;
then A7: x - (PI * ((k + 1) + 1)) in (dom sin) /\ ((dom cos) \ (cos " {0})) by XBOOLE_0:def_4;
then  ( x + (PI * ((k + 1) + 1)) in dom tan & x - (PI * ((k + 1) + 1)) in dom tan ) by A6, RFUNCT_1:def_1;
then tan . (x + (PI * ((k + 1) + 1))) = (sin . ((x + (PI * (k + 1))) + PI)) / (cos . ((x + (PI * (k + 1))) + PI)) by RFUNCT_1:def_1
.= (- (sin . (x + (PI * (k + 1))))) / (cos . ((x + (PI * (k + 1))) + PI)) by SIN_COS:78
.= (- (sin . (x + (PI * (k + 1))))) / (- (cos . (x + (PI * (k + 1))))) by SIN_COS:78
.= (sin . (x + (PI * (k + 1)))) / (cos . (x + (PI * (k + 1)))) by XCMPLX_1:191
.= tan . x by A4, RFUNCT_1:def_1 ;
hence  ( x + (PI * ((k + 1) + 1)) in dom tan & x - (PI * ((k + 1) + 1)) in dom tan & tan . x = tan . (x + (PI * ((k + 1) + 1))) ) by A7, A6, RFUNCT_1:def_1; ::_thesis: verum
end;
hence  tan is PI * ((k + 1) + 1) -periodic by Th1; ::_thesis: verum
end;
hence  S1[k + 1] ; ::_thesis: verum
end;
 for n being Nat holds S1[n] from NAT_1:sch_2(A1, A2);
hence  tan is PI * (k + 1) -periodic ; ::_thesis: verum
end;

theorem :: FUNCT_9:25
for i being non zero Integer holds tan is PI * i -periodic
proof
let i be non zero Integer; ::_thesis: tan is PI * i -periodic
 i in INT by INT_1:def_2;
then consider k being Element of NAT  such that
A1: ( i = k or i = - k ) by INT_1:def_1;
percases ( i = k or i = - k ) by A1;
suppose i = k ; ::_thesis: tan is PI * i -periodic
then  ex m being Nat st i = m + 1 by NAT_1:6;
hence  tan is PI * i -periodic by Lm12; ::_thesis: verum
end;
supposeA2: i = - k ; ::_thesis: tan is PI * i -periodic
then consider m being Nat such that
A3: - i = m + 1 by NAT_1:6;
 tan is PI * (m + 1) -periodic by Lm12;
then  tan is - (PI * (m + 1)) -periodic by Th14;
hence  tan is PI * i -periodic by A2, A3; ::_thesis: verum
end;
end;
end;

Lm13:  for k being Nat holds cot is PI * (k + 1) -periodic
proof
let k be Nat; ::_thesis: cot is PI * (k + 1) -periodic
defpred S1[ Nat] means  cot is PI * ($1 + 1) -periodic ;
A1: S1[ 0 ] by Lm11;
A2: for k being Nat st S1[k] holds
S1[k + 1]
proof
let k be Nat; ::_thesis: ( S1[k] implies S1[k + 1] )
assume A3: cot is PI * (k + 1) -periodic ; ::_thesis: S1[k + 1]
 cot is PI * ((k + 1) + 1) -periodic
proof
 for x being real number st x in dom cot holds
( x + (PI * ((k + 1) + 1)) in dom cot & x - (PI * ((k + 1) + 1)) in dom cot & cot . x = cot . (x + (PI * ((k + 1) + 1))) )
proof
let x be real number ; ::_thesis: ( x in dom cot implies ( x + (PI * ((k + 1) + 1)) in dom cot & x - (PI * ((k + 1) + 1)) in dom cot & cot . x = cot . (x + (PI * ((k + 1) + 1))) ) )
assume  x in dom cot ; ::_thesis: ( x + (PI * ((k + 1) + 1)) in dom cot & x - (PI * ((k + 1) + 1)) in dom cot & cot . x = cot . (x + (PI * ((k + 1) + 1))) )
then A4: ( x + (PI * (k + 1)) in dom cot & x - (PI * (k + 1)) in dom cot & cot . x = cot . (x + (PI * (k + 1))) ) by A3, Th1;
then  ( x + (PI * (k + 1)) in (dom cos) /\ ((dom sin) \ (sin " {0})) & x - (PI * (k + 1)) in (dom cos) /\ ((dom sin) \ (sin " {0})) ) by RFUNCT_1:def_1;
then  ( x + (PI * (k + 1)) in dom cos & x + (PI * (k + 1)) in (dom sin) \ (sin " {0}) & x - (PI * (k + 1)) in dom cos & x - (PI * (k + 1)) in (dom sin) \ (sin " {0}) ) by XBOOLE_0:def_4;
then  ( x + (PI * (k + 1)) in dom cos & x + (PI * (k + 1)) in dom sin & not x + (PI * (k + 1)) in sin " {0} & x - (PI * (k + 1)) in dom cos & x - (PI * (k + 1)) in dom sin & not x - (PI * (k + 1)) in sin " {0} ) by XBOOLE_0:def_5;
then  ( not sin . (x + (PI * (k + 1))) in {0} & not sin . (x - (PI * (k + 1))) in {0} ) by FUNCT_1:def_7;
then A5: ( sin . (x + (PI * (k + 1))) <> 0 & sin . (x - (PI * (k + 1))) <> 0 ) by TARSKI:def_1;
 sin . ((x + (PI * (k + 1))) + PI) = - (sin . (x + (PI * (k + 1)))) by SIN_COS:78;
then  not sin . ((x + (PI * (k + 1))) + PI) in {0} by A5, TARSKI:def_1;
then  ( (x + (PI * (k + 1))) + PI in dom cos & (x + (PI * (k + 1))) + PI in dom sin & not (x + (PI * (k + 1))) + PI in sin " {0} ) by FUNCT_1:def_7, SIN_COS:24;
then  ( (x + (PI * (k + 1))) + PI in dom cos & (x + (PI * (k + 1))) + PI in (dom sin) \ (sin " {0}) ) by XBOOLE_0:def_5;
then A6: (x + (PI * (k + 1))) + PI in (dom cos) /\ ((dom sin) \ (sin " {0})) by XBOOLE_0:def_4;
 sin . ((x - (PI * ((k + 1) + 1))) + PI) = - (sin . (x - (PI * ((k + 1) + 1)))) by SIN_COS:78;
then  sin . (x - (PI * ((k + 1) + 1))) = - (sin . (x - (PI * (k + 1)))) ;
then  not sin . (x - (PI * ((k + 1) + 1))) in {0} by A5, TARSKI:def_1;
then  ( x - (PI * ((k + 1) + 1)) in dom cos & x - (PI * ((k + 1) + 1)) in dom sin & not x - (PI * ((k + 1) + 1)) in sin " {0} ) by FUNCT_1:def_7, SIN_COS:24;
then  ( x - (PI * ((k + 1) + 1)) in dom cos & x - (PI * ((k + 1) + 1)) in (dom sin) \ (sin " {0}) ) by XBOOLE_0:def_5;
then A7: x - (PI * ((k + 1) + 1)) in (dom cos) /\ ((dom sin) \ (sin " {0})) by XBOOLE_0:def_4;
then  ( x + (PI * ((k + 1) + 1)) in dom cot & x - (PI * ((k + 1) + 1)) in dom cot ) by A6, RFUNCT_1:def_1;
then cot . (x + (PI * ((k + 1) + 1))) = (cos . ((x + (PI * (k + 1))) + PI)) / (sin . ((x + (PI * (k + 1))) + PI)) by RFUNCT_1:def_1
.= (- (cos . (x + (PI * (k + 1))))) / (sin . ((x + (PI * (k + 1))) + PI)) by SIN_COS:78
.= (- (cos . (x + (PI * (k + 1))))) / (- (sin . (x + (PI * (k + 1))))) by SIN_COS:78
.= (cos . (x + (PI * (k + 1)))) / (sin . (x + (PI * (k + 1)))) by XCMPLX_1:191
.= cot . x by A4, RFUNCT_1:def_1 ;
hence  ( x + (PI * ((k + 1) + 1)) in dom cot & x - (PI * ((k + 1) + 1)) in dom cot & cot . x = cot . (x + (PI * ((k + 1) + 1))) ) by A7, A6, RFUNCT_1:def_1; ::_thesis: verum
end;
hence  cot is PI * ((k + 1) + 1) -periodic by Th1; ::_thesis: verum
end;
hence  S1[k + 1] ; ::_thesis: verum
end;
 for n being Nat holds S1[n] from NAT_1:sch_2(A1, A2);
hence  cot is PI * (k + 1) -periodic ; ::_thesis: verum
end;

theorem :: FUNCT_9:26
for i being non zero Integer holds cot is PI * i -periodic
proof
let i be non zero Integer; ::_thesis: cot is PI * i -periodic
 i in INT by INT_1:def_2;
then consider k being Element of NAT  such that
A1: ( i = k or i = - k ) by INT_1:def_1;
percases ( i = k or i = - k ) by A1;
suppose i = k ; ::_thesis: cot is PI * i -periodic
then  ex m being Nat st i = m + 1 by NAT_1:6;
hence  cot is PI * i -periodic by Lm13; ::_thesis: verum
end;
supposeA2: i = - k ; ::_thesis: cot is PI * i -periodic
then consider m being Nat such that
A3: - i = m + 1 by NAT_1:6;
 cot is PI * (m + 1) -periodic by Lm13;
then  cot is - (PI * (m + 1)) -periodic by Th14;
hence  cot is PI * i -periodic by A2, A3; ::_thesis: verum
end;
end;
end;

Lm14:  |.sin.| is PI -periodic
proof
 for x being real number st x in dom |.sin.| holds
( x + PI in dom |.sin.| & x - PI in dom |.sin.| & |.sin.| . x = |.sin.| . (x + PI) )
proof
let x be real number ; ::_thesis: ( x in dom |.sin.| implies ( x + PI in dom |.sin.| & x - PI in dom |.sin.| & |.sin.| . x = |.sin.| . (x + PI) ) )
assume A1: x in dom |.sin.| ; ::_thesis: ( x + PI in dom |.sin.| & x - PI in dom |.sin.| & |.sin.| . x = |.sin.| . (x + PI) )
A2: ( x + PI in dom sin & x - PI in dom sin ) by SIN_COS:24;
then  ( x + PI in dom |.sin.| & x - PI in dom |.sin.| ) by VALUED_1:def_11;
then |.sin.| . (x + PI) = |.(sin (x + PI)).| by VALUED_1:def_11
.= |.(- (sin . x)).| by SIN_COS:78
.= |.(sin . x).| by COMPLEX1:52
.= |.sin.| . x by A1, VALUED_1:def_11 ;
hence  ( x + PI in dom |.sin.| & x - PI in dom |.sin.| & |.sin.| . x = |.sin.| . (x + PI) ) by A2, VALUED_1:def_11; ::_thesis: verum
end;
hence  |.sin.| is PI -periodic by Th1; ::_thesis: verum
end;

Lm15:  |.cos.| is PI -periodic
proof
 for x being real number st x in dom |.cos.| holds
( x + PI in dom |.cos.| & x - PI in dom |.cos.| & |.cos.| . x = |.cos.| . (x + PI) )
proof
let x be real number ; ::_thesis: ( x in dom |.cos.| implies ( x + PI in dom |.cos.| & x - PI in dom |.cos.| & |.cos.| . x = |.cos.| . (x + PI) ) )
assume A1: x in dom |.cos.| ; ::_thesis: ( x + PI in dom |.cos.| & x - PI in dom |.cos.| & |.cos.| . x = |.cos.| . (x + PI) )
A2: ( x + PI in dom cos & x - PI in dom cos ) by SIN_COS:24;
then  ( x + PI in dom |.cos.| & x - PI in dom |.cos.| ) by VALUED_1:def_11;
then |.cos.| . (x + PI) = |.(cos (x + PI)).| by VALUED_1:def_11
.= |.(- (cos . x)).| by SIN_COS:78
.= |.(cos . x).| by COMPLEX1:52
.= |.cos.| . x by A1, VALUED_1:def_11 ;
hence  ( x + PI in dom |.cos.| & x - PI in dom |.cos.| & |.cos.| . x = |.cos.| . (x + PI) ) by A2, VALUED_1:def_11; ::_thesis: verum
end;
hence  |.cos.| is PI -periodic by Th1; ::_thesis: verum
end;

Lm16:  for k being Nat holds |.sin.| is PI * (k + 1) -periodic
proof
let k be Nat; ::_thesis: |.sin.| is PI * (k + 1) -periodic
defpred S1[ Nat] means |.sin.| is PI * ($1 + 1) -periodic ;
A1: S1[ 0 ] by Lm14;
A2: for k being Nat st S1[k] holds
S1[k + 1]
proof
let k be Nat; ::_thesis: ( S1[k] implies S1[k + 1] )
assume A3: |.sin.| is PI * (k + 1) -periodic ; ::_thesis: S1[k + 1]
 |.sin.| is PI * ((k + 1) + 1) -periodic
proof
 for x being real number st x in dom |.sin.| holds
( x + (PI * ((k + 1) + 1)) in dom |.sin.| & x - (PI * ((k + 1) + 1)) in dom |.sin.| & |.sin.| . x = |.sin.| . (x + (PI * ((k + 1) + 1))) )
proof
let x be real number ; ::_thesis: ( x in dom |.sin.| implies ( x + (PI * ((k + 1) + 1)) in dom |.sin.| & x - (PI * ((k + 1) + 1)) in dom |.sin.| & |.sin.| . x = |.sin.| . (x + (PI * ((k + 1) + 1))) ) )
assume A4: x in dom |.sin.| ; ::_thesis: ( x + (PI * ((k + 1) + 1)) in dom |.sin.| & x - (PI * ((k + 1) + 1)) in dom |.sin.| & |.sin.| . x = |.sin.| . (x + (PI * ((k + 1) + 1))) )
then A5: ( x + (PI * (k + 1)) in dom |.sin.| & x - (PI * (k + 1)) in dom |.sin.| ) by A3, Th1;
A6: ( x + (PI * ((k + 1) + 1)) in dom sin & x - (PI * ((k + 1) + 1)) in dom sin ) by SIN_COS:24;
then  ( x + (PI * ((k + 1) + 1)) in dom |.sin.| & x - (PI * ((k + 1) + 1)) in dom |.sin.| ) by VALUED_1:def_11;
then |.sin.| . (x + (PI * ((k + 1) + 1))) = |.(sin . ((x + (PI * (k + 1))) + PI)).| by VALUED_1:def_11
.= |.(- (sin . (x + (PI * (k + 1))))).| by SIN_COS:78
.= |.(sin . (x + (PI * (k + 1)))).| by COMPLEX1:52
.= |.sin.| . (x + (PI * (k + 1))) by A5, VALUED_1:def_11 ;
hence  ( x + (PI * ((k + 1) + 1)) in dom |.sin.| & x - (PI * ((k + 1) + 1)) in dom |.sin.| & |.sin.| . x = |.sin.| . (x + (PI * ((k + 1) + 1))) ) by A3, Th1, A4, A6, VALUED_1:def_11; ::_thesis: verum
end;
hence  |.sin.| is PI * ((k + 1) + 1) -periodic by Th1; ::_thesis: verum
end;
hence  S1[k + 1] ; ::_thesis: verum
end;
 for n being Nat holds S1[n] from NAT_1:sch_2(A1, A2);
hence  |.sin.| is PI * (k + 1) -periodic ; ::_thesis: verum
end;

theorem :: FUNCT_9:27
for i being non zero Integer holds |.sin.| is PI * i -periodic
proof
let i be non zero Integer; ::_thesis: |.sin.| is PI * i -periodic
 i in INT by INT_1:def_2;
then consider k being Element of NAT  such that
A1: ( i = k or i = - k ) by INT_1:def_1;
percases ( i = k or i = - k ) by A1;
suppose i = k ; ::_thesis: |.sin.| is PI * i -periodic
then  ex m being Nat st i = m + 1 by NAT_1:6;
hence  |.sin.| is PI * i -periodic by Lm16; ::_thesis: verum
end;
supposeA2: i = - k ; ::_thesis: |.sin.| is PI * i -periodic
then consider m being Nat such that
A3: - i = m + 1 by NAT_1:6;
 |.sin.| is PI * (m + 1) -periodic by Lm16;
then  |.sin.| is - (PI * (m + 1)) -periodic by Th14;
hence  |.sin.| is PI * i -periodic by A2, A3; ::_thesis: verum
end;
end;
end;

Lm17:  for k being Nat holds |.cos.| is PI * (k + 1) -periodic
proof
let k be Nat; ::_thesis: |.cos.| is PI * (k + 1) -periodic
defpred S1[ Nat] means |.cos.| is PI * ($1 + 1) -periodic ;
A1: S1[ 0 ] by Lm15;
A2: for k being Nat st S1[k] holds
S1[k + 1]
proof
let k be Nat; ::_thesis: ( S1[k] implies S1[k + 1] )
assume A3: |.cos.| is PI * (k + 1) -periodic ; ::_thesis: S1[k + 1]
 |.cos.| is PI * ((k + 1) + 1) -periodic
proof
 for x being real number st x in dom |.cos.| holds
( x + (PI * ((k + 1) + 1)) in dom |.cos.| & x - (PI * ((k + 1) + 1)) in dom |.cos.| & |.cos.| . x = |.cos.| . (x + (PI * ((k + 1) + 1))) )
proof
let x be real number ; ::_thesis: ( x in dom |.cos.| implies ( x + (PI * ((k + 1) + 1)) in dom |.cos.| & x - (PI * ((k + 1) + 1)) in dom |.cos.| & |.cos.| . x = |.cos.| . (x + (PI * ((k + 1) + 1))) ) )
assume A4: x in dom |.cos.| ; ::_thesis: ( x + (PI * ((k + 1) + 1)) in dom |.cos.| & x - (PI * ((k + 1) + 1)) in dom |.cos.| & |.cos.| . x = |.cos.| . (x + (PI * ((k + 1) + 1))) )
then A5: ( x + (PI * (k + 1)) in dom |.cos.| & x - (PI * (k + 1)) in dom |.cos.| ) by A3, Th1;
A6: ( x + (PI * ((k + 1) + 1)) in dom cos & x - (PI * ((k + 1) + 1)) in dom cos ) by SIN_COS:24;
then  ( x + (PI * ((k + 1) + 1)) in dom |.cos.| & x - (PI * ((k + 1) + 1)) in dom |.cos.| ) by VALUED_1:def_11;
then |.cos.| . (x + (PI * ((k + 1) + 1))) = |.(cos . ((x + (PI * (k + 1))) + PI)).| by VALUED_1:def_11
.= |.(- (cos . (x + (PI * (k + 1))))).| by SIN_COS:78
.= |.(cos . (x + (PI * (k + 1)))).| by COMPLEX1:52
.= |.cos.| . (x + (PI * (k + 1))) by A5, VALUED_1:def_11 ;
hence  ( x + (PI * ((k + 1) + 1)) in dom |.cos.| & x - (PI * ((k + 1) + 1)) in dom |.cos.| & |.cos.| . x = |.cos.| . (x + (PI * ((k + 1) + 1))) ) by A3, Th1, A4, A6, VALUED_1:def_11; ::_thesis: verum
end;
hence  |.cos.| is PI * ((k + 1) + 1) -periodic by Th1; ::_thesis: verum
end;
hence  S1[k + 1] ; ::_thesis: verum
end;
 for n being Nat holds S1[n] from NAT_1:sch_2(A1, A2);
hence  |.cos.| is PI * (k + 1) -periodic ; ::_thesis: verum
end;

theorem :: FUNCT_9:28
for i being non zero Integer holds |.cos.| is PI * i -periodic
proof
let i be non zero Integer; ::_thesis: |.cos.| is PI * i -periodic
 i in INT by INT_1:def_2;
then consider k being Element of NAT  such that
A1: ( i = k or i = - k ) by INT_1:def_1;
percases ( i = k or i = - k ) by A1;
suppose i = k ; ::_thesis: |.cos.| is PI * i -periodic
then  ex m being Nat st i = m + 1 by NAT_1:6;
hence  |.cos.| is PI * i -periodic by Lm17; ::_thesis: verum
end;
supposeA2: i = - k ; ::_thesis: |.cos.| is PI * i -periodic
then consider m being Nat such that
A3: - i = m + 1 by NAT_1:6;
 |.cos.| is PI * (m + 1) -periodic by Lm17;
then  |.cos.| is - (PI * (m + 1)) -periodic by Th14;
hence  |.cos.| is PI * i -periodic by A2, A3; ::_thesis: verum
end;
end;
end;

Lm18:  |.sin.| + |.cos.| is PI / 2 -periodic
proof
 for x being real number st x in dom (|.sin.| + |.cos.|) holds
( x + (PI / 2) in dom (|.sin.| + |.cos.|) & x - (PI / 2) in dom (|.sin.| + |.cos.|) & (|.sin.| + |.cos.|) . x = (|.sin.| + |.cos.|) . (x + (PI / 2)) )
proof
let x be real number ; ::_thesis: ( x in dom (|.sin.| + |.cos.|) implies ( x + (PI / 2) in dom (|.sin.| + |.cos.|) & x - (PI / 2) in dom (|.sin.| + |.cos.|) & (|.sin.| + |.cos.|) . x = (|.sin.| + |.cos.|) . (x + (PI / 2)) ) )
assume A1: x in dom (|.sin.| + |.cos.|) ; ::_thesis: ( x + (PI / 2) in dom (|.sin.| + |.cos.|) & x - (PI / 2) in dom (|.sin.| + |.cos.|) & (|.sin.| + |.cos.|) . x = (|.sin.| + |.cos.|) . (x + (PI / 2)) )
A2: ( dom (|.sin.| + |.cos.|) = REAL & dom |.sin.| = REAL & dom |.cos.| = REAL )
proof
A3: dom (|.sin.| + |.cos.|) = (dom |.sin.|) /\ (dom |.cos.|) by VALUED_1:def_1;
 ( dom |.sin.| = REAL & dom |.cos.| = REAL ) by SIN_COS:24, VALUED_1:def_11;
hence  ( dom (|.sin.| + |.cos.|) = REAL & dom |.sin.| = REAL & dom |.cos.| = REAL ) by A3; ::_thesis: verum
end;
then (|.sin.| + |.cos.|) . (x + (PI / 2)) = (|.sin.| . (x + (PI / 2))) + (|.cos.| . (x + (PI / 2))) by VALUED_1:def_1
.= |.(sin . (x + (PI / 2))).| + (|.cos.| . (x + (PI / 2))) by A2, VALUED_1:def_11
.= |.(sin . (x + (PI / 2))).| + |.(cos . (x + (PI / 2))).| by A2, VALUED_1:def_11
.= |.(cos . x).| + |.(cos . (x + (PI / 2))).| by SIN_COS:78
.= |.(cos . x).| + |.(- (sin . x)).| by SIN_COS:78
.= |.(cos . x).| + |.(sin . x).| by COMPLEX1:52
.= (|.cos.| . x) + |.(sin . x).| by A1, A2, VALUED_1:def_11
.= (|.cos.| . x) + (|.sin.| . x) by A1, A2, VALUED_1:def_11
.= (|.sin.| + |.cos.|) . x by A1, VALUED_1:def_1 ;
hence  ( x + (PI / 2) in dom (|.sin.| + |.cos.|) & x - (PI / 2) in dom (|.sin.| + |.cos.|) & (|.sin.| + |.cos.|) . x = (|.sin.| + |.cos.|) . (x + (PI / 2)) ) by A2; ::_thesis: verum
end;
hence  |.sin.| + |.cos.| is PI / 2 -periodic by Th1; ::_thesis: verum
end;

Lm19:  for k being Nat holds |.sin.| + |.cos.| is (PI / 2) * (k + 1) -periodic
proof
let k be Nat; ::_thesis: |.sin.| + |.cos.| is (PI / 2) * (k + 1) -periodic
defpred S1[ Nat] means |.sin.| + |.cos.| is (PI / 2) * ($1 + 1) -periodic ;
A1: S1[ 0 ] by Lm18;
A2: for k being Nat st S1[k] holds
S1[k + 1]
proof
let k be Nat; ::_thesis: ( S1[k] implies S1[k + 1] )
assume A3: |.sin.| + |.cos.| is (PI / 2) * (k + 1) -periodic ; ::_thesis: S1[k + 1]
A4: ( dom (|.sin.| + |.cos.|) = REAL & dom |.sin.| = REAL & dom |.cos.| = REAL )
proof
A5: dom (|.sin.| + |.cos.|) = (dom |.sin.|) /\ (dom |.cos.|) by VALUED_1:def_1;
 ( dom |.sin.| = REAL & dom |.cos.| = REAL ) by SIN_COS:24, VALUED_1:def_11;
hence  ( dom (|.sin.| + |.cos.|) = REAL & dom |.sin.| = REAL & dom |.cos.| = REAL ) by A5; ::_thesis: verum
end;
 |.sin.| + |.cos.| is (PI / 2) * ((k + 1) + 1) -periodic
proof
 for x being real number st x in dom (|.sin.| + |.cos.|) holds
( x + ((PI / 2) * ((k + 1) + 1)) in dom (|.sin.| + |.cos.|) & x - ((PI / 2) * ((k + 1) + 1)) in dom (|.sin.| + |.cos.|) & (|.sin.| + |.cos.|) . x = (|.sin.| + |.cos.|) . (x + ((PI / 2) * ((k + 1) + 1))) )
proof
let x be real number ; ::_thesis: ( x in dom (|.sin.| + |.cos.|) implies ( x + ((PI / 2) * ((k + 1) + 1)) in dom (|.sin.| + |.cos.|) & x - ((PI / 2) * ((k + 1) + 1)) in dom (|.sin.| + |.cos.|) & (|.sin.| + |.cos.|) . x = (|.sin.| + |.cos.|) . (x + ((PI / 2) * ((k + 1) + 1))) ) )
assume A6: x in dom (|.sin.| + |.cos.|) ; ::_thesis: ( x + ((PI / 2) * ((k + 1) + 1)) in dom (|.sin.| + |.cos.|) & x - ((PI / 2) * ((k + 1) + 1)) in dom (|.sin.| + |.cos.|) & (|.sin.| + |.cos.|) . x = (|.sin.| + |.cos.|) . (x + ((PI / 2) * ((k + 1) + 1))) )
(|.sin.| + |.cos.|) . (x + ((PI / 2) * ((k + 1) + 1))) = (|.sin.| . (x + ((PI / 2) * ((k + 1) + 1)))) + (|.cos.| . (x + ((PI / 2) * ((k + 1) + 1)))) by A4, VALUED_1:def_1
.= |.(sin . (x + ((PI / 2) * ((k + 1) + 1)))).| + (|.cos.| . (x + ((PI / 2) * ((k + 1) + 1)))) by A4, VALUED_1:def_11
.= |.(sin . ((x + ((PI / 2) * (k + 1))) + (PI / 2))).| + |.(cos . ((x + ((PI / 2) * (k + 1))) + (PI / 2))).| by A4, VALUED_1:def_11
.= |.(cos . (x + ((PI / 2) * (k + 1)))).| + |.(cos . ((x + ((PI / 2) * (k + 1))) + (PI / 2))).| by SIN_COS:78
.= |.(cos . (x + ((PI / 2) * (k + 1)))).| + |.(- (sin . (x + ((PI / 2) * (k + 1))))).| by SIN_COS:78
.= |.(cos . (x + ((PI / 2) * (k + 1)))).| + |.(sin . (x + ((PI / 2) * (k + 1)))).| by COMPLEX1:52
.= (|.cos.| . (x + ((PI / 2) * (k + 1)))) + |.(sin . (x + ((PI / 2) * (k + 1)))).| by A4, VALUED_1:def_11
.= (|.cos.| . (x + ((PI / 2) * (k + 1)))) + (|.sin.| . (x + ((PI / 2) * (k + 1)))) by A4, VALUED_1:def_11
.= (|.sin.| + |.cos.|) . (x + ((PI / 2) * (k + 1))) by A4, VALUED_1:def_1 ;
hence  ( x + ((PI / 2) * ((k + 1) + 1)) in dom (|.sin.| + |.cos.|) & x - ((PI / 2) * ((k + 1) + 1)) in dom (|.sin.| + |.cos.|) & (|.sin.| + |.cos.|) . x = (|.sin.| + |.cos.|) . (x + ((PI / 2) * ((k + 1) + 1))) ) by A3, Th1, A4, A6; ::_thesis: verum
end;
hence  |.sin.| + |.cos.| is (PI / 2) * ((k + 1) + 1) -periodic by Th1; ::_thesis: verum
end;
hence  S1[k + 1] ; ::_thesis: verum
end;
 for n being Nat holds S1[n] from NAT_1:sch_2(A1, A2);
hence  |.sin.| + |.cos.| is (PI / 2) * (k + 1) -periodic ; ::_thesis: verum
end;

theorem :: FUNCT_9:29
for i being non zero Integer holds |.sin.| + |.cos.| is (PI / 2) * i -periodic
proof
let i be non zero Integer; ::_thesis: |.sin.| + |.cos.| is (PI / 2) * i -periodic
 i in INT by INT_1:def_2;
then consider k being Element of NAT  such that
A1: ( i = k or i = - k ) by INT_1:def_1;
percases ( i = k or i = - k ) by A1;
suppose i = k ; ::_thesis: |.sin.| + |.cos.| is (PI / 2) * i -periodic
then  ex m being Nat st i = m + 1 by NAT_1:6;
hence  |.sin.| + |.cos.| is (PI / 2) * i -periodic by Lm19; ::_thesis: verum
end;
supposeA2: i = - k ; ::_thesis: |.sin.| + |.cos.| is (PI / 2) * i -periodic
then consider m being Nat such that
A3: - i = m + 1 by NAT_1:6;
 |.sin.| + |.cos.| is (PI / 2) * (m + 1) -periodic by Lm19;
then  |.sin.| + |.cos.| is - ((PI / 2) * (m + 1)) -periodic by Th14;
hence  |.sin.| + |.cos.| is (PI / 2) * i -periodic by A2, A3; ::_thesis: verum
end;
end;
end;

Lm20:  sin ^2 is PI -periodic
proof
 for x being real number st x in dom (sin ^2) holds
( x + PI in dom (sin ^2) & x - PI in dom (sin ^2) & (sin ^2) . x = (sin ^2) . (x + PI) )
proof
let x be real number ; ::_thesis: ( x in dom (sin ^2) implies ( x + PI in dom (sin ^2) & x - PI in dom (sin ^2) & (sin ^2) . x = (sin ^2) . (x + PI) ) )
assume  x in dom (sin ^2) ; ::_thesis: ( x + PI in dom (sin ^2) & x - PI in dom (sin ^2) & (sin ^2) . x = (sin ^2) . (x + PI) )
A1: ( x + PI in dom sin & x - PI in dom sin ) by SIN_COS:24;
(sin ^2) . (x + PI) = (sin (x + PI)) ^2 by VALUED_1:11
.= (- (sin . x)) ^2 by SIN_COS:78
.= (sin . x) ^2
.= (sin ^2) . x by VALUED_1:11 ;
hence  ( x + PI in dom (sin ^2) & x - PI in dom (sin ^2) & (sin ^2) . x = (sin ^2) . (x + PI) ) by A1, VALUED_1:11; ::_thesis: verum
end;
hence  sin ^2 is PI -periodic by Th1; ::_thesis: verum
end;

Lm21:  cos ^2 is PI -periodic
proof
 for x being real number st x in dom (cos ^2) holds
( x + PI in dom (cos ^2) & x - PI in dom (cos ^2) & (cos ^2) . x = (cos ^2) . (x + PI) )
proof
let x be real number ; ::_thesis: ( x in dom (cos ^2) implies ( x + PI in dom (cos ^2) & x - PI in dom (cos ^2) & (cos ^2) . x = (cos ^2) . (x + PI) ) )
assume  x in dom (cos ^2) ; ::_thesis: ( x + PI in dom (cos ^2) & x - PI in dom (cos ^2) & (cos ^2) . x = (cos ^2) . (x + PI) )
A1: ( x + PI in dom cos & x - PI in dom cos ) by SIN_COS:24;
(cos ^2) . (x + PI) = (cos (x + PI)) ^2 by VALUED_1:11
.= (- (cos . x)) ^2 by SIN_COS:78
.= (cos . x) ^2
.= (cos ^2) . x by VALUED_1:11 ;
hence  ( x + PI in dom (cos ^2) & x - PI in dom (cos ^2) & (cos ^2) . x = (cos ^2) . (x + PI) ) by A1, VALUED_1:11; ::_thesis: verum
end;
hence  cos ^2 is PI -periodic by Th1; ::_thesis: verum
end;

Lm22:  for k being Nat holds sin ^2 is PI * (k + 1) -periodic
proof
let k be Nat; ::_thesis: sin ^2 is PI * (k + 1) -periodic
defpred S1[ Nat] means sin ^2 is PI * ($1 + 1) -periodic ;
A1: S1[ 0 ] by Lm20;
A2: for k being Nat st S1[k] holds
S1[k + 1]
proof
let k be Nat; ::_thesis: ( S1[k] implies S1[k + 1] )
assume A3: sin ^2 is PI * (k + 1) -periodic ; ::_thesis: S1[k + 1]
 sin ^2 is PI * ((k + 1) + 1) -periodic
proof
 for x being real number st x in dom (sin ^2) holds
( x + (PI * ((k + 1) + 1)) in dom (sin ^2) & x - (PI * ((k + 1) + 1)) in dom (sin ^2) & (sin ^2) . x = (sin ^2) . (x + (PI * ((k + 1) + 1))) )
proof
let x be real number ; ::_thesis: ( x in dom (sin ^2) implies ( x + (PI * ((k + 1) + 1)) in dom (sin ^2) & x - (PI * ((k + 1) + 1)) in dom (sin ^2) & (sin ^2) . x = (sin ^2) . (x + (PI * ((k + 1) + 1))) ) )
assume A4: x in dom (sin ^2) ; ::_thesis: ( x + (PI * ((k + 1) + 1)) in dom (sin ^2) & x - (PI * ((k + 1) + 1)) in dom (sin ^2) & (sin ^2) . x = (sin ^2) . (x + (PI * ((k + 1) + 1))) )
A5: ( x + (PI * ((k + 1) + 1)) in dom sin & x - (PI * ((k + 1) + 1)) in dom sin ) by SIN_COS:24;
(sin ^2) . (x + (PI * ((k + 1) + 1))) = (sin . ((x + (PI * (k + 1))) + PI)) ^2 by VALUED_1:11
.= (- (sin . (x + (PI * (k + 1))))) ^2 by SIN_COS:78
.= (sin . (x + (PI * (k + 1)))) ^2
.= (sin ^2) . (x + (PI * (k + 1))) by VALUED_1:11 ;
hence  ( x + (PI * ((k + 1) + 1)) in dom (sin ^2) & x - (PI * ((k + 1) + 1)) in dom (sin ^2) & (sin ^2) . x = (sin ^2) . (x + (PI * ((k + 1) + 1))) ) by A3, Th1, A4, A5, VALUED_1:11; ::_thesis: verum
end;
hence  sin ^2 is PI * ((k + 1) + 1) -periodic by Th1; ::_thesis: verum
end;
hence  S1[k + 1] ; ::_thesis: verum
end;
 for n being Nat holds S1[n] from NAT_1:sch_2(A1, A2);
hence  sin ^2 is PI * (k + 1) -periodic ; ::_thesis: verum
end;

theorem :: FUNCT_9:30
for i being non zero Integer holds sin ^2 is PI * i -periodic
proof
let i be non zero Integer; ::_thesis: sin ^2 is PI * i -periodic
 i in INT by INT_1:def_2;
then consider k being Element of NAT  such that
A1: ( i = k or i = - k ) by INT_1:def_1;
percases ( i = k or i = - k ) by A1;
suppose i = k ; ::_thesis: sin ^2 is PI * i -periodic
then  ex m being Nat st i = m + 1 by NAT_1:6;
hence  sin ^2 is PI * i -periodic by Lm22; ::_thesis: verum
end;
supposeA2: i = - k ; ::_thesis: sin ^2 is PI * i -periodic
then consider m being Nat such that
A3: - i = m + 1 by NAT_1:6;
 sin ^2 is PI * (m + 1) -periodic by Lm22;
then  sin ^2 is - (PI * (m + 1)) -periodic by Th14;
hence  sin ^2 is PI * i -periodic by A2, A3; ::_thesis: verum
end;
end;
end;

Lm23:  for k being Nat holds cos ^2 is PI * (k + 1) -periodic
proof
let k be Nat; ::_thesis: cos ^2 is PI * (k + 1) -periodic
defpred S1[ Nat] means cos ^2 is PI * ($1 + 1) -periodic ;
A1: S1[ 0 ] by Lm21;
A2: for k being Nat st S1[k] holds
S1[k + 1]
proof
let k be Nat; ::_thesis: ( S1[k] implies S1[k + 1] )
assume A3: cos ^2 is PI * (k + 1) -periodic ; ::_thesis: S1[k + 1]
 cos ^2 is PI * ((k + 1) + 1) -periodic
proof
 for x being real number st x in dom (cos ^2) holds
( x + (PI * ((k + 1) + 1)) in dom (cos ^2) & x - (PI * ((k + 1) + 1)) in dom (cos ^2) & (cos ^2) . x = (cos ^2) . (x + (PI * ((k + 1) + 1))) )
proof
let x be real number ; ::_thesis: ( x in dom (cos ^2) implies ( x + (PI * ((k + 1) + 1)) in dom (cos ^2) & x - (PI * ((k + 1) + 1)) in dom (cos ^2) & (cos ^2) . x = (cos ^2) . (x + (PI * ((k + 1) + 1))) ) )
assume A4: x in dom (cos ^2) ; ::_thesis: ( x + (PI * ((k + 1) + 1)) in dom (cos ^2) & x - (PI * ((k + 1) + 1)) in dom (cos ^2) & (cos ^2) . x = (cos ^2) . (x + (PI * ((k + 1) + 1))) )
A5: ( x + (PI * ((k + 1) + 1)) in dom cos & x - (PI * ((k + 1) + 1)) in dom cos ) by SIN_COS:24;
(cos ^2) . (x + (PI * ((k + 1) + 1))) = (cos . ((x + (PI * (k + 1))) + PI)) ^2 by VALUED_1:11
.= (- (cos . (x + (PI * (k + 1))))) ^2 by SIN_COS:78
.= (cos . (x + (PI * (k + 1)))) ^2
.= (cos ^2) . (x + (PI * (k + 1))) by VALUED_1:11 ;
hence  ( x + (PI * ((k + 1) + 1)) in dom (cos ^2) & x - (PI * ((k + 1) + 1)) in dom (cos ^2) & (cos ^2) . x = (cos ^2) . (x + (PI * ((k + 1) + 1))) ) by A3, Th1, A4, A5, VALUED_1:11; ::_thesis: verum
end;
hence  cos ^2 is PI * ((k + 1) + 1) -periodic by Th1; ::_thesis: verum
end;
hence  S1[k + 1] ; ::_thesis: verum
end;
 for n being Nat holds S1[n] from NAT_1:sch_2(A1, A2);
hence  cos ^2 is PI * (k + 1) -periodic ; ::_thesis: verum
end;

theorem :: FUNCT_9:31
for i being non zero Integer holds cos ^2 is PI * i -periodic
proof
let i be non zero Integer; ::_thesis: cos ^2 is PI * i -periodic
 i in INT by INT_1:def_2;
then consider k being Element of NAT  such that
A1: ( i = k or i = - k ) by INT_1:def_1;
percases ( i = k or i = - k ) by A1;
suppose i = k ; ::_thesis: cos ^2 is PI * i -periodic
then  ex m being Nat st i = m + 1 by NAT_1:6;
hence  cos ^2 is PI * i -periodic by Lm23; ::_thesis: verum
end;
supposeA2: i = - k ; ::_thesis: cos ^2 is PI * i -periodic
then consider m being Nat such that
A3: - i = m + 1 by NAT_1:6;
 cos ^2 is PI * (m + 1) -periodic by Lm23;
then  cos ^2 is - (PI * (m + 1)) -periodic by Th14;
hence  cos ^2 is PI * i -periodic by A2, A3; ::_thesis: verum
end;
end;
end;

Lm24:  sin (#) cos is PI -periodic
proof
 for x being real number st x in dom (sin (#) cos) holds
( x + PI in dom (sin (#) cos) & x - PI in dom (sin (#) cos) & (sin (#) cos) . x = (sin (#) cos) . (x + PI) )
proof
let x be real number ; ::_thesis: ( x in dom (sin (#) cos) implies ( x + PI in dom (sin (#) cos) & x - PI in dom (sin (#) cos) & (sin (#) cos) . x = (sin (#) cos) . (x + PI) ) )
assume A1: x in dom (sin (#) cos) ; ::_thesis: ( x + PI in dom (sin (#) cos) & x - PI in dom (sin (#) cos) & (sin (#) cos) . x = (sin (#) cos) . (x + PI) )
A2: ( x + PI in (dom sin) /\ (dom cos) & x - PI in (dom sin) /\ (dom cos) ) by SIN_COS:24;
then  ( x + PI in dom (sin (#) cos) & x - PI in dom (sin (#) cos) ) by VALUED_1:def_4;
then (sin (#) cos) . (x + PI) = (sin . (x + PI)) * (cos . (x + PI)) by VALUED_1:def_4
.= (- (sin . x)) * (cos . (x + PI)) by SIN_COS:78
.= (- (sin . x)) * (- (cos . x)) by SIN_COS:78
.= (sin . x) * (cos . x)
.= (sin (#) cos) . x by A1, VALUED_1:def_4 ;
hence  ( x + PI in dom (sin (#) cos) & x - PI in dom (sin (#) cos) & (sin (#) cos) . x = (sin (#) cos) . (x + PI) ) by A2, VALUED_1:def_4; ::_thesis: verum
end;
hence  sin (#) cos is PI -periodic by Th1; ::_thesis: verum
end;

Lm25:  for k being Nat holds sin (#) cos is PI * (k + 1) -periodic
proof
let k be Nat; ::_thesis: sin (#) cos is PI * (k + 1) -periodic
defpred S1[ Nat] means sin (#) cos is PI * ($1 + 1) -periodic ;
A1: S1[ 0 ] by Lm24;
A2: for k being Nat st S1[k] holds
S1[k + 1]
proof
let k be Nat; ::_thesis: ( S1[k] implies S1[k + 1] )
assume A3: sin (#) cos is PI * (k + 1) -periodic ; ::_thesis: S1[k + 1]
 sin (#) cos is PI * ((k + 1) + 1) -periodic
proof
 for x being real number st x in dom (sin (#) cos) holds
( x + (PI * ((k + 1) + 1)) in dom (sin (#) cos) & x - (PI * ((k + 1) + 1)) in dom (sin (#) cos) & (sin (#) cos) . x = (sin (#) cos) . (x + (PI * ((k + 1) + 1))) )
proof
let x be real number ; ::_thesis: ( x in dom (sin (#) cos) implies ( x + (PI * ((k + 1) + 1)) in dom (sin (#) cos) & x - (PI * ((k + 1) + 1)) in dom (sin (#) cos) & (sin (#) cos) . x = (sin (#) cos) . (x + (PI * ((k + 1) + 1))) ) )
assume A4: x in dom (sin (#) cos) ; ::_thesis: ( x + (PI * ((k + 1) + 1)) in dom (sin (#) cos) & x - (PI * ((k + 1) + 1)) in dom (sin (#) cos) & (sin (#) cos) . x = (sin (#) cos) . (x + (PI * ((k + 1) + 1))) )
then A5: ( x + (PI * (k + 1)) in dom (sin (#) cos) & x - (PI * (k + 1)) in dom (sin (#) cos) ) by A3, Th1;
A6: ( x + (PI * ((k + 1) + 1)) in (dom cos) /\ (dom sin) & x - (PI * ((k + 1) + 1)) in (dom cos) /\ (dom sin) ) by SIN_COS:24;
then  ( x + (PI * ((k + 1) + 1)) in dom (sin (#) cos) & x - (PI * ((k + 1) + 1)) in dom (sin (#) cos) ) by VALUED_1:def_4;
then (sin (#) cos) . (x + (PI * ((k + 1) + 1))) = (sin . ((x + (PI * (k + 1))) + PI)) * (cos . ((x + (PI * (k + 1))) + PI)) by VALUED_1:def_4
.= (- (sin . (x + (PI * (k + 1))))) * (cos . ((x + (PI * (k + 1))) + PI)) by SIN_COS:78
.= (- (sin . (x + (PI * (k + 1))))) * (- (cos . (x + (PI * (k + 1))))) by SIN_COS:78
.= (sin . (x + (PI * (k + 1)))) * (cos . (x + (PI * (k + 1))))
.= (sin (#) cos) . (x + (PI * (k + 1))) by A5, VALUED_1:def_4 ;
hence  ( x + (PI * ((k + 1) + 1)) in dom (sin (#) cos) & x - (PI * ((k + 1) + 1)) in dom (sin (#) cos) & (sin (#) cos) . x = (sin (#) cos) . (x + (PI * ((k + 1) + 1))) ) by A3, Th1, A4, A6, VALUED_1:def_4; ::_thesis: verum
end;
hence  sin (#) cos is PI * ((k + 1) + 1) -periodic by Th1; ::_thesis: verum
end;
hence  S1[k + 1] ; ::_thesis: verum
end;
 for n being Nat holds S1[n] from NAT_1:sch_2(A1, A2);
hence  sin (#) cos is PI * (k + 1) -periodic ; ::_thesis: verum
end;

theorem :: FUNCT_9:32
for i being non zero Integer holds sin (#) cos is PI * i -periodic
proof
let i be non zero Integer; ::_thesis: sin (#) cos is PI * i -periodic
 i in INT by INT_1:def_2;
then consider k being Element of NAT  such that
A1: ( i = k or i = - k ) by INT_1:def_1;
percases ( i = k or i = - k ) by A1;
suppose i = k ; ::_thesis: sin (#) cos is PI * i -periodic
then  ex m being Nat st i = m + 1 by NAT_1:6;
hence  sin (#) cos is PI * i -periodic by Lm25; ::_thesis: verum
end;
supposeA2: i = - k ; ::_thesis: sin (#) cos is PI * i -periodic
then consider m being Nat such that
A3: - i = m + 1 by NAT_1:6;
 sin (#) cos is PI * (m + 1) -periodic by Lm25;
then  sin (#) cos is - (PI * (m + 1)) -periodic by Th14;
hence  sin (#) cos is PI * i -periodic by A2, A3; ::_thesis: verum
end;
end;
end;

Lm26:  for b, a being real number holds b + (a (#) sin) is 2 * PI -periodic
proof
let b, a be real number ; ::_thesis: b + (a (#) sin) is 2 * PI -periodic
 for x being real number st x in dom (b + (a (#) sin)) holds
( x + (2 * PI) in dom (b + (a (#) sin)) & x - (2 * PI) in dom (b + (a (#) sin)) & (b + (a (#) sin)) . x = (b + (a (#) sin)) . (x + (2 * PI)) )
proof
let x be real number ; ::_thesis: ( x in dom (b + (a (#) sin)) implies ( x + (2 * PI) in dom (b + (a (#) sin)) & x - (2 * PI) in dom (b + (a (#) sin)) & (b + (a (#) sin)) . x = (b + (a (#) sin)) . (x + (2 * PI)) ) )
assume  x in dom (b + (a (#) sin)) ; ::_thesis: ( x + (2 * PI) in dom (b + (a (#) sin)) & x - (2 * PI) in dom (b + (a (#) sin)) & (b + (a (#) sin)) . x = (b + (a (#) sin)) . (x + (2 * PI)) )
 x in REAL by XREAL_0:def_1;
then A1: x in dom (a (#) sin) by SIN_COS:24, VALUED_1:def_5;
then A2: ( x in dom (b + (a (#) sin)) & x in dom (b + (a (#) sin)) ) by VALUED_1:def_2;
 ( x + (2 * PI) in dom sin & x - (2 * PI) in dom sin ) by SIN_COS:24;
then A3: ( x + (2 * PI) in dom (a (#) sin) & x - (2 * PI) in dom (a (#) sin) ) by VALUED_1:def_5;
then  ( x + (2 * PI) in dom (b + (a (#) sin)) & x - (2 * PI) in dom (b + (a (#) sin)) ) by VALUED_1:def_2;
then (b + (a (#) sin)) . (x + (2 * PI)) = b + ((a (#) sin) . (x + (2 * PI))) by VALUED_1:def_2
.= b + (a * (sin . (x + (2 * PI)))) by A3, VALUED_1:def_5
.= b + (a * (sin . x)) by SIN_COS:78
.= b + ((a (#) sin) . x) by A1, VALUED_1:def_5
.= (b + (a (#) sin)) . x by A2, VALUED_1:def_2 ;
hence  ( x + (2 * PI) in dom (b + (a (#) sin)) & x - (2 * PI) in dom (b + (a (#) sin)) & (b + (a (#) sin)) . x = (b + (a (#) sin)) . (x + (2 * PI)) ) by A3, VALUED_1:def_2; ::_thesis: verum
end;
hence  b + (a (#) sin) is 2 * PI -periodic by Th1; ::_thesis: verum
end;

Lm27:  for b, a being real number holds b + (a (#) cos) is 2 * PI -periodic
proof
let b, a be real number ; ::_thesis: b + (a (#) cos) is 2 * PI -periodic
 for x being real number st x in dom (b + (a (#) cos)) holds
( x + (2 * PI) in dom (b + (a (#) cos)) & x - (2 * PI) in dom (b + (a (#) cos)) & (b + (a (#) cos)) . x = (b + (a (#) cos)) . (x + (2 * PI)) )
proof
let x be real number ; ::_thesis: ( x in dom (b + (a (#) cos)) implies ( x + (2 * PI) in dom (b + (a (#) cos)) & x - (2 * PI) in dom (b + (a (#) cos)) & (b + (a (#) cos)) . x = (b + (a (#) cos)) . (x + (2 * PI)) ) )
assume  x in dom (b + (a (#) cos)) ; ::_thesis: ( x + (2 * PI) in dom (b + (a (#) cos)) & x - (2 * PI) in dom (b + (a (#) cos)) & (b + (a (#) cos)) . x = (b + (a (#) cos)) . (x + (2 * PI)) )
 x in REAL by XREAL_0:def_1;
then A1: x in dom (a (#) cos) by SIN_COS:24, VALUED_1:def_5;
then A2: ( x in dom (b + (a (#) cos)) & x in dom (b + (a (#) cos)) ) by VALUED_1:def_2;
 ( x + (2 * PI) in dom cos & x - (2 * PI) in dom cos ) by SIN_COS:24;
then A3: ( x + (2 * PI) in dom (a (#) cos) & x - (2 * PI) in dom (a (#) cos) ) by VALUED_1:def_5;
then  ( x + (2 * PI) in dom (b + (a (#) cos)) & x - (2 * PI) in dom (b + (a (#) cos)) ) by VALUED_1:def_2;
then (b + (a (#) cos)) . (x + (2 * PI)) = b + ((a (#) cos) . (x + (2 * PI))) by VALUED_1:def_2
.= b + (a * (cos . (x + (2 * PI)))) by A3, VALUED_1:def_5
.= b + (a * (cos . x)) by SIN_COS:78
.= b + ((a (#) cos) . x) by A1, VALUED_1:def_5
.= (b + (a (#) cos)) . x by A2, VALUED_1:def_2 ;
hence  ( x + (2 * PI) in dom (b + (a (#) cos)) & x - (2 * PI) in dom (b + (a (#) cos)) & (b + (a (#) cos)) . x = (b + (a (#) cos)) . (x + (2 * PI)) ) by A3, VALUED_1:def_2; ::_thesis: verum
end;
hence  b + (a (#) cos) is 2 * PI -periodic by Th1; ::_thesis: verum
end;

Lm28:  for b, a being real number
for k being Nat holds b + (a (#) sin) is (2 * PI) * (k + 1) -periodic
proof
let b, a be real number ; ::_thesis: for k being Nat holds b + (a (#) sin) is (2 * PI) * (k + 1) -periodic
let k be Nat; ::_thesis: b + (a (#) sin) is (2 * PI) * (k + 1) -periodic
defpred S1[ Nat] means b + (a (#) sin) is (2 * PI) * ($1 + 1) -periodic ;
A1: S1[ 0 ] by Lm26;
A2: for k being Nat st S1[k] holds
S1[k + 1]
proof
let k be Nat; ::_thesis: ( S1[k] implies S1[k + 1] )
assume A3: b + (a (#) sin) is (2 * PI) * (k + 1) -periodic ; ::_thesis: S1[k + 1]
 b + (a (#) sin) is (2 * PI) * ((k + 1) + 1) -periodic
proof
 for x being real number st x in dom (b + (a (#) sin)) holds
( x + ((2 * PI) * ((k + 1) + 1)) in dom (b + (a (#) sin)) & x - ((2 * PI) * ((k + 1) + 1)) in dom (b + (a (#) sin)) & (b + (a (#) sin)) . x = (b + (a (#) sin)) . (x + ((2 * PI) * ((k + 1) + 1))) )
proof
let x be real number ; ::_thesis: ( x in dom (b + (a (#) sin)) implies ( x + ((2 * PI) * ((k + 1) + 1)) in dom (b + (a (#) sin)) & x - ((2 * PI) * ((k + 1) + 1)) in dom (b + (a (#) sin)) & (b + (a (#) sin)) . x = (b + (a (#) sin)) . (x + ((2 * PI) * ((k + 1) + 1))) ) )
assume  x in dom (b + (a (#) sin)) ; ::_thesis: ( x + ((2 * PI) * ((k + 1) + 1)) in dom (b + (a (#) sin)) & x - ((2 * PI) * ((k + 1) + 1)) in dom (b + (a (#) sin)) & (b + (a (#) sin)) . x = (b + (a (#) sin)) . (x + ((2 * PI) * ((k + 1) + 1))) )
 x in REAL by XREAL_0:def_1;
then  x in dom (a (#) sin) by SIN_COS:24, VALUED_1:def_5;
then A4: x in dom (b + (a (#) sin)) by VALUED_1:def_2;
 ( x + ((2 * PI) * ((k + 1) + 1)) in dom sin & x - ((2 * PI) * ((k + 1) + 1)) in dom sin & x + ((2 * PI) * (k + 1)) in dom sin & x - ((2 * PI) * (k + 1)) in dom sin ) by SIN_COS:24;
then A5: ( x + ((2 * PI) * ((k + 1) + 1)) in dom (a (#) sin) & x - ((2 * PI) * ((k + 1) + 1)) in dom (a (#) sin) & x + ((2 * PI) * (k + 1)) in dom (a (#) sin) & x - ((2 * PI) * (k + 1)) in dom (a (#) sin) ) by VALUED_1:def_5;
then A6: ( x + ((2 * PI) * ((k + 1) + 1)) in dom (b + (a (#) sin)) & x - ((2 * PI) * ((k + 1) + 1)) in dom (b + (a (#) sin)) & x + ((2 * PI) * (k + 1)) in dom (b + (a (#) sin)) & x - ((2 * PI) * (k + 1)) in dom (b + (a (#) sin)) ) by VALUED_1:def_2;
then (b + (a (#) sin)) . (x + ((2 * PI) * ((k + 1) + 1))) = b + ((a (#) sin) . (x + ((2 * PI) * ((k + 1) + 1)))) by VALUED_1:def_2
.= b + (a * (sin . ((x + ((2 * PI) * (k + 1))) + (2 * PI)))) by A5, VALUED_1:def_5
.= b + (a * (sin . (x + ((2 * PI) * (k + 1))))) by SIN_COS:78
.= b + ((a (#) sin) . (x + ((2 * PI) * (k + 1)))) by A5, VALUED_1:def_5
.= (b + (a (#) sin)) . (x + ((2 * PI) * (k + 1))) by A6, VALUED_1:def_2 ;
hence  ( x + ((2 * PI) * ((k + 1) + 1)) in dom (b + (a (#) sin)) & x - ((2 * PI) * ((k + 1) + 1)) in dom (b + (a (#) sin)) & (b + (a (#) sin)) . x = (b + (a (#) sin)) . (x + ((2 * PI) * ((k + 1) + 1))) ) by A3, Th1, A5, A4, VALUED_1:def_2; ::_thesis: verum
end;
hence  b + (a (#) sin) is (2 * PI) * ((k + 1) + 1) -periodic by Th1; ::_thesis: verum
end;
hence  S1[k + 1] ; ::_thesis: verum
end;
 for n being Nat holds S1[n] from NAT_1:sch_2(A1, A2);
hence  b + (a (#) sin) is (2 * PI) * (k + 1) -periodic ; ::_thesis: verum
end;

theorem Th33: :: FUNCT_9:33
for b, a being real number
for i being non zero Integer holds b + (a (#) sin) is (2 * PI) * i -periodic
proof
let b, a be real number ; ::_thesis: for i being non zero Integer holds b + (a (#) sin) is (2 * PI) * i -periodic
let i be non zero Integer; ::_thesis: b + (a (#) sin) is (2 * PI) * i -periodic
 i in INT by INT_1:def_2;
then consider k being Element of NAT  such that
A1: ( i = k or i = - k ) by INT_1:def_1;
percases ( i = k or i = - k ) by A1;
suppose i = k ; ::_thesis: b + (a (#) sin) is (2 * PI) * i -periodic
then  ex m being Nat st i = m + 1 by NAT_1:6;
hence  b + (a (#) sin) is (2 * PI) * i -periodic by Lm28; ::_thesis: verum
end;
supposeA2: i = - k ; ::_thesis: b + (a (#) sin) is (2 * PI) * i -periodic
then consider m being Nat such that
A3: - i = m + 1 by NAT_1:6;
 b + (a (#) sin) is (2 * PI) * (m + 1) -periodic by Lm28;
then  b + (a (#) sin) is - ((2 * PI) * (m + 1)) -periodic by Th14;
hence  b + (a (#) sin) is (2 * PI) * i -periodic by A2, A3; ::_thesis: verum
end;
end;
end;

theorem :: FUNCT_9:34
for a, b being real number
for i being non zero Integer holds (a (#) sin) - b is (2 * PI) * i -periodic by Th33;

Lm29:  for b, a being real number
for k being Nat holds b + (a (#) cos) is (2 * PI) * (k + 1) -periodic
proof
let b, a be real number ; ::_thesis: for k being Nat holds b + (a (#) cos) is (2 * PI) * (k + 1) -periodic
let k be Nat; ::_thesis: b + (a (#) cos) is (2 * PI) * (k + 1) -periodic
defpred S1[ Nat] means b + (a (#) cos) is (2 * PI) * ($1 + 1) -periodic ;
A1: S1[ 0 ] by Lm27;
A2: for k being Nat st S1[k] holds
S1[k + 1]
proof
let k be Nat; ::_thesis: ( S1[k] implies S1[k + 1] )
assume A3: b + (a (#) cos) is (2 * PI) * (k + 1) -periodic ; ::_thesis: S1[k + 1]
 b + (a (#) cos) is (2 * PI) * ((k + 1) + 1) -periodic
proof
 for x being real number st x in dom (b + (a (#) cos)) holds
( x + ((2 * PI) * ((k + 1) + 1)) in dom (b + (a (#) cos)) & x - ((2 * PI) * ((k + 1) + 1)) in dom (b + (a (#) cos)) & (b + (a (#) cos)) . x = (b + (a (#) cos)) . (x + ((2 * PI) * ((k + 1) + 1))) )
proof
let x be real number ; ::_thesis: ( x in dom (b + (a (#) cos)) implies ( x + ((2 * PI) * ((k + 1) + 1)) in dom (b + (a (#) cos)) & x - ((2 * PI) * ((k + 1) + 1)) in dom (b + (a (#) cos)) & (b + (a (#) cos)) . x = (b + (a (#) cos)) . (x + ((2 * PI) * ((k + 1) + 1))) ) )
assume  x in dom (b + (a (#) cos)) ; ::_thesis: ( x + ((2 * PI) * ((k + 1) + 1)) in dom (b + (a (#) cos)) & x - ((2 * PI) * ((k + 1) + 1)) in dom (b + (a (#) cos)) & (b + (a (#) cos)) . x = (b + (a (#) cos)) . (x + ((2 * PI) * ((k + 1) + 1))) )
 x in REAL by XREAL_0:def_1;
then  x in dom (a (#) cos) by SIN_COS:24, VALUED_1:def_5;
then A4: x in dom (b + (a (#) cos)) by VALUED_1:def_2;
 ( x + ((2 * PI) * ((k + 1) + 1)) in dom cos & x - ((2 * PI) * ((k + 1) + 1)) in dom cos & x + ((2 * PI) * (k + 1)) in dom cos & x - ((2 * PI) * (k + 1)) in dom cos ) by SIN_COS:24;
then A5: ( x + ((2 * PI) * ((k + 1) + 1)) in dom (a (#) cos) & x - ((2 * PI) * ((k + 1) + 1)) in dom (a (#) cos) & x + ((2 * PI) * (k + 1)) in dom (a (#) cos) & x - ((2 * PI) * (k + 1)) in dom (a (#) cos) ) by VALUED_1:def_5;
then A6: ( x + ((2 * PI) * ((k + 1) + 1)) in dom (b + (a (#) cos)) & x - ((2 * PI) * ((k + 1) + 1)) in dom (b + (a (#) cos)) & x + ((2 * PI) * (k + 1)) in dom (b + (a (#) cos)) & x - ((2 * PI) * (k + 1)) in dom (b + (a (#) cos)) ) by VALUED_1:def_2;
then (b + (a (#) cos)) . (x + ((2 * PI) * ((k + 1) + 1))) = b + ((a (#) cos) . (x + ((2 * PI) * ((k + 1) + 1)))) by VALUED_1:def_2
.= b + (a * (cos . ((x + ((2 * PI) * (k + 1))) + (2 * PI)))) by A5, VALUED_1:def_5
.= b + (a * (cos . (x + ((2 * PI) * (k + 1))))) by SIN_COS:78
.= b + ((a (#) cos) . (x + ((2 * PI) * (k + 1)))) by A5, VALUED_1:def_5
.= (b + (a (#) cos)) . (x + ((2 * PI) * (k + 1))) by A6, VALUED_1:def_2 ;
hence  ( x + ((2 * PI) * ((k + 1) + 1)) in dom (b + (a (#) cos)) & x - ((2 * PI) * ((k + 1) + 1)) in dom (b + (a (#) cos)) & (b + (a (#) cos)) . x = (b + (a (#) cos)) . (x + ((2 * PI) * ((k + 1) + 1))) ) by A3, Th1, A5, A4, VALUED_1:def_2; ::_thesis: verum
end;
hence  b + (a (#) cos) is (2 * PI) * ((k + 1) + 1) -periodic by Th1; ::_thesis: verum
end;
hence  S1[k + 1] ; ::_thesis: verum
end;
 for n being Nat holds S1[n] from NAT_1:sch_2(A1, A2);
hence  b + (a (#) cos) is (2 * PI) * (k + 1) -periodic ; ::_thesis: verum
end;

theorem Th35: :: FUNCT_9:35
for b, a being real number
for i being non zero Integer holds b + (a (#) cos) is (2 * PI) * i -periodic
proof
let b, a be real number ; ::_thesis: for i being non zero Integer holds b + (a (#) cos) is (2 * PI) * i -periodic
let i be non zero Integer; ::_thesis: b + (a (#) cos) is (2 * PI) * i -periodic
 i in INT by INT_1:def_2;
then consider k being Element of NAT  such that
A1: ( i = k or i = - k ) by INT_1:def_1;
percases ( i = k or i = - k ) by A1;
suppose i = k ; ::_thesis: b + (a (#) cos) is (2 * PI) * i -periodic
then  ex m being Nat st i = m + 1 by NAT_1:6;
hence  b + (a (#) cos) is (2 * PI) * i -periodic by Lm29; ::_thesis: verum
end;
supposeA2: i = - k ; ::_thesis: b + (a (#) cos) is (2 * PI) * i -periodic
then consider m being Nat such that
A3: - i = m + 1 by NAT_1:6;
 b + (a (#) cos) is (2 * PI) * (m + 1) -periodic by Lm29;
then  b + (a (#) cos) is - ((2 * PI) * (m + 1)) -periodic by Th14;
hence  b + (a (#) cos) is (2 * PI) * i -periodic by A2, A3; ::_thesis: verum
end;
end;
end;

theorem :: FUNCT_9:36
for a, b being real number
for i being non zero Integer holds (a (#) cos) - b is (2 * PI) * i -periodic by Th35;

theorem :: FUNCT_9:37
for t, a being real number st t <> 0 holds
REAL --> a is t -periodic by Lm1;

registration
let a be real number ;
clusterREAL --> a ->  periodic ;
coherence
 REAL --> a is periodic
proof
take  1 ; :: according to FUNCT_9:def_2 ::_thesis: REAL --> a is 1 -periodic
thus  REAL --> a is 1 -periodic by Lm1; ::_thesis: verum
end;
end;

registration
let t be non zero real number ;
cluster Relation-like Function-like V27( REAL , REAL ) complex-valued ext-real-valued real-valued t -periodic for Element of K6(K7(REAL,REAL));
existence
 ex b1 being Function of REAL,REAL st b1 is t -periodic
proof
take  REAL --> the Real ; ::_thesis: REAL --> the Real is t -periodic
thus  REAL --> the Real is t -periodic by Lm1; ::_thesis: verum
end;
end;