take id X ; :: thesis: ( id X is one-to-one & id X is onto )
thus id X is one-to-one ; :: thesis: id X is onto
thus rng (id X) = X by RELAT_1:45; :: according to FUNCT_2:def 3 :: thesis: verum