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:91, 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:91;
A13: x in dom (G | A) by A3, A8, A10, RELAT_1:91;
A14: - x in dom (F | A) by A5, A8, A11, RELAT_1:91;
A15: - x in dom (G | A) by A3, A8, A11, RELAT_1:91;
((F /" G) | A) . (- x) = ((F /" G) | A) /. (- x) by A11, PARTFUN1:def 8
.= (F /" G) /. (- x) by A6, A7, A8, A11, PARTFUN2:35
.= (F /" G) . (- x) by A6, A7, A8, A11, PARTFUN1:def 8
.= (F . (- x)) / (G . (- x)) by VALUED_1:17
.= (F /. (- x)) / (G . (- x)) by A5, A8, A11, PARTFUN1:def 8
.= (F /. (- x)) / (G /. (- x)) by A3, A8, A11, PARTFUN1:def 8
.= ((F | A) /. (- x)) / (G /. (- x)) by A5, A8, A11, PARTFUN2:35
.= ((F | A) /. (- x)) / ((G | A) /. (- x)) by A3, A8, A11, PARTFUN2:35
.= ((F | A) . (- x)) / ((G | A) /. (- x)) by A14, PARTFUN1:def 8
.= ((F | A) . (- x)) / ((G | A) . (- x)) by A15, PARTFUN1:def 8
.= (- ((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:192
.= ((F | A) /. x) / ((G | A) . x) by A12, PARTFUN1:def 8
.= ((F | A) /. x) / ((G | A) /. x) by A13, PARTFUN1:def 8
.= (F /. x) / ((G | A) /. x) by A5, A8, A10, PARTFUN2:35
.= (F /. x) / (G /. x) by A3, A8, A10, PARTFUN2:35
.= (F . x) / (G /. x) by A5, A8, A10, PARTFUN1:def 8
.= (F . x) / (G . x) by A3, A8, A10, PARTFUN1:def 8
.= (F /" G) . x by VALUED_1:17
.= (F /" G) /. x by A6, A7, A8, A10, PARTFUN1:def 8
.= ((F /" G) | A) /. x by A6, A7, A8, A10, PARTFUN2:35
.= ((F /" G) | A) . x by A10, PARTFUN1:def 8 ;
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