let A be symmetrical Subset of COMPLEX; :: thesis: for F being PartFunc of REAL,REAL st F is_even_on A & ( for x being Real st x in A holds
F . x <> 0 ) holds
( A c= dom F & ( for x being Real st x in A holds
(F . x) / (F . (- x)) = 1 ) )
let F be PartFunc of REAL,REAL; :: thesis: ( F is_even_on A & ( for x being Real st x in A holds
F . x <> 0 ) implies ( A c= dom F & ( for x being Real st x in A holds
(F . x) / (F . (- x)) = 1 ) ) )
assume that
A1: F is_even_on A and
A2: for x being Real st x in A holds
F . x <> 0 ; :: thesis: ( A c= dom F & ( for x being Real st x in A holds
(F . x) / (F . (- x)) = 1 ) )
A3: A c= dom F by A1;
A4: F | A is even by A1;
for x being Real st x in A holds
(F . x) / (F . (- x)) = 1

proof

let x be Real; :: thesis: ( x in A implies (F . x) / (F . (- x)) = 1 )
assume A5: x in A ; :: thesis: (F . x) / (F . (- x)) = 1
then A6: x in dom (F | A) by A3, RELAT_1:62;
reconsider x = x as Element of REAL by XREAL_0:def 1;
A7: F . x = F /. x by A3, A5, PARTFUN1:def 6
.= (F | A) /. x by A3, A5, PARTFUN2:17
.= (F | A) . x by A6, PARTFUN1:def 6 ;
A8: - x in A by A5, Def1;
then A9: - x in dom (F | A) by A3, RELAT_1:62;
(F . x) / (F . (- x)) = (F /. x) / (F . (- x)) by A3, A5, PARTFUN1:def 6
.= (F /. x) / (F /. (- x)) by A3, A8, PARTFUN1:def 6
.= ((F | A) /. x) / (F /. (- x)) by A3, A5, PARTFUN2:17
.= ((F | A) /. x) / ((F | A) /. (- x)) by A3, A8, PARTFUN2:17
.= ((F | A) . x) / ((F | A) /. (- x)) by A6, PARTFUN1:def 6
.= ((F | A) . x) / ((F | A) . (- x)) by A9, PARTFUN1:def 6
.= ((F | A) . x) / ((F | A) . x) by A4, A6, A9, Def3
.= 1 by A2, A5, A7, XCMPLX_1:60 ;
hence (F . x) / (F . (- x)) = 1 ; :: thesis: verum

end;

hence ( A c= dom F & ( for x being Real st x in A holds
(F . x) / (F . (- x)) = 1 ) ) by A1; :: thesis: verum