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
A7: (dom F) /\ (dom G) = dom (F (#) G) by VALUED_1:def 4;
then A8: ( dom (F (#) G) c= dom F & dom (F (#) G) c= dom G ) by 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 A9: ( 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:def 4, A9
.= (F . x) * (G . (- x)) by A1, Def3, A8, A9
.= (F . x) * (- (G . x)) by A2, Def6, A8, A9
.= - ((F . x) * (G . x))
.= - ((F (#) G) . x) by VALUED_1:def 4, A9 ;
hence (F (#) G) . (- x) = - ((F (#) G) . x) ; :: thesis: verum

end;

then ( F (#) G is with_symmetrical_domain & F (#) G is quasi_odd ) by Def6, A3, A7, Def2;
hence F (#) G is odd ; :: thesis: verum