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 )
A1: ( dom F = [:X,X:] & rng F c= X )

proof

( X = {} implies [:X,X:] = {} ) ;
hence ( dom F = [:X,X:] & rng F c= X ) by FUNCT_2:def 1, RELAT_1:def 19; :: thesis: verum

end;

assume x in [:X,X:] ; :: thesis: F . x in X
then F . x in rng F by A1, FUNCT_1:def 5;
hence F . x in X by A1; :: thesis: verum