let A be symmetrical Subset of COMPLEX; :: thesis: 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; :: thesis: ( 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 ; :: thesis: 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; :: thesis: ( x in A implies F . x = 0 )
assume A5: x in A ; :: thesis: 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 ; :: thesis: verum