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
A7: (dom F) /\ (dom G) = dom (F + G) by VALUED_1:def 1;
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 1, A9
.= (F . x) + (G . (- x)) by A1, Def3, A8, A9
.= (F . x) + (G . x) by A2, Def3, A8, A9
.= (F + G) . x by VALUED_1:def 1, A9 ;
hence (F + G) . (- x) = (F + G) . x ; :: thesis: verum

end;

then ( F + G is with_symmetrical_domain & F + G is quasi_even ) by Def3, A3, A7, Def2;
hence F + G is even ; :: thesis: verum