theorem :: FUNCT_8:8

for A being symmetrical Subset of COMPLEX
for F being PartFunc of REAL,REAL st F is_even_on A holds
for x being Real st x in A holds
F . x = F . |.x.|