theorem Th70: :: RFUNCT_3:70

for D being non empty set
for F being PartFunc of D,REAL
for X being set
for d being Element of D st dom (F | X) is finite & d in dom (F | X) & (FinS (F,X)) . (len (FinS (F,X))) = F . d holds
FinS (F,X) = (FinS (F,(X \ {d}))) ^ <*(F . d)*>