theorem Th56: :: PROB_3:56

for X being set
for Si being SigmaField of X
for FSi being FinSequence of Si ex ASeq being SetSequence of Si st
( ( for k being Nat st k in dom FSi holds
ASeq . k = FSi . k ) & ( for k being Nat st not k in dom FSi holds
ASeq . k = {} ) )