:: Basic properties of even and odd functions :: by Bo Li and Yanhong Men :: :: Received May 25, 2009 :: Copyright (c) 2009-2019 Association of Mizar Users :: (Stowarzyszenie Uzytkownikow Mizara, Bialystok, Poland). :: This code can be distributed under the GNU General Public Licence :: version 3.0 or later, or the Creative Commons Attribution-ShareAlike :: License version 3.0 or later, subject to the binding interpretation :: detailed in file COPYING.interpretation. :: See COPYING.GPL and COPYING.CC-BY-SA for the full text of these :: licenses, or see http://www.gnu.org/licenses/gpl.html and :: http://creativecommons.org/licenses/by-sa/3.0/. environ vocabularies NUMBERS, REAL_1, XCMPLX_0, ARYTM_1, SUBSET_1, RELAT_1, XBOOLE_0, MEMBERED, PARTFUN1, FUNCT_1, ABIAN, TARSKI, ARYTM_3, CARD_1, COMPLEX1, VALUED_1, SQUARE_1, ABSVALUE, XXREAL_0, EUCLID, SIN_COS, SIN_COS2, XXREAL_1, SIN_COS9, SIN_COS4, FUNCT_8, FUNCT_7; notations COMPLEX1, XCMPLX_0, ORDINAL1, NUMBERS, XREAL_0, XXREAL_0, REAL_1, MEMBERED, ABSVALUE, PARTFUN1, TARSKI, XBOOLE_0, SUBSET_1, EUCLID, RELAT_1, FUNCT_1, FUNCT_2, SIN_COS, SIN_COS2, VALUED_1, RCOMP_1, SIN_COS4, SQUARE_1, SIN_COS9, RELSET_1, FDIFF_9; constructors REAL_1, RCOMP_1, EUCLID, SQUARE_1, ABSVALUE, SIN_COS2, RFUNCT_1, RELSET_1, SIN_COS9, BINOP_2, SIN_COS, FDIFF_9, SIN_COS4, NEWTON; registrations XXREAL_0, XREAL_0, XBOOLE_0, MEMBERED, XCMPLX_0, NUMBERS, VALUED_0, FUNCT_1, RELAT_1, FUNCT_2, RELSET_1, SIN_COS9, ORDINAL1; requirements REAL, NUMERALS, SUBSET, ARITHM, BOOLE; definitions MEMBERED; equalities SIN_COS4, VALUED_1, SIN_COS, SIN_COS9, XCMPLX_0, SQUARE_1, SUBSET_1, FDIFF_9; expansions MEMBERED; theorems SIN_COS4, XREAL_0, ABSVALUE, FUNCT_2, COMPLEX1, XBOOLE_0, EUCLID, XCMPLX_1, SIN_COS9, XXREAL_1, VALUED_1, XBOOLE_1, SIN_COS, SIN_COS2, RFUNCT_1, XCMPLX_0, RELAT_1, PARTFUN2, FUNCT_1, TARSKI, PARTFUN1, NUMBERS, FDIFF_8; schemes FUNCT_2; begin :: Even and odd functions reserve x, r for Real; definition let A be set; attr A is symmetrical means :Def1: for x being 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; 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; 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; 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; 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; 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; 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; 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 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 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 (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 (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 (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 (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 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 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 (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 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 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 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 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 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 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 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 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 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 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 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 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 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 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 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 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 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 F is_even_on A implies F^2 is_even_on A by Th23; theorem F is_odd_on A implies F^2 is_even_on A by Th22; theorem 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 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 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 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 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 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 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 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 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 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 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 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 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 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 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 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 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 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 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 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 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 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 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 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 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 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 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 :: Examples definition func signum -> Function of REAL, REAL means :Def9: for x being Real holds it .x = sgn x; existence proof deffunc U(Real) = In(sgn\$1,REAL); consider f being Function of REAL, REAL such that A1: for x being 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 being Real holds f1.x=sgn x; assume A3: for x being Real holds f2.x=sgn x; for x being 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 Th56: for x being 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 Th57: for x being 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 Th58: signum.0 = 0 proof signum.0 = sgn 0 by Def9 .= 0 by ABSVALUE:def 2; hence thesis; end; theorem Th59: for x being 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 for A being 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 Th61: for x being 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 Th62: for x being 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 Th63: for x being 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 for A being 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 Th65: for A being 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 Th66: for A being 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 being 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 for A being 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 for A being 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 being 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 being 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 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 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 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 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 for A being 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 for A being 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 for A being 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 for A being 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 for A being 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 for A being 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 for A being 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 for A being 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 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 (for x being Real st x in B holds cos.x<>0) implies sec is_even_on B proof assume A1: for x being 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 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 (for x being Real st x in B holds sin.x<>0) implies cosec is_odd_on B proof assume A1: for x being 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;