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 )
A1: rng g c= X ;
( dom f = X & dom g = X ) by Th51;
hence ( f * g = f & f is one-to-one implies g = id X ) by A1, FUNCT_1:28; :: thesis: verum