theorem :: FUNCT_8:28

for A being symmetrical Subset of COMPLEX
for F being PartFunc of REAL,REAL st F is_odd_on A holds
F ^2 is_even_on A by Th22;