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