theorem Th47: :: HILB10_7:47

for F being FinSequence-yielding FinSequence
for p being FinSequence holds
( p in doms F iff ( len p = len F & ( for i being Nat st i in dom p holds
p . i in dom (F . i) ) ) )