theorem :: FUNCT_8:15

for r being Real
for A being symmetrical Subset of COMPLEX
for F being PartFunc of REAL,REAL st F is_even_on A holds
r (#) F is_even_on A