:: deftheorem defines even FUNCT_8:def 4 :
for X, Y being complex-membered set
for F being PartFunc of X,Y holds
( F is even iff ( F is with_symmetrical_domain & F is quasi_even ) );