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;
for i being object st i in I holds
F . i is Subgroup of G by A2;
then reconsider F = F as Subgroup-Family of I,G by Def1;
take F ; :: thesis: F is component-commutative
for i, j being Element of I
for gi, gj being Element of G st i <> j & gi in F . i & gj in F . j holds
gi * gj = gj * gi

proof

let i, j be Element of I; :: thesis: for gi, gj being Element of G st i <> j & gi in F . i & gj in F . j holds
gi * gj = gj * gi
let gi, gj be Element of G; :: thesis: ( i <> j & gi in F . i & gj in F . j implies gi * gj = gj * gi )
assume ( i <> j & gi in F . i & gj in F . j ) ; :: thesis: gi * gj = gj * gi
then ( gi in (1). G & gj in (1). G ) by A2;
then ( gi in {(1_ G)} & gj in {(1_ G)} ) by GROUP_2:def 7;
then ( gi = 1_ G & gj = 1_ G ) by TARSKI:def 1;
hence gi * gj = gj * gi ; :: thesis: verum

end;

hence F is component-commutative ; :: thesis: verum