hereby :: according to TARSKI:def 3,XBOOLE_0:def 10 :: thesis: {(id {})} c= Funcs ({},{})
let f be object ; :: thesis: ( f in Funcs ({},{}) implies f in {(id {})} )
assume f in Funcs ({},{}) ; :: thesis: f in {(id {})}
then reconsider f9 = f as Function of {},{} by Th65;
f9 = id {} ;
hence f in {(id {})} by TARSKI:def 1; :: thesis: verum
end;
thus {(id {})} c= Funcs ({},{}) by Th125, ZFMISC_1:31; :: thesis: verum