theorem :: FUNCT_8:53

for F, G being PartFunc of REAL,REAL st F is even & G is even & (dom F) /\ (dom G) is symmetrical holds
F /" G is even