theorem :: CLOSURE2:18

for i, I being set
for M being ManySortedSet of I
for f being Function
for SF being SubsetFamily of M st i in I & SF = {f} holds
|:SF:| . i = {(f . i)}