theorem Th65: :: RFUNCT_3:65

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