let X, x be set ; :: thesis: Funcs X,{x} = {(X --> x)}
thus Funcs X,{x} c= {(X --> x)} :: according to XBOOLE_0:def 10 :: thesis: {(X --> x)} c= Funcs X,{x}

proof

let y be set ; :: according to TARSKI:def 3 :: thesis: ( not y in Funcs X,{x} or y in {(X --> x)} )
assume y in Funcs X,{x} ; :: thesis: y in {(X --> x)}
then consider f being Function such that
A1: ( y = f & dom f = X & rng f c= {x} ) by FUNCT_2:def 2;

A2: now

given z being set such that A3: z in X ; :: thesis: f = X --> x
f . z in rng f by A1, A3, FUNCT_1:def 5;
then ( f . z = x & {(f . z)} c= rng f ) by A1, TARSKI:def 1, ZFMISC_1:37;
then rng f = {x} by A1, XBOOLE_0:def 10;
hence f = X --> x by A1, FUNCOP_1:15; :: thesis: verum

end;

now

assume A4: for z being set holds not z in X ; :: thesis: f = X --> x
consider z being Element of X;
( X <> {} implies z in X ) ;
then ( X = {} & dom ({} --> x) = {} & ( for y being set st y in {} holds
f . y = ({} --> x) . y ) ) by A4;
hence f = X --> x by A1; :: thesis: verum

end;

hence y in {(X --> x)} by A1, A2, TARSKI:def 1; :: thesis: verum

end;

let y be set ; :: according to TARSKI:def 3 :: thesis: ( not y in {(X --> x)} or y in Funcs X,{x} )
assume y in {(X --> x)} ; :: thesis: y in Funcs X,{x}
then ( y = X --> x & dom (X --> x) = X & rng (X --> x) c= {x} ) by FUNCOP_1:19, TARSKI:def 1;
hence y in Funcs X,{x} by FUNCT_2:def 2; :: thesis: verum