let X be set ; :: thesis: ex f being Function st
( f is one-to-one & dom f = X & rng f = X )
take id X ; :: thesis: ( id X is one-to-one & dom (id X) = X & rng (id X) = X )
thus ( id X is one-to-one & dom (id X) = X & rng (id X) = X ) ; :: thesis: verum