theorem Th45: :: HILB10_7:45

for F being FinSequence-yielding FinSequence holds
( not doms F is empty iff F is non-empty )