:: deftheorem defines is_even_on FUNCT_8:def 5 :
for A being set
for X, Y being complex-membered set
for F being PartFunc of X,Y holds
( F is_even_on A iff ( A c= dom F & F | A is even ) );