theorem Th67: :: RFUNCT_3:67

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