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 and
A2: dom f = X and
A3: rng f c= {x} by FUNCT_2:def 2;

A4: now

set z = the Element of X;
A5: ( X <> {} implies the Element of X in X ) ;
A6: dom ({} --> x) = {} ;
assume for z being set holds not z in X ; :: thesis: f = X --> x
hence f = X --> x by A2, A5, A6; :: thesis: verum

end;

now

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

end;

hence y in {(X --> x)} by A1, A4, 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 A8: y = X --> x by TARSKI:def 1;
( dom (X --> x) = X & rng (X --> x) c= {x} ) by FUNCOP_1:13;
hence y in Funcs (X,{x}) by A8, FUNCT_2:def 2; :: thesis: verum