let X, x be set ; :: thesis: for F being Function of [:X,X:],X st x in [:X,X:] holds
F . x in X
let F be Function of [:X,X:],X; :: thesis: ( x in [:X,X:] implies F . x in X )
( X = {} implies [:X,X:] = {} ) ;
then A1: dom F = [:X,X:] by FUNCT_2:def 1;
assume x in [:X,X:] ; :: thesis: F . x in X
then ( rng F c= X & F . x in rng F ) by A1, FUNCT_1:def 3, RELAT_1:def 19;
hence F . x in X ; :: thesis: verum