reconsider f = id X as Function of X,X ;
rng f = X ;
hence id X is onto by FUNCT_2:def 3; :: thesis: verum