theorem :: GROUP_6:19

for G being Group
for N being normal Subgroup of G
for T1, T2 being Element of (G ./. N) holds (@ T1) * (@ T2) = T1 * T2 by Def3;