funct_9.miz



    begin

    reserve x,t,t1,t2,r,a,b for Real;

    reserve F,G for real-valued Function;

    reserve k for Nat;

    reserve i for non zero Integer;

    definition

      let t be Real;

      let F be Function;

      :: FUNCT_9:def1

      attr F is t -periodic means t <> 0 & for x holds (x in ( dom F) iff (x + t) in ( dom F)) & (x in ( dom F) implies (F . x) = (F . (x + t)));

    end

    definition

      let F be Function;

      :: FUNCT_9:def2

      attr F is periodic means

      : Def2: ex t st F is t -periodic;

    end

    theorem :: FUNCT_9:1

    

     Th1: F is t -periodic iff t <> 0 & for x st x in ( dom F) holds (x + t) in ( dom F) & (x - t) in ( dom F) & (F . x) = (F . (x + t))

    proof

      thus F is t -periodic implies t <> 0 & for x st x in ( dom F) holds (x + t) in ( dom F) & (x - t) in ( dom F) & (F . x) = (F . (x + t))

      proof

        assume

         A1: F is t -periodic;

        for x st x in ( dom F) holds (x + t) in ( dom F) & (x - t) in ( dom F) & (F . x) = (F . (x + t))

        proof

          let x;

          assume x in ( dom F);

          then ((x - t) + t) in ( dom F);

          hence thesis by A1;

        end;

        hence thesis by A1;

      end;

      assume

       A2: t <> 0 & for x st x in ( dom F) holds ((x + t) in ( dom F) & (x - t) in ( dom F)) & (F . x) = (F . (x + t));

      for x holds (x in ( dom F) iff (x + t) in ( dom F)) & (x in ( dom F) implies (F . x) = (F . (x + t)))

      proof

        let x;

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

            then ((x + t) - t) in ( dom F) by A2;

            hence thesis;

          end;

          hence thesis by A2;

        end;

        hence thesis by A2;

      end;

      hence thesis by A2;

    end;

    theorem :: FUNCT_9:2

    

     Th2: F is t -periodic & G is t -periodic implies (F + G) is t -periodic

    proof

      assume that

       A1: F is t -periodic and

       A2: G is t -periodic;

      

       A3: t <> 0 & for x 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 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;

        assume

         A4: x in ( dom (F + G));

        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, A5, A6

        .= ((F . (x + t)) + (G . (x + t))) by A2, A5, A6

        .= ((F + G) . (x + t)) by A9, VALUED_1:def 1;

        hence thesis by A8, VALUED_1:def 1;

      end;

      hence thesis by A3, Th1;

    end;

    

     Lm1: t <> 0 implies ( REAL --> a) is t -periodic

    proof

      set F = ( REAL --> a);

      assume t <> 0 ;

      hence t <> 0 ;

      let x;

      

       A1: x in REAL & (x + t) in REAL by XREAL_0:def 1;

      hence x in ( dom F) iff (x + t) in ( dom F);

      assume x in ( dom F);

      

      thus (F . x) = a by A1, FUNCOP_1: 7

      .= (F . (x + t)) by A1, FUNCOP_1: 7;

    end;

    theorem :: FUNCT_9:3

    

     Th3: F is t -periodic & G is t -periodic implies (F - G) is t -periodic

    proof

      assume that

       A1: F is t -periodic and

       A2: G is t -periodic;

      

       A3: t <> 0 & for x 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 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;

        assume

         A4: x in ( dom (F - G));

        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, A5, A6

        .= ((F . (x + t)) - (G . (x + t))) by A2, A5, A6

        .= ((F - G) . (x + t)) by A9, VALUED_1: 13;

        hence thesis by A8, VALUED_1: 12;

      end;

      hence thesis by A3, Th1;

    end;

    theorem :: FUNCT_9:4

    

     Th4: F is t -periodic & G is t -periodic implies (F (#) G) is t -periodic

    proof

      assume that

       A1: F is t -periodic and

       A2: G is t -periodic;

      

       A3: t <> 0 & for x 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 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;

        assume

         A4: x in ( dom (F (#) G));

        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, A5, A6

        .= ((F . (x + t)) * (G . (x + t))) by A2, A5, A6

        .= ((F (#) G) . (x + t)) by A9, VALUED_1:def 4;

        hence thesis by A8, VALUED_1:def 4;

      end;

      hence thesis by A3, Th1;

    end;

    theorem :: FUNCT_9:5

    

     Th5: F is t -periodic & G is t -periodic implies (F /" G) is t -periodic

    proof

      assume that

       A1: F is t -periodic and

       A2: G is t -periodic;

      

       A3: t <> 0 & for x 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 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;

        assume x in ( dom (F /" G));

        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, A4, A5

        .= ((F . (x + t)) / (G . (x + t))) by A2, A4, A5

        .= ((F /" G) . (x + t)) by VALUED_1: 17;

        hence thesis by A7, VALUED_1: 16;

      end;

      hence thesis by A3, Th1;

    end;

    theorem :: FUNCT_9:6

    

     Th6: F is t -periodic implies ( - F) is t -periodic

    proof

      assume

       A1: F is t -periodic;

      then

       A2: t <> 0 & for x 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 st x in ( dom ( - F)) holds ((x + t) in ( dom ( - F)) & (x - t) in ( dom ( - F))) & (( - F) . x) = (( - F) . (x + t))

      proof

        let x;

        assume x in ( dom ( - F));

        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, A3

        .= (( - F) . (x + t)) by VALUED_1: 8;

        hence thesis by A4, VALUED_1: 8;

      end;

      hence thesis by A2, Th1;

    end;

    theorem :: FUNCT_9:7

    

     Th7: F is t -periodic implies (r (#) F) is t -periodic

    proof

      assume

       A1: F is t -periodic;

      then

       A2: t <> 0 & for x 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 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;

        assume

         A3: x in ( dom (r (#) F));

        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, A4

        .= ((r (#) F) . (x + t)) by A6, VALUED_1:def 5;

        hence thesis by A5, VALUED_1:def 5;

      end;

      hence thesis by A2, Th1;

    end;

    theorem :: FUNCT_9:8

    

     Th8: F is t -periodic implies (r + F) is t -periodic

    proof

      assume

       A1: F is t -periodic;

      then

       A2: t <> 0 & for x 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 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;

        assume

         A3: x in ( dom (r + F));

        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, A4

        .= ((r + F) . (x + t)) by A6, VALUED_1:def 2;

        hence thesis by A5, VALUED_1:def 2;

      end;

      hence thesis by A2, Th1;

    end;

    theorem :: FUNCT_9:9

    F is t -periodic implies (F - r) is t -periodic by Th8;

    theorem :: FUNCT_9:10

    

     Th10: F is t -periodic implies |.F.| is t -periodic

    proof

      assume

       A1: F is t -periodic;

      then

       A2: t <> 0 & for x 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 st x in ( dom |.F.|) holds ((x + t) in ( dom |.F.|) & (x - t) in ( dom |.F.|)) & ( |.F.| . x) = ( |.F.| . (x + t))

      proof

        let x;

        assume

         A3: x in ( dom |.F.|);

        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, A4

        .= ( |.F.| . (x + t)) by A6, VALUED_1:def 11;

        hence thesis by A5, VALUED_1:def 11;

      end;

      hence thesis by A2, Th1;

    end;

    theorem :: FUNCT_9:11

    

     Th11: F is t -periodic implies (F " ) is t -periodic

    proof

      assume

       A1: F is t -periodic;

      then

       A2: t <> 0 & for x 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 st x in ( dom (F " )) holds ((x + t) in ( dom (F " )) & (x - t) in ( dom (F " ))) & ((F " ) . x) = ((F " ) . (x + t))

      proof

        let x;

        assume

         A3: x in ( dom (F " ));

        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, A4

        .= ((F " ) . (x + t)) by A6, VALUED_1:def 7;

        hence thesis by A5, VALUED_1:def 7;

      end;

      hence thesis by A2, Th1;

    end;

    theorem :: FUNCT_9:12

    F is t -periodic implies (F ^2 ) is t -periodic by Th4;

    theorem :: FUNCT_9:13

    

     Th13: F is t -periodic implies for x st x in ( dom F) holds (F . x) = (F . (x - t))

    proof

      assume

       A1: F is t -periodic;

      let x;

      assume x in ( dom F);

      then (x + t) in ( dom F) & (x - t) in ( dom F) by A1, Th1;

      

      then (F . (x - t)) = (F . ((x - t) + t)) by A1

      .= (F . x);

      hence thesis;

    end;

    theorem :: FUNCT_9:14

    

     Th14: F is t -periodic implies F is ( - t) -periodic

    proof

      assume

       A1: F is t -periodic;

      then

       A2: ( - t) <> 0 ;

      for x st x in ( dom F) holds ((x + ( - t)) in ( dom F) & (x - ( - t)) in ( dom F)) & (F . x) = (F . (x + ( - t)))

      proof

        let x;

        assume x in ( dom F);

        then (x + t) in ( dom F) & (x - t) in ( dom F) by A1, Th1;

        hence thesis by A1, Th13;

      end;

      hence thesis by A2, Th1;

    end;

    theorem :: FUNCT_9:15

    F is t1 -periodic & F is t2 -periodic & (t1 + t2) <> 0 implies F is (t1 + t2) -periodic

    proof

      assume

       A1: F is t1 -periodic & F is t2 -periodic & (t1 + t2) <> 0 ;

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

        assume

         A2: x in ( dom F);

        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 thesis by A1, A2;

      end;

      hence thesis by A1, Th1;

    end;

    theorem :: FUNCT_9:16

    F is t1 -periodic & F is t2 -periodic & (t1 - t2) <> 0 implies F is (t1 - t2) -periodic

    proof

      assume

       A1: F is t1 -periodic & F is t2 -periodic & (t1 - t2) <> 0 ;

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

        assume

         A2: x in ( dom F);

        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

        .= (F . ((x - t2) + t2)) by A1, A4

        .= (F . x);

        hence thesis by A3;

      end;

      hence thesis by A1, Th1;

    end;

    theorem :: FUNCT_9:17

    (t <> 0 & for x 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

    proof

      assume that

       A1: t <> 0 and

       A2: for x st x in ( dom F) holds ((x + t) in ( dom F) & (x - t) in ( dom F) & (F . (x + t)) = (F . (x - t)));

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

        assume x in ( dom F);

        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 thesis by A4;

      end;

      then F is (2 * t) -periodic by A1, Th1;

      hence thesis;

    end;

    theorem :: FUNCT_9:18

    ((t1 + t2) <> 0 & for x 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

    proof

      assume that

       A1: (t1 + t2) <> 0 and

       A2: for x 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)));

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

        assume x in ( dom F);

        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 thesis by A4;

      end;

      then F is (t1 + t2) -periodic by Th1, A1;

      hence thesis;

    end;

    theorem :: FUNCT_9:19

    ((t1 - t2) <> 0 & for x 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

    proof

      assume that

       A1: (t1 - t2) <> 0 and

       A2: for x 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)));

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

        assume x in ( dom F);

        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 thesis by A4;

      end;

      then F is (t1 - t2) -periodic by Th1, A1;

      hence thesis;

    end;

    theorem :: FUNCT_9:20

    (t <> 0 & for x 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

    proof

      assume that

       A1: t <> 0 and

       A2: for x st x in ( dom F) holds ((x + t) in ( dom F) & (x - t) in ( dom F) & (F . (x + t)) = ((F . x) " ));

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

        assume

         A3: x in ( dom F);

        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 thesis by A5;

      end;

      then F is (2 * t) -periodic by A1, Th1;

      hence thesis;

    end;

    

     Lm2: sin is (2 * PI ) -periodic by SIN_COS: 24, SIN_COS: 78, XREAL_0:def 1;

    registration

      cluster periodic real-valued for Function;

      existence by Lm2, Def2;

      cluster periodic for PartFunc of REAL , REAL ;

      existence

      proof

        take sin ;

        thus thesis by Lm2;

      end;

    end

    registration

      let t be non zero Real;

      cluster ( REAL --> t) -> t -periodic;

      coherence by Lm1;

      cluster t -periodic real-valued for Function;

      existence

      proof

        take ( REAL --> t);

        thus thesis;

      end;

    end

    registration

      let t be non zero Real;

      let F,G be t -periodic real-valued Function;

      cluster (F + G) -> t -periodic;

      coherence by Th2;

      cluster (F - G) -> t -periodic;

      coherence by Th3;

      cluster (F (#) G) -> t -periodic;

      coherence by Th4;

      cluster (F /" G) -> t -periodic;

      coherence by Th5;

    end

    registration

      let F be periodic real-valued Function;

      cluster ( - F) -> periodic;

      coherence

      proof

        consider t such that

         A1: F is t -periodic by Def2;

        ( - F) is t -periodic by A1, Th6;

        hence thesis;

      end;

    end

    registration

      let F be periodic real-valued Function;

      let r be Real;

      cluster (r (#) F) -> periodic;

      coherence

      proof

        consider t such that

         A1: F is t -periodic by Def2;

        (r (#) F) is t -periodic by A1, Th7;

        hence thesis;

      end;

      cluster (r + F) -> periodic;

      coherence

      proof

        consider t such that

         A2: F is t -periodic by Def2;

        (r + F) is t -periodic by A2, Th8;

        hence thesis;

      end;

      cluster (F - r) -> periodic;

      coherence ;

    end

    registration

      let F be periodic real-valued Function;

      cluster |.F.| -> periodic;

      coherence

      proof

        consider t such that

         A1: F is t -periodic by Def2;

         |.F.| is t -periodic by A1, Th10;

        hence thesis;

      end;

      cluster (F " ) -> periodic;

      coherence

      proof

        consider t such that

         A2: F is t -periodic by Def2;

        (F " ) is t -periodic by A2, Th11;

        hence thesis;

      end;

      cluster (F ^2 ) -> periodic;

      coherence

      proof

        consider t such that

         A3: F is t -periodic by Def2;

        (F ^2 ) is t -periodic by A3;

        hence thesis;

      end;

    end

    begin

    

     Lm3: cos is (2 * PI ) -periodic by SIN_COS: 24, SIN_COS: 78, XREAL_0:def 1;

    registration

      cluster sin -> periodic;

      coherence by Lm2;

      cluster cos -> periodic;

      coherence by Lm3;

    end

    

     Lm4: sin is ((2 * PI ) * (k + 1)) -periodic

    proof

      defpred X[ Nat] means sin is ((2 * PI ) * ($1 + 1)) -periodic;

      

       A1: X[ 0 ] by Lm2;

      

       A2: for k be Nat st X[k] holds X[(k + 1)]

      proof

        let k be Nat such that

         A3: sin is ((2 * PI ) * (k + 1)) -periodic;

         sin is ((2 * PI ) * ((k + 1) + 1)) -periodic

        proof

          for x st x in ( dom sin ) holds ( sin . x) = ( sin . (x + ((2 * PI ) * ((k + 1) + 1))))

          proof

            let x;

            assume

             A4: x in ( dom sin );

            ( sin . (x + ((2 * PI ) * (k + 1)))) = ( sin . ((x + ((2 * PI ) * (k + 1))) + (2 * PI ))) by SIN_COS: 78;

            hence thesis by A3, A4;

          end;

          then ((2 * PI ) * ((k + 1) + 1)) <> 0 & for x 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, XREAL_0:def 1;

          hence thesis by Th1;

        end;

        hence thesis;

      end;

      for n be Nat holds X[n] from NAT_1:sch 2( A1, A2);

      hence thesis;

    end;

    theorem :: FUNCT_9:21

     sin is ((2 * PI ) * i) -periodic

    proof

      i in INT by INT_1:def 2;

      then

      consider k be Nat such that

       A1: i = k or i = ( - k) by INT_1:def 1;

      per cases by A1;

        suppose i = k;

        then ex m be Nat st i = (m + 1) by NAT_1: 6;

        hence thesis by Lm4;

      end;

        suppose

         A2: i = ( - k);

        then

        consider m be 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 thesis by A2, A3;

      end;

    end;

    

     Lm5: cos is ((2 * PI ) * (k + 1)) -periodic

    proof

      defpred X[ Nat] means cos is ((2 * PI ) * ($1 + 1)) -periodic;

      

       A1: X[ 0 ] by Lm3;

      

       A2: for k be Nat st X[k] holds X[(k + 1)]

      proof

        let k be Nat such that

         A3: cos is ((2 * PI ) * (k + 1)) -periodic;

         cos is ((2 * PI ) * ((k + 1) + 1)) -periodic

        proof

          for x st x in ( dom cos ) holds ( cos . x) = ( cos . (x + ((2 * PI ) * ((k + 1) + 1))))

          proof

            let x;

            assume

             A4: x in ( dom cos );

            ( cos . (x + ((2 * PI ) * (k + 1)))) = ( cos . ((x + ((2 * PI ) * (k + 1))) + (2 * PI ))) by SIN_COS: 78;

            hence thesis by A3, A4;

          end;

          then ((2 * PI ) * ((k + 1) + 1)) <> 0 & for x 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, XREAL_0:def 1;

          hence thesis by Th1;

        end;

        hence thesis;

      end;

      for n be Nat holds X[n] from NAT_1:sch 2( A1, A2);

      hence thesis;

    end;

    theorem :: FUNCT_9:22

     cos is ((2 * PI ) * i) -periodic

    proof

      i in INT by INT_1:def 2;

      then

      consider k be Nat such that

       A1: i = k or i = ( - k) by INT_1:def 1;

      per cases by A1;

        suppose i = k;

        then ex m be Nat st i = (m + 1) by NAT_1: 6;

        hence thesis by Lm5;

      end;

        suppose

         A2: i = ( - k);

        then

        consider m be 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 thesis by A2, A3;

      end;

    end;

    

     Lm6: cosec is (2 * PI ) -periodic

    proof

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

        assume

         A1: x in ( dom cosec );

        then x in (( dom sin ) \ ( sin " { 0 })) by RFUNCT_1:def 2;

        then x in ( dom sin ) & not x in ( sin " { 0 }) by XBOOLE_0:def 5;

        then

         A2: not ( sin . x) in { 0 } by FUNCT_1:def 7;

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

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

        then not ( sin . (x + (2 * PI ))) in { 0 } by TARSKI:def 1;

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

        then

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

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

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

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

        then

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

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

        

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

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

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

        hence thesis by A3, A4, RFUNCT_1:def 2;

      end;

      hence thesis by Th1;

    end;

    

     Lm7: sec is (2 * PI ) -periodic

    proof

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

        assume

         A1: x in ( dom sec );

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

        then

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

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

        then ( cos . (x - (2 * PI ))) = ( cos . ((x - (2 * PI )) + (2 * PI ))) by Lm3;

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

        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 thesis by A3, A4, RFUNCT_1:def 2;

      end;

      hence thesis by Th1;

    end;

    registration

      cluster cosec -> periodic;

      coherence by Lm6;

      cluster sec -> periodic;

      coherence by Lm7;

    end

    

     Lm8: sec is ((2 * PI ) * (k + 1)) -periodic

    proof

      defpred X[ Nat] means sec is ((2 * PI ) * ($1 + 1)) -periodic;

      

       A1: X[ 0 ] by Lm7;

      

       A2: for k be Nat st X[k] holds X[(k + 1)]

      proof

        let k be Nat such that

         A3: sec is ((2 * PI ) * (k + 1)) -periodic;

         sec is ((2 * PI ) * ((k + 1) + 1)) -periodic

        proof

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

            assume x in ( dom sec );

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

            then

             A6: (x + ((2 * PI ) * ((k + 1) + 1))) in (( dom cos ) \ ( cos " { 0 })) by XBOOLE_0:def 5;

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

            then ( cos . (x - ((2 * PI ) * ((k + 1) + 1)))) = ( cos . ((x - ((2 * PI ) * ((k + 1) + 1))) + (2 * PI ))) by Lm3;

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

            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 thesis by A6, A7, RFUNCT_1:def 2;

          end;

          hence thesis by Th1;

        end;

        hence thesis;

      end;

      for n be Nat holds X[n] from NAT_1:sch 2( A1, A2);

      hence thesis;

    end;

    theorem :: FUNCT_9:23

     sec is ((2 * PI ) * i) -periodic

    proof

      i in INT by INT_1:def 2;

      then

      consider k be Nat such that

       A1: i = k or i = ( - k) by INT_1:def 1;

      per cases by A1;

        suppose i = k;

        then ex m be Nat st i = (m + 1) by NAT_1: 6;

        hence thesis by Lm8;

      end;

        suppose

         A2: i = ( - k);

        then

        consider m be 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 thesis by A2, A3;

      end;

    end;

    

     Lm9: cosec is ((2 * PI ) * (k + 1)) -periodic

    proof

      defpred X[ Nat] means cosec is ((2 * PI ) * ($1 + 1)) -periodic;

      

       A1: X[ 0 ] by Lm6;

      

       A2: for k be Nat st X[k] holds X[(k + 1)]

      proof

        let k be Nat such that

         A3: cosec is ((2 * PI ) * (k + 1)) -periodic;

         cosec is ((2 * PI ) * ((k + 1) + 1)) -periodic

        proof

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

            assume x in ( dom cosec );

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

            then

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

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

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

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

            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 thesis by A6, A7, RFUNCT_1:def 2;

          end;

          hence thesis by Th1;

        end;

        hence thesis;

      end;

      for n be Nat holds X[n] from NAT_1:sch 2( A1, A2);

      hence thesis;

    end;

    theorem :: FUNCT_9:24

     cosec is ((2 * PI ) * i) -periodic

    proof

      i in INT by INT_1:def 2;

      then

      consider k be Nat such that

       A1: i = k or i = ( - k) by INT_1:def 1;

      per cases by A1;

        suppose i = k;

        then ex m be Nat st i = (m + 1) by NAT_1: 6;

        hence thesis by Lm9;

      end;

        suppose

         A2: i = ( - k);

        then

        consider m be 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 thesis by A2, A3;

      end;

    end;

    

     Lm10: tan is PI -periodic

    proof

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

      proof

        let x;

        assume

         A1: x in ( dom tan );

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

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

        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 thesis by A4, A5, RFUNCT_1:def 1;

      end;

      hence thesis by Th1;

    end;

    

     Lm11: cot is PI -periodic

    proof

      for x st x in ( dom cot ) holds ((x + PI ) in ( dom cot ) & (x - PI ) in ( dom cot )) & ( cot . x) = ( cot . (x + PI ))

      proof

        let x;

        assume

         A1: x in ( dom cot );

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

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

        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 thesis by A4, A5, RFUNCT_1:def 1;

      end;

      hence thesis by Th1;

    end;

    registration

      cluster tan -> periodic;

      coherence by Lm10;

      cluster cot -> periodic;

      coherence by Lm11;

    end

    

     Lm12: tan is ( PI * (k + 1)) -periodic

    proof

      defpred X[ Nat] means tan is ( PI * ($1 + 1)) -periodic;

      

       A1: X[ 0 ] by Lm10;

      

       A2: for k be Nat st X[k] holds X[(k + 1)]

      proof

        let k be Nat such that

         A3: tan is ( PI * (k + 1)) -periodic;

         tan is ( PI * ((k + 1) + 1)) -periodic

        proof

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

            assume x in ( dom tan );

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

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

            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 thesis by A7, A6, RFUNCT_1:def 1;

          end;

          hence thesis by Th1;

        end;

        hence thesis;

      end;

      for n be Nat holds X[n] from NAT_1:sch 2( A1, A2);

      hence thesis;

    end;

    theorem :: FUNCT_9:25

     tan is ( PI * i) -periodic

    proof

      i in INT by INT_1:def 2;

      then

      consider k be Nat such that

       A1: i = k or i = ( - k) by INT_1:def 1;

      per cases by A1;

        suppose i = k;

        then ex m be Nat st i = (m + 1) by NAT_1: 6;

        hence thesis by Lm12;

      end;

        suppose

         A2: i = ( - k);

        then

        consider m be 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 thesis by A2, A3;

      end;

    end;

    

     Lm13: cot is ( PI * (k + 1)) -periodic

    proof

      defpred X[ Nat] means cot is ( PI * ($1 + 1)) -periodic;

      

       A1: X[ 0 ] by Lm11;

      

       A2: for k be Nat st X[k] holds X[(k + 1)]

      proof

        let k be Nat such that

         A3: cot is ( PI * (k + 1)) -periodic;

         cot is ( PI * ((k + 1) + 1)) -periodic

        proof

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

            assume x in ( dom cot );

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

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

            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 thesis by A7, A6, RFUNCT_1:def 1;

          end;

          hence thesis by Th1;

        end;

        hence thesis;

      end;

      for n be Nat holds X[n] from NAT_1:sch 2( A1, A2);

      hence thesis;

    end;

    theorem :: FUNCT_9:26

     cot is ( PI * i) -periodic

    proof

      i in INT by INT_1:def 2;

      then

      consider k be Nat such that

       A1: i = k or i = ( - k) by INT_1:def 1;

      per cases by A1;

        suppose i = k;

        then ex m be Nat st i = (m + 1) by NAT_1: 6;

        hence thesis by Lm13;

      end;

        suppose

         A2: i = ( - k);

        then

        consider m be 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 thesis by A2, A3;

      end;

    end;

    

     Lm14: |. sin .| is PI -periodic

    proof

      for x st x in ( dom |. sin .|) holds ((x + PI ) in ( dom |. sin .|) & (x - PI ) in ( dom |. sin .|)) & ( |. sin .| . x) = ( |. sin .| . (x + PI ))

      proof

        let x;

        assume

         A1: x in ( dom |. sin .|);

        

         A2: (x + PI ) in ( dom sin ) & (x - PI ) in ( dom sin ) by SIN_COS: 24, XREAL_0:def 1;

        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 thesis by A2, VALUED_1:def 11;

      end;

      hence thesis by Th1;

    end;

    

     Lm15: |. cos .| is PI -periodic

    proof

      for x st x in ( dom |. cos .|) holds ((x + PI ) in ( dom |. cos .|) & (x - PI ) in ( dom |. cos .|)) & ( |. cos .| . x) = ( |. cos .| . (x + PI ))

      proof

        let x;

        assume

         A1: x in ( dom |. cos .|);

        

         A2: (x + PI ) in ( dom cos ) & (x - PI ) in ( dom cos ) by SIN_COS: 24, XREAL_0:def 1;

        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 thesis by A2, VALUED_1:def 11;

      end;

      hence thesis by Th1;

    end;

    

     Lm16: |. sin .| is ( PI * (k + 1)) -periodic

    proof

      defpred X[ Nat] means |. sin .| is ( PI * ($1 + 1)) -periodic;

      

       A1: X[ 0 ] by Lm14;

      

       A2: for k be Nat st X[k] holds X[(k + 1)]

      proof

        let k be Nat such that

         A3: |. sin .| is ( PI * (k + 1)) -periodic;

         |. sin .| is ( PI * ((k + 1) + 1)) -periodic

        proof

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

            assume

             A4: x in ( dom |. sin .|);

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

            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 thesis by A3, A4, A6, VALUED_1:def 11;

          end;

          hence thesis by Th1;

        end;

        hence thesis;

      end;

      for n be Nat holds X[n] from NAT_1:sch 2( A1, A2);

      hence thesis;

    end;

    theorem :: FUNCT_9:27

     |. sin .| is ( PI * i) -periodic

    proof

      i in INT by INT_1:def 2;

      then

      consider k be Nat such that

       A1: i = k or i = ( - k) by INT_1:def 1;

      per cases by A1;

        suppose i = k;

        then ex m be Nat st i = (m + 1) by NAT_1: 6;

        hence thesis by Lm16;

      end;

        suppose

         A2: i = ( - k);

        then

        consider m be 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 thesis by A2, A3;

      end;

    end;

    

     Lm17: |. cos .| is ( PI * (k + 1)) -periodic

    proof

      defpred X[ Nat] means |. cos .| is ( PI * ($1 + 1)) -periodic;

      

       A1: X[ 0 ] by Lm15;

      

       A2: for k be Nat st X[k] holds X[(k + 1)]

      proof

        let k be Nat such that

         A3: |. cos .| is ( PI * (k + 1)) -periodic;

         |. cos .| is ( PI * ((k + 1) + 1)) -periodic

        proof

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

            assume

             A4: x in ( dom |. cos .|);

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

            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 thesis by A3, A4, A6, VALUED_1:def 11;

          end;

          hence thesis by Th1;

        end;

        hence thesis;

      end;

      for n be Nat holds X[n] from NAT_1:sch 2( A1, A2);

      hence thesis;

    end;

    theorem :: FUNCT_9:28

     |. cos .| is ( PI * i) -periodic

    proof

      i in INT by INT_1:def 2;

      then

      consider k be Nat such that

       A1: i = k or i = ( - k) by INT_1:def 1;

      per cases by A1;

        suppose i = k;

        then ex m be Nat st i = (m + 1) by NAT_1: 6;

        hence thesis by Lm17;

      end;

        suppose

         A2: i = ( - k);

        then

        consider m be 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 thesis by A2, A3;

      end;

    end;

    

     Lm18: ( |. sin .| + |. cos .|) is ( PI / 2) -periodic

    proof

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

        assume

         A1: x in ( dom ( |. sin .| + |. cos .|));

        

         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 thesis by A3;

        end;

        

        then (( |. sin .| + |. cos .|) . (x + ( PI / 2))) = (( |. sin .| . (x + ( PI / 2))) + ( |. cos .| . (x + ( PI / 2)))) by VALUED_1:def 1, XREAL_0:def 1

        .= ( |.( sin . (x + ( PI / 2))).| + ( |. cos .| . (x + ( PI / 2)))) by A2, VALUED_1:def 11, XREAL_0:def 1

        .= ( |.( sin . (x + ( PI / 2))).| + |.( cos . (x + ( PI / 2))).|) by A2, VALUED_1:def 11, XREAL_0:def 1

        .= ( |.( 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 thesis by A2, XREAL_0:def 1;

      end;

      hence thesis by Th1;

    end;

    

     Lm19: ( |. sin .| + |. cos .|) is (( PI / 2) * (k + 1)) -periodic

    proof

      defpred X[ Nat] means ( |. sin .| + |. cos .|) is (( PI / 2) * ($1 + 1)) -periodic;

      

       A1: X[ 0 ] by Lm18;

      

       A2: for k be Nat st X[k] holds X[(k + 1)]

      proof

        let k be Nat such that

         A3: ( |. sin .| + |. cos .|) is (( PI / 2) * (k + 1)) -periodic;

        

         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 thesis by A5;

        end;

        ( |. sin .| + |. cos .|) is (( PI / 2) * ((k + 1) + 1)) -periodic

        proof

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

            assume x in ( dom ( |. sin .| + |. cos .|));

            (( |. 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, XREAL_0:def 1

            .= ( |.( sin . (x + (( PI / 2) * ((k + 1) + 1)))).| + ( |. cos .| . (x + (( PI / 2) * ((k + 1) + 1))))) by A4, VALUED_1:def 11, XREAL_0:def 1

            .= ( |.( sin . ((x + (( PI / 2) * (k + 1))) + ( PI / 2))).| + |.( cos . ((x + (( PI / 2) * (k + 1))) + ( PI / 2))).|) by A4, VALUED_1:def 11, XREAL_0:def 1

            .= ( |.( 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, XREAL_0:def 1

            .= (( |. cos .| . (x + (( PI / 2) * (k + 1)))) + ( |. sin .| . (x + (( PI / 2) * (k + 1))))) by A4, VALUED_1:def 11, XREAL_0:def 1

            .= (( |. sin .| + |. cos .|) . (x + (( PI / 2) * (k + 1)))) by A4, VALUED_1:def 1, XREAL_0:def 1;

            hence thesis by A3, A4, XREAL_0:def 1;

          end;

          hence thesis by Th1;

        end;

        hence thesis;

      end;

      for n be Nat holds X[n] from NAT_1:sch 2( A1, A2);

      hence thesis;

    end;

    theorem :: FUNCT_9:29

    ( |. sin .| + |. cos .|) is (( PI / 2) * i) -periodic

    proof

      i in INT by INT_1:def 2;

      then

      consider k be Nat such that

       A1: i = k or i = ( - k) by INT_1:def 1;

      per cases by A1;

        suppose i = k;

        then ex m be Nat st i = (m + 1) by NAT_1: 6;

        hence thesis by Lm19;

      end;

        suppose

         A2: i = ( - k);

        then

        consider m be 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 thesis by A2, A3;

      end;

    end;

    

     Lm20: ( sin ^2 ) is PI -periodic

    proof

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

        assume x in ( dom ( sin ^2 ));

        

         A1: (x + PI ) in ( dom sin ) & (x - PI ) in ( dom sin ) by SIN_COS: 24, XREAL_0:def 1;

        (( 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 thesis by A1, VALUED_1: 11;

      end;

      hence thesis by Th1;

    end;

    

     Lm21: ( cos ^2 ) is PI -periodic

    proof

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

        assume x in ( dom ( cos ^2 ));

        

         A1: (x + PI ) in ( dom cos ) & (x - PI ) in ( dom cos ) by SIN_COS: 24, XREAL_0:def 1;

        (( 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 thesis by A1, VALUED_1: 11;

      end;

      hence thesis by Th1;

    end;

    

     Lm22: ( sin ^2 ) is ( PI * (k + 1)) -periodic

    proof

      defpred X[ Nat] means ( sin ^2 ) is ( PI * ($1 + 1)) -periodic;

      

       A1: X[ 0 ] by Lm20;

      

       A2: for k be Nat st X[k] holds X[(k + 1)]

      proof

        let k be Nat such that

         A3: ( sin ^2 ) is ( PI * (k + 1)) -periodic;

        ( sin ^2 ) is ( PI * ((k + 1) + 1)) -periodic

        proof

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

            assume

             A4: x in ( dom ( sin ^2 ));

            

             A5: (x + ( PI * ((k + 1) + 1))) in ( dom sin ) & (x - ( PI * ((k + 1) + 1))) in ( dom sin ) by SIN_COS: 24, XREAL_0:def 1;

            (( 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 thesis by A3, A4, A5, VALUED_1: 11;

          end;

          hence thesis by Th1;

        end;

        hence thesis;

      end;

      for n be Nat holds X[n] from NAT_1:sch 2( A1, A2);

      hence thesis;

    end;

    theorem :: FUNCT_9:30

    ( sin ^2 ) is ( PI * i) -periodic

    proof

      i in INT by INT_1:def 2;

      then

      consider k be Nat such that

       A1: i = k or i = ( - k) by INT_1:def 1;

      per cases by A1;

        suppose i = k;

        then ex m be Nat st i = (m + 1) by NAT_1: 6;

        hence thesis by Lm22;

      end;

        suppose

         A2: i = ( - k);

        then

        consider m be 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 thesis by A2, A3;

      end;

    end;

    

     Lm23: ( cos ^2 ) is ( PI * (k + 1)) -periodic

    proof

      defpred X[ Nat] means ( cos ^2 ) is ( PI * ($1 + 1)) -periodic;

      

       A1: X[ 0 ] by Lm21;

      

       A2: for k be Nat st X[k] holds X[(k + 1)]

      proof

        let k be Nat such that

         A3: ( cos ^2 ) is ( PI * (k + 1)) -periodic;

        ( cos ^2 ) is ( PI * ((k + 1) + 1)) -periodic

        proof

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

            assume

             A4: x in ( dom ( cos ^2 ));

            

             A5: (x + ( PI * ((k + 1) + 1))) in ( dom cos ) & (x - ( PI * ((k + 1) + 1))) in ( dom cos ) by SIN_COS: 24, XREAL_0:def 1;

            (( 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 thesis by A3, A4, A5, VALUED_1: 11;

          end;

          hence thesis by Th1;

        end;

        hence thesis;

      end;

      for n be Nat holds X[n] from NAT_1:sch 2( A1, A2);

      hence thesis;

    end;

    theorem :: FUNCT_9:31

    ( cos ^2 ) is ( PI * i) -periodic

    proof

      i in INT by INT_1:def 2;

      then

      consider k be Nat such that

       A1: i = k or i = ( - k) by INT_1:def 1;

      per cases by A1;

        suppose i = k;

        then ex m be Nat st i = (m + 1) by NAT_1: 6;

        hence thesis by Lm23;

      end;

        suppose

         A2: i = ( - k);

        then

        consider m be 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 thesis by A2, A3;

      end;

    end;

    

     Lm24: ( sin (#) cos ) is PI -periodic

    proof

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

        assume

         A1: x in ( dom ( sin (#) cos ));

        

         A2: (x + PI ) in (( dom sin ) /\ ( dom cos )) & (x - PI ) in (( dom sin ) /\ ( dom cos )) by SIN_COS: 24, XREAL_0:def 1;

        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 thesis by A2, VALUED_1:def 4;

      end;

      hence thesis by Th1;

    end;

    

     Lm25: ( sin (#) cos ) is ( PI * (k + 1)) -periodic

    proof

      defpred X[ Nat] means ( sin (#) cos ) is ( PI * ($1 + 1)) -periodic;

      

       A1: X[ 0 ] by Lm24;

      

       A2: for k be Nat st X[k] holds X[(k + 1)]

      proof

        let k be Nat such that

         A3: ( sin (#) cos ) is ( PI * (k + 1)) -periodic;

        ( sin (#) cos ) is ( PI * ((k + 1) + 1)) -periodic

        proof

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

            assume

             A4: x in ( dom ( sin (#) cos ));

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

            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 thesis by A3, A4, A6, VALUED_1:def 4;

          end;

          hence thesis by Th1;

        end;

        hence thesis;

      end;

      for n be Nat holds X[n] from NAT_1:sch 2( A1, A2);

      hence thesis;

    end;

    theorem :: FUNCT_9:32

    ( sin (#) cos ) is ( PI * i) -periodic

    proof

      i in INT by INT_1:def 2;

      then

      consider k be Nat such that

       A1: i = k or i = ( - k) by INT_1:def 1;

      per cases by A1;

        suppose i = k;

        then ex m be Nat st i = (m + 1) by NAT_1: 6;

        hence thesis by Lm25;

      end;

        suppose

         A2: i = ( - k);

        then

        consider m be 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 thesis by A2, A3;

      end;

    end;

    

     Lm26: (b + (a (#) sin )) is (2 * PI ) -periodic

    proof

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

        assume x in ( dom (b + (a (#) sin )));

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

        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 thesis by A3, VALUED_1:def 2;

      end;

      hence thesis by Th1;

    end;

    

     Lm27: (b + (a (#) cos )) is (2 * PI ) -periodic

    proof

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

        assume x in ( dom (b + (a (#) cos )));

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

        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 thesis by A3, VALUED_1:def 2;

      end;

      hence thesis by Th1;

    end;

    

     Lm28: (b + (a (#) sin )) is ((2 * PI ) * (k + 1)) -periodic

    proof

      defpred X[ Nat] means (b + (a (#) sin )) is ((2 * PI ) * ($1 + 1)) -periodic;

      

       A1: X[ 0 ] by Lm26;

      

       A2: for k be Nat st X[k] holds X[(k + 1)]

      proof

        let k be Nat such that

         A3: (b + (a (#) sin )) is ((2 * PI ) * (k + 1)) -periodic;

        (b + (a (#) sin )) is ((2 * PI ) * ((k + 1) + 1)) -periodic

        proof

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

            assume x in ( dom (b + (a (#) sin )));

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

            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 thesis by A3, A5, A4, VALUED_1:def 2;

          end;

          hence thesis by Th1;

        end;

        hence thesis;

      end;

      for n be Nat holds X[n] from NAT_1:sch 2( A1, A2);

      hence thesis;

    end;

    theorem :: FUNCT_9:33

    

     Th33: (b + (a (#) sin )) is ((2 * PI ) * i) -periodic

    proof

      i in INT by INT_1:def 2;

      then

      consider k be Nat such that

       A1: i = k or i = ( - k) by INT_1:def 1;

      per cases by A1;

        suppose i = k;

        then ex m be Nat st i = (m + 1) by NAT_1: 6;

        hence thesis by Lm28;

      end;

        suppose

         A2: i = ( - k);

        then

        consider m be 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 thesis by A2, A3;

      end;

    end;

    theorem :: FUNCT_9:34

    ((a (#) sin ) - b) is ((2 * PI ) * i) -periodic by Th33;

    

     Lm29: (b + (a (#) cos )) is ((2 * PI ) * (k + 1)) -periodic

    proof

      defpred X[ Nat] means (b + (a (#) cos )) is ((2 * PI ) * ($1 + 1)) -periodic;

      

       A1: X[ 0 ] by Lm27;

      

       A2: for k be Nat st X[k] holds X[(k + 1)]

      proof

        let k be Nat such that

         A3: (b + (a (#) cos )) is ((2 * PI ) * (k + 1)) -periodic;

        (b + (a (#) cos )) is ((2 * PI ) * ((k + 1) + 1)) -periodic

        proof

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

            assume x in ( dom (b + (a (#) cos )));

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

            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 thesis by A3, A5, A4, VALUED_1:def 2;

          end;

          hence thesis by Th1;

        end;

        hence thesis;

      end;

      for n be Nat holds X[n] from NAT_1:sch 2( A1, A2);

      hence thesis;

    end;

    theorem :: FUNCT_9:35

    

     Th35: (b + (a (#) cos )) is ((2 * PI ) * i) -periodic

    proof

      i in INT by INT_1:def 2;

      then

      consider k be Nat such that

       A1: i = k or i = ( - k) by INT_1:def 1;

      per cases by A1;

        suppose i = k;

        then ex m be Nat st i = (m + 1) by NAT_1: 6;

        hence thesis by Lm29;

      end;

        suppose

         A2: i = ( - k);

        then

        consider m be 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 thesis by A2, A3;

      end;

    end;

    theorem :: FUNCT_9:36

    ((a (#) cos ) - b) is ((2 * PI ) * i) -periodic by Th35;

    theorem :: FUNCT_9:37

    t <> 0 implies ( REAL --> a) is t -periodic by Lm1;

    registration

      let a;

      cluster ( REAL --> a) -> periodic;

      coherence

      proof

        take 1;

        thus thesis by Lm1;

      end;

    end

    registration

      let t be non zero Real;

      cluster t -periodic for Function of REAL , REAL ;

      existence

      proof

        take ( REAL --> the Element of REAL );

        thus thesis by Lm1;

      end;

    end