:: FUNCT_8 semantic presentation begin definition let A be set ; attrA is symmetrical means :Def1: :: FUNCT_8:def 1 for x being complex number st x in A holds - x in A; end; :: deftheorem Def1 defines symmetrical FUNCT_8:def_1_:_ for A being set holds ( A is symmetrical iff for x being complex number st x in A holds - x in A ); registration cluster complex-membered symmetrical for Element of K6(COMPLEX); existence ex b1 being Subset of COMPLEX st b1 is symmetrical proof take [#] COMPLEX ; ::_thesis: [#] COMPLEX is symmetrical let x be complex number ; :: according to FUNCT_8:def_1 ::_thesis: ( x in [#] COMPLEX implies - x in [#] COMPLEX ) thus ( x in [#] COMPLEX implies - x in [#] COMPLEX ) by XCMPLX_0:def_2; ::_thesis: verum end; end; registration cluster complex-membered ext-real-membered real-membered symmetrical for Element of K6(REAL); existence ex b1 being Subset of REAL st b1 is symmetrical proof take [#] REAL ; ::_thesis: [#] REAL is symmetrical let x be complex number ; :: according to FUNCT_8:def_1 ::_thesis: ( x in [#] REAL implies - x in [#] REAL ) for x being Real st x in REAL holds - x in REAL ; hence ( x in [#] REAL implies - x in [#] REAL ) ; ::_thesis: verum end; end; definition let R be Relation; attrR is with_symmetrical_domain means :Def2: :: FUNCT_8:def 2 dom R is symmetrical ; end; :: deftheorem Def2 defines with_symmetrical_domain FUNCT_8:def_2_:_ for R being Relation holds ( R is with_symmetrical_domain iff dom R is symmetrical ); registration cluster empty Relation-like -> with_symmetrical_domain for set ; coherence for b1 being Relation st b1 is empty holds b1 is with_symmetrical_domain proof A1: {} is symmetrical proof assume not {} is symmetrical ; ::_thesis: contradiction then ex x being complex number st ( x in {} & not - x in {} ) by Def1; hence contradiction ; ::_thesis: verum end; dom {} = {} ; hence for b1 being Relation st b1 is empty holds b1 is with_symmetrical_domain by A1, Def2; ::_thesis: verum end; end; registration let R be with_symmetrical_domain Relation; cluster dom R -> symmetrical ; coherence dom R is symmetrical by Def2; end; definition let X, Y be complex-membered set ; let F be PartFunc of X,Y; attrF is quasi_even means :Def3: :: FUNCT_8:def 3 for x being Real st x in dom F & - x in dom F holds F . (- x) = F . x; end; :: deftheorem Def3 defines quasi_even FUNCT_8:def_3_:_ for X, Y being complex-membered set for F being PartFunc of X,Y holds ( F is quasi_even iff for x being Real st x in dom F & - x in dom F holds F . (- x) = F . x ); definition let X, Y be complex-membered set ; let F be PartFunc of X,Y; attrF is even means :Def4: :: FUNCT_8:def 4 ( F is with_symmetrical_domain & F is quasi_even ); end; :: deftheorem Def4 defines even FUNCT_8:def_4_:_ for X, Y being complex-membered set for F being PartFunc of X,Y holds ( F is even iff ( F is with_symmetrical_domain & F is quasi_even ) ); registration let X, Y be complex-membered set ; cluster Function-like with_symmetrical_domain quasi_even -> even for Element of K6(K7(X,Y)); coherence for b1 being PartFunc of X,Y st b1 is with_symmetrical_domain & b1 is quasi_even holds b1 is even by Def4; cluster Function-like even -> with_symmetrical_domain quasi_even for Element of K6(K7(X,Y)); coherence for b1 being PartFunc of X,Y st b1 is even holds ( b1 is with_symmetrical_domain & b1 is quasi_even ) by Def4; end; definition let A be set ; let X, Y be complex-membered set ; let F be PartFunc of X,Y; predF is_even_on A means :Def5: :: FUNCT_8:def 5 ( A c= dom F & F | A is even ); end; :: deftheorem Def5 defines is_even_on FUNCT_8:def_5_:_ for A being set for X, Y being complex-membered set for F being PartFunc of X,Y holds ( F is_even_on A iff ( A c= dom F & F | A is even ) ); definition let X, Y be complex-membered set ; let F be PartFunc of X,Y; attrF is quasi_odd means :Def6: :: FUNCT_8:def 6 for x being Real st x in dom F & - x in dom F holds F . (- x) = - (F . x); end; :: deftheorem Def6 defines quasi_odd FUNCT_8:def_6_:_ for X, Y being complex-membered set for F being PartFunc of X,Y holds ( F is quasi_odd iff for x being Real st x in dom F & - x in dom F holds F . (- x) = - (F . x) ); definition let X, Y be complex-membered set ; let F be PartFunc of X,Y; attrF is odd means :Def7: :: FUNCT_8:def 7 ( F is with_symmetrical_domain & F is quasi_odd ); end; :: deftheorem Def7 defines odd FUNCT_8:def_7_:_ for X, Y being complex-membered set for F being PartFunc of X,Y holds ( F is odd iff ( F is with_symmetrical_domain & F is quasi_odd ) ); registration let X, Y be complex-membered set ; cluster Function-like with_symmetrical_domain quasi_odd -> odd for Element of K6(K7(X,Y)); coherence for b1 being PartFunc of X,Y st b1 is with_symmetrical_domain & b1 is quasi_odd holds b1 is odd by Def7; cluster Function-like odd -> with_symmetrical_domain quasi_odd for Element of K6(K7(X,Y)); coherence for b1 being PartFunc of X,Y st b1 is odd holds ( b1 is with_symmetrical_domain & b1 is quasi_odd ) by Def7; end; definition let A be set ; let X, Y be complex-membered set ; let F be PartFunc of X,Y; predF is_odd_on A means :Def8: :: FUNCT_8:def 8 ( A c= dom F & F | A is odd ); end; :: deftheorem Def8 defines is_odd_on FUNCT_8:def_8_:_ for A being set for X, Y being complex-membered set for F being PartFunc of X,Y holds ( F is_odd_on A iff ( A c= dom F & F | A is odd ) ); theorem :: FUNCT_8:1 for A being symmetrical Subset of COMPLEX for F being PartFunc of REAL,REAL holds ( F is_odd_on A iff ( A c= dom F & ( for x being Real st x in A holds (F . x) + (F . (- x)) = 0 ) ) ) proof let A be symmetrical Subset of COMPLEX; ::_thesis: for F being PartFunc of REAL,REAL holds ( F is_odd_on A iff ( A c= dom F & ( for x being Real st x in A holds (F . x) + (F . (- x)) = 0 ) ) ) let F be PartFunc of REAL,REAL; ::_thesis: ( F is_odd_on A iff ( A c= dom F & ( for x being Real st x in A holds (F . x) + (F . (- x)) = 0 ) ) ) A1: ( A c= dom F & ( for x being Real 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 being Real st x in A holds (F . x) + (F . (- x)) = 0 ; ::_thesis: F is_odd_on A A4: dom (F | A) = A by A2, RELAT_1:62; A5: for x being Real st x in A holds F . (- x) = - (F . x) proof let x be Real; ::_thesis: ( x in A implies F . (- x) = - (F . x) ) assume x in A ; ::_thesis: F . (- x) = - (F . x) then (F . x) + (F . (- x)) = 0 by A3; hence F . (- x) = - (F . x) ; ::_thesis: verum end; for x being Real st x in dom (F | A) & - x in dom (F | A) holds (F | A) . (- x) = - ((F | A) . x) proof let x be Real; ::_thesis: ( x in dom (F | A) & - x in dom (F | A) implies (F | A) . (- x) = - ((F | A) . x) ) assume that A6: x in dom (F | A) and A7: - x in dom (F | A) ; ::_thesis: (F | A) . (- x) = - ((F | A) . x) (F | A) . (- x) = (F | A) /. (- x) by A7, PARTFUN1:def_6 .= F /. (- x) by A2, A4, A7, PARTFUN2:17 .= F . (- x) by A2, A4, A7, PARTFUN1:def_6 .= - (F . x) by A5, A6 .= - (F /. x) by A2, A4, A6, PARTFUN1:def_6 .= - ((F | A) /. x) by A2, A4, A6, PARTFUN2:17 .= - ((F | A) . x) by A6, PARTFUN1:def_6 ; hence (F | A) . (- x) = - ((F | A) . x) ; ::_thesis: verum end; then ( F | A is with_symmetrical_domain & F | A is quasi_odd ) by A4, Def2, Def6; hence F is_odd_on A by A2, Def8; ::_thesis: verum end; ( F is_odd_on A implies ( A c= dom F & ( for x being Real st x in A holds (F . x) + (F . (- x)) = 0 ) ) ) proof assume A8: F is_odd_on A ; ::_thesis: ( A c= dom F & ( for x being Real st x in A holds (F . x) + (F . (- x)) = 0 ) ) then A9: A c= dom F by Def8; A10: F | A is odd by A8, Def8; for x being Real st x in A holds (F . x) + (F . (- x)) = 0 proof let x be Real; ::_thesis: ( x in A implies (F . x) + (F . (- x)) = 0 ) assume A11: x in A ; ::_thesis: (F . x) + (F . (- x)) = 0 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; (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 (F . x) + (F . (- x)) = 0 ; ::_thesis: verum end; hence ( A c= dom F & ( for x being Real st x in A holds (F . x) + (F . (- x)) = 0 ) ) by A8, Def8; ::_thesis: verum end; hence ( F is_odd_on A iff ( A c= dom F & ( for x being Real st x in A holds (F . x) + (F . (- x)) = 0 ) ) ) by A1; ::_thesis: verum end; theorem :: FUNCT_8:2 for A being symmetrical Subset of COMPLEX for F being PartFunc of REAL,REAL holds ( F is_even_on A iff ( A c= dom F & ( for x being Real st x in A holds (F . x) - (F . (- x)) = 0 ) ) ) proof let A be symmetrical Subset of COMPLEX; ::_thesis: for F being PartFunc of REAL,REAL holds ( F is_even_on A iff ( A c= dom F & ( for x being Real st x in A holds (F . x) - (F . (- x)) = 0 ) ) ) let F be PartFunc of REAL,REAL; ::_thesis: ( F is_even_on A iff ( A c= dom F & ( for x being Real st x in A holds (F . x) - (F . (- x)) = 0 ) ) ) A1: ( A c= dom F & ( for x being Real 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 being Real st x in A holds (F . x) - (F . (- x)) = 0 ; ::_thesis: F is_even_on A A4: dom (F | A) = A by A2, RELAT_1:62; A5: for x being Real st x in A holds F . (- x) = F . x proof let x be Real; ::_thesis: ( x in A implies F . (- x) = F . x ) assume x in A ; ::_thesis: F . (- x) = F . x then (F . x) - (F . (- x)) = 0 by A3; hence F . (- x) = F . x ; ::_thesis: verum end; for x being Real st x in dom (F | A) & - x in dom (F | A) holds (F | A) . (- x) = (F | A) . x proof let x be Real; ::_thesis: ( x in dom (F | A) & - x in dom (F | A) implies (F | A) . (- x) = (F | A) . x ) assume that A6: x in dom (F | A) and A7: - x in dom (F | A) ; ::_thesis: (F | A) . (- x) = (F | A) . x (F | A) . (- x) = (F | A) /. (- x) by A7, PARTFUN1:def_6 .= F /. (- x) by A2, A4, A7, PARTFUN2:17 .= F . (- x) by A2, A4, A7, PARTFUN1:def_6 .= F . x by A5, A6 .= F /. x by A2, A4, A6, PARTFUN1:def_6 .= (F | A) /. x by A2, A4, A6, PARTFUN2:17 .= (F | A) . x by A6, PARTFUN1:def_6 ; hence (F | A) . (- x) = (F | A) . x ; ::_thesis: verum end; then ( F | A is with_symmetrical_domain & F | A is quasi_even ) by A4, Def2, Def3; hence F is_even_on A by A2, Def5; ::_thesis: verum end; ( F is_even_on A implies ( A c= dom F & ( for x being Real st x in A holds (F . x) - (F . (- x)) = 0 ) ) ) proof assume A8: F is_even_on A ; ::_thesis: ( A c= dom F & ( for x being Real st x in A holds (F . x) - (F . (- x)) = 0 ) ) then A9: A c= dom F by Def5; A10: F | A is even by A8, Def5; for x being Real st x in A holds (F . x) - (F . (- x)) = 0 proof let x be Real; ::_thesis: ( x in A implies (F . x) - (F . (- x)) = 0 ) assume A11: x in A ; ::_thesis: (F . x) - (F . (- x)) = 0 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; (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 (F . x) - (F . (- x)) = 0 ; ::_thesis: verum end; hence ( A c= dom F & ( for x being Real st x in A holds (F . x) - (F . (- x)) = 0 ) ) by A8, Def5; ::_thesis: verum end; hence ( F is_even_on A iff ( A c= dom F & ( for x being Real st x in A holds (F . x) - (F . (- x)) = 0 ) ) ) by A1; ::_thesis: verum end; theorem :: FUNCT_8:3 for A being symmetrical Subset of COMPLEX for F being PartFunc of REAL,REAL st F is_odd_on A & ( for x being Real st x in A holds F . x <> 0 ) holds ( A c= dom F & ( for x being Real st x in A holds (F . x) / (F . (- x)) = - 1 ) ) proof let A be symmetrical Subset of COMPLEX; ::_thesis: for F being PartFunc of REAL,REAL st F is_odd_on A & ( for x being Real st x in A holds F . x <> 0 ) holds ( A c= dom F & ( for x being Real st x in A holds (F . x) / (F . (- x)) = - 1 ) ) let F be PartFunc of REAL,REAL; ::_thesis: ( F is_odd_on A & ( for x being Real st x in A holds F . x <> 0 ) implies ( A c= dom F & ( for x being Real st x in A holds (F . x) / (F . (- x)) = - 1 ) ) ) assume that A1: F is_odd_on A and A2: for x being Real st x in A holds F . x <> 0 ; ::_thesis: ( A c= dom F & ( for x being Real st x in A holds (F . x) / (F . (- x)) = - 1 ) ) A3: A c= dom F by A1, Def8; A4: F | A is odd by A1, Def8; for x being Real st x in A holds (F . x) / (F . (- x)) = - 1 proof let x be Real; ::_thesis: ( x in A implies (F . x) / (F . (- x)) = - 1 ) assume A5: x in A ; ::_thesis: (F . x) / (F . (- x)) = - 1 then A6: x in dom (F | A) by A3, RELAT_1:62; 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 (F . x) / (F . (- x)) = - 1 ; ::_thesis: verum end; hence ( A c= dom F & ( for x being Real st x in A holds (F . x) / (F . (- x)) = - 1 ) ) by A1, Def8; ::_thesis: verum end; theorem :: FUNCT_8:4 for A being symmetrical Subset of COMPLEX for F being PartFunc of REAL,REAL st A c= dom F & ( for x being Real st x in A holds (F . x) / (F . (- x)) = - 1 ) holds F is_odd_on A proof let A be symmetrical Subset of COMPLEX; ::_thesis: for F being PartFunc of REAL,REAL st A c= dom F & ( for x being Real st x in A holds (F . x) / (F . (- x)) = - 1 ) holds F is_odd_on A let F be PartFunc of REAL,REAL; ::_thesis: ( A c= dom F & ( for x being Real st x in A holds (F . x) / (F . (- x)) = - 1 ) implies F is_odd_on A ) assume that A1: A c= dom F and A2: for x being Real st x in A holds (F . x) / (F . (- x)) = - 1 ; ::_thesis: F is_odd_on A A3: dom (F | A) = A by A1, RELAT_1:62; A4: for x being Real st x in A holds F . (- x) = - (F . x) proof let x be Real; ::_thesis: ( x in A implies F . (- x) = - (F . x) ) assume x in A ; ::_thesis: F . (- x) = - (F . x) then (F . x) / (F . (- x)) = - 1 by A2; hence F . (- x) = - (F . x) by XCMPLX_1:195; ::_thesis: verum end; for x being Real st x in dom (F | A) & - x in dom (F | A) holds (F | A) . (- x) = - ((F | A) . x) proof let x be Real; ::_thesis: ( x in dom (F | A) & - x in dom (F | A) implies (F | A) . (- x) = - ((F | A) . x) ) assume that A5: x in dom (F | A) and A6: - x in dom (F | A) ; ::_thesis: (F | A) . (- x) = - ((F | A) . x) (F | A) . (- x) = (F | A) /. (- x) by A6, PARTFUN1:def_6 .= F /. (- x) by A1, A3, A6, PARTFUN2:17 .= F . (- x) by A1, A3, A6, PARTFUN1:def_6 .= - (F . x) by A4, A5 .= - (F /. x) by A1, A3, A5, PARTFUN1:def_6 .= - ((F | A) /. x) by A1, A3, A5, PARTFUN2:17 .= - ((F | A) . x) by A5, PARTFUN1:def_6 ; hence (F | A) . (- x) = - ((F | A) . x) ; ::_thesis: verum end; then ( F | A is with_symmetrical_domain & F | A is quasi_odd ) by A3, Def2, Def6; hence F is_odd_on A by A1, Def8; ::_thesis: verum end; theorem :: FUNCT_8:5 for A being symmetrical Subset of COMPLEX for F being PartFunc of REAL,REAL st F is_even_on A & ( for x being Real st x in A holds F . x <> 0 ) holds ( A c= dom F & ( for x being Real st x in A holds (F . x) / (F . (- x)) = 1 ) ) proof let A be symmetrical Subset of COMPLEX; ::_thesis: for F being PartFunc of REAL,REAL st F is_even_on A & ( for x being Real st x in A holds F . x <> 0 ) holds ( A c= dom F & ( for x being Real st x in A holds (F . x) / (F . (- x)) = 1 ) ) let F be PartFunc of REAL,REAL; ::_thesis: ( F is_even_on A & ( for x being Real st x in A holds F . x <> 0 ) implies ( A c= dom F & ( for x being Real st x in A holds (F . x) / (F . (- x)) = 1 ) ) ) assume that A1: F is_even_on A and A2: for x being Real st x in A holds F . x <> 0 ; ::_thesis: ( A c= dom F & ( for x being Real st x in A holds (F . x) / (F . (- x)) = 1 ) ) A3: A c= dom F by A1, Def5; A4: F | A is even by A1, Def5; for x being Real st x in A holds (F . x) / (F . (- x)) = 1 proof let x be Real; ::_thesis: ( x in A implies (F . x) / (F . (- x)) = 1 ) assume A5: x in A ; ::_thesis: (F . x) / (F . (- x)) = 1 then A6: x in dom (F | A) by A3, RELAT_1:62; 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 (F . x) / (F . (- x)) = 1 ; ::_thesis: verum end; hence ( A c= dom F & ( for x being Real st x in A holds (F . x) / (F . (- x)) = 1 ) ) by A1, Def5; ::_thesis: verum end; theorem :: FUNCT_8:6 for A being symmetrical Subset of COMPLEX for F being PartFunc of REAL,REAL st A c= dom F & ( for x being Real st x in A holds (F . x) / (F . (- x)) = 1 ) holds F is_even_on A proof let A be symmetrical Subset of COMPLEX; ::_thesis: for F being PartFunc of REAL,REAL st A c= dom F & ( for x being Real st x in A holds (F . x) / (F . (- x)) = 1 ) holds F is_even_on A let F be PartFunc of REAL,REAL; ::_thesis: ( A c= dom F & ( for x being Real st x in A holds (F . x) / (F . (- x)) = 1 ) implies F is_even_on A ) assume that A1: A c= dom F and A2: for x being Real st x in A holds (F . x) / (F . (- x)) = 1 ; ::_thesis: F is_even_on A A3: dom (F | A) = A by A1, RELAT_1:62; A4: for x being Real st x in A holds F . (- x) = F . x proof let x be Real; ::_thesis: ( x in A implies F . (- x) = F . x ) assume x in A ; ::_thesis: F . (- x) = F . x then (F . x) / (F . (- x)) = 1 by A2; hence F . (- x) = F . x by XCMPLX_1:58; ::_thesis: verum end; for x being Real st x in dom (F | A) & - x in dom (F | A) holds (F | A) . (- x) = (F | A) . x proof let x be Real; ::_thesis: ( x in dom (F | A) & - x in dom (F | A) implies (F | A) . (- x) = (F | A) . x ) assume that A5: x in dom (F | A) and A6: - x in dom (F | A) ; ::_thesis: (F | A) . (- x) = (F | A) . x (F | A) . (- x) = (F | A) /. (- x) by A6, PARTFUN1:def_6 .= F /. (- x) by A1, A3, A6, PARTFUN2:17 .= F . (- x) by A1, A3, A6, PARTFUN1:def_6 .= F . x by A4, A5 .= F /. x by A1, A3, A5, PARTFUN1:def_6 .= (F | A) /. x by A1, A3, A5, PARTFUN2:17 .= (F | A) . x by A5, PARTFUN1:def_6 ; hence (F | A) . (- x) = (F | A) . x ; ::_thesis: verum end; then ( F | A is with_symmetrical_domain & F | A is quasi_even ) by A3, Def2, Def3; hence F is_even_on A by A1, Def5; ::_thesis: verum end; theorem :: FUNCT_8:7 for A being symmetrical Subset of COMPLEX for F being PartFunc of REAL,REAL st F is_even_on A & F is_odd_on A holds for x being Real st x in A holds F . x = 0 proof let A be symmetrical Subset of COMPLEX; ::_thesis: for F being PartFunc of REAL,REAL st F is_even_on A & F is_odd_on A holds for x being Real st x in A holds F . x = 0 let F be PartFunc of REAL,REAL; ::_thesis: ( F is_even_on A & F is_odd_on A implies for x being Real st x in A holds F . x = 0 ) assume that A1: F is_even_on A and A2: F is_odd_on A ; ::_thesis: for x being Real st x in A holds F . x = 0 A3: F | A is even by A1, Def5; A4: F | A is odd by A2, Def8; let x be Real; ::_thesis: ( x in A implies F . x = 0 ) assume A5: x in A ; ::_thesis: F . x = 0 A6: A c= dom F by A1, Def5; 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; 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 F . x = 0 ; ::_thesis: verum end; theorem :: FUNCT_8:8 for A being symmetrical Subset of COMPLEX for F being PartFunc of REAL,REAL st F is_even_on A holds for x being Real st x in A holds F . x = F . (abs x) proof let A be symmetrical Subset of COMPLEX; ::_thesis: for F being PartFunc of REAL,REAL st F is_even_on A holds for x being Real st x in A holds F . x = F . (abs x) let F be PartFunc of REAL,REAL; ::_thesis: ( F is_even_on A implies for x being Real st x in A holds F . x = F . (abs x) ) assume A1: F is_even_on A ; ::_thesis: for x being Real st x in A holds F . x = F . (abs x) then A2: A c= dom F by Def5; A3: F | A is even by A1, Def5; let x be Real; ::_thesis: ( x in A implies F . x = F . (abs x) ) assume A4: x in A ; ::_thesis: F . x = F . (abs x) 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; percases ( x < 0 or 0 < x or x = 0 ) ; suppose x < 0 ; ::_thesis: F . x = F . (abs x) then F . (abs 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 F . x = F . (abs x) ; ::_thesis: verum end; suppose 0 < x ; ::_thesis: F . x = F . (abs x) hence F . x = F . (abs x) by ABSVALUE:def_1; ::_thesis: verum end; suppose x = 0 ; ::_thesis: F . x = F . (abs x) hence F . x = F . (abs x) by ABSVALUE:def_1; ::_thesis: verum end; end; end; theorem :: FUNCT_8:9 for A being symmetrical Subset of COMPLEX for F being PartFunc of REAL,REAL st A c= dom F & ( for x being Real st x in A holds F . x = F . (abs x) ) holds F is_even_on A proof let A be symmetrical Subset of COMPLEX; ::_thesis: for F being PartFunc of REAL,REAL st A c= dom F & ( for x being Real st x in A holds F . x = F . (abs x) ) holds F is_even_on A let F be PartFunc of REAL,REAL; ::_thesis: ( A c= dom F & ( for x being Real st x in A holds F . x = F . (abs x) ) implies F is_even_on A ) assume that A1: A c= dom F and A2: for x being Real st x in A holds F . x = F . (abs x) ; ::_thesis: F is_even_on A A3: dom (F | A) = A by A1, RELAT_1:62; A4: for x being Real st x in A holds - x in A by Def1; A5: for x being Real st x in A holds F . (- x) = F . x proof let x be Real; ::_thesis: ( x in A implies F . (- x) = F . x ) assume A6: x in A ; ::_thesis: F . (- x) = F . x percases ( x < 0 or 0 < x or x = 0 ) ; suppose x < 0 ; ::_thesis: F . (- x) = F . x then F . (- x) = F . (abs x) by ABSVALUE:def_1 .= F . x by A2, A6 ; hence F . (- x) = F . x ; ::_thesis: verum end; suppose 0 < x ; ::_thesis: F . (- x) = F . x then abs (- x) = - (- x) by ABSVALUE:def_1 .= x ; hence F . (- x) = F . x by A2, A4, A6; ::_thesis: verum end; suppose x = 0 ; ::_thesis: F . (- x) = F . x hence F . (- x) = F . x ; ::_thesis: verum end; end; end; for x being Real st x in dom (F | A) & - x in dom (F | A) holds (F | A) . (- x) = (F | A) . x proof let x be Real; ::_thesis: ( x in dom (F | A) & - x in dom (F | A) implies (F | A) . (- x) = (F | A) . x ) assume that A7: x in dom (F | A) and A8: - x in dom (F | A) ; ::_thesis: (F | A) . (- x) = (F | A) . x (F | A) . (- x) = (F | A) /. (- x) by A8, PARTFUN1:def_6 .= F /. (- x) by A1, A3, A8, PARTFUN2:17 .= F . (- x) by A1, A3, A8, PARTFUN1:def_6 .= F . x by A5, A7 .= F /. x by A1, A3, A7, PARTFUN1:def_6 .= (F | A) /. x by A1, A3, A7, PARTFUN2:17 .= (F | A) . x by A7, PARTFUN1:def_6 ; hence (F | A) . (- x) = (F | A) . x ; ::_thesis: verum end; then ( F | A is with_symmetrical_domain & F | A is quasi_even ) by A3, Def2, Def3; hence F is_even_on A by A1, Def5; ::_thesis: verum end; theorem :: FUNCT_8:10 for A being symmetrical Subset of COMPLEX for F, G being PartFunc of REAL,REAL st F is_odd_on A & G is_odd_on A holds F + G is_odd_on A proof let A be symmetrical Subset of COMPLEX; ::_thesis: for F, G being PartFunc of REAL,REAL st F is_odd_on A & G is_odd_on A holds F + G is_odd_on A let F, G be PartFunc of REAL,REAL; ::_thesis: ( F is_odd_on A & G is_odd_on A implies F + G is_odd_on A ) assume that A1: F is_odd_on A and A2: G is_odd_on A ; ::_thesis: F + G is_odd_on A A3: A c= dom G by A2, Def8; A4: G | A is odd by A2, Def8; A5: A c= dom F by A1, Def8; 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, Def8; for x being Real 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 be Real; ::_thesis: ( x in dom ((F + G) | A) & - x in dom ((F + G) | A) implies ((F + G) | A) . (- x) = - (((F + G) | A) . x) ) assume that A10: x in dom ((F + G) | A) and A11: - x in dom ((F + G) | A) ; ::_thesis: ((F + G) | A) . (- x) = - (((F + G) | A) . x) 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; ((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, A8, A11, PARTFUN1:def_6 .= (F . (- x)) + (G . (- x)) by A6, A7, A8, A11, VALUED_1:def_1 .= (F /. (- x)) + (G . (- x)) by A5, A8, A11, PARTFUN1:def_6 .= (F /. (- x)) + (G /. (- x)) by A3, A8, 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, A8, A10, PARTFUN1:def_6 .= - ((F . x) + (G . x)) by A3, A8, A10, PARTFUN1:def_6 .= - ((F + G) . x) by A6, A7, A8, A10, VALUED_1:def_1 .= - ((F + G) /. x) by A6, A7, A8, 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 ((F + G) | A) . (- x) = - (((F + G) | A) . x) ; ::_thesis: verum end; then ( (F + G) | A is with_symmetrical_domain & (F + G) | A is quasi_odd ) by A8, Def2, Def6; hence F + G is_odd_on A by A6, A7, Def8; ::_thesis: verum end; theorem :: FUNCT_8:11 for A being symmetrical Subset of COMPLEX for F, G being PartFunc of REAL,REAL st F is_even_on A & G is_even_on A holds F + G is_even_on A proof let A be symmetrical Subset of COMPLEX; ::_thesis: for F, G being PartFunc of REAL,REAL st F is_even_on A & G is_even_on A holds F + G is_even_on A let F, G be PartFunc of REAL,REAL; ::_thesis: ( F is_even_on A & G is_even_on A implies F + G is_even_on A ) assume that A1: F is_even_on A and A2: G is_even_on A ; ::_thesis: F + G is_even_on A A3: A c= dom G by A2, Def5; A4: G | A is even by A2, Def5; A5: A c= dom F by A1, Def5; 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, Def5; for x being Real 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 be Real; ::_thesis: ( x in dom ((F + G) | A) & - x in dom ((F + G) | A) implies ((F + G) | A) . (- x) = ((F + G) | A) . x ) assume that A10: x in dom ((F + G) | A) and A11: - x in dom ((F + G) | A) ; ::_thesis: ((F + G) | A) . (- x) = ((F + G) | A) . x 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; ((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, A8, A11, PARTFUN1:def_6 .= (F . (- x)) + (G . (- x)) by A6, A7, A8, A11, VALUED_1:def_1 .= (F /. (- x)) + (G . (- x)) by A5, A8, A11, PARTFUN1:def_6 .= (F /. (- x)) + (G /. (- x)) by A3, A8, 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, A8, A10, PARTFUN1:def_6 .= (F . x) + (G . x) by A3, A8, A10, PARTFUN1:def_6 .= (F + G) . x by A6, A7, A8, A10, VALUED_1:def_1 .= (F + G) /. x by A6, A7, A8, 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 ((F + G) | A) . (- x) = ((F + G) | A) . x ; ::_thesis: verum end; then ( (F + G) | A is with_symmetrical_domain & (F + G) | A is quasi_even ) by A8, Def2, Def3; hence F + G is_even_on A by A6, A7, Def5; ::_thesis: verum end; theorem :: FUNCT_8:12 for A being symmetrical Subset of COMPLEX for F, G being PartFunc of REAL,REAL st F is_odd_on A & G is_odd_on A holds F - G is_odd_on A proof let A be symmetrical Subset of COMPLEX; ::_thesis: for F, G being PartFunc of REAL,REAL st F is_odd_on A & G is_odd_on A holds F - G is_odd_on A let F, G be PartFunc of REAL,REAL; ::_thesis: ( F is_odd_on A & G is_odd_on A implies F - G is_odd_on A ) assume that A1: F is_odd_on A and A2: G is_odd_on A ; ::_thesis: F - G is_odd_on A A3: A c= dom G by A2, Def8; A4: G | A is odd by A2, Def8; A5: A c= dom F by A1, Def8; 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, Def8; for x being Real 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 be Real; ::_thesis: ( x in dom ((F - G) | A) & - x in dom ((F - G) | A) implies ((F - G) | A) . (- x) = - (((F - G) | A) . x) ) assume that A10: x in dom ((F - G) | A) and A11: - x in dom ((F - G) | A) ; ::_thesis: ((F - G) | A) . (- x) = - (((F - G) | A) . x) 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; ((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, A8, A11, PARTFUN1:def_6 .= (F . (- x)) - (G . (- x)) by A6, A7, A8, A11, VALUED_1:13 .= (F /. (- x)) - (G . (- x)) by A5, A8, A11, PARTFUN1:def_6 .= (F /. (- x)) - (G /. (- x)) by A3, A8, 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, A8, A10, PARTFUN1:def_6 .= - ((F . x) - (G . x)) by A3, A8, A10, PARTFUN1:def_6 .= - ((F - G) . x) by A6, A7, A8, A10, VALUED_1:13 .= - ((F - G) /. x) by A6, A7, A8, 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 ((F - G) | A) . (- x) = - (((F - G) | A) . x) ; ::_thesis: verum end; then ( (F - G) | A is with_symmetrical_domain & (F - G) | A is quasi_odd ) by A8, Def2, Def6; hence F - G is_odd_on A by A6, A7, Def8; ::_thesis: verum end; theorem :: FUNCT_8:13 for A being symmetrical Subset of COMPLEX for F, G being PartFunc of REAL,REAL st F is_even_on A & G is_even_on A holds F - G is_even_on A proof let A be symmetrical Subset of COMPLEX; ::_thesis: for F, G being PartFunc of REAL,REAL st F is_even_on A & G is_even_on A holds F - G is_even_on A let F, G be PartFunc of REAL,REAL; ::_thesis: ( F is_even_on A & G is_even_on A implies F - G is_even_on A ) assume that A1: F is_even_on A and A2: G is_even_on A ; ::_thesis: F - G is_even_on A A3: A c= dom G by A2, Def5; A4: G | A is even by A2, Def5; A5: A c= dom F by A1, Def5; 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, Def5; for x being Real 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 be Real; ::_thesis: ( x in dom ((F - G) | A) & - x in dom ((F - G) | A) implies ((F - G) | A) . (- x) = ((F - G) | A) . x ) assume that A10: x in dom ((F - G) | A) and A11: - x in dom ((F - G) | A) ; ::_thesis: ((F - G) | A) . (- x) = ((F - G) | A) . x 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; ((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, A8, A11, PARTFUN1:def_6 .= (F . (- x)) - (G . (- x)) by A6, A7, A8, A11, VALUED_1:13 .= (F /. (- x)) - (G . (- x)) by A5, A8, A11, PARTFUN1:def_6 .= (F /. (- x)) - (G /. (- x)) by A3, A8, 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, A8, A10, PARTFUN1:def_6 .= (F . x) - (G . x) by A3, A8, A10, PARTFUN1:def_6 .= (F - G) . x by A6, A7, A8, A10, VALUED_1:13 .= (F - G) /. x by A6, A7, A8, 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 ((F - G) | A) . (- x) = ((F - G) | A) . x ; ::_thesis: verum end; then ( (F - G) | A is with_symmetrical_domain & (F - G) | A is quasi_even ) by A8, Def2, Def3; hence F - G is_even_on A by A6, A7, Def5; ::_thesis: verum end; theorem :: FUNCT_8:14 for r being Real for A being symmetrical Subset of COMPLEX for F being PartFunc of REAL,REAL st F is_odd_on A holds r (#) F is_odd_on A proof let r be Real; ::_thesis: for A being symmetrical Subset of COMPLEX for F being PartFunc of REAL,REAL st F is_odd_on A holds r (#) F is_odd_on A let A be symmetrical Subset of COMPLEX; ::_thesis: for F being PartFunc of REAL,REAL st F is_odd_on A holds r (#) F is_odd_on A let F be PartFunc of REAL,REAL; ::_thesis: ( F is_odd_on A implies r (#) F is_odd_on A ) assume A1: F is_odd_on A ; ::_thesis: r (#) F is_odd_on A then A2: A c= dom F by Def8; 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, Def8; for x being Real 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 be Real; ::_thesis: ( x in dom ((r (#) F) | A) & - x in dom ((r (#) F) | A) implies ((r (#) F) | A) . (- x) = - (((r (#) F) | A) . x) ) assume that A6: x in dom ((r (#) F) | A) and A7: - x in dom ((r (#) F) | A) ; ::_thesis: ((r (#) F) | A) . (- x) = - (((r (#) F) | A) . x) 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; ((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, A4, A7, PARTFUN1:def_6 .= r * (F . (- x)) by A3, A4, A7, VALUED_1:def_5 .= r * (F /. (- x)) by A2, A4, 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, A4, A6, PARTFUN1:def_6 .= - ((r (#) F) . x) by A3, A4, A6, VALUED_1:def_5 .= - ((r (#) F) /. x) by A3, A4, A6, PARTFUN1:def_6 .= - (((r (#) F) | A) /. x) by A3, A4, A6, PARTFUN2:17 .= - (((r (#) F) | A) . x) by A6, PARTFUN1:def_6 ; hence ((r (#) F) | A) . (- x) = - (((r (#) F) | A) . x) ; ::_thesis: verum end; then ( (r (#) F) | A is with_symmetrical_domain & (r (#) F) | A is quasi_odd ) by A4, Def2, Def6; hence r (#) F is_odd_on A by A3, Def8; ::_thesis: verum end; theorem :: FUNCT_8:15 for r being Real for A being symmetrical Subset of COMPLEX for F being PartFunc of REAL,REAL st F is_even_on A holds r (#) F is_even_on A proof let r be Real; ::_thesis: for A being symmetrical Subset of COMPLEX for F being PartFunc of REAL,REAL st F is_even_on A holds r (#) F is_even_on A let A be symmetrical Subset of COMPLEX; ::_thesis: for F being PartFunc of REAL,REAL st F is_even_on A holds r (#) F is_even_on A let F be PartFunc of REAL,REAL; ::_thesis: ( F is_even_on A implies r (#) F is_even_on A ) assume A1: F is_even_on A ; ::_thesis: r (#) F is_even_on A then A2: A c= dom F by Def5; 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, Def5; for x being Real 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 be Real; ::_thesis: ( x in dom ((r (#) F) | A) & - x in dom ((r (#) F) | A) implies ((r (#) F) | A) . (- x) = ((r (#) F) | A) . x ) assume that A6: x in dom ((r (#) F) | A) and A7: - x in dom ((r (#) F) | A) ; ::_thesis: ((r (#) F) | A) . (- x) = ((r (#) F) | A) . x 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; ((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, A4, A7, PARTFUN1:def_6 .= r * (F . (- x)) by A3, A4, A7, VALUED_1:def_5 .= r * (F /. (- x)) by A2, A4, 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, A4, A6, PARTFUN1:def_6 .= (r (#) F) . x by A3, A4, A6, VALUED_1:def_5 .= (r (#) F) /. x by A3, A4, A6, PARTFUN1:def_6 .= ((r (#) F) | A) /. x by A3, A4, A6, PARTFUN2:17 .= ((r (#) F) | A) . x by A6, PARTFUN1:def_6 ; hence ((r (#) F) | A) . (- x) = ((r (#) F) | A) . x ; ::_thesis: verum end; then ( (r (#) F) | A is with_symmetrical_domain & (r (#) F) | A is quasi_even ) by A4, Def2, Def3; hence r (#) F is_even_on A by A3, Def5; ::_thesis: verum end; theorem Th16: :: FUNCT_8:16 for A being symmetrical Subset of COMPLEX for F being PartFunc of REAL,REAL st F is_odd_on A holds - F is_odd_on A proof let A be symmetrical Subset of COMPLEX; ::_thesis: for F being PartFunc of REAL,REAL st F is_odd_on A holds - F is_odd_on A let F be PartFunc of REAL,REAL; ::_thesis: ( F is_odd_on A implies - F is_odd_on A ) assume A1: F is_odd_on A ; ::_thesis: - F is_odd_on A then A2: A c= dom F by Def8; 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, Def8; for x being Real st x in dom ((- F) | A) & - x in dom ((- F) | A) holds ((- F) | A) . (- x) = - (((- F) | A) . x) proof let x be Real; ::_thesis: ( x in dom ((- F) | A) & - x in dom ((- F) | A) implies ((- F) | A) . (- x) = - (((- F) | A) . x) ) assume that A6: x in dom ((- F) | A) and A7: - x in dom ((- F) | A) ; ::_thesis: ((- F) | A) . (- x) = - (((- F) | A) . x) 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; ((- F) | A) . (- x) = ((- F) | A) /. (- x) by A7, PARTFUN1:def_6 .= (- F) /. (- x) by A3, A4, A7, PARTFUN2:17 .= (- F) . (- x) by A3, A4, A7, PARTFUN1:def_6 .= - (F . (- x)) by VALUED_1:8 .= - (F /. (- x)) by A2, A4, 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, A4, A6, PARTFUN1:def_6 .= - ((- F) . x) by VALUED_1:8 .= - ((- F) /. x) by A3, A4, A6, PARTFUN1:def_6 .= - (((- F) | A) /. x) by A3, A4, A6, PARTFUN2:17 .= - (((- F) | A) . x) by A6, PARTFUN1:def_6 ; hence ((- F) | A) . (- x) = - (((- F) | A) . x) ; ::_thesis: verum end; then ( (- F) | A is with_symmetrical_domain & (- F) | A is quasi_odd ) by A4, Def2, Def6; hence - F is_odd_on A by A3, Def8; ::_thesis: verum end; theorem Th17: :: FUNCT_8:17 for A being symmetrical Subset of COMPLEX for F being PartFunc of REAL,REAL st F is_even_on A holds - F is_even_on A proof let A be symmetrical Subset of COMPLEX; ::_thesis: for F being PartFunc of REAL,REAL st F is_even_on A holds - F is_even_on A let F be PartFunc of REAL,REAL; ::_thesis: ( F is_even_on A implies - F is_even_on A ) assume A1: F is_even_on A ; ::_thesis: - F is_even_on A then A2: A c= dom F by Def5; 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, Def5; for x being Real st x in dom ((- F) | A) & - x in dom ((- F) | A) holds ((- F) | A) . (- x) = ((- F) | A) . x proof let x be Real; ::_thesis: ( x in dom ((- F) | A) & - x in dom ((- F) | A) implies ((- F) | A) . (- x) = ((- F) | A) . x ) assume that A6: x in dom ((- F) | A) and A7: - x in dom ((- F) | A) ; ::_thesis: ((- F) | A) . (- x) = ((- F) | A) . x 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; ((- F) | A) . (- x) = ((- F) | A) /. (- x) by A7, PARTFUN1:def_6 .= (- F) /. (- x) by A3, A4, A7, PARTFUN2:17 .= (- F) . (- x) by A3, A4, A7, PARTFUN1:def_6 .= - (F . (- x)) by VALUED_1:8 .= - (F /. (- x)) by A2, A4, 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, A4, A6, PARTFUN1:def_6 .= (- F) . x by VALUED_1:8 .= (- F) /. x by A3, A4, A6, PARTFUN1:def_6 .= ((- F) | A) /. x by A3, A4, A6, PARTFUN2:17 .= ((- F) | A) . x by A6, PARTFUN1:def_6 ; hence ((- F) | A) . (- x) = ((- F) | A) . x ; ::_thesis: verum end; then ( (- F) | A is with_symmetrical_domain & (- F) | A is quasi_even ) by A4, Def2, Def3; hence - F is_even_on A by A3, Def5; ::_thesis: verum end; theorem Th18: :: FUNCT_8:18 for A being symmetrical Subset of COMPLEX for F being PartFunc of REAL,REAL st F is_odd_on A holds F " is_odd_on A proof let A be symmetrical Subset of COMPLEX; ::_thesis: for F being PartFunc of REAL,REAL st F is_odd_on A holds F " is_odd_on A let F be PartFunc of REAL,REAL; ::_thesis: ( F is_odd_on A implies F " is_odd_on A ) assume A1: F is_odd_on A ; ::_thesis: F " is_odd_on A then A2: A c= dom F by Def8; 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, Def8; for x being Real st x in dom ((F ") | A) & - x in dom ((F ") | A) holds ((F ") | A) . (- x) = - (((F ") | A) . x) proof let x be Real; ::_thesis: ( x in dom ((F ") | A) & - x in dom ((F ") | A) implies ((F ") | A) . (- x) = - (((F ") | A) . x) ) assume that A6: x in dom ((F ") | A) and A7: - x in dom ((F ") | A) ; ::_thesis: ((F ") | A) . (- x) = - (((F ") | A) . x) 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; ((F ") | A) . (- x) = ((F ") | A) /. (- x) by A7, PARTFUN1:def_6 .= (F ") /. (- x) by A3, A4, A7, PARTFUN2:17 .= (F ") . (- x) by A3, A4, A7, PARTFUN1:def_6 .= (F . (- x)) " by A3, A4, A7, VALUED_1:def_7 .= (F /. (- x)) " by A2, A4, 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, A4, A6, PARTFUN1:def_6 .= - ((F . x) ") by XCMPLX_1:222 .= - ((F ") . x) by A3, A4, A6, VALUED_1:def_7 .= - ((F ") /. x) by A3, A4, A6, PARTFUN1:def_6 .= - (((F ") | A) /. x) by A3, A4, A6, PARTFUN2:17 .= - (((F ") | A) . x) by A6, PARTFUN1:def_6 ; hence ((F ") | A) . (- x) = - (((F ") | A) . x) ; ::_thesis: verum end; then ( (F ") | A is with_symmetrical_domain & (F ") | A is quasi_odd ) by A4, Def2, Def6; hence F " is_odd_on A by A3, Def8; ::_thesis: verum end; theorem Th19: :: FUNCT_8:19 for A being symmetrical Subset of COMPLEX for F being PartFunc of REAL,REAL st F is_even_on A holds F " is_even_on A proof let A be symmetrical Subset of COMPLEX; ::_thesis: for F being PartFunc of REAL,REAL st F is_even_on A holds F " is_even_on A let F be PartFunc of REAL,REAL; ::_thesis: ( F is_even_on A implies F " is_even_on A ) assume A1: F is_even_on A ; ::_thesis: F " is_even_on A then A2: A c= dom F by Def5; 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, Def5; for x being Real st x in dom ((F ") | A) & - x in dom ((F ") | A) holds ((F ") | A) . (- x) = ((F ") | A) . x proof let x be Real; ::_thesis: ( x in dom ((F ") | A) & - x in dom ((F ") | A) implies ((F ") | A) . (- x) = ((F ") | A) . x ) assume that A6: x in dom ((F ") | A) and A7: - x in dom ((F ") | A) ; ::_thesis: ((F ") | A) . (- x) = ((F ") | A) . x 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; ((F ") | A) . (- x) = ((F ") | A) /. (- x) by A7, PARTFUN1:def_6 .= (F ") /. (- x) by A3, A4, A7, PARTFUN2:17 .= (F ") . (- x) by A3, A4, A7, PARTFUN1:def_6 .= (F . (- x)) " by A3, A4, A7, VALUED_1:def_7 .= (F /. (- x)) " by A2, A4, 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, A4, A6, PARTFUN1:def_6 .= (F ") . x by A3, A4, A6, VALUED_1:def_7 .= (F ") /. x by A3, A4, A6, PARTFUN1:def_6 .= ((F ") | A) /. x by A3, A4, A6, PARTFUN2:17 .= ((F ") | A) . x by A6, PARTFUN1:def_6 ; hence ((F ") | A) . (- x) = ((F ") | A) . x ; ::_thesis: verum end; then ( (F ") | A is with_symmetrical_domain & (F ") | A is quasi_even ) by A4, Def2, Def3; hence F " is_even_on A by A3, Def5; ::_thesis: verum end; theorem Th20: :: FUNCT_8:20 for A being symmetrical Subset of COMPLEX for F being PartFunc of REAL,REAL st F is_odd_on A holds |.F.| is_even_on A proof let A be symmetrical Subset of COMPLEX; ::_thesis: for F being PartFunc of REAL,REAL st F is_odd_on A holds |.F.| is_even_on A let F be PartFunc of REAL,REAL; ::_thesis: ( F is_odd_on A implies |.F.| is_even_on A ) assume A1: F is_odd_on A ; ::_thesis: |.F.| is_even_on A then A2: A c= dom F by Def8; 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, Def8; for x being Real st x in dom (|.F.| | A) & - x in dom (|.F.| | A) holds (|.F.| | A) . (- x) = (|.F.| | A) . x proof let x be Real; ::_thesis: ( x in dom (|.F.| | A) & - x in dom (|.F.| | A) implies (|.F.| | A) . (- x) = (|.F.| | A) . x ) assume that A6: x in dom (|.F.| | A) and A7: - x in dom (|.F.| | A) ; ::_thesis: (|.F.| | A) . (- x) = (|.F.| | A) . x 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; (|.F.| | A) . (- x) = (|.F.| | A) /. (- x) by A7, PARTFUN1:def_6 .= |.F.| /. (- x) by A3, A4, A7, PARTFUN2:17 .= |.F.| . (- x) by A3, A4, A7, PARTFUN1:def_6 .= |.(F . (- x)).| by A3, A4, A7, VALUED_1:def_11 .= |.(F /. (- x)).| by A2, A4, 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, A4, A6, PARTFUN1:def_6 .= |.(F . x).| by COMPLEX1:52 .= |.F.| . x by A3, A4, A6, VALUED_1:def_11 .= |.F.| /. x by A3, A4, A6, PARTFUN1:def_6 .= (|.F.| | A) /. x by A3, A4, A6, PARTFUN2:17 .= (|.F.| | A) . x by A6, PARTFUN1:def_6 ; hence (|.F.| | A) . (- x) = (|.F.| | A) . x ; ::_thesis: verum end; then ( |.F.| | A is with_symmetrical_domain & |.F.| | A is quasi_even ) by A4, Def2, Def3; hence |.F.| is_even_on A by A3, Def5; ::_thesis: verum end; theorem Th21: :: FUNCT_8:21 for A being symmetrical Subset of COMPLEX for F being PartFunc of REAL,REAL st F is_even_on A holds |.F.| is_even_on A proof let A be symmetrical Subset of COMPLEX; ::_thesis: for F being PartFunc of REAL,REAL st F is_even_on A holds |.F.| is_even_on A let F be PartFunc of REAL,REAL; ::_thesis: ( F is_even_on A implies |.F.| is_even_on A ) assume A1: F is_even_on A ; ::_thesis: |.F.| is_even_on A then A2: A c= dom F by Def5; 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, Def5; for x being Real st x in dom (|.F.| | A) & - x in dom (|.F.| | A) holds (|.F.| | A) . (- x) = (|.F.| | A) . x proof let x be Real; ::_thesis: ( x in dom (|.F.| | A) & - x in dom (|.F.| | A) implies (|.F.| | A) . (- x) = (|.F.| | A) . x ) assume that A6: x in dom (|.F.| | A) and A7: - x in dom (|.F.| | A) ; ::_thesis: (|.F.| | A) . (- x) = (|.F.| | A) . x 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; (|.F.| | A) . (- x) = (|.F.| | A) /. (- x) by A7, PARTFUN1:def_6 .= |.F.| /. (- x) by A3, A4, A7, PARTFUN2:17 .= |.F.| . (- x) by A3, A4, A7, PARTFUN1:def_6 .= |.(F . (- x)).| by A3, A4, A7, VALUED_1:def_11 .= |.(F /. (- x)).| by A2, A4, 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, A4, A6, PARTFUN1:def_6 .= |.F.| . x by A3, A4, A6, VALUED_1:def_11 .= |.F.| /. x by A3, A4, A6, PARTFUN1:def_6 .= (|.F.| | A) /. x by A3, A4, A6, PARTFUN2:17 .= (|.F.| | A) . x by A6, PARTFUN1:def_6 ; hence (|.F.| | A) . (- x) = (|.F.| | A) . x ; ::_thesis: verum end; then ( |.F.| | A is with_symmetrical_domain & |.F.| | A is quasi_even ) by A4, Def2, Def3; hence |.F.| is_even_on A by A3, Def5; ::_thesis: verum end; theorem Th22: :: FUNCT_8:22 for A being symmetrical Subset of COMPLEX for F, G being PartFunc of REAL,REAL st F is_odd_on A & G is_odd_on A holds F (#) G is_even_on A proof let A be symmetrical Subset of COMPLEX; ::_thesis: for F, G being PartFunc of REAL,REAL st F is_odd_on A & G is_odd_on A holds F (#) G is_even_on A let F, G be PartFunc of REAL,REAL; ::_thesis: ( F is_odd_on A & G is_odd_on A implies F (#) G is_even_on A ) assume that A1: F is_odd_on A and A2: G is_odd_on A ; ::_thesis: F (#) G is_even_on A A3: A c= dom G by A2, Def8; A4: G | A is odd by A2, Def8; A5: A c= dom F by A1, Def8; 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, Def8; for x being Real 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 be Real; ::_thesis: ( x in dom ((F (#) G) | A) & - x in dom ((F (#) G) | A) implies ((F (#) G) | A) . (- x) = ((F (#) G) | A) . x ) assume that A10: x in dom ((F (#) G) | A) and A11: - x in dom ((F (#) G) | A) ; ::_thesis: ((F (#) G) | A) . (- x) = ((F (#) G) | A) . x 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; ((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, A8, A11, PARTFUN1:def_6 .= (F . (- x)) * (G . (- x)) by A6, A7, A8, A11, VALUED_1:def_4 .= (F /. (- x)) * (G . (- x)) by A5, A8, A11, PARTFUN1:def_6 .= (F /. (- x)) * (G /. (- x)) by A3, A8, 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, A8, A10, PARTFUN1:def_6 .= (F . x) * (G . x) by A3, A8, A10, PARTFUN1:def_6 .= (F (#) G) . x by A6, A7, A8, A10, VALUED_1:def_4 .= (F (#) G) /. x by A6, A7, A8, 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 ((F (#) G) | A) . (- x) = ((F (#) G) | A) . x ; ::_thesis: verum end; then ( (F (#) G) | A is with_symmetrical_domain & (F (#) G) | A is quasi_even ) by A8, Def2, Def3; hence F (#) G is_even_on A by A6, A7, Def5; ::_thesis: verum end; theorem Th23: :: FUNCT_8:23 for A being symmetrical Subset of COMPLEX for F, G being PartFunc of REAL,REAL st F is_even_on A & G is_even_on A holds F (#) G is_even_on A proof let A be symmetrical Subset of COMPLEX; ::_thesis: for F, G being PartFunc of REAL,REAL st F is_even_on A & G is_even_on A holds F (#) G is_even_on A let F, G be PartFunc of REAL,REAL; ::_thesis: ( F is_even_on A & G is_even_on A implies F (#) G is_even_on A ) assume that A1: F is_even_on A and A2: G is_even_on A ; ::_thesis: F (#) G is_even_on A A3: A c= dom G by A2, Def5; A4: G | A is even by A2, Def5; A5: A c= dom F by A1, Def5; 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, Def5; for x being Real 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 be Real; ::_thesis: ( x in dom ((F (#) G) | A) & - x in dom ((F (#) G) | A) implies ((F (#) G) | A) . (- x) = ((F (#) G) | A) . x ) assume that A10: x in dom ((F (#) G) | A) and A11: - x in dom ((F (#) G) | A) ; ::_thesis: ((F (#) G) | A) . (- x) = ((F (#) G) | A) . x 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; ((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, A8, A11, PARTFUN1:def_6 .= (F . (- x)) * (G . (- x)) by A6, A7, A8, A11, VALUED_1:def_4 .= (F /. (- x)) * (G . (- x)) by A5, A8, A11, PARTFUN1:def_6 .= (F /. (- x)) * (G /. (- x)) by A3, A8, 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, A8, A10, PARTFUN1:def_6 .= (F . x) * (G . x) by A3, A8, A10, PARTFUN1:def_6 .= (F (#) G) . x by A6, A7, A8, A10, VALUED_1:def_4 .= (F (#) G) /. x by A6, A7, A8, 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 ((F (#) G) | A) . (- x) = ((F (#) G) | A) . x ; ::_thesis: verum end; then ( (F (#) G) | A is with_symmetrical_domain & (F (#) G) | A is quasi_even ) by A8, Def2, Def3; hence F (#) G is_even_on A by A6, A7, Def5; ::_thesis: verum end; theorem :: FUNCT_8:24 for A being symmetrical Subset of COMPLEX for F, G being PartFunc of REAL,REAL st F is_even_on A & G is_odd_on A holds F (#) G is_odd_on A proof let A be symmetrical Subset of COMPLEX; ::_thesis: for F, G being PartFunc of REAL,REAL st F is_even_on A & G is_odd_on A holds F (#) G is_odd_on A let F, G be PartFunc of REAL,REAL; ::_thesis: ( F is_even_on A & G is_odd_on A implies F (#) G is_odd_on A ) assume that A1: F is_even_on A and A2: G is_odd_on A ; ::_thesis: F (#) G is_odd_on A A3: A c= dom G by A2, Def8; A4: G | A is odd by A2, Def8; A5: A c= dom F by A1, Def5; 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, Def5; for x being Real 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 be Real; ::_thesis: ( x in dom ((F (#) G) | A) & - x in dom ((F (#) G) | A) implies ((F (#) G) | A) . (- x) = - (((F (#) G) | A) . x) ) assume that A10: x in dom ((F (#) G) | A) and A11: - x in dom ((F (#) G) | A) ; ::_thesis: ((F (#) G) | A) . (- x) = - (((F (#) G) | A) . x) 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; ((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, A8, A11, PARTFUN1:def_6 .= (F . (- x)) * (G . (- x)) by A6, A7, A8, A11, VALUED_1:def_4 .= (F /. (- x)) * (G . (- x)) by A5, A8, A11, PARTFUN1:def_6 .= (F /. (- x)) * (G /. (- x)) by A3, A8, 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, A8, A10, PARTFUN1:def_6 .= - ((F . x) * (G . x)) by A3, A8, A10, PARTFUN1:def_6 .= - ((F (#) G) . x) by A6, A7, A8, A10, VALUED_1:def_4 .= - ((F (#) G) /. x) by A6, A7, A8, 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 ((F (#) G) | A) . (- x) = - (((F (#) G) | A) . x) ; ::_thesis: verum end; then ( (F (#) G) | A is with_symmetrical_domain & (F (#) G) | A is quasi_odd ) by A8, Def2, Def6; hence F (#) G is_odd_on A by A6, A7, Def8; ::_thesis: verum end; theorem :: FUNCT_8:25 for r being Real for A being symmetrical Subset of COMPLEX for F being PartFunc of REAL,REAL st F is_even_on A holds r + F is_even_on A proof let r be Real; ::_thesis: for A being symmetrical Subset of COMPLEX for F being PartFunc of REAL,REAL st F is_even_on A holds r + F is_even_on A let A be symmetrical Subset of COMPLEX; ::_thesis: for F being PartFunc of REAL,REAL st F is_even_on A holds r + F is_even_on A let F be PartFunc of REAL,REAL; ::_thesis: ( F is_even_on A implies r + F is_even_on A ) assume A1: F is_even_on A ; ::_thesis: r + F is_even_on A then A2: A c= dom F by Def5; 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, Def5; for x being Real 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 be Real; ::_thesis: ( x in dom ((r + F) | A) & - x in dom ((r + F) | A) implies ((r + F) | A) . (- x) = ((r + F) | A) . x ) assume that A6: x in dom ((r + F) | A) and A7: - x in dom ((r + F) | A) ; ::_thesis: ((r + F) | A) . (- x) = ((r + F) | A) . x 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; ((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, A4, A7, PARTFUN1:def_6 .= r + (F . (- x)) by A3, A4, A7, VALUED_1:def_2 .= r + (F /. (- x)) by A2, A4, 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, A4, A6, PARTFUN1:def_6 .= (r + F) . x by A3, A4, A6, VALUED_1:def_2 .= (r + F) /. x by A3, A4, A6, PARTFUN1:def_6 .= ((r + F) | A) /. x by A3, A4, A6, PARTFUN2:17 .= ((r + F) | A) . x by A6, PARTFUN1:def_6 ; hence ((r + F) | A) . (- x) = ((r + F) | A) . x ; ::_thesis: verum end; then ( (r + F) | A is with_symmetrical_domain & (r + F) | A is quasi_even ) by A4, Def2, Def3; hence r + F is_even_on A by A3, Def5; ::_thesis: verum end; theorem :: FUNCT_8:26 for r being Real for A being symmetrical Subset of COMPLEX for F being PartFunc of REAL,REAL st F is_even_on A holds F - r is_even_on A proof let r be Real; ::_thesis: for A being symmetrical Subset of COMPLEX for F being PartFunc of REAL,REAL st F is_even_on A holds F - r is_even_on A let A be symmetrical Subset of COMPLEX; ::_thesis: for F being PartFunc of REAL,REAL st F is_even_on A holds F - r is_even_on A let F be PartFunc of REAL,REAL; ::_thesis: ( F is_even_on A implies F - r is_even_on A ) assume A1: F is_even_on A ; ::_thesis: F - r is_even_on A then A2: A c= dom F by Def5; 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, Def5; for x being Real 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 be Real; ::_thesis: ( x in dom ((F - r) | A) & - x in dom ((F - r) | A) implies ((F - r) | A) . (- x) = ((F - r) | A) . x ) assume that A6: x in dom ((F - r) | A) and A7: - x in dom ((F - r) | A) ; ::_thesis: ((F - r) | A) . (- x) = ((F - r) | A) . x 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; ((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, A4, A7, PARTFUN1:def_6 .= (F . (- x)) - r by A2, A4, A7, VALUED_1:3 .= (F /. (- x)) - r by A2, A4, 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, A4, A6, PARTFUN1:def_6 .= (F - r) . x by A2, A4, A6, VALUED_1:3 .= (F - r) /. x by A3, A4, A6, PARTFUN1:def_6 .= ((F - r) | A) /. x by A3, A4, A6, PARTFUN2:17 .= ((F - r) | A) . x by A6, PARTFUN1:def_6 ; hence ((F - r) | A) . (- x) = ((F - r) | A) . x ; ::_thesis: verum end; then ( (F - r) | A is with_symmetrical_domain & (F - r) | A is quasi_even ) by A4, Def2, Def3; hence F - r is_even_on A by A3, Def5; ::_thesis: verum end; theorem :: FUNCT_8:27 for A being symmetrical Subset of COMPLEX for F being PartFunc of REAL,REAL st F is_even_on A holds F ^2 is_even_on A by Th23; theorem :: FUNCT_8:28 for A being symmetrical Subset of COMPLEX for F being PartFunc of REAL,REAL st F is_odd_on A holds F ^2 is_even_on A by Th22; theorem :: FUNCT_8:29 for A being symmetrical Subset of COMPLEX for F, G being PartFunc of REAL,REAL st F is_odd_on A & G is_odd_on A holds F /" G is_even_on A proof let A be symmetrical Subset of COMPLEX; ::_thesis: for F, G being PartFunc of REAL,REAL st F is_odd_on A & G is_odd_on A holds F /" G is_even_on A let F, G be PartFunc of REAL,REAL; ::_thesis: ( F is_odd_on A & G is_odd_on A implies F /" G is_even_on A ) assume that A1: F is_odd_on A and A2: G is_odd_on A ; ::_thesis: F /" G is_even_on A A3: A c= dom G by A2, Def8; A4: G | A is odd by A2, Def8; A5: A c= dom F by A1, Def8; 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, Def8; for x being Real 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 be Real; ::_thesis: ( x in dom ((F /" G) | A) & - x in dom ((F /" G) | A) implies ((F /" G) | A) . (- x) = ((F /" G) | A) . x ) assume that A10: x in dom ((F /" G) | A) and A11: - x in dom ((F /" G) | A) ; ::_thesis: ((F /" G) | A) . (- x) = ((F /" G) | A) . x 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; ((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, A8, A11, PARTFUN1:def_6 .= (F . (- x)) / (G . (- x)) by VALUED_1:17 .= (F /. (- x)) / (G . (- x)) by A5, A8, A11, PARTFUN1:def_6 .= (F /. (- x)) / (G /. (- x)) by A3, A8, 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, A8, A10, PARTFUN1:def_6 .= (F . x) / (G . x) by A3, A8, A10, PARTFUN1:def_6 .= (F /" G) . x by VALUED_1:17 .= (F /" G) /. x by A6, A7, A8, 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 ((F /" G) | A) . (- x) = ((F /" G) | A) . x ; ::_thesis: verum end; then ( (F /" G) | A is with_symmetrical_domain & (F /" G) | A is quasi_even ) by A8, Def2, Def3; hence F /" G is_even_on A by A6, A7, Def5; ::_thesis: verum end; theorem :: FUNCT_8:30 for A being symmetrical Subset of COMPLEX for F, G being PartFunc of REAL,REAL st F is_even_on A & G is_even_on A holds F /" G is_even_on A proof let A be symmetrical Subset of COMPLEX; ::_thesis: for F, G being PartFunc of REAL,REAL st F is_even_on A & G is_even_on A holds F /" G is_even_on A let F, G be PartFunc of REAL,REAL; ::_thesis: ( F is_even_on A & G is_even_on A implies F /" G is_even_on A ) assume that A1: F is_even_on A and A2: G is_even_on A ; ::_thesis: F /" G is_even_on A A3: A c= dom G by A2, Def5; A4: G | A is even by A2, Def5; A5: A c= dom F by A1, Def5; 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, Def5; for x being Real 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 be Real; ::_thesis: ( x in dom ((F /" G) | A) & - x in dom ((F /" G) | A) implies ((F /" G) | A) . (- x) = ((F /" G) | A) . x ) assume that A10: x in dom ((F /" G) | A) and A11: - x in dom ((F /" G) | A) ; ::_thesis: ((F /" G) | A) . (- x) = ((F /" G) | A) . x 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; ((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, A8, A11, PARTFUN1:def_6 .= (F . (- x)) / (G . (- x)) by VALUED_1:17 .= (F /. (- x)) / (G . (- x)) by A5, A8, A11, PARTFUN1:def_6 .= (F /. (- x)) / (G /. (- x)) by A3, A8, 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, A8, A10, PARTFUN1:def_6 .= (F . x) / (G . x) by A3, A8, A10, PARTFUN1:def_6 .= (F /" G) . x by VALUED_1:17 .= (F /" G) /. x by A6, A7, A8, 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 ((F /" G) | A) . (- x) = ((F /" G) | A) . x ; ::_thesis: verum end; then ( (F /" G) | A is with_symmetrical_domain & (F /" G) | A is quasi_even ) by A8, Def2, Def3; hence F /" G is_even_on A by A6, A7, Def5; ::_thesis: verum end; theorem :: FUNCT_8:31 for A being symmetrical Subset of COMPLEX for F, G being PartFunc of REAL,REAL st F is_odd_on A & G is_even_on A holds F /" G is_odd_on A proof let A be symmetrical Subset of COMPLEX; ::_thesis: for F, G being PartFunc of REAL,REAL st F is_odd_on A & G is_even_on A holds F /" G is_odd_on A let F, G be PartFunc of REAL,REAL; ::_thesis: ( F is_odd_on A & G is_even_on A implies F /" G is_odd_on A ) assume that A1: F is_odd_on A and A2: G is_even_on A ; ::_thesis: F /" G is_odd_on A A3: A c= dom G by A2, Def5; A4: G | A is even by A2, Def5; A5: A c= dom F by A1, Def8; 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, Def8; for x being Real 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 be Real; ::_thesis: ( x in dom ((F /" G) | A) & - x in dom ((F /" G) | A) implies ((F /" G) | A) . (- x) = - (((F /" G) | A) . x) ) assume that A10: x in dom ((F /" G) | A) and A11: - x in dom ((F /" G) | A) ; ::_thesis: ((F /" G) | A) . (- x) = - (((F /" G) | A) . x) 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; ((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, A8, A11, PARTFUN1:def_6 .= (F . (- x)) / (G . (- x)) by VALUED_1:17 .= (F /. (- x)) / (G . (- x)) by A5, A8, A11, PARTFUN1:def_6 .= (F /. (- x)) / (G /. (- x)) by A3, A8, 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, A8, A10, PARTFUN1:def_6 .= - ((F . x) / (G . x)) by A3, A8, A10, PARTFUN1:def_6 .= - ((F /" G) . x) by VALUED_1:17 .= - ((F /" G) /. x) by A6, A7, A8, 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 ((F /" G) | A) . (- x) = - (((F /" G) | A) . x) ; ::_thesis: verum end; then ( (F /" G) | A is with_symmetrical_domain & (F /" G) | A is quasi_odd ) by A8, Def2, Def6; hence F /" G is_odd_on A by A6, A7, Def8; ::_thesis: verum end; theorem :: FUNCT_8:32 for A being symmetrical Subset of COMPLEX for F, G being PartFunc of REAL,REAL st F is_even_on A & G is_odd_on A holds F /" G is_odd_on A proof let A be symmetrical Subset of COMPLEX; ::_thesis: for F, G being PartFunc of REAL,REAL st F is_even_on A & G is_odd_on A holds F /" G is_odd_on A let F, G be PartFunc of REAL,REAL; ::_thesis: ( F is_even_on A & G is_odd_on A implies F /" G is_odd_on A ) assume that A1: F is_even_on A and A2: G is_odd_on A ; ::_thesis: F /" G is_odd_on A A3: A c= dom G by A2, Def8; A4: G | A is odd by A2, Def8; A5: A c= dom F by A1, Def5; 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, Def5; for x being Real 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 be Real; ::_thesis: ( x in dom ((F /" G) | A) & - x in dom ((F /" G) | A) implies ((F /" G) | A) . (- x) = - (((F /" G) | A) . x) ) assume that A10: x in dom ((F /" G) | A) and A11: - x in dom ((F /" G) | A) ; ::_thesis: ((F /" G) | A) . (- x) = - (((F /" G) | A) . x) 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; ((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, A8, A11, PARTFUN1:def_6 .= (F . (- x)) / (G . (- x)) by VALUED_1:17 .= (F /. (- x)) / (G . (- x)) by A5, A8, A11, PARTFUN1:def_6 .= (F /. (- x)) / (G /. (- x)) by A3, A8, 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, A8, A10, PARTFUN1:def_6 .= - ((F . x) / (G . x)) by A3, A8, A10, PARTFUN1:def_6 .= - ((F /" G) . x) by VALUED_1:17 .= - ((F /" G) /. x) by A6, A7, A8, 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 ((F /" G) | A) . (- x) = - (((F /" G) | A) . x) ; ::_thesis: verum end; then ( (F /" G) | A is with_symmetrical_domain & (F /" G) | A is quasi_odd ) by A8, Def2, Def6; hence F /" G is_odd_on A by A6, A7, Def8; ::_thesis: verum end; theorem :: FUNCT_8:33 for F being PartFunc of REAL,REAL st F is odd holds - F is odd proof let F be PartFunc of REAL,REAL; ::_thesis: ( F is odd implies - F is odd ) A1: dom F = dom (- F) by VALUED_1:8; assume A2: F is odd ; ::_thesis: - F is odd for x being Real st x in dom (- F) & - x in dom (- F) holds (- F) . (- x) = - ((- F) . x) proof let x be Real; ::_thesis: ( x in dom (- F) & - x in dom (- F) implies (- F) . (- x) = - ((- F) . x) ) assume A3: ( x in dom (- F) & - x in dom (- F) ) ; ::_thesis: (- F) . (- x) = - ((- F) . x) (- F) . (- x) = - (F . (- x)) by VALUED_1:8 .= - (- (F . x)) by A2, A1, A3, Def6 .= - ((- F) . x) by VALUED_1:8 ; hence (- F) . (- x) = - ((- F) . x) ; ::_thesis: verum end; then ( - F is with_symmetrical_domain & - F is quasi_odd ) by A2, A1, Def2, Def6; hence - F is odd ; ::_thesis: verum end; theorem :: FUNCT_8:34 for F being PartFunc of REAL,REAL st F is even holds - F is even proof let F be PartFunc of REAL,REAL; ::_thesis: ( F is even implies - F is even ) A1: dom F = dom (- F) by VALUED_1:8; assume A2: F is even ; ::_thesis: - F is even for x being Real st x in dom (- F) & - x in dom (- F) holds (- F) . (- x) = (- F) . x proof let x be Real; ::_thesis: ( x in dom (- F) & - x in dom (- F) implies (- F) . (- x) = (- F) . x ) assume A3: ( x in dom (- F) & - x in dom (- F) ) ; ::_thesis: (- F) . (- x) = (- F) . x (- F) . (- x) = - (F . (- x)) by VALUED_1:8 .= - (F . x) by A2, A1, A3, Def3 .= (- F) . x by VALUED_1:8 ; hence (- F) . (- x) = (- F) . x ; ::_thesis: verum end; then ( - F is with_symmetrical_domain & - F is quasi_even ) by A2, A1, Def2, Def3; hence - F is even ; ::_thesis: verum end; theorem :: FUNCT_8:35 for F being PartFunc of REAL,REAL st F is odd holds F " is odd proof let F be PartFunc of REAL,REAL; ::_thesis: ( F is odd implies F " is odd ) A1: dom F = dom (F ") by VALUED_1:def_7; assume A2: F is odd ; ::_thesis: F " is odd for x being Real st x in dom (F ") & - x in dom (F ") holds (F ") . (- x) = - ((F ") . x) proof let x be Real; ::_thesis: ( x in dom (F ") & - x in dom (F ") implies (F ") . (- x) = - ((F ") . x) ) assume that A3: x in dom (F ") and A4: - x in dom (F ") ; ::_thesis: (F ") . (- x) = - ((F ") . x) (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 (F ") . (- x) = - ((F ") . x) ; ::_thesis: verum end; then ( F " is with_symmetrical_domain & F " is quasi_odd ) by A2, A1, Def2, Def6; hence F " is odd ; ::_thesis: verum end; theorem :: FUNCT_8:36 for F being PartFunc of REAL,REAL st F is even holds F " is even proof let F be PartFunc of REAL,REAL; ::_thesis: ( F is even implies F " is even ) A1: dom F = dom (F ") by VALUED_1:def_7; assume A2: F is even ; ::_thesis: F " is even for x being Real st x in dom (F ") & - x in dom (F ") holds (F ") . (- x) = (F ") . x proof let x be Real; ::_thesis: ( x in dom (F ") & - x in dom (F ") implies (F ") . (- x) = (F ") . x ) assume that A3: x in dom (F ") and A4: - x in dom (F ") ; ::_thesis: (F ") . (- x) = (F ") . x (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 (F ") . (- x) = (F ") . x ; ::_thesis: verum end; then ( F " is with_symmetrical_domain & F " is quasi_even ) by A2, A1, Def2, Def3; hence F " is even ; ::_thesis: verum end; theorem :: FUNCT_8:37 for F being PartFunc of REAL,REAL st F is odd holds |.F.| is even proof let F be PartFunc of REAL,REAL; ::_thesis: ( F is odd implies |.F.| is even ) A1: dom F = dom |.F.| by VALUED_1:def_11; assume A2: F is odd ; ::_thesis: |.F.| is even for x being Real st x in dom |.F.| & - x in dom |.F.| holds |.F.| . (- x) = |.F.| . x proof let x be Real; ::_thesis: ( x in dom |.F.| & - x in dom |.F.| implies |.F.| . (- x) = |.F.| . x ) assume that A3: x in dom |.F.| and A4: - x in dom |.F.| ; ::_thesis: |.F.| . (- x) = |.F.| . x |.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 |.F.| . (- x) = |.F.| . x ; ::_thesis: verum end; then ( |.F.| is with_symmetrical_domain & |.F.| is quasi_even ) by A2, A1, Def2, Def3; hence |.F.| is even ; ::_thesis: verum end; theorem :: FUNCT_8:38 for F being PartFunc of REAL,REAL st F is even holds |.F.| is even proof let F be PartFunc of REAL,REAL; ::_thesis: ( F is even implies |.F.| is even ) A1: dom F = dom |.F.| by VALUED_1:def_11; assume A2: F is even ; ::_thesis: |.F.| is even for x being Real st x in dom |.F.| & - x in dom |.F.| holds |.F.| . (- x) = |.F.| . x proof let x be Real; ::_thesis: ( x in dom |.F.| & - x in dom |.F.| implies |.F.| . (- x) = |.F.| . x ) assume that A3: x in dom |.F.| and A4: - x in dom |.F.| ; ::_thesis: |.F.| . (- x) = |.F.| . x |.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 |.F.| . (- x) = |.F.| . x ; ::_thesis: verum end; then ( |.F.| is with_symmetrical_domain & |.F.| is quasi_even ) by A2, A1, Def2, Def3; hence |.F.| is even ; ::_thesis: verum end; theorem :: FUNCT_8:39 for F being PartFunc of REAL,REAL st F is odd holds F ^2 is even proof let F be PartFunc of REAL,REAL; ::_thesis: ( F is odd implies F ^2 is even ) A1: dom F = dom (F ^2) by VALUED_1:11; assume A2: F is odd ; ::_thesis: F ^2 is even for x being Real st x in dom (F ^2) & - x in dom (F ^2) holds (F ^2) . (- x) = (F ^2) . x proof let x be Real; ::_thesis: ( x in dom (F ^2) & - x in dom (F ^2) implies (F ^2) . (- x) = (F ^2) . x ) assume A3: ( x in dom (F ^2) & - x in dom (F ^2) ) ; ::_thesis: (F ^2) . (- x) = (F ^2) . x (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 (F ^2) . (- x) = (F ^2) . x ; ::_thesis: verum end; then ( F ^2 is with_symmetrical_domain & F ^2 is quasi_even ) by A2, A1, Def2, Def3; hence F ^2 is even ; ::_thesis: verum end; theorem :: FUNCT_8:40 for F being PartFunc of REAL,REAL st F is even holds F ^2 is even proof let F be PartFunc of REAL,REAL; ::_thesis: ( F is even implies F ^2 is even ) A1: dom F = dom (F ^2) by VALUED_1:11; assume A2: F is even ; ::_thesis: F ^2 is even for x being Real st x in dom (F ^2) & - x in dom (F ^2) holds (F ^2) . (- x) = (F ^2) . x proof let x be Real; ::_thesis: ( x in dom (F ^2) & - x in dom (F ^2) implies (F ^2) . (- x) = (F ^2) . x ) assume A3: ( x in dom (F ^2) & - x in dom (F ^2) ) ; ::_thesis: (F ^2) . (- x) = (F ^2) . x (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 (F ^2) . (- x) = (F ^2) . x ; ::_thesis: verum end; then ( F ^2 is with_symmetrical_domain & F ^2 is quasi_even ) by A2, A1, Def2, Def3; hence F ^2 is even ; ::_thesis: verum end; theorem :: FUNCT_8:41 for r being Real for F being PartFunc of REAL,REAL st F is even holds r + F is even proof let r be Real; ::_thesis: for F being PartFunc of REAL,REAL st F is even holds r + F is even let F be PartFunc of REAL,REAL; ::_thesis: ( F is even implies r + F is even ) A1: dom F = dom (r + F) by VALUED_1:def_2; assume A2: F is even ; ::_thesis: r + F is even for x being Real st x in dom (r + F) & - x in dom (r + F) holds (r + F) . (- x) = (r + F) . x proof let x be Real; ::_thesis: ( x in dom (r + F) & - x in dom (r + F) implies (r + F) . (- x) = (r + F) . x ) assume that A3: x in dom (r + F) and A4: - x in dom (r + F) ; ::_thesis: (r + F) . (- x) = (r + F) . x (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 (r + F) . (- x) = (r + F) . x ; ::_thesis: verum end; then ( r + F is with_symmetrical_domain & r + F is quasi_even ) by A2, A1, Def2, Def3; hence r + F is even ; ::_thesis: verum end; theorem :: FUNCT_8:42 for r being Real for F being PartFunc of REAL,REAL st F is even holds F - r is even proof let r be Real; ::_thesis: for F being PartFunc of REAL,REAL st F is even holds F - r is even let F be PartFunc of REAL,REAL; ::_thesis: ( F is even implies F - r is even ) A1: dom F = dom (F - r) by VALUED_1:3; assume A2: F is even ; ::_thesis: F - r is even for x being Real st x in dom (F - r) & - x in dom (F - r) holds (F - r) . (- x) = (F - r) . x proof let x be Real; ::_thesis: ( x in dom (F - r) & - x in dom (F - r) implies (F - r) . (- x) = (F - r) . x ) assume that A3: x in dom (F - r) and A4: - x in dom (F - r) ; ::_thesis: (F - r) . (- x) = (F - r) . x 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 (F - r) . (- x) = (F - r) . x ; ::_thesis: verum end; then ( F - r is with_symmetrical_domain & F - r is quasi_even ) by A2, A1, Def2, Def3; hence F - r is even ; ::_thesis: verum end; theorem :: FUNCT_8:43 for r being Real for F being PartFunc of REAL,REAL st F is odd holds r (#) F is odd proof let r be Real; ::_thesis: for F being PartFunc of REAL,REAL st F is odd holds r (#) F is odd let F be PartFunc of REAL,REAL; ::_thesis: ( F is odd implies r (#) F is odd ) A1: dom F = dom (r (#) F) by VALUED_1:def_5; assume A2: F is odd ; ::_thesis: r (#) F is odd for x being Real st x in dom (r (#) F) & - x in dom (r (#) F) holds (r (#) F) . (- x) = - ((r (#) F) . x) proof let x be Real; ::_thesis: ( x in dom (r (#) F) & - x in dom (r (#) F) implies (r (#) F) . (- x) = - ((r (#) F) . x) ) assume that A3: x in dom (r (#) F) and A4: - x in dom (r (#) F) ; ::_thesis: (r (#) F) . (- x) = - ((r (#) F) . x) (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 (r (#) F) . (- x) = - ((r (#) F) . x) ; ::_thesis: verum end; then ( r (#) F is with_symmetrical_domain & r (#) F is quasi_odd ) by A2, A1, Def2, Def6; hence r (#) F is odd ; ::_thesis: verum end; theorem :: FUNCT_8:44 for r being Real for F being PartFunc of REAL,REAL st F is even holds r (#) F is even proof let r be Real; ::_thesis: for F being PartFunc of REAL,REAL st F is even holds r (#) F is even let F be PartFunc of REAL,REAL; ::_thesis: ( F is even implies r (#) F is even ) A1: dom F = dom (r (#) F) by VALUED_1:def_5; assume A2: F is even ; ::_thesis: r (#) F is even for x being Real st x in dom (r (#) F) & - x in dom (r (#) F) holds (r (#) F) . (- x) = (r (#) F) . x proof let x be Real; ::_thesis: ( x in dom (r (#) F) & - x in dom (r (#) F) implies (r (#) F) . (- x) = (r (#) F) . x ) assume that A3: x in dom (r (#) F) and A4: - x in dom (r (#) F) ; ::_thesis: (r (#) F) . (- x) = (r (#) F) . x (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 (r (#) F) . (- x) = (r (#) F) . x ; ::_thesis: verum end; then ( r (#) F is with_symmetrical_domain & r (#) F is quasi_even ) by A2, A1, Def2, Def3; hence r (#) F is even ; ::_thesis: verum end; theorem :: FUNCT_8:45 for F, G being PartFunc of REAL,REAL st F is odd & G is odd & (dom F) /\ (dom G) is symmetrical holds F + G is odd proof let F, G be PartFunc of REAL,REAL; ::_thesis: ( F is odd & G is odd & (dom F) /\ (dom G) is symmetrical implies F + G is odd ) assume that A1: F is odd and A2: G is odd and A3: (dom F) /\ (dom G) is symmetrical ; ::_thesis: F + G is odd 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 being Real st x in dom (F + G) & - x in dom (F + G) holds (F + G) . (- x) = - ((F + G) . x) proof let x be Real; ::_thesis: ( x in dom (F + G) & - x in dom (F + G) implies (F + G) . (- x) = - ((F + G) . x) ) assume that A7: x in dom (F + G) and A8: - x in dom (F + G) ; ::_thesis: (F + G) . (- x) = - ((F + G) . x) (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 (F + G) . (- x) = - ((F + G) . x) ; ::_thesis: verum end; then ( F + G is with_symmetrical_domain & F + G is quasi_odd ) by A3, A4, Def2, Def6; hence F + G is odd ; ::_thesis: verum end; theorem :: FUNCT_8:46 for F, G being PartFunc of REAL,REAL st F is even & G is even & (dom F) /\ (dom G) is symmetrical holds F + G is even proof let F, G be PartFunc of REAL,REAL; ::_thesis: ( F is even & G is even & (dom F) /\ (dom G) is symmetrical implies F + G is even ) assume that A1: F is even and A2: G is even and A3: (dom F) /\ (dom G) is symmetrical ; ::_thesis: F + G is even 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 being Real st x in dom (F + G) & - x in dom (F + G) holds (F + G) . (- x) = (F + G) . x proof let x be Real; ::_thesis: ( x in dom (F + G) & - x in dom (F + G) implies (F + G) . (- x) = (F + G) . x ) assume that A7: x in dom (F + G) and A8: - x in dom (F + G) ; ::_thesis: (F + G) . (- x) = (F + G) . x (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 (F + G) . (- x) = (F + G) . x ; ::_thesis: verum end; then ( F + G is with_symmetrical_domain & F + G is quasi_even ) by A3, A4, Def2, Def3; hence F + G is even ; ::_thesis: verum end; theorem :: FUNCT_8:47 for F, G being PartFunc of REAL,REAL st F is odd & G is odd & (dom F) /\ (dom G) is symmetrical holds F - G is odd proof let F, G be PartFunc of REAL,REAL; ::_thesis: ( F is odd & G is odd & (dom F) /\ (dom G) is symmetrical implies F - G is odd ) assume that A1: F is odd and A2: G is odd and A3: (dom F) /\ (dom G) is symmetrical ; ::_thesis: F - G is odd 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 being Real st x in dom (F - G) & - x in dom (F - G) holds (F - G) . (- x) = - ((F - G) . x) proof let x be Real; ::_thesis: ( x in dom (F - G) & - x in dom (F - G) implies (F - G) . (- x) = - ((F - G) . x) ) assume that A7: x in dom (F - G) and A8: - x in dom (F - G) ; ::_thesis: (F - G) . (- x) = - ((F - G) . x) (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 (F - G) . (- x) = - ((F - G) . x) ; ::_thesis: verum end; then ( F - G is with_symmetrical_domain & F - G is quasi_odd ) by A3, A4, Def2, Def6; hence F - G is odd ; ::_thesis: verum end; theorem :: FUNCT_8:48 for F, G being PartFunc of REAL,REAL st F is even & G is even & (dom F) /\ (dom G) is symmetrical holds F - G is even proof let F, G be PartFunc of REAL,REAL; ::_thesis: ( F is even & G is even & (dom F) /\ (dom G) is symmetrical implies F - G is even ) assume that A1: F is even and A2: G is even and A3: (dom F) /\ (dom G) is symmetrical ; ::_thesis: F - G is even 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 being Real st x in dom (F - G) & - x in dom (F - G) holds (F - G) . (- x) = (F - G) . x proof let x be Real; ::_thesis: ( x in dom (F - G) & - x in dom (F - G) implies (F - G) . (- x) = (F - G) . x ) assume that A7: x in dom (F - G) and A8: - x in dom (F - G) ; ::_thesis: (F - G) . (- x) = (F - G) . x (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 (F - G) . (- x) = (F - G) . x ; ::_thesis: verum end; then ( F - G is with_symmetrical_domain & F - G is quasi_even ) by A3, A4, Def2, Def3; hence F - G is even ; ::_thesis: verum end; theorem :: FUNCT_8:49 for F, G being PartFunc of REAL,REAL st F is odd & G is odd & (dom F) /\ (dom G) is symmetrical holds F (#) G is even proof let F, G be PartFunc of REAL,REAL; ::_thesis: ( F is odd & G is odd & (dom F) /\ (dom G) is symmetrical implies F (#) G is even ) assume that A1: F is odd and A2: G is odd and A3: (dom F) /\ (dom G) is symmetrical ; ::_thesis: F (#) G is even 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 being Real st x in dom (F (#) G) & - x in dom (F (#) G) holds (F (#) G) . (- x) = (F (#) G) . x proof let x be Real; ::_thesis: ( x in dom (F (#) G) & - x in dom (F (#) G) implies (F (#) G) . (- x) = (F (#) G) . x ) assume that A7: x in dom (F (#) G) and A8: - x in dom (F (#) G) ; ::_thesis: (F (#) G) . (- x) = (F (#) G) . x (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 (F (#) G) . (- x) = (F (#) G) . x ; ::_thesis: verum end; then ( F (#) G is with_symmetrical_domain & F (#) G is quasi_even ) by A3, A4, Def2, Def3; hence F (#) G is even ; ::_thesis: verum end; theorem :: FUNCT_8:50 for F, G being PartFunc of REAL,REAL st F is even & G is even & (dom F) /\ (dom G) is symmetrical holds F (#) G is even proof let F, G be PartFunc of REAL,REAL; ::_thesis: ( F is even & G is even & (dom F) /\ (dom G) is symmetrical implies F (#) G is even ) assume that A1: F is even and A2: G is even and A3: (dom F) /\ (dom G) is symmetrical ; ::_thesis: F (#) G is even 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 being Real st x in dom (F (#) G) & - x in dom (F (#) G) holds (F (#) G) . (- x) = (F (#) G) . x proof let x be Real; ::_thesis: ( x in dom (F (#) G) & - x in dom (F (#) G) implies (F (#) G) . (- x) = (F (#) G) . x ) assume that A7: x in dom (F (#) G) and A8: - x in dom (F (#) G) ; ::_thesis: (F (#) G) . (- x) = (F (#) G) . x (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 (F (#) G) . (- x) = (F (#) G) . x ; ::_thesis: verum end; then ( F (#) G is with_symmetrical_domain & F (#) G is quasi_even ) by A3, A4, Def2, Def3; hence F (#) G is even ; ::_thesis: verum end; theorem :: FUNCT_8:51 for F, G being PartFunc of REAL,REAL st F is even & G is odd & (dom F) /\ (dom G) is symmetrical holds F (#) G is odd proof let F, G be PartFunc of REAL,REAL; ::_thesis: ( F is even & G is odd & (dom F) /\ (dom G) is symmetrical implies F (#) G is odd ) assume that A1: F is even and A2: G is odd and A3: (dom F) /\ (dom G) is symmetrical ; ::_thesis: F (#) G is odd 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 being Real st x in dom (F (#) G) & - x in dom (F (#) G) holds (F (#) G) . (- x) = - ((F (#) G) . x) proof let x be Real; ::_thesis: ( x in dom (F (#) G) & - x in dom (F (#) G) implies (F (#) G) . (- x) = - ((F (#) G) . x) ) assume that A7: x in dom (F (#) G) and A8: - x in dom (F (#) G) ; ::_thesis: (F (#) G) . (- x) = - ((F (#) G) . x) (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 (F (#) G) . (- x) = - ((F (#) G) . x) ; ::_thesis: verum end; then ( F (#) G is with_symmetrical_domain & F (#) G is quasi_odd ) by A3, A4, Def2, Def6; hence F (#) G is odd ; ::_thesis: verum end; theorem :: FUNCT_8:52 for F, G being PartFunc of REAL,REAL st F is odd & G is odd & (dom F) /\ (dom G) is symmetrical holds F /" G is even proof let F, G be PartFunc of REAL,REAL; ::_thesis: ( F is odd & G is odd & (dom F) /\ (dom G) is symmetrical implies F /" G is even ) assume that A1: F is odd and A2: G is odd and A3: (dom F) /\ (dom G) is symmetrical ; ::_thesis: F /" G is even 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 being Real st x in dom (F /" G) & - x in dom (F /" G) holds (F /" G) . (- x) = (F /" G) . x proof let x be Real; ::_thesis: ( x in dom (F /" G) & - x in dom (F /" G) implies (F /" G) . (- x) = (F /" G) . x ) assume A7: ( x in dom (F /" G) & - x in dom (F /" G) ) ; ::_thesis: (F /" G) . (- x) = (F /" G) . x (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 (F /" G) . (- x) = (F /" G) . x ; ::_thesis: verum end; then ( F /" G is with_symmetrical_domain & F /" G is quasi_even ) by A3, A4, Def2, Def3; hence F /" G is even ; ::_thesis: verum end; theorem :: FUNCT_8:53 for F, G being PartFunc of REAL,REAL st F is even & G is even & (dom F) /\ (dom G) is symmetrical holds F /" G is even proof let F, G be PartFunc of REAL,REAL; ::_thesis: ( F is even & G is even & (dom F) /\ (dom G) is symmetrical implies F /" G is even ) assume that A1: F is even and A2: G is even and A3: (dom F) /\ (dom G) is symmetrical ; ::_thesis: F /" G is even 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 being Real st x in dom (F /" G) & - x in dom (F /" G) holds (F /" G) . (- x) = (F /" G) . x proof let x be Real; ::_thesis: ( x in dom (F /" G) & - x in dom (F /" G) implies (F /" G) . (- x) = (F /" G) . x ) assume A7: ( x in dom (F /" G) & - x in dom (F /" G) ) ; ::_thesis: (F /" G) . (- x) = (F /" G) . x (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 (F /" G) . (- x) = (F /" G) . x ; ::_thesis: verum end; then ( F /" G is with_symmetrical_domain & F /" G is quasi_even ) by A3, A4, Def2, Def3; hence F /" G is even ; ::_thesis: verum end; theorem :: FUNCT_8:54 for F, G being PartFunc of REAL,REAL st F is odd & G is even & (dom F) /\ (dom G) is symmetrical holds F /" G is odd proof let F, G be PartFunc of REAL,REAL; ::_thesis: ( F is odd & G is even & (dom F) /\ (dom G) is symmetrical implies F /" G is odd ) assume that A1: F is odd and A2: G is even and A3: (dom F) /\ (dom G) is symmetrical ; ::_thesis: F /" G is odd 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 being Real st x in dom (F /" G) & - x in dom (F /" G) holds (F /" G) . (- x) = - ((F /" G) . x) proof let x be Real; ::_thesis: ( x in dom (F /" G) & - x in dom (F /" G) implies (F /" G) . (- x) = - ((F /" G) . x) ) assume A7: ( x in dom (F /" G) & - x in dom (F /" G) ) ; ::_thesis: (F /" G) . (- x) = - ((F /" G) . x) (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 (F /" G) . (- x) = - ((F /" G) . x) ; ::_thesis: verum end; then ( F /" G is with_symmetrical_domain & F /" G is quasi_odd ) by A3, A4, Def2, Def6; hence F /" G is odd ; ::_thesis: verum end; theorem :: FUNCT_8:55 for F, G being PartFunc of REAL,REAL st F is even & G is odd & (dom F) /\ (dom G) is symmetrical holds F /" G is odd proof let F, G be PartFunc of REAL,REAL; ::_thesis: ( F is even & G is odd & (dom F) /\ (dom G) is symmetrical implies F /" G is odd ) assume that A1: F is even and A2: G is odd and A3: (dom F) /\ (dom G) is symmetrical ; ::_thesis: F /" G is odd 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 being Real st x in dom (F /" G) & - x in dom (F /" G) holds (F /" G) . (- x) = - ((F /" G) . x) proof let x be Real; ::_thesis: ( x in dom (F /" G) & - x in dom (F /" G) implies (F /" G) . (- x) = - ((F /" G) . x) ) assume A7: ( x in dom (F /" G) & - x in dom (F /" G) ) ; ::_thesis: (F /" G) . (- x) = - ((F /" G) . x) (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 (F /" G) . (- x) = - ((F /" G) . x) ; ::_thesis: verum end; then ( F /" G is with_symmetrical_domain & F /" G is quasi_odd ) by A3, A4, Def2, Def6; hence F /" G is odd ; ::_thesis: verum end; begin definition func signum -> Function of REAL,REAL means :Def9: :: FUNCT_8:def 9 for x being Real holds it . x = sgn x; existence ex b1 being Function of REAL,REAL st for x being Real holds b1 . x = sgn x proof deffunc H1( Element of REAL ) -> Element of REAL = sgn \$1; consider f being Function of REAL,REAL such that A1: for x being Real holds f . x = H1(x) from FUNCT_2:sch_4(); take f ; ::_thesis: for x being Real holds f . x = sgn x thus for x being Real holds f . x = sgn x by A1; ::_thesis: verum end; uniqueness for b1, b2 being Function of REAL,REAL st ( for x being Real holds b1 . x = sgn x ) & ( for x being Real holds b2 . x = sgn x ) holds b1 = b2 proof let f1, f2 be Function of REAL,REAL; ::_thesis: ( ( for x being Real holds f1 . x = sgn x ) & ( for x being Real holds f2 . x = sgn x ) implies f1 = f2 ) assume A2: for x being Real holds f1 . x = sgn x ; ::_thesis: ( ex x being Real st not f2 . x = sgn x or f1 = f2 ) assume A3: for x being Real holds f2 . x = sgn x ; ::_thesis: f1 = f2 for x being Real holds f1 . x = f2 . x proof let x be Real; ::_thesis: f1 . x = f2 . x thus f1 . x = sgn x by A2 .= f2 . x by A3 ; ::_thesis: verum end; hence f1 = f2 by FUNCT_2:63; ::_thesis: verum end; end; :: deftheorem Def9 defines signum FUNCT_8:def_9_:_ for b1 being Function of REAL,REAL holds ( b1 = signum iff for x being Real holds b1 . x = sgn x ); theorem Th56: :: FUNCT_8:56 for x being real number st x > 0 holds signum . x = 1 proof let x be real number ; ::_thesis: ( x > 0 implies signum . x = 1 ) assume A1: 0 < x ; ::_thesis: signum . x = 1 x in REAL by XREAL_0:def_1; then signum . x = sgn x by Def9 .= 1 by A1, ABSVALUE:def_2 ; hence signum . x = 1 ; ::_thesis: verum end; theorem Th57: :: FUNCT_8:57 for x being real number st x < 0 holds signum . x = - 1 proof let x be real number ; ::_thesis: ( x < 0 implies signum . x = - 1 ) assume A1: 0 > x ; ::_thesis: signum . x = - 1 x in REAL by XREAL_0:def_1; then signum . x = sgn x by Def9 .= - 1 by A1, ABSVALUE:def_2 ; hence signum . x = - 1 ; ::_thesis: verum end; theorem Th58: :: FUNCT_8:58 signum . 0 = 0 proof signum . 0 = sgn 0 by Def9 .= 0 by ABSVALUE:def_2 ; hence signum . 0 = 0 ; ::_thesis: verum end; theorem Th59: :: FUNCT_8:59 for x being real number holds signum . (- x) = - (signum . x) proof let x be real number ; ::_thesis: signum . (- x) = - (signum . x) percases ( x < 0 or 0 < x or x = 0 ) ; supposeA1: x < 0 ; ::_thesis: signum . (- x) = - (signum . x) then signum . x = - 1 by Th57; hence signum . (- x) = - (signum . x) by A1, Th56; ::_thesis: verum end; supposeA2: 0 < x ; ::_thesis: signum . (- x) = - (signum . x) then signum . x = 1 by Th56; hence signum . (- x) = - (signum . x) by A2, Th57; ::_thesis: verum end; suppose x = 0 ; ::_thesis: signum . (- x) = - (signum . x) hence signum . (- x) = - (signum . x) by Th58; ::_thesis: verum end; end; end; theorem :: FUNCT_8:60 for A being symmetrical Subset of REAL holds signum is_odd_on A proof let A be symmetrical Subset of REAL; ::_thesis: signum is_odd_on A A1: dom signum = REAL by FUNCT_2:def_1; then A2: dom (signum | A) = A by RELAT_1:62; for x being Real st x in dom (signum | A) & - x in dom (signum | A) holds (signum | A) . (- x) = - ((signum | A) . x) proof let x be Real; ::_thesis: ( x in dom (signum | A) & - x in dom (signum | A) implies (signum | A) . (- x) = - ((signum | A) . x) ) assume that A3: x in dom (signum | A) and A4: - x in dom (signum | A) ; ::_thesis: (signum | A) . (- x) = - ((signum | A) . x) (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 (signum | A) . (- x) = - ((signum | A) . x) ; ::_thesis: verum end; then ( signum | A is with_symmetrical_domain & signum | A is quasi_odd ) by A2, Def2, Def6; hence signum is_odd_on A by A1, Def8; ::_thesis: verum end; theorem Th61: :: FUNCT_8:61 for x being real number st x >= 0 holds absreal . x = x proof let x be real number ; ::_thesis: ( x >= 0 implies absreal . x = x ) assume A1: 0 <= x ; ::_thesis: absreal . x = x absreal . x = abs x by EUCLID:def_2 .= x by A1, ABSVALUE:def_1 ; hence absreal . x = x ; ::_thesis: verum end; theorem Th62: :: FUNCT_8:62 for x being real number st x < 0 holds absreal . x = - x proof let x be real number ; ::_thesis: ( x < 0 implies absreal . x = - x ) assume A1: 0 > x ; ::_thesis: absreal . x = - x absreal . x = abs x by EUCLID:def_2 .= - x by A1, ABSVALUE:def_1 ; hence absreal . x = - x ; ::_thesis: verum end; theorem Th63: :: FUNCT_8:63 for x being real number holds absreal . (- x) = absreal . x proof let x be real number ; ::_thesis: absreal . (- x) = absreal . x percases ( x < 0 or 0 < x or x = 0 ) ; supposeA1: x < 0 ; ::_thesis: absreal . (- x) = absreal . x then absreal . (- x) = - x by Th61; hence absreal . (- x) = absreal . x by A1, Th62; ::_thesis: verum end; supposeA2: 0 < x ; ::_thesis: absreal . (- x) = absreal . x then absreal . (- x) = - (- x) by Th62 .= x ; hence absreal . (- x) = absreal . x by A2, Th61; ::_thesis: verum end; suppose x = 0 ; ::_thesis: absreal . (- x) = absreal . x hence absreal . (- x) = absreal . x ; ::_thesis: verum end; end; end; theorem :: FUNCT_8:64 for A being symmetrical Subset of REAL holds absreal is_even_on A proof let A be symmetrical Subset of REAL; ::_thesis: absreal is_even_on A A1: dom absreal = REAL by FUNCT_2:def_1; then A2: dom (absreal | A) = A by RELAT_1:62; for x being Real st x in dom (absreal | A) & - x in dom (absreal | A) holds (absreal | A) . (- x) = (absreal | A) . x proof let x be Real; ::_thesis: ( x in dom (absreal | A) & - x in dom (absreal | A) implies (absreal | A) . (- x) = (absreal | A) . x ) assume that A3: x in dom (absreal | A) and A4: - x in dom (absreal | A) ; ::_thesis: (absreal | A) . (- x) = (absreal | A) . x (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 (absreal | A) . (- x) = (absreal | A) . x ; ::_thesis: verum end; then ( absreal | A is with_symmetrical_domain & absreal | A is quasi_even ) by A2, Def2, Def3; hence absreal is_even_on A by A1, Def5; ::_thesis: verum end; theorem Th65: :: FUNCT_8:65 for A being symmetrical Subset of REAL holds sin is_odd_on A proof let A be symmetrical Subset of REAL; ::_thesis: sin is_odd_on A A1: dom (sin | A) = A by RELAT_1:62, SIN_COS:24; for x being Real st x in dom (sin | A) & - x in dom (sin | A) holds (sin | A) . (- x) = - ((sin | A) . x) proof let x be Real; ::_thesis: ( x in dom (sin | A) & - x in dom (sin | A) implies (sin | A) . (- x) = - ((sin | A) . x) ) assume that A2: x in dom (sin | A) and A3: - x in dom (sin | A) ; ::_thesis: (sin | A) . (- x) = - ((sin | A) . x) (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 (sin | A) . (- x) = - ((sin | A) . x) ; ::_thesis: verum end; then ( sin | A is with_symmetrical_domain & sin | A is quasi_odd ) by A1, Def2, Def6; hence sin is_odd_on A by Def8, SIN_COS:24; ::_thesis: verum end; theorem Th66: :: FUNCT_8:66 for A being symmetrical Subset of REAL holds cos is_even_on A proof let A be symmetrical Subset of REAL; ::_thesis: cos is_even_on A A1: dom (cos | A) = A by RELAT_1:62, SIN_COS:24; for x being Real st x in dom (cos | A) & - x in dom (cos | A) holds (cos | A) . (- x) = (cos | A) . x proof let x be Real; ::_thesis: ( x in dom (cos | A) & - x in dom (cos | A) implies (cos | A) . (- x) = (cos | A) . x ) assume that A2: x in dom (cos | A) and A3: - x in dom (cos | A) ; ::_thesis: (cos | A) . (- x) = (cos | A) . x (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 (cos | A) . (- x) = (cos | A) . x ; ::_thesis: verum end; then ( cos | A is with_symmetrical_domain & cos | A is quasi_even ) by A1, Def2, Def3; hence cos is_even_on A by Def5, SIN_COS:24; ::_thesis: verum end; registration cluster sin -> odd ; coherence sin is odd proof for x being complex number st x in REAL holds - x in REAL by XREAL_0:def_1; then ( ( for x being Real st x in dom sin & - x in dom sin holds sin . (- x) = - (sin . x) ) & REAL is symmetrical ) by Def1, SIN_COS:30; then ( sin is with_symmetrical_domain & sin is quasi_odd ) by Def2, Def6, SIN_COS:24; hence sin is odd ; ::_thesis: verum end; end; registration cluster cos -> even ; coherence cos is even proof for x being Real st x in dom cos & - x in dom cos holds cos . (- x) = cos . x by SIN_COS:30; then ( cos is with_symmetrical_domain & cos is quasi_even ) by Def2, Def3, SIN_COS:24; hence cos is even ; ::_thesis: verum end; end; theorem :: FUNCT_8:67 for A being symmetrical Subset of REAL holds sinh is_odd_on A proof let A be symmetrical Subset of REAL; ::_thesis: sinh is_odd_on A A1: dom sinh = REAL by FUNCT_2:def_1; then A2: dom (sinh | A) = A by RELAT_1:62; for x being Real st x in dom (sinh | A) & - x in dom (sinh | A) holds (sinh | A) . (- x) = - ((sinh | A) . x) proof let x be Real; ::_thesis: ( x in dom (sinh | A) & - x in dom (sinh | A) implies (sinh | A) . (- x) = - ((sinh | A) . x) ) assume that A3: x in dom (sinh | A) and A4: - x in dom (sinh | A) ; ::_thesis: (sinh | A) . (- x) = - ((sinh | A) . x) (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 (sinh | A) . (- x) = - ((sinh | A) . x) ; ::_thesis: verum end; then ( sinh | A is with_symmetrical_domain & sinh | A is quasi_odd ) by A2, Def2, Def6; hence sinh is_odd_on A by A1, Def8; ::_thesis: verum end; theorem :: FUNCT_8:68 for A being symmetrical Subset of REAL holds cosh is_even_on A proof let A be symmetrical Subset of REAL; ::_thesis: cosh is_even_on A A1: dom cosh = REAL by FUNCT_2:def_1; then A2: dom (cosh | A) = A by RELAT_1:62; for x being Real st x in dom (cosh | A) & - x in dom (cosh | A) holds (cosh | A) . (- x) = (cosh | A) . x proof let x be Real; ::_thesis: ( x in dom (cosh | A) & - x in dom (cosh | A) implies (cosh | A) . (- x) = (cosh | A) . x ) assume that A3: x in dom (cosh | A) and A4: - x in dom (cosh | A) ; ::_thesis: (cosh | A) . (- x) = (cosh | A) . x (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 (cosh | A) . (- x) = (cosh | A) . x ; ::_thesis: verum end; then ( cosh | A is with_symmetrical_domain & cosh | A is quasi_even ) by A2, Def2, Def3; hence cosh is_even_on A by A1, Def5; ::_thesis: verum end; registration cluster sinh -> odd ; coherence sinh is odd proof for x being complex number st x in REAL holds - x in REAL by XREAL_0:def_1; then A1: REAL is symmetrical by Def1; ( ( for x being Real 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 & sinh is quasi_odd ) by A1, Def2, Def6; hence sinh is odd ; ::_thesis: verum end; end; registration cluster cosh -> even ; coherence cosh is even proof for x being complex number st x in REAL holds - x in REAL by XREAL_0:def_1; then A1: REAL is symmetrical by Def1; ( ( for x being Real 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 & cosh is quasi_even ) by A1, Def2, Def3; hence cosh is even ; ::_thesis: verum end; end; theorem :: FUNCT_8:69 for A being symmetrical Subset of COMPLEX st A c= ].(- (PI / 2)),(PI / 2).[ holds tan is_odd_on A proof let A be symmetrical Subset of COMPLEX; ::_thesis: ( A c= ].(- (PI / 2)),(PI / 2).[ implies tan is_odd_on A ) assume A1: A c= ].(- (PI / 2)),(PI / 2).[ ; ::_thesis: tan is_odd_on A then A2: A c= dom tan by SIN_COS9:1, XBOOLE_1:1; A3: dom (tan | A) = A by A1, RELAT_1:62, SIN_COS9:1, XBOOLE_1:1; A4: for x being Real st x in A holds tan . (- x) = - (tan . x) proof let x be Real; ::_thesis: ( x in A implies tan . (- x) = - (tan . x) ) assume A5: x in A ; ::_thesis: tan . (- x) = - (tan . x) 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 tan . (- x) = - (tan . x) ; ::_thesis: verum end; for x being Real st x in dom (tan | A) & - x in dom (tan | A) holds (tan | A) . (- x) = - ((tan | A) . x) proof let x be Real; ::_thesis: ( x in dom (tan | A) & - x in dom (tan | A) implies (tan | A) . (- x) = - ((tan | A) . x) ) assume that A6: x in dom (tan | A) and A7: - x in dom (tan | A) ; ::_thesis: (tan | A) . (- x) = - ((tan | A) . x) (tan | A) . (- x) = (tan | A) /. (- x) by A7, PARTFUN1:def_6 .= tan /. (- x) by A2, A3, A7, PARTFUN2:17 .= tan . (- x) by A2, A3, A7, PARTFUN1:def_6 .= - (tan . x) by A4, A6 .= - (tan /. x) by A2, A3, A6, PARTFUN1:def_6 .= - ((tan | A) /. x) by A2, A3, A6, PARTFUN2:17 .= - ((tan | A) . x) by A6, PARTFUN1:def_6 ; hence (tan | A) . (- x) = - ((tan | A) . x) ; ::_thesis: verum end; then ( tan | A is with_symmetrical_domain & tan | A is quasi_odd ) by A3, Def2, Def6; hence tan is_odd_on A by A2, Def8; ::_thesis: verum end; theorem :: FUNCT_8:70 for A being symmetrical Subset of COMPLEX st A c= dom tan holds tan is_odd_on A proof let A be symmetrical Subset of COMPLEX; ::_thesis: ( A c= dom tan implies tan is_odd_on A ) assume A1: A c= dom tan ; ::_thesis: tan is_odd_on A A2: dom (tan | A) = A by A1, RELAT_1:62; A3: for x being Real st x in A holds tan . (- x) = - (tan . x) proof let x be Real; ::_thesis: ( x in A implies tan . (- x) = - (tan . x) ) assume A4: x in A ; ::_thesis: tan . (- x) = - (tan . x) 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 tan . (- x) = - (tan . x) ; ::_thesis: verum end; for x being Real st x in dom (tan | A) & - x in dom (tan | A) holds (tan | A) . (- x) = - ((tan | A) . x) proof let x be Real; ::_thesis: ( x in dom (tan | A) & - x in dom (tan | A) implies (tan | A) . (- x) = - ((tan | A) . x) ) assume that A6: x in dom (tan | A) and A7: - x in dom (tan | A) ; ::_thesis: (tan | A) . (- x) = - ((tan | A) . x) (tan | A) . (- x) = (tan | A) /. (- x) by A7, PARTFUN1:def_6 .= tan /. (- x) by A1, A2, A7, PARTFUN2:17 .= tan . (- x) by A1, A2, A7, PARTFUN1:def_6 .= - (tan . x) by A3, A6 .= - (tan /. x) by A1, A2, A6, PARTFUN1:def_6 .= - ((tan | A) /. x) by A1, A2, A6, PARTFUN2:17 .= - ((tan | A) . x) by A6, PARTFUN1:def_6 ; hence (tan | A) . (- x) = - ((tan | A) . x) ; ::_thesis: verum end; then ( tan | A is with_symmetrical_domain & tan | A is quasi_odd ) by A2, Def2, Def6; hence tan is_odd_on A by A1, Def8; ::_thesis: verum end; theorem :: FUNCT_8:71 for A being symmetrical Subset of COMPLEX st A c= dom cot holds cot is_odd_on A proof let A be symmetrical Subset of COMPLEX; ::_thesis: ( A c= dom cot implies cot is_odd_on A ) assume A1: A c= dom cot ; ::_thesis: cot is_odd_on A A2: dom (cot | A) = A by A1, RELAT_1:62; A3: for x being Real st x in A holds cot . (- x) = - (cot . x) proof let x be Real; ::_thesis: ( x in A implies cot . (- x) = - (cot . x) ) assume A4: x in A ; ::_thesis: cot . (- x) = - (cot . x) 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 cot . (- x) = - (cot . x) ; ::_thesis: verum end; for x being Real st x in dom (cot | A) & - x in dom (cot | A) holds (cot | A) . (- x) = - ((cot | A) . x) proof let x be Real; ::_thesis: ( x in dom (cot | A) & - x in dom (cot | A) implies (cot | A) . (- x) = - ((cot | A) . x) ) assume that A6: x in dom (cot | A) and A7: - x in dom (cot | A) ; ::_thesis: (cot | A) . (- x) = - ((cot | A) . x) (cot | A) . (- x) = (cot | A) /. (- x) by A7, PARTFUN1:def_6 .= cot /. (- x) by A1, A2, A7, PARTFUN2:17 .= cot . (- x) by A1, A2, A7, PARTFUN1:def_6 .= - (cot . x) by A3, A6 .= - (cot /. x) by A1, A2, A6, PARTFUN1:def_6 .= - ((cot | A) /. x) by A1, A2, A6, PARTFUN2:17 .= - ((cot | A) . x) by A6, PARTFUN1:def_6 ; hence (cot | A) . (- x) = - ((cot | A) . x) ; ::_thesis: verum end; then ( cot | A is with_symmetrical_domain & cot | A is quasi_odd ) by A2, Def2, Def6; hence cot is_odd_on A by A1, Def8; ::_thesis: verum end; theorem :: FUNCT_8:72 for A being symmetrical Subset of COMPLEX st A c= [.(- 1),1.] holds arctan is_odd_on A proof let A be symmetrical Subset of COMPLEX; ::_thesis: ( A c= [.(- 1),1.] implies arctan is_odd_on A ) assume A1: A c= [.(- 1),1.] ; ::_thesis: arctan is_odd_on A then A2: A c= dom arctan by SIN_COS9:23, XBOOLE_1:1; A3: dom (arctan | A) = A by A1, RELAT_1:62, SIN_COS9:23, XBOOLE_1:1; A4: for x being Real st x in A holds arctan . (- x) = - (arctan . x) proof let x be Real; ::_thesis: ( x in A implies arctan . (- x) = - (arctan . x) ) assume x in A ; ::_thesis: arctan . (- x) = - (arctan . x) then ( - 1 <= x & x <= 1 ) by A1, XXREAL_1:1; then arctan x = - (arctan (- x)) by SIN_COS9:67; hence arctan . (- x) = - (arctan . x) ; ::_thesis: verum end; for x being Real st x in dom (arctan | A) & - x in dom (arctan | A) holds (arctan | A) . (- x) = - ((arctan | A) . x) proof let x be Real; ::_thesis: ( x in dom (arctan | A) & - x in dom (arctan | A) implies (arctan | A) . (- x) = - ((arctan | A) . x) ) assume that A5: x in dom (arctan | A) and A6: - x in dom (arctan | A) ; ::_thesis: (arctan | A) . (- x) = - ((arctan | A) . x) (arctan | A) . (- x) = (arctan | A) /. (- x) by A6, PARTFUN1:def_6 .= arctan /. (- x) by A2, A3, A6, PARTFUN2:17 .= arctan . (- x) by A2, A3, A6, PARTFUN1:def_6 .= - (arctan . x) by A4, A5 .= - (arctan /. x) by A2, A3, A5, PARTFUN1:def_6 .= - ((arctan | A) /. x) by A2, A3, A5, PARTFUN2:17 .= - ((arctan | A) . x) by A5, PARTFUN1:def_6 ; hence (arctan | A) . (- x) = - ((arctan | A) . x) ; ::_thesis: verum end; then ( arctan | A is with_symmetrical_domain & arctan | A is quasi_odd ) by A3, Def2, Def6; hence arctan is_odd_on A by A2, Def8; ::_thesis: verum end; theorem :: FUNCT_8:73 for A being symmetrical Subset of REAL holds |.sin.| is_even_on A proof let A be symmetrical Subset of REAL; ::_thesis: |.sin.| is_even_on A A is symmetrical Subset of COMPLEX by NUMBERS:11, XBOOLE_1:1; hence |.sin.| is_even_on A by Th20, Th65; ::_thesis: verum end; theorem :: FUNCT_8:74 for A being symmetrical Subset of REAL holds |.cos.| is_even_on A proof let A be symmetrical Subset of REAL; ::_thesis: |.cos.| is_even_on A A is symmetrical Subset of COMPLEX by NUMBERS:11, XBOOLE_1:1; hence |.cos.| is_even_on A by Th21, Th66; ::_thesis: verum end; theorem :: FUNCT_8:75 for A being symmetrical Subset of REAL holds sin " is_odd_on A proof let A be symmetrical Subset of REAL; ::_thesis: sin " is_odd_on A A is symmetrical Subset of COMPLEX by NUMBERS:11, XBOOLE_1:1; hence sin " is_odd_on A by Th18, Th65; ::_thesis: verum end; theorem :: FUNCT_8:76 for A being symmetrical Subset of REAL holds cos " is_even_on A proof let A be symmetrical Subset of REAL; ::_thesis: cos " is_even_on A A is symmetrical Subset of COMPLEX by NUMBERS:11, XBOOLE_1:1; hence cos " is_even_on A by Th19, Th66; ::_thesis: verum end; theorem :: FUNCT_8:77 for A being symmetrical Subset of REAL holds - sin is_odd_on A proof let A be symmetrical Subset of REAL; ::_thesis: - sin is_odd_on A A is symmetrical Subset of COMPLEX by NUMBERS:11, XBOOLE_1:1; hence - sin is_odd_on A by Th16, Th65; ::_thesis: verum end; theorem :: FUNCT_8:78 for A being symmetrical Subset of REAL holds - cos is_even_on A proof let A be symmetrical Subset of REAL; ::_thesis: - cos is_even_on A A is symmetrical Subset of COMPLEX by NUMBERS:11, XBOOLE_1:1; hence - cos is_even_on A by Th17, Th66; ::_thesis: verum end; theorem :: FUNCT_8:79 for A being symmetrical Subset of REAL holds sin ^2 is_even_on A proof let A be symmetrical Subset of REAL; ::_thesis: sin ^2 is_even_on A ( A is symmetrical Subset of COMPLEX & sin is_odd_on A ) by Th65, NUMBERS:11, XBOOLE_1:1; hence sin ^2 is_even_on A by Th22; ::_thesis: verum end; theorem :: FUNCT_8:80 for A being symmetrical Subset of REAL holds cos ^2 is_even_on A proof let A be symmetrical Subset of REAL; ::_thesis: cos ^2 is_even_on A ( A is symmetrical Subset of COMPLEX & cos is_even_on A ) by Th66, NUMBERS:11, XBOOLE_1:1; hence cos ^2 is_even_on A by Th23; ::_thesis: verum end; theorem Th81: :: FUNCT_8:81 for B being symmetrical Subset of REAL st B c= dom sec holds sec is_even_on B proof let B be symmetrical Subset of REAL; ::_thesis: ( B c= dom sec implies sec is_even_on B ) assume A1: B c= dom sec ; ::_thesis: sec is_even_on B then A2: dom (sec | B) = B by RELAT_1:62; A3: for x being Real st x in B holds sec . (- x) = sec . x proof let x be Real; ::_thesis: ( x in B implies sec . (- x) = sec . x ) assume A4: x in B ; ::_thesis: sec . (- x) = sec . x 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 sec . (- x) = sec . x ; ::_thesis: verum end; for x being Real st x in dom (sec | B) & - x in dom (sec | B) holds (sec | B) . (- x) = (sec | B) . x proof let x be Real; ::_thesis: ( x in dom (sec | B) & - x in dom (sec | B) implies (sec | B) . (- x) = (sec | B) . x ) assume that A5: x in dom (sec | B) and A6: - x in dom (sec | B) ; ::_thesis: (sec | B) . (- x) = (sec | B) . x (sec | B) . (- x) = (sec | B) /. (- x) by A6, PARTFUN1:def_6 .= sec /. (- x) by A1, A2, A6, PARTFUN2:17 .= sec . (- x) by A1, A2, A6, PARTFUN1:def_6 .= sec . x by A3, A5 .= sec /. x by A1, A2, A5, PARTFUN1:def_6 .= (sec | B) /. x by A1, A2, A5, PARTFUN2:17 .= (sec | B) . x by A5, PARTFUN1:def_6 ; hence (sec | B) . (- x) = (sec | B) . x ; ::_thesis: verum end; then ( sec | B is with_symmetrical_domain & sec | B is quasi_even ) by A2, Def2, Def3; hence sec is_even_on B by A1, Def5; ::_thesis: verum end; theorem :: FUNCT_8:82 for B being symmetrical Subset of REAL st ( for x being real number st x in B holds cos . x <> 0 ) holds sec is_even_on B proof let B be symmetrical Subset of REAL; ::_thesis: ( ( for x being real number st x in B holds cos . x <> 0 ) implies sec is_even_on B ) assume A1: for x being real number st x in B holds cos . x <> 0 ; ::_thesis: sec is_even_on B B c= dom sec proof let x be real number ; :: according to MEMBERED:def_9 ::_thesis: ( not x in B or x in dom sec ) assume A2: x in B ; ::_thesis: x in dom sec 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 x in dom sec by RFUNCT_1:def_2; ::_thesis: verum end; hence sec is_even_on B by Th81; ::_thesis: verum end; theorem Th83: :: FUNCT_8:83 for B being symmetrical Subset of REAL st B c= dom cosec holds cosec is_odd_on B proof let B be symmetrical Subset of REAL; ::_thesis: ( B c= dom cosec implies cosec is_odd_on B ) assume A1: B c= dom cosec ; ::_thesis: cosec is_odd_on B then A2: dom (cosec | B) = B by RELAT_1:62; A3: for x being Real st x in B holds cosec . (- x) = - (cosec . x) proof let x be Real; ::_thesis: ( x in B implies cosec . (- x) = - (cosec . x) ) assume A4: x in B ; ::_thesis: cosec . (- x) = - (cosec . x) 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 cosec . (- x) = - (cosec . x) ; ::_thesis: verum end; for x being Real st x in dom (cosec | B) & - x in dom (cosec | B) holds (cosec | B) . (- x) = - ((cosec | B) . x) proof let x be Real; ::_thesis: ( x in dom (cosec | B) & - x in dom (cosec | B) implies (cosec | B) . (- x) = - ((cosec | B) . x) ) assume that A5: x in dom (cosec | B) and A6: - x in dom (cosec | B) ; ::_thesis: (cosec | B) . (- x) = - ((cosec | B) . x) (cosec | B) . (- x) = (cosec | B) /. (- x) by A6, PARTFUN1:def_6 .= cosec /. (- x) by A1, A2, A6, PARTFUN2:17 .= cosec . (- x) by A1, A2, A6, PARTFUN1:def_6 .= - (cosec . x) by A3, A5 .= - (cosec /. x) by A1, A2, A5, PARTFUN1:def_6 .= - ((cosec | B) /. x) by A1, A2, A5, PARTFUN2:17 .= - ((cosec | B) . x) by A5, PARTFUN1:def_6 ; hence (cosec | B) . (- x) = - ((cosec | B) . x) ; ::_thesis: verum end; then ( cosec | B is with_symmetrical_domain & cosec | B is quasi_odd ) by A2, Def2, Def6; hence cosec is_odd_on B by A1, Def8; ::_thesis: verum end; theorem :: FUNCT_8:84 for B being symmetrical Subset of REAL st ( for x being real number st x in B holds sin . x <> 0 ) holds cosec is_odd_on B proof let B be symmetrical Subset of REAL; ::_thesis: ( ( for x being real number st x in B holds sin . x <> 0 ) implies cosec is_odd_on B ) assume A1: for x being real number st x in B holds sin . x <> 0 ; ::_thesis: cosec is_odd_on B B c= dom cosec proof let x be real number ; :: according to MEMBERED:def_9 ::_thesis: ( not x in B or x in dom cosec ) assume A2: x in B ; ::_thesis: x in dom cosec 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 x in dom cosec by RFUNCT_1:def_2; ::_thesis: verum end; hence cosec is_odd_on B by Th83; ::_thesis: verum end;