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:

let x be set ; :: thesis:
assume x in rng E ; :: thesis:
then consider i being object such that
A3: i in I and
A4: E . i = x by A2, FUNCT_1:def 3;
reconsider j = a . i as Element of J by A3, FUNCT_2:5;
F . j is non empty multMagma ;
hence x is non empty multMagma by A1, A3, A4, FUNCT_1:13; :: thesis:

end;

hence a * F is multMagma-Family of I by GROUP_7:def 1; :: thesis: