reconsider E = F * a as ManySortedSet of I ;
A1: dom a = I by FUNCT_2:def 1;
A2: dom E = I by PARTFUN1:def 2;
now :: thesis: for i being object st i in I holds
E . i is Group
let i be object ; :: thesis: ( i in I implies E . i is Group )
assume i in I ; :: thesis: E . i is Group
then reconsider i1 = i as Element of I ;
E . i1 = F . (a . i1) by A1, FUNCT_1:13;
hence E . i is Group ; :: thesis: verum
end;
hence a * F is Group-Family of I by A2, GROUP_19:2; :: thesis: verum