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

proof

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

end;

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