:: deftheorem Def8 defines IFEQ FUNCOP_1:def 8 :
for x, y, a, b being object holds
( ( x = y implies IFEQ (x,y,a,b) = a ) & ( not x = y implies IFEQ (x,y,a,b) = b ) );