let I, i be set ; :: thesis: for A being V30() ManySortedSet of I st i in I holds
A . i is finite
let A be V30() ManySortedSet of I; :: thesis: ( i in I implies A . i is finite )
assume i in I ; :: thesis: A . i is finite
then i in dom A by PARTFUN1:def 4;
then A . i in rng A by FUNCT_1:12;
hence A . i is finite by FINSET_1:def 2; :: thesis: verum