now :: thesis: for i being object st i in I holds
(F * a) . i is Subgroup of G

let i be object ; :: thesis: ( i in I implies (F * a) . i is Subgroup of G )
assume A1: i in I ; :: thesis: (F * a) . i is Subgroup of G
then reconsider j = a . i as Element of J by FUNCT_2:5;
A2: F . j is Subgroup of G by GROUP_20:def 1;
dom a = I by FUNCT_2:def 1;
hence (F * a) . i is Subgroup of G by A1, A2, FUNCT_1:13; :: thesis: verum

end;

hence F * a is Subgroup-Family of I,G by GROUP_20:def 1; :: thesis: verum