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 f' = f as Function of {} ,{} by FUNCT_2:121;
for x, y being set holds
( [x,y] in f' iff ( x in {} & x = y ) ) ;
then f' = 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:37; :: thesis: verum