theorem Th17: :: FUNCT_1:17

for X being set
for f being Function holds
( f = id X iff ( dom f = X & ( for x being object st x in X holds
f . x = x ) ) )