let F be PartFunc of REAL,REAL; :: thesis: ( F is even implies F " is even )
A1: dom F = dom (F ") by VALUED_1:def 7;
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 that
A3: x in dom (F ") and
A4: - x in dom (F ") ; :: thesis: (F ") . (- x) = (F ") . x
(F ") . (- x) = (F . (- x)) " by A4, VALUED_1:def 7
.= (F . x) " by A2, A1, A3, A4, Def3
.= (F ") . x by A3, VALUED_1:def 7 ;
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