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 )

A1: dom F = dom (F - r) by VALUED_1:3;

assume A2: F is even ; :: thesis: F - r is even

for x being Real st x in dom (F - r) & - x in dom (F - r) holds

(F - r) . (- x) = (F - r) . x

hence F - r is even ; :: thesis: verum

F - r is even

let F be PartFunc of REAL,REAL; :: thesis: ( F is even implies F - r is even )

A1: dom F = dom (F - r) by VALUED_1:3;

assume A2: F is even ; :: thesis: F - r is even

for x being Real st x in dom (F - r) & - x in dom (F - r) holds

(F - r) . (- x) = (F - r) . x

proof

then
( F - r is with_symmetrical_domain & F - r is quasi_even )
by A2, A1;
let x be Real; :: thesis: ( x in dom (F - r) & - x in dom (F - r) implies (F - r) . (- x) = (F - r) . x )

assume that

A3: x in dom (F - r) and

A4: - x in dom (F - r) ; :: thesis: (F - r) . (- x) = (F - r) . x

A5: x in dom F by A3, VALUED_1:3;

- x in dom F by A4, VALUED_1:3;

then (F - r) . (- x) = (F . (- x)) - r by VALUED_1:3

.= (F . x) - r by A2, A1, A3, A4, Def3

.= (F - r) . x by A5, VALUED_1:3 ;

hence (F - r) . (- x) = (F - r) . x ; :: thesis: verum

end;assume that

A3: x in dom (F - r) and

A4: - x in dom (F - r) ; :: thesis: (F - r) . (- x) = (F - r) . x

A5: x in dom F by A3, VALUED_1:3;

- x in dom F by A4, VALUED_1:3;

then (F - r) . (- x) = (F . (- x)) - r by VALUED_1:3

.= (F . x) - r by A2, A1, A3, A4, Def3

.= (F - r) . x by A5, VALUED_1:3 ;

hence (F - r) . (- x) = (F - r) . x ; :: thesis: verum

hence F - r is even ; :: thesis: verum