deffunc H₁( object ) -> Subgroup of G = (1). G;
consider F being Function such that
A1: dom F = I and
A2: for i being object st i in I holds
F . i = H₁(i) from FUNCT_1:sch 3();
for i being object st i in I holds
F . i is Group by A2;
then reconsider F = F as Group-Family of I by A1, GROUP_19:2;
take F ; :: thesis: for i being object st i in I holds
F . i is Subgroup of G
thus for i being object st i in I holds
F . i is Subgroup of G by A2; :: thesis: verum