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