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
B2: ( A c= dom F & F | A is even ) by Def5, A1;
B3: ( A c= dom F & F | A is odd ) by Def8, A2;
let x be Real; :: thesis: ( x in A implies F . x = 0 )
assume A3: x in A ; :: thesis: F . x = 0
then ( x in A & - x in A ) by Def1;
then A5: ( x in dom (F | A) & - x in dom (F | A) ) by RELAT_1:91, B2;
F . x = F /. x by B2, A3, PARTFUN1:def 8
.= (F | A) /. x by PARTFUN2:35, B2, A3
.= (F | A) . x by PARTFUN1:def 8, A5
.= (F | A) . (- x) by B2, Def3, A5
.= - ((F | A) . x) by B3, Def6, A5
.= - ((F | A) /. x) by PARTFUN1:def 8, A5
.= - (F /. x) by PARTFUN2:35, B2, A3
.= - (F . x) by B2, A3, PARTFUN1:def 8 ;
hence F . x = 0 ; :: thesis: verum