let A be symmetrical Subset of COMPLEX ; :: thesis: for F, G being PartFunc of REAL ,REAL st F is_even_on A & G is_even_on A holds
F + G is_even_on A
let F, G be PartFunc of REAL ,REAL ; :: thesis: ( F is_even_on A & G is_even_on A implies F + G is_even_on A )
assume that
A1: F is_even_on A and
A2: G is_even_on A ; :: thesis: F + G is_even_on A
B1: ( A c= dom F & F | A is even ) by Def5, A1;
B2: ( A c= dom G & G | A is even ) by Def5, A2;
B3: A c= (dom F) /\ (dom G) by XBOOLE_1:19, B1, B2;
A7: (dom F) /\ (dom G) = dom (F + G) by VALUED_1:def 1;
A8: dom ((F + G) | A) = A by RELAT_1:91, A7, XBOOLE_1:19, B1, B2;
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 A9: ( x in dom ((F + G) | A) & - x in dom ((F + G) | A) ) ; :: thesis: ((F + G) | A) . (- x) = ((F + G) | A) . x
then A10: ( x in dom (F | A) & - x in dom (F | A) & x in dom (G | A) & - x in dom (G | A) ) by RELAT_1:91, B1, B2, A8;
((F + G) | A) . (- x) = ((F + G) | A) /. (- x) by PARTFUN1:def 8, A9
.= (F + G) /. (- x) by PARTFUN2:35, A9, A8, B3, A7
.= (F + G) . (- x) by PARTFUN1:def 8, A9, A8, B3, A7
.= (F . (- x)) + (G . (- x)) by B3, VALUED_1:def 1, A7, A9, A8
.= (F /. (- x)) + (G . (- x)) by PARTFUN1:def 8, B1, A9, A8
.= (F /. (- x)) + (G /. (- x)) by PARTFUN1:def 8, B2, A9, A8
.= ((F | A) /. (- x)) + (G /. (- x)) by PARTFUN2:35, A9, B1, A8
.= ((F | A) /. (- x)) + ((G | A) /. (- x)) by PARTFUN2:35, A9, B2, A8
.= ((F | A) . (- x)) + ((G | A) /. (- x)) by PARTFUN1:def 8, A10
.= ((F | A) . (- x)) + ((G | A) . (- x)) by PARTFUN1:def 8, A10
.= ((F | A) . x) + ((G | A) . (- x)) by B1, Def3, A10
.= ((F | A) . x) + ((G | A) . x) by B2, Def3, A10
.= ((F | A) /. x) + ((G | A) . x) by PARTFUN1:def 8, A10
.= ((F | A) /. x) + ((G | A) /. x) by PARTFUN1:def 8, A10
.= (F /. x) + ((G | A) /. x) by PARTFUN2:35, B1, A9, A8
.= (F /. x) + (G /. x) by PARTFUN2:35, B2, A9, A8
.= (F . x) + (G /. x) by PARTFUN1:def 8, B1, A9, A8
.= (F . x) + (G . x) by PARTFUN1:def 8, B2, A9, A8
.= (F + G) . x by B3, VALUED_1:def 1, A7, A9, A8
.= (F + G) /. x by PARTFUN1:def 8, A9, A8, B3, A7
.= ((F + G) | A) /. x by PARTFUN2:35, A9, A8, B3, A7
.= ((F + G) | A) . x by PARTFUN1:def 8, A9 ;
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 Def3, A8, Def2;
hence F + G is_even_on A by A7, B3, Def5; :: thesis: verum