theorem Th20: :: CLOSURE2:20

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