let X be set ; :: thesis: for x being object holds Funcs (X,{x}) = {(X --> x)}
let x be object ; :: 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 object ; :: 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 :: thesis: ( ( for z being object holds not z in X ) implies f = X --> x )
set z = the Element of X;
A5: ( X <> {} implies the Element of X in X ) ;
assume for z being object holds not z in X ; :: thesis: f = X --> x
hence f = X --> x by A2, A5; :: thesis: verum
end;
now :: thesis: ( ex z being object st z in X implies f = X --> x )
given z being object such that A6: z in X ; :: thesis: f = X --> x
f . z in rng f by A2, A6, FUNCT_1:def 3;
then ( f . z = x & {(f . z)} c= rng f ) by A3, TARSKI:def 1;
then rng f = {x} by A3;
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 object ; :: 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 A7: 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 A7, FUNCT_2:def 2; :: thesis: verum