let X, x be set ; 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; ( x in [:X,X:] implies F . x in X )
A1:
dom F = [:X,X:]
by PARTFUN1:def 2;
assume
x in [:X,X:]
; 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
; verum