theorem :: RELAT_1:168

for X, Y being set
for x being object st x in X holds
Im ([:X,Y:],x) = Y