for X, Y being set
for f being PartFunc of X,Y
for x, y being object st x in X & y in Y holds
f +* (x .--> y) is PartFunc of X,Y