theorem Th51: :: HILB10_7:51

for f, g being FinSequence holds
( f in doms <*g*> iff ( len f = 1 & f . 1 in dom g ) )