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