hereby :: according to TARSKI:def 3,XBOOLE_0:def 10 :: thesis: {(id {})} c= Funcs ({},{})

let f be set ; :: thesis: ( f in Funcs ({},{}) implies f in {(id {})} )
assume f in Funcs ({},{}) ; :: thesis: f in {(id {})}
then reconsider f9 = f as Function of {},{} by FUNCT_2:66;
for x, y being set holds
( [x,y] in f9 iff ( x in {} & x = y ) ) ;
then f9 = id {} by RELAT_1:def 10;
hence f in {(id {})} by TARSKI:def 1; :: thesis: verum

end;

id {} in Funcs ({},{}) by Th2;
hence {(id {})} c= Funcs ({},{}) by ZFMISC_1:31; :: thesis: verum