theorem Th1: :: REALSET1:1

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