for X, x being set
for F being Function of [:X,X:],X st x in [:X,X:] holds
F . x in X