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