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

( 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