theorem :: FUNCT_8:5

for A being symmetrical Subset of COMPLEX
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 ) )