funct_8.miz



    begin

    reserve x,r for Real;

    definition

      let A be set;

      :: FUNCT_8:def1

      attr A is symmetrical means

      : Def1: for x be Complex st x in A holds ( - x) in A;

    end

    registration

      cluster symmetrical for Subset of COMPLEX ;

      existence

      proof

        take ( [#] COMPLEX );

        let x be Complex;

        thus thesis by XCMPLX_0:def 2;

      end;

    end

    registration

      cluster symmetrical for Subset of REAL ;

      existence

      proof

        take ( [#] REAL );

        let x be Complex;

        for x st x in REAL holds ( - x) in REAL by XREAL_0:def 1;

        hence thesis;

      end;

    end

    reserve A for symmetrical Subset of COMPLEX ;

    definition

      let R be Relation;

      :: FUNCT_8:def2

      attr R is with_symmetrical_domain means

      : Def2: ( dom R) is symmetrical;

    end

    registration

      cluster empty -> with_symmetrical_domain for Relation;

      coherence

      proof

        

         A1: {} is symmetrical;

        thus thesis by A1;

      end;

    end

    registration

      let R be with_symmetrical_domain Relation;

      cluster ( dom R) -> symmetrical;

      coherence by Def2;

    end

    definition

      let X,Y be complex-membered set;

      let F be PartFunc of X, Y;

      :: FUNCT_8:def3

      attr F is quasi_even means

      : Def3: for x st x in ( dom F) & ( - x) in ( dom F) holds (F . ( - x)) = (F . x);

    end

    definition

      let X,Y be complex-membered set;

      let F be PartFunc of X, Y;

      :: FUNCT_8:def4

      attr F is even means F is with_symmetrical_domain quasi_even;

    end

    registration

      let X,Y be complex-membered set;

      cluster with_symmetrical_domain quasi_even -> even for PartFunc of X, Y;

      coherence ;

      cluster even -> with_symmetrical_domain quasi_even for PartFunc of X, Y;

      coherence ;

    end

    definition

      let A be set;

      let X,Y be complex-membered set;

      let F be PartFunc of X, Y;

      :: FUNCT_8:def5

      pred F is_even_on A means A c= ( dom F) & (F | A) is even;

    end

    definition

      let X,Y be complex-membered set;

      let F be PartFunc of X, Y;

      :: FUNCT_8:def6

      attr F is quasi_odd means

      : Def6: for x st x in ( dom F) & ( - x) in ( dom F) holds (F . ( - x)) = ( - (F . x));

    end

    definition

      let X,Y be complex-membered set;

      let F be PartFunc of X, Y;

      :: FUNCT_8:def7

      attr F is odd means F is with_symmetrical_domain quasi_odd;

    end

    registration

      let X,Y be complex-membered set;

      cluster with_symmetrical_domain quasi_odd -> odd for PartFunc of X, Y;

      coherence ;

      cluster odd -> with_symmetrical_domain quasi_odd for PartFunc of X, Y;

      coherence ;

    end

    definition

      let A be set;

      let X,Y be complex-membered set;

      let F be PartFunc of X, Y;

      :: FUNCT_8:def8

      pred F is_odd_on A means A c= ( dom F) & (F | A) is odd;

    end

    reserve F,G for PartFunc of REAL , REAL ;

    theorem :: FUNCT_8:1

    F is_odd_on A iff (A c= ( dom F) & for x st x in A holds ((F . x) + (F . ( - x))) = 0 )

    proof

      

       A1: (A c= ( dom F) & for x st x in A holds ((F . x) + (F . ( - x))) = 0 ) implies F is_odd_on A

      proof

        assume that

         A2: A c= ( dom F) and

         A3: for x st x in A holds ((F . x) + (F . ( - x))) = 0 ;

        

         A4: ( dom (F | A)) = A by A2, RELAT_1: 62;

        

         A5: for x st x in A holds (F . ( - x)) = ( - (F . x))

        proof

          let x;

          assume x in A;

          then ((F . x) + (F . ( - x))) = 0 by A3;

          hence thesis;

        end;

        for x st x in ( dom (F | A)) & ( - x) in ( dom (F | A)) holds ((F | A) . ( - x)) = ( - ((F | A) . x))

        proof

          let x be Real;

          assume that

           A6: x in ( dom (F | A)) and

           A7: ( - x) in ( dom (F | A));

          reconsider x as Element of REAL by XREAL_0:def 1;

          ((F | A) . ( - x)) = ((F | A) /. ( - x)) by A7, PARTFUN1:def 6

          .= (F /. ( - x)) by A2, A4, A7, PARTFUN2: 17

          .= (F . ( - x)) by A2, A7, PARTFUN1:def 6

          .= ( - (F . x)) by A5, A6

          .= ( - (F /. x)) by A2, A6, PARTFUN1:def 6

          .= ( - ((F | A) /. x)) by A2, A4, A6, PARTFUN2: 17

          .= ( - ((F | A) . x)) by A6, PARTFUN1:def 6;

          hence thesis;

        end;

        then (F | A) is with_symmetrical_domain quasi_odd by A4;

        hence thesis by A2;

      end;

      F is_odd_on A implies (A c= ( dom F) & for x st x in A holds ((F . x) + (F . ( - x))) = 0 )

      proof

        assume

         A8: F is_odd_on A;

        then

         A9: A c= ( dom F);

        

         A10: (F | A) is odd by A8;

        for x st x in A holds ((F . x) + (F . ( - x))) = 0

        proof

          let x;

          assume

           A11: x in A;

          then

           A12: x in ( dom (F | A)) by A9, RELAT_1: 62;

          

           A13: ( - x) in A by A11, Def1;

          then

           A14: ( - x) in ( dom (F | A)) by A9, RELAT_1: 62;

          reconsider x as Element of REAL by XREAL_0:def 1;

          ((F . x) + (F . ( - x))) = ((F /. x) + (F . ( - x))) by A9, A11, PARTFUN1:def 6

          .= ((F /. x) + (F /. ( - x))) by A9, A13, PARTFUN1:def 6

          .= (((F | A) /. x) + (F /. ( - x))) by A9, A11, PARTFUN2: 17

          .= (((F | A) /. x) + ((F | A) /. ( - x))) by A9, A13, PARTFUN2: 17

          .= (((F | A) /. x) + ((F | A) . ( - x))) by A14, PARTFUN1:def 6

          .= (((F | A) . x) + ((F | A) . ( - x))) by A12, PARTFUN1:def 6

          .= (((F | A) . x) + ( - ((F | A) . x))) by A10, A12, A14, Def6

          .= 0 ;

          hence thesis;

        end;

        hence thesis by A8;

      end;

      hence thesis by A1;

    end;

    theorem :: FUNCT_8:2

    F is_even_on A iff (A c= ( dom F) & for x st x in A holds ((F . x) - (F . ( - x))) = 0 )

    proof

      

       A1: (A c= ( dom F) & for x st x in A holds ((F . x) - (F . ( - x))) = 0 ) implies F is_even_on A

      proof

        assume that

         A2: A c= ( dom F) and

         A3: for x st x in A holds ((F . x) - (F . ( - x))) = 0 ;

        

         A4: ( dom (F | A)) = A by A2, RELAT_1: 62;

        

         A5: for x st x in A holds (F . ( - x)) = (F . x)

        proof

          let x;

          assume x in A;

          then ((F . x) - (F . ( - x))) = 0 by A3;

          hence thesis;

        end;

        for x st x in ( dom (F | A)) & ( - x) in ( dom (F | A)) holds ((F | A) . ( - x)) = ((F | A) . x)

        proof

          let x;

          assume that

           A6: x in ( dom (F | A)) and

           A7: ( - x) in ( dom (F | A));

          reconsider x as Element of REAL by XREAL_0:def 1;

          ((F | A) . ( - x)) = ((F | A) /. ( - x)) by A7, PARTFUN1:def 6

          .= (F /. ( - x)) by A2, A4, A7, PARTFUN2: 17

          .= (F . ( - x)) by A2, A7, PARTFUN1:def 6

          .= (F . x) by A5, A6

          .= (F /. x) by A2, A6, PARTFUN1:def 6

          .= ((F | A) /. x) by A2, A4, A6, PARTFUN2: 17

          .= ((F | A) . x) by A6, PARTFUN1:def 6;

          hence thesis;

        end;

        then (F | A) is with_symmetrical_domain quasi_even by A4;

        hence thesis by A2;

      end;

      F is_even_on A implies (A c= ( dom F) & for x st x in A holds ((F . x) - (F . ( - x))) = 0 )

      proof

        assume

         A8: F is_even_on A;

        then

         A9: A c= ( dom F);

        

         A10: (F | A) is even by A8;

        for x st x in A holds ((F . x) - (F . ( - x))) = 0

        proof

          let x;

          assume

           A11: x in A;

          then

           A12: x in ( dom (F | A)) by A9, RELAT_1: 62;

          

           A13: ( - x) in A by A11, Def1;

          then

           A14: ( - x) in ( dom (F | A)) by A9, RELAT_1: 62;

          reconsider x as Element of REAL by XREAL_0:def 1;

          ((F . x) - (F . ( - x))) = ((F /. x) - (F . ( - x))) by A9, A11, PARTFUN1:def 6

          .= ((F /. x) - (F /. ( - x))) by A9, A13, PARTFUN1:def 6

          .= (((F | A) /. x) - (F /. ( - x))) by A9, A11, PARTFUN2: 17

          .= (((F | A) /. x) - ((F | A) /. ( - x))) by A9, A13, PARTFUN2: 17

          .= (((F | A) . x) - ((F | A) /. ( - x))) by A12, PARTFUN1:def 6

          .= (((F | A) . x) - ((F | A) . ( - x))) by A14, PARTFUN1:def 6

          .= (((F | A) . x) - ((F | A) . x)) by A10, A12, A14, Def3

          .= 0 ;

          hence thesis;

        end;

        hence thesis by A8;

      end;

      hence thesis by A1;

    end;

    theorem :: FUNCT_8:3

    (F is_odd_on A & for x st x in A holds (F . x) <> 0 ) implies (A c= ( dom F) & for x st x in A holds ((F . x) / (F . ( - x))) = ( - 1))

    proof

      assume that

       A1: F is_odd_on A and

       A2: for x st x in A holds (F . x) <> 0 ;

      

       A3: A c= ( dom F) by A1;

      

       A4: (F | A) is odd by A1;

      for x st x in A holds ((F . x) / (F . ( - x))) = ( - 1)

      proof

        let x;

        assume

         A5: x in A;

        then

         A6: x in ( dom (F | A)) by A3, RELAT_1: 62;

        reconsider x as Element of REAL by XREAL_0:def 1;

        

         A7: (F . x) = (F /. x) by A3, A5, PARTFUN1:def 6

        .= ((F | A) /. x) by A3, A5, PARTFUN2: 17

        .= ((F | A) . x) by A6, PARTFUN1:def 6;

        

         A8: ( - x) in A by A5, Def1;

        then

         A9: ( - x) in ( dom (F | A)) by A3, RELAT_1: 62;

        ((F . x) / (F . ( - x))) = ((F /. x) / (F . ( - x))) by A3, A5, PARTFUN1:def 6

        .= ((F /. x) / (F /. ( - x))) by A3, A8, PARTFUN1:def 6

        .= (((F | A) /. x) / (F /. ( - x))) by A3, A5, PARTFUN2: 17

        .= (((F | A) /. x) / ((F | A) /. ( - x))) by A3, A8, PARTFUN2: 17

        .= (((F | A) . x) / ((F | A) /. ( - x))) by A6, PARTFUN1:def 6

        .= (((F | A) . x) / ((F | A) . ( - x))) by A9, PARTFUN1:def 6

        .= (((F | A) . x) / ( - ((F | A) . x))) by A4, A6, A9, Def6

        .= ( - (((F | A) . x) / ((F | A) . x))) by XCMPLX_1: 188

        .= ( - 1) by A2, A5, A7, XCMPLX_1: 60;

        hence thesis;

      end;

      hence thesis by A1;

    end;

    theorem :: FUNCT_8:4

    (A c= ( dom F) & for x st x in A holds ((F . x) / (F . ( - x))) = ( - 1)) implies F is_odd_on A

    proof

      assume that

       A1: A c= ( dom F) and

       A2: for x st x in A holds ((F . x) / (F . ( - x))) = ( - 1);

      

       A3: ( dom (F | A)) = A by A1, RELAT_1: 62;

      

       A4: for x st x in A holds (F . ( - x)) = ( - (F . x))

      proof

        let x;

        assume x in A;

        then ((F . x) / (F . ( - x))) = ( - 1) by A2;

        hence thesis by XCMPLX_1: 195;

      end;

      for x st x in ( dom (F | A)) & ( - x) in ( dom (F | A)) holds ((F | A) . ( - x)) = ( - ((F | A) . x))

      proof

        let x;

        assume that

         A5: x in ( dom (F | A)) and

         A6: ( - x) in ( dom (F | A));

        reconsider x as Element of REAL by XREAL_0:def 1;

        ((F | A) . ( - x)) = ((F | A) /. ( - x)) by A6, PARTFUN1:def 6

        .= (F /. ( - x)) by A1, A3, A6, PARTFUN2: 17

        .= (F . ( - x)) by A1, A6, PARTFUN1:def 6

        .= ( - (F . x)) by A4, A5

        .= ( - (F /. x)) by A1, A5, PARTFUN1:def 6

        .= ( - ((F | A) /. x)) by A1, A3, A5, PARTFUN2: 17

        .= ( - ((F | A) . x)) by A5, PARTFUN1:def 6;

        hence thesis;

      end;

      then (F | A) is with_symmetrical_domain quasi_odd by A3;

      hence thesis by A1;

    end;

    theorem :: FUNCT_8:5

    (F is_even_on A & for x st x in A holds (F . x) <> 0 ) implies (A c= ( dom F) & for x st x in A holds ((F . x) / (F . ( - x))) = 1)

    proof

      assume that

       A1: F is_even_on A and

       A2: for x st x in A holds (F . x) <> 0 ;

      

       A3: A c= ( dom F) by A1;

      

       A4: (F | A) is even by A1;

      for x st x in A holds ((F . x) / (F . ( - x))) = 1

      proof

        let x;

        assume

         A5: x in A;

        then

         A6: x in ( dom (F | A)) by A3, RELAT_1: 62;

        reconsider x as Element of REAL by XREAL_0:def 1;

        

         A7: (F . x) = (F /. x) by A3, A5, PARTFUN1:def 6

        .= ((F | A) /. x) by A3, A5, PARTFUN2: 17

        .= ((F | A) . x) by A6, PARTFUN1:def 6;

        

         A8: ( - x) in A by A5, Def1;

        then

         A9: ( - x) in ( dom (F | A)) by A3, RELAT_1: 62;

        ((F . x) / (F . ( - x))) = ((F /. x) / (F . ( - x))) by A3, A5, PARTFUN1:def 6

        .= ((F /. x) / (F /. ( - x))) by A3, A8, PARTFUN1:def 6

        .= (((F | A) /. x) / (F /. ( - x))) by A3, A5, PARTFUN2: 17

        .= (((F | A) /. x) / ((F | A) /. ( - x))) by A3, A8, PARTFUN2: 17

        .= (((F | A) . x) / ((F | A) /. ( - x))) by A6, PARTFUN1:def 6

        .= (((F | A) . x) / ((F | A) . ( - x))) by A9, PARTFUN1:def 6

        .= (((F | A) . x) / ((F | A) . x)) by A4, A6, A9, Def3

        .= 1 by A2, A5, A7, XCMPLX_1: 60;

        hence thesis;

      end;

      hence thesis by A1;

    end;

    theorem :: FUNCT_8:6

    (A c= ( dom F) & for x st x in A holds ((F . x) / (F . ( - x))) = 1) implies F is_even_on A

    proof

      assume that

       A1: A c= ( dom F) and

       A2: for x st x in A holds ((F . x) / (F . ( - x))) = 1;

      

       A3: ( dom (F | A)) = A by A1, RELAT_1: 62;

      

       A4: for x st x in A holds (F . ( - x)) = (F . x)

      proof

        let x;

        assume x in A;

        then ((F . x) / (F . ( - x))) = 1 by A2;

        hence thesis by XCMPLX_1: 58;

      end;

      for x st x in ( dom (F | A)) & ( - x) in ( dom (F | A)) holds ((F | A) . ( - x)) = ((F | A) . x)

      proof

        let x;

        assume that

         A5: x in ( dom (F | A)) and

         A6: ( - x) in ( dom (F | A));

        reconsider x as Element of REAL by XREAL_0:def 1;

        ((F | A) . ( - x)) = ((F | A) /. ( - x)) by A6, PARTFUN1:def 6

        .= (F /. ( - x)) by A1, A3, A6, PARTFUN2: 17

        .= (F . ( - x)) by A1, A6, PARTFUN1:def 6

        .= (F . x) by A4, A5

        .= (F /. x) by A1, A5, PARTFUN1:def 6

        .= ((F | A) /. x) by A1, A3, A5, PARTFUN2: 17

        .= ((F | A) . x) by A5, PARTFUN1:def 6;

        hence thesis;

      end;

      then (F | A) is with_symmetrical_domain quasi_even by A3;

      hence thesis by A1;

    end;

    theorem :: FUNCT_8:7

    F is_even_on A & F is_odd_on A implies for x st x in A holds (F . x) = 0

    proof

      assume that

       A1: F is_even_on A and

       A2: F is_odd_on A;

      

       A3: (F | A) is even by A1;

      

       A4: (F | A) is odd by A2;

      let x;

      assume

       A5: x in A;

      

       A6: A c= ( dom F) by A1;

      then

       A7: x in ( dom (F | A)) by A5, RELAT_1: 62;

      ( - x) in A by A5, Def1;

      then

       A8: ( - x) in ( dom (F | A)) by A6, RELAT_1: 62;

      reconsider x as Element of REAL by XREAL_0:def 1;

      (F . x) = (F /. x) by A6, A5, PARTFUN1:def 6

      .= ((F | A) /. x) by A6, A5, PARTFUN2: 17

      .= ((F | A) . x) by A7, PARTFUN1:def 6

      .= ((F | A) . ( - x)) by A3, A7, A8, Def3

      .= ( - ((F | A) . x)) by A4, A7, A8, Def6

      .= ( - ((F | A) /. x)) by A7, PARTFUN1:def 6

      .= ( - (F /. x)) by A6, A5, PARTFUN2: 17

      .= ( - (F . x)) by A6, A5, PARTFUN1:def 6;

      hence thesis;

    end;

    theorem :: FUNCT_8:8

    F is_even_on A implies for x st x in A holds (F . x) = (F . |.x.|)

    proof

      assume

       A1: F is_even_on A;

      then

       A2: A c= ( dom F);

      

       A3: (F | A) is even by A1;

      let x such that

       A4: x in A;

      

       A5: x in ( dom (F | A)) by A2, A4, RELAT_1: 62;

      

       A6: ( - x) in A by A4, Def1;

      then

       A7: ( - x) in ( dom (F | A)) by A2, RELAT_1: 62;

      reconsider x as Element of REAL by XREAL_0:def 1;

      per cases ;

        suppose x < 0 ;

        

        then (F . |.x.|) = (F . ( - x)) by ABSVALUE:def 1

        .= (F /. ( - x)) by A2, A6, PARTFUN1:def 6

        .= ((F | A) /. ( - x)) by A2, A6, PARTFUN2: 17

        .= ((F | A) . ( - x)) by A7, PARTFUN1:def 6

        .= ((F | A) . x) by A3, A5, A7, Def3

        .= ((F | A) /. x) by A5, PARTFUN1:def 6

        .= (F /. x) by A2, A4, PARTFUN2: 17

        .= (F . x) by A2, A4, PARTFUN1:def 6;

        hence thesis;

      end;

        suppose 0 < x;

        hence thesis by ABSVALUE:def 1;

      end;

        suppose x = 0 ;

        hence thesis by ABSVALUE:def 1;

      end;

    end;

    theorem :: FUNCT_8:9

    (A c= ( dom F) & for x st x in A holds (F . x) = (F . |.x.|)) implies F is_even_on A

    proof

      assume that

       A1: A c= ( dom F) and

       A2: for x st x in A holds (F . x) = (F . |.x.|);

      

       A3: ( dom (F | A)) = A by A1, RELAT_1: 62;

      

       A4: for x st x in A holds ( - x) in A by Def1;

      

       A5: for x st x in A holds (F . ( - x)) = (F . x)

      proof

        let x;

        assume

         A6: x in A;

        per cases ;

          suppose x < 0 ;

          

          then (F . ( - x)) = (F . |.x.|) by ABSVALUE:def 1

          .= (F . x) by A2, A6;

          hence thesis;

        end;

          suppose 0 < x;

          

          then |.( - x).| = ( - ( - x)) by ABSVALUE:def 1

          .= x;

          hence thesis by A2, A4, A6;

        end;

          suppose x = 0 ;

          hence thesis;

        end;

      end;

      for x st x in ( dom (F | A)) & ( - x) in ( dom (F | A)) holds ((F | A) . ( - x)) = ((F | A) . x)

      proof

        let x;

        assume that

         A7: x in ( dom (F | A)) and

         A8: ( - x) in ( dom (F | A));

        reconsider x as Element of REAL by XREAL_0:def 1;

        ((F | A) . ( - x)) = ((F | A) /. ( - x)) by A8, PARTFUN1:def 6

        .= (F /. ( - x)) by A1, A3, A8, PARTFUN2: 17

        .= (F . ( - x)) by A1, A8, PARTFUN1:def 6

        .= (F . x) by A5, A7

        .= (F /. x) by A1, A7, PARTFUN1:def 6

        .= ((F | A) /. x) by A1, A3, A7, PARTFUN2: 17

        .= ((F | A) . x) by A7, PARTFUN1:def 6;

        hence thesis;

      end;

      then (F | A) is with_symmetrical_domain quasi_even by A3;

      hence thesis by A1;

    end;

    theorem :: FUNCT_8:10

    F is_odd_on A & G is_odd_on A implies (F + G) is_odd_on A

    proof

      assume that

       A1: F is_odd_on A and

       A2: G is_odd_on A;

      

       A3: A c= ( dom G) by A2;

      

       A4: (G | A) is odd by A2;

      

       A5: A c= ( dom F) by A1;

      then

       A6: A c= (( dom F) /\ ( dom G)) by A3, XBOOLE_1: 19;

      

       A7: (( dom F) /\ ( dom G)) = ( dom (F + G)) by VALUED_1:def 1;

      then

       A8: ( dom ((F + G) | A)) = A by A5, A3, RELAT_1: 62, XBOOLE_1: 19;

      

       A9: (F | A) is odd by A1;

      for x st x in ( dom ((F + G) | A)) & ( - x) in ( dom ((F + G) | A)) holds (((F + G) | A) . ( - x)) = ( - (((F + G) | A) . x))

      proof

        let x;

        assume that

         A10: x in ( dom ((F + G) | A)) and

         A11: ( - x) in ( dom ((F + G) | A));

        

         A12: x in ( dom (F | A)) by A5, A8, A10, RELAT_1: 62;

        

         A13: x in ( dom (G | A)) by A3, A8, A10, RELAT_1: 62;

        

         A14: ( - x) in ( dom (F | A)) by A5, A8, A11, RELAT_1: 62;

        

         A15: ( - x) in ( dom (G | A)) by A3, A8, A11, RELAT_1: 62;

        reconsider x as Element of REAL by XREAL_0:def 1;

        (((F + G) | A) . ( - x)) = (((F + G) | A) /. ( - x)) by A11, PARTFUN1:def 6

        .= ((F + G) /. ( - x)) by A6, A7, A8, A11, PARTFUN2: 17

        .= ((F + G) . ( - x)) by A6, A7, A11, PARTFUN1:def 6

        .= ((F . ( - x)) + (G . ( - x))) by A6, A7, A11, VALUED_1:def 1

        .= ((F /. ( - x)) + (G . ( - x))) by A5, A11, PARTFUN1:def 6

        .= ((F /. ( - x)) + (G /. ( - x))) by A3, A11, PARTFUN1:def 6

        .= (((F | A) /. ( - x)) + (G /. ( - x))) by A5, A8, A11, PARTFUN2: 17

        .= (((F | A) /. ( - x)) + ((G | A) /. ( - x))) by A3, A8, A11, PARTFUN2: 17

        .= (((F | A) . ( - x)) + ((G | A) /. ( - x))) by A14, PARTFUN1:def 6

        .= (((F | A) . ( - x)) + ((G | A) . ( - x))) by A15, PARTFUN1:def 6

        .= (( - ((F | A) . x)) + ((G | A) . ( - x))) by A9, A12, A14, Def6

        .= (( - ((F | A) . x)) + ( - ((G | A) . x))) by A4, A13, A15, Def6

        .= ( - (((F | A) . x) + ((G | A) . x)))

        .= ( - (((F | A) /. x) + ((G | A) . x))) by A12, PARTFUN1:def 6

        .= ( - (((F | A) /. x) + ((G | A) /. x))) by A13, PARTFUN1:def 6

        .= ( - ((F /. x) + ((G | A) /. x))) by A5, A8, A10, PARTFUN2: 17

        .= ( - ((F /. x) + (G /. x))) by A3, A8, A10, PARTFUN2: 17

        .= ( - ((F . x) + (G /. x))) by A5, A10, PARTFUN1:def 6

        .= ( - ((F . x) + (G . x))) by A3, A10, PARTFUN1:def 6

        .= ( - ((F + G) . x)) by A6, A7, A10, VALUED_1:def 1

        .= ( - ((F + G) /. x)) by A6, A7, A10, PARTFUN1:def 6

        .= ( - (((F + G) | A) /. x)) by A6, A7, A8, A10, PARTFUN2: 17

        .= ( - (((F + G) | A) . x)) by A10, PARTFUN1:def 6;

        hence thesis;

      end;

      then ((F + G) | A) is with_symmetrical_domain quasi_odd by A8;

      hence thesis by A6, A7;

    end;

    theorem :: FUNCT_8:11

    F is_even_on A & G is_even_on A implies (F + G) is_even_on A

    proof

      assume that

       A1: F is_even_on A and

       A2: G is_even_on A;

      

       A3: A c= ( dom G) by A2;

      

       A4: (G | A) is even by A2;

      

       A5: A c= ( dom F) by A1;

      then

       A6: A c= (( dom F) /\ ( dom G)) by A3, XBOOLE_1: 19;

      

       A7: (( dom F) /\ ( dom G)) = ( dom (F + G)) by VALUED_1:def 1;

      then

       A8: ( dom ((F + G) | A)) = A by A5, A3, RELAT_1: 62, XBOOLE_1: 19;

      

       A9: (F | A) is even by A1;

      for x st x in ( dom ((F + G) | A)) & ( - x) in ( dom ((F + G) | A)) holds (((F + G) | A) . ( - x)) = (((F + G) | A) . x)

      proof

        let x;

        assume that

         A10: x in ( dom ((F + G) | A)) and

         A11: ( - x) in ( dom ((F + G) | A));

        

         A12: x in ( dom (F | A)) by A5, A8, A10, RELAT_1: 62;

        

         A13: x in ( dom (G | A)) by A3, A8, A10, RELAT_1: 62;

        

         A14: ( - x) in ( dom (F | A)) by A5, A8, A11, RELAT_1: 62;

        

         A15: ( - x) in ( dom (G | A)) by A3, A8, A11, RELAT_1: 62;

        reconsider x as Element of REAL by XREAL_0:def 1;

        (((F + G) | A) . ( - x)) = (((F + G) | A) /. ( - x)) by A11, PARTFUN1:def 6

        .= ((F + G) /. ( - x)) by A6, A7, A8, A11, PARTFUN2: 17

        .= ((F + G) . ( - x)) by A6, A7, A11, PARTFUN1:def 6

        .= ((F . ( - x)) + (G . ( - x))) by A6, A7, A11, VALUED_1:def 1

        .= ((F /. ( - x)) + (G . ( - x))) by A5, A11, PARTFUN1:def 6

        .= ((F /. ( - x)) + (G /. ( - x))) by A3, A11, PARTFUN1:def 6

        .= (((F | A) /. ( - x)) + (G /. ( - x))) by A5, A8, A11, PARTFUN2: 17

        .= (((F | A) /. ( - x)) + ((G | A) /. ( - x))) by A3, A8, A11, PARTFUN2: 17

        .= (((F | A) . ( - x)) + ((G | A) /. ( - x))) by A14, PARTFUN1:def 6

        .= (((F | A) . ( - x)) + ((G | A) . ( - x))) by A15, PARTFUN1:def 6

        .= (((F | A) . x) + ((G | A) . ( - x))) by A9, A12, A14, Def3

        .= (((F | A) . x) + ((G | A) . x)) by A4, A13, A15, Def3

        .= (((F | A) /. x) + ((G | A) . x)) by A12, PARTFUN1:def 6

        .= (((F | A) /. x) + ((G | A) /. x)) by A13, PARTFUN1:def 6

        .= ((F /. x) + ((G | A) /. x)) by A5, A8, A10, PARTFUN2: 17

        .= ((F /. x) + (G /. x)) by A3, A8, A10, PARTFUN2: 17

        .= ((F . x) + (G /. x)) by A5, A10, PARTFUN1:def 6

        .= ((F . x) + (G . x)) by A3, A10, PARTFUN1:def 6

        .= ((F + G) . x) by A6, A7, A10, VALUED_1:def 1

        .= ((F + G) /. x) by A6, A7, A10, PARTFUN1:def 6

        .= (((F + G) | A) /. x) by A6, A7, A8, A10, PARTFUN2: 17

        .= (((F + G) | A) . x) by A10, PARTFUN1:def 6;

        hence thesis;

      end;

      then ((F + G) | A) is with_symmetrical_domain quasi_even by A8;

      hence thesis by A6, A7;

    end;

    theorem :: FUNCT_8:12

    F is_odd_on A & G is_odd_on A implies (F - G) is_odd_on A

    proof

      assume that

       A1: F is_odd_on A and

       A2: G is_odd_on A;

      

       A3: A c= ( dom G) by A2;

      

       A4: (G | A) is odd by A2;

      

       A5: A c= ( dom F) by A1;

      then

       A6: A c= (( dom F) /\ ( dom G)) by A3, XBOOLE_1: 19;

      

       A7: (( dom F) /\ ( dom G)) = ( dom (F - G)) by VALUED_1: 12;

      then

       A8: ( dom ((F - G) | A)) = A by A5, A3, RELAT_1: 62, XBOOLE_1: 19;

      

       A9: (F | A) is odd by A1;

      for x st x in ( dom ((F - G) | A)) & ( - x) in ( dom ((F - G) | A)) holds (((F - G) | A) . ( - x)) = ( - (((F - G) | A) . x))

      proof

        let x;

        assume that

         A10: x in ( dom ((F - G) | A)) and

         A11: ( - x) in ( dom ((F - G) | A));

        

         A12: x in ( dom (F | A)) by A5, A8, A10, RELAT_1: 62;

        

         A13: x in ( dom (G | A)) by A3, A8, A10, RELAT_1: 62;

        

         A14: ( - x) in ( dom (F | A)) by A5, A8, A11, RELAT_1: 62;

        

         A15: ( - x) in ( dom (G | A)) by A3, A8, A11, RELAT_1: 62;

        reconsider x as Element of REAL by XREAL_0:def 1;

        (((F - G) | A) . ( - x)) = (((F - G) | A) /. ( - x)) by A11, PARTFUN1:def 6

        .= ((F - G) /. ( - x)) by A6, A7, A8, A11, PARTFUN2: 17

        .= ((F - G) . ( - x)) by A6, A7, A11, PARTFUN1:def 6

        .= ((F . ( - x)) - (G . ( - x))) by A6, A7, A11, VALUED_1: 13

        .= ((F /. ( - x)) - (G . ( - x))) by A5, A11, PARTFUN1:def 6

        .= ((F /. ( - x)) - (G /. ( - x))) by A3, A11, PARTFUN1:def 6

        .= (((F | A) /. ( - x)) - (G /. ( - x))) by A5, A8, A11, PARTFUN2: 17

        .= (((F | A) /. ( - x)) - ((G | A) /. ( - x))) by A3, A8, A11, PARTFUN2: 17

        .= (((F | A) . ( - x)) - ((G | A) /. ( - x))) by A14, PARTFUN1:def 6

        .= (((F | A) . ( - x)) - ((G | A) . ( - x))) by A15, PARTFUN1:def 6

        .= (( - ((F | A) . x)) - ((G | A) . ( - x))) by A9, A12, A14, Def6

        .= (( - ((F | A) . x)) - ( - ((G | A) . x))) by A4, A13, A15, Def6

        .= ( - (((F | A) . x) - ((G | A) . x)))

        .= ( - (((F | A) /. x) - ((G | A) . x))) by A12, PARTFUN1:def 6

        .= ( - (((F | A) /. x) - ((G | A) /. x))) by A13, PARTFUN1:def 6

        .= ( - ((F /. x) - ((G | A) /. x))) by A5, A8, A10, PARTFUN2: 17

        .= ( - ((F /. x) - (G /. x))) by A3, A8, A10, PARTFUN2: 17

        .= ( - ((F . x) - (G /. x))) by A5, A10, PARTFUN1:def 6

        .= ( - ((F . x) - (G . x))) by A3, A10, PARTFUN1:def 6

        .= ( - ((F - G) . x)) by A6, A7, A10, VALUED_1: 13

        .= ( - ((F - G) /. x)) by A6, A7, A10, PARTFUN1:def 6

        .= ( - (((F - G) | A) /. x)) by A6, A7, A8, A10, PARTFUN2: 17

        .= ( - (((F - G) | A) . x)) by A10, PARTFUN1:def 6;

        hence thesis;

      end;

      then ((F - G) | A) is with_symmetrical_domain quasi_odd by A8;

      hence thesis by A6, A7;

    end;

    theorem :: FUNCT_8:13

    F is_even_on A & G is_even_on A implies (F - G) is_even_on A

    proof

      assume that

       A1: F is_even_on A and

       A2: G is_even_on A;

      

       A3: A c= ( dom G) by A2;

      

       A4: (G | A) is even by A2;

      

       A5: A c= ( dom F) by A1;

      then

       A6: A c= (( dom F) /\ ( dom G)) by A3, XBOOLE_1: 19;

      

       A7: (( dom F) /\ ( dom G)) = ( dom (F - G)) by VALUED_1: 12;

      then

       A8: ( dom ((F - G) | A)) = A by A5, A3, RELAT_1: 62, XBOOLE_1: 19;

      

       A9: (F | A) is even by A1;

      for x st x in ( dom ((F - G) | A)) & ( - x) in ( dom ((F - G) | A)) holds (((F - G) | A) . ( - x)) = (((F - G) | A) . x)

      proof

        let x;

        assume that

         A10: x in ( dom ((F - G) | A)) and

         A11: ( - x) in ( dom ((F - G) | A));

        

         A12: x in ( dom (F | A)) by A5, A8, A10, RELAT_1: 62;

        

         A13: x in ( dom (G | A)) by A3, A8, A10, RELAT_1: 62;

        

         A14: ( - x) in ( dom (F | A)) by A5, A8, A11, RELAT_1: 62;

        

         A15: ( - x) in ( dom (G | A)) by A3, A8, A11, RELAT_1: 62;

        reconsider x as Element of REAL by XREAL_0:def 1;

        (((F - G) | A) . ( - x)) = (((F - G) | A) /. ( - x)) by A11, PARTFUN1:def 6

        .= ((F - G) /. ( - x)) by A6, A7, A8, A11, PARTFUN2: 17

        .= ((F - G) . ( - x)) by A6, A7, A11, PARTFUN1:def 6

        .= ((F . ( - x)) - (G . ( - x))) by A6, A7, A11, VALUED_1: 13

        .= ((F /. ( - x)) - (G . ( - x))) by A5, A11, PARTFUN1:def 6

        .= ((F /. ( - x)) - (G /. ( - x))) by A3, A11, PARTFUN1:def 6

        .= (((F | A) /. ( - x)) - (G /. ( - x))) by A5, A8, A11, PARTFUN2: 17

        .= (((F | A) /. ( - x)) - ((G | A) /. ( - x))) by A3, A8, A11, PARTFUN2: 17

        .= (((F | A) . ( - x)) - ((G | A) /. ( - x))) by A14, PARTFUN1:def 6

        .= (((F | A) . ( - x)) - ((G | A) . ( - x))) by A15, PARTFUN1:def 6

        .= (((F | A) . x) - ((G | A) . ( - x))) by A9, A12, A14, Def3

        .= (((F | A) . x) - ((G | A) . x)) by A4, A13, A15, Def3

        .= (((F | A) /. x) - ((G | A) . x)) by A12, PARTFUN1:def 6

        .= (((F | A) /. x) - ((G | A) /. x)) by A13, PARTFUN1:def 6

        .= ((F /. x) - ((G | A) /. x)) by A5, A8, A10, PARTFUN2: 17

        .= ((F /. x) - (G /. x)) by A3, A8, A10, PARTFUN2: 17

        .= ((F . x) - (G /. x)) by A5, A10, PARTFUN1:def 6

        .= ((F . x) - (G . x)) by A3, A10, PARTFUN1:def 6

        .= ((F - G) . x) by A6, A7, A10, VALUED_1: 13

        .= ((F - G) /. x) by A6, A7, A10, PARTFUN1:def 6

        .= (((F - G) | A) /. x) by A6, A7, A8, A10, PARTFUN2: 17

        .= (((F - G) | A) . x) by A10, PARTFUN1:def 6;

        hence thesis;

      end;

      then ((F - G) | A) is with_symmetrical_domain quasi_even by A8;

      hence thesis by A6, A7;

    end;

    theorem :: FUNCT_8:14

    F is_odd_on A implies (r (#) F) is_odd_on A

    proof

      assume

       A1: F is_odd_on A;

      then

       A2: A c= ( dom F);

      then

       A3: A c= ( dom (r (#) F)) by VALUED_1:def 5;

      then

       A4: ( dom ((r (#) F) | A)) = A by RELAT_1: 62;

      

       A5: (F | A) is odd by A1;

      for x st x in ( dom ((r (#) F) | A)) & ( - x) in ( dom ((r (#) F) | A)) holds (((r (#) F) | A) . ( - x)) = ( - (((r (#) F) | A) . x))

      proof

        let x;

        assume that

         A6: x in ( dom ((r (#) F) | A)) and

         A7: ( - x) in ( dom ((r (#) F) | A));

        

         A8: x in ( dom (F | A)) by A2, A4, A6, RELAT_1: 62;

        

         A9: ( - x) in ( dom (F | A)) by A2, A4, A7, RELAT_1: 62;

        reconsider x as Element of REAL by XREAL_0:def 1;

        (((r (#) F) | A) . ( - x)) = (((r (#) F) | A) /. ( - x)) by A7, PARTFUN1:def 6

        .= ((r (#) F) /. ( - x)) by A3, A4, A7, PARTFUN2: 17

        .= ((r (#) F) . ( - x)) by A3, A7, PARTFUN1:def 6

        .= (r * (F . ( - x))) by A3, A7, VALUED_1:def 5

        .= (r * (F /. ( - x))) by A2, A7, PARTFUN1:def 6

        .= (r * ((F | A) /. ( - x))) by A2, A4, A7, PARTFUN2: 17

        .= (r * ((F | A) . ( - x))) by A9, PARTFUN1:def 6

        .= (r * ( - ((F | A) . x))) by A5, A8, A9, Def6

        .= ( - (r * ((F | A) . x)))

        .= ( - (r * ((F | A) /. x))) by A8, PARTFUN1:def 6

        .= ( - (r * (F /. x))) by A2, A4, A6, PARTFUN2: 17

        .= ( - (r * (F . x))) by A2, A6, PARTFUN1:def 6

        .= ( - ((r (#) F) . x)) by A3, A6, VALUED_1:def 5

        .= ( - ((r (#) F) /. x)) by A3, A6, PARTFUN1:def 6

        .= ( - (((r (#) F) | A) /. x)) by A3, A4, A6, PARTFUN2: 17

        .= ( - (((r (#) F) | A) . x)) by A6, PARTFUN1:def 6;

        hence thesis;

      end;

      then ((r (#) F) | A) is with_symmetrical_domain quasi_odd by A4;

      hence thesis by A3;

    end;

    theorem :: FUNCT_8:15

    F is_even_on A implies (r (#) F) is_even_on A

    proof

      assume

       A1: F is_even_on A;

      then

       A2: A c= ( dom F);

      then

       A3: A c= ( dom (r (#) F)) by VALUED_1:def 5;

      then

       A4: ( dom ((r (#) F) | A)) = A by RELAT_1: 62;

      

       A5: (F | A) is even by A1;

      for x st x in ( dom ((r (#) F) | A)) & ( - x) in ( dom ((r (#) F) | A)) holds (((r (#) F) | A) . ( - x)) = (((r (#) F) | A) . x)

      proof

        let x;

        assume that

         A6: x in ( dom ((r (#) F) | A)) and

         A7: ( - x) in ( dom ((r (#) F) | A));

        

         A8: x in ( dom (F | A)) by A2, A4, A6, RELAT_1: 62;

        

         A9: ( - x) in ( dom (F | A)) by A2, A4, A7, RELAT_1: 62;

        reconsider x as Element of REAL by XREAL_0:def 1;

        (((r (#) F) | A) . ( - x)) = (((r (#) F) | A) /. ( - x)) by A7, PARTFUN1:def 6

        .= ((r (#) F) /. ( - x)) by A3, A4, A7, PARTFUN2: 17

        .= ((r (#) F) . ( - x)) by A3, A7, PARTFUN1:def 6

        .= (r * (F . ( - x))) by A3, A7, VALUED_1:def 5

        .= (r * (F /. ( - x))) by A2, A7, PARTFUN1:def 6

        .= (r * ((F | A) /. ( - x))) by A2, A4, A7, PARTFUN2: 17

        .= (r * ((F | A) . ( - x))) by A9, PARTFUN1:def 6

        .= (r * ((F | A) . x)) by A5, A8, A9, Def3

        .= (r * ((F | A) /. x)) by A8, PARTFUN1:def 6

        .= (r * (F /. x)) by A2, A4, A6, PARTFUN2: 17

        .= (r * (F . x)) by A2, A6, PARTFUN1:def 6

        .= ((r (#) F) . x) by A3, A6, VALUED_1:def 5

        .= ((r (#) F) /. x) by A3, A6, PARTFUN1:def 6

        .= (((r (#) F) | A) /. x) by A3, A4, A6, PARTFUN2: 17

        .= (((r (#) F) | A) . x) by A6, PARTFUN1:def 6;

        hence thesis;

      end;

      then ((r (#) F) | A) is with_symmetrical_domain quasi_even by A4;

      hence thesis by A3;

    end;

    theorem :: FUNCT_8:16

    

     Th16: F is_odd_on A implies ( - F) is_odd_on A

    proof

      assume

       A1: F is_odd_on A;

      then

       A2: A c= ( dom F);

      then

       A3: A c= ( dom ( - F)) by VALUED_1: 8;

      then

       A4: ( dom (( - F) | A)) = A by RELAT_1: 62;

      

       A5: (F | A) is odd by A1;

      for x st x in ( dom (( - F) | A)) & ( - x) in ( dom (( - F) | A)) holds ((( - F) | A) . ( - x)) = ( - ((( - F) | A) . x))

      proof

        let x;

        assume that

         A6: x in ( dom (( - F) | A)) and

         A7: ( - x) in ( dom (( - F) | A));

        

         A8: x in ( dom (F | A)) by A2, A4, A6, RELAT_1: 62;

        

         A9: ( - x) in ( dom (F | A)) by A2, A4, A7, RELAT_1: 62;

        reconsider x as Element of REAL by XREAL_0:def 1;

        ((( - F) | A) . ( - x)) = ((( - F) | A) /. ( - x)) by A7, PARTFUN1:def 6

        .= (( - F) /. ( - x)) by A3, A4, A7, PARTFUN2: 17

        .= (( - F) . ( - x)) by A3, A7, PARTFUN1:def 6

        .= ( - (F . ( - x))) by VALUED_1: 8

        .= ( - (F /. ( - x))) by A2, A7, PARTFUN1:def 6

        .= ( - ((F | A) /. ( - x))) by A2, A4, A7, PARTFUN2: 17

        .= ( - ((F | A) . ( - x))) by A9, PARTFUN1:def 6

        .= ( - ( - ((F | A) . x))) by A5, A8, A9, Def6

        .= ( - ( - ((F | A) /. x))) by A8, PARTFUN1:def 6

        .= ( - ( - (F /. x))) by A2, A4, A6, PARTFUN2: 17

        .= ( - ( - (F . x))) by A2, A6, PARTFUN1:def 6

        .= ( - (( - F) . x)) by VALUED_1: 8

        .= ( - (( - F) /. x)) by A3, A6, PARTFUN1:def 6

        .= ( - ((( - F) | A) /. x)) by A3, A4, A6, PARTFUN2: 17

        .= ( - ((( - F) | A) . x)) by A6, PARTFUN1:def 6;

        hence thesis;

      end;

      then (( - F) | A) is with_symmetrical_domain quasi_odd by A4;

      hence thesis by A3;

    end;

    theorem :: FUNCT_8:17

    

     Th17: F is_even_on A implies ( - F) is_even_on A

    proof

      assume

       A1: F is_even_on A;

      then

       A2: A c= ( dom F);

      then

       A3: A c= ( dom ( - F)) by VALUED_1: 8;

      then

       A4: ( dom (( - F) | A)) = A by RELAT_1: 62;

      

       A5: (F | A) is even by A1;

      for x st x in ( dom (( - F) | A)) & ( - x) in ( dom (( - F) | A)) holds ((( - F) | A) . ( - x)) = ((( - F) | A) . x)

      proof

        let x;

        assume that

         A6: x in ( dom (( - F) | A)) and

         A7: ( - x) in ( dom (( - F) | A));

        

         A8: x in ( dom (F | A)) by A2, A4, A6, RELAT_1: 62;

        

         A9: ( - x) in ( dom (F | A)) by A2, A4, A7, RELAT_1: 62;

        reconsider x as Element of REAL by XREAL_0:def 1;

        ((( - F) | A) . ( - x)) = ((( - F) | A) /. ( - x)) by A7, PARTFUN1:def 6

        .= (( - F) /. ( - x)) by A3, A4, A7, PARTFUN2: 17

        .= (( - F) . ( - x)) by A3, A7, PARTFUN1:def 6

        .= ( - (F . ( - x))) by VALUED_1: 8

        .= ( - (F /. ( - x))) by A2, A7, PARTFUN1:def 6

        .= ( - ((F | A) /. ( - x))) by A2, A4, A7, PARTFUN2: 17

        .= ( - ((F | A) . ( - x))) by A9, PARTFUN1:def 6

        .= ( - ((F | A) . x)) by A5, A8, A9, Def3

        .= ( - ((F | A) /. x)) by A8, PARTFUN1:def 6

        .= ( - (F /. x)) by A2, A4, A6, PARTFUN2: 17

        .= ( - (F . x)) by A2, A6, PARTFUN1:def 6

        .= (( - F) . x) by VALUED_1: 8

        .= (( - F) /. x) by A3, A6, PARTFUN1:def 6

        .= ((( - F) | A) /. x) by A3, A4, A6, PARTFUN2: 17

        .= ((( - F) | A) . x) by A6, PARTFUN1:def 6;

        hence thesis;

      end;

      then (( - F) | A) is with_symmetrical_domain quasi_even by A4;

      hence thesis by A3;

    end;

    theorem :: FUNCT_8:18

    

     Th18: F is_odd_on A implies (F " ) is_odd_on A

    proof

      assume

       A1: F is_odd_on A;

      then

       A2: A c= ( dom F);

      then

       A3: A c= ( dom (F " )) by VALUED_1:def 7;

      then

       A4: ( dom ((F " ) | A)) = A by RELAT_1: 62;

      

       A5: (F | A) is odd by A1;

      for x st x in ( dom ((F " ) | A)) & ( - x) in ( dom ((F " ) | A)) holds (((F " ) | A) . ( - x)) = ( - (((F " ) | A) . x))

      proof

        let x;

        assume that

         A6: x in ( dom ((F " ) | A)) and

         A7: ( - x) in ( dom ((F " ) | A));

        

         A8: x in ( dom (F | A)) by A2, A4, A6, RELAT_1: 62;

        

         A9: ( - x) in ( dom (F | A)) by A2, A4, A7, RELAT_1: 62;

        reconsider x as Element of REAL by XREAL_0:def 1;

        (((F " ) | A) . ( - x)) = (((F " ) | A) /. ( - x)) by A7, PARTFUN1:def 6

        .= ((F " ) /. ( - x)) by A3, A4, A7, PARTFUN2: 17

        .= ((F " ) . ( - x)) by A3, A7, PARTFUN1:def 6

        .= ((F . ( - x)) " ) by A3, A7, VALUED_1:def 7

        .= ((F /. ( - x)) " ) by A2, A7, PARTFUN1:def 6

        .= (((F | A) /. ( - x)) " ) by A2, A4, A7, PARTFUN2: 17

        .= (((F | A) . ( - x)) " ) by A9, PARTFUN1:def 6

        .= (( - ((F | A) . x)) " ) by A5, A8, A9, Def6

        .= (( - ((F | A) /. x)) " ) by A8, PARTFUN1:def 6

        .= (( - (F /. x)) " ) by A2, A4, A6, PARTFUN2: 17

        .= (( - (F . x)) " ) by A2, A6, PARTFUN1:def 6

        .= ( - ((F . x) " )) by XCMPLX_1: 222

        .= ( - ((F " ) . x)) by A3, A6, VALUED_1:def 7

        .= ( - ((F " ) /. x)) by A3, A6, PARTFUN1:def 6

        .= ( - (((F " ) | A) /. x)) by A3, A4, A6, PARTFUN2: 17

        .= ( - (((F " ) | A) . x)) by A6, PARTFUN1:def 6;

        hence thesis;

      end;

      then ((F " ) | A) is with_symmetrical_domain quasi_odd by A4;

      hence thesis by A3;

    end;

    theorem :: FUNCT_8:19

    

     Th19: F is_even_on A implies (F " ) is_even_on A

    proof

      assume

       A1: F is_even_on A;

      then

       A2: A c= ( dom F);

      then

       A3: A c= ( dom (F " )) by VALUED_1:def 7;

      then

       A4: ( dom ((F " ) | A)) = A by RELAT_1: 62;

      

       A5: (F | A) is even by A1;

      for x st x in ( dom ((F " ) | A)) & ( - x) in ( dom ((F " ) | A)) holds (((F " ) | A) . ( - x)) = (((F " ) | A) . x)

      proof

        let x;

        assume that

         A6: x in ( dom ((F " ) | A)) and

         A7: ( - x) in ( dom ((F " ) | A));

        

         A8: x in ( dom (F | A)) by A2, A4, A6, RELAT_1: 62;

        

         A9: ( - x) in ( dom (F | A)) by A2, A4, A7, RELAT_1: 62;

        reconsider x as Element of REAL by XREAL_0:def 1;

        (((F " ) | A) . ( - x)) = (((F " ) | A) /. ( - x)) by A7, PARTFUN1:def 6

        .= ((F " ) /. ( - x)) by A3, A4, A7, PARTFUN2: 17

        .= ((F " ) . ( - x)) by A3, A7, PARTFUN1:def 6

        .= ((F . ( - x)) " ) by A3, A7, VALUED_1:def 7

        .= ((F /. ( - x)) " ) by A2, A7, PARTFUN1:def 6

        .= (((F | A) /. ( - x)) " ) by A2, A4, A7, PARTFUN2: 17

        .= (((F | A) . ( - x)) " ) by A9, PARTFUN1:def 6

        .= (((F | A) . x) " ) by A5, A8, A9, Def3

        .= (((F | A) /. x) " ) by A8, PARTFUN1:def 6

        .= ((F /. x) " ) by A2, A4, A6, PARTFUN2: 17

        .= ((F . x) " ) by A2, A6, PARTFUN1:def 6

        .= ((F " ) . x) by A3, A6, VALUED_1:def 7

        .= ((F " ) /. x) by A3, A6, PARTFUN1:def 6

        .= (((F " ) | A) /. x) by A3, A4, A6, PARTFUN2: 17

        .= (((F " ) | A) . x) by A6, PARTFUN1:def 6;

        hence thesis;

      end;

      then ((F " ) | A) is with_symmetrical_domain quasi_even by A4;

      hence thesis by A3;

    end;

    theorem :: FUNCT_8:20

    

     Th20: F is_odd_on A implies |.F.| is_even_on A

    proof

      assume

       A1: F is_odd_on A;

      then

       A2: A c= ( dom F);

      then

       A3: A c= ( dom |.F.|) by VALUED_1:def 11;

      then

       A4: ( dom ( |.F.| | A)) = A by RELAT_1: 62;

      

       A5: (F | A) is odd by A1;

      for x st x in ( dom ( |.F.| | A)) & ( - x) in ( dom ( |.F.| | A)) holds (( |.F.| | A) . ( - x)) = (( |.F.| | A) . x)

      proof

        let x;

        assume that

         A6: x in ( dom ( |.F.| | A)) and

         A7: ( - x) in ( dom ( |.F.| | A));

        

         A8: x in ( dom (F | A)) by A2, A4, A6, RELAT_1: 62;

        

         A9: ( - x) in ( dom (F | A)) by A2, A4, A7, RELAT_1: 62;

        reconsider x as Element of REAL by XREAL_0:def 1;

        (( |.F.| | A) . ( - x)) = (( |.F.| | A) /. ( - x)) by A7, PARTFUN1:def 6

        .= ( |.F.| /. ( - x)) by A3, A4, A7, PARTFUN2: 17

        .= ( |.F.| . ( - x)) by A3, A7, PARTFUN1:def 6

        .= |.(F . ( - x)).| by A3, A7, VALUED_1:def 11

        .= |.(F /. ( - x)).| by A2, A7, PARTFUN1:def 6

        .= |.((F | A) /. ( - x)).| by A2, A4, A7, PARTFUN2: 17

        .= |.((F | A) . ( - x)).| by A9, PARTFUN1:def 6

        .= |.( - ((F | A) . x)).| by A5, A8, A9, Def6

        .= |.( - ((F | A) /. x)).| by A8, PARTFUN1:def 6

        .= |.( - (F /. x)).| by A2, A4, A6, PARTFUN2: 17

        .= |.( - (F . x)).| by A2, A6, PARTFUN1:def 6

        .= |.(F . x).| by COMPLEX1: 52

        .= ( |.F.| . x) by A3, A6, VALUED_1:def 11

        .= ( |.F.| /. x) by A3, A6, PARTFUN1:def 6

        .= (( |.F.| | A) /. x) by A3, A4, A6, PARTFUN2: 17

        .= (( |.F.| | A) . x) by A6, PARTFUN1:def 6;

        hence thesis;

      end;

      then ( |.F.| | A) is with_symmetrical_domain quasi_even by A4;

      hence thesis by A3;

    end;

    theorem :: FUNCT_8:21

    

     Th21: F is_even_on A implies |.F.| is_even_on A

    proof

      assume

       A1: F is_even_on A;

      then

       A2: A c= ( dom F);

      then

       A3: A c= ( dom |.F.|) by VALUED_1:def 11;

      then

       A4: ( dom ( |.F.| | A)) = A by RELAT_1: 62;

      

       A5: (F | A) is even by A1;

      for x st x in ( dom ( |.F.| | A)) & ( - x) in ( dom ( |.F.| | A)) holds (( |.F.| | A) . ( - x)) = (( |.F.| | A) . x)

      proof

        let x;

        assume that

         A6: x in ( dom ( |.F.| | A)) and

         A7: ( - x) in ( dom ( |.F.| | A));

        

         A8: x in ( dom (F | A)) by A2, A4, A6, RELAT_1: 62;

        

         A9: ( - x) in ( dom (F | A)) by A2, A4, A7, RELAT_1: 62;

        reconsider x as Element of REAL by XREAL_0:def 1;

        (( |.F.| | A) . ( - x)) = (( |.F.| | A) /. ( - x)) by A7, PARTFUN1:def 6

        .= ( |.F.| /. ( - x)) by A3, A4, A7, PARTFUN2: 17

        .= ( |.F.| . ( - x)) by A3, A7, PARTFUN1:def 6

        .= |.(F . ( - x)).| by A3, A7, VALUED_1:def 11

        .= |.(F /. ( - x)).| by A2, A7, PARTFUN1:def 6

        .= |.((F | A) /. ( - x)).| by A2, A4, A7, PARTFUN2: 17

        .= |.((F | A) . ( - x)).| by A9, PARTFUN1:def 6

        .= |.((F | A) . x).| by A5, A8, A9, Def3

        .= |.((F | A) /. x).| by A8, PARTFUN1:def 6

        .= |.(F /. x).| by A2, A4, A6, PARTFUN2: 17

        .= |.(F . x).| by A2, A6, PARTFUN1:def 6

        .= ( |.F.| . x) by A3, A6, VALUED_1:def 11

        .= ( |.F.| /. x) by A3, A6, PARTFUN1:def 6

        .= (( |.F.| | A) /. x) by A3, A4, A6, PARTFUN2: 17

        .= (( |.F.| | A) . x) by A6, PARTFUN1:def 6;

        hence thesis;

      end;

      then ( |.F.| | A) is with_symmetrical_domain quasi_even by A4;

      hence thesis by A3;

    end;

    theorem :: FUNCT_8:22

    

     Th22: F is_odd_on A & G is_odd_on A implies (F (#) G) is_even_on A

    proof

      assume that

       A1: F is_odd_on A and

       A2: G is_odd_on A;

      

       A3: A c= ( dom G) by A2;

      

       A4: (G | A) is odd by A2;

      

       A5: A c= ( dom F) by A1;

      then

       A6: A c= (( dom F) /\ ( dom G)) by A3, XBOOLE_1: 19;

      

       A7: (( dom F) /\ ( dom G)) = ( dom (F (#) G)) by VALUED_1:def 4;

      then

       A8: ( dom ((F (#) G) | A)) = A by A5, A3, RELAT_1: 62, XBOOLE_1: 19;

      

       A9: (F | A) is odd by A1;

      for x st x in ( dom ((F (#) G) | A)) & ( - x) in ( dom ((F (#) G) | A)) holds (((F (#) G) | A) . ( - x)) = (((F (#) G) | A) . x)

      proof

        let x;

        assume that

         A10: x in ( dom ((F (#) G) | A)) and

         A11: ( - x) in ( dom ((F (#) G) | A));

        

         A12: x in ( dom (F | A)) by A5, A8, A10, RELAT_1: 62;

        

         A13: x in ( dom (G | A)) by A3, A8, A10, RELAT_1: 62;

        

         A14: ( - x) in ( dom (F | A)) by A5, A8, A11, RELAT_1: 62;

        

         A15: ( - x) in ( dom (G | A)) by A3, A8, A11, RELAT_1: 62;

        reconsider x as Element of REAL by XREAL_0:def 1;

        (((F (#) G) | A) . ( - x)) = (((F (#) G) | A) /. ( - x)) by A11, PARTFUN1:def 6

        .= ((F (#) G) /. ( - x)) by A6, A7, A8, A11, PARTFUN2: 17

        .= ((F (#) G) . ( - x)) by A6, A7, A11, PARTFUN1:def 6

        .= ((F . ( - x)) * (G . ( - x))) by A6, A7, A11, VALUED_1:def 4

        .= ((F /. ( - x)) * (G . ( - x))) by A5, A11, PARTFUN1:def 6

        .= ((F /. ( - x)) * (G /. ( - x))) by A3, A11, PARTFUN1:def 6

        .= (((F | A) /. ( - x)) * (G /. ( - x))) by A5, A8, A11, PARTFUN2: 17

        .= (((F | A) /. ( - x)) * ((G | A) /. ( - x))) by A3, A8, A11, PARTFUN2: 17

        .= (((F | A) . ( - x)) * ((G | A) /. ( - x))) by A14, PARTFUN1:def 6

        .= (((F | A) . ( - x)) * ((G | A) . ( - x))) by A15, PARTFUN1:def 6

        .= (( - ((F | A) . x)) * ((G | A) . ( - x))) by A9, A12, A14, Def6

        .= (( - ((F | A) . x)) * ( - ((G | A) . x))) by A4, A13, A15, Def6

        .= (((F | A) . x) * ((G | A) . x))

        .= (((F | A) /. x) * ((G | A) . x)) by A12, PARTFUN1:def 6

        .= (((F | A) /. x) * ((G | A) /. x)) by A13, PARTFUN1:def 6

        .= ((F /. x) * ((G | A) /. x)) by A5, A8, A10, PARTFUN2: 17

        .= ((F /. x) * (G /. x)) by A3, A8, A10, PARTFUN2: 17

        .= ((F . x) * (G /. x)) by A5, A10, PARTFUN1:def 6

        .= ((F . x) * (G . x)) by A3, A10, PARTFUN1:def 6

        .= ((F (#) G) . x) by A6, A7, A10, VALUED_1:def 4

        .= ((F (#) G) /. x) by A6, A7, A10, PARTFUN1:def 6

        .= (((F (#) G) | A) /. x) by A6, A7, A8, A10, PARTFUN2: 17

        .= (((F (#) G) | A) . x) by A10, PARTFUN1:def 6;

        hence thesis;

      end;

      then ((F (#) G) | A) is with_symmetrical_domain quasi_even by A8;

      hence thesis by A6, A7;

    end;

    theorem :: FUNCT_8:23

    

     Th23: F is_even_on A & G is_even_on A implies (F (#) G) is_even_on A

    proof

      assume that

       A1: F is_even_on A and

       A2: G is_even_on A;

      

       A3: A c= ( dom G) by A2;

      

       A4: (G | A) is even by A2;

      

       A5: A c= ( dom F) by A1;

      then

       A6: A c= (( dom F) /\ ( dom G)) by A3, XBOOLE_1: 19;

      

       A7: (( dom F) /\ ( dom G)) = ( dom (F (#) G)) by VALUED_1:def 4;

      then

       A8: ( dom ((F (#) G) | A)) = A by A5, A3, RELAT_1: 62, XBOOLE_1: 19;

      

       A9: (F | A) is even by A1;

      for x st x in ( dom ((F (#) G) | A)) & ( - x) in ( dom ((F (#) G) | A)) holds (((F (#) G) | A) . ( - x)) = (((F (#) G) | A) . x)

      proof

        let x;

        assume that

         A10: x in ( dom ((F (#) G) | A)) and

         A11: ( - x) in ( dom ((F (#) G) | A));

        

         A12: x in ( dom (F | A)) by A5, A8, A10, RELAT_1: 62;

        

         A13: x in ( dom (G | A)) by A3, A8, A10, RELAT_1: 62;

        

         A14: ( - x) in ( dom (F | A)) by A5, A8, A11, RELAT_1: 62;

        

         A15: ( - x) in ( dom (G | A)) by A3, A8, A11, RELAT_1: 62;

        reconsider x as Element of REAL by XREAL_0:def 1;

        (((F (#) G) | A) . ( - x)) = (((F (#) G) | A) /. ( - x)) by A11, PARTFUN1:def 6

        .= ((F (#) G) /. ( - x)) by A6, A7, A8, A11, PARTFUN2: 17

        .= ((F (#) G) . ( - x)) by A6, A7, A11, PARTFUN1:def 6

        .= ((F . ( - x)) * (G . ( - x))) by A6, A7, A11, VALUED_1:def 4

        .= ((F /. ( - x)) * (G . ( - x))) by A5, A11, PARTFUN1:def 6

        .= ((F /. ( - x)) * (G /. ( - x))) by A3, A11, PARTFUN1:def 6

        .= (((F | A) /. ( - x)) * (G /. ( - x))) by A5, A8, A11, PARTFUN2: 17

        .= (((F | A) /. ( - x)) * ((G | A) /. ( - x))) by A3, A8, A11, PARTFUN2: 17

        .= (((F | A) . ( - x)) * ((G | A) /. ( - x))) by A14, PARTFUN1:def 6

        .= (((F | A) . ( - x)) * ((G | A) . ( - x))) by A15, PARTFUN1:def 6

        .= (((F | A) . x) * ((G | A) . ( - x))) by A9, A12, A14, Def3

        .= (((F | A) . x) * ((G | A) . x)) by A4, A13, A15, Def3

        .= (((F | A) /. x) * ((G | A) . x)) by A12, PARTFUN1:def 6

        .= (((F | A) /. x) * ((G | A) /. x)) by A13, PARTFUN1:def 6

        .= ((F /. x) * ((G | A) /. x)) by A5, A8, A10, PARTFUN2: 17

        .= ((F /. x) * (G /. x)) by A3, A8, A10, PARTFUN2: 17

        .= ((F . x) * (G /. x)) by A5, A10, PARTFUN1:def 6

        .= ((F . x) * (G . x)) by A3, A10, PARTFUN1:def 6

        .= ((F (#) G) . x) by A6, A7, A10, VALUED_1:def 4

        .= ((F (#) G) /. x) by A6, A7, A10, PARTFUN1:def 6

        .= (((F (#) G) | A) /. x) by A6, A7, A8, A10, PARTFUN2: 17

        .= (((F (#) G) | A) . x) by A10, PARTFUN1:def 6;

        hence thesis;

      end;

      then ((F (#) G) | A) is with_symmetrical_domain quasi_even by A8;

      hence thesis by A6, A7;

    end;

    theorem :: FUNCT_8:24

    F is_even_on A & G is_odd_on A implies (F (#) G) is_odd_on A

    proof

      assume that

       A1: F is_even_on A and

       A2: G is_odd_on A;

      

       A3: A c= ( dom G) by A2;

      

       A4: (G | A) is odd by A2;

      

       A5: A c= ( dom F) by A1;

      then

       A6: A c= (( dom F) /\ ( dom G)) by A3, XBOOLE_1: 19;

      

       A7: (( dom F) /\ ( dom G)) = ( dom (F (#) G)) by VALUED_1:def 4;

      then

       A8: ( dom ((F (#) G) | A)) = A by A5, A3, RELAT_1: 62, XBOOLE_1: 19;

      

       A9: (F | A) is even by A1;

      for x st x in ( dom ((F (#) G) | A)) & ( - x) in ( dom ((F (#) G) | A)) holds (((F (#) G) | A) . ( - x)) = ( - (((F (#) G) | A) . x))

      proof

        let x;

        assume that

         A10: x in ( dom ((F (#) G) | A)) and

         A11: ( - x) in ( dom ((F (#) G) | A));

        

         A12: x in ( dom (F | A)) by A5, A8, A10, RELAT_1: 62;

        

         A13: x in ( dom (G | A)) by A3, A8, A10, RELAT_1: 62;

        

         A14: ( - x) in ( dom (F | A)) by A5, A8, A11, RELAT_1: 62;

        

         A15: ( - x) in ( dom (G | A)) by A3, A8, A11, RELAT_1: 62;

        reconsider x as Element of REAL by XREAL_0:def 1;

        (((F (#) G) | A) . ( - x)) = (((F (#) G) | A) /. ( - x)) by A11, PARTFUN1:def 6

        .= ((F (#) G) /. ( - x)) by A6, A7, A8, A11, PARTFUN2: 17

        .= ((F (#) G) . ( - x)) by A6, A7, A11, PARTFUN1:def 6

        .= ((F . ( - x)) * (G . ( - x))) by A6, A7, A11, VALUED_1:def 4

        .= ((F /. ( - x)) * (G . ( - x))) by A5, A11, PARTFUN1:def 6

        .= ((F /. ( - x)) * (G /. ( - x))) by A3, A11, PARTFUN1:def 6

        .= (((F | A) /. ( - x)) * (G /. ( - x))) by A5, A8, A11, PARTFUN2: 17

        .= (((F | A) /. ( - x)) * ((G | A) /. ( - x))) by A3, A8, A11, PARTFUN2: 17

        .= (((F | A) . ( - x)) * ((G | A) /. ( - x))) by A14, PARTFUN1:def 6

        .= (((F | A) . ( - x)) * ((G | A) . ( - x))) by A15, PARTFUN1:def 6

        .= (((F | A) . x) * ((G | A) . ( - x))) by A9, A12, A14, Def3

        .= (((F | A) . x) * ( - ((G | A) . x))) by A4, A13, A15, Def6

        .= ( - (((F | A) . x) * ((G | A) . x)))

        .= ( - (((F | A) /. x) * ((G | A) . x))) by A12, PARTFUN1:def 6

        .= ( - (((F | A) /. x) * ((G | A) /. x))) by A13, PARTFUN1:def 6

        .= ( - ((F /. x) * ((G | A) /. x))) by A5, A8, A10, PARTFUN2: 17

        .= ( - ((F /. x) * (G /. x))) by A3, A8, A10, PARTFUN2: 17

        .= ( - ((F . x) * (G /. x))) by A5, A10, PARTFUN1:def 6

        .= ( - ((F . x) * (G . x))) by A3, A10, PARTFUN1:def 6

        .= ( - ((F (#) G) . x)) by A6, A7, A10, VALUED_1:def 4

        .= ( - ((F (#) G) /. x)) by A6, A7, A10, PARTFUN1:def 6

        .= ( - (((F (#) G) | A) /. x)) by A6, A7, A8, A10, PARTFUN2: 17

        .= ( - (((F (#) G) | A) . x)) by A10, PARTFUN1:def 6;

        hence thesis;

      end;

      then ((F (#) G) | A) is with_symmetrical_domain quasi_odd by A8;

      hence thesis by A6, A7;

    end;

    theorem :: FUNCT_8:25

    F is_even_on A implies (r + F) is_even_on A

    proof

      assume

       A1: F is_even_on A;

      then

       A2: A c= ( dom F);

      then

       A3: A c= ( dom (r + F)) by VALUED_1:def 2;

      then

       A4: ( dom ((r + F) | A)) = A by RELAT_1: 62;

      

       A5: (F | A) is even by A1;

      for x st x in ( dom ((r + F) | A)) & ( - x) in ( dom ((r + F) | A)) holds (((r + F) | A) . ( - x)) = (((r + F) | A) . x)

      proof

        let x;

        assume that

         A6: x in ( dom ((r + F) | A)) and

         A7: ( - x) in ( dom ((r + F) | A));

        

         A8: x in ( dom (F | A)) by A2, A4, A6, RELAT_1: 62;

        

         A9: ( - x) in ( dom (F | A)) by A2, A4, A7, RELAT_1: 62;

        reconsider x as Element of REAL by XREAL_0:def 1;

        (((r + F) | A) . ( - x)) = (((r + F) | A) /. ( - x)) by A7, PARTFUN1:def 6

        .= ((r + F) /. ( - x)) by A3, A4, A7, PARTFUN2: 17

        .= ((r + F) . ( - x)) by A3, A7, PARTFUN1:def 6

        .= (r + (F . ( - x))) by A3, A7, VALUED_1:def 2

        .= (r + (F /. ( - x))) by A2, A7, PARTFUN1:def 6

        .= (r + ((F | A) /. ( - x))) by A2, A4, A7, PARTFUN2: 17

        .= (r + ((F | A) . ( - x))) by A9, PARTFUN1:def 6

        .= (r + ((F | A) . x)) by A5, A8, A9, Def3

        .= (r + ((F | A) /. x)) by A8, PARTFUN1:def 6

        .= (r + (F /. x)) by A2, A4, A6, PARTFUN2: 17

        .= (r + (F . x)) by A2, A6, PARTFUN1:def 6

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

        .= ((r + F) /. x) by A3, A6, PARTFUN1:def 6

        .= (((r + F) | A) /. x) by A3, A4, A6, PARTFUN2: 17

        .= (((r + F) | A) . x) by A6, PARTFUN1:def 6;

        hence thesis;

      end;

      then ((r + F) | A) is with_symmetrical_domain quasi_even by A4;

      hence thesis by A3;

    end;

    theorem :: FUNCT_8:26

    F is_even_on A implies (F - r) is_even_on A

    proof

      assume

       A1: F is_even_on A;

      then

       A2: A c= ( dom F);

      then

       A3: A c= ( dom (F - r)) by VALUED_1: 3;

      then

       A4: ( dom ((F - r) | A)) = A by RELAT_1: 62;

      

       A5: (F | A) is even by A1;

      for x st x in ( dom ((F - r) | A)) & ( - x) in ( dom ((F - r) | A)) holds (((F - r) | A) . ( - x)) = (((F - r) | A) . x)

      proof

        let x;

        assume that

         A6: x in ( dom ((F - r) | A)) and

         A7: ( - x) in ( dom ((F - r) | A));

        

         A8: x in ( dom (F | A)) by A2, A4, A6, RELAT_1: 62;

        

         A9: ( - x) in ( dom (F | A)) by A2, A4, A7, RELAT_1: 62;

        reconsider x as Element of REAL by XREAL_0:def 1;

        (((F - r) | A) . ( - x)) = (((F - r) | A) /. ( - x)) by A7, PARTFUN1:def 6

        .= ((F - r) /. ( - x)) by A3, A4, A7, PARTFUN2: 17

        .= ((F - r) . ( - x)) by A3, A7, PARTFUN1:def 6

        .= ((F . ( - x)) - r) by A2, A7, VALUED_1: 3

        .= ((F /. ( - x)) - r) by A2, A7, PARTFUN1:def 6

        .= (((F | A) /. ( - x)) - r) by A2, A4, A7, PARTFUN2: 17

        .= (((F | A) . ( - x)) - r) by A9, PARTFUN1:def 6

        .= (((F | A) . x) - r) by A5, A8, A9, Def3

        .= (((F | A) /. x) - r) by A8, PARTFUN1:def 6

        .= ((F /. x) - r) by A2, A4, A6, PARTFUN2: 17

        .= ((F . x) - r) by A2, A6, PARTFUN1:def 6

        .= ((F - r) . x) by A2, A6, VALUED_1: 3

        .= ((F - r) /. x) by A3, A6, PARTFUN1:def 6

        .= (((F - r) | A) /. x) by A3, A4, A6, PARTFUN2: 17

        .= (((F - r) | A) . x) by A6, PARTFUN1:def 6;

        hence thesis;

      end;

      then ((F - r) | A) is with_symmetrical_domain quasi_even by A4;

      hence thesis by A3;

    end;

    theorem :: FUNCT_8:27

    F is_even_on A implies (F ^2 ) is_even_on A by Th23;

    theorem :: FUNCT_8:28

    F is_odd_on A implies (F ^2 ) is_even_on A by Th22;

    theorem :: FUNCT_8:29

    F is_odd_on A & G is_odd_on A implies (F /" G) is_even_on A

    proof

      assume that

       A1: F is_odd_on A and

       A2: G is_odd_on A;

      

       A3: A c= ( dom G) by A2;

      

       A4: (G | A) is odd by A2;

      

       A5: A c= ( dom F) by A1;

      then

       A6: A c= (( dom F) /\ ( dom G)) by A3, XBOOLE_1: 19;

      

       A7: (( dom F) /\ ( dom G)) = ( dom (F /" G)) by VALUED_1: 16;

      then

       A8: ( dom ((F /" G) | A)) = A by A5, A3, RELAT_1: 62, XBOOLE_1: 19;

      

       A9: (F | A) is odd by A1;

      for x st x in ( dom ((F /" G) | A)) & ( - x) in ( dom ((F /" G) | A)) holds (((F /" G) | A) . ( - x)) = (((F /" G) | A) . x)

      proof

        let x;

        assume that

         A10: x in ( dom ((F /" G) | A)) and

         A11: ( - x) in ( dom ((F /" G) | A));

        

         A12: x in ( dom (F | A)) by A5, A8, A10, RELAT_1: 62;

        

         A13: x in ( dom (G | A)) by A3, A8, A10, RELAT_1: 62;

        

         A14: ( - x) in ( dom (F | A)) by A5, A8, A11, RELAT_1: 62;

        

         A15: ( - x) in ( dom (G | A)) by A3, A8, A11, RELAT_1: 62;

        reconsider x as Element of REAL by XREAL_0:def 1;

        (((F /" G) | A) . ( - x)) = (((F /" G) | A) /. ( - x)) by A11, PARTFUN1:def 6

        .= ((F /" G) /. ( - x)) by A6, A7, A8, A11, PARTFUN2: 17

        .= ((F /" G) . ( - x)) by A6, A7, A11, PARTFUN1:def 6

        .= ((F . ( - x)) / (G . ( - x))) by VALUED_1: 17

        .= ((F /. ( - x)) / (G . ( - x))) by A5, A11, PARTFUN1:def 6

        .= ((F /. ( - x)) / (G /. ( - x))) by A3, A11, PARTFUN1:def 6

        .= (((F | A) /. ( - x)) / (G /. ( - x))) by A5, A8, A11, PARTFUN2: 17

        .= (((F | A) /. ( - x)) / ((G | A) /. ( - x))) by A3, A8, A11, PARTFUN2: 17

        .= (((F | A) . ( - x)) / ((G | A) /. ( - x))) by A14, PARTFUN1:def 6

        .= (((F | A) . ( - x)) / ((G | A) . ( - x))) by A15, PARTFUN1:def 6

        .= (( - ((F | A) . x)) / ((G | A) . ( - x))) by A9, A12, A14, Def6

        .= (( - ((F | A) . x)) / ( - ((G | A) . x))) by A4, A13, A15, Def6

        .= (((F | A) . x) / ((G | A) . x)) by XCMPLX_1: 191

        .= (((F | A) /. x) / ((G | A) . x)) by A12, PARTFUN1:def 6

        .= (((F | A) /. x) / ((G | A) /. x)) by A13, PARTFUN1:def 6

        .= ((F /. x) / ((G | A) /. x)) by A5, A8, A10, PARTFUN2: 17

        .= ((F /. x) / (G /. x)) by A3, A8, A10, PARTFUN2: 17

        .= ((F . x) / (G /. x)) by A5, A10, PARTFUN1:def 6

        .= ((F . x) / (G . x)) by A3, A10, PARTFUN1:def 6

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

        .= ((F /" G) /. x) by A6, A7, A10, PARTFUN1:def 6

        .= (((F /" G) | A) /. x) by A6, A7, A8, A10, PARTFUN2: 17

        .= (((F /" G) | A) . x) by A10, PARTFUN1:def 6;

        hence thesis;

      end;

      then ((F /" G) | A) is with_symmetrical_domain quasi_even by A8;

      hence thesis by A6, A7;

    end;

    theorem :: FUNCT_8:30

    F is_even_on A & G is_even_on A implies (F /" G) is_even_on A

    proof

      assume that

       A1: F is_even_on A and

       A2: G is_even_on A;

      

       A3: A c= ( dom G) by A2;

      

       A4: (G | A) is even by A2;

      

       A5: A c= ( dom F) by A1;

      then

       A6: A c= (( dom F) /\ ( dom G)) by A3, XBOOLE_1: 19;

      

       A7: (( dom F) /\ ( dom G)) = ( dom (F /" G)) by VALUED_1: 16;

      then

       A8: ( dom ((F /" G) | A)) = A by A5, A3, RELAT_1: 62, XBOOLE_1: 19;

      

       A9: (F | A) is even by A1;

      for x st x in ( dom ((F /" G) | A)) & ( - x) in ( dom ((F /" G) | A)) holds (((F /" G) | A) . ( - x)) = (((F /" G) | A) . x)

      proof

        let x;

        assume that

         A10: x in ( dom ((F /" G) | A)) and

         A11: ( - x) in ( dom ((F /" G) | A));

        

         A12: x in ( dom (F | A)) by A5, A8, A10, RELAT_1: 62;

        

         A13: x in ( dom (G | A)) by A3, A8, A10, RELAT_1: 62;

        

         A14: ( - x) in ( dom (F | A)) by A5, A8, A11, RELAT_1: 62;

        

         A15: ( - x) in ( dom (G | A)) by A3, A8, A11, RELAT_1: 62;

        reconsider x as Element of REAL by XREAL_0:def 1;

        (((F /" G) | A) . ( - x)) = (((F /" G) | A) /. ( - x)) by A11, PARTFUN1:def 6

        .= ((F /" G) /. ( - x)) by A6, A7, A8, A11, PARTFUN2: 17

        .= ((F /" G) . ( - x)) by A6, A7, A11, PARTFUN1:def 6

        .= ((F . ( - x)) / (G . ( - x))) by VALUED_1: 17

        .= ((F /. ( - x)) / (G . ( - x))) by A5, A11, PARTFUN1:def 6

        .= ((F /. ( - x)) / (G /. ( - x))) by A3, A11, PARTFUN1:def 6

        .= (((F | A) /. ( - x)) / (G /. ( - x))) by A5, A8, A11, PARTFUN2: 17

        .= (((F | A) /. ( - x)) / ((G | A) /. ( - x))) by A3, A8, A11, PARTFUN2: 17

        .= (((F | A) . ( - x)) / ((G | A) /. ( - x))) by A14, PARTFUN1:def 6

        .= (((F | A) . ( - x)) / ((G | A) . ( - x))) by A15, PARTFUN1:def 6

        .= (((F | A) . x) / ((G | A) . ( - x))) by A9, A12, A14, Def3

        .= (((F | A) . x) / ((G | A) . x)) by A4, A13, A15, Def3

        .= (((F | A) /. x) / ((G | A) . x)) by A12, PARTFUN1:def 6

        .= (((F | A) /. x) / ((G | A) /. x)) by A13, PARTFUN1:def 6

        .= ((F /. x) / ((G | A) /. x)) by A5, A8, A10, PARTFUN2: 17

        .= ((F /. x) / (G /. x)) by A3, A8, A10, PARTFUN2: 17

        .= ((F . x) / (G /. x)) by A5, A10, PARTFUN1:def 6

        .= ((F . x) / (G . x)) by A3, A10, PARTFUN1:def 6

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

        .= ((F /" G) /. x) by A6, A7, A10, PARTFUN1:def 6

        .= (((F /" G) | A) /. x) by A6, A7, A8, A10, PARTFUN2: 17

        .= (((F /" G) | A) . x) by A10, PARTFUN1:def 6;

        hence thesis;

      end;

      then ((F /" G) | A) is with_symmetrical_domain quasi_even by A8;

      hence thesis by A6, A7;

    end;

    theorem :: FUNCT_8:31

    F is_odd_on A & G is_even_on A implies (F /" G) is_odd_on A

    proof

      assume that

       A1: F is_odd_on A and

       A2: G is_even_on A;

      

       A3: A c= ( dom G) by A2;

      

       A4: (G | A) is even by A2;

      

       A5: A c= ( dom F) by A1;

      then

       A6: A c= (( dom F) /\ ( dom G)) by A3, XBOOLE_1: 19;

      

       A7: (( dom F) /\ ( dom G)) = ( dom (F /" G)) by VALUED_1: 16;

      then

       A8: ( dom ((F /" G) | A)) = A by A5, A3, RELAT_1: 62, XBOOLE_1: 19;

      

       A9: (F | A) is odd by A1;

      for x st x in ( dom ((F /" G) | A)) & ( - x) in ( dom ((F /" G) | A)) holds (((F /" G) | A) . ( - x)) = ( - (((F /" G) | A) . x))

      proof

        let x;

        assume that

         A10: x in ( dom ((F /" G) | A)) and

         A11: ( - x) in ( dom ((F /" G) | A));

        

         A12: x in ( dom (F | A)) by A5, A8, A10, RELAT_1: 62;

        

         A13: x in ( dom (G | A)) by A3, A8, A10, RELAT_1: 62;

        

         A14: ( - x) in ( dom (F | A)) by A5, A8, A11, RELAT_1: 62;

        

         A15: ( - x) in ( dom (G | A)) by A3, A8, A11, RELAT_1: 62;

        reconsider x as Element of REAL by XREAL_0:def 1;

        (((F /" G) | A) . ( - x)) = (((F /" G) | A) /. ( - x)) by A11, PARTFUN1:def 6

        .= ((F /" G) /. ( - x)) by A6, A7, A8, A11, PARTFUN2: 17

        .= ((F /" G) . ( - x)) by A6, A7, A11, PARTFUN1:def 6

        .= ((F . ( - x)) / (G . ( - x))) by VALUED_1: 17

        .= ((F /. ( - x)) / (G . ( - x))) by A5, A11, PARTFUN1:def 6

        .= ((F /. ( - x)) / (G /. ( - x))) by A3, A11, PARTFUN1:def 6

        .= (((F | A) /. ( - x)) / (G /. ( - x))) by A5, A8, A11, PARTFUN2: 17

        .= (((F | A) /. ( - x)) / ((G | A) /. ( - x))) by A3, A8, A11, PARTFUN2: 17

        .= (((F | A) . ( - x)) / ((G | A) /. ( - x))) by A14, PARTFUN1:def 6

        .= (((F | A) . ( - x)) / ((G | A) . ( - x))) by A15, PARTFUN1:def 6

        .= (( - ((F | A) . x)) / ((G | A) . ( - x))) by A9, A12, A14, Def6

        .= (( - ((F | A) . x)) / ((G | A) . x)) by A4, A13, A15, Def3

        .= ( - (((F | A) . x) / ((G | A) . x)))

        .= ( - (((F | A) /. x) / ((G | A) . x))) by A12, PARTFUN1:def 6

        .= ( - (((F | A) /. x) / ((G | A) /. x))) by A13, PARTFUN1:def 6

        .= ( - ((F /. x) / ((G | A) /. x))) by A5, A8, A10, PARTFUN2: 17

        .= ( - ((F /. x) / (G /. x))) by A3, A8, A10, PARTFUN2: 17

        .= ( - ((F . x) / (G /. x))) by A5, A10, PARTFUN1:def 6

        .= ( - ((F . x) / (G . x))) by A3, A10, PARTFUN1:def 6

        .= ( - ((F /" G) . x)) by VALUED_1: 17

        .= ( - ((F /" G) /. x)) by A6, A7, A10, PARTFUN1:def 6

        .= ( - (((F /" G) | A) /. x)) by A6, A7, A8, A10, PARTFUN2: 17

        .= ( - (((F /" G) | A) . x)) by A10, PARTFUN1:def 6;

        hence thesis;

      end;

      then ((F /" G) | A) is with_symmetrical_domain quasi_odd by A8;

      hence thesis by A6, A7;

    end;

    theorem :: FUNCT_8:32

    F is_even_on A & G is_odd_on A implies (F /" G) is_odd_on A

    proof

      assume that

       A1: F is_even_on A and

       A2: G is_odd_on A;

      

       A3: A c= ( dom G) by A2;

      

       A4: (G | A) is odd by A2;

      

       A5: A c= ( dom F) by A1;

      then

       A6: A c= (( dom F) /\ ( dom G)) by A3, XBOOLE_1: 19;

      

       A7: (( dom F) /\ ( dom G)) = ( dom (F /" G)) by VALUED_1: 16;

      then

       A8: ( dom ((F /" G) | A)) = A by A5, A3, RELAT_1: 62, XBOOLE_1: 19;

      

       A9: (F | A) is even by A1;

      for x st x in ( dom ((F /" G) | A)) & ( - x) in ( dom ((F /" G) | A)) holds (((F /" G) | A) . ( - x)) = ( - (((F /" G) | A) . x))

      proof

        let x;

        assume that

         A10: x in ( dom ((F /" G) | A)) and

         A11: ( - x) in ( dom ((F /" G) | A));

        

         A12: x in ( dom (F | A)) by A5, A8, A10, RELAT_1: 62;

        

         A13: x in ( dom (G | A)) by A3, A8, A10, RELAT_1: 62;

        

         A14: ( - x) in ( dom (F | A)) by A5, A8, A11, RELAT_1: 62;

        

         A15: ( - x) in ( dom (G | A)) by A3, A8, A11, RELAT_1: 62;

        reconsider x as Element of REAL by XREAL_0:def 1;

        (((F /" G) | A) . ( - x)) = (((F /" G) | A) /. ( - x)) by A11, PARTFUN1:def 6

        .= ((F /" G) /. ( - x)) by A6, A7, A8, A11, PARTFUN2: 17

        .= ((F /" G) . ( - x)) by A6, A7, A11, PARTFUN1:def 6

        .= ((F . ( - x)) / (G . ( - x))) by VALUED_1: 17

        .= ((F /. ( - x)) / (G . ( - x))) by A5, A11, PARTFUN1:def 6

        .= ((F /. ( - x)) / (G /. ( - x))) by A3, A11, PARTFUN1:def 6

        .= (((F | A) /. ( - x)) / (G /. ( - x))) by A5, A8, A11, PARTFUN2: 17

        .= (((F | A) /. ( - x)) / ((G | A) /. ( - x))) by A3, A8, A11, PARTFUN2: 17

        .= (((F | A) . ( - x)) / ((G | A) /. ( - x))) by A14, PARTFUN1:def 6

        .= (((F | A) . ( - x)) / ((G | A) . ( - x))) by A15, PARTFUN1:def 6

        .= (((F | A) . x) / ((G | A) . ( - x))) by A9, A12, A14, Def3

        .= (((F | A) . x) / ( - ((G | A) . x))) by A4, A13, A15, Def6

        .= ( - (((F | A) . x) / ((G | A) . x))) by XCMPLX_1: 188

        .= ( - (((F | A) /. x) / ((G | A) . x))) by A12, PARTFUN1:def 6

        .= ( - (((F | A) /. x) / ((G | A) /. x))) by A13, PARTFUN1:def 6

        .= ( - ((F /. x) / ((G | A) /. x))) by A5, A8, A10, PARTFUN2: 17

        .= ( - ((F /. x) / (G /. x))) by A3, A8, A10, PARTFUN2: 17

        .= ( - ((F . x) / (G /. x))) by A5, A10, PARTFUN1:def 6

        .= ( - ((F . x) / (G . x))) by A3, A10, PARTFUN1:def 6

        .= ( - ((F /" G) . x)) by VALUED_1: 17

        .= ( - ((F /" G) /. x)) by A6, A7, A10, PARTFUN1:def 6

        .= ( - (((F /" G) | A) /. x)) by A6, A7, A8, A10, PARTFUN2: 17

        .= ( - (((F /" G) | A) . x)) by A10, PARTFUN1:def 6;

        hence thesis;

      end;

      then ((F /" G) | A) is with_symmetrical_domain quasi_odd by A8;

      hence thesis by A6, A7;

    end;

    theorem :: FUNCT_8:33

    F is odd implies ( - F) is odd

    proof

      

       A1: ( dom F) = ( dom ( - F)) by VALUED_1: 8;

      assume

       A2: F is odd;

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

      proof

        let x;

        assume

         A3: x in ( dom ( - F)) & ( - x) in ( dom ( - F));

        (( - F) . ( - x)) = ( - (F . ( - x))) by VALUED_1: 8

        .= ( - ( - (F . x))) by A2, A1, A3, Def6

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

        hence thesis;

      end;

      then ( - F) is with_symmetrical_domain quasi_odd by A2, A1;

      hence thesis;

    end;

    theorem :: FUNCT_8:34

    F is even implies ( - F) is even

    proof

      

       A1: ( dom F) = ( dom ( - F)) by VALUED_1: 8;

      assume

       A2: F is even;

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

      proof

        let x;

        assume

         A3: x in ( dom ( - F)) & ( - x) in ( dom ( - F));

        (( - F) . ( - x)) = ( - (F . ( - x))) by VALUED_1: 8

        .= ( - (F . x)) by A2, A1, A3, Def3

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

        hence thesis;

      end;

      then ( - F) is with_symmetrical_domain quasi_even by A2, A1;

      hence thesis;

    end;

    theorem :: FUNCT_8:35

    F is odd implies (F " ) is odd

    proof

      

       A1: ( dom F) = ( dom (F " )) by VALUED_1:def 7;

      assume

       A2: F is odd;

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

      proof

        let x;

        assume that

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

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

        ((F " ) . ( - x)) = ((F . ( - x)) " ) by A4, VALUED_1:def 7

        .= (( - (F . x)) " ) by A2, A1, A3, A4, Def6

        .= ( - ((F . x) " )) by XCMPLX_1: 222

        .= ( - ((F " ) . x)) by A3, VALUED_1:def 7;

        hence thesis;

      end;

      then (F " ) is with_symmetrical_domain quasi_odd by A2, A1;

      hence thesis;

    end;

    theorem :: FUNCT_8:36

    F is even implies (F " ) is even

    proof

      

       A1: ( dom F) = ( dom (F " )) by VALUED_1:def 7;

      assume

       A2: F is even;

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

      proof

        let x;

        assume that

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

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

        ((F " ) . ( - x)) = ((F . ( - x)) " ) by A4, VALUED_1:def 7

        .= ((F . x) " ) by A2, A1, A3, A4, Def3

        .= ((F " ) . x) by A3, VALUED_1:def 7;

        hence thesis;

      end;

      then (F " ) is with_symmetrical_domain quasi_even by A2, A1;

      hence thesis;

    end;

    theorem :: FUNCT_8:37

    F is odd implies |.F.| is even

    proof

      

       A1: ( dom F) = ( dom |.F.|) by VALUED_1:def 11;

      assume

       A2: F is odd;

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

      proof

        let x;

        assume that

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

         A4: ( - x) in ( dom |.F.|);

        ( |.F.| . ( - x)) = |.(F . ( - x)).| by A4, VALUED_1:def 11

        .= |.( - (F . x)).| by A2, A1, A3, A4, Def6

        .= |.(F . x).| by COMPLEX1: 52

        .= ( |.F.| . x) by A3, VALUED_1:def 11;

        hence thesis;

      end;

      then |.F.| is with_symmetrical_domain quasi_even by A2, A1;

      hence thesis;

    end;

    theorem :: FUNCT_8:38

    F is even implies |.F.| is even

    proof

      

       A1: ( dom F) = ( dom |.F.|) by VALUED_1:def 11;

      assume

       A2: F is even;

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

      proof

        let x;

        assume that

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

         A4: ( - x) in ( dom |.F.|);

        ( |.F.| . ( - x)) = |.(F . ( - x)).| by A4, VALUED_1:def 11

        .= |.(F . x).| by A2, A1, A3, A4, Def3

        .= ( |.F.| . x) by A3, VALUED_1:def 11;

        hence thesis;

      end;

      then |.F.| is with_symmetrical_domain quasi_even by A2, A1;

      hence thesis;

    end;

    theorem :: FUNCT_8:39

    F is odd implies (F ^2 ) is even

    proof

      

       A1: ( dom F) = ( dom (F ^2 )) by VALUED_1: 11;

      assume

       A2: F is odd;

      for x st x in ( dom (F ^2 )) & ( - x) in ( dom (F ^2 )) holds ((F ^2 ) . ( - x)) = ((F ^2 ) . x)

      proof

        let x;

        assume

         A3: x in ( dom (F ^2 )) & ( - x) in ( dom (F ^2 ));

        ((F ^2 ) . ( - x)) = ((F . ( - x)) ^2 ) by VALUED_1: 11

        .= (( - (F . x)) ^2 ) by A2, A1, A3, Def6

        .= ((F . x) ^2 )

        .= ((F ^2 ) . x) by VALUED_1: 11;

        hence thesis;

      end;

      then (F ^2 ) is with_symmetrical_domain quasi_even by A2, A1;

      hence thesis;

    end;

    theorem :: FUNCT_8:40

    F is even implies (F ^2 ) is even

    proof

      

       A1: ( dom F) = ( dom (F ^2 )) by VALUED_1: 11;

      assume

       A2: F is even;

      for x st x in ( dom (F ^2 )) & ( - x) in ( dom (F ^2 )) holds ((F ^2 ) . ( - x)) = ((F ^2 ) . x)

      proof

        let x;

        assume

         A3: x in ( dom (F ^2 )) & ( - x) in ( dom (F ^2 ));

        ((F ^2 ) . ( - x)) = ((F . ( - x)) ^2 ) by VALUED_1: 11

        .= ((F . x) ^2 ) by A2, A1, A3, Def3

        .= ((F ^2 ) . x) by VALUED_1: 11;

        hence thesis;

      end;

      then (F ^2 ) is with_symmetrical_domain quasi_even by A2, A1;

      hence thesis;

    end;

    theorem :: FUNCT_8:41

    F is even implies (r + F) is even

    proof

      

       A1: ( dom F) = ( dom (r + F)) by VALUED_1:def 2;

      assume

       A2: F is even;

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

      proof

        let x;

        assume that

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

         A4: ( - x) in ( dom (r + F));

        ((r + F) . ( - x)) = (r + (F . ( - x))) by A4, VALUED_1:def 2

        .= (r + (F . x)) by A2, A1, A3, A4, Def3

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

        hence thesis;

      end;

      then (r + F) is with_symmetrical_domain quasi_even by A2, A1;

      hence thesis;

    end;

    theorem :: FUNCT_8:42

    F is even implies (F - r) is even

    proof

      

       A1: ( dom F) = ( dom (F - r)) by VALUED_1: 3;

      assume

       A2: F is even;

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

      proof

        let x;

        assume that

         A3: x in ( dom (F - r)) and

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

        

         A5: x in ( dom F) by A3, VALUED_1: 3;

        ( - x) in ( dom F) by A4, VALUED_1: 3;

        

        then ((F - r) . ( - x)) = ((F . ( - x)) - r) by VALUED_1: 3

        .= ((F . x) - r) by A2, A1, A3, A4, Def3

        .= ((F - r) . x) by A5, VALUED_1: 3;

        hence thesis;

      end;

      then (F - r) is with_symmetrical_domain quasi_even by A2, A1;

      hence thesis;

    end;

    theorem :: FUNCT_8:43

    F is odd implies (r (#) F) is odd

    proof

      

       A1: ( dom F) = ( dom (r (#) F)) by VALUED_1:def 5;

      assume

       A2: F is odd;

      for x st x in ( dom (r (#) F)) & ( - x) in ( dom (r (#) F)) holds ((r (#) F) . ( - x)) = ( - ((r (#) F) . x))

      proof

        let x;

        assume that

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

         A4: ( - x) in ( dom (r (#) F));

        ((r (#) F) . ( - x)) = (r * (F . ( - x))) by A4, VALUED_1:def 5

        .= (r * ( - (F . x))) by A2, A1, A3, A4, Def6

        .= ( - (r * (F . x)))

        .= ( - ((r (#) F) . x)) by A3, VALUED_1:def 5;

        hence thesis;

      end;

      then (r (#) F) is with_symmetrical_domain quasi_odd by A2, A1;

      hence thesis;

    end;

    theorem :: FUNCT_8:44

    F is even implies (r (#) F) is even

    proof

      

       A1: ( dom F) = ( dom (r (#) F)) by VALUED_1:def 5;

      assume

       A2: F is even;

      for x st x in ( dom (r (#) F)) & ( - x) in ( dom (r (#) F)) holds ((r (#) F) . ( - x)) = ((r (#) F) . x)

      proof

        let x;

        assume that

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

         A4: ( - x) in ( dom (r (#) F));

        ((r (#) F) . ( - x)) = (r * (F . ( - x))) by A4, VALUED_1:def 5

        .= (r * (F . x)) by A2, A1, A3, A4, Def3

        .= ((r (#) F) . x) by A3, VALUED_1:def 5;

        hence thesis;

      end;

      then (r (#) F) is with_symmetrical_domain quasi_even by A2, A1;

      hence thesis;

    end;

    theorem :: FUNCT_8:45

    F is odd & G is odd & (( dom F) /\ ( dom G)) is symmetrical implies (F + G) is odd

    proof

      assume that

       A1: F is odd and

       A2: G is odd and

       A3: (( dom F) /\ ( dom G)) is symmetrical;

      

       A4: (( dom F) /\ ( dom G)) = ( dom (F + G)) by VALUED_1:def 1;

      then

       A5: ( dom (F + G)) c= ( dom G) by XBOOLE_1: 17;

      

       A6: ( dom (F + G)) c= ( dom F) by A4, XBOOLE_1: 17;

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

      proof

        let x;

        assume that

         A7: x in ( dom (F + G)) and

         A8: ( - x) in ( dom (F + G));

        ((F + G) . ( - x)) = ((F . ( - x)) + (G . ( - x))) by A8, VALUED_1:def 1

        .= (( - (F . x)) + (G . ( - x))) by A1, A6, A7, A8, Def6

        .= (( - (F . x)) + ( - (G . x))) by A2, A5, A7, A8, Def6

        .= ( - ((F . x) + (G . x)))

        .= ( - ((F + G) . x)) by A7, VALUED_1:def 1;

        hence thesis;

      end;

      then (F + G) is with_symmetrical_domain quasi_odd by A3, A4;

      hence thesis;

    end;

    theorem :: FUNCT_8:46

    F is even & G is even & (( dom F) /\ ( dom G)) is symmetrical implies (F + G) is even

    proof

      assume that

       A1: F is even and

       A2: G is even and

       A3: (( dom F) /\ ( dom G)) is symmetrical;

      

       A4: (( dom F) /\ ( dom G)) = ( dom (F + G)) by VALUED_1:def 1;

      then

       A5: ( dom (F + G)) c= ( dom G) by XBOOLE_1: 17;

      

       A6: ( dom (F + G)) c= ( dom F) by A4, XBOOLE_1: 17;

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

      proof

        let x;

        assume that

         A7: x in ( dom (F + G)) and

         A8: ( - x) in ( dom (F + G));

        ((F + G) . ( - x)) = ((F . ( - x)) + (G . ( - x))) by A8, VALUED_1:def 1

        .= ((F . x) + (G . ( - x))) by A1, A6, A7, A8, Def3

        .= ((F . x) + (G . x)) by A2, A5, A7, A8, Def3

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

        hence thesis;

      end;

      then (F + G) is with_symmetrical_domain quasi_even by A3, A4;

      hence thesis;

    end;

    theorem :: FUNCT_8:47

    F is odd & G is odd & (( dom F) /\ ( dom G)) is symmetrical implies (F - G) is odd

    proof

      assume that

       A1: F is odd and

       A2: G is odd and

       A3: (( dom F) /\ ( dom G)) is symmetrical;

      

       A4: (( dom F) /\ ( dom G)) = ( dom (F - G)) by VALUED_1: 12;

      then

       A5: ( dom (F - G)) c= ( dom G) by XBOOLE_1: 17;

      

       A6: ( dom (F - G)) c= ( dom F) by A4, XBOOLE_1: 17;

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

      proof

        let x;

        assume that

         A7: x in ( dom (F - G)) and

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

        ((F - G) . ( - x)) = ((F . ( - x)) - (G . ( - x))) by A8, VALUED_1: 13

        .= (( - (F . x)) - (G . ( - x))) by A1, A6, A7, A8, Def6

        .= (( - (F . x)) - ( - (G . x))) by A2, A5, A7, A8, Def6

        .= ( - ((F . x) - (G . x)))

        .= ( - ((F - G) . x)) by A7, VALUED_1: 13;

        hence thesis;

      end;

      then (F - G) is with_symmetrical_domain quasi_odd by A3, A4;

      hence thesis;

    end;

    theorem :: FUNCT_8:48

    F is even & G is even & (( dom F) /\ ( dom G)) is symmetrical implies (F - G) is even

    proof

      assume that

       A1: F is even and

       A2: G is even and

       A3: (( dom F) /\ ( dom G)) is symmetrical;

      

       A4: (( dom F) /\ ( dom G)) = ( dom (F - G)) by VALUED_1: 12;

      then

       A5: ( dom (F - G)) c= ( dom G) by XBOOLE_1: 17;

      

       A6: ( dom (F - G)) c= ( dom F) by A4, XBOOLE_1: 17;

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

      proof

        let x;

        assume that

         A7: x in ( dom (F - G)) and

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

        ((F - G) . ( - x)) = ((F . ( - x)) - (G . ( - x))) by A8, VALUED_1: 13

        .= ((F . x) - (G . ( - x))) by A1, A6, A7, A8, Def3

        .= ((F . x) - (G . x)) by A2, A5, A7, A8, Def3

        .= ((F - G) . x) by A7, VALUED_1: 13;

        hence thesis;

      end;

      then (F - G) is with_symmetrical_domain quasi_even by A3, A4;

      hence thesis;

    end;

    theorem :: FUNCT_8:49

    F is odd & G is odd & (( dom F) /\ ( dom G)) is symmetrical implies (F (#) G) is even

    proof

      assume that

       A1: F is odd and

       A2: G is odd and

       A3: (( dom F) /\ ( dom G)) is symmetrical;

      

       A4: (( dom F) /\ ( dom G)) = ( dom (F (#) G)) by VALUED_1:def 4;

      then

       A5: ( dom (F (#) G)) c= ( dom G) by XBOOLE_1: 17;

      

       A6: ( dom (F (#) G)) c= ( dom F) by A4, XBOOLE_1: 17;

      for x st x in ( dom (F (#) G)) & ( - x) in ( dom (F (#) G)) holds ((F (#) G) . ( - x)) = ((F (#) G) . x)

      proof

        let x;

        assume that

         A7: x in ( dom (F (#) G)) and

         A8: ( - x) in ( dom (F (#) G));

        ((F (#) G) . ( - x)) = ((F . ( - x)) * (G . ( - x))) by A8, VALUED_1:def 4

        .= (( - (F . x)) * (G . ( - x))) by A1, A6, A7, A8, Def6

        .= (( - (F . x)) * ( - (G . x))) by A2, A5, A7, A8, Def6

        .= ((F . x) * (G . x))

        .= ((F (#) G) . x) by A7, VALUED_1:def 4;

        hence thesis;

      end;

      then (F (#) G) is with_symmetrical_domain quasi_even by A3, A4;

      hence thesis;

    end;

    theorem :: FUNCT_8:50

    F is even & G is even & (( dom F) /\ ( dom G)) is symmetrical implies (F (#) G) is even

    proof

      assume that

       A1: F is even and

       A2: G is even and

       A3: (( dom F) /\ ( dom G)) is symmetrical;

      

       A4: (( dom F) /\ ( dom G)) = ( dom (F (#) G)) by VALUED_1:def 4;

      then

       A5: ( dom (F (#) G)) c= ( dom G) by XBOOLE_1: 17;

      

       A6: ( dom (F (#) G)) c= ( dom F) by A4, XBOOLE_1: 17;

      for x st x in ( dom (F (#) G)) & ( - x) in ( dom (F (#) G)) holds ((F (#) G) . ( - x)) = ((F (#) G) . x)

      proof

        let x;

        assume that

         A7: x in ( dom (F (#) G)) and

         A8: ( - x) in ( dom (F (#) G));

        ((F (#) G) . ( - x)) = ((F . ( - x)) * (G . ( - x))) by A8, VALUED_1:def 4

        .= ((F . x) * (G . ( - x))) by A1, A6, A7, A8, Def3

        .= ((F . x) * (G . x)) by A2, A5, A7, A8, Def3

        .= ((F (#) G) . x) by A7, VALUED_1:def 4;

        hence thesis;

      end;

      then (F (#) G) is with_symmetrical_domain quasi_even by A3, A4;

      hence thesis;

    end;

    theorem :: FUNCT_8:51

    F is even & G is odd & (( dom F) /\ ( dom G)) is symmetrical implies (F (#) G) is odd

    proof

      assume that

       A1: F is even and

       A2: G is odd and

       A3: (( dom F) /\ ( dom G)) is symmetrical;

      

       A4: (( dom F) /\ ( dom G)) = ( dom (F (#) G)) by VALUED_1:def 4;

      then

       A5: ( dom (F (#) G)) c= ( dom G) by XBOOLE_1: 17;

      

       A6: ( dom (F (#) G)) c= ( dom F) by A4, XBOOLE_1: 17;

      for x st x in ( dom (F (#) G)) & ( - x) in ( dom (F (#) G)) holds ((F (#) G) . ( - x)) = ( - ((F (#) G) . x))

      proof

        let x;

        assume that

         A7: x in ( dom (F (#) G)) and

         A8: ( - x) in ( dom (F (#) G));

        ((F (#) G) . ( - x)) = ((F . ( - x)) * (G . ( - x))) by A8, VALUED_1:def 4

        .= ((F . x) * (G . ( - x))) by A1, A6, A7, A8, Def3

        .= ((F . x) * ( - (G . x))) by A2, A5, A7, A8, Def6

        .= ( - ((F . x) * (G . x)))

        .= ( - ((F (#) G) . x)) by A7, VALUED_1:def 4;

        hence thesis;

      end;

      then (F (#) G) is with_symmetrical_domain quasi_odd by A3, A4;

      hence thesis;

    end;

    theorem :: FUNCT_8:52

    F is odd & G is odd & (( dom F) /\ ( dom G)) is symmetrical implies (F /" G) is even

    proof

      assume that

       A1: F is odd and

       A2: G is odd and

       A3: (( dom F) /\ ( dom G)) is symmetrical;

      

       A4: (( dom F) /\ ( dom G)) = ( dom (F /" G)) by VALUED_1: 16;

      then

       A5: ( dom (F /" G)) c= ( dom G) by XBOOLE_1: 17;

      

       A6: ( dom (F /" G)) c= ( dom F) by A4, XBOOLE_1: 17;

      for x st x in ( dom (F /" G)) & ( - x) in ( dom (F /" G)) holds ((F /" G) . ( - x)) = ((F /" G) . x)

      proof

        let x;

        assume

         A7: x in ( dom (F /" G)) & ( - x) in ( dom (F /" G));

        ((F /" G) . ( - x)) = ((F . ( - x)) / (G . ( - x))) by VALUED_1: 17

        .= (( - (F . x)) / (G . ( - x))) by A1, A6, A7, Def6

        .= (( - (F . x)) / ( - (G . x))) by A2, A5, A7, Def6

        .= ((F . x) / (G . x)) by XCMPLX_1: 191

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

        hence thesis;

      end;

      then (F /" G) is with_symmetrical_domain quasi_even by A3, A4;

      hence thesis;

    end;

    theorem :: FUNCT_8:53

    F is even & G is even & (( dom F) /\ ( dom G)) is symmetrical implies (F /" G) is even

    proof

      assume that

       A1: F is even and

       A2: G is even and

       A3: (( dom F) /\ ( dom G)) is symmetrical;

      

       A4: (( dom F) /\ ( dom G)) = ( dom (F /" G)) by VALUED_1: 16;

      then

       A5: ( dom (F /" G)) c= ( dom G) by XBOOLE_1: 17;

      

       A6: ( dom (F /" G)) c= ( dom F) by A4, XBOOLE_1: 17;

      for x st x in ( dom (F /" G)) & ( - x) in ( dom (F /" G)) holds ((F /" G) . ( - x)) = ((F /" G) . x)

      proof

        let x;

        assume

         A7: x in ( dom (F /" G)) & ( - x) in ( dom (F /" G));

        ((F /" G) . ( - x)) = ((F . ( - x)) / (G . ( - x))) by VALUED_1: 17

        .= ((F . x) / (G . ( - x))) by A1, A6, A7, Def3

        .= ((F . x) / (G . x)) by A2, A5, A7, Def3

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

        hence thesis;

      end;

      then (F /" G) is with_symmetrical_domain quasi_even by A3, A4;

      hence thesis;

    end;

    theorem :: FUNCT_8:54

    F is odd & G is even & (( dom F) /\ ( dom G)) is symmetrical implies (F /" G) is odd

    proof

      assume that

       A1: F is odd and

       A2: G is even and

       A3: (( dom F) /\ ( dom G)) is symmetrical;

      

       A4: (( dom F) /\ ( dom G)) = ( dom (F /" G)) by VALUED_1: 16;

      then

       A5: ( dom (F /" G)) c= ( dom G) by XBOOLE_1: 17;

      

       A6: ( dom (F /" G)) c= ( dom F) by A4, XBOOLE_1: 17;

      for x st x in ( dom (F /" G)) & ( - x) in ( dom (F /" G)) holds ((F /" G) . ( - x)) = ( - ((F /" G) . x))

      proof

        let x;

        assume

         A7: x in ( dom (F /" G)) & ( - x) in ( dom (F /" G));

        ((F /" G) . ( - x)) = ((F . ( - x)) / (G . ( - x))) by VALUED_1: 17

        .= (( - (F . x)) / (G . ( - x))) by A1, A6, A7, Def6

        .= (( - (F . x)) / (G . x)) by A2, A5, A7, Def3

        .= ( - ((F . x) / (G . x)))

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

        hence thesis;

      end;

      then (F /" G) is with_symmetrical_domain quasi_odd by A3, A4;

      hence thesis;

    end;

    theorem :: FUNCT_8:55

    F is even & G is odd & (( dom F) /\ ( dom G)) is symmetrical implies (F /" G) is odd

    proof

      assume that

       A1: F is even and

       A2: G is odd and

       A3: (( dom F) /\ ( dom G)) is symmetrical;

      

       A4: (( dom F) /\ ( dom G)) = ( dom (F /" G)) by VALUED_1: 16;

      then

       A5: ( dom (F /" G)) c= ( dom G) by XBOOLE_1: 17;

      

       A6: ( dom (F /" G)) c= ( dom F) by A4, XBOOLE_1: 17;

      for x st x in ( dom (F /" G)) & ( - x) in ( dom (F /" G)) holds ((F /" G) . ( - x)) = ( - ((F /" G) . x))

      proof

        let x;

        assume

         A7: x in ( dom (F /" G)) & ( - x) in ( dom (F /" G));

        ((F /" G) . ( - x)) = ((F . ( - x)) / (G . ( - x))) by VALUED_1: 17

        .= ((F . x) / (G . ( - x))) by A1, A6, A7, Def3

        .= ((F . x) / ( - (G . x))) by A2, A5, A7, Def6

        .= ( - ((F . x) / (G . x))) by XCMPLX_1: 188

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

        hence thesis;

      end;

      then (F /" G) is with_symmetrical_domain quasi_odd by A3, A4;

      hence thesis;

    end;

    begin

    definition

      :: FUNCT_8:def9

      func signum -> Function of REAL , REAL means

      : Def9: for x be Real holds (it . x) = ( sgn x);

      existence

      proof

        deffunc U( Real) = ( In (( sgn $1), REAL ));

        consider f be Function of REAL , REAL such that

         A1: for x be Element of REAL holds (f . x) = U(x) from FUNCT_2:sch 4;

        take f;

        let x be Real;

        x in REAL by XREAL_0:def 1;

        then (f . x) = U(x) by A1;

        hence thesis;

      end;

      uniqueness

      proof

        let f1,f2 be Function of REAL , REAL ;

        assume

         A2: for x be Real holds (f1 . x) = ( sgn x);

        assume

         A3: for x be Real holds (f2 . x) = ( sgn x);

        for x be Element of REAL holds (f1 . x) = (f2 . x)

        proof

          let x be Element of REAL ;

          

          thus (f1 . x) = ( sgn x) by A2

          .= (f2 . x) by A3;

        end;

        hence f1 = f2 by FUNCT_2: 63;

      end;

    end

    theorem :: FUNCT_8:56

    

     Th56: for x be Real st x > 0 holds ( signum . x) = 1

    proof

      let x be Real;

      assume

       A1: 0 < x;

      ( signum . x) = ( sgn x) by Def9

      .= 1 by A1, ABSVALUE:def 2;

      hence thesis;

    end;

    theorem :: FUNCT_8:57

    

     Th57: for x be Real st x < 0 holds ( signum . x) = ( - 1)

    proof

      let x be Real;

      assume

       A1: 0 > x;

      ( signum . x) = ( sgn x) by Def9

      .= ( - 1) by A1, ABSVALUE:def 2;

      hence thesis;

    end;

    theorem :: FUNCT_8:58

    

     Th58: ( signum . 0 ) = 0

    proof

      ( signum . 0 ) = ( sgn 0 ) by Def9

      .= 0 by ABSVALUE:def 2;

      hence thesis;

    end;

    theorem :: FUNCT_8:59

    

     Th59: for x be Real holds ( signum . ( - x)) = ( - ( signum . x))

    proof

      let x be Real;

      per cases ;

        suppose

         A1: x < 0 ;

        then ( signum . x) = ( - 1) by Th57;

        hence thesis by A1, Th56;

      end;

        suppose

         A2: 0 < x;

        then ( signum . x) = 1 by Th56;

        hence thesis by A2, Th57;

      end;

        suppose x = 0 ;

        hence thesis by Th58;

      end;

    end;

    theorem :: FUNCT_8:60

    for A be symmetrical Subset of REAL holds signum is_odd_on A

    proof

      let A be symmetrical Subset of REAL ;

      

       A1: ( dom signum ) = REAL by FUNCT_2:def 1;

      then

       A2: ( dom ( signum | A)) = A by RELAT_1: 62;

      for x st x in ( dom ( signum | A)) & ( - x) in ( dom ( signum | A)) holds (( signum | A) . ( - x)) = ( - (( signum | A) . x))

      proof

        let x;

        assume that

         A3: x in ( dom ( signum | A)) and

         A4: ( - x) in ( dom ( signum | A));

        reconsider x as Element of REAL by XREAL_0:def 1;

        (( signum | A) . ( - x)) = (( signum | A) /. ( - x)) by A4, PARTFUN1:def 6

        .= ( signum /. ( - x)) by A1, A4, PARTFUN2: 17

        .= ( - ( signum /. x)) by Th59

        .= ( - (( signum | A) /. x)) by A1, A3, PARTFUN2: 17

        .= ( - (( signum | A) . x)) by A3, PARTFUN1:def 6;

        hence thesis;

      end;

      then ( signum | A) is with_symmetrical_domain quasi_odd by A2;

      hence thesis by A1;

    end;

    theorem :: FUNCT_8:61

    

     Th61: for x be Real st x >= 0 holds ( absreal . x) = x

    proof

      let x be Real;

      assume

       A1: 0 <= x;

      ( absreal . x) = |.x.| by EUCLID:def 2

      .= x by A1, ABSVALUE:def 1;

      hence thesis;

    end;

    theorem :: FUNCT_8:62

    

     Th62: for x be Real st x < 0 holds ( absreal . x) = ( - x)

    proof

      let x be Real;

      assume

       A1: 0 > x;

      ( absreal . x) = |.x.| by EUCLID:def 2

      .= ( - x) by A1, ABSVALUE:def 1;

      hence thesis;

    end;

    theorem :: FUNCT_8:63

    

     Th63: for x be Real holds ( absreal . ( - x)) = ( absreal . x)

    proof

      let x be Real;

      per cases ;

        suppose

         A1: x < 0 ;

        then ( absreal . ( - x)) = ( - x) by Th61;

        hence thesis by A1, Th62;

      end;

        suppose

         A2: 0 < x;

        

        then ( absreal . ( - x)) = ( - ( - x)) by Th62

        .= x;

        hence thesis by A2, Th61;

      end;

        suppose x = 0 ;

        hence thesis;

      end;

    end;

    theorem :: FUNCT_8:64

    for A be symmetrical Subset of REAL holds absreal is_even_on A

    proof

      let A be symmetrical Subset of REAL ;

      

       A1: ( dom absreal ) = REAL by FUNCT_2:def 1;

      then

       A2: ( dom ( absreal | A)) = A by RELAT_1: 62;

      for x st x in ( dom ( absreal | A)) & ( - x) in ( dom ( absreal | A)) holds (( absreal | A) . ( - x)) = (( absreal | A) . x)

      proof

        let x;

        assume that

         A3: x in ( dom ( absreal | A)) and

         A4: ( - x) in ( dom ( absreal | A));

        reconsider x as Element of REAL by XREAL_0:def 1;

        (( absreal | A) . ( - x)) = (( absreal | A) /. ( - x)) by A4, PARTFUN1:def 6

        .= ( absreal /. ( - x)) by A1, A4, PARTFUN2: 17

        .= ( absreal /. x) by Th63

        .= (( absreal | A) /. x) by A1, A3, PARTFUN2: 17

        .= (( absreal | A) . x) by A3, PARTFUN1:def 6;

        hence thesis;

      end;

      then ( absreal | A) is with_symmetrical_domain quasi_even by A2;

      hence thesis by A1;

    end;

    theorem :: FUNCT_8:65

    

     Th65: for A be symmetrical Subset of REAL holds sin is_odd_on A

    proof

      let A be symmetrical Subset of REAL ;

      

       A1: ( dom ( sin | A)) = A by RELAT_1: 62, SIN_COS: 24;

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

      proof

        let x;

        assume that

         A2: x in ( dom ( sin | A)) and

         A3: ( - x) in ( dom ( sin | A));

        reconsider x as Element of REAL by XREAL_0:def 1;

        (( sin | A) . ( - x)) = (( sin | A) /. ( - x)) by A3, PARTFUN1:def 6

        .= ( sin /. ( - x)) by A3, PARTFUN2: 17, SIN_COS: 24

        .= ( - ( sin /. x)) by SIN_COS: 30

        .= ( - (( sin | A) /. x)) by A2, PARTFUN2: 17, SIN_COS: 24

        .= ( - (( sin | A) . x)) by A2, PARTFUN1:def 6;

        hence thesis;

      end;

      then ( sin | A) is with_symmetrical_domain quasi_odd by A1;

      hence thesis by SIN_COS: 24;

    end;

    theorem :: FUNCT_8:66

    

     Th66: for A be symmetrical Subset of REAL holds cos is_even_on A

    proof

      let A be symmetrical Subset of REAL ;

      

       A1: ( dom ( cos | A)) = A by RELAT_1: 62, SIN_COS: 24;

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

      proof

        let x;

        assume that

         A2: x in ( dom ( cos | A)) and

         A3: ( - x) in ( dom ( cos | A));

        reconsider x as Element of REAL by XREAL_0:def 1;

        (( cos | A) . ( - x)) = (( cos | A) /. ( - x)) by A3, PARTFUN1:def 6

        .= ( cos /. ( - x)) by A3, PARTFUN2: 17, SIN_COS: 24

        .= ( cos /. x) by SIN_COS: 30

        .= (( cos | A) /. x) by A2, PARTFUN2: 17, SIN_COS: 24

        .= (( cos | A) . x) by A2, PARTFUN1:def 6;

        hence thesis;

      end;

      then ( cos | A) is with_symmetrical_domain quasi_even by A1;

      hence thesis by SIN_COS: 24;

    end;

    registration

      cluster sin -> odd;

      coherence

      proof

        for x be Complex st x in REAL holds ( - x) in REAL by XREAL_0:def 1;

        then (for x st x in ( dom sin ) & ( - x) in ( dom sin ) holds ( sin . ( - x)) = ( - ( sin . x))) & REAL is symmetrical by SIN_COS: 30;

        then sin is with_symmetrical_domain quasi_odd by SIN_COS: 24;

        hence thesis;

      end;

    end

    registration

      cluster cos -> even;

      coherence

      proof

        for x st x in ( dom cos ) & ( - x) in ( dom cos ) holds ( cos . ( - x)) = ( cos . x) by SIN_COS: 30;

        then cos is with_symmetrical_domain quasi_even by SIN_COS: 24;

        hence thesis;

      end;

    end

    theorem :: FUNCT_8:67

    for A be symmetrical Subset of REAL holds sinh is_odd_on A

    proof

      let A be symmetrical Subset of REAL ;

      

       A1: ( dom sinh ) = REAL by FUNCT_2:def 1;

      then

       A2: ( dom ( sinh | A)) = A by RELAT_1: 62;

      for x st x in ( dom ( sinh | A)) & ( - x) in ( dom ( sinh | A)) holds (( sinh | A) . ( - x)) = ( - (( sinh | A) . x))

      proof

        let x;

        assume that

         A3: x in ( dom ( sinh | A)) and

         A4: ( - x) in ( dom ( sinh | A));

        reconsider x as Element of REAL by XREAL_0:def 1;

        (( sinh | A) . ( - x)) = (( sinh | A) /. ( - x)) by A4, PARTFUN1:def 6

        .= ( sinh /. ( - x)) by A1, A4, PARTFUN2: 17

        .= ( - ( sinh /. x)) by SIN_COS2: 19

        .= ( - (( sinh | A) /. x)) by A1, A3, PARTFUN2: 17

        .= ( - (( sinh | A) . x)) by A3, PARTFUN1:def 6;

        hence thesis;

      end;

      then ( sinh | A) is with_symmetrical_domain quasi_odd by A2;

      hence thesis by A1;

    end;

    theorem :: FUNCT_8:68

    for A be symmetrical Subset of REAL holds cosh is_even_on A

    proof

      let A be symmetrical Subset of REAL ;

      

       A1: ( dom cosh ) = REAL by FUNCT_2:def 1;

      then

       A2: ( dom ( cosh | A)) = A by RELAT_1: 62;

      for x st x in ( dom ( cosh | A)) & ( - x) in ( dom ( cosh | A)) holds (( cosh | A) . ( - x)) = (( cosh | A) . x)

      proof

        let x;

        assume that

         A3: x in ( dom ( cosh | A)) and

         A4: ( - x) in ( dom ( cosh | A));

        reconsider x as Element of REAL by XREAL_0:def 1;

        (( cosh | A) . ( - x)) = (( cosh | A) /. ( - x)) by A4, PARTFUN1:def 6

        .= ( cosh /. ( - x)) by A1, A4, PARTFUN2: 17

        .= ( cosh /. x) by SIN_COS2: 19

        .= (( cosh | A) /. x) by A1, A3, PARTFUN2: 17

        .= (( cosh | A) . x) by A3, PARTFUN1:def 6;

        hence thesis;

      end;

      then ( cosh | A) is with_symmetrical_domain quasi_even by A2;

      hence thesis by A1;

    end;

    registration

      cluster sinh -> odd;

      coherence

      proof

        for x be Complex st x in REAL holds ( - x) in REAL by XREAL_0:def 1;

        then

         A1: REAL is symmetrical;

        (for x st x in ( dom sinh ) & ( - x) in ( dom sinh ) holds ( sinh . ( - x)) = ( - ( sinh . x))) & ( dom sinh ) = REAL by FUNCT_2:def 1, SIN_COS2: 19;

        then sinh is with_symmetrical_domain quasi_odd by A1;

        hence thesis;

      end;

    end

    registration

      cluster cosh -> even;

      coherence

      proof

        for x be Complex st x in REAL holds ( - x) in REAL by XREAL_0:def 1;

        then

         A1: REAL is symmetrical;

        (for x st x in ( dom cosh ) & ( - x) in ( dom cosh ) holds ( cosh . ( - x)) = ( cosh . x)) & ( dom cosh ) = REAL by FUNCT_2:def 1, SIN_COS2: 19;

        then cosh is with_symmetrical_domain quasi_even by A1;

        hence thesis;

      end;

    end

    theorem :: FUNCT_8:69

    A c= ].( - ( PI / 2)), ( PI / 2).[ implies tan is_odd_on A

    proof

      assume

       A1: A c= ].( - ( PI / 2)), ( PI / 2).[;

      then

       A2: A c= ( dom tan ) by SIN_COS9: 1;

      

       A3: ( dom ( tan | A)) = A by A1, RELAT_1: 62, SIN_COS9: 1, XBOOLE_1: 1;

      

       A4: for x st x in A holds ( tan . ( - x)) = ( - ( tan . x))

      proof

        let x;

        assume

         A5: x in A;

        then ( - x) in A by Def1;

        

        then ( tan . ( - x)) = ( tan ( - x)) by A1, SIN_COS9: 13

        .= ( - ( tan x)) by SIN_COS4: 1

        .= ( - ( tan . x)) by A1, A5, SIN_COS9: 13;

        hence thesis;

      end;

      for x st x in ( dom ( tan | A)) & ( - x) in ( dom ( tan | A)) holds (( tan | A) . ( - x)) = ( - (( tan | A) . x))

      proof

        let x;

        assume that

         A6: x in ( dom ( tan | A)) and

         A7: ( - x) in ( dom ( tan | A));

        reconsider x as Element of REAL by XREAL_0:def 1;

        (( tan | A) . ( - x)) = (( tan | A) /. ( - x)) by A7, PARTFUN1:def 6

        .= ( tan /. ( - x)) by A2, A3, A7, PARTFUN2: 17

        .= ( tan . ( - x)) by A2, A7, PARTFUN1:def 6

        .= ( - ( tan . x)) by A4, A6

        .= ( - ( tan /. x)) by A2, A6, PARTFUN1:def 6

        .= ( - (( tan | A) /. x)) by A2, A3, A6, PARTFUN2: 17

        .= ( - (( tan | A) . x)) by A6, PARTFUN1:def 6;

        hence thesis;

      end;

      then ( tan | A) is with_symmetrical_domain quasi_odd by A3;

      hence thesis by A2;

    end;

    theorem :: FUNCT_8:70

    A c= ( dom tan ) implies tan is_odd_on A

    proof

      assume that

       A1: A c= ( dom tan );

      

       A2: ( dom ( tan | A)) = A by A1, RELAT_1: 62;

      

       A3: for x st x in A holds ( tan . ( - x)) = ( - ( tan . x))

      proof

        let x;

        assume

         A4: x in A;

        then

         A5: ( cos . x) <> 0 by A1, FDIFF_8: 1;

        ( - x) in A by Def1, A4;

        

        then ( tan . ( - x)) = ( tan ( - x)) by A1, FDIFF_8: 1, SIN_COS9: 15

        .= ( - ( tan x)) by SIN_COS4: 1

        .= ( - ( tan . x)) by A5, SIN_COS9: 15;

        hence thesis;

      end;

      for x st x in ( dom ( tan | A)) & ( - x) in ( dom ( tan | A)) holds (( tan | A) . ( - x)) = ( - (( tan | A) . x))

      proof

        let x;

        assume that

         A6: x in ( dom ( tan | A)) and

         A7: ( - x) in ( dom ( tan | A));

        reconsider x as Element of REAL by XREAL_0:def 1;

        (( tan | A) . ( - x)) = (( tan | A) /. ( - x)) by A7, PARTFUN1:def 6

        .= ( tan /. ( - x)) by A1, A2, A7, PARTFUN2: 17

        .= ( tan . ( - x)) by A1, A7, PARTFUN1:def 6

        .= ( - ( tan . x)) by A3, A6

        .= ( - ( tan /. x)) by A1, A6, PARTFUN1:def 6

        .= ( - (( tan | A) /. x)) by A1, A2, A6, PARTFUN2: 17

        .= ( - (( tan | A) . x)) by A6, PARTFUN1:def 6;

        hence thesis;

      end;

      then ( tan | A) is with_symmetrical_domain quasi_odd by A2;

      hence thesis by A1;

    end;

    theorem :: FUNCT_8:71

    A c= ( dom cot ) implies cot is_odd_on A

    proof

      assume that

       A1: A c= ( dom cot );

      

       A2: ( dom ( cot | A)) = A by A1, RELAT_1: 62;

      

       A3: for x st x in A holds ( cot . ( - x)) = ( - ( cot . x))

      proof

        let x;

        assume

         A4: x in A;

        then

         A5: ( sin . x) <> 0 by A1, FDIFF_8: 2;

        ( - x) in A by A4, Def1;

        

        then ( cot . ( - x)) = ( cot ( - x)) by A1, FDIFF_8: 2, SIN_COS9: 16

        .= ( - ( cot x)) by SIN_COS4: 3

        .= ( - ( cot . x)) by A5, SIN_COS9: 16;

        hence thesis;

      end;

      for x st x in ( dom ( cot | A)) & ( - x) in ( dom ( cot | A)) holds (( cot | A) . ( - x)) = ( - (( cot | A) . x))

      proof

        let x;

        assume that

         A6: x in ( dom ( cot | A)) and

         A7: ( - x) in ( dom ( cot | A));

        reconsider x as Element of REAL by XREAL_0:def 1;

        (( cot | A) . ( - x)) = (( cot | A) /. ( - x)) by A7, PARTFUN1:def 6

        .= ( cot /. ( - x)) by A1, A2, A7, PARTFUN2: 17

        .= ( cot . ( - x)) by A1, A7, PARTFUN1:def 6

        .= ( - ( cot . x)) by A3, A6

        .= ( - ( cot /. x)) by A1, A6, PARTFUN1:def 6

        .= ( - (( cot | A) /. x)) by A1, A2, A6, PARTFUN2: 17

        .= ( - (( cot | A) . x)) by A6, PARTFUN1:def 6;

        hence thesis;

      end;

      then ( cot | A) is with_symmetrical_domain quasi_odd by A2;

      hence thesis by A1;

    end;

    theorem :: FUNCT_8:72

    A c= [.( - 1), 1.] implies arctan is_odd_on A

    proof

      assume

       A1: A c= [.( - 1), 1.];

      then

       A2: A c= ( dom arctan ) by SIN_COS9: 23;

      

       A3: ( dom ( arctan | A)) = A by A1, RELAT_1: 62, SIN_COS9: 23, XBOOLE_1: 1;

      

       A4: for x st x in A holds ( arctan . ( - x)) = ( - ( arctan . x))

      proof

        let x;

        assume x in A;

        then ( - 1) <= x & x <= 1 by A1, XXREAL_1: 1;

        then ( arctan x) = ( - ( arctan ( - x))) by SIN_COS9: 67;

        hence thesis;

      end;

      for x st x in ( dom ( arctan | A)) & ( - x) in ( dom ( arctan | A)) holds (( arctan | A) . ( - x)) = ( - (( arctan | A) . x))

      proof

        let x;

        assume that

         A5: x in ( dom ( arctan | A)) and

         A6: ( - x) in ( dom ( arctan | A));

        reconsider x as Element of REAL by XREAL_0:def 1;

        (( arctan | A) . ( - x)) = (( arctan | A) /. ( - x)) by A6, PARTFUN1:def 6

        .= ( arctan /. ( - x)) by A2, A3, A6, PARTFUN2: 17

        .= ( arctan . ( - x)) by A2, A6, PARTFUN1:def 6

        .= ( - ( arctan . x)) by A4, A5

        .= ( - ( arctan /. x)) by A2, A5, PARTFUN1:def 6

        .= ( - (( arctan | A) /. x)) by A2, A3, A5, PARTFUN2: 17

        .= ( - (( arctan | A) . x)) by A5, PARTFUN1:def 6;

        hence thesis;

      end;

      then ( arctan | A) is with_symmetrical_domain quasi_odd by A3;

      hence thesis by A2;

    end;

    theorem :: FUNCT_8:73

    for A be symmetrical Subset of REAL holds |. sin .| is_even_on A

    proof

      let A be symmetrical Subset of REAL ;

      A is symmetrical Subset of COMPLEX by NUMBERS: 11, XBOOLE_1: 1;

      hence thesis by Th20, Th65;

    end;

    theorem :: FUNCT_8:74

    for A be symmetrical Subset of REAL holds |. cos .| is_even_on A

    proof

      let A be symmetrical Subset of REAL ;

      A is symmetrical Subset of COMPLEX by NUMBERS: 11, XBOOLE_1: 1;

      hence thesis by Th21, Th66;

    end;

    theorem :: FUNCT_8:75

    for A be symmetrical Subset of REAL holds ( sin " ) is_odd_on A

    proof

      let A be symmetrical Subset of REAL ;

      A is symmetrical Subset of COMPLEX by NUMBERS: 11, XBOOLE_1: 1;

      hence thesis by Th18, Th65;

    end;

    theorem :: FUNCT_8:76

    for A be symmetrical Subset of REAL holds ( cos " ) is_even_on A

    proof

      let A be symmetrical Subset of REAL ;

      A is symmetrical Subset of COMPLEX by NUMBERS: 11, XBOOLE_1: 1;

      hence thesis by Th19, Th66;

    end;

    theorem :: FUNCT_8:77

    for A be symmetrical Subset of REAL holds ( - sin ) is_odd_on A

    proof

      let A be symmetrical Subset of REAL ;

      A is symmetrical Subset of COMPLEX by NUMBERS: 11, XBOOLE_1: 1;

      hence thesis by Th16, Th65;

    end;

    theorem :: FUNCT_8:78

    for A be symmetrical Subset of REAL holds ( - cos ) is_even_on A

    proof

      let A be symmetrical Subset of REAL ;

      A is symmetrical Subset of COMPLEX by NUMBERS: 11, XBOOLE_1: 1;

      hence thesis by Th17, Th66;

    end;

    theorem :: FUNCT_8:79

    for A be symmetrical Subset of REAL holds ( sin ^2 ) is_even_on A

    proof

      let A be symmetrical Subset of REAL ;

      A is symmetrical Subset of COMPLEX & sin is_odd_on A by Th65, NUMBERS: 11, XBOOLE_1: 1;

      hence thesis by Th22;

    end;

    theorem :: FUNCT_8:80

    for A be symmetrical Subset of REAL holds ( cos ^2 ) is_even_on A

    proof

      let A be symmetrical Subset of REAL ;

      A is symmetrical Subset of COMPLEX & cos is_even_on A by Th66, NUMBERS: 11, XBOOLE_1: 1;

      hence thesis by Th23;

    end;

    reserve B for symmetrical Subset of REAL ;

    theorem :: FUNCT_8:81

    

     Th81: B c= ( dom sec ) implies sec is_even_on B

    proof

      assume

       A1: B c= ( dom sec );

      then

       A2: ( dom ( sec | B)) = B by RELAT_1: 62;

      

       A3: for x st x in B holds ( sec . ( - x)) = ( sec . x)

      proof

        let x;

        assume

         A4: x in B;

        then ( - x) in B by Def1;

        

        then ( sec . ( - x)) = (( cos . ( - x)) " ) by A1, RFUNCT_1:def 2

        .= (( cos . x) " ) by SIN_COS: 30

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

        hence thesis;

      end;

      for x st x in ( dom ( sec | B)) & ( - x) in ( dom ( sec | B)) holds (( sec | B) . ( - x)) = (( sec | B) . x)

      proof

        let x;

        assume that

         A5: x in ( dom ( sec | B)) and

         A6: ( - x) in ( dom ( sec | B));

        (( sec | B) . ( - x)) = (( sec | B) /. ( - x)) by A6, PARTFUN1:def 6

        .= ( sec /. ( - x)) by A1, A2, A6, PARTFUN2: 17

        .= ( sec . ( - x)) by A1, A6, PARTFUN1:def 6

        .= ( sec . x) by A3, A5

        .= ( sec /. x) by A1, A5, PARTFUN1:def 6

        .= (( sec | B) /. x) by A1, A2, A5, PARTFUN2: 17

        .= (( sec | B) . x) by A5, PARTFUN1:def 6;

        hence thesis;

      end;

      then ( sec | B) is with_symmetrical_domain quasi_even by A2;

      hence thesis by A1;

    end;

    theorem :: FUNCT_8:82

    (for x be Real st x in B holds ( cos . x) <> 0 ) implies sec is_even_on B

    proof

      assume

       A1: for x be Real st x in B holds ( cos . x) <> 0 ;

      B c= ( dom sec )

      proof

        let x be Real;

        assume

         A2: x in B;

        then ( cos . x) <> 0 by A1;

        then not ( cos . x) in { 0 } by TARSKI:def 1;

        then not x in ( cos " { 0 }) by FUNCT_1:def 7;

        then x in (( dom cos ) \ ( cos " { 0 })) by A2, SIN_COS: 24, XBOOLE_0:def 5;

        hence thesis by RFUNCT_1:def 2;

      end;

      hence thesis by Th81;

    end;

    theorem :: FUNCT_8:83

    

     Th83: B c= ( dom cosec ) implies cosec is_odd_on B

    proof

      assume

       A1: B c= ( dom cosec );

      then

       A2: ( dom ( cosec | B)) = B by RELAT_1: 62;

      

       A3: for x st x in B holds ( cosec . ( - x)) = ( - ( cosec . x))

      proof

        let x;

        assume

         A4: x in B;

        then ( - x) in B by Def1;

        

        then ( cosec . ( - x)) = (( sin . ( - x)) " ) by A1, RFUNCT_1:def 2

        .= (( - ( sin . x)) " ) by SIN_COS: 30

        .= ( - (( sin . x) " )) by XCMPLX_1: 222

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

        hence thesis;

      end;

      for x st x in ( dom ( cosec | B)) & ( - x) in ( dom ( cosec | B)) holds (( cosec | B) . ( - x)) = ( - (( cosec | B) . x))

      proof

        let x;

        assume that

         A5: x in ( dom ( cosec | B)) and

         A6: ( - x) in ( dom ( cosec | B));

        (( cosec | B) . ( - x)) = (( cosec | B) /. ( - x)) by A6, PARTFUN1:def 6

        .= ( cosec /. ( - x)) by A1, A2, A6, PARTFUN2: 17

        .= ( cosec . ( - x)) by A1, A6, PARTFUN1:def 6

        .= ( - ( cosec . x)) by A3, A5

        .= ( - ( cosec /. x)) by A1, A5, PARTFUN1:def 6

        .= ( - (( cosec | B) /. x)) by A1, A2, A5, PARTFUN2: 17

        .= ( - (( cosec | B) . x)) by A5, PARTFUN1:def 6;

        hence thesis;

      end;

      then ( cosec | B) is with_symmetrical_domain quasi_odd by A2;

      hence thesis by A1;

    end;

    theorem :: FUNCT_8:84

    (for x be Real st x in B holds ( sin . x) <> 0 ) implies cosec is_odd_on B

    proof

      assume

       A1: for x be Real st x in B holds ( sin . x) <> 0 ;

      B c= ( dom cosec )

      proof

        let x be Real;

        assume

         A2: x in B;

        then ( sin . x) <> 0 by A1;

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

        then not x in ( sin " { 0 }) by FUNCT_1:def 7;

        then x in (( dom sin ) \ ( sin " { 0 })) by A2, SIN_COS: 24, XBOOLE_0:def 5;

        hence thesis by RFUNCT_1:def 2;

      end;

      hence thesis by Th83;

    end;