theorem :: FUNCT_8:6

for A being symmetrical Subset of COMPLEX
for F being PartFunc of REAL,REAL st A c= dom F & ( for x being Real st x in A holds
(F . x) / (F . (- x)) = 1 ) holds
F is_even_on A