let X be set ; :: thesis: for f, g being Function of X,X st g * f = f & rng f = X holds
g = id X
let f, g be Function of X,X; :: thesis: ( g * f = f & rng f = X implies g = id X )
( dom f = X & dom g = X ) by Th67;
hence ( g * f = f & rng f = X implies g = id X ) by FUNCT_1:44; :: thesis: verum