theorem Th12: :: NOMIN_9:12

for V, A being set
for loc being b₁ -valued Function
for d1 being NonatomicND of V,A st Seg 10 c= dom loc & loc is_valid_wrt d1 holds
{(loc /. 1),(loc /. 2),(loc /. 3),(loc /. 4),(loc /. 5),(loc /. 6),(loc /. 7),(loc /. 8),(loc /. 9),(loc /. 10)} c= dom d1