theorem Th1: :: LATTICE2:1

for A being set
for C being non empty set
for B being Subset of A
for g being Function of A,C holds dom (g | B) = B