theorem :: FUNCT_2:54

for X being set
for f, g being Function of X,X st g * f = f & rng f = X holds
g = id X