deffunc H_{1}( 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_{1}(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

consider F being Function such that

A1: dom F = I and

A2: for i being object st i in I holds

F . i = H

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