theorem Th76: :: RFUNCT_3:76

for D being non empty set
for F being PartFunc of D,REAL
for X, Y being set st dom (F | (X \/ Y)) is finite & X misses Y holds
FinS (F,(X \/ Y)),(FinS (F,X)) ^ (FinS (F,Y)) are_fiberwise_equipotent