deffunc H₁( Group) -> Subgroup of I = (1). I;
A1: for G being Group holds H₁(G) is Subgroup of G ;
consider S being Subgroup-Family of F such that
A2: for i being Element of I holds S . i = H₁(F . i) from GROUP_23:sch 2(A1);
take S ; :: thesis: S is componentwise_strict
for i being Element of I holds S . i is strict Subgroup of F . i

proof

let i be Element of I; :: thesis: S . i is strict Subgroup of F . i
S . i = (1). (F . i) by A2;
hence S . i is strict Subgroup of F . i ; :: thesis: verum

end;

hence S is componentwise_strict ; :: thesis: verum