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

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

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

then
( r + F is with_symmetrical_domain & r + F is quasi_even )
by A2, A1;
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;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

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