take id X ; :: thesis: id X is bijective
thus ( id X is one-to-one & rng (id X) = X ) ; :: according to FUNCT_2:def 3,FUNCT_2:def 4 :: thesis: verum