:: deftheorem Def8 defines ./. GROUP_23:def 7 :
for I being non empty set
for F being Group-Family of I
for N being normal Subgroup-Family of F
for b₄ being Group-Family of I holds
( b₄ = F ./. N iff for i being Element of I holds b₄ . i = (F . i) ./. (N . i) );