theorem Th9: :: LATTICE2:9

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