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 x being set st x in rng E holds
x is non empty multMagma

let x be set ; :: thesis: ( x in rng E implies x is non empty multMagma )
assume x in rng E ; :: thesis: x is non empty multMagma
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: verum

end;

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