for D being non empty set
for F being PartFunc of D,REAL
for r being Real
for X being set
for Z being finite set st Z = dom (F | X) holds
FinS ((F - r),X) = (FinS (F,X)) - ((card Z) |-> r)