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

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