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

proof

let x be Real; :: thesis: ( x in dom (- F) & - x in dom (- F) implies (- F) . (- x) = (- F) . x )
assume A3: ( x in dom (- F) & - x in dom (- F) ) ; :: thesis: (- F) . (- x) = (- F) . x
(- F) . (- x) = - (F . (- x)) by VALUED_1:8
.= - (F . x) by A2, A1, A3, Def3
.= (- F) . x by VALUED_1:8 ;
hence (- F) . (- x) = (- F) . x ; :: thesis: verum

end;

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