let r be Real; :: thesis: for A being symmetrical Subset of COMPLEX
for F being PartFunc of REAL ,REAL st F is_even_on A holds
r + F is_even_on A
let A be symmetrical Subset of COMPLEX ; :: thesis: for F being PartFunc of REAL ,REAL st F is_even_on A holds
r + F is_even_on A
let F be PartFunc of REAL ,REAL ; :: thesis: ( F is_even_on A implies r + F is_even_on A )
assume
F is_even_on A
; :: thesis: r + F is_even_on A
then A1:
( A c= dom F & F | A is even )
by Def5;
A2:
A c= dom (r + F)
by A1, VALUED_1:def 2;
A3:
dom ((r + F) | A) = A
by RELAT_1:91, A2;
for x being Real st x in dom ((r + F) | A) & - x in dom ((r + F) | A) holds
((r + F) | A) . (- x) = ((r + F) | A) . x
proof
let x be
Real;
:: thesis: ( x in dom ((r + F) | A) & - x in dom ((r + F) | A) implies ((r + F) | A) . (- x) = ((r + F) | A) . x )
assume A5:
(
x in dom ((r + F) | A) &
- x in dom ((r + F) | A) )
;
:: thesis: ((r + F) | A) . (- x) = ((r + F) | A) . x
then A6:
(
x in dom (F | A) &
- x in dom (F | A) )
by RELAT_1:91, A1, A3;
((r + F) | A) . (- x) =
((r + F) | A) /. (- x)
by PARTFUN1:def 8, A5
.=
(r + F) /. (- x)
by PARTFUN2:35, A2, A3, A5
.=
(r + F) . (- x)
by PARTFUN1:def 8, A2, A3, A5
.=
r + (F . (- x))
by VALUED_1:def 2, A2, A3, A5
.=
r + (F /. (- x))
by PARTFUN1:def 8, A3, A1, A5
.=
r + ((F | A) /. (- x))
by PARTFUN2:35, A1, A3, A5
.=
r + ((F | A) . (- x))
by PARTFUN1:def 8, A6
.=
r + ((F | A) . x)
by A1, Def3, A6
.=
r + ((F | A) /. x)
by PARTFUN1:def 8, A6
.=
r + (F /. x)
by PARTFUN2:35, A1, A3, A5
.=
r + (F . x)
by PARTFUN1:def 8, A1, A3, A5
.=
(r + F) . x
by VALUED_1:def 2, A2, A3, A5
.=
(r + F) /. x
by PARTFUN1:def 8, A2, A3, A5
.=
((r + F) | A) /. x
by PARTFUN2:35, A2, A3, A5
.=
((r + F) | A) . x
by PARTFUN1:def 8, A5
;
hence
((r + F) | A) . (- x) = ((r + F) | A) . x
;
:: thesis: verum
end;
then
( (r + F) | A is with_symmetrical_domain & (r + F) | A is quasi_even )
by Def3, A3, Def2;
hence
r + F is_even_on A
by A2, Def5; :: thesis: verum