deffunc H₁( Element of I) -> multMagma = (F . $1) ./. (N . $1);
thus ex Fam being Group-Family of I st
for i being Element of I holds Fam . i = H₁(i) from GROUP_23:sch 1(); :: thesis: verum