theorem Th9: :: ALGSPEC1:9

for X, x being set
for f being Function st x in X holds
( ( x in dom f implies (X -indexing f) . x = f . x ) & ( not x in dom f implies (X -indexing f) . x = x ) )