:: deftheorem Def13 defines FinS RFUNCT_3:def 13 :
for D being non empty set
for F being PartFunc of D,REAL
for X being set st dom (F | X) is finite holds
for b₄ being non-increasing FinSequence of REAL holds
( b₄ = FinS (F,X) iff F | X,b₄ are_fiberwise_equipotent );