let I, i be set ; :: thesis: for A being V33() ManySortedSet of I st i in I holds
A . i is finite
let A be V33() 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 2;
then A . i in rng A by FUNCT_1:3;
hence A . i is finite by FINSET_1:def 2; :: thesis: verum