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;
hence F (#) G is even ; :: thesis: verum