let r be Real; :: thesis: for F being PartFunc of REAL,REAL st F is even holds
r + F is even
let F be PartFunc of REAL,REAL; :: thesis: ( F is even implies r + F is even )
A1: dom F = dom (r + F) by VALUED_1:def 2;
assume A2: F is even ; :: thesis: r + F is even
for x being Real st x in dom (r + F) & - x in dom (r + F) holds
(r + F) . (- x) = (r + F) . x

proof

let x be Real; :: thesis: ( x in dom (r + F) & - x in dom (r + F) implies (r + F) . (- x) = (r + F) . x )
assume that
A3: x in dom (r + F) and
A4: - x in dom (r + F) ; :: thesis: (r + F) . (- x) = (r + F) . x
(r + F) . (- x) = r + (F . (- x)) by A4, VALUED_1:def 2
.= r + (F . x) by A2, A1, A3, A4, Def3
.= (r + F) . x by A3, VALUED_1:def 2 ;
hence (r + F) . (- x) = (r + F) . x ; :: thesis: verum

end;

then ( r + F is with_symmetrical_domain & r + F is quasi_even ) by A2, A1;
hence r + F is even ; :: thesis: verum