theorem Th7: :: ALGSPEC1:7

for X being set
for f being Function holds rng (X -indexing f) = (X \ (dom f)) \/ (f .: X)