theorem Th1: :: KOLMOG01:1

for f being Function
for X being set st X c= dom f & X <> {} holds
rng (f | X) <> {}