:: deftheorem defines --> FUNCT_4:def 4 :
for x, y, a, b being object holds (x,y) --> (a,b) = (x .--> a) +* (y .--> b);