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 g = X by Th51;
hence ( g * f = f & rng f = X implies g = id X ) by FUNCT_1:23; :: thesis: verum