theorem Th63: :: RFUNCT_3:63

for D being non empty set
for F being PartFunc of D,REAL
for X being set st dom (F | X) is finite holds
FinS (F,(dom (F | X))) = FinS (F,X)