let A be set ; :: thesis: id A in Funcs (A,A)
( dom (id A) = A & rng (id A) = A ) ;
hence id A in Funcs (A,A) by Def2; :: thesis: verum