consider J being finite Subset of I, f being ManySortedSet of J such that
A1: ( J = support (a,F) & a = (1_ (product F)) +* f & ( for j being object st j in I \ J holds
a . j = 1_ (F . j) ) & ( for j being object st j in J holds
a . j = f . j ) ) by Th7;
thus support (a,F) is finite by A1; :: thesis: verum