set F = I --> ((1). G);
reconsider F = I --> ((1). G) as Group-Family of I ;
for i being object st i in I holds
F . i is Subgroup of G by FUNCOP_1:7;
then reconsider F = F as Subgroup-Family of I,G by GROUP_20:def 1;
take F ; :: thesis: ( F is componentwise_strict & F is normal )
thus ( F is componentwise_strict & F is normal ) by FUNCOP_1:7; :: thesis: verum