theorem Th6: :: NUMERAL2:6

for F being XFinSequence
for X being set holds dom (SubXFinS (F,X)) = dom (Sgm0 (X /\ (dom F)))