theorem :: FUNCT_2:124

for X being non empty set
for f being Function of X,X st ( for x being Element of X holds f . x = x ) holds
f = id X ;