let A be symmetrical Subset of COMPLEX; for F being PartFunc of REAL,REAL st F is_even_on A & F is_odd_on A holds
for x being Real st x in A holds
F . x = 0
let F be PartFunc of REAL,REAL; ( F is_even_on A & F is_odd_on A implies for x being Real st x in A holds
F . x = 0 )
assume that
A1:
F is_even_on A
and
A2:
F is_odd_on A
; for x being Real st x in A holds
F . x = 0
A3:
F | A is even
by A1;
A4:
F | A is odd
by A2;
let x be Real; ( x in A implies F . x = 0 )
assume A5:
x in A
; F . x = 0
A6:
A c= dom F
by A1;
then A7:
x in dom (F | A)
by A5, RELAT_1:62;
- x in A
by A5, Def1;
then A8:
- x in dom (F | A)
by A6, RELAT_1:62;
reconsider x = x as Element of REAL by XREAL_0:def 1;
F . x =
F /. x
by A6, A5, PARTFUN1:def 6
.=
(F | A) /. x
by A6, A5, PARTFUN2:17
.=
(F | A) . x
by A7, PARTFUN1:def 6
.=
(F | A) . (- x)
by A3, A7, A8, Def3
.=
- ((F | A) . x)
by A4, A7, A8, Def6
.=
- ((F | A) /. x)
by A7, PARTFUN1:def 6
.=
- (F /. x)
by A6, A5, PARTFUN2:17
.=
- (F . x)
by A6, A5, PARTFUN1:def 6
;
hence
F . x = 0
; verum