theorem :: RFUNCT_3:75

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