let A be ManySortedSet of I; :: thesis: ( A is empty-yielding implies A is finite-yielding )
assume A1: A is empty-yielding ; :: thesis: A is finite-yielding
let i be object ; :: according to FINSET_1:def 5 :: thesis: ( not i in I or A . i is finite )
assume i in I ; :: thesis: A . i is finite
reconsider B = A . i as empty set by A1;
B is finite ;
hence A . i is finite ; :: thesis: verum