let A be set ; :: thesis: id A in Funcs A,A
( dom (id A) = A & rng (id A) = A ) by RELAT_1:71;
hence id A in Funcs A,A by FUNCT_2:def 2; :: thesis: verum