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