for D being non empty set
for F being PartFunc of D,REAL
for X being set st dom (F | X) is finite & ( for d being Element of D st d in dom (F | X) holds
F . d >= 0 ) holds
FinS ((max+ F),X) = FinS (F,X)