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;
hence F /" G is odd ; :: thesis: verum