:: deftheorem defines --> FUNCT_4:def 7 :
for x, y, w, z, a, b, c, d being object holds (x,y,w,z) --> (a,b,c,d) = ((x,y) --> (a,b)) +* ((w,z) --> (c,d));