deffunc H₁( Group) -> Subgroup of $1 = (1). $1;
A1: for G being Group holds H₁(G) is strict Subgroup of G ;
thus ex S being componentwise_strict Subgroup-Family of F st
for i being Element of I holds S . i = H₁(F . i) from GROUP_23:sch 3(A1); :: thesis: verum